let R be Relation; :: thesis: for X being set st R partially_orders X & field R = X & X has_upper_Zorn_property_wrt R holds
ex x being set st x is_maximal_in R
let FIELD be set ; :: thesis: ( R partially_orders FIELD & field R = FIELD & FIELD has_upper_Zorn_property_wrt R implies ex x being set st x is_maximal_in R )
assume that
A1: R is_reflexive_in FIELD and
A2: R is_transitive_in FIELD and
A3: R is_antisymmetric_in FIELD and
A4: field R = FIELD and
A5: FIELD has_upper_Zorn_property_wrt R ; :: according to ORDERS_1:def 8 :: thesis: ex x being set st x is_maximal_in R
reconsider XD = FIELD as non empty set by A5, Th49;
consider D being non empty set such that
A6: D = XD ;
A7: D in bool D by ZFMISC_1:def 1;
not D in {{}} by TARSKI:def 1;
then reconsider M = (bool D) \ {{}} as non empty set by A7, XBOOLE_0:def 5;
set f = the Choice_Function of M;
defpred S1[ object , object ] means ( ( $1 <> {} & $2 = the Choice_Function of M . $1 ) or ( $1 = {} & $2 = D ) );
A8: for x being object st x in bool D holds
ex y being object st S1[x,y]
proof
let x be object ; :: thesis: ( x in bool D implies ex y being object st S1[x,y] )
assume x in bool D ; :: thesis: ex y being object st S1[x,y]
( x = {} implies ex y being object st S1[x,y] ) ;
hence ex y being object st S1[x,y] ; :: thesis: verum
end;
A9: for x, y, z being object st x in bool D & S1[x,y] & S1[x,z] holds
y = z ;
consider g being Function such that
A10: ( dom g = bool D & ( for x being object st x in bool D holds
S1[x,g . x] ) ) from FUNCT_1:sch 2(A9, A8);
 defpred S2[ Ordinal, object ] means ex L being Sequence st
( $2 = g . { d where d is Element of D : for x being set st x in rng L holds
( x <> d & [x,d] in R ) } & dom L = $1 & ( for A being Ordinal
for L1 being Sequence st A in $1 & L1 = L | A holds
L . A = g . { d1 where d1 is Element of D : for x being set st x in rng L1 holds
( x <> d1 & [x,d1] in R ) } ) );
A11: for x, y being set
for A being Ordinal st S2[A,x] & S2[A,y] holds
x = y
proof
let x, y be set ; :: thesis: for A being Ordinal st S2[A,x] & S2[A,y] holds
x = y
let A be Ordinal; :: thesis: ( S2[A,x] & S2[A,y] implies x = y )
given L1 being Sequence such that A12: x = g . { d1 where d1 is Element of D : for x being set st x in rng L1 holds
( x <> d1 & [x,d1] in R ) } and
A13: ( dom L1 = A & ( for C being Ordinal
for L being Sequence st C in A & L = L1 | C holds
L1 . C = g . { d2 where d2 is Element of D : for x being set st x in rng L holds
( x <> d2 & [x,d2] in R ) } ) ) ; :: thesis: ( not S2[A,y] or x = y )
A14: L1 = L1 | A by A13;
given L2 being Sequence such that A15: y = g . { d1 where d1 is Element of D : for x being set st x in rng L2 holds
( x <> d1 & [x,d1] in R ) } and
A16: ( dom L2 = A & ( for C being Ordinal
for L being Sequence st C in A & L = L2 | C holds
L2 . C = g . { d2 where d2 is Element of D : for x being set st x in rng L holds
( x <> d2 & [x,d2] in R ) } ) ) ; :: thesis: x = y
defpred S3[ Ordinal] means ( $1 c= A implies L1 | $1 = L2 | $1 );
A17: for A1 being Ordinal st ( for A2 being Ordinal st A2 in A1 holds
S3[A2] ) holds
S3[A1]
proof
let A1 be Ordinal; :: thesis: ( ( for A2 being Ordinal st A2 in A1 holds
S3[A2] ) implies S3[A1] )
assume that
A18: for A2 being Ordinal st A2 in A1 & A2 c= A holds
L1 | A2 = L2 | A2 and
A19: A1 c= A ; :: thesis: L1 | A1 = L2 | A1
A20: dom (L2 | A1) = A1 by A16, A19, RELAT_1:62;
A21: now :: thesis: for x being object st x in A1 holds
(L1 | A1) . x = (L2 | A1) . x
let x be object ; :: thesis: ( x in A1 implies (L1 | A1) . x = (L2 | A1) . x )
assume A22: x in A1 ; :: thesis: (L1 | A1) . x = (L2 | A1) . x
then reconsider A3 = x as Ordinal ;
A23: L1 . x = (L1 | A1) . x by A22, FUNCT_1:49;
A3 c= A by A19, A22, ORDINAL1:def 2;
then A24: L1 | A3 = L2 | A3 by A18, A22;
A25: L2 . A3 = g . { d2 where d2 is Element of D : for x being set st x in rng (L2 | A3) holds
( x <> d2 & [x,d2] in R ) } by A16, A19, A22;
L1 . A3 = g . { d1 where d1 is Element of D : for x being set st x in rng (L1 | A3) holds
( x <> d1 & [x,d1] in R ) } by A13, A19, A22;
hence (L1 | A1) . x = (L2 | A1) . x by A22, A24, A23, A25, FUNCT_1:49; :: thesis: verum
end;
dom (L1 | A1) = A1 by A13, A19, RELAT_1:62;
hence L1 | A1 = L2 | A1 by A20, A21, FUNCT_1:2; :: thesis: verum
end;
for A1 being Ordinal holds S3[A1] from ORDINAL1:sch 2(A17);
 then A26: L1 | A = L2 | A ;
