let M be Cardinal; :: thesis: for X being set st ( for Z being set st Z in X holds
card Z in M ) & X is c=-linear holds
card (union X) c= M
let X be set ; :: thesis: ( ( for Z being set st Z in X holds
card Z in M ) & X is c=-linear implies card (union X) c= M )
assume that
A1: for Z being set st Z in X holds
card Z in M and
A2: X is c=-linear ; :: thesis: card (union X) c= M
consider XX being set such that
A3: ( XX c= X & union XX = union X ) and
A4: for Z being set st Z c= XX & Z <> {} holds
ex Z1 being set st
( Z1 in Z & ( for Z2 being set st Z2 in Z holds
Z1 c= Z2 ) ) by A2, Th61;
A5: now
let Z1, Z2 be set ; :: thesis: ( Z1 in XX & Z2 in XX & not Z1 c= Z2 implies Z2 c= Z1 )
assume ( Z1 in XX & Z2 in XX ) ; :: thesis: ( Z1 c= Z2 or Z2 c= Z1 )
then Z1,Z2 are_c=-comparable by A2, A3, ORDINAL1:def 9;
hence ( Z1 c= Z2 or Z2 c= Z1 ) by XBOOLE_0:def 9; :: thesis: verum
end;
consider R being Relation such that
A6: R well_orders union X by WELLORD2:26;
A7: ( R is_reflexive_in union X & R is_transitive_in union X & R is_antisymmetric_in union X & R is_connected_in union X & R is_well_founded_in union X ) by A6, WELLORD1:def 5;
defpred S2[ set , set ] means ( ex Z1 being set st
( Z1 in XX & $1 in Z1 & not $2 in Z1 ) or ( ( for Z1 being set st Z1 in XX holds
( $1 in Z1 iff $2 in Z1 ) ) & [$1,$2] in R ) );
consider Q being Relation such that
A8: for x, y being set holds
( [x,y] in Q iff ( x in union X & y in union X & S2[x,y] ) ) from RELAT_1:sch 1();
 A9: field Q = union X
