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 and
A4: union XX = union X and
A5: 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;
A6: now
let Z1, Z2 be set ; :: thesis: ( Z1 in XX & Z2 in XX & not Z1 c= Z2 implies Z2 c= Z1 )
assume that
A7: Z1 in XX and
A8: Z2 in XX ; :: thesis: ( Z1 c= Z2 or Z2 c= Z1 )
Z1,Z2 are_c=-comparable by A2, A3, A7, A8, 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
A9: R well_orders union X by WELLORD2:26;
A10: R is_reflexive_in union X by A9, WELLORD1:def 5;
A11: R is_transitive_in union X by A9, WELLORD1:def 5;
A12: R is_antisymmetric_in union X by A9, WELLORD1:def 5;
A13: R is_connected_in union X by A9, 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
A14: 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();
 A15: 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 A14; :: thesis: verum
end;
let x be set ; :: according to TARSKI:def 3 :: thesis: ( not x in union X or x in field Q )
assume A16: x in union X ; :: thesis: x in field Q
then A17: [x,x] in R by A10, RELAT_2:def 1;
for Z1 being set st Z1 in XX holds
( x in Z1 iff x in Z1 ) ;
then [x,x] in Q by A14, A16, A17;
hence x in field Q by RELAT_1:30; :: thesis: verum
end;
A18: Q is reflexive
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 A19: x in field Q ; :: thesis: [x,x] in Q
then A20: [x,x] in R by A10, A15, RELAT_2:def 1;
for Z1 being set st Z1 in XX holds
( x in Z1 iff x in Z1 ) ;
hence [x,x] in Q by A14, A15, A19, A20; :: thesis: verum
end;
A21: Q is transitive
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 that
A22: x in field Q and
A23: y in field Q and
A24: z in field Q and
A25: [x,y] in Q and
A26: [y,z] in Q ; :: thesis: [x,z] in Q
A27: now
given Z1 being set such that A28: Z1 in XX and
A29: x in Z1 and
A30: 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 A31: Z2 in XX and
A32: y in Z2 and
A33: not z in Z2 ; :: thesis: [x,z] in Q
( Z1 c= Z2 or Z2 c= Z1 ) by A6, A28, A31;
hence [x,z] in Q by A14, A15, A22, A24, A29, A30, A31, A32, A33; :: thesis: verum
end;
A34: now
given Z1 being set such that A35: Z1 in XX and
A36: x in Z1 and
A37: 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 that
A38: for Z1 being set st Z1 in XX holds
( y in Z1 iff z in Z1 ) and
[y,z] in R ; :: thesis: [x,z] in Q
not z in Z1 by A35, A37, A38;
hence [x,z] in Q by A14, A15, A22, A24, A35, A36; :: thesis: verum
end;
A39: now
given Z1 being set such that A40: Z1 in XX and
A41: y in Z1 and
A42: 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 that
A43: for Z1 being set st Z1 in XX holds
( x in Z1 iff y in Z1 ) and
[x,y] in R ; :: thesis: [x,z] in Q
x in Z1 by A40, A41, A43;
hence [x,z] in Q by A14, A15, A22, A24, A40, A42; :: thesis: verum
end;
now
assume that
A44: for Z1 being set st Z1 in XX holds
( x in Z1 iff y in Z1 ) and
A45: [x,y] in R and
A46: for Z1 being set st Z1 in XX holds
( y in Z1 iff z in Z1 ) and
A47: [y,z] in R ; :: thesis: [x,z] in Q
A48: [x,z] in R by A11, A15, A22, A23, A24, A45, A47, RELAT_2:def 8;
now
let Z be set ; :: thesis: ( Z in XX implies ( x in Z iff z in Z ) )
assume A49: Z in XX ; :: thesis: ( x in Z iff z in Z )
then ( x in Z iff y in Z ) by A44;
hence ( x in Z iff z in Z ) by A46, A49; :: thesis: verum
end;
hence [x,z] in Q by A14, A15, A22, A24, A48; :: thesis: verum
end;
hence [x,z] in Q by A14, A25, A26, A27, A34, A39; :: thesis: verum
end;
A50: Q is antisymmetric
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 that
A51: x in field Q and
A52: y in field Q and
A53: [x,y] in Q and
A54: [y,x] in Q ; :: thesis: x = y
A55: ( 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 ) ) by A14, A53;
A56: ( 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 A14, A54;
now
given Z1 being set such that A57: Z1 in XX and
A58: x in Z1 and
A59: 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 A60: Z2 in XX and
A61: y in Z2 and
A62: not x in Z2 ; :: thesis: x = y
( Z1 c= Z2 or Z2 c= Z1 ) by A6, A57, A60;
hence x = y by A58, A59, A61, A62; :: thesis: verum
end;
hence x = y by A12, A15, A51, A52, A55, A56, RELAT_2:def 4; :: thesis: verum
end;
A63: Q is connected
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 that
A64: x in field Q and
A65: y in field Q and
A66: x <> y ; :: thesis: ( [x,y] in Q or [y,x] in Q )
now
assume A67: 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 )
A68: ( [x,y] in R or [y,x] in R ) by A13, A15, A64, A65, A66, RELAT_2:def 6;
for Z being set st Z in XX holds
( y in Z iff x in Z ) by A67;
hence ( [x,y] in Q or [y,x] in Q ) by A14, A15, A64, A65, A67, A68; :: thesis: verum
end;
hence ( [x,y] in Q or [y,x] in Q ) by A14, A15, A64, A65; :: thesis: verum
end;
Q is well_founded
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 that
A69: Y c= field Q and
A70: 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
A71: for x being set holds
( x in Z iff ( x in XX & S3[x] ) ) from XBOOLE_0:sch 1();
 A72: 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 A71; :: thesis: verum
