:: Morphisms Into Chains, Part {I} :: by Artur Korni{\l}owicz :: :: Received February 6, 2003 :: Copyright (c) 2003-2012 Association of Mizar Users begin Lm1: for x, y, X being set holds ( not y in {x} \/ X or y = x or y in X ) proofend; begin registration let L be RelStr ; cluster Relation-like the carrier of L -defined the carrier of L -valued auxiliary(i) for Element of bool [: the carrier of L, the carrier of L:]; existence ex b1 being Relation of L st b1 is auxiliary(i) proofend; end; registration let L be transitive RelStr ; cluster Relation-like the carrier of L -defined the carrier of L -valued auxiliary(i) auxiliary(ii) for Element of bool [: the carrier of L, the carrier of L:]; existence ex b1 being Relation of L st ( b1 is auxiliary(i) & b1 is auxiliary(ii) ) proofend; end; registration let L be antisymmetric with_suprema RelStr ; cluster Relation-like the carrier of L -defined the carrier of L -valued auxiliary(iii) for Element of bool [: the carrier of L, the carrier of L:]; existence ex b1 being Relation of L st b1 is auxiliary(iii) proofend; end; registration let L be non empty antisymmetric lower-bounded RelStr ; cluster Relation-like the carrier of L -defined the carrier of L -valued auxiliary(iv) for Element of bool [: the carrier of L, the carrier of L:]; existence ex b1 being Relation of L st b1 is auxiliary(iv) proofend; end; :: Definition 2.1, p. 203 definition let L be non empty RelStr ; let R be Relation of L; attrR is extra-order means :Def1: :: WAYBEL35:def 1 ( R is auxiliary(i) & R is auxiliary(ii) & R is auxiliary(iv) ); end; :: deftheorem Def1 defines extra-order WAYBEL35:def_1_:_ for L being non empty RelStr for R being Relation of L holds ( R is extra-order iff ( R is auxiliary(i) & R is auxiliary(ii) & R is auxiliary(iv) ) ); registration let L be non empty RelStr ; cluster extra-order -> auxiliary(i) auxiliary(ii) auxiliary(iv) for Element of bool [: the carrier of L, the carrier of L:]; coherence for b1 being Relation of L st b1 is extra-order holds ( b1 is auxiliary(i) & b1 is auxiliary(ii) & b1 is auxiliary(iv) ) by Def1; cluster auxiliary(i) auxiliary(ii) auxiliary(iv) -> extra-order for Element of bool [: the carrier of L, the carrier of L:]; coherence for b1 being Relation of L st b1 is auxiliary(i) & b1 is auxiliary(ii) & b1 is auxiliary(iv) holds b1 is extra-order by Def1; end; registration let L be non empty RelStr ; cluster auxiliary(iii) extra-order -> auxiliary for Element of bool [: the carrier of L, the carrier of L:]; coherence for b1 being Relation of L st b1 is extra-order & b1 is auxiliary(iii) holds b1 is auxiliary ; cluster auxiliary -> extra-order for Element of bool [: the carrier of L, the carrier of L:]; coherence for b1 being Relation of L st b1 is auxiliary holds b1 is extra-order ; end; registration let L be non empty transitive antisymmetric lower-bounded RelStr ; cluster Relation-like the carrier of L -defined the carrier of L -valued extra-order for Element of bool [: the carrier of L, the carrier of L:]; existence ex b1 being Relation of L st b1 is extra-order proofend; end; definition let L be lower-bounded with_suprema Poset; let R be auxiliary(ii) Relation of L; funcR -LowerMap -> Function of L,(InclPoset (LOWER L)) means :Def2: :: WAYBEL35:def 2 for x being Element of L holds it . x = R -below x; existence ex b1 being Function of L,(InclPoset (LOWER L)) st for x being Element of L holds b1 . x = R -below x proofend; uniqueness for b1, b2 being Function of L,(InclPoset (LOWER L)) st ( for x being Element of L holds b1 . x = R -below x ) & ( for x being Element of L holds b2 . x = R -below x ) holds b1 = b2 proofend; end; :: deftheorem Def2 defines -LowerMap WAYBEL35:def_2_:_ for L being lower-bounded with_suprema Poset for R being auxiliary(ii) Relation of L for b3 being Function of L,(InclPoset (LOWER L)) holds ( b3 = R -LowerMap iff for x being Element of L holds b3 . x = R -below x ); registration let L be lower-bounded with_suprema Poset; let R be auxiliary(ii) Relation of L; clusterR -LowerMap -> monotone ; coherence R -LowerMap is monotone proofend; end; definition let L be 1-sorted ; let R be Relation of the carrier of L; mode strict_chain of R -> Subset of L means :Def3: :: WAYBEL35:def 3 for x, y being set st x in it & y in it & not [x,y] in R & not x = y holds [y,x] in R; existence ex b1 being Subset of L st for x, y being set st x in b1 & y in b1 & not [x,y] in R & not x = y holds [y,x] in R proofend; end; :: deftheorem Def3 defines strict_chain WAYBEL35:def_3_:_ for L being 1-sorted for R being Relation of the carrier of L for b3 being Subset of L holds ( b3 is strict_chain of R iff for x, y being set st x in b3 & y in b3 & not [x,y] in R & not x = y holds [y,x] in R ); theorem Th1: :: WAYBEL35:1 for L being 1-sorted for C being trivial Subset of L for R being Relation of the carrier of L holds C is strict_chain of R proofend; registration let L be non empty 1-sorted ; let R be Relation of the carrier of L; cluster1 -element for strict_chain of R; existence ex b1 being strict_chain of R st b1 is 1 -element proofend; end; theorem Th2: :: WAYBEL35:2 for L being antisymmetric RelStr for R being auxiliary(i) Relation of L for C being strict_chain of R for x, y being Element of L st x in C & y in C & x < y holds [x,y] in R proofend; theorem :: WAYBEL35:3 for L being antisymmetric RelStr for R being auxiliary(i) Relation of L for x, y being Element of L st [x,y] in R & [y,x] in R holds x = y proofend; theorem :: WAYBEL35:4 for L being non empty antisymmetric lower-bounded RelStr for x being Element of L for R being auxiliary(iv) Relation of L holds {(Bottom L),x} is strict_chain of R proofend; theorem Th5: :: WAYBEL35:5 for L being non empty antisymmetric lower-bounded RelStr for R being auxiliary(iv) Relation of L for C being strict_chain of R holds C \/ {(Bottom L)} is strict_chain of R proofend; definition let L be 1-sorted ; let R be Relation of the carrier of L; let C be strict_chain of R; attrC is maximal means :Def4: :: WAYBEL35:def 4 for D being strict_chain of R st C c= D holds C = D; end; :: deftheorem Def4 defines maximal WAYBEL35:def_4_:_ for L being 1-sorted for R being Relation of the carrier of L for C being strict_chain of R holds ( C is maximal iff for D being strict_chain of R st C c= D holds C = D ); definition let L be 1-sorted ; let R be Relation of the carrier of L; let C be set ; defpred S1[ set ] means ( $1 is strict_chain of R & C c= $1 ); func Strict_Chains (R,C) -> set means :Def5: :: WAYBEL35:def 5 for x being set holds ( x in it iff ( x is strict_chain of R & C c= x ) ); existence ex b1 being set st for x being set holds ( x in b1 iff ( x is strict_chain of R & C c= x ) ) proofend; uniqueness for b1, b2 being set st ( for x being set holds ( x in b1 iff ( x is strict_chain of R & C c= x ) ) ) & ( for x being set holds ( x in b2 iff ( x is strict_chain of R & C c= x ) ) ) holds b1 = b2 proofend; end; :: deftheorem Def5 defines Strict_Chains WAYBEL35:def_5_:_ for L being 1-sorted for R being Relation of the carrier of L for C being set for b4 being set holds ( b4 = Strict_Chains (R,C) iff for x being set holds ( x in b4 iff ( x is strict_chain of R & C c= x ) ) ); registration let L be 1-sorted ; let R be Relation of the carrier of L; let C be strict_chain of R; cluster Strict_Chains (R,C) -> non empty ; coherence not Strict_Chains (R,C) is empty by Def5; end; notation let R be Relation; let X be set ; synonym X is_inductive_wrt R for X has_upper_Zorn_property_wrt R; end; :: Lemma 2.2, p. 203 theorem :: WAYBEL35:6 for L being 1-sorted 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 ) ) proofend; :: Lemma 2.3 (ii), p. 203 :: It is a trivial consequence of YELLOW_0:65 :: Maybe to cancel theorem Th7: :: WAYBEL35:7 for L being non empty transitive RelStr for C being non empty Subset of L for X being Subset of C st ex_sup_of X,L & "\/" (X,L) in C holds ( ex_sup_of X, subrelstr C & "\/" (X,L) = "\/" (X,(subrelstr C)) ) proofend; Lm2: for L being non empty Poset for R being auxiliary(i) auxiliary(ii) Relation of L for C being non empty strict_chain of R for X being Subset of C st ex_sup_of X,L & C is maximal & not "\/" (X,L) in C holds ex cs being Element of L st ( cs in C & "\/" (X,L) < cs & not [("\/" (X,L)),cs] in R & ex cs1 being Element of (subrelstr C) st ( cs = cs1 & X is_<=_than cs1 & ( for a being Element of (subrelstr C) st X is_<=_than a holds cs1 <= a ) ) ) proofend; :: Lemma 2.3, p. 203 theorem Th8: :: WAYBEL35:8 for L being non empty Poset for R being auxiliary(i) auxiliary(ii) Relation of L for C being non empty strict_chain of R for X being Subset of C st ex_sup_of X,L & C is maximal holds ex_sup_of X, subrelstr C proofend; :: Lemma 2.3 (i), (iii), p. 203 theorem :: WAYBEL35:9 for L being non empty Poset for R being auxiliary(i) auxiliary(ii) Relation of L for C being non empty strict_chain of R for X being Subset of C st ex_inf_of (uparrow ("\/" (X,L))) /\ C,L & ex_sup_of X,L & C is maximal holds ( "\/" (X,(subrelstr C)) = "/\" (((uparrow ("\/" (X,L))) /\ C),L) & ( not "\/" (X,L) in C implies "\/" (X,L) < "/\" (((uparrow ("\/" (X,L))) /\ C),L) ) ) proofend; :: Proposition 2.4, p. 204 theorem :: WAYBEL35:10 for L being non empty complete Poset for R being auxiliary(i) auxiliary(ii) Relation of L for C being non empty strict_chain of R st C is maximal holds subrelstr C is complete proofend; :: Proposition 2.5 (i), p. 204 theorem :: WAYBEL35:11 for L being non empty antisymmetric lower-bounded RelStr for R being auxiliary(iv) Relation of L for C being strict_chain of R st C is maximal holds Bottom L in C proofend; :: Proposition 2.5 (ii), p. 204 theorem :: WAYBEL35:12 for L being non empty upper-bounded Poset for R being auxiliary(ii) Relation of L for C being strict_chain of R for m being Element of L st C is maximal & m is_maximum_of C & [m,(Top L)] in R holds ( [(Top L),(Top L)] in R & m = Top L ) proofend; :: Definition (SI_C) p. 204 definition let L be RelStr ; let C be set ; let R be Relation of the carrier of L; predR satisfies_SIC_on C means :Def6: :: WAYBEL35:def 6 for x, z being Element of L st x in C & z in C & [x,z] in R & x <> z holds ex y being Element of L st ( y in C & [x,y] in R & [y,z] in R & x <> y ); end; :: deftheorem Def6 defines satisfies_SIC_on WAYBEL35:def_6_:_ for L being RelStr for C being set for R being Relation of the carrier of L holds ( R satisfies_SIC_on C iff for x, z being Element of L st x in C & z in C & [x,z] in R & x <> z holds ex y being Element of L st ( y in C & [x,y] in R & [y,z] in R & x <> y ) ); definition let L be RelStr ; let R be Relation of the carrier of L; let C be strict_chain of R; attrC is satisfying_SIC means :Def7: :: WAYBEL35:def 7 R satisfies_SIC_on C; end; :: deftheorem Def7 defines satisfying_SIC WAYBEL35:def_7_:_ for L being RelStr for R being Relation of the carrier of L for C being strict_chain of R holds ( C is satisfying_SIC iff R satisfies_SIC_on C ); theorem Th13: :: WAYBEL35:13 for L being RelStr for C being set for R being auxiliary(i) Relation of L st R satisfies_SIC_on C holds for x, z being Element of L st x in C & z in C & [x,z] in R & x <> z holds ex y being Element of L st ( y in C & [x,y] in R & [y,z] in R & x < y ) proofend; registration let L be RelStr ; let R be Relation of the carrier of L; cluster trivial -> satisfying_SIC for strict_chain of R; coherence for b1 being strict_chain of R st b1 is trivial holds b1 is satisfying_SIC proofend; end; registration let L be non empty RelStr ; let R be Relation of the carrier of L; cluster1 -element for strict_chain of R; existence ex b1 being strict_chain of R st b1 is 1 -element proofend; end; :: Proposition 2.5 (iii), p. 204 theorem :: WAYBEL35:14 for L being lower-bounded with_suprema Poset for R being auxiliary(i) auxiliary(ii) Relation of L for C being strict_chain of R st C is maximal & R is satisfying_SI holds R satisfies_SIC_on C proofend; definition let R be Relation; let C, y be set ; func SetBelow (R,C,y) -> set equals :: WAYBEL35:def 8 (R " {y}) /\ C; coherence (R " {y}) /\ C is set ; end; :: deftheorem defines SetBelow WAYBEL35:def_8_:_ for R being Relation for C, y being set holds SetBelow (R,C,y) = (R " {y}) /\ C; theorem Th15: :: WAYBEL35:15 for R being Relation for C, x, y being set holds ( x in SetBelow (R,C,y) iff ( [x,y] in R & x in C ) ) proofend; definition let L be 1-sorted ; let R be Relation of the carrier of L; let C, y be set ; :: original:SetBelow redefine func SetBelow (R,C,y) -> Subset of L; coherence SetBelow (R,C,y) is Subset of L proofend; end; theorem Th16: :: WAYBEL35:16 for L being RelStr for R being auxiliary(i) Relation of L for C being set for y being Element of L holds SetBelow (R,C,y) is_<=_than y proofend; theorem Th17: :: WAYBEL35:17 for L being reflexive transitive RelStr for R being auxiliary(ii) Relation of L for C being Subset of L for x, y being Element of L st x <= y holds SetBelow (R,C,x) c= SetBelow (R,C,y) proofend; theorem Th18: :: WAYBEL35:18 for L being RelStr for R being auxiliary(i) Relation of L for C being set for x being Element of L st x in C & [x,x] in R & ex_sup_of SetBelow (R,C,x),L holds x = sup (SetBelow (R,C,x)) proofend; definition let L be RelStr ; let C be Subset of L; attrC is sup-closed means :Def9: :: WAYBEL35:def 9 for X being Subset of C st ex_sup_of X,L holds "\/" (X,L) = "\/" (X,(subrelstr C)); end; :: deftheorem Def9 defines sup-closed WAYBEL35:def_9_:_ for L being RelStr for C being Subset of L holds ( C is sup-closed iff for X being Subset of C st ex_sup_of X,L holds "\/" (X,L) = "\/" (X,(subrelstr C)) ); :: Lemma 2.6, p. 205 theorem Th19: :: WAYBEL35:19 for L being non empty complete Poset for R being extra-order Relation of L for C being satisfying_SIC strict_chain of R for p, q being Element of L st p in C & q in C & p < q holds ex y being Element of L st ( p < y & [y,q] in R & y = sup (SetBelow (R,C,y)) ) proofend; :: Lemma 2.7, p. 205, 1 => 2 theorem :: WAYBEL35:20 for L being non empty lower-bounded Poset for R being extra-order Relation of L for C being non empty strict_chain of R st C is sup-closed & ( for c being Element of L st c in C holds ex_sup_of SetBelow (R,C,c),L ) & R satisfies_SIC_on C holds for c being Element of L st c in C holds c = sup (SetBelow (R,C,c)) proofend; :: Lemma 2.7, p. 205, 2 => 1 theorem :: WAYBEL35:21 for L being non empty reflexive antisymmetric RelStr for R being auxiliary(i) Relation of L for C being strict_chain of R st ( for c being Element of L st c in C holds ( ex_sup_of SetBelow (R,C,c),L & c = sup (SetBelow (R,C,c)) ) ) holds R satisfies_SIC_on C proofend; definition let L be non empty RelStr ; let R be Relation of the carrier of L; let C be set ; defpred S1[ set ] means $1 = sup (SetBelow (R,C,$1)); func SupBelow (R,C) -> set means :Def10: :: WAYBEL35:def 10 for y being set holds ( y in it iff y = sup (SetBelow (R,C,y)) ); existence ex b1 being set st for y being set holds ( y in b1 iff y = sup (SetBelow (R,C,y)) ) proofend; uniqueness for b1, b2 being set st ( for y being set holds ( y in b1 iff y = sup (SetBelow (R,C,y)) ) ) & ( for y being set holds ( y in b2 iff y = sup (SetBelow (R,C,y)) ) ) holds b1 = b2 proofend; end; :: deftheorem Def10 defines SupBelow WAYBEL35:def_10_:_ for L being non empty RelStr for R being Relation of the carrier of L for C being set for b4 being set holds ( b4 = SupBelow (R,C) iff for y being set holds ( y in b4 iff y = sup (SetBelow (R,C,y)) ) ); definition let L be non empty RelStr ; let R be Relation of the carrier of L; let C be set ; :: original:SupBelow redefine func SupBelow (R,C) -> Subset of L; coherence SupBelow (R,C) is Subset of L proofend; end; :: Lemma 2.8, (i) a), p. 205 theorem Th22: :: WAYBEL35:22 for L being non empty reflexive transitive RelStr for R being auxiliary(i) auxiliary(ii) Relation of L for C being strict_chain of R st ( for c being Element of L holds ex_sup_of SetBelow (R,C,c),L ) holds SupBelow (R,C) is strict_chain of R proofend; :: Lemma 2.8, (i) b), p. 205 theorem :: WAYBEL35:23 for L being non empty Poset for R being auxiliary(i) auxiliary(ii) Relation of L for C being Subset of L st ( for c being Element of L holds ex_sup_of SetBelow (R,C,c),L ) holds SupBelow (R,C) is sup-closed proofend; theorem Th24: :: WAYBEL35:24 for L being non empty complete Poset for R being extra-order Relation of L for C being satisfying_SIC strict_chain of R for d being Element of L st d in SupBelow (R,C) holds d = "\/" ( { b where b is Element of L : ( b in SupBelow (R,C) & [b,d] in R ) } ,L) proofend; :: Lemma 2.8, (ii), p. 205 theorem :: WAYBEL35:25 for L being non empty complete Poset for R being extra-order Relation of L for C being satisfying_SIC strict_chain of R holds R satisfies_SIC_on SupBelow (R,C) proofend; :: Lemma 2.8, (iii), p. 205 theorem :: WAYBEL35:26 for L being non empty complete Poset for R being extra-order Relation of L for C being satisfying_SIC strict_chain of R for a, b being Element of L st a in C & b in C & a < b holds ex d being Element of L st ( d in SupBelow (R,C) & a < d & [d,b] in R ) proofend;