let X be finite set ; card { [x,y] where x, y is Element of union X : {x,y} in PairsOf X } = 2 * (card (PairsOf X))
set Y = union X;
set B = { [x,y] where x, y is Element of union X : {x,y} in PairsOf X } ;
set A = { {x,[y,(union X)]} where x, y is Element of union X : {x,y} in PairsOf X } ;
per cases
( { [x,y] where x, y is Element of union X : {x,y} in PairsOf X } is empty or not { [x,y] where x, y is Element of union X : {x,y} in PairsOf X } is empty )
;
suppose A1:
{ [x,y] where x, y is Element of union X : {x,y} in PairsOf X } is
empty
;
card { [x,y] where x, y is Element of union X : {x,y} in PairsOf X } = 2 * (card (PairsOf X))now { {x,[y,(union X)]} where x, y is Element of union X : {x,y} in PairsOf X } is empty assume
not
{ {x,[y,(union X)]} where x, y is Element of union X : {x,y} in PairsOf X } is
empty
;
contradictionthen consider a being
object such that A2:
a in { {x,[y,(union X)]} where x, y is Element of union X : {x,y} in PairsOf X }
;
consider x,
y being
Element of
union X such that
a = {x,[y,(union X)]}
and A3:
{x,y} in PairsOf X
by A2;
[x,y] in { [x,y] where x, y is Element of union X : {x,y} in PairsOf X }
by A3;
hence
contradiction
by A1;
verum end; hence
card { [x,y] where x, y is Element of union X : {x,y} in PairsOf X } = 2
* (card (PairsOf X))
by A1, Th15;
verum end; suppose A4:
not
{ [x,y] where x, y is Element of union X : {x,y} in PairsOf X } is
empty
;
card { [x,y] where x, y is Element of union X : {x,y} in PairsOf X } = 2 * (card (PairsOf X))then consider b being
object such that A5:
b in { [x,y] where x, y is Element of union X : {x,y} in PairsOf X }
;
consider x,
y being
Element of
union X such that
b = [x,y]
and A6:
{x,y} in PairsOf X
by A5;
A7:
x in {x,y}
by TARSKI:def 2;
A8:
union X <> {}
by A6, A7, TARSKI:def 4;
defpred S1[
object ,
object ]
means for
a,
b being
Element of
union X st
a in union X &
b in union X & $1
= {a,[b,(union X)]} holds
$2
= [a,b];
A9:
for
c being
object st
c in { {x,[y,(union X)]} where x, y is Element of union X : {x,y} in PairsOf X } holds
ex
d being
object st
(
d in { [x,y] where x, y is Element of union X : {x,y} in PairsOf X } &
S1[
c,
d] )
proof
let c be
object ;
( c in { {x,[y,(union X)]} where x, y is Element of union X : {x,y} in PairsOf X } implies ex d being object st
( d in { [x,y] where x, y is Element of union X : {x,y} in PairsOf X } & S1[c,d] ) )
assume
c in { {x,[y,(union X)]} where x, y is Element of union X : {x,y} in PairsOf X }
;
ex d being object st
( d in { [x,y] where x, y is Element of union X : {x,y} in PairsOf X } & S1[c,d] )
then consider x,
y being
Element of
union X such that A10:
c = {x,[y,(union X)]}
and A11:
{x,y} in PairsOf X
;
take d =
[x,y];
( d in { [x,y] where x, y is Element of union X : {x,y} in PairsOf X } & S1[c,d] )
thus
d in { [x,y] where x, y is Element of union X : {x,y} in PairsOf X }
by A11;
S1[c,d]
thus
S1[
c,
d]
verumproof
let a,
b be
Element of
union X;
( a in union X & b in union X & c = {a,[b,(union X)]} implies d = [a,b] )
assume A12:
(
a in union X &
b in union X )
;
( not c = {a,[b,(union X)]} or d = [a,b] )
assume
c = {a,[b,(union X)]}
;
d = [a,b]
then
(
a = x &
b = y )
by A10, A12, Th4;
hence
d = [a,b]
;
verum
end;
end; consider f being
Function of
{ {x,[y,(union X)]} where x, y is Element of union X : {x,y} in PairsOf X } ,
{ [x,y] where x, y is Element of union X : {x,y} in PairsOf X } such that A13:
for
c being
object st
c in { {x,[y,(union X)]} where x, y is Element of union X : {x,y} in PairsOf X } holds
S1[
c,
f . c]
from FUNCT_2:sch 1(A9);
A14:
dom f = { {x,[y,(union X)]} where x, y is Element of union X : {x,y} in PairsOf X }
by A4, FUNCT_2:def 1;
A15:
f is
one-to-one
proof
let c1,
c2 be
object ;
FUNCT_1:def 4 ( not c1 in dom f or not c2 in dom f or not f . c1 = f . c2 or c1 = c2 )
assume that A16:
c1 in dom f
and A17:
c2 in dom f
and A18:
f . c1 = f . c2
;
c1 = c2
consider x1,
y1 being
Element of
union X such that A19:
c1 = {x1,[y1,(union X)]}
and
{x1,y1} in PairsOf X
by A16, A14;
consider x2,
y2 being
Element of
union X such that A20:
c2 = {x2,[y2,(union X)]}
and
{x2,y2} in PairsOf X
by A17, A14;
A21:
f . c1 = [x1,y1]
by A13, A16, A14, A8, A19;
A22:
f . c2 = [x2,y2]
by A13, A17, A14, A8, A20;
(
x1 = x2 &
y1 = y2 )
by A18, A21, A22, XTUPLE_0:1;
hence
c1 = c2
by A19, A20;
verum
end; A23:
rng f = { [x,y] where x, y is Element of union X : {x,y} in PairsOf X }
proof
thus
rng f c= { [x,y] where x, y is Element of union X : {x,y} in PairsOf X }
XBOOLE_0:def 10 { [x,y] where x, y is Element of union X : {x,y} in PairsOf X } c= rng fproof
let b be
object ;
TARSKI:def 3 ( not b in rng f or b in { [x,y] where x, y is Element of union X : {x,y} in PairsOf X } )
assume
b in rng f
;
b in { [x,y] where x, y is Element of union X : {x,y} in PairsOf X }
then consider a being
object such that A24:
a in dom f
and A25:
b = f . a
by FUNCT_1:def 3;
consider x,
y being
Element of
union X such that A26:
a = {x,[y,(union X)]}
and A27:
{x,y} in PairsOf X
by A24, A14;
A28:
b = [x,y]
by A25, A24, A13, A14, A8, A26;
thus
b in { [x,y] where x, y is Element of union X : {x,y} in PairsOf X }
by A28, A27;
verum
end;
thus
{ [x,y] where x, y is Element of union X : {x,y} in PairsOf X } c= rng f
verumproof
let b be
object ;
TARSKI:def 3 ( not b in { [x,y] where x, y is Element of union X : {x,y} in PairsOf X } or b in rng f )
assume A29:
b in { [x,y] where x, y is Element of union X : {x,y} in PairsOf X }
;
b in rng f
consider x,
y being
Element of
union X such that A30:
b = [x,y]
and A31:
{x,y} in PairsOf X
by A29;
set a =
{x,[y,(union X)]};
A32:
{x,[y,(union X)]} in { {x,[y,(union X)]} where x, y is Element of union X : {x,y} in PairsOf X }
by A31;
A33:
f . {x,[y,(union X)]} = b
by A32, A13, A30, A8;
thus
b in rng f
by A32, A33, A14, FUNCT_1:3;
verum
end;
end; A34:
f is
onto
by A23, FUNCT_2:def 3;
thus card { [x,y] where x, y is Element of union X : {x,y} in PairsOf X } =
card { {x,[y,(union X)]} where x, y is Element of union X : {x,y} in PairsOf X }
by A15, A34, A4, EULER_1:11
.=
2
* (card (PairsOf X))
by Th15
;
verum end; end;