REAL , real-anti-diagonal are_equipotent

proof

hence
card real-anti-diagonal = continuum
by TOPGEN_3:def 4, CARD_1:5; :: thesis: verum
defpred S_{1}[ 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_{1}[r,a] )

A2: for r being object st r in REAL holds

S_{1}[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 <> {}

thus rng Z = real-anti-diagonal :: thesis: verum

end;( $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

proof

consider Z being Function of REAL,real-anti-diagonal such that
let r be object ; :: thesis: ( r in REAL implies ex a being object st

( a in real-anti-diagonal & S_{1}[r,a] ) )

assume r in REAL ; :: thesis: ex a being object st

( a in real-anti-diagonal & S_{1}[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_{1}[r,a] )
; :: thesis: verum

end;( a in real-anti-diagonal & S

assume r in REAL ; :: thesis: ex a being object st

( a in real-anti-diagonal & S

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

A2: for r being object st r in REAL holds

S

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

thus
Z is one-to-one
:: thesis: ( dom Z = REAL & rng Z = real-anti-diagonal )
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;set z = [x,y];

[x,y] in real-anti-diagonal ;

hence real-anti-diagonal <> {} ; :: thesis: verum

proof

thus
dom Z = REAL
by A3, FUNCT_2:def 1; :: thesis: rng Z = real-anti-diagonal
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;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

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

end;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;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