:: ORDERS_1 semantic presentation begin Lm1: for Y being set holds ( ex X being set st ( X <> {} & X in Y ) iff union Y <> {} ) proof let Y be set ; ::_thesis: ( ex X being set st ( X <> {} & X in Y ) iff union Y <> {} ) thus ( ex X being set st ( X <> {} & X in Y ) implies union Y <> {} ) ::_thesis: ( union Y <> {} implies ex X being set st ( X <> {} & X in Y ) ) proof given X being set such that A1: X <> {} and A2: X in Y ; ::_thesis: union Y <> {} set x = the Element of X; the Element of X in X by A1; hence union Y <> {} by A2, TARSKI:def_4; ::_thesis: verum end; set x = the Element of union Y; assume union Y <> {} ; ::_thesis: ex X being set st ( X <> {} & X in Y ) then consider X being set such that A3: the Element of union Y in X and A4: X in Y by TARSKI:def_4; take X ; ::_thesis: ( X <> {} & X in Y ) thus ( X <> {} & X in Y ) by A3, A4; ::_thesis: verum end; definition let M be non empty set ; assume A1: not {} in M ; mode Choice_Function of M -> Function of M,(union M) means :Def1: :: ORDERS_1:def 1 for X being set st X in M holds it . X in X; existence ex b1 being Function of M,(union M) st for X being set st X in M holds b1 . X in X proof deffunc H1( set ) -> set = \$1 `2 ; set x = the Element of M; deffunc H2( set ) -> set = [:{\$1},\$1:]; consider f being Function such that A2: dom f = M and A3: for X being set st X in M holds f . X = H2(X) from FUNCT_1:sch_3(); A4: the Element of M in M ; then reconsider N = rng f as non empty set by A2, FUNCT_1:3; A5: now__::_thesis:_for_X,_Y_being_set_st_X_in_N_&_Y_in_N_&_X_<>_Y_holds_ not_X_meets_Y let X, Y be set ; ::_thesis: ( X in N & Y in N & X <> Y implies not X meets Y ) assume that A6: X in N and A7: Y in N and A8: X <> Y ; ::_thesis: not X meets Y consider y being set such that A9: y in dom f and A10: f . y = Y by A7, FUNCT_1:def_3; A11: Y = [:{y},y:] by A2, A3, A9, A10; set z = the Element of X /\ Y; assume X meets Y ; ::_thesis: contradiction then A12: X /\ Y <> {} by XBOOLE_0:def_7; consider x being set such that A13: x in dom f and A14: f . x = X by A6, FUNCT_1:def_3; X = [:{x},x:] by A2, A3, A13, A14; then consider x1, x2 being set such that the Element of X /\ Y = [x1,x2] and A15: x1 in {x} /\ {y} and x2 in x /\ y by A11, A12, ZFMISC_1:85; x1 in {x} by A15, XBOOLE_0:def_4; then A16: x1 = x by TARSKI:def_1; x1 in {y} by A15, XBOOLE_0:def_4; hence contradiction by A8, A14, A10, A16, TARSKI:def_1; ::_thesis: verum end; now__::_thesis:_for_X_being_set_st_X_in_N_holds_ X_<>_{} let X be set ; ::_thesis: ( X in N implies X <> {} ) assume X in N ; ::_thesis: X <> {} then consider y being set such that A17: y in dom f and A18: f . y = X by FUNCT_1:def_3; A19: y <> {} by A1, A2, A17; X = [:{y},y:] by A2, A3, A17, A18; hence X <> {} by A19; ::_thesis: verum end; then consider Choice being set such that A20: for X being set st X in N holds ex x being set st Choice /\ X = {x} by A5, WELLORD2:18; defpred S1[ set , set ] means \$2 in \$1 /\ Choice; A21: for X being set st X in N holds ex y being set st S1[X,y] proof let X be set ; ::_thesis: ( X in N implies ex y being set st S1[X,y] ) assume X in N ; ::_thesis: ex y being set st S1[X,y] then consider x being set such that A22: Choice /\ X = {x} by A20; take x ; ::_thesis: S1[X,x] thus S1[X,x] by A22, TARSKI:def_1; ::_thesis: verum end; A23: for X, y1, y2 being set st X in N & S1[X,y1] & S1[X,y2] holds y1 = y2 proof let X, y1, y2 be set ; ::_thesis: ( X in N & S1[X,y1] & S1[X,y2] implies y1 = y2 ) assume that A24: X in N and A25: y1 in X /\ Choice and A26: y2 in X /\ Choice ; ::_thesis: y1 = y2 consider x being set such that A27: {x} = Choice /\ X by A20, A24; x = y1 by A25, A27, TARSKI:def_1; hence y1 = y2 by A26, A27, TARSKI:def_1; ::_thesis: verum end; consider g being Function such that A28: dom g = N and A29: for X being set st X in N holds S1[X,g . X] from FUNCT_1:sch_2(A23, A21); A30: rng g c= union N proof let x be set ; :: according to TARSKI:def_3 ::_thesis: ( not x in rng g or x in union N ) assume x in rng g ; ::_thesis: x in union N then consider y being set such that A31: y in dom g and A32: g . y = x by FUNCT_1:def_3; x in y /\ Choice by A28, A29, A31, A32; then x in y by XBOOLE_0:def_4; hence x in union N by A28, A31, TARSKI:def_4; ::_thesis: verum end; f . the Element of M in rng f by A2, FUNCT_1:def_3; then consider x1 being set such that A33: x1 in N ; consider x2 being set such that A34: x2 in dom f and A35: f . x2 = x1 by A33, FUNCT_1:def_3; A36: x2 <> {} by A1, A2, A34; reconsider f = f as Function of M,N by A2, FUNCT_2:def_1, RELSET_1:4; consider h being Function such that A37: dom h = union N and A38: for x being set st x in union N holds h . x = H1(x) from FUNCT_1:sch_3(); A39: rng h c= union M proof let x be set ; :: according to TARSKI:def_3 ::_thesis: ( not x in rng h or x in union M ) assume x in rng h ; ::_thesis: x in union M then consider y being set such that A40: y in dom h and A41: h . y = x by FUNCT_1:def_3; consider Y being set such that A42: y in Y and A43: Y in N by A37, A40, TARSKI:def_4; consider z being set such that A44: z in dom f and A45: f . z = Y by A43, FUNCT_1:def_3; A46: Y = [:{z},z:] by A3, A44, A45; then consider x1, x2 being set such that A47: y = [x1,x2] by A42, RELAT_1:def_1; A48: x2 in z by A42, A46, A47, ZFMISC_1:87; x = [x1,x2] `2 by A37, A38, A40, A41, A47; then x in z by A48; hence x in union M by A44, TARSKI:def_4; ::_thesis: verum end; x1 = [:{x2},x2:] by A2, A3, A34, A35; then A49: union N <> {} by A33, A36, Lm1; then reconsider g = g as Function of N,(union N) by A28, A30, FUNCT_2:def_1, RELSET_1:4; union M <> {} by A1, A4, Lm1; then reconsider h = h as Function of (union N),(union M) by A37, A39, FUNCT_2:def_1, RELSET_1:4; A50: dom (g * f) = M by A49, FUNCT_2:def_1; reconsider F = h * (g * f) as Function of M,(union M) by A49; take F ; ::_thesis: for X being set st X in M holds F . X in X let X be set ; ::_thesis: ( X in M implies F . X in X ) assume A51: X in M ; ::_thesis: F . X in X then A52: f . X = [:{X},X:] by A3; set fX = f . X; A53: f . X in N by A2, A51, FUNCT_1:def_3; then g . (f . X) in rng g by A28, FUNCT_1:def_3; then A54: h . (g . (f . X)) = (g . (f . X)) `2 by A38; A55: g . (f . X) in (f . X) /\ Choice by A29, A53; then consider x1, x2 being set such that A56: [x1,x2] = g . (f . X) by A52, RELAT_1:def_1; g . (f . X) in f . X by A55, XBOOLE_0:def_4; then x2 in X by A52, A56, ZFMISC_1:87; then A57: h . (g . (f . X)) in X by A56, A54, MCART_1:7; (g * f) . X = g . (f . X) by A2, A51, FUNCT_1:13; hence F . X in X by A50, A51, A57, FUNCT_1:13; ::_thesis: verum end; end; :: deftheorem Def1 defines Choice_Function ORDERS_1:def_1_:_ for M being non empty set st not {} in M holds for b2 being Function of M,(union M) holds ( b2 is Choice_Function of M iff for X being set st X in M holds b2 . X in X ); definition let D be set ; func BOOL D -> set equals :: ORDERS_1:def 2 (bool D) \ {{}}; coherence (bool D) \ {{}} is set ; end; :: deftheorem defines BOOL ORDERS_1:def_2_:_ for D being set holds BOOL D = (bool D) \ {{}}; registration let D be non empty set ; cluster BOOL D -> non empty ; coherence not BOOL D is empty proof A1: not D in {{}} by TARSKI:def_1; D in bool D by ZFMISC_1:def_1; hence not BOOL D is empty by A1, XBOOLE_0:def_5; ::_thesis: verum end; end; theorem :: ORDERS_1:1 for D being non empty set holds not {} in BOOL D proof let D be non empty set ; ::_thesis: not {} in BOOL D assume {} in BOOL D ; ::_thesis: contradiction then not {} in {{}} by XBOOLE_0:def_5; hence contradiction by TARSKI:def_1; ::_thesis: verum end; theorem :: ORDERS_1:2 for X being set for D being non empty set holds ( D c= X iff D in BOOL X ) proof let X be set ; ::_thesis: for D being non empty set holds ( D c= X iff D in BOOL X ) let D be non empty set ; ::_thesis: ( D c= X iff D in BOOL X ) thus ( D c= X implies D in BOOL X ) ::_thesis: ( D in BOOL X implies D c= X ) proof A1: not D in {{}} by TARSKI:def_1; assume D c= X ; ::_thesis: D in BOOL X hence D in BOOL X by A1, XBOOLE_0:def_5; ::_thesis: verum end; assume D in BOOL X ; ::_thesis: D c= X hence D c= X ; ::_thesis: verum end; definition let X be set ; mode Order of X is reflexive antisymmetric transitive total Relation of X; end; Lm2: for X being set for R being total Relation of X holds field R = X proof let X be set ; ::_thesis: for R being total Relation of X holds field R = X let R be total Relation of X; ::_thesis: field R = X thus field R = X \/ (rng R) by PARTFUN1:def_2 .= X by XBOOLE_1:12 ; ::_thesis: verum end; theorem Th3: :: ORDERS_1:3 for X, x being set for O being Order of X st x in X holds [x,x] in O proof let X, x be set ; ::_thesis: for O being Order of X st x in X holds [x,x] in O let O be Order of X; ::_thesis: ( x in X implies [x,x] in O ) field O = X by Lm2; then O is_reflexive_in X by RELAT_2:def_9; hence ( x in X implies [x,x] in O ) by RELAT_2:def_1; ::_thesis: verum end; theorem :: ORDERS_1:4 for X, x, y being set for O being Order of X st x in X & y in X & [x,y] in O & [y,x] in O holds x = y proof let X, x, y be set ; ::_thesis: for O being Order of X st x in X & y in X & [x,y] in O & [y,x] in O holds x = y let O be Order of X; ::_thesis: ( x in X & y in X & [x,y] in O & [y,x] in O implies x = y ) field O = X by Lm2; then O is_antisymmetric_in X by RELAT_2:def_12; hence ( x in X & y in X & [x,y] in O & [y,x] in O implies x = y ) by RELAT_2:def_4; ::_thesis: verum end; theorem :: ORDERS_1:5 for X, x, y, z being set for O being Order of X st x in X & y in X & z in X & [x,y] in O & [y,z] in O holds [x,z] in O proof let X, x, y, z be set ; ::_thesis: for O being Order of X st x in X & y in X & z in X & [x,y] in O & [y,z] in O holds [x,z] in O let O be Order of X; ::_thesis: ( x in X & y in X & z in X & [x,y] in O & [y,z] in O implies [x,z] in O ) field O = X by Lm2; then O is_transitive_in X by RELAT_2:def_16; hence ( x in X & y in X & z in X & [x,y] in O & [y,z] in O implies [x,z] in O ) by RELAT_2:def_8; ::_thesis: verum end; theorem :: ORDERS_1:6 for Y being set holds ( ex X being set st ( X <> {} & X in Y ) iff union Y <> {} ) by Lm1; theorem :: ORDERS_1:7 for X being set for P being Relation holds ( P is_strongly_connected_in X iff ( P is_reflexive_in X & P is_connected_in X ) ) proof let X be set ; ::_thesis: for P being Relation holds ( P is_strongly_connected_in X iff ( P is_reflexive_in X & P is_connected_in X ) ) let P be Relation; ::_thesis: ( P is_strongly_connected_in X iff ( P is_reflexive_in X & P is_connected_in X ) ) thus ( P is_strongly_connected_in X implies ( P is_reflexive_in X & P is_connected_in X ) ) ::_thesis: ( P is_reflexive_in X & P is_connected_in X implies P is_strongly_connected_in X ) proof assume A1: P is_strongly_connected_in X ; ::_thesis: ( P is_reflexive_in X & P is_connected_in X ) thus P is_reflexive_in X ::_thesis: P is_connected_in X proof let x be set ; :: according to RELAT_2:def_1 ::_thesis: ( not x in X or [x,x] in P ) assume x in X ; ::_thesis: [x,x] in P hence [x,x] in P by A1, RELAT_2:def_7; ::_thesis: verum end; let x be set ; :: according to RELAT_2:def_6 ::_thesis: for b1 being set holds ( not x in X or not b1 in X or x = b1 or [x,b1] in P or [b1,x] in P ) let y be set ; ::_thesis: ( not x in X or not y in X or x = y or [x,y] in P or [y,x] in P ) assume that A2: x in X and A3: y in X ; ::_thesis: ( x = y or [x,y] in P or [y,x] in P ) thus ( x = y or [x,y] in P or [y,x] in P ) by A1, A2, A3, RELAT_2:def_7; ::_thesis: verum end; assume that A4: P is_reflexive_in X and A5: P is_connected_in X ; ::_thesis: P is_strongly_connected_in X let x be set ; :: according to RELAT_2:def_7 ::_thesis: for b1 being set holds ( not x in X or not b1 in X or [x,b1] in P or [b1,x] in P ) let y be set ; ::_thesis: ( not x in X or not y in X or [x,y] in P or [y,x] in P ) assume that A6: x in X and A7: y in X ; ::_thesis: ( [x,y] in P or [y,x] in P ) ( x = y & not [x,y] in P implies [y,x] in P ) by A4, A6, RELAT_2:def_1; hence ( [x,y] in P or [y,x] in P ) by A5, A6, A7, RELAT_2:def_6; ::_thesis: verum end; theorem Th8: :: ORDERS_1:8 for X, Y being set for P being Relation st P is_reflexive_in X & Y c= X holds P is_reflexive_in Y proof let X, Y be set ; ::_thesis: for P being Relation st P is_reflexive_in X & Y c= X holds P is_reflexive_in Y let P be Relation; ::_thesis: ( P is_reflexive_in X & Y c= X implies P is_reflexive_in Y ) assume that A1: P is_reflexive_in X and A2: Y c= X ; ::_thesis: P is_reflexive_in Y let x be set ; :: according to RELAT_2:def_1 ::_thesis: ( not x in Y or [x,x] in P ) assume x in Y ; ::_thesis: [x,x] in P hence [x,x] in P by A1, A2, RELAT_2:def_1; ::_thesis: verum end; theorem Th9: :: ORDERS_1:9 for X, Y being set for P being Relation st P is_antisymmetric_in X & Y c= X holds P is_antisymmetric_in Y proof let X, Y be set ; ::_thesis: for P being Relation st P is_antisymmetric_in X & Y c= X holds P is_antisymmetric_in Y let P be Relation; ::_thesis: ( P is_antisymmetric_in X & Y c= X implies P is_antisymmetric_in Y ) assume that A1: P is_antisymmetric_in X and A2: Y c= X ; ::_thesis: P is_antisymmetric_in Y let x be set ; :: according to RELAT_2:def_4 ::_thesis: for b1 being set holds ( not x in Y or not b1 in Y or not [x,b1] in P or not [b1,x] in P or x = b1 ) let y be set ; ::_thesis: ( not x in Y or not y in Y or not [x,y] in P or not [y,x] in P or x = y ) assume that A3: x in Y and A4: y in Y ; ::_thesis: ( not [x,y] in P or not [y,x] in P or x = y ) thus ( not [x,y] in P or not [y,x] in P or x = y ) by A1, A2, A3, A4, RELAT_2:def_4; ::_thesis: verum end; theorem Th10: :: ORDERS_1:10 for X, Y being set for P being Relation st P is_transitive_in X & Y c= X holds P is_transitive_in Y proof let X, Y be set ; ::_thesis: for P being Relation st P is_transitive_in X & Y c= X holds P is_transitive_in Y let P be Relation; ::_thesis: ( P is_transitive_in X & Y c= X implies P is_transitive_in Y ) assume that A1: P is_transitive_in X and A2: Y c= X ; ::_thesis: P is_transitive_in Y let x be set ; :: according to RELAT_2:def_8 ::_thesis: for b1, b2 being set holds ( not x in Y or not b1 in Y or not b2 in Y or not [x,b1] in P or not [b1,b2] in P or [x,b2] in P ) let y, z be set ; ::_thesis: ( not x in Y or not y in Y or not z in Y or not [x,y] in P or not [y,z] in P or [x,z] in P ) assume that A3: x in Y and A4: y in Y and A5: z in Y ; ::_thesis: ( not [x,y] in P or not [y,z] in P or [x,z] in P ) thus ( not [x,y] in P or not [y,z] in P or [x,z] in P ) by A1, A2, A3, A4, A5, RELAT_2:def_8; ::_thesis: verum end; theorem :: ORDERS_1:11 for X, Y being set for P being Relation st P is_strongly_connected_in X & Y c= X holds P is_strongly_connected_in Y proof let X, Y be set ; ::_thesis: for P being Relation st P is_strongly_connected_in X & Y c= X holds P is_strongly_connected_in Y let P be Relation; ::_thesis: ( P is_strongly_connected_in X & Y c= X implies P is_strongly_connected_in Y ) assume that A1: P is_strongly_connected_in X and A2: Y c= X ; ::_thesis: P is_strongly_connected_in Y let x be set ; :: according to RELAT_2:def_7 ::_thesis: for b1 being set holds ( not x in Y or not b1 in Y or [x,b1] in P or [b1,x] in P ) let y be set ; ::_thesis: ( not x in Y or not y in Y or [x,y] in P or [y,x] in P ) assume that A3: x in Y and A4: y in Y ; ::_thesis: ( [x,y] in P or [y,x] in P ) thus ( [x,y] in P or [y,x] in P ) by A1, A2, A3, A4, RELAT_2:def_7; ::_thesis: verum end; theorem :: ORDERS_1:12 for X being set for R being total Relation of X holds field R = X by Lm2; theorem Th13: :: ORDERS_1:13 for A being set for R being Relation of A st R is_reflexive_in A holds ( dom R = A & field R = A ) proof let A be set ; ::_thesis: for R being Relation of A st R is_reflexive_in A holds ( dom R = A & field R = A ) let R be Relation of A; ::_thesis: ( R is_reflexive_in A implies ( dom R = A & field R = A ) ) assume A1: R is_reflexive_in A ; ::_thesis: ( dom R = A & field R = A ) A2: A c= dom R proof let x be set ; :: according to TARSKI:def_3 ::_thesis: ( not x in A or x in dom R ) assume x in A ; ::_thesis: x in dom R then [x,x] in R by A1, RELAT_2:def_1; hence x in dom R by XTUPLE_0:def_12; ::_thesis: verum end; hence dom R = A by XBOOLE_0:def_10; ::_thesis: field R = A thus field R = A \/ (rng R) by A2, XBOOLE_0:def_10 .= A by XBOOLE_1:12 ; ::_thesis: verum end; begin theorem Th14: :: ORDERS_1:14 for X being set for O being Order of X holds ( dom O = X & rng O = X ) proof let X be set ; ::_thesis: for O being Order of X holds ( dom O = X & rng O = X ) let O be Order of X; ::_thesis: ( dom O = X & rng O = X ) thus dom O = X ::_thesis: rng O = X proof thus dom O c= X ; :: according to XBOOLE_0:def_10 ::_thesis: X c= dom O let x be set ; :: according to TARSKI:def_3 ::_thesis: ( not x in X or x in dom O ) assume x in X ; ::_thesis: x in dom O then [x,x] in O by Th3; hence x in dom O by XTUPLE_0:def_12; ::_thesis: verum end; thus rng O c= X ; :: according to XBOOLE_0:def_10 ::_thesis: X c= rng O let x be set ; :: according to TARSKI:def_3 ::_thesis: ( not x in X or x in rng O ) assume x in X ; ::_thesis: x in rng O then [x,x] in O by Th3; hence x in rng O by XTUPLE_0:def_13; ::_thesis: verum end; theorem :: ORDERS_1:15 for X being set for O being Order of X holds field O = X proof let X be set ; ::_thesis: for O being Order of X holds field O = X let O be Order of X; ::_thesis: field O = X thus X = X \/ X .= (dom O) \/ X by Th14 .= field O by Th14 ; ::_thesis: verum end; definition let R be Relation; attrR is being_quasi-order means :: ORDERS_1:def 3 ( R is reflexive & R is transitive ); attrR is being_partial-order means :Def4: :: ORDERS_1:def 4 ( R is reflexive & R is transitive & R is antisymmetric ); attrR is being_linear-order means :Def5: :: ORDERS_1:def 5 ( R is reflexive & R is transitive & R is antisymmetric & R is connected ); end; :: deftheorem defines being_quasi-order ORDERS_1:def_3_:_ for R being Relation holds ( R is being_quasi-order iff ( R is reflexive & R is transitive ) ); :: deftheorem Def4 defines being_partial-order ORDERS_1:def_4_:_ for R being Relation holds ( R is being_partial-order iff ( R is reflexive & R is transitive & R is antisymmetric ) ); :: deftheorem Def5 defines being_linear-order ORDERS_1:def_5_:_ for R being Relation holds ( R is being_linear-order iff ( R is reflexive & R is transitive & R is antisymmetric & R is connected ) ); theorem :: ORDERS_1:16 for R being Relation st R is being_quasi-order holds R ~ is being_quasi-order proof let R be Relation; ::_thesis: ( R is being_quasi-order implies R ~ is being_quasi-order ) assume that A1: R is reflexive and A2: R is transitive ; :: according to ORDERS_1:def_3 ::_thesis: R ~ is being_quasi-order thus ( R ~ is reflexive & R ~ is transitive ) by A1, A2; :: according to ORDERS_1:def_3 ::_thesis: verum end; theorem :: ORDERS_1:17 for R being Relation st R is being_partial-order holds R ~ is being_partial-order proof let R be Relation; ::_thesis: ( R is being_partial-order implies R ~ is being_partial-order ) assume that A1: R is reflexive and A2: R is transitive and A3: R is antisymmetric ; :: according to ORDERS_1:def_4 ::_thesis: R ~ is being_partial-order thus ( R ~ is reflexive & R ~ is transitive & R ~ is antisymmetric ) by A1, A2, A3; :: according to ORDERS_1:def_4 ::_thesis: verum end; Lm3: for R being Relation st R is connected holds R ~ is connected proof let R be Relation; ::_thesis: ( R is connected implies R ~ is connected ) assume A1: for x, y being set st x in field R & y in field R & x <> y & not [x,y] in R holds [y,x] in R ; :: according to RELAT_2:def_6,RELAT_2:def_14 ::_thesis: R ~ is connected let x be set ; :: according to RELAT_2:def_6,RELAT_2:def_14 ::_thesis: for b1 being set holds ( not x in field (R ~) or not b1 in field (R ~) or x = b1 or [x,b1] in R ~ or [b1,x] in R ~ ) let y be set ; ::_thesis: ( not x in field (R ~) or not y in field (R ~) or x = y or [x,y] in R ~ or [y,x] in R ~ ) assume that A2: x in field (R ~) and A3: y in field (R ~) and A4: x <> y ; ::_thesis: ( [x,y] in R ~ or [y,x] in R ~ ) field R = field (R ~) by RELAT_1:21; then ( [x,y] in R or [y,x] in R ) by A1, A2, A3, A4; hence ( [x,y] in R ~ or [y,x] in R ~ ) by RELAT_1:def_7; ::_thesis: verum end; theorem Th18: :: ORDERS_1:18 for R being Relation st R is being_linear-order holds R ~ is being_linear-order proof let R be Relation; ::_thesis: ( R is being_linear-order implies R ~ is being_linear-order ) assume that A1: R is reflexive and A2: R is transitive and A3: R is antisymmetric and A4: R is connected ; :: according to ORDERS_1:def_5 ::_thesis: R ~ is being_linear-order thus ( R ~ is reflexive & R ~ is transitive & R ~ is antisymmetric & R ~ is connected ) by A1, A2, A3, A4, Lm3; :: according to ORDERS_1:def_5 ::_thesis: verum end; theorem :: ORDERS_1:19 for R being Relation st R is well-ordering holds ( R is being_quasi-order & R is being_partial-order & R is being_linear-order ) proof let R be Relation; ::_thesis: ( R is well-ordering implies ( R is being_quasi-order & R is being_partial-order & R is being_linear-order ) ) assume that A1: R is reflexive and A2: R is transitive and A3: R is antisymmetric and A4: R is connected and R is well_founded ; :: according to WELLORD1:def_4 ::_thesis: ( R is being_quasi-order & R is being_partial-order & R is being_linear-order ) thus ( R is reflexive & R is transitive & R is reflexive & R is transitive & R is antisymmetric & R is reflexive & R is transitive & R is antisymmetric & R is connected ) by A1, A2, A3, A4; :: according to ORDERS_1:def_3,ORDERS_1:def_4,ORDERS_1:def_5 ::_thesis: verum end; theorem :: ORDERS_1:20 for R being Relation st R is being_linear-order holds ( R is being_quasi-order & R is being_partial-order ) proof let R be Relation; ::_thesis: ( R is being_linear-order implies ( R is being_quasi-order & R is being_partial-order ) ) assume that A1: R is reflexive and A2: R is transitive and A3: R is antisymmetric and R is connected ; :: according to ORDERS_1:def_5 ::_thesis: ( R is being_quasi-order & R is being_partial-order ) thus ( R is reflexive & R is transitive & R is reflexive & R is transitive & R is antisymmetric ) by A1, A2, A3; :: according to ORDERS_1:def_3,ORDERS_1:def_4 ::_thesis: verum end; theorem Th21: :: ORDERS_1:21 for R being Relation st R is being_partial-order holds R is being_quasi-order proof let R be Relation; ::_thesis: ( R is being_partial-order implies R is being_quasi-order ) assume that A1: R is reflexive and A2: R is transitive and R is antisymmetric ; :: according to ORDERS_1:def_4 ::_thesis: R is being_quasi-order thus ( R is reflexive & R is transitive ) by A1, A2; :: according to ORDERS_1:def_3 ::_thesis: verum end; theorem :: ORDERS_1:22 for X being set for O being Order of X holds O is being_partial-order by Def4; theorem :: ORDERS_1:23 for X being set for O being Order of X holds O is being_quasi-order proof let X be set ; ::_thesis: for O being Order of X holds O is being_quasi-order let O be Order of X; ::_thesis: O is being_quasi-order O is being_partial-order by Def4; hence O is being_quasi-order by Th21; ::_thesis: verum end; theorem :: ORDERS_1:24 for X being set for O being Order of X st O is connected holds O is being_linear-order by Def5; Lm4: for R being Relation holds R c= [:(field R),(field R):] proof let R be Relation; ::_thesis: R c= [:(field R),(field R):] let y be set ; :: according to RELAT_1:def_3 ::_thesis: for b1 being set holds ( not [y,b1] in R or [y,b1] in [:(field R),(field R):] ) let z be set ; ::_thesis: ( not [y,z] in R or [y,z] in [:(field R),(field R):] ) assume A1: [y,z] in R ; ::_thesis: [y,z] in [:(field R),(field R):] then A2: z in field R by RELAT_1:15; y in field R by A1, RELAT_1:15; hence [y,z] in [:(field R),(field R):] by A2, ZFMISC_1:87; ::_thesis: verum end; Lm5: for R being Relation for X being set st R is reflexive & X c= field R holds field (R |_2 X) = X proof let R be Relation; ::_thesis: for X being set st R is reflexive & X c= field R holds field (R |_2 X) = X let X be set ; ::_thesis: ( R is reflexive & X c= field R implies field (R |_2 X) = X ) assume that A1: for x being set st x in field R holds [x,x] in R and A2: X c= field R ; :: according to RELAT_2:def_1,RELAT_2:def_9 ::_thesis: field (R |_2 X) = X thus field (R |_2 X) c= X :: according to XBOOLE_0:def_10 ::_thesis: X c= field (R |_2 X) proof let y be set ; :: according to TARSKI:def_3 ::_thesis: ( not y in field (R |_2 X) or y in X ) thus ( not y in field (R |_2 X) or y in X ) by WELLORD1:12; ::_thesis: verum end; let y be set ; :: according to TARSKI:def_3 ::_thesis: ( not y in X or y in field (R |_2 X) ) assume A3: y in X ; ::_thesis: y in field (R |_2 X) then A4: [y,y] in [:X,X:] by ZFMISC_1:87; [y,y] in R by A1, A2, A3; then [y,y] in R |_2 X by A4, XBOOLE_0:def_4; hence y in field (R |_2 X) by RELAT_1:15; ::_thesis: verum end; theorem :: ORDERS_1:25 for R being Relation for X being set st R is being_quasi-order holds R |_2 X is being_quasi-order proof let R be Relation; ::_thesis: for X being set st R is being_quasi-order holds R |_2 X is being_quasi-order let X be set ; ::_thesis: ( R is being_quasi-order implies R |_2 X is being_quasi-order ) assume that A1: R is reflexive and A2: R is transitive ; :: according to ORDERS_1:def_3 ::_thesis: R |_2 X is being_quasi-order thus ( R |_2 X is reflexive & R |_2 X is transitive ) by A1, A2, WELLORD1:15, WELLORD1:17; :: according to ORDERS_1:def_3 ::_thesis: verum end; theorem :: ORDERS_1:26 for R being Relation for X being set st R is being_partial-order holds R |_2 X is being_partial-order proof let R be Relation; ::_thesis: for X being set st R is being_partial-order holds R |_2 X is being_partial-order let X be set ; ::_thesis: ( R is being_partial-order implies R |_2 X is being_partial-order ) assume that A1: R is reflexive and A2: R is transitive and A3: R is antisymmetric ; :: according to ORDERS_1:def_4 ::_thesis: R |_2 X is being_partial-order thus ( R |_2 X is reflexive & R |_2 X is transitive & R |_2 X is antisymmetric ) by A1, A2, A3, WELLORD1:15, WELLORD1:17; :: according to ORDERS_1:def_4 ::_thesis: verum end; theorem :: ORDERS_1:27 for R being Relation for X being set st R is being_linear-order holds R |_2 X is being_linear-order proof let R be Relation; ::_thesis: for X being set st R is being_linear-order holds R |_2 X is being_linear-order let X be set ; ::_thesis: ( R is being_linear-order implies R |_2 X is being_linear-order ) assume that A1: R is reflexive and A2: R is transitive and A3: R is antisymmetric and A4: R is connected ; :: according to ORDERS_1:def_5 ::_thesis: R |_2 X is being_linear-order thus ( R |_2 X is reflexive & R |_2 X is transitive & R |_2 X is antisymmetric & R |_2 X is connected ) by A1, A2, A3, A4, WELLORD1:15, WELLORD1:16, WELLORD1:17; :: according to ORDERS_1:def_5 ::_thesis: verum end; registration let R be empty Relation; cluster field R -> empty ; coherence field R is empty ; end; registration cluster empty Relation-like -> well-ordering being_quasi-order being_partial-order being_linear-order for set ; coherence for b1 being Relation st b1 is empty holds ( b1 is being_quasi-order & b1 is being_partial-order & b1 is being_linear-order & b1 is well-ordering ) proof let R be Relation; ::_thesis: ( R is empty implies ( R is being_quasi-order & R is being_partial-order & R is being_linear-order & R is well-ordering ) ) assume A1: R is empty ; ::_thesis: ( R is being_quasi-order & R is being_partial-order & R is being_linear-order & R is well-ordering ) thus A2: R is reflexive :: according to ORDERS_1:def_3 ::_thesis: ( R is transitive & R is being_partial-order & R is being_linear-order & R is well-ordering ) proof let x be set ; :: according to RELAT_2:def_1,RELAT_2:def_9 ::_thesis: ( not x in field R or [x,x] in R ) assume x in field R ; ::_thesis: [x,x] in R hence [x,x] in R by A1; ::_thesis: verum end; thus A3: R is transitive ::_thesis: ( R is being_partial-order & R is being_linear-order & R is well-ordering ) proof let x be set ; :: according to RELAT_2:def_8,RELAT_2:def_16 ::_thesis: for b1, b2 being set holds ( not x in field R or not b1 in field R or not b2 in field R or not [x,b1] in R or not [b1,b2] in R or [x,b2] in R ) let y, z be set ; ::_thesis: ( not x in field R or not y in field R or not z in field R or not [x,y] in R or not [y,z] in R or [x,z] in R ) assume x in field R ; ::_thesis: ( not y in field R or not z in field R or not [x,y] in R or not [y,z] in R or [x,z] in R ) thus ( not y in field R or not z in field R or not [x,y] in R or not [y,z] in R or [x,z] in R ) by A1; ::_thesis: verum end; hence ( R is reflexive & R is transitive ) by A2; :: according to ORDERS_1:def_4 ::_thesis: ( R is antisymmetric & R is being_linear-order & R is well-ordering ) thus A4: R is antisymmetric ::_thesis: ( R is being_linear-order & R is well-ordering ) proof let x be set ; :: according to RELAT_2:def_4,RELAT_2:def_12 ::_thesis: for b1 being set holds ( not x in field R or not b1 in field R or not [x,b1] in R or not [b1,x] in R or x = b1 ) let y be set ; ::_thesis: ( not x in field R or not y in field R or not [x,y] in R or not [y,x] in R or x = y ) assume x in field R ; ::_thesis: ( not y in field R or not [x,y] in R or not [y,x] in R or x = y ) thus ( not y in field R or not [x,y] in R or not [y,x] in R or x = y ) by A1; ::_thesis: verum end; hence ( R is reflexive & R is transitive & R is antisymmetric ) by A2, A3; :: according to ORDERS_1:def_5 ::_thesis: ( R is connected & R is well-ordering ) thus R is connected ::_thesis: R is well-ordering proof let x be set ; :: according to RELAT_2:def_6,RELAT_2:def_14 ::_thesis: for b1 being set holds ( not x in field R or not b1 in field R or x = b1 or [x,b1] in R or [b1,x] in R ) let y be set ; ::_thesis: ( not x in field R or not y in field R or x = y or [x,y] in R or [y,x] in R ) assume x in field R ; ::_thesis: ( not y in field R or x = y or [x,y] in R or [y,x] in R ) thus ( not y in field R or x = y or [x,y] in R or [y,x] in R ) by A1; ::_thesis: verum end; hence ( R is reflexive & R is transitive & R is antisymmetric & R is connected ) by A2, A3, A4; :: according to WELLORD1:def_4 ::_thesis: R is well_founded let Y be set ; :: according to WELLORD1:def_2 ::_thesis: ( not Y c= field R or Y = {} or ex b1 being set st ( b1 in Y & R -Seg b1 misses Y ) ) assume that A5: Y c= field R and A6: Y <> {} ; ::_thesis: ex b1 being set st ( b1 in Y & R -Seg b1 misses Y ) thus ex b1 being set st ( b1 in Y & R -Seg b1 misses Y ) by A5, A6, A1; ::_thesis: verum end; end; registration let X be set ; cluster id X -> being_quasi-order being_partial-order ; coherence ( id X is being_quasi-order & id X is being_partial-order ) proof thus ( id X is reflexive & id X is transitive & id X is reflexive & id X is transitive & id X is antisymmetric ) ; :: according to ORDERS_1:def_3,ORDERS_1:def_4 ::_thesis: verum end; end; definition let R be Relation; let X be set ; predR quasi_orders X means :Def6: :: ORDERS_1:def 6 ( R is_reflexive_in X & R is_transitive_in X ); predR partially_orders X means :Def7: :: ORDERS_1:def 7 ( R is_reflexive_in X & R is_transitive_in X & R is_antisymmetric_in X ); predR linearly_orders X means :: ORDERS_1:def 8 ( R is_reflexive_in X & R is_transitive_in X & R is_antisymmetric_in X & R is_connected_in X ); end; :: deftheorem Def6 defines quasi_orders ORDERS_1:def_6_:_ for R being Relation for X being set holds ( R quasi_orders X iff ( R is_reflexive_in X & R is_transitive_in X ) ); :: deftheorem Def7 defines partially_orders ORDERS_1:def_7_:_ for R being Relation for X being set holds ( R partially_orders X iff ( R is_reflexive_in X & R is_transitive_in X & R is_antisymmetric_in X ) ); :: deftheorem defines linearly_orders ORDERS_1:def_8_:_ for R being Relation for X being set holds ( R linearly_orders X iff ( R is_reflexive_in X & R is_transitive_in X & R is_antisymmetric_in X & R is_connected_in X ) ); theorem Th28: :: ORDERS_1:28 for R being Relation for X being set st R well_orders X holds ( R quasi_orders X & R partially_orders X & R linearly_orders X ) proof let R be Relation; ::_thesis: for X being set st R well_orders X holds ( R quasi_orders X & R partially_orders X & R linearly_orders X ) let X be set ; ::_thesis: ( R well_orders X implies ( R quasi_orders X & R partially_orders X & R linearly_orders X ) ) assume that A1: R is_reflexive_in X and A2: R is_transitive_in X and A3: R is_antisymmetric_in X and A4: R is_connected_in X and R is_well_founded_in X ; :: according to WELLORD1:def_5 ::_thesis: ( R quasi_orders X & R partially_orders X & R linearly_orders X ) thus ( R is_reflexive_in X & R is_transitive_in X & R is_reflexive_in X & R is_transitive_in X & R is_antisymmetric_in X & R is_reflexive_in X & R is_transitive_in X & R is_antisymmetric_in X & R is_connected_in X ) by A1, A2, A3, A4; :: according to ORDERS_1:def_6,ORDERS_1:def_7,ORDERS_1:def_8 ::_thesis: verum end; theorem Th29: :: ORDERS_1:29 for R being Relation for X being set st R linearly_orders X holds ( R quasi_orders X & R partially_orders X ) proof let R be Relation; ::_thesis: for X being set st R linearly_orders X holds ( R quasi_orders X & R partially_orders X ) let X be set ; ::_thesis: ( R linearly_orders X implies ( R quasi_orders X & R partially_orders X ) ) assume that A1: R is_reflexive_in X and A2: R is_transitive_in X and A3: R is_antisymmetric_in X and R is_connected_in X ; :: according to ORDERS_1:def_8 ::_thesis: ( R quasi_orders X & R partially_orders X ) thus ( R is_reflexive_in X & R is_transitive_in X & R is_reflexive_in X & R is_transitive_in X & R is_antisymmetric_in X ) by A1, A2, A3; :: according to ORDERS_1:def_6,ORDERS_1:def_7 ::_thesis: verum end; theorem :: ORDERS_1:30 for R being Relation for X being set st R partially_orders X holds R quasi_orders X proof let R be Relation; ::_thesis: for X being set st R partially_orders X holds R quasi_orders X let X be set ; ::_thesis: ( R partially_orders X implies R quasi_orders X ) assume that A1: R is_reflexive_in X and A2: R is_transitive_in X and R is_antisymmetric_in X ; :: according to ORDERS_1:def_7 ::_thesis: R quasi_orders X thus ( R is_reflexive_in X & R is_transitive_in X ) by A1, A2; :: according to ORDERS_1:def_6 ::_thesis: verum end; theorem Th31: :: ORDERS_1:31 for R being Relation st R is being_quasi-order holds R quasi_orders field R proof let R be Relation; ::_thesis: ( R is being_quasi-order implies R quasi_orders field R ) assume that A1: R is_reflexive_in field R and A2: R is_transitive_in field R ; :: according to RELAT_2:def_9,RELAT_2:def_16,ORDERS_1:def_3 ::_thesis: R quasi_orders field R thus ( R is_reflexive_in field R & R is_transitive_in field R ) by A1, A2; :: according to ORDERS_1:def_6 ::_thesis: verum end; theorem :: ORDERS_1:32 for R being Relation for Y, X being set st R quasi_orders Y & X c= Y holds R quasi_orders X proof let R be Relation; ::_thesis: for Y, X being set st R quasi_orders Y & X c= Y holds R quasi_orders X let Y, X be set ; ::_thesis: ( R quasi_orders Y & X c= Y implies R quasi_orders X ) assume that A1: R is_reflexive_in Y and A2: R is_transitive_in Y and A3: X c= Y ; :: according to ORDERS_1:def_6 ::_thesis: R quasi_orders X thus ( R is_reflexive_in X & R is_transitive_in X ) by A1, A2, A3, Th8, Th10; :: according to ORDERS_1:def_6 ::_thesis: verum end; Lm6: for R being Relation for X being set st R is_reflexive_in X holds R |_2 X is reflexive proof let R be Relation; ::_thesis: for X being set st R is_reflexive_in X holds R |_2 X is reflexive let X be set ; ::_thesis: ( R is_reflexive_in X implies R |_2 X is reflexive ) assume A1: for x being set st x in X holds [x,x] in R ; :: according to RELAT_2:def_1 ::_thesis: R |_2 X is reflexive let x be set ; :: according to RELAT_2:def_1,RELAT_2:def_9 ::_thesis: ( not x in field (R |_2 X) or [x,x] in R |_2 X ) assume A2: x in field (R |_2 X) ; ::_thesis: [x,x] in R |_2 X then x in X by WELLORD1:12; then A3: [x,x] in [:X,X:] by ZFMISC_1:87; [x,x] in R by A1, A2, WELLORD1:12; hence [x,x] in R |_2 X by A3, XBOOLE_0:def_4; ::_thesis: verum end; Lm7: for R being Relation for X being set st R is_transitive_in X holds R |_2 X is transitive proof let R be Relation; ::_thesis: for X being set st R is_transitive_in X holds R |_2 X is transitive let X be set ; ::_thesis: ( R is_transitive_in X implies R |_2 X is transitive ) assume A1: for x, y, z being set st x in X & y in X & z in X & [x,y] in R & [y,z] in R holds [x,z] in R ; :: according to RELAT_2:def_8 ::_thesis: R |_2 X is transitive let x be set ; :: according to RELAT_2:def_8,RELAT_2:def_16 ::_thesis: for b1, b2 being set holds ( not x in field (R |_2 X) or not b1 in field (R |_2 X) or not b2 in field (R |_2 X) or not [x,b1] in R |_2 X or not [b1,b2] in R |_2 X or [x,b2] in R |_2 X ) let y, z be set ; ::_thesis: ( not x in field (R |_2 X) or not y in field (R |_2 X) or not z in field (R |_2 X) or not [x,y] in R |_2 X or not [y,z] in R |_2 X or [x,z] in R |_2 X ) assume that A2: x in field (R |_2 X) and A3: y in field (R |_2 X) and A4: z in field (R |_2 X) ; ::_thesis: ( not [x,y] in R |_2 X or not [y,z] in R |_2 X or [x,z] in R |_2 X ) A5: z in X by A4, WELLORD1:12; A6: x in X by A2, WELLORD1:12; then A7: [x,z] in [:X,X:] by A5, ZFMISC_1:87; assume that A8: [x,y] in R |_2 X and A9: [y,z] in R |_2 X ; ::_thesis: [x,z] in R |_2 X A10: [x,y] in R by A8, XBOOLE_0:def_4; A11: [y,z] in R by A9, XBOOLE_0:def_4; y in X by A3, WELLORD1:12; then [x,z] in R by A1, A6, A5, A10, A11; hence [x,z] in R |_2 X by A7, XBOOLE_0:def_4; ::_thesis: verum end; Lm8: for R being Relation for X being set st R is_antisymmetric_in X holds R |_2 X is antisymmetric proof let R be Relation; ::_thesis: for X being set st R is_antisymmetric_in X holds R |_2 X is antisymmetric let X be set ; ::_thesis: ( R is_antisymmetric_in X implies R |_2 X is antisymmetric ) assume A1: for x, y being set st x in X & y in X & [x,y] in R & [y,x] in R holds x = y ; :: according to RELAT_2:def_4 ::_thesis: R |_2 X is antisymmetric let x be set ; :: according to RELAT_2:def_4,RELAT_2:def_12 ::_thesis: for b1 being set holds ( not x in field (R |_2 X) or not b1 in field (R |_2 X) or not [x,b1] in R |_2 X or not [b1,x] in R |_2 X or x = b1 ) let y be set ; ::_thesis: ( not x in field (R |_2 X) or not y in field (R |_2 X) or not [x,y] in R |_2 X or not [y,x] in R |_2 X or x = y ) assume that A2: x in field (R |_2 X) and A3: y in field (R |_2 X) ; ::_thesis: ( not [x,y] in R |_2 X or not [y,x] in R |_2 X or x = y ) A4: y in X by A3, WELLORD1:12; assume that A5: [x,y] in R |_2 X and A6: [y,x] in R |_2 X ; ::_thesis: x = y A7: [x,y] in R by A5, XBOOLE_0:def_4; A8: [y,x] in R by A6, XBOOLE_0:def_4; x in X by A2, WELLORD1:12; hence x = y by A1, A4, A7, A8; ::_thesis: verum end; Lm9: for R being Relation for X being set st R is_connected_in X holds R |_2 X is connected proof let R be Relation; ::_thesis: for X being set st R is_connected_in X holds R |_2 X is connected let X be set ; ::_thesis: ( R is_connected_in X implies R |_2 X is connected ) assume A1: for x, y being set st x in X & y in X & x <> y & not [x,y] in R holds [y,x] in R ; :: according to RELAT_2:def_6 ::_thesis: R |_2 X is connected let x be set ; :: according to RELAT_2:def_6,RELAT_2:def_14 ::_thesis: for b1 being set holds ( not x in field (R |_2 X) or not b1 in field (R |_2 X) or x = b1 or [x,b1] in R |_2 X or [b1,x] in R |_2 X ) let y be set ; ::_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 A2: x in field (R |_2 X) and A3: y in field (R |_2 X) and A4: x <> y ; ::_thesis: ( [x,y] in R |_2 X or [y,x] in R |_2 X ) A5: y in X by A3, WELLORD1:12; A6: x in X by A2, WELLORD1:12; then A7: [x,y] in [:X,X:] by A5, ZFMISC_1:87; A8: [y,x] in [:X,X:] by A6, A5, ZFMISC_1:87; ( [x,y] in R or [y,x] in R ) by A1, A4, A6, A5; hence ( [x,y] in R |_2 X or [y,x] in R |_2 X ) by A7, A8, XBOOLE_0:def_4; ::_thesis: verum end; theorem :: ORDERS_1:33 for R being Relation for X being set st R quasi_orders X holds R |_2 X is being_quasi-order proof let R be Relation; ::_thesis: for X being set st R quasi_orders X holds R |_2 X is being_quasi-order let X be set ; ::_thesis: ( R quasi_orders X implies R |_2 X is being_quasi-order ) assume that A1: R is_reflexive_in X and A2: R is_transitive_in X ; :: according to ORDERS_1:def_6 ::_thesis: R |_2 X is being_quasi-order thus ( R |_2 X is reflexive & R |_2 X is transitive ) by A1, A2, Lm6, Lm7; :: according to ORDERS_1:def_3 ::_thesis: verum end; theorem Th34: :: ORDERS_1:34 for R being Relation st R is being_partial-order holds R partially_orders field R proof let R be Relation; ::_thesis: ( R is being_partial-order implies R partially_orders field R ) assume that A1: R is_reflexive_in field R and A2: R is_transitive_in field R and A3: R is_antisymmetric_in field R ; :: according to RELAT_2:def_9,RELAT_2:def_12,RELAT_2:def_16,ORDERS_1:def_4 ::_thesis: R partially_orders field R thus ( R is_reflexive_in field R & R is_transitive_in field R & R is_antisymmetric_in field R ) by A1, A2, A3; :: according to ORDERS_1:def_7 ::_thesis: verum end; theorem :: ORDERS_1:35 for R being Relation for Y, X being set st R partially_orders Y & X c= Y holds R partially_orders X proof let R be Relation; ::_thesis: for Y, X being set st R partially_orders Y & X c= Y holds R partially_orders X let Y, X be set ; ::_thesis: ( R partially_orders Y & X c= Y implies R partially_orders X ) assume that A1: R is_reflexive_in Y and A2: R is_transitive_in Y and A3: R is_antisymmetric_in Y and A4: X c= Y ; :: according to ORDERS_1:def_7 ::_thesis: R partially_orders X thus ( R is_reflexive_in X & R is_transitive_in X & R is_antisymmetric_in X ) by A1, A2, A3, A4, Th8, Th9, Th10; :: according to ORDERS_1:def_7 ::_thesis: verum end; theorem :: ORDERS_1:36 for R being Relation for X being set st R partially_orders X holds R |_2 X is being_partial-order proof let R be Relation; ::_thesis: for X being set st R partially_orders X holds R |_2 X is being_partial-order let X be set ; ::_thesis: ( R partially_orders X implies R |_2 X is being_partial-order ) assume that A1: R is_reflexive_in X and A2: R is_transitive_in X and A3: R is_antisymmetric_in X ; :: according to ORDERS_1:def_7 ::_thesis: R |_2 X is being_partial-order thus ( R |_2 X is reflexive & R |_2 X is transitive & R |_2 X is antisymmetric ) by A1, A2, A3, Lm6, Lm7, Lm8; :: according to ORDERS_1:def_4 ::_thesis: verum end; Lm10: for R being Relation for X, Y being set st R is_connected_in X & Y c= X holds R is_connected_in Y proof let R be Relation; ::_thesis: for X, Y being set st R is_connected_in X & Y c= X holds R is_connected_in Y let X, Y be set ; ::_thesis: ( R is_connected_in X & Y c= X implies R is_connected_in Y ) assume that A1: R is_connected_in X and A2: Y c= X ; ::_thesis: R is_connected_in Y let x be set ; :: according to RELAT_2:def_6 ::_thesis: for b1 being set holds ( not x in Y or not b1 in Y or x = b1 or [x,b1] in R or [b1,x] in R ) let y be set ; ::_thesis: ( not x in Y or not y in Y or x = y or [x,y] in R or [y,x] in R ) assume that A3: x in Y and A4: y in Y ; ::_thesis: ( x = y or [x,y] in R or [y,x] in R ) thus ( x = y or [x,y] in R or [y,x] in R ) by A1, A2, A3, A4, RELAT_2:def_6; ::_thesis: verum end; theorem :: ORDERS_1:37 for R being Relation st R is being_linear-order holds R linearly_orders field R proof let R be Relation; ::_thesis: ( R is being_linear-order implies R linearly_orders field R ) assume that A1: R is_reflexive_in field R and A2: R is_transitive_in field R and A3: R is_antisymmetric_in field R and A4: R is_connected_in field R ; :: according to RELAT_2:def_9,RELAT_2:def_12,RELAT_2:def_14,RELAT_2:def_16,ORDERS_1:def_5 ::_thesis: R linearly_orders field R thus ( R is_reflexive_in field R & R is_transitive_in field R & R is_antisymmetric_in field R & R is_connected_in field R ) by A1, A2, A3, A4; :: according to ORDERS_1:def_8 ::_thesis: verum end; theorem :: ORDERS_1:38 for R being Relation for Y, X being set st R linearly_orders Y & X c= Y holds R linearly_orders X proof let R be Relation; ::_thesis: for Y, X being set st R linearly_orders Y & X c= Y holds R linearly_orders X let Y, X be set ; ::_thesis: ( R linearly_orders Y & X c= Y implies R linearly_orders X ) assume that A1: R is_reflexive_in Y and A2: R is_transitive_in Y and A3: R is_antisymmetric_in Y and A4: R is_connected_in Y and A5: X c= Y ; :: according to ORDERS_1:def_8 ::_thesis: R linearly_orders X thus ( R is_reflexive_in X & R is_transitive_in X & R is_antisymmetric_in X & R is_connected_in X ) by A1, A2, A3, A4, A5, Lm10, Th8, Th9, Th10; :: according to ORDERS_1:def_8 ::_thesis: verum end; theorem :: ORDERS_1:39 for R being Relation for X being set st R linearly_orders X holds R |_2 X is being_linear-order proof let R be Relation; ::_thesis: for X being set st R linearly_orders X holds R |_2 X is being_linear-order let X be set ; ::_thesis: ( R linearly_orders X implies R |_2 X is being_linear-order ) assume that A1: R is_reflexive_in X and A2: R is_transitive_in X and A3: R is_antisymmetric_in X and A4: R is_connected_in X ; :: according to ORDERS_1:def_8 ::_thesis: R |_2 X is being_linear-order thus ( R |_2 X is reflexive & R |_2 X is transitive & R |_2 X is antisymmetric & R |_2 X is connected ) by A1, A2, A3, A4, Lm6, Lm7, Lm8, Lm9; :: according to ORDERS_1:def_5 ::_thesis: verum end; Lm11: for R being Relation for X being set st R is_reflexive_in X holds R ~ is_reflexive_in X proof let R be Relation; ::_thesis: for X being set st R is_reflexive_in X holds R ~ is_reflexive_in X let X be set ; ::_thesis: ( R is_reflexive_in X implies R ~ is_reflexive_in X ) assume A1: for x being set st x in X holds [x,x] in R ; :: according to RELAT_2:def_1 ::_thesis: R ~ is_reflexive_in X let x be set ; :: according to RELAT_2:def_1 ::_thesis: ( not x in X or [x,x] in R ~ ) assume x in X ; ::_thesis: [x,x] in R ~ then [x,x] in R by A1; hence [x,x] in R ~ by RELAT_1:def_7; ::_thesis: verum end; Lm12: for R being Relation for X being set st R is_transitive_in X holds R ~ is_transitive_in X proof let R be Relation; ::_thesis: for X being set st R is_transitive_in X holds R ~ is_transitive_in X let X be set ; ::_thesis: ( R is_transitive_in X implies R ~ is_transitive_in X ) assume A1: for x, y, z being set st x in X & y in X & z in X & [x,y] in R & [y,z] in R holds [x,z] in R ; :: according to RELAT_2:def_8 ::_thesis: R ~ is_transitive_in X let x be set ; :: according to RELAT_2:def_8 ::_thesis: for b1, b2 being set holds ( not x in X or not b1 in X or not b2 in X or not [x,b1] in R ~ or not [b1,b2] in R ~ or [x,b2] in R ~ ) let y, z be set ; ::_thesis: ( not x in X or not y in X or not z in X or not [x,y] in R ~ or not [y,z] in R ~ or [x,z] in R ~ ) assume that A2: x in X and A3: y in X and A4: z in X and A5: [x,y] in R ~ and A6: [y,z] in R ~ ; ::_thesis: [x,z] in R ~ A7: [z,y] in R by A6, RELAT_1:def_7; [y,x] in R by A5, RELAT_1:def_7; then [z,x] in R by A1, A2, A3, A4, A7; hence [x,z] in R ~ by RELAT_1:def_7; ::_thesis: verum end; Lm13: for R being Relation for X being set st R is_antisymmetric_in X holds R ~ is_antisymmetric_in X proof let R be Relation; ::_thesis: for X being set st R is_antisymmetric_in X holds R ~ is_antisymmetric_in X let X be set ; ::_thesis: ( R is_antisymmetric_in X implies R ~ is_antisymmetric_in X ) assume A1: for x, y being set st x in X & y in X & [x,y] in R & [y,x] in R holds x = y ; :: according to RELAT_2:def_4 ::_thesis: R ~ is_antisymmetric_in X let x be set ; :: according to RELAT_2:def_4 ::_thesis: for b1 being set holds ( not x in X or not b1 in X or not [x,b1] in R ~ or not [b1,x] in R ~ or x = b1 ) let y be set ; ::_thesis: ( not x in X or not y in X or not [x,y] in R ~ or not [y,x] in R ~ or x = y ) assume that A2: x in X and A3: y in X and A4: [x,y] in R ~ and A5: [y,x] in R ~ ; ::_thesis: x = y A6: [y,x] in R by A4, RELAT_1:def_7; [x,y] in R by A5, RELAT_1:def_7; hence x = y by A1, A2, A3, A6; ::_thesis: verum end; Lm14: for R being Relation for X being set st R is_connected_in X holds R ~ is_connected_in X proof let R be Relation; ::_thesis: for X being set st R is_connected_in X holds R ~ is_connected_in X let X be set ; ::_thesis: ( R is_connected_in X implies R ~ is_connected_in X ) assume A1: for x, y being set st x in X & y in X & x <> y & not [x,y] in R holds [y,x] in R ; :: according to RELAT_2:def_6 ::_thesis: R ~ is_connected_in X let x be set ; :: according to RELAT_2:def_6 ::_thesis: for b1 being set holds ( not x in X or not b1 in X or x = b1 or [x,b1] in R ~ or [b1,x] in R ~ ) let y be set ; ::_thesis: ( not x in X or not y in X or x = y or [x,y] in R ~ or [y,x] in R ~ ) assume that A2: x in X and A3: y in X and A4: x <> y ; ::_thesis: ( [x,y] in R ~ or [y,x] in R ~ ) ( [x,y] in R or [y,x] in R ) by A1, A2, A3, A4; hence ( [x,y] in R ~ or [y,x] in R ~ ) by RELAT_1:def_7; ::_thesis: verum end; theorem :: ORDERS_1:40 for R being Relation for X being set st R quasi_orders X holds R ~ quasi_orders X proof let R be Relation; ::_thesis: for X being set st R quasi_orders X holds R ~ quasi_orders X let X be set ; ::_thesis: ( R quasi_orders X implies R ~ quasi_orders X ) assume that A1: R is_reflexive_in X and A2: R is_transitive_in X ; :: according to ORDERS_1:def_6 ::_thesis: R ~ quasi_orders X thus ( R ~ is_reflexive_in X & R ~ is_transitive_in X ) by A1, A2, Lm11, Lm12; :: according to ORDERS_1:def_6 ::_thesis: verum end; theorem Th41: :: ORDERS_1:41 for R being Relation for X being set st R partially_orders X holds R ~ partially_orders X proof let R be Relation; ::_thesis: for X being set st R partially_orders X holds R ~ partially_orders X let X be set ; ::_thesis: ( R partially_orders X implies R ~ partially_orders X ) assume that A1: R is_reflexive_in X and A2: R is_transitive_in X and A3: R is_antisymmetric_in X ; :: according to ORDERS_1:def_7 ::_thesis: R ~ partially_orders X thus ( R ~ is_reflexive_in X & R ~ is_transitive_in X & R ~ is_antisymmetric_in X ) by A1, A2, A3, Lm11, Lm12, Lm13; :: according to ORDERS_1:def_7 ::_thesis: verum end; theorem :: ORDERS_1:42 for R being Relation for X being set st R linearly_orders X holds R ~ linearly_orders X proof let R be Relation; ::_thesis: for X being set st R linearly_orders X holds R ~ linearly_orders X let X be set ; ::_thesis: ( R linearly_orders X implies R ~ linearly_orders X ) assume that A1: R is_reflexive_in X and A2: R is_transitive_in X and A3: R is_antisymmetric_in X and A4: R is_connected_in X ; :: according to ORDERS_1:def_8 ::_thesis: R ~ linearly_orders X thus ( R ~ is_reflexive_in X & R ~ is_transitive_in X & R ~ is_antisymmetric_in X & R ~ is_connected_in X ) by A1, A2, A3, A4, Lm11, Lm12, Lm13, Lm14; :: according to ORDERS_1:def_8 ::_thesis: verum end; theorem :: ORDERS_1:43 for X being set for O being Order of X holds O quasi_orders X proof let X be set ; ::_thesis: for O being Order of X holds O quasi_orders X let O be Order of X; ::_thesis: O quasi_orders X A1: field O = X by Lm2; then A2: O is_transitive_in X by RELAT_2:def_16; O is_reflexive_in X by A1, RELAT_2:def_9; hence O quasi_orders X by A2, Def6; ::_thesis: verum end; theorem :: ORDERS_1:44 for X being set for O being Order of X holds O partially_orders X proof let X be set ; ::_thesis: for O being Order of X holds O partially_orders X let O be Order of X; ::_thesis: O partially_orders X A1: field O = X by Lm2; then A2: O is_antisymmetric_in X by RELAT_2:def_12; A3: O is_transitive_in X by A1, RELAT_2:def_16; O is_reflexive_in X by A1, RELAT_2:def_9; hence O partially_orders X by A2, A3, Def7; ::_thesis: verum end; theorem Th45: :: ORDERS_1:45 for R being Relation for X being set st R partially_orders X holds R |_2 X is Order of X proof let R be Relation; ::_thesis: for X being set st R partially_orders X holds R |_2 X is Order of X let X be set ; ::_thesis: ( R partially_orders X implies R |_2 X is Order of X ) set S = R |_2 X; A1: field (R |_2 X) c= X by WELLORD1:13; rng (R |_2 X) c= field (R |_2 X) by XBOOLE_1:7; then A2: rng (R |_2 X) c= X by A1, XBOOLE_1:1; dom (R |_2 X) c= field (R |_2 X) by XBOOLE_1:7; then dom (R |_2 X) c= X by A1, XBOOLE_1:1; then reconsider S = R |_2 X as Relation of X by A2, RELSET_1:4; assume A3: R partially_orders X ; ::_thesis: R |_2 X is Order of X A4: R |_2 X is_antisymmetric_in X proof A5: R is_antisymmetric_in X by A3, Def7; let x be set ; :: according to RELAT_2:def_4 ::_thesis: for b1 being set holds ( not x in X or not b1 in X or not [x,b1] in R |_2 X or not [b1,x] in R |_2 X or x = b1 ) let y be set ; ::_thesis: ( not x in X or not y in X or not [x,y] in R |_2 X or not [y,x] in R |_2 X or x = y ) assume that A6: x in X and A7: y in X and A8: [x,y] in R |_2 X and A9: [y,x] in R |_2 X ; ::_thesis: x = y A10: [y,x] in R by A9, XBOOLE_0:def_4; [x,y] in R by A8, XBOOLE_0:def_4; hence x = y by A6, A7, A10, A5, RELAT_2:def_4; ::_thesis: verum end; A11: R |_2 X is_transitive_in X proof A12: R is_transitive_in X by A3, Def7; let x be set ; :: according to RELAT_2:def_8 ::_thesis: for b1, b2 being set holds ( not x in X or not b1 in X or not b2 in X or not [x,b1] in R |_2 X or not [b1,b2] in R |_2 X or [x,b2] in R |_2 X ) let y, z be set ; ::_thesis: ( not x in X or not y in X or not z in X or not [x,y] in R |_2 X or not [y,z] in R |_2 X or [x,z] in R |_2 X ) assume that A13: x in X and A14: y in X and A15: z in X and A16: [x,y] in R |_2 X and A17: [y,z] in R |_2 X ; ::_thesis: [x,z] in R |_2 X A18: [x,z] in [:X,X:] by A13, A15, ZFMISC_1:87; A19: [y,z] in R by A17, XBOOLE_0:def_4; [x,y] in R by A16, XBOOLE_0:def_4; then [x,z] in R by A13, A14, A15, A19, A12, RELAT_2:def_8; hence [x,z] in R |_2 X by A18, XBOOLE_0:def_4; ::_thesis: verum end; A20: R is_reflexive_in X by A3, Def7; A21: R |_2 X is_reflexive_in X proof let x be set ; :: according to RELAT_2:def_1 ::_thesis: ( not x in X or [x,x] in R |_2 X ) assume A22: x in X ; ::_thesis: [x,x] in R |_2 X then A23: [x,x] in [:X,X:] by ZFMISC_1:87; [x,x] in R by A20, A22, RELAT_2:def_1; hence [x,x] in R |_2 X by A23, XBOOLE_0:def_4; ::_thesis: verum end; then A24: field S = X by Th13; dom S = X by A21, Th13; hence R |_2 X is Order of X by A21, A24, A4, A11, PARTFUN1:def_2, RELAT_2:def_9, RELAT_2:def_12, RELAT_2:def_16; ::_thesis: verum end; theorem :: ORDERS_1:46 for R being Relation for X being set st R linearly_orders X holds R |_2 X is Order of X by Th29, Th45; theorem :: ORDERS_1:47 for R being Relation for X being set st R well_orders X holds R |_2 X is Order of X by Th28, Th45; theorem :: ORDERS_1:48 for X being set holds ( id X quasi_orders X & id X partially_orders X ) proof let X be set ; ::_thesis: ( id X quasi_orders X & id X partially_orders X ) field (id X) = X \/ (rng (id X)) .= X \/ X .= X ; hence ( id X quasi_orders X & id X partially_orders X ) by Th31, Th34; ::_thesis: verum end; definition let R be Relation; let X be set ; predX has_upper_Zorn_property_wrt R means :Def9: :: ORDERS_1:def 9 for Y being set st Y c= X & R |_2 Y is being_linear-order holds ex x being set st ( x in X & ( for y being set st y in Y holds [y,x] in R ) ); predX has_lower_Zorn_property_wrt R means :: ORDERS_1:def 10 for Y being set st Y c= X & R |_2 Y is being_linear-order holds ex x being set st ( x in X & ( for y being set st y in Y holds [x,y] in R ) ); end; :: deftheorem Def9 defines has_upper_Zorn_property_wrt ORDERS_1:def_9_:_ for R being Relation for X being set holds ( X has_upper_Zorn_property_wrt R iff for Y being set st Y c= X & R |_2 Y is being_linear-order holds ex x being set st ( x in X & ( for y being set st y in Y holds [y,x] in R ) ) ); :: deftheorem defines has_lower_Zorn_property_wrt ORDERS_1:def_10_:_ for R being Relation for X being set holds ( X has_lower_Zorn_property_wrt R iff for Y being set st Y c= X & R |_2 Y is being_linear-order holds ex x being set st ( x in X & ( for y being set st y in Y holds [x,y] in R ) ) ); Lm15: for R being Relation for X being set holds (R |_2 X) ~ = (R ~) |_2 X proof let R be Relation; ::_thesis: for X being set holds (R |_2 X) ~ = (R ~) |_2 X let X be set ; ::_thesis: (R |_2 X) ~ = (R ~) |_2 X now__::_thesis:_for_x,_y_being_set_holds_ (_(_[x,y]_in_(R_~)_|_2_X_implies_[y,x]_in_R_|_2_X_)_&_(_[y,x]_in_R_|_2_X_implies_[x,y]_in_(R_~)_|_2_X_)_) let x, y be set ; ::_thesis: ( ( [x,y] in (R ~) |_2 X implies [y,x] in R |_2 X ) & ( [y,x] in R |_2 X implies [x,y] in (R ~) |_2 X ) ) thus ( [x,y] in (R ~) |_2 X implies [y,x] in R |_2 X ) ::_thesis: ( [y,x] in R |_2 X implies [x,y] in (R ~) |_2 X ) proof assume A1: [x,y] in (R ~) |_2 X ; ::_thesis: [y,x] in R |_2 X then [x,y] in [:X,X:] by XBOOLE_0:def_4; then A2: [y,x] in [:X,X:] by ZFMISC_1:88; [x,y] in R ~ by A1, XBOOLE_0:def_4; then [y,x] in R by RELAT_1:def_7; hence [y,x] in R |_2 X by A2, XBOOLE_0:def_4; ::_thesis: verum end; assume A3: [y,x] in R |_2 X ; ::_thesis: [x,y] in (R ~) |_2 X then [y,x] in [:X,X:] by XBOOLE_0:def_4; then A4: [x,y] in [:X,X:] by ZFMISC_1:88; [y,x] in R by A3, XBOOLE_0:def_4; then [x,y] in R ~ by RELAT_1:def_7; hence [x,y] in (R ~) |_2 X by A4, XBOOLE_0:def_4; ::_thesis: verum end; hence (R |_2 X) ~ = (R ~) |_2 X by RELAT_1:def_7; ::_thesis: verum end; Lm16: now__::_thesis:_for_R_being_Relation_holds_R_|_2_{}_=_{} let R be Relation; ::_thesis: R |_2 {} = {} thus R |_2 {} = ({} |` R) | {} by WELLORD1:10 .= {} ; ::_thesis: verum end; theorem Th49: :: ORDERS_1:49 for R being Relation for X being set st X has_upper_Zorn_property_wrt R holds X <> {} proof let R be Relation; ::_thesis: for X being set st X has_upper_Zorn_property_wrt R holds X <> {} let X be set ; ::_thesis: ( X has_upper_Zorn_property_wrt R implies X <> {} ) assume A1: for Y being set st Y c= X & R |_2 Y is being_linear-order holds ex x being set st ( x in X & ( for y being set st y in Y holds [y,x] in R ) ) ; :: according to ORDERS_1:def_9 ::_thesis: X <> {} R |_2 {} is being_linear-order by Lm16; then ex x being set st ( x in X & ( for y being set st y in {} holds [y,x] in R ) ) by A1, XBOOLE_1:2; hence X <> {} ; ::_thesis: verum end; theorem :: ORDERS_1:50 for R being Relation for X being set st X has_lower_Zorn_property_wrt R holds X <> {} proof let R be Relation; ::_thesis: for X being set st X has_lower_Zorn_property_wrt R holds X <> {} let X be set ; ::_thesis: ( X has_lower_Zorn_property_wrt R implies X <> {} ) assume A1: for Y being set st Y c= X & R |_2 Y is being_linear-order holds ex x being set st ( x in X & ( for y being set st y in Y holds [x,y] in R ) ) ; :: according to ORDERS_1:def_10 ::_thesis: X <> {} R |_2 {} is being_linear-order by Lm16; then ex x being set st ( x in X & ( for y being set st y in {} holds [x,y] in R ) ) by A1, XBOOLE_1:2; hence X <> {} ; ::_thesis: verum end; theorem Th51: :: ORDERS_1:51 for R being Relation for X being set holds ( X has_upper_Zorn_property_wrt R iff X has_lower_Zorn_property_wrt R ~ ) proof let R be Relation; ::_thesis: for X being set holds ( X has_upper_Zorn_property_wrt R iff X has_lower_Zorn_property_wrt R ~ ) let X be set ; ::_thesis: ( X has_upper_Zorn_property_wrt R iff X has_lower_Zorn_property_wrt R ~ ) thus ( X has_upper_Zorn_property_wrt R implies X has_lower_Zorn_property_wrt R ~ ) ::_thesis: ( X has_lower_Zorn_property_wrt R ~ implies X has_upper_Zorn_property_wrt R ) proof assume A1: for Y being set st Y c= X & R |_2 Y is being_linear-order holds ex x being set st ( x in X & ( for y being set st y in Y holds [y,x] in R ) ) ; :: according to ORDERS_1:def_9 ::_thesis: X has_lower_Zorn_property_wrt R ~ let Y be set ; :: according to ORDERS_1:def_10 ::_thesis: ( Y c= X & (R ~) |_2 Y is being_linear-order implies ex x being set st ( x in X & ( for y being set st y in Y holds [x,y] in R ~ ) ) ) A2: ((R |_2 Y) ~) ~ = R |_2 Y ; assume that A3: Y c= X and A4: (R ~) |_2 Y is being_linear-order ; ::_thesis: ex x being set st ( x in X & ( for y being set st y in Y holds [x,y] in R ~ ) ) (R ~) |_2 Y = (R |_2 Y) ~ by Lm15; then consider x being set such that A5: x in X and A6: for y being set st y in Y holds [y,x] in R by A1, A2, A3, A4, Th18; take x ; ::_thesis: ( x in X & ( for y being set st y in Y holds [x,y] in R ~ ) ) thus x in X by A5; ::_thesis: for y being set st y in Y holds [x,y] in R ~ let y be set ; ::_thesis: ( y in Y implies [x,y] in R ~ ) assume y in Y ; ::_thesis: [x,y] in R ~ then [y,x] in R by A6; hence [x,y] in R ~ by RELAT_1:def_7; ::_thesis: verum end; assume A7: for Y being set st Y c= X & (R ~) |_2 Y is being_linear-order holds ex x being set st ( x in X & ( for y being set st y in Y holds [x,y] in R ~ ) ) ; :: according to ORDERS_1:def_10 ::_thesis: X has_upper_Zorn_property_wrt R let Y be set ; :: according to ORDERS_1:def_9 ::_thesis: ( Y c= X & R |_2 Y is being_linear-order implies ex x being set st ( x in X & ( for y being set st y in Y holds [y,x] in R ) ) ) assume that A8: Y c= X and A9: R |_2 Y is being_linear-order ; ::_thesis: ex x being set st ( x in X & ( for y being set st y in Y holds [y,x] in R ) ) (R ~) |_2 Y = (R |_2 Y) ~ by Lm15; then consider x being set such that A10: x in X and A11: for y being set st y in Y holds [x,y] in R ~ by A7, A8, A9, Th18; take x ; ::_thesis: ( x in X & ( for y being set st y in Y holds [y,x] in R ) ) thus x in X by A10; ::_thesis: for y being set st y in Y holds [y,x] in R let y be set ; ::_thesis: ( y in Y implies [y,x] in R ) assume y in Y ; ::_thesis: [y,x] in R then [x,y] in R ~ by A11; hence [y,x] in R by RELAT_1:def_7; ::_thesis: verum end; theorem :: ORDERS_1:52 for R being Relation for X being set holds ( X has_upper_Zorn_property_wrt R ~ iff X has_lower_Zorn_property_wrt R ) proof let R be Relation; ::_thesis: for X being set holds ( X has_upper_Zorn_property_wrt R ~ iff X has_lower_Zorn_property_wrt R ) let X be set ; ::_thesis: ( X has_upper_Zorn_property_wrt R ~ iff X has_lower_Zorn_property_wrt R ) (R ~) ~ = R ; hence ( X has_upper_Zorn_property_wrt R ~ iff X has_lower_Zorn_property_wrt R ) by Th51; ::_thesis: verum end; definition let R be Relation; let x be set ; predx is_maximal_in R means :Def11: :: ORDERS_1:def 11 ( x in field R & ( for y being set holds ( not y in field R or not y <> x or not [x,y] in R ) ) ); predx is_minimal_in R means :Def12: :: ORDERS_1:def 12 ( x in field R & ( for y being set holds ( not y in field R or not y <> x or not [y,x] in R ) ) ); predx is_superior_of R means :Def13: :: ORDERS_1:def 13 ( x in field R & ( for y being set st y in field R & y <> x holds [y,x] in R ) ); predx is_inferior_of R means :Def14: :: ORDERS_1:def 14 ( x in field R & ( for y being set st y in field R & y <> x holds [x,y] in R ) ); end; :: deftheorem Def11 defines is_maximal_in ORDERS_1:def_11_:_ for R being Relation for x being set holds ( x is_maximal_in R iff ( x in field R & ( for y being set holds ( not y in field R or not y <> x or not [x,y] in R ) ) ) ); :: deftheorem Def12 defines is_minimal_in ORDERS_1:def_12_:_ for R being Relation for x being set holds ( x is_minimal_in R iff ( x in field R & ( for y being set holds ( not y in field R or not y <> x or not [y,x] in R ) ) ) ); :: deftheorem Def13 defines is_superior_of ORDERS_1:def_13_:_ for R being Relation for x being set holds ( x is_superior_of R iff ( x in field R & ( for y being set st y in field R & y <> x holds [y,x] in R ) ) ); :: deftheorem Def14 defines is_inferior_of ORDERS_1:def_14_:_ for R being Relation for x being set holds ( x is_inferior_of R iff ( x in field R & ( for y being set st y in field R & y <> x holds [x,y] in R ) ) ); theorem :: ORDERS_1:53 for R being Relation for x being set st x is_inferior_of R & R is antisymmetric holds x is_minimal_in R proof let R be Relation; ::_thesis: for x being set st x is_inferior_of R & R is antisymmetric holds x is_minimal_in R let x be set ; ::_thesis: ( x is_inferior_of R & R is antisymmetric implies x is_minimal_in R ) assume that A1: x is_inferior_of R and A2: R is antisymmetric ; ::_thesis: x is_minimal_in R A3: R is_antisymmetric_in field R by A2, RELAT_2:def_12; thus A4: x in field R by A1, Def14; :: according to ORDERS_1:def_12 ::_thesis: for y being set holds ( not y in field R or not y <> x or not [y,x] in R ) let y be set ; ::_thesis: ( not y in field R or not y <> x or not [y,x] in R ) assume that A5: y in field R and A6: y <> x and A7: [y,x] in R ; ::_thesis: contradiction [x,y] in R by A1, A5, A6, Def14; hence contradiction by A4, A5, A6, A7, A3, RELAT_2:def_4; ::_thesis: verum end; theorem :: ORDERS_1:54 for R being Relation for x being set st x is_superior_of R & R is antisymmetric holds x is_maximal_in R proof let R be Relation; ::_thesis: for x being set st x is_superior_of R & R is antisymmetric holds x is_maximal_in R let x be set ; ::_thesis: ( x is_superior_of R & R is antisymmetric implies x is_maximal_in R ) assume that A1: x is_superior_of R and A2: R is antisymmetric ; ::_thesis: x is_maximal_in R A3: R is_antisymmetric_in field R by A2, RELAT_2:def_12; thus A4: x in field R by A1, Def13; :: according to ORDERS_1:def_11 ::_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 A5: y in field R and A6: y <> x and A7: [x,y] in R ; ::_thesis: contradiction [y,x] in R by A1, A5, A6, Def13; hence contradiction by A4, A5, A6, A7, A3, RELAT_2:def_4; ::_thesis: verum end; theorem :: ORDERS_1:55 for R being Relation for x being set st x is_minimal_in R & R is connected holds x is_inferior_of R proof let R be Relation; ::_thesis: for x being set st x is_minimal_in R & R is connected holds x is_inferior_of R let x be set ; ::_thesis: ( x is_minimal_in R & R is connected implies x is_inferior_of R ) assume that A1: x is_minimal_in R and A2: R is connected ; ::_thesis: x is_inferior_of R thus A3: x in field R by A1, Def12; :: according to ORDERS_1:def_14 ::_thesis: for y being set st y in field R & y <> x holds [x,y] in R let y be set ; ::_thesis: ( y in field R & y <> x implies [x,y] in R ) assume that A4: y in field R and A5: y <> x ; ::_thesis: [x,y] in R R is_connected_in field R by A2, RELAT_2:def_14; then ( [x,y] in R or [y,x] in R ) by A3, A4, A5, RELAT_2:def_6; hence [x,y] in R by A1, A4, Def12; ::_thesis: verum end; theorem :: ORDERS_1:56 for R being Relation for x being set st x is_maximal_in R & R is connected holds x is_superior_of R proof let R be Relation; ::_thesis: for x being set st x is_maximal_in R & R is connected holds x is_superior_of R let x be set ; ::_thesis: ( x is_maximal_in R & R is connected implies x is_superior_of R ) assume that A1: x is_maximal_in R and A2: R is connected ; ::_thesis: x is_superior_of R thus A3: x in field R by A1, Def11; :: according to ORDERS_1:def_13 ::_thesis: for y being set st y in field R & y <> x holds [y,x] in R let y be set ; ::_thesis: ( y in field R & y <> x implies [y,x] in R ) assume that A4: y in field R and A5: y <> x ; ::_thesis: [y,x] in R R is_connected_in field R by A2, RELAT_2:def_14; then ( [x,y] in R or [y,x] in R ) by A3, A4, A5, RELAT_2:def_6; hence [y,x] in R by A1, A4, Def11; ::_thesis: verum end; theorem :: ORDERS_1:57 for R being Relation for x, X being set st x in X & x is_superior_of R & X c= field R & R is reflexive holds X has_upper_Zorn_property_wrt R proof let R be Relation; ::_thesis: for x, X being set st x in X & x is_superior_of R & X c= field R & R is reflexive holds X has_upper_Zorn_property_wrt R let x, X be set ; ::_thesis: ( x in X & x is_superior_of R & X c= field R & R is reflexive implies X has_upper_Zorn_property_wrt R ) assume that A1: x in X and A2: x is_superior_of R and A3: X c= field R and A4: R is_reflexive_in field R ; :: according to RELAT_2:def_9 ::_thesis: X has_upper_Zorn_property_wrt R let Y be set ; :: according to ORDERS_1:def_9 ::_thesis: ( Y c= X & R |_2 Y is being_linear-order implies ex x being set st ( x in X & ( for y being set st y in Y holds [y,x] in R ) ) ) assume that A5: Y c= X and R |_2 Y is being_linear-order ; ::_thesis: ex x being set st ( x in X & ( for y being set st y in Y holds [y,x] in R ) ) take x ; ::_thesis: ( x in X & ( for y being set st y in Y holds [y,x] in R ) ) thus x in X by A1; ::_thesis: for y being set st y in Y holds [y,x] in R let y be set ; ::_thesis: ( y in Y implies [y,x] in R ) assume y in Y ; ::_thesis: [y,x] in R then A6: y in X by A5; ( y = x or y <> x ) ; hence [y,x] in R by A2, A3, A4, A6, Def13, RELAT_2:def_1; ::_thesis: verum end; theorem :: ORDERS_1:58 for R being Relation for x, X being set st x in X & x is_inferior_of R & X c= field R & R is reflexive holds X has_lower_Zorn_property_wrt R proof let R be Relation; ::_thesis: for x, X being set st x in X & x is_inferior_of R & X c= field R & R is reflexive holds X has_lower_Zorn_property_wrt R let x, X be set ; ::_thesis: ( x in X & x is_inferior_of R & X c= field R & R is reflexive implies X has_lower_Zorn_property_wrt R ) assume that A1: x in X and A2: x is_inferior_of R and A3: X c= field R and A4: R is_reflexive_in field R ; :: according to RELAT_2:def_9 ::_thesis: X has_lower_Zorn_property_wrt R let Y be set ; :: according to ORDERS_1:def_10 ::_thesis: ( Y c= X & R |_2 Y is being_linear-order implies ex x being set st ( x in X & ( for y being set st y in Y holds [x,y] in R ) ) ) assume that A5: Y c= X and R |_2 Y is being_linear-order ; ::_thesis: ex x being set st ( x in X & ( for y being set st y in Y holds [x,y] in R ) ) take x ; ::_thesis: ( x in X & ( for y being set st y in Y holds [x,y] in R ) ) thus x in X by A1; ::_thesis: for y being set st y in Y holds [x,y] in R let y be set ; ::_thesis: ( y in Y implies [x,y] in R ) assume y in Y ; ::_thesis: [x,y] in R then A6: y in X by A5; ( y = x or y <> x ) ; hence [x,y] in R by A2, A3, A4, A6, Def14, RELAT_2:def_1; ::_thesis: verum end; theorem Th59: :: ORDERS_1:59 for R being Relation for x being set holds ( x is_minimal_in R iff x is_maximal_in R ~ ) proof let R be Relation; ::_thesis: for x being set holds ( x is_minimal_in R iff x is_maximal_in R ~ ) let x be set ; ::_thesis: ( x is_minimal_in R iff x is_maximal_in R ~ ) A1: field R = field (R ~) by RELAT_1:21; thus ( x is_minimal_in R implies x is_maximal_in R ~ ) ::_thesis: ( x is_maximal_in R ~ implies x is_minimal_in R ) proof assume that A2: x in field R and A3: for y being set holds ( not y in field R or not y <> x or not [y,x] in R ) ; :: according to ORDERS_1:def_12 ::_thesis: x is_maximal_in R ~ thus x in field (R ~) by A2, RELAT_1:21; :: according to ORDERS_1:def_11 ::_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 A4: y in field (R ~) and A5: y <> x ; ::_thesis: not [x,y] in R ~ not [y,x] in R by A1, A3, A4, A5; hence not [x,y] in R ~ by RELAT_1:def_7; ::_thesis: verum end; assume that A6: x in field (R ~) and A7: for y being set holds ( not y in field (R ~) or not y <> x or not [x,y] in R ~ ) ; :: according to ORDERS_1:def_11 ::_thesis: x is_minimal_in R thus x in field R by A6, RELAT_1:21; :: according to ORDERS_1:def_12 ::_thesis: for y being set holds ( not y in field R or not y <> x or not [y,x] in R ) let y be set ; ::_thesis: ( not y in field R or not y <> x or not [y,x] in R ) assume that A8: y in field R and A9: y <> x ; ::_thesis: not [y,x] in R not [x,y] in R ~ by A1, A7, A8, A9; hence not [y,x] in R by RELAT_1:def_7; ::_thesis: verum end; theorem :: ORDERS_1:60 for R being Relation for x being set holds ( x is_minimal_in R ~ iff x is_maximal_in R ) proof let R be Relation; ::_thesis: for x being set holds ( x is_minimal_in R ~ iff x is_maximal_in R ) let x be set ; ::_thesis: ( x is_minimal_in R ~ iff x is_maximal_in R ) A1: field R = field (R ~) by RELAT_1:21; thus ( x is_minimal_in R ~ implies x is_maximal_in R ) ::_thesis: ( x is_maximal_in R implies x is_minimal_in R ~ ) proof assume that A2: x in field (R ~) and A3: for y being set holds ( not y in field (R ~) or not y <> x or not [y,x] in R ~ ) ; :: according to ORDERS_1:def_12 ::_thesis: x is_maximal_in R thus x in field R by A2, RELAT_1:21; :: according to ORDERS_1:def_11 ::_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 A4: y in field R and A5: y <> x ; ::_thesis: not [x,y] in R not [y,x] in R ~ by A1, A3, A4, A5; hence not [x,y] in R by RELAT_1:def_7; ::_thesis: verum end; assume that A6: x in field R and A7: for y being set holds ( not y in field R or not y <> x or not [x,y] in R ) ; :: according to ORDERS_1:def_11 ::_thesis: x is_minimal_in R ~ thus x in field (R ~) by A6, RELAT_1:21; :: according to ORDERS_1:def_12 ::_thesis: for y being set holds ( not y in field (R ~) or not y <> x or not [y,x] in R ~ ) let y be set ; ::_thesis: ( not y in field (R ~) or not y <> x or not [y,x] in R ~ ) assume that A8: y in field (R ~) and A9: y <> x ; ::_thesis: not [y,x] in R ~ not [x,y] in R by A1, A7, A8, A9; hence not [y,x] in R ~ by RELAT_1:def_7; ::_thesis: verum end; theorem :: ORDERS_1:61 for R being Relation for x being set holds ( x is_inferior_of R iff x is_superior_of R ~ ) proof let R be Relation; ::_thesis: for x being set holds ( x is_inferior_of R iff x is_superior_of R ~ ) let x be set ; ::_thesis: ( x is_inferior_of R iff x is_superior_of R ~ ) A1: field R = field (R ~) by RELAT_1:21; thus ( x is_inferior_of R implies x is_superior_of R ~ ) ::_thesis: ( x is_superior_of R ~ implies x is_inferior_of R ) proof assume that A2: x in field R and A3: for y being set st y in field R & y <> x holds [x,y] in R ; :: according to ORDERS_1:def_14 ::_thesis: x is_superior_of R ~ thus x in field (R ~) by A2, RELAT_1:21; :: according to ORDERS_1:def_13 ::_thesis: for y being set st y in field (R ~) & y <> x holds [y,x] in R ~ let y be set ; ::_thesis: ( y in field (R ~) & y <> x implies [y,x] in R ~ ) assume that A4: y in field (R ~) and A5: y <> x ; ::_thesis: [y,x] in R ~ [x,y] in R by A1, A3, A4, A5; hence [y,x] in R ~ by RELAT_1:def_7; ::_thesis: verum end; assume that A6: x in field (R ~) and A7: for y being set st y in field (R ~) & y <> x holds [y,x] in R ~ ; :: according to ORDERS_1:def_13 ::_thesis: x is_inferior_of R thus x in field R by A6, RELAT_1:21; :: according to ORDERS_1:def_14 ::_thesis: for y being set st y in field R & y <> x holds [x,y] in R let y be set ; ::_thesis: ( y in field R & y <> x implies [x,y] in R ) assume that A8: y in field R and A9: y <> x ; ::_thesis: [x,y] in R [y,x] in R ~ by A1, A7, A8, A9; hence [x,y] in R by RELAT_1:def_7; ::_thesis: verum end; theorem :: ORDERS_1:62 for R being Relation for x being set holds ( x is_inferior_of R ~ iff x is_superior_of R ) proof let R be Relation; ::_thesis: for x being set holds ( x is_inferior_of R ~ iff x is_superior_of R ) let x be set ; ::_thesis: ( x is_inferior_of R ~ iff x is_superior_of R ) A1: field R = field (R ~) by RELAT_1:21; thus ( x is_inferior_of R ~ implies x is_superior_of R ) ::_thesis: ( x is_superior_of R implies x is_inferior_of R ~ ) proof assume that A2: x in field (R ~) and A3: for y being set st y in field (R ~) & y <> x holds [x,y] in R ~ ; :: according to ORDERS_1:def_14 ::_thesis: x is_superior_of R thus x in field R by A2, RELAT_1:21; :: according to ORDERS_1:def_13 ::_thesis: for y being set st y in field R & y <> x holds [y,x] in R let y be set ; ::_thesis: ( y in field R & y <> x implies [y,x] in R ) assume that A4: y in field R and A5: y <> x ; ::_thesis: [y,x] in R [x,y] in R ~ by A1, A3, A4, A5; hence [y,x] in R by RELAT_1:def_7; ::_thesis: verum end; assume that A6: x in field R and A7: for y being set st y in field R & y <> x holds [y,x] in R ; :: according to ORDERS_1:def_13 ::_thesis: x is_inferior_of R ~ thus x in field (R ~) by A6, RELAT_1:21; :: according to ORDERS_1:def_14 ::_thesis: for y being set st y in field (R ~) & y <> x holds [x,y] in R ~ let y be set ; ::_thesis: ( y in field (R ~) & y <> x implies [x,y] in R ~ ) assume that A8: y in field (R ~) and A9: y <> x ; ::_thesis: [x,y] in R ~ [y,x] in R by A1, A7, A8, A9; hence [x,y] in R ~ by RELAT_1:def_7; ::_thesis: verum end; Lm17: for R being Relation for X, Y being set st R well_orders X & Y c= X holds R well_orders Y proof let R be Relation; ::_thesis: for X, Y being set st R well_orders X & Y c= X holds R well_orders Y let X, Y be set ; ::_thesis: ( R well_orders X & Y c= X implies R well_orders Y ) assume that A1: R well_orders X and A2: Y c= X ; ::_thesis: R well_orders Y A3: R is_transitive_in X by A1, WELLORD1:def_5; A4: R is_connected_in X by A1, WELLORD1:def_5; A5: R is_antisymmetric_in X by A1, WELLORD1:def_5; A6: R is_well_founded_in X by A1, WELLORD1:def_5; R is_reflexive_in X by A1, WELLORD1:def_5; hence ( R is_reflexive_in Y & R is_transitive_in Y & R is_antisymmetric_in Y & R is_connected_in Y ) by A2, A3, A5, A4, Lm10, Th8, Th9, Th10; :: according to WELLORD1:def_5 ::_thesis: R is_well_founded_in Y let Z be set ; :: according to WELLORD1:def_3 ::_thesis: ( not Z c= Y or Z = {} or ex b1 being set st ( b1 in Z & R -Seg b1 misses Z ) ) assume that A7: Z c= Y and A8: Z <> {} ; ::_thesis: ex b1 being set st ( b1 in Z & R -Seg b1 misses Z ) Z c= X by A2, A7, XBOOLE_1:1; hence ex b1 being set st ( b1 in Z & R -Seg b1 misses Z ) by A8, A6, WELLORD1:def_3; ::_thesis: verum end; theorem Th63: :: ORDERS_1:63 for R being Relation 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 proof 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_7 ::_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[ set , set ] means ( ( \$1 <> {} & \$2 = the Choice_Function of M . \$1 ) or ( \$1 = {} & \$2 = D ) ); A8: for x being set st x in bool D holds ex y being set st S1[x,y] proof let x be set ; ::_thesis: ( x in bool D implies ex y being set st S1[x,y] ) assume x in bool D ; ::_thesis: ex y being set st S1[x,y] ( x = {} implies ex y being set st S1[x,y] ) ; hence ex y being set st S1[x,y] ; ::_thesis: verum end; A9: for x, y, z being set 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 set st x in bool D holds S1[x,g . x] ) ) from FUNCT_1:sch_2(A9, A8); defpred S2[ Ordinal, set ] means ex L being T-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 T-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 T-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 T-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, RELAT_1:68; given L2 being T-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 T-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_set_st_x_in_A1_holds_ (L1_|_A1)_._x_=_(L2_|_A1)_._x let x be set ; ::_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, RELAT_1:68; 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, Def1; ::_thesis: verum end; defpred S3[ Ordinal] means S2[\$1,D]; {} c= D by XBOOLE_1:2; then A32: g . {} = D by A10; A33: now__::_thesis:_for_A,_B_being_Ordinal for_L1,_L2_being_T-Sequence_st_dom_L1_=_A_&_(_for_C_being_Ordinal for_L_being_T-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_T-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 T-Sequence st dom L1 = A & ( for C being Ordinal for L being T-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 T-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 T-Sequence; ::_thesis: ( dom L1 = A & ( for C being Ordinal for L being T-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 T-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 T-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 T-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_set_st_x_in_A1_holds_ (L1_|_A1)_._x_=_(L2_|_A1)_._x let x be set ; ::_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 T-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 T-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 T-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 T-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 set ; :: 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, RELAT_1:68 ; 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, Def1; 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 set ; :: 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, RELAT_1:68 ; 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, Def1; 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 A being Ordinal st S3[A] proof defpred S4[ set , set ] 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 A being Ordinal holds not S2[A,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[ set , set ] 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 set st x in A holds ex y being set st S6[x,y] proof let x be set ; ::_thesis: ( x in A implies ex y being set st S6[x,y] ) assume A75: x in A ; ::_thesis: ex y being set 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 set 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 set st x in A holds S6[x,h . x] ) ) from FUNCT_1:sch_2(A77, A74); reconsider h = h as T-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 set ; :: 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 T-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 T-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 T-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 T-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 T-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 T-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 set st x in B holds L1 . x = (h | B) . x proof let x be set ; ::_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 T-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 T-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 T-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 T-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 T-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 T-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 d = 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 d ; ::_thesis: S2[A,d] thus S2[A,d] by A80; ::_thesis: verum end; A92: for A being Ordinal holds S5[A] from ORDINAL1:sch_2(A72); A93: for x, y, z being set st S4[x,y] & S4[x,z] holds y = z proof let x, y, z be set ; ::_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 set holds ( x in X iff ex y being set 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 T-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 T-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 set ; :: 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 T-Sequence such that A103: ( dom L = {} & ( for B being Ordinal for L1 being T-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 T-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 set ; :: 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 T-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 T-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 T-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[ set ] means ex B being Ordinal st ( B in A & S2[B,\$1] ); consider X being set such that A106: for x being set 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, XBOOLE_0:def_8; then {} in A by ORDINAL1:11; then reconsider X = X as non empty set by A106, A102; consider L being T-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 T-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, RELAT_2:def_16; then A109: R |_2 X is transitive by WELLORD1:17; A110: rng L c= X proof let z be set ; :: 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 set 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 T-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 T-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 T-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 T-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 T-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 T-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 be set ; :: according to RELAT_2:def_6,RELAT_2:def_14 ::_thesis: for b1 being set holds ( not x in field (R |_2 X) or not b1 in field (R |_2 X) or x = b1 or [x,b1] in R |_2 X or [b1,x] in R |_2 X ) let y be set ; ::_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 T-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 T-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 T-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 T-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, RELAT_1:68 ; 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, RELAT_1:68 ; 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, RELAT_2:def_12; 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 proof let x be set ; :: according to TARSKI:def_3 ::_thesis: ( not x in X or x in D ) thus ( not x in X or x in D ) by A106; ::_thesis: verum end; R is reflexive by A1, A4, RELAT_2:def_9; then R |_2 X is reflexive by WELLORD1:15; then R |_2 X is being_linear-order by A109, A142, A119, Def5; 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, Def9; take x ; ::_thesis: x is_maximal_in R thus x in field R by A4, A6, A144; :: according to ORDERS_1:def_11 ::_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, RELAT_2:def_4; ::_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, RELAT_2:def_8; ::_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 end; theorem Th64: :: ORDERS_1:64 for R being Relation for X being set st R partially_orders X & field R = X & X has_lower_Zorn_property_wrt R holds ex x being set st x is_minimal_in R proof let R be Relation; ::_thesis: for X being set st R partially_orders X & field R = X & X has_lower_Zorn_property_wrt R holds ex x being set st x is_minimal_in R let X be set ; ::_thesis: ( R partially_orders X & field R = X & X has_lower_Zorn_property_wrt R implies ex x being set st x is_minimal_in R ) assume that A1: R partially_orders X and A2: field R = X and A3: X has_lower_Zorn_property_wrt R ; ::_thesis: ex x being set st x is_minimal_in R R = (R ~) ~ ; then A4: X has_upper_Zorn_property_wrt R ~ by A3, Th51; field (R ~) = X by A2, RELAT_1:21; then consider x being set such that A5: x is_maximal_in R ~ by A1, A4, Th41, Th63; take x ; ::_thesis: x is_minimal_in R thus x is_minimal_in R by A5, Th59; ::_thesis: verum end; theorem Th65: :: ORDERS_1:65 for X being set st X <> {} & ( for Z being set st Z c= X & Z is c=-linear holds ex Y being set st ( Y in X & ( for X1 being set st X1 in Z holds X1 c= Y ) ) ) holds ex Y being set st ( Y in X & ( for Z being set st Z in X & Z <> Y holds not Y c= Z ) ) proof let X be set ; ::_thesis: ( X <> {} & ( for Z being set st Z c= X & Z is c=-linear holds ex Y being set st ( Y in X & ( for X1 being set st X1 in Z holds X1 c= Y ) ) ) implies ex Y being set st ( Y in X & ( for Z being set st Z in X & Z <> Y holds not Y c= Z ) ) ) assume that A1: X <> {} and A2: for Z being set st Z c= X & Z is c=-linear holds ex Y being set st ( Y in X & ( for X1 being set st X1 in Z holds X1 c= Y ) ) ; ::_thesis: ex Y being set st ( Y in X & ( for Z being set st Z in X & Z <> Y holds not Y c= Z ) ) reconsider D = X as non empty set by A1; set R = RelIncl D; A3: D has_upper_Zorn_property_wrt RelIncl D proof let Z be set ; :: according to ORDERS_1:def_9 ::_thesis: ( Z c= D & (RelIncl D) |_2 Z is being_linear-order implies ex x being set st ( x in D & ( for y being set st y in Z holds [y,x] in RelIncl D ) ) ) assume that A4: Z c= D and A5: (RelIncl D) |_2 Z is being_linear-order ; ::_thesis: ex x being set st ( x in D & ( for y being set st y in Z holds [y,x] in RelIncl D ) ) set Q = (RelIncl D) |_2 Z; A6: Z c= field ((RelIncl D) |_2 Z) proof let x be set ; :: according to TARSKI:def_3 ::_thesis: ( not x in Z or x in field ((RelIncl D) |_2 Z) ) assume A7: x in Z ; ::_thesis: x in field ((RelIncl D) |_2 Z) then A8: [x,x] in [:Z,Z:] by ZFMISC_1:87; [x,x] in RelIncl D by A4, A7, WELLORD2:def_1; then [x,x] in (RelIncl D) |_2 Z by A8, XBOOLE_0:def_4; hence x in field ((RelIncl D) |_2 Z) by RELAT_1:15; ::_thesis: verum end; (RelIncl D) |_2 Z is connected by A5, Def5; then A9: (RelIncl D) |_2 Z is_connected_in field ((RelIncl D) |_2 Z) by RELAT_2:def_14; Z is c=-linear proof let X1 be set ; :: according to ORDINAL1:def_8 ::_thesis: for b1 being set holds ( not X1 in Z or not b1 in Z or X1,b1 are_c=-comparable ) let X2 be set ; ::_thesis: ( not X1 in Z or not X2 in Z or X1,X2 are_c=-comparable ) assume that A10: X1 in Z and A11: X2 in Z ; ::_thesis: X1,X2 are_c=-comparable ( not X1 <> X2 or [X1,X2] in (RelIncl D) |_2 Z or [X2,X1] in (RelIncl D) |_2 Z ) by A9, A6, A10, A11, RELAT_2:def_6; then ( not X1 <> X2 or [X1,X2] in RelIncl D or [X2,X1] in RelIncl D ) by XBOOLE_0:def_4; hence ( X1 c= X2 or X2 c= X1 ) by A4, A10, A11, WELLORD2:def_1; :: according to XBOOLE_0:def_9 ::_thesis: verum end; then consider Y being set such that A12: Y in X and A13: for X1 being set st X1 in Z holds X1 c= Y by A2, A4; take x = Y; ::_thesis: ( x in D & ( for y being set st y in Z holds [y,x] in RelIncl D ) ) thus x in D by A12; ::_thesis: for y being set st y in Z holds [y,x] in RelIncl D let y be set ; ::_thesis: ( y in Z implies [y,x] in RelIncl D ) assume A14: y in Z ; ::_thesis: [y,x] in RelIncl D then y c= Y by A13; hence [y,x] in RelIncl D by A4, A12, A14, WELLORD2:def_1; ::_thesis: verum end; A15: field (RelIncl D) = D by WELLORD2:def_1; A16: RelIncl D is_antisymmetric_in D by A15, RELAT_2:def_12; A17: RelIncl D is_transitive_in D by A15, RELAT_2:def_16; RelIncl D is_reflexive_in D by A15, RELAT_2:def_9; then RelIncl D partially_orders D by A17, A16, Def7; then consider x being set such that A18: x is_maximal_in RelIncl D by A15, A3, Th63; take Y = x; ::_thesis: ( Y in X & ( for Z being set st Z in X & Z <> Y holds not Y c= Z ) ) A19: Y in field (RelIncl D) by A18, Def11; thus Y in X by A15, A18, Def11; ::_thesis: for Z being set st Z in X & Z <> Y holds not Y c= Z let Z be set ; ::_thesis: ( Z in X & Z <> Y implies not Y c= Z ) assume that A20: Z in X and A21: Z <> Y ; ::_thesis: not Y c= Z not [Y,Z] in RelIncl D by A15, A18, A20, A21, Def11; hence not Y c= Z by A15, A19, A20, WELLORD2:def_1; ::_thesis: verum end; theorem Th66: :: ORDERS_1:66 for X being set st X <> {} & ( for Z being set st Z c= X & Z is c=-linear holds ex Y being set st ( Y in X & ( for X1 being set st X1 in Z holds Y c= X1 ) ) ) holds ex Y being set st ( Y in X & ( for Z being set st Z in X & Z <> Y holds not Z c= Y ) ) proof let X be set ; ::_thesis: ( X <> {} & ( for Z being set st Z c= X & Z is c=-linear holds ex Y being set st ( Y in X & ( for X1 being set st X1 in Z holds Y c= X1 ) ) ) implies ex Y being set st ( Y in X & ( for Z being set st Z in X & Z <> Y holds not Z c= Y ) ) ) assume that A1: X <> {} and A2: for Z being set st Z c= X & Z is c=-linear holds ex Y being set st ( Y in X & ( for X1 being set st X1 in Z holds Y c= X1 ) ) ; ::_thesis: ex Y being set st ( Y in X & ( for Z being set st Z in X & Z <> Y holds not Z c= Y ) ) reconsider D = X as non empty set by A1; set R = (RelIncl D) ~ ; A3: for x being set st x in D holds [x,x] in (RelIncl D) ~ proof let x be set ; ::_thesis: ( x in D implies [x,x] in (RelIncl D) ~ ) ( x in D implies [x,x] in RelIncl D ) by WELLORD2:def_1; hence ( x in D implies [x,x] in (RelIncl D) ~ ) by RELAT_1:def_7; ::_thesis: verum end; A4: D has_upper_Zorn_property_wrt (RelIncl D) ~ proof let Z be set ; :: according to ORDERS_1:def_9 ::_thesis: ( Z c= D & ((RelIncl D) ~) |_2 Z is being_linear-order implies ex x being set st ( x in D & ( for y being set st y in Z holds [y,x] in (RelIncl D) ~ ) ) ) assume that A5: Z c= D and A6: ((RelIncl D) ~) |_2 Z is being_linear-order ; ::_thesis: ex x being set st ( x in D & ( for y being set st y in Z holds [y,x] in (RelIncl D) ~ ) ) set Q = ((RelIncl D) ~) |_2 Z; A7: Z c= field (((RelIncl D) ~) |_2 Z) proof let x be set ; :: according to TARSKI:def_3 ::_thesis: ( not x in Z or x in field (((RelIncl D) ~) |_2 Z) ) assume A8: x in Z ; ::_thesis: x in field (((RelIncl D) ~) |_2 Z) then A9: [x,x] in [:Z,Z:] by ZFMISC_1:87; [x,x] in (RelIncl D) ~ by A3, A5, A8; then [x,x] in ((RelIncl D) ~) |_2 Z by A9, XBOOLE_0:def_4; hence x in field (((RelIncl D) ~) |_2 Z) by RELAT_1:15; ::_thesis: verum end; ((RelIncl D) ~) |_2 Z is connected by A6, Def5; then A10: ((RelIncl D) ~) |_2 Z is_connected_in field (((RelIncl D) ~) |_2 Z) by RELAT_2:def_14; Z is c=-linear proof let X1 be set ; :: according to ORDINAL1:def_8 ::_thesis: for b1 being set holds ( not X1 in Z or not b1 in Z or X1,b1 are_c=-comparable ) let X2 be set ; ::_thesis: ( not X1 in Z or not X2 in Z or X1,X2 are_c=-comparable ) assume that A11: X1 in Z and A12: X2 in Z ; ::_thesis: X1,X2 are_c=-comparable ( not X1 <> X2 or [X1,X2] in ((RelIncl D) ~) |_2 Z or [X2,X1] in ((RelIncl D) ~) |_2 Z ) by A10, A7, A11, A12, RELAT_2:def_6; then ( not X1 <> X2 or [X1,X2] in (RelIncl D) ~ or [X2,X1] in (RelIncl D) ~ ) by XBOOLE_0:def_4; then ( not X1 <> X2 or [X1,X2] in RelIncl D or [X2,X1] in RelIncl D ) by RELAT_1:def_7; hence ( X1 c= X2 or X2 c= X1 ) by A5, A11, A12, WELLORD2:def_1; :: according to XBOOLE_0:def_9 ::_thesis: verum end; then consider Y being set such that A13: Y in X and A14: for X1 being set st X1 in Z holds Y c= X1 by A2, A5; take x = Y; ::_thesis: ( x in D & ( for y being set st y in Z holds [y,x] in (RelIncl D) ~ ) ) thus x in D by A13; ::_thesis: for y being set st y in Z holds [y,x] in (RelIncl D) ~ let y be set ; ::_thesis: ( y in Z implies [y,x] in (RelIncl D) ~ ) assume A15: y in Z ; ::_thesis: [y,x] in (RelIncl D) ~ then Y c= y by A14; then [Y,y] in RelIncl D by A5, A13, A15, WELLORD2:def_1; hence [y,x] in (RelIncl D) ~ by RELAT_1:def_7; ::_thesis: verum end; A16: field ((RelIncl D) ~) = field (RelIncl D) by RELAT_1:21 .= D by WELLORD2:def_1 ; A17: field (RelIncl D) = D by WELLORD2:def_1; RelIncl D is_antisymmetric_in D by A17, RELAT_2:def_12; then A18: (RelIncl D) ~ is_antisymmetric_in D by Lm13; RelIncl D is_transitive_in D by A17, RELAT_2:def_16; then A19: (RelIncl D) ~ is_transitive_in D by Lm12; RelIncl D is_reflexive_in D by A17, RELAT_2:def_9; then (RelIncl D) ~ is_reflexive_in D by Lm11; then (RelIncl D) ~ partially_orders D by A19, A18, Def7; then consider x being set such that A20: x is_maximal_in (RelIncl D) ~ by A16, A4, Th63; take Y = x; ::_thesis: ( Y in X & ( for Z being set st Z in X & Z <> Y holds not Z c= Y ) ) A21: Y in field ((RelIncl D) ~) by A20, Def11; thus Y in X by A16, A20, Def11; ::_thesis: for Z being set st Z in X & Z <> Y holds not Z c= Y let Z be set ; ::_thesis: ( Z in X & Z <> Y implies not Z c= Y ) assume that A22: Z in X and A23: Z <> Y ; ::_thesis: not Z c= Y not [Y,Z] in (RelIncl D) ~ by A16, A20, A22, A23, Def11; then not [Z,Y] in RelIncl D by RELAT_1:def_7; hence not Z c= Y by A16, A21, A22, WELLORD2:def_1; ::_thesis: verum end; theorem Th67: :: ORDERS_1:67 for X being set st X <> {} & ( for Z being set st Z <> {} & Z c= X & Z is c=-linear holds union Z in X ) holds ex Y being set st ( Y in X & ( for Z being set st Z in X & Z <> Y holds not Y c= Z ) ) proof let X be set ; ::_thesis: ( X <> {} & ( for Z being set st Z <> {} & Z c= X & Z is c=-linear holds union Z in X ) implies ex Y being set st ( Y in X & ( for Z being set st Z in X & Z <> Y holds not Y c= Z ) ) ) assume that A1: X <> {} and A2: for Z being set st Z <> {} & Z c= X & Z is c=-linear holds union Z in X ; ::_thesis: ex Y being set st ( Y in X & ( for Z being set st Z in X & Z <> Y holds not Y c= Z ) ) for Z being set st Z c= X & Z is c=-linear holds ex Y being set st ( Y in X & ( for X1 being set st X1 in Z holds X1 c= Y ) ) proof set x = the Element of X; let Z be set ; ::_thesis: ( Z c= X & Z is c=-linear implies ex Y being set st ( Y in X & ( for X1 being set st X1 in Z holds X1 c= Y ) ) ) assume that A3: Z c= X and A4: Z is c=-linear ; ::_thesis: ex Y being set st ( Y in X & ( for X1 being set st X1 in Z holds X1 c= Y ) ) ( Z <> {} or Z = {} ) ; then consider Y being set such that A5: ( ( Y = union Z & Z <> {} ) or ( Y = the Element of X & Z = {} ) ) ; take Y ; ::_thesis: ( Y in X & ( for X1 being set st X1 in Z holds X1 c= Y ) ) thus ( Y in X & ( for X1 being set st X1 in Z holds X1 c= Y ) ) by A1, A2, A3, A4, A5, ZFMISC_1:74; ::_thesis: verum end; hence ex Y being set st ( Y in X & ( for Z being set st Z in X & Z <> Y holds not Y c= Z ) ) by A1, Th65; ::_thesis: verum end; theorem :: ORDERS_1:68 for X being set st X <> {} & ( for Z being set st Z <> {} & Z c= X & Z is c=-linear holds meet Z in X ) holds ex Y being set st ( Y in X & ( for Z being set st Z in X & Z <> Y holds not Z c= Y ) ) proof let X be set ; ::_thesis: ( X <> {} & ( for Z being set st Z <> {} & Z c= X & Z is c=-linear holds meet Z in X ) implies ex Y being set st ( Y in X & ( for Z being set st Z in X & Z <> Y holds not Z c= Y ) ) ) assume that A1: X <> {} and A2: for Z being set st Z <> {} & Z c= X & Z is c=-linear holds meet Z in X ; ::_thesis: ex Y being set st ( Y in X & ( for Z being set st Z in X & Z <> Y holds not Z c= Y ) ) for Z being set st Z c= X & Z is c=-linear holds ex Y being set st ( Y in X & ( for X1 being set st X1 in Z holds Y c= X1 ) ) proof set x = the Element of X; let Z be set ; ::_thesis: ( Z c= X & Z is c=-linear implies ex Y being set st ( Y in X & ( for X1 being set st X1 in Z holds Y c= X1 ) ) ) assume that A3: Z c= X and A4: Z is c=-linear ; ::_thesis: ex Y being set st ( Y in X & ( for X1 being set st X1 in Z holds Y c= X1 ) ) ( Z <> {} or Z = {} ) ; then consider Y being set such that A5: ( ( Y = meet Z & Z <> {} ) or ( Y = the Element of X & Z = {} ) ) ; take Y ; ::_thesis: ( Y in X & ( for X1 being set st X1 in Z holds Y c= X1 ) ) thus ( Y in X & ( for X1 being set st X1 in Z holds Y c= X1 ) ) by A1, A2, A3, A4, A5, SETFAM_1:3; ::_thesis: verum end; hence ex Y being set st ( Y in X & ( for Z being set st Z in X & Z <> Y holds not Z c= Y ) ) by A1, Th66; ::_thesis: verum end; scheme :: ORDERS_1:sch 1 ZornMax{ F1() -> non empty set , P1[ set , set ] } : ex x being Element of F1() st for y being Element of F1() st x <> y holds not P1[x,y] provided A1: for x being Element of F1() holds P1[x,x] and A2: for x, y being Element of F1() st P1[x,y] & P1[y,x] holds x = y and A3: for x, y, z being Element of F1() st P1[x,y] & P1[y,z] holds P1[x,z] and A4: for X being set st X c= F1() & ( for x, y being Element of F1() st x in X & y in X & P1[x,y] holds P1[y,x] ) holds ex y being Element of F1() st for x being Element of F1() st x in X holds P1[x,y] proof consider R being Relation of F1() such that A5: for x, y being Element of F1() holds ( [x,y] in R iff P1[x,y] ) from RELSET_1:sch_2(); A6: R is_transitive_in F1() proof let x be set ; :: according to RELAT_2:def_8 ::_thesis: for b1, b2 being set holds ( not x in F1() or not b1 in F1() or not b2 in F1() or not [x,b1] in R or not [b1,b2] in R or [x,b2] in R ) let y, z be set ; ::_thesis: ( not x in F1() or not y in F1() or not z in F1() or not [x,y] in R or not [y,z] in R or [x,z] in R ) assume that A7: x in F1() and A8: y in F1() and A9: z in F1() ; ::_thesis: ( not [x,y] in R or not [y,z] in R or [x,z] in R ) reconsider x9 = x, y9 = y, z9 = z as Element of F1() by A7, A8, A9; assume that A10: [x,y] in R and A11: [y,z] in R ; ::_thesis: [x,z] in R A12: P1[y9,z9] by A5, A11; P1[x9,y9] by A5, A10; then P1[x9,z9] by A3, A12; hence [x,z] in R by A5; ::_thesis: verum end; F1() c= dom R proof let x be set ; :: according to TARSKI:def_3 ::_thesis: ( not x in F1() or x in dom R ) assume x in F1() ; ::_thesis: x in dom R then reconsider x9 = x as Element of F1() ; P1[x9,x9] by A1; then [x,x] in R by A5; hence x in dom R by XTUPLE_0:def_12; ::_thesis: verum end; then dom R = F1() by XBOOLE_0:def_10; then A13: F1() c= field R by XBOOLE_1:7; field R = (dom R) \/ (rng R) ; then A14: field R = F1() by A13, XBOOLE_0:def_10; A15: R is_reflexive_in F1() proof let x be set ; :: according to RELAT_2:def_1 ::_thesis: ( not x in F1() or [x,x] in R ) assume x in F1() ; ::_thesis: [x,x] in R then reconsider x9 = x as Element of F1() ; P1[x9,x9] by A1; hence [x,x] in R by A5; ::_thesis: verum end; A16: F1() has_upper_Zorn_property_wrt R proof let Y be set ; :: according to ORDERS_1:def_9 ::_thesis: ( Y c= F1() & R |_2 Y is being_linear-order implies ex x being set st ( x in F1() & ( for y being set st y in Y holds [y,x] in R ) ) ) assume that A17: Y c= F1() and A18: R |_2 Y is being_linear-order ; ::_thesis: ex x being set st ( x in F1() & ( for y being set st y in Y holds [y,x] in R ) ) for x, y being Element of F1() st x in Y & y in Y & P1[x,y] holds P1[y,x] proof let x, y be Element of F1(); ::_thesis: ( x in Y & y in Y & P1[x,y] implies P1[y,x] ) assume that A19: x in Y and A20: y in Y ; ::_thesis: ( P1[x,y] or P1[y,x] ) A21: ( R |_2 Y is reflexive & R |_2 Y is connected ) by A18, Def5; Y c= field (R |_2 Y) proof let x be set ; :: according to TARSKI:def_3 ::_thesis: ( not x in Y or x in field (R |_2 Y) ) assume A22: x in Y ; ::_thesis: x in field (R |_2 Y) then A23: [x,x] in [:Y,Y:] by ZFMISC_1:87; [x,x] in R by A15, A17, A22, RELAT_2:def_1; then [x,x] in R |_2 Y by A23, XBOOLE_0:def_4; hence x in field (R |_2 Y) by RELAT_1:15; ::_thesis: verum end; then A24: Y = field ((R |_2 Y) |_2 Y) by A21, Lm5 .= field (R |_2 Y) by WELLORD1:21 ; then A25: R |_2 Y is_connected_in Y by A21, RELAT_2:def_14; A26: R |_2 Y is_reflexive_in Y by A21, A24, RELAT_2:def_9; ( x = y or x <> y ) ; then ( [x,y] in R |_2 Y or [y,x] in R |_2 Y ) by A19, A20, A25, A26, RELAT_2:def_1, RELAT_2:def_6; then ( [x,y] in R or [y,x] in R ) by XBOOLE_0:def_4; hence ( P1[x,y] or P1[y,x] ) by A5; ::_thesis: verum end; then consider y being Element of F1() such that A27: for x being Element of F1() st x in Y holds P1[x,y] by A4, A17; take y ; ::_thesis: ( y in F1() & ( for y being set st y in Y holds [y,y] in R ) ) thus y in F1() ; ::_thesis: for y being set st y in Y holds [y,y] in R let x be set ; ::_thesis: ( x in Y implies [x,y] in R ) assume A28: x in Y ; ::_thesis: [x,y] in R then P1[x,y] by A17, A27; hence [x,y] in R by A5, A17, A28; ::_thesis: verum end; R is_antisymmetric_in F1() proof let x be set ; :: according to RELAT_2:def_4 ::_thesis: for b1 being set holds ( not x in F1() or not b1 in F1() or not [x,b1] in R or not [b1,x] in R or x = b1 ) let y be set ; ::_thesis: ( not x in F1() or not y in F1() or not [x,y] in R or not [y,x] in R or x = y ) assume that A29: x in F1() and A30: y in F1() ; ::_thesis: ( not [x,y] in R or not [y,x] in R or x = y ) reconsider x9 = x, y9 = y as Element of F1() by A29, A30; assume that A31: [x,y] in R and A32: [y,x] in R ; ::_thesis: x = y A33: P1[y9,x9] by A5, A32; P1[x9,y9] by A5, A31; hence x = y by A2, A33; ::_thesis: verum end; then R partially_orders F1() by A15, A6, Def7; then consider x being set such that A34: x is_maximal_in R by A14, A16, Th63; take x ; ::_thesis: ( x is Element of F1() & ( for y being Element of F1() st x <> y holds not P1[x,y] ) ) thus x is Element of F1() by A14, A34, Def11; ::_thesis: for y being Element of F1() st x <> y holds not P1[x,y] let y be Element of F1(); ::_thesis: ( x <> y implies not P1[x,y] ) assume x <> y ; ::_thesis: P1[x,y] then A35: not [x,y] in R by A14, A34, Def11; x in F1() by A14, A34, Def11; hence P1[x,y] by A5, A35; ::_thesis: verum end; scheme :: ORDERS_1:sch 2 ZornMin{ F1() -> non empty set , P1[ set , set ] } : ex x being Element of F1() st for y being Element of F1() st x <> y holds not P1[y,x] provided A1: for x being Element of F1() holds P1[x,x] and A2: for x, y being Element of F1() st P1[x,y] & P1[y,x] holds x = y and A3: for x, y, z being Element of F1() st P1[x,y] & P1[y,z] holds P1[x,z] and A4: for X being set st X c= F1() & ( for x, y being Element of F1() st x in X & y in X & P1[x,y] holds P1[y,x] ) holds ex y being Element of F1() st for x being Element of F1() st x in X holds P1[y,x] proof consider R being Relation of F1() such that A5: for x, y being Element of F1() holds ( [x,y] in R iff P1[x,y] ) from RELSET_1:sch_2(); A6: R is_transitive_in F1() proof let x be set ; :: according to RELAT_2:def_8 ::_thesis: for b1, b2 being set holds ( not x in F1() or not b1 in F1() or not b2 in F1() or not [x,b1] in R or not [b1,b2] in R or [x,b2] in R ) let y, z be set ; ::_thesis: ( not x in F1() or not y in F1() or not z in F1() or not [x,y] in R or not [y,z] in R or [x,z] in R ) assume that A7: x in F1() and A8: y in F1() and A9: z in F1() ; ::_thesis: ( not [x,y] in R or not [y,z] in R or [x,z] in R ) reconsider x9 = x, y9 = y, z9 = z as Element of F1() by A7, A8, A9; assume that A10: [x,y] in R and A11: [y,z] in R ; ::_thesis: [x,z] in R A12: P1[y9,z9] by A5, A11; P1[x9,y9] by A5, A10; then P1[x9,z9] by A3, A12; hence [x,z] in R by A5; ::_thesis: verum end; F1() c= dom R proof let x be set ; :: according to TARSKI:def_3 ::_thesis: ( not x in F1() or x in dom R ) assume x in F1() ; ::_thesis: x in dom R then reconsider x9 = x as Element of F1() ; P1[x9,x9] by A1; then [x,x] in R by A5; hence x in dom R by XTUPLE_0:def_12; ::_thesis: verum end; then dom R = F1() by XBOOLE_0:def_10; then A13: F1() c= field R by XBOOLE_1:7; field R = (dom R) \/ (rng R) ; then A14: field R = F1() by A13, XBOOLE_0:def_10; A15: R is_reflexive_in F1() proof let x be set ; :: according to RELAT_2:def_1 ::_thesis: ( not x in F1() or [x,x] in R ) assume x in F1() ; ::_thesis: [x,x] in R then reconsider x9 = x as Element of F1() ; P1[x9,x9] by A1; hence [x,x] in R by A5; ::_thesis: verum end; A16: F1() has_lower_Zorn_property_wrt R proof let Y be set ; :: according to ORDERS_1:def_10 ::_thesis: ( Y c= F1() & R |_2 Y is being_linear-order implies ex x being set st ( x in F1() & ( for y being set st y in Y holds [x,y] in R ) ) ) assume that A17: Y c= F1() and A18: R |_2 Y is being_linear-order ; ::_thesis: ex x being set st ( x in F1() & ( for y being set st y in Y holds [x,y] in R ) ) for x, y being Element of F1() st x in Y & y in Y & P1[x,y] holds P1[y,x] proof let x, y be Element of F1(); ::_thesis: ( x in Y & y in Y & P1[x,y] implies P1[y,x] ) assume that A19: x in Y and A20: y in Y ; ::_thesis: ( P1[x,y] or P1[y,x] ) A21: ( R |_2 Y is reflexive & R |_2 Y is connected ) by A18, Def5; Y c= field (R |_2 Y) proof let x be set ; :: according to TARSKI:def_3 ::_thesis: ( not x in Y or x in field (R |_2 Y) ) assume A22: x in Y ; ::_thesis: x in field (R |_2 Y) then A23: [x,x] in [:Y,Y:] by ZFMISC_1:87; [x,x] in R by A15, A17, A22, RELAT_2:def_1; then [x,x] in R |_2 Y by A23, XBOOLE_0:def_4; hence x in field (R |_2 Y) by RELAT_1:15; ::_thesis: verum end; then A24: Y = field ((R |_2 Y) |_2 Y) by A21, Lm5 .= field (R |_2 Y) by WELLORD1:21 ; then A25: R |_2 Y is_connected_in Y by A21, RELAT_2:def_14; A26: R |_2 Y is_reflexive_in Y by A21, A24, RELAT_2:def_9; ( x = y or x <> y ) ; then ( [x,y] in R |_2 Y or [y,x] in R |_2 Y ) by A19, A20, A25, A26, RELAT_2:def_1, RELAT_2:def_6; then ( [x,y] in R or [y,x] in R ) by XBOOLE_0:def_4; hence ( P1[x,y] or P1[y,x] ) by A5; ::_thesis: verum end; then consider y being Element of F1() such that A27: for x being Element of F1() st x in Y holds P1[y,x] by A4, A17; take y ; ::_thesis: ( y in F1() & ( for y being set st y in Y holds [y,y] in R ) ) thus y in F1() ; ::_thesis: for y being set st y in Y holds [y,y] in R let x be set ; ::_thesis: ( x in Y implies [y,x] in R ) assume A28: x in Y ; ::_thesis: [y,x] in R then P1[y,x] by A17, A27; hence [y,x] in R by A5, A17, A28; ::_thesis: verum end; R is_antisymmetric_in F1() proof let x be set ; :: according to RELAT_2:def_4 ::_thesis: for b1 being set holds ( not x in F1() or not b1 in F1() or not [x,b1] in R or not [b1,x] in R or x = b1 ) let y be set ; ::_thesis: ( not x in F1() or not y in F1() or not [x,y] in R or not [y,x] in R or x = y ) assume that A29: x in F1() and A30: y in F1() ; ::_thesis: ( not [x,y] in R or not [y,x] in R or x = y ) reconsider x9 = x, y9 = y as Element of F1() by A29, A30; assume that A31: [x,y] in R and A32: [y,x] in R ; ::_thesis: x = y A33: P1[y9,x9] by A5, A32; P1[x9,y9] by A5, A31; hence x = y by A2, A33; ::_thesis: verum end; then R partially_orders F1() by A15, A6, Def7; then consider x being set such that A34: x is_minimal_in R by A14, A16, Th64; take x ; ::_thesis: ( x is Element of F1() & ( for y being Element of F1() st x <> y holds not P1[y,x] ) ) thus x is Element of F1() by A14, A34, Def12; ::_thesis: for y being Element of F1() st x <> y holds not P1[y,x] let y be Element of F1(); ::_thesis: ( x <> y implies not P1[y,x] ) assume x <> y ; ::_thesis: P1[y,x] then A35: not [y,x] in R by A14, A34, Def12; x in F1() by A14, A34, Def12; hence P1[y,x] by A5, A35; ::_thesis: verum end; theorem :: ORDERS_1:69 for R being Relation for X being set st R partially_orders X & field R = X holds ex P being Relation st ( R c= P & P linearly_orders X & field P = X ) proof let R be Relation; ::_thesis: for X being set st R partially_orders X & field R = X holds ex P being Relation st ( R c= P & P linearly_orders X & field P = X ) let X be set ; ::_thesis: ( R partially_orders X & field R = X implies ex P being Relation st ( R c= P & P linearly_orders X & field P = X ) ) assume that A1: R partially_orders X and A2: field R = X ; ::_thesis: ex P being Relation st ( R c= P & P linearly_orders X & field P = X ) defpred S1[ set ] means ex P being Relation st ( \$1 = P & R c= P & P partially_orders X & field P = X ); consider Rel being set such that A3: for x being set holds ( x in Rel iff ( x in bool [:X,X:] & S1[x] ) ) from XBOOLE_0:sch_1(); A4: for Z being set st Z <> {} & Z c= Rel & Z is c=-linear holds union Z in Rel proof reconsider T = [:X,X:] as Relation ; let Z be set ; ::_thesis: ( Z <> {} & Z c= Rel & Z is c=-linear implies union Z in Rel ) assume that A5: Z <> {} and A6: Z c= Rel and A7: Z is c=-linear ; ::_thesis: union Z in Rel A8: union (bool [:X,X:]) = T by ZFMISC_1:81; Z c= bool [:X,X:] proof let x be set ; :: according to TARSKI:def_3 ::_thesis: ( not x in Z or x in bool [:X,X:] ) assume x in Z ; ::_thesis: x in bool [:X,X:] hence x in bool [:X,X:] by A3, A6; ::_thesis: verum end; then A9: union Z c= union (bool [:X,X:]) by ZFMISC_1:77; then reconsider S = union Z as Relation ; set y = the Element of Z; the Element of Z in Rel by A5, A6, TARSKI:def_3; then consider P being Relation such that A10: the Element of Z = P and A11: R c= P and A12: P partially_orders X and field P = X by A3; A13: S is_antisymmetric_in X proof let x be set ; :: according to RELAT_2:def_4 ::_thesis: for b1 being set holds ( not x in X or not b1 in X or not [x,b1] in S or not [b1,x] in S or x = b1 ) let y be set ; ::_thesis: ( not x in X or not y in X or not [x,y] in S or not [y,x] in S or x = y ) assume that A14: x in X and A15: y in X and A16: [x,y] in S and A17: [y,x] in S ; ::_thesis: x = y consider X1 being set such that A18: [x,y] in X1 and A19: X1 in Z by A16, TARSKI:def_4; consider P1 being Relation such that A20: X1 = P1 and R c= P1 and A21: P1 partially_orders X and field P1 = X by A3, A6, A19; consider X2 being set such that A22: [y,x] in X2 and A23: X2 in Z by A17, TARSKI:def_4; X1,X2 are_c=-comparable by A7, A19, A23, ORDINAL1:def_8; then A24: ( X1 c= X2 or X2 c= X1 ) by XBOOLE_0:def_9; consider P2 being Relation such that A25: X2 = P2 and R c= P2 and A26: P2 partially_orders X and field P2 = X by A3, A6, A23; A27: P2 is_antisymmetric_in X by A26, Def7; P1 is_antisymmetric_in X by A21, Def7; hence x = y by A14, A15, A18, A22, A24, A20, A25, A27, RELAT_2:def_4; ::_thesis: verum end; A28: S is_transitive_in X proof let x be set ; :: according to RELAT_2:def_8 ::_thesis: for b1, b2 being set holds ( not x in X or not b1 in X or not b2 in X or not [x,b1] in S or not [b1,b2] in S or [x,b2] in S ) let y, z be set ; ::_thesis: ( not x in X or not y in X or not z in X or not [x,y] in S or not [y,z] in S or [x,z] in S ) assume that A29: x in X and A30: y in X and A31: z in X and A32: [x,y] in S and A33: [y,z] in S ; ::_thesis: [x,z] in S consider X1 being set such that A34: [x,y] in X1 and A35: X1 in Z by A32, TARSKI:def_4; consider P1 being Relation such that A36: X1 = P1 and R c= P1 and A37: P1 partially_orders X and field P1 = X by A3, A6, A35; consider X2 being set such that A38: [y,z] in X2 and A39: X2 in Z by A33, TARSKI:def_4; X1,X2 are_c=-comparable by A7, A35, A39, ORDINAL1:def_8; then A40: ( X1 c= X2 or X2 c= X1 ) by XBOOLE_0:def_9; consider P2 being Relation such that A41: X2 = P2 and R c= P2 and A42: P2 partially_orders X and field P2 = X by A3, A6, A39; A43: P2 is_transitive_in X by A42, Def7; P1 is_transitive_in X by A37, Def7; then ( [x,z] in P1 or [x,z] in P2 ) by A29, A30, A31, A34, A38, A40, A36, A41, A43, RELAT_2:def_8; hence [x,z] in S by A35, A39, A36, A41, TARSKI:def_4; ::_thesis: verum end; A44: P is_reflexive_in X by A12, Def7; S is_reflexive_in X proof let x be set ; :: according to RELAT_2:def_1 ::_thesis: ( not x in X or [x,x] in S ) assume x in X ; ::_thesis: [x,x] in S then [x,x] in P by A44, RELAT_2:def_1; hence [x,x] in S by A5, A10, TARSKI:def_4; ::_thesis: verum end; then A45: S partially_orders X by A28, A13, Def7; A46: field S c= X proof let x be set ; :: according to TARSKI:def_3 ::_thesis: ( not x in field S or x in X ) A47: now__::_thesis:_(_x_in_dom_S_&_x_in_field_S_implies_x_in_X_) assume x in dom S ; ::_thesis: ( not x in field S or x in X ) then consider y being set such that A48: [x,y] in S by XTUPLE_0:def_12; consider Y being set such that A49: [x,y] in Y and A50: Y in Z by A48, TARSKI:def_4; ex P being Relation st ( Y = P & R c= P & P partially_orders X & field P = X ) by A3, A6, A50; hence ( not x in field S or x in X ) by A49, RELAT_1:15; ::_thesis: verum end; A51: now__::_thesis:_(_x_in_rng_S_&_x_in_field_S_implies_x_in_X_) assume x in rng S ; ::_thesis: ( not x in field S or x in X ) then consider y being set such that A52: [y,x] in S by XTUPLE_0:def_13; consider Y being set such that A53: [y,x] in Y and A54: Y in Z by A52, TARSKI:def_4; ex P being Relation st ( Y = P & R c= P & P partially_orders X & field P = X ) by A3, A6, A54; hence ( not x in field S or x in X ) by A53, RELAT_1:15; ::_thesis: verum end; assume x in field S ; ::_thesis: x in X hence x in X by A47, A51, XBOOLE_0:def_3; ::_thesis: verum end; A55: R c= S proof let x be set ; :: according to RELAT_1:def_3 ::_thesis: for b1 being set holds ( not [x,b1] in R or [x,b1] in S ) let y be set ; ::_thesis: ( not [x,y] in R or [x,y] in S ) assume [x,y] in R ; ::_thesis: [x,y] in S hence [x,y] in S by A5, A10, A11, TARSKI:def_4; ::_thesis: verum end; then X c= field S by A2, RELAT_1:16; then field S = X by A46, XBOOLE_0:def_10; hence union Z in Rel by A3, A9, A8, A55, A45; ::_thesis: verum end; R c= [:X,X:] by A2, Lm4; then Rel <> {} by A1, A2, A3; then consider Y being set such that A56: Y in Rel and A57: for Z being set st Z in Rel & Z <> Y holds not Y c= Z by A4, Th67; consider P being Relation such that A58: Y = P and A59: R c= P and A60: P partially_orders X and A61: field P = X by A3, A56; take P ; ::_thesis: ( R c= P & P linearly_orders X & field P = X ) thus R c= P by A59; ::_thesis: ( P linearly_orders X & field P = X ) thus A62: ( P is_reflexive_in X & P is_transitive_in X & P is_antisymmetric_in X ) by A60, Def7; :: according to ORDERS_1:def_8 ::_thesis: ( P is_connected_in X & field P = X ) thus P is_connected_in X ::_thesis: field P = X proof let x be set ; :: according to RELAT_2:def_6 ::_thesis: for b1 being set holds ( not x in X or not b1 in X or x = b1 or [x,b1] in P or [b1,x] in P ) let y be set ; ::_thesis: ( not x in X or not y in X or x = y or [x,y] in P or [y,x] in P ) assume that A63: x in X and A64: y in X and x <> y and A65: not [x,y] in P and A66: not [y,x] in P ; ::_thesis: contradiction defpred S2[ set , set ] means ( [\$1,\$2] in P or ( [\$1,x] in P & [y,\$2] in P ) ); consider Q being Relation such that A67: for z, u being set holds ( [z,u] in Q iff ( z in X & u in X & S2[z,u] ) ) from RELAT_1:sch_1(); A68: field Q c= X proof let z be set ; :: according to TARSKI:def_3 ::_thesis: ( not z in field Q or z in X ) A69: now__::_thesis:_(_z_in_dom_Q_&_z_in_field_Q_implies_z_in_X_) assume z in dom Q ; ::_thesis: ( not z in field Q or z in X ) then ex u being set st [z,u] in Q by XTUPLE_0:def_12; hence ( not z in field Q or z in X ) by A67; ::_thesis: verum end; A70: now__::_thesis:_(_z_in_rng_Q_&_z_in_field_Q_implies_z_in_X_) assume z in rng Q ; ::_thesis: ( not z in field Q or z in X ) then ex u being set st [u,z] in Q by XTUPLE_0:def_13; hence ( not z in field Q or z in X ) by A67; ::_thesis: verum end; assume z in field Q ; ::_thesis: z in X hence z in X by A69, A70, XBOOLE_0:def_3; ::_thesis: verum end; A71: P c= Q proof let z be set ; :: according to RELAT_1:def_3 ::_thesis: for b1 being set holds ( not [z,b1] in P or [z,b1] in Q ) let u be set ; ::_thesis: ( not [z,u] in P or [z,u] in Q ) assume A72: [z,u] in P ; ::_thesis: [z,u] in Q then A73: u in field P by RELAT_1:15; z in field P by A72, RELAT_1:15; hence [z,u] in Q by A61, A67, A72, A73; ::_thesis: verum end; then X c= field Q by A61, RELAT_1:16; then A74: field Q = X by A68, XBOOLE_0:def_10; A75: Q is_transitive_in X proof let a, b, c be set ; :: according to RELAT_2:def_8 ::_thesis: ( not a in X or not b in X or not c in X or not [a,b] in Q or not [b,c] in Q or [a,c] in Q ) assume that A76: a in X and A77: b in X and A78: c in X and A79: [a,b] in Q and A80: [b,c] in Q ; ::_thesis: [a,c] in Q A81: ( [b,c] in P or ( [b,x] in P & [y,c] in P ) ) by A67, A80; ( [a,b] in P or ( [a,x] in P & [y,b] in P ) ) by A67, A79; then ( [a,c] in P or ( [a,x] in P & [y,c] in P ) or ( [a,x] in P & [y,c] in P ) or [y,x] in P ) by A62, A63, A64, A76, A77, A78, A81, RELAT_2:def_8; hence [a,c] in Q by A66, A67, A76, A78; ::_thesis: verum end; A82: Q is_antisymmetric_in X proof let a, b be set ; :: according to RELAT_2:def_4 ::_thesis: ( not a in X or not b in X or not [a,b] in Q or not [b,a] in Q or a = b ) assume that A83: a in X and A84: b in X and A85: [a,b] in Q and A86: [b,a] in Q ; ::_thesis: a = b A87: ( [b,a] in P or ( [b,x] in P & [y,a] in P ) ) by A67, A86; ( [a,b] in P or ( [a,x] in P & [y,b] in P ) ) by A67, A85; then ( a = b or ( [a,x] in P & [y,a] in P ) or [y,x] in P ) by A62, A63, A64, A83, A84, A87, RELAT_2:def_4, RELAT_2:def_8; hence a = b by A62, A63, A64, A66, A83, RELAT_2:def_8; ::_thesis: verum end; Q is_reflexive_in X proof let z be set ; :: according to RELAT_2:def_1 ::_thesis: ( not z in X or [z,z] in Q ) assume A88: z in X ; ::_thesis: [z,z] in Q then [z,z] in P by A62, RELAT_2:def_1; hence [z,z] in Q by A67, A88; ::_thesis: verum end; then A89: Q partially_orders X by A75, A82, Def7; A90: Q c= [:X,X:] proof let y be set ; :: according to RELAT_1:def_3 ::_thesis: for b1 being set holds ( not [y,b1] in Q or [y,b1] in [:X,X:] ) let z be set ; ::_thesis: ( not [y,z] in Q or [y,z] in [:X,X:] ) assume A91: [y,z] in Q ; ::_thesis: [y,z] in [:X,X:] then A92: z in X by A67; y in X by A67, A91; hence [y,z] in [:X,X:] by A92, ZFMISC_1:87; ::_thesis: verum end; R c= Q by A59, A71, XBOOLE_1:1; then Q in Rel by A3, A90, A74, A89; then A93: Q = P by A57, A58, A71; A94: [y,y] in P by A62, A64, RELAT_2:def_1; [x,x] in P by A62, A63, RELAT_2:def_1; hence contradiction by A63, A64, A65, A67, A93, A94; ::_thesis: verum end; thus field P = X by A61; ::_thesis: verum end; theorem :: ORDERS_1:70 for R being Relation holds R c= [:(field R),(field R):] by Lm4; theorem :: ORDERS_1:71 for R being Relation for X being set st R is reflexive & X c= field R holds field (R |_2 X) = X by Lm5; theorem :: ORDERS_1:72 for R being Relation for X being set st R is_reflexive_in X holds R |_2 X is reflexive by Lm6; theorem :: ORDERS_1:73 for R being Relation for X being set st R is_transitive_in X holds R |_2 X is transitive by Lm7; theorem :: ORDERS_1:74 for R being Relation for X being set st R is_antisymmetric_in X holds R |_2 X is antisymmetric by Lm8; theorem :: ORDERS_1:75 for R being Relation for X being set st R is_connected_in X holds R |_2 X is connected by Lm9; theorem :: ORDERS_1:76 for R being Relation for X, Y being set st R is_connected_in X & Y c= X holds R is_connected_in Y by Lm10; theorem :: ORDERS_1:77 for R being Relation for X, Y being set st R well_orders X & Y c= X holds R well_orders Y by Lm17; theorem :: ORDERS_1:78 for R being Relation st R is connected holds R ~ is connected by Lm3; theorem :: ORDERS_1:79 for R being Relation for X being set st R is_reflexive_in X holds R ~ is_reflexive_in X by Lm11; theorem :: ORDERS_1:80 for R being Relation for X being set st R is_transitive_in X holds R ~ is_transitive_in X by Lm12; theorem :: ORDERS_1:81 for R being Relation for X being set st R is_antisymmetric_in X holds R ~ is_antisymmetric_in X by Lm13; theorem :: ORDERS_1:82 for R being Relation for X being set st R is_connected_in X holds R ~ is_connected_in X by Lm14; theorem :: ORDERS_1:83 for R being Relation for X being set holds (R |_2 X) ~ = (R ~) |_2 X by Lm15; theorem :: ORDERS_1:84 for R being Relation holds R |_2 {} = {} by Lm16; begin theorem :: ORDERS_1:85 for f being Function for Z being set st Z is finite & Z c= rng f holds ex Y being set st ( Y c= dom f & Y is finite & f .: Y = Z ) proof let f be Function; ::_thesis: for Z being set st Z is finite & Z c= rng f holds ex Y being set st ( Y c= dom f & Y is finite & f .: Y = Z ) let Z be set ; ::_thesis: ( Z is finite & Z c= rng f implies ex Y being set st ( Y c= dom f & Y is finite & f .: Y = Z ) ) assume that A1: Z is finite and A2: Z c= rng f ; ::_thesis: ex Y being set st ( Y c= dom f & Y is finite & f .: Y = Z ) percases ( Z = {} or Z <> {} ) ; supposeA3: Z = {} ; ::_thesis: ex Y being set st ( Y c= dom f & Y is finite & f .: Y = Z ) take Y = {} ; ::_thesis: ( Y c= dom f & Y is finite & f .: Y = Z ) thus ( Y c= dom f & Y is finite ) by XBOOLE_1:2; ::_thesis: f .: Y = Z thus f .: Y = Z by A3; ::_thesis: verum end; supposeA4: Z <> {} ; ::_thesis: ex Y being set st ( Y c= dom f & Y is finite & f .: Y = Z ) deffunc H1( set ) -> set = f " {\$1}; consider g being Function such that A5: dom g = Z and A6: for x being set st x in Z holds g . x = H1(x) from FUNCT_1:sch_3(); reconsider AA = rng g as non empty set by A4, A5, RELAT_1:42; set ff = the Choice_Function of AA; take Y = the Choice_Function of AA .: AA; ::_thesis: ( Y c= dom f & Y is finite & f .: Y = Z ) A7: for X being set st X in AA holds X <> {} proof let X be set ; ::_thesis: ( X in AA implies X <> {} ) assume X in AA ; ::_thesis: X <> {} then consider x being set such that A8: x in dom g and A9: g . x = X by FUNCT_1:def_3; g . x = f " {x} by A5, A6, A8; hence X <> {} by A2, A5, A8, A9, FUNCT_1:72; ::_thesis: verum end; then A10: not {} in AA ; thus A11: Y c= dom f ::_thesis: ( Y is finite & f .: Y = Z ) proof let x be set ; :: according to TARSKI:def_3 ::_thesis: ( not x in Y or x in dom f ) assume x in Y ; ::_thesis: x in dom f then consider y being set such that y in dom the Choice_Function of AA and A12: y in AA and A13: the Choice_Function of AA . y = x by FUNCT_1:def_6; y in g .: Z by A5, A12, RELAT_1:113; then consider z being set such that z in dom g and A14: z in Z and A15: g . z = y by FUNCT_1:def_6; A16: g . z = f " {z} by A6, A14; x in g . z by A10, A12, A13, A15, Def1; hence x in dom f by A16, FUNCT_1:def_7; ::_thesis: verum end; AA = g .: Z by A5, RELAT_1:113; hence Y is finite by A1; ::_thesis: f .: Y = Z set z = the Element of AA; set y = the Element of the Element of AA; the Element of AA <> {} by A7; then the Element of the Element of AA in the Element of AA ; then reconsider AA9 = union AA as non empty set by TARSKI:def_4; reconsider f9 = the Choice_Function of AA as Function of AA,AA9 ; A17: dom f9 = AA by FUNCT_2:def_1; for x being set holds ( x in f .: Y iff x in Z ) proof let x be set ; ::_thesis: ( x in f .: Y iff x in Z ) thus ( x in f .: Y implies x in Z ) ::_thesis: ( x in Z implies x in f .: Y ) proof assume x in f .: Y ; ::_thesis: x in Z then consider y being set such that y in dom f and A18: y in Y and A19: f . y = x by FUNCT_1:def_6; consider z being set such that A20: z in dom the Choice_Function of AA and z in AA and A21: the Choice_Function of AA . z = y by A18, FUNCT_1:def_6; consider a being set such that A22: a in dom g and A23: g . a = z by A20, FUNCT_1:def_3; g . a = f " {a} by A5, A6, A22; then y in f " {a} by A10, A20, A21, A23, Def1; then f . y in {a} by FUNCT_1:def_7; hence x in Z by A5, A19, A22, TARSKI:def_1; ::_thesis: verum end; set y = the Choice_Function of AA . (g . x); assume A24: x in Z ; ::_thesis: x in f .: Y then A25: g . x in AA by A5, FUNCT_1:def_3; g . x = f " {x} by A6, A24; then the Choice_Function of AA . (g . x) in f " {x} by A10, A25, Def1; then f . ( the Choice_Function of AA . (g . x)) in {x} by FUNCT_1:def_7; then A26: f . ( the Choice_Function of AA . (g . x)) = x by TARSKI:def_1; the Choice_Function of AA . (g . x) in rng the Choice_Function of AA by A17, A25, FUNCT_1:def_3; then the Choice_Function of AA . (g . x) in Y by A17, RELAT_1:113; hence x in f .: Y by A11, A26, FUNCT_1:def_6; ::_thesis: verum end; hence f .: Y = Z by TARSKI:1; ::_thesis: verum end; end; end; theorem Th86: :: ORDERS_1:86 for R being Relation st field R is finite holds R is finite proof let R be Relation; ::_thesis: ( field R is finite implies R is finite ) assume field R is finite ; ::_thesis: R is finite then reconsider A = field R as finite set ; R c= [:A,A:] by Lm4; hence R is finite ; ::_thesis: verum end; theorem :: ORDERS_1:87 for R being Relation st dom R is finite & rng R is finite holds R is finite proof let R be Relation; ::_thesis: ( dom R is finite & rng R is finite implies R is finite ) assume that A1: dom R is finite and A2: rng R is finite ; ::_thesis: R is finite field R is finite by A1, A2; hence R is finite by Th86; ::_thesis: verum end; registration cluster order_type_of {} -> empty ; coherence order_type_of {} is empty proof {} , RelIncl {} are_isomorphic by WELLORD1:38; hence order_type_of {} is empty by WELLORD2:def_2; ::_thesis: verum end; end; theorem :: ORDERS_1:88 for O being Ordinal holds order_type_of (RelIncl O) = O proof let O be Ordinal; ::_thesis: order_type_of (RelIncl O) = O ( RelIncl O is well-ordering & RelIncl O, RelIncl O are_isomorphic ) by WELLORD1:38; hence order_type_of (RelIncl O) = O by WELLORD2:def_2; ::_thesis: verum end;