:: 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;