proof
thus field Q c= union X :: according to XBOOLE_0:def 10 :: thesis: union X c= field Q
proof
let x be set ; :: according to TARSKI:def 3 :: thesis: ( not x in field Q or x in union X )
assume x in field Q ; :: thesis: x in union X
then ex y being set st
( [x,y] in Q or [y,x] in Q ) by Lm2;
hence x in union X by A8; :: thesis: verum
end;
let x be set ; :: according to TARSKI:def 3 :: thesis: ( not x in union X or x in field Q )
assume A10: x in union X ; :: thesis: x in field Q
then ( [x,x] in R & ( for Z1 being set st Z1 in XX holds
( x in Z1 iff x in Z1 ) ) ) by A7, RELAT_2:def 1;
then [x,x] in Q by A8, A10;
hence x in field Q by RELAT_1:30; :: thesis: verum
end;
Q is well-ordering
proof
thus Q is reflexive :: according to WELLORD1:def 4 :: thesis: ( Q is transitive & Q is antisymmetric & Q is connected & Q is well_founded )
proof
let x be set ; :: according to RELAT_2:def 1,RELAT_2:def 9 :: thesis: ( not x in field Q or [x,x] in Q )
assume A11: x in field Q ; :: thesis: [x,x] in Q
then ( [x,x] in R & ( for Z1 being set st Z1 in XX holds
( x in Z1 iff x in Z1 ) ) ) by A7, A9, RELAT_2:def 1;
hence [x,x] in Q by A8, A9, A11; :: thesis: verum
end;
thus Q is transitive :: thesis: ( Q is antisymmetric & Q is connected & Q is well_founded )
proof
let x be set ; :: according to RELAT_2:def 8,RELAT_2:def 16 :: thesis: for b1, b2 being set holds
( not x in field Q or not b1 in field Q or not b2 in field Q or not [x,b1] in Q or not [b1,b2] in Q or [x,b2] in Q )
let y, z be set ; :: thesis: ( not x in field Q or not y in field Q or not z in field Q or not [x,y] in Q or not [y,z] in Q or [x,z] in Q )
assume A12: ( x in field Q & y in field Q & z in field Q & [x,y] in Q & [y,z] in Q ) ; :: thesis: [x,z] in Q
A13: now
given Z1 being set such that A14: ( Z1 in XX & x in Z1 & not y in Z1 ) ; :: thesis: ( ex Z2 being set st
( Z2 in XX & y in Z2 & not z in Z2 ) implies [x,z] in Q )
given Z2 being set such that A15: ( Z2 in XX & y in Z2 & not z in Z2 ) ; :: thesis: [x,z] in Q
( Z1 c= Z2 or Z2 c= Z1 ) by A5, A14, A15;
hence [x,z] in Q by A8, A9, A12, A14, A15; :: thesis: verum
end;
A16: now
given Z1 being set such that A17: ( Z1 in XX & x in Z1 & not y in Z1 ) ; :: thesis: ( ( for Z1 being set st Z1 in XX holds
( y in Z1 iff z in Z1 ) ) & [y,z] in R implies [x,z] in Q )
assume ( ( for Z1 being set st Z1 in XX holds
( y in Z1 iff z in Z1 ) ) & [y,z] in R ) ; :: thesis: [x,z] in Q
then not z in Z1 by A17;
hence [x,z] in Q by A8, A9, A12, A17; :: thesis: verum
end;
A18: now
given Z1 being set such that A19: ( Z1 in XX & y in Z1 & not z in Z1 ) ; :: thesis: ( ( for Z1 being set st Z1 in XX holds
( x in Z1 iff y in Z1 ) ) & [x,y] in R implies [x,z] in Q )
assume ( ( for Z1 being set st Z1 in XX holds
( x in Z1 iff y in Z1 ) ) & [x,y] in R ) ; :: thesis: [x,z] in Q
then x in Z1 by A19;
hence [x,z] in Q by A8, A9, A12, A19; :: thesis: verum
end;
now
assume A20: ( ( for Z1 being set st Z1 in XX holds
( x in Z1 iff y in Z1 ) ) & [x,y] in R & ( for Z1 being set st Z1 in XX holds
( y in Z1 iff z in Z1 ) ) & [y,z] in R ) ; :: thesis: [x,z] in Q
then A21: [x,z] in R by A7, A9, A12, RELAT_2:def 8;
now
let Z be set ; :: thesis: ( Z in XX implies ( x in Z iff z in Z ) )
assume Z in XX ; :: thesis: ( x in Z iff z in Z )
then ( ( x in Z implies y in Z ) & ( y in Z implies x in Z ) & ( y in Z implies z in Z ) & ( z in Z implies y in Z ) ) by A20;
hence ( x in Z iff z in Z ) ; :: thesis: verum
end;
hence [x,z] in Q by A8, A9, A12, A21; :: thesis: verum
end;
hence [x,z] in Q by A8, A12, A13, A16, A18; :: thesis: verum
end;
thus Q is antisymmetric :: thesis: ( Q is connected & Q is well_founded )
proof
let x be set ; :: according to RELAT_2:def 4,RELAT_2:def 12 :: thesis: for b1 being set holds
( not x in field Q or not b1 in field Q or not [x,b1] in Q or not [b1,x] in Q or x = b1 )
let y be set ; :: thesis: ( not x in field Q or not y in field Q or not [x,y] in Q or not [y,x] in Q or x = y )
assume A22: ( x in field Q & y in field Q & [x,y] in Q & [y,x] in Q ) ; :: thesis: x = y
then A23: ( ( ex Z1 being set st
( Z1 in XX & x in Z1 & not y in Z1 ) or ( ( for Z1 being set st Z1 in XX holds
( x in Z1 iff y in Z1 ) ) & [x,y] in R ) ) & ( ex Z1 being set st
( Z1 in XX & y in Z1 & not x in Z1 ) or ( ( for Z1 being set st Z1 in XX holds
( y in Z1 iff x in Z1 ) ) & [y,x] in R ) ) ) by A8;
now
given Z1 being set such that A24: ( Z1 in XX & x in Z1 & not y in Z1 ) ; :: thesis: ( ex Z2 being set st
( Z2 in XX & y in Z2 & not x in Z2 ) implies x = y )
given Z2 being set such that A25: ( Z2 in XX & y in Z2 & not x in Z2 ) ; :: thesis: x = y
( Z1 c= Z2 or Z2 c= Z1 ) by A5, A24, A25;
hence x = y by A24, A25; :: thesis: verum
end;
hence x = y by A7, A9, A22, A23, RELAT_2:def 4; :: thesis: verum
end;
thus Q is connected :: thesis: Q is well_founded
proof
let x be set ; :: according to RELAT_2:def 6,RELAT_2:def 14 :: thesis: for b1 being set holds
( not x in field Q or not b1 in field Q or x = b1 or [x,b1] in Q or [b1,x] in Q )
let y be set ; :: thesis: ( not x in field Q or not y in field Q or x = y or [x,y] in Q or [y,x] in Q )
assume A26: ( x in field Q & y in field Q & x <> y ) ; :: thesis: ( [x,y] in Q or [y,x] in Q )
now
assume A27: for Z being set st Z in XX holds
( x in Z iff y in Z ) ; :: thesis: ( [x,y] in Q or [y,x] in Q )
then ( ( [x,y] in R or [y,x] in R ) & ( for Z being set st Z in XX holds
( y in Z iff x in Z ) ) ) by A7, A9, A26, RELAT_2:def 6;
hence ( [x,y] in Q or [y,x] in Q ) by A8, A9, A26, A27; :: thesis: verum
end;
hence ( [x,y] in Q or [y,x] in Q ) by A8, A9, A26; :: thesis: verum
end;
thus Q is well_founded :: thesis: verum
proof
let Y be set ; :: according to WELLORD1:def 2 :: thesis: ( not Y c= field Q or Y = {} or ex b1 being set st
( b1 in Y & Q -Seg b1 misses Y ) )
assume A28: ( Y c= field Q & Y <> {} ) ; :: thesis: ex b1 being set st
( b1 in Y & Q -Seg b1 misses Y )
defpred S3[ set ] means $1 /\ Y <> {} ;
consider Z being set such that
A29: for x being set holds
( x in Z iff ( x in XX & S3[x] ) ) from XBOOLE_0:sch 1();
 A30: Z c= XX