L2 = L2 | A by A16;
hence x = y by A12, A15, A26, A14; :: thesis: verum
end;
{} in {{}} by TARSKI:def 1;
then A27: not {} in M by XBOOLE_0:def 5;
A28: for X being set st X in bool D & X <> {} holds
g . X in X
proof
let X be set ; :: thesis: ( X in bool D & X <> {} implies g . X in X )
assume that
A29: X in bool D and
A30: X <> {} ; :: thesis: g . X in X
not X in {{}} by A30, TARSKI:def 1;
then A31: X in M by A29, XBOOLE_0:def 5;
the Choice_Function of M . X = g . X by A10, A29, A30;
hence g . X in X by A27, A31, Lm2; :: thesis: verum
end;
defpred S3[ Ordinal] means S2[$1,D];
{} c= D ;
then A32: g . {} = D by A10;
A33: now :: thesis: for A, B being Ordinal
for L1, L2 being Sequence st dom L1 = A & ( for C being Ordinal
for L being Sequence st C in A & L = L1 | C holds
L1 . C = g . { d2 where d2 is Element of D : for x being set st x in rng L holds
( x <> d2 & [x,d2] in R ) } ) & dom L2 = B & ( for C being Ordinal
for L being Sequence st C in B & L = L2 | C holds
L2 . C = g . { d2 where d2 is Element of D : for x being set st x in rng L holds
( x <> d2 & [x,d2] in R ) } ) holds
for C being Ordinal st C c= A & C c= B holds
L1 | C = L2 | C
let A, B be Ordinal; :: thesis: for L1, L2 being Sequence st dom L1 = A & ( for C being Ordinal
for L being Sequence st C in A & L = L1 | C holds
L1 . C = g . { d2 where d2 is Element of D : for x being set st x in rng L holds
( x <> d2 & [x,d2] in R ) } ) & dom L2 = B & ( for C being Ordinal
for L being Sequence st C in B & L = L2 | C holds
L2 . C = g . { d2 where d2 is Element of D : for x being set st x in rng L holds
( x <> d2 & [x,d2] in R ) } ) holds
for C being Ordinal st C c= A & C c= B holds
L1 | C = L2 | C
let L1, L2 be Sequence; :: thesis: ( dom L1 = A & ( for C being Ordinal
for L being Sequence st C in A & L = L1 | C holds
L1 . C = g . { d2 where d2 is Element of D : for x being set st x in rng L holds
( x <> d2 & [x,d2] in R ) } ) & dom L2 = B & ( for C being Ordinal
for L being Sequence st C in B & L = L2 | C holds
L2 . C = g . { d2 where d2 is Element of D : for x being set st x in rng L holds
( x <> d2 & [x,d2] in R ) } ) implies for C being Ordinal st C c= A & C c= B holds
L1 | C = L2 | C )
assume that
A34: ( dom L1 = A & ( for C being Ordinal
for L being Sequence st C in A & L = L1 | C holds
L1 . C = g . { d2 where d2 is Element of D : for x being set st x in rng L holds
( x <> d2 & [x,d2] in R ) } ) ) and
A35: ( dom L2 = B & ( for C being Ordinal
for L being Sequence st C in B & L = L2 | C holds
L2 . C = g . { d2 where d2 is Element of D : for x being set st x in rng L holds
( x <> d2 & [x,d2] in R ) } ) ) ; :: thesis: for C being Ordinal st C c= A & C c= B holds
L1 | C = L2 | C
let C be Ordinal; :: thesis: ( C c= A & C c= B implies L1 | C = L2 | C )
assume that
A36: C c= A and
A37: C c= B ; :: thesis: L1 | C = L2 | C
defpred S4[ Ordinal] means ( $1 c= C implies L1 | $1 = L2 | $1 );
A38: for A1 being Ordinal st ( for A2 being Ordinal st A2 in A1 holds
S4[A2] ) holds
S4[A1]
proof
let A1 be Ordinal; :: thesis: ( ( for A2 being Ordinal st A2 in A1 holds
S4[A2] ) implies S4[A1] )
assume that
A39: for A2 being Ordinal st A2 in A1 & A2 c= C holds
L1 | A2 = L2 | A2 and
A40: A1 c= C ; :: thesis: L1 | A1 = L2 | A1
A41: dom (L2 | A1) = A1 by A35, A37, A40, RELAT_1:62, XBOOLE_1:1;
A42: now :: thesis: for x being object st x in A1 holds
(L1 | A1) . x = (L2 | A1) . x
let x be object ; :: thesis: ( x in A1 implies (L1 | A1) . x = (L2 | A1) . x )
assume A43: x in A1 ; :: thesis: (L1 | A1) . x = (L2 | A1) . x
then reconsider A3 = x as Ordinal ;
A44: L1 . x = (L1 | A1) . x by A43, FUNCT_1:49;
A3 c= C by A40, A43, ORDINAL1:def 2;
then A45: L1 | A3 = L2 | A3 by A39, A43;
A46: A3 in C by A40, A43;
then A47: L2 . A3 = g . { d2 where d2 is Element of D : for x being set st x in rng (L2 | A3) holds
( x <> d2 & [x,d2] in R ) } by A35, A37;
L1 . A3 = g . { d1 where d1 is Element of D : for x being set st x in rng (L1 | A3) holds
( x <> d1 & [x,d1] in R ) } by A34, A36, A46;
hence (L1 | A1) . x = (L2 | A1) . x by A43, A45, A44, A47, FUNCT_1:49; :: thesis: verum
end;
dom (L1 | A1) = A1 by A34, A36, A40, RELAT_1:62, XBOOLE_1:1;
hence L1 | A1 = L2 | A1 by A41, A42, FUNCT_1:2; :: thesis: verum
end;
for A1 being Ordinal holds S4[A1] from ORDINAL1:sch 2(A38);
hence L1 | C = L2 | C ; :: thesis: verum
end;
A48: for d being Element of D
for A, B being Ordinal st S2[A,d] & S2[B,d] holds
A = B
proof
let d be Element of D; :: thesis: for A, B being Ordinal st S2[A,d] & S2[B,d] holds
A = B
let A, B be Ordinal; :: thesis: ( S2[A,d] & S2[B,d] implies A = B )
given L1 being Sequence such that A49: d = g . { d1 where d1 is Element of D : for x being set st x in rng L1 holds
( x <> d1 & [x,d1] in R ) } and
A50: ( dom L1 = A & ( for C being Ordinal
for L being Sequence st C in A & L = L1 | C holds
L1 . C = g . { d2 where d2 is Element of D : for x being set st x in rng L holds
( x <> d2 & [x,d2] in R ) } ) ) ; :: thesis: ( not S2[B,d] or A = B )
given L2 being Sequence such that A51: d = g . { d1 where d1 is Element of D : for x being set st x in rng L2 holds
( x <> d1 & [x,d1] in R ) } and
A52: ( dom L2 = B & ( for C being Ordinal
for L being Sequence st C in B & L = L2 | C holds
L2 . C = g . { d2 where d2 is Element of D : for x being set st x in rng L holds
( x <> d2 & [x,d2] in R ) } ) ) ; :: thesis: A = B
A53: now :: thesis: not B in A
set Y = { d1 where d1 is Element of D : for x being set st x in rng L1 holds
( x <> d1 & [x,d1] in R ) } ;
set X = { d1 where d1 is Element of D : for x being set st x in rng (L1 | B) holds
( x <> d1 & [x,d1] in R ) } ;
A54: { d1 where d1 is Element of D : for x being set st x in rng L1 holds
( x <> d1 & [x,d1] in R ) } c= D
proof
let x be object ; :: according to TARSKI:def 3 :: thesis: ( not x in { d1 where d1 is Element of D : for x being set st x in rng L1 holds
( x <> d1 & [x,d1] in R ) } or x in D )
assume x in { d1 where d1 is Element of D : for x being set st x in rng L1 holds
( x <> d1 & [x,d1] in R ) } ; :: thesis: x in D
then ex d1 being Element of D st
( x = d1 & ( for x being set st x in rng L1 holds
( x <> d1 & [x,d1] in R ) ) ) ;
hence x in D ; :: thesis: verum
end;
assume A55: B in A ; :: thesis: contradiction
then B c= A by ORDINAL1:def 2;
then A56: L1 | B = L2 | B by A33, A50, A52
.= L2 by A52 ;
L1 . B = g . { d1 where d1 is Element of D : for x being set st x in rng (L1 | B) holds
( x <> d1 & [x,d1] in R ) } by A50, A55;
then A57: d in rng L1 by A50, A51, A55, A56, FUNCT_1:def 3;
A58: now :: thesis: not { d1 where d1 is Element of D : for x being set st x in rng L1 holds
( x <> d1 & [x,d1] in R ) } <> {}
assume A59: { d1 where d1 is Element of D : for x being set st x in rng L1 holds
( x <> d1 & [x,d1] in R ) } <> {} ; :: thesis: contradiction
then not { d1 where d1 is Element of D : for x being set st x in rng L1 holds
( x <> d1 & [x,d1] in R ) } in {{}} by TARSKI:def 1;
then A60: { d1 where d1 is Element of D : for x being set st x in rng L1 holds
( x <> d1 & [x,d1] in R ) } in M by A54, XBOOLE_0:def 5;
g . { d1 where d1 is Element of D : for x being set st x in rng L1 holds
( x <> d1 & [x,d1] in R ) } = the Choice_Function of M . { d1 where d1 is Element of D : for x being set st x in rng L1 holds
( x <> d1 & [x,d1] in R ) } by A10, A54, A59;
then d in { d1 where d1 is Element of D : for x being set st x in rng L1 holds
( x <> d1 & [x,d1] in R ) } by A27, A49, A60, Lm2;
then ex d1 being Element of D st
( d = d1 & ( for x being set st x in rng L1 holds
( x <> d1 & [x,d1] in R ) ) ) ;
hence contradiction by A57; :: thesis: verum
end;
A61: not d in d ;
S1[ { d1 where d1 is Element of D : for x being set st x in rng L1 holds
( x <> d1 & [x,d1] in R ) } ,g . { d1 where d1 is Element of D : for x being set st x in rng L1 holds
( x <> d1 & [x,d1] in R ) } ] by A10, A54;
hence contradiction by A49, A61, A58; :: thesis: verum
end;
now :: thesis: not A in B
set Y = { d1 where d1 is Element of D : for x being set st x in rng L2 holds
( x <> d1 & [x,d1] in R ) } ;
set X = { d1 where d1 is Element of D : for x being set st x in rng (L2 | A) holds
( x <> d1 & [x,d1] in R ) } ;
A62: { d1 where d1 is Element of D : for x being set st x in rng L2 holds
( x <> d1 & [x,d1] in R ) } c= D
proof
let x be object ; :: according to TARSKI:def 3 :: thesis: ( not x in { d1 where d1 is Element of D : for x being set st x in rng L2 holds
( x <> d1 & [x,d1] in R ) } or x in D )
assume x in { d1 where d1 is Element of D : for x being set st x in rng L2 holds
( x <> d1 & [x,d1] in R ) } ; :: thesis: x in D
then ex d1 being Element of D st
( x = d1 & ( for x being set st x in rng L2 holds
( x <> d1 & [x,d1] in R ) ) ) ;
hence x in D ; :: thesis: verum
end;
assume A63: A in B ; :: thesis: contradiction
then A c= B by ORDINAL1:def 2;
then A64: L2 | A = L1 | A by A33, A50, A52
.= L1 by A50 ;
L2 . A = g . { d1 where d1 is Element of D : for x being set st x in rng (L2 | A) holds
( x <> d1 & [x,d1] in R ) } by A52, A63;
then A65: d in rng L2 by A49, A52, A63, A64, FUNCT_1:def 3;
A66: now :: thesis: not { d1 where d1 is Element of D : for x being set st x in rng L2 holds
( x <> d1 & [x,d1] in R ) } <> {}
assume A67: { d1 where d1 is Element of D : for x being set st x in rng L2 holds
( x <> d1 & [x,d1] in R ) } <> {} ; :: thesis: contradiction
then not { d1 where d1 is Element of D : for x being set st x in rng L2 holds
( x <> d1 & [x,d1] in R ) } in {{}} by TARSKI:def 1;
then A68: { d1 where d1 is Element of D : for x being set st x in rng L2 holds
( x <> d1 & [x,d1] in R ) } in M by A62, XBOOLE_0:def 5;
g . { d1 where d1 is Element of D : for x being set st x in rng L2 holds
( x <> d1 & [x,d1] in R ) } = the Choice_Function of M . { d1 where d1 is Element of D : for x being set st x in rng L2 holds
( x <> d1 & [x,d1] in R ) } by A10, A62, A67;
then d in { d1 where d1 is Element of D : for x being set st x in rng L2 holds
( x <> d1 & [x,d1] in R ) } by A27, A51, A68, Lm2;
then ex d1 being Element of D st
( d = d1 & ( for x being set st x in rng L2 holds
( x <> d1 & [x,d1] in R ) ) ) ;
hence contradiction by A65; :: thesis: verum
end;
A69: not d in d ;
S1[ { d1 where d1 is Element of D : for x being set st x in rng L2 holds
( x <> d1 & [x,d1] in R ) } ,g . { d1 where d1 is Element of D : for x being set st x in rng L2 holds
( x <> d1 & [x,d1] in R ) } ] by A10, A62;
hence contradiction by A51, A69, A66; :: thesis: verum
end;
hence A = B by A53, ORDINAL1:14; :: thesis: verum
end;
A70: ex A1 being Ordinal st S3[A1]
proof
defpred S4[ object , object ] means ex A being Ordinal st
( $2 = A & S2[A,$1] );
defpred S5[ Ordinal] means ex d being Element of D st S2[$1,d];
assume A71: for A1 being Ordinal holds not S2[A1,D] ; :: thesis: contradiction
A72: for A being Ordinal st ( for B being Ordinal st B in A holds
S5[B] ) holds
S5[A]
proof
defpred S6[ object , object ] means ex C being Ordinal st
( $1 = C & S2[C,$2] );
let A be Ordinal; :: thesis: ( ( for B being Ordinal st B in A holds
S5[B] ) implies S5[A] )
assume A73: for B being Ordinal st B in A holds
ex d being Element of D st S2[B,d] ; :: thesis: S5[A]
A74: for x being object st x in A holds
ex y being object st S6[x,y]
proof
let x be object ; :: thesis: ( x in A implies ex y being object st S6[x,y] )
assume A75: x in A ; :: thesis: ex y being object st S6[x,y]
then reconsider C = x as Ordinal ;
consider d being Element of D such that
A76: S2[C,d] by A73, A75;
reconsider y = d as set ;
take y ; :: thesis: S6[x,y]
take C ; :: thesis: ( x = C & S2[C,y] )
thus ( x = C & S2[C,y] ) by A76; :: thesis: verum
end;
A77: for x, y, z being object st x in A & S6[x,y] & S6[x,z] holds
y = z by A11;
consider h being Function such that
A78: ( dom h = A & ( for x being object st x in A holds
S6[x,h . x] ) ) from FUNCT_1:sch 2(A77, A74);
 reconsider h = h as Sequence by A78, ORDINAL1:def 7;
