:: YELLOW21 semantic presentation begin definition let a be set ; funca as_1-sorted -> 1-sorted equals :Def1: :: YELLOW21:def 1 a if a is 1-sorted otherwise 1-sorted(# a #); coherence ( ( a is 1-sorted implies a is 1-sorted ) & ( a is not 1-sorted implies 1-sorted(# a #) is 1-sorted ) ) ; consistency for b1 being 1-sorted holds verum ; end; :: deftheorem Def1 defines as_1-sorted YELLOW21:def_1_:_ for a being set holds ( ( a is 1-sorted implies a as_1-sorted = a ) & ( a is not 1-sorted implies a as_1-sorted = 1-sorted(# a #) ) ); definition let W be set ; defpred S1[ set ] means ( \$1 is strict Poset & the carrier of (\$1 as_1-sorted) in W ); func POSETS W -> set means :Def2: :: YELLOW21:def 2 for x being set holds ( x in it iff ( x is strict Poset & the carrier of (x as_1-sorted) in W ) ); uniqueness for b1, b2 being set st ( for x being set holds ( x in b1 iff ( x is strict Poset & the carrier of (x as_1-sorted) in W ) ) ) & ( for x being set holds ( x in b2 iff ( x is strict Poset & the carrier of (x as_1-sorted) in W ) ) ) holds b1 = b2 proof let A, B be set ; ::_thesis: ( ( for x being set holds ( x in A iff ( x is strict Poset & the carrier of (x as_1-sorted) in W ) ) ) & ( for x being set holds ( x in B iff ( x is strict Poset & the carrier of (x as_1-sorted) in W ) ) ) implies A = B ) assume that A1: for x being set holds ( x in A iff S1[x] ) and A2: for x being set holds ( x in B iff S1[x] ) ; ::_thesis: A = B thus A = B from XBOOLE_0:sch_2(A1, A2); ::_thesis: verum end; existence ex b1 being set st for x being set holds ( x in b1 iff ( x is strict Poset & the carrier of (x as_1-sorted) in W ) ) proof defpred S2[ set , set ] means ex P being strict Poset st ( \$2 = P & the InternalRel of P = \$1 ); defpred S3[ set , set ] means \$2 is Order of \$1; deffunc H1( set ) -> set = bool [:\$1,\$1:]; consider F being Function such that A3: dom F = W and A4: for x being set st x in W holds for y being set holds ( y in F . x iff ( y in H1(x) & S3[x,y] ) ) from CARD_3:sch_2(); A5: now__::_thesis:_for_x,_y,_z_being_set_st_S2[x,y]_&_S2[x,z]_holds_ y_=_z let x, y, z be set ; ::_thesis: ( S2[x,y] & S2[x,z] implies y = z ) assume S2[x,y] ; ::_thesis: ( S2[x,z] implies y = z ) then consider P1 being strict Poset such that A6: ( y = P1 & the InternalRel of P1 = x ) ; A7: dom the InternalRel of P1 = the carrier of P1 by ORDERS_1:14; assume S2[x,z] ; ::_thesis: y = z hence y = z by A6, A7, ORDERS_1:14; ::_thesis: verum end; consider A being set such that A8: for x being set holds ( x in A iff ex y being set st ( y in Union F & S2[y,x] ) ) from TARSKI:sch_1(A5); take A ; ::_thesis: for x being set holds ( x in A iff ( x is strict Poset & the carrier of (x as_1-sorted) in W ) ) let x be set ; ::_thesis: ( x in A iff ( x is strict Poset & the carrier of (x as_1-sorted) in W ) ) hereby ::_thesis: ( x is strict Poset & the carrier of (x as_1-sorted) in W implies x in A ) assume x in A ; ::_thesis: ( x is strict Poset & the carrier of (x as_1-sorted) in W ) then consider y being set such that A9: y in Union F and A10: ex P being strict Poset st ( x = P & the InternalRel of P = y ) by A8; consider P being strict Poset such that A11: x = P and A12: the InternalRel of P = y by A10; thus x is strict Poset by A11; ::_thesis: the carrier of (x as_1-sorted) in W consider z being set such that A13: z in W and A14: y in F . z by A3, A9, CARD_5:2; reconsider y = y as Order of z by A4, A13, A14; ( dom y = z & dom y = the carrier of P ) by A12, ORDERS_1:14; hence the carrier of (x as_1-sorted) in W by A11, A13, Def1; ::_thesis: verum end; assume that A15: x is strict Poset and A16: the carrier of (x as_1-sorted) in W ; ::_thesis: x in A reconsider P = x as strict Poset by A15; A17: x as_1-sorted = P by Def1; then the InternalRel of P in F . the carrier of P by A4, A16; then the InternalRel of P in Union F by A3, A16, A17, CARD_5:2; hence x in A by A8; ::_thesis: verum end; end; :: deftheorem Def2 defines POSETS YELLOW21:def_2_:_ for W being set for b2 being set holds ( b2 = POSETS W iff for x being set holds ( x in b2 iff ( x is strict Poset & the carrier of (x as_1-sorted) in W ) ) ); registration let W be non empty set ; cluster POSETS W -> non empty ; coherence not POSETS W is empty proof set x = the Element of W; set y = the Order of the Element of W; RelStr(# the Element of W, the Order of the Element of W #) as_1-sorted = RelStr(# the Element of W, the Order of the Element of W #) by Def1; hence not POSETS W is empty by Def2; ::_thesis: verum end; end; registration let W be with_non-empty_elements set ; cluster POSETS W -> POSet_set-like ; coherence POSETS W is POSet_set-like proof let a be set ; :: according to ORDERS_3:def_4 ::_thesis: ( not a in POSETS W or a is RelStr ) assume A1: a in POSETS W ; ::_thesis: a is RelStr then A2: the carrier of (a as_1-sorted) in W by Def2; reconsider a = a as Poset by A1, Def2; a = a as_1-sorted by Def1; hence a is RelStr by A2; ::_thesis: verum end; end; definition let C be category; attrC is carrier-underlaid means :Def3: :: YELLOW21:def 3 for a being object of C ex S being 1-sorted st ( a = S & the_carrier_of a = the carrier of S ); end; :: deftheorem Def3 defines carrier-underlaid YELLOW21:def_3_:_ for C being category holds ( C is carrier-underlaid iff for a being object of C ex S being 1-sorted st ( a = S & the_carrier_of a = the carrier of S ) ); definition let C be category; attrC is lattice-wise means :Def4: :: YELLOW21:def 4 ( C is semi-functional & C is set-id-inheriting & ( for a being object of C holds a is LATTICE ) & ( for a, b being object of C for A, B being LATTICE st A = a & B = b holds <^a,b^> c= MonFuncs (A,B) ) ); end; :: deftheorem Def4 defines lattice-wise YELLOW21:def_4_:_ for C being category holds ( C is lattice-wise iff ( C is semi-functional & C is set-id-inheriting & ( for a being object of C holds a is LATTICE ) & ( for a, b being object of C for A, B being LATTICE st A = a & B = b holds <^a,b^> c= MonFuncs (A,B) ) ) ); definition let C be category; attrC is with_complete_lattices means :Def5: :: YELLOW21:def 5 ( C is lattice-wise & ( for a being object of C holds a is complete LATTICE ) ); end; :: deftheorem Def5 defines with_complete_lattices YELLOW21:def_5_:_ for C being category holds ( C is with_complete_lattices iff ( C is lattice-wise & ( for a being object of C holds a is complete LATTICE ) ) ); registration cluster non empty transitive V110() with_units with_complete_lattices -> lattice-wise for AltCatStr ; coherence for b1 being category st b1 is with_complete_lattices holds b1 is lattice-wise by Def5; cluster non empty transitive V110() with_units lattice-wise -> concrete carrier-underlaid for AltCatStr ; coherence for b1 being category st b1 is lattice-wise holds ( b1 is concrete & b1 is carrier-underlaid ) proof deffunc H1( set ) -> set = the carrier of (c1 as_1-sorted); let C be category; ::_thesis: ( C is lattice-wise implies ( C is concrete & C is carrier-underlaid ) ) assume that A1: ( C is semi-functional & C is set-id-inheriting ) and A2: for a being object of C holds a is LATTICE and A3: for a, b being object of C for A, B being LATTICE st A = a & B = b holds <^a,b^> c= MonFuncs (A,B) ; :: according to YELLOW21:def_4 ::_thesis: ( C is concrete & C is carrier-underlaid ) consider F being ManySortedSet of C such that A4: for i being Element of C holds F . i = H1(i) from PBOOLE:sch_5(); C is para-functional proof take F ; :: according to YELLOW18:def_7 ::_thesis: for b1, b2 being Element of the carrier of C holds <^b1,b2^> c= Funcs ((F . b1),(F . b2)) let a, b be object of C; ::_thesis: <^a,b^> c= Funcs ((F . a),(F . b)) reconsider A = a, B = b as LATTICE by A2; A5: <^a,b^> c= MonFuncs (A,B) by A3; b as_1-sorted = B by Def1; then A6: F . b = the carrier of B by A4; a as_1-sorted = A by Def1; then F . a = the carrier of A by A4; then MonFuncs (A,B) c= Funcs ((F . a),(F . b)) by A6, ORDERS_3:11; hence <^a,b^> c= Funcs ((F . a),(F . b)) by A5, XBOOLE_1:1; ::_thesis: verum end; hence C is concrete by A1; ::_thesis: C is carrier-underlaid let a be object of C; :: according to YELLOW21:def_3 ::_thesis: ex S being 1-sorted st ( a = S & the_carrier_of a = the carrier of S ) reconsider S = a as LATTICE by A2; ( idm a in <^a,a^> & <^a,a^> c= MonFuncs (S,S) ) by A3; then consider f being Function of S,S such that A7: idm a = f and A8: f in Funcs ( the carrier of S, the carrier of S) and f is monotone by ORDERS_3:def_6; take S ; ::_thesis: ( a = S & the_carrier_of a = the carrier of S ) thus a = S ; ::_thesis: the_carrier_of a = the carrier of S thus the_carrier_of a = dom (id (the_carrier_of a)) by RELAT_1:45 .= dom f by A1, A7, YELLOW18:def_10 .= the carrier of S by A8, FUNCT_2:92 ; ::_thesis: verum end; end; scheme :: YELLOW21:sch 1 localCLCatEx{ F1() -> non empty set , P1[ set , set , set ] } : ex C being strict category st ( C is lattice-wise & the carrier of C = F1() & ( for a, b being LATTICE for f being monotone Function of a,b holds ( f in the Arrows of C . (a,b) iff ( a in F1() & b in F1() & P1[a,b,f] ) ) ) ) provided A1: for a being Element of F1() holds a is LATTICE and A2: for a, b, c being LATTICE st a in F1() & b in F1() & c in F1() holds for f being Function of a,b for g being Function of b,c st P1[a,b,f] & P1[b,c,g] holds P1[a,c,g * f] and A3: for a being LATTICE st a in F1() holds P1[a,a, id a] proof defpred S1[ set , set ] means ex a, b being LATTICE st ( \$1 = [a,b] & ( for f being set holds ( f in \$2 iff ( f in MonFuncs (a,b) & P1[a,b,f] ) ) ) ); set A = F1(); A4: now__::_thesis:_for_x_being_set_st_x_in_[:F1(),F1():]_holds_ ex_y_being_set_st_S1[x,y] let x be set ; ::_thesis: ( x in [:F1(),F1():] implies ex y being set st S1[x,y] ) assume x in [:F1(),F1():] ; ::_thesis: ex y being set st S1[x,y] then consider a, b being set such that A5: ( a in F1() & b in F1() ) and A6: x = [a,b] by ZFMISC_1:def_2; reconsider a = a, b = b as LATTICE by A1, A5; defpred S2[ set ] means P1[a,b,\$1]; consider y being set such that A7: for f being set holds ( f in y iff ( f in MonFuncs (a,b) & S2[f] ) ) from XBOOLE_0:sch_1(); take y = y; ::_thesis: S1[x,y] thus S1[x,y] by A6, A7; ::_thesis: verum end; consider F being Function such that dom F = [:F1(),F1():] and A8: for x being set st x in [:F1(),F1():] holds S1[x,F . x] from CLASSES1:sch_1(A4); defpred S2[ set , set ] means for a being LATTICE st a = \$1 holds \$2 = the carrier of a; A9: now__::_thesis:_for_x_being_set_st_x_in_F1()_holds_ ex_b_being_set_st_S2[x,b] let x be set ; ::_thesis: ( x in F1() implies ex b being set st S2[x,b] ) assume x in F1() ; ::_thesis: ex b being set st S2[x,b] then reconsider a = x as LATTICE by A1; reconsider b = the carrier of a as set ; take b = b; ::_thesis: S2[x,b] thus S2[x,b] ; ::_thesis: verum end; consider D being Function such that dom D = F1() and A10: for x being set st x in F1() holds S2[x,D . x] from CLASSES1:sch_1(A9); deffunc H1( set , set ) -> set = F . [\$1,\$2]; A11: now__::_thesis:_for_a,_b_being_LATTICE_st_a_in_F1()_&_b_in_F1()_holds_ for_f_being_set_holds_ (_(_f_in_F_._[a,b]_implies_(_P1[a,b,f]_&_f_in_MonFuncs_(a,b)_&_f_in_Funcs_(_the_carrier_of_a,_the_carrier_of_b)_&_f_is_monotone_Function_of_a,b_)_)_&_(_f_is_monotone_Function_of_a,b_&_P1[a,b,f]_implies_f_in_F_._[a,b]_)_) let a, b be LATTICE; ::_thesis: ( a in F1() & b in F1() implies for f being set holds ( ( f in F . [a,b] implies ( P1[a,b,f] & f in MonFuncs (a,b) & f in Funcs ( the carrier of a, the carrier of b) & f is monotone Function of a,b ) ) & ( f is monotone Function of a,b & P1[a,b,f] implies f in F . [a,b] ) ) ) assume ( a in F1() & b in F1() ) ; ::_thesis: for f being set holds ( ( f in F . [a,b] implies ( P1[a,b,f] & f in MonFuncs (a,b) & f in Funcs ( the carrier of a, the carrier of b) & f is monotone Function of a,b ) ) & ( f is monotone Function of a,b & P1[a,b,f] implies f in F . [a,b] ) ) then [a,b] in [:F1(),F1():] by ZFMISC_1:87; then consider a9, b9 being LATTICE such that A12: [a,b] = [a9,b9] and A13: for f being set holds ( f in F . [a,b] iff ( f in MonFuncs (a9,b9) & P1[a9,b9,f] ) ) by A8; let f be set ; ::_thesis: ( ( f in F . [a,b] implies ( P1[a,b,f] & f in MonFuncs (a,b) & f in Funcs ( the carrier of a, the carrier of b) & f is monotone Function of a,b ) ) & ( f is monotone Function of a,b & P1[a,b,f] implies f in F . [a,b] ) ) A14: ( a = a9 & b = b9 ) by A12, XTUPLE_0:1; hereby ::_thesis: ( f is monotone Function of a,b & P1[a,b,f] implies f in F . [a,b] ) assume A15: f in F . [a,b] ; ::_thesis: ( P1[a,b,f] & f in MonFuncs (a,b) & f in Funcs ( the carrier of a, the carrier of b) & f is monotone Function of a,b ) hence P1[a,b,f] by A13, A14; ::_thesis: ( f in MonFuncs (a,b) & f in Funcs ( the carrier of a, the carrier of b) & f is monotone Function of a,b ) thus f in MonFuncs (a,b) by A13, A14, A15; ::_thesis: ( f in Funcs ( the carrier of a, the carrier of b) & f is monotone Function of a,b ) then ex g being Function of a,b st ( f = g & g in Funcs ( the carrier of a, the carrier of b) & g is monotone ) by ORDERS_3:def_6; hence ( f in Funcs ( the carrier of a, the carrier of b) & f is monotone Function of a,b ) ; ::_thesis: verum end; assume f is monotone Function of a,b ; ::_thesis: ( P1[a,b,f] implies f in F . [a,b] ) then reconsider g = f as monotone Function of a,b ; ( the carrier of b <> {} implies ( dom g = the carrier of a & rng g c= the carrier of b ) ) by FUNCT_2:def_1; then g in Funcs ( the carrier of a, the carrier of b) by FUNCT_2:def_2; then f in MonFuncs (a,b) by ORDERS_3:def_6; hence ( P1[a,b,f] implies f in F . [a,b] ) by A13, A14; ::_thesis: verum end; A16: for a, b, c being Element of F1() for f, g being Function st f in H1(a,b) & g in H1(b,c) holds g * f in H1(a,c) proof let a, b, c be Element of F1(); ::_thesis: for f, g being Function st f in H1(a,b) & g in H1(b,c) holds g * f in H1(a,c) let f, g be Function; ::_thesis: ( f in H1(a,b) & g in H1(b,c) implies g * f in H1(a,c) ) assume that A17: f in F . [a,b] and A18: g in F . [b,c] ; ::_thesis: g * f in H1(a,c) reconsider x = a, y = b, z = c as LATTICE by A1; reconsider g9 = g as monotone Function of y,z by A11, A18; reconsider f9 = f as monotone Function of x,y by A11, A17; ( P1[x,y,f9] & P1[y,z,g9] ) by A11, A17, A18; then P1[a,c,g9 * f9] by A2; then ( g9 * f9 is monotone Function of x,z implies g9 * f9 in F . [x,z] ) by A11; hence g * f in H1(a,c) by YELLOW_2:12; ::_thesis: verum end; deffunc H2( set ) -> set = D . \$1; A19: for a, b being Element of F1() holds H1(a,b) c= Funcs (H2(a),H2(b)) proof let a, b be Element of F1(); ::_thesis: H1(a,b) c= Funcs (H2(a),H2(b)) let f be set ; :: according to TARSKI:def_3 ::_thesis: ( not f in H1(a,b) or f in Funcs (H2(a),H2(b)) ) reconsider x = a, y = b as LATTICE by A1; assume f in F . [a,b] ; ::_thesis: f in Funcs (H2(a),H2(b)) then f in Funcs ( the carrier of x, the carrier of y) by A11; then f in Funcs ((D . a), the carrier of y) by A10; hence f in Funcs (H2(a),H2(b)) by A10; ::_thesis: verum end; A20: now__::_thesis:_for_a_being_Element_of_F1()_holds_id_H2(a)_in_H1(a,a) let a be Element of F1(); ::_thesis: id H2(a) in H1(a,a) reconsider x = a as LATTICE by A1; ( id (D . a) = id x & P1[x,x, id x] ) by A3, A10; hence id H2(a) in H1(a,a) by A11; ::_thesis: verum end; consider C being strict concrete category such that A21: the carrier of C = F1() and for a being object of C holds the_carrier_of a = H2(a) and A22: for a, b being object of C holds <^a,b^> = H1(a,b) from YELLOW18:sch_16(A16, A19, A20); take C ; ::_thesis: ( C is lattice-wise & the carrier of C = F1() & ( for a, b being LATTICE for f being monotone Function of a,b holds ( f in the Arrows of C . (a,b) iff ( a in F1() & b in F1() & P1[a,b,f] ) ) ) ) thus ( C is semi-functional & C is set-id-inheriting ) ; :: according to YELLOW21:def_4 ::_thesis: ( ( for a being object of C holds a is LATTICE ) & ( for a, b being object of C for A, B being LATTICE st A = a & B = b holds <^a,b^> c= MonFuncs (A,B) ) & the carrier of C = F1() & ( for a, b being LATTICE for f being monotone Function of a,b holds ( f in the Arrows of C . (a,b) iff ( a in F1() & b in F1() & P1[a,b,f] ) ) ) ) thus for a being object of C holds a is LATTICE by A1, A21; ::_thesis: ( ( for a, b being object of C for A, B being LATTICE st A = a & B = b holds <^a,b^> c= MonFuncs (A,B) ) & the carrier of C = F1() & ( for a, b being LATTICE for f being monotone Function of a,b holds ( f in the Arrows of C . (a,b) iff ( a in F1() & b in F1() & P1[a,b,f] ) ) ) ) thus for a, b being object of C for A, B being LATTICE st A = a & B = b holds <^a,b^> c= MonFuncs (A,B) ::_thesis: ( the carrier of C = F1() & ( for a, b being LATTICE for f being monotone Function of a,b holds ( f in the Arrows of C . (a,b) iff ( a in F1() & b in F1() & P1[a,b,f] ) ) ) ) proof let a, b be object of C; ::_thesis: for A, B being LATTICE st A = a & B = b holds <^a,b^> c= MonFuncs (A,B) let A, B be LATTICE; ::_thesis: ( A = a & B = b implies <^a,b^> c= MonFuncs (A,B) ) assume A23: ( A = a & B = b ) ; ::_thesis: <^a,b^> c= MonFuncs (A,B) let f be set ; :: according to TARSKI:def_3 ::_thesis: ( not f in <^a,b^> or f in MonFuncs (A,B) ) <^a,b^> = F . [A,B] by A22, A23; hence ( not f in <^a,b^> or f in MonFuncs (A,B) ) by A11, A21, A23; ::_thesis: verum end; thus the carrier of C = F1() by A21; ::_thesis: for a, b being LATTICE for f being monotone Function of a,b holds ( f in the Arrows of C . (a,b) iff ( a in F1() & b in F1() & P1[a,b,f] ) ) let a, b be LATTICE; ::_thesis: for f being monotone Function of a,b holds ( f in the Arrows of C . (a,b) iff ( a in F1() & b in F1() & P1[a,b,f] ) ) let f be monotone Function of a,b; ::_thesis: ( f in the Arrows of C . (a,b) iff ( a in F1() & b in F1() & P1[a,b,f] ) ) hereby ::_thesis: ( a in F1() & b in F1() & P1[a,b,f] implies f in the Arrows of C . (a,b) ) assume A24: f in the Arrows of C . (a,b) ; ::_thesis: ( a in F1() & b in F1() & P1[a,b,f] ) then [a,b] in dom the Arrows of C by FUNCT_1:def_2; then A25: [a,b] in [:F1(),F1():] by A21; hence ( a in F1() & b in F1() ) by ZFMISC_1:87; ::_thesis: P1[a,b,f] reconsider x = a, y = b as object of C by A21, A25, ZFMISC_1:87; the Arrows of C . [a,b] = <^x,y^> .= F . [x,y] by A22 ; hence P1[a,b,f] by A11, A21, A24; ::_thesis: verum end; assume A26: ( a in F1() & b in F1() ) ; ::_thesis: ( not P1[a,b,f] or f in the Arrows of C . (a,b) ) then reconsider x = a, y = b as object of C by A21; the Arrows of C . [a,b] = <^x,y^> .= F . [x,y] by A22 ; hence ( not P1[a,b,f] or f in the Arrows of C . (a,b) ) by A11, A26; ::_thesis: verum end; registration cluster non empty transitive strict V110() with_units reflexive with_complete_lattices for AltCatStr ; existence ex b1 being category st ( b1 is strict & b1 is with_complete_lattices ) proof defpred S1[ set , set , set ] means c3 = c3; set L = the complete LATTICE; A1: for a, b, c being LATTICE st a in { the complete LATTICE} & b in { the complete LATTICE} & c in { the complete LATTICE} holds for f being Function of a,b for g being Function of b,c st S1[a,b,f] & S1[b,c,g] holds S1[a,c,g * f] ; A2: for a being LATTICE st a in { the complete LATTICE} holds S1[a,a, id a] ; A3: for a being Element of { the complete LATTICE} holds a is LATTICE by TARSKI:def_1; consider C being strict category such that A4: C is lattice-wise and A5: the carrier of C = { the complete LATTICE} and for a, b being LATTICE for f being monotone Function of a,b holds ( f in the Arrows of C . (a,b) iff ( a in { the complete LATTICE} & b in { the complete LATTICE} & S1[a,b,f] ) ) from YELLOW21:sch_1(A3, A1, A2); take C ; ::_thesis: ( C is strict & C is with_complete_lattices ) thus C is strict ; ::_thesis: C is with_complete_lattices thus C is lattice-wise by A4; :: according to YELLOW21:def_5 ::_thesis: for a being object of C holds a is complete LATTICE let a be object of C; ::_thesis: a is complete LATTICE thus a is complete LATTICE by A5, TARSKI:def_1; ::_thesis: verum end; end; theorem :: YELLOW21:1 for C being carrier-underlaid category for a being object of C holds the_carrier_of a = the carrier of (a as_1-sorted) proof let C be carrier-underlaid category; ::_thesis: for a being object of C holds the_carrier_of a = the carrier of (a as_1-sorted) let a be object of C; ::_thesis: the_carrier_of a = the carrier of (a as_1-sorted) ex S being 1-sorted st ( a = S & the_carrier_of a = the carrier of S ) by Def3; hence the_carrier_of a = the carrier of (a as_1-sorted) by Def1; ::_thesis: verum end; theorem Th2: :: YELLOW21:2 for C being set-id-inheriting carrier-underlaid category for a being object of C holds idm a = id (a as_1-sorted) proof let C be set-id-inheriting carrier-underlaid category; ::_thesis: for a being object of C holds idm a = id (a as_1-sorted) let a be object of C; ::_thesis: idm a = id (a as_1-sorted) ex S being 1-sorted st ( a = S & the_carrier_of a = the carrier of S ) by Def3; then the_carrier_of a = the carrier of (a as_1-sorted) by Def1; hence idm a = id (a as_1-sorted) by YELLOW18:def_10; ::_thesis: verum end; notation let C be lattice-wise category; let a be object of C; synonym latt a for C as_1-sorted ; end; definition let C be lattice-wise category; let a be object of C; :: original: as_1-sorted redefine func latt a -> LATTICE equals :: YELLOW21:def 6 a; coherence a as_1-sorted is LATTICE proof a is LATTICE by Def4; hence a as_1-sorted is LATTICE by Def1; ::_thesis: verum end; compatibility for b1 being LATTICE holds ( b1 = a as_1-sorted iff b1 = a ) proof a is LATTICE by Def4; hence for b1 being LATTICE holds ( b1 = a as_1-sorted iff b1 = a ) by Def1; ::_thesis: verum end; end; :: deftheorem defines latt YELLOW21:def_6_:_ for C being lattice-wise category for a being object of C holds latt a = a; notation let C be with_complete_lattices category; let a be object of C; synonym latt a for C as_1-sorted ; end; definition let C be with_complete_lattices category; let a be object of C; :: original: as_1-sorted redefine func latt a -> complete LATTICE; coherence a as_1-sorted is complete LATTICE by Def5; end; definition let C be lattice-wise category; let a, b be object of C; assume A1: <^a,b^> <> {} ; let f be Morphism of a,b; func @ f -> monotone Function of (latt a),(latt b) equals :Def7: :: YELLOW21:def 7 f; coherence f is monotone Function of (latt a),(latt b) proof ( f in <^a,b^> & <^a,b^> c= MonFuncs ((latt a),(latt b)) ) by A1, Def4; then ex g being Function of (latt a),(latt b) st ( f = g & g in Funcs ( the carrier of (latt a), the carrier of (latt b)) & g is monotone ) by ORDERS_3:def_6; hence f is monotone Function of (latt a),(latt b) ; ::_thesis: verum end; end; :: deftheorem Def7 defines @ YELLOW21:def_7_:_ for C being lattice-wise category for a, b being object of C st <^a,b^> <> {} holds for f being Morphism of a,b holds @ f = f; theorem Th3: :: YELLOW21:3 for C being lattice-wise category for a, b, c being object of C st <^a,b^> <> {} & <^b,c^> <> {} holds for f being Morphism of a,b for g being Morphism of b,c holds g * f = (@ g) * (@ f) proof let C be lattice-wise category; ::_thesis: for a, b, c being object of C st <^a,b^> <> {} & <^b,c^> <> {} holds for f being Morphism of a,b for g being Morphism of b,c holds g * f = (@ g) * (@ f) let a, b, c be object of C; ::_thesis: ( <^a,b^> <> {} & <^b,c^> <> {} implies for f being Morphism of a,b for g being Morphism of b,c holds g * f = (@ g) * (@ f) ) assume A1: ( <^a,b^> <> {} & <^b,c^> <> {} ) ; ::_thesis: for f being Morphism of a,b for g being Morphism of b,c holds g * f = (@ g) * (@ f) let f be Morphism of a,b; ::_thesis: for g being Morphism of b,c holds g * f = (@ g) * (@ f) let g be Morphism of b,c; ::_thesis: g * f = (@ g) * (@ f) ( f = @ f & g = @ g ) by A1, Def7; hence g * f = (@ g) * (@ f) by A1, YELLOW18:36; ::_thesis: verum end; scheme :: YELLOW21:sch 2 CLCatEx1{ F1() -> non empty set , P1[ set , set , set ] } : ex C being strict lattice-wise category st ( the carrier of C = F1() & ( for a, b being object of C for f being monotone Function of (latt a),(latt b) holds ( f in <^a,b^> iff P1[ latt a, latt b,f] ) ) ) provided A1: for a being Element of F1() holds a is LATTICE and A2: for a, b, c being LATTICE st a in F1() & b in F1() & c in F1() holds for f being Function of a,b for g being Function of b,c st P1[a,b,f] & P1[b,c,g] holds P1[a,c,g * f] and A3: for a being LATTICE st a in F1() holds P1[a,a, id a] proof A4: for a being LATTICE st a in F1() holds P1[a,a, id a] by A3; A5: for a, b, c being LATTICE st a in F1() & b in F1() & c in F1() holds for f being Function of a,b for g being Function of b,c st P1[a,b,f] & P1[b,c,g] holds P1[a,c,g * f] by A2; consider C being strict category such that A6: C is lattice-wise and A7: the carrier of C = F1() and A8: for a, b being LATTICE for f being monotone Function of a,b holds ( f in the Arrows of C . (a,b) iff ( a in F1() & b in F1() & P1[a,b,f] ) ) from YELLOW21:sch_1(A1, A5, A4); reconsider C = C as strict lattice-wise category by A6; take C ; ::_thesis: ( the carrier of C = F1() & ( for a, b being object of C for f being monotone Function of (latt a),(latt b) holds ( f in <^a,b^> iff P1[ latt a, latt b,f] ) ) ) thus the carrier of C = F1() by A7; ::_thesis: for a, b being object of C for f being monotone Function of (latt a),(latt b) holds ( f in <^a,b^> iff P1[ latt a, latt b,f] ) let a, b be object of C; ::_thesis: for f being monotone Function of (latt a),(latt b) holds ( f in <^a,b^> iff P1[ latt a, latt b,f] ) thus for f being monotone Function of (latt a),(latt b) holds ( f in <^a,b^> iff P1[ latt a, latt b,f] ) by A7, A8; ::_thesis: verum end; scheme :: YELLOW21:sch 3 CLCatEx2{ F1() -> non empty set , P1[ set ], P2[ set , set , set ] } : ex C being strict lattice-wise category st ( ( for x being LATTICE holds ( x is object of C iff ( x is strict & P1[x] & the carrier of x in F1() ) ) ) & ( for a, b being object of C for f being monotone Function of (latt a),(latt b) holds ( f in <^a,b^> iff P2[ latt a, latt b,f] ) ) ) provided A1: ex x being strict LATTICE st ( P1[x] & the carrier of x in F1() ) and A2: for a, b, c being LATTICE st P1[a] & P1[b] & P1[c] holds for f being Function of a,b for g being Function of b,c st P2[a,b,f] & P2[b,c,g] holds P2[a,c,g * f] and A3: for a being LATTICE st P1[a] holds P2[a,a, id a] proof defpred S1[ set ] means ( \$1 is LATTICE & P1[\$1] ); consider A being set such that A4: for x being set holds ( x in A iff ( x in POSETS F1() & S1[x] ) ) from XBOOLE_0:sch_1(); consider x being strict LATTICE such that A5: P1[x] and A6: the carrier of x in F1() by A1; x as_1-sorted = x by Def1; then x in POSETS F1() by A6, Def2; then reconsider A = A as non empty set by A4, A5; A7: now__::_thesis:_for_a,_b,_c_being_LATTICE_st_a_in_A_&_b_in_A_&_c_in_A_holds_ for_f_being_Function_of_a,b for_g_being_Function_of_b,c_st_P2[a,b,f]_&_P2[b,c,g]_holds_ P2[a,c,g_*_f] let a, b, c be LATTICE; ::_thesis: ( a in A & b in A & c in A implies for f being Function of a,b for g being Function of b,c st P2[a,b,f] & P2[b,c,g] holds P2[a,c,g * f] ) assume that A8: ( a in A & b in A ) and A9: c in A ; ::_thesis: for f being Function of a,b for g being Function of b,c st P2[a,b,f] & P2[b,c,g] holds P2[a,c,g * f] A10: P1[c] by A4, A9; ( P1[a] & P1[b] ) by A4, A8; hence for f being Function of a,b for g being Function of b,c st P2[a,b,f] & P2[b,c,g] holds P2[a,c,g * f] by A2, A10; ::_thesis: verum end; A11: now__::_thesis:_for_a_being_LATTICE_st_a_in_A_holds_ P2[a,a,_id_a] let a be LATTICE; ::_thesis: ( a in A implies P2[a,a, id a] ) assume a in A ; ::_thesis: P2[a,a, id a] then P1[a] by A4; hence P2[a,a, id a] by A3; ::_thesis: verum end; A12: for a being Element of A holds a is LATTICE by A4; consider C being strict lattice-wise category such that A13: the carrier of C = A and A14: for a, b being object of C for f being monotone Function of (latt a),(latt b) holds ( f in <^a,b^> iff P2[ latt a, latt b,f] ) from YELLOW21:sch_2(A12, A7, A11); take C ; ::_thesis: ( ( for x being LATTICE holds ( x is object of C iff ( x is strict & P1[x] & the carrier of x in F1() ) ) ) & ( for a, b being object of C for f being monotone Function of (latt a),(latt b) holds ( f in <^a,b^> iff P2[ latt a, latt b,f] ) ) ) hereby ::_thesis: for a, b being object of C for f being monotone Function of (latt a),(latt b) holds ( f in <^a,b^> iff P2[ latt a, latt b,f] ) let x be LATTICE; ::_thesis: ( x is object of C iff ( x is strict & P1[x] & the carrier of x in F1() ) ) x as_1-sorted = x by Def1; then ( x in POSETS F1() iff ( x is strict Poset & the carrier of x in F1() ) ) by Def2; hence ( x is object of C iff ( x is strict & P1[x] & the carrier of x in F1() ) ) by A4, A13; ::_thesis: verum end; thus for a, b being object of C for f being monotone Function of (latt a),(latt b) holds ( f in <^a,b^> iff P2[ latt a, latt b,f] ) by A14; ::_thesis: verum end; scheme :: YELLOW21:sch 4 CLCatUniq1{ F1() -> non empty set , P1[ set , set , set ] } : for C1, C2 being lattice-wise category st the carrier of C1 = F1() & ( for a, b being object of C1 for f being monotone Function of (latt a),(latt b) holds ( f in <^a,b^> iff P1[a,b,f] ) ) & the carrier of C2 = F1() & ( for a, b being object of C2 for f being monotone Function of (latt a),(latt b) holds ( f in <^a,b^> iff P1[a,b,f] ) ) holds AltCatStr(# the carrier of C1, the Arrows of C1, the Comp of C1 #) = AltCatStr(# the carrier of C2, the Arrows of C2, the Comp of C2 #) proof let A1, A2 be lattice-wise category; ::_thesis: ( the carrier of A1 = F1() & ( for a, b being object of A1 for f being monotone Function of (latt a),(latt b) holds ( f in <^a,b^> iff P1[a,b,f] ) ) & the carrier of A2 = F1() & ( for a, b being object of A2 for f being monotone Function of (latt a),(latt b) holds ( f in <^a,b^> iff P1[a,b,f] ) ) implies AltCatStr(# the carrier of A1, the Arrows of A1, the Comp of A1 #) = AltCatStr(# the carrier of A2, the Arrows of A2, the Comp of A2 #) ) deffunc H1( set , set ) -> set = the Arrows of A1 . (\$1,\$2); assume that A1: the carrier of A1 = F1() and A2: for a, b being object of A1 for f being monotone Function of (latt a),(latt b) holds ( f in <^a,b^> iff P1[a,b,f] ) and A3: the carrier of A2 = F1() and A4: for a, b being object of A2 for f being monotone Function of (latt a),(latt b) holds ( f in <^a,b^> iff P1[a,b,f] ) ; ::_thesis: AltCatStr(# the carrier of A1, the Arrows of A1, the Comp of A1 #) = AltCatStr(# the carrier of A2, the Arrows of A2, the Comp of A2 #) A5: now__::_thesis:_for_a,_b_being_object_of_A2_holds_<^a,b^>_=_the_Arrows_of_A1_._(a,b) let a, b be object of A2; ::_thesis: <^a,b^> = the Arrows of A1 . (a,b) reconsider a9 = a, b9 = b as object of A1 by A1, A3; A6: <^a9,b9^> = the Arrows of A1 . (a9,b9) ; thus <^a,b^> = the Arrows of A1 . (a,b) ::_thesis: verum proof hereby :: according to TARSKI:def_3,XBOOLE_0:def_10 ::_thesis: the Arrows of A1 . (a,b) c= <^a,b^> let x be set ; ::_thesis: ( x in <^a,b^> implies x in the Arrows of A1 . (a,b) ) assume A7: x in <^a,b^> ; ::_thesis: x in the Arrows of A1 . (a,b) then reconsider f = x as Morphism of a,b ; A8: @ f = f by A7, Def7; then P1[ latt a9, latt b9, @ f] by A4, A7; hence x in the Arrows of A1 . (a,b) by A2, A6, A8; ::_thesis: verum end; let x be set ; :: according to TARSKI:def_3 ::_thesis: ( not x in the Arrows of A1 . (a,b) or x in <^a,b^> ) assume A9: x in the Arrows of A1 . (a,b) ; ::_thesis: x in <^a,b^> then reconsider f = x as Morphism of a9,b9 ; A10: @ f = f by A9, Def7; then P1[ latt a, latt b, @ f] by A2, A9; hence x in <^a,b^> by A4, A10; ::_thesis: verum end; end; A11: for a, b being object of A1 holds <^a,b^> = the Arrows of A1 . (a,b) ; for C1, C2 being semi-functional para-functional category st the carrier of C1 = F1() & ( for a, b being object of C1 holds <^a,b^> = H1(a,b) ) & the carrier of C2 = F1() & ( for a, b being object of C2 holds <^a,b^> = H1(a,b) ) holds AltCatStr(# the carrier of C1, the Arrows of C1, the Comp of C1 #) = AltCatStr(# the carrier of C2, the Arrows of C2, the Comp of C2 #) from YELLOW18:sch_19(); hence AltCatStr(# the carrier of A1, the Arrows of A1, the Comp of A1 #) = AltCatStr(# the carrier of A2, the Arrows of A2, the Comp of A2 #) by A1, A3, A11, A5; ::_thesis: verum end; scheme :: YELLOW21:sch 5 CLCatUniq2{ F1() -> non empty set , P1[ set ], P2[ set , set , set ] } : for C1, C2 being lattice-wise category st ( for x being LATTICE holds ( x is object of C1 iff ( x is strict & P1[x] & the carrier of x in F1() ) ) ) & ( for a, b being object of C1 for f being monotone Function of (latt a),(latt b) holds ( f in <^a,b^> iff P2[a,b,f] ) ) & ( for x being LATTICE holds ( x is object of C2 iff ( x is strict & P1[x] & the carrier of x in F1() ) ) ) & ( for a, b being object of C2 for f being monotone Function of (latt a),(latt b) holds ( f in <^a,b^> iff P2[a,b,f] ) ) holds AltCatStr(# the carrier of C1, the Arrows of C1, the Comp of C1 #) = AltCatStr(# the carrier of C2, the Arrows of C2, the Comp of C2 #) proof let A1, A2 be lattice-wise category; ::_thesis: ( ( for x being LATTICE holds ( x is object of A1 iff ( x is strict & P1[x] & the carrier of x in F1() ) ) ) & ( for a, b being object of A1 for f being monotone Function of (latt a),(latt b) holds ( f in <^a,b^> iff P2[a,b,f] ) ) & ( for x being LATTICE holds ( x is object of A2 iff ( x is strict & P1[x] & the carrier of x in F1() ) ) ) & ( for a, b being object of A2 for f being monotone Function of (latt a),(latt b) holds ( f in <^a,b^> iff P2[a,b,f] ) ) implies AltCatStr(# the carrier of A1, the Arrows of A1, the Comp of A1 #) = AltCatStr(# the carrier of A2, the Arrows of A2, the Comp of A2 #) ) assume that A1: for x being LATTICE holds ( x is object of A1 iff ( x is strict & P1[x] & the carrier of x in F1() ) ) and A2: for a, b being object of A1 for f being monotone Function of (latt a),(latt b) holds ( f in <^a,b^> iff P2[a,b,f] ) and A3: for x being LATTICE holds ( x is object of A2 iff ( x is strict & P1[x] & the carrier of x in F1() ) ) ; ::_thesis: ( ex a, b being object of A2 ex f being monotone Function of (latt a),(latt b) st ( ( f in <^a,b^> implies P2[a,b,f] ) implies ( P2[a,b,f] & not f in <^a,b^> ) ) or AltCatStr(# the carrier of A1, the Arrows of A1, the Comp of A1 #) = AltCatStr(# the carrier of A2, the Arrows of A2, the Comp of A2 #) ) A4: the carrier of A2 = the carrier of A1 proof hereby :: according to TARSKI:def_3,XBOOLE_0:def_10 ::_thesis: the carrier of A1 c= the carrier of A2 let x be set ; ::_thesis: ( x in the carrier of A2 implies x in the carrier of A1 ) assume A5: x in the carrier of A2 ; ::_thesis: x in the carrier of A1 then A6: x is LATTICE by Def4; then A7: ( x is strict LATTICE & P1[x] ) by A3, A5; A8: x as_1-sorted = x by A6, Def1; then the carrier of (x as_1-sorted) in F1() by A3, A5, A6; then x is object of A1 by A1, A8, A7; hence x in the carrier of A1 ; ::_thesis: verum end; let x be set ; :: according to TARSKI:def_3 ::_thesis: ( not x in the carrier of A1 or x in the carrier of A2 ) assume A9: x in the carrier of A1 ; ::_thesis: x in the carrier of A2 then A10: x is LATTICE by Def4; then A11: ( x is strict LATTICE & P1[x] ) by A1, A9; A12: x as_1-sorted = x by A10, Def1; then the carrier of (x as_1-sorted) in F1() by A1, A9, A10; then x is object of A2 by A3, A12, A11; hence x in the carrier of A2 ; ::_thesis: verum end; for C1, C2 being lattice-wise category st the carrier of C1 = the carrier of A1 & ( for a, b being object of C1 for f being monotone Function of (latt a),(latt b) holds ( f in <^a,b^> iff P2[a,b,f] ) ) & the carrier of C2 = the carrier of A1 & ( for a, b being object of C2 for f being monotone Function of (latt a),(latt b) holds ( f in <^a,b^> iff P2[a,b,f] ) ) holds AltCatStr(# the carrier of C1, the Arrows of C1, the Comp of C1 #) = AltCatStr(# the carrier of C2, the Arrows of C2, the Comp of C2 #) from YELLOW21:sch_4(); hence ( ex a, b being object of A2 ex f being monotone Function of (latt a),(latt b) st ( ( f in <^a,b^> implies P2[a,b,f] ) implies ( P2[a,b,f] & not f in <^a,b^> ) ) or AltCatStr(# the carrier of A1, the Arrows of A1, the Comp of A1 #) = AltCatStr(# the carrier of A2, the Arrows of A2, the Comp of A2 #) ) by A2, A4; ::_thesis: verum end; scheme :: YELLOW21:sch 6 CLCovariantFunctorEx{ P1[ set , set , set ], P2[ set , set , set ], F1() -> lattice-wise category, F2() -> lattice-wise category, F3( set ) -> LATTICE, F4( set , set , set ) -> Function } : ex F being strict covariant Functor of F1(),F2() st ( ( for a being object of F1() holds F . a = F3((latt a)) ) & ( for a, b being object of F1() st <^a,b^> <> {} holds for f being Morphism of a,b holds F . f = F4((latt a),(latt b),(@ f)) ) ) provided A1: for a, b being LATTICE for f being Function of a,b holds ( f in the Arrows of F1() . (a,b) iff ( a in the carrier of F1() & b in the carrier of F1() & P1[a,b,f] ) ) and A2: for a, b being LATTICE for f being Function of a,b holds ( f in the Arrows of F2() . (a,b) iff ( a in the carrier of F2() & b in the carrier of F2() & P2[a,b,f] ) ) and A3: for a being LATTICE st a in the carrier of F1() holds F3(a) in the carrier of F2() and A4: for a, b being LATTICE for f being Function of a,b st P1[a,b,f] holds ( F4(a,b,f) is Function of F3(a),F3(b) & P2[F3(a),F3(b),F4(a,b,f)] ) and A5: for a being LATTICE st a in the carrier of F1() holds F4(a,a,(id a)) = id F3(a) and A6: for a, b, c being LATTICE for f being Function of a,b for g being Function of b,c st P1[a,b,f] & P1[b,c,g] holds F4(a,c,(g * f)) = F4(b,c,g) * F4(a,b,f) proof A7: for a, b being object of F1() st <^a,b^> <> {} holds for f being Morphism of a,b holds F4(a,b,f) in the Arrows of F2() . (F3(a),F3(b)) proof let a, b be object of F1(); ::_thesis: ( <^a,b^> <> {} implies for f being Morphism of a,b holds F4(a,b,f) in the Arrows of F2() . (F3(a),F3(b)) ) assume A8: <^a,b^> <> {} ; ::_thesis: for f being Morphism of a,b holds F4(a,b,f) in the Arrows of F2() . (F3(a),F3(b)) let f be Morphism of a,b; ::_thesis: F4(a,b,f) in the Arrows of F2() . (F3(a),F3(b)) A9: f = @ f by A8, Def7; then P1[a,b,f] by A1, A8; then A10: ( F4(a,b,f) is Function of F3(a),F3(b) & P2[F3(a),F3(b),F4(a,b,f)] ) by A4, A9; ( F3(a) in the carrier of F2() & F3(b) in the carrier of F2() ) by A3, A9; hence F4(a,b,f) in the Arrows of F2() . (F3(a),F3(b)) by A2, A10; ::_thesis: verum end; A11: now__::_thesis:_for_a,_b,_c_being_object_of_F1()_st_<^a,b^>_<>_{}_&_<^b,c^>_<>_{}_holds_ for_f_being_Morphism_of_a,b for_g_being_Morphism_of_b,c for_a9,_b9,_c9_being_object_of_F2()_st_a9_=_F3(a)_&_b9_=_F3(b)_&_c9_=_F3(c)_holds_ for_f9_being_Morphism_of_a9,b9 for_g9_being_Morphism_of_b9,c9_st_f9_=_F4(a,b,f)_&_g9_=_F4(b,c,g)_holds_ F4(a,c,(g_*_f))_=_g9_*_f9 let a, b, c be object of F1(); ::_thesis: ( <^a,b^> <> {} & <^b,c^> <> {} implies for f being Morphism of a,b for g being Morphism of b,c for a9, b9, c9 being object of F2() st a9 = F3(a) & b9 = F3(b) & c9 = F3(c) holds for f9 being Morphism of a9,b9 for g9 being Morphism of b9,c9 st f9 = F4(a,b,f) & g9 = F4(b,c,g) holds F4(a,c,(g * f)) = g9 * f9 ) assume that A12: <^a,b^> <> {} and A13: <^b,c^> <> {} ; ::_thesis: for f being Morphism of a,b for g being Morphism of b,c for a9, b9, c9 being object of F2() st a9 = F3(a) & b9 = F3(b) & c9 = F3(c) holds for f9 being Morphism of a9,b9 for g9 being Morphism of b9,c9 st f9 = F4(a,b,f) & g9 = F4(b,c,g) holds F4(a,c,(g * f)) = g9 * f9 let f be Morphism of a,b; ::_thesis: for g being Morphism of b,c for a9, b9, c9 being object of F2() st a9 = F3(a) & b9 = F3(b) & c9 = F3(c) holds for f9 being Morphism of a9,b9 for g9 being Morphism of b9,c9 st f9 = F4(a,b,f) & g9 = F4(b,c,g) holds F4(a,c,(g * f)) = g9 * f9 let g be Morphism of b,c; ::_thesis: for a9, b9, c9 being object of F2() st a9 = F3(a) & b9 = F3(b) & c9 = F3(c) holds for f9 being Morphism of a9,b9 for g9 being Morphism of b9,c9 st f9 = F4(a,b,f) & g9 = F4(b,c,g) holds F4(a,c,(g * f)) = g9 * f9 let a9, b9, c9 be object of F2(); ::_thesis: ( a9 = F3(a) & b9 = F3(b) & c9 = F3(c) implies for f9 being Morphism of a9,b9 for g9 being Morphism of b9,c9 st f9 = F4(a,b,f) & g9 = F4(b,c,g) holds F4(a,c,(g * f)) = g9 * f9 ) assume that A14: a9 = F3(a) and A15: b9 = F3(b) and A16: c9 = F3(c) ; ::_thesis: for f9 being Morphism of a9,b9 for g9 being Morphism of b9,c9 st f9 = F4(a,b,f) & g9 = F4(b,c,g) holds F4(a,c,(g * f)) = g9 * f9 let f9 be Morphism of a9,b9; ::_thesis: for g9 being Morphism of b9,c9 st f9 = F4(a,b,f) & g9 = F4(b,c,g) holds F4(a,c,(g * f)) = g9 * f9 let g9 be Morphism of b9,c9; ::_thesis: ( f9 = F4(a,b,f) & g9 = F4(b,c,g) implies F4(a,c,(g * f)) = g9 * f9 ) assume A17: ( f9 = F4(a,b,f) & g9 = F4(b,c,g) ) ; ::_thesis: F4(a,c,(g * f)) = g9 * f9 A18: F4(a,b,f) in the Arrows of F2() . (F3(a),F3(b)) by A7, A12; then A19: @ f9 = f9 by A14, A15, Def7; A20: @ g = g by A13, Def7; then A21: P1[b,c,g] by A1, A13; A22: F4(b,c,g) in the Arrows of F2() . (F3(b),F3(c)) by A7, A13; then A23: @ g9 = g9 by A15, A16, Def7; A24: @ f = f by A12, Def7; then P1[a,b,f] by A1, A12; then F4(a,c,((@ g) * (@ f))) = F4(b,c,g) * F4(a,b,f) by A6, A24, A20, A21 .= g9 * f9 by A14, A15, A16, A17, A18, A22, A19, A23, Th3 ; hence F4(a,c,(g * f)) = g9 * f9 by A12, A13, Th3; ::_thesis: verum end; A25: now__::_thesis:_for_a_being_object_of_F1() for_a9_being_object_of_F2()_st_a9_=_F3(a)_holds_ F4(a,a,(idm_a))_=_idm_a9 let a be object of F1(); ::_thesis: for a9 being object of F2() st a9 = F3(a) holds F4(a,a,(idm a)) = idm a9 let a9 be object of F2(); ::_thesis: ( a9 = F3(a) implies F4(a,a,(idm a)) = idm a9 ) assume A26: a9 = F3(a) ; ::_thesis: F4(a,a,(idm a)) = idm a9 idm a = id (latt a) by Th2; hence F4(a,a,(idm a)) = id (latt a9) by A5, A26 .= idm a9 by Th2 ; ::_thesis: verum end; A27: for a being object of F1() holds F3(a) is object of F2() proof let a be object of F1(); ::_thesis: F3(a) is object of F2() a is LATTICE by Def4; hence F3(a) is object of F2() by A3; ::_thesis: verum end; consider F being strict covariant Functor of F1(),F2() such that A28: for a being object of F1() holds F . a = F3(a) and A29: for a, b being object of F1() st <^a,b^> <> {} holds for f being Morphism of a,b holds F . f = F4(a,b,f) from YELLOW18:sch_8(A27, A7, A11, A25); take F ; ::_thesis: ( ( for a being object of F1() holds F . a = F3((latt a)) ) & ( for a, b being object of F1() st <^a,b^> <> {} holds for f being Morphism of a,b holds F . f = F4((latt a),(latt b),(@ f)) ) ) thus for a being object of F1() holds F . a = F3((latt a)) by A28; ::_thesis: for a, b being object of F1() st <^a,b^> <> {} holds for f being Morphism of a,b holds F . f = F4((latt a),(latt b),(@ f)) let a, b be object of F1(); ::_thesis: ( <^a,b^> <> {} implies for f being Morphism of a,b holds F . f = F4((latt a),(latt b),(@ f)) ) assume A30: <^a,b^> <> {} ; ::_thesis: for f being Morphism of a,b holds F . f = F4((latt a),(latt b),(@ f)) let f be Morphism of a,b; ::_thesis: F . f = F4((latt a),(latt b),(@ f)) f = @ f by A30, Def7; hence F . f = F4((latt a),(latt b),(@ f)) by A29, A30; ::_thesis: verum end; scheme :: YELLOW21:sch 7 CLContravariantFunctorEx{ P1[ set , set , set ], P2[ set , set , set ], F1() -> lattice-wise category, F2() -> lattice-wise category, F3( set ) -> LATTICE, F4( set , set , set ) -> Function } : ex F being strict contravariant Functor of F1(),F2() st ( ( for a being object of F1() holds F . a = F3((latt a)) ) & ( for a, b being object of F1() st <^a,b^> <> {} holds for f being Morphism of a,b holds F . f = F4((latt a),(latt b),(@ f)) ) ) provided A1: for a, b being LATTICE for f being Function of a,b holds ( f in the Arrows of F1() . (a,b) iff ( a in the carrier of F1() & b in the carrier of F1() & P1[a,b,f] ) ) and A2: for a, b being LATTICE for f being Function of a,b holds ( f in the Arrows of F2() . (a,b) iff ( a in the carrier of F2() & b in the carrier of F2() & P2[a,b,f] ) ) and A3: for a being LATTICE st a in the carrier of F1() holds F3(a) in the carrier of F2() and A4: for a, b being LATTICE for f being Function of a,b st P1[a,b,f] holds ( F4(a,b,f) is Function of F3(b),F3(a) & P2[F3(b),F3(a),F4(a,b,f)] ) and A5: for a being LATTICE st a in the carrier of F1() holds F4(a,a,(id a)) = id F3(a) and A6: for a, b, c being LATTICE for f being Function of a,b for g being Function of b,c st P1[a,b,f] & P1[b,c,g] holds F4(a,c,(g * f)) = F4(a,b,f) * F4(b,c,g) proof A7: for a, b being object of F1() st <^a,b^> <> {} holds for f being Morphism of a,b holds F4(a,b,f) in the Arrows of F2() . (F3(b),F3(a)) proof let a, b be object of F1(); ::_thesis: ( <^a,b^> <> {} implies for f being Morphism of a,b holds F4(a,b,f) in the Arrows of F2() . (F3(b),F3(a)) ) assume A8: <^a,b^> <> {} ; ::_thesis: for f being Morphism of a,b holds F4(a,b,f) in the Arrows of F2() . (F3(b),F3(a)) let f be Morphism of a,b; ::_thesis: F4(a,b,f) in the Arrows of F2() . (F3(b),F3(a)) A9: f = @ f by A8, Def7; then P1[a,b,f] by A1, A8; then A10: ( F4(a,b,f) is Function of F3(b),F3(a) & P2[F3(b),F3(a),F4(a,b,f)] ) by A4, A9; ( F3(a) in the carrier of F2() & F3(b) in the carrier of F2() ) by A3, A9; hence F4(a,b,f) in the Arrows of F2() . (F3(b),F3(a)) by A2, A10; ::_thesis: verum end; A11: now__::_thesis:_for_a,_b,_c_being_object_of_F1()_st_<^a,b^>_<>_{}_&_<^b,c^>_<>_{}_holds_ for_f_being_Morphism_of_a,b for_g_being_Morphism_of_b,c for_a9,_b9,_c9_being_object_of_F2()_st_a9_=_F3(a)_&_b9_=_F3(b)_&_c9_=_F3(c)_holds_ for_f9_being_Morphism_of_b9,a9 for_g9_being_Morphism_of_c9,b9_st_f9_=_F4(a,b,f)_&_g9_=_F4(b,c,g)_holds_ F4(a,c,(g_*_f))_=_f9_*_g9 let a, b, c be object of F1(); ::_thesis: ( <^a,b^> <> {} & <^b,c^> <> {} implies for f being Morphism of a,b for g being Morphism of b,c for a9, b9, c9 being object of F2() st a9 = F3(a) & b9 = F3(b) & c9 = F3(c) holds for f9 being Morphism of b9,a9 for g9 being Morphism of c9,b9 st f9 = F4(a,b,f) & g9 = F4(b,c,g) holds F4(a,c,(g * f)) = f9 * g9 ) assume that A12: <^a,b^> <> {} and A13: <^b,c^> <> {} ; ::_thesis: for f being Morphism of a,b for g being Morphism of b,c for a9, b9, c9 being object of F2() st a9 = F3(a) & b9 = F3(b) & c9 = F3(c) holds for f9 being Morphism of b9,a9 for g9 being Morphism of c9,b9 st f9 = F4(a,b,f) & g9 = F4(b,c,g) holds F4(a,c,(g * f)) = f9 * g9 let f be Morphism of a,b; ::_thesis: for g being Morphism of b,c for a9, b9, c9 being object of F2() st a9 = F3(a) & b9 = F3(b) & c9 = F3(c) holds for f9 being Morphism of b9,a9 for g9 being Morphism of c9,b9 st f9 = F4(a,b,f) & g9 = F4(b,c,g) holds F4(a,c,(g * f)) = f9 * g9 let g be Morphism of b,c; ::_thesis: for a9, b9, c9 being object of F2() st a9 = F3(a) & b9 = F3(b) & c9 = F3(c) holds for f9 being Morphism of b9,a9 for g9 being Morphism of c9,b9 st f9 = F4(a,b,f) & g9 = F4(b,c,g) holds F4(a,c,(g * f)) = f9 * g9 let a9, b9, c9 be object of F2(); ::_thesis: ( a9 = F3(a) & b9 = F3(b) & c9 = F3(c) implies for f9 being Morphism of b9,a9 for g9 being Morphism of c9,b9 st f9 = F4(a,b,f) & g9 = F4(b,c,g) holds F4(a,c,(g * f)) = f9 * g9 ) assume that A14: a9 = F3(a) and A15: b9 = F3(b) and A16: c9 = F3(c) ; ::_thesis: for f9 being Morphism of b9,a9 for g9 being Morphism of c9,b9 st f9 = F4(a,b,f) & g9 = F4(b,c,g) holds F4(a,c,(g * f)) = f9 * g9 let f9 be Morphism of b9,a9; ::_thesis: for g9 being Morphism of c9,b9 st f9 = F4(a,b,f) & g9 = F4(b,c,g) holds F4(a,c,(g * f)) = f9 * g9 let g9 be Morphism of c9,b9; ::_thesis: ( f9 = F4(a,b,f) & g9 = F4(b,c,g) implies F4(a,c,(g * f)) = f9 * g9 ) assume A17: ( f9 = F4(a,b,f) & g9 = F4(b,c,g) ) ; ::_thesis: F4(a,c,(g * f)) = f9 * g9 A18: F4(a,b,f) in the Arrows of F2() . (F3(b),F3(a)) by A7, A12; then A19: @ f9 = f9 by A14, A15, Def7; A20: @ g = g by A13, Def7; then A21: P1[b,c,g] by A1, A13; A22: F4(b,c,g) in the Arrows of F2() . (F3(c),F3(b)) by A7, A13; then A23: @ g9 = g9 by A15, A16, Def7; A24: @ f = f by A12, Def7; then P1[a,b,f] by A1, A12; then F4(a,c,((@ g) * (@ f))) = F4(a,b,f) * F4(b,c,g) by A6, A24, A20, A21 .= f9 * g9 by A14, A15, A16, A17, A18, A22, A19, A23, Th3 ; hence F4(a,c,(g * f)) = f9 * g9 by A12, A13, Th3; ::_thesis: verum end; A25: now__::_thesis:_for_a_being_object_of_F1() for_a9_being_object_of_F2()_st_a9_=_F3(a)_holds_ F4(a,a,(idm_a))_=_idm_a9 let a be object of F1(); ::_thesis: for a9 being object of F2() st a9 = F3(a) holds F4(a,a,(idm a)) = idm a9 let a9 be object of F2(); ::_thesis: ( a9 = F3(a) implies F4(a,a,(idm a)) = idm a9 ) assume A26: a9 = F3(a) ; ::_thesis: F4(a,a,(idm a)) = idm a9 idm a = id (latt a) by Th2; hence F4(a,a,(idm a)) = id (latt a9) by A5, A26 .= idm a9 by Th2 ; ::_thesis: verum end; A27: for a being object of F1() holds F3(a) is object of F2() proof let a be object of F1(); ::_thesis: F3(a) is object of F2() a is LATTICE by Def4; hence F3(a) is object of F2() by A3; ::_thesis: verum end; consider F being strict contravariant Functor of F1(),F2() such that A28: for a being object of F1() holds F . a = F3(a) and A29: for a, b being object of F1() st <^a,b^> <> {} holds for f being Morphism of a,b holds F . f = F4(a,b,f) from YELLOW18:sch_9(A27, A7, A11, A25); take F ; ::_thesis: ( ( for a being object of F1() holds F . a = F3((latt a)) ) & ( for a, b being object of F1() st <^a,b^> <> {} holds for f being Morphism of a,b holds F . f = F4((latt a),(latt b),(@ f)) ) ) thus for a being object of F1() holds F . a = F3((latt a)) by A28; ::_thesis: for a, b being object of F1() st <^a,b^> <> {} holds for f being Morphism of a,b holds F . f = F4((latt a),(latt b),(@ f)) let a, b be object of F1(); ::_thesis: ( <^a,b^> <> {} implies for f being Morphism of a,b holds F . f = F4((latt a),(latt b),(@ f)) ) assume A30: <^a,b^> <> {} ; ::_thesis: for f being Morphism of a,b holds F . f = F4((latt a),(latt b),(@ f)) let f be Morphism of a,b; ::_thesis: F . f = F4((latt a),(latt b),(@ f)) f = @ f by A30, Def7; hence F . f = F4((latt a),(latt b),(@ f)) by A29, A30; ::_thesis: verum end; scheme :: YELLOW21:sch 8 CLCatIsomorphism{ P1[ set , set , set ], P2[ set , set , set ], F1() -> lattice-wise category, F2() -> lattice-wise category, F3( set ) -> LATTICE, F4( set , set , set ) -> Function } : F1(),F2() are_isomorphic provided A1: for a, b being LATTICE for f being Function of a,b holds ( f in the Arrows of F1() . (a,b) iff ( a in the carrier of F1() & b in the carrier of F1() & P1[a,b,f] ) ) and A2: for a, b being LATTICE for f being Function of a,b holds ( f in the Arrows of F2() . (a,b) iff ( a in the carrier of F2() & b in the carrier of F2() & P2[a,b,f] ) ) and A3: ex F being covariant Functor of F1(),F2() st ( ( for a being object of F1() holds F . a = F3(a) ) & ( for a, b being object of F1() st <^a,b^> <> {} holds for f being Morphism of a,b holds F . f = F4(a,b,f) ) ) and A4: for a, b being LATTICE st a in the carrier of F1() & b in the carrier of F1() & F3(a) = F3(b) holds a = b and A5: for a, b being LATTICE for f, g being Function of a,b st P1[a,b,f] & P1[a,b,g] & F4(a,b,f) = F4(a,b,g) holds f = g and A6: for a, b being LATTICE for f being Function of a,b st P2[a,b,f] holds ex c, d being LATTICE ex g being Function of c,d st ( c in the carrier of F1() & d in the carrier of F1() & P1[c,d,g] & a = F3(c) & b = F3(d) & f = F4(c,d,g) ) proof A7: for a, b being object of F1() st F3(a) = F3(b) holds a = b proof let a, b be object of F1(); ::_thesis: ( F3(a) = F3(b) implies a = b ) ( a = latt a & b = latt b ) ; hence ( F3(a) = F3(b) implies a = b ) by A4; ::_thesis: verum end; A8: now__::_thesis:_for_a,_b_being_object_of_F2()_st_<^a,b^>_<>_{}_holds_ for_f_being_Morphism_of_a,b_ex_c,_d_being_object_of_F1()_ex_g_being_Morphism_of_c,d_st_ (_a_=_F3(c)_&_b_=_F3(d)_&_<^c,d^>_<>_{}_&_f_=_F4(c,d,g)_) let a, b be object of F2(); ::_thesis: ( <^a,b^> <> {} implies for f being Morphism of a,b ex c, d being object of F1() ex g being Morphism of c,d st ( a = F3(c) & b = F3(d) & <^c,d^> <> {} & f = F4(c,d,g) ) ) assume A9: <^a,b^> <> {} ; ::_thesis: for f being Morphism of a,b ex c, d being object of F1() ex g being Morphism of c,d st ( a = F3(c) & b = F3(d) & <^c,d^> <> {} & f = F4(c,d,g) ) let f be Morphism of a,b; ::_thesis: ex c, d being object of F1() ex g being Morphism of c,d st ( a = F3(c) & b = F3(d) & <^c,d^> <> {} & f = F4(c,d,g) ) A10: @ f = f by A9, Def7; then P2[ latt a, latt b, @ f] by A2, A9; then consider c, d being LATTICE, g being Function of c,d such that A11: ( c in the carrier of F1() & d in the carrier of F1() ) and A12: P1[c,d,g] and A13: ( latt a = F3(c) & latt b = F3(d) & @ f = F4(c,d,g) ) by A6; reconsider c9 = c, d9 = d as object of F1() by A11; g in <^c9,d9^> by A1, A12; hence ex c, d being object of F1() ex g being Morphism of c,d st ( a = F3(c) & b = F3(d) & <^c,d^> <> {} & f = F4(c,d,g) ) by A10, A13; ::_thesis: verum end; A14: for a, b being object of F1() st <^a,b^> <> {} holds for f, g being Morphism of a,b st F4(a,b,f) = F4(a,b,g) holds f = g proof let a, b be object of F1(); ::_thesis: ( <^a,b^> <> {} implies for f, g being Morphism of a,b st F4(a,b,f) = F4(a,b,g) holds f = g ) assume A15: <^a,b^> <> {} ; ::_thesis: for f, g being Morphism of a,b st F4(a,b,f) = F4(a,b,g) holds f = g let f, g be Morphism of a,b; ::_thesis: ( F4(a,b,f) = F4(a,b,g) implies f = g ) A16: @ g = g by A15, Def7; then A17: P1[ latt a, latt b, @ g] by A1, A15; A18: @ f = f by A15, Def7; then P1[ latt a, latt b, @ f] by A1, A15; hence ( F4(a,b,f) = F4(a,b,g) implies f = g ) by A5, A18, A16, A17; ::_thesis: verum end; A19: ex F being covariant Functor of F1(),F2() st ( ( for a being object of F1() holds F . a = F3(a) ) & ( for a, b being object of F1() st <^a,b^> <> {} holds for f being Morphism of a,b holds F . f = F4(a,b,f) ) ) by A3; thus F1(),F2() are_isomorphic from YELLOW18:sch_11(A19, A7, A14, A8); ::_thesis: verum end; scheme :: YELLOW21:sch 9 CLCatAntiIsomorphism{ P1[ set , set , set ], P2[ set , set , set ], F1() -> lattice-wise category, F2() -> lattice-wise category, F3( set ) -> LATTICE, F4( set , set , set ) -> Function } : F1(),F2() are_anti-isomorphic provided A1: for a, b being LATTICE for f being Function of a,b holds ( f in the Arrows of F1() . (a,b) iff ( a in the carrier of F1() & b in the carrier of F1() & P1[a,b,f] ) ) and A2: for a, b being LATTICE for f being Function of a,b holds ( f in the Arrows of F2() . (a,b) iff ( a in the carrier of F2() & b in the carrier of F2() & P2[a,b,f] ) ) and A3: ex F being contravariant Functor of F1(),F2() st ( ( for a being object of F1() holds F . a = F3(a) ) & ( for a, b being object of F1() st <^a,b^> <> {} holds for f being Morphism of a,b holds F . f = F4(a,b,f) ) ) and A4: for a, b being LATTICE st a in the carrier of F1() & b in the carrier of F1() & F3(a) = F3(b) holds a = b and A5: for a, b being LATTICE for f, g being Function of a,b st F4(a,b,f) = F4(a,b,g) holds f = g and A6: for a, b being LATTICE for f being Function of a,b st P2[a,b,f] holds ex c, d being LATTICE ex g being Function of c,d st ( c in the carrier of F1() & d in the carrier of F1() & P1[c,d,g] & b = F3(c) & a = F3(d) & f = F4(c,d,g) ) proof A7: for a, b being object of F1() st F3(a) = F3(b) holds a = b proof let a, b be object of F1(); ::_thesis: ( F3(a) = F3(b) implies a = b ) ( a = latt a & b = latt b ) ; hence ( F3(a) = F3(b) implies a = b ) by A4; ::_thesis: verum end; A8: now__::_thesis:_for_a,_b_being_object_of_F2()_st_<^a,b^>_<>_{}_holds_ for_f_being_Morphism_of_a,b_ex_c,_d_being_object_of_F1()_ex_g_being_Morphism_of_c,d_st_ (_b_=_F3(c)_&_a_=_F3(d)_&_<^c,d^>_<>_{}_&_f_=_F4(c,d,g)_) let a, b be object of F2(); ::_thesis: ( <^a,b^> <> {} implies for f being Morphism of a,b ex c, d being object of F1() ex g being Morphism of c,d st ( b = F3(c) & a = F3(d) & <^c,d^> <> {} & f = F4(c,d,g) ) ) assume A9: <^a,b^> <> {} ; ::_thesis: for f being Morphism of a,b ex c, d being object of F1() ex g being Morphism of c,d st ( b = F3(c) & a = F3(d) & <^c,d^> <> {} & f = F4(c,d,g) ) let f be Morphism of a,b; ::_thesis: ex c, d being object of F1() ex g being Morphism of c,d st ( b = F3(c) & a = F3(d) & <^c,d^> <> {} & f = F4(c,d,g) ) A10: @ f = f by A9, Def7; then P2[ latt a, latt b, @ f] by A2, A9; then consider c, d being LATTICE, g being Function of c,d such that A11: ( c in the carrier of F1() & d in the carrier of F1() ) and A12: P1[c,d,g] and A13: ( latt b = F3(c) & latt a = F3(d) & @ f = F4(c,d,g) ) by A6; reconsider c9 = c, d9 = d as object of F1() by A11; g in <^c9,d9^> by A1, A12; hence ex c, d being object of F1() ex g being Morphism of c,d st ( b = F3(c) & a = F3(d) & <^c,d^> <> {} & f = F4(c,d,g) ) by A10, A13; ::_thesis: verum end; A14: for a, b being object of F1() st <^a,b^> <> {} holds for f, g being Morphism of a,b st F4(a,b,f) = F4(a,b,g) holds f = g proof let a, b be object of F1(); ::_thesis: ( <^a,b^> <> {} implies for f, g being Morphism of a,b st F4(a,b,f) = F4(a,b,g) holds f = g ) assume A15: <^a,b^> <> {} ; ::_thesis: for f, g being Morphism of a,b st F4(a,b,f) = F4(a,b,g) holds f = g let f, g be Morphism of a,b; ::_thesis: ( F4(a,b,f) = F4(a,b,g) implies f = g ) ( @ f = f & @ g = g ) by A15, Def7; hence ( F4(a,b,f) = F4(a,b,g) implies f = g ) by A5; ::_thesis: verum end; A16: ex F being contravariant Functor of F1(),F2() st ( ( for a being object of F1() holds F . a = F3(a) ) & ( for a, b being object of F1() st <^a,b^> <> {} holds for f being Morphism of a,b holds F . f = F4(a,b,f) ) ) by A3; thus F1(),F2() are_anti-isomorphic from YELLOW18:sch_13(A16, A7, A14, A8); ::_thesis: verum end; begin definition let C be lattice-wise category; attrC is with_all_isomorphisms means :Def8: :: YELLOW21:def 8 for a, b being object of C for f being Function of (latt a),(latt b) st f is isomorphic holds f in <^a,b^>; end; :: deftheorem Def8 defines with_all_isomorphisms YELLOW21:def_8_:_ for C being lattice-wise category holds ( C is with_all_isomorphisms iff for a, b being object of C for f being Function of (latt a),(latt b) st f is isomorphic holds f in <^a,b^> ); registration cluster non empty transitive strict semi-functional V110() with_units reflexive para-functional set-id-inheriting concrete carrier-underlaid lattice-wise with_all_isomorphisms for AltCatStr ; existence ex b1 being strict lattice-wise category st b1 is with_all_isomorphisms proof defpred S1[ set , set , set ] means c3 = c3; set L = the LATTICE; A1: for a, b, c being LATTICE st a in { the LATTICE} & b in { the LATTICE} & c in { the LATTICE} holds for f being Function of a,b for g being Function of b,c st S1[a,b,f] & S1[b,c,g] holds S1[a,c,g * f] ; A2: for a being LATTICE st a in { the LATTICE} holds S1[a,a, id a] ; A3: for a being Element of { the LATTICE} holds a is LATTICE by TARSKI:def_1; consider C being strict category such that A4: C is lattice-wise and A5: ( the carrier of C = { the LATTICE} & ( for a, b being LATTICE for f being monotone Function of a,b holds ( f in the Arrows of C . (a,b) iff ( a in { the LATTICE} & b in { the LATTICE} & S1[a,b,f] ) ) ) ) from YELLOW21:sch_1(A3, A1, A2); reconsider C = C as strict lattice-wise category by A4; take C ; ::_thesis: C is with_all_isomorphisms let a, b be object of C; :: according to YELLOW21:def_8 ::_thesis: for f being Function of (latt a),(latt b) st f is isomorphic holds f in <^a,b^> let f be Function of (latt a),(latt b); ::_thesis: ( f is isomorphic implies f in <^a,b^> ) thus ( f is isomorphic implies f in <^a,b^> ) by A5; ::_thesis: verum end; end; theorem :: YELLOW21:4 for C being lattice-wise with_all_isomorphisms category for a, b being object of C for f being Morphism of a,b st @ f is isomorphic holds f is iso proof let C be lattice-wise with_all_isomorphisms category; ::_thesis: for a, b being object of C for f being Morphism of a,b st @ f is isomorphic holds f is iso let a, b be object of C; ::_thesis: for f being Morphism of a,b st @ f is isomorphic holds f is iso let f be Morphism of a,b; ::_thesis: ( @ f is isomorphic implies f is iso ) assume A1: @ f is isomorphic ; ::_thesis: f is iso then consider g being monotone Function of (latt b),(latt a) such that A2: (@ f) * g = id (latt b) and A3: g * (@ f) = id (latt a) by YELLOW16:15; A4: @ f in <^a,b^> by A1, Def8; A5: g is isomorphic by A2, A3, YELLOW16:15; then A6: g in <^b,a^> by Def8; reconsider g = g as Morphism of b,a by A5, Def8; A7: @ g = g by A6, Def7; idm b = id (latt b) by Th2; then A8: f * g = idm b by A2, A4, A6, A7, Th3; then A9: g is_right_inverse_of f by ALTCAT_3:def_1; idm a = id (latt a) by Th2; then A10: g * f = idm a by A3, A4, A6, A7, Th3; then A11: g is_left_inverse_of f by ALTCAT_3:def_1; then ( f is retraction & f is coretraction ) by A9, ALTCAT_3:def_2, ALTCAT_3:def_3; hence ( f * (f ") = idm b & (f ") * f = idm a ) by A4, A6, A8, A10, A11, A9, ALTCAT_3:def_4; :: according to ALTCAT_3:def_5 ::_thesis: verum end; theorem :: YELLOW21:5 for C being lattice-wise category for a, b being object of C st <^a,b^> <> {} & <^b,a^> <> {} holds for f being Morphism of a,b st f is iso holds @ f is isomorphic proof let C be lattice-wise category; ::_thesis: for a, b being object of C st <^a,b^> <> {} & <^b,a^> <> {} holds for f being Morphism of a,b st f is iso holds @ f is isomorphic let a, b be object of C; ::_thesis: ( <^a,b^> <> {} & <^b,a^> <> {} implies for f being Morphism of a,b st f is iso holds @ f is isomorphic ) assume A1: ( <^a,b^> <> {} & <^b,a^> <> {} ) ; ::_thesis: for f being Morphism of a,b st f is iso holds @ f is isomorphic let f be Morphism of a,b; ::_thesis: ( f is iso implies @ f is isomorphic ) assume A2: ( f * (f ") = idm b & (f ") * f = idm a ) ; :: according to ALTCAT_3:def_5 ::_thesis: @ f is isomorphic A3: ( idm a = id (latt a) & idm b = id (latt b) ) by Th2; ( (@ f) * (@ (f ")) = f * (f ") & (@ (f ")) * (@ f) = (f ") * f ) by A1, Th3; hence @ f is isomorphic by A2, A3, YELLOW16:15; ::_thesis: verum end; scheme :: YELLOW21:sch 10 CLCatEquivalence{ P1[ set , set , set ], P2[ set , set , set ], F1() -> lattice-wise category, F2() -> lattice-wise category, F3( set ) -> LATTICE, F4( set ) -> LATTICE, F5( set , set , set ) -> Function, F6( set , set , set ) -> Function, F7( set ) -> Function, F8( set ) -> Function } : F1(),F2() are_equivalent provided A1: for a, b being object of F1() for f being monotone Function of (latt a),(latt b) holds ( f in <^a,b^> iff P1[ latt a, latt b,f] ) and A2: for a, b being object of F2() for f being monotone Function of (latt a),(latt b) holds ( f in <^a,b^> iff P2[ latt a, latt b,f] ) and A3: ex F being covariant Functor of F1(),F2() st ( ( for a being object of F1() holds F . a = F3(a) ) & ( for a, b being object of F1() st <^a,b^> <> {} holds for f being Morphism of a,b holds F . f = F5(a,b,f) ) ) and A4: ex G being covariant Functor of F2(),F1() st ( ( for a being object of F2() holds G . a = F4(a) ) & ( for a, b being object of F2() st <^a,b^> <> {} holds for f being Morphism of a,b holds G . f = F6(a,b,f) ) ) and A5: for a being LATTICE st a in the carrier of F1() holds ex f being monotone Function of F4(F3(a)),a st ( f = F7(a) & f is isomorphic & P1[F4(F3(a)),a,f] & P1[a,F4(F3(a)),f " ] ) and A6: for a being LATTICE st a in the carrier of F2() holds ex f being monotone Function of a,F3(F4(a)) st ( f = F8(a) & f is isomorphic & P2[a,F3(F4(a)),f] & P2[F3(F4(a)),a,f " ] ) and A7: for a, b being object of F1() st <^a,b^> <> {} holds for f being Morphism of a,b holds F7(b) * F6(F3(a),F3(b),F5(a,b,f)) = (@ f) * F7(a) and A8: for a, b being object of F2() st <^a,b^> <> {} holds for f being Morphism of a,b holds F5(F4(a),F4(b),F6(a,b,f)) * F8(a) = F8(b) * (@ f) proof A9: ex G being covariant Functor of F2(),F1() st ( ( for a being object of F2() holds G . a = F4(a) ) & ( for a, b being object of F2() st <^a,b^> <> {} holds for f being Morphism of a,b holds G . f = F6(a,b,f) ) ) by A4; A10: for a, b being object of F2() st <^a,b^> <> {} holds for f being Morphism of a,b holds F5(F4(a),F4(b),F6(a,b,f)) * F8(a) = F8(b) * f proof let a, b be object of F2(); ::_thesis: ( <^a,b^> <> {} implies for f being Morphism of a,b holds F5(F4(a),F4(b),F6(a,b,f)) * F8(a) = F8(b) * f ) assume A11: <^a,b^> <> {} ; ::_thesis: for f being Morphism of a,b holds F5(F4(a),F4(b),F6(a,b,f)) * F8(a) = F8(b) * f let f be Morphism of a,b; ::_thesis: F5(F4(a),F4(b),F6(a,b,f)) * F8(a) = F8(b) * f @ f = f by A11, Def7; hence F5(F4(a),F4(b),F6(a,b,f)) * F8(a) = F8(b) * f by A8, A11; ::_thesis: verum end; A12: for a, b being object of F1() st <^a,b^> <> {} holds for f being Morphism of a,b holds F7(b) * F6(F3(a),F3(b),F5(a,b,f)) = f * F7(a) proof let a, b be object of F1(); ::_thesis: ( <^a,b^> <> {} implies for f being Morphism of a,b holds F7(b) * F6(F3(a),F3(b),F5(a,b,f)) = f * F7(a) ) assume A13: <^a,b^> <> {} ; ::_thesis: for f being Morphism of a,b holds F7(b) * F6(F3(a),F3(b),F5(a,b,f)) = f * F7(a) let f be Morphism of a,b; ::_thesis: F7(b) * F6(F3(a),F3(b),F5(a,b,f)) = f * F7(a) @ f = f by A13, Def7; hence F7(b) * F6(F3(a),F3(b),F5(a,b,f)) = f * F7(a) by A7, A13; ::_thesis: verum end; A14: for a, b being object of F2() st b = F3(F4(a)) holds ( F8(a) in <^a,b^> & F8(a) " in <^b,a^> & F8(a) is one-to-one ) proof let a, b be object of F2(); ::_thesis: ( b = F3(F4(a)) implies ( F8(a) in <^a,b^> & F8(a) " in <^b,a^> & F8(a) is one-to-one ) ) assume A15: b = F3(F4(a)) ; ::_thesis: ( F8(a) in <^a,b^> & F8(a) " in <^b,a^> & F8(a) is one-to-one ) consider f being monotone Function of (latt a),F3(F4(a)) such that A16: f = F8(a) and A17: f is isomorphic and A18: P2[ latt a,F3(F4(a)),f] and A19: P2[F3(F4(a)), latt a,f " ] by A6; A20: latt b = b ; hence F8(a) in <^a,b^> by A2, A15, A16, A18; ::_thesis: ( F8(a) " in <^b,a^> & F8(a) is one-to-one ) ex g being Function of F3(F4(a)),(latt a) st ( g = f " & g is monotone ) by A17, WAYBEL_0:def_38; hence F8(a) " in <^b,a^> by A2, A15, A20, A16, A19; ::_thesis: F8(a) is one-to-one thus F8(a) is one-to-one by A16, A17; ::_thesis: verum end; A21: for a, b being object of F1() st a = F4(F3(b)) holds ( F7(b) in <^a,b^> & F7(b) " in <^b,a^> & F7(b) is one-to-one ) proof let a, b be object of F1(); ::_thesis: ( a = F4(F3(b)) implies ( F7(b) in <^a,b^> & F7(b) " in <^b,a^> & F7(b) is one-to-one ) ) assume A22: a = F4(F3(b)) ; ::_thesis: ( F7(b) in <^a,b^> & F7(b) " in <^b,a^> & F7(b) is one-to-one ) consider f being monotone Function of F4(F3(b)),(latt b) such that A23: f = F7(b) and A24: f is isomorphic and A25: P1[F4(F3(b)), latt b,f] and A26: P1[ latt b,F4(F3(b)),f " ] by A5; A27: latt a = a ; hence F7(b) in <^a,b^> by A1, A22, A23, A25; ::_thesis: ( F7(b) " in <^b,a^> & F7(b) is one-to-one ) ex g being Function of (latt b),F4(F3(b)) st ( g = f " & g is monotone ) by A24, WAYBEL_0:def_38; hence F7(b) " in <^b,a^> by A1, A22, A27, A23, A26; ::_thesis: F7(b) is one-to-one thus F7(b) is one-to-one by A23, A24; ::_thesis: verum end; A28: ex F being covariant Functor of F1(),F2() st ( ( for a being object of F1() holds F . a = F3(a) ) & ( for a, b being object of F1() st <^a,b^> <> {} holds for f being Morphism of a,b holds F . f = F5(a,b,f) ) ) by A3; thus F1(),F2() are_equivalent from YELLOW18:sch_22(A28, A9, A21, A14, A12, A10); ::_thesis: verum end; begin definition let R be Relation; attrR is upper-bounded means :Def9: :: YELLOW21:def 9 ex x being set st for y being set st y in field R holds [y,x] in R; end; :: deftheorem Def9 defines upper-bounded YELLOW21:def_9_:_ for R being Relation holds ( R is upper-bounded iff ex x being set st for y being set st y in field R holds [y,x] in R ); Lm1: for x, X being set holds ( x in X iff X = (X \ {x}) \/ {x} ) proof let x, X be set ; ::_thesis: ( x in X iff X = (X \ {x}) \/ {x} ) ( x in X iff {x} c= X ) by ZFMISC_1:31; hence ( x in X iff X = (X \ {x}) \/ {x} ) by XBOOLE_1:7, XBOOLE_1:45; ::_thesis: verum end; registration cluster Relation-like well-ordering -> well_founded reflexive antisymmetric connected transitive for set ; coherence for b1 being Relation st b1 is well-ordering holds ( b1 is reflexive & b1 is transitive & b1 is antisymmetric & b1 is connected & b1 is well_founded ) ; end; registration cluster Relation-like well-ordering for set ; existence ex b1 being Relation st b1 is well-ordering proof consider r being Relation such that A1: r well_orders 5 by WELLORD2:17; take r |_2 5 ; ::_thesis: r |_2 5 is well-ordering thus r |_2 5 is well-ordering by A1, WELLORD2:16; ::_thesis: verum end; end; theorem Th6: :: YELLOW21:6 for x, y being set for f being one-to-one Function for R being Relation holds ( [x,y] in (f * R) * (f ") iff ( x in dom f & y in dom f & [(f . x),(f . y)] in R ) ) proof let x, y be set ; ::_thesis: for f being one-to-one Function for R being Relation holds ( [x,y] in (f * R) * (f ") iff ( x in dom f & y in dom f & [(f . x),(f . y)] in R ) ) let f be one-to-one Function; ::_thesis: for R being Relation holds ( [x,y] in (f * R) * (f ") iff ( x in dom f & y in dom f & [(f . x),(f . y)] in R ) ) let R be Relation; ::_thesis: ( [x,y] in (f * R) * (f ") iff ( x in dom f & y in dom f & [(f . x),(f . y)] in R ) ) A1: rng f = dom (f ") by FUNCT_1:33; A2: dom f = rng (f ") by FUNCT_1:33; hereby ::_thesis: ( x in dom f & y in dom f & [(f . x),(f . y)] in R implies [x,y] in (f * R) * (f ") ) assume [x,y] in (f * R) * (f ") ; ::_thesis: ( x in dom f & y in dom f & [(f . x),(f . y)] in R ) then consider a being set such that A3: [x,a] in f * R and A4: [a,y] in f " by RELAT_1:def_8; A5: ( y = (f ") . a & a in rng f ) by A1, A4, FUNCT_1:1; consider b being set such that A6: [x,b] in f and A7: [b,a] in R by A3, RELAT_1:def_8; thus ( x in dom f & y in dom f ) by A2, A4, A6, XTUPLE_0:def_12, XTUPLE_0:def_13; ::_thesis: [(f . x),(f . y)] in R b = f . x by A6, FUNCT_1:1; hence [(f . x),(f . y)] in R by A7, A5, FUNCT_1:35; ::_thesis: verum end; assume that A8: x in dom f and A9: y in dom f and A10: [(f . x),(f . y)] in R ; ::_thesis: [x,y] in (f * R) * (f ") ( (f ") . (f . y) = y & f . y in rng f ) by A9, FUNCT_1:34, FUNCT_1:def_3; then A11: [(f . y),y] in f " by A1, FUNCT_1:1; [x,(f . x)] in f by A8, FUNCT_1:1; then [x,(f . y)] in f * R by A10, RELAT_1:def_8; hence [x,y] in (f * R) * (f ") by A11, RELAT_1:def_8; ::_thesis: verum end; registration let f be one-to-one Function; let R be reflexive Relation; cluster(f * R) * (f ") -> reflexive ; coherence (f * R) * (f ") is reflexive proof let x be set ; :: according to RELAT_2:def_1,RELAT_2:def_9 ::_thesis: ( not x in field ((f * R) * (f ")) or [x,x] in (f * R) * (f ") ) A1: R is_reflexive_in field R by RELAT_2:def_9; assume x in field ((f * R) * (f ")) ; ::_thesis: [x,x] in (f * R) * (f ") then A2: x in (dom ((f * R) * (f "))) \/ (rng ((f * R) * (f "))) by RELAT_1:def_6; percases ( x in dom ((f * R) * (f ")) or x in rng ((f * R) * (f ")) ) by A2, XBOOLE_0:def_3; suppose x in dom ((f * R) * (f ")) ; ::_thesis: [x,x] in (f * R) * (f ") then consider y being set such that A3: [x,y] in (f * R) * (f ") by XTUPLE_0:def_12; [(f . x),(f . y)] in R by A3, Th6; then f . x in field R by RELAT_1:15; then A4: [(f . x),(f . x)] in R by A1, RELAT_2:def_1; x in dom f by A3, Th6; hence [x,x] in (f * R) * (f ") by A4, Th6; ::_thesis: verum end; suppose x in rng ((f * R) * (f ")) ; ::_thesis: [x,x] in (f * R) * (f ") then consider y being set such that A5: [y,x] in (f * R) * (f ") by XTUPLE_0:def_13; [(f . y),(f . x)] in R by A5, Th6; then f . x in field R by RELAT_1:15; then A6: [(f . x),(f . x)] in R by A1, RELAT_2:def_1; x in dom f by A5, Th6; hence [x,x] in (f * R) * (f ") by A6, Th6; ::_thesis: verum end; end; end; end; registration let f be one-to-one Function; let R be antisymmetric Relation; cluster(f * R) * (f ") -> antisymmetric ; coherence (f * R) * (f ") is antisymmetric proof let x, y be set ; :: according to RELAT_2:def_4,RELAT_2:def_12 ::_thesis: ( not x in field ((f * R) * (f ")) or not y in field ((f * R) * (f ")) or not [x,y] in (f * R) * (f ") or not [y,x] in (f * R) * (f ") or x = y ) assume that x in field ((f * R) * (f ")) and y in field ((f * R) * (f ")) ; ::_thesis: ( not [x,y] in (f * R) * (f ") or not [y,x] in (f * R) * (f ") or x = y ) assume that A1: [x,y] in (f * R) * (f ") and A2: [y,x] in (f * R) * (f ") ; ::_thesis: x = y A3: ( x in dom f & y in dom f ) by A1, Th6; A4: R is_antisymmetric_in field R by RELAT_2:def_12; A5: [(f . y),(f . x)] in R by A2, Th6; A6: [(f . x),(f . y)] in R by A1, Th6; then ( f . x in field R & f . y in field R ) by RELAT_1:15; then f . x = f . y by A6, A5, A4, RELAT_2:def_4; hence x = y by A3, FUNCT_1:def_4; ::_thesis: verum end; end; registration let f be one-to-one Function; let R be transitive Relation; cluster(f * R) * (f ") -> transitive ; coherence (f * R) * (f ") is transitive proof let x, y, z be set ; :: according to RELAT_2:def_8,RELAT_2:def_16 ::_thesis: ( not x in field ((f * R) * (f ")) or not y in field ((f * R) * (f ")) or not z in field ((f * R) * (f ")) or not [x,y] in (f * R) * (f ") or not [y,z] in (f * R) * (f ") or [x,z] in (f * R) * (f ") ) assume that x in field ((f * R) * (f ")) and y in field ((f * R) * (f ")) and z in field ((f * R) * (f ")) ; ::_thesis: ( not [x,y] in (f * R) * (f ") or not [y,z] in (f * R) * (f ") or [x,z] in (f * R) * (f ") ) assume that A1: [x,y] in (f * R) * (f ") and A2: [y,z] in (f * R) * (f ") ; ::_thesis: [x,z] in (f * R) * (f ") A3: ( x in dom f & z in dom f ) by A1, A2, Th6; A4: [(f . y),(f . z)] in R by A2, Th6; then A5: f . z in field R by RELAT_1:15; A6: R is_transitive_in field R by RELAT_2:def_16; A7: [(f . x),(f . y)] in R by A1, Th6; then ( f . x in field R & f . y in field R ) by RELAT_1:15; then [(f . x),(f . z)] in R by A7, A4, A5, A6, RELAT_2:def_8; hence [x,z] in (f * R) * (f ") by A3, Th6; ::_thesis: verum end; end; theorem Th7: :: YELLOW21:7 for X being set for A being Ordinal st X,A are_equipotent holds ex R being Order of X st ( R well_orders X & order_type_of R = A ) proof let X be set ; ::_thesis: for A being Ordinal st X,A are_equipotent holds ex R being Order of X st ( R well_orders X & order_type_of R = A ) let A be Ordinal; ::_thesis: ( X,A are_equipotent implies ex R being Order of X st ( R well_orders X & order_type_of R = A ) ) given f being Function such that A1: f is one-to-one and A2: dom f = X and A3: rng f = A ; :: according to WELLORD2:def_4 ::_thesis: ex R being Order of X st ( R well_orders X & order_type_of R = A ) reconsider f = f as Function of X,A by A2, A3, FUNCT_2:2; reconsider g = f " as Function of A,X by A1, A3, FUNCT_2:25; A4: dom g = A by A1, A3, FUNCT_1:33; reconsider f9 = f as one-to-one Function by A1; A5: dom (RelIncl A) = A by ORDERS_1:14; rng (RelIncl A) = A by ORDERS_1:14; then A6: rng (f * (RelIncl A)) = A by A3, A5, RELAT_1:28; set R = (f * (RelIncl A)) * g; dom (f * (RelIncl A)) = X by A2, A3, A5, RELAT_1:27; then A7: dom ((f * (RelIncl A)) * g) = X by A4, A6, RELAT_1:27; rng g = X by A1, A2, FUNCT_1:33; then rng ((f * (RelIncl A)) * g) = X by A4, A6, RELAT_1:28; then A8: field ((f * (RelIncl A)) * g) = X \/ X by A7, RELAT_1:def_6 .= X ; reconsider R = (f * (RelIncl A)) * g as Relation of X ; (f9 * (RelIncl A)) * (f9 ") is_reflexive_in X by A8, RELAT_2:def_9; then reconsider R = R as Order of X by A7, PARTFUN1:def_2; A9: f is_isomorphism_of R, RelIncl A proof thus ( dom f = field R & rng f = field (RelIncl A) & f is one-to-one ) by A1, A2, A3, A8, WELLORD2:def_1; :: according to WELLORD1:def_7 ::_thesis: for b1, b2 being set holds ( ( not [b1,b2] in R or ( b1 in field R & b2 in field R & [(f . b1),(f . b2)] in RelIncl A ) ) & ( not b1 in field R or not b2 in field R or not [(f . b1),(f . b2)] in RelIncl A or [b1,b2] in R ) ) let a, b be set ; ::_thesis: ( ( not [a,b] in R or ( a in field R & b in field R & [(f . a),(f . b)] in RelIncl A ) ) & ( not a in field R or not b in field R or not [(f . a),(f . b)] in RelIncl A or [a,b] in R ) ) hereby ::_thesis: ( not a in field R or not b in field R or not [(f . a),(f . b)] in RelIncl A or [a,b] in R ) assume A10: [a,b] in R ; ::_thesis: ( a in field R & b in field R & [(f . a),(f . b)] in RelIncl A ) hence ( a in field R & b in field R ) by RELAT_1:15; ::_thesis: [(f . a),(f . b)] in RelIncl A consider x being set such that A11: [a,x] in f * (RelIncl A) and A12: [x,b] in g by A10, RELAT_1:def_8; A13: ( b = g . x & x in dom g ) by A12, FUNCT_1:1; consider y being set such that A14: [a,y] in f and A15: [y,x] in RelIncl A by A11, RELAT_1:def_8; y = f . a by A14, FUNCT_1:1; hence [(f . a),(f . b)] in RelIncl A by A1, A3, A15, A13, FUNCT_1:35; ::_thesis: verum end; assume that A16: a in field R and A17: b in field R and A18: [(f . a),(f . b)] in RelIncl A ; ::_thesis: [a,b] in R [a,(f . a)] in f by A2, A8, A16, FUNCT_1:1; then A19: [a,(f . b)] in f * (RelIncl A) by A18, RELAT_1:def_8; ( (f ") . (f . b) = b & f . b in A ) by A1, A2, A3, A8, A17, FUNCT_1:34, FUNCT_1:def_3; then [(f . b),b] in g by A4, FUNCT_1:1; hence [a,b] in R by A19, RELAT_1:def_8; ::_thesis: verum end; then f " is_isomorphism_of RelIncl A,R by WELLORD1:39; then ( R is connected & R is well_founded ) by WELLORD1:43; then A20: ( R is_connected_in X & R is_well_founded_in X ) by A8, RELAT_2:def_14, WELLORD1:3; take R ; ::_thesis: ( R well_orders X & order_type_of R = A ) A21: R is_antisymmetric_in X by A8, RELAT_2:def_12; ( R is_reflexive_in X & R is_transitive_in X ) by A8, RELAT_2:def_9, RELAT_2:def_16; hence R well_orders X by A21, A20, WELLORD1:def_5; ::_thesis: order_type_of R = A then A22: R is well-ordering by A8, WELLORD1:4; R, RelIncl A are_isomorphic by A9, WELLORD1:def_8; hence order_type_of R = A by A22, WELLORD2:def_2; ::_thesis: verum end; registration let X be non empty set ; cluster Relation-like X -defined X -valued well-ordering V16(X) quasi_total reflexive antisymmetric transitive upper-bounded for Element of bool [:X,X:]; existence ex b1 being Order of X st ( b1 is upper-bounded & b1 is well-ordering ) proof set x = the Element of X; A1: ( X \ { the Element of X}, card (X \ { the Element of X}) are_equipotent & { the Element of X},{(card (X \ { the Element of X}))} are_equipotent ) by CARD_1:28, CARD_1:def_2; A2: succ (card (X \ { the Element of X})) = (card (X \ { the Element of X})) \/ {(card (X \ { the Element of X}))} by ORDINAL1:def_1; not card (X \ { the Element of X}) in card (X \ { the Element of X}) ; then A3: {(card (X \ { the Element of X}))} misses card (X \ { the Element of X}) by ZFMISC_1:50; ( { the Element of X} misses X \ { the Element of X} & X = (X \ { the Element of X}) \/ { the Element of X} ) by Lm1, XBOOLE_1:79; then consider r being Order of X such that A4: r well_orders X and A5: order_type_of r = succ (card (X \ { the Element of X})) by A1, A3, A2, Th7, CARD_1:31; take r ; ::_thesis: ( r is upper-bounded & r is well-ordering ) A6: field r = X by ORDERS_1:15; then r is well-ordering by A4, WELLORD1:4; then r, RelIncl (order_type_of r) are_isomorphic by WELLORD2:def_2; then RelIncl (order_type_of r),r are_isomorphic by WELLORD1:40; then consider f being Function such that A7: f is_isomorphism_of RelIncl (order_type_of r),r by WELLORD1:def_8; A8: f is one-to-one by A7, WELLORD1:def_7; A9: rng f = X by A6, A7, WELLORD1:def_7; field (RelIncl (order_type_of r)) = order_type_of r by WELLORD2:def_1; then A10: dom f = order_type_of r by A7, WELLORD1:def_7; thus r is upper-bounded ::_thesis: r is well-ordering proof take a = f . (card (X \ { the Element of X})); :: according to YELLOW21:def_9 ::_thesis: for y being set st y in field r holds [y,a] in r let y be set ; ::_thesis: ( y in field r implies [y,a] in r ) A11: card (X \ { the Element of X}) in order_type_of r by A2, A5, ZFMISC_1:136; assume A12: y in field r ; ::_thesis: [y,a] in r then A13: (f ") . y in order_type_of r by A6, A8, A10, A9, FUNCT_1:32; then reconsider b = (f ") . y as Ordinal ; ( (f ") . y in card (X \ { the Element of X}) or (f ") . y = card (X \ { the Element of X}) ) by A2, A5, A13, ZFMISC_1:136; then b c= card (X \ { the Element of X}) by ORDINAL1:def_2; then [b,(card (X \ { the Element of X}))] in RelIncl (order_type_of r) by A13, A11, WELLORD2:def_1; then [(f . b),a] in r by A7, WELLORD1:def_7; hence [y,a] in r by A6, A8, A9, A12, FUNCT_1:35; ::_thesis: verum end; thus r is well-ordering by A4, A6, WELLORD1:4; ::_thesis: verum end; end; theorem Th8: :: YELLOW21:8 for P being non empty reflexive RelStr holds ( P is upper-bounded iff the InternalRel of P is upper-bounded ) proof let P be non empty reflexive RelStr ; ::_thesis: ( P is upper-bounded iff the InternalRel of P is upper-bounded ) the carrier of P \/ the carrier of P = the carrier of P ; then A1: field the InternalRel of P c= the carrier of P by RELSET_1:8; thus ( P is upper-bounded implies the InternalRel of P is upper-bounded ) ::_thesis: ( the InternalRel of P is upper-bounded implies P is upper-bounded ) proof given x being Element of P such that A2: x is_>=_than the carrier of P ; :: according to YELLOW_0:def_5 ::_thesis: the InternalRel of P is upper-bounded take x ; :: according to YELLOW21:def_9 ::_thesis: for y being set st y in field the InternalRel of P holds [y,x] in the InternalRel of P let y be set ; ::_thesis: ( y in field the InternalRel of P implies [y,x] in the InternalRel of P ) assume y in field the InternalRel of P ; ::_thesis: [y,x] in the InternalRel of P then reconsider y = y as Element of P by A1; x >= y by A2, LATTICE3:def_9; hence [y,x] in the InternalRel of P by ORDERS_2:def_5; ::_thesis: verum end; set y = the Element of P; given x being set such that A3: for y being set st y in field the InternalRel of P holds [y,x] in the InternalRel of P ; :: according to YELLOW21:def_9 ::_thesis: P is upper-bounded the Element of P <= the Element of P ; then [ the Element of P, the Element of P] in the InternalRel of P by ORDERS_2:def_5; then the Element of P in field the InternalRel of P by RELAT_1:15; then [ the Element of P,x] in the InternalRel of P by A3; then x in field the InternalRel of P by RELAT_1:15; then reconsider x = x as Element of P by A1; take x ; :: according to YELLOW_0:def_5 ::_thesis: the carrier of P is_<=_than x let y be Element of P; :: according to LATTICE3:def_9 ::_thesis: ( not y in the carrier of P or y <= x ) y <= y ; then [y,y] in the InternalRel of P by ORDERS_2:def_5; then y in field the InternalRel of P by RELAT_1:15; then [y,x] in the InternalRel of P by A3; hence ( not y in the carrier of P or y <= x ) by ORDERS_2:def_5; ::_thesis: verum end; theorem Th9: :: YELLOW21:9 for P being non empty upper-bounded Poset st the InternalRel of P is well-ordering holds ( P is connected & P is complete & P is continuous ) proof let P be non empty upper-bounded Poset; ::_thesis: ( the InternalRel of P is well-ordering implies ( P is connected & P is complete & P is continuous ) ) assume A1: the InternalRel of P is well-ordering ; ::_thesis: ( P is connected & P is complete & P is continuous ) A2: field the InternalRel of P = the carrier of P by ORDERS_1:15; thus A3: P is connected ::_thesis: ( P is complete & P is continuous ) proof let x, y be Element of P; :: according to WAYBEL_0:def_29 ::_thesis: ( x <= y or y <= x ) A4: ( x = y or x <> y ) ; ( the InternalRel of P is_connected_in the carrier of P & the InternalRel of P is_reflexive_in the carrier of P ) by A1, A2, RELAT_2:def_9, RELAT_2:def_14; then ( [x,y] in the InternalRel of P or [y,x] in the InternalRel of P ) by A4, RELAT_2:def_1, RELAT_2:def_6; hence ( x <= y or y <= x ) by ORDERS_2:def_5; ::_thesis: verum end; thus P is complete ::_thesis: P is continuous proof set y = the Element of P; let X be set ; :: according to LATTICE3:def_12 ::_thesis: ex b1 being Element of the carrier of P st ( X is_<=_than b1 & ( for b2 being Element of the carrier of P holds ( not X is_<=_than b2 or b1 <= b2 ) ) ) defpred S1[ set ] means for y being Element of P st y in X holds [y,\$1] in the InternalRel of P; consider Y being set such that A5: for x being set holds ( x in Y iff ( x in the carrier of P & S1[x] ) ) from XBOOLE_0:sch_1(); A6: Y c= the carrier of P proof let x be set ; :: according to TARSKI:def_3 ::_thesis: ( not x in Y or x in the carrier of P ) thus ( not x in Y or x in the carrier of P ) by A5; ::_thesis: verum end; the InternalRel of P is upper-bounded by Th8; then consider x being set such that A7: for y being set st y in field the InternalRel of P holds [y,x] in the InternalRel of P by Def9; [ the Element of P,x] in the InternalRel of P by A2, A7; then reconsider x = x as Element of P by A2, RELAT_1:15; for y being Element of P st y in X holds [y,x] in the InternalRel of P by A2, A7; then x in Y by A5; then consider a being set such that A8: a in Y and A9: for b being set st b in Y holds [a,b] in the InternalRel of P by A1, A2, A6, WELLORD1:6; reconsider a = a as Element of P by A6, A8; take a ; ::_thesis: ( X is_<=_than a & ( for b1 being Element of the carrier of P holds ( not X is_<=_than b1 or a <= b1 ) ) ) hereby :: according to LATTICE3:def_9 ::_thesis: for b1 being Element of the carrier of P holds ( not X is_<=_than b1 or a <= b1 ) let y be Element of P; ::_thesis: ( y in X implies y <= a ) assume y in X ; ::_thesis: y <= a then [y,a] in the InternalRel of P by A5, A8; hence y <= a by ORDERS_2:def_5; ::_thesis: verum end; let b be Element of P; ::_thesis: ( not X is_<=_than b or a <= b ) assume A10: for c being Element of P st c in X holds c <= b ; :: according to LATTICE3:def_9 ::_thesis: a <= b now__::_thesis:_for_c_being_Element_of_P_st_c_in_X_holds_ [c,b]_in_the_InternalRel_of_P let c be Element of P; ::_thesis: ( c in X implies [c,b] in the InternalRel of P ) assume c in X ; ::_thesis: [c,b] in the InternalRel of P then c <= b by A10; hence [c,b] in the InternalRel of P by ORDERS_2:def_5; ::_thesis: verum end; then b in Y by A5; then [a,b] in the InternalRel of P by A9; hence a <= b by ORDERS_2:def_5; ::_thesis: verum end; hence P is continuous by A3; ::_thesis: verum end; theorem Th10: :: YELLOW21:10 for P being non empty upper-bounded Poset st the InternalRel of P is well-ordering holds for x, y being Element of P st y < x holds ex z being Element of P st ( z is compact & y <= z & z <= x ) proof let P be non empty upper-bounded Poset; ::_thesis: ( the InternalRel of P is well-ordering implies for x, y being Element of P st y < x holds ex z being Element of P st ( z is compact & y <= z & z <= x ) ) set R = the InternalRel of P; set A = order_type_of the InternalRel of P; A1: field (RelIncl (order_type_of the InternalRel of P)) = order_type_of the InternalRel of P by WELLORD2:def_1; assume A2: the InternalRel of P is well-ordering ; ::_thesis: for x, y being Element of P st y < x holds ex z being Element of P st ( z is compact & y <= z & z <= x ) then reconsider L = P as complete Chain by Th9; let x, y be Element of P; ::_thesis: ( y < x implies ex z being Element of P st ( z is compact & y <= z & z <= x ) ) the InternalRel of P, RelIncl (order_type_of the InternalRel of P) are_isomorphic by A2, WELLORD2:def_2; then consider f being Function such that A3: f is_isomorphism_of the InternalRel of P, RelIncl (order_type_of the InternalRel of P) by WELLORD1:def_8; assume A4: y < x ; ::_thesis: ex z being Element of P st ( z is compact & y <= z & z <= x ) then y <= x by ORDERS_2:def_6; then A5: [y,x] in the InternalRel of P by ORDERS_2:def_5; then A6: [(f . y),(f . x)] in RelIncl (order_type_of the InternalRel of P) by A3, A4, WELLORD1:36; then A7: f . x in order_type_of the InternalRel of P by A1, RELAT_1:15; A8: f . x <> f . y by A3, A4, A5, WELLORD1:36; A9: f . y in order_type_of the InternalRel of P by A6, A1, RELAT_1:15; then reconsider a = f . x, b = f . y as Ordinal by A7; b c= a by A6, A7, A9, WELLORD2:def_1; then b c< a by A8, XBOOLE_0:def_8; then b in a by ORDINAL1:11; then A10: succ b c= a by ORDINAL1:21; then A11: succ b in order_type_of the InternalRel of P by A7, ORDINAL1:12; then A12: [(succ b),(f . x)] in RelIncl (order_type_of the InternalRel of P) by A7, A10, WELLORD2:def_1; A13: b c= succ b by ORDINAL3:1; rng f = order_type_of the InternalRel of P by A3, A1, WELLORD1:def_7; then consider z being set such that A14: z in dom f and A15: succ b = f . z by A11, FUNCT_1:def_3; A16: field the InternalRel of P = the carrier of P by ORDERS_1:15; then reconsider z = z as Element of P by A3, A14, WELLORD1:def_7; take z ; ::_thesis: ( z is compact & y <= z & z <= x ) A17: dom f = field the InternalRel of P by A3, WELLORD1:def_7; thus z is compact ::_thesis: ( y <= z & z <= x ) proof let D be non empty directed Subset of P; :: according to WAYBEL_3:def_1,WAYBEL_3:def_2 ::_thesis: ( not z <= sup D or ex b1 being Element of the carrier of P st ( b1 in D & z <= b1 ) ) assume that A18: z <= sup D and A19: for d being Element of P st d in D holds not z <= d ; ::_thesis: contradiction A20: L is complete ; D is_<=_than y proof let c be Element of P; :: according to LATTICE3:def_9 ::_thesis: ( not c in D or c <= y ) A21: f is one-to-one by A3, WELLORD1:def_7; assume A22: c in D ; ::_thesis: c <= y then not z <= c by A19; then z >= c by A20, WAYBEL_0:def_29; then [c,z] in the InternalRel of P by ORDERS_2:def_5; then A23: [(f . c),(succ b)] in RelIncl (order_type_of the InternalRel of P) by A3, A15, WELLORD1:def_7; then A24: f . c in order_type_of the InternalRel of P by A1, RELAT_1:15; then reconsider fc = f . c as Ordinal ; A25: fc c= succ b by A11, A23, A24, WELLORD2:def_1; c <> z by A19, A22; then fc <> succ b by A15, A16, A17, A21, FUNCT_1:def_4; then fc c< succ b by A25, XBOOLE_0:def_8; then fc in succ b by ORDINAL1:11; then fc c= b by ORDINAL1:22; then [fc,b] in RelIncl (order_type_of the InternalRel of P) by A9, A24, WELLORD2:def_1; hence [c,y] in the InternalRel of P by A3, A16, WELLORD1:def_7; :: according to ORDERS_2:def_5 ::_thesis: verum end; then sup D <= y by A20, YELLOW_0:32; then z <= y by A18, YELLOW_0:def_2; then [z,y] in the InternalRel of P by ORDERS_2:def_5; then [(succ b),b] in RelIncl (order_type_of the InternalRel of P) by A3, A15, WELLORD1:def_7; then succ b c= b by A9, A11, WELLORD2:def_1; then b = succ b by A13, XBOOLE_0:def_10; hence contradiction by ORDINAL1:9; ::_thesis: verum end; [(f . y),(succ b)] in RelIncl (order_type_of the InternalRel of P) by A9, A13, A11, WELLORD2:def_1; hence ( [y,z] in the InternalRel of P & [z,x] in the InternalRel of P ) by A3, A15, A16, A12, WELLORD1:def_7; :: according to ORDERS_2:def_5 ::_thesis: verum end; theorem Th11: :: YELLOW21:11 for P being non empty upper-bounded Poset st the InternalRel of P is well-ordering holds P is algebraic proof let P be non empty upper-bounded Poset; ::_thesis: ( the InternalRel of P is well-ordering implies P is algebraic ) assume A1: the InternalRel of P is well-ordering ; ::_thesis: P is algebraic then reconsider L = P as non empty complete connected continuous Poset by Th9; now__::_thesis:_for_x,_y_being_Element_of_L_st_x_<<_y_holds_ ex_z_being_Element_of_L_st_ (_z_in_the_carrier_of_(CompactSublatt_L)_&_x_<=_z_&_z_<=_y_) let x, y be Element of L; ::_thesis: ( x << y implies ex z being Element of L st ( z in the carrier of (CompactSublatt L) & x <= z & z <= y ) ) assume x << y ; ::_thesis: ex z being Element of L st ( z in the carrier of (CompactSublatt L) & x <= z & z <= y ) then ( ( x is compact & x <= x & x <= y ) or x < y ) by WAYBEL_3:1, WAYBEL_3:14; then consider z being Element of L such that A2: z is compact and A3: ( x <= z & z <= y ) by A1, Th10; take z = z; ::_thesis: ( z in the carrier of (CompactSublatt L) & x <= z & z <= y ) thus z in the carrier of (CompactSublatt L) by A2, WAYBEL_8:def_1; ::_thesis: ( x <= z & z <= y ) thus ( x <= z & z <= y ) by A3; ::_thesis: verum end; hence P is algebraic by WAYBEL_8:7; ::_thesis: verum end; registration let X be non empty set ; let R be well-ordering upper-bounded Order of X; cluster RelStr(# X,R #) -> algebraic complete connected continuous ; coherence ( RelStr(# X,R #) is complete & RelStr(# X,R #) is connected & RelStr(# X,R #) is continuous & RelStr(# X,R #) is algebraic ) proof RelStr(# X,R #) is upper-bounded by Th8; hence ( RelStr(# X,R #) is complete & RelStr(# X,R #) is connected & RelStr(# X,R #) is continuous & RelStr(# X,R #) is algebraic ) by Th9, Th11; ::_thesis: verum end; end; definition defpred S1[ LATTICE, LATTICE, Function of \$1,\$2] means \$3 is directed-sups-preserving ; defpred S2[ LATTICE] means \$1 is complete ; let W be non empty set ; given w being Element of W such that A1: not w is empty ; funcW -UPS_category -> strict lattice-wise category means :Def10: :: YELLOW21:def 10 ( ( for x being LATTICE holds ( x is object of it iff ( x is strict & x is complete & the carrier of x in W ) ) ) & ( for a, b being object of it for f being monotone Function of (latt a),(latt b) holds ( f in <^a,b^> iff f is directed-sups-preserving ) ) ); existence ex b1 being strict lattice-wise category st ( ( for x being LATTICE holds ( x is object of b1 iff ( x is strict & x is complete & the carrier of x in W ) ) ) & ( for a, b being object of b1 for f being monotone Function of (latt a),(latt b) holds ( f in <^a,b^> iff f is directed-sups-preserving ) ) ) proof reconsider w = w as non empty set by A1; set r = the well-ordering upper-bounded Order of w; A2: for a being LATTICE st S2[a] holds S1[a,a, id a] ; RelStr(# w, the well-ordering upper-bounded Order of w #) is complete ; then A3: ex x being strict LATTICE st ( S2[x] & the carrier of x in W ) ; A4: for a, b, c being LATTICE st S2[a] & S2[b] & S2[c] holds for f being Function of a,b for g being Function of b,c st S1[a,b,f] & S1[b,c,g] holds S1[a,c,g * f] by WAYBEL20:28; thus ex It being strict lattice-wise category st ( ( for x being LATTICE holds ( x is object of It iff ( x is strict & S2[x] & the carrier of x in W ) ) ) & ( for a, b being object of It for f being monotone Function of (latt a),(latt b) holds ( f in <^a,b^> iff S1[ latt a, latt b,f] ) ) ) from YELLOW21:sch_3(A3, A4, A2); ::_thesis: verum end; correctness uniqueness for b1, b2 being strict lattice-wise category st ( for x being LATTICE holds ( x is object of b1 iff ( x is strict & x is complete & the carrier of x in W ) ) ) & ( for a, b being object of b1 for f being monotone Function of (latt a),(latt b) holds ( f in <^a,b^> iff f is directed-sups-preserving ) ) & ( for x being LATTICE holds ( x is object of b2 iff ( x is strict & x is complete & the carrier of x in W ) ) ) & ( for a, b being object of b2 for f being monotone Function of (latt a),(latt b) holds ( f in <^a,b^> iff f is directed-sups-preserving ) ) holds b1 = b2; proof reconsider w = w as non empty set by A1; let C1, C2 be strict lattice-wise category; ::_thesis: ( ( for x being LATTICE holds ( x is object of C1 iff ( x is strict & x is complete & the carrier of x in W ) ) ) & ( for a, b being object of C1 for f being monotone Function of (latt a),(latt b) holds ( f in <^a,b^> iff f is directed-sups-preserving ) ) & ( for x being LATTICE holds ( x is object of C2 iff ( x is strict & x is complete & the carrier of x in W ) ) ) & ( for a, b being object of C2 for f being monotone Function of (latt a),(latt b) holds ( f in <^a,b^> iff f is directed-sups-preserving ) ) implies C1 = C2 ) assume that A5: for x being LATTICE holds ( x is object of C1 iff ( x is strict & S2[x] & the carrier of x in W ) ) and A6: for a, b being object of C1 for f being monotone Function of (latt a),(latt b) holds ( f in <^a,b^> iff f is directed-sups-preserving ) and A7: for x being LATTICE holds ( x is object of C2 iff ( x is strict & S2[x] & the carrier of x in W ) ) and A8: for a, b being object of C2 for f being monotone Function of (latt a),(latt b) holds ( f in <^a,b^> iff f is directed-sups-preserving ) ; ::_thesis: C1 = C2 defpred S3[ set , set , set ] means ex L1, L2 being LATTICE ex f being Function of L1,L2 st ( \$1 = L1 & \$2 = L2 & \$3 = f & f is directed-sups-preserving ); A9: now__::_thesis:_for_a,_b_being_object_of_C1 for_f_being_monotone_Function_of_(latt_a),(latt_b)_holds_ (_f_in_<^a,b^>_iff_S3[a,b,f]_) let a, b be object of C1; ::_thesis: for f being monotone Function of (latt a),(latt b) holds ( f in <^a,b^> iff S3[a,b,f] ) let f be monotone Function of (latt a),(latt b); ::_thesis: ( f in <^a,b^> iff S3[a,b,f] ) ( f in <^a,b^> iff f is directed-sups-preserving ) by A6; hence ( f in <^a,b^> iff S3[a,b,f] ) ; ::_thesis: verum end; A10: now__::_thesis:_for_a,_b_being_object_of_C2 for_f_being_monotone_Function_of_(latt_a),(latt_b)_holds_ (_f_in_<^a,b^>_iff_S3[a,b,f]_) let a, b be object of C2; ::_thesis: for f being monotone Function of (latt a),(latt b) holds ( f in <^a,b^> iff S3[a,b,f] ) let f be monotone Function of (latt a),(latt b); ::_thesis: ( f in <^a,b^> iff S3[a,b,f] ) ( f in <^a,b^> iff f is directed-sups-preserving ) by A8; hence ( f in <^a,b^> iff S3[a,b,f] ) ; ::_thesis: verum end; for C1, C2 being lattice-wise category st ( for x being LATTICE holds ( x is object of C1 iff ( x is strict & S2[x] & the carrier of x in W ) ) ) & ( for a, b being object of C1 for f being monotone Function of (latt a),(latt b) holds ( f in <^a,b^> iff S3[a,b,f] ) ) & ( for x being LATTICE holds ( x is object of C2 iff ( x is strict & S2[x] & the carrier of x in W ) ) ) & ( for a, b being object of C2 for f being monotone Function of (latt a),(latt b) holds ( f in <^a,b^> iff S3[a,b,f] ) ) holds AltCatStr(# the carrier of C1, the Arrows of C1, the Comp of C1 #) = AltCatStr(# the carrier of C2, the Arrows of C2, the Comp of C2 #) from YELLOW21:sch_5(); hence C1 = C2 by A5, A7, A9, A10; ::_thesis: verum end; end; :: deftheorem Def10 defines -UPS_category YELLOW21:def_10_:_ for W being non empty set st not for w being Element of W holds w is empty holds for b2 being strict lattice-wise category holds ( b2 = W -UPS_category iff ( ( for x being LATTICE holds ( x is object of b2 iff ( x is strict & x is complete & the carrier of x in W ) ) ) & ( for a, b being object of b2 for f being monotone Function of (latt a),(latt b) holds ( f in <^a,b^> iff f is directed-sups-preserving ) ) ) ); registration let W be with_non-empty_element set ; clusterW -UPS_category -> strict lattice-wise with_complete_lattices with_all_isomorphisms ; coherence ( W -UPS_category is with_complete_lattices & W -UPS_category is with_all_isomorphisms ) proof set C = W -UPS_category ; thus W -UPS_category is lattice-wise ; :: according to YELLOW21:def_5 ::_thesis: ( ( for a being object of (W -UPS_category) holds a is complete LATTICE ) & W -UPS_category is with_all_isomorphisms ) A1: ex w being non empty set st w in W by SETFAM_1:def_10; hereby ::_thesis: W -UPS_category is with_all_isomorphisms let a be object of (W -UPS_category); ::_thesis: a is complete LATTICE a = latt a ; hence a is complete LATTICE by A1, Def10; ::_thesis: verum end; let a, b be object of (W -UPS_category); :: according to YELLOW21:def_8 ::_thesis: for f being Function of (latt a),(latt b) st f is isomorphic holds f in <^a,b^> let f be Function of (latt a),(latt b); ::_thesis: ( f is isomorphic implies f in <^a,b^> ) reconsider S = latt a, T = latt b as complete LATTICE by A1, Def10; assume f is isomorphic ; ::_thesis: f in <^a,b^> then f is sups-preserving Function of S,T by WAYBEL13:20; hence f in <^a,b^> by A1, Def10; ::_thesis: verum end; end; theorem Th12: :: YELLOW21:12 for W being with_non-empty_element set holds the carrier of (W -UPS_category) c= POSETS W proof let W be with_non-empty_element set ; ::_thesis: the carrier of (W -UPS_category) c= POSETS W let x be set ; :: according to TARSKI:def_3 ::_thesis: ( not x in the carrier of (W -UPS_category) or x in POSETS W ) assume x in the carrier of (W -UPS_category) ; ::_thesis: x in POSETS W then reconsider x = x as object of (W -UPS_category) ; A1: ex w being non empty set st w in W by SETFAM_1:def_10; then A2: the carrier of (latt x) in W by Def10; latt x = x ; then x is strict Poset by A1, Def10; hence x in POSETS W by A2, Def2; ::_thesis: verum end; theorem Th13: :: YELLOW21:13 for W being with_non-empty_element set for x being set holds ( x is object of (W -UPS_category) iff ( x is complete LATTICE & x in POSETS W ) ) proof let W be with_non-empty_element set ; ::_thesis: for x being set holds ( x is object of (W -UPS_category) iff ( x is complete LATTICE & x in POSETS W ) ) let x be set ; ::_thesis: ( x is object of (W -UPS_category) iff ( x is complete LATTICE & x in POSETS W ) ) hereby ::_thesis: ( x is complete LATTICE & x in POSETS W implies x is object of (W -UPS_category) ) assume x is object of (W -UPS_category) ; ::_thesis: ( x is complete LATTICE & x in POSETS W ) then reconsider a = x as object of (W -UPS_category) ; latt a = x ; hence x is complete LATTICE ; ::_thesis: x in POSETS W ( a in the carrier of (W -UPS_category) & the carrier of (W -UPS_category) c= POSETS W ) by Th12; hence x in POSETS W ; ::_thesis: verum end; assume x is complete LATTICE ; ::_thesis: ( not x in POSETS W or x is object of (W -UPS_category) ) then reconsider L = x as complete LATTICE ; assume x in POSETS W ; ::_thesis: x is object of (W -UPS_category) then A1: ( the carrier of (L as_1-sorted) in W & L is strict ) by Def2; L as_1-sorted = L by Def1; hence x is object of (W -UPS_category) by A1, Def10; ::_thesis: verum end; theorem Th14: :: YELLOW21:14 for W being with_non-empty_element set for L being LATTICE st the carrier of L in W holds ( L is object of (W -UPS_category) iff ( L is strict & L is complete ) ) proof let W be with_non-empty_element set ; ::_thesis: for L being LATTICE st the carrier of L in W holds ( L is object of (W -UPS_category) iff ( L is strict & L is complete ) ) let L be LATTICE; ::_thesis: ( the carrier of L in W implies ( L is object of (W -UPS_category) iff ( L is strict & L is complete ) ) ) assume A1: the carrier of L in W ; ::_thesis: ( L is object of (W -UPS_category) iff ( L is strict & L is complete ) ) L as_1-sorted = L by Def1; then ( L in POSETS W iff L is strict ) by A1, Def2; hence ( L is object of (W -UPS_category) iff ( L is strict & L is complete ) ) by Th13; ::_thesis: verum end; theorem Th15: :: YELLOW21:15 for W being with_non-empty_element set for a, b being object of (W -UPS_category) for f being set holds ( f in <^a,b^> iff f is directed-sups-preserving Function of (latt a),(latt b) ) proof let W be with_non-empty_element set ; ::_thesis: for a, b being object of (W -UPS_category) for f being set holds ( f in <^a,b^> iff f is directed-sups-preserving Function of (latt a),(latt b) ) let a, b be object of (W -UPS_category); ::_thesis: for f being set holds ( f in <^a,b^> iff f is directed-sups-preserving Function of (latt a),(latt b) ) let f be set ; ::_thesis: ( f in <^a,b^> iff f is directed-sups-preserving Function of (latt a),(latt b) ) A1: ex w being non empty set st w in W by SETFAM_1:def_10; hereby ::_thesis: ( f is directed-sups-preserving Function of (latt a),(latt b) implies f in <^a,b^> ) assume A2: f in <^a,b^> ; ::_thesis: f is directed-sups-preserving Function of (latt a),(latt b) then reconsider g = f as Morphism of a,b ; f = @ g by A2, Def7; hence f is directed-sups-preserving Function of (latt a),(latt b) by A1, A2, Def10; ::_thesis: verum end; thus ( f is directed-sups-preserving Function of (latt a),(latt b) implies f in <^a,b^> ) by A1, Def10; ::_thesis: verum end; registration let W be with_non-empty_element set ; let a, b be object of (W -UPS_category); cluster<^a,b^> -> non empty ; coherence not <^a,b^> is empty proof set f = the directed-sups-preserving Function of (latt a),(latt b); the directed-sups-preserving Function of (latt a),(latt b) in <^a,b^> by Th15; hence not <^a,b^> is empty ; ::_thesis: verum end; end; begin registration let A be set-id-inheriting category; cluster non empty transitive id-inheriting -> non empty set-id-inheriting for SubCatStr of A; coherence for b1 being non empty subcategory of A holds b1 is set-id-inheriting proof let B be non empty subcategory of A; ::_thesis: B is set-id-inheriting let b be object of B; :: according to YELLOW18:def_10 ::_thesis: idm b = id (B -carrier_of b) ( b in the carrier of B & the carrier of B c= the carrier of A ) by ALTCAT_2:def_11; then reconsider a = b as object of A ; thus idm b = idm a by ALTCAT_2:34 .= id (the_carrier_of a) by YELLOW18:def_10 .= id (the_carrier_of b) by ALTCAT_2:34 ; ::_thesis: verum end; end; registration let A be para-functional category; cluster non empty transitive id-inheriting -> non empty para-functional for SubCatStr of A; coherence for b1 being non empty subcategory of A holds b1 is para-functional proof let B be non empty subcategory of A; ::_thesis: B is para-functional consider F being ManySortedSet of A such that A1: for a1, a2 being object of A holds <^a1,a2^> c= Funcs ((F . a1),(F . a2)) by YELLOW18:def_7; set G = F | the carrier of B; A2: the carrier of B c= the carrier of A by ALTCAT_2:def_11; dom F = the carrier of A by PARTFUN1:def_2; then dom (F | the carrier of B) = the carrier of B by A2, RELAT_1:62; then reconsider G = F | the carrier of B as ManySortedSet of B by PARTFUN1:def_2, RELAT_1:def_18; take G ; :: according to YELLOW18:def_7 ::_thesis: for b1, b2 being Element of the carrier of B holds <^b1,b2^> c= Funcs ((G . b1),(G . b2)) let a1, a2 be object of B; ::_thesis: <^a1,a2^> c= Funcs ((G . a1),(G . a2)) ( a1 in the carrier of B & a2 in the carrier of B ) ; then reconsider b1 = a1, b2 = a2 as object of A by A2; ( F . a1 = G . a1 & F . a2 = G . a2 ) by FUNCT_1:49; then ( <^a1,a2^> c= <^b1,b2^> & <^b1,b2^> c= Funcs ((G . a1),(G . a2)) ) by A1, ALTCAT_2:31; hence <^a1,a2^> c= Funcs ((G . a1),(G . a2)) by XBOOLE_1:1; ::_thesis: verum end; end; registration let A be semi-functional category; cluster non empty transitive -> non empty transitive semi-functional for SubCatStr of A; coherence for b1 being non empty transitive SubCatStr of A holds b1 is semi-functional proof let B be non empty transitive SubCatStr of A; ::_thesis: B is semi-functional let b1, b2, b3 be object of B; :: according to ALTCAT_1:def_12 ::_thesis: ( <^b1,b2^> = {} or <^b2,b3^> = {} or <^b1,b3^> = {} or for b1 being Element of <^b1,b2^> for b2 being Element of <^b2,b3^> for b3, b4 being set holds ( not b1 = b3 or not b2 = b4 or b2 * b1 = b3 * b4 ) ) assume that A1: <^b1,b2^> <> {} and A2: <^b2,b3^> <> {} and A3: <^b1,b3^> <> {} ; ::_thesis: for b1 being Element of <^b1,b2^> for b2 being Element of <^b2,b3^> for b3, b4 being set holds ( not b1 = b3 or not b2 = b4 or b2 * b1 = b3 * b4 ) reconsider a1 = b1, a2 = b2, a3 = b3 as object of A by ALTCAT_2:29; A4: ( <^a1,a2^> <> {} & <^a2,a3^> <> {} ) by A1, A2, ALTCAT_2:31, XBOOLE_1:3; let f1 be Morphism of b1,b2; ::_thesis: for b1 being Element of <^b2,b3^> for b2, b3 being set holds ( not f1 = b2 or not b1 = b3 or b1 * f1 = b2 * b3 ) let f2 be Morphism of b2,b3; ::_thesis: for b1, b2 being set holds ( not f1 = b1 or not f2 = b2 or f2 * f1 = b1 * b2 ) reconsider g2 = f2 as Morphism of a2,a3 by A2, ALTCAT_2:33; reconsider g1 = f1 as Morphism of a1,a2 by A1, ALTCAT_2:33; A5: <^a1,a3^> <> {} by A3, ALTCAT_2:31, XBOOLE_1:3; let f9, g9 be Function; ::_thesis: ( not f1 = f9 or not f2 = g9 or f2 * f1 = f9 * g9 ) assume ( f1 = f9 & f2 = g9 ) ; ::_thesis: f2 * f1 = f9 * g9 then g2 * g1 = g9 * f9 by A4, A5, ALTCAT_1:def_12; hence f2 * f1 = f9 * g9 by A1, A2, ALTCAT_2:32; ::_thesis: verum end; end; registration let A be carrier-underlaid category; cluster non empty transitive id-inheriting -> non empty carrier-underlaid for SubCatStr of A; coherence for b1 being non empty subcategory of A holds b1 is carrier-underlaid proof let B be non empty subcategory of A; ::_thesis: B is carrier-underlaid let b be object of B; :: according to YELLOW21:def_3 ::_thesis: ex S being 1-sorted st ( b = S & the_carrier_of b = the carrier of S ) reconsider a = b as object of A by ALTCAT_2:29; consider S being 1-sorted such that A1: a = S and A2: the_carrier_of a = the carrier of S by Def3; take S ; ::_thesis: ( b = S & the_carrier_of b = the carrier of S ) thus b = S by A1; ::_thesis: the_carrier_of b = the carrier of S thus the_carrier_of b = the carrier of S by A2, ALTCAT_2:34; ::_thesis: verum end; end; registration let A be lattice-wise category; cluster non empty transitive id-inheriting -> non empty lattice-wise for SubCatStr of A; coherence for b1 being non empty subcategory of A holds b1 is lattice-wise proof let B be non empty subcategory of A; ::_thesis: B is lattice-wise thus ( B is semi-functional & B is set-id-inheriting ) ; :: according to YELLOW21:def_4 ::_thesis: ( ( for a being object of B holds a is LATTICE ) & ( for a, b being object of B for A, B being LATTICE st A = a & B = b holds <^a,b^> c= MonFuncs (A,B) ) ) hereby ::_thesis: for a, b being object of B for A, B being LATTICE st A = a & B = b holds <^a,b^> c= MonFuncs (A,B) let b be object of B; ::_thesis: b is LATTICE reconsider a = b as object of A by ALTCAT_2:29; a is LATTICE by Def4; hence b is LATTICE ; ::_thesis: verum end; let a, b be object of B; ::_thesis: for A, B being LATTICE st A = a & B = b holds <^a,b^> c= MonFuncs (A,B) reconsider a9 = a, b9 = b as object of A by ALTCAT_2:29; let A, B be LATTICE; ::_thesis: ( A = a & B = b implies <^a,b^> c= MonFuncs (A,B) ) assume ( A = a & B = b ) ; ::_thesis: <^a,b^> c= MonFuncs (A,B) then ( <^a,b^> c= <^a9,b9^> & <^a9,b9^> c= MonFuncs (A,B) ) by Def4, ALTCAT_2:31; hence <^a,b^> c= MonFuncs (A,B) by XBOOLE_1:1; ::_thesis: verum end; end; registration let A be lattice-wise with_all_isomorphisms category; cluster non empty transitive full id-inheriting -> non empty with_all_isomorphisms for SubCatStr of A; coherence for b1 being non empty subcategory of A st b1 is full holds b1 is with_all_isomorphisms proof let B be non empty subcategory of A; ::_thesis: ( B is full implies B is with_all_isomorphisms ) assume A1: B is full ; ::_thesis: B is with_all_isomorphisms let a, b be object of B; :: according to YELLOW21:def_8 ::_thesis: for f being Function of (latt a),(latt b) st f is isomorphic holds f in <^a,b^> let f be Function of (latt a),(latt b); ::_thesis: ( f is isomorphic implies f in <^a,b^> ) reconsider a9 = a, b9 = b as object of A by ALTCAT_2:29; assume f is isomorphic ; ::_thesis: f in <^a,b^> then f in <^a9,b9^> by Def8; hence f in <^a,b^> by A1, ALTCAT_2:28; ::_thesis: verum end; end; registration let A be with_complete_lattices category; cluster non empty transitive id-inheriting -> non empty with_complete_lattices for SubCatStr of A; coherence for b1 being non empty subcategory of A holds b1 is with_complete_lattices proof let B be non empty subcategory of A; ::_thesis: B is with_complete_lattices thus B is lattice-wise ; :: according to YELLOW21:def_5 ::_thesis: for a being object of B holds a is complete LATTICE let b be object of B; ::_thesis: b is complete LATTICE reconsider a = b as object of A by ALTCAT_2:29; a is complete LATTICE by Def5; hence b is complete LATTICE ; ::_thesis: verum end; end; definition let W be with_non-empty_element set ; defpred S1[ object of (W -UPS_category)] means latt \$1 is continuous ; consider a being non empty set such that A1: a in W by SETFAM_1:def_10; set r = the well-ordering upper-bounded Order of a; set b = RelStr(# a, the well-ordering upper-bounded Order of a #); funcW -CONT_category -> non empty strict full subcategory of W -UPS_category means :Def11: :: YELLOW21:def 11 for a being object of (W -UPS_category) holds ( a is object of it iff latt a is continuous ); existence ex b1 being non empty strict full subcategory of W -UPS_category st for a being object of (W -UPS_category) holds ( a is object of b1 iff latt a is continuous ) proof reconsider b = RelStr(# a, the well-ordering upper-bounded Order of a #) as object of (W -UPS_category) by A1, Def10; b = latt b ; then A2: ex b being object of (W -UPS_category) st S1[b] ; thus ex C being non empty strict full subcategory of W -UPS_category st for a being object of (W -UPS_category) holds ( a is object of C iff S1[a] ) from YELLOW20:sch_2(A2); ::_thesis: verum end; correctness uniqueness for b1, b2 being non empty strict full subcategory of W -UPS_category st ( for a being object of (W -UPS_category) holds ( a is object of b1 iff latt a is continuous ) ) & ( for a being object of (W -UPS_category) holds ( a is object of b2 iff latt a is continuous ) ) holds b1 = b2; proof let B1, B2 be non empty strict full subcategory of W -UPS_category ; ::_thesis: ( ( for a being object of (W -UPS_category) holds ( a is object of B1 iff latt a is continuous ) ) & ( for a being object of (W -UPS_category) holds ( a is object of B2 iff latt a is continuous ) ) implies B1 = B2 ) assume that A3: for a being object of (W -UPS_category) holds ( a is object of B1 iff S1[a] ) and A4: for a being object of (W -UPS_category) holds ( a is object of B2 iff S1[a] ) ; ::_thesis: B1 = B2 AltCatStr(# the carrier of B1, the Arrows of B1, the Comp of B1 #) = AltCatStr(# the carrier of B2, the Arrows of B2, the Comp of B2 #) from YELLOW20:sch_3(A3, A4); hence B1 = B2 ; ::_thesis: verum end; end; :: deftheorem Def11 defines -CONT_category YELLOW21:def_11_:_ for W being with_non-empty_element set for b2 being non empty strict full subcategory of W -UPS_category holds ( b2 = W -CONT_category iff for a being object of (W -UPS_category) holds ( a is object of b2 iff latt a is continuous ) ); definition let W be with_non-empty_element set ; defpred S1[ object of (W -CONT_category)] means latt \$1 is algebraic ; consider a being non empty set such that A1: a in W by SETFAM_1:def_10; set r = the well-ordering upper-bounded Order of a; set b = RelStr(# a, the well-ordering upper-bounded Order of a #); funcW -ALG_category -> non empty strict full subcategory of W -CONT_category means :Def12: :: YELLOW21:def 12 for a being object of (W -CONT_category) holds ( a is object of it iff latt a is algebraic ); existence ex b1 being non empty strict full subcategory of W -CONT_category st for a being object of (W -CONT_category) holds ( a is object of b1 iff latt a is algebraic ) proof reconsider b = RelStr(# a, the well-ordering upper-bounded Order of a #) as object of (W -UPS_category) by A1, Def10; b = latt b ; then reconsider b = b as object of (W -CONT_category) by Def11; b = latt b ; then A2: ex b being object of (W -CONT_category) st S1[b] ; thus ex C being non empty strict full subcategory of W -CONT_category st for a being object of (W -CONT_category) holds ( a is object of C iff S1[a] ) from YELLOW20:sch_2(A2); ::_thesis: verum end; correctness uniqueness for b1, b2 being non empty strict full subcategory of W -CONT_category st ( for a being object of (W -CONT_category) holds ( a is object of b1 iff latt a is algebraic ) ) & ( for a being object of (W -CONT_category) holds ( a is object of b2 iff latt a is algebraic ) ) holds b1 = b2; proof let B1, B2 be non empty strict full subcategory of W -CONT_category ; ::_thesis: ( ( for a being object of (W -CONT_category) holds ( a is object of B1 iff latt a is algebraic ) ) & ( for a being object of (W -CONT_category) holds ( a is object of B2 iff latt a is algebraic ) ) implies B1 = B2 ) assume that A3: for a being object of (W -CONT_category) holds ( a is object of B1 iff S1[a] ) and A4: for a being object of (W -CONT_category) holds ( a is object of B2 iff S1[a] ) ; ::_thesis: B1 = B2 AltCatStr(# the carrier of B1, the Arrows of B1, the Comp of B1 #) = AltCatStr(# the carrier of B2, the Arrows of B2, the Comp of B2 #) from YELLOW20:sch_3(A3, A4); hence B1 = B2 ; ::_thesis: verum end; end; :: deftheorem Def12 defines -ALG_category YELLOW21:def_12_:_ for W being with_non-empty_element set for b2 being non empty strict full subcategory of W -CONT_category holds ( b2 = W -ALG_category iff for a being object of (W -CONT_category) holds ( a is object of b2 iff latt a is algebraic ) ); theorem Th16: :: YELLOW21:16 for W being with_non-empty_element set for L being LATTICE st the carrier of L in W holds ( L is object of (W -CONT_category) iff ( L is strict & L is complete & L is continuous ) ) proof let W be with_non-empty_element set ; ::_thesis: for L being LATTICE st the carrier of L in W holds ( L is object of (W -CONT_category) iff ( L is strict & L is complete & L is continuous ) ) let L be LATTICE; ::_thesis: ( the carrier of L in W implies ( L is object of (W -CONT_category) iff ( L is strict & L is complete & L is continuous ) ) ) assume A1: the carrier of L in W ; ::_thesis: ( L is object of (W -CONT_category) iff ( L is strict & L is complete & L is continuous ) ) hereby ::_thesis: ( L is strict & L is complete & L is continuous implies L is object of (W -CONT_category) ) assume L is object of (W -CONT_category) ; ::_thesis: ( L is strict & L is complete & L is continuous ) then reconsider a = L as object of (W -CONT_category) ; ( L = latt a & a is object of (W -UPS_category) ) by ALTCAT_2:29; hence ( L is strict & L is complete & L is continuous ) by A1, Def11, Th14; ::_thesis: verum end; assume A2: ( L is strict & L is complete & L is continuous ) ; ::_thesis: L is object of (W -CONT_category) then reconsider a = L as object of (W -UPS_category) by A1, Th14; latt a = L ; hence L is object of (W -CONT_category) by A2, Def11; ::_thesis: verum end; theorem :: YELLOW21:17 for W being with_non-empty_element set for L being LATTICE st the carrier of L in W holds ( L is object of (W -ALG_category) iff ( L is strict & L is complete & L is algebraic ) ) proof let W be with_non-empty_element set ; ::_thesis: for L being LATTICE st the carrier of L in W holds ( L is object of (W -ALG_category) iff ( L is strict & L is complete & L is algebraic ) ) let L be LATTICE; ::_thesis: ( the carrier of L in W implies ( L is object of (W -ALG_category) iff ( L is strict & L is complete & L is algebraic ) ) ) assume A1: the carrier of L in W ; ::_thesis: ( L is object of (W -ALG_category) iff ( L is strict & L is complete & L is algebraic ) ) hereby ::_thesis: ( L is strict & L is complete & L is algebraic implies L is object of (W -ALG_category) ) assume L is object of (W -ALG_category) ; ::_thesis: ( L is strict & L is complete & L is algebraic ) then reconsider a = L as object of (W -ALG_category) ; ( L = latt a & a is object of (W -CONT_category) ) by ALTCAT_2:29; hence ( L is strict & L is complete & L is algebraic ) by A1, Def12, Th16; ::_thesis: verum end; assume A2: ( L is strict & L is complete & L is algebraic ) ; ::_thesis: L is object of (W -ALG_category) then reconsider a = L as object of (W -CONT_category) by A1, Th16; latt a = L ; hence L is object of (W -ALG_category) by A2, Def12; ::_thesis: verum end; theorem Th18: :: YELLOW21:18 for W being with_non-empty_element set for a, b being object of (W -CONT_category) for f being set holds ( f in <^a,b^> iff f is directed-sups-preserving Function of (latt a),(latt b) ) proof let W be with_non-empty_element set ; ::_thesis: for a, b being object of (W -CONT_category) for f being set holds ( f in <^a,b^> iff f is directed-sups-preserving Function of (latt a),(latt b) ) let a, b be object of (W -CONT_category); ::_thesis: for f being set holds ( f in <^a,b^> iff f is directed-sups-preserving Function of (latt a),(latt b) ) let f be set ; ::_thesis: ( f in <^a,b^> iff f is directed-sups-preserving Function of (latt a),(latt b) ) reconsider a1 = a, b1 = b as object of (W -UPS_category) by ALTCAT_2:29; <^a,b^> = <^a1,b1^> by ALTCAT_2:28; hence ( f in <^a,b^> iff f is directed-sups-preserving Function of (latt a),(latt b) ) by Th15; ::_thesis: verum end; theorem Th19: :: YELLOW21:19 for W being with_non-empty_element set for a, b being object of (W -ALG_category) for f being set holds ( f in <^a,b^> iff f is directed-sups-preserving Function of (latt a),(latt b) ) proof let W be with_non-empty_element set ; ::_thesis: for a, b being object of (W -ALG_category) for f being set holds ( f in <^a,b^> iff f is directed-sups-preserving Function of (latt a),(latt b) ) let a, b be object of (W -ALG_category); ::_thesis: for f being set holds ( f in <^a,b^> iff f is directed-sups-preserving Function of (latt a),(latt b) ) let f be set ; ::_thesis: ( f in <^a,b^> iff f is directed-sups-preserving Function of (latt a),(latt b) ) reconsider a1 = a, b1 = b as object of (W -CONT_category) by ALTCAT_2:29; <^a,b^> = <^a1,b1^> by ALTCAT_2:28; hence ( f in <^a,b^> iff f is directed-sups-preserving Function of (latt a),(latt b) ) by Th18; ::_thesis: verum end; registration let W be with_non-empty_element set ; let a, b be object of (W -CONT_category); cluster<^a,b^> -> non empty ; coherence not <^a,b^> is empty proof set f = the directed-sups-preserving Function of (latt a),(latt b); the directed-sups-preserving Function of (latt a),(latt b) in <^a,b^> by Th18; hence not <^a,b^> is empty ; ::_thesis: verum end; end; registration let W be with_non-empty_element set ; let a, b be object of (W -ALG_category); cluster<^a,b^> -> non empty ; coherence not <^a,b^> is empty proof set f = the directed-sups-preserving Function of (latt a),(latt b); the directed-sups-preserving Function of (latt a),(latt b) in <^a,b^> by Th19; hence not <^a,b^> is empty ; ::_thesis: verum end; end;