proof
let x be set ; :: according to TARSKI:def 3 :: thesis: ( not x in Z or x in XX )
thus ( not x in Z or x in XX ) by A29; :: thesis: verum
end;
consider x being Element of Y;
x in union XX by A3, A9, A28, TARSKI:def 3;
then consider Z1 being set such that
A31: ( x in Z1 & Z1 in XX ) by TARSKI:def 4;
Z1 /\ Y <> {} by A28, A31, XBOOLE_0:def 4;
then Z <> {} by A29, A31;
then consider Z1 being set such that
A32: ( Z1 in Z & ( for Z2 being set st Z2 in Z holds
Z1 c= Z2 ) ) by A4, A30;
A33: Z1 in XX by A29, A32;
then ( Z1 /\ Y c= Z1 & Z1 c= union X & Z1 /\ Y <> {} ) by A3, A29, A32, XBOOLE_1:17, ZFMISC_1:92;
then consider x being set such that
A34: ( x in Z1 /\ Y & ( for y being set st y in Z1 /\ Y holds
[x,y] in R ) ) by A6, WELLORD1:9, XBOOLE_1:1;
take x ; :: thesis: ( x in Y & Q -Seg x misses Y )
thus x in Y by A34, XBOOLE_0:def 4; :: thesis: Q -Seg x misses Y
assume A35: (Q -Seg x) /\ Y <> {} ; :: according to XBOOLE_0:def 7 :: thesis: contradiction
consider y being Element of (Q -Seg x) /\ Y;
A36: x in Z1 by A34, XBOOLE_0:def 4;
A37: ( y in Q -Seg x & y in Y ) by A35, XBOOLE_0:def 4;
then A38: ( y <> x & [y,x] in Q & y in Y ) by WELLORD1:def 1;
now
given Z2 being set such that A39: ( Z2 in XX & y in Z2 & not x in Z2 ) ; :: thesis: contradiction
Z2 /\ Y <> {} by A37, A39, XBOOLE_0:def 4;
then Z2 in Z by A29, A39;
then Z1 c= Z2 by A32;
hence contradiction by A36, A39; :: thesis: verum
end;
then A40: ( y in Z1 & [y,x] in R ) by A8, A33, A36, A38;
then y in Z1 /\ Y by A37, XBOOLE_0:def 4;
then ( [x,y] in R & x in union X & y in union X ) by A8, A34, A38;
hence contradiction by A7, A38, A40, RELAT_2:def 4; :: thesis: verum
end;
end;
then Q, RelIncl (order_type_of Q) are_isomorphic by WELLORD2:def 2;
then RelIncl (order_type_of Q),Q are_isomorphic by WELLORD1:50;
then consider g being Function such that
A41: g is_isomorphism_of RelIncl (order_type_of Q),Q by WELLORD1:def 8;
field (RelIncl (order_type_of Q)) = order_type_of Q by WELLORD2:def 1;
then A42: ( dom g = order_type_of Q & rng g = union X & g is one-to-one & ( for x, y being set holds
( [x,y] in RelIncl (order_type_of Q) iff ( x in order_type_of Q & y in order_type_of Q & [(g . x),(g . y)] in Q ) ) ) ) by A9, A41, WELLORD1:def 7;
A43: for Z, x being set st Z in XX & x in Z holds
Q -Seg x c= Z
proof
let Z, x be set ; :: thesis: ( Z in XX & x in Z implies Q -Seg x c= Z )
assume A44: ( Z in XX & x in Z ) ; :: thesis: Q -Seg x c= Z
let y be set ; :: according to TARSKI:def 3 :: thesis: ( not y in Q -Seg x or y in Z )
assume y in Q -Seg x ; :: thesis: y in Z
then A45: [y,x] in Q by WELLORD1:def 1;
now
given Z1 being set such that A46: ( Z1 in XX & y in Z1 & not x in Z1 ) ; :: thesis: y in Z
( Z1 c= Z or Z c= Z1 ) by A5, A44, A46;
hence y in Z by A44, A46; :: thesis: verum
end;
hence y in Z by A8, A44, A45; :: thesis: verum
end;
A47: for A being Ordinal st A in order_type_of Q holds
card A = card (Q -Seg (g . A))
proof
let A be Ordinal; :: thesis: ( A in order_type_of Q implies card A = card (Q -Seg (g . A)) )
assume A48: A in order_type_of Q ; :: thesis: card A = card (Q -Seg (g . A))
A,Q -Seg (g . A) are_equipotent
proof
take f = g | A; :: according to WELLORD2:def 4 :: thesis: ( f is one-to-one & dom f = A & rng f = Q -Seg (g . A) )
A c= dom g by A42, A48, ORDINAL1:def 2;
hence A49: ( f is one-to-one & dom f = A ) by A42, FUNCT_1:84, RELAT_1:91; :: thesis: rng f = Q -Seg (g . A)
thus rng f c= Q -Seg (g . A) :: according to XBOOLE_0:def 10 :: thesis: Q -Seg (g . A) c= rng f
proof
let x be set ; :: according to TARSKI:def 3 :: thesis: ( not x in rng f or x in Q -Seg (g . A) )
assume x in rng f ; :: thesis: x in Q -Seg (g . A)
then consider y being set such that
A50: ( y in dom f & x = f . y ) by FUNCT_1:def 5;
reconsider B = y as Ordinal by A49, A50;
A51: ( B in order_type_of Q & B c= A ) by A48, A49, A50, ORDINAL1:19, ORDINAL1:def 2;
then ( [B,A] in RelIncl (order_type_of Q) & x = g . B & A <> B ) by A48, A49, A50, FUNCT_1:70, WELLORD2:def 1;
then ( [x,(g . A)] in Q & x <> g . A ) by A42, A48, A51, FUNCT_1:def 8;
hence x in Q -Seg (g . A) by WELLORD1:def 1; :: thesis: verum
end;
let x be set ; :: according to TARSKI:def 3 :: thesis: ( not x in Q -Seg (g . A) or x in rng f )
assume A52: x in Q -Seg (g . A) ; :: thesis: x in rng f
then A53: ( [x,(g . A)] in Q & x <> g . A ) by WELLORD1:def 1;
then x in union X by A8;
then consider y being set such that
A54: ( y in dom g & x = g . y ) by A42, FUNCT_1:def 5;
reconsider B = y as Ordinal by A42, A54;
[B,A] in RelIncl (order_type_of Q) by A42, A48, A53, A54;
then ( B c= A & B <> A ) by A42, A48, A52, A54, WELLORD1:def 1, WELLORD2:def 1;
then B c< A by XBOOLE_0:def 8;
hence x in rng f by A54, FUNCT_1:73, ORDINAL1:21; :: thesis: verum
end;
hence card A = card (Q -Seg (g . A)) by CARD_1:21; :: thesis: verum
end;
A55: order_type_of Q c= M
proof
let x be Ordinal; :: according to ORDINAL1:def 5 :: thesis: ( not x in order_type_of Q or x in M )
assume A56: x in order_type_of Q ; :: thesis: x in M
reconsider A = x as Ordinal ;
g . x in union X by A42, A56, FUNCT_1:def 5;
then consider Z being set such that
A57: ( g . x in Z & Z in XX ) by A3, TARSKI:def 4;
Q -Seg (g . x) c= Z by A43, A57;
then ( card (Q -Seg (g . x)) c= card Z & card Z in M ) by A1, A3, A57, CARD_1:27;
then ( card (Q -Seg (g . x)) = card A & card (Q -Seg (g . x)) in M ) by A47, A56, ORDINAL1:22;
hence x in M by Th60; :: thesis: verum
end;
order_type_of Q, union X are_equipotent by A42, WELLORD2:def 4;
then ( card (order_type_of Q) = card (union X) & card M = M ) by CARD_1:21, CARD_1:def 5;
hence card (union X) c= M by A55, CARD_1:27; :: thesis: verum