REAL , real-anti-diagonal are_equipotent

proof

defpred S₁[ object , object ] means ex x being Real st
( $1 = x & $2 = [x,(- x)] );
A1: for r being object st r in REAL holds
ex a being object st
( a in real-anti-diagonal & S₁[r,a] )

proof

let r be object ; :: thesis: ( r in REAL implies ex a being object st
( a in real-anti-diagonal & S₁[r,a] ) )
assume r in REAL ; :: thesis: ex a being object st
( a in real-anti-diagonal & S₁[r,a] )
then reconsider r = r as Real ;
set a = [r,(- r)];
[r,(- r)] in real-anti-diagonal ;
hence ex a being object st
( a in real-anti-diagonal & S₁[r,a] ) ; :: thesis: verum

end;

consider Z being Function of REAL,real-anti-diagonal such that
A2: for r being object st r in REAL holds
S₁[r,Z . r] from FUNCT_2:sch 1(A1);
take Z ; :: according to WELLORD2:def 4 :: thesis: ( Z is one-to-one & dom Z = REAL & rng Z = real-anti-diagonal )
A3: real-anti-diagonal <> {}

proof

reconsider x = 1, y = - 1 as Element of REAL by XREAL_0:def 1;
set z = [x,y];
[x,y] in real-anti-diagonal ;
hence real-anti-diagonal <> {} ; :: thesis: verum

end;

thus Z is one-to-one :: thesis: ( dom Z = REAL & rng Z = real-anti-diagonal )

proof

let r1, r2 be object ; :: according to FUNCT_1:def 4 :: thesis: ( not r1 in dom Z or not r2 in dom Z or not Z . r1 = Z . r2 or r1 = r2 )
assume that
A4: ( r1 in dom Z & r2 in dom Z ) and
A5: Z . r1 = Z . r2 ; :: thesis: r1 = r2
consider x1 being Real such that
A6: ( r1 = x1 & Z . r1 = [x1,(- x1)] ) by A2, A4;
consider x2 being Real such that
A7: ( r2 = x2 & Z . r2 = [x2,(- x2)] ) by A2, A4;
thus r1 = r2 by A6, A7, A5, XTUPLE_0:1; :: thesis: verum

end;

thus dom Z = REAL by A3, FUNCT_2:def 1; :: thesis: rng Z = real-anti-diagonal
thus rng Z = real-anti-diagonal :: thesis: verum

proof

thus rng Z c= real-anti-diagonal ; :: according to XBOOLE_0:def 10 :: thesis: real-anti-diagonal c= rng Z
thus real-anti-diagonal c= rng Z :: thesis: verum

proof

let z be object ; :: according to TARSKI:def 3 :: thesis: ( not z in real-anti-diagonal or z in rng Z )
assume z in real-anti-diagonal ; :: thesis: z in rng Z
then consider x, y being Real such that
A8: z = [x,y] and
A9: y = - x ;
consider x1 being Real such that
A10: ( x = x1 & Z . x = [x1,(- x1)] ) by A2, XREAL_0:def 1;
thus z in rng Z by A10, A8, A9, FUNCT_2:4, A3, XREAL_0:def 1; :: thesis: verum

end;

end;

end;

hence card real-anti-diagonal = continuum by TOPGEN_3:def 4, CARD_1:5; :: thesis: verum