:: ORDERS_3 semantic presentation begin definition let IT be RelStr ; attrIT is discrete means :Def1: :: ORDERS_3:def 1 the InternalRel of IT = id the carrier of IT; end; :: deftheorem Def1 defines discrete ORDERS_3:def_1_:_ for IT being RelStr holds ( IT is discrete iff the InternalRel of IT = id the carrier of IT ); registration cluster non empty strict V65() reflexive transitive antisymmetric discrete for RelStr ; existence ex b1 being Poset st ( b1 is strict & b1 is discrete & not b1 is empty ) proof set A = the non empty set ; reconsider R = id the non empty set as Relation of the non empty set ; reconsider R = R as Order of the non empty set ; take RelStr(# the non empty set ,R #) ; ::_thesis: ( RelStr(# the non empty set ,R #) is strict & RelStr(# the non empty set ,R #) is discrete & not RelStr(# the non empty set ,R #) is empty ) thus ( RelStr(# the non empty set ,R #) is strict & RelStr(# the non empty set ,R #) is discrete & not RelStr(# the non empty set ,R #) is empty ) by Def1; ::_thesis: verum end; end; registration cluster RelStr(# {},(id {}) #) -> empty ; coherence RelStr(# {},(id {}) #) is empty ; let P be empty RelStr ; cluster the InternalRel of P -> empty ; coherence the InternalRel of P is empty ; end; Lm1: for P being RelStr st P is empty holds P is discrete proof let P be RelStr ; ::_thesis: ( P is empty implies P is discrete ) assume P is empty ; ::_thesis: P is discrete then ( the carrier of P = {} & the InternalRel of P = {} ) ; hence P is discrete by Def1, RELAT_1:55; ::_thesis: verum end; registration cluster empty -> discrete for RelStr ; coherence for b1 being RelStr st b1 is empty holds b1 is discrete by Lm1; end; definition let P be RelStr ; let IT be Subset of P; attrIT is disconnected means :Def2: :: ORDERS_3:def 2 ex A, B being Subset of P st ( A <> {} & B <> {} & IT = A \/ B & A misses B & the InternalRel of P = ( the InternalRel of P |_2 A) \/ ( the InternalRel of P |_2 B) ); end; :: deftheorem Def2 defines disconnected ORDERS_3:def_2_:_ for P being RelStr for IT being Subset of P holds ( IT is disconnected iff ex A, B being Subset of P st ( A <> {} & B <> {} & IT = A \/ B & A misses B & the InternalRel of P = ( the InternalRel of P |_2 A) \/ ( the InternalRel of P |_2 B) ) ); notation let P be RelStr ; let IT be Subset of P; antonym connected IT for disconnected ; end; definition let IT be RelStr ; attrIT is disconnected means :Def3: :: ORDERS_3:def 3 [#] IT is disconnected ; end; :: deftheorem Def3 defines disconnected ORDERS_3:def_3_:_ for IT being RelStr holds ( IT is disconnected iff [#] IT is disconnected ); notation let IT be RelStr ; antonym connected IT for disconnected ; end; theorem :: ORDERS_3:1 for DP being non empty discrete RelStr for x, y being Element of DP holds ( x <= y iff x = y ) proof let DP be non empty discrete RelStr ; ::_thesis: for x, y being Element of DP holds ( x <= y iff x = y ) let x, y be Element of DP; ::_thesis: ( x <= y iff x = y ) hereby ::_thesis: ( x = y implies x <= y ) assume x <= y ; ::_thesis: x = y then [x,y] in the InternalRel of DP by ORDERS_2:def_5; then [x,y] in id the carrier of DP by Def1; hence x = y by RELAT_1:def_10; ::_thesis: verum end; assume x = y ; ::_thesis: x <= y then [x,y] in id the carrier of DP by RELAT_1:def_10; then [x,y] in the InternalRel of DP by Def1; hence x <= y by ORDERS_2:def_5; ::_thesis: verum end; theorem :: ORDERS_3:2 for R being Relation for a being set st R is Order of {a} holds R = id {a} proof let R be Relation; ::_thesis: for a being set st R is Order of {a} holds R = id {a} let a be set ; ::_thesis: ( R is Order of {a} implies R = id {a} ) assume A1: R is Order of {a} ; ::_thesis: R = id {a} then A2: R <> {} ; R c= [:{a},{a}:] by A1; then R c= {[a,a]} by ZFMISC_1:29; then R = {[a,a]} by A2, ZFMISC_1:33; hence R = id {a} by SYSREL:13; ::_thesis: verum end; theorem :: ORDERS_3:3 for T being non empty RelStr for a being Element of T st T is reflexive & [#] T = {a} holds T is discrete proof let T be non empty RelStr ; ::_thesis: for a being Element of T st T is reflexive & [#] T = {a} holds T is discrete let a be Element of T; ::_thesis: ( T is reflexive & [#] T = {a} implies T is discrete ) assume A1: T is reflexive ; ::_thesis: ( not [#] T = {a} or T is discrete ) set R = the InternalRel of T; assume A2: [#] T = {a} ; ::_thesis: T is discrete the InternalRel of T = id {a} proof A3: id {a} = {[a,a]} by SYSREL:13; the InternalRel of T c= [:{a},{a}:] by A2; hence the InternalRel of T c= id {a} by A3, ZFMISC_1:29; :: according to XBOOLE_0:def_10 ::_thesis: id {a} c= the InternalRel of T let x be set ; :: according to TARSKI:def_3 ::_thesis: ( not x in id {a} or x in the InternalRel of T ) assume x in id {a} ; ::_thesis: x in the InternalRel of T then A4: x = [a,a] by A3, TARSKI:def_1; a >= a by A1, ORDERS_2:1; hence x in the InternalRel of T by A4, ORDERS_2:def_5; ::_thesis: verum end; hence T is discrete by A2, Def1; ::_thesis: verum end; theorem Th4: :: ORDERS_3:4 for T being non empty RelStr for a being set st [#] T = {a} holds T is connected proof let T be non empty RelStr ; ::_thesis: for a being set st [#] T = {a} holds T is connected let a be set ; ::_thesis: ( [#] T = {a} implies T is connected ) reconsider OT = [#] T as non empty set ; assume A1: [#] T = {a} ; ::_thesis: T is connected A2: for Z, Z9 being non empty Subset of OT holds not Z misses Z9 proof let Z, Z9 be non empty Subset of OT; ::_thesis: not Z misses Z9 Z = {a} by A1, ZFMISC_1:33; hence not Z misses Z9 by A1, ZFMISC_1:33; ::_thesis: verum end; [#] T is connected proof assume [#] T is disconnected ; ::_thesis: contradiction then ex A, B being Subset of T st ( A <> {} & B <> {} & [#] T = A \/ B & A misses B & the InternalRel of T = ( the InternalRel of T |_2 A) \/ ( the InternalRel of T |_2 B) ) by Def2; hence contradiction by A2; ::_thesis: verum end; hence T is connected by Def3; ::_thesis: verum end; theorem Th5: :: ORDERS_3:5 for DP being non empty discrete Poset st ex a, b being Element of DP st a <> b holds DP is disconnected proof let DP be non empty discrete Poset; ::_thesis: ( ex a, b being Element of DP st a <> b implies DP is disconnected ) given a, b being Element of DP such that A1: a <> b ; ::_thesis: DP is disconnected not b in {a} by A1, TARSKI:def_1; then reconsider A = the carrier of DP \ {a} as non empty Subset of DP by XBOOLE_0:def_5; reconsider B = {a} as non empty Subset of DP ; A2: ( the carrier of DP = ( the carrier of DP \ {a}) \/ {a} & the carrier of DP \ {a} misses {a} ) by XBOOLE_1:45, XBOOLE_1:79; the InternalRel of DP c= [:A,A:] \/ [:B,B:] proof let x be set ; :: according to TARSKI:def_3 ::_thesis: ( not x in the InternalRel of DP or x in [:A,A:] \/ [:B,B:] ) assume A3: x in the InternalRel of DP ; ::_thesis: x in [:A,A:] \/ [:B,B:] then consider x1, x2 being set such that A4: x = [x1,x2] by RELAT_1:def_1; A5: x in id the carrier of DP by A3, Def1; then A6: x1 = x2 by A4, RELAT_1:def_10; percases ( x1 in A or not x1 in A ) ; supposeA7: x1 in A ; ::_thesis: x in [:A,A:] \/ [:B,B:] A8: [:A,A:] c= [:A,A:] \/ [:B,B:] by XBOOLE_1:7; [x1,x1] in [:A,A:] by A7, ZFMISC_1:87; hence x in [:A,A:] \/ [:B,B:] by A4, A6, A8; ::_thesis: verum end; supposeA9: not x1 in A ; ::_thesis: x in [:A,A:] \/ [:B,B:] x1 in the carrier of DP by A5, A4, RELAT_1:def_10; then x1 in the carrier of DP \ A by A9, XBOOLE_0:def_5; then x1 in the carrier of DP /\ B by XBOOLE_1:48; then x1 in B by XBOOLE_1:28; then A10: [x1,x1] in [:B,B:] by ZFMISC_1:87; [:B,B:] c= [:A,A:] \/ [:B,B:] by XBOOLE_1:7; hence x in [:A,A:] \/ [:B,B:] by A4, A6, A10; ::_thesis: verum end; end; end; then A11: the InternalRel of DP = the InternalRel of DP /\ ([:A,A:] \/ [:B,B:]) by XBOOLE_1:28; ( the InternalRel of DP |_2 A = the InternalRel of DP /\ [:A,A:] & the InternalRel of DP |_2 B = the InternalRel of DP /\ [:B,B:] ) by WELLORD1:def_6; then the InternalRel of DP = ( the InternalRel of DP |_2 A) \/ ( the InternalRel of DP |_2 B) by A11, XBOOLE_1:23; then [#] DP is disconnected by A2, Def2; hence DP is disconnected by Def3; ::_thesis: verum end; registration cluster non empty strict V65() reflexive transitive antisymmetric connected for RelStr ; existence ex b1 being non empty Poset st ( b1 is strict & b1 is connected ) proof set x = the set ; reconsider A = RelStr(# { the set },(id { the set }) #) as non empty Poset ; [#] A = { the set } ; then A is connected by Th4; hence ex b1 being non empty Poset st ( b1 is strict & b1 is connected ) ; ::_thesis: verum end; cluster non empty strict V65() reflexive transitive antisymmetric discrete disconnected for RelStr ; existence ex b1 being non empty Poset st ( b1 is strict & b1 is disconnected & b1 is discrete ) proof ex Y being non empty Poset st ( Y is strict & Y is disconnected & Y is discrete ) proof reconsider A = RelStr(# {1,2},(id {1,2}) #) as non empty Poset ; reconsider A = A as non empty discrete Poset by Def1; take A ; ::_thesis: ( A is strict & A is disconnected & A is discrete ) ex a, b being Element of A st a <> b proof set a = 1; set b = 2; reconsider a = 1, b = 2 as Element of A by TARSKI:def_2; take a ; ::_thesis: ex b being Element of A st a <> b take b ; ::_thesis: a <> b thus a <> b ; ::_thesis: verum end; hence ( A is strict & A is disconnected & A is discrete ) by Th5; ::_thesis: verum end; hence ex b1 being non empty Poset st ( b1 is strict & b1 is disconnected & b1 is discrete ) ; ::_thesis: verum end; end; begin definition let IT be set ; attrIT is POSet_set-like means :Def4: :: ORDERS_3:def 4 for a being set st a in IT holds a is non empty Poset; end; :: deftheorem Def4 defines POSet_set-like ORDERS_3:def_4_:_ for IT being set holds ( IT is POSet_set-like iff for a being set st a in IT holds a is non empty Poset ); registration cluster non empty POSet_set-like for set ; existence ex b1 being set st ( not b1 is empty & b1 is POSet_set-like ) proof set P = the non empty Poset; set A = { the non empty Poset}; take { the non empty Poset} ; ::_thesis: ( not { the non empty Poset} is empty & { the non empty Poset} is POSet_set-like ) for a being set st a in { the non empty Poset} holds a is non empty Poset by TARSKI:def_1; hence ( not { the non empty Poset} is empty & { the non empty Poset} is POSet_set-like ) by Def4; ::_thesis: verum end; end; definition mode POSet_set is POSet_set-like set ; end; definition let P be non empty POSet_set; :: original: Element redefine mode Element of P -> non empty Poset; coherence for b1 being Element of P holds b1 is non empty Poset by Def4; end; definition let L1, L2 be RelStr ; let f be Function of L1,L2; attrf is monotone means :Def5: :: ORDERS_3:def 5 for x, y being Element of L1 st x <= y holds for a, b being Element of L2 st a = f . x & b = f . y holds a <= b; end; :: deftheorem Def5 defines monotone ORDERS_3:def_5_:_ for L1, L2 being RelStr for f being Function of L1,L2 holds ( f is monotone iff for x, y being Element of L1 st x <= y holds for a, b being Element of L2 st a = f . x & b = f . y holds a <= b ); Lm2: for A, B, C being non empty RelStr for f being Function of A,B for g being Function of B,C st f is monotone & g is monotone holds ex gf being Function of A,C st ( gf = g * f & gf is monotone ) proof let A, B, C be non empty RelStr ; ::_thesis: for f being Function of A,B for g being Function of B,C st f is monotone & g is monotone holds ex gf being Function of A,C st ( gf = g * f & gf is monotone ) let f be Function of A,B; ::_thesis: for g being Function of B,C st f is monotone & g is monotone holds ex gf being Function of A,C st ( gf = g * f & gf is monotone ) let g be Function of B,C; ::_thesis: ( f is monotone & g is monotone implies ex gf being Function of A,C st ( gf = g * f & gf is monotone ) ) assume that A1: f is monotone and A2: g is monotone ; ::_thesis: ex gf being Function of A,C st ( gf = g * f & gf is monotone ) reconsider gf = g * f as Function of A,C ; take gf ; ::_thesis: ( gf = g * f & gf is monotone ) now__::_thesis:_for_p1,_p2_being_Element_of_A_st_p1_<=_p2_holds_ for_r1,_r2_being_Element_of_C_st_r1_=_gf_._p1_&_r2_=_gf_._p2_holds_ r1_<=_r2 let p1, p2 be Element of A; ::_thesis: ( p1 <= p2 implies for r1, r2 being Element of C st r1 = gf . p1 & r2 = gf . p2 holds r1 <= r2 ) reconsider p19 = f . p1, p29 = f . p2 as Element of B ; dom f = the carrier of A by FUNCT_2:def_1; then A3: ( g . (f . p1) = (g * f) . p1 & g . (f . p2) = (g * f) . p2 ) by FUNCT_1:13; assume p1 <= p2 ; ::_thesis: for r1, r2 being Element of C st r1 = gf . p1 & r2 = gf . p2 holds r1 <= r2 then A4: p19 <= p29 by A1, Def5; let r1, r2 be Element of C; ::_thesis: ( r1 = gf . p1 & r2 = gf . p2 implies r1 <= r2 ) assume ( r1 = gf . p1 & r2 = gf . p2 ) ; ::_thesis: r1 <= r2 hence r1 <= r2 by A2, A3, A4, Def5; ::_thesis: verum end; hence ( gf = g * f & gf is monotone ) by Def5; ::_thesis: verum end; Lm3: for T being non empty RelStr holds id T is monotone proof let T be non empty RelStr ; ::_thesis: id T is monotone set IT = id T; let p1, p2 be Element of T; :: according to ORDERS_3:def_5 ::_thesis: ( p1 <= p2 implies for a, b being Element of T st a = (id T) . p1 & b = (id T) . p2 holds a <= b ) assume A1: p1 <= p2 ; ::_thesis: for a, b being Element of T st a = (id T) . p1 & b = (id T) . p2 holds a <= b let r1, r2 be Element of T; ::_thesis: ( r1 = (id T) . p1 & r2 = (id T) . p2 implies r1 <= r2 ) reconsider p19 = p1 as Element of T ; A2: (id T) . p19 = p19 by FUNCT_1:18; assume ( r1 = (id T) . p1 & r2 = (id T) . p2 ) ; ::_thesis: r1 <= r2 hence r1 <= r2 by A1, A2, FUNCT_1:18; ::_thesis: verum end; definition let A, B be RelStr ; func MonFuncs (A,B) -> set means :Def6: :: ORDERS_3:def 6 for a being set holds ( a in it iff ex f being Function of A,B st ( a = f & f in Funcs ( the carrier of A, the carrier of B) & f is monotone ) ); existence ex b1 being set st for a being set holds ( a in b1 iff ex f being Function of A,B st ( a = f & f in Funcs ( the carrier of A, the carrier of B) & f is monotone ) ) proof defpred S1[ set ] means ex f being Function of A,B st ( f = \$1 & f is monotone ); consider AB being set such that A1: for a being set holds ( a in AB iff ( a in Funcs ( the carrier of A, the carrier of B) & S1[a] ) ) from XBOOLE_0:sch_1(); take AB ; ::_thesis: for a being set holds ( a in AB iff ex f being Function of A,B st ( a = f & f in Funcs ( the carrier of A, the carrier of B) & f is monotone ) ) thus for a being set holds ( a in AB iff ex f being Function of A,B st ( a = f & f in Funcs ( the carrier of A, the carrier of B) & f is monotone ) ) ::_thesis: verum proof let a be set ; ::_thesis: ( a in AB iff ex f being Function of A,B st ( a = f & f in Funcs ( the carrier of A, the carrier of B) & f is monotone ) ) hereby ::_thesis: ( ex f being Function of A,B st ( a = f & f in Funcs ( the carrier of A, the carrier of B) & f is monotone ) implies a in AB ) assume A2: a in AB ; ::_thesis: ex f being Function of A,B st ( a = f & f in Funcs ( the carrier of A, the carrier of B) & f is monotone ) then consider f being Function of A,B such that A3: ( f = a & f is monotone ) by A1; take f = f; ::_thesis: ( a = f & f in Funcs ( the carrier of A, the carrier of B) & f is monotone ) thus ( a = f & f in Funcs ( the carrier of A, the carrier of B) & f is monotone ) by A1, A2, A3; ::_thesis: verum end; given f being Function of A,B such that A4: ( a = f & f in Funcs ( the carrier of A, the carrier of B) & f is monotone ) ; ::_thesis: a in AB thus a in AB by A1, A4; ::_thesis: verum end; end; uniqueness for b1, b2 being set st ( for a being set holds ( a in b1 iff ex f being Function of A,B st ( a = f & f in Funcs ( the carrier of A, the carrier of B) & f is monotone ) ) ) & ( for a being set holds ( a in b2 iff ex f being Function of A,B st ( a = f & f in Funcs ( the carrier of A, the carrier of B) & f is monotone ) ) ) holds b1 = b2 proof let A1, A2 be set ; ::_thesis: ( ( for a being set holds ( a in A1 iff ex f being Function of A,B st ( a = f & f in Funcs ( the carrier of A, the carrier of B) & f is monotone ) ) ) & ( for a being set holds ( a in A2 iff ex f being Function of A,B st ( a = f & f in Funcs ( the carrier of A, the carrier of B) & f is monotone ) ) ) implies A1 = A2 ) assume that A5: for a being set holds ( a in A1 iff ex f being Function of A,B st ( a = f & f in Funcs ( the carrier of A, the carrier of B) & f is monotone ) ) and A6: for a being set holds ( a in A2 iff ex f being Function of A,B st ( a = f & f in Funcs ( the carrier of A, the carrier of B) & f is monotone ) ) ; ::_thesis: A1 = A2 for a being set st a in A2 holds a in A1 proof let a be set ; ::_thesis: ( a in A2 implies a in A1 ) assume a in A2 ; ::_thesis: a in A1 then ex f being Function of A,B st ( a = f & f in Funcs ( the carrier of A, the carrier of B) & f is monotone ) by A6; hence a in A1 by A5; ::_thesis: verum end; then A7: A2 c= A1 by TARSKI:def_3; for a being set st a in A1 holds a in A2 proof let a be set ; ::_thesis: ( a in A1 implies a in A2 ) assume a in A1 ; ::_thesis: a in A2 then ex f being Function of A,B st ( a = f & f in Funcs ( the carrier of A, the carrier of B) & f is monotone ) by A5; hence a in A2 by A6; ::_thesis: verum end; then A1 c= A2 by TARSKI:def_3; hence A1 = A2 by A7, XBOOLE_0:def_10; ::_thesis: verum end; end; :: deftheorem Def6 defines MonFuncs ORDERS_3:def_6_:_ for A, B being RelStr for b3 being set holds ( b3 = MonFuncs (A,B) iff for a being set holds ( a in b3 iff ex f being Function of A,B st ( a = f & f in Funcs ( the carrier of A, the carrier of B) & f is monotone ) ) ); theorem Th6: :: ORDERS_3:6 for A, B, C being non empty RelStr for f, g being Function st f in MonFuncs (A,B) & g in MonFuncs (B,C) holds g * f in MonFuncs (A,C) proof let A, B, C be non empty RelStr ; ::_thesis: for f, g being Function st f in MonFuncs (A,B) & g in MonFuncs (B,C) holds g * f in MonFuncs (A,C) let f, g be Function; ::_thesis: ( f in MonFuncs (A,B) & g in MonFuncs (B,C) implies g * f in MonFuncs (A,C) ) assume that A1: f in MonFuncs (A,B) and A2: g in MonFuncs (B,C) ; ::_thesis: g * f in MonFuncs (A,C) consider f9 being Function of A,B such that A3: f = f9 and f9 in Funcs ( the carrier of A, the carrier of B) and A4: f9 is monotone by A1, Def6; consider g9 being Function of B,C such that A5: g = g9 and g9 in Funcs ( the carrier of B, the carrier of C) and A6: g9 is monotone by A2, Def6; consider gf being Function of A,C such that A7: ( gf = g9 * f9 & gf is monotone ) by A4, A6, Lm2; gf in Funcs ( the carrier of A, the carrier of C) by FUNCT_2:8; hence g * f in MonFuncs (A,C) by A3, A5, A7, Def6; ::_thesis: verum end; theorem Th7: :: ORDERS_3:7 for T being non empty RelStr holds id the carrier of T in MonFuncs (T,T) proof let T be non empty RelStr ; ::_thesis: id the carrier of T in MonFuncs (T,T) reconsider IT = id T as Function of the carrier of T, the carrier of T ; reconsider IT9 = IT as Function of T,T ; ( id T is monotone & IT9 in Funcs ( the carrier of T, the carrier of T) ) by Lm3, FUNCT_2:9; hence id the carrier of T in MonFuncs (T,T) by Def6; ::_thesis: verum end; registration let T be non empty RelStr ; cluster MonFuncs (T,T) -> non empty ; coherence not MonFuncs (T,T) is empty by Th7; end; definition let X be set ; func Carr X -> set means :Def7: :: ORDERS_3:def 7 for a being set holds ( a in it iff ex s being 1-sorted st ( s in X & a = the carrier of s ) ); existence ex b1 being set st for a being set holds ( a in b1 iff ex s being 1-sorted st ( s in X & a = the carrier of s ) ) proof defpred S1[ set , set ] means ex s being 1-sorted st ( s = \$1 & \$2 = the carrier of s ); A1: for x, y, z being set st S1[x,y] & S1[x,z] holds y = z ; consider CX being set such that A2: for x being set holds ( x in CX iff ex y being set st ( y in X & S1[y,x] ) ) from TARSKI:sch_1(A1); take CX ; ::_thesis: for a being set holds ( a in CX iff ex s being 1-sorted st ( s in X & a = the carrier of s ) ) let x be set ; ::_thesis: ( x in CX iff ex s being 1-sorted st ( s in X & x = the carrier of s ) ) ( x in CX iff ex s being 1-sorted st ( s in X & x = the carrier of s ) ) proof thus ( x in CX implies ex s being 1-sorted st ( s in X & x = the carrier of s ) ) ::_thesis: ( ex s being 1-sorted st ( s in X & x = the carrier of s ) implies x in CX ) proof assume x in CX ; ::_thesis: ex s being 1-sorted st ( s in X & x = the carrier of s ) then consider y being set such that A3: y in X and A4: ex s being 1-sorted st ( s = y & x = the carrier of s ) by A2; consider s being 1-sorted such that A5: s = y and x = the carrier of s by A4; take s ; ::_thesis: ( s in X & x = the carrier of s ) thus ( s in X & x = the carrier of s ) by A3, A4, A5; ::_thesis: verum end; given s being 1-sorted such that A6: ( s in X & x = the carrier of s ) ; ::_thesis: x in CX thus x in CX by A2, A6; ::_thesis: verum end; hence ( x in CX iff ex s being 1-sorted st ( s in X & x = the carrier of s ) ) ; ::_thesis: verum end; uniqueness for b1, b2 being set st ( for a being set holds ( a in b1 iff ex s being 1-sorted st ( s in X & a = the carrier of s ) ) ) & ( for a being set holds ( a in b2 iff ex s being 1-sorted st ( s in X & a = the carrier of s ) ) ) holds b1 = b2 proof let C1, C2 be set ; ::_thesis: ( ( for a being set holds ( a in C1 iff ex s being 1-sorted st ( s in X & a = the carrier of s ) ) ) & ( for a being set holds ( a in C2 iff ex s being 1-sorted st ( s in X & a = the carrier of s ) ) ) implies C1 = C2 ) assume that A7: for a being set holds ( a in C1 iff ex s being 1-sorted st ( s in X & a = the carrier of s ) ) and A8: for a being set holds ( a in C2 iff ex s being 1-sorted st ( s in X & a = the carrier of s ) ) ; ::_thesis: C1 = C2 for a being set holds ( a in C1 iff a in C2 ) proof let a be set ; ::_thesis: ( a in C1 iff a in C2 ) thus ( a in C1 implies a in C2 ) ::_thesis: ( a in C2 implies a in C1 ) proof assume a in C1 ; ::_thesis: a in C2 then ex s being 1-sorted st ( s in X & a = the carrier of s ) by A7; hence a in C2 by A8; ::_thesis: verum end; thus ( a in C2 implies a in C1 ) ::_thesis: verum proof assume a in C2 ; ::_thesis: a in C1 then ex s being 1-sorted st ( s in X & a = the carrier of s ) by A8; hence a in C1 by A7; ::_thesis: verum end; end; hence C1 = C2 by TARSKI:1; ::_thesis: verum end; end; :: deftheorem Def7 defines Carr ORDERS_3:def_7_:_ for X, b2 being set holds ( b2 = Carr X iff for a being set holds ( a in b2 iff ex s being 1-sorted st ( s in X & a = the carrier of s ) ) ); Lm4: for P being non empty POSet_set for A being Element of P holds the carrier of A in Carr P by Def7; registration let P be non empty POSet_set; cluster Carr P -> non empty ; coherence not Carr P is empty by Lm4; end; theorem :: ORDERS_3:8 for f being 1-sorted holds Carr {f} = { the carrier of f} proof let f be 1-sorted ; ::_thesis: Carr {f} = { the carrier of f} thus Carr {f} c= { the carrier of f} :: according to XBOOLE_0:def_10 ::_thesis: { the carrier of f} c= Carr {f} proof let a be set ; :: according to TARSKI:def_3 ::_thesis: ( not a in Carr {f} or a in { the carrier of f} ) assume a in Carr {f} ; ::_thesis: a in { the carrier of f} then consider s being 1-sorted such that A1: s in {f} and A2: a = the carrier of s by Def7; s = f by A1, TARSKI:def_1; hence a in { the carrier of f} by A2, TARSKI:def_1; ::_thesis: verum end; A3: f in {f} by TARSKI:def_1; thus { the carrier of f} c= Carr {f} ::_thesis: verum proof let a be set ; :: according to TARSKI:def_3 ::_thesis: ( not a in { the carrier of f} or a in Carr {f} ) assume a in { the carrier of f} ; ::_thesis: a in Carr {f} then a = the carrier of f by TARSKI:def_1; hence a in Carr {f} by A3, Def7; ::_thesis: verum end; end; theorem :: ORDERS_3:9 for f, g being 1-sorted holds Carr {f,g} = { the carrier of f, the carrier of g} proof let f, g be 1-sorted ; ::_thesis: Carr {f,g} = { the carrier of f, the carrier of g} thus Carr {f,g} c= { the carrier of f, the carrier of g} :: according to XBOOLE_0:def_10 ::_thesis: { the carrier of f, the carrier of g} c= Carr {f,g} proof let a be set ; :: according to TARSKI:def_3 ::_thesis: ( not a in Carr {f,g} or a in { the carrier of f, the carrier of g} ) assume a in Carr {f,g} ; ::_thesis: a in { the carrier of f, the carrier of g} then consider s being 1-sorted such that A1: s in {f,g} and A2: a = the carrier of s by Def7; percases ( s = f or s = g ) by A1, TARSKI:def_2; suppose s = f ; ::_thesis: a in { the carrier of f, the carrier of g} hence a in { the carrier of f, the carrier of g} by A2, TARSKI:def_2; ::_thesis: verum end; suppose s = g ; ::_thesis: a in { the carrier of f, the carrier of g} hence a in { the carrier of f, the carrier of g} by A2, TARSKI:def_2; ::_thesis: verum end; end; end; thus { the carrier of f, the carrier of g} c= Carr {f,g} ::_thesis: verum proof let a be set ; :: according to TARSKI:def_3 ::_thesis: ( not a in { the carrier of f, the carrier of g} or a in Carr {f,g} ) A3: f in {f,g} by TARSKI:def_2; A4: g in {f,g} by TARSKI:def_2; assume A5: a in { the carrier of f, the carrier of g} ; ::_thesis: a in Carr {f,g} percases ( a = the carrier of f or a = the carrier of g ) by A5, TARSKI:def_2; suppose a = the carrier of f ; ::_thesis: a in Carr {f,g} hence a in Carr {f,g} by A3, Def7; ::_thesis: verum end; suppose a = the carrier of g ; ::_thesis: a in Carr {f,g} hence a in Carr {f,g} by A4, Def7; ::_thesis: verum end; end; end; end; theorem Th10: :: ORDERS_3:10 for P being non empty POSet_set for A, B being Element of P holds MonFuncs (A,B) c= Funcs (Carr P) proof let P be non empty POSet_set; ::_thesis: for A, B being Element of P holds MonFuncs (A,B) c= Funcs (Carr P) let A, B be Element of P; ::_thesis: MonFuncs (A,B) c= Funcs (Carr P) reconsider CA = the carrier of A, CB = the carrier of B as Element of Carr P by Def7; let x be set ; :: according to TARSKI:def_3 ::_thesis: ( not x in MonFuncs (A,B) or x in Funcs (Carr P) ) assume x in MonFuncs (A,B) ; ::_thesis: x in Funcs (Carr P) then A1: ex g being Function of A,B st ( x = g & g in Funcs ( the carrier of A, the carrier of B) & g is monotone ) by Def6; Funcs (CA,CB) c= Funcs (Carr P) by ENS_1:2; hence x in Funcs (Carr P) by A1; ::_thesis: verum end; theorem Th11: :: ORDERS_3:11 for A, B being RelStr holds MonFuncs (A,B) c= Funcs ( the carrier of A, the carrier of B) proof let A, B be RelStr ; ::_thesis: MonFuncs (A,B) c= Funcs ( the carrier of A, the carrier of B) let a be set ; :: according to TARSKI:def_3 ::_thesis: ( not a in MonFuncs (A,B) or a in Funcs ( the carrier of A, the carrier of B) ) assume a in MonFuncs (A,B) ; ::_thesis: a in Funcs ( the carrier of A, the carrier of B) then ex f being Function of A,B st ( a = f & f in Funcs ( the carrier of A, the carrier of B) & f is monotone ) by Def6; hence a in Funcs ( the carrier of A, the carrier of B) ; ::_thesis: verum end; registration let A, B be non empty Poset; cluster MonFuncs (A,B) -> functional ; coherence MonFuncs (A,B) is functional proof reconsider X = MonFuncs (A,B) as Subset of (Funcs ( the carrier of A, the carrier of B)) by Th11; X is functional ; hence MonFuncs (A,B) is functional ; ::_thesis: verum end; end; definition let P be non empty POSet_set; func POSCat P -> strict with_triple-like_morphisms Category means :: ORDERS_3:def 8 ( the carrier of it = P & ( for a, b being Element of P for f being Element of Funcs (Carr P) st f in MonFuncs (a,b) holds [[a,b],f] is Morphism of it ) & ( for m being Morphism of it ex a, b being Element of P ex f being Element of Funcs (Carr P) st ( m = [[a,b],f] & f in MonFuncs (a,b) ) ) & ( for m1, m2 being Morphism of it for a1, a2, a3 being Element of P for f1, f2 being Element of Funcs (Carr P) st m1 = [[a1,a2],f1] & m2 = [[a2,a3],f2] holds m2 (*) m1 = [[a1,a3],(f2 * f1)] ) ); existence ex b1 being strict with_triple-like_morphisms Category st ( the carrier of b1 = P & ( for a, b being Element of P for f being Element of Funcs (Carr P) st f in MonFuncs (a,b) holds [[a,b],f] is Morphism of b1 ) & ( for m being Morphism of b1 ex a, b being Element of P ex f being Element of Funcs (Carr P) st ( m = [[a,b],f] & f in MonFuncs (a,b) ) ) & ( for m1, m2 being Morphism of b1 for a1, a2, a3 being Element of P for f1, f2 being Element of Funcs (Carr P) st m1 = [[a1,a2],f1] & m2 = [[a2,a3],f2] holds m2 (*) m1 = [[a1,a3],(f2 * f1)] ) ) proof deffunc H1( Function, Function) -> set = \$1 * \$2; defpred S1[ Element of P, Element of P, set ] means \$3 in MonFuncs (\$1,\$2); A1: for a, b, c being Element of P for f, g being Element of Funcs (Carr P) st S1[a,b,f] & S1[b,c,g] holds ( H1(g,f) in Funcs (Carr P) & S1[a,c,H1(g,f)] ) proof let a, b, c be Element of P; ::_thesis: for f, g being Element of Funcs (Carr P) st S1[a,b,f] & S1[b,c,g] holds ( H1(g,f) in Funcs (Carr P) & S1[a,c,H1(g,f)] ) let f, g be Element of Funcs (Carr P); ::_thesis: ( S1[a,b,f] & S1[b,c,g] implies ( H1(g,f) in Funcs (Carr P) & S1[a,c,H1(g,f)] ) ) assume ( f in MonFuncs (a,b) & g in MonFuncs (b,c) ) ; ::_thesis: ( H1(g,f) in Funcs (Carr P) & S1[a,c,H1(g,f)] ) then A2: g * f in MonFuncs (a,c) by Th6; MonFuncs (a,c) c= Funcs (Carr P) by Th10; hence ( H1(g,f) in Funcs (Carr P) & S1[a,c,H1(g,f)] ) by A2; ::_thesis: verum end; A3: for a being Element of P ex f being Element of Funcs (Carr P) st ( S1[a,a,f] & ( for b being Element of P for g being Element of Funcs (Carr P) holds ( ( S1[a,b,g] implies H1(g,f) = g ) & ( S1[b,a,g] implies H1(f,g) = g ) ) ) ) proof let a be Element of P; ::_thesis: ex f being Element of Funcs (Carr P) st ( S1[a,a,f] & ( for b being Element of P for g being Element of Funcs (Carr P) holds ( ( S1[a,b,g] implies H1(g,f) = g ) & ( S1[b,a,g] implies H1(f,g) = g ) ) ) ) set f = id the carrier of a; ( MonFuncs (a,a) c= Funcs (Carr P) & id the carrier of a in MonFuncs (a,a) ) by Th7, Th10; then reconsider f = id the carrier of a as Element of Funcs (Carr P) ; take f ; ::_thesis: ( S1[a,a,f] & ( for b being Element of P for g being Element of Funcs (Carr P) holds ( ( S1[a,b,g] implies H1(g,f) = g ) & ( S1[b,a,g] implies H1(f,g) = g ) ) ) ) now__::_thesis:_for_b_being_Element_of_P for_g_being_Element_of_Funcs_(Carr_P)_holds_ (_(_g_in_MonFuncs_(a,b)_implies_g_*_f_=_g_)_&_(_g_in_MonFuncs_(b,a)_implies_f_*_g_=_g_)_) let b be Element of P; ::_thesis: for g being Element of Funcs (Carr P) holds ( ( g in MonFuncs (a,b) implies g * f = g ) & ( g in MonFuncs (b,a) implies f * g = g ) ) let g be Element of Funcs (Carr P); ::_thesis: ( ( g in MonFuncs (a,b) implies g * f = g ) & ( g in MonFuncs (b,a) implies f * g = g ) ) A4: ( g in MonFuncs (b,a) implies f * g = g ) proof assume g in MonFuncs (b,a) ; ::_thesis: f * g = g then ex g9 being Function of b,a st ( g9 = g & g9 in Funcs ( the carrier of b, the carrier of a) & g9 is monotone ) by Def6; then reconsider g = g as Function of the carrier of b, the carrier of a ; rng g c= the carrier of a ; hence f * g = g by RELAT_1:53; ::_thesis: verum end; ( g in MonFuncs (a,b) implies g * f = g ) proof assume g in MonFuncs (a,b) ; ::_thesis: g * f = g then ex g9 being Function of a,b st ( g9 = g & g9 in Funcs ( the carrier of a, the carrier of b) & g9 is monotone ) by Def6; then reconsider g = g as Function of the carrier of a, the carrier of b ; dom g = the carrier of a by FUNCT_2:def_1; hence g * f = g by RELAT_1:51; ::_thesis: verum end; hence ( ( g in MonFuncs (a,b) implies g * f = g ) & ( g in MonFuncs (b,a) implies f * g = g ) ) by A4; ::_thesis: verum end; hence ( S1[a,a,f] & ( for b being Element of P for g being Element of Funcs (Carr P) holds ( ( S1[a,b,g] implies H1(g,f) = g ) & ( S1[b,a,g] implies H1(f,g) = g ) ) ) ) by Th7; ::_thesis: verum end; A5: for a, b, c, d being Element of P for f, g, h being Element of Funcs (Carr P) st S1[a,b,f] & S1[b,c,g] & S1[c,d,h] holds H1(h,H1(g,f)) = H1(H1(h,g),f) by RELAT_1:36; ex C being strict with_triple-like_morphisms Category st ( the carrier of C = P & ( for a, b being Element of P for f being Element of Funcs (Carr P) st S1[a,b,f] holds [[a,b],f] is Morphism of C ) & ( for m being Morphism of C ex a, b being Element of P ex f being Element of Funcs (Carr P) st ( m = [[a,b],f] & S1[a,b,f] ) ) & ( for m1, m2 being Morphism of C for a1, a2, a3 being Element of P for f1, f2 being Element of Funcs (Carr P) st m1 = [[a1,a2],f1] & m2 = [[a2,a3],f2] holds m2 (*) m1 = [[a1,a3],H1(f2,f1)] ) ) from CAT_5:sch_1(A1, A3, A5); hence ex b1 being strict with_triple-like_morphisms Category st ( the carrier of b1 = P & ( for a, b being Element of P for f being Element of Funcs (Carr P) st f in MonFuncs (a,b) holds [[a,b],f] is Morphism of b1 ) & ( for m being Morphism of b1 ex a, b being Element of P ex f being Element of Funcs (Carr P) st ( m = [[a,b],f] & f in MonFuncs (a,b) ) ) & ( for m1, m2 being Morphism of b1 for a1, a2, a3 being Element of P for f1, f2 being Element of Funcs (Carr P) st m1 = [[a1,a2],f1] & m2 = [[a2,a3],f2] holds m2 (*) m1 = [[a1,a3],(f2 * f1)] ) ) ; ::_thesis: verum end; uniqueness for b1, b2 being strict with_triple-like_morphisms Category st the carrier of b1 = P & ( for a, b being Element of P for f being Element of Funcs (Carr P) st f in MonFuncs (a,b) holds [[a,b],f] is Morphism of b1 ) & ( for m being Morphism of b1 ex a, b being Element of P ex f being Element of Funcs (Carr P) st ( m = [[a,b],f] & f in MonFuncs (a,b) ) ) & ( for m1, m2 being Morphism of b1 for a1, a2, a3 being Element of P for f1, f2 being Element of Funcs (Carr P) st m1 = [[a1,a2],f1] & m2 = [[a2,a3],f2] holds m2 (*) m1 = [[a1,a3],(f2 * f1)] ) & the carrier of b2 = P & ( for a, b being Element of P for f being Element of Funcs (Carr P) st f in MonFuncs (a,b) holds [[a,b],f] is Morphism of b2 ) & ( for m being Morphism of b2 ex a, b being Element of P ex f being Element of Funcs (Carr P) st ( m = [[a,b],f] & f in MonFuncs (a,b) ) ) & ( for m1, m2 being Morphism of b2 for a1, a2, a3 being Element of P for f1, f2 being Element of Funcs (Carr P) st m1 = [[a1,a2],f1] & m2 = [[a2,a3],f2] holds m2 (*) m1 = [[a1,a3],(f2 * f1)] ) holds b1 = b2 proof deffunc H1( Element of Funcs (Carr P), Element of Funcs (Carr P)) -> set = \$1 * \$2; defpred S1[ Element of P, Element of P, Element of Funcs (Carr P)] means \$3 in MonFuncs (\$1,\$2); A6: now__::_thesis:_for_a_being_Element_of_P_ex_f_being_Element_of_Funcs_(Carr_P)_st_ (_S1[a,a,f]_&_(_for_b_being_Element_of_P for_g_being_Element_of_Funcs_(Carr_P)_holds_ (_(_S1[a,b,g]_implies_H1(g,f)_=_g_)_&_(_S1[b,a,g]_implies_H1(f,g)_=_g_)_)_)_) let a be Element of P; ::_thesis: ex f being Element of Funcs (Carr P) st ( S1[a,a,f] & ( for b being Element of P for g being Element of Funcs (Carr P) holds ( ( S1[a,b,g] implies H1(g,f) = g ) & ( S1[b,a,g] implies H1(f,g) = g ) ) ) ) thus ex f being Element of Funcs (Carr P) st ( S1[a,a,f] & ( for b being Element of P for g being Element of Funcs (Carr P) holds ( ( S1[a,b,g] implies H1(g,f) = g ) & ( S1[b,a,g] implies H1(f,g) = g ) ) ) ) ::_thesis: verum proof set f = id the carrier of a; A7: id the carrier of a in MonFuncs (a,a) by Th7; MonFuncs (a,a) c= Funcs (Carr P) by Th10; then reconsider f = id the carrier of a as Element of Funcs (Carr P) by A7; now__::_thesis:_for_b_being_Element_of_P for_g_being_Element_of_Funcs_(Carr_P)_holds_ (_(_g_in_MonFuncs_(a,b)_implies_g_*_f_=_g_)_&_(_g_in_MonFuncs_(b,a)_implies_f_*_g_=_g_)_) let b be Element of P; ::_thesis: for g being Element of Funcs (Carr P) holds ( ( g in MonFuncs (a,b) implies g * f = g ) & ( g in MonFuncs (b,a) implies f * g = g ) ) let g be Element of Funcs (Carr P); ::_thesis: ( ( g in MonFuncs (a,b) implies g * f = g ) & ( g in MonFuncs (b,a) implies f * g = g ) ) A8: ( g in MonFuncs (b,a) implies f * g = g ) proof assume g in MonFuncs (b,a) ; ::_thesis: f * g = g then ex g9 being Function of b,a st ( g9 = g & g9 in Funcs ( the carrier of b, the carrier of a) & g9 is monotone ) by Def6; then reconsider g = g as Function of the carrier of b, the carrier of a ; rng g c= the carrier of a ; hence f * g = g by RELAT_1:53; ::_thesis: verum end; ( g in MonFuncs (a,b) implies g * f = g ) proof assume g in MonFuncs (a,b) ; ::_thesis: g * f = g then ex g9 being Function of a,b st ( g9 = g & g9 in Funcs ( the carrier of a, the carrier of b) & g9 is monotone ) by Def6; then reconsider g = g as Function of the carrier of a, the carrier of b ; dom g = the carrier of a by FUNCT_2:def_1; hence g * f = g by RELAT_1:51; ::_thesis: verum end; hence ( ( g in MonFuncs (a,b) implies g * f = g ) & ( g in MonFuncs (b,a) implies f * g = g ) ) by A8; ::_thesis: verum end; hence ex f being Element of Funcs (Carr P) st ( S1[a,a,f] & ( for b being Element of P for g being Element of Funcs (Carr P) holds ( ( S1[a,b,g] implies H1(g,f) = g ) & ( S1[b,a,g] implies H1(f,g) = g ) ) ) ) by A7; ::_thesis: verum end; end; thus for C1, C2 being strict with_triple-like_morphisms Category st the carrier of C1 = P & ( for a, b being Element of P for f being Element of Funcs (Carr P) st S1[a,b,f] holds [[a,b],f] is Morphism of C1 ) & ( for m being Morphism of C1 ex a, b being Element of P ex f being Element of Funcs (Carr P) st ( m = [[a,b],f] & S1[a,b,f] ) ) & ( for m1, m2 being Morphism of C1 for a1, a2, a3 being Element of P for f1, f2 being Element of Funcs (Carr P) st m1 = [[a1,a2],f1] & m2 = [[a2,a3],f2] holds m2 (*) m1 = [[a1,a3],H1(f2,f1)] ) & the carrier of C2 = P & ( for a, b being Element of P for f being Element of Funcs (Carr P) st S1[a,b,f] holds [[a,b],f] is Morphism of C2 ) & ( for m being Morphism of C2 ex a, b being Element of P ex f being Element of Funcs (Carr P) st ( m = [[a,b],f] & S1[a,b,f] ) ) & ( for m1, m2 being Morphism of C2 for a1, a2, a3 being Element of P for f1, f2 being Element of Funcs (Carr P) st m1 = [[a1,a2],f1] & m2 = [[a2,a3],f2] holds m2 (*) m1 = [[a1,a3],H1(f2,f1)] ) holds C1 = C2 from CAT_5:sch_2(A6); ::_thesis: verum end; end; :: deftheorem defines POSCat ORDERS_3:def_8_:_ for P being non empty POSet_set for b2 being strict with_triple-like_morphisms Category holds ( b2 = POSCat P iff ( the carrier of b2 = P & ( for a, b being Element of P for f being Element of Funcs (Carr P) st f in MonFuncs (a,b) holds [[a,b],f] is Morphism of b2 ) & ( for m being Morphism of b2 ex a, b being Element of P ex f being Element of Funcs (Carr P) st ( m = [[a,b],f] & f in MonFuncs (a,b) ) ) & ( for m1, m2 being Morphism of b2 for a1, a2, a3 being Element of P for f1, f2 being Element of Funcs (Carr P) st m1 = [[a1,a2],f1] & m2 = [[a2,a3],f2] holds m2 (*) m1 = [[a1,a3],(f2 * f1)] ) ) ); begin scheme :: ORDERS_3:sch 1 AltCatEx{ F1() -> non empty set , F2( set , set ) -> functional set } : ex C being strict AltCatStr st ( the carrier of C = F1() & ( for i, j being Element of F1() holds ( the Arrows of C . (i,j) = F2(i,j) & ( for i, j, k being Element of F1() holds the Comp of C . (i,j,k) = FuncComp (F2(i,j),F2(j,k)) ) ) ) ) provided A1: for i, j, k being Element of F1() for f, g being Function st f in F2(i,j) & g in F2(j,k) holds g * f in F2(i,k) proof deffunc H1( set , set , set ) -> set = FuncComp (F2(\$1,\$2),F2(\$2,\$3)); consider M being ManySortedSet of [:F1(),F1():] such that A2: for i, j being Element of F1() holds M . (i,j) = F2(i,j) from ALTCAT_1:sch_2(); consider c being ManySortedSet of [:F1(),F1(),F1():] such that A3: for i, j, k being Element of F1() holds c . (i,j,k) = H1(i,j,k) from ALTCAT_1:sch_4(); c is Function-yielding proof let i be set ; :: according to FUNCOP_1:def_6 ::_thesis: ( not i in dom c or c . i is set ) assume i in dom c ; ::_thesis: c . i is set then i in [:F1(),F1(),F1():] ; then consider x1, x2, x3 being set such that A4: ( x1 in F1() & x2 in F1() & x3 in F1() ) and A5: i = [x1,x2,x3] by MCART_1:68; c . i = c . (x1,x2,x3) by A5, MULTOP_1:def_1 .= FuncComp (F2(x1,x2),F2(x2,x3)) by A3, A4 ; hence c . i is set ; ::_thesis: verum end; then reconsider c = c as ManySortedFunction of [:F1(),F1(),F1():] ; now__::_thesis:_for_i_being_set_st_i_in_[:F1(),F1(),F1():]_holds_ c_._i_is_Function_of_({|M,M|}_._i),({|M|}_._i) let i be set ; ::_thesis: ( i in [:F1(),F1(),F1():] implies c . i is Function of ({|M,M|} . i),({|M|} . i) ) assume i in [:F1(),F1(),F1():] ; ::_thesis: c . i is Function of ({|M,M|} . i),({|M|} . i) then consider x1, x2, x3 being set such that A6: x1 in F1() and A7: x2 in F1() and A8: x3 in F1() and A9: i = [x1,x2,x3] by MCART_1:68; M . (x1,x2) = F2(x1,x2) by A2, A6, A7; then A10: [:F2(x2,x3),F2(x1,x2):] = [:(M . (x2,x3)),(M . (x1,x2)):] by A2, A7, A8 .= {|M,M|} . (x1,x2,x3) by A6, A7, A8, ALTCAT_1:def_4 .= {|M,M|} . i by A9, MULTOP_1:def_1 ; A11: {|M|} . i = {|M|} . (x1,x2,x3) by A9, MULTOP_1:def_1 .= M . (x1,x3) by A6, A7, A8, ALTCAT_1:def_3 ; A12: now__::_thesis:_(_{|M,M|}_._i_<>_{}_implies_{|M|}_._i_<>_{}_) assume {|M,M|} . i <> {} ; ::_thesis: {|M|} . i <> {} then consider j being set such that A13: j in [:F2(x2,x3),F2(x1,x2):] by A10, XBOOLE_0:def_1; consider j1, j2 being set such that A14: j1 in F2(x2,x3) and A15: j2 in F2(x1,x2) and j = [j1,j2] by A13, ZFMISC_1:84; reconsider j2 = j2 as Function by A15; reconsider j1 = j1 as Function by A14; j1 * j2 in F2(x1,x3) by A1, A6, A7, A8, A14, A15; hence {|M|} . i <> {} by A2, A6, A8, A11; ::_thesis: verum end; A16: c . i = c . (x1,x2,x3) by A9, MULTOP_1:def_1 .= FuncComp (F2(x1,x2),F2(x2,x3)) by A3, A6, A7, A8 ; then reconsider ci = c . i as Function ; A17: dom ci = [:F2(x2,x3),F2(x1,x2):] by A16, PARTFUN1:def_2; rng (FuncComp (F2(x1,x2),F2(x2,x3))) c= F2(x1,x3) proof set F = FuncComp (F2(x1,x2),F2(x2,x3)); let i be set ; :: according to TARSKI:def_3 ::_thesis: ( not i in rng (FuncComp (F2(x1,x2),F2(x2,x3))) or i in F2(x1,x3) ) assume i in rng (FuncComp (F2(x1,x2),F2(x2,x3))) ; ::_thesis: i in F2(x1,x3) then consider j being set such that A18: j in dom (FuncComp (F2(x1,x2),F2(x2,x3))) and A19: i = (FuncComp (F2(x1,x2),F2(x2,x3))) . j by FUNCT_1:def_3; consider f, g being Function such that A20: j = [g,f] and A21: (FuncComp (F2(x1,x2),F2(x2,x3))) . j = g * f by A18, ALTCAT_1:def_9; ( g in F2(x2,x3) & f in F2(x1,x2) ) by A18, A20, ZFMISC_1:87; hence i in F2(x1,x3) by A1, A6, A7, A8, A19, A21; ::_thesis: verum end; then rng ci c= {|M|} . i by A2, A6, A8, A16, A11; hence c . i is Function of ({|M,M|} . i),({|M|} . i) by A17, A10, A12, FUNCT_2:def_1, RELSET_1:4; ::_thesis: verum end; then reconsider c = c as BinComp of M by PBOOLE:def_15; set C = AltCatStr(# F1(),M,c #); take AltCatStr(# F1(),M,c #) ; ::_thesis: ( the carrier of AltCatStr(# F1(),M,c #) = F1() & ( for i, j being Element of F1() holds ( the Arrows of AltCatStr(# F1(),M,c #) . (i,j) = F2(i,j) & ( for i, j, k being Element of F1() holds the Comp of AltCatStr(# F1(),M,c #) . (i,j,k) = FuncComp (F2(i,j),F2(j,k)) ) ) ) ) thus the carrier of AltCatStr(# F1(),M,c #) = F1() ; ::_thesis: for i, j being Element of F1() holds ( the Arrows of AltCatStr(# F1(),M,c #) . (i,j) = F2(i,j) & ( for i, j, k being Element of F1() holds the Comp of AltCatStr(# F1(),M,c #) . (i,j,k) = FuncComp (F2(i,j),F2(j,k)) ) ) let i, j be Element of F1(); ::_thesis: ( the Arrows of AltCatStr(# F1(),M,c #) . (i,j) = F2(i,j) & ( for i, j, k being Element of F1() holds the Comp of AltCatStr(# F1(),M,c #) . (i,j,k) = FuncComp (F2(i,j),F2(j,k)) ) ) thus the Arrows of AltCatStr(# F1(),M,c #) . (i,j) = F2(i,j) by A2; ::_thesis: for i, j, k being Element of F1() holds the Comp of AltCatStr(# F1(),M,c #) . (i,j,k) = FuncComp (F2(i,j),F2(j,k)) let i, j, k be Element of F1(); ::_thesis: the Comp of AltCatStr(# F1(),M,c #) . (i,j,k) = FuncComp (F2(i,j),F2(j,k)) thus the Comp of AltCatStr(# F1(),M,c #) . (i,j,k) = FuncComp (F2(i,j),F2(j,k)) by A3; ::_thesis: verum end; scheme :: ORDERS_3:sch 2 AltCatUniq{ F1() -> non empty set , F2( set , set ) -> functional set } : for C1, C2 being strict AltCatStr st the carrier of C1 = F1() & ( for i, j being Element of F1() holds ( the Arrows of C1 . (i,j) = F2(i,j) & ( for i, j, k being Element of F1() holds the Comp of C1 . (i,j,k) = FuncComp (F2(i,j),F2(j,k)) ) ) ) & the carrier of C2 = F1() & ( for i, j being Element of F1() holds ( the Arrows of C2 . (i,j) = F2(i,j) & ( for i, j, k being Element of F1() holds the Comp of C2 . (i,j,k) = FuncComp (F2(i,j),F2(j,k)) ) ) ) holds C1 = C2 proof let C1, C2 be strict AltCatStr ; ::_thesis: ( the carrier of C1 = F1() & ( for i, j being Element of F1() holds ( the Arrows of C1 . (i,j) = F2(i,j) & ( for i, j, k being Element of F1() holds the Comp of C1 . (i,j,k) = FuncComp (F2(i,j),F2(j,k)) ) ) ) & the carrier of C2 = F1() & ( for i, j being Element of F1() holds ( the Arrows of C2 . (i,j) = F2(i,j) & ( for i, j, k being Element of F1() holds the Comp of C2 . (i,j,k) = FuncComp (F2(i,j),F2(j,k)) ) ) ) implies C1 = C2 ) assume that A1: the carrier of C1 = F1() and A2: for i, j being Element of F1() holds ( the Arrows of C1 . (i,j) = F2(i,j) & ( for i, j, k being Element of F1() holds the Comp of C1 . (i,j,k) = FuncComp (F2(i,j),F2(j,k)) ) ) and A3: the carrier of C2 = F1() and A4: for i, j being Element of F1() holds ( the Arrows of C2 . (i,j) = F2(i,j) & ( for i, j, k being Element of F1() holds the Comp of C2 . (i,j,k) = FuncComp (F2(i,j),F2(j,k)) ) ) ; ::_thesis: C1 = C2 A5: now__::_thesis:_for_i,_j,_k_being_set_st_i_in_F1()_&_j_in_F1()_&_k_in_F1()_holds_ the_Comp_of_C1_._(i,j,k)_=_the_Comp_of_C2_._(i,j,k) let i, j, k be set ; ::_thesis: ( i in F1() & j in F1() & k in F1() implies the Comp of C1 . (i,j,k) = the Comp of C2 . (i,j,k) ) assume A6: ( i in F1() & j in F1() & k in F1() ) ; ::_thesis: the Comp of C1 . (i,j,k) = the Comp of C2 . (i,j,k) hence the Comp of C1 . (i,j,k) = FuncComp (F2(i,j),F2(j,k)) by A2 .= the Comp of C2 . (i,j,k) by A4, A6 ; ::_thesis: verum end; now__::_thesis:_for_i,_j_being_Element_of_F1()_holds_the_Arrows_of_C1_._(i,j)_=_the_Arrows_of_C2_._(i,j) let i, j be Element of F1(); ::_thesis: the Arrows of C1 . (i,j) = the Arrows of C2 . (i,j) thus the Arrows of C1 . (i,j) = F2(i,j) by A2 .= the Arrows of C2 . (i,j) by A4 ; ::_thesis: verum end; then the Arrows of C1 = the Arrows of C2 by A1, A3, ALTCAT_1:7; hence C1 = C2 by A1, A3, A5, ALTCAT_1:8; ::_thesis: verum end; definition let P be non empty POSet_set; func POSAltCat P -> strict AltCatStr means :Def9: :: ORDERS_3:def 9 ( the carrier of it = P & ( for i, j being Element of P holds ( the Arrows of it . (i,j) = MonFuncs (i,j) & ( for i, j, k being Element of P holds the Comp of it . (i,j,k) = FuncComp ((MonFuncs (i,j)),(MonFuncs (j,k))) ) ) ) ); existence ex b1 being strict AltCatStr st ( the carrier of b1 = P & ( for i, j being Element of P holds ( the Arrows of b1 . (i,j) = MonFuncs (i,j) & ( for i, j, k being Element of P holds the Comp of b1 . (i,j,k) = FuncComp ((MonFuncs (i,j)),(MonFuncs (j,k))) ) ) ) ) proof A1: for i, j, k being Element of P for f, g being Function st f in MonFuncs (i,j) & g in MonFuncs (j,k) holds g * f in MonFuncs (i,k) by Th6; thus ex C being strict AltCatStr st ( the carrier of C = P & ( for i, j being Element of P holds ( the Arrows of C . (i,j) = MonFuncs (i,j) & ( for i, j, k being Element of P holds the Comp of C . (i,j,k) = FuncComp ((MonFuncs (i,j)),(MonFuncs (j,k))) ) ) ) ) from ORDERS_3:sch_1(A1); ::_thesis: verum end; uniqueness for b1, b2 being strict AltCatStr st the carrier of b1 = P & ( for i, j being Element of P holds ( the Arrows of b1 . (i,j) = MonFuncs (i,j) & ( for i, j, k being Element of P holds the Comp of b1 . (i,j,k) = FuncComp ((MonFuncs (i,j)),(MonFuncs (j,k))) ) ) ) & the carrier of b2 = P & ( for i, j being Element of P holds ( the Arrows of b2 . (i,j) = MonFuncs (i,j) & ( for i, j, k being Element of P holds the Comp of b2 . (i,j,k) = FuncComp ((MonFuncs (i,j)),(MonFuncs (j,k))) ) ) ) holds b1 = b2 proof thus for C1, C2 being strict AltCatStr st the carrier of C1 = P & ( for i, j being Element of P holds ( the Arrows of C1 . (i,j) = MonFuncs (i,j) & ( for i, j, k being Element of P holds the Comp of C1 . (i,j,k) = FuncComp ((MonFuncs (i,j)),(MonFuncs (j,k))) ) ) ) & the carrier of C2 = P & ( for i, j being Element of P holds ( the Arrows of C2 . (i,j) = MonFuncs (i,j) & ( for i, j, k being Element of P holds the Comp of C2 . (i,j,k) = FuncComp ((MonFuncs (i,j)),(MonFuncs (j,k))) ) ) ) holds C1 = C2 from ORDERS_3:sch_2(); ::_thesis: verum end; end; :: deftheorem Def9 defines POSAltCat ORDERS_3:def_9_:_ for P being non empty POSet_set for b2 being strict AltCatStr holds ( b2 = POSAltCat P iff ( the carrier of b2 = P & ( for i, j being Element of P holds ( the Arrows of b2 . (i,j) = MonFuncs (i,j) & ( for i, j, k being Element of P holds the Comp of b2 . (i,j,k) = FuncComp ((MonFuncs (i,j)),(MonFuncs (j,k))) ) ) ) ) ); registration let P be non empty POSet_set; cluster POSAltCat P -> non empty transitive strict ; coherence ( POSAltCat P is transitive & not POSAltCat P is empty ) proof set A = POSAltCat P; thus POSAltCat P is transitive ::_thesis: not POSAltCat P is empty proof let o1, o2, o3 be object of (POSAltCat P); :: according to ALTCAT_1:def_2 ::_thesis: ( <^o1,o2^> = {} or <^o2,o3^> = {} or not <^o1,o3^> = {} ) reconsider o19 = o1, o29 = o2, o39 = o3 as Element of P by Def9; assume that A1: <^o1,o2^> <> {} and A2: <^o2,o3^> <> {} ; ::_thesis: not <^o1,o3^> = {} MonFuncs (o19,o29) <> {} by A1, Def9; then consider f being set such that A3: f in MonFuncs (o19,o29) by XBOOLE_0:def_1; MonFuncs (o29,o39) <> {} by A2, Def9; then consider g being set such that A4: g in MonFuncs (o29,o39) by XBOOLE_0:def_1; reconsider f = f, g = g as Function by A3, A4; g * f in MonFuncs (o19,o39) by A3, A4, Th6; hence not <^o1,o3^> = {} by Def9; ::_thesis: verum end; thus not POSAltCat P is empty by Def9; ::_thesis: verum end; end; registration let P be non empty POSet_set; cluster POSAltCat P -> strict associative with_units ; coherence ( POSAltCat P is associative & POSAltCat P is with_units ) proof set A = POSAltCat P; set G = the Arrows of (POSAltCat P); set C = the Comp of (POSAltCat P); thus the Comp of (POSAltCat P) is associative :: according to ALTCAT_1:def_15 ::_thesis: POSAltCat P is with_units proof let i, j, k, l be Element of (POSAltCat P); :: according to ALTCAT_1:def_5 ::_thesis: for b1, b2, b3 being set holds ( not b1 in the Arrows of (POSAltCat P) . (i,j) or not b2 in the Arrows of (POSAltCat P) . (j,k) or not b3 in the Arrows of (POSAltCat P) . (k,l) or ( the Comp of (POSAltCat P) . (i,k,l)) . (b3,(( the Comp of (POSAltCat P) . (i,j,k)) . (b2,b1))) = ( the Comp of (POSAltCat P) . (i,j,l)) . ((( the Comp of (POSAltCat P) . (j,k,l)) . (b3,b2)),b1) ) let f, g, h be set ; ::_thesis: ( not f in the Arrows of (POSAltCat P) . (i,j) or not g in the Arrows of (POSAltCat P) . (j,k) or not h in the Arrows of (POSAltCat P) . (k,l) or ( the Comp of (POSAltCat P) . (i,k,l)) . (h,(( the Comp of (POSAltCat P) . (i,j,k)) . (g,f))) = ( the Comp of (POSAltCat P) . (i,j,l)) . ((( the Comp of (POSAltCat P) . (j,k,l)) . (h,g)),f) ) reconsider i9 = i, j9 = j, k9 = k, l9 = l as Element of P by Def9; assume that A1: f in the Arrows of (POSAltCat P) . (i,j) and A2: g in the Arrows of (POSAltCat P) . (j,k) and A3: h in the Arrows of (POSAltCat P) . (k,l) ; ::_thesis: ( the Comp of (POSAltCat P) . (i,k,l)) . (h,(( the Comp of (POSAltCat P) . (i,j,k)) . (g,f))) = ( the Comp of (POSAltCat P) . (i,j,l)) . ((( the Comp of (POSAltCat P) . (j,k,l)) . (h,g)),f) A4: g in MonFuncs (j9,k9) by A2, Def9; A5: h in MonFuncs (k9,l9) by A3, Def9; A6: f in MonFuncs (i9,j9) by A1, Def9; then reconsider f9 = f, g9 = g, h9 = h as Function by A4, A5; A7: the Comp of (POSAltCat P) . (i,j,l) = FuncComp ((MonFuncs (i9,j9)),(MonFuncs (j9,l9))) by Def9; the Comp of (POSAltCat P) . (j,k,l) = FuncComp ((MonFuncs (j9,k9)),(MonFuncs (k9,l9))) by Def9; then A8: ( the Comp of (POSAltCat P) . (j,k,l)) . (h,g) = h9 * g9 by A4, A5, ALTCAT_1:11; the Comp of (POSAltCat P) . (i,j,k) = FuncComp ((MonFuncs (i9,j9)),(MonFuncs (j9,k9))) by Def9; then A9: ( the Comp of (POSAltCat P) . (i,j,k)) . (g,f) = g9 * f9 by A6, A4, ALTCAT_1:11; h9 * g9 in MonFuncs (j9,l9) by A4, A5, Th6; then A10: ( the Comp of (POSAltCat P) . (i,j,l)) . ((h9 * g9),f9) = (h9 * g9) * f9 by A6, A7, ALTCAT_1:11; A11: the Comp of (POSAltCat P) . (i,k,l) = FuncComp ((MonFuncs (i9,k9)),(MonFuncs (k9,l9))) by Def9; g9 * f9 in MonFuncs (i9,k9) by A6, A4, Th6; then ( the Comp of (POSAltCat P) . (i,k,l)) . (h,(g9 * f9)) = h9 * (g9 * f9) by A5, A11, ALTCAT_1:11; hence ( the Comp of (POSAltCat P) . (i,k,l)) . (h,(( the Comp of (POSAltCat P) . (i,j,k)) . (g,f))) = ( the Comp of (POSAltCat P) . (i,j,l)) . ((( the Comp of (POSAltCat P) . (j,k,l)) . (h,g)),f) by A9, A8, A10, RELAT_1:36; ::_thesis: verum end; thus the Comp of (POSAltCat P) is with_left_units :: according to ALTCAT_1:def_16 ::_thesis: the Comp of (POSAltCat P) is with_right_units proof let j be Element of (POSAltCat P); :: according to ALTCAT_1:def_7 ::_thesis: ex b1 being set st ( b1 in the Arrows of (POSAltCat P) . (j,j) & ( for b2 being Element of the carrier of (POSAltCat P) for b3 being set holds ( not b3 in the Arrows of (POSAltCat P) . (b2,j) or ( the Comp of (POSAltCat P) . (b2,j,j)) . (b1,b3) = b3 ) ) ) reconsider j9 = j as Element of P by Def9; take e = id the carrier of j9; ::_thesis: ( e in the Arrows of (POSAltCat P) . (j,j) & ( for b1 being Element of the carrier of (POSAltCat P) for b2 being set holds ( not b2 in the Arrows of (POSAltCat P) . (b1,j) or ( the Comp of (POSAltCat P) . (b1,j,j)) . (e,b2) = b2 ) ) ) the Arrows of (POSAltCat P) . (j,j) = MonFuncs (j9,j9) by Def9; hence e in the Arrows of (POSAltCat P) . (j,j) by Th7; ::_thesis: for b1 being Element of the carrier of (POSAltCat P) for b2 being set holds ( not b2 in the Arrows of (POSAltCat P) . (b1,j) or ( the Comp of (POSAltCat P) . (b1,j,j)) . (e,b2) = b2 ) let i be Element of (POSAltCat P); ::_thesis: for b1 being set holds ( not b1 in the Arrows of (POSAltCat P) . (i,j) or ( the Comp of (POSAltCat P) . (i,j,j)) . (e,b1) = b1 ) let f be set ; ::_thesis: ( not f in the Arrows of (POSAltCat P) . (i,j) or ( the Comp of (POSAltCat P) . (i,j,j)) . (e,f) = f ) reconsider i9 = i as Element of P by Def9; A12: the Comp of (POSAltCat P) . (i,j,j) = FuncComp ((MonFuncs (i9,j9)),(MonFuncs (j9,j9))) by Def9; assume f in the Arrows of (POSAltCat P) . (i,j) ; ::_thesis: ( the Comp of (POSAltCat P) . (i,j,j)) . (e,f) = f then A13: f in MonFuncs (i9,j9) by Def9; then consider f9 being Function of i9,j9 such that A14: f = f9 and f9 in Funcs ( the carrier of i9, the carrier of j9) and f9 is monotone by Def6; A15: e in MonFuncs (j9,j9) by Th7; then consider e9 being Function of j9,j9 such that A16: e = e9 and e9 in Funcs ( the carrier of j9, the carrier of j9) and e9 is monotone by Def6; rng f9 c= the carrier of j9 ; then e9 * f9 = f by A16, A14, RELAT_1:53; hence ( the Comp of (POSAltCat P) . (i,j,j)) . (e,f) = f by A15, A16, A13, A14, A12, ALTCAT_1:11; ::_thesis: verum end; thus the Comp of (POSAltCat P) is with_right_units ::_thesis: verum proof let i be Element of (POSAltCat P); :: according to ALTCAT_1:def_6 ::_thesis: ex b1 being set st ( b1 in the Arrows of (POSAltCat P) . (i,i) & ( for b2 being Element of the carrier of (POSAltCat P) for b3 being set holds ( not b3 in the Arrows of (POSAltCat P) . (i,b2) or ( the Comp of (POSAltCat P) . (i,i,b2)) . (b3,b1) = b3 ) ) ) reconsider i9 = i as Element of P by Def9; take e = id the carrier of i9; ::_thesis: ( e in the Arrows of (POSAltCat P) . (i,i) & ( for b1 being Element of the carrier of (POSAltCat P) for b2 being set holds ( not b2 in the Arrows of (POSAltCat P) . (i,b1) or ( the Comp of (POSAltCat P) . (i,i,b1)) . (b2,e) = b2 ) ) ) the Arrows of (POSAltCat P) . (i,i) = MonFuncs (i9,i9) by Def9; hence e in the Arrows of (POSAltCat P) . (i,i) by Th7; ::_thesis: for b1 being Element of the carrier of (POSAltCat P) for b2 being set holds ( not b2 in the Arrows of (POSAltCat P) . (i,b1) or ( the Comp of (POSAltCat P) . (i,i,b1)) . (b2,e) = b2 ) let j be Element of (POSAltCat P); ::_thesis: for b1 being set holds ( not b1 in the Arrows of (POSAltCat P) . (i,j) or ( the Comp of (POSAltCat P) . (i,i,j)) . (b1,e) = b1 ) let f be set ; ::_thesis: ( not f in the Arrows of (POSAltCat P) . (i,j) or ( the Comp of (POSAltCat P) . (i,i,j)) . (f,e) = f ) reconsider j9 = j as Element of P by Def9; A17: the Comp of (POSAltCat P) . (i,i,j) = FuncComp ((MonFuncs (i9,i9)),(MonFuncs (i9,j9))) by Def9; assume f in the Arrows of (POSAltCat P) . (i,j) ; ::_thesis: ( the Comp of (POSAltCat P) . (i,i,j)) . (f,e) = f then A18: f in MonFuncs (i9,j9) by Def9; then consider f9 being Function of i9,j9 such that A19: f = f9 and f9 in Funcs ( the carrier of i9, the carrier of j9) and f9 is monotone by Def6; A20: e in MonFuncs (i9,i9) by Th7; then consider e9 being Function of i9,i9 such that A21: e = e9 and e9 in Funcs ( the carrier of i9, the carrier of i9) and e9 is monotone by Def6; dom f9 = the carrier of i9 by FUNCT_2:def_1; then f9 * e9 = f by A21, A19, RELAT_1:52; hence ( the Comp of (POSAltCat P) . (i,i,j)) . (f,e) = f by A20, A21, A18, A19, A17, ALTCAT_1:11; ::_thesis: verum end; end; end; theorem :: ORDERS_3:12 for P being non empty POSet_set for o1, o2 being object of (POSAltCat P) for A, B being Element of P st o1 = A & o2 = B holds <^o1,o2^> c= Funcs ( the carrier of A, the carrier of B) proof let P be non empty POSet_set; ::_thesis: for o1, o2 being object of (POSAltCat P) for A, B being Element of P st o1 = A & o2 = B holds <^o1,o2^> c= Funcs ( the carrier of A, the carrier of B) let o1, o2 be object of (POSAltCat P); ::_thesis: for A, B being Element of P st o1 = A & o2 = B holds <^o1,o2^> c= Funcs ( the carrier of A, the carrier of B) let A, B be Element of P; ::_thesis: ( o1 = A & o2 = B implies <^o1,o2^> c= Funcs ( the carrier of A, the carrier of B) ) assume A1: ( o1 = A & o2 = B ) ; ::_thesis: <^o1,o2^> c= Funcs ( the carrier of A, the carrier of B) let x be set ; :: according to TARSKI:def_3 ::_thesis: ( not x in <^o1,o2^> or x in Funcs ( the carrier of A, the carrier of B) ) assume x in <^o1,o2^> ; ::_thesis: x in Funcs ( the carrier of A, the carrier of B) then x in MonFuncs (A,B) by A1, Def9; then ex f being Function of A,B st ( f = x & f in Funcs ( the carrier of A, the carrier of B) & f is monotone ) by Def6; hence x in Funcs ( the carrier of A, the carrier of B) ; ::_thesis: verum end;