let X be set ; ( X is c=-linear implies ex Y being set st
( Y c= X & union Y = union X & ( for Z being set st Z c= Y & Z <> {} holds
ex Z1 being set st
( Z1 in Z & ( for Z2 being set st Z2 in Z holds
Z1 c= Z2 ) ) ) ) )
assume A1:
X is c=-linear
; ex Y being set st
( Y c= X & union Y = union X & ( for Z being set st Z c= Y & Z <> {} holds
ex Z1 being set st
( Z1 in Z & ( for Z2 being set st Z2 in Z holds
Z1 c= Z2 ) ) ) )
consider R being Relation such that
A2:
R well_orders X
by WELLORD2:17;
A3:
R |_2 X is well-ordering
by A2, WELLORD2:16;
A4:
field (R |_2 X) = X
by A2, WELLORD2:16;
R |_2 X, RelIncl (order_type_of (R |_2 X)) are_isomorphic
by A3, WELLORD2:def 2;
then
RelIncl (order_type_of (R |_2 X)),R |_2 X are_isomorphic
by WELLORD1:40;
then consider f being Function such that
A5:
f is_isomorphism_of RelIncl (order_type_of (R |_2 X)),R |_2 X
;
field (RelIncl (order_type_of (R |_2 X))) = order_type_of (R |_2 X)
by WELLORD2:def 1;
then A6:
dom f = order_type_of (R |_2 X)
by A5;
A7:
rng f = X
by A4, A5;
defpred S2[ object ] means for A, B being Ordinal st B in A & $1 = A holds
f . B c= f . A;
consider Y being set such that
A8:
for x being set holds
( x in Y iff ( x in dom f & S2[x] ) )
from XFAMILY:sch 1();
take Z = f .: Y; ( Z c= X & union Z = union X & ( for Z being set st Z c= Z & Z <> {} holds
ex Z1 being set st
( Z1 in Z & ( for Z2 being set st Z2 in Z holds
Z1 c= Z2 ) ) ) )
thus
Z c= X
by A7, RELAT_1:111; ( union Z = union X & ( for Z being set st Z c= Z & Z <> {} holds
ex Z1 being set st
( Z1 in Z & ( for Z2 being set st Z2 in Z holds
Z1 c= Z2 ) ) ) )
thus
union Z c= union X
by A7, RELAT_1:111, ZFMISC_1:77; XBOOLE_0:def 10 ( union X c= union Z & ( for Z being set st Z c= Z & Z <> {} holds
ex Z1 being set st
( Z1 in Z & ( for Z2 being set st Z2 in Z holds
Z1 c= Z2 ) ) ) )
thus
union X c= union Z
for Z being set st Z c= Z & Z <> {} holds
ex Z1 being set st
( Z1 in Z & ( for Z2 being set st Z2 in Z holds
Z1 c= Z2 ) )proof
let x be
object ;
TARSKI:def 3 ( not x in union X or x in union Z )
assume
x in union X
;
x in union Z
then consider Z1 being
set such that A9:
x in Z1
and A10:
Z1 in X
by TARSKI:def 4;
consider y being
object such that A11:
y in dom f
and A12:
Z1 = f . y
by A7, A10, FUNCT_1:def 3;
reconsider y =
y as
Ordinal by A6, A11;
defpred S3[
Ordinal]
means ( $1
c= y &
x in f . $1 );
A13:
ex
A being
Ordinal st
S3[
A]
by A9, A12;
consider A being
Ordinal such that A14:
(
S3[
A] & ( for
B being
Ordinal st
S3[
B] holds
A c= B ) )
from ORDINAL1:sch 1(A13);
A15:
A in dom f
by A6, A11, A14, ORDINAL1:12;
now for B, C being Ordinal st C in B & A = B holds
f . C c= f . Blet B,
C be
Ordinal;
( C in B & A = B implies f . C c= f . B )assume that A16:
C in B
and A17:
A = B
;
f . C c= f . BA18:
C in dom f
by A6, A11, A14, A16, A17, ORDINAL1:10;
A19:
( not
C c= y or not
x in f . C )
by A14, A16, A17, ORDINAL1:5;
A20:
f . A in X
by A7, A15, FUNCT_1:def 3;
f . C in X
by A7, A18, FUNCT_1:def 3;
then
f . C,
f . A are_c=-comparable
by A1, A20;
then
(
f . C c= f . A or
f . A c= f . C )
;
hence
f . C c= f . B
by A14, A16, A17, A19, ORDINAL1:def 2;
verum end;
then
A in Y
by A8, A15;
then
f . A in Z
by A15, FUNCT_1:def 6;
hence
x in union Z
by A14, TARSKI:def 4;
verum
end;
let V be set ; ( V c= Z & V <> {} implies ex Z1 being set st
( Z1 in V & ( for Z2 being set st Z2 in V holds
Z1 c= Z2 ) ) )
assume that
A21:
V c= Z
and
A22:
V <> {}
; ex Z1 being set st
( Z1 in V & ( for Z2 being set st Z2 in V holds
Z1 c= Z2 ) )
set x = the Element of V;
the Element of V in Z
by A21, A22;
then consider y being object such that
A23:
y in dom f
and
A24:
y in Y
and
A25:
the Element of V = f . y
by FUNCT_1:def 6;
reconsider y = y as Ordinal by A6, A23;
defpred S3[ Ordinal] means ( $1 in Y & f . $1 in V );
y = y
;
then A26:
ex A being Ordinal st S3[A]
by A22, A24, A25;
consider A being Ordinal such that
A27:
( S3[A] & ( for B being Ordinal st S3[B] holds
A c= B ) )
from ORDINAL1:sch 1(A26);
take Z1 = f . A; ( Z1 in V & ( for Z2 being set st Z2 in V holds
Z1 c= Z2 ) )
thus
Z1 in V
by A27; for Z2 being set st Z2 in V holds
Z1 c= Z2
let Z2 be set ; ( Z2 in V implies Z1 c= Z2 )
assume A28:
Z2 in V
; Z1 c= Z2
then consider y being object such that
A29:
y in dom f
and
A30:
y in Y
and
A31:
Z2 = f . y
by A21, FUNCT_1:def 6;
reconsider y = y as Ordinal by A6, A29;
( A c< y iff ( A c= y & A <> y ) )
;
then
( A = y or A in y )
by A27, A28, A30, A31, ORDINAL1:11;
hence
Z1 c= Z2
by A8, A30, A31; verum