:: COH_SP semantic presentation begin definition let IT be set ; attrIT is binary_complete means :Def1: :: COH_SP:def 1 for A being set st A c= IT & ( for a, b being set st a in A & b in A holds a \/ b in IT ) holds union A in IT; end; :: deftheorem Def1 defines binary_complete COH_SP:def_1_:_ for IT being set holds ( IT is binary_complete iff for A being set st A c= IT & ( for a, b being set st a in A & b in A holds a \/ b in IT ) holds union A in IT ); registration cluster non empty subset-closed binary_complete for set ; existence ex b1 being set st ( b1 is subset-closed & b1 is binary_complete & not b1 is empty ) proof take X = {{}}; ::_thesis: ( X is subset-closed & X is binary_complete & not X is empty ) thus for a, b being set st a in X & b c= a holds b in X :: according to CLASSES1:def_1 ::_thesis: ( X is binary_complete & not X is empty ) proof let a, b be set ; ::_thesis: ( a in X & b c= a implies b in X ) assume that A1: a in X and A2: b c= a ; ::_thesis: b in X a = {} by A1, TARSKI:def_1; hence b in X by A1, A2; ::_thesis: verum end; thus for A being set st A c= X & ( for a, b being set st a in A & b in A holds a \/ b in X ) holds union A in X :: according to COH_SP:def_1 ::_thesis: not X is empty proof let A be set ; ::_thesis: ( A c= X & ( for a, b being set st a in A & b in A holds a \/ b in X ) implies union A in X ) assume that A3: A c= X and for a, b being set st a in A & b in A holds a \/ b in X ; ::_thesis: union A in X now__::_thesis:_union_A_in_X percases ( A = {} or A = {{}} ) by A3, ZFMISC_1:33; suppose A = {} ; ::_thesis: union A in X hence union A in X by TARSKI:def_1, ZFMISC_1:2; ::_thesis: verum end; suppose A = {{}} ; ::_thesis: union A in X then union A = {} by ZFMISC_1:25; hence union A in X by TARSKI:def_1; ::_thesis: verum end; end; end; hence union A in X ; ::_thesis: verum end; thus not X is empty ; ::_thesis: verum end; end; definition mode Coherence_Space is non empty subset-closed binary_complete set ; end; theorem :: COH_SP:1 for C being Coherence_Space holds {} in C proof let C be Coherence_Space; ::_thesis: {} in C ( {} c= C & ( for a, b being set st a in {} & b in {} holds a \/ b in C ) ) by XBOOLE_1:2; hence {} in C by Def1, ZFMISC_1:2; ::_thesis: verum end; theorem Th2: :: COH_SP:2 for X being set holds bool X is Coherence_Space proof let X be set ; ::_thesis: bool X is Coherence_Space A1: for A being set st A c= bool X & ( for a, b being set st a in A & b in A holds a \/ b in bool X ) holds union A in bool X proof let A be set ; ::_thesis: ( A c= bool X & ( for a, b being set st a in A & b in A holds a \/ b in bool X ) implies union A in bool X ) assume that A2: A c= bool X and for a, b being set st a in A & b in A holds a \/ b in bool X ; ::_thesis: union A in bool X for a being set st a in A holds a c= X by A2; then union A c= X by ZFMISC_1:76; hence union A in bool X ; ::_thesis: verum end; for a, b being set st a in bool X & b c= a holds b in bool X proof let a, b be set ; ::_thesis: ( a in bool X & b c= a implies b in bool X ) assume ( a in bool X & b c= a ) ; ::_thesis: b in bool X then b c= X by XBOOLE_1:1; hence b in bool X ; ::_thesis: verum end; hence bool X is Coherence_Space by A1, Def1, CLASSES1:def_1; ::_thesis: verum end; theorem :: COH_SP:3 {{}} is Coherence_Space by Th2, ZFMISC_1:1; theorem Th4: :: COH_SP:4 for x being set for C being Coherence_Space st x in union C holds {x} in C proof let x be set ; ::_thesis: for C being Coherence_Space st x in union C holds {x} in C let C be Coherence_Space; ::_thesis: ( x in union C implies {x} in C ) assume x in union C ; ::_thesis: {x} in C then consider X being set such that A1: x in X and A2: X in C by TARSKI:def_4; {x} c= X by A1, ZFMISC_1:31; hence {x} in C by A2, CLASSES1:def_1; ::_thesis: verum end; definition let C be Coherence_Space; func Web C -> Tolerance of (union C) means :Def2: :: COH_SP:def 2 for x, y being set holds ( [x,y] in it iff ex X being set st ( X in C & x in X & y in X ) ); existence ex b1 being Tolerance of (union C) st for x, y being set holds ( [x,y] in b1 iff ex X being set st ( X in C & x in X & y in X ) ) proof defpred S1[ set , set ] means ex X being set st ( X in C & \$1 in X & \$2 in X ); A1: for x being set st x in union C holds S1[x,x] proof let x be set ; ::_thesis: ( x in union C implies S1[x,x] ) assume A2: x in union C ; ::_thesis: S1[x,x] take {x} ; ::_thesis: ( {x} in C & x in {x} & x in {x} ) thus ( {x} in C & x in {x} & x in {x} ) by A2, Th4, TARSKI:def_1; ::_thesis: verum end; A3: for x, y being set st x in union C & y in union C & S1[x,y] holds S1[y,x] ; consider T being Tolerance of (union C) such that A4: for x, y being set st x in union C & y in union C holds ( [x,y] in T iff S1[x,y] ) from TOLER_1:sch_1(A1, A3); take T ; ::_thesis: for x, y being set holds ( [x,y] in T iff ex X being set st ( X in C & x in X & y in X ) ) let x, y be set ; ::_thesis: ( [x,y] in T iff ex X being set st ( X in C & x in X & y in X ) ) thus ( [x,y] in T implies ex X being set st ( X in C & x in X & y in X ) ) ::_thesis: ( ex X being set st ( X in C & x in X & y in X ) implies [x,y] in T ) proof assume A5: [x,y] in T ; ::_thesis: ex X being set st ( X in C & x in X & y in X ) then ( x in union C & y in union C ) by ZFMISC_1:87; hence ex X being set st ( X in C & x in X & y in X ) by A4, A5; ::_thesis: verum end; given X being set such that A6: ( X in C & x in X & y in X ) ; ::_thesis: [x,y] in T ( x in union C & y in union C ) by A6, TARSKI:def_4; hence [x,y] in T by A4, A6; ::_thesis: verum end; uniqueness for b1, b2 being Tolerance of (union C) st ( for x, y being set holds ( [x,y] in b1 iff ex X being set st ( X in C & x in X & y in X ) ) ) & ( for x, y being set holds ( [x,y] in b2 iff ex X being set st ( X in C & x in X & y in X ) ) ) holds b1 = b2 by TOLER_1:25; end; :: deftheorem Def2 defines Web COH_SP:def_2_:_ for C being Coherence_Space for b2 being Tolerance of (union C) holds ( b2 = Web C iff for x, y being set holds ( [x,y] in b2 iff ex X being set st ( X in C & x in X & y in X ) ) ); theorem Th5: :: COH_SP:5 for C being Coherence_Space for T being Tolerance of (union C) holds ( T = Web C iff for x, y being set holds ( [x,y] in T iff {x,y} in C ) ) proof let C be Coherence_Space; ::_thesis: for T being Tolerance of (union C) holds ( T = Web C iff for x, y being set holds ( [x,y] in T iff {x,y} in C ) ) let T be Tolerance of (union C); ::_thesis: ( T = Web C iff for x, y being set holds ( [x,y] in T iff {x,y} in C ) ) thus ( T = Web C implies for x, y being set holds ( [x,y] in T iff {x,y} in C ) ) ::_thesis: ( ( for x, y being set holds ( [x,y] in T iff {x,y} in C ) ) implies T = Web C ) proof assume A1: T = Web C ; ::_thesis: for x, y being set holds ( [x,y] in T iff {x,y} in C ) let x, y be set ; ::_thesis: ( [x,y] in T iff {x,y} in C ) thus ( [x,y] in T implies {x,y} in C ) ::_thesis: ( {x,y} in C implies [x,y] in T ) proof assume [x,y] in T ; ::_thesis: {x,y} in C then consider X being set such that A2: X in C and A3: ( x in X & y in X ) by A1, Def2; {x,y} c= X by A3, ZFMISC_1:32; hence {x,y} in C by A2, CLASSES1:def_1; ::_thesis: verum end; A4: ( x in {x,y} & y in {x,y} ) by TARSKI:def_2; assume {x,y} in C ; ::_thesis: [x,y] in T hence [x,y] in T by A1, A4, Def2; ::_thesis: verum end; assume A5: for x, y being set holds ( [x,y] in T iff {x,y} in C ) ; ::_thesis: T = Web C for x, y being set holds ( [x,y] in T iff ex X being set st ( X in C & x in X & y in X ) ) proof let x, y be set ; ::_thesis: ( [x,y] in T iff ex X being set st ( X in C & x in X & y in X ) ) thus ( [x,y] in T implies ex X being set st ( X in C & x in X & y in X ) ) ::_thesis: ( ex X being set st ( X in C & x in X & y in X ) implies [x,y] in T ) proof assume A6: [x,y] in T ; ::_thesis: ex X being set st ( X in C & x in X & y in X ) take {x,y} ; ::_thesis: ( {x,y} in C & x in {x,y} & y in {x,y} ) thus ( {x,y} in C & x in {x,y} & y in {x,y} ) by A5, A6, TARSKI:def_2; ::_thesis: verum end; given X being set such that A7: X in C and A8: ( x in X & y in X ) ; ::_thesis: [x,y] in T {x,y} c= X by A8, ZFMISC_1:32; then {x,y} in C by A7, CLASSES1:def_1; hence [x,y] in T by A5; ::_thesis: verum end; hence T = Web C by Def2; ::_thesis: verum end; theorem Th6: :: COH_SP:6 for a being set for C being Coherence_Space holds ( a in C iff for x, y being set st x in a & y in a holds {x,y} in C ) proof let a be set ; ::_thesis: for C being Coherence_Space holds ( a in C iff for x, y being set st x in a & y in a holds {x,y} in C ) let C be Coherence_Space; ::_thesis: ( a in C iff for x, y being set st x in a & y in a holds {x,y} in C ) defpred S1[ set , set ] means {\$1} = \$2; thus ( a in C implies for x, y being set st x in a & y in a holds {x,y} in C ) ::_thesis: ( ( for x, y being set st x in a & y in a holds {x,y} in C ) implies a in C ) proof assume A1: a in C ; ::_thesis: for x, y being set st x in a & y in a holds {x,y} in C let x, y be set ; ::_thesis: ( x in a & y in a implies {x,y} in C ) assume ( x in a & y in a ) ; ::_thesis: {x,y} in C then {x,y} c= a by ZFMISC_1:32; hence {x,y} in C by A1, CLASSES1:def_1; ::_thesis: verum end; A2: for x, y, z being set st S1[x,y] & S1[x,z] holds y = z ; consider X being set such that A3: for x being set holds ( x in X iff ex y being set st ( y in a & S1[y,x] ) ) from TARSKI:sch_1(A2); assume A4: for x, y being set st x in a & y in a holds {x,y} in C ; ::_thesis: a in C A5: for b, c being set st b in X & c in X holds b \/ c in C proof let b, c be set ; ::_thesis: ( b in X & c in X implies b \/ c in C ) assume that A6: b in X and A7: c in X ; ::_thesis: b \/ c in C consider z being set such that A8: z in a and A9: {z} = c by A3, A7; consider y being set such that A10: y in a and A11: {y} = b by A3, A6; {y,z} in C by A4, A10, A8; hence b \/ c in C by A11, A9, ENUMSET1:1; ::_thesis: verum end; A12: union X = a proof thus union X c= a :: according to XBOOLE_0:def_10 ::_thesis: a c= union X proof let x be set ; :: according to TARSKI:def_3 ::_thesis: ( not x in union X or x in a ) assume x in union X ; ::_thesis: x in a then consider Z being set such that A13: x in Z and A14: Z in X by TARSKI:def_4; ex y being set st ( y in a & Z = {y} ) by A3, A14; hence x in a by A13, TARSKI:def_1; ::_thesis: verum end; let x be set ; :: according to TARSKI:def_3 ::_thesis: ( not x in a or x in union X ) assume x in a ; ::_thesis: x in union X then A15: {x} in X by A3; x in {x} by TARSKI:def_1; hence x in union X by A15, TARSKI:def_4; ::_thesis: verum end; X c= C proof let x be set ; :: according to TARSKI:def_3 ::_thesis: ( not x in X or x in C ) assume x in X ; ::_thesis: x in C then consider y being set such that A16: y in a and A17: {y} = x by A3; {y,y} in C by A4, A16; hence x in C by A17, ENUMSET1:29; ::_thesis: verum end; hence a in C by A5, A12, Def1; ::_thesis: verum end; theorem Th7: :: COH_SP:7 for a being set for C being Coherence_Space holds ( a in C iff for x, y being set st x in a & y in a holds [x,y] in Web C ) proof let a be set ; ::_thesis: for C being Coherence_Space holds ( a in C iff for x, y being set st x in a & y in a holds [x,y] in Web C ) let C be Coherence_Space; ::_thesis: ( a in C iff for x, y being set st x in a & y in a holds [x,y] in Web C ) thus ( a in C implies for x, y being set st x in a & y in a holds [x,y] in Web C ) ::_thesis: ( ( for x, y being set st x in a & y in a holds [x,y] in Web C ) implies a in C ) proof assume A1: a in C ; ::_thesis: for x, y being set st x in a & y in a holds [x,y] in Web C let x, y be set ; ::_thesis: ( x in a & y in a implies [x,y] in Web C ) assume ( x in a & y in a ) ; ::_thesis: [x,y] in Web C then {x,y} in C by A1, Th6; hence [x,y] in Web C by Th5; ::_thesis: verum end; assume A2: for x, y being set st x in a & y in a holds [x,y] in Web C ; ::_thesis: a in C now__::_thesis:_for_x,_y_being_set_st_x_in_a_&_y_in_a_holds_ {x,y}_in_C let x, y be set ; ::_thesis: ( x in a & y in a implies {x,y} in C ) assume ( x in a & y in a ) ; ::_thesis: {x,y} in C then [x,y] in Web C by A2; hence {x,y} in C by Th5; ::_thesis: verum end; hence a in C by Th6; ::_thesis: verum end; theorem :: COH_SP:8 for a being set for C being Coherence_Space st ( for x, y being set st x in a & y in a holds {x,y} in C ) holds a c= union C proof let a be set ; ::_thesis: for C being Coherence_Space st ( for x, y being set st x in a & y in a holds {x,y} in C ) holds a c= union C let C be Coherence_Space; ::_thesis: ( ( for x, y being set st x in a & y in a holds {x,y} in C ) implies a c= union C ) assume A1: for x, y being set st x in a & y in a holds {x,y} in C ; ::_thesis: a c= union C let x be set ; :: according to TARSKI:def_3 ::_thesis: ( not x in a or x in union C ) assume x in a ; ::_thesis: x in union C then {x,x} in C by A1; then A2: {x} in C by ENUMSET1:29; x in {x} by TARSKI:def_1; hence x in union C by A2, TARSKI:def_4; ::_thesis: verum end; theorem :: COH_SP:9 for C, D being Coherence_Space st Web C = Web D holds C = D proof let C, D be Coherence_Space; ::_thesis: ( Web C = Web D implies C = D ) assume A1: Web C = Web D ; ::_thesis: C = D thus C c= D :: according to XBOOLE_0:def_10 ::_thesis: D c= C proof let x be set ; :: according to TARSKI:def_3 ::_thesis: ( not x in C or x in D ) assume x in C ; ::_thesis: x in D then for z, y being set st z in x & y in x holds [z,y] in Web D by A1, Th7; hence x in D by Th7; ::_thesis: verum end; let x be set ; :: according to TARSKI:def_3 ::_thesis: ( not x in D or x in C ) assume x in D ; ::_thesis: x in C then for z, y being set st z in x & y in x holds [z,y] in Web C by A1, Th7; hence x in C by Th7; ::_thesis: verum end; theorem :: COH_SP:10 for C being Coherence_Space st union C in C holds C = bool (union C) proof let C be Coherence_Space; ::_thesis: ( union C in C implies C = bool (union C) ) assume A1: union C in C ; ::_thesis: C = bool (union C) thus C c= bool (union C) by ZFMISC_1:82; :: according to XBOOLE_0:def_10 ::_thesis: bool (union C) c= C let x be set ; :: according to TARSKI:def_3 ::_thesis: ( not x in bool (union C) or x in C ) assume x in bool (union C) ; ::_thesis: x in C hence x in C by A1, CLASSES1:def_1; ::_thesis: verum end; theorem :: COH_SP:11 for C being Coherence_Space st C = bool (union C) holds Web C = Total (union C) proof let C be Coherence_Space; ::_thesis: ( C = bool (union C) implies Web C = Total (union C) ) reconsider t = Total (union C) as Tolerance of (union C) ; assume A1: C = bool (union C) ; ::_thesis: Web C = Total (union C) now__::_thesis:_for_x,_y_being_set_holds_ (_(_[x,y]_in_t_implies_{x,y}_in_C_)_&_(_{x,y}_in_C_implies_[x,y]_in_t_)_) let x, y be set ; ::_thesis: ( ( [x,y] in t implies {x,y} in C ) & ( {x,y} in C implies [x,y] in t ) ) thus ( [x,y] in t implies {x,y} in C ) ::_thesis: ( {x,y} in C implies [x,y] in t ) proof assume [x,y] in t ; ::_thesis: {x,y} in C then A2: ( x in union C & y in union C ) by ZFMISC_1:87; {x,y} c= union C proof let z be set ; :: according to TARSKI:def_3 ::_thesis: ( not z in {x,y} or z in union C ) assume z in {x,y} ; ::_thesis: z in union C hence z in union C by A2, TARSKI:def_2; ::_thesis: verum end; hence {x,y} in C by A1; ::_thesis: verum end; assume {x,y} in C ; ::_thesis: [x,y] in t then ( x in union C & y in union C ) by A1, ZFMISC_1:32; hence [x,y] in t by TOLER_1:2; ::_thesis: verum end; hence Web C = Total (union C) by Th5; ::_thesis: verum end; definition let X be set ; let E be Tolerance of X; func CohSp E -> Coherence_Space means :Def3: :: COH_SP:def 3 for a being set holds ( a in it iff for x, y being set st x in a & y in a holds [x,y] in E ); existence ex b1 being Coherence_Space st for a being set holds ( a in b1 iff for x, y being set st x in a & y in a holds [x,y] in E ) proof defpred S1[ set ] means for x, y being set st x in \$1 & y in \$1 holds [x,y] in E; consider Z being set such that A1: for x being set holds ( x in Z iff ( x in bool X & S1[x] ) ) from XBOOLE_0:sch_1(); A2: for A being set st A c= Z & ( for a, b being set st a in A & b in A holds a \/ b in Z ) holds union A in Z proof let A be set ; ::_thesis: ( A c= Z & ( for a, b being set st a in A & b in A holds a \/ b in Z ) implies union A in Z ) assume that A3: A c= Z and A4: for a, b being set st a in A & b in A holds a \/ b in Z ; ::_thesis: union A in Z A5: now__::_thesis:_for_x,_y_being_set_st_x_in_union_A_&_y_in_union_A_holds_ [x,y]_in_E let x, y be set ; ::_thesis: ( x in union A & y in union A implies [x,y] in E ) assume that A6: x in union A and A7: y in union A ; ::_thesis: [x,y] in E consider Y1 being set such that A8: y in Y1 and A9: Y1 in A by A7, TARSKI:def_4; consider X1 being set such that A10: x in X1 and A11: X1 in A by A6, TARSKI:def_4; A12: x in X1 \/ Y1 by A10, XBOOLE_0:def_3; A13: y in X1 \/ Y1 by A8, XBOOLE_0:def_3; X1 \/ Y1 in Z by A4, A11, A9; hence [x,y] in E by A1, A12, A13; ::_thesis: verum end; now__::_thesis:_for_a_being_set_st_a_in_A_holds_ a_c=_X let a be set ; ::_thesis: ( a in A implies a c= X ) assume a in A ; ::_thesis: a c= X then a in bool X by A1, A3; hence a c= X ; ::_thesis: verum end; then union A c= X by ZFMISC_1:76; hence union A in Z by A1, A5; ::_thesis: verum end; A14: for a, b being set st a in Z & b c= a holds b in Z proof let a, b be set ; ::_thesis: ( a in Z & b c= a implies b in Z ) assume that A15: a in Z and A16: b c= a ; ::_thesis: b in Z a in bool X by A1, A15; then A17: b c= X by A16, XBOOLE_1:1; for x, y being set st x in b & y in b holds [x,y] in E by A1, A15, A16; hence b in Z by A1, A17; ::_thesis: verum end; ( S1[ {} ] & {} c= X ) by XBOOLE_1:2; then reconsider Z = Z as Coherence_Space by A1, A14, A2, Def1, CLASSES1:def_1; take Z ; ::_thesis: for a being set holds ( a in Z iff for x, y being set st x in a & y in a holds [x,y] in E ) let a be set ; ::_thesis: ( a in Z iff for x, y being set st x in a & y in a holds [x,y] in E ) thus ( a in Z implies for x, y being set st x in a & y in a holds [x,y] in E ) by A1; ::_thesis: ( ( for x, y being set st x in a & y in a holds [x,y] in E ) implies a in Z ) assume A18: for x, y being set st x in a & y in a holds [x,y] in E ; ::_thesis: a in Z then a c= X by TOLER_1:18, TOLER_1:def_1; hence a in Z by A1, A18; ::_thesis: verum end; uniqueness for b1, b2 being Coherence_Space st ( for a being set holds ( a in b1 iff for x, y being set st x in a & y in a holds [x,y] in E ) ) & ( for a being set holds ( a in b2 iff for x, y being set st x in a & y in a holds [x,y] in E ) ) holds b1 = b2 proof let C, D be Coherence_Space; ::_thesis: ( ( for a being set holds ( a in C iff for x, y being set st x in a & y in a holds [x,y] in E ) ) & ( for a being set holds ( a in D iff for x, y being set st x in a & y in a holds [x,y] in E ) ) implies C = D ) assume that A19: for a being set holds ( a in C iff for x, y being set st x in a & y in a holds [x,y] in E ) and A20: for a being set holds ( a in D iff for x, y being set st x in a & y in a holds [x,y] in E ) ; ::_thesis: C = D thus C c= D :: according to XBOOLE_0:def_10 ::_thesis: D c= C proof let x be set ; :: according to TARSKI:def_3 ::_thesis: ( not x in C or x in D ) assume x in C ; ::_thesis: x in D then for z, y being set st z in x & y in x holds [z,y] in E by A19; hence x in D by A20; ::_thesis: verum end; let x be set ; :: according to TARSKI:def_3 ::_thesis: ( not x in D or x in C ) assume x in D ; ::_thesis: x in C then for z, y being set st z in x & y in x holds [z,y] in E by A20; hence x in C by A19; ::_thesis: verum end; end; :: deftheorem Def3 defines CohSp COH_SP:def_3_:_ for X being set for E being Tolerance of X for b3 being Coherence_Space holds ( b3 = CohSp E iff for a being set holds ( a in b3 iff for x, y being set st x in a & y in a holds [x,y] in E ) ); theorem :: COH_SP:12 for X being set for E being Tolerance of X holds Web (CohSp E) = E proof let X be set ; ::_thesis: for E being Tolerance of X holds Web (CohSp E) = E let E be Tolerance of X; ::_thesis: Web (CohSp E) = E now__::_thesis:_for_x,_y_being_set_holds_ (_(_[x,y]_in_Web_(CohSp_E)_implies_[x,y]_in_E_)_&_(_[x,y]_in_E_implies_[x,y]_in_Web_(CohSp_E)_)_) let x, y be set ; ::_thesis: ( ( [x,y] in Web (CohSp E) implies [x,y] in E ) & ( [x,y] in E implies [x,y] in Web (CohSp E) ) ) thus ( [x,y] in Web (CohSp E) implies [x,y] in E ) ::_thesis: ( [x,y] in E implies [x,y] in Web (CohSp E) ) proof assume [x,y] in Web (CohSp E) ; ::_thesis: [x,y] in E then A1: {x,y} in CohSp E by Th5; ( x in {x,y} & y in {x,y} ) by TARSKI:def_2; hence [x,y] in E by A1, Def3; ::_thesis: verum end; assume A2: [x,y] in E ; ::_thesis: [x,y] in Web (CohSp E) then A3: ( x in X & y in X ) by ZFMISC_1:87; for u, v being set st u in {x,y} & v in {x,y} holds [u,v] in E proof let u, v be set ; ::_thesis: ( u in {x,y} & v in {x,y} implies [u,v] in E ) assume that A4: u in {x,y} and A5: v in {x,y} ; ::_thesis: [u,v] in E A6: ( v = x or v = y ) by A5, TARSKI:def_2; ( u = x or u = y ) by A4, TARSKI:def_2; hence [u,v] in E by A2, A3, A6, EQREL_1:6, TOLER_1:7; ::_thesis: verum end; then {x,y} in CohSp E by Def3; hence [x,y] in Web (CohSp E) by Th5; ::_thesis: verum end; hence Web (CohSp E) = E by RELAT_1:def_2; ::_thesis: verum end; theorem :: COH_SP:13 for C being Coherence_Space holds CohSp (Web C) = C proof let C be Coherence_Space; ::_thesis: CohSp (Web C) = C thus CohSp (Web C) c= C :: according to XBOOLE_0:def_10 ::_thesis: C c= CohSp (Web C) proof let x be set ; :: according to TARSKI:def_3 ::_thesis: ( not x in CohSp (Web C) or x in C ) assume x in CohSp (Web C) ; ::_thesis: x in C then for y, z being set st y in x & z in x holds [y,z] in Web C by Def3; hence x in C by Th7; ::_thesis: verum end; let x be set ; :: according to TARSKI:def_3 ::_thesis: ( not x in C or x in CohSp (Web C) ) assume x in C ; ::_thesis: x in CohSp (Web C) then for y, z being set st y in x & z in x holds [y,z] in Web C by Th7; hence x in CohSp (Web C) by Def3; ::_thesis: verum end; theorem Th14: :: COH_SP:14 for X, a being set for E being Tolerance of X holds ( a in CohSp E iff a is TolSet of E ) proof let X, a be set ; ::_thesis: for E being Tolerance of X holds ( a in CohSp E iff a is TolSet of E ) let E be Tolerance of X; ::_thesis: ( a in CohSp E iff a is TolSet of E ) thus ( a in CohSp E implies a is TolSet of E ) ::_thesis: ( a is TolSet of E implies a in CohSp E ) proof assume a in CohSp E ; ::_thesis: a is TolSet of E then for x, y being set st x in a & y in a holds [x,y] in E by Def3; hence a is TolSet of E by TOLER_1:def_1; ::_thesis: verum end; assume a is TolSet of E ; ::_thesis: a in CohSp E then for x, y being set st x in a & y in a holds [x,y] in E by TOLER_1:def_1; hence a in CohSp E by Def3; ::_thesis: verum end; theorem :: COH_SP:15 for X being set for E being Tolerance of X holds CohSp E = TolSets E proof let X be set ; ::_thesis: for E being Tolerance of X holds CohSp E = TolSets E let E be Tolerance of X; ::_thesis: CohSp E = TolSets E thus CohSp E c= TolSets E :: according to XBOOLE_0:def_10 ::_thesis: TolSets E c= CohSp E proof let x be set ; :: according to TARSKI:def_3 ::_thesis: ( not x in CohSp E or x in TolSets E ) assume x in CohSp E ; ::_thesis: x in TolSets E then x is TolSet of E by Th14; hence x in TolSets E by TOLER_1:def_3; ::_thesis: verum end; let x be set ; :: according to TARSKI:def_3 ::_thesis: ( not x in TolSets E or x in CohSp E ) assume x in TolSets E ; ::_thesis: x in CohSp E then x is TolSet of E by TOLER_1:def_3; hence x in CohSp E by Th14; ::_thesis: verum end; begin definition let X be set ; func CSp X -> set equals :: COH_SP:def 4 { x where x is Subset-Family of X : x is Coherence_Space } ; coherence { x where x is Subset-Family of X : x is Coherence_Space } is set ; end; :: deftheorem defines CSp COH_SP:def_4_:_ for X being set holds CSp X = { x where x is Subset-Family of X : x is Coherence_Space } ; registration let X be set ; cluster CSp X -> non empty ; coherence not CSp X is empty proof reconsider b = bool X as Subset-Family of X ; set F = { x where x is Subset-Family of X : x is Coherence_Space } ; b is Coherence_Space by Th2; then b in { x where x is Subset-Family of X : x is Coherence_Space } ; hence not CSp X is empty ; ::_thesis: verum end; end; registration let X be set ; cluster -> non empty subset-closed binary_complete for Element of CSp X; coherence for b1 being Element of CSp X holds ( b1 is subset-closed & b1 is binary_complete & not b1 is empty ) proof let C be Element of CSp X; ::_thesis: ( C is subset-closed & C is binary_complete & not C is empty ) C in { x where x is Subset-Family of X : x is Coherence_Space } ; then ex x being Subset-Family of X st ( C = x & x is Coherence_Space ) ; hence ( C is subset-closed & C is binary_complete & not C is empty ) ; ::_thesis: verum end; end; theorem Th16: :: COH_SP:16 for X, x, y being set for C being Element of CSp X st {x,y} in C holds ( x in union C & y in union C ) proof let X, x, y be set ; ::_thesis: for C being Element of CSp X st {x,y} in C holds ( x in union C & y in union C ) let C be Element of CSp X; ::_thesis: ( {x,y} in C implies ( x in union C & y in union C ) ) A1: ( {x} c= {x,y} & {y} c= {x,y} ) by ZFMISC_1:7; A2: ( x in {x} & y in {y} ) by TARSKI:def_1; assume {x,y} in C ; ::_thesis: ( x in union C & y in union C ) hence ( x in union C & y in union C ) by A1, A2, TARSKI:def_4; ::_thesis: verum end; definition let X be set ; func FuncsC X -> set equals :: COH_SP:def 5 union { (Funcs ((union x),(union y))) where x, y is Element of CSp X : verum } ; coherence union { (Funcs ((union x),(union y))) where x, y is Element of CSp X : verum } is set ; end; :: deftheorem defines FuncsC COH_SP:def_5_:_ for X being set holds FuncsC X = union { (Funcs ((union x),(union y))) where x, y is Element of CSp X : verum } ; registration let X be set ; cluster FuncsC X -> functional non empty ; coherence ( not FuncsC X is empty & FuncsC X is functional ) proof reconsider A = bool X as Subset-Family of X ; A is Coherence_Space by Th2; then A in { x where x is Subset-Family of X : x is Coherence_Space } ; then reconsider A = A as Element of CSp X ; set F = { (Funcs ((union T),(union TT))) where T, TT is Element of CSp X : verum } ; ( id (union A) in Funcs ((union A),(union A)) & Funcs ((union A),(union A)) in { (Funcs ((union T),(union TT))) where T, TT is Element of CSp X : verum } ) by FUNCT_2:9; then reconsider UF = union { (Funcs ((union T),(union TT))) where T, TT is Element of CSp X : verum } as non empty set by TARSKI:def_4; now__::_thesis:_for_f_being_set_st_f_in_UF_holds_ f_is_Function let f be set ; ::_thesis: ( f in UF implies f is Function ) assume f in UF ; ::_thesis: f is Function then consider C being set such that A1: f in C and A2: C in { (Funcs ((union T),(union TT))) where T, TT is Element of CSp X : verum } by TARSKI:def_4; ex A, B being Element of CSp X st C = Funcs ((union A),(union B)) by A2; hence f is Function by A1; ::_thesis: verum end; hence ( not FuncsC X is empty & FuncsC X is functional ) by FUNCT_1:def_13; ::_thesis: verum end; end; theorem Th17: :: COH_SP:17 for x, X being set holds ( x in FuncsC X iff ex C1, C2 being Element of CSp X st ( ( union C2 = {} implies union C1 = {} ) & x is Function of (union C1),(union C2) ) ) proof let x, X be set ; ::_thesis: ( x in FuncsC X iff ex C1, C2 being Element of CSp X st ( ( union C2 = {} implies union C1 = {} ) & x is Function of (union C1),(union C2) ) ) set F = { (Funcs ((union xx),(union y))) where xx, y is Element of CSp X : verum } ; thus ( x in FuncsC X implies ex C1, C2 being Element of CSp X st ( ( union C2 = {} implies union C1 = {} ) & x is Function of (union C1),(union C2) ) ) ::_thesis: ( ex C1, C2 being Element of CSp X st ( ( union C2 = {} implies union C1 = {} ) & x is Function of (union C1),(union C2) ) implies x in FuncsC X ) proof assume x in FuncsC X ; ::_thesis: ex C1, C2 being Element of CSp X st ( ( union C2 = {} implies union C1 = {} ) & x is Function of (union C1),(union C2) ) then consider C being set such that A1: x in C and A2: C in { (Funcs ((union xx),(union y))) where xx, y is Element of CSp X : verum } by TARSKI:def_4; consider A, B being Element of CSp X such that A3: C = Funcs ((union A),(union B)) by A2; take A ; ::_thesis: ex C2 being Element of CSp X st ( ( union C2 = {} implies union A = {} ) & x is Function of (union A),(union C2) ) take B ; ::_thesis: ( ( union B = {} implies union A = {} ) & x is Function of (union A),(union B) ) thus ( ( union B = {} implies union A = {} ) & x is Function of (union A),(union B) ) by A1, A3, FUNCT_2:66; ::_thesis: verum end; given A, B being Element of CSp X such that A4: ( ( union B = {} implies union A = {} ) & x is Function of (union A),(union B) ) ; ::_thesis: x in FuncsC X A5: Funcs ((union A),(union B)) in { (Funcs ((union xx),(union y))) where xx, y is Element of CSp X : verum } ; x in Funcs ((union A),(union B)) by A4, FUNCT_2:8; hence x in FuncsC X by A5, TARSKI:def_4; ::_thesis: verum end; definition let X be set ; func MapsC X -> set equals :: COH_SP:def 6 { [[C,CC],f] where C, CC is Element of CSp X, f is Element of FuncsC X : ( ( union CC = {} implies union C = {} ) & f is Function of (union C),(union CC) & ( for x, y being set st {x,y} in C holds {(f . x),(f . y)} in CC ) ) } ; coherence { [[C,CC],f] where C, CC is Element of CSp X, f is Element of FuncsC X : ( ( union CC = {} implies union C = {} ) & f is Function of (union C),(union CC) & ( for x, y being set st {x,y} in C holds {(f . x),(f . y)} in CC ) ) } is set ; end; :: deftheorem defines MapsC COH_SP:def_6_:_ for X being set holds MapsC X = { [[C,CC],f] where C, CC is Element of CSp X, f is Element of FuncsC X : ( ( union CC = {} implies union C = {} ) & f is Function of (union C),(union CC) & ( for x, y being set st {x,y} in C holds {(f . x),(f . y)} in CC ) ) } ; registration let X be set ; cluster MapsC X -> non empty ; coherence not MapsC X is empty proof set FV = { [[T,TT],f] where T, TT is Element of CSp X, f is Element of FuncsC X : ( ( union TT = {} implies union T = {} ) & f is Function of (union T),(union TT) & ( for x, y being set st {x,y} in T holds {(f . x),(f . y)} in TT ) ) } ; now__::_thesis:_ex_m_being_set_st_m_in__{__[[T,TT],f]_where_T,_TT_is_Element_of_CSp_X,_f_is_Element_of_FuncsC_X_:_(_(_union_TT_=_{}_implies_union_T_=_{}_)_&_f_is_Function_of_(union_T),(union_TT)_&_(_for_x,_y_being_set_st_{x,y}_in_T_holds_ {(f_._x),(f_._y)}_in_TT_)_)__}_ reconsider A = bool X as Subset-Family of X ; A is Coherence_Space by Th2; then A in { xx where xx is Subset-Family of X : xx is Coherence_Space } ; then reconsider A = A as Element of CSp X ; set f = id (union A); take m = [[A,A],(id (union A))]; ::_thesis: m in { [[T,TT],f] where T, TT is Element of CSp X, f is Element of FuncsC X : ( ( union TT = {} implies union T = {} ) & f is Function of (union T),(union TT) & ( for x, y being set st {x,y} in T holds {(f . x),(f . y)} in TT ) ) } A1: ( union A = {} implies union A = {} ) ; reconsider f = id (union A) as Element of FuncsC X by Th17; now__::_thesis:_for_x,_y_being_set_st_{x,y}_in_A_holds_ {(f_._x),(f_._y)}_in_A let x, y be set ; ::_thesis: ( {x,y} in A implies {(f . x),(f . y)} in A ) assume A2: {x,y} in A ; ::_thesis: {(f . x),(f . y)} in A then x in union A by Th16; then A3: f . x = x by FUNCT_1:18; y in union A by A2, Th16; hence {(f . x),(f . y)} in A by A2, A3, FUNCT_1:18; ::_thesis: verum end; hence m in { [[T,TT],f] where T, TT is Element of CSp X, f is Element of FuncsC X : ( ( union TT = {} implies union T = {} ) & f is Function of (union T),(union TT) & ( for x, y being set st {x,y} in T holds {(f . x),(f . y)} in TT ) ) } by A1; ::_thesis: verum end; hence not MapsC X is empty ; ::_thesis: verum end; end; theorem Th18: :: COH_SP:18 for X being set for l being Element of MapsC X ex g being Element of FuncsC X ex C1, C2 being Element of CSp X st ( l = [[C1,C2],g] & ( union C2 = {} implies union C1 = {} ) & g is Function of (union C1),(union C2) & ( for x, y being set st {x,y} in C1 holds {(g . x),(g . y)} in C2 ) ) proof let X be set ; ::_thesis: for l being Element of MapsC X ex g being Element of FuncsC X ex C1, C2 being Element of CSp X st ( l = [[C1,C2],g] & ( union C2 = {} implies union C1 = {} ) & g is Function of (union C1),(union C2) & ( for x, y being set st {x,y} in C1 holds {(g . x),(g . y)} in C2 ) ) let l be Element of MapsC X; ::_thesis: ex g being Element of FuncsC X ex C1, C2 being Element of CSp X st ( l = [[C1,C2],g] & ( union C2 = {} implies union C1 = {} ) & g is Function of (union C1),(union C2) & ( for x, y being set st {x,y} in C1 holds {(g . x),(g . y)} in C2 ) ) l in { [[C1,C2],g] where C1, C2 is Element of CSp X, g is Element of FuncsC X : ( ( union C2 = {} implies union C1 = {} ) & g is Function of (union C1),(union C2) & ( for x, y being set st {x,y} in C1 holds {(g . x),(g . y)} in C2 ) ) } ; then ex C1, C2 being Element of CSp X ex g being Element of FuncsC X st ( l = [[C1,C2],g] & ( union C2 = {} implies union C1 = {} ) & g is Function of (union C1),(union C2) & ( for x, y being set st {x,y} in C1 holds {(g . x),(g . y)} in C2 ) ) ; hence ex g being Element of FuncsC X ex C1, C2 being Element of CSp X st ( l = [[C1,C2],g] & ( union C2 = {} implies union C1 = {} ) & g is Function of (union C1),(union C2) & ( for x, y being set st {x,y} in C1 holds {(g . x),(g . y)} in C2 ) ) ; ::_thesis: verum end; theorem Th19: :: COH_SP:19 for X being set for C1, C2 being Element of CSp X for f being Function of (union C1),(union C2) st ( union C2 = {} implies union C1 = {} ) & ( for x, y being set st {x,y} in C1 holds {(f . x),(f . y)} in C2 ) holds [[C1,C2],f] in MapsC X proof let X be set ; ::_thesis: for C1, C2 being Element of CSp X for f being Function of (union C1),(union C2) st ( union C2 = {} implies union C1 = {} ) & ( for x, y being set st {x,y} in C1 holds {(f . x),(f . y)} in C2 ) holds [[C1,C2],f] in MapsC X let C1, C2 be Element of CSp X; ::_thesis: for f being Function of (union C1),(union C2) st ( union C2 = {} implies union C1 = {} ) & ( for x, y being set st {x,y} in C1 holds {(f . x),(f . y)} in C2 ) holds [[C1,C2],f] in MapsC X let f be Function of (union C1),(union C2); ::_thesis: ( ( union C2 = {} implies union C1 = {} ) & ( for x, y being set st {x,y} in C1 holds {(f . x),(f . y)} in C2 ) implies [[C1,C2],f] in MapsC X ) assume that A1: ( union C2 = {} implies union C1 = {} ) and A2: for x, y being set st {x,y} in C1 holds {(f . x),(f . y)} in C2 ; ::_thesis: [[C1,C2],f] in MapsC X reconsider f9 = f as Element of FuncsC X by A1, Th17; for x, y being set st {x,y} in C1 holds {(f9 . x),(f9 . y)} in C2 by A2; hence [[C1,C2],f] in MapsC X by A1; ::_thesis: verum end; registration let X be set ; let l be Element of MapsC X; clusterl `2 -> Relation-like Function-like ; coherence ( l `2 is Function-like & l `2 is Relation-like ) proof consider g being Element of FuncsC X, C1, C2 being Element of CSp X such that W: ( l = [[C1,C2],g] & ( union C2 = {} implies union C1 = {} ) & g is Function of (union C1),(union C2) & ( for x, y being set st {x,y} in C1 holds {(g . x),(g . y)} in C2 ) ) by Th18; [[C1,C2],g] `2 = g ; hence ( l `2 is Function-like & l `2 is Relation-like ) by W; ::_thesis: verum end; end; definition let X be set ; let l be Element of MapsC X; func dom l -> Element of CSp X equals :: COH_SP:def 7 (l `1) `1 ; coherence (l `1) `1 is Element of CSp X proof consider g being Element of FuncsC X, C1, C2 being Element of CSp X such that A1: l = [[C1,C2],g] and ( union C2 = {} implies union C1 = {} ) and g is Function of (union C1),(union C2) and for x, y being set st {x,y} in C1 holds {(g . x),(g . y)} in C2 by Th18; ( [C1,C2] = [[C1,C2],g] `1 & [C1,C2] `1 = C1 ) ; hence (l `1) `1 is Element of CSp X by A1; ::_thesis: verum end; func cod l -> Element of CSp X equals :: COH_SP:def 8 (l `1) `2 ; coherence (l `1) `2 is Element of CSp X proof consider g being Element of FuncsC X, C1, C2 being Element of CSp X such that A2: l = [[C1,C2],g] and ( union C2 = {} implies union C1 = {} ) and g is Function of (union C1),(union C2) and for x, y being set st {x,y} in C1 holds {(g . x),(g . y)} in C2 by Th18; ( [C1,C2] = [[C1,C2],g] `1 & [C1,C2] `2 = C2 ) ; hence (l `1) `2 is Element of CSp X by A2; ::_thesis: verum end; end; :: deftheorem defines dom COH_SP:def_7_:_ for X being set for l being Element of MapsC X holds dom l = (l `1) `1 ; :: deftheorem defines cod COH_SP:def_8_:_ for X being set for l being Element of MapsC X holds cod l = (l `1) `2 ; theorem Th20: :: COH_SP:20 for X being set for l being Element of MapsC X holds l = [[(dom l),(cod l)],(l `2)] proof let X be set ; ::_thesis: for l being Element of MapsC X holds l = [[(dom l),(cod l)],(l `2)] let l be Element of MapsC X; ::_thesis: l = [[(dom l),(cod l)],(l `2)] consider g being Element of FuncsC X, C1, C2 being Element of CSp X such that A1: l = [[C1,C2],g] and ( union C2 = {} implies union C1 = {} ) and g is Function of (union C1),(union C2) and for x, y being set st {x,y} in C1 holds {(g . x),(g . y)} in C2 by Th18; [C1,C2] = [[C1,C2],g] `1 ; then l `1 = [(dom l),(cod l)] by A1, MCART_1:8; hence l = [[(dom l),(cod l)],(l `2)] by A1, MCART_1:8; ::_thesis: verum end; Lm1: for X being set for l, l1 being Element of MapsC X st l `2 = l1 `2 & dom l = dom l1 & cod l = cod l1 holds l = l1 proof let X be set ; ::_thesis: for l, l1 being Element of MapsC X st l `2 = l1 `2 & dom l = dom l1 & cod l = cod l1 holds l = l1 let l, l1 be Element of MapsC X; ::_thesis: ( l `2 = l1 `2 & dom l = dom l1 & cod l = cod l1 implies l = l1 ) l = [[(dom l),(cod l)],(l `2)] by Th20; hence ( l `2 = l1 `2 & dom l = dom l1 & cod l = cod l1 implies l = l1 ) by Th20; ::_thesis: verum end; definition let X be set ; let C be Element of CSp X; func id\$ C -> Element of MapsC X equals :: COH_SP:def 9 [[C,C],(id (union C))]; coherence [[C,C],(id (union C))] is Element of MapsC X proof set f = id (union C); now__::_thesis:_for_x,_y_being_set_st_{x,y}_in_C_holds_ {((id_(union_C))_._x),((id_(union_C))_._y)}_in_C let x, y be set ; ::_thesis: ( {x,y} in C implies {((id (union C)) . x),((id (union C)) . y)} in C ) assume A1: {x,y} in C ; ::_thesis: {((id (union C)) . x),((id (union C)) . y)} in C then x in union C by Th16; then A2: (id (union C)) . x = x by FUNCT_1:18; y in union C by A1, Th16; hence {((id (union C)) . x),((id (union C)) . y)} in C by A1, A2, FUNCT_1:18; ::_thesis: verum end; hence [[C,C],(id (union C))] is Element of MapsC X by Th19; ::_thesis: verum end; end; :: deftheorem defines id\$ COH_SP:def_9_:_ for X being set for C being Element of CSp X holds id\$ C = [[C,C],(id (union C))]; Lm2: for x1, y1, x2, y2, x3, y3 being set st [[x1,x2],x3] = [[y1,y2],y3] holds ( x1 = y1 & x2 = y2 ) proof let x1, y1, x2, y2, x3, y3 be set ; ::_thesis: ( [[x1,x2],x3] = [[y1,y2],y3] implies ( x1 = y1 & x2 = y2 ) ) assume [[x1,x2],x3] = [[y1,y2],y3] ; ::_thesis: ( x1 = y1 & x2 = y2 ) then [x1,x2] = [y1,y2] by XTUPLE_0:1; hence ( x1 = y1 & x2 = y2 ) by XTUPLE_0:1; ::_thesis: verum end; theorem Th21: :: COH_SP:21 for X being set for l being Element of MapsC X holds ( ( union (cod l) <> {} or union (dom l) = {} ) & l `2 is Function of (union (dom l)),(union (cod l)) & ( for x, y being set st {x,y} in dom l holds {((l `2) . x),((l `2) . y)} in cod l ) ) proof let X be set ; ::_thesis: for l being Element of MapsC X holds ( ( union (cod l) <> {} or union (dom l) = {} ) & l `2 is Function of (union (dom l)),(union (cod l)) & ( for x, y being set st {x,y} in dom l holds {((l `2) . x),((l `2) . y)} in cod l ) ) let l be Element of MapsC X; ::_thesis: ( ( union (cod l) <> {} or union (dom l) = {} ) & l `2 is Function of (union (dom l)),(union (cod l)) & ( for x, y being set st {x,y} in dom l holds {((l `2) . x),((l `2) . y)} in cod l ) ) consider g being Element of FuncsC X, C1, C2 being Element of CSp X such that A1: l = [[C1,C2],g] and A2: ( ( union C2 = {} implies union C1 = {} ) & g is Function of (union C1),(union C2) ) and A3: for x, y being set st {x,y} in C1 holds {(g . x),(g . y)} in C2 by Th18; A4: l = [[(dom l),(cod l)],(l `2)] by Th20; then A5: C2 = cod l by A1, Lm2; A6: ( g = l `2 & C1 = dom l ) by A1, A4, Lm2, XTUPLE_0:1; hence ( ( union (cod l) <> {} or union (dom l) = {} ) & l `2 is Function of (union (dom l)),(union (cod l)) ) by A1, A2, A4, Lm2; ::_thesis: for x, y being set st {x,y} in dom l holds {((l `2) . x),((l `2) . y)} in cod l let x, y be set ; ::_thesis: ( {x,y} in dom l implies {((l `2) . x),((l `2) . y)} in cod l ) assume {x,y} in dom l ; ::_thesis: {((l `2) . x),((l `2) . y)} in cod l hence {((l `2) . x),((l `2) . y)} in cod l by A3, A6, A5; ::_thesis: verum end; definition let X be set ; let l1, l2 be Element of MapsC X; assume A1: cod l1 = dom l2 ; funcl2 * l1 -> Element of MapsC X equals :Def10: :: COH_SP:def 10 [[(dom l1),(cod l2)],((l2 `2) * (l1 `2))]; coherence [[(dom l1),(cod l2)],((l2 `2) * (l1 `2))] is Element of MapsC X proof A2: ( union (cod l2) <> {} or union (dom l2) = {} ) by Th21; A3: ( union (cod l1) <> {} or union (dom l1) = {} ) by Th21; A4: l1 `2 is Function of (union (dom l1)),(union (cod l1)) by Th21; A5: now__::_thesis:_for_x,_y_being_set_st_{x,y}_in_dom_l1_holds_ {(((l2_`2)_*_(l1_`2))_._x),(((l2_`2)_*_(l1_`2))_._y)}_in_cod_l2 let x, y be set ; ::_thesis: ( {x,y} in dom l1 implies {(((l2 `2) * (l1 `2)) . x),(((l2 `2) * (l1 `2)) . y)} in cod l2 ) assume A6: {x,y} in dom l1 ; ::_thesis: {(((l2 `2) * (l1 `2)) . x),(((l2 `2) * (l1 `2)) . y)} in cod l2 then x in union (dom l1) by Th16; then A7: x in dom (l1 `2) by A3, A4, FUNCT_2:def_1; y in union (dom l1) by A6, Th16; then A8: y in dom (l1 `2) by A3, A4, FUNCT_2:def_1; {((l1 `2) . x),((l1 `2) . y)} in cod l1 by A6, Th21; then {((l2 `2) . ((l1 `2) . x)),((l2 `2) . ((l1 `2) . y))} in cod l2 by A1, Th21; then {(((l2 `2) * (l1 `2)) . x),((l2 `2) . ((l1 `2) . y))} in cod l2 by A7, FUNCT_1:13; hence {(((l2 `2) * (l1 `2)) . x),(((l2 `2) * (l1 `2)) . y)} in cod l2 by A8, FUNCT_1:13; ::_thesis: verum end; l2 `2 is Function of (union (dom l2)),(union (cod l2)) by Th21; then (l2 `2) * (l1 `2) is Function of (union (dom l1)),(union (cod l2)) by A1, A3, A4, FUNCT_2:13; hence [[(dom l1),(cod l2)],((l2 `2) * (l1 `2))] is Element of MapsC X by A1, A3, A2, A5, Th19; ::_thesis: verum end; end; :: deftheorem Def10 defines * COH_SP:def_10_:_ for X being set for l1, l2 being Element of MapsC X st cod l1 = dom l2 holds l2 * l1 = [[(dom l1),(cod l2)],((l2 `2) * (l1 `2))]; theorem Th22: :: COH_SP:22 for X being set for l2, l1 being Element of MapsC X st dom l2 = cod l1 holds ( (l2 * l1) `2 = (l2 `2) * (l1 `2) & dom (l2 * l1) = dom l1 & cod (l2 * l1) = cod l2 ) proof let X be set ; ::_thesis: for l2, l1 being Element of MapsC X st dom l2 = cod l1 holds ( (l2 * l1) `2 = (l2 `2) * (l1 `2) & dom (l2 * l1) = dom l1 & cod (l2 * l1) = cod l2 ) let l2, l1 be Element of MapsC X; ::_thesis: ( dom l2 = cod l1 implies ( (l2 * l1) `2 = (l2 `2) * (l1 `2) & dom (l2 * l1) = dom l1 & cod (l2 * l1) = cod l2 ) ) assume dom l2 = cod l1 ; ::_thesis: ( (l2 * l1) `2 = (l2 `2) * (l1 `2) & dom (l2 * l1) = dom l1 & cod (l2 * l1) = cod l2 ) then [[(dom l1),(cod l2)],((l2 `2) * (l1 `2))] = l2 * l1 by Def10 .= [[(dom (l2 * l1)),(cod (l2 * l1))],((l2 * l1) `2)] by Th20 ; hence ( (l2 * l1) `2 = (l2 `2) * (l1 `2) & dom (l2 * l1) = dom l1 & cod (l2 * l1) = cod l2 ) by Lm2, XTUPLE_0:1; ::_thesis: verum end; theorem Th23: :: COH_SP:23 for X being set for l2, l1, l3 being Element of MapsC X st dom l2 = cod l1 & dom l3 = cod l2 holds l3 * (l2 * l1) = (l3 * l2) * l1 proof let X be set ; ::_thesis: for l2, l1, l3 being Element of MapsC X st dom l2 = cod l1 & dom l3 = cod l2 holds l3 * (l2 * l1) = (l3 * l2) * l1 let l2, l1, l3 be Element of MapsC X; ::_thesis: ( dom l2 = cod l1 & dom l3 = cod l2 implies l3 * (l2 * l1) = (l3 * l2) * l1 ) assume that A1: dom l2 = cod l1 and A2: dom l3 = cod l2 ; ::_thesis: l3 * (l2 * l1) = (l3 * l2) * l1 A3: cod (l2 * l1) = cod l2 by A1, Th22; (l2 * l1) `2 = (l2 `2) * (l1 `2) by A1, Th22; then A4: (l3 * (l2 * l1)) `2 = (l3 `2) * ((l2 `2) * (l1 `2)) by A2, A3, Th22; A5: dom (l3 * l2) = dom l2 by A2, Th22; then A6: dom ((l3 * l2) * l1) = dom l1 by A1, Th22; dom (l2 * l1) = dom l1 by A1, Th22; then A7: dom (l3 * (l2 * l1)) = dom l1 by A2, A3, Th22; cod (l3 * l2) = cod l3 by A2, Th22; then A8: cod ((l3 * l2) * l1) = cod l3 by A1, A5, Th22; (l3 * l2) `2 = (l3 `2) * (l2 `2) by A2, Th22; then A9: ((l3 * l2) * l1) `2 = ((l3 `2) * (l2 `2)) * (l1 `2) by A1, A5, Th22; cod (l3 * (l2 * l1)) = cod l3 by A2, A3, Th22; hence l3 * (l2 * l1) = (l3 * l2) * l1 by A4, A7, A9, A6, A8, Lm1, RELAT_1:36; ::_thesis: verum end; theorem Th24: :: COH_SP:24 for X being set for C being Element of CSp X holds ( (id\$ C) `2 = id (union C) & dom (id\$ C) = C & cod (id\$ C) = C ) proof let X be set ; ::_thesis: for C being Element of CSp X holds ( (id\$ C) `2 = id (union C) & dom (id\$ C) = C & cod (id\$ C) = C ) let C be Element of CSp X; ::_thesis: ( (id\$ C) `2 = id (union C) & dom (id\$ C) = C & cod (id\$ C) = C ) [[(dom (id\$ C)),(cod (id\$ C))],((id\$ C) `2)] = [[C,C],(id (union C))] by Th20; hence ( (id\$ C) `2 = id (union C) & dom (id\$ C) = C & cod (id\$ C) = C ) by Lm2, XTUPLE_0:1; ::_thesis: verum end; theorem Th25: :: COH_SP:25 for X being set for l being Element of MapsC X holds ( l * (id\$ (dom l)) = l & (id\$ (cod l)) * l = l ) proof let X be set ; ::_thesis: for l being Element of MapsC X holds ( l * (id\$ (dom l)) = l & (id\$ (cod l)) * l = l ) let l be Element of MapsC X; ::_thesis: ( l * (id\$ (dom l)) = l & (id\$ (cod l)) * l = l ) set i1 = id\$ (dom l); set i2 = id\$ (cod l); A1: ( (id\$ (dom l)) `2 = id (union (dom l)) & dom (id\$ (dom l)) = dom l ) by Th24; A2: l `2 is Function of (union (dom l)),(union (cod l)) by Th21; then A3: rng (l `2) c= union (cod l) by RELAT_1:def_19; ( union (cod l) <> {} or union (dom l) = {} ) by Th21; then A4: dom (l `2) = union (dom l) by A2, FUNCT_2:def_1; A5: cod (id\$ (dom l)) = dom l by Th24; then A6: cod (l * (id\$ (dom l))) = cod l by Th22; ( (l * (id\$ (dom l))) `2 = (l `2) * ((id\$ (dom l)) `2) & dom (l * (id\$ (dom l))) = dom (id\$ (dom l)) ) by A5, Th22; hence l * (id\$ (dom l)) = l by A4, A1, A6, Lm1, RELAT_1:52; ::_thesis: (id\$ (cod l)) * l = l A7: ( (id\$ (cod l)) `2 = id (union (cod l)) & cod (id\$ (cod l)) = cod l ) by Th24; A8: dom (id\$ (cod l)) = cod l by Th24; then A9: cod ((id\$ (cod l)) * l) = cod (id\$ (cod l)) by Th22; ( ((id\$ (cod l)) * l) `2 = ((id\$ (cod l)) `2) * (l `2) & dom ((id\$ (cod l)) * l) = dom l ) by A8, Th22; hence (id\$ (cod l)) * l = l by A3, A7, A9, Lm1, RELAT_1:53; ::_thesis: verum end; definition let X be set ; func CDom X -> Function of (MapsC X),(CSp X) means :Def11: :: COH_SP:def 11 for l being Element of MapsC X holds it . l = dom l; existence ex b1 being Function of (MapsC X),(CSp X) st for l being Element of MapsC X holds b1 . l = dom l proof deffunc H1( Element of MapsC X) -> Element of CSp X = dom \$1; thus ex f being Function of (MapsC X),(CSp X) st for x being Element of MapsC X holds f . x = H1(x) from FUNCT_2:sch_4(); ::_thesis: verum end; uniqueness for b1, b2 being Function of (MapsC X),(CSp X) st ( for l being Element of MapsC X holds b1 . l = dom l ) & ( for l being Element of MapsC X holds b2 . l = dom l ) holds b1 = b2 proof let h1, h2 be Function of (MapsC X),(CSp X); ::_thesis: ( ( for l being Element of MapsC X holds h1 . l = dom l ) & ( for l being Element of MapsC X holds h2 . l = dom l ) implies h1 = h2 ) assume that A1: for l being Element of MapsC X holds h1 . l = dom l and A2: for l being Element of MapsC X holds h2 . l = dom l ; ::_thesis: h1 = h2 now__::_thesis:_for_l_being_Element_of_MapsC_X_holds_h1_._l_=_h2_._l let l be Element of MapsC X; ::_thesis: h1 . l = h2 . l thus h1 . l = dom l by A1 .= h2 . l by A2 ; ::_thesis: verum end; hence h1 = h2 by FUNCT_2:63; ::_thesis: verum end; func CCod X -> Function of (MapsC X),(CSp X) means :Def12: :: COH_SP:def 12 for l being Element of MapsC X holds it . l = cod l; existence ex b1 being Function of (MapsC X),(CSp X) st for l being Element of MapsC X holds b1 . l = cod l proof deffunc H1( Element of MapsC X) -> Element of CSp X = cod \$1; thus ex f being Function of (MapsC X),(CSp X) st for x being Element of MapsC X holds f . x = H1(x) from FUNCT_2:sch_4(); ::_thesis: verum end; uniqueness for b1, b2 being Function of (MapsC X),(CSp X) st ( for l being Element of MapsC X holds b1 . l = cod l ) & ( for l being Element of MapsC X holds b2 . l = cod l ) holds b1 = b2 proof let h1, h2 be Function of (MapsC X),(CSp X); ::_thesis: ( ( for l being Element of MapsC X holds h1 . l = cod l ) & ( for l being Element of MapsC X holds h2 . l = cod l ) implies h1 = h2 ) assume that A3: for l being Element of MapsC X holds h1 . l = cod l and A4: for l being Element of MapsC X holds h2 . l = cod l ; ::_thesis: h1 = h2 now__::_thesis:_for_l_being_Element_of_MapsC_X_holds_h1_._l_=_h2_._l let l be Element of MapsC X; ::_thesis: h1 . l = h2 . l thus h1 . l = cod l by A3 .= h2 . l by A4 ; ::_thesis: verum end; hence h1 = h2 by FUNCT_2:63; ::_thesis: verum end; func CComp X -> PartFunc of [:(MapsC X),(MapsC X):],(MapsC X) means :Def13: :: COH_SP:def 13 ( ( for l2, l1 being Element of MapsC X holds ( [l2,l1] in dom it iff dom l2 = cod l1 ) ) & ( for l2, l1 being Element of MapsC X st dom l2 = cod l1 holds it . [l2,l1] = l2 * l1 ) ); existence ex b1 being PartFunc of [:(MapsC X),(MapsC X):],(MapsC X) st ( ( for l2, l1 being Element of MapsC X holds ( [l2,l1] in dom b1 iff dom l2 = cod l1 ) ) & ( for l2, l1 being Element of MapsC X st dom l2 = cod l1 holds b1 . [l2,l1] = l2 * l1 ) ) proof defpred S1[ set , set , set ] means for l2, l1 being Element of MapsC X st l2 = \$1 & l1 = \$2 holds ( dom l2 = cod l1 & \$3 = l2 * l1 ); A5: for x, y, z1, z2 being set st x in MapsC X & y in MapsC X & S1[x,y,z1] & S1[x,y,z2] holds z1 = z2 proof let x, y, z1, z2 be set ; ::_thesis: ( x in MapsC X & y in MapsC X & S1[x,y,z1] & S1[x,y,z2] implies z1 = z2 ) assume ( x in MapsC X & y in MapsC X ) ; ::_thesis: ( not S1[x,y,z1] or not S1[x,y,z2] or z1 = z2 ) then reconsider l2 = x, l1 = y as Element of MapsC X ; assume that A6: S1[x,y,z1] and A7: S1[x,y,z2] ; ::_thesis: z1 = z2 z1 = l2 * l1 by A6; hence z1 = z2 by A7; ::_thesis: verum end; A8: for x, y, z being set st x in MapsC X & y in MapsC X & S1[x,y,z] holds z in MapsC X proof let x, y, z be set ; ::_thesis: ( x in MapsC X & y in MapsC X & S1[x,y,z] implies z in MapsC X ) assume ( x in MapsC X & y in MapsC X ) ; ::_thesis: ( not S1[x,y,z] or z in MapsC X ) then reconsider l2 = x, l1 = y as Element of MapsC X ; assume S1[x,y,z] ; ::_thesis: z in MapsC X then z = l2 * l1 ; hence z in MapsC X ; ::_thesis: verum end; consider h being PartFunc of [:(MapsC X),(MapsC X):],(MapsC X) such that A9: for x, y being set holds ( [x,y] in dom h iff ( x in MapsC X & y in MapsC X & ex z being set st S1[x,y,z] ) ) and A10: for x, y being set st [x,y] in dom h holds S1[x,y,h . (x,y)] from BINOP_1:sch_5(A8, A5); take h ; ::_thesis: ( ( for l2, l1 being Element of MapsC X holds ( [l2,l1] in dom h iff dom l2 = cod l1 ) ) & ( for l2, l1 being Element of MapsC X st dom l2 = cod l1 holds h . [l2,l1] = l2 * l1 ) ) thus A11: for l2, l1 being Element of MapsC X holds ( [l2,l1] in dom h iff dom l2 = cod l1 ) ::_thesis: for l2, l1 being Element of MapsC X st dom l2 = cod l1 holds h . [l2,l1] = l2 * l1 proof let l2, l1 be Element of MapsC X; ::_thesis: ( [l2,l1] in dom h iff dom l2 = cod l1 ) thus ( [l2,l1] in dom h implies dom l2 = cod l1 ) ::_thesis: ( dom l2 = cod l1 implies [l2,l1] in dom h ) proof assume [l2,l1] in dom h ; ::_thesis: dom l2 = cod l1 then ex z being set st S1[l2,l1,z] by A9; hence dom l2 = cod l1 ; ::_thesis: verum end; assume dom l2 = cod l1 ; ::_thesis: [l2,l1] in dom h then S1[l2,l1,l2 * l1] ; hence [l2,l1] in dom h by A9; ::_thesis: verum end; let l2, l1 be Element of MapsC X; ::_thesis: ( dom l2 = cod l1 implies h . [l2,l1] = l2 * l1 ) assume dom l2 = cod l1 ; ::_thesis: h . [l2,l1] = l2 * l1 then [l2,l1] in dom h by A11; then S1[l2,l1,h . (l2,l1)] by A10; hence h . [l2,l1] = l2 * l1 ; ::_thesis: verum end; uniqueness for b1, b2 being PartFunc of [:(MapsC X),(MapsC X):],(MapsC X) st ( for l2, l1 being Element of MapsC X holds ( [l2,l1] in dom b1 iff dom l2 = cod l1 ) ) & ( for l2, l1 being Element of MapsC X st dom l2 = cod l1 holds b1 . [l2,l1] = l2 * l1 ) & ( for l2, l1 being Element of MapsC X holds ( [l2,l1] in dom b2 iff dom l2 = cod l1 ) ) & ( for l2, l1 being Element of MapsC X st dom l2 = cod l1 holds b2 . [l2,l1] = l2 * l1 ) holds b1 = b2 proof let h1, h2 be PartFunc of [:(MapsC X),(MapsC X):],(MapsC X); ::_thesis: ( ( for l2, l1 being Element of MapsC X holds ( [l2,l1] in dom h1 iff dom l2 = cod l1 ) ) & ( for l2, l1 being Element of MapsC X st dom l2 = cod l1 holds h1 . [l2,l1] = l2 * l1 ) & ( for l2, l1 being Element of MapsC X holds ( [l2,l1] in dom h2 iff dom l2 = cod l1 ) ) & ( for l2, l1 being Element of MapsC X st dom l2 = cod l1 holds h2 . [l2,l1] = l2 * l1 ) implies h1 = h2 ) assume that A12: for l2, l1 being Element of MapsC X holds ( [l2,l1] in dom h1 iff dom l2 = cod l1 ) and A13: for l2, l1 being Element of MapsC X st dom l2 = cod l1 holds h1 . [l2,l1] = l2 * l1 and A14: for l2, l1 being Element of MapsC X holds ( [l2,l1] in dom h2 iff dom l2 = cod l1 ) and A15: for l2, l1 being Element of MapsC X st dom l2 = cod l1 holds h2 . [l2,l1] = l2 * l1 ; ::_thesis: h1 = h2 A16: dom h1 = dom h2 proof let x, y be set ; :: according to RELAT_1:def_2 ::_thesis: ( ( not [x,y] in dom h1 or [x,y] in dom h2 ) & ( not [x,y] in dom h2 or [x,y] in dom h1 ) ) thus ( [x,y] in dom h1 implies [x,y] in dom h2 ) ::_thesis: ( not [x,y] in dom h2 or [x,y] in dom h1 ) proof assume A17: [x,y] in dom h1 ; ::_thesis: [x,y] in dom h2 then reconsider l2 = x, l1 = y as Element of MapsC X by ZFMISC_1:87; dom l2 = cod l1 by A12, A17; hence [x,y] in dom h2 by A14; ::_thesis: verum end; assume A18: [x,y] in dom h2 ; ::_thesis: [x,y] in dom h1 then reconsider l2 = x, l1 = y as Element of MapsC X by ZFMISC_1:87; dom l2 = cod l1 by A14, A18; hence [x,y] in dom h1 by A12; ::_thesis: verum end; now__::_thesis:_for_l_being_Element_of_[:(MapsC_X),(MapsC_X):]_st_l_in_dom_h1_holds_ h1_._l_=_h2_._l let l be Element of [:(MapsC X),(MapsC X):]; ::_thesis: ( l in dom h1 implies h1 . l = h2 . l ) assume A19: l in dom h1 ; ::_thesis: h1 . l = h2 . l consider l2, l1 being Element of MapsC X such that A20: l = [l2,l1] by DOMAIN_1:1; A21: dom l2 = cod l1 by A12, A19, A20; then h1 . [l2,l1] = l2 * l1 by A13; hence h1 . l = h2 . l by A15, A20, A21; ::_thesis: verum end; hence h1 = h2 by A16, PARTFUN1:5; ::_thesis: verum end; end; :: deftheorem Def11 defines CDom COH_SP:def_11_:_ for X being set for b2 being Function of (MapsC X),(CSp X) holds ( b2 = CDom X iff for l being Element of MapsC X holds b2 . l = dom l ); :: deftheorem Def12 defines CCod COH_SP:def_12_:_ for X being set for b2 being Function of (MapsC X),(CSp X) holds ( b2 = CCod X iff for l being Element of MapsC X holds b2 . l = cod l ); :: deftheorem Def13 defines CComp COH_SP:def_13_:_ for X being set for b2 being PartFunc of [:(MapsC X),(MapsC X):],(MapsC X) holds ( b2 = CComp X iff ( ( for l2, l1 being Element of MapsC X holds ( [l2,l1] in dom b2 iff dom l2 = cod l1 ) ) & ( for l2, l1 being Element of MapsC X st dom l2 = cod l1 holds b2 . [l2,l1] = l2 * l1 ) ) ); theorem :: COH_SP:26 canceled; definition canceled; let X be set ; func CohCat X -> non empty non void strict CatStr equals :: COH_SP:def 15 CatStr(# (CSp X),(MapsC X),(CDom X),(CCod X),(CComp X) #); coherence CatStr(# (CSp X),(MapsC X),(CDom X),(CCod X),(CComp X) #) is non empty non void strict CatStr ; end; :: deftheorem COH_SP:def_14_:_ canceled; :: deftheorem defines CohCat COH_SP:def_15_:_ for X being set holds CohCat X = CatStr(# (CSp X),(MapsC X),(CDom X),(CCod X),(CComp X) #); registration let X be set ; cluster CohCat X -> non empty non void strict Category-like transitive associative reflexive ; coherence ( CohCat X is Category-like & CohCat X is transitive & CohCat X is associative & CohCat X is reflexive ) proof set M = MapsC X; set d = CDom X; set c = CCod X; set p = CComp X; set C = CohCat X; thus P1: CohCat X is Category-like ::_thesis: ( CohCat X is transitive & CohCat X is associative & CohCat X is reflexive ) proof let ff, gg be Morphism of (CohCat X); :: according to CAT_1:def_6 ::_thesis: ( ( not [gg,ff] in proj1 the Comp of (CohCat X) or dom gg = cod ff ) & ( not dom gg = cod ff or [gg,ff] in proj1 the Comp of (CohCat X) ) ) reconsider f = ff, g = gg as Element of MapsC X ; ( (CDom X) . gg = dom g & (CCod X) . ff = cod f ) by Def11, Def12; hence ( ( not [gg,ff] in proj1 the Comp of (CohCat X) or dom gg = cod ff ) & ( not dom gg = cod ff or [gg,ff] in proj1 the Comp of (CohCat X) ) ) by Def13; ::_thesis: verum end; thus P2: CohCat X is transitive ::_thesis: ( CohCat X is associative & CohCat X is reflexive ) proof let ff, gg be Morphism of (CohCat X); :: according to CAT_1:def_7 ::_thesis: ( not dom gg = cod ff or ( dom (gg (*) ff) = dom ff & cod (gg (*) ff) = cod gg ) ) assume A1: dom gg = cod ff ; ::_thesis: ( dom (gg (*) ff) = dom ff & cod (gg (*) ff) = cod gg ) [gg,ff] in dom the Comp of (CohCat X) by A1, P1, CAT_1:def_6; then U: the Comp of (CohCat X) . (gg,ff) = gg (*) ff by CAT_1:def_1; reconsider f = ff, g = gg as Element of MapsC X ; A2: ( (CDom X) . g = dom g & (CCod X) . f = cod f ) by Def11, Def12; then A3: (CComp X) . [g,f] = g * f by A1, Def13; A4: ( (CDom X) . f = dom f & (CCod X) . g = cod g ) by Def11, Def12; ( dom (g * f) = dom f & cod (g * f) = cod g ) by A1, A2, Th22; hence ( dom (gg (*) ff) = dom ff & cod (gg (*) ff) = cod gg ) by A3, A4, Def11, Def12, U; ::_thesis: verum end; thus CohCat X is associative ::_thesis: CohCat X is reflexive proof let ff, gg, hh be Morphism of (CohCat X); :: according to CAT_1:def_8 ::_thesis: ( not dom hh = cod gg or not dom gg = cod ff or hh (*) (gg (*) ff) = (hh (*) gg) (*) ff ) assume that A5: dom hh = cod gg and A6: dom gg = cod ff ; ::_thesis: hh (*) (gg (*) ff) = (hh (*) gg) (*) ff reconsider f = ff, g = gg, h = hh as Element of MapsC X ; A7: ( dom h = (CDom X) . h & cod g = (CCod X) . g ) by Def11, Def12; then A8: dom (h * g) = dom g by A5, Th22; A9: ( dom g = (CDom X) . g & cod f = (CCod X) . f ) by Def11, Def12; then A10: cod (g * f) = dom h by A5, A6, A7, Th22; [hh,gg] in dom the Comp of (CohCat X) by P1, CAT_1:def_6, A5; then X2: hh (*) gg = the Comp of (CohCat X) . (hh,gg) by CAT_1:def_1; dom (hh (*) gg) = dom gg by P2, CAT_1:def_7, A5; then X3: [(hh (*) gg),ff] in dom the Comp of (CohCat X) by P1, CAT_1:def_6, A6; [gg,ff] in dom the Comp of (CohCat X) by P1, CAT_1:def_6, A6; then X1: gg (*) ff = the Comp of (CohCat X) . (gg,ff) by CAT_1:def_1; cod (gg (*) ff) = cod gg by P2, CAT_1:def_7, A6; then [hh,(gg (*) ff)] in dom the Comp of (CohCat X) by P1, CAT_1:def_6, A5; hence hh (*) (gg (*) ff) = the Comp of (CohCat X) . (hh,( the Comp of (CohCat X) . (gg,ff))) by X1, CAT_1:def_1 .= (CComp X) . [h,(g * f)] by A6, A9, Def13 .= h * (g * f) by A10, Def13 .= (h * g) * f by A5, A6, A7, A9, Th23 .= (CComp X) . [(h * g),f] by A6, A9, A8, Def13 .= the Comp of (CohCat X) . (( the Comp of (CohCat X) . (hh,gg)),ff) by A5, A7, Def13 .= (hh (*) gg) (*) ff by X2, X3, CAT_1:def_1 ; ::_thesis: verum end; let a be Object of (CohCat X); :: according to CAT_1:def_9 ::_thesis: not Hom (a,a) = {} reconsider aa = a as Element of CSp X ; reconsider ii = id\$ aa as Morphism of (CohCat X) ; A12: cod ii = cod (id\$ aa) by Def12 .= aa by Th24 ; dom ii = dom (id\$ aa) by Def11 .= aa by Th24 ; then id\$ aa in Hom (a,a) by A12; hence Hom (a,a) <> {} ; ::_thesis: verum end; end; LmX: for X being set for a being Element of (CohCat X) for aa being Element of CSp X st a = aa holds for i being Morphism of a,a st i = id\$ aa holds for b being Element of (CohCat X) holds ( ( Hom (a,b) <> {} implies for g being Morphism of a,b holds g (*) i = g ) & ( Hom (b,a) <> {} implies for f being Morphism of b,a holds i (*) f = f ) ) proof let X be set ; ::_thesis: for a being Element of (CohCat X) for aa being Element of CSp X st a = aa holds for i being Morphism of a,a st i = id\$ aa holds for b being Element of (CohCat X) holds ( ( Hom (a,b) <> {} implies for g being Morphism of a,b holds g (*) i = g ) & ( Hom (b,a) <> {} implies for f being Morphism of b,a holds i (*) f = f ) ) let a be Element of (CohCat X); ::_thesis: for aa being Element of CSp X st a = aa holds for i being Morphism of a,a st i = id\$ aa holds for b being Element of (CohCat X) holds ( ( Hom (a,b) <> {} implies for g being Morphism of a,b holds g (*) i = g ) & ( Hom (b,a) <> {} implies for f being Morphism of b,a holds i (*) f = f ) ) let aa be Element of CSp X; ::_thesis: ( a = aa implies for i being Morphism of a,a st i = id\$ aa holds for b being Element of (CohCat X) holds ( ( Hom (a,b) <> {} implies for g being Morphism of a,b holds g (*) i = g ) & ( Hom (b,a) <> {} implies for f being Morphism of b,a holds i (*) f = f ) ) ) assume Z1: a = aa ; ::_thesis: for i being Morphism of a,a st i = id\$ aa holds for b being Element of (CohCat X) holds ( ( Hom (a,b) <> {} implies for g being Morphism of a,b holds g (*) i = g ) & ( Hom (b,a) <> {} implies for f being Morphism of b,a holds i (*) f = f ) ) let i be Morphism of a,a; ::_thesis: ( i = id\$ aa implies for b being Element of (CohCat X) holds ( ( Hom (a,b) <> {} implies for g being Morphism of a,b holds g (*) i = g ) & ( Hom (b,a) <> {} implies for f being Morphism of b,a holds i (*) f = f ) ) ) assume Z2: i = id\$ aa ; ::_thesis: for b being Element of (CohCat X) holds ( ( Hom (a,b) <> {} implies for g being Morphism of a,b holds g (*) i = g ) & ( Hom (b,a) <> {} implies for f being Morphism of b,a holds i (*) f = f ) ) let b be Element of (CohCat X); ::_thesis: ( ( Hom (a,b) <> {} implies for g being Morphism of a,b holds g (*) i = g ) & ( Hom (b,a) <> {} implies for f being Morphism of b,a holds i (*) f = f ) ) thus ( Hom (a,b) <> {} implies for g being Morphism of a,b holds g (*) i = g ) ::_thesis: ( Hom (b,a) <> {} implies for f being Morphism of b,a holds i (*) f = f ) proof assume Z3: Hom (a,b) <> {} ; ::_thesis: for g being Morphism of a,b holds g (*) i = g let g be Morphism of a,b; ::_thesis: g (*) i = g reconsider gg = g as Element of MapsC X ; Hom (a,a) <> {} ; then A1: cod i = a by CAT_1:5 .= dom g by Z3, CAT_1:5 ; A3: dom gg = dom g by Def11 .= aa by Z1, Z3, CAT_1:5 ; then A2: cod (id\$ aa) = dom gg by Th24; [g,i] in dom the Comp of (CohCat X) by A1, CAT_1:def_6; hence g (*) i = the Comp of (CohCat X) . (g,i) by CAT_1:def_1 .= gg * (id\$ aa) by A2, Z2, Def13 .= g by A3, Th25 ; ::_thesis: verum end; thus ( Hom (b,a) <> {} implies for f being Morphism of b,a holds i (*) f = f ) ::_thesis: verum proof assume Z3: Hom (b,a) <> {} ; ::_thesis: for f being Morphism of b,a holds i (*) f = f let g be Morphism of b,a; ::_thesis: i (*) g = g reconsider gg = g as Element of MapsC X ; Hom (a,a) <> {} ; then A1: dom i = a by CAT_1:5 .= cod g by Z3, CAT_1:5 ; A3: cod gg = cod g by Def12 .= aa by Z1, Z3, CAT_1:5 ; then A2: dom (id\$ aa) = cod gg by Th24; [i,g] in dom the Comp of (CohCat X) by A1, CAT_1:def_6; hence i (*) g = the Comp of (CohCat X) . (i,g) by CAT_1:def_1 .= (id\$ aa) * gg by Z2, A2, Def13 .= g by A3, Th25 ; ::_thesis: verum end; end; registration let X be set ; cluster CohCat X -> non empty non void strict with_identities ; coherence CohCat X is with_identities proof let a be Element of (CohCat X); :: according to CAT_1:def_10 ::_thesis: ex b1 being Morphism of a,a st for b2 being Element of the carrier of (CohCat X) holds ( ( Hom (a,b2) = {} or for b3 being Morphism of a,b2 holds b3 (*) b1 = b3 ) & ( Hom (b2,a) = {} or for b3 being Morphism of b2,a holds b1 (*) b3 = b3 ) ) reconsider aa = a as Element of CSp X ; reconsider ii = id\$ aa as Morphism of (CohCat X) ; A12: cod ii = cod (id\$ aa) by Def12 .= aa by Th24 ; dom ii = dom (id\$ aa) by Def11 .= aa by Th24 ; then ii in Hom (a,a) by A12; then reconsider ii = ii as Morphism of a,a by CAT_1:def_5; take ii ; ::_thesis: for b1 being Element of the carrier of (CohCat X) holds ( ( Hom (a,b1) = {} or for b2 being Morphism of a,b1 holds b2 (*) ii = b2 ) & ( Hom (b1,a) = {} or for b2 being Morphism of b1,a holds ii (*) b2 = b2 ) ) thus for b1 being Element of the carrier of (CohCat X) holds ( ( Hom (a,b1) = {} or for b2 being Morphism of a,b1 holds b2 (*) ii = b2 ) & ( Hom (b1,a) = {} or for b2 being Morphism of b1,a holds ii (*) b2 = b2 ) ) by LmX; ::_thesis: verum end; end; begin definition let X be set ; func Toler X -> set means :Def16: :: COH_SP:def 16 for x being set holds ( x in it iff x is Tolerance of X ); existence ex b1 being set st for x being set holds ( x in b1 iff x is Tolerance of X ) proof defpred S1[ set ] means \$1 is Tolerance of X; consider a being set such that A1: for x being set holds ( x in a iff ( x in bool [:X,X:] & S1[x] ) ) from XBOOLE_0:sch_1(); take a ; ::_thesis: for x being set holds ( x in a iff x is Tolerance of X ) let x be set ; ::_thesis: ( x in a iff x is Tolerance of X ) thus ( x in a implies x is Tolerance of X ) by A1; ::_thesis: ( x is Tolerance of X implies x in a ) assume x is Tolerance of X ; ::_thesis: x in a hence x in a by A1; ::_thesis: verum end; uniqueness for b1, b2 being set st ( for x being set holds ( x in b1 iff x is Tolerance of X ) ) & ( for x being set holds ( x in b2 iff x is Tolerance of X ) ) holds b1 = b2 proof let a, b be set ; ::_thesis: ( ( for x being set holds ( x in a iff x is Tolerance of X ) ) & ( for x being set holds ( x in b iff x is Tolerance of X ) ) implies a = b ) assume that A2: for x being set holds ( x in a iff x is Tolerance of X ) and A3: for x being set holds ( x in b iff x is Tolerance of X ) ; ::_thesis: a = b now__::_thesis:_for_x_being_set_holds_ (_x_in_a_iff_x_in_b_) let x be set ; ::_thesis: ( x in a iff x in b ) A4: now__::_thesis:_(_x_in_b_implies_x_in_a_) assume x in b ; ::_thesis: x in a then x is Tolerance of X by A3; hence x in a by A2; ::_thesis: verum end; now__::_thesis:_(_x_in_a_implies_x_in_b_) assume x in a ; ::_thesis: x in b then x is Tolerance of X by A2; hence x in b by A3; ::_thesis: verum end; hence ( x in a iff x in b ) by A4; ::_thesis: verum end; hence a = b by TARSKI:1; ::_thesis: verum end; end; :: deftheorem Def16 defines Toler COH_SP:def_16_:_ for X, b2 being set holds ( b2 = Toler X iff for x being set holds ( x in b2 iff x is Tolerance of X ) ); registration let X be set ; cluster Toler X -> non empty ; coherence not Toler X is empty proof set T = the Tolerance of X; the Tolerance of X in Toler X by Def16; hence not Toler X is empty ; ::_thesis: verum end; end; definition let X be set ; func Toler_on_subsets X -> set equals :: COH_SP:def 17 union { (Toler Y) where Y is Subset of X : verum } ; coherence union { (Toler Y) where Y is Subset of X : verum } is set ; end; :: deftheorem defines Toler_on_subsets COH_SP:def_17_:_ for X being set holds Toler_on_subsets X = union { (Toler Y) where Y is Subset of X : verum } ; registration let X be set ; cluster Toler_on_subsets X -> non empty ; coherence not Toler_on_subsets X is empty proof set F = { (Toler Y) where Y is Subset of X : verum } ; {} c= X by XBOOLE_1:2; then A1: Toler {} in { (Toler Y) where Y is Subset of X : verum } ; {} in Toler {} by Def16, TOLER_1:14; hence not Toler_on_subsets X is empty by A1, TARSKI:def_4; ::_thesis: verum end; end; theorem :: COH_SP:27 for x, X being set holds ( x in Toler_on_subsets X iff ex A being set st ( A c= X & x is Tolerance of A ) ) proof let x, X be set ; ::_thesis: ( x in Toler_on_subsets X iff ex A being set st ( A c= X & x is Tolerance of A ) ) set f = { (Toler Y) where Y is Subset of X : verum } ; thus ( x in Toler_on_subsets X implies ex A being set st ( A c= X & x is Tolerance of A ) ) ::_thesis: ( ex A being set st ( A c= X & x is Tolerance of A ) implies x in Toler_on_subsets X ) proof assume x in Toler_on_subsets X ; ::_thesis: ex A being set st ( A c= X & x is Tolerance of A ) then consider a being set such that A1: x in a and A2: a in { (Toler Y) where Y is Subset of X : verum } by TARSKI:def_4; consider Y being Subset of X such that A3: a = Toler Y by A2; take Y ; ::_thesis: ( Y c= X & x is Tolerance of Y ) thus ( Y c= X & x is Tolerance of Y ) by A1, A3, Def16; ::_thesis: verum end; given A being set such that A4: A c= X and A5: x is Tolerance of A ; ::_thesis: x in Toler_on_subsets X reconsider A = A as Subset of X by A4; A6: Toler A in { (Toler Y) where Y is Subset of X : verum } ; x in Toler A by A5, Def16; hence x in Toler_on_subsets X by A6, TARSKI:def_4; ::_thesis: verum end; theorem :: COH_SP:28 for a being set holds Total a in Toler a by Def16; theorem Th29: :: COH_SP:29 for X being set holds {} in Toler_on_subsets X proof let X be set ; ::_thesis: {} in Toler_on_subsets X set F = { (Toler Y) where Y is Subset of X : verum } ; {} c= X by XBOOLE_1:2; then A1: Toler {} in { (Toler Y) where Y is Subset of X : verum } ; {} in Toler {} by Def16, TOLER_1:14; hence {} in Toler_on_subsets X by A1, TARSKI:def_4; ::_thesis: verum end; theorem Th30: :: COH_SP:30 for a, X being set st a c= X holds Total a in Toler_on_subsets X proof let a, X be set ; ::_thesis: ( a c= X implies Total a in Toler_on_subsets X ) set F = { (Toler Y) where Y is Subset of X : verum } ; assume a c= X ; ::_thesis: Total a in Toler_on_subsets X then A1: Toler a in { (Toler Y) where Y is Subset of X : verum } ; Total a in Toler a by Def16; hence Total a in Toler_on_subsets X by A1, TARSKI:def_4; ::_thesis: verum end; theorem Th31: :: COH_SP:31 for a, X being set st a c= X holds id a in Toler_on_subsets X proof let a, X be set ; ::_thesis: ( a c= X implies id a in Toler_on_subsets X ) set F = { (Toler Y) where Y is Subset of X : verum } ; assume a c= X ; ::_thesis: id a in Toler_on_subsets X then A1: Toler a in { (Toler Y) where Y is Subset of X : verum } ; id a in Toler a by Def16; hence id a in Toler_on_subsets X by A1, TARSKI:def_4; ::_thesis: verum end; theorem :: COH_SP:32 for X being set holds Total X in Toler_on_subsets X by Th30; theorem :: COH_SP:33 for X being set holds id X in Toler_on_subsets X by Th31; definition let X be set ; func TOL X -> set equals :: COH_SP:def 18 { [t,Y] where t is Element of Toler_on_subsets X, Y is Subset of X : t is Tolerance of Y } ; coherence { [t,Y] where t is Element of Toler_on_subsets X, Y is Subset of X : t is Tolerance of Y } is set ; end; :: deftheorem defines TOL COH_SP:def_18_:_ for X being set holds TOL X = { [t,Y] where t is Element of Toler_on_subsets X, Y is Subset of X : t is Tolerance of Y } ; registration let X be set ; cluster TOL X -> non empty ; coherence not TOL X is empty proof set FV = { [t,Y] where t is Element of Toler_on_subsets X, Y is Subset of X : t is Tolerance of Y } ; now__::_thesis:_ex_m_being_set_st_m_in__{__[t,Y]_where_t_is_Element_of_Toler_on_subsets_X,_Y_is_Subset_of_X_:_t_is_Tolerance_of_Y__}_ reconsider o = {} as Subset of X by XBOOLE_1:2; reconsider e = {} as Element of Toler_on_subsets X by Th29; take m = [e,o]; ::_thesis: m in { [t,Y] where t is Element of Toler_on_subsets X, Y is Subset of X : t is Tolerance of Y } thus m in { [t,Y] where t is Element of Toler_on_subsets X, Y is Subset of X : t is Tolerance of Y } by TOLER_1:14; ::_thesis: verum end; hence not TOL X is empty ; ::_thesis: verum end; end; theorem :: COH_SP:34 for X being set holds [{},{}] in TOL X proof let X be set ; ::_thesis: [{},{}] in TOL X ( {} in Toler_on_subsets X & {} c= X ) by Th29, XBOOLE_1:2; hence [{},{}] in TOL X by TOLER_1:14; ::_thesis: verum end; theorem Th35: :: COH_SP:35 for a, X being set st a c= X holds [(id a),a] in TOL X proof let a, X be set ; ::_thesis: ( a c= X implies [(id a),a] in TOL X ) assume A1: a c= X ; ::_thesis: [(id a),a] in TOL X then id a in Toler_on_subsets X by Th31; hence [(id a),a] in TOL X by A1; ::_thesis: verum end; theorem Th36: :: COH_SP:36 for a, X being set st a c= X holds [(Total a),a] in TOL X proof let a, X be set ; ::_thesis: ( a c= X implies [(Total a),a] in TOL X ) assume A1: a c= X ; ::_thesis: [(Total a),a] in TOL X then Total a in Toler_on_subsets X by Th30; hence [(Total a),a] in TOL X by A1; ::_thesis: verum end; theorem :: COH_SP:37 for X being set holds [(id X),X] in TOL X by Th35; theorem :: COH_SP:38 for X being set holds [(Total X),X] in TOL X by Th36; definition let X be set ; let T be Element of TOL X; :: original: `2 redefine funcT `2 -> Subset of X; coherence T `2 is Subset of X proof T in { [t,Y] where t is Element of Toler_on_subsets X, Y is Subset of X : t is Tolerance of Y } ; then consider t being Element of Toler_on_subsets X, Y being Subset of X such that W: ( T = [t,Y] & t is Tolerance of Y ) ; [t,Y] `2 = Y ; hence T `2 is Subset of X by W; ::_thesis: verum end; :: original: `1 redefine funcT `1 -> Tolerance of (T `2); coherence T `1 is Tolerance of (T `2) proof T in { [t,Y] where t is Element of Toler_on_subsets X, Y is Subset of X : t is Tolerance of Y } ; then consider t being Element of Toler_on_subsets X, Y being Subset of X such that A1: T = [t,Y] and A2: t is Tolerance of Y ; ( [t,Y] `2 = Y & [t,Y] `1 = t ) ; hence T `1 is Tolerance of (T `2) by A1, A2; ::_thesis: verum end; end; definition let X be set ; func FuncsT X -> set equals :: COH_SP:def 19 union { (Funcs ((T `2),(TT `2))) where T, TT is Element of TOL X : verum } ; coherence union { (Funcs ((T `2),(TT `2))) where T, TT is Element of TOL X : verum } is set ; end; :: deftheorem defines FuncsT COH_SP:def_19_:_ for X being set holds FuncsT X = union { (Funcs ((T `2),(TT `2))) where T, TT is Element of TOL X : verum } ; registration let X be set ; cluster FuncsT X -> functional non empty ; coherence ( not FuncsT X is empty & FuncsT X is functional ) proof set F = { (Funcs ((T `2),(TT `2))) where T, TT is Element of TOL X : verum } ; reconsider T = [(Total ({} X)),({} X)] as Element of TOL X by Th36; [(Total ({} X)),({} X)] `2 = {} X ; then A1: id ({} X) in Funcs ((T `2),(T `2)) by FUNCT_2:9; Funcs ((T `2),(T `2)) in { (Funcs ((T `2),(TT `2))) where T, TT is Element of TOL X : verum } ; then reconsider UF = union { (Funcs ((T `2),(TT `2))) where T, TT is Element of TOL X : verum } as non empty set by A1, TARSKI:def_4; now__::_thesis:_for_f_being_set_st_f_in_UF_holds_ f_is_Function let f be set ; ::_thesis: ( f in UF implies f is Function ) assume f in UF ; ::_thesis: f is Function then consider C being set such that A2: f in C and A3: C in { (Funcs ((T `2),(TT `2))) where T, TT is Element of TOL X : verum } by TARSKI:def_4; ex A, B being Element of TOL X st C = Funcs ((A `2),(B `2)) by A3; hence f is Function by A2; ::_thesis: verum end; hence ( not FuncsT X is empty & FuncsT X is functional ) by FUNCT_1:def_13; ::_thesis: verum end; end; theorem Th39: :: COH_SP:39 for x, X being set holds ( x in FuncsT X iff ex T1, T2 being Element of TOL X st ( ( T2 `2 = {} implies T1 `2 = {} ) & x is Function of (T1 `2),(T2 `2) ) ) proof let x, X be set ; ::_thesis: ( x in FuncsT X iff ex T1, T2 being Element of TOL X st ( ( T2 `2 = {} implies T1 `2 = {} ) & x is Function of (T1 `2),(T2 `2) ) ) set F = { (Funcs ((T `2),(TT `2))) where T, TT is Element of TOL X : verum } ; thus ( x in FuncsT X implies ex A, B being Element of TOL X st ( ( B `2 = {} implies A `2 = {} ) & x is Function of (A `2),(B `2) ) ) ::_thesis: ( ex T1, T2 being Element of TOL X st ( ( T2 `2 = {} implies T1 `2 = {} ) & x is Function of (T1 `2),(T2 `2) ) implies x in FuncsT X ) proof assume x in FuncsT X ; ::_thesis: ex A, B being Element of TOL X st ( ( B `2 = {} implies A `2 = {} ) & x is Function of (A `2),(B `2) ) then consider C being set such that A1: x in C and A2: C in { (Funcs ((T `2),(TT `2))) where T, TT is Element of TOL X : verum } by TARSKI:def_4; consider A, B being Element of TOL X such that A3: C = Funcs ((A `2),(B `2)) by A2; take A ; ::_thesis: ex B being Element of TOL X st ( ( B `2 = {} implies A `2 = {} ) & x is Function of (A `2),(B `2) ) take B ; ::_thesis: ( ( B `2 = {} implies A `2 = {} ) & x is Function of (A `2),(B `2) ) thus ( ( B `2 = {} implies A `2 = {} ) & x is Function of (A `2),(B `2) ) by A1, A3, FUNCT_2:66; ::_thesis: verum end; given A, B being Element of TOL X such that A4: ( ( B `2 = {} implies A `2 = {} ) & x is Function of (A `2),(B `2) ) ; ::_thesis: x in FuncsT X A5: Funcs ((A `2),(B `2)) in { (Funcs ((T `2),(TT `2))) where T, TT is Element of TOL X : verum } ; x in Funcs ((A `2),(B `2)) by A4, FUNCT_2:8; hence x in FuncsT X by A5, TARSKI:def_4; ::_thesis: verum end; definition let X be set ; func MapsT X -> set equals :: COH_SP:def 20 { [[T,TT],f] where T, TT is Element of TOL X, f is Element of FuncsT X : ( ( TT `2 = {} implies T `2 = {} ) & f is Function of (T `2),(TT `2) & ( for x, y being set st [x,y] in T `1 holds [(f . x),(f . y)] in TT `1 ) ) } ; coherence { [[T,TT],f] where T, TT is Element of TOL X, f is Element of FuncsT X : ( ( TT `2 = {} implies T `2 = {} ) & f is Function of (T `2),(TT `2) & ( for x, y being set st [x,y] in T `1 holds [(f . x),(f . y)] in TT `1 ) ) } is set ; end; :: deftheorem defines MapsT COH_SP:def_20_:_ for X being set holds MapsT X = { [[T,TT],f] where T, TT is Element of TOL X, f is Element of FuncsT X : ( ( TT `2 = {} implies T `2 = {} ) & f is Function of (T `2),(TT `2) & ( for x, y being set st [x,y] in T `1 holds [(f . x),(f . y)] in TT `1 ) ) } ; registration let X be set ; cluster MapsT X -> non empty ; coherence not MapsT X is empty proof set FV = { [[T,TT],f] where T, TT is Element of TOL X, f is Element of FuncsT X : ( ( TT `2 = {} implies T `2 = {} ) & f is Function of (T `2),(TT `2) & ( for x, y being set st [x,y] in T `1 holds [(f . x),(f . y)] in TT `1 ) ) } ; now__::_thesis:_ex_m_being_set_st_m_in__{__[[T,TT],f]_where_T,_TT_is_Element_of_TOL_X,_f_is_Element_of_FuncsT_X_:_(_(_TT_`2_=_{}_implies_T_`2_=_{}_)_&_f_is_Function_of_(T_`2),(TT_`2)_&_(_for_x,_y_being_set_st_[x,y]_in_T_`1_holds_ [(f_._x),(f_._y)]_in_TT_`1_)_)__}_ set a = [(Total ({} X)),({} X)]; set f = id ([(Total ({} X)),({} X)] `2); take m = [[[(Total ({} X)),({} X)],[(Total ({} X)),({} X)]],(id ([(Total ({} X)),({} X)] `2))]; ::_thesis: m in { [[T,TT],f] where T, TT is Element of TOL X, f is Element of FuncsT X : ( ( TT `2 = {} implies T `2 = {} ) & f is Function of (T `2),(TT `2) & ( for x, y being set st [x,y] in T `1 holds [(f . x),(f . y)] in TT `1 ) ) } reconsider a = [(Total ({} X)),({} X)] as Element of TOL X by Th36; ( a `2 = {} implies a `2 = {} ) ; then reconsider f = id ([(Total ({} X)),({} X)] `2) as Element of FuncsT X by Th39; for x, y being set st [x,y] in a `1 holds [(f . x),(f . y)] in a `1 ; hence m in { [[T,TT],f] where T, TT is Element of TOL X, f is Element of FuncsT X : ( ( TT `2 = {} implies T `2 = {} ) & f is Function of (T `2),(TT `2) & ( for x, y being set st [x,y] in T `1 holds [(f . x),(f . y)] in TT `1 ) ) } ; ::_thesis: verum end; hence not MapsT X is empty ; ::_thesis: verum end; end; theorem Th40: :: COH_SP:40 for X being set for m being Element of MapsT X ex f being Element of FuncsT X ex T1, T2 being Element of TOL X st ( m = [[T1,T2],f] & ( T2 `2 = {} implies T1 `2 = {} ) & f is Function of (T1 `2),(T2 `2) & ( for x, y being set st [x,y] in T1 `1 holds [(f . x),(f . y)] in T2 `1 ) ) proof let X be set ; ::_thesis: for m being Element of MapsT X ex f being Element of FuncsT X ex T1, T2 being Element of TOL X st ( m = [[T1,T2],f] & ( T2 `2 = {} implies T1 `2 = {} ) & f is Function of (T1 `2),(T2 `2) & ( for x, y being set st [x,y] in T1 `1 holds [(f . x),(f . y)] in T2 `1 ) ) let m be Element of MapsT X; ::_thesis: ex f being Element of FuncsT X ex T1, T2 being Element of TOL X st ( m = [[T1,T2],f] & ( T2 `2 = {} implies T1 `2 = {} ) & f is Function of (T1 `2),(T2 `2) & ( for x, y being set st [x,y] in T1 `1 holds [(f . x),(f . y)] in T2 `1 ) ) m in { [[T1,T2],f] where T1, T2 is Element of TOL X, f is Element of FuncsT X : ( ( T2 `2 = {} implies T1 `2 = {} ) & f is Function of (T1 `2),(T2 `2) & ( for x, y being set st [x,y] in T1 `1 holds [(f . x),(f . y)] in T2 `1 ) ) } ; then ex T1, T2 being Element of TOL X ex f being Element of FuncsT X st ( m = [[T1,T2],f] & ( T2 `2 = {} implies T1 `2 = {} ) & f is Function of (T1 `2),(T2 `2) & ( for x, y being set st [x,y] in T1 `1 holds [(f . x),(f . y)] in T2 `1 ) ) ; hence ex f being Element of FuncsT X ex T1, T2 being Element of TOL X st ( m = [[T1,T2],f] & ( T2 `2 = {} implies T1 `2 = {} ) & f is Function of (T1 `2),(T2 `2) & ( for x, y being set st [x,y] in T1 `1 holds [(f . x),(f . y)] in T2 `1 ) ) ; ::_thesis: verum end; theorem Th41: :: COH_SP:41 for X being set for T1, T2 being Element of TOL X for f being Function of (T1 `2),(T2 `2) st ( T2 `2 = {} implies T1 `2 = {} ) & ( for x, y being set st [x,y] in T1 `1 holds [(f . x),(f . y)] in T2 `1 ) holds [[T1,T2],f] in MapsT X proof let X be set ; ::_thesis: for T1, T2 being Element of TOL X for f being Function of (T1 `2),(T2 `2) st ( T2 `2 = {} implies T1 `2 = {} ) & ( for x, y being set st [x,y] in T1 `1 holds [(f . x),(f . y)] in T2 `1 ) holds [[T1,T2],f] in MapsT X let T1, T2 be Element of TOL X; ::_thesis: for f being Function of (T1 `2),(T2 `2) st ( T2 `2 = {} implies T1 `2 = {} ) & ( for x, y being set st [x,y] in T1 `1 holds [(f . x),(f . y)] in T2 `1 ) holds [[T1,T2],f] in MapsT X let f be Function of (T1 `2),(T2 `2); ::_thesis: ( ( T2 `2 = {} implies T1 `2 = {} ) & ( for x, y being set st [x,y] in T1 `1 holds [(f . x),(f . y)] in T2 `1 ) implies [[T1,T2],f] in MapsT X ) assume that A1: ( T2 `2 = {} implies T1 `2 = {} ) and A2: for x, y being set st [x,y] in T1 `1 holds [(f . x),(f . y)] in T2 `1 ; ::_thesis: [[T1,T2],f] in MapsT X reconsider f9 = f as Element of FuncsT X by A1, Th39; for x, y being set st [x,y] in T1 `1 holds [(f9 . x),(f9 . y)] in T2 `1 by A2; hence [[T1,T2],f] in MapsT X by A1; ::_thesis: verum end; registration let X be set ; let m be Element of MapsT X; clusterm `2 -> Relation-like Function-like ; coherence ( m `2 is Function-like & m `2 is Relation-like ) proof consider f being Element of FuncsT X, T1, T2 being Element of TOL X such that W: ( m = [[T1,T2],f] & ( T2 `2 = {} implies T1 `2 = {} ) & f is Function of (T1 `2),(T2 `2) & ( for x, y being set st [x,y] in T1 `1 holds [(f . x),(f . y)] in T2 `1 ) ) by Th40; [[T1,T2],f] `2 = f ; hence ( m `2 is Function-like & m `2 is Relation-like ) by W; ::_thesis: verum end; end; definition let X be set ; let m be Element of MapsT X; func dom m -> Element of TOL X equals :: COH_SP:def 21 (m `1) `1 ; coherence (m `1) `1 is Element of TOL X proof consider f being Element of FuncsT X, T1, T2 being Element of TOL X such that A1: m = [[T1,T2],f] and ( T2 `2 = {} implies T1 `2 = {} ) and f is Function of (T1 `2),(T2 `2) and for x, y being set st [x,y] in T1 `1 holds [(f . x),(f . y)] in T2 `1 by Th40; ( [T1,T2] = [[T1,T2],f] `1 & [T1,T2] `1 = T1 ) ; hence (m `1) `1 is Element of TOL X by A1; ::_thesis: verum end; func cod m -> Element of TOL X equals :: COH_SP:def 22 (m `1) `2 ; coherence (m `1) `2 is Element of TOL X proof consider f being Element of FuncsT X, T1, T2 being Element of TOL X such that A2: m = [[T1,T2],f] and ( T2 `2 = {} implies T1 `2 = {} ) and f is Function of (T1 `2),(T2 `2) and for x, y being set st [x,y] in T1 `1 holds [(f . x),(f . y)] in T2 `1 by Th40; ( [T1,T2] = [[T1,T2],f] `1 & [T1,T2] `2 = T2 ) ; hence (m `1) `2 is Element of TOL X by A2; ::_thesis: verum end; end; :: deftheorem defines dom COH_SP:def_21_:_ for X being set for m being Element of MapsT X holds dom m = (m `1) `1 ; :: deftheorem defines cod COH_SP:def_22_:_ for X being set for m being Element of MapsT X holds cod m = (m `1) `2 ; theorem Th42: :: COH_SP:42 for X being set for m being Element of MapsT X holds m = [[(dom m),(cod m)],(m `2)] proof let X be set ; ::_thesis: for m being Element of MapsT X holds m = [[(dom m),(cod m)],(m `2)] let m be Element of MapsT X; ::_thesis: m = [[(dom m),(cod m)],(m `2)] consider f being Element of FuncsT X, T1, T2 being Element of TOL X such that A1: m = [[T1,T2],f] and ( T2 `2 = {} implies T1 `2 = {} ) and f is Function of (T1 `2),(T2 `2) and for x, y being set st [x,y] in T1 `1 holds [(f . x),(f . y)] in T2 `1 by Th40; [T1,T2] = [[T1,T2],f] `1 ; then m `1 = [(dom m),(cod m)] by A1, MCART_1:8; hence m = [[(dom m),(cod m)],(m `2)] by A1, MCART_1:8; ::_thesis: verum end; Lm3: for X being set for m, m1 being Element of MapsT X st m `2 = m1 `2 & dom m = dom m1 & cod m = cod m1 holds m = m1 proof let X be set ; ::_thesis: for m, m1 being Element of MapsT X st m `2 = m1 `2 & dom m = dom m1 & cod m = cod m1 holds m = m1 let m, m1 be Element of MapsT X; ::_thesis: ( m `2 = m1 `2 & dom m = dom m1 & cod m = cod m1 implies m = m1 ) m = [[(dom m),(cod m)],(m `2)] by Th42; hence ( m `2 = m1 `2 & dom m = dom m1 & cod m = cod m1 implies m = m1 ) by Th42; ::_thesis: verum end; definition let X be set ; let T be Element of TOL X; func id\$ T -> Element of MapsT X equals :: COH_SP:def 23 [[T,T],(id (T `2))]; coherence [[T,T],(id (T `2))] is Element of MapsT X proof set f = id (T `2); now__::_thesis:_for_x,_y_being_set_st_[x,y]_in_T_`1_holds_ [((id_(T_`2))_._x),((id_(T_`2))_._y)]_in_T_`1 let x, y be set ; ::_thesis: ( [x,y] in T `1 implies [((id (T `2)) . x),((id (T `2)) . y)] in T `1 ) assume A1: [x,y] in T `1 ; ::_thesis: [((id (T `2)) . x),((id (T `2)) . y)] in T `1 then x in T `2 by ZFMISC_1:87; then A2: (id (T `2)) . x = x by FUNCT_1:18; y in T `2 by A1, ZFMISC_1:87; hence [((id (T `2)) . x),((id (T `2)) . y)] in T `1 by A1, A2, FUNCT_1:18; ::_thesis: verum end; hence [[T,T],(id (T `2))] is Element of MapsT X by Th41; ::_thesis: verum end; end; :: deftheorem defines id\$ COH_SP:def_23_:_ for X being set for T being Element of TOL X holds id\$ T = [[T,T],(id (T `2))]; theorem Th43: :: COH_SP:43 for X being set for m being Element of MapsT X holds ( ( (cod m) `2 <> {} or (dom m) `2 = {} ) & m `2 is Function of ((dom m) `2),((cod m) `2) & ( for x, y being set st [x,y] in (dom m) `1 holds [((m `2) . x),((m `2) . y)] in (cod m) `1 ) ) proof let X be set ; ::_thesis: for m being Element of MapsT X holds ( ( (cod m) `2 <> {} or (dom m) `2 = {} ) & m `2 is Function of ((dom m) `2),((cod m) `2) & ( for x, y being set st [x,y] in (dom m) `1 holds [((m `2) . x),((m `2) . y)] in (cod m) `1 ) ) let m be Element of MapsT X; ::_thesis: ( ( (cod m) `2 <> {} or (dom m) `2 = {} ) & m `2 is Function of ((dom m) `2),((cod m) `2) & ( for x, y being set st [x,y] in (dom m) `1 holds [((m `2) . x),((m `2) . y)] in (cod m) `1 ) ) consider f being Element of FuncsT X, T1, T2 being Element of TOL X such that A1: m = [[T1,T2],f] and A2: ( ( T2 `2 = {} implies T1 `2 = {} ) & f is Function of (T1 `2),(T2 `2) ) and A3: for x, y being set st [x,y] in T1 `1 holds [(f . x),(f . y)] in T2 `1 by Th40; A4: m = [[(dom m),(cod m)],(m `2)] by Th42; then A5: T2 = cod m by A1, Lm2; A6: ( f = m `2 & T1 = dom m ) by A1, A4, Lm2, XTUPLE_0:1; hence ( ( (cod m) `2 <> {} or (dom m) `2 = {} ) & m `2 is Function of ((dom m) `2),((cod m) `2) ) by A1, A2, A4, Lm2; ::_thesis: for x, y being set st [x,y] in (dom m) `1 holds [((m `2) . x),((m `2) . y)] in (cod m) `1 let x, y be set ; ::_thesis: ( [x,y] in (dom m) `1 implies [((m `2) . x),((m `2) . y)] in (cod m) `1 ) assume [x,y] in (dom m) `1 ; ::_thesis: [((m `2) . x),((m `2) . y)] in (cod m) `1 hence [((m `2) . x),((m `2) . y)] in (cod m) `1 by A3, A6, A5; ::_thesis: verum end; definition let X be set ; let m1, m2 be Element of MapsT X; assume A1: cod m1 = dom m2 ; funcm2 * m1 -> Element of MapsT X equals :Def24: :: COH_SP:def 24 [[(dom m1),(cod m2)],((m2 `2) * (m1 `2))]; coherence [[(dom m1),(cod m2)],((m2 `2) * (m1 `2))] is Element of MapsT X proof A2: ( (cod m2) `2 <> {} or (dom m2) `2 = {} ) by Th43; A3: ( (cod m1) `2 <> {} or (dom m1) `2 = {} ) by Th43; A4: m1 `2 is Function of ((dom m1) `2),((cod m1) `2) by Th43; A5: now__::_thesis:_for_x,_y_being_set_st_[x,y]_in_(dom_m1)_`1_holds_ [(((m2_`2)_*_(m1_`2))_._x),(((m2_`2)_*_(m1_`2))_._y)]_in_(cod_m2)_`1 let x, y be set ; ::_thesis: ( [x,y] in (dom m1) `1 implies [(((m2 `2) * (m1 `2)) . x),(((m2 `2) * (m1 `2)) . y)] in (cod m2) `1 ) assume A6: [x,y] in (dom m1) `1 ; ::_thesis: [(((m2 `2) * (m1 `2)) . x),(((m2 `2) * (m1 `2)) . y)] in (cod m2) `1 then x in (dom m1) `2 by ZFMISC_1:87; then A7: x in dom (m1 `2) by A3, A4, FUNCT_2:def_1; y in (dom m1) `2 by A6, ZFMISC_1:87; then A8: y in dom (m1 `2) by A3, A4, FUNCT_2:def_1; [((m1 `2) . x),((m1 `2) . y)] in (cod m1) `1 by A6, Th43; then [((m2 `2) . ((m1 `2) . x)),((m2 `2) . ((m1 `2) . y))] in (cod m2) `1 by A1, Th43; then [(((m2 `2) * (m1 `2)) . x),((m2 `2) . ((m1 `2) . y))] in (cod m2) `1 by A7, FUNCT_1:13; hence [(((m2 `2) * (m1 `2)) . x),(((m2 `2) * (m1 `2)) . y)] in (cod m2) `1 by A8, FUNCT_1:13; ::_thesis: verum end; m2 `2 is Function of ((dom m2) `2),((cod m2) `2) by Th43; then (m2 `2) * (m1 `2) is Function of ((dom m1) `2),((cod m2) `2) by A1, A3, A4, FUNCT_2:13; hence [[(dom m1),(cod m2)],((m2 `2) * (m1 `2))] is Element of MapsT X by A1, A3, A2, A5, Th41; ::_thesis: verum end; end; :: deftheorem Def24 defines * COH_SP:def_24_:_ for X being set for m1, m2 being Element of MapsT X st cod m1 = dom m2 holds m2 * m1 = [[(dom m1),(cod m2)],((m2 `2) * (m1 `2))]; theorem Th44: :: COH_SP:44 for X being set for m2, m1 being Element of MapsT X st dom m2 = cod m1 holds ( (m2 * m1) `2 = (m2 `2) * (m1 `2) & dom (m2 * m1) = dom m1 & cod (m2 * m1) = cod m2 ) proof let X be set ; ::_thesis: for m2, m1 being Element of MapsT X st dom m2 = cod m1 holds ( (m2 * m1) `2 = (m2 `2) * (m1 `2) & dom (m2 * m1) = dom m1 & cod (m2 * m1) = cod m2 ) let m2, m1 be Element of MapsT X; ::_thesis: ( dom m2 = cod m1 implies ( (m2 * m1) `2 = (m2 `2) * (m1 `2) & dom (m2 * m1) = dom m1 & cod (m2 * m1) = cod m2 ) ) assume dom m2 = cod m1 ; ::_thesis: ( (m2 * m1) `2 = (m2 `2) * (m1 `2) & dom (m2 * m1) = dom m1 & cod (m2 * m1) = cod m2 ) then [[(dom m1),(cod m2)],((m2 `2) * (m1 `2))] = m2 * m1 by Def24 .= [[(dom (m2 * m1)),(cod (m2 * m1))],((m2 * m1) `2)] by Th42 ; hence ( (m2 * m1) `2 = (m2 `2) * (m1 `2) & dom (m2 * m1) = dom m1 & cod (m2 * m1) = cod m2 ) by Lm2, XTUPLE_0:1; ::_thesis: verum end; theorem Th45: :: COH_SP:45 for X being set for m2, m1, m3 being Element of MapsT X st dom m2 = cod m1 & dom m3 = cod m2 holds m3 * (m2 * m1) = (m3 * m2) * m1 proof let X be set ; ::_thesis: for m2, m1, m3 being Element of MapsT X st dom m2 = cod m1 & dom m3 = cod m2 holds m3 * (m2 * m1) = (m3 * m2) * m1 let m2, m1, m3 be Element of MapsT X; ::_thesis: ( dom m2 = cod m1 & dom m3 = cod m2 implies m3 * (m2 * m1) = (m3 * m2) * m1 ) assume that A1: dom m2 = cod m1 and A2: dom m3 = cod m2 ; ::_thesis: m3 * (m2 * m1) = (m3 * m2) * m1 A3: cod (m2 * m1) = cod m2 by A1, Th44; (m2 * m1) `2 = (m2 `2) * (m1 `2) by A1, Th44; then A4: (m3 * (m2 * m1)) `2 = (m3 `2) * ((m2 `2) * (m1 `2)) by A2, A3, Th44; A5: dom (m3 * m2) = dom m2 by A2, Th44; then A6: dom ((m3 * m2) * m1) = dom m1 by A1, Th44; dom (m2 * m1) = dom m1 by A1, Th44; then A7: dom (m3 * (m2 * m1)) = dom m1 by A2, A3, Th44; cod (m3 * m2) = cod m3 by A2, Th44; then A8: cod ((m3 * m2) * m1) = cod m3 by A1, A5, Th44; (m3 * m2) `2 = (m3 `2) * (m2 `2) by A2, Th44; then A9: ((m3 * m2) * m1) `2 = ((m3 `2) * (m2 `2)) * (m1 `2) by A1, A5, Th44; cod (m3 * (m2 * m1)) = cod m3 by A2, A3, Th44; hence m3 * (m2 * m1) = (m3 * m2) * m1 by A4, A7, A9, A6, A8, Lm3, RELAT_1:36; ::_thesis: verum end; theorem Th46: :: COH_SP:46 for X being set for T being Element of TOL X holds ( (id\$ T) `2 = id (T `2) & dom (id\$ T) = T & cod (id\$ T) = T ) proof let X be set ; ::_thesis: for T being Element of TOL X holds ( (id\$ T) `2 = id (T `2) & dom (id\$ T) = T & cod (id\$ T) = T ) let T be Element of TOL X; ::_thesis: ( (id\$ T) `2 = id (T `2) & dom (id\$ T) = T & cod (id\$ T) = T ) [[(dom (id\$ T)),(cod (id\$ T))],((id\$ T) `2)] = [[T,T],(id (T `2))] by Th42; hence ( (id\$ T) `2 = id (T `2) & dom (id\$ T) = T & cod (id\$ T) = T ) by Lm2, XTUPLE_0:1; ::_thesis: verum end; theorem Th47: :: COH_SP:47 for X being set for m being Element of MapsT X holds ( m * (id\$ (dom m)) = m & (id\$ (cod m)) * m = m ) proof let X be set ; ::_thesis: for m being Element of MapsT X holds ( m * (id\$ (dom m)) = m & (id\$ (cod m)) * m = m ) let m be Element of MapsT X; ::_thesis: ( m * (id\$ (dom m)) = m & (id\$ (cod m)) * m = m ) set i1 = id\$ (dom m); set i2 = id\$ (cod m); A1: ( (id\$ (dom m)) `2 = id ((dom m) `2) & dom (id\$ (dom m)) = dom m ) by Th46; A2: m `2 is Function of ((dom m) `2),((cod m) `2) by Th43; then A3: rng (m `2) c= (cod m) `2 by RELAT_1:def_19; ( (cod m) `2 <> {} or (dom m) `2 = {} ) by Th43; then A4: dom (m `2) = (dom m) `2 by A2, FUNCT_2:def_1; A5: cod (id\$ (dom m)) = dom m by Th46; then A6: cod (m * (id\$ (dom m))) = cod m by Th44; ( (m * (id\$ (dom m))) `2 = (m `2) * ((id\$ (dom m)) `2) & dom (m * (id\$ (dom m))) = dom (id\$ (dom m)) ) by A5, Th44; hence m * (id\$ (dom m)) = m by A4, A1, A6, Lm3, RELAT_1:52; ::_thesis: (id\$ (cod m)) * m = m A7: ( (id\$ (cod m)) `2 = id ((cod m) `2) & cod (id\$ (cod m)) = cod m ) by Th46; A8: dom (id\$ (cod m)) = cod m by Th46; then A9: cod ((id\$ (cod m)) * m) = cod (id\$ (cod m)) by Th44; ( ((id\$ (cod m)) * m) `2 = ((id\$ (cod m)) `2) * (m `2) & dom ((id\$ (cod m)) * m) = dom m ) by A8, Th44; hence (id\$ (cod m)) * m = m by A3, A7, A9, Lm3, RELAT_1:53; ::_thesis: verum end; definition let X be set ; func fDom X -> Function of (MapsT X),(TOL X) means :Def25: :: COH_SP:def 25 for m being Element of MapsT X holds it . m = dom m; existence ex b1 being Function of (MapsT X),(TOL X) st for m being Element of MapsT X holds b1 . m = dom m proof deffunc H1( Element of MapsT X) -> Element of TOL X = dom \$1; thus ex f being Function of (MapsT X),(TOL X) st for x being Element of MapsT X holds f . x = H1(x) from FUNCT_2:sch_4(); ::_thesis: verum end; uniqueness for b1, b2 being Function of (MapsT X),(TOL X) st ( for m being Element of MapsT X holds b1 . m = dom m ) & ( for m being Element of MapsT X holds b2 . m = dom m ) holds b1 = b2 proof let h1, h2 be Function of (MapsT X),(TOL X); ::_thesis: ( ( for m being Element of MapsT X holds h1 . m = dom m ) & ( for m being Element of MapsT X holds h2 . m = dom m ) implies h1 = h2 ) assume that A1: for m being Element of MapsT X holds h1 . m = dom m and A2: for m being Element of MapsT X holds h2 . m = dom m ; ::_thesis: h1 = h2 now__::_thesis:_for_m_being_Element_of_MapsT_X_holds_h1_._m_=_h2_._m let m be Element of MapsT X; ::_thesis: h1 . m = h2 . m thus h1 . m = dom m by A1 .= h2 . m by A2 ; ::_thesis: verum end; hence h1 = h2 by FUNCT_2:63; ::_thesis: verum end; func fCod X -> Function of (MapsT X),(TOL X) means :Def26: :: COH_SP:def 26 for m being Element of MapsT X holds it . m = cod m; existence ex b1 being Function of (MapsT X),(TOL X) st for m being Element of MapsT X holds b1 . m = cod m proof deffunc H1( Element of MapsT X) -> Element of TOL X = cod \$1; thus ex f being Function of (MapsT X),(TOL X) st for x being Element of MapsT X holds f . x = H1(x) from FUNCT_2:sch_4(); ::_thesis: verum end; uniqueness for b1, b2 being Function of (MapsT X),(TOL X) st ( for m being Element of MapsT X holds b1 . m = cod m ) & ( for m being Element of MapsT X holds b2 . m = cod m ) holds b1 = b2 proof let h1, h2 be Function of (MapsT X),(TOL X); ::_thesis: ( ( for m being Element of MapsT X holds h1 . m = cod m ) & ( for m being Element of MapsT X holds h2 . m = cod m ) implies h1 = h2 ) assume that A3: for m being Element of MapsT X holds h1 . m = cod m and A4: for m being Element of MapsT X holds h2 . m = cod m ; ::_thesis: h1 = h2 now__::_thesis:_for_m_being_Element_of_MapsT_X_holds_h1_._m_=_h2_._m let m be Element of MapsT X; ::_thesis: h1 . m = h2 . m thus h1 . m = cod m by A3 .= h2 . m by A4 ; ::_thesis: verum end; hence h1 = h2 by FUNCT_2:63; ::_thesis: verum end; func fComp X -> PartFunc of [:(MapsT X),(MapsT X):],(MapsT X) means :Def27: :: COH_SP:def 27 ( ( for m2, m1 being Element of MapsT X holds ( [m2,m1] in dom it iff dom m2 = cod m1 ) ) & ( for m2, m1 being Element of MapsT X st dom m2 = cod m1 holds it . [m2,m1] = m2 * m1 ) ); existence ex b1 being PartFunc of [:(MapsT X),(MapsT X):],(MapsT X) st ( ( for m2, m1 being Element of MapsT X holds ( [m2,m1] in dom b1 iff dom m2 = cod m1 ) ) & ( for m2, m1 being Element of MapsT X st dom m2 = cod m1 holds b1 . [m2,m1] = m2 * m1 ) ) proof defpred S1[ set , set , set ] means for m2, m1 being Element of MapsT X st m2 = \$1 & m1 = \$2 holds ( dom m2 = cod m1 & \$3 = m2 * m1 ); A5: for x, y, z1, z2 being set st x in MapsT X & y in MapsT X & S1[x,y,z1] & S1[x,y,z2] holds z1 = z2 proof let x, y, z1, z2 be set ; ::_thesis: ( x in MapsT X & y in MapsT X & S1[x,y,z1] & S1[x,y,z2] implies z1 = z2 ) assume ( x in MapsT X & y in MapsT X ) ; ::_thesis: ( not S1[x,y,z1] or not S1[x,y,z2] or z1 = z2 ) then reconsider m2 = x, m1 = y as Element of MapsT X ; assume that A6: S1[x,y,z1] and A7: S1[x,y,z2] ; ::_thesis: z1 = z2 z1 = m2 * m1 by A6; hence z1 = z2 by A7; ::_thesis: verum end; A8: for x, y, z being set st x in MapsT X & y in MapsT X & S1[x,y,z] holds z in MapsT X proof let x, y, z be set ; ::_thesis: ( x in MapsT X & y in MapsT X & S1[x,y,z] implies z in MapsT X ) assume ( x in MapsT X & y in MapsT X ) ; ::_thesis: ( not S1[x,y,z] or z in MapsT X ) then reconsider m2 = x, m1 = y as Element of MapsT X ; assume S1[x,y,z] ; ::_thesis: z in MapsT X then z = m2 * m1 ; hence z in MapsT X ; ::_thesis: verum end; consider h being PartFunc of [:(MapsT X),(MapsT X):],(MapsT X) such that A9: for x, y being set holds ( [x,y] in dom h iff ( x in MapsT X & y in MapsT X & ex z being set st S1[x,y,z] ) ) and A10: for x, y being set st [x,y] in dom h holds S1[x,y,h . (x,y)] from BINOP_1:sch_5(A8, A5); take h ; ::_thesis: ( ( for m2, m1 being Element of MapsT X holds ( [m2,m1] in dom h iff dom m2 = cod m1 ) ) & ( for m2, m1 being Element of MapsT X st dom m2 = cod m1 holds h . [m2,m1] = m2 * m1 ) ) thus A11: for m2, m1 being Element of MapsT X holds ( [m2,m1] in dom h iff dom m2 = cod m1 ) ::_thesis: for m2, m1 being Element of MapsT X st dom m2 = cod m1 holds h . [m2,m1] = m2 * m1 proof let m2, m1 be Element of MapsT X; ::_thesis: ( [m2,m1] in dom h iff dom m2 = cod m1 ) thus ( [m2,m1] in dom h implies dom m2 = cod m1 ) ::_thesis: ( dom m2 = cod m1 implies [m2,m1] in dom h ) proof assume [m2,m1] in dom h ; ::_thesis: dom m2 = cod m1 then ex z being set st S1[m2,m1,z] by A9; hence dom m2 = cod m1 ; ::_thesis: verum end; assume dom m2 = cod m1 ; ::_thesis: [m2,m1] in dom h then S1[m2,m1,m2 * m1] ; hence [m2,m1] in dom h by A9; ::_thesis: verum end; let m2, m1 be Element of MapsT X; ::_thesis: ( dom m2 = cod m1 implies h . [m2,m1] = m2 * m1 ) assume dom m2 = cod m1 ; ::_thesis: h . [m2,m1] = m2 * m1 then [m2,m1] in dom h by A11; then S1[m2,m1,h . (m2,m1)] by A10; hence h . [m2,m1] = m2 * m1 ; ::_thesis: verum end; uniqueness for b1, b2 being PartFunc of [:(MapsT X),(MapsT X):],(MapsT X) st ( for m2, m1 being Element of MapsT X holds ( [m2,m1] in dom b1 iff dom m2 = cod m1 ) ) & ( for m2, m1 being Element of MapsT X st dom m2 = cod m1 holds b1 . [m2,m1] = m2 * m1 ) & ( for m2, m1 being Element of MapsT X holds ( [m2,m1] in dom b2 iff dom m2 = cod m1 ) ) & ( for m2, m1 being Element of MapsT X st dom m2 = cod m1 holds b2 . [m2,m1] = m2 * m1 ) holds b1 = b2 proof let h1, h2 be PartFunc of [:(MapsT X),(MapsT X):],(MapsT X); ::_thesis: ( ( for m2, m1 being Element of MapsT X holds ( [m2,m1] in dom h1 iff dom m2 = cod m1 ) ) & ( for m2, m1 being Element of MapsT X st dom m2 = cod m1 holds h1 . [m2,m1] = m2 * m1 ) & ( for m2, m1 being Element of MapsT X holds ( [m2,m1] in dom h2 iff dom m2 = cod m1 ) ) & ( for m2, m1 being Element of MapsT X st dom m2 = cod m1 holds h2 . [m2,m1] = m2 * m1 ) implies h1 = h2 ) assume that A12: for m2, m1 being Element of MapsT X holds ( [m2,m1] in dom h1 iff dom m2 = cod m1 ) and A13: for m2, m1 being Element of MapsT X st dom m2 = cod m1 holds h1 . [m2,m1] = m2 * m1 and A14: for m2, m1 being Element of MapsT X holds ( [m2,m1] in dom h2 iff dom m2 = cod m1 ) and A15: for m2, m1 being Element of MapsT X st dom m2 = cod m1 holds h2 . [m2,m1] = m2 * m1 ; ::_thesis: h1 = h2 A16: dom h1 = dom h2 proof let x, y be set ; :: according to RELAT_1:def_2 ::_thesis: ( ( not [x,y] in dom h1 or [x,y] in dom h2 ) & ( not [x,y] in dom h2 or [x,y] in dom h1 ) ) thus ( [x,y] in dom h1 implies [x,y] in dom h2 ) ::_thesis: ( not [x,y] in dom h2 or [x,y] in dom h1 ) proof assume A17: [x,y] in dom h1 ; ::_thesis: [x,y] in dom h2 then reconsider m2 = x, m1 = y as Element of MapsT X by ZFMISC_1:87; dom m2 = cod m1 by A12, A17; hence [x,y] in dom h2 by A14; ::_thesis: verum end; assume A18: [x,y] in dom h2 ; ::_thesis: [x,y] in dom h1 then reconsider m2 = x, m1 = y as Element of MapsT X by ZFMISC_1:87; dom m2 = cod m1 by A14, A18; hence [x,y] in dom h1 by A12; ::_thesis: verum end; now__::_thesis:_for_m_being_Element_of_[:(MapsT_X),(MapsT_X):]_st_m_in_dom_h1_holds_ h1_._m_=_h2_._m let m be Element of [:(MapsT X),(MapsT X):]; ::_thesis: ( m in dom h1 implies h1 . m = h2 . m ) assume A19: m in dom h1 ; ::_thesis: h1 . m = h2 . m consider m2, m1 being Element of MapsT X such that A20: m = [m2,m1] by DOMAIN_1:1; A21: dom m2 = cod m1 by A12, A19, A20; then h1 . [m2,m1] = m2 * m1 by A13; hence h1 . m = h2 . m by A15, A20, A21; ::_thesis: verum end; hence h1 = h2 by A16, PARTFUN1:5; ::_thesis: verum end; end; :: deftheorem Def25 defines fDom COH_SP:def_25_:_ for X being set for b2 being Function of (MapsT X),(TOL X) holds ( b2 = fDom X iff for m being Element of MapsT X holds b2 . m = dom m ); :: deftheorem Def26 defines fCod COH_SP:def_26_:_ for X being set for b2 being Function of (MapsT X),(TOL X) holds ( b2 = fCod X iff for m being Element of MapsT X holds b2 . m = cod m ); :: deftheorem Def27 defines fComp COH_SP:def_27_:_ for X being set for b2 being PartFunc of [:(MapsT X),(MapsT X):],(MapsT X) holds ( b2 = fComp X iff ( ( for m2, m1 being Element of MapsT X holds ( [m2,m1] in dom b2 iff dom m2 = cod m1 ) ) & ( for m2, m1 being Element of MapsT X st dom m2 = cod m1 holds b2 . [m2,m1] = m2 * m1 ) ) ); definition canceled; let X be set ; func TolCat X -> non empty non void strict CatStr equals :: COH_SP:def 29 CatStr(# (TOL X),(MapsT X),(fDom X),(fCod X),(fComp X) #); coherence CatStr(# (TOL X),(MapsT X),(fDom X),(fCod X),(fComp X) #) is non empty non void strict CatStr ; end; :: deftheorem COH_SP:def_28_:_ canceled; :: deftheorem defines TolCat COH_SP:def_29_:_ for X being set holds TolCat X = CatStr(# (TOL X),(MapsT X),(fDom X),(fCod X),(fComp X) #); registration let X be set ; cluster TolCat X -> non empty non void strict Category-like transitive associative reflexive ; coherence ( TolCat X is Category-like & TolCat X is transitive & TolCat X is associative & TolCat X is reflexive ) proof set C = TolCat X; set M = MapsT X; set d = fDom X; set c = fCod X; set p = fComp X; thus P1: TolCat X is Category-like ::_thesis: ( TolCat X is transitive & TolCat X is associative & TolCat X is reflexive ) proof let ff, gg be Morphism of (TolCat X); :: according to CAT_1:def_6 ::_thesis: ( ( not [gg,ff] in proj1 the Comp of (TolCat X) or dom gg = cod ff ) & ( not dom gg = cod ff or [gg,ff] in proj1 the Comp of (TolCat X) ) ) reconsider f = ff, g = gg as Element of MapsT X ; ( (fDom X) . g = dom g & (fCod X) . f = cod f ) by Def25, Def26; hence ( ( not [gg,ff] in proj1 the Comp of (TolCat X) or dom gg = cod ff ) & ( not dom gg = cod ff or [gg,ff] in proj1 the Comp of (TolCat X) ) ) by Def27; ::_thesis: verum end; thus P2: TolCat X is transitive ::_thesis: ( TolCat X is associative & TolCat X is reflexive ) proof let ff, gg be Morphism of (TolCat X); :: according to CAT_1:def_7 ::_thesis: ( not dom gg = cod ff or ( dom (gg (*) ff) = dom ff & cod (gg (*) ff) = cod gg ) ) assume A1: dom gg = cod ff ; ::_thesis: ( dom (gg (*) ff) = dom ff & cod (gg (*) ff) = cod gg ) [gg,ff] in dom the Comp of (TolCat X) by A1, P1, CAT_1:def_6; then U: the Comp of (TolCat X) . (gg,ff) = gg (*) ff by CAT_1:def_1; reconsider f = ff, g = gg as Element of MapsT X ; A2: ( (fDom X) . g = dom g & (fCod X) . f = cod f ) by Def25, Def26; then A3: (fComp X) . [g,f] = g * f by A1, Def27; A4: ( (fDom X) . f = dom f & (fCod X) . g = cod g ) by Def25, Def26; ( dom (g * f) = dom f & cod (g * f) = cod g ) by A1, A2, Th44; hence ( dom (gg (*) ff) = dom ff & cod (gg (*) ff) = cod gg ) by A3, A4, Def25, Def26, U; ::_thesis: verum end; thus TolCat X is associative ::_thesis: TolCat X is reflexive proof let ff, gg, hh be Morphism of (TolCat X); :: according to CAT_1:def_8 ::_thesis: ( not dom hh = cod gg or not dom gg = cod ff or hh (*) (gg (*) ff) = (hh (*) gg) (*) ff ) assume that A5: dom hh = cod gg and A6: dom gg = cod ff ; ::_thesis: hh (*) (gg (*) ff) = (hh (*) gg) (*) ff reconsider f = ff, g = gg, h = hh as Element of MapsT X ; A7: ( dom h = (fDom X) . h & cod g = (fCod X) . g ) by Def25, Def26; then A8: dom (h * g) = dom g by A5, Th44; A9: ( dom g = (fDom X) . g & cod f = (fCod X) . f ) by Def25, Def26; then A10: cod (g * f) = dom h by A5, A6, A7, Th44; [hh,gg] in dom the Comp of (TolCat X) by A5, P1, CAT_1:def_6; then X2: hh (*) gg = the Comp of (TolCat X) . (hh,gg) by CAT_1:def_1; [gg,ff] in dom the Comp of (TolCat X) by A6, P1, CAT_1:def_6; then X1: gg (*) ff = the Comp of (TolCat X) . (gg,ff) by CAT_1:def_1; dom (hh (*) gg) = dom gg by P2, CAT_1:def_7, A5; then X3: [(hh (*) gg),ff] in dom the Comp of (TolCat X) by P1, CAT_1:def_6, A6; cod (gg (*) ff) = cod gg by P2, CAT_1:def_7, A6; then [hh,(gg (*) ff)] in dom the Comp of (TolCat X) by P1, CAT_1:def_6, A5; hence hh (*) (gg (*) ff) = the Comp of (TolCat X) . (hh,( the Comp of (TolCat X) . (gg,ff))) by X1, CAT_1:def_1 .= (fComp X) . [h,(g * f)] by A6, A9, Def27 .= h * (g * f) by A10, Def27 .= (h * g) * f by A5, A6, A7, A9, Th45 .= (fComp X) . [(h * g),f] by A6, A9, A8, Def27 .= the Comp of (TolCat X) . (( the Comp of (TolCat X) . (hh,gg)),ff) by A5, A7, Def27 .= (hh (*) gg) (*) ff by X2, X3, CAT_1:def_1 ; ::_thesis: verum end; let a be Object of (TolCat X); :: according to CAT_1:def_9 ::_thesis: not Hom (a,a) = {} reconsider aa = a as Element of TOL X ; reconsider ii = id\$ aa as Morphism of (TolCat X) ; A12: cod ii = cod (id\$ aa) by Def26 .= aa by Th46 ; dom ii = dom (id\$ aa) by Def25 .= aa by Th46 ; then id\$ aa in Hom (a,a) by A12; hence Hom (a,a) <> {} ; ::_thesis: verum end; end; LmX: for X being set for a being Element of (TolCat X) for aa being Element of TOL X st a = aa holds for i being Morphism of a,a st i = id\$ aa holds for b being Element of (TolCat X) holds ( ( Hom (a,b) <> {} implies for g being Morphism of a,b holds g (*) i = g ) & ( Hom (b,a) <> {} implies for f being Morphism of b,a holds i (*) f = f ) ) proof let X be set ; ::_thesis: for a being Element of (TolCat X) for aa being Element of TOL X st a = aa holds for i being Morphism of a,a st i = id\$ aa holds for b being Element of (TolCat X) holds ( ( Hom (a,b) <> {} implies for g being Morphism of a,b holds g (*) i = g ) & ( Hom (b,a) <> {} implies for f being Morphism of b,a holds i (*) f = f ) ) let a be Element of (TolCat X); ::_thesis: for aa being Element of TOL X st a = aa holds for i being Morphism of a,a st i = id\$ aa holds for b being Element of (TolCat X) holds ( ( Hom (a,b) <> {} implies for g being Morphism of a,b holds g (*) i = g ) & ( Hom (b,a) <> {} implies for f being Morphism of b,a holds i (*) f = f ) ) let aa be Element of TOL X; ::_thesis: ( a = aa implies for i being Morphism of a,a st i = id\$ aa holds for b being Element of (TolCat X) holds ( ( Hom (a,b) <> {} implies for g being Morphism of a,b holds g (*) i = g ) & ( Hom (b,a) <> {} implies for f being Morphism of b,a holds i (*) f = f ) ) ) assume Z1: a = aa ; ::_thesis: for i being Morphism of a,a st i = id\$ aa holds for b being Element of (TolCat X) holds ( ( Hom (a,b) <> {} implies for g being Morphism of a,b holds g (*) i = g ) & ( Hom (b,a) <> {} implies for f being Morphism of b,a holds i (*) f = f ) ) let i be Morphism of a,a; ::_thesis: ( i = id\$ aa implies for b being Element of (TolCat X) holds ( ( Hom (a,b) <> {} implies for g being Morphism of a,b holds g (*) i = g ) & ( Hom (b,a) <> {} implies for f being Morphism of b,a holds i (*) f = f ) ) ) assume Z2: i = id\$ aa ; ::_thesis: for b being Element of (TolCat X) holds ( ( Hom (a,b) <> {} implies for g being Morphism of a,b holds g (*) i = g ) & ( Hom (b,a) <> {} implies for f being Morphism of b,a holds i (*) f = f ) ) let b be Element of (TolCat X); ::_thesis: ( ( Hom (a,b) <> {} implies for g being Morphism of a,b holds g (*) i = g ) & ( Hom (b,a) <> {} implies for f being Morphism of b,a holds i (*) f = f ) ) thus ( Hom (a,b) <> {} implies for g being Morphism of a,b holds g (*) i = g ) ::_thesis: ( Hom (b,a) <> {} implies for f being Morphism of b,a holds i (*) f = f ) proof assume Z3: Hom (a,b) <> {} ; ::_thesis: for g being Morphism of a,b holds g (*) i = g let g be Morphism of a,b; ::_thesis: g (*) i = g reconsider gg = g as Element of MapsT X ; Hom (a,a) <> {} ; then A1: cod i = a by CAT_1:5 .= dom g by Z3, CAT_1:5 ; A3: dom gg = dom g by Def25 .= aa by Z1, Z3, CAT_1:5 ; then A2: cod (id\$ aa) = dom gg by Th46; [g,i] in dom the Comp of (TolCat X) by A1, CAT_1:def_6; hence g (*) i = the Comp of (TolCat X) . (g,i) by CAT_1:def_1 .= gg * (id\$ aa) by A2, Z2, Def27 .= g by A3, Th47 ; ::_thesis: verum end; thus ( Hom (b,a) <> {} implies for f being Morphism of b,a holds i (*) f = f ) ::_thesis: verum proof assume Z3: Hom (b,a) <> {} ; ::_thesis: for f being Morphism of b,a holds i (*) f = f let g be Morphism of b,a; ::_thesis: i (*) g = g reconsider gg = g as Element of MapsT X ; Hom (a,a) <> {} ; then A1: dom i = a by CAT_1:5 .= cod g by Z3, CAT_1:5 ; A3: cod gg = cod g by Def26 .= aa by Z1, Z3, CAT_1:5 ; then A2: dom (id\$ aa) = cod gg by Th46; [i,g] in dom the Comp of (TolCat X) by A1, CAT_1:def_6; hence i (*) g = the Comp of (TolCat X) . (i,g) by CAT_1:def_1 .= (id\$ aa) * gg by Z2, A2, Def27 .= g by A3, Th47 ; ::_thesis: verum end; end; registration let X be set ; cluster TolCat X -> non empty non void strict with_identities ; coherence TolCat X is with_identities proof let a be Element of (TolCat X); :: according to CAT_1:def_10 ::_thesis: ex b1 being Morphism of a,a st for b2 being Element of the carrier of (TolCat X) holds ( ( Hom (a,b2) = {} or for b3 being Morphism of a,b2 holds b3 (*) b1 = b3 ) & ( Hom (b2,a) = {} or for b3 being Morphism of b2,a holds b1 (*) b3 = b3 ) ) reconsider aa = a as Element of TOL X ; reconsider ii = id\$ aa as Morphism of (TolCat X) ; A12: cod ii = cod (id\$ aa) by Def26 .= aa by Th46 ; dom ii = dom (id\$ aa) by Def25 .= aa by Th46 ; then ii in Hom (a,a) by A12; then reconsider ii = ii as Morphism of a,a by CAT_1:def_5; take ii ; ::_thesis: for b1 being Element of the carrier of (TolCat X) holds ( ( Hom (a,b1) = {} or for b2 being Morphism of a,b1 holds b2 (*) ii = b2 ) & ( Hom (b1,a) = {} or for b2 being Morphism of b1,a holds ii (*) b2 = b2 ) ) thus for b1 being Element of the carrier of (TolCat X) holds ( ( Hom (a,b1) = {} or for b2 being Morphism of a,b1 holds b2 (*) ii = b2 ) & ( Hom (b1,a) = {} or for b2 being Morphism of b1,a holds ii (*) b2 = b2 ) ) by LmX; ::_thesis: verum end; end;