### The Mizar article:

### Partially Ordered Sets

**by****Wojciech A. Trybulec**

- Received August 30, 1989
Copyright (c) 1989 Association of Mizar Users

- MML identifier: ORDERS_1
- [ MML identifier index ]

environ vocabulary FUNCT_1, BOOLE, TARSKI, RELAT_1, MCART_1, RELAT_2, WELLORD1, SUBSET_1, ORDERS_1, PARTFUN1; notation TARSKI, XBOOLE_0, ZFMISC_1, SUBSET_1, RELAT_1, RELAT_2, FUNCT_1, RELSET_1, PARTFUN1, FUNCT_2, MCART_1, WELLORD1, STRUCT_0, PRE_TOPC; constructors RELAT_2, MCART_1, WELLORD1, PRE_TOPC, PARTFUN1, MEMBERED, XBOOLE_0; clusters RELSET_1, STRUCT_0, PRE_TOPC, SUBSET_1, MEMBERED, ZFMISC_1, PARTFUN1, XBOOLE_0; requirements BOOLE, SUBSET; definitions RELAT_2, TARSKI, WELLORD1, STRUCT_0, XBOOLE_0; theorems FUNCT_1, FUNCT_2, MCART_1, RELAT_1, RELAT_2, RELSET_1, TARSKI, WELLORD1, WELLORD2, ZFMISC_1, STRUCT_0, PRE_TOPC, XBOOLE_0, XBOOLE_1, PARTFUN1; schemes FUNCT_1, XBOOLE_0; begin reserve X,Y for set, x,x1,x2,y,y1,y2,z for set, f,g,h for Function; Lm1: (ex X st X <> {} & X in Y) iff union Y <> {} proof thus (ex X st X <> {} & X in Y) implies union Y <> {} proof given X such that A1: X <> {} and A2: X in Y; consider x being Element of X; x in X by A1; hence thesis by A2,TARSKI:def 4; end; consider x being Element of union Y; assume union Y <> {}; then consider X such that A3: x in X & X in Y by TARSKI:def 4; take X; thus thesis by A3; end; :: :: Choice function. :: reserve M for non empty set; definition let M; assume A1: not {} in M; mode Choice_Function of M -> Function of M, union M means :Def1: for X st X in M holds it.X in X; existence proof deffunc F(set)=[:{$1},$1:]; consider f such that A2: dom f = M and A3: for X st X in M holds f.X = F(X) from Lambda; consider x being Element of M; A4: f.x in rng f by A2,FUNCT_1:def 5; A5: x in M; then reconsider N = rng f as non empty set by A2,FUNCT_1:12; A6: now let X; assume X in N; then consider y such that A7: y in dom f & f.y = X by FUNCT_1:def 5; X = [:{y},y:] & y <> {} & {y} <> {} by A1,A2,A3,A7; hence X <> {} by ZFMISC_1:113; end; now let X,Y; assume that A8: X in N and A9: Y in N and A10: X <> Y; consider x such that A11: x in dom f and A12: f.x = X by A8,FUNCT_1:def 5; consider y such that A13: y in dom f and A14: f.y = Y by A9,FUNCT_1:def 5; A15: X = [:{x},x:] & Y = [:{y},y:] by A2,A3,A11,A12,A13,A14; consider z being Element of X /\ Y; assume X meets Y; then X /\ Y <> {} by XBOOLE_0:def 7; then consider x1,x2 such that z = [x1,x2] and A16: x1 in {x} /\ {y} and x2 in x /\ y by A15,ZFMISC_1:104; x1 in {x} & x1 in{y} by A16,XBOOLE_0:def 3; then x1 = x & x1 = y by TARSKI:def 1; hence contradiction by A10,A12,A14; end; then consider Choice being set such that A17: for X st X in N ex x st Choice /\ X = {x} by A6,WELLORD2:27; defpred P[set,set] means $2 in $1 /\ Choice; A18: for X,y1,y2 st X in N & P[X,y1] & P[X,y2] holds y1 = y2 proof let X,y1,y2; assume that A19: X in N and A20: y1 in X /\ Choice & y2 in X /\ Choice; consider x such that A21: {x} = Choice /\ X by A17,A19; x = y1 & x = y2 by A20,A21,TARSKI:def 1; hence y1 = y2; end; A22: for X st X in N ex y st P[X,y] proof let X; assume X in N; then consider x such that A23: Choice /\ X = {x} by A17; take x; thus thesis by A23,TARSKI:def 1; end; consider g such that A24: dom g = N and A25: for X st X in N holds P[X,g.X] from FuncEx(A18,A22); deffunc FF(set)=$1`2; consider h such that A26: dom h = union N and A27: for x st x in union N holds h.x = FF(x) from Lambda; A28: union M <> {} by A1,A5,Lm1; consider x1 such that A29: x1 in N by A4; consider x2 such that A30: x2 in dom f & f.x2 = x1 by A29,FUNCT_1:def 5; x1 = [:{x2},x2:] & x2 <> {} & {x2} <> {} by A1,A2,A3,A30; then x1 <> {} by ZFMISC_1:113; then A31: union N <> {} by A29,Lm1; reconsider f as Function of M,N by A2,FUNCT_2:def 1,RELSET_1:11; rng g c= union N proof let x; assume x in rng g; then consider y such that A32: y in dom g and A33: g.y = x by FUNCT_1: def 5; x in y /\ Choice by A24,A25,A32,A33; then x in y by XBOOLE_0:def 3; hence thesis by A24,A32,TARSKI:def 4; end; then reconsider g as Function of N, union N by A24,A31,FUNCT_2:def 1, RELSET_1:11; rng h c= union M proof let x; assume x in rng h; then consider y such that A34: y in dom h and A35: h.y = x by FUNCT_1: def 5; consider Y such that A36: y in Y and A37: Y in N by A26,A34,TARSKI:def 4; consider z such that A38: z in dom f & f.z = Y by A37,FUNCT_1:def 5; A39: Y = [:{z},z:] by A3,A38; then consider x1,x2 such that A40: y = [x1,x2] by A36,ZFMISC_1:102; x2 in z & x = [x1,x2]`2 by A26,A27,A34,A35,A36,A39,A40,ZFMISC_1:106 ; then x in z by MCART_1:7; hence thesis by A38,TARSKI:def 4; end; then reconsider h as Function of union N, union M by A26,A28,FUNCT_2:def 1, RELSET_1:11; reconsider F = h * (g * f) as Function of M, union M by A31,FUNCT_2:19; A41: dom(g * f) = M by A31,FUNCT_2:def 1; take F; let X; set fX = f.X; assume A42: X in M; then A43: f.X in N by A2,FUNCT_1:def 5; then g.(fX) in fX /\ Choice by A25; then A44: g.(fX) in fX & f.X = [:{X},X:] by A3,A42,XBOOLE_0:def 3; then consider x1,x2 such that A45: [x1,x2] = g.(fX) by ZFMISC_1:102; A46: x2 in X by A44,A45,ZFMISC_1:106; g.(fX) in rng g by A24,A43,FUNCT_1:def 5; then h.(g.fX) = (g.fX)`2 by A27; then A47: h.(g.fX) in X by A45,A46,MCART_1:7; (g * f).X = g.fX by A2,A42,FUNCT_1:23; hence F.X in X by A41,A42,A47,FUNCT_1:23; end; end; reserve D,D1 for non empty set; definition let D be set; func BOOL D -> set equals :Def2: bool D \ {{}}; coherence; end; definition let D; cluster BOOL D -> non empty; coherence proof D in bool D & not D in {{}} by TARSKI:def 1,ZFMISC_1:def 1; then bool D \ {{}} is non empty by XBOOLE_0:def 4; hence thesis by Def2; end; end; canceled 3; theorem Th4: not {} in BOOL D proof assume not thesis; then {} in bool D \ {{}} by Def2; then not {} in {{}} by XBOOLE_0:def 4; hence thesis by TARSKI:def 1; end; theorem Th5: D1 c= D iff D1 in BOOL D proof thus D1 c= D implies D1 in BOOL D proof assume D1 c= D; then D1 in bool D & not D1 in {{}} by TARSKI:def 1; then D1 in bool D \ {{}} by XBOOLE_0:def 4; hence thesis by Def2; end; assume D1 in BOOL D; then D1 in bool D \ {{}} by Def2; then D1 in bool D by XBOOLE_0:def 4; hence thesis; end; theorem D1 is Subset of D iff D1 in BOOL D by Th5; theorem D in BOOL D by Th5; reserve P for Relation; Lm2: P is_strongly_connected_in X iff P is_reflexive_in X & P is_connected_in X proof thus P is_strongly_connected_in X implies P is_reflexive_in X & P is_connected_in X proof assume A1: P is_strongly_connected_in X; thus P is_reflexive_in X proof let x; assume x in X; hence thesis by A1,RELAT_2:def 7; end; let x,y; assume x in X & y in X; hence thesis by A1,RELAT_2:def 7; end; assume that A2: P is_reflexive_in X and A3: P is_connected_in X; let x,y; assume A4: x in X & y in X; then x = y implies thesis by A2,RELAT_2:def 1; hence thesis by A3,A4,RELAT_2:def 6; end; :: :: Orders. :: definition let X; mode Order of X is total reflexive antisymmetric transitive Relation of X; end; reserve O for Order of X; canceled 4; Lm3: for R being total reflexive Relation of X holds field R = X proof let R be total reflexive Relation of X; dom R = X by PARTFUN1:def 4; hence field R = X \/ rng R by RELAT_1:def 6 .= X by XBOOLE_1:12; end; theorem x in X implies [x,x] in O proof field O = X by Lm3; then O is_reflexive_in X by RELAT_2:def 9; hence thesis by RELAT_2:def 1; end; theorem x in X & y in X & [x,y] in O & [y,x] in O implies x = y proof field O = X by Lm3; then O is_antisymmetric_in X by RELAT_2:def 12; hence thesis by RELAT_2:def 4; end; theorem x in X & y in X & z in X & [x,y] in O & [y,z] in O implies [x,z] in O proof field O = X by Lm3; then O is_transitive_in X by RELAT_2:def 16; hence thesis by RELAT_2:def 8; end; :: :: Partially ordered sets. :: definition canceled; struct(1-sorted) RelStr (# carrier -> set, InternalRel -> Relation of the carrier #); end; definition let X be non empty set; let R be Relation of X; cluster RelStr(#X,R#) -> non empty; coherence proof thus the carrier of RelStr(#X,R#) is non empty; end; end; definition let A be RelStr; attr A is reflexive means :Def4: the InternalRel of A is_reflexive_in the carrier of A; attr A is transitive means :Def5: the InternalRel of A is_transitive_in the carrier of A; attr A is antisymmetric means :Def6: the InternalRel of A is_antisymmetric_in the carrier of A; end; definition cluster non empty reflexive transitive antisymmetric strict RelStr; existence proof consider A being non empty set; consider R being Order of A; take L = RelStr(#A,R#); thus the carrier of L is non empty; A1: field R = the carrier of L by Lm3; hence the InternalRel of L is_reflexive_in the carrier of L by RELAT_2:def 9; thus the InternalRel of L is_transitive_in the carrier of L by A1,RELAT_2:def 16; thus the InternalRel of L is_antisymmetric_in the carrier of L by A1,RELAT_2:def 12; thus thesis; end; end; definition mode Poset is reflexive transitive antisymmetric RelStr; end; Lm4: for A being set, R being Relation of A st R is_reflexive_in A holds dom R = A & field R = A proof let A be set, R be Relation of A such that A1: R is_reflexive_in A; A c= dom R proof let x; assume x in A; then [x,x] in R by A1,RELAT_2:def 1; hence x in dom R by RELAT_1:def 4; end; hence dom R = A by XBOOLE_0:def 10; hence field R = A \/ rng R by RELAT_1:def 6 .= A by XBOOLE_1:12; end; definition let A be Poset; cluster the InternalRel of A -> total reflexive antisymmetric transitive; coherence proof set R = the InternalRel of A; A1: R is_reflexive_in the carrier of A by Def4; A2: field R = the carrier of A by A1,Lm4; dom R = the carrier of A by A1,Lm4; hence the InternalRel of A is total by PARTFUN1:def 4; the InternalRel of A is_reflexive_in the carrier of A by Def4; hence the InternalRel of A is reflexive by A2,RELAT_2:def 9; the InternalRel of A is_antisymmetric_in the carrier of A by Def6; hence the InternalRel of A is antisymmetric by A2,RELAT_2:def 12; the InternalRel of A is_transitive_in the carrier of A by Def5; hence the InternalRel of A is transitive by A2,RELAT_2:def 16; end; end; definition let X be set; let O be Order of X; cluster RelStr(#X,O#) -> reflexive transitive antisymmetric; coherence proof set A = RelStr(#X,O#); field O = X by Lm3; hence the InternalRel of A is_reflexive_in the carrier of A & the InternalRel of A is_transitive_in the carrier of A & the InternalRel of A is_antisymmetric_in the carrier of A by RELAT_2:def 9,def 12,def 16; end; end; reserve A for non empty Poset; reserve a,a1,a2,a3,b,c for Element of A; reserve S,T for Subset of A; Lm5: x in S implies x is Element of A; definition let A be RelStr; let a1,a2 be Element of A; canceled 2; pred a1 <= a2 means :Def9: [a1,a2] in the InternalRel of A; synonym a2 >= a1; end; definition let A be RelStr; let a1,a2 be Element of A; pred a1 < a2 means :Def10: a1 <= a2 & a1 <> a2; irreflexivity; synonym a2 > a1; end; canceled 9; theorem Th24: for A being reflexive non empty RelStr, a being Element of A holds a <= a proof let A be reflexive non empty RelStr, a be Element of A; the InternalRel of A is_reflexive_in the carrier of A by Def4; then [a,a] in the InternalRel of A by RELAT_2:def 1; hence thesis by Def9; end; definition let A be reflexive non empty RelStr; let a1,a2 be Element of A; redefine pred a1 <= a2; reflexivity by Th24; end; theorem Th25: for A being antisymmetric RelStr, a1,a2 being Element of A st a1 <= a2 & a2 <= a1 holds a1 = a2 proof let A be antisymmetric RelStr, a1,a2 be Element of A; assume A1: [a1,a2] in the InternalRel of A & [a2,a1] in the InternalRel of A; then a1 in the carrier of A & a2 in the carrier of A & the InternalRel of A is_antisymmetric_in the carrier of A by Def6,ZFMISC_1:106; hence thesis by A1,RELAT_2:def 4; end; theorem Th26: for A being transitive RelStr, a1,a2,a3 being Element of A holds a1 <= a2 & a2 <= a3 implies a1 <= a3 proof let A be transitive RelStr, a1,a2,a3 be Element of A; assume A1: [a1,a2] in the InternalRel of A & [a2,a3] in the InternalRel of A; then a1 in the carrier of A & a2 in the carrier of A & a3 in the carrier of A & the InternalRel of A is_transitive_in the carrier of A by Def5,ZFMISC_1:106; hence [a1,a3] in the InternalRel of A by A1,RELAT_2:def 8; end; canceled; theorem Th28: for A being antisymmetric RelStr, a1,a2 being Element of A holds not(a1 < a2 & a2 < a1) proof let A be antisymmetric RelStr, a1,a2 be Element of A; assume a1 < a2 & a2 < a1; then a1 <= a2 & a1 <> a2 & a2 <= a1 by Def10; hence thesis by Th25; end; theorem Th29: for A being transitive antisymmetric RelStr for a1,a2,a3 being Element of A holds a1 < a2 & a2 < a3 implies a1 < a3 proof let A be transitive antisymmetric RelStr; let a1,a2,a3 be Element of A; assume A1: a1 < a2 & a2 < a3; then a1 <= a2 & a2 <= a3 by Def10; hence a1 <= a3 by Th26; thus thesis by A1,Th28; end; theorem Th30: for A being antisymmetric RelStr, a1,a2 being Element of A holds a1 <= a2 implies not a2 < a1 proof let A be antisymmetric RelStr, a1,a2 be Element of A; assume that A1: a1 <= a2 and A2: a2 < a1; a2 <= a1 by A2,Def10; hence thesis by A1,A2,Th25; end; canceled; theorem for A being transitive antisymmetric RelStr for a1,a2,a3 being Element of A holds (a1 < a2 & a2 <= a3) or (a1 <= a2 & a2 < a3) implies a1 < a3 proof let A be transitive antisymmetric RelStr; let a1,a2,a3 be Element of A; assume A1: (a1 < a2 & a2 <= a3) or (a1 <= a2 & a2 < a3); A2: now assume A3: a1 < a2 & a2 <= a3; then A4: a1 <= a2 & a2 <= a3 by Def10; then A5: a1 <= a3 by Th26; a1 <> a3 by A3,A4,Th25; hence thesis by A5,Def10; end; now assume A6: a1 <= a2 & a2 < a3; then A7: a1 <= a2 & a2 <= a3 by Def10; then A8: a1 <= a3 by Th26; a1 <> a3 by A6,A7,Th25; hence thesis by A8,Def10; end; hence thesis by A1,A2; end; :: :: Chains. :: definition let A be RelStr; let IT be Subset of A; attr IT is strongly_connected means :Def11: the InternalRel of A is_strongly_connected_in IT; end; definition let A be RelStr; cluster {}A -> strongly_connected; coherence proof let x1,x2; thus thesis; end; end; definition let A be RelStr; cluster strongly_connected Subset of A; existence proof take {}A; thus thesis; end; end; definition let A be RelStr; mode Chain of A is strongly_connected Subset of A; end; canceled 2; theorem Th35: for A being non empty reflexive RelStr for a being Element of A holds {a} is Chain of A proof let A be non empty reflexive RelStr, a be Element of A; A1: a in the carrier of A & the InternalRel of A is_reflexive_in the carrier of A by Def4; {a} is strongly_connected proof let x1,x2; assume x1 in {a} & x2 in {a}; then x1 = a & x2 = a by TARSKI:def 1; hence thesis by A1,RELAT_2:def 1; end; hence thesis; end; theorem Th36: for A being non empty reflexive RelStr, a1,a2 being Element of A holds {a1,a2} is Chain of A iff a1 <= a2 or a2 <= a1 proof let A be non empty reflexive RelStr, a1,a2 be Element of A; thus {a1,a2} is Chain of A implies a1 <= a2 or a2 <= a1 proof A1: a1 in {a1,a2} & a2 in {a1,a2} by TARSKI:def 2; assume {a1,a2} is Chain of A; then the InternalRel of A is_strongly_connected_in {a1,a2} by Def11; then [a1,a2] in the InternalRel of A or [a2,a1] in the InternalRel of A by A1,RELAT_2:def 7; hence thesis by Def9; end; assume A2: a1 <= a2 or a2 <= a1; A3: a1 <= a1 & a2 <= a2; {a1,a2} is strongly_connected proof let x,y; assume A4: x in {a1,a2} & y in {a1,a2}; now per cases by A4,TARSKI:def 2; suppose x = a1 & y = a1; hence thesis by A3,Def9; suppose x = a1 & y = a2; hence thesis by A2,Def9; suppose x = a2 & y = a1; hence thesis by A2,Def9; suppose x = a2 & y = a2; hence thesis by A3,Def9; end; hence thesis; end; hence thesis; end; Lm6: P is_strongly_connected_in X & Y c= X implies P is_strongly_connected_in Y proof assume that A1: P is_strongly_connected_in X and A2: Y c= X; let x,y; assume x in Y & y in Y; hence thesis by A1,A2,RELAT_2:def 7; end; theorem for A being RelStr, C being Chain of A, S being Subset of A holds S c= C implies S is Chain of A proof let A be RelStr, C be Chain of A, S be Subset of A; assume A1: S c= C; the InternalRel of A is_strongly_connected_in C by Def11; then the InternalRel of A is_strongly_connected_in S by A1,Lm6; hence thesis by Def11; end; theorem Th38: for A being reflexive RelStr, a1,a2 being Element of A holds (ex C being Chain of A st a1 in C & a2 in C) iff a1 <= a2 or a2 <= a1 proof let A be reflexive RelStr; let a1,a2 be Element of A; thus (ex C being Chain of A st a1 in C & a2 in C) implies a1 <= a2 or a2 <= a1 proof given C being Chain of A such that A1: a1 in C & a2 in C; the InternalRel of A is_strongly_connected_in C by Def11; then [a1,a2] in the InternalRel of A or [a2,a1] in the InternalRel of A by A1,RELAT_2:def 7; hence thesis by Def9; end; assume A2: a1 <= a2 or a2 <= a1; then [a1,a2] in the InternalRel of A or [a2,a1] in the InternalRel of A by Def9; then a1 in the carrier of A by ZFMISC_1:106; then reconsider B = A as non empty reflexive RelStr by STRUCT_0:def 1; reconsider b1 = a1, b2 = a2 as Element of B; reconsider Y = {b1,b2} as Chain of A by A2,Th36; take Y; thus thesis by TARSKI:def 2; end; theorem Th39: for A being reflexive antisymmetric RelStr, a1,a2 being Element of A holds (ex C being Chain of A st a1 in C & a2 in C) iff (a1 < a2 iff not a2 <= a1) proof let A be reflexive antisymmetric RelStr; let a1,a2 be Element of A; thus (ex C being Chain of A st a1 in C & a2 in C) implies (a1 < a2 iff not a2 <= a1) proof given C being Chain of A such that A1: a1 in C & a2 in C; thus a1 < a2 implies not a2 <= a1 by Th30; assume that A2: not a2 <= a1 and A3: not a1 < a2; not a1 <= a2 or a1 = a2 by A3,Def10; hence thesis by A1,A2,Th38; end; assume a1 < a2 iff not a2 <= a1; then a1 <= a2 or a2 <= a1 by Def10; hence thesis by Th38; end; theorem Th40: for A being RelStr, T being Subset of A holds the InternalRel of A well_orders T implies T is Chain of A proof let A be RelStr, T be Subset of A; assume the InternalRel of A well_orders T; then the InternalRel of A is_connected_in T & the InternalRel of A is_reflexive_in T by WELLORD1:def 5; then the InternalRel of A is_strongly_connected_in T by Lm2; hence thesis by Def11; end; :: :: Upper and lower cones. :: definition let A; let S; func UpperCone(S) -> Subset of A equals :Def12: {a1 : for a2 st a2 in S holds a2 < a1}; coherence proof set T = {a1 : for a2 st a2 in S holds a2 < a1}; T c= the carrier of A proof let x; assume x in T; then ex a1 st x = a1 & for a2 st a2 in S holds a2 < a1; hence thesis; end; hence T is Subset of A; thus thesis; end; end; definition let A; let S; func LowerCone(S) -> Subset of A equals :Def13: {a1 : for a2 st a2 in S holds a1 < a2}; coherence proof set T = {a1 : for a2 st a2 in S holds a1 < a2}; T c= the carrier of A proof let x; assume x in T; then ex a1 st x = a1 & for a2 st a2 in S holds a1 < a2; hence thesis; end; hence T is Subset of A; thus thesis; end; end; canceled 2; theorem Th43: UpperCone({}(A)) = the carrier of A proof thus UpperCone({}(A)) c= the carrier of A; let x; assume x in the carrier of A; then reconsider a = x as Element of A; for a2 st a2 in {}(A) holds a2 < a; then a in {a1 : for a2 st a2 in {}(A) holds a2 < a1}; hence thesis by Def12; end; theorem UpperCone([#](A)) = {} proof thus UpperCone([#](A)) c= {} proof let x; assume x in UpperCone([#](A)); then x in {a1 : for a2 st a2 in [#](A) holds a2 < a1} by Def12; then consider a such that x = a and A1: for a2 st a2 in [#](A) holds a2 < a; a in the carrier of A; then a in [#](A) by PRE_TOPC:12; hence thesis by A1; end; thus thesis by XBOOLE_1:2; end; theorem LowerCone({}(A)) = the carrier of A proof thus LowerCone({}(A)) c= the carrier of A; let x; assume x in the carrier of A; then reconsider a = x as Element of A; for a2 st a2 in {}(A) holds a < a2; then a in {a1 : for a2 st a2 in {}(A) holds a1 < a2}; hence thesis by Def13; end; theorem LowerCone([#](A)) = {} proof thus LowerCone([#](A)) c= {} proof let x; assume x in LowerCone([#](A)); then x in {a1 : for a2 st a2 in [#](A) holds a1 < a2} by Def13; then consider a such that x = a and A1: for a2 st a2 in [#](A) holds a < a2; a in the carrier of A; then a in [#](A) by PRE_TOPC:12; hence thesis by A1; end; thus thesis by XBOOLE_1:2; end; theorem Th47: a in S implies not a in UpperCone(S) proof assume that A1: a in S and A2: a in UpperCone(S); a in {a1 : for a2 st a2 in S holds a2 < a1} by A2,Def12; then ex a1 st a1 = a & for a2 st a2 in S holds a2 < a1; hence thesis by A1; end; theorem not a in UpperCone{a} proof a in {a} by TARSKI:def 1; hence thesis by Th47; end; theorem Th49: a in S implies not a in LowerCone(S) proof assume that A1: a in S and A2: a in LowerCone(S); a in {a1 : for a2 st a2 in S holds a1 < a2} by A2,Def13; then ex a1 st a1 = a & for a2 st a2 in S holds a1 < a2; hence thesis by A1; end; theorem Th50: not a in LowerCone{a} proof a in {a} by TARSKI:def 1; hence thesis by Th49; end; theorem c < a iff a in UpperCone{c} proof thus c < a implies a in UpperCone{c} proof assume c < a; then for b holds b in {c} implies b < a by TARSKI:def 1; then a in {a1 : for a2 st a2 in {c} holds a2 < a1}; hence thesis by Def12; end; assume a in UpperCone{c}; then a in {a1 : for a2 st a2 in {c} holds a2 < a1} by Def12; then A1: ex a1 st a1 = a & for a2 st a2 in {c} holds a2 < a1; c in {c} by TARSKI:def 1; hence thesis by A1; end; theorem Th52: a < c iff a in LowerCone{c} proof thus a < c implies a in LowerCone{c} proof assume a < c; then for b holds b in {c} implies a < b by TARSKI:def 1; then a in {a1 : for a2 st a2 in {c} holds a1 < a2}; hence thesis by Def13; end; assume a in LowerCone{c}; then a in {a1 : for a2 st a2 in {c} holds a1 < a2} by Def13; then A1: ex a1 st a1 = a & for a2 st a2 in {c} holds a1 < a2; c in {c} by TARSKI:def 1; hence thesis by A1; end; :: :: Initial segments. :: definition let A; let S; let a; func InitSegm(S,a) -> Subset of A equals :Def14: LowerCone{a} /\ S; correctness; end; definition let A; let S; mode Initial_Segm of S -> Subset of A means :Def15: ex a st a in S & it = InitSegm(S,a) if S <> {} otherwise it = {}; existence proof now consider x being Element of S; assume A1: S <> {}; then reconsider x as Element of A by Lm5; take T = InitSegm(S,x); thus S <> {} implies ex a st a in S & T = InitSegm(S,a); thus S = {} implies T = {} by A1; end; hence thesis; end; consistency; end; reserve I for Initial_Segm of S; canceled 3; theorem Th56: x in InitSegm(S,a) iff x in LowerCone{a} & x in S proof x in InitSegm(S,a) iff x in LowerCone{a} /\ S by Def14; hence thesis by XBOOLE_0:def 3; end; theorem Th57: a in InitSegm(S,b) iff a < b & a in S proof a in InitSegm(S,b) iff a in LowerCone{b} & a in S by Th56; hence thesis by Th52; end; canceled 2; theorem InitSegm({}(A),a) = {} proof thus InitSegm({}(A),a) = LowerCone{a} /\ {} by Def14 .= {}; end; theorem Th61: InitSegm(S,a) c= S proof InitSegm(S,a) = LowerCone{a} /\ S by Def14; hence thesis by XBOOLE_1:17; end; theorem Th62: not a in InitSegm(S,a) proof assume not thesis; then a in LowerCone{a} /\ S by Def14; then a in LowerCone{a} by XBOOLE_0:def 3; then a in {a1 : for a2 st a2 in {a} holds a1 < a2} by Def13; then A1: ex a1 st a = a1 & for a2 st a2 in {a} holds a1 < a2; a in {a} by TARSKI:def 1; hence thesis by A1; end; canceled; theorem a1 < a2 implies InitSegm(S,a1) c= InitSegm(S,a2) proof assume A1: a1 < a2; let x; assume x in InitSegm(S,a1); then A2: x in LowerCone{a1} /\ S by Def14; then A3: x in S by XBOOLE_0:def 3; x in LowerCone{a1} by A2,XBOOLE_0:def 3; then x in {a : for b st b in {a1} holds a < b} by Def13; then consider a such that A4: a = x and A5: for b st b in {a1} holds a < b; a1 in {a1} by TARSKI:def 1; then a < a1 by A5; then a < a2 by A1,Th29; then for b holds b in {a2} implies a < b by TARSKI:def 1; then a in {c : for b st b in {a2} holds c < b}; then x in LowerCone{a2} by A4,Def13; then x in LowerCone{a2} /\ S by A3,XBOOLE_0:def 3; hence thesis by Def14; end; theorem S c= T implies InitSegm(S,a) c= InitSegm(T,a) proof assume A1: S c= T; let x; assume x in InitSegm(S,a); then A2: x in LowerCone{a} /\ S by Def14; then x in S by XBOOLE_0:def 3; then x in T & x in LowerCone{a} by A1,A2,XBOOLE_0:def 3; then x in LowerCone{a} /\ T by XBOOLE_0:def 3; hence thesis by Def14; end; canceled; theorem Th67: I c= S proof now per cases; suppose S = {}; hence thesis by Def15; suppose S <> {}; then consider a such that a in S and A1: I = InitSegm(S,a) by Def15; I = LowerCone{a} /\ S by A1,Def14; hence thesis by XBOOLE_1:17; end; hence thesis; end; theorem Th68: S <> {} iff not S is Initial_Segm of S proof thus S <> {} implies not S is Initial_Segm of S proof assume S <> {} & S is Initial_Segm of S; then consider a such that A1: a in S and A2: S = InitSegm(S,a) by Def15; S = LowerCone{a} /\ S by A2,Def14; then a in LowerCone{a} by A1,XBOOLE_0:def 3; hence thesis by Th50; end; thus thesis by Def15; end; theorem Th69: (S <> {} or T <> {}) & (S is Initial_Segm of T) implies not T is Initial_Segm of S proof assume that A1: S <> {} or T <> {} and A2: S is Initial_Segm of T and A3: T is Initial_Segm of S; now per cases; suppose S = {}; hence thesis by A1,A3,Def15; suppose T = {}; hence thesis by A1,A2,Def15; suppose A4: S <> {} & T <> {}; then consider a1 such that A5: a1 in S & T = InitSegm(S,a1) by A3,Def15 ; consider a2 such that A6: a2 in T & S = InitSegm(T,a2) by A2,A4,Def15; a1 in LowerCone{a2} /\ T & a2 in LowerCone{a1} /\ S by A5,A6,Def14; then a1 in LowerCone{a2} & a2 in LowerCone{a1} by XBOOLE_0:def 3; then A7: a1 in {a : for b st b in {a2} holds a < b} & a2 in {a3 : for b st b in {a1} holds a3 < b} by Def13; then A8: ex a st a = a1 & for b st b in {a2} holds a < b; A9: ex a3 st a3 = a2 & for b st b in {a1} holds a3 < b by A7; a1 in {a1} & a2 in {a2} by TARSKI:def 1; then a1 < a2 & a2 < a1 by A8,A9; hence thesis by Th28; end; hence thesis; end; theorem Th70: a1 < a2 & a1 in S & a2 in T & T is Initial_Segm of S implies a1 in T proof assume that A1: a1 < a2 and A2: a1 in S and A3: a2 in T and A4: T is Initial_Segm of S; consider a such that a in S and A5: T = InitSegm(S,a) by A2,A4,Def15; now let b; assume b in {a}; then A6: b = a by TARSKI:def 1; a2 in LowerCone{a} /\ S by A3,A5,Def14; then a2 in LowerCone{a} by XBOOLE_0:def 3; then a2 in {a3 : for c st c in {a} holds a3 < c} by Def13; then A7: ex a3 st a3 = a2 & for c st c in {a} holds a3 < c; a in {a} by TARSKI:def 1; then a2 < a by A7; hence a1 < b by A1,A6,Th29; end; then a1 in {b: for c st c in {a} holds b < c}; then a1 in LowerCone{a} by Def13; then a1 in LowerCone{a} /\ S by A2,XBOOLE_0:def 3; hence thesis by A5,Def14; end; theorem Th71: a in S & S is Initial_Segm of T implies InitSegm(S,a) = InitSegm(T,a) proof assume that A1: a in S and A2: S is Initial_Segm of T; A3: S c= T by A2,Th67; thus InitSegm(S,a) c= InitSegm(T,a) proof let x; assume x in InitSegm(S,a); then x in LowerCone{a} /\ S by Def14; then x in LowerCone{a} & x in S by XBOOLE_0:def 3; then x in LowerCone{a} /\ T by A3,XBOOLE_0:def 3; hence thesis by Def14; end; let x; assume x in InitSegm(T,a); then A4: x in LowerCone{a} /\ T by Def14; then A5: x in LowerCone{a} by XBOOLE_0:def 3; then x in {a1 : for a2 st a2 in {a} holds a1 < a2} by Def13; then consider a1 such that A6: x = a1 and A7: for a2 st a2 in {a} holds a1 < a2; a in {a} by TARSKI:def 1; then a1 < a & a1 in T by A4,A6,A7,XBOOLE_0:def 3; then x in S by A1,A2,A6,Th70; then x in LowerCone{a} /\ S by A5,XBOOLE_0:def 3; hence thesis by Def14; end; Lm7: P is_reflexive_in X & Y c= X implies P is_reflexive_in Y proof assume that A1: P is_reflexive_in X and A2: Y c= X; let x; assume x in Y; hence thesis by A1,A2,RELAT_2:def 1; end; Lm8: P is_antisymmetric_in X & Y c= X implies P is_antisymmetric_in Y proof assume that A1: P is_antisymmetric_in X and A2: Y c= X; let x,y; assume x in Y & y in Y; hence thesis by A1,A2,RELAT_2:def 4; end; Lm9: P is_transitive_in X & Y c= X implies P is_transitive_in Y proof assume that A1: P is_transitive_in X and A2: Y c= X; let x,y,z; assume x in Y & y in Y & z in Y; hence thesis by A1,A2,RELAT_2:def 8; end; theorem S c= T & the InternalRel of A well_orders T & (for a1,a2 st a2 in S & a1 < a2 holds a1 in S) implies S = T or S is Initial_Segm of T proof assume that A1: S c= T and A2: the InternalRel of A well_orders T and A3: for a1,a2 st a2 in S & a1 < a2 holds a1 in S and A4: S <> T; per cases; case T <> {}; set Y = T \ S; not T c= S by A1,A4,XBOOLE_0:def 10; then Y c= T & Y <> {} by XBOOLE_1:36,37; then consider x such that A5: x in Y and A6: for y st y in Y holds [x,y] in the InternalRel of A by A2,WELLORD1 :9; reconsider x as Element of A by A5; take x; thus A7: x in T by A5,XBOOLE_0:def 4; S = LowerCone{x} /\ T proof thus S c= LowerCone{x} /\ T proof let y; assume A8: y in S; then reconsider a = y as Element of A; now let a1; assume that A9: a1 in {x} and A10: not a < a1; A11: T is Chain of A & a1 = x by A2,A9,Th40,TARSKI:def 1; then a1 <= a & a1 <> a by A1,A5,A7,A8,A10,Th39,XBOOLE_0:def 4 ; then a1 < a by Def10; then a1 in S by A3,A8; hence contradiction by A5,A11,XBOOLE_0:def 4; end; then y in {a1 : for a2 st a2 in {x} holds a1 < a2}; then y in LowerCone{x} by Def13; hence thesis by A1,A8,XBOOLE_0:def 3; end; let y; assume A12: y in LowerCone{x} /\ T; then y in LowerCone{x} by XBOOLE_0:def 3; then y in {a1 : for a2 st a2 in {x} holds a1 < a2} by Def13; then consider a such that A13: a = y and A14: for a2 st a2 in {x} holds a < a2; A15: now assume y in Y; then [x,y] in the InternalRel of A by A6; then A16: x <= a by A13,Def9; x in {x} by TARSKI:def 1; then a < x by A14; hence contradiction by A16,Th30; end; y in T by A12,XBOOLE_0:def 3; hence thesis by A15,XBOOLE_0:def 4; end; hence thesis by Def14; case T = {}; hence thesis by A1,XBOOLE_1:3; end; theorem Th73: S c= T & the InternalRel of A well_orders T & (for a1,a2 st a2 in S & a1 in T & a1 < a2 holds a1 in S) implies S = T or S is Initial_Segm of T proof assume that A1: S c= T and A2: the InternalRel of A well_orders T and A3: for a1,a2 st a2 in S & a1 in T & a1 < a2 holds a1 in S and A4: S <> T; per cases; case T <> {}; set Y = T \ S; not T c= S by A1,A4,XBOOLE_0:def 10; then Y c= T & Y <> {} by XBOOLE_1:36,37; then consider x such that A5: x in Y and A6: for y st y in Y holds [x,y] in the InternalRel of A by A2,WELLORD1 :9; reconsider x as Element of A by A5; take x; thus A7: x in T by A5,XBOOLE_0:def 4; S = LowerCone{x} /\ T proof thus S c= LowerCone{x} /\ T proof let y; assume A8: y in S; then reconsider a = y as Element of A; now let a1; assume that A9: a1 in {x} and A10: not a < a1; A11: T is Chain of A & a1 = x by A2,A9,Th40,TARSKI:def 1; then a1 <= a & a1 <> a by A1,A5,A7,A8,A10,Th39,XBOOLE_0:def 4 ; then a1 < a by Def10; then a1 in S by A3,A7,A8,A11; hence contradiction by A5,A11,XBOOLE_0:def 4; end; then y in {a1 : for a2 st a2 in {x} holds a1 < a2}; then y in LowerCone{x} by Def13; hence thesis by A1,A8,XBOOLE_0:def 3; end; let y; assume A12: y in LowerCone{x} /\ T; then y in LowerCone{x} by XBOOLE_0:def 3; then y in {a1 : for a2 st a2 in {x} holds a1 < a2} by Def13; then consider a such that A13: a = y and A14: for a2 st a2 in {x} holds a < a2; A15: now assume y in Y; then [x,y] in the InternalRel of A by A6; then A16: x <= a by A13,Def9; x in {x} by TARSKI:def 1; then a < x by A14; hence contradiction by A16,Th30; end; y in T by A12,XBOOLE_0:def 3; hence thesis by A15,XBOOLE_0:def 4; end; hence thesis by Def14; case T = {}; hence thesis by A1,XBOOLE_1:3; end; :: :: Chains of choice function of BOOL of partially ordered sets. :: reserve f for Choice_Function of BOOL(the carrier of A); definition let A; let f; mode Chain of f -> Chain of A means :Def16: it <> {} & the InternalRel of A well_orders it & for a st a in it holds f.UpperCone(InitSegm(it,a)) = a; existence proof set AC = the carrier of A; AC in BOOL AC & not {} in BOOL AC by Th4,Th5; then f.AC is Element of A by Def1; then reconsider aa = f.AC as Element of A; reconsider X = {aa} as Chain of A by Th35; take X; thus X <> {}; X c= the carrier of A & the InternalRel of A is_reflexive_in the carrier of A & the InternalRel of A is_transitive_in the carrier of A & the InternalRel of A is_antisymmetric_in the carrier of A by Def4,Def5,Def6; hence the InternalRel of A is_reflexive_in X & the InternalRel of A is_transitive_in X & the InternalRel of A is_antisymmetric_in X by Lm7,Lm8,Lm9; the InternalRel of A is_strongly_connected_in X by Def11; hence the InternalRel of A is_connected_in X by Lm2; thus the InternalRel of A is_well_founded_in X proof let Y; assume that A1: Y c= X and A2: Y <> {}; reconsider x = aa as set; take x; Y = X by A1,A2,ZFMISC_1:39; hence x in Y by TARSKI:def 1; thus (the InternalRel of A)-Seg(x) /\ Y c= {} proof let y; assume A3: y in (the InternalRel of A)-Seg(x) /\ Y; then y in Y by XBOOLE_0:def 3; then A4: y = aa by A1,TARSKI:def 1; y in (the InternalRel of A)-Seg(x) by A3,XBOOLE_0:def 3; hence thesis by A4,WELLORD1:def 1; end; thus {} c= (the InternalRel of A)-Seg(x) /\ Y by XBOOLE_1:2; end; let a; assume a in X; then A5: a = aa by TARSKI:def 1; LowerCone{a} /\ X = {}(A) proof thus LowerCone{a} /\ X c= {}(A) proof let x; assume A6: x in LowerCone{a} /\ X; then A7: x in X by XBOOLE_0:def 3; x in LowerCone{a} by A6,XBOOLE_0:def 3; then x in {a1 : for a2 st a2 in {a} holds a1 < a2} by Def13; then consider a1 such that A8: x = a1 and A9: for a2 st a2 in {a} holds a1 < a2; thus thesis by A5,A7,A8,A9; end; thus thesis by XBOOLE_1:2; end; then UpperCone(LowerCone{a} /\ X) = the carrier of A by Th43; hence thesis by A5,Def14; end; end; reserve fC,fC1,fC2 for Chain of f; canceled 4; theorem Th78: {f.(the carrier of A)} is Chain of f proof set AC = the carrier of A; AC in BOOL AC & not {} in BOOL AC by Th4,Th5; then f.AC is Element of A by Def1; then reconsider aa = f.AC as Element of A; reconsider X = {aa} as Chain of A by Th35; X c= the carrier of A & the InternalRel of A is_reflexive_in the carrier of A & the InternalRel of A is_transitive_in the carrier of A & the InternalRel of A is_antisymmetric_in the carrier of A by Def4,Def5,Def6; then A1: the InternalRel of A is_reflexive_in X & the InternalRel of A is_transitive_in X & the InternalRel of A is_antisymmetric_in X by Lm7,Lm8,Lm9; the InternalRel of A is_strongly_connected_in X by Def11; then A2: the InternalRel of A is_connected_in X by Lm2; the InternalRel of A is_well_founded_in X proof let Y; assume that A3: Y c= X and A4: Y <> {}; reconsider x = aa as set; take x; Y = X by A3,A4,ZFMISC_1:39; hence x in Y by TARSKI:def 1; thus (the InternalRel of A)-Seg(x) /\ Y c= {} proof let y; assume A5: y in (the InternalRel of A)-Seg(x) /\ Y; then y in Y by XBOOLE_0:def 3; then A6: y = aa by A3,TARSKI:def 1; y in (the InternalRel of A)-Seg(x) by A5,XBOOLE_0:def 3; hence thesis by A6,WELLORD1:def 1; end; thus {} c= (the InternalRel of A)-Seg(x) /\ Y by XBOOLE_1:2; end; then A7: the InternalRel of A well_orders X by A1,A2,WELLORD1:def 5; for a st a in X holds f.UpperCone(InitSegm(X,a)) = a proof let a; assume a in X; then A8: a = aa by TARSKI:def 1; LowerCone{a} /\ X = {}(A) proof thus LowerCone{a} /\ X c= {}(A) proof let x; assume A9: x in LowerCone{a} /\ X; then A10: x in X by XBOOLE_0:def 3; x in LowerCone{a} by A9,XBOOLE_0:def 3; then x in {a1 : for a2 st a2 in {a} holds a1 < a2} by Def13; then consider a1 such that A11: x = a1 and A12: for a2 st a2 in {a} holds a1 < a2; thus thesis by A8,A10,A11,A12; end; thus thesis by XBOOLE_1:2; end; then UpperCone(LowerCone{a} /\ X) = the carrier of A by Th43; hence thesis by A8,Def14; end; hence thesis by A7,Def16; end; theorem Th79: f.(the carrier of A) in fC proof the InternalRel of A well_orders fC & fC <> {} & fC c= fC by Def16; then consider x such that A1: x in fC and A2: for y st y in fC holds [x,y] in the InternalRel of A by WELLORD1:9; reconsider x as Element of A by A1; A3: now consider y being Element of LowerCone{x} /\ fC; assume A4: LowerCone{x} /\ fC <> {}(A); then A5: y in fC by XBOOLE_0:def 3; reconsider a = y as Element of A by A4,Lm5; [x,y] in the InternalRel of A by A2,A5; then A6: x <= a by Def9; a in LowerCone{x} by A4,XBOOLE_0:def 3; then a in {a1 : for a2 st a2 in {x} holds a1 < a2} by Def13; then A7: ex a1 st a = a1 & for a2 st a2 in {x} holds a1 < a2; x in {x} by TARSKI:def 1; then a < x by A7; hence contradiction by A6,Th30; end; LowerCone{x} /\ fC = InitSegm(fC,x) by Def14; then f.UpperCone(LowerCone{x} /\ fC) = x by A1,Def16; hence thesis by A1,A3,Th43; end; theorem Th80: a in fC & b = f.(the carrier of A) implies b <= a proof assume that A1: a in fC and A2: b = f.(the carrier of A); the InternalRel of A well_orders fC & fC <> {} & fC c= fC by Def16; then consider x such that A3: x in fC and A4: for y st y in fC holds [x,y] in the InternalRel of A by WELLORD1:9; reconsider x as Element of A by A3; A5: now consider y being Element of LowerCone{x} /\ fC; assume A6: LowerCone{x} /\ fC <> {}(A); then A7: y in fC by XBOOLE_0:def 3; reconsider a = y as Element of A by A6,Lm5; [x,y] in the InternalRel of A by A4,A7; then A8: x <= a by Def9; a in LowerCone{x} by A6,XBOOLE_0:def 3; then a in {a1 : for a2 st a2 in {x} holds a1 < a2} by Def13; then A9: ex a1 st a = a1 & for a2 st a2 in {x} holds a1 < a2; x in {x} by TARSKI:def 1; then a < x by A9; hence contradiction by A8,Th30; end; LowerCone{x} /\ fC = InitSegm(fC,x) by Def14; then f.UpperCone(LowerCone{x} /\ fC) = x by A3,Def16; then A10: f.(the carrier of A) = x by A5,Th43; [x,a] in the InternalRel of A by A1,A4; hence thesis by A2,A10,Def9; end; theorem a = f.(the carrier of A) implies InitSegm(fC,a) = {} proof assume A1: a = f.(the carrier of A); then A2: a in fC by Th79; consider x being Element of LowerCone{a} /\ fC; assume InitSegm(fC,a) <> {}; then A3: LowerCone {a} /\ fC <> {} by Def14; then A4: x in fC & fC c= the carrier of A by XBOOLE_0:def 3; reconsider b = x as Element of A by A3,Lm5; x in LowerCone{a} by A3,XBOOLE_0:def 3; then b in {a1 : for a2 st a2 in {a} holds a1 < a2} by Def13; then A5: ex a1 st a1 = b & for a2 st a2 in {a} holds a1 < a2; a in {a} by TARSKI:def 1; then a <= b & b < a by A1,A4,A5,Th80; hence contradiction by A2,A4,Th39; end; theorem fC1 meets fC2 proof f.(the carrier of A) in fC1 & f.(the carrier of A) in fC2 by Th79; hence thesis by XBOOLE_0:3; end; theorem Th83: fC1 <> fC2 implies (fC1 is Initial_Segm of fC2 iff not fC2 is Initial_Segm of fC1) proof assume A1: fC1 <> fC2; set N = {a : a in fC1 /\ fC2 & InitSegm(fC1,a) = InitSegm(fC2,a)}; A2: N c= fC1 proof let x; assume x in N; then ex a st a = x & a in fC1 /\ fC2 & InitSegm(fC1,a) = InitSegm(fC2,a); hence thesis by XBOOLE_0:def 3; end; then N is Subset of A by XBOOLE_1:1; then reconsider N as Subset of A; A3: the InternalRel of A well_orders fC1 by Def16; A4: now let a1,a2; assume that A5: a2 in N and A6: a1 in fC1 and A7: a1 < a2; A8: ex a st a = a2 & a in fC1 /\ fC2 & InitSegm(fC1,a) = InitSegm(fC2,a) by A5; then a1 in InitSegm(fC2,a2) by A6,A7,Th57; then a1 in LowerCone{a2} /\ fC2 by Def14; then a1 in fC2 by XBOOLE_0:def 3; then A9: a1 in fC1 /\ fC2 by A6,XBOOLE_0:def 3; InitSegm(fC1,a1) = InitSegm(fC2,a1) proof thus InitSegm(fC1,a1) c= InitSegm(fC2,a1) proof let x; assume A10: x in InitSegm(fC1,a1); then reconsider b = x as Element of A; A11: b < a1 by A10,Th57; then b < a2 & b in fC1 by A7,A10,Th29,Th57; then b in InitSegm(fC1,a2) by Th57; then b in fC2 by A8,Th57; hence thesis by A11,Th57; end; let x; assume A12: x in InitSegm(fC2,a1); then reconsider b = x as Element of A; A13: b < a1 by A12,Th57; then b < a2 & b in fC2 by A7,A12,Th29,Th57; then b in InitSegm(fC2,a2) by Th57; then b in fC1 by A8,Th57; hence thesis by A13,Th57; end; hence a1 in N by A9; end; A14: the InternalRel of A well_orders fC2 by Def16; A15: N c= fC2 proof let x; assume x in N; then ex a st a = x & a in fC1 /\ fC2 & InitSegm(fC1,a) = InitSegm(fC2,a); hence thesis by XBOOLE_0:def 3; end; A16: now let a1,a2; assume that A17: a2 in N and A18: a1 in fC2 and A19: a1 < a2; A20: ex a st a = a2 & a in fC1 /\ fC2 & InitSegm(fC1,a) = InitSegm(fC2,a) by A17; then a1 in InitSegm(fC1,a2) by A18,A19,Th57; then a1 in LowerCone{a2} /\ fC1 by Def14; then a1 in fC1 by XBOOLE_0:def 3; then A21: a1 in fC1 /\ fC2 by A18,XBOOLE_0:def 3; InitSegm(fC1,a1) = InitSegm(fC2,a1) proof thus InitSegm(fC1,a1) c= InitSegm(fC2,a1) proof let x; assume A22: x in InitSegm(fC1,a1); then reconsider b = x as Element of A; A23: b < a1 by A22,Th57; then b < a2 & b in fC1 by A19,A22,Th29,Th57; then b in InitSegm(fC1,a2) by Th57; then b in fC2 by A20,Th57; hence thesis by A23,Th57; end; let x; assume A24: x in InitSegm(fC2,a1); then reconsider b = x as Element of A; A25: b < a1 by A24,Th57; then b < a2 & b in fC2 by A19,A24,Th29,Th57; then b in InitSegm(fC2,a2) by Th57; then b in fC1 by A20,Th57; hence thesis by A25,Th57; end; hence a1 in N by A21; end; now per cases by A2,A3,A4,A14,A15,A16,Th73; suppose N is Initial_Segm of fC1 & N = fC2; then fC2 is Initial_Segm of fC1 & fC1 <> {} by Def16; hence thesis by Th69; suppose N is Initial_Segm of fC2 & N = fC1; then fC1 is Initial_Segm of fC2 & fC2 <> {} by Def16; hence thesis by Th69; suppose N = fC1 & N = fC2; hence thesis by A1; suppose A26: N is Initial_Segm of fC1 & N is Initial_Segm of fC2; fC1 <> {} by Def16; then consider a such that A27: a in fC1 and A28: N = InitSegm(fC1,a) by A26,Def15 ; fC2 <> {} by Def16; then consider b such that A29: b in fC2 and A30: N = InitSegm(fC2,b) by A26,Def15 ; A31: a = f.UpperCone(InitSegm(fC2,b)) by A27,A28,A30,Def16 .= b by A29,Def16; then a in fC1 /\ fC2 by A27,A29,XBOOLE_0:def 3; then a in N by A28,A30,A31; hence thesis by A28,Th62; end; hence thesis; end; theorem Th84: fC1 c< fC2 iff fC1 is Initial_Segm of fC2 proof thus fC1 c< fC2 implies fC1 is Initial_Segm of fC2 proof assume A1: fC1 c< fC2; then A2: fC1 c= fC2 by XBOOLE_0:def 8; now assume A3: fC2 is Initial_Segm of fC1; fC1 <> {} by Def16; then ex a st a in fC1 & fC2 = InitSegm(fC1,a) by A3,Def15; then fC2 c= fC1 by Th61; hence contradiction by A1,A2,XBOOLE_0:def 10; end; hence thesis by A1,Th83; end; assume A4: fC1 is Initial_Segm of fC2; fC2 <> {} by Def16; then ex a st a in fC2 & fC1 = InitSegm(fC2,a) by A4,Def15; then fC1 <> fC2 & fC1 c= fC2 by A4,Th61,Th68; hence thesis by XBOOLE_0:def 8; end; definition let A; let f; func Chains f -> set means :Def17: x in it iff x is Chain of f; existence proof defpred P[set] means $1 is Chain of f; consider X such that A1: for x holds x in X iff x in bool(the carrier of A) & P[x] from Separation; take X; let x; thus x in X implies x is Chain of f by A1; assume x is Chain of f; hence thesis by A1; end; uniqueness proof let D1,D2 be set; assume A2: for x holds x in D1 iff x is Chain of f; assume A3: for x holds x in D2 iff x is Chain of f; thus D1 c= D2 proof let x; assume x in D1; then x is Chain of f by A2; hence thesis by A3; end; let x; assume x in D2; then x is Chain of f by A3; hence thesis by A2; end; end; definition let A; let f; cluster Chains f -> non empty; coherence proof consider x being Chain of f; x in Chains f by Def17; hence thesis; end; end; Lm10: union(Chains(f)) is Subset of A proof now let X; assume X in Chains(f); then X is Chain of f by Def17; hence X c= the carrier of A; end; then union(Chains(f)) is Subset of A by ZFMISC_1:94; hence thesis; end; Lm11: union(Chains(f)) is Chain of A proof reconsider C = union(Chains(f)) as Subset of A by Lm10; the InternalRel of A is_strongly_connected_in C proof let x,y; assume that A1: x in C and A2: y in C; consider X such that A3: x in X and A4: X in Chains(f) by A1,TARSKI:def 4; consider Y such that A5: y in Y and A6: Y in Chains(f) by A2,TARSKI:def 4; reconsider X,Y as Chain of f by A4,A6,Def17; A7: the InternalRel of A is_strongly_connected_in X by Def11; A8: the InternalRel of A is_strongly_connected_in Y by Def11; now per cases; suppose X = Y; hence thesis by A3,A5,A7,RELAT_2:def 7; suppose A9: X <> Y; now per cases by A9,Th83; suppose X is Initial_Segm of Y; then X c< Y by Th84; then X c= Y by XBOOLE_0:def 8; hence thesis by A3,A5,A8,RELAT_2:def 7; suppose Y is Initial_Segm of X; then Y c< X by Th84; then Y c= X by XBOOLE_0:def 8; hence thesis by A3,A5,A7,RELAT_2:def 7; end; hence thesis; end; hence thesis; end; hence thesis by Def11; end; canceled 2; theorem Th87: union(Chains(f)) <> {} proof {f.(the carrier of A)} is Chain of f by Th78; then {f.(the carrier of A)} in Chains(f) & {f.(the carrier of A)} <> {} by Def17; hence thesis by Lm1; end; theorem Th88: fC <> union(Chains(f)) & S = union(Chains(f)) implies fC is Initial_Segm of S proof assume that A1: fC <> union(Chains(f)) and A2: S = union(Chains(f)); consider x being Element of S \ fC; fC in Chains(f) by Def17; then fC c= union(Chains(f)) by ZFMISC_1:92; then not union(Chains(f)) c= fC by A1,XBOOLE_0:def 10; then A3: S \ fC <> {} by A2,XBOOLE_1:37; then x in S by XBOOLE_0:def 4; then consider X such that A4: x in X and A5: X in Chains(f) by A2,TARSKI: def 4; reconsider X as Chain of f by A5,Def17; A6: not x in fC by A3,XBOOLE_0:def 4; fC <> X & not X c= fC by A3,A4,XBOOLE_0:def 4; then not X c< fC by XBOOLE_0:def 8; then not X is Initial_Segm of fC by Th84; then fC is Initial_Segm of X & X <> {} by A4,A6,Th83; then consider a such that A7: a in X and A8: fC = InitSegm(X,a) by Def15; A9: X c= S by A2,A5,ZFMISC_1:92; InitSegm(S,a) = InitSegm(X,a) proof thus InitSegm(S,a) c= InitSegm(X,a) proof let x; assume x in InitSegm(S,a); then A10: x in LowerCone{a} /\ S by Def14; then A11: x in LowerCone{a} by XBOOLE_0:def 3; then x in {a1 : for a2 st a2 in {a} holds a1 < a2} by Def13; then consider b such that A12: b = x and A13: for a2 st a2 in {a} holds b < a2; a in {a} by TARSKI:def 1; then A14: b < a by A13; b in S by A10,A12,XBOOLE_0:def 3; then consider Y such that A15: b in Y and A16: Y in Chains(f) by A2,TARSKI:def 4; reconsider Y as Chain of f by A16,Def17; now per cases; suppose X = Y; then x in LowerCone{a} /\ X by A11,A12,A15,XBOOLE_0:def 3; hence thesis by Def14; suppose A17: X <> Y; now per cases by A17,Th83; suppose X is Initial_Segm of Y; then x in X by A7,A12,A14,A15,Th70; then x in LowerCone{a} /\ X by A11,XBOOLE_0:def 3; hence thesis by Def14; suppose Y is Initial_Segm of X; then Y c< X by Th84; then Y c= X by XBOOLE_0:def 8; then x in LowerCone{a} /\ X by A11,A12,A15,XBOOLE_0:def 3; hence thesis by Def14; end; hence thesis; end; hence thesis; end; let x; assume x in InitSegm(X,a); then x in LowerCone{a} /\ X by Def14; then x in LowerCone{a} & x in X by XBOOLE_0:def 3; then x in LowerCone{a} /\ S by A9,XBOOLE_0:def 3; hence thesis by Def14; end; hence thesis by A7,A8,A9,Def15; end; theorem union(Chains(f)) is Chain of f proof reconsider C = union(Chains(f)) as Chain of A by Lm11; A1: C <> {} by Th87; A2: the InternalRel of A well_orders C proof the InternalRel of A is_reflexive_in the carrier of A & the InternalRel of A is_transitive_in the carrier of A & the InternalRel of A is_antisymmetric_in the carrier of A by Def4,Def5,Def6; hence the InternalRel of A is_reflexive_in C & the InternalRel of A is_transitive_in C & the InternalRel of A is_antisymmetric_in C by Lm7,Lm8,Lm9; the InternalRel of A is_strongly_connected_in C by Def11; hence the InternalRel of A is_connected_in C by Lm2; let Y; consider x being Element of Y; assume that A3: Y c= C and A4: Y <> {}; x in C by A3,A4,TARSKI:def 3; then consider X such that A5: x in X and A6: X in Chains(f) by TARSKI: def 4; reconsider X as Chain of f by A6,Def17; X /\ Y <> {} & X /\ Y c= X & the InternalRel of A well_orders X by A4,A5,Def16,XBOOLE_0: def 3,XBOOLE_1:17; then consider a being set such that A7: a in X /\ Y and A8: for x st x in X /\ Y holds [a,x] in the InternalRel of A by WELLORD1:9; a in X by A7,XBOOLE_0:def 3; then reconsider aa = a as Element of A; take a; thus a in Y by A7,XBOOLE_0:def 3; thus (the InternalRel of A)-Seg(a) /\ Y c= {} proof let y; assume y in (the InternalRel of A)-Seg(a) /\ Y; then A9: y in Y & y in (the InternalRel of A)-Seg(a) by XBOOLE_0:def 3; then y in C & C c= the carrier of A by A3; then reconsider b = y as Element of A; A10: y <> a & [y,a] in the InternalRel of A by A9,WELLORD1:def 1; then A11: b <= aa by Def9; now per cases; suppose X <> C; then a in X & b < aa & X is Initial_Segm of C & y in C by A3,A7,A9,A10,A11,Def10,Th88,XBOOLE_0:def 3 ; hence y in X by Th70; suppose X = C; hence y in X by A3,A9; end; then y in X /\ Y by A9,XBOOLE_0:def 3; then [a,y] in the InternalRel of A by A8; then aa <= b by Def9; hence thesis by A10,A11,Th25; end; thus {} c= (the InternalRel of A)-Seg(a) /\ Y by XBOOLE_1:2; end; now let a; assume A12: a in C; then consider X such that A13: a in X and A14: X in Chains(f) by TARSKI:def 4; reconsider X as Chain of f by A14,Def17; now per cases; suppose X = C; hence f.UpperCone(InitSegm(C,a)) = a by A12,Def16; suppose X <> C; then X is Initial_Segm of C by Th88; then InitSegm(C,a) = InitSegm(X,a) & f.UpperCone(InitSegm(X,a)) = a by A13,Def16,Th71; hence f.UpperCone(InitSegm(C,a)) = a; end; hence f.UpperCone(InitSegm(C,a)) = a; end; hence thesis by A1,A2,Def16; end; :: :: Auxiliary theorems. :: canceled; theorem (ex X st X <> {} & X in Y) iff union Y <> {} by Lm1; theorem P is_strongly_connected_in X iff P is_reflexive_in X & P is_connected_in X by Lm2; theorem P is_reflexive_in X & Y c= X implies P is_reflexive_in Y by Lm7; theorem P is_antisymmetric_in X & Y c= X implies P is_antisymmetric_in Y by Lm8; theorem P is_transitive_in X & Y c= X implies P is_transitive_in Y by Lm9; theorem P is_strongly_connected_in X & Y c= X implies P is_strongly_connected_in Y by Lm6; theorem for R being total reflexive Relation of X holds field R = X by Lm3; theorem for A being set, R being Relation of A st R is_reflexive_in A holds dom R = A & field R = A by Lm4;

Back to top