set X = { d1 where d1 is Element of D : for x being set st x in rng h holds
( x <> d1 & [x,d1] in R ) } ;
A79: { d1 where d1 is Element of D : for x being set st x in rng h holds
( x <> d1 & [x,d1] in R ) } c= D
proof
let x be object ; :: according to TARSKI:def 3 :: thesis: ( not x in { d1 where d1 is Element of D : for x being set st x in rng h holds
( x <> d1 & [x,d1] in R ) } or x in D )
assume x in { d1 where d1 is Element of D : for x being set st x in rng h holds
( x <> d1 & [x,d1] in R ) } ; :: thesis: x in D
then ex d1 being Element of D st
( x = d1 & ( for x being set st x in rng h holds
( x <> d1 & [x,d1] in R ) ) ) ;
hence x in D ; :: thesis: verum
end;
A80: S2[A,g . { d1 where d1 is Element of D : for x being set st x in rng h holds
( x <> d1 & [x,d1] in R ) } ]
proof
take h ; :: thesis: ( g . { d1 where d1 is Element of D : for x being set st x in rng h holds
( x <> d1 & [x,d1] in R ) } = g . { d where d is Element of D : for x being set st x in rng h holds
( x <> d & [x,d] in R ) } & dom h = A & ( for A being Ordinal
for L1 being Sequence st A in A & L1 = h | A holds
h . A = g . { d1 where d1 is Element of D : for x being set st x in rng L1 holds
( x <> d1 & [x,d1] in R ) } ) )
thus ( g . { d1 where d1 is Element of D : for x being set st x in rng h holds
( x <> d1 & [x,d1] in R ) } = g . { d1 where d1 is Element of D : for x being set st x in rng h holds
( x <> d1 & [x,d1] in R ) } & dom h = A ) by A78; :: thesis: for A being Ordinal
for L1 being Sequence st A in A & L1 = h | A holds
h . A = g . { d1 where d1 is Element of D : for x being set st x in rng L1 holds
( x <> d1 & [x,d1] in R ) }
let B be Ordinal; :: thesis: for L1 being Sequence st B in A & L1 = h | B holds
h . B = g . { d1 where d1 is Element of D : for x being set st x in rng L1 holds
( x <> d1 & [x,d1] in R ) }
let L be Sequence; :: thesis: ( B in A & L = h | B implies h . B = g . { d1 where d1 is Element of D : for x being set st x in rng L holds
( x <> d1 & [x,d1] in R ) } )
assume that
A81: B in A and
A82: L = h | B ; :: thesis: h . B = g . { d1 where d1 is Element of D : for x being set st x in rng L holds
( x <> d1 & [x,d1] in R ) }
ex C being Ordinal st
( B = C & S2[C,h . B] ) by A78, A81;
then consider L1 being Sequence such that
A83: h . B = g . { d1 where d1 is Element of D : for x being set st x in rng L1 holds
( x <> d1 & [x,d1] in R ) } and
A84: ( dom L1 = B & ( for C being Ordinal
for L being Sequence st C in B & L = L1 | C holds
L1 . C = g . { d1 where d1 is Element of D : for x being set st x in rng L holds
( x <> d1 & [x,d1] in R ) } ) ) ;
A85: for x being object st x in B holds
L1 . x = (h | B) . x
proof
let x be object ; :: thesis: ( x in B implies L1 . x = (h | B) . x )
assume A86: x in B ; :: thesis: L1 . x = (h | B) . x
then reconsider A1 = x as Ordinal ;
A87: (h | B) . x = h . x by A86, FUNCT_1:49;
A88: S2[A1,L1 . x]
proof
reconsider K = L1 | A1 as Sequence ;
take K ; :: thesis: ( L1 . x = g . { d where d is Element of D : for x being set st x in rng K holds
( x <> d & [x,d] in R ) } & dom K = A1 & ( for A being Ordinal
for L1 being Sequence st A in A1 & L1 = K | A holds
K . A = g . { d1 where d1 is Element of D : for x being set st x in rng L1 holds
( x <> d1 & [x,d1] in R ) } ) )
thus L1 . x = g . { d1 where d1 is Element of D : for x being set st x in rng K holds
( x <> d1 & [x,d1] in R ) } by A84, A86; :: thesis: ( dom K = A1 & ( for A being Ordinal
for L1 being Sequence st A in A1 & L1 = K | A holds
K . A = g . { d1 where d1 is Element of D : for x being set st x in rng L1 holds
( x <> d1 & [x,d1] in R ) } ) )
A1 c= B by A86, ORDINAL1:def 2;
hence dom K = A1 by A84, RELAT_1:62; :: thesis: for A being Ordinal
for L1 being Sequence st A in A1 & L1 = K | A holds
K . A = g . { d1 where d1 is Element of D : for x being set st x in rng L1 holds
( x <> d1 & [x,d1] in R ) }
let A2 be Ordinal; :: thesis: for L1 being Sequence st A2 in A1 & L1 = K | A2 holds
K . A2 = g . { d1 where d1 is Element of D : for x being set st x in rng L1 holds
( x <> d1 & [x,d1] in R ) }
let L2 be Sequence; :: thesis: ( A2 in A1 & L2 = K | A2 implies K . A2 = g . { d1 where d1 is Element of D : for x being set st x in rng L2 holds
( x <> d1 & [x,d1] in R ) } )
assume that
A89: A2 in A1 and
A90: L2 = K | A2 ; :: thesis: K . A2 = g . { d1 where d1 is Element of D : for x being set st x in rng L2 holds
( x <> d1 & [x,d1] in R ) }
A2 c= A1 by A89, ORDINAL1:def 2;
then A91: L2 = L1 | A2 by A90, FUNCT_1:51;
K . A2 = L1 . A2 by A89, FUNCT_1:49;
hence K . A2 = g . { d1 where d1 is Element of D : for x being set st x in rng L2 holds
( x <> d1 & [x,d1] in R ) } by A84, A86, A89, A91, ORDINAL1:10; :: thesis: verum
end;
ex A2 being Ordinal st
( x = A2 & S2[A2,h . x] ) by A78, A81, A86, ORDINAL1:10;
hence L1 . x = (h | B) . x by A11, A88, A87; :: thesis: verum
end;
B c= A by A81, ORDINAL1:def 2;
then dom (h | B) = B by A78, RELAT_1:62;
then h | B = L1 by A84, A85, FUNCT_1:2;
hence h . B = g . { d1 where d1 is Element of D : for x being set st x in rng L holds
( x <> d1 & [x,d1] in R ) } by A82, A83; :: thesis: verum
end;
then { d1 where d1 is Element of D : for x being set st x in rng h holds
( x <> d1 & [x,d1] in R ) } <> {} by A32, A71;
then g . { d1 where d1 is Element of D : for x being set st x in rng h holds
( x <> d1 & [x,d1] in R ) } in { d1 where d1 is Element of D : for x being set st x in rng h holds
( x <> d1 & [x,d1] in R ) } by A28, A79;
then reconsider dd = g . { d1 where d1 is Element of D : for x being set st x in rng h holds
( x <> d1 & [x,d1] in R ) } as Element of D by A79;
take dd ; :: thesis: S2[A,dd]
thus S2[A,dd] by A80; :: thesis: verum
end;
A92: for A being Ordinal holds S5[A] from ORDINAL1:sch 2(A72);
 A93: for x, y, z being object st S4[x,y] & S4[x,z] holds