end;
consider x being Element of Y;
x in union XX by A4, A15, A69, A70, TARSKI:def 3;
then consider Z1 being set such that
A73: x in Z1 and
A74: Z1 in XX by TARSKI:def 4;
Z1 /\ Y <> {} by A70, A73, XBOOLE_0:def 4;
then Z <> {} by A71, A74;
then consider Z1 being set such that
A75: Z1 in Z and
A76: for Z2 being set st Z2 in Z holds
Z1 c= Z2 by A5, A72;
A77: Z1 in XX by A71, A75;
A78: Z1 /\ Y c= Z1 by XBOOLE_1:17;
A79: Z1 c= union X by A3, A77, ZFMISC_1:92;
Z1 /\ Y <> {} by A71, A75;
then consider x being set such that
A80: x in Z1 /\ Y and
A81: for y being set st y in Z1 /\ Y holds
[x,y] in R by A9, A78, A79, WELLORD1:9, XBOOLE_1:1;
take x ; :: thesis: ( x in Y & Q -Seg x misses Y )
thus x in Y by A80, XBOOLE_0:def 4; :: thesis: Q -Seg x misses Y
assume A82: (Q -Seg x) /\ Y <> {} ; :: according to XBOOLE_0:def 7 :: thesis: contradiction
consider y being Element of (Q -Seg x) /\ Y;
A83: x in Z1 by A80, XBOOLE_0:def 4;
A84: y in Q -Seg x by A82, XBOOLE_0:def 4;
A85: y in Y by A82, XBOOLE_0:def 4;
A86: y <> x by A84, WELLORD1:def 1;
A87: [y,x] in Q by A84, WELLORD1:def 1;
A88: now
given Z2 being set such that A89: Z2 in XX and
A90: y in Z2 and
A91: not x in Z2 ; :: thesis: contradiction
Z2 /\ Y <> {} by A85, A90, XBOOLE_0:def 4;
then Z2 in Z by A71, A89;
then Z1 c= Z2 by A76;
hence contradiction by A83, A91; :: thesis: verum
end;
then A92: y in Z1 by A14, A77, A83, A87;
A93: [y,x] in R by A14, A87, A88;
y in Z1 /\ Y by A85, A92, XBOOLE_0:def 4;
then A94: [x,y] in R by A81;
A95: x in union X by A14, A87;
y in union X by A14, A87;
hence contradiction by A12, A86, A93, A94, A95, RELAT_2:def 4; :: thesis: verum
end;
then Q is well-ordering by A18, A21, A50, A63, WELLORD1:def 4;
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
A96: g is_isomorphism_of RelIncl (order_type_of Q),Q by WELLORD1:def 8;
A97: field (RelIncl (order_type_of Q)) = order_type_of Q by WELLORD2:def 1;
then A98: dom g = order_type_of Q by A96, WELLORD1:def 7;
A99: rng g = union X by A15, A96, WELLORD1:def 7;
A100: g is one-to-one by A96, WELLORD1:def 7;
A101: 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 that
A102: Z in XX and
A103: 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 A104: [y,x] in Q by WELLORD1:def 1;
now
given Z1 being set such that A105: Z1 in XX and
A106: y in Z1 and
A107: not x in Z1 ; :: thesis: y in Z
( Z1 c= Z or Z c= Z1 ) by A6, A102, A105;
hence y in Z by A103, A106, A107; :: thesis: verum
end;
hence y in Z by A14, A102, A103, A104; :: thesis: verum
end;
A108: 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 A109: 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 & proj1 f = A & proj2 f = Q -Seg (g . A) )
A c= dom g by A98, A109, ORDINAL1:def 2;
hence A110: ( f is one-to-one & dom f = A ) by A100, FUNCT_1:84, RELAT_1:91; :: thesis: proj2 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= proj2 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
A111: y in dom f and
A112: x = f . y by FUNCT_1:def 5;
reconsider B = y as Ordinal by A110, A111;
A113: B in order_type_of Q by A109, A110, A111, ORDINAL1:19;
B c= A by A110, A111, ORDINAL1:def 2;
then A114: [B,A] in RelIncl (order_type_of Q) by A109, A113, WELLORD2:def 1;
A115: x = g . B by A111, A112, FUNCT_1:70;
A116: A <> B by A110, A111;
A117: [x,(g . A)] in Q by A96, A114, A115, WELLORD1:def 7;
x <> g . A by A98, A100, A109, A113, A115, A116, FUNCT_1:def 8;
hence x in Q -Seg (g . A) by A117, 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 proj2 f )
assume A118: x in Q -Seg (g . A) ; :: thesis: x in proj2 f
then A119: [x,(g . A)] in Q by WELLORD1:def 1;
then x in union X by A14;
then consider y being set such that
A120: y in dom g and
A121: x = g . y by A99, FUNCT_1:def 5;
reconsider B = y as Ordinal by A98, A120;
[B,A] in RelIncl (order_type_of Q) by A96, A97, A98, A109, A119, A120, A121, WELLORD1:def 7;
then A122: B c= A by A98, A109, A120, WELLORD2:def 1;
B <> A by A118, A121, WELLORD1:def 1;
then B c< A by A122, XBOOLE_0:def 8;
hence x in proj2 f by A120, A121, FUNCT_1:73, ORDINAL1:21; :: thesis: verum
end;
hence card A = card (Q -Seg (g . A)) by CARD_1:21; :: thesis: verum
end;
A123: 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 A124: x in order_type_of Q ; :: thesis: x in M
reconsider A = x as Ordinal ;
g . x in union X by A98, A99, A124, FUNCT_1:def 5;
then consider Z being set such that
A125: g . x in Z and
A126: Z in XX by A4, TARSKI:def 4;
A127: card (Q -Seg (g . x)) c= card Z by A101, A125, A126, CARD_1:27;
A128: card (Q -Seg (g . x)) = card A by A108, A124;
card (Q -Seg (g . x)) in M by A1, A3, A126, A127, ORDINAL1:22;
hence x in M by A128, Th60; :: thesis: verum
end;
order_type_of Q, union X are_equipotent by A98, A99, A100, WELLORD2:def 4;
then A129: card (order_type_of Q) = card (union X) by CARD_1:21;
card M = M by CARD_1:def 5;
hence card (union X) c= M by A123, A129, CARD_1:27; :: thesis: verum