:: MSUALG_8 semantic presentation begin theorem Th1: :: MSUALG_8:1 for n being Element of NAT for p being FinSequence holds ( 1 <= n & n < len p iff ( n in dom p & n + 1 in dom p ) ) proof let n be Element of NAT ; ::_thesis: for p being FinSequence holds ( 1 <= n & n < len p iff ( n in dom p & n + 1 in dom p ) ) let p be FinSequence; ::_thesis: ( 1 <= n & n < len p iff ( n in dom p & n + 1 in dom p ) ) thus ( 1 <= n & n < len p implies ( n in dom p & n + 1 in dom p ) ) ::_thesis: ( n in dom p & n + 1 in dom p implies ( 1 <= n & n < len p ) ) proof assume that A1: 1 <= n and A2: n < len p ; ::_thesis: ( n in dom p & n + 1 in dom p ) ( 1 <= n + 1 & n + 1 <= len p ) by A2, NAT_1:11, NAT_1:13; then A3: n + 1 in Seg (len p) by FINSEQ_1:1; n in Seg (len p) by A1, A2, FINSEQ_1:1; hence ( n in dom p & n + 1 in dom p ) by A3, FINSEQ_1:def_3; ::_thesis: verum end; thus ( n in dom p & n + 1 in dom p implies ( 1 <= n & n < len p ) ) ::_thesis: verum proof assume that A4: n in dom p and A5: n + 1 in dom p ; ::_thesis: ( 1 <= n & n < len p ) n + 1 in Seg (len p) by A5, FINSEQ_1:def_3; then A6: n + 1 <= len p by FINSEQ_1:1; n in Seg (len p) by A4, FINSEQ_1:def_3; hence ( 1 <= n & n < len p ) by A6, FINSEQ_1:1, NAT_1:13; ::_thesis: verum end; end; scheme :: MSUALG_8:sch 1 NonUniqSeqEx{ F1() -> Element of NAT , P1[ set , set ] } : ex p being FinSequence st ( dom p = Seg F1() & ( for k being Element of NAT st k in Seg F1() holds P1[k,p . k] ) ) provided A1: for k being Element of NAT st k in Seg F1() holds ex x being set st P1[k,x] proof A2: for x being set st x in Seg F1() holds ex y being set st P1[x,y] by A1; consider f being Function such that A3: ( dom f = Seg F1() & ( for x being set st x in Seg F1() holds P1[x,f . x] ) ) from CLASSES1:sch_1(A2); reconsider p = f as FinSequence by A3, FINSEQ_1:def_2; take p ; ::_thesis: ( dom p = Seg F1() & ( for k being Element of NAT st k in Seg F1() holds P1[k,p . k] ) ) thus ( dom p = Seg F1() & ( for k being Element of NAT st k in Seg F1() holds P1[k,p . k] ) ) by A3; ::_thesis: verum end; theorem Th2: :: MSUALG_8:2 for Y being set for a, b being Element of (EqRelLatt Y) for A, B being Equivalence_Relation of Y st a = A & b = B holds ( a [= b iff A c= B ) proof let Y be set ; ::_thesis: for a, b being Element of (EqRelLatt Y) for A, B being Equivalence_Relation of Y st a = A & b = B holds ( a [= b iff A c= B ) let a, b be Element of (EqRelLatt Y); ::_thesis: for A, B being Equivalence_Relation of Y st a = A & b = B holds ( a [= b iff A c= B ) let A, B be Equivalence_Relation of Y; ::_thesis: ( a = A & b = B implies ( a [= b iff A c= B ) ) assume that A1: a = A and A2: b = B ; ::_thesis: ( a [= b iff A c= B ) thus ( a [= b implies A c= B ) ::_thesis: ( A c= B implies a [= b ) proof assume A3: a [= b ; ::_thesis: A c= B A /\ B = the L_meet of (EqRelLatt Y) . (A,B) by MSUALG_5:def_2 .= a "/\" b by A1, A2, LATTICES:def_2 .= A by A1, A3, LATTICES:4 ; hence A c= B by XBOOLE_1:17; ::_thesis: verum end; thus ( A c= B implies a [= b ) ::_thesis: verum proof assume A4: A c= B ; ::_thesis: a [= b a "/\" b = the L_meet of (EqRelLatt Y) . (A,B) by A1, A2, LATTICES:def_2 .= A /\ B by MSUALG_5:def_2 .= a by A1, A4, XBOOLE_1:28 ; hence a [= b by LATTICES:4; ::_thesis: verum end; end; registration let Y be set ; cluster EqRelLatt Y -> bounded ; coherence EqRelLatt Y is bounded proof ex c being Element of (EqRelLatt Y) st for a being Element of (EqRelLatt Y) holds ( c "\/" a = c & a "\/" c = c ) proof set c9 = nabla Y; reconsider c = nabla Y as Element of (EqRelLatt Y) by MSUALG_5:21; take c ; ::_thesis: for a being Element of (EqRelLatt Y) holds ( c "\/" a = c & a "\/" c = c ) let a be Element of (EqRelLatt Y); ::_thesis: ( c "\/" a = c & a "\/" c = c ) reconsider a9 = a as Equivalence_Relation of Y by MSUALG_5:21; thus c "\/" a = the L_join of (EqRelLatt Y) . (c,a) by LATTICES:def_1 .= (nabla Y) "\/" a9 by MSUALG_5:def_2 .= EqCl ((nabla Y) \/ a9) by MSUALG_5:1 .= EqCl (nabla Y) by EQREL_1:1 .= c by MSUALG_5:2 ; ::_thesis: a "\/" c = c hence a "\/" c = c ; ::_thesis: verum end; then A1: EqRelLatt Y is upper-bounded by LATTICES:def_14; ex c being Element of (EqRelLatt Y) st for a being Element of (EqRelLatt Y) holds ( c "/\" a = c & a "/\" c = c ) proof set c9 = id Y; reconsider c = id Y as Element of (EqRelLatt Y) by MSUALG_5:21; take c ; ::_thesis: for a being Element of (EqRelLatt Y) holds ( c "/\" a = c & a "/\" c = c ) let a be Element of (EqRelLatt Y); ::_thesis: ( c "/\" a = c & a "/\" c = c ) reconsider a9 = a as Equivalence_Relation of Y by MSUALG_5:21; thus c "/\" a = the L_meet of (EqRelLatt Y) . (c,a) by LATTICES:def_2 .= (id Y) /\ a9 by MSUALG_5:def_2 .= c by EQREL_1:10 ; ::_thesis: a "/\" c = c hence a "/\" c = c ; ::_thesis: verum end; then EqRelLatt Y is lower-bounded by LATTICES:def_13; hence EqRelLatt Y is bounded by A1; ::_thesis: verum end; end; theorem :: MSUALG_8:3 for Y being set holds Bottom (EqRelLatt Y) = id Y proof let Y be set ; ::_thesis: Bottom (EqRelLatt Y) = id Y reconsider K = id Y as Element of (EqRelLatt Y) by MSUALG_5:21; now__::_thesis:_for_a_being_Element_of_(EqRelLatt_Y)_holds_ (_K_"/\"_a_=_K_&_a_"/\"_K_=_K_) let a be Element of (EqRelLatt Y); ::_thesis: ( K "/\" a = K & a "/\" K = K ) reconsider a9 = a as Equivalence_Relation of Y by MSUALG_5:21; thus K "/\" a = the L_meet of (EqRelLatt Y) . (K,a) by LATTICES:def_2 .= (id Y) /\ a9 by MSUALG_5:def_2 .= K by EQREL_1:10 ; ::_thesis: a "/\" K = K hence a "/\" K = K ; ::_thesis: verum end; hence Bottom (EqRelLatt Y) = id Y by LATTICES:def_16; ::_thesis: verum end; theorem :: MSUALG_8:4 for Y being set holds Top (EqRelLatt Y) = nabla Y proof let Y be set ; ::_thesis: Top (EqRelLatt Y) = nabla Y reconsider K = nabla Y as Element of (EqRelLatt Y) by MSUALG_5:21; now__::_thesis:_for_a_being_Element_of_(EqRelLatt_Y)_holds_ (_K_"\/"_a_=_K_&_a_"\/"_K_=_K_) let a be Element of (EqRelLatt Y); ::_thesis: ( K "\/" a = K & a "\/" K = K ) reconsider a9 = a as Equivalence_Relation of Y by MSUALG_5:21; thus K "\/" a = the L_join of (EqRelLatt Y) . (K,a) by LATTICES:def_1 .= (nabla Y) "\/" a9 by MSUALG_5:def_2 .= EqCl ((nabla Y) \/ a9) by MSUALG_5:1 .= EqCl (nabla Y) by EQREL_1:1 .= K by MSUALG_5:2 ; ::_thesis: a "\/" K = K hence a "\/" K = K ; ::_thesis: verum end; hence Top (EqRelLatt Y) = nabla Y by LATTICES:def_17; ::_thesis: verum end; theorem Th5: :: MSUALG_8:5 for Y being set holds EqRelLatt Y is complete proof let Y be set ; ::_thesis: EqRelLatt Y is complete for X being Subset of (EqRelLatt Y) ex a being Element of (EqRelLatt Y) st ( a is_less_than X & ( for b being Element of (EqRelLatt Y) st b is_less_than X holds b [= a ) ) proof let X be Subset of (EqRelLatt Y); ::_thesis: ex a being Element of (EqRelLatt Y) st ( a is_less_than X & ( for b being Element of (EqRelLatt Y) st b is_less_than X holds b [= a ) ) percases ( X is empty or not X is empty ) ; supposeA1: X is empty ; ::_thesis: ex a being Element of (EqRelLatt Y) st ( a is_less_than X & ( for b being Element of (EqRelLatt Y) st b is_less_than X holds b [= a ) ) take a = Top (EqRelLatt Y); ::_thesis: ( a is_less_than X & ( for b being Element of (EqRelLatt Y) st b is_less_than X holds b [= a ) ) for q being Element of (EqRelLatt Y) st q in X holds a [= q by A1; hence a is_less_than X by LATTICE3:def_16; ::_thesis: for b being Element of (EqRelLatt Y) st b is_less_than X holds b [= a let b be Element of (EqRelLatt Y); ::_thesis: ( b is_less_than X implies b [= a ) assume b is_less_than X ; ::_thesis: b [= a thus b [= a by LATTICES:19; ::_thesis: verum end; supposeA2: not X is empty ; ::_thesis: ex a being Element of (EqRelLatt Y) st ( a is_less_than X & ( for b being Element of (EqRelLatt Y) st b is_less_than X holds b [= a ) ) set a = meet X; X c= bool [:Y,Y:] proof let x be set ; :: according to TARSKI:def_3 ::_thesis: ( not x in X or x in bool [:Y,Y:] ) assume x in X ; ::_thesis: x in bool [:Y,Y:] then x is Equivalence_Relation of Y by MSUALG_5:21; hence x in bool [:Y,Y:] ; ::_thesis: verum end; then reconsider X9 = X as Subset-Family of [:Y,Y:] ; for Z being set st Z in X holds Z is Equivalence_Relation of Y by MSUALG_5:21; then meet X9 is Equivalence_Relation of Y by A2, EQREL_1:11; then reconsider a = meet X as Equivalence_Relation of Y ; set a9 = a; reconsider a = a as Element of (EqRelLatt Y) by MSUALG_5:21; take a ; ::_thesis: ( a is_less_than X & ( for b being Element of (EqRelLatt Y) st b is_less_than X holds b [= a ) ) now__::_thesis:_for_q_being_Element_of_(EqRelLatt_Y)_st_q_in_X_holds_ a_[=_q let q be Element of (EqRelLatt Y); ::_thesis: ( q in X implies a [= q ) reconsider q9 = q as Equivalence_Relation of Y by MSUALG_5:21; assume q in X ; ::_thesis: a [= q then a c= q9 by SETFAM_1:3; hence a [= q by Th2; ::_thesis: verum end; hence a is_less_than X by LATTICE3:def_16; ::_thesis: for b being Element of (EqRelLatt Y) st b is_less_than X holds b [= a now__::_thesis:_for_b_being_Element_of_(EqRelLatt_Y)_st_b_is_less_than_X_holds_ b_[=_a let b be Element of (EqRelLatt Y); ::_thesis: ( b is_less_than X implies b [= a ) reconsider b9 = b as Equivalence_Relation of Y by MSUALG_5:21; assume A3: b is_less_than X ; ::_thesis: b [= a now__::_thesis:_for_x_being_set_st_x_in_b9_holds_ x_in_meet_X let x be set ; ::_thesis: ( x in b9 implies x in meet X ) assume A4: x in b9 ; ::_thesis: x in meet X now__::_thesis:_for_Z_being_set_st_Z_in_X_holds_ x_in_Z let Z be set ; ::_thesis: ( Z in X implies x in Z ) assume A5: Z in X ; ::_thesis: x in Z then reconsider Z1 = Z as Element of (EqRelLatt Y) ; reconsider Z9 = Z1 as Equivalence_Relation of Y by MSUALG_5:21; b [= Z1 by A3, A5, LATTICE3:def_16; then b9 c= Z9 by Th2; hence x in Z by A4; ::_thesis: verum end; hence x in meet X by A2, SETFAM_1:def_1; ::_thesis: verum end; then b9 c= meet X by TARSKI:def_3; hence b [= a by Th2; ::_thesis: verum end; hence for b being Element of (EqRelLatt Y) st b is_less_than X holds b [= a ; ::_thesis: verum end; end; end; hence EqRelLatt Y is complete by VECTSP_8:def_6; ::_thesis: verum end; registration let Y be set ; cluster EqRelLatt Y -> complete ; coherence EqRelLatt Y is complete by Th5; end; theorem Th6: :: MSUALG_8:6 for Y being set for X being Subset of (EqRelLatt Y) holds union X is Relation of Y proof let Y be set ; ::_thesis: for X being Subset of (EqRelLatt Y) holds union X is Relation of Y let X be Subset of (EqRelLatt Y); ::_thesis: union X is Relation of Y now__::_thesis:_for_x_being_set_st_x_in_union_X_holds_ x_in_[:Y,Y:] let x be set ; ::_thesis: ( x in union X implies x in [:Y,Y:] ) assume x in union X ; ::_thesis: x in [:Y,Y:] then consider X9 being set such that A1: x in X9 and A2: X9 in X by TARSKI:def_4; X9 is Equivalence_Relation of Y by A2, MSUALG_5:21; hence x in [:Y,Y:] by A1; ::_thesis: verum end; hence union X is Relation of Y by TARSKI:def_3; ::_thesis: verum end; theorem Th7: :: MSUALG_8:7 for Y being set for X being Subset of (EqRelLatt Y) holds union X c= "\/" X proof let Y be set ; ::_thesis: for X being Subset of (EqRelLatt Y) holds union X c= "\/" X let X be Subset of (EqRelLatt Y); ::_thesis: union X c= "\/" X reconsider X9 = "\/" X as Equivalence_Relation of Y by MSUALG_5:21; let x be set ; :: according to TARSKI:def_3 ::_thesis: ( not x in union X or x in "\/" X ) assume x in union X ; ::_thesis: x in "\/" X then consider X1 being set such that A1: x in X1 and A2: X1 in X by TARSKI:def_4; reconsider X1 = X1 as Element of (EqRelLatt Y) by A2; reconsider X2 = X1 as Equivalence_Relation of Y by MSUALG_5:21; X is_less_than "\/" X by LATTICE3:def_21; then X1 [= "\/" X by A2, LATTICE3:def_17; then X2 c= X9 by Th2; hence x in "\/" X by A1; ::_thesis: verum end; theorem Th8: :: MSUALG_8:8 for Y being set for X being Subset of (EqRelLatt Y) for R being Relation of Y st R = union X holds "\/" X = EqCl R proof let Y be set ; ::_thesis: for X being Subset of (EqRelLatt Y) for R being Relation of Y st R = union X holds "\/" X = EqCl R let X be Subset of (EqRelLatt Y); ::_thesis: for R being Relation of Y st R = union X holds "\/" X = EqCl R let R be Relation of Y; ::_thesis: ( R = union X implies "\/" X = EqCl R ) reconsider X1 = "\/" X as Equivalence_Relation of Y by MSUALG_5:21; assume A1: R = union X ; ::_thesis: "\/" X = EqCl R A2: now__::_thesis:_for_EqR_being_Equivalence_Relation_of_Y_st_R_c=_EqR_holds_ X1_c=_EqR let EqR be Equivalence_Relation of Y; ::_thesis: ( R c= EqR implies X1 c= EqR ) reconsider EqR1 = EqR as Element of (EqRelLatt Y) by MSUALG_5:21; assume A3: R c= EqR ; ::_thesis: X1 c= EqR now__::_thesis:_for_q_being_Element_of_(EqRelLatt_Y)_st_q_in_X_holds_ q_[=_EqR1 let q be Element of (EqRelLatt Y); ::_thesis: ( q in X implies q [= EqR1 ) reconsider q1 = q as Equivalence_Relation of Y by MSUALG_5:21; assume A4: q in X ; ::_thesis: q [= EqR1 now__::_thesis:_for_x_being_set_st_x_in_q1_holds_ x_in_EqR let x be set ; ::_thesis: ( x in q1 implies x in EqR ) assume x in q1 ; ::_thesis: x in EqR then x in union X by A4, TARSKI:def_4; hence x in EqR by A1, A3; ::_thesis: verum end; then q1 c= EqR by TARSKI:def_3; hence q [= EqR1 by Th2; ::_thesis: verum end; then X is_less_than EqR1 by LATTICE3:def_17; then "\/" X [= EqR1 by LATTICE3:def_21; hence X1 c= EqR by Th2; ::_thesis: verum end; R c= "\/" X by A1, Th7; hence "\/" X = EqCl R by A2, MSUALG_5:def_1; ::_thesis: verum end; theorem Th9: :: MSUALG_8:9 for Y being set for X being Subset of (EqRelLatt Y) for R being Relation st R = union X holds R = R ~ proof let Y be set ; ::_thesis: for X being Subset of (EqRelLatt Y) for R being Relation st R = union X holds R = R ~ let X be Subset of (EqRelLatt Y); ::_thesis: for R being Relation st R = union X holds R = R ~ let R be Relation; ::_thesis: ( R = union X implies R = R ~ ) assume A1: R = union X ; ::_thesis: R = R ~ now__::_thesis:_for_x,_y_being_set_holds_ (_(_[x,y]_in_R_implies_[x,y]_in_R_~_)_&_(_[x,y]_in_R_~_implies_[x,y]_in_R_)_) let x, y be set ; ::_thesis: ( ( [x,y] in R implies [x,y] in R ~ ) & ( [x,y] in R ~ implies [x,y] in R ) ) thus ( [x,y] in R implies [x,y] in R ~ ) ::_thesis: ( [x,y] in R ~ implies [x,y] in R ) proof assume [x,y] in R ; ::_thesis: [x,y] in R ~ then consider Z being set such that A2: [x,y] in Z and A3: Z in X by A1, TARSKI:def_4; reconsider Z = Z as Equivalence_Relation of Y by A3, MSUALG_5:21; [y,x] in Z by A2, EQREL_1:6; then [y,x] in R by A1, A3, TARSKI:def_4; hence [x,y] in R ~ by RELAT_1:def_7; ::_thesis: verum end; thus ( [x,y] in R ~ implies [x,y] in R ) ::_thesis: verum proof assume [x,y] in R ~ ; ::_thesis: [x,y] in R then [y,x] in R by RELAT_1:def_7; then consider Z being set such that A4: [y,x] in Z and A5: Z in X by A1, TARSKI:def_4; reconsider Z = Z as Equivalence_Relation of Y by A5, MSUALG_5:21; [x,y] in Z by A4, EQREL_1:6; hence [x,y] in R by A1, A5, TARSKI:def_4; ::_thesis: verum end; end; hence R = R ~ by RELAT_1:def_2; ::_thesis: verum end; theorem Th10: :: MSUALG_8:10 for x, y, Y being set for X being Subset of (EqRelLatt Y) st x in Y & y in Y holds ( [x,y] in "\/" X iff ex f being FinSequence st ( 1 <= len f & x = f . 1 & y = f . (len f) & ( for i being Element of NAT st 1 <= i & i < len f holds [(f . i),(f . (i + 1))] in union X ) ) ) proof let x, y, Y be set ; ::_thesis: for X being Subset of (EqRelLatt Y) st x in Y & y in Y holds ( [x,y] in "\/" X iff ex f being FinSequence st ( 1 <= len f & x = f . 1 & y = f . (len f) & ( for i being Element of NAT st 1 <= i & i < len f holds [(f . i),(f . (i + 1))] in union X ) ) ) let X be Subset of (EqRelLatt Y); ::_thesis: ( x in Y & y in Y implies ( [x,y] in "\/" X iff ex f being FinSequence st ( 1 <= len f & x = f . 1 & y = f . (len f) & ( for i being Element of NAT st 1 <= i & i < len f holds [(f . i),(f . (i + 1))] in union X ) ) ) ) assume that A1: x in Y and A2: y in Y ; ::_thesis: ( [x,y] in "\/" X iff ex f being FinSequence st ( 1 <= len f & x = f . 1 & y = f . (len f) & ( for i being Element of NAT st 1 <= i & i < len f holds [(f . i),(f . (i + 1))] in union X ) ) ) reconsider Y9 = Y as non empty set by A1; reconsider x9 = x, y9 = y as Element of Y9 by A1, A2; reconsider R = union X as Relation of Y9 by Th6; R = R ~ by Th9; then A3: R \/ (R ~) = R ; A4: ( [x,y] in "\/" X implies R reduces x,y ) proof assume [x,y] in "\/" X ; ::_thesis: R reduces x,y then [x9,y9] in EqCl R by Th8; then x,y are_convertible_wrt R by MSUALG_6:41; hence R reduces x,y by A3, REWRITE1:def_4; ::_thesis: verum end; thus ( [x,y] in "\/" X implies ex f being FinSequence st ( 1 <= len f & x = f . 1 & y = f . (len f) & ( for i being Element of NAT st 1 <= i & i < len f holds [(f . i),(f . (i + 1))] in union X ) ) ) ::_thesis: ( ex f being FinSequence st ( 1 <= len f & x = f . 1 & y = f . (len f) & ( for i being Element of NAT st 1 <= i & i < len f holds [(f . i),(f . (i + 1))] in union X ) ) implies [x,y] in "\/" X ) proof assume [x,y] in "\/" X ; ::_thesis: ex f being FinSequence st ( 1 <= len f & x = f . 1 & y = f . (len f) & ( for i being Element of NAT st 1 <= i & i < len f holds [(f . i),(f . (i + 1))] in union X ) ) then consider f being FinSequence such that A5: len f > 0 and A6: ( x = f . 1 & y = f . (len f) ) and A7: for i being Element of NAT st i in dom f & i + 1 in dom f holds [(f . i),(f . (i + 1))] in R by A4, REWRITE1:11; take f ; ::_thesis: ( 1 <= len f & x = f . 1 & y = f . (len f) & ( for i being Element of NAT st 1 <= i & i < len f holds [(f . i),(f . (i + 1))] in union X ) ) 0 + 1 <= len f by A5, NAT_1:13; hence ( 1 <= len f & x = f . 1 & y = f . (len f) ) by A6; ::_thesis: for i being Element of NAT st 1 <= i & i < len f holds [(f . i),(f . (i + 1))] in union X let i be Element of NAT ; ::_thesis: ( 1 <= i & i < len f implies [(f . i),(f . (i + 1))] in union X ) assume ( 1 <= i & i < len f ) ; ::_thesis: [(f . i),(f . (i + 1))] in union X then ( i in dom f & i + 1 in dom f ) by Th1; hence [(f . i),(f . (i + 1))] in union X by A7; ::_thesis: verum end; A8: ( R reduces x,y implies [x,y] in "\/" X ) proof assume R reduces x,y ; ::_thesis: [x,y] in "\/" X then x,y are_convertible_wrt R by REWRITE1:25; then [x9,y9] in EqCl R by MSUALG_6:41; hence [x,y] in "\/" X by Th8; ::_thesis: verum end; thus ( ex f being FinSequence st ( 1 <= len f & x = f . 1 & y = f . (len f) & ( for i being Element of NAT st 1 <= i & i < len f holds [(f . i),(f . (i + 1))] in union X ) ) implies [x,y] in "\/" X ) ::_thesis: verum proof given f being FinSequence such that A9: 1 <= len f and A10: ( x = f . 1 & y = f . (len f) ) and A11: for i being Element of NAT st 1 <= i & i < len f holds [(f . i),(f . (i + 1))] in union X ; ::_thesis: [x,y] in "\/" X A12: now__::_thesis:_for_i_being_Element_of_NAT_st_i_in_dom_f_&_i_+_1_in_dom_f_holds_ [(f_._i),(f_._(i_+_1))]_in_union_X let i be Element of NAT ; ::_thesis: ( i in dom f & i + 1 in dom f implies [(f . i),(f . (i + 1))] in union X ) assume ( i in dom f & i + 1 in dom f ) ; ::_thesis: [(f . i),(f . (i + 1))] in union X then ( 1 <= i & i < len f ) by Th1; hence [(f . i),(f . (i + 1))] in union X by A11; ::_thesis: verum end; 0 + 1 <= len f by A9; then len f > 0 by NAT_1:13; hence [x,y] in "\/" X by A8, A10, A12, REWRITE1:11; ::_thesis: verum end; end; begin theorem Th11: :: MSUALG_8:11 for S being non empty non void ManySortedSign for A being non-empty MSAlgebra over S for B being Subset of (CongrLatt A) holds "/\" (B,(EqRelLatt the Sorts of A)) is MSCongruence of A proof let S be non empty non void ManySortedSign ; ::_thesis: for A being non-empty MSAlgebra over S for B being Subset of (CongrLatt A) holds "/\" (B,(EqRelLatt the Sorts of A)) is MSCongruence of A let A be non-empty MSAlgebra over S; ::_thesis: for B being Subset of (CongrLatt A) holds "/\" (B,(EqRelLatt the Sorts of A)) is MSCongruence of A set M = the Sorts of A; set E = EqRelLatt the Sorts of A; set C = CongrLatt A; let B be Subset of (CongrLatt A); ::_thesis: "/\" (B,(EqRelLatt the Sorts of A)) is MSCongruence of A set d9 = "/\" (B,(EqRelLatt the Sorts of A)); reconsider d = "/\" (B,(EqRelLatt the Sorts of A)) as Equivalence_Relation of the Sorts of A by MSUALG_5:def_5; reconsider d = d as MSEquivalence-like ManySortedRelation of A by MSUALG_4:def_3; the carrier of (CongrLatt A) c= the carrier of (EqRelLatt the Sorts of A) by NAT_LAT:def_12; then reconsider B1 = B as Subset of (EqRelLatt the Sorts of A) by XBOOLE_1:1; reconsider B1 = B1 as SubsetFamily of [| the Sorts of A, the Sorts of A|] by MSUALG_7:5; percases ( B is empty or not B is empty ) ; suppose B is empty ; ::_thesis: "/\" (B,(EqRelLatt the Sorts of A)) is MSCongruence of A then reconsider B9 = B as empty Subset of (CongrLatt A) ; for q being Element of (EqRelLatt the Sorts of A) st q in B9 holds Top (EqRelLatt the Sorts of A) [= q ; then A1: Top (EqRelLatt the Sorts of A) is_less_than B by LATTICE3:def_16; for b being Element of (EqRelLatt the Sorts of A) st b is_less_than B holds b [= Top (EqRelLatt the Sorts of A) by LATTICES:19; then "/\" (B,(EqRelLatt the Sorts of A)) = Top (EqRelLatt the Sorts of A) by A1, LATTICE3:34 .= [| the Sorts of A, the Sorts of A|] by MSUALG_7:4 ; hence "/\" (B,(EqRelLatt the Sorts of A)) is MSCongruence of A by MSUALG_5:18; ::_thesis: verum end; supposeA2: not B is empty ; ::_thesis: "/\" (B,(EqRelLatt the Sorts of A)) is MSCongruence of A for o being OperSymbol of S for x, y being Element of Args (o,A) st ( for n being Nat st n in dom x holds [(x . n),(y . n)] in d . ((the_arity_of o) /. n) ) holds [((Den (o,A)) . x),((Den (o,A)) . y)] in d . (the_result_sort_of o) proof reconsider B19 = B1 as non empty SubsetFamily of [| the Sorts of A, the Sorts of A|] by A2; reconsider m = meet |:B1:| as Equivalence_Relation of the Sorts of A by A2, MSUALG_7:8; let o be OperSymbol of S; ::_thesis: for x, y being Element of Args (o,A) st ( for n being Nat st n in dom x holds [(x . n),(y . n)] in d . ((the_arity_of o) /. n) ) holds [((Den (o,A)) . x),((Den (o,A)) . y)] in d . (the_result_sort_of o) let x, y be Element of Args (o,A); ::_thesis: ( ( for n being Nat st n in dom x holds [(x . n),(y . n)] in d . ((the_arity_of o) /. n) ) implies [((Den (o,A)) . x),((Den (o,A)) . y)] in d . (the_result_sort_of o) ) A3: |:B19:| is V2() ; assume A4: for n being Nat st n in dom x holds [(x . n),(y . n)] in d . ((the_arity_of o) /. n) ; ::_thesis: [((Den (o,A)) . x),((Den (o,A)) . y)] in d . (the_result_sort_of o) A5: now__::_thesis:_for_q_being_MSCongruence_of_A_st_q_in_B_holds_ [((Den_(o,A))_._x),((Den_(o,A))_._y)]_in_q_._(the_result_sort_of_o) let q be MSCongruence of A; ::_thesis: ( q in B implies [((Den (o,A)) . x),((Den (o,A)) . y)] in q . (the_result_sort_of o) ) assume A6: q in B ; ::_thesis: [((Den (o,A)) . x),((Den (o,A)) . y)] in q . (the_result_sort_of o) now__::_thesis:_for_n_being_Nat_st_n_in_dom_x_holds_ [(x_._n),(y_._n)]_in_q_._((the_arity_of_o)_/._n) let n be Nat; ::_thesis: ( n in dom x implies [(x . n),(y . n)] in q . ((the_arity_of o) /. n) ) assume n in dom x ; ::_thesis: [(x . n),(y . n)] in q . ((the_arity_of o) /. n) then [(x . n),(y . n)] in d . ((the_arity_of o) /. n) by A4; then A7: [(x . n),(y . n)] in m . ((the_arity_of o) /. n) by A2, MSUALG_7:10; m c= q by A6, MSUALG_7:7; then m . ((the_arity_of o) /. n) c= q . ((the_arity_of o) /. n) by PBOOLE:def_2; hence [(x . n),(y . n)] in q . ((the_arity_of o) /. n) by A7; ::_thesis: verum end; hence [((Den (o,A)) . x),((Den (o,A)) . y)] in q . (the_result_sort_of o) by MSUALG_4:def_4; ::_thesis: verum end; A8: |:B1:| . (the_result_sort_of o) = { (x1 . (the_result_sort_of o)) where x1 is Element of Bool [| the Sorts of A, the Sorts of A|] : x1 in B } by A2, CLOSURE2:14; now__::_thesis:_for_Y_being_set_st_Y_in_|:B1:|_._(the_result_sort_of_o)_holds_ [((Den_(o,A))_._x),((Den_(o,A))_._y)]_in_Y let Y be set ; ::_thesis: ( Y in |:B1:| . (the_result_sort_of o) implies [((Den (o,A)) . x),((Den (o,A)) . y)] in Y ) assume Y in |:B1:| . (the_result_sort_of o) ; ::_thesis: [((Den (o,A)) . x),((Den (o,A)) . y)] in Y then consider z being Element of Bool [| the Sorts of A, the Sorts of A|] such that A9: Y = z . (the_result_sort_of o) and A10: z in B by A8; reconsider z9 = z as MSCongruence of A by A10, MSUALG_5:def_6; [((Den (o,A)) . x),((Den (o,A)) . y)] in z9 . (the_result_sort_of o) by A5, A10; hence [((Den (o,A)) . x),((Den (o,A)) . y)] in Y by A9; ::_thesis: verum end; then ( ex Q being Subset-Family of ([| the Sorts of A, the Sorts of A|] . (the_result_sort_of o)) st ( Q = |:B1:| . (the_result_sort_of o) & m . (the_result_sort_of o) = Intersect Q ) & [((Den (o,A)) . x),((Den (o,A)) . y)] in meet (|:B1:| . (the_result_sort_of o)) ) by A3, MSSUBFAM:def_1, SETFAM_1:def_1; then [((Den (o,A)) . x),((Den (o,A)) . y)] in m . (the_result_sort_of o) by A3, SETFAM_1:def_9; hence [((Den (o,A)) . x),((Den (o,A)) . y)] in d . (the_result_sort_of o) by A2, MSUALG_7:10; ::_thesis: verum end; hence "/\" (B,(EqRelLatt the Sorts of A)) is MSCongruence of A by MSUALG_4:def_4; ::_thesis: verum end; end; end; definition let S be non empty non void ManySortedSign ; let A be non-empty MSAlgebra over S; let E be Element of (EqRelLatt the Sorts of A); func CongrCl E -> MSCongruence of A equals :: MSUALG_8:def 1 "/\" ( { x where x is Element of (EqRelLatt the Sorts of A) : ( x is MSCongruence of A & E [= x ) } ,(EqRelLatt the Sorts of A)); coherence "/\" ( { x where x is Element of (EqRelLatt the Sorts of A) : ( x is MSCongruence of A & E [= x ) } ,(EqRelLatt the Sorts of A)) is MSCongruence of A proof set Z = { x where x is Element of (EqRelLatt the Sorts of A) : ( x is MSCongruence of A & E [= x ) } ; now__::_thesis:_for_z_being_set_st_z_in__{__x_where_x_is_Element_of_(EqRelLatt_the_Sorts_of_A)_:_(_x_is_MSCongruence_of_A_&_E_[=_x_)__}__holds_ z_in_the_carrier_of_(CongrLatt_A) let z be set ; ::_thesis: ( z in { x where x is Element of (EqRelLatt the Sorts of A) : ( x is MSCongruence of A & E [= x ) } implies z in the carrier of (CongrLatt A) ) assume z in { x where x is Element of (EqRelLatt the Sorts of A) : ( x is MSCongruence of A & E [= x ) } ; ::_thesis: z in the carrier of (CongrLatt A) then ex z1 being Element of (EqRelLatt the Sorts of A) st ( z = z1 & z1 is MSCongruence of A & E [= z1 ) ; hence z in the carrier of (CongrLatt A) by MSUALG_5:def_6; ::_thesis: verum end; then reconsider Z9 = { x where x is Element of (EqRelLatt the Sorts of A) : ( x is MSCongruence of A & E [= x ) } as Subset of (CongrLatt A) by TARSKI:def_3; "/\" (Z9,(EqRelLatt the Sorts of A)) is MSCongruence of A by Th11; hence "/\" ( { x where x is Element of (EqRelLatt the Sorts of A) : ( x is MSCongruence of A & E [= x ) } ,(EqRelLatt the Sorts of A)) is MSCongruence of A ; ::_thesis: verum end; end; :: deftheorem defines CongrCl MSUALG_8:def_1_:_ for S being non empty non void ManySortedSign for A being non-empty MSAlgebra over S for E being Element of (EqRelLatt the Sorts of A) holds CongrCl E = "/\" ( { x where x is Element of (EqRelLatt the Sorts of A) : ( x is MSCongruence of A & E [= x ) } ,(EqRelLatt the Sorts of A)); definition let S be non empty non void ManySortedSign ; let A be non-empty MSAlgebra over S; let X be Subset of (EqRelLatt the Sorts of A); func CongrCl X -> MSCongruence of A equals :: MSUALG_8:def 2 "/\" ( { x where x is Element of (EqRelLatt the Sorts of A) : ( x is MSCongruence of A & X is_less_than x ) } ,(EqRelLatt the Sorts of A)); coherence "/\" ( { x where x is Element of (EqRelLatt the Sorts of A) : ( x is MSCongruence of A & X is_less_than x ) } ,(EqRelLatt the Sorts of A)) is MSCongruence of A proof set Z = { x where x is Element of (EqRelLatt the Sorts of A) : ( x is MSCongruence of A & X is_less_than x ) } ; now__::_thesis:_for_z_being_set_st_z_in__{__x_where_x_is_Element_of_(EqRelLatt_the_Sorts_of_A)_:_(_x_is_MSCongruence_of_A_&_X_is_less_than_x_)__}__holds_ z_in_the_carrier_of_(CongrLatt_A) let z be set ; ::_thesis: ( z in { x where x is Element of (EqRelLatt the Sorts of A) : ( x is MSCongruence of A & X is_less_than x ) } implies z in the carrier of (CongrLatt A) ) assume z in { x where x is Element of (EqRelLatt the Sorts of A) : ( x is MSCongruence of A & X is_less_than x ) } ; ::_thesis: z in the carrier of (CongrLatt A) then ex z1 being Element of (EqRelLatt the Sorts of A) st ( z = z1 & z1 is MSCongruence of A & X is_less_than z1 ) ; hence z in the carrier of (CongrLatt A) by MSUALG_5:def_6; ::_thesis: verum end; then reconsider Z9 = { x where x is Element of (EqRelLatt the Sorts of A) : ( x is MSCongruence of A & X is_less_than x ) } as Subset of (CongrLatt A) by TARSKI:def_3; "/\" (Z9,(EqRelLatt the Sorts of A)) is MSCongruence of A by Th11; hence "/\" ( { x where x is Element of (EqRelLatt the Sorts of A) : ( x is MSCongruence of A & X is_less_than x ) } ,(EqRelLatt the Sorts of A)) is MSCongruence of A ; ::_thesis: verum end; end; :: deftheorem defines CongrCl MSUALG_8:def_2_:_ for S being non empty non void ManySortedSign for A being non-empty MSAlgebra over S for X being Subset of (EqRelLatt the Sorts of A) holds CongrCl X = "/\" ( { x where x is Element of (EqRelLatt the Sorts of A) : ( x is MSCongruence of A & X is_less_than x ) } ,(EqRelLatt the Sorts of A)); theorem :: MSUALG_8:12 for S being non empty non void ManySortedSign for A being non-empty MSAlgebra over S for C being Element of (EqRelLatt the Sorts of A) st C is MSCongruence of A holds CongrCl C = C proof let S be non empty non void ManySortedSign ; ::_thesis: for A being non-empty MSAlgebra over S for C being Element of (EqRelLatt the Sorts of A) st C is MSCongruence of A holds CongrCl C = C let A be non-empty MSAlgebra over S; ::_thesis: for C being Element of (EqRelLatt the Sorts of A) st C is MSCongruence of A holds CongrCl C = C let C be Element of (EqRelLatt the Sorts of A); ::_thesis: ( C is MSCongruence of A implies CongrCl C = C ) set Z = { x where x is Element of (EqRelLatt the Sorts of A) : ( x is MSCongruence of A & C [= x ) } ; now__::_thesis:_for_q_being_Element_of_(EqRelLatt_the_Sorts_of_A)_st_q_in__{__x_where_x_is_Element_of_(EqRelLatt_the_Sorts_of_A)_:_(_x_is_MSCongruence_of_A_&_C_[=_x_)__}__holds_ C_[=_q let q be Element of (EqRelLatt the Sorts of A); ::_thesis: ( q in { x where x is Element of (EqRelLatt the Sorts of A) : ( x is MSCongruence of A & C [= x ) } implies C [= q ) assume q in { x where x is Element of (EqRelLatt the Sorts of A) : ( x is MSCongruence of A & C [= x ) } ; ::_thesis: C [= q then ex x being Element of (EqRelLatt the Sorts of A) st ( q = x & x is MSCongruence of A & C [= x ) ; hence C [= q ; ::_thesis: verum end; then A1: C is_less_than { x where x is Element of (EqRelLatt the Sorts of A) : ( x is MSCongruence of A & C [= x ) } by LATTICE3:def_16; assume C is MSCongruence of A ; ::_thesis: CongrCl C = C then C in { x where x is Element of (EqRelLatt the Sorts of A) : ( x is MSCongruence of A & C [= x ) } ; hence CongrCl C = C by A1, LATTICE3:41; ::_thesis: verum end; theorem :: MSUALG_8:13 for S being non empty non void ManySortedSign for A being non-empty MSAlgebra over S for X being Subset of (EqRelLatt the Sorts of A) holds CongrCl ("\/" (X,(EqRelLatt the Sorts of A))) = CongrCl X proof let S be non empty non void ManySortedSign ; ::_thesis: for A being non-empty MSAlgebra over S for X being Subset of (EqRelLatt the Sorts of A) holds CongrCl ("\/" (X,(EqRelLatt the Sorts of A))) = CongrCl X let A be non-empty MSAlgebra over S; ::_thesis: for X being Subset of (EqRelLatt the Sorts of A) holds CongrCl ("\/" (X,(EqRelLatt the Sorts of A))) = CongrCl X let X be Subset of (EqRelLatt the Sorts of A); ::_thesis: CongrCl ("\/" (X,(EqRelLatt the Sorts of A))) = CongrCl X set D1 = { x where x is Element of (EqRelLatt the Sorts of A) : ( x is MSCongruence of A & "\/" (X,(EqRelLatt the Sorts of A)) [= x ) } ; set D2 = { x where x is Element of (EqRelLatt the Sorts of A) : ( x is MSCongruence of A & X is_less_than x ) } ; A1: { x where x is Element of (EqRelLatt the Sorts of A) : ( x is MSCongruence of A & "\/" (X,(EqRelLatt the Sorts of A)) [= x ) } c= { x where x is Element of (EqRelLatt the Sorts of A) : ( x is MSCongruence of A & X is_less_than x ) } proof let x1 be set ; :: according to TARSKI:def_3 ::_thesis: ( not x1 in { x where x is Element of (EqRelLatt the Sorts of A) : ( x is MSCongruence of A & "\/" (X,(EqRelLatt the Sorts of A)) [= x ) } or x1 in { x where x is Element of (EqRelLatt the Sorts of A) : ( x is MSCongruence of A & X is_less_than x ) } ) assume x1 in { x where x is Element of (EqRelLatt the Sorts of A) : ( x is MSCongruence of A & "\/" (X,(EqRelLatt the Sorts of A)) [= x ) } ; ::_thesis: x1 in { x where x is Element of (EqRelLatt the Sorts of A) : ( x is MSCongruence of A & X is_less_than x ) } then consider x being Element of (EqRelLatt the Sorts of A) such that A2: ( x1 = x & x is MSCongruence of A ) and A3: "\/" (X,(EqRelLatt the Sorts of A)) [= x ; now__::_thesis:_for_q_being_Element_of_(EqRelLatt_the_Sorts_of_A)_st_q_in_X_holds_ q_[=_x let q be Element of (EqRelLatt the Sorts of A); ::_thesis: ( q in X implies q [= x ) A4: X is_less_than "\/" (X,(EqRelLatt the Sorts of A)) by LATTICE3:def_21; assume q in X ; ::_thesis: q [= x then q [= "\/" (X,(EqRelLatt the Sorts of A)) by A4, LATTICE3:def_17; hence q [= x by A3, LATTICES:7; ::_thesis: verum end; then X is_less_than x by LATTICE3:def_17; hence x1 in { x where x is Element of (EqRelLatt the Sorts of A) : ( x is MSCongruence of A & X is_less_than x ) } by A2; ::_thesis: verum end; { x where x is Element of (EqRelLatt the Sorts of A) : ( x is MSCongruence of A & X is_less_than x ) } c= { x where x is Element of (EqRelLatt the Sorts of A) : ( x is MSCongruence of A & "\/" (X,(EqRelLatt the Sorts of A)) [= x ) } proof let x1 be set ; :: according to TARSKI:def_3 ::_thesis: ( not x1 in { x where x is Element of (EqRelLatt the Sorts of A) : ( x is MSCongruence of A & X is_less_than x ) } or x1 in { x where x is Element of (EqRelLatt the Sorts of A) : ( x is MSCongruence of A & "\/" (X,(EqRelLatt the Sorts of A)) [= x ) } ) assume x1 in { x where x is Element of (EqRelLatt the Sorts of A) : ( x is MSCongruence of A & X is_less_than x ) } ; ::_thesis: x1 in { x where x is Element of (EqRelLatt the Sorts of A) : ( x is MSCongruence of A & "\/" (X,(EqRelLatt the Sorts of A)) [= x ) } then consider x being Element of (EqRelLatt the Sorts of A) such that A5: ( x1 = x & x is MSCongruence of A ) and A6: X is_less_than x ; "\/" (X,(EqRelLatt the Sorts of A)) [= x by A6, LATTICE3:def_21; hence x1 in { x where x is Element of (EqRelLatt the Sorts of A) : ( x is MSCongruence of A & "\/" (X,(EqRelLatt the Sorts of A)) [= x ) } by A5; ::_thesis: verum end; hence CongrCl ("\/" (X,(EqRelLatt the Sorts of A))) = CongrCl X by A1, XBOOLE_0:def_10; ::_thesis: verum end; theorem :: MSUALG_8:14 for S being non empty non void ManySortedSign for A being non-empty MSAlgebra over S for B1, B2 being Subset of (CongrLatt A) for C1, C2 being MSCongruence of A st C1 = "\/" (B1,(EqRelLatt the Sorts of A)) & C2 = "\/" (B2,(EqRelLatt the Sorts of A)) holds C1 "\/" C2 = "\/" ((B1 \/ B2),(EqRelLatt the Sorts of A)) proof let S be non empty non void ManySortedSign ; ::_thesis: for A being non-empty MSAlgebra over S for B1, B2 being Subset of (CongrLatt A) for C1, C2 being MSCongruence of A st C1 = "\/" (B1,(EqRelLatt the Sorts of A)) & C2 = "\/" (B2,(EqRelLatt the Sorts of A)) holds C1 "\/" C2 = "\/" ((B1 \/ B2),(EqRelLatt the Sorts of A)) let A be non-empty MSAlgebra over S; ::_thesis: for B1, B2 being Subset of (CongrLatt A) for C1, C2 being MSCongruence of A st C1 = "\/" (B1,(EqRelLatt the Sorts of A)) & C2 = "\/" (B2,(EqRelLatt the Sorts of A)) holds C1 "\/" C2 = "\/" ((B1 \/ B2),(EqRelLatt the Sorts of A)) let B1, B2 be Subset of (CongrLatt A); ::_thesis: for C1, C2 being MSCongruence of A st C1 = "\/" (B1,(EqRelLatt the Sorts of A)) & C2 = "\/" (B2,(EqRelLatt the Sorts of A)) holds C1 "\/" C2 = "\/" ((B1 \/ B2),(EqRelLatt the Sorts of A)) let C1, C2 be MSCongruence of A; ::_thesis: ( C1 = "\/" (B1,(EqRelLatt the Sorts of A)) & C2 = "\/" (B2,(EqRelLatt the Sorts of A)) implies C1 "\/" C2 = "\/" ((B1 \/ B2),(EqRelLatt the Sorts of A)) ) set C = EqRelLatt the Sorts of A; assume A1: ( C1 = "\/" (B1,(EqRelLatt the Sorts of A)) & C2 = "\/" (B2,(EqRelLatt the Sorts of A)) ) ; ::_thesis: C1 "\/" C2 = "\/" ((B1 \/ B2),(EqRelLatt the Sorts of A)) the carrier of (CongrLatt A) c= the carrier of (EqRelLatt the Sorts of A) by NAT_LAT:def_12; then reconsider D1 = B1, D2 = B2 as Subset of (EqRelLatt the Sorts of A) by XBOOLE_1:1; A2: {("\/" D1),("\/" D2)} c= { ("\/" Y) where Y is Subset of (EqRelLatt the Sorts of A) : Y in {B1,B2} } proof let x be set ; :: according to TARSKI:def_3 ::_thesis: ( not x in {("\/" D1),("\/" D2)} or x in { ("\/" Y) where Y is Subset of (EqRelLatt the Sorts of A) : Y in {B1,B2} } ) assume x in {("\/" D1),("\/" D2)} ; ::_thesis: x in { ("\/" Y) where Y is Subset of (EqRelLatt the Sorts of A) : Y in {B1,B2} } then A3: ( x = "\/" D1 or x = "\/" D2 ) by TARSKI:def_2; ( D1 in {B1,B2} & D2 in {B1,B2} ) by TARSKI:def_2; hence x in { ("\/" Y) where Y is Subset of (EqRelLatt the Sorts of A) : Y in {B1,B2} } by A3; ::_thesis: verum end; { ("\/" Y) where Y is Subset of (EqRelLatt the Sorts of A) : Y in {B1,B2} } c= {("\/" D1),("\/" D2)} proof let x be set ; :: according to TARSKI:def_3 ::_thesis: ( not x in { ("\/" Y) where Y is Subset of (EqRelLatt the Sorts of A) : Y in {B1,B2} } or x in {("\/" D1),("\/" D2)} ) assume x in { ("\/" Y) where Y is Subset of (EqRelLatt the Sorts of A) : Y in {B1,B2} } ; ::_thesis: x in {("\/" D1),("\/" D2)} then consider X1 being Subset of (EqRelLatt the Sorts of A) such that A4: x = "\/" X1 and A5: X1 in {B1,B2} ; ( X1 = B1 or X1 = B2 ) by A5, TARSKI:def_2; hence x in {("\/" D1),("\/" D2)} by A4, TARSKI:def_2; ::_thesis: verum end; then A6: { ("\/" Y) where Y is Subset of (EqRelLatt the Sorts of A) : Y in {B1,B2} } = {("\/" D1),("\/" D2)} by A2, XBOOLE_0:def_10; now__::_thesis:_for_i_being_set_st_i_in_{B1,B2}_holds_ i_in_bool_the_carrier_of_(EqRelLatt_the_Sorts_of_A) let i be set ; ::_thesis: ( i in {B1,B2} implies i in bool the carrier of (EqRelLatt the Sorts of A) ) assume i in {B1,B2} ; ::_thesis: i in bool the carrier of (EqRelLatt the Sorts of A) then ( i = D1 or i = D2 ) by TARSKI:def_2; hence i in bool the carrier of (EqRelLatt the Sorts of A) ; ::_thesis: verum end; then A7: {B1,B2} c= bool the carrier of (EqRelLatt the Sorts of A) by TARSKI:def_3; thus "\/" ((B1 \/ B2),(EqRelLatt the Sorts of A)) = "\/" ((union {B1,B2}),(EqRelLatt the Sorts of A)) by ZFMISC_1:75 .= "\/" ( { ("\/" Y) where Y is Subset of (EqRelLatt the Sorts of A) : Y in {B1,B2} } ,(EqRelLatt the Sorts of A)) by A7, LATTICE3:48 .= ("\/" D1) "\/" ("\/" D2) by A6, LATTICE3:43 .= the L_join of (EqRelLatt the Sorts of A) . (C1,C2) by A1, LATTICES:def_1 .= C1 "\/" C2 by MSUALG_5:def_5 ; ::_thesis: verum end; theorem :: MSUALG_8:15 for S being non empty non void ManySortedSign for A being non-empty MSAlgebra over S for X being Subset of (CongrLatt A) holds "\/" (X,(EqRelLatt the Sorts of A)) = "\/" ( { ("\/" (X0,(EqRelLatt the Sorts of A))) where X0 is Subset of (EqRelLatt the Sorts of A) : X0 is finite Subset of X } ,(EqRelLatt the Sorts of A)) proof let S be non empty non void ManySortedSign ; ::_thesis: for A being non-empty MSAlgebra over S for X being Subset of (CongrLatt A) holds "\/" (X,(EqRelLatt the Sorts of A)) = "\/" ( { ("\/" (X0,(EqRelLatt the Sorts of A))) where X0 is Subset of (EqRelLatt the Sorts of A) : X0 is finite Subset of X } ,(EqRelLatt the Sorts of A)) let A be non-empty MSAlgebra over S; ::_thesis: for X being Subset of (CongrLatt A) holds "\/" (X,(EqRelLatt the Sorts of A)) = "\/" ( { ("\/" (X0,(EqRelLatt the Sorts of A))) where X0 is Subset of (EqRelLatt the Sorts of A) : X0 is finite Subset of X } ,(EqRelLatt the Sorts of A)) let X be Subset of (CongrLatt A); ::_thesis: "\/" (X,(EqRelLatt the Sorts of A)) = "\/" ( { ("\/" (X0,(EqRelLatt the Sorts of A))) where X0 is Subset of (EqRelLatt the Sorts of A) : X0 is finite Subset of X } ,(EqRelLatt the Sorts of A)) set E = EqRelLatt the Sorts of A; set X1 = { X0 where X0 is Subset of (EqRelLatt the Sorts of A) : X0 is finite Subset of X } ; set B1 = { ("\/" Y) where Y is Subset of (EqRelLatt the Sorts of A) : Y in { X0 where X0 is Subset of (EqRelLatt the Sorts of A) : X0 is finite Subset of X } } ; set B2 = { ("\/" (X0,(EqRelLatt the Sorts of A))) where X0 is Subset of (EqRelLatt the Sorts of A) : X0 is finite Subset of X } ; A1: { ("\/" (X0,(EqRelLatt the Sorts of A))) where X0 is Subset of (EqRelLatt the Sorts of A) : X0 is finite Subset of X } c= { ("\/" Y) where Y is Subset of (EqRelLatt the Sorts of A) : Y in { X0 where X0 is Subset of (EqRelLatt the Sorts of A) : X0 is finite Subset of X } } proof let x be set ; :: according to TARSKI:def_3 ::_thesis: ( not x in { ("\/" (X0,(EqRelLatt the Sorts of A))) where X0 is Subset of (EqRelLatt the Sorts of A) : X0 is finite Subset of X } or x in { ("\/" Y) where Y is Subset of (EqRelLatt the Sorts of A) : Y in { X0 where X0 is Subset of (EqRelLatt the Sorts of A) : X0 is finite Subset of X } } ) assume x in { ("\/" (X0,(EqRelLatt the Sorts of A))) where X0 is Subset of (EqRelLatt the Sorts of A) : X0 is finite Subset of X } ; ::_thesis: x in { ("\/" Y) where Y is Subset of (EqRelLatt the Sorts of A) : Y in { X0 where X0 is Subset of (EqRelLatt the Sorts of A) : X0 is finite Subset of X } } then consider Y1 being Subset of (EqRelLatt the Sorts of A) such that A2: x = "\/" Y1 and A3: Y1 is finite Subset of X ; Y1 in { X0 where X0 is Subset of (EqRelLatt the Sorts of A) : X0 is finite Subset of X } by A3; hence x in { ("\/" Y) where Y is Subset of (EqRelLatt the Sorts of A) : Y in { X0 where X0 is Subset of (EqRelLatt the Sorts of A) : X0 is finite Subset of X } } by A2; ::_thesis: verum end; A4: X c= union { X0 where X0 is Subset of (EqRelLatt the Sorts of A) : X0 is finite Subset of X } proof let x be set ; :: according to TARSKI:def_3 ::_thesis: ( not x in X or x in union { X0 where X0 is Subset of (EqRelLatt the Sorts of A) : X0 is finite Subset of X } ) assume A5: x in X ; ::_thesis: x in union { X0 where X0 is Subset of (EqRelLatt the Sorts of A) : X0 is finite Subset of X } then reconsider x9 = x as Element of (CongrLatt A) ; the carrier of (CongrLatt A) c= the carrier of (EqRelLatt the Sorts of A) by NAT_LAT:def_12; then reconsider x9 = x9 as Element of (EqRelLatt the Sorts of A) by TARSKI:def_3; {x9} is finite Subset of X by A5, SUBSET_1:41; then ( x in {x} & {x9} in { X0 where X0 is Subset of (EqRelLatt the Sorts of A) : X0 is finite Subset of X } ) by TARSKI:def_1; hence x in union { X0 where X0 is Subset of (EqRelLatt the Sorts of A) : X0 is finite Subset of X } by TARSKI:def_4; ::_thesis: verum end; union { X0 where X0 is Subset of (EqRelLatt the Sorts of A) : X0 is finite Subset of X } c= X proof let x be set ; :: according to TARSKI:def_3 ::_thesis: ( not x in union { X0 where X0 is Subset of (EqRelLatt the Sorts of A) : X0 is finite Subset of X } or x in X ) assume x in union { X0 where X0 is Subset of (EqRelLatt the Sorts of A) : X0 is finite Subset of X } ; ::_thesis: x in X then consider Y1 being set such that A6: x in Y1 and A7: Y1 in { X0 where X0 is Subset of (EqRelLatt the Sorts of A) : X0 is finite Subset of X } by TARSKI:def_4; ex Y2 being Subset of (EqRelLatt the Sorts of A) st ( Y1 = Y2 & Y2 is finite Subset of X ) by A7; hence x in X by A6; ::_thesis: verum end; then A8: X = union { X0 where X0 is Subset of (EqRelLatt the Sorts of A) : X0 is finite Subset of X } by A4, XBOOLE_0:def_10; now__::_thesis:_for_i_being_set_st_i_in__{__X0_where_X0_is_Subset_of_(EqRelLatt_the_Sorts_of_A)_:_X0_is_finite_Subset_of_X__}__holds_ i_in_bool_the_carrier_of_(EqRelLatt_the_Sorts_of_A) let i be set ; ::_thesis: ( i in { X0 where X0 is Subset of (EqRelLatt the Sorts of A) : X0 is finite Subset of X } implies i in bool the carrier of (EqRelLatt the Sorts of A) ) assume i in { X0 where X0 is Subset of (EqRelLatt the Sorts of A) : X0 is finite Subset of X } ; ::_thesis: i in bool the carrier of (EqRelLatt the Sorts of A) then ex I1 being Subset of (EqRelLatt the Sorts of A) st ( i = I1 & I1 is finite Subset of X ) ; hence i in bool the carrier of (EqRelLatt the Sorts of A) ; ::_thesis: verum end; then A9: { X0 where X0 is Subset of (EqRelLatt the Sorts of A) : X0 is finite Subset of X } c= bool the carrier of (EqRelLatt the Sorts of A) by TARSKI:def_3; { ("\/" Y) where Y is Subset of (EqRelLatt the Sorts of A) : Y in { X0 where X0 is Subset of (EqRelLatt the Sorts of A) : X0 is finite Subset of X } } c= { ("\/" (X0,(EqRelLatt the Sorts of A))) where X0 is Subset of (EqRelLatt the Sorts of A) : X0 is finite Subset of X } proof let x be set ; :: according to TARSKI:def_3 ::_thesis: ( not x in { ("\/" Y) where Y is Subset of (EqRelLatt the Sorts of A) : Y in { X0 where X0 is Subset of (EqRelLatt the Sorts of A) : X0 is finite Subset of X } } or x in { ("\/" (X0,(EqRelLatt the Sorts of A))) where X0 is Subset of (EqRelLatt the Sorts of A) : X0 is finite Subset of X } ) assume x in { ("\/" Y) where Y is Subset of (EqRelLatt the Sorts of A) : Y in { X0 where X0 is Subset of (EqRelLatt the Sorts of A) : X0 is finite Subset of X } } ; ::_thesis: x in { ("\/" (X0,(EqRelLatt the Sorts of A))) where X0 is Subset of (EqRelLatt the Sorts of A) : X0 is finite Subset of X } then consider Y1 being Subset of (EqRelLatt the Sorts of A) such that A10: x = "\/" Y1 and A11: Y1 in { X0 where X0 is Subset of (EqRelLatt the Sorts of A) : X0 is finite Subset of X } ; ex Y2 being Subset of (EqRelLatt the Sorts of A) st ( Y1 = Y2 & Y2 is finite Subset of X ) by A11; hence x in { ("\/" (X0,(EqRelLatt the Sorts of A))) where X0 is Subset of (EqRelLatt the Sorts of A) : X0 is finite Subset of X } by A10; ::_thesis: verum end; then { ("\/" Y) where Y is Subset of (EqRelLatt the Sorts of A) : Y in { X0 where X0 is Subset of (EqRelLatt the Sorts of A) : X0 is finite Subset of X } } = { ("\/" (X0,(EqRelLatt the Sorts of A))) where X0 is Subset of (EqRelLatt the Sorts of A) : X0 is finite Subset of X } by A1, XBOOLE_0:def_10; hence "\/" (X,(EqRelLatt the Sorts of A)) = "\/" ( { ("\/" (X0,(EqRelLatt the Sorts of A))) where X0 is Subset of (EqRelLatt the Sorts of A) : X0 is finite Subset of X } ,(EqRelLatt the Sorts of A)) by A9, A8, LATTICE3:48; ::_thesis: verum end; theorem Th16: :: MSUALG_8:16 for I being non empty set for M being ManySortedSet of I for i being Element of I for e being Equivalence_Relation of (M . i) ex E being Equivalence_Relation of M st ( E . i = e & ( for j being Element of I st j <> i holds E . j = nabla (M . j) ) ) proof let I be non empty set ; ::_thesis: for M being ManySortedSet of I for i being Element of I for e being Equivalence_Relation of (M . i) ex E being Equivalence_Relation of M st ( E . i = e & ( for j being Element of I st j <> i holds E . j = nabla (M . j) ) ) let M be ManySortedSet of I; ::_thesis: for i being Element of I for e being Equivalence_Relation of (M . i) ex E being Equivalence_Relation of M st ( E . i = e & ( for j being Element of I st j <> i holds E . j = nabla (M . j) ) ) let i be Element of I; ::_thesis: for e being Equivalence_Relation of (M . i) ex E being Equivalence_Relation of M st ( E . i = e & ( for j being Element of I st j <> i holds E . j = nabla (M . j) ) ) let e be Equivalence_Relation of (M . i); ::_thesis: ex E being Equivalence_Relation of M st ( E . i = e & ( for j being Element of I st j <> i holds E . j = nabla (M . j) ) ) defpred S1[ set ] means $1 = i; deffunc H1( set ) -> Equivalence_Relation of (M . i) = e; deffunc H2( set ) -> Element of bool [:(M . $1),(M . $1):] = nabla (M . $1); consider E being Function such that A1: dom E = I and A2: for j being set st j in I holds ( ( S1[j] implies E . j = H1(j) ) & ( not S1[j] implies E . j = H2(j) ) ) from PARTFUN1:sch_1(); reconsider E = E as ManySortedSet of I by A1, PARTFUN1:def_2, RELAT_1:def_18; now__::_thesis:_for_k_being_set_st_k_in_I_holds_ E_._k_is_Relation_of_(M_._k) let k be set ; ::_thesis: ( k in I implies E . b1 is Relation of (M . b1) ) assume A3: k in I ; ::_thesis: E . b1 is Relation of (M . b1) percases ( k = i or k <> i ) ; suppose k = i ; ::_thesis: E . b1 is Relation of (M . b1) hence E . k is Relation of (M . k) by A2; ::_thesis: verum end; suppose k <> i ; ::_thesis: E . b1 is Relation of (M . b1) then E . k = nabla (M . k) by A2, A3; hence E . k is Relation of (M . k) ; ::_thesis: verum end; end; end; then reconsider E = E as ManySortedRelation of M by MSUALG_4:def_1; now__::_thesis:_for_k_being_set_ for_R_being_Relation_of_(M_._k)_st_k_in_I_&_E_._k_=_R_holds_ R_is_Equivalence_Relation_of_(M_._k) let k be set ; ::_thesis: for R being Relation of (M . k) st k in I & E . k = R holds b3 is Equivalence_Relation of (M . b2) let R be Relation of (M . k); ::_thesis: ( k in I & E . k = R implies b2 is Equivalence_Relation of (M . b1) ) assume that A4: k in I and A5: E . k = R ; ::_thesis: b2 is Equivalence_Relation of (M . b1) percases ( k = i or k <> i ) ; suppose k = i ; ::_thesis: b2 is Equivalence_Relation of (M . b1) hence R is Equivalence_Relation of (M . k) by A2, A5; ::_thesis: verum end; suppose k <> i ; ::_thesis: b2 is Equivalence_Relation of (M . b1) then E . k = nabla (M . k) by A2, A4; hence R is Equivalence_Relation of (M . k) by A5; ::_thesis: verum end; end; end; then reconsider E = E as Equivalence_Relation of M by MSUALG_4:def_2; take E ; ::_thesis: ( E . i = e & ( for j being Element of I st j <> i holds E . j = nabla (M . j) ) ) thus E . i = e by A2; ::_thesis: for j being Element of I st j <> i holds E . j = nabla (M . j) let j be Element of I; ::_thesis: ( j <> i implies E . j = nabla (M . j) ) assume j <> i ; ::_thesis: E . j = nabla (M . j) hence E . j = nabla (M . j) by A2; ::_thesis: verum end; notation let I be non empty set ; let M be ManySortedSet of I; let i be Element of I; let X be Subset of (EqRelLatt M); synonym EqRelSet (X,i) for pi (M,I); end; definition let I be non empty set ; let M be ManySortedSet of I; let i be Element of I; let X be Subset of (EqRelLatt M); :: original: EqRelSet redefine func EqRelSet (X,i) -> Subset of (EqRelLatt (M . i)) means :Def3: :: MSUALG_8:def 3 for x being set holds ( x in it iff ex Eq being Equivalence_Relation of M st ( x = Eq . i & Eq in X ) ); coherence EqRelSet (,) is Subset of (EqRelLatt (M . i)) proof pi (X,i) c= the carrier of (EqRelLatt (M . i)) proof let z be set ; :: according to TARSKI:def_3 ::_thesis: ( not z in pi (X,i) or z in the carrier of (EqRelLatt (M . i)) ) assume z in pi (X,i) ; ::_thesis: z in the carrier of (EqRelLatt (M . i)) then consider f being Function such that A1: f in X and A2: z = f . i by CARD_3:def_6; reconsider f = f as Equivalence_Relation of M by A1, MSUALG_5:def_5; f . i is Equivalence_Relation of (M . i) by MSUALG_4:def_2; hence z in the carrier of (EqRelLatt (M . i)) by A2, MSUALG_5:21; ::_thesis: verum end; hence EqRelSet (,) is Subset of (EqRelLatt (M . i)) ; ::_thesis: verum end; compatibility for b1 being Subset of (EqRelLatt (M . i)) holds ( b1 = EqRelSet (,) iff for x being set holds ( x in b1 iff ex Eq being Equivalence_Relation of M st ( x = Eq . i & Eq in X ) ) ) proof thus for Y being Subset of (EqRelLatt (M . i)) holds ( Y = pi (X,i) iff for x being set holds ( x in Y iff ex Eq being Equivalence_Relation of M st ( x = Eq . i & Eq in X ) ) ) ::_thesis: verum proof let Y be Subset of (EqRelLatt (M . i)); ::_thesis: ( Y = pi (X,i) iff for x being set holds ( x in Y iff ex Eq being Equivalence_Relation of M st ( x = Eq . i & Eq in X ) ) ) thus ( Y = pi (X,i) implies for x being set holds ( x in Y iff ex Eq being Equivalence_Relation of M st ( x = Eq . i & Eq in X ) ) ) ::_thesis: ( ( for x being set holds ( x in Y iff ex Eq being Equivalence_Relation of M st ( x = Eq . i & Eq in X ) ) ) implies Y = pi (X,i) ) proof assume A3: Y = pi (X,i) ; ::_thesis: for x being set holds ( x in Y iff ex Eq being Equivalence_Relation of M st ( x = Eq . i & Eq in X ) ) let x be set ; ::_thesis: ( x in Y iff ex Eq being Equivalence_Relation of M st ( x = Eq . i & Eq in X ) ) thus ( x in Y implies ex Eq being Equivalence_Relation of M st ( x = Eq . i & Eq in X ) ) ::_thesis: ( ex Eq being Equivalence_Relation of M st ( x = Eq . i & Eq in X ) implies x in Y ) proof assume x in Y ; ::_thesis: ex Eq being Equivalence_Relation of M st ( x = Eq . i & Eq in X ) then consider f being Function such that A4: f in X and A5: x = f . i by A3, CARD_3:def_6; reconsider f = f as Equivalence_Relation of M by A4, MSUALG_5:def_5; take f ; ::_thesis: ( x = f . i & f in X ) thus ( x = f . i & f in X ) by A4, A5; ::_thesis: verum end; thus ( ex Eq being Equivalence_Relation of M st ( x = Eq . i & Eq in X ) implies x in Y ) by A3, CARD_3:def_6; ::_thesis: verum end; thus ( ( for x being set holds ( x in Y iff ex Eq being Equivalence_Relation of M st ( x = Eq . i & Eq in X ) ) ) implies Y = pi (X,i) ) ::_thesis: verum proof assume A6: for x being set holds ( x in Y iff ex Eq being Equivalence_Relation of M st ( x = Eq . i & Eq in X ) ) ; ::_thesis: Y = pi (X,i) thus Y c= pi (X,i) :: according to XBOOLE_0:def_10 ::_thesis: pi (X,i) c= Y proof let y1 be set ; :: according to TARSKI:def_3 ::_thesis: ( not y1 in Y or y1 in pi (X,i) ) assume y1 in Y ; ::_thesis: y1 in pi (X,i) then ex Eq being Equivalence_Relation of M st ( y1 = Eq . i & Eq in X ) by A6; hence y1 in pi (X,i) by CARD_3:def_6; ::_thesis: verum end; thus pi (X,i) c= Y ::_thesis: verum proof let y1 be set ; :: according to TARSKI:def_3 ::_thesis: ( not y1 in pi (X,i) or y1 in Y ) assume y1 in pi (X,i) ; ::_thesis: y1 in Y then consider f being Function such that A7: f in X and A8: y1 = f . i by CARD_3:def_6; reconsider f = f as Equivalence_Relation of M by A7, MSUALG_5:def_5; ex Eq being Equivalence_Relation of M st ( y1 = Eq . i & Eq in X ) proof take f ; ::_thesis: ( y1 = f . i & f in X ) thus ( y1 = f . i & f in X ) by A7, A8; ::_thesis: verum end; hence y1 in Y by A6; ::_thesis: verum end; end; end; end; end; :: deftheorem Def3 defines EqRelSet MSUALG_8:def_3_:_ for I being non empty set for M being ManySortedSet of I for i being Element of I for X being Subset of (EqRelLatt M) for b5 being Subset of (EqRelLatt (M . i)) holds ( b5 = EqRelSet (X,i) iff for x being set holds ( x in b5 iff ex Eq being Equivalence_Relation of M st ( x = Eq . i & Eq in X ) ) ); theorem Th17: :: MSUALG_8:17 for S being non empty non void ManySortedSign for A being non-empty MSAlgebra over S for i being Element of S for X being Subset of (EqRelLatt the Sorts of A) for B being Equivalence_Relation of the Sorts of A st B = "\/" X holds B . i = "\/" ((EqRelSet (X,i)),(EqRelLatt ( the Sorts of A . i))) proof let S be non empty non void ManySortedSign ; ::_thesis: for A being non-empty MSAlgebra over S for i being Element of S for X being Subset of (EqRelLatt the Sorts of A) for B being Equivalence_Relation of the Sorts of A st B = "\/" X holds B . i = "\/" ((EqRelSet (X,i)),(EqRelLatt ( the Sorts of A . i))) let A be non-empty MSAlgebra over S; ::_thesis: for i being Element of S for X being Subset of (EqRelLatt the Sorts of A) for B being Equivalence_Relation of the Sorts of A st B = "\/" X holds B . i = "\/" ((EqRelSet (X,i)),(EqRelLatt ( the Sorts of A . i))) let i be Element of S; ::_thesis: for X being Subset of (EqRelLatt the Sorts of A) for B being Equivalence_Relation of the Sorts of A st B = "\/" X holds B . i = "\/" ((EqRelSet (X,i)),(EqRelLatt ( the Sorts of A . i))) set M = the Sorts of A; set E = EqRelLatt the Sorts of A; set Ei = EqRelLatt ( the Sorts of A . i); let X be Subset of (EqRelLatt the Sorts of A); ::_thesis: for B being Equivalence_Relation of the Sorts of A st B = "\/" X holds B . i = "\/" ((EqRelSet (X,i)),(EqRelLatt ( the Sorts of A . i))) let B be Equivalence_Relation of the Sorts of A; ::_thesis: ( B = "\/" X implies B . i = "\/" ((EqRelSet (X,i)),(EqRelLatt ( the Sorts of A . i))) ) reconsider B9 = B as Element of (EqRelLatt the Sorts of A) by MSUALG_5:def_5; reconsider Bi = B . i as Equivalence_Relation of ( the Sorts of A . i) by MSUALG_4:def_2; reconsider Bi9 = Bi as Element of (EqRelLatt ( the Sorts of A . i)) by MSUALG_5:21; assume A1: B = "\/" X ; ::_thesis: B . i = "\/" ((EqRelSet (X,i)),(EqRelLatt ( the Sorts of A . i))) A2: now__::_thesis:_for_ri_being_Element_of_(EqRelLatt_(_the_Sorts_of_A_._i))_st_EqRelSet_(X,i)_is_less_than_ri_holds_ Bi9_[=_ri let ri be Element of (EqRelLatt ( the Sorts of A . i)); ::_thesis: ( EqRelSet (X,i) is_less_than ri implies Bi9 [= ri ) reconsider ri9 = ri as Equivalence_Relation of ( the Sorts of A . i) by MSUALG_5:21; consider r9 being Equivalence_Relation of the Sorts of A such that A3: r9 . i = ri9 and A4: for j being SortSymbol of S st j <> i holds r9 . j = nabla ( the Sorts of A . j) by Th16; reconsider r = r9 as Element of (EqRelLatt the Sorts of A) by MSUALG_5:def_5; assume A5: EqRelSet (X,i) is_less_than ri ; ::_thesis: Bi9 [= ri now__::_thesis:_for_c_being_Element_of_(EqRelLatt_the_Sorts_of_A)_st_c_in_X_holds_ c_[=_r let c be Element of (EqRelLatt the Sorts of A); ::_thesis: ( c in X implies c [= r ) reconsider c9 = c as Equivalence_Relation of the Sorts of A by MSUALG_5:def_5; reconsider ci9 = c9 . i as Equivalence_Relation of ( the Sorts of A . i) by MSUALG_4:def_2; reconsider ci = ci9 as Element of (EqRelLatt ( the Sorts of A . i)) by MSUALG_5:21; assume c in X ; ::_thesis: c [= r then ci in EqRelSet (X,i) by Def3; then A6: ci [= ri by A5, LATTICE3:def_17; now__::_thesis:_for_j_being_set_st_j_in_the_carrier_of_S_holds_ c9_._j_c=_r9_._j let j be set ; ::_thesis: ( j in the carrier of S implies c9 . b1 c= r9 . b1 ) assume A7: j in the carrier of S ; ::_thesis: c9 . b1 c= r9 . b1 then reconsider j9 = j as Element of S ; reconsider rj9 = r9 . j9, cj9 = c9 . j9 as Equivalence_Relation of ( the Sorts of A . j) by MSUALG_4:def_2; percases ( j = i or j <> i ) ; suppose j = i ; ::_thesis: c9 . b1 c= r9 . b1 hence c9 . j c= r9 . j by A3, A6, Th2; ::_thesis: verum end; suppose j <> i ; ::_thesis: c9 . b1 c= r9 . b1 then r9 . j = nabla ( the Sorts of A . j) by A4, A7; then cj9 /\ rj9 = cj9 by XBOOLE_1:28; hence c9 . j c= r9 . j by XBOOLE_1:17; ::_thesis: verum end; end; end; then c9 c= r9 by PBOOLE:def_2; hence c [= r by MSUALG_7:6; ::_thesis: verum end; then X is_less_than r by LATTICE3:def_17; then B9 [= r by A1, LATTICE3:def_21; then B c= r9 by MSUALG_7:6; then Bi c= ri9 by A3, PBOOLE:def_2; hence Bi9 [= ri by Th2; ::_thesis: verum end; now__::_thesis:_for_q9_being_Element_of_(EqRelLatt_(_the_Sorts_of_A_._i))_st_q9_in_EqRelSet_(X,i)_holds_ q9_[=_Bi9 let q9 be Element of (EqRelLatt ( the Sorts of A . i)); ::_thesis: ( q9 in EqRelSet (X,i) implies q9 [= Bi9 ) reconsider q = q9 as Equivalence_Relation of ( the Sorts of A . i) by MSUALG_5:21; assume q9 in EqRelSet (X,i) ; ::_thesis: q9 [= Bi9 then consider Eq being Equivalence_Relation of the Sorts of A such that A8: q9 = Eq . i and A9: Eq in X by Def3; reconsider Eq9 = Eq as Element of (EqRelLatt the Sorts of A) by MSUALG_5:def_5; Eq9 [= B9 by A1, A9, LATTICE3:38; then Eq c= B by MSUALG_7:6; then q c= Bi by A8, PBOOLE:def_2; hence q9 [= Bi9 by Th2; ::_thesis: verum end; then EqRelSet (X,i) is_less_than Bi9 by LATTICE3:def_17; hence B . i = "\/" ((EqRelSet (X,i)),(EqRelLatt ( the Sorts of A . i))) by A2, LATTICE3:def_21; ::_thesis: verum end; theorem Th18: :: MSUALG_8:18 for S being non empty non void ManySortedSign for A being non-empty MSAlgebra over S for X being Subset of (CongrLatt A) holds "\/" (X,(EqRelLatt the Sorts of A)) is MSCongruence of A proof let S be non empty non void ManySortedSign ; ::_thesis: for A being non-empty MSAlgebra over S for X being Subset of (CongrLatt A) holds "\/" (X,(EqRelLatt the Sorts of A)) is MSCongruence of A let A be non-empty MSAlgebra over S; ::_thesis: for X being Subset of (CongrLatt A) holds "\/" (X,(EqRelLatt the Sorts of A)) is MSCongruence of A let X9 be Subset of (CongrLatt A); ::_thesis: "\/" (X9,(EqRelLatt the Sorts of A)) is MSCongruence of A set M = the Sorts of A; set E = EqRelLatt the Sorts of A; the carrier of (CongrLatt A) c= the carrier of (EqRelLatt the Sorts of A) by NAT_LAT:def_12; then reconsider X = X9 as Subset of (EqRelLatt the Sorts of A) by XBOOLE_1:1; reconsider V = "\/" (X,(EqRelLatt the Sorts of A)) as Equivalence_Relation of the Sorts of A by MSUALG_5:def_5; reconsider V = V as ManySortedRelation of A ; reconsider V = V as MSEquivalence-like ManySortedRelation of A by MSUALG_4:def_3; for s1, s2 being SortSymbol of S for t being Function st t is_e.translation_of A,s1,s2 holds for a, b being set st [a,b] in V . s1 holds [(t . a),(t . b)] in V . s2 proof let s1, s2 be SortSymbol of S; ::_thesis: for t being Function st t is_e.translation_of A,s1,s2 holds for a, b being set st [a,b] in V . s1 holds [(t . a),(t . b)] in V . s2 let t be Function; ::_thesis: ( t is_e.translation_of A,s1,s2 implies for a, b being set st [a,b] in V . s1 holds [(t . a),(t . b)] in V . s2 ) assume A1: t is_e.translation_of A,s1,s2 ; ::_thesis: for a, b being set st [a,b] in V . s1 holds [(t . a),(t . b)] in V . s2 then reconsider t9 = t as Function of ( the Sorts of A . s1),( the Sorts of A . s2) by MSUALG_6:11; let a, b be set ; ::_thesis: ( [a,b] in V . s1 implies [(t . a),(t . b)] in V . s2 ) assume A2: [a,b] in V . s1 ; ::_thesis: [(t . a),(t . b)] in V . s2 then A3: a in the Sorts of A . s1 by ZFMISC_1:87; A4: b in the Sorts of A . s1 by A2, ZFMISC_1:87; then A5: t9 . b in the Sorts of A . s2 by FUNCT_2:5; [a,b] in "\/" (EqRelSet (X,s1)) by A2, Th17; then consider f being FinSequence such that A6: 1 <= len f and A7: a = f . 1 and A8: b = f . (len f) and A9: for i being Element of NAT st 1 <= i & i < len f holds [(f . i),(f . (i + 1))] in union (EqRelSet (X,s1)) by A3, A4, Th10; A10: ex g being FinSequence st ( 1 <= len g & t . a = g . 1 & t . b = g . (len g) & ( for i being Element of NAT st 1 <= i & i < len g holds [(g . i),(g . (i + 1))] in union (EqRelSet (X,s2)) ) ) proof deffunc H1( set ) -> set = t . (f . $1); consider g being FinSequence such that A11: ( len g = len f & ( for k being Nat st k in dom g holds g . k = H1(k) ) ) from FINSEQ_1:sch_2(); take g ; ::_thesis: ( 1 <= len g & t . a = g . 1 & t . b = g . (len g) & ( for i being Element of NAT st 1 <= i & i < len g holds [(g . i),(g . (i + 1))] in union (EqRelSet (X,s2)) ) ) thus 1 <= len g by A6, A11; ::_thesis: ( t . a = g . 1 & t . b = g . (len g) & ( for i being Element of NAT st 1 <= i & i < len g holds [(g . i),(g . (i + 1))] in union (EqRelSet (X,s2)) ) ) A12: dom g = Seg (len f) by A11, FINSEQ_1:def_3; 1 in Seg (len f) by A6, FINSEQ_1:1; hence g . 1 = t . a by A7, A11, A12; ::_thesis: ( t . b = g . (len g) & ( for i being Element of NAT st 1 <= i & i < len g holds [(g . i),(g . (i + 1))] in union (EqRelSet (X,s2)) ) ) len g in Seg (len f) by A6, A11, FINSEQ_1:1; hence g . (len g) = t . b by A8, A11, A12; ::_thesis: for i being Element of NAT st 1 <= i & i < len g holds [(g . i),(g . (i + 1))] in union (EqRelSet (X,s2)) let j be Element of NAT ; ::_thesis: ( 1 <= j & j < len g implies [(g . j),(g . (j + 1))] in union (EqRelSet (X,s2)) ) assume that A13: 1 <= j and A14: j < len g ; ::_thesis: [(g . j),(g . (j + 1))] in union (EqRelSet (X,s2)) A15: 1 <= j + 1 by A13, NAT_1:13; [(f . j),(f . (j + 1))] in union (EqRelSet (X,s1)) by A9, A11, A13, A14; then consider Z being set such that A16: [(f . j),(f . (j + 1))] in Z and A17: Z in EqRelSet (X,s1) by TARSKI:def_4; consider Eq being Equivalence_Relation of the Sorts of A such that A18: Z = Eq . s1 and A19: Eq in X by A17, Def3; reconsider Eq = Eq as ManySortedRelation of A ; reconsider Eq = Eq as MSEquivalence-like ManySortedRelation of A by MSUALG_4:def_3; Eq is MSCongruence of A by A19, MSUALG_5:def_6; then reconsider Eq = Eq as MSEquivalence-like compatible ManySortedRelation of A by MSUALG_6:27; ex W being set st ( [(t . (f . j)),(t . (f . (j + 1)))] in W & W in EqRelSet (X,s2) ) proof take W = Eq . s2; ::_thesis: ( [(t . (f . j)),(t . (f . (j + 1)))] in W & W in EqRelSet (X,s2) ) thus [(t . (f . j)),(t . (f . (j + 1)))] in W by A1, A16, A18, MSUALG_6:def_8; ::_thesis: W in EqRelSet (X,s2) thus W in EqRelSet (X,s2) by A19, Def3; ::_thesis: verum end; then A20: [(t . (f . j)),(t . (f . (j + 1)))] in union (EqRelSet (X,s2)) by TARSKI:def_4; j + 1 <= len f by A11, A14, NAT_1:13; then A21: j + 1 in Seg (len f) by A15, FINSEQ_1:1; j in Seg (len f) by A11, A13, A14, FINSEQ_1:1; then g . j = t . (f . j) by A11, A12; hence [(g . j),(g . (j + 1))] in union (EqRelSet (X,s2)) by A11, A12, A20, A21; ::_thesis: verum end; t9 . a in the Sorts of A . s2 by A3, FUNCT_2:5; then [(t . a),(t . b)] in "\/" (EqRelSet (X,s2)) by A5, A10, Th10; hence [(t . a),(t . b)] in V . s2 by Th17; ::_thesis: verum end; then reconsider V = V as MSEquivalence-like invariant ManySortedRelation of A by MSUALG_6:def_8; V is compatible ; hence "\/" (X9,(EqRelLatt the Sorts of A)) is MSCongruence of A by MSUALG_6:27; ::_thesis: verum end; theorem Th19: :: MSUALG_8:19 for S being non empty non void ManySortedSign for A being non-empty MSAlgebra over S holds CongrLatt A is /\-inheriting proof let S be non empty non void ManySortedSign ; ::_thesis: for A being non-empty MSAlgebra over S holds CongrLatt A is /\-inheriting let A be non-empty MSAlgebra over S; ::_thesis: CongrLatt A is /\-inheriting set E = EqRelLatt the Sorts of A; set C = CongrLatt A; now__::_thesis:_for_B_being_Subset_of_(CongrLatt_A)_holds_"/\"_(B,(EqRelLatt_the_Sorts_of_A))_in_the_carrier_of_(CongrLatt_A) let B be Subset of (CongrLatt A); ::_thesis: "/\" (B,(EqRelLatt the Sorts of A)) in the carrier of (CongrLatt A) reconsider d = "/\" (B,(EqRelLatt the Sorts of A)) as MSCongruence of A by Th11; d in the carrier of (CongrLatt A) by MSUALG_5:def_6; hence "/\" (B,(EqRelLatt the Sorts of A)) in the carrier of (CongrLatt A) ; ::_thesis: verum end; hence CongrLatt A is /\-inheriting by MSUALG_7:def_2; ::_thesis: verum end; theorem Th20: :: MSUALG_8:20 for S being non empty non void ManySortedSign for A being non-empty MSAlgebra over S holds CongrLatt A is \/-inheriting proof let S be non empty non void ManySortedSign ; ::_thesis: for A being non-empty MSAlgebra over S holds CongrLatt A is \/-inheriting let A be non-empty MSAlgebra over S; ::_thesis: CongrLatt A is \/-inheriting set E = EqRelLatt the Sorts of A; set C = CongrLatt A; now__::_thesis:_for_B_being_Subset_of_(CongrLatt_A)_holds_"\/"_(B,(EqRelLatt_the_Sorts_of_A))_in_the_carrier_of_(CongrLatt_A) let B be Subset of (CongrLatt A); ::_thesis: "\/" (B,(EqRelLatt the Sorts of A)) in the carrier of (CongrLatt A) reconsider d = "\/" (B,(EqRelLatt the Sorts of A)) as MSCongruence of A by Th18; d in the carrier of (CongrLatt A) by MSUALG_5:def_6; hence "\/" (B,(EqRelLatt the Sorts of A)) in the carrier of (CongrLatt A) ; ::_thesis: verum end; hence CongrLatt A is \/-inheriting by MSUALG_7:def_3; ::_thesis: verum end; registration let S be non empty non void ManySortedSign ; let A be non-empty MSAlgebra over S; cluster CongrLatt A -> /\-inheriting \/-inheriting ; coherence ( CongrLatt A is /\-inheriting & CongrLatt A is \/-inheriting ) by Th19, Th20; end;