y = z
proof
let x, y, z be object ; :: thesis: ( S4[x,y] & S4[x,z] implies y = z )
given A1 being Ordinal such that A94: y = A1 and
A95: S2[A1,x] ; :: thesis: ( not S4[x,z] or y = z )
consider d1 being Element of D such that
A96: S2[A1,d1] by A92;
given A2 being Ordinal such that A97: z = A2 and
A98: S2[A2,x] ; :: thesis: y = z
d1 = x by A11, A95, A96;
hence y = z by A48, A94, A95, A97, A98; :: thesis: verum
end;
consider X being set such that
A99: for x being object holds
( x in X iff ex y being object st
( y in D & S4[y,x] ) ) from TARSKI:sch 1(A93);
 for A being Ordinal holds A in X
proof
let A be Ordinal; :: thesis: A in X
ex d being Element of D st S2[A,d] by A92;
hence A in X by A99; :: thesis: verum
end;
hence contradiction by ORDINAL1:26; :: thesis: verum
end;
consider A being Ordinal such that
A100: ( S3[A] & ( for B being Ordinal st S3[B] holds
A c= B ) ) from ORDINAL1:sch 1(A70);
 A101: for L being Sequence holds { d where d is Element of D : for x being set st x in rng L holds
( x <> d & [x,d] in R ) } c= D
proof
let L be Sequence; :: thesis: { d where d is Element of D : for x being set st x in rng L holds
( x <> d & [x,d] in R ) } c= D
let x be object ; :: according to TARSKI:def 3 :: thesis: ( not x in { d where d is Element of D : for x being set st x in rng L holds
( x <> d & [x,d] in R ) } or x in D )
assume x in { d where d is Element of D : for x being set st x in rng L holds
( x <> d & [x,d] in R ) } ; :: thesis: x in D
then ex d1 being Element of D st
( x = d1 & ( for x being set st x in rng L holds
( x <> d1 & [x,d1] in R ) ) ) ;
hence x in D ; :: thesis: verum
end;
D in bool D by ZFMISC_1:def 1;
then reconsider d = g . D as Element of D by A28;
A102: ( d in D & S2[ {} ,d] )
proof
deffunc H1( set ) -> set = {} ;
thus d in D ; :: thesis: S2[ {} ,d]
consider L being Sequence such that
A103: ( dom L = {} & ( for B being Ordinal
for L1 being Sequence st B in {} & L1 = L | B holds
L . B = H1(L1) ) ) from ORDINAL1:sch 4();
 take L ; :: thesis: ( d = g . { d where d is Element of D : for x being set st x in rng L holds
( x <> d & [x,d] in R ) } & dom L = {} & ( for A being Ordinal
for L1 being Sequence st A in {} & L1 = L | A holds
L . A = g . { d1 where d1 is Element of D : for x being set st x in rng L1 holds
( x <> d1 & [x,d1] in R ) } ) )
A104: D c= { d1 where d1 is Element of D : for x being set st x in rng L holds
( x <> d1 & [x,d1] in R ) }
proof
let x be object ; :: according to TARSKI:def 3 :: thesis: ( not x in D or x in { d1 where d1 is Element of D : for x being set st x in rng L holds
( x <> d1 & [x,d1] in R ) } )
assume x in D ; :: thesis: x in { d1 where d1 is Element of D : for x being set st x in rng L holds
( x <> d1 & [x,d1] in R ) }
then reconsider d = x as Element of D ;
for x being set st x in rng L holds
( x <> d & [x,d] in R ) by A103, RELAT_1:42;
hence x in { d1 where d1 is Element of D : for x being set st x in rng L holds
( x <> d1 & [x,d1] in R ) } ; :: thesis: verum
end;
{ d1 where d1 is Element of D : for x being set st x in rng L holds
( x <> d1 & [x,d1] in R ) } c= D by A101;
hence d = g . { d1 where d1 is Element of D : for x being set st x in rng L holds
( x <> d1 & [x,d1] in R ) } by A104, XBOOLE_0:def 10; :: thesis: ( dom L = {} & ( for A being Ordinal
for L1 being Sequence st A in {} & L1 = L | A holds
L . A = g . { d1 where d1 is Element of D : for x being set st x in rng L1 holds
( x <> d1 & [x,d1] in R ) } ) )
thus dom L = {} by A103; :: thesis: for A being Ordinal
for L1 being Sequence st A in {} & L1 = L | A holds
L . A = g . { d1 where d1 is Element of D : for x being set st x in rng L1 holds
( x <> d1 & [x,d1] in R ) }
thus for A being Ordinal
for L1 being Sequence st A in {} & L1 = L | A holds
L . A = g . { d1 where d1 is Element of D : for x being set st x in rng L1 holds
( x <> d1 & [x,d1] in R ) } ; :: thesis: verum
end;
A105: {} c= A ;
defpred S4[ object ] means ex B being Ordinal st
( B in A & S2[B,$1] );
consider X being set such that
A106: for x being object holds
( x in X iff ( x in D & S4[x] ) ) from XBOOLE_0:sch 1();
 for Y being set holds not Y in Y ;
