let L be 1-sorted ; :: thesis: for R being Relation of the carrier of L
for C being strict_chain of R holds
( Strict_Chains (R,C) is_inductive_wrt RelIncl (Strict_Chains (R,C)) & ex D being set st
( D is_maximal_in RelIncl (Strict_Chains (R,C)) & C c= D ) )
let R be Relation of the carrier of L; :: thesis: for C being strict_chain of R holds
( Strict_Chains (R,C) is_inductive_wrt RelIncl (Strict_Chains (R,C)) & ex D being set st
( D is_maximal_in RelIncl (Strict_Chains (R,C)) & C c= D ) )
let C be strict_chain of R; :: thesis: ( Strict_Chains (R,C) is_inductive_wrt RelIncl (Strict_Chains (R,C)) & ex D being set st
( D is_maximal_in RelIncl (Strict_Chains (R,C)) & C c= D ) )
set X = Strict_Chains (R,C);
A1: field (RelIncl (Strict_Chains (R,C))) = Strict_Chains (R,C) by WELLORD2:def 1;
thus A2: Strict_Chains (R,C) is_inductive_wrt RelIncl (Strict_Chains (R,C)) :: thesis: ex D being set st
( D is_maximal_in RelIncl (Strict_Chains (R,C)) & C c= D )
proof
let Y be set ; :: according to ORDERS_1:def 10 :: thesis: ( not Y c= Strict_Chains (R,C) or not (RelIncl (Strict_Chains (R,C))) |_2 Y is being_linear-order or ex b1 being set st
( b1 in Strict_Chains (R,C) & ( for b2 being set holds
( not b2 in Y or [b2,b1] in RelIncl (Strict_Chains (R,C)) ) ) ) )
assume that
A3: Y c= Strict_Chains (R,C) and
A4: (RelIncl (Strict_Chains (R,C))) |_2 Y is being_linear-order ; :: thesis: ex b1 being set st
( b1 in Strict_Chains (R,C) & ( for b2 being set holds
( not b2 in Y or [b2,b1] in RelIncl (Strict_Chains (R,C)) ) ) )
per cases ( Y is empty or not Y is empty ) ;
suppose A5: Y is empty ; :: thesis: ex b1 being set st
( b1 in Strict_Chains (R,C) & ( for b2 being set holds
( not b2 in Y or [b2,b1] in RelIncl (Strict_Chains (R,C)) ) ) )
take C ; :: thesis: ( C in Strict_Chains (R,C) & ( for b1 being set holds
( not b1 in Y or [b1,C] in RelIncl (Strict_Chains (R,C)) ) ) )
thus ( C in Strict_Chains (R,C) & ( for b1 being set holds
( not b1 in Y or [b1,C] in RelIncl (Strict_Chains (R,C)) ) ) ) by A5, Def5; :: thesis: verum
end;
suppose A6: not Y is empty ; :: thesis: ex b1 being set st
( b1 in Strict_Chains (R,C) & ( for b2 being set holds
( not b2 in Y or [b2,b1] in RelIncl (Strict_Chains (R,C)) ) ) )
take Z = union Y; :: thesis: ( Z in Strict_Chains (R,C) & ( for b1 being set holds
( not b1 in Y or [b1,Z] in RelIncl (Strict_Chains (R,C)) ) ) )
Z c= the carrier of L
proof
let z be object ; :: according to TARSKI:def 3 :: thesis: ( not z in Z or z in the carrier of L )
assume z in Z ; :: thesis: z in the carrier of L
then consider A being set such that
A7: z in A and
A8: A in Y by TARSKI:def 4;
A is strict_chain of R by A3, A8, Def5;
hence z in the carrier of L by A7; :: thesis: verum
end;
then reconsider S = Z as Subset of L ;
A9: S is strict_chain of R
proof
(RelIncl (Strict_Chains (R,C))) |_2 Y is connected by A4;
then A10: (RelIncl (Strict_Chains (R,C))) |_2 Y is_connected_in field ((RelIncl (Strict_Chains (R,C))) |_2 Y) by RELAT_2:def 14;
A11: (RelIncl (Strict_Chains (R,C))) |_2 Y = RelIncl Y by A3, WELLORD2:7;
let x, y be set ; :: according to WAYBEL35:def 3 :: thesis: ( x in S & y in S & not [x,y] in R & not x = y implies [y,x] in R )
A12: field (RelIncl Y) = Y by WELLORD2:def 1;
assume x in S ; :: thesis: ( not y in S or [x,y] in R or x = y or [y,x] in R )
then consider A being set such that
A13: x in A and
A14: A in Y by TARSKI:def 4;
A15: A is strict_chain of R by A3, A14, Def5;
assume y in S ; :: thesis: ( [x,y] in R or x = y or [y,x] in R )
then consider B being set such that
A16: y in B and
A17: B in Y by TARSKI:def 4;
A18: B is strict_chain of R by A3, A17, Def5;
per cases ( A <> B or A = B ) ;
suppose A <> B ; :: thesis: ( [x,y] in R or x = y or [y,x] in R )
then ( [A,B] in RelIncl Y or [B,A] in RelIncl Y ) by A14, A17, A10, A11, A12, RELAT_2:def 6;
then ( A c= B or B c= A ) by A14, A17, WELLORD2:def 1;
hence ( [x,y] in R or x = y or [y,x] in R ) by A13, A16, A15, A18, Def3; :: thesis: verum
end;
suppose A = B ; :: thesis: ( [x,y] in R or x = y or [y,x] in R )
hence ( [x,y] in R or x = y or [y,x] in R ) by A13, A16, A15, Def3; :: thesis: verum
end;
end;
end;
C c= Z
proof
let c be object ; :: according to TARSKI:def 3 :: thesis: ( not c in C or c in Z )
assume A19: c in C ; :: thesis: c in Z
consider y being object such that
A20: y in Y by A6;
reconsider y = y as set by TARSKI:1;
C c= y by A3, A20, Def5;
hence c in Z by A19, A20, TARSKI:def 4; :: thesis: verum
end;
hence A21: Z in Strict_Chains (R,C) by A9, Def5; :: thesis: for b1 being set holds
( not b1 in Y or [b1,Z] in RelIncl (Strict_Chains (R,C)) )
let y be set ; :: thesis: ( not y in Y or [y,Z] in RelIncl (Strict_Chains (R,C)) )
assume A22: y in Y ; :: thesis: [y,Z] in RelIncl (Strict_Chains (R,C))
then y c= Z by ZFMISC_1:74;
hence [y,Z] in RelIncl (Strict_Chains (R,C)) by A3, A21, A22, WELLORD2:def 1; :: thesis: verum
end;
end;
end;
A23: RelIncl (Strict_Chains (R,C)) is_transitive_in Strict_Chains (R,C) by WELLORD2:20;
A24: RelIncl (Strict_Chains (R,C)) is_antisymmetric_in Strict_Chains (R,C) by WELLORD2:21;
RelIncl (Strict_Chains (R,C)) is_reflexive_in Strict_Chains (R,C) by WELLORD2:19;
then RelIncl (Strict_Chains (R,C)) partially_orders Strict_Chains (R,C) by A23, A24;
then consider D being set such that
A25: D is_maximal_in RelIncl (Strict_Chains (R,C)) by A1, A2, ORDERS_1:63;
take D ; :: thesis: ( D is_maximal_in RelIncl (Strict_Chains (R,C)) & C c= D )
thus D is_maximal_in RelIncl (Strict_Chains (R,C)) by A25; :: thesis: C c= D
D in field (RelIncl (Strict_Chains (R,C))) by A25;
hence C c= D by A1, Def5; :: thesis: verum