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