then d <> D ;
then {} <> A by A11, A100, A102;
then {} c< A by A105;
then {} in A by ORDINAL1:11;
then reconsider X = X as non empty set by A106, A102;
consider L being Sequence such that
A107: D = g . { d1 where d1 is Element of D : for x being set st x in rng L holds
( x <> d1 & [x,d1] in R ) } and
A108: ( dom L = A & ( for B being Ordinal
for L1 being Sequence st B in A & L1 = L | B holds
L . B = g . { d2 where d2 is Element of D : for x being set st x in rng L1 holds
( x <> d2 & [x,d2] in R ) } ) ) by A100;
R is transitive by A2, A4;
then A109: R |_2 X is transitive by WELLORD1:17;
A110: rng L c= X
proof
let z be object ; :: according to TARSKI:def 3 :: thesis: ( not z in rng L or z in X )
assume z in rng L ; :: thesis: z in X
then consider y being object such that
A111: y in dom L and
A112: z = L . y by FUNCT_1:def 3;
reconsider y = y as Ordinal by A111;
set Z = { d2 where d2 is Element of D : for x being set st x in rng (L | y) holds
( x <> d2 & [x,d2] in R ) } ;
A113: { d2 where d2 is Element of D : for x being set st x in rng (L | y) holds
( x <> d2 & [x,d2] in R ) } c= D by A101;
A114: S2[y,z]
proof
reconsider K = L | y as Sequence ;
take K ; :: thesis: ( z = g . { d where d is Element of D : for x being set st x in rng K holds
( x <> d & [x,d] in R ) } & dom K = y & ( for A being Ordinal
for L1 being Sequence st A in y & L1 = K | A holds
K . A = g . { d1 where d1 is Element of D : for x being set st x in rng L1 holds
( x <> d1 & [x,d1] in R ) } ) )
thus z = g . { d2 where d2 is Element of D : for x being set st x in rng K holds
( x <> d2 & [x,d2] in R ) } by A108, A111, A112; :: thesis: ( dom K = y & ( for A being Ordinal
for L1 being Sequence st A in y & L1 = K | A holds
K . A = g . { d1 where d1 is Element of D : for x being set st x in rng L1 holds
( x <> d1 & [x,d1] in R ) } ) )
y c= dom L by A111, ORDINAL1:def 2;
hence A115: dom K = y by RELAT_1:62; :: thesis: for A being Ordinal
for L1 being Sequence st A in y & L1 = K | A holds
K . A = g . { d1 where d1 is Element of D : for x being set st x in rng L1 holds
( x <> d1 & [x,d1] in R ) }
let B be Ordinal; :: thesis: for L1 being Sequence st B in y & L1 = K | B holds
K . B = g . { d1 where d1 is Element of D : for x being set st x in rng L1 holds
( x <> d1 & [x,d1] in R ) }
let L1 be Sequence; :: thesis: ( B in y & L1 = K | B implies K . B = g . { d1 where d1 is Element of D : for x being set st x in rng L1 holds
( x <> d1 & [x,d1] in R ) } )
assume that
A116: B in y and
A117: L1 = K | B ; :: thesis: K . B = g . { d1 where d1 is Element of D : for x being set st x in rng L1 holds
( x <> d1 & [x,d1] in R ) }
B c= y by A116, ORDINAL1:def 2;
then A118: L1 = L | B by A117, FUNCT_1:51;
K . B = L . B by A115, A116, FUNCT_1:47;
hence K . B = g . { d1 where d1 is Element of D : for x being set st x in rng L1 holds
( x <> d1 & [x,d1] in R ) } by A108, A111, A116, A118, ORDINAL1:10; :: thesis: verum
end;
now :: thesis: not { d2 where d2 is Element of D : for x being set st x in rng (L | y) holds
( x <> d2 & [x,d2] in R ) } = {}
assume { d2 where d2 is Element of D : for x being set st x in rng (L | y) holds
( x <> d2 & [x,d2] in R ) } = {} ; :: thesis: contradiction
then z = D by A32, A108, A111, A112;
then dom L c= y by A100, A108, A114;
hence contradiction by A111, ORDINAL1:5; :: thesis: verum
end;
then g . { d2 where d2 is Element of D : for x being set st x in rng (L | y) holds
( x <> d2 & [x,d2] in R ) } in { d2 where d2 is Element of D : for x being set st x in rng (L | y) holds
( x <> d2 & [x,d2] in R ) } by A28, A113;
then z in { d2 where d2 is Element of D : for x being set st x in rng (L | y) holds
( x <> d2 & [x,d2] in R ) } by A108, A111, A112;
hence z in X by A106, A108, A111, A114, A113; :: thesis: verum
end;
A119: R |_2 X is connected
proof
let x, y be object ; :: according to RELAT_2:def 6,RELAT_2:def 14 :: thesis: ( not x in field (R |_2 X) or not y in field (R |_2 X) or x = y or [x,y] in R |_2 X or [y,x] in R |_2 X )
assume that
A120: x in field (R |_2 X) and
A121: y in field (R |_2 X) ; :: thesis: ( x = y or [x,y] in R |_2 X or [y,x] in R |_2 X )
A122: x in X by A120, WELLORD1:12;
then consider A1 being Ordinal such that
A1 in A and
A123: S2[A1,x] by A106;
A124: y in X by A121, WELLORD1:12;
then consider A2 being Ordinal such that
A2 in A and
A125: S2[A2,y] by A106;
reconsider x9 = x, y9 = y as Element of D by A106, A122, A124;
consider L1 being Sequence such that
A126: x9 = g . { d1 where d1 is Element of D : for x being set st x in rng L1 holds
( x <> d1 & [x,d1] in R ) } and
A127: ( dom L1 = A1 & ( for C being Ordinal
for L being Sequence st C in A1 & L = L1 | C holds
L1 . C = g . { d2 where d2 is Element of D : for x being set st x in rng L holds
( x <> d2 & [x,d2] in R ) } ) ) by A123;
consider L2 being Sequence such that
A128: y9 = g . { d1 where d1 is Element of D : for x being set st x in rng L2 holds
( x <> d1 & [x,d1] in R ) } and
A129: ( dom L2 = A2 & ( for C being Ordinal
for L being Sequence st C in A2 & L = L2 | C holds
L2 . C = g . { d2 where d2 is Element of D : for x being set st x in rng L holds
( x <> d2 & [x,d2] in R ) } ) ) by A125;
A130: [x,y] in [:X,X:] by A122, A124, ZFMISC_1:87;
A131: now :: thesis: ( A1 in A2 & not x = y & not [x,y] in R |_2 X implies [y,x] in R |_2 X )
set Y = { d1 where d1 is Element of D : for x being set st x in rng L2 holds
( x <> d1 & [x,d1] in R ) } ;
set Z = { d1 where d1 is Element of D : for x being set st x in rng (L2 | A1) holds
( x <> d1 & [x,d1] in R ) } ;
not y9 in y9 ;
then A132: { d1 where d1 is Element of D : for x being set st x in rng L2 holds
( x <> d1 & [x,d1] in R ) } <> {} by A32, A128;
{ d1 where d1 is Element of D : for x being set st x in rng L2 holds
( x <> d1 & [x,d1] in R ) } c= D by A101;
then y9 in { d1 where d1 is Element of D : for x being set st x in rng L2 holds
( x <> d1 & [x,d1] in R ) } by A28, A128, A132;
then A133: ex d1 being Element of D st
( y9 = d1 & ( for x being set st x in rng L2 holds
( x <> d1 & [x,d1] in R ) ) ) ;
assume A134: A1 in A2 ; :: thesis: ( x = y or [x,y] in R |_2 X or [y,x] in R |_2 X )
then A1 c= A2 by ORDINAL1:def 2;
then A135: L2 | A1 = L1 | A1 by A33, A127, A129
.= L1 by A127 ;
L2 . A1 = g . { d1 where d1 is Element of D : for x being set st x in rng (L2 | A1) holds
( x <> d1 & [x,d1] in R ) } by A129, A134;
then x9 in rng L2 by A126, A129, A134, A135, FUNCT_1:def 3;
then [x,y] in R by A133;
hence ( x = y or [x,y] in R |_2 X or [y,x] in R |_2 X ) by A130, XBOOLE_0:def 4; :: thesis: verum
end;
A136: [y,x] in [:X,X:] by A122, A124, ZFMISC_1:87;
A137: now :: thesis: ( A2 in A1 & not x = y & not [x,y] in R |_2 X implies [y,x] in R |_2 X )
set Y = { d1 where d1 is Element of D : for x being set st x in rng L1 holds
( x <> d1 & [x,d1] in R ) } ;
set Z = { d1 where d1 is Element of D : for x being set st x in rng (L1 | A2) holds
( x <> d1 & [x,d1] in R ) } ;
for d1 being Element of D holds not d1 in d1 ;
then A138: { d1 where d1 is Element of D : for x being set st x in rng L1 holds
( x <> d1 & [x,d1] in R ) } <> {} by A32, A126;
{ d1 where d1 is Element of D : for x being set st x in rng L1 holds
( x <> d1 & [x,d1] in R ) } c= D by A101;
then x9 in { d1 where d1 is Element of D : for x being set st x in rng L1 holds
( x <> d1 & [x,d1] in R ) } by A28, A126, A138;
then A139: ex d1 being Element of D st
( x9 = d1 & ( for x being set st x in rng L1 holds
( x <> d1 & [x,d1] in R ) ) ) ;
assume A140: A2 in A1 ; :: thesis: ( x = y or [x,y] in R |_2 X or [y,x] in R |_2 X )
then A2 c= A1 by ORDINAL1:def 2;
then A141: L1 | A2 = L2 | A2 by A33, A127, A129
.= L2 by A129 ;
L1 . A2 = g . { d1 where d1 is Element of D : for x being set st x in rng (L1 | A2) holds
( x <> d1 & [x,d1] in R ) } by A127, A140;
then y9 in rng L1 by A127, A128, A140, A141, FUNCT_1:def 3;
then [y,x] in R by A139;
hence ( x = y or [x,y] in R |_2 X or [y,x] in R |_2 X ) by A136, XBOOLE_0:def 4; :: thesis: verum
end;
( A1 = A2 & not x = y & not [x,y] in R |_2 X implies [y,x] in R |_2 X ) by A11, A123, A125;
hence ( x = y or [x,y] in R |_2 X or [y,x] in R |_2 X ) by A131, A137, ORDINAL1:14; :: thesis: verum
end;
R is antisymmetric by A3, A4;
then A142: R |_2 X is antisymmetric ;
set Z = { d1 where d1 is Element of D : for x being set st x in rng L holds
( x <> d1 & [x,d1] in R ) } ;
A143: X c= D by A106;
R is reflexive by A1, A4;
then R |_2 X is reflexive by WELLORD1:15;
then R |_2 X is being_linear-order by A109, A142, A119;
then consider x being set such that
A144: x in D and
A145: for y being set st y in X holds
[y,x] in R by A5, A6, A143;
take x ; :: thesis: x is_maximal_in R
thus x in field R by A4, A6, A144; :: according to ORDERS_1:def 12 :: thesis: for y being set holds
( not y in field R or not y <> x or not [x,y] in R )
let y be set ; :: thesis: ( not y in field R or not y <> x or not [x,y] in R )
assume that
A146: y in field R and
A147: y <> x and
A148: [x,y] in R ; :: thesis: contradiction
reconsider y9 = y as Element of D by A4, A6, A146;
A149: now :: thesis: not y in X
assume y in X ; :: thesis: contradiction
then [y,x] in R by A145;
hence contradiction by A3, A4, A6, A144, A146, A147, A148; :: thesis: verum
end;
now :: thesis: for z being set st z in rng L holds
( z <> y9 & [z,y] in R )
let z be set ; :: thesis: ( z in rng L implies ( z <> y9 & [z,y] in R ) )
assume A150: z in rng L ; :: thesis: ( z <> y9 & [z,y] in R )
then reconsider z9 = z as Element of X by A110;
thus z <> y9 by A110, A149, A150; :: thesis: [z,y] in R
A151: [z9,x] in R by A145;
z in D by A106, A110, A150;
hence [z,y] in R by A2, A4, A6, A144, A146, A148, A151; :: thesis: verum
end;
then A152: y in { d1 where d1 is Element of D : for x being set st x in rng L holds
( x <> d1 & [x,d1] in R ) } ;
{ d1 where d1 is Element of D : for x being set st x in rng L holds
( x <> d1 & [x,d1] in R ) } c= D by A101;
hence contradiction by A28, A107, A152, ORDINAL1:5; :: thesis: verum