:: SUBSTLAT semantic presentation
begin
definition
let V, C be set ;
func SubstitutionSet (V,C) -> Subset of (Fin (PFuncs (V,C))) equals :: SUBSTLAT:def 1
{ A where A is Element of Fin (PFuncs (V,C)) : ( ( for u being set st u in A holds
u is finite ) & ( for s, t being Element of PFuncs (V,C) st s in A & t in A & s c= t holds
s = t ) ) } ;
coherence
{ A where A is Element of Fin (PFuncs (V,C)) : ( ( for u being set st u in A holds
u is finite ) & ( for s, t being Element of PFuncs (V,C) st s in A & t in A & s c= t holds
s = t ) ) } is Subset of (Fin (PFuncs (V,C)))
proof
set IT = { A where A is Element of Fin (PFuncs (V,C)) : ( ( for u being set st u in A holds
u is finite ) & ( for s, t being Element of PFuncs (V,C) st s in A & t in A & s c= t holds
s = t ) ) } ;
{ A where A is Element of Fin (PFuncs (V,C)) : ( ( for u being set st u in A holds
u is finite ) & ( for s, t being Element of PFuncs (V,C) st s in A & t in A & s c= t holds
s = t ) ) } c= Fin (PFuncs (V,C))
proof
let x be set ; :: according to TARSKI:def_3 ::_thesis: ( not x in { A where A is Element of Fin (PFuncs (V,C)) : ( ( for u being set st u in A holds
u is finite ) & ( for s, t being Element of PFuncs (V,C) st s in A & t in A & s c= t holds
s = t ) ) } or x in Fin (PFuncs (V,C)) )
assume x in { A where A is Element of Fin (PFuncs (V,C)) : ( ( for u being set st u in A holds
u is finite ) & ( for s, t being Element of PFuncs (V,C) st s in A & t in A & s c= t holds
s = t ) ) } ; ::_thesis: x in Fin (PFuncs (V,C))
then ex B being Element of Fin (PFuncs (V,C)) st
( B = x & ( for u being set st u in B holds
u is finite ) & ( for s, t being Element of PFuncs (V,C) st s in B & t in B & s c= t holds
s = t ) ) ;
hence x in Fin (PFuncs (V,C)) ; ::_thesis: verum
end;
hence { A where A is Element of Fin (PFuncs (V,C)) : ( ( for u being set st u in A holds
u is finite ) & ( for s, t being Element of PFuncs (V,C) st s in A & t in A & s c= t holds
s = t ) ) } is Subset of (Fin (PFuncs (V,C))) ; ::_thesis: verum
end;
end;
:: deftheorem defines SubstitutionSet SUBSTLAT:def_1_:_
for V, C being set holds SubstitutionSet (V,C) = { A where A is Element of Fin (PFuncs (V,C)) : ( ( for u being set st u in A holds
u is finite ) & ( for s, t being Element of PFuncs (V,C) st s in A & t in A & s c= t holds
s = t ) ) } ;
Lm1: for V, C, a, b being set st b in SubstitutionSet (V,C) & a in b holds
a is finite
proof
let V, C be set ; ::_thesis: for a, b being set st b in SubstitutionSet (V,C) & a in b holds
a is finite
let a, b be set ; ::_thesis: ( b in SubstitutionSet (V,C) & a in b implies a is finite )
assume that
A1: b in SubstitutionSet (V,C) and
A2: a in b ; ::_thesis: a is finite
ex A being Element of Fin (PFuncs (V,C)) st
( A = b & ( for u being set st u in A holds
u is finite ) & ( for s, t being Element of PFuncs (V,C) st s in A & t in A & s c= t holds
s = t ) ) by A1;
hence a is finite by A2; ::_thesis: verum
end;
theorem Th1: :: SUBSTLAT:1
for V, C being set holds {} in SubstitutionSet (V,C)
proof
let V, C be set ; ::_thesis: {} in SubstitutionSet (V,C)
{} c= PFuncs (V,C) by XBOOLE_1:2;
then A1: {} in Fin (PFuncs (V,C)) by FINSUB_1:def_5;
( ( for u being set st u in {} holds
u is finite ) & ( for s, t being Element of PFuncs (V,C) st s in {} & t in {} & s c= t holds
s = t ) ) ;
hence {} in SubstitutionSet (V,C) by A1; ::_thesis: verum
end;
theorem Th2: :: SUBSTLAT:2
for V, C being set holds {{}} in SubstitutionSet (V,C)
proof
let V, C be set ; ::_thesis: {{}} in SubstitutionSet (V,C)
A1: for s, t being Element of PFuncs (V,C) st s in {{}} & t in {{}} & s c= t holds
s = t
proof
let s, t be Element of PFuncs (V,C); ::_thesis: ( s in {{}} & t in {{}} & s c= t implies s = t )
assume that
A2: s in {{}} and
A3: t in {{}} and
s c= t ; ::_thesis: s = t
s = {} by A2, TARSKI:def_1;
hence s = t by A3, TARSKI:def_1; ::_thesis: verum
end;
{} is PartFunc of V,C by RELSET_1:12;
then {} in PFuncs (V,C) by PARTFUN1:45;
then {{}} c= PFuncs (V,C) by ZFMISC_1:31;
then A4: {{}} in Fin (PFuncs (V,C)) by FINSUB_1:def_5;
for u being set st u in {{}} holds
u is finite ;
hence {{}} in SubstitutionSet (V,C) by A4, A1; ::_thesis: verum
end;
registration
let V, C be set ;
cluster SubstitutionSet (V,C) -> non empty ;
coherence
not SubstitutionSet (V,C) is empty by Th2;
end;
definition
let V, C be set ;
let A, B be Element of SubstitutionSet (V,C);
:: original: \/
redefine funcA \/ B -> Element of Fin (PFuncs (V,C));
coherence
A \/ B is Element of Fin (PFuncs (V,C))
proof
A \/ B in Fin (PFuncs (V,C)) ;
hence A \/ B is Element of Fin (PFuncs (V,C)) ; ::_thesis: verum
end;
end;
registration
let V, C be set ;
cluster non empty for Element of SubstitutionSet (V,C);
existence
not for b1 being Element of SubstitutionSet (V,C) holds b1 is empty
proof
{{}} in SubstitutionSet (V,C) by Th2;
hence not for b1 being Element of SubstitutionSet (V,C) holds b1 is empty ; ::_thesis: verum
end;
end;
registration
let V, C be set ;
cluster -> finite for Element of SubstitutionSet (V,C);
coherence
for b1 being Element of SubstitutionSet (V,C) holds b1 is finite ;
end;
definition
let V, C be set ;
let A be Element of Fin (PFuncs (V,C));
func mi A -> Element of SubstitutionSet (V,C) equals :: SUBSTLAT:def 2
{ t where t is Element of PFuncs (V,C) : ( t is finite & ( for s being Element of PFuncs (V,C) holds
( ( s in A & s c= t ) iff s = t ) ) ) } ;
coherence
{ t where t is Element of PFuncs (V,C) : ( t is finite & ( for s being Element of PFuncs (V,C) holds
( ( s in A & s c= t ) iff s = t ) ) ) } is Element of SubstitutionSet (V,C)
proof
set M = { t where t is Element of PFuncs (V,C) : ( t is finite & ( for s being Element of PFuncs (V,C) holds
( ( s in A & s c= t ) iff s = t ) ) ) } ;
A1: { t where t is Element of PFuncs (V,C) : ( t is finite & ( for s being Element of PFuncs (V,C) holds
( ( s in A & s c= t ) iff s = t ) ) ) } c= PFuncs (V,C)
proof
let a be set ; :: according to TARSKI:def_3 ::_thesis: ( not a in { t where t is Element of PFuncs (V,C) : ( t is finite & ( for s being Element of PFuncs (V,C) holds
( ( s in A & s c= t ) iff s = t ) ) ) } or a in PFuncs (V,C) )
assume a in { t where t is Element of PFuncs (V,C) : ( t is finite & ( for s being Element of PFuncs (V,C) holds
( ( s in A & s c= t ) iff s = t ) ) ) } ; ::_thesis: a in PFuncs (V,C)
then ex t9 being Element of PFuncs (V,C) st
( a = t9 & t9 is finite & ( for s being Element of PFuncs (V,C) holds
( ( s in A & s c= t9 ) iff s = t9 ) ) ) ;
hence a in PFuncs (V,C) ; ::_thesis: verum
end;
A2: now__::_thesis:_for_x_being_set_st_x_in__{__t_where_t_is_Element_of_PFuncs_(V,C)_:_(_t_is_finite_&_(_for_s_being_Element_of_PFuncs_(V,C)_holds_
(_(_s_in_A_&_s_c=_t_)_iff_s_=_t_)_)_)__}__holds_
x_in_A
let x be set ; ::_thesis: ( x in { t where t is Element of PFuncs (V,C) : ( t is finite & ( for s being Element of PFuncs (V,C) holds
( ( s in A & s c= t ) iff s = t ) ) ) } implies x in A )
assume x in { t where t is Element of PFuncs (V,C) : ( t is finite & ( for s being Element of PFuncs (V,C) holds
( ( s in A & s c= t ) iff s = t ) ) ) } ; ::_thesis: x in A
then ex t being Element of PFuncs (V,C) st
( x = t & t is finite & ( for s being Element of PFuncs (V,C) holds
( ( s in A & s c= t ) iff s = t ) ) ) ;
hence x in A ; ::_thesis: verum
end;
then A3: { t where t is Element of PFuncs (V,C) : ( t is finite & ( for s being Element of PFuncs (V,C) holds
( ( s in A & s c= t ) iff s = t ) ) ) } c= A by TARSKI:def_3;
reconsider M = { t where t is Element of PFuncs (V,C) : ( t is finite & ( for s being Element of PFuncs (V,C) holds
( ( s in A & s c= t ) iff s = t ) ) ) } as set ;
reconsider M9 = M as Element of Fin (PFuncs (V,C)) by A1, A3, FINSUB_1:def_5;
A4: for u being set st u in M9 holds
u is finite
proof
let u be set ; ::_thesis: ( u in M9 implies u is finite )
assume u in M9 ; ::_thesis: u is finite
then ex t9 being Element of PFuncs (V,C) st
( u = t9 & t9 is finite & ( for s being Element of PFuncs (V,C) holds
( ( s in A & s c= t9 ) iff s = t9 ) ) ) ;
hence u is finite ; ::_thesis: verum
end;
for s, t being Element of PFuncs (V,C) st s in M9 & t in M9 & s c= t holds
s = t
proof
let s, t be Element of PFuncs (V,C); ::_thesis: ( s in M9 & t in M9 & s c= t implies s = t )
assume that
A5: ( s in M9 & t in M9 ) and
A6: s c= t ; ::_thesis: s = t
( s in A & ex tt being Element of PFuncs (V,C) st
( t = tt & tt is finite & ( for ss being Element of PFuncs (V,C) holds
( ( ss in A & ss c= tt ) iff ss = tt ) ) ) ) by A2, A5;
hence s = t by A6; ::_thesis: verum
end;
then M in { A1 where A1 is Element of Fin (PFuncs (V,C)) : ( ( for u being set st u in A1 holds
u is finite ) & ( for s, t being Element of PFuncs (V,C) st s in A1 & t in A1 & s c= t holds
s = t ) ) } by A4;
hence { t where t is Element of PFuncs (V,C) : ( t is finite & ( for s being Element of PFuncs (V,C) holds
( ( s in A & s c= t ) iff s = t ) ) ) } is Element of SubstitutionSet (V,C) ; ::_thesis: verum
end;
end;
:: deftheorem defines mi SUBSTLAT:def_2_:_
for V, C being set
for A being Element of Fin (PFuncs (V,C)) holds mi A = { t where t is Element of PFuncs (V,C) : ( t is finite & ( for s being Element of PFuncs (V,C) holds
( ( s in A & s c= t ) iff s = t ) ) ) } ;
registration
let V, C be set ;
cluster -> functional for Element of SubstitutionSet (V,C);
coherence
for b1 being Element of SubstitutionSet (V,C) holds b1 is functional
proof
let A be Element of SubstitutionSet (V,C); ::_thesis: A is functional
A c= PFuncs (V,C) by FINSUB_1:def_5;
hence A is functional ; ::_thesis: verum
end;
end;
definition
let V, C be set ;
let A, B be Element of Fin (PFuncs (V,C));
funcA ^ B -> Element of Fin (PFuncs (V,C)) equals :: SUBSTLAT:def 3
{ (s \/ t) where s, t is Element of PFuncs (V,C) : ( s in A & t in B & s tolerates t ) } ;
coherence
{ (s \/ t) where s, t is Element of PFuncs (V,C) : ( s in A & t in B & s tolerates t ) } is Element of Fin (PFuncs (V,C))
proof
deffunc H1( Element of PFuncs (V,C), Element of PFuncs (V,C)) -> set = $1 \/ $2;
set M = { H1(s,t) where s, t is Element of PFuncs (V,C) : ( s in A & t in B & s tolerates t ) } ;
set N = { H1(s,t) where s, t is Element of PFuncs (V,C) : ( s in A & t in B ) } ;
A1: { H1(s,t) where s, t is Element of PFuncs (V,C) : ( s in A & t in B & s tolerates t ) } c= { H1(s,t) where s, t is Element of PFuncs (V,C) : ( s in A & t in B ) }
proof
let a be set ; :: according to TARSKI:def_3 ::_thesis: ( not a in { H1(s,t) where s, t is Element of PFuncs (V,C) : ( s in A & t in B & s tolerates t ) } or a in { H1(s,t) where s, t is Element of PFuncs (V,C) : ( s in A & t in B ) } )
assume a in { H1(s,t) where s, t is Element of PFuncs (V,C) : ( s in A & t in B & s tolerates t ) } ; ::_thesis: a in { H1(s,t) where s, t is Element of PFuncs (V,C) : ( s in A & t in B ) }
then ex s, t being Element of PFuncs (V,C) st
( a = s \/ t & s in A & t in B & s tolerates t ) ;
hence a in { H1(s,t) where s, t is Element of PFuncs (V,C) : ( s in A & t in B ) } ; ::_thesis: verum
end;
A2: { H1(s,t) where s, t is Element of PFuncs (V,C) : ( s in A & t in B & s tolerates t ) } c= PFuncs (V,C)
proof
let y be set ; :: according to TARSKI:def_3 ::_thesis: ( not y in { H1(s,t) where s, t is Element of PFuncs (V,C) : ( s in A & t in B & s tolerates t ) } or y in PFuncs (V,C) )
assume y in { H1(s,t) where s, t is Element of PFuncs (V,C) : ( s in A & t in B & s tolerates t ) } ; ::_thesis: y in PFuncs (V,C)
then consider s, t being Element of PFuncs (V,C) such that
A3: y = s \/ t and
s in A and
t in B and
A4: s tolerates t ;
reconsider s99 = s, t99 = t as PartFunc of V,C by PARTFUN1:47;
reconsider s9 = s, t9 = t as Function ;
( s is PartFunc of V,C & t is PartFunc of V,C ) by PARTFUN1:47;
then s9 +* t9 is PartFunc of V,C by FUNCT_4:40;
then s99 \/ t99 is PartFunc of V,C by A4, FUNCT_4:30;
hence y in PFuncs (V,C) by A3, PARTFUN1:45; ::_thesis: verum
end;
A5: B is finite ;
A6: A is finite ;
{ H1(s,t) where s, t is Element of PFuncs (V,C) : ( s in A & t in B ) } is finite from FRAENKEL:sch_22(A6, A5);
hence { (s \/ t) where s, t is Element of PFuncs (V,C) : ( s in A & t in B & s tolerates t ) } is Element of Fin (PFuncs (V,C)) by A1, A2, FINSUB_1:def_5; ::_thesis: verum
end;
end;
:: deftheorem defines ^ SUBSTLAT:def_3_:_
for V, C being set
for A, B being Element of Fin (PFuncs (V,C)) holds A ^ B = { (s \/ t) where s, t is Element of PFuncs (V,C) : ( s in A & t in B & s tolerates t ) } ;
theorem Th3: :: SUBSTLAT:3
for V, C being set
for A, B being Element of Fin (PFuncs (V,C)) holds A ^ B = B ^ A
proof
let V, C be set ; ::_thesis: for A, B being Element of Fin (PFuncs (V,C)) holds A ^ B = B ^ A
let A, B be Element of Fin (PFuncs (V,C)); ::_thesis: A ^ B = B ^ A
deffunc H1( Element of PFuncs (V,C), Element of PFuncs (V,C)) -> set = $1 \/ $2;
defpred S1[ Function, Function] means ( $1 in A & $2 in B & $1 tolerates $2 );
defpred S2[ Function, Function] means ( $2 in B & $1 in A & $2 tolerates $1 );
set X1 = { H1(s,t) where s, t is Element of PFuncs (V,C) : S1[s,t] } ;
set X2 = { H1(t,s) where s, t is Element of PFuncs (V,C) : S2[s,t] } ;
A1: now__::_thesis:_for_x_being_set_holds_
(_x_in__{__H1(t,s)_where_s,_t_is_Element_of_PFuncs_(V,C)_:_S2[s,t]__}__iff_x_in__{__(t_\/_s)_where_t,_s_is_Element_of_PFuncs_(V,C)_:_(_t_in_B_&_s_in_A_&_t_tolerates_s_)__}__)
let x be set ; ::_thesis: ( x in { H1(t,s) where s, t is Element of PFuncs (V,C) : S2[s,t] } iff x in { (t \/ s) where t, s is Element of PFuncs (V,C) : ( t in B & s in A & t tolerates s ) } )
( x in { H1(t,s) where s, t is Element of PFuncs (V,C) : S2[s,t] } iff ex s, t being Element of PFuncs (V,C) st
( x = H1(t,s) & S2[s,t] ) ) ;
then ( x in { H1(t,s) where s, t is Element of PFuncs (V,C) : S2[s,t] } iff ex t, s being Element of PFuncs (V,C) st
( x = t \/ s & t in B & s in A & t tolerates s ) ) ;
hence ( x in { H1(t,s) where s, t is Element of PFuncs (V,C) : S2[s,t] } iff x in { (t \/ s) where t, s is Element of PFuncs (V,C) : ( t in B & s in A & t tolerates s ) } ) ; ::_thesis: verum
end;
A2: for s, t being Element of PFuncs (V,C) holds H1(s,t) = H1(t,s) ;
A3: for s, t being Element of PFuncs (V,C) holds
( S1[s,t] iff S2[s,t] ) ;
{ H1(s,t) where s, t is Element of PFuncs (V,C) : S1[s,t] } = { H1(t,s) where s, t is Element of PFuncs (V,C) : S2[s,t] } from FRAENKEL:sch_8(A3, A2);
hence A ^ B = B ^ A by A1, TARSKI:1; ::_thesis: verum
end;
theorem Th4: :: SUBSTLAT:4
for V, C being set
for B, A being Element of Fin (PFuncs (V,C)) st B = {{}} holds
A ^ B = A
proof
let V, C be set ; ::_thesis: for B, A being Element of Fin (PFuncs (V,C)) st B = {{}} holds
A ^ B = A
let B, A be Element of Fin (PFuncs (V,C)); ::_thesis: ( B = {{}} implies A ^ B = A )
A1: { (s \/ t) where s, t is Element of PFuncs (V,C) : ( s in A & t in {{}} & s tolerates t ) } c= A
proof
let a be set ; :: according to TARSKI:def_3 ::_thesis: ( not a in { (s \/ t) where s, t is Element of PFuncs (V,C) : ( s in A & t in {{}} & s tolerates t ) } or a in A )
assume a in { (s \/ t) where s, t is Element of PFuncs (V,C) : ( s in A & t in {{}} & s tolerates t ) } ; ::_thesis: a in A
then consider s9, t9 being Element of PFuncs (V,C) such that
A2: ( a = s9 \/ t9 & s9 in A ) and
A3: t9 in {{}} and
s9 tolerates t9 ;
t9 = {} by A3, TARSKI:def_1;
hence a in A by A2; ::_thesis: verum
end;
A4: A c= { (s \/ t) where s, t is Element of PFuncs (V,C) : ( s in A & t in {{}} & s tolerates t ) }
proof
{} is PartFunc of V,C by RELSET_1:12;
then reconsider b = {} as Element of PFuncs (V,C) by PARTFUN1:45;
let a be set ; :: according to TARSKI:def_3 ::_thesis: ( not a in A or a in { (s \/ t) where s, t is Element of PFuncs (V,C) : ( s in A & t in {{}} & s tolerates t ) } )
assume A5: a in A ; ::_thesis: a in { (s \/ t) where s, t is Element of PFuncs (V,C) : ( s in A & t in {{}} & s tolerates t ) }
A c= PFuncs (V,C) by FINSUB_1:def_5;
then reconsider a9 = a as Element of PFuncs (V,C) by A5;
A6: b in {{}} by TARSKI:def_1;
( a = a9 \/ b & a9 tolerates b ) by PARTFUN1:59;
hence a in { (s \/ t) where s, t is Element of PFuncs (V,C) : ( s in A & t in {{}} & s tolerates t ) } by A5, A6; ::_thesis: verum
end;
assume B = {{}} ; ::_thesis: A ^ B = A
hence A ^ B = A by A1, A4, XBOOLE_0:def_10; ::_thesis: verum
end;
theorem Th5: :: SUBSTLAT:5
for V, C being set
for B being Element of Fin (PFuncs (V,C))
for a, b being set st B in SubstitutionSet (V,C) & a in B & b in B & a c= b holds
a = b
proof
let V, C be set ; ::_thesis: for B being Element of Fin (PFuncs (V,C))
for a, b being set st B in SubstitutionSet (V,C) & a in B & b in B & a c= b holds
a = b
let B be Element of Fin (PFuncs (V,C)); ::_thesis: for a, b being set st B in SubstitutionSet (V,C) & a in B & b in B & a c= b holds
a = b
let a, b be set ; ::_thesis: ( B in SubstitutionSet (V,C) & a in B & b in B & a c= b implies a = b )
assume B in SubstitutionSet (V,C) ; ::_thesis: ( not a in B or not b in B or not a c= b or a = b )
then A1: ex A1 being Element of Fin (PFuncs (V,C)) st
( A1 = B & ( for u being set st u in A1 holds
u is finite ) & ( for s, t being Element of PFuncs (V,C) st s in A1 & t in A1 & s c= t holds
s = t ) ) ;
assume that
A2: ( a in B & b in B ) and
A3: a c= b ; ::_thesis: a = b
B c= PFuncs (V,C) by FINSUB_1:def_5;
then reconsider a9 = a, b9 = b as Element of PFuncs (V,C) by A2;
a9 = b9 by A1, A2, A3;
hence a = b ; ::_thesis: verum
end;
theorem Th6: :: SUBSTLAT:6
for V, C being set
for B being Element of Fin (PFuncs (V,C))
for a being set st a in mi B holds
( a in B & ( for b being set st b in B & b c= a holds
b = a ) )
proof
let V, C be set ; ::_thesis: for B being Element of Fin (PFuncs (V,C))
for a being set st a in mi B holds
( a in B & ( for b being set st b in B & b c= a holds
b = a ) )
let B be Element of Fin (PFuncs (V,C)); ::_thesis: for a being set st a in mi B holds
( a in B & ( for b being set st b in B & b c= a holds
b = a ) )
let a be set ; ::_thesis: ( a in mi B implies ( a in B & ( for b being set st b in B & b c= a holds
b = a ) ) )
assume a in mi B ; ::_thesis: ( a in B & ( for b being set st b in B & b c= a holds
b = a ) )
then A1: ex t being Element of PFuncs (V,C) st
( a = t & t is finite & ( for s being Element of PFuncs (V,C) holds
( ( s in B & s c= t ) iff s = t ) ) ) ;
hence a in B ; ::_thesis: for b being set st b in B & b c= a holds
b = a
let b be set ; ::_thesis: ( b in B & b c= a implies b = a )
assume that
A2: b in B and
A3: b c= a ; ::_thesis: b = a
B c= PFuncs (V,C) by FINSUB_1:def_5;
then reconsider b9 = b as Element of PFuncs (V,C) by A2;
b9 = a by A1, A2, A3;
hence b = a ; ::_thesis: verum
end;
Lm2: for V, C being set
for A, B being Element of Fin (PFuncs (V,C)) st ( for a being set st a in A holds
a in B ) holds
A c= B
proof
let V, C be set ; ::_thesis: for A, B being Element of Fin (PFuncs (V,C)) st ( for a being set st a in A holds
a in B ) holds
A c= B
let A, B be Element of Fin (PFuncs (V,C)); ::_thesis: ( ( for a being set st a in A holds
a in B ) implies A c= B )
assume A1: for a being set st a in A holds
a in B ; ::_thesis: A c= B
let x be set ; :: according to TARSKI:def_3 ::_thesis: ( not x in A or x in B )
assume x in A ; ::_thesis: x in B
hence x in B by A1; ::_thesis: verum
end;
registration
let V, C be set ;
clusterV1() Function-like finite for Element of PFuncs (V,C);
existence
ex b1 being Element of PFuncs (V,C) st b1 is finite
proof
{} is PartFunc of V,C by RELSET_1:12;
then reconsider e = {} as Element of PFuncs (V,C) by PARTFUN1:45;
take e ; ::_thesis: e is finite
thus e is finite ; ::_thesis: verum
end;
end;
theorem Th7: :: SUBSTLAT:7
for V, C being set
for B being Element of Fin (PFuncs (V,C))
for a being finite set st a in B & ( for b being finite set st b in B & b c= a holds
b = a ) holds
a in mi B
proof
let V, C be set ; ::_thesis: for B being Element of Fin (PFuncs (V,C))
for a being finite set st a in B & ( for b being finite set st b in B & b c= a holds
b = a ) holds
a in mi B
let B be Element of Fin (PFuncs (V,C)); ::_thesis: for a being finite set st a in B & ( for b being finite set st b in B & b c= a holds
b = a ) holds
a in mi B
let a be finite set ; ::_thesis: ( a in B & ( for b being finite set st b in B & b c= a holds
b = a ) implies a in mi B )
assume that
A1: a in B and
A2: for s being finite set st s in B & s c= a holds
s = a ; ::_thesis: a in mi B
B c= PFuncs (V,C) by FINSUB_1:def_5;
then reconsider a9 = a as Element of PFuncs (V,C) by A1;
for s being Element of PFuncs (V,C) holds
( ( s in B & s c= a ) iff s = a ) by A1, A2;
then a9 in { t where t is Element of PFuncs (V,C) : ( t is finite & ( for s being Element of PFuncs (V,C) holds
( ( s in B & s c= t ) iff s = t ) ) ) } ;
hence a in mi B ; ::_thesis: verum
end;
theorem Th8: :: SUBSTLAT:8
for V, C being set
for A being Element of Fin (PFuncs (V,C)) holds mi A c= A
proof
let V, C be set ; ::_thesis: for A being Element of Fin (PFuncs (V,C)) holds mi A c= A
let A be Element of Fin (PFuncs (V,C)); ::_thesis: mi A c= A
for a being set st a in mi A holds
a in A by Th6;
hence mi A c= A by TARSKI:def_3; ::_thesis: verum
end;
theorem :: SUBSTLAT:9
for V, C being set
for A being Element of Fin (PFuncs (V,C)) st A = {} holds
mi A = {} by Th8, XBOOLE_1:3;
theorem Th10: :: SUBSTLAT:10
for V, C being set
for B being Element of Fin (PFuncs (V,C))
for b being finite set st b in B holds
ex c being set st
( c c= b & c in mi B )
proof
let V, C be set ; ::_thesis: for B being Element of Fin (PFuncs (V,C))
for b being finite set st b in B holds
ex c being set st
( c c= b & c in mi B )
let B be Element of Fin (PFuncs (V,C)); ::_thesis: for b being finite set st b in B holds
ex c being set st
( c c= b & c in mi B )
defpred S1[ set , set ] means $1 c= $2;
let b be finite set ; ::_thesis: ( b in B implies ex c being set st
( c c= b & c in mi B ) )
assume A1: b in B ; ::_thesis: ex c being set st
( c c= b & c in mi B )
A2: B c= PFuncs (V,C) by FINSUB_1:def_5;
then reconsider b9 = b as Element of PFuncs (V,C) by A1;
A3: for a, b, c being Element of PFuncs (V,C) st S1[a,b] & S1[b,c] holds
S1[a,c] by XBOOLE_1:1;
A4: for a being Element of PFuncs (V,C) holds S1[a,a] ;
for a being Element of PFuncs (V,C) st a in B holds
ex b being Element of PFuncs (V,C) st
( b in B & S1[b,a] & ( for c being Element of PFuncs (V,C) st c in B & S1[c,b] holds
S1[b,c] ) ) from FRAENKEL:sch_23(A4, A3);
then consider c being Element of PFuncs (V,C) such that
A5: c in B and
A6: c c= b9 and
A7: for a being Element of PFuncs (V,C) st a in B & a c= c holds
c c= a by A1;
take c ; ::_thesis: ( c c= b & c in mi B )
thus c c= b by A6; ::_thesis: c in mi B
now__::_thesis:_for_b_being_finite_set_st_b_in_B_&_b_c=_c_holds_
b_=_c
let b be finite set ; ::_thesis: ( b in B & b c= c implies b = c )
assume that
A8: b in B and
A9: b c= c ; ::_thesis: b = c
reconsider b9 = b as Element of PFuncs (V,C) by A2, A8;
c c= b9 by A7, A8, A9;
hence b = c by A9, XBOOLE_0:def_10; ::_thesis: verum
end;
hence c in mi B by A5, A6, Th7; ::_thesis: verum
end;
theorem Th11: :: SUBSTLAT:11
for V, C being set
for K being Element of SubstitutionSet (V,C) holds mi K = K
proof
let V, C be set ; ::_thesis: for K being Element of SubstitutionSet (V,C) holds mi K = K
let K be Element of SubstitutionSet (V,C); ::_thesis: mi K = K
thus mi K c= K by Th8; :: according to XBOOLE_0:def_10 ::_thesis: K c= mi K
now__::_thesis:_for_a_being_set_st_a_in_K_holds_
a_in_mi_K
let a be set ; ::_thesis: ( a in K implies a in mi K )
assume A1: a in K ; ::_thesis: a in mi K
then ( a is finite & ( for b being finite set st b in K & b c= a holds
b = a ) ) by Lm1, Th5;
hence a in mi K by A1, Th7; ::_thesis: verum
end;
hence K c= mi K by Lm2; ::_thesis: verum
end;
theorem Th12: :: SUBSTLAT:12
for V, C being set
for A, B being Element of Fin (PFuncs (V,C)) holds mi (A \/ B) c= (mi A) \/ B
proof
let V, C be set ; ::_thesis: for A, B being Element of Fin (PFuncs (V,C)) holds mi (A \/ B) c= (mi A) \/ B
let A, B be Element of Fin (PFuncs (V,C)); ::_thesis: mi (A \/ B) c= (mi A) \/ B
now__::_thesis:_for_a_being_set_st_a_in_mi_(A_\/_B)_holds_
a_in_(mi_A)_\/_B
let a be set ; ::_thesis: ( a in mi (A \/ B) implies a in (mi A) \/ B )
assume A1: a in mi (A \/ B) ; ::_thesis: a in (mi A) \/ B
then reconsider a9 = a as finite set by Lm1;
A2: a in A \/ B by A1, Th6;
now__::_thesis:_a_in_(mi_A)_\/_B
percases ( a in A or a in B ) by A2, XBOOLE_0:def_3;
supposeA3: a in A ; ::_thesis: a in (mi A) \/ B
now__::_thesis:_for_b_being_finite_set_st_b_in_A_&_b_c=_a_holds_
b_=_a
let b be finite set ; ::_thesis: ( b in A & b c= a implies b = a )
assume b in A ; ::_thesis: ( b c= a implies b = a )
then b in A \/ B by XBOOLE_0:def_3;
hence ( b c= a implies b = a ) by A1, Th6; ::_thesis: verum
end;
then a9 in mi A by A3, Th7;
hence a in (mi A) \/ B by XBOOLE_0:def_3; ::_thesis: verum
end;
suppose a in B ; ::_thesis: a in (mi A) \/ B
hence a in (mi A) \/ B by XBOOLE_0:def_3; ::_thesis: verum
end;
end;
end;
hence a in (mi A) \/ B ; ::_thesis: verum
end;
hence mi (A \/ B) c= (mi A) \/ B by Lm2; ::_thesis: verum
end;
theorem Th13: :: SUBSTLAT:13
for V, C being set
for A, B being Element of Fin (PFuncs (V,C)) holds mi ((mi A) \/ B) = mi (A \/ B)
proof
let V, C be set ; ::_thesis: for A, B being Element of Fin (PFuncs (V,C)) holds mi ((mi A) \/ B) = mi (A \/ B)
let A, B be Element of Fin (PFuncs (V,C)); ::_thesis: mi ((mi A) \/ B) = mi (A \/ B)
A1: (mi A) \/ B c= A \/ B by Th8, XBOOLE_1:9;
now__::_thesis:_for_a_being_set_st_a_in_mi_((mi_A)_\/_B)_holds_
a_in_mi_(A_\/_B)
let a be set ; ::_thesis: ( a in mi ((mi A) \/ B) implies a in mi (A \/ B) )
assume A2: a in mi ((mi A) \/ B) ; ::_thesis: a in mi (A \/ B)
then reconsider a9 = a as finite set by Lm1;
A3: now__::_thesis:_for_b_being_finite_set_st_b_in_A_\/_B_&_b_c=_a_holds_
b_=_a
let b be finite set ; ::_thesis: ( b in A \/ B & b c= a implies b = a )
assume that
A4: b in A \/ B and
A5: b c= a ; ::_thesis: b = a
now__::_thesis:_b_=_a
percases ( b in A or b in B ) by A4, XBOOLE_0:def_3;
suppose b in A ; ::_thesis: b = a
then consider c being set such that
A6: c c= b and
A7: c in mi A by Th10;
( c in (mi A) \/ B & c c= a ) by A5, A6, A7, XBOOLE_0:def_3, XBOOLE_1:1;
then c = a by A2, Th6;
hence b = a by A5, A6, XBOOLE_0:def_10; ::_thesis: verum
end;
suppose b in B ; ::_thesis: b = a
then b in (mi A) \/ B by XBOOLE_0:def_3;
hence b = a by A2, A5, Th6; ::_thesis: verum
end;
end;
end;
hence b = a ; ::_thesis: verum
end;
a in (mi A) \/ B by A2, Th6;
then a9 in mi (A \/ B) by A1, A3, Th7;
hence a in mi (A \/ B) ; ::_thesis: verum
end;
hence mi ((mi A) \/ B) c= mi (A \/ B) by Lm2; :: according to XBOOLE_0:def_10 ::_thesis: mi (A \/ B) c= mi ((mi A) \/ B)
A8: mi (A \/ B) c= (mi A) \/ B by Th12;
now__::_thesis:_for_a_being_set_st_a_in_mi_(A_\/_B)_holds_
a_in_mi_((mi_A)_\/_B)
let a be set ; ::_thesis: ( a in mi (A \/ B) implies a in mi ((mi A) \/ B) )
assume A9: a in mi (A \/ B) ; ::_thesis: a in mi ((mi A) \/ B)
then reconsider a9 = a as finite set by Lm1;
for b being finite set st b in (mi A) \/ B & b c= a holds
b = a by A1, A9, Th6;
then a9 in mi ((mi A) \/ B) by A8, A9, Th7;
hence a in mi ((mi A) \/ B) ; ::_thesis: verum
end;
hence mi (A \/ B) c= mi ((mi A) \/ B) by Lm2; ::_thesis: verum
end;
theorem Th14: :: SUBSTLAT:14
for V, C being set
for A, B, D being Element of Fin (PFuncs (V,C)) st A c= B holds
A ^ D c= B ^ D
proof
let V, C be set ; ::_thesis: for A, B, D being Element of Fin (PFuncs (V,C)) st A c= B holds
A ^ D c= B ^ D
let A, B, D be Element of Fin (PFuncs (V,C)); ::_thesis: ( A c= B implies A ^ D c= B ^ D )
deffunc H1( Element of PFuncs (V,C), Element of PFuncs (V,C)) -> set = $1 \/ $2;
defpred S1[ Function, Function] means ( $1 in A & $2 in D & $1 tolerates $2 );
defpred S2[ Function, Function] means ( $1 in B & $2 in D & $1 tolerates $2 );
set X1 = { H1(s,t) where s, t is Element of PFuncs (V,C) : S1[s,t] } ;
set X2 = { H1(s,t) where s, t is Element of PFuncs (V,C) : S2[s,t] } ;
assume A c= B ; ::_thesis: A ^ D c= B ^ D
then A1: for s, t being Element of PFuncs (V,C) st S1[s,t] holds
S2[s,t] ;
{ H1(s,t) where s, t is Element of PFuncs (V,C) : S1[s,t] } c= { H1(s,t) where s, t is Element of PFuncs (V,C) : S2[s,t] } from FRAENKEL:sch_2(A1);
hence A ^ D c= B ^ D ; ::_thesis: verum
end;
theorem Th15: :: SUBSTLAT:15
for V, C being set
for A, B being Element of Fin (PFuncs (V,C))
for a being set st a in A ^ B holds
ex b, c being set st
( b in A & c in B & a = b \/ c )
proof
let V, C be set ; ::_thesis: for A, B being Element of Fin (PFuncs (V,C))
for a being set st a in A ^ B holds
ex b, c being set st
( b in A & c in B & a = b \/ c )
let A, B be Element of Fin (PFuncs (V,C)); ::_thesis: for a being set st a in A ^ B holds
ex b, c being set st
( b in A & c in B & a = b \/ c )
let a be set ; ::_thesis: ( a in A ^ B implies ex b, c being set st
( b in A & c in B & a = b \/ c ) )
assume a in A ^ B ; ::_thesis: ex b, c being set st
( b in A & c in B & a = b \/ c )
then ex s, t being Element of PFuncs (V,C) st
( a = s \/ t & s in A & t in B & s tolerates t ) ;
hence ex b, c being set st
( b in A & c in B & a = b \/ c ) ; ::_thesis: verum
end;
theorem :: SUBSTLAT:16
for V, C being set
for A, B being Element of Fin (PFuncs (V,C))
for b, c being Element of PFuncs (V,C) st b in A & c in B & b tolerates c holds
b \/ c in A ^ B ;
Lm3: for V, C being set
for A, B being Element of Fin (PFuncs (V,C))
for a being finite set st a in A ^ B holds
ex b being finite set st
( b c= a & b in (mi A) ^ B )
proof
let V, C be set ; ::_thesis: for A, B being Element of Fin (PFuncs (V,C))
for a being finite set st a in A ^ B holds
ex b being finite set st
( b c= a & b in (mi A) ^ B )
let A, B be Element of Fin (PFuncs (V,C)); ::_thesis: for a being finite set st a in A ^ B holds
ex b being finite set st
( b c= a & b in (mi A) ^ B )
let a be finite set ; ::_thesis: ( a in A ^ B implies ex b being finite set st
( b c= a & b in (mi A) ^ B ) )
assume a in A ^ B ; ::_thesis: ex b being finite set st
( b c= a & b in (mi A) ^ B )
then consider b, c being Element of PFuncs (V,C) such that
A1: a = b \/ c and
A2: b in A and
A3: c in B and
A4: b tolerates c ;
b is finite by A1, FINSET_1:1, XBOOLE_1:7;
then consider d being set such that
A5: d c= b and
A6: d in mi A by A2, Th10;
A7: mi A c= PFuncs (V,C) by FINSUB_1:def_5;
then reconsider d9 = d, c9 = c as Element of PFuncs (V,C) by A6;
reconsider d1 = d, b1 = b, c1 = c as PartFunc of V,C by A6, A7, PARTFUN1:46;
d1 c= b1 by A5;
then A8: d9 tolerates c9 by A4, PARTFUN1:58;
then d9 \/ c9 = d9 +* c9 by FUNCT_4:30;
then reconsider e = d1 \/ c1 as Element of PFuncs (V,C) by PARTFUN1:45;
reconsider e = e as finite set by A1, A5, FINSET_1:1, XBOOLE_1:9;
take e ; ::_thesis: ( e c= a & e in (mi A) ^ B )
thus e c= a by A1, A5, XBOOLE_1:9; ::_thesis: e in (mi A) ^ B
thus e in (mi A) ^ B by A3, A6, A8; ::_thesis: verum
end;
theorem Th17: :: SUBSTLAT:17
for V, C being set
for A, B being Element of Fin (PFuncs (V,C)) holds mi (A ^ B) c= (mi A) ^ B
proof
let V, C be set ; ::_thesis: for A, B being Element of Fin (PFuncs (V,C)) holds mi (A ^ B) c= (mi A) ^ B
let A, B be Element of Fin (PFuncs (V,C)); ::_thesis: mi (A ^ B) c= (mi A) ^ B
A1: (mi A) ^ B c= A ^ B by Th8, Th14;
now__::_thesis:_for_a_being_set_st_a_in_mi_(A_^_B)_holds_
a_in_(mi_A)_^_B
let a be set ; ::_thesis: ( a in mi (A ^ B) implies a in (mi A) ^ B )
assume A2: a in mi (A ^ B) ; ::_thesis: a in (mi A) ^ B
then ( a in A ^ B & a is finite ) by Lm1, Th6;
then ex b being finite set st
( b c= a & b in (mi A) ^ B ) by Lm3;
hence a in (mi A) ^ B by A1, A2, Th6; ::_thesis: verum
end;
hence mi (A ^ B) c= (mi A) ^ B by Lm2; ::_thesis: verum
end;
theorem Th18: :: SUBSTLAT:18
for V, C being set
for A, B, D being Element of Fin (PFuncs (V,C)) st A c= B holds
D ^ A c= D ^ B
proof
let V, C be set ; ::_thesis: for A, B, D being Element of Fin (PFuncs (V,C)) st A c= B holds
D ^ A c= D ^ B
let A, B, D be Element of Fin (PFuncs (V,C)); ::_thesis: ( A c= B implies D ^ A c= D ^ B )
( D ^ A = A ^ D & D ^ B = B ^ D ) by Th3;
hence ( A c= B implies D ^ A c= D ^ B ) by Th14; ::_thesis: verum
end;
theorem Th19: :: SUBSTLAT:19
for V, C being set
for A, B being Element of Fin (PFuncs (V,C)) holds mi ((mi A) ^ B) = mi (A ^ B)
proof
let V, C be set ; ::_thesis: for A, B being Element of Fin (PFuncs (V,C)) holds mi ((mi A) ^ B) = mi (A ^ B)
let A, B be Element of Fin (PFuncs (V,C)); ::_thesis: mi ((mi A) ^ B) = mi (A ^ B)
A1: (mi A) ^ B c= A ^ B by Th8, Th14;
now__::_thesis:_for_a_being_set_st_a_in_mi_((mi_A)_^_B)_holds_
a_in_mi_(A_^_B)
let a be set ; ::_thesis: ( a in mi ((mi A) ^ B) implies a in mi (A ^ B) )
assume A2: a in mi ((mi A) ^ B) ; ::_thesis: a in mi (A ^ B)
A3: now__::_thesis:_for_b_being_finite_set_st_b_in_A_^_B_&_b_c=_a_holds_
b_=_a
let b be finite set ; ::_thesis: ( b in A ^ B & b c= a implies b = a )
assume b in A ^ B ; ::_thesis: ( b c= a implies b = a )
then consider c being finite set such that
A4: c c= b and
A5: c in (mi A) ^ B by Lm3;
assume A6: b c= a ; ::_thesis: b = a
then c c= a by A4, XBOOLE_1:1;
then c = a by A2, A5, Th6;
hence b = a by A4, A6, XBOOLE_0:def_10; ::_thesis: verum
end;
( a in (mi A) ^ B & a is finite ) by A2, Lm1, Th6;
hence a in mi (A ^ B) by A1, A3, Th7; ::_thesis: verum
end;
hence mi ((mi A) ^ B) c= mi (A ^ B) by Lm2; :: according to XBOOLE_0:def_10 ::_thesis: mi (A ^ B) c= mi ((mi A) ^ B)
A7: mi (A ^ B) c= (mi A) ^ B by Th17;
now__::_thesis:_for_a_being_set_st_a_in_mi_(A_^_B)_holds_
a_in_mi_((mi_A)_^_B)
let a be set ; ::_thesis: ( a in mi (A ^ B) implies a in mi ((mi A) ^ B) )
assume A8: a in mi (A ^ B) ; ::_thesis: a in mi ((mi A) ^ B)
then ( a is finite & ( for b being finite set st b in (mi A) ^ B & b c= a holds
b = a ) ) by A1, Lm1, Th6;
hence a in mi ((mi A) ^ B) by A7, A8, Th7; ::_thesis: verum
end;
hence mi (A ^ B) c= mi ((mi A) ^ B) by Lm2; ::_thesis: verum
end;
theorem Th20: :: SUBSTLAT:20
for V, C being set
for A, B being Element of Fin (PFuncs (V,C)) holds mi (A ^ (mi B)) = mi (A ^ B)
proof
let V, C be set ; ::_thesis: for A, B being Element of Fin (PFuncs (V,C)) holds mi (A ^ (mi B)) = mi (A ^ B)
let A, B be Element of Fin (PFuncs (V,C)); ::_thesis: mi (A ^ (mi B)) = mi (A ^ B)
( A ^ (mi B) = (mi B) ^ A & A ^ B = B ^ A ) by Th3;
hence mi (A ^ (mi B)) = mi (A ^ B) by Th19; ::_thesis: verum
end;
theorem Th21: :: SUBSTLAT:21
for V, C being set
for K, L, M being Element of Fin (PFuncs (V,C)) holds K ^ (L ^ M) = (K ^ L) ^ M
proof
let V, C be set ; ::_thesis: for K, L, M being Element of Fin (PFuncs (V,C)) holds K ^ (L ^ M) = (K ^ L) ^ M
let K, L, M be Element of Fin (PFuncs (V,C)); ::_thesis: K ^ (L ^ M) = (K ^ L) ^ M
A1: ( L ^ M = M ^ L & K ^ L = L ^ K ) by Th3;
A2: now__::_thesis:_for_K,_L,_M_being_Element_of_Fin_(PFuncs_(V,C))_holds_K_^_(L_^_M)_c=_(K_^_L)_^_M
let K, L, M be Element of Fin (PFuncs (V,C)); ::_thesis: K ^ (L ^ M) c= (K ^ L) ^ M
A3: ( K c= PFuncs (V,C) & L c= PFuncs (V,C) ) by FINSUB_1:def_5;
A4: M c= PFuncs (V,C) by FINSUB_1:def_5;
now__::_thesis:_for_a_being_set_st_a_in_K_^_(L_^_M)_holds_
a_in_(K_^_L)_^_M
let a be set ; ::_thesis: ( a in K ^ (L ^ M) implies a in (K ^ L) ^ M )
A5: K ^ (L ^ M) c= PFuncs (V,C) by FINSUB_1:def_5;
assume A6: a in K ^ (L ^ M) ; ::_thesis: a in (K ^ L) ^ M
then consider b, c being set such that
A7: b in K and
A8: c in L ^ M and
A9: a = b \/ c by Th15;
A10: c c= b \/ c by XBOOLE_1:7;
consider b1, c1 being set such that
A11: b1 in L and
A12: c1 in M and
A13: c = b1 \/ c1 by A8, Th15;
reconsider b2 = b, b12 = b1 as PartFunc of V,C by A3, A7, A11, PARTFUN1:46;
reconsider b9 = b, b19 = b1, c19 = c1 as Element of PFuncs (V,C) by A3, A4, A7, A11, A12;
b1 c= c by A13, XBOOLE_1:7;
then A14: ( b c= b \/ c & b1 c= b \/ c ) by A10, XBOOLE_1:1, XBOOLE_1:7;
then A15: b9 tolerates b19 by A6, A9, A5, PARTFUN1:57;
then b9 \/ b19 = b9 +* b19 by FUNCT_4:30;
then b2 \/ b12 is PartFunc of V,C ;
then reconsider c2 = b9 \/ b19 as Element of PFuncs (V,C) by PARTFUN1:45;
A16: ( b \/ (b1 \/ c1) = (b \/ b1) \/ c1 & c2 in K ^ L ) by A7, A11, A15, XBOOLE_1:4;
c1 c= c by A13, XBOOLE_1:7;
then A17: c1 c= b \/ c by A10, XBOOLE_1:1;
c2 c= b \/ c by A14, XBOOLE_1:8;
then c2 tolerates c19 by A6, A9, A5, A17, PARTFUN1:57;
hence a in (K ^ L) ^ M by A9, A12, A13, A16; ::_thesis: verum
end;
hence K ^ (L ^ M) c= (K ^ L) ^ M by Lm2; ::_thesis: verum
end;
then A18: K ^ (L ^ M) c= (K ^ L) ^ M ;
( (K ^ L) ^ M = M ^ (K ^ L) & K ^ (L ^ M) = (L ^ M) ^ K ) by Th3;
then (K ^ L) ^ M c= K ^ (L ^ M) by A1, A2;
hence K ^ (L ^ M) = (K ^ L) ^ M by A18, XBOOLE_0:def_10; ::_thesis: verum
end;
theorem Th22: :: SUBSTLAT:22
for V, C being set
for K, L, M being Element of Fin (PFuncs (V,C)) holds K ^ (L \/ M) = (K ^ L) \/ (K ^ M)
proof
let V, C be set ; ::_thesis: for K, L, M being Element of Fin (PFuncs (V,C)) holds K ^ (L \/ M) = (K ^ L) \/ (K ^ M)
let K, L, M be Element of Fin (PFuncs (V,C)); ::_thesis: K ^ (L \/ M) = (K ^ L) \/ (K ^ M)
now__::_thesis:_for_a_being_set_st_a_in_K_^_(L_\/_M)_holds_
a_in_(K_^_L)_\/_(K_^_M)
let a be set ; ::_thesis: ( a in K ^ (L \/ M) implies a in (K ^ L) \/ (K ^ M) )
assume A1: a in K ^ (L \/ M) ; ::_thesis: a in (K ^ L) \/ (K ^ M)
then consider b, c being set such that
A2: b in K and
A3: c in L \/ M and
A4: a = b \/ c by Th15;
K ^ (L \/ M) c= PFuncs (V,C) by FINSUB_1:def_5;
then reconsider a9 = a as Element of PFuncs (V,C) by A1;
( K c= PFuncs (V,C) & L \/ M c= PFuncs (V,C) ) by FINSUB_1:def_5;
then reconsider b9 = b, c9 = c as Element of PFuncs (V,C) by A2, A3;
( b9 c= a9 & c9 c= a9 ) by A4, XBOOLE_1:7;
then A5: b9 tolerates c9 by PARTFUN1:57;
( c9 in L or c9 in M ) by A3, XBOOLE_0:def_3;
then ( a in K ^ L or a in K ^ M ) by A2, A4, A5;
hence a in (K ^ L) \/ (K ^ M) by XBOOLE_0:def_3; ::_thesis: verum
end;
hence K ^ (L \/ M) c= (K ^ L) \/ (K ^ M) by Lm2; :: according to XBOOLE_0:def_10 ::_thesis: (K ^ L) \/ (K ^ M) c= K ^ (L \/ M)
( K ^ L c= K ^ (L \/ M) & K ^ M c= K ^ (L \/ M) ) by Th18, XBOOLE_1:7;
hence (K ^ L) \/ (K ^ M) c= K ^ (L \/ M) by XBOOLE_1:8; ::_thesis: verum
end;
Lm4: for V, C being set
for A, B being Element of Fin (PFuncs (V,C))
for a being set st a in A ^ B holds
ex c being set st
( c in B & c c= a )
proof
let V, C be set ; ::_thesis: for A, B being Element of Fin (PFuncs (V,C))
for a being set st a in A ^ B holds
ex c being set st
( c in B & c c= a )
let A, B be Element of Fin (PFuncs (V,C)); ::_thesis: for a being set st a in A ^ B holds
ex c being set st
( c in B & c c= a )
let a be set ; ::_thesis: ( a in A ^ B implies ex c being set st
( c in B & c c= a ) )
assume a in A ^ B ; ::_thesis: ex c being set st
( c in B & c c= a )
then consider b, c being set such that
b in A and
A1: c in B and
A2: a = b \/ c by Th15;
take c ; ::_thesis: ( c in B & c c= a )
thus c in B by A1; ::_thesis: c c= a
thus c c= a by A2, XBOOLE_1:7; ::_thesis: verum
end;
Lm5: for V, C being set
for K, L being Element of Fin (PFuncs (V,C)) holds mi ((K ^ L) \/ L) = mi L
proof
let V, C be set ; ::_thesis: for K, L being Element of Fin (PFuncs (V,C)) holds mi ((K ^ L) \/ L) = mi L
let K, L be Element of Fin (PFuncs (V,C)); ::_thesis: mi ((K ^ L) \/ L) = mi L
now__::_thesis:_for_a_being_set_st_a_in_mi_((K_^_L)_\/_L)_holds_
a_in_mi_L
let a be set ; ::_thesis: ( a in mi ((K ^ L) \/ L) implies a in mi L )
assume A1: a in mi ((K ^ L) \/ L) ; ::_thesis: a in mi L
then a in (K ^ L) \/ L by Th6;
then A2: ( a in K ^ L or a in L ) by XBOOLE_0:def_3;
A3: now__::_thesis:_for_b_being_finite_set_st_b_in_L_&_b_c=_a_holds_
b_=_a
let b be finite set ; ::_thesis: ( b in L & b c= a implies b = a )
assume b in L ; ::_thesis: ( b c= a implies b = a )
then b in (K ^ L) \/ L by XBOOLE_0:def_3;
hence ( b c= a implies b = a ) by A1, Th6; ::_thesis: verum
end;
A4: now__::_thesis:_(_a_in_K_^_L_implies_a_in_L_)
assume a in K ^ L ; ::_thesis: a in L
then consider b being set such that
A5: b in L and
A6: b c= a by Lm4;
b in (K ^ L) \/ L by A5, XBOOLE_0:def_3;
hence a in L by A1, A5, A6, Th6; ::_thesis: verum
end;
a is finite by A1, Lm1;
hence a in mi L by A2, A4, A3, Th7; ::_thesis: verum
end;
hence mi ((K ^ L) \/ L) c= mi L by Lm2; :: according to XBOOLE_0:def_10 ::_thesis: mi L c= mi ((K ^ L) \/ L)
now__::_thesis:_for_a_being_set_st_a_in_mi_L_holds_
a_in_mi_((K_^_L)_\/_L)
let a be set ; ::_thesis: ( a in mi L implies a in mi ((K ^ L) \/ L) )
assume A7: a in mi L ; ::_thesis: a in mi ((K ^ L) \/ L)
then A8: a in L by Th6;
then A9: a in (K ^ L) \/ L by XBOOLE_0:def_3;
A10: now__::_thesis:_for_b_being_finite_set_st_b_in_(K_^_L)_\/_L_&_b_c=_a_holds_
b_=_a
let b be finite set ; ::_thesis: ( b in (K ^ L) \/ L & b c= a implies b = a )
assume b in (K ^ L) \/ L ; ::_thesis: ( b c= a implies b = a )
then A11: ( b in K ^ L or b in L ) by XBOOLE_0:def_3;
assume A12: b c= a ; ::_thesis: b = a
now__::_thesis:_(_b_in_K_^_L_implies_b_in_L_)
assume b in K ^ L ; ::_thesis: b in L
then consider c being set such that
A13: c in L and
A14: c c= b by Lm4;
c c= a by A12, A14, XBOOLE_1:1;
then c = a by A7, A13, Th6;
hence b in L by A8, A12, A14, XBOOLE_0:def_10; ::_thesis: verum
end;
hence b = a by A7, A11, A12, Th6; ::_thesis: verum
end;
a is finite by A7, Lm1;
hence a in mi ((K ^ L) \/ L) by A9, A10, Th7; ::_thesis: verum
end;
hence mi L c= mi ((K ^ L) \/ L) by Lm2; ::_thesis: verum
end;
theorem Th23: :: SUBSTLAT:23
for V, C being set
for B being Element of Fin (PFuncs (V,C)) holds B c= B ^ B
proof
let V, C be set ; ::_thesis: for B being Element of Fin (PFuncs (V,C)) holds B c= B ^ B
let B be Element of Fin (PFuncs (V,C)); ::_thesis: B c= B ^ B
now__::_thesis:_for_a_being_set_st_a_in_B_holds_
a_in_B_^_B
let a be set ; ::_thesis: ( a in B implies a in B ^ B )
assume A1: a in B ; ::_thesis: a in B ^ B
B c= PFuncs (V,C) by FINSUB_1:def_5;
then reconsider a9 = a as Element of PFuncs (V,C) by A1;
( a = a \/ a & a9 tolerates a9 ) ;
hence a in B ^ B by A1; ::_thesis: verum
end;
hence B c= B ^ B by Lm2; ::_thesis: verum
end;
theorem Th24: :: SUBSTLAT:24
for V, C being set
for A being Element of Fin (PFuncs (V,C)) holds mi (A ^ A) = mi A
proof
let V, C be set ; ::_thesis: for A being Element of Fin (PFuncs (V,C)) holds mi (A ^ A) = mi A
let A be Element of Fin (PFuncs (V,C)); ::_thesis: mi (A ^ A) = mi A
thus mi (A ^ A) = mi ((A ^ A) \/ A) by Th23, XBOOLE_1:12
.= mi A by Lm5 ; ::_thesis: verum
end;
theorem :: SUBSTLAT:25
for V, C being set
for K being Element of SubstitutionSet (V,C) holds mi (K ^ K) = K
proof
let V, C be set ; ::_thesis: for K being Element of SubstitutionSet (V,C) holds mi (K ^ K) = K
let K be Element of SubstitutionSet (V,C); ::_thesis: mi (K ^ K) = K
thus mi (K ^ K) = mi K by Th24
.= K by Th11 ; ::_thesis: verum
end;
begin
definition
let V, C be set ;
func SubstLatt (V,C) -> strict LattStr means :Def4: :: SUBSTLAT:def 4
( the carrier of it = SubstitutionSet (V,C) & ( for A, B being Element of SubstitutionSet (V,C) holds
( the L_join of it . (A,B) = mi (A \/ B) & the L_meet of it . (A,B) = mi (A ^ B) ) ) );
existence
ex b1 being strict LattStr st
( the carrier of b1 = SubstitutionSet (V,C) & ( for A, B being Element of SubstitutionSet (V,C) holds
( the L_join of b1 . (A,B) = mi (A \/ B) & the L_meet of b1 . (A,B) = mi (A ^ B) ) ) )
proof
deffunc H1( Element of SubstitutionSet (V,C), Element of SubstitutionSet (V,C)) -> Element of SubstitutionSet (V,C) = mi ($1 \/ $2);
consider j being BinOp of (SubstitutionSet (V,C)) such that
A1: for x, y being Element of SubstitutionSet (V,C) holds j . (x,y) = H1(x,y) from BINOP_1:sch_4();
deffunc H2( Element of SubstitutionSet (V,C), Element of SubstitutionSet (V,C)) -> Element of SubstitutionSet (V,C) = mi ($1 ^ $2);
consider m being BinOp of (SubstitutionSet (V,C)) such that
A2: for x, y being Element of SubstitutionSet (V,C) holds m . (x,y) = H2(x,y) from BINOP_1:sch_4();
take LattStr(# (SubstitutionSet (V,C)),j,m #) ; ::_thesis: ( the carrier of LattStr(# (SubstitutionSet (V,C)),j,m #) = SubstitutionSet (V,C) & ( for A, B being Element of SubstitutionSet (V,C) holds
( the L_join of LattStr(# (SubstitutionSet (V,C)),j,m #) . (A,B) = mi (A \/ B) & the L_meet of LattStr(# (SubstitutionSet (V,C)),j,m #) . (A,B) = mi (A ^ B) ) ) )
thus ( the carrier of LattStr(# (SubstitutionSet (V,C)),j,m #) = SubstitutionSet (V,C) & ( for A, B being Element of SubstitutionSet (V,C) holds
( the L_join of LattStr(# (SubstitutionSet (V,C)),j,m #) . (A,B) = mi (A \/ B) & the L_meet of LattStr(# (SubstitutionSet (V,C)),j,m #) . (A,B) = mi (A ^ B) ) ) ) by A1, A2; ::_thesis: verum
end;
uniqueness
for b1, b2 being strict LattStr st the carrier of b1 = SubstitutionSet (V,C) & ( for A, B being Element of SubstitutionSet (V,C) holds
( the L_join of b1 . (A,B) = mi (A \/ B) & the L_meet of b1 . (A,B) = mi (A ^ B) ) ) & the carrier of b2 = SubstitutionSet (V,C) & ( for A, B being Element of SubstitutionSet (V,C) holds
( the L_join of b2 . (A,B) = mi (A \/ B) & the L_meet of b2 . (A,B) = mi (A ^ B) ) ) holds
b1 = b2
proof
let A1, A2 be strict LattStr ; ::_thesis: ( the carrier of A1 = SubstitutionSet (V,C) & ( for A, B being Element of SubstitutionSet (V,C) holds
( the L_join of A1 . (A,B) = mi (A \/ B) & the L_meet of A1 . (A,B) = mi (A ^ B) ) ) & the carrier of A2 = SubstitutionSet (V,C) & ( for A, B being Element of SubstitutionSet (V,C) holds
( the L_join of A2 . (A,B) = mi (A \/ B) & the L_meet of A2 . (A,B) = mi (A ^ B) ) ) implies A1 = A2 )
assume that
A3: the carrier of A1 = SubstitutionSet (V,C) and
A4: for A, B being Element of SubstitutionSet (V,C) holds
( the L_join of A1 . (A,B) = mi (A \/ B) & the L_meet of A1 . (A,B) = mi (A ^ B) ) and
A5: the carrier of A2 = SubstitutionSet (V,C) and
A6: for A, B being Element of SubstitutionSet (V,C) holds
( the L_join of A2 . (A,B) = mi (A \/ B) & the L_meet of A2 . (A,B) = mi (A ^ B) ) ; ::_thesis: A1 = A2
reconsider a3 = the L_meet of A1, a4 = the L_meet of A2, a1 = the L_join of A1, a2 = the L_join of A2 as BinOp of (SubstitutionSet (V,C)) by A3, A5;
now__::_thesis:_for_x,_y_being_Element_of_SubstitutionSet_(V,C)_holds_a1_._(x,y)_=_a2_._(x,y)
let x, y be Element of SubstitutionSet (V,C); ::_thesis: a1 . (x,y) = a2 . (x,y)
thus a1 . (x,y) = mi (x \/ y) by A4
.= a2 . (x,y) by A6 ; ::_thesis: verum
end;
then A7: a1 = a2 by BINOP_1:2;
now__::_thesis:_for_x,_y_being_Element_of_SubstitutionSet_(V,C)_holds_a3_._(x,y)_=_a4_._(x,y)
let x, y be Element of SubstitutionSet (V,C); ::_thesis: a3 . (x,y) = a4 . (x,y)
thus a3 . (x,y) = mi (x ^ y) by A4
.= a4 . (x,y) by A6 ; ::_thesis: verum
end;
hence A1 = A2 by A3, A5, A7, BINOP_1:2; ::_thesis: verum
end;
end;
:: deftheorem Def4 defines SubstLatt SUBSTLAT:def_4_:_
for V, C being set
for b3 being strict LattStr holds
( b3 = SubstLatt (V,C) iff ( the carrier of b3 = SubstitutionSet (V,C) & ( for A, B being Element of SubstitutionSet (V,C) holds
( the L_join of b3 . (A,B) = mi (A \/ B) & the L_meet of b3 . (A,B) = mi (A ^ B) ) ) ) );
registration
let V, C be set ;
cluster SubstLatt (V,C) -> non empty strict ;
coherence
not SubstLatt (V,C) is empty
proof
the carrier of (SubstLatt (V,C)) = SubstitutionSet (V,C) by Def4;
hence not SubstLatt (V,C) is empty ; ::_thesis: verum
end;
end;
Lm6: for V, C being set
for a, b being Element of (SubstLatt (V,C)) holds a "\/" b = b "\/" a
proof
let V, C be set ; ::_thesis: for a, b being Element of (SubstLatt (V,C)) holds a "\/" b = b "\/" a
set G = SubstLatt (V,C);
let a, b be Element of (SubstLatt (V,C)); ::_thesis: a "\/" b = b "\/" a
reconsider a9 = a, b9 = b as Element of SubstitutionSet (V,C) by Def4;
a "\/" b = mi (b9 \/ a9) by Def4
.= b "\/" a by Def4 ;
hence a "\/" b = b "\/" a ; ::_thesis: verum
end;
Lm7: for V, C being set
for a, b, c being Element of (SubstLatt (V,C)) holds a "\/" (b "\/" c) = (a "\/" b) "\/" c
proof
let V, C be set ; ::_thesis: for a, b, c being Element of (SubstLatt (V,C)) holds a "\/" (b "\/" c) = (a "\/" b) "\/" c
let a, b, c be Element of (SubstLatt (V,C)); ::_thesis: a "\/" (b "\/" c) = (a "\/" b) "\/" c
reconsider a9 = a, b9 = b, c9 = c as Element of SubstitutionSet (V,C) by Def4;
set G = SubstLatt (V,C);
a "\/" (b "\/" c) = the L_join of (SubstLatt (V,C)) . (a,(mi (b9 \/ c9))) by Def4
.= mi ((mi (b9 \/ c9)) \/ a9) by Def4
.= mi (a9 \/ (b9 \/ c9)) by Th13
.= mi ((a9 \/ b9) \/ c9) by XBOOLE_1:4
.= mi ((mi (a9 \/ b9)) \/ c9) by Th13
.= the L_join of (SubstLatt (V,C)) . ((mi (a9 \/ b9)),c9) by Def4
.= (a "\/" b) "\/" c by Def4 ;
hence a "\/" (b "\/" c) = (a "\/" b) "\/" c ; ::_thesis: verum
end;
Lm8: for V, C being set
for K, L being Element of SubstitutionSet (V,C) holds the L_join of (SubstLatt (V,C)) . (( the L_meet of (SubstLatt (V,C)) . (K,L)),L) = L
proof
let V, C be set ; ::_thesis: for K, L being Element of SubstitutionSet (V,C) holds the L_join of (SubstLatt (V,C)) . (( the L_meet of (SubstLatt (V,C)) . (K,L)),L) = L
let K, L be Element of SubstitutionSet (V,C); ::_thesis: the L_join of (SubstLatt (V,C)) . (( the L_meet of (SubstLatt (V,C)) . (K,L)),L) = L
thus the L_join of (SubstLatt (V,C)) . (( the L_meet of (SubstLatt (V,C)) . (K,L)),L) = the L_join of (SubstLatt (V,C)) . ((mi (K ^ L)),L) by Def4
.= mi ((mi (K ^ L)) \/ L) by Def4
.= mi ((K ^ L) \/ L) by Th13
.= mi L by Lm5
.= L by Th11 ; ::_thesis: verum
end;
Lm9: for V, C being set
for a, b being Element of (SubstLatt (V,C)) holds (a "/\" b) "\/" b = b
proof
let V, C be set ; ::_thesis: for a, b being Element of (SubstLatt (V,C)) holds (a "/\" b) "\/" b = b
let a, b be Element of (SubstLatt (V,C)); ::_thesis: (a "/\" b) "\/" b = b
reconsider a9 = a, b9 = b as Element of SubstitutionSet (V,C) by Def4;
set G = SubstLatt (V,C);
thus (a "/\" b) "\/" b = the L_join of (SubstLatt (V,C)) . (( the L_meet of (SubstLatt (V,C)) . (a9,b9)),b9)
.= b by Lm8 ; ::_thesis: verum
end;
Lm10: for V, C being set
for a, b being Element of (SubstLatt (V,C)) holds a "/\" b = b "/\" a
proof
let V, C be set ; ::_thesis: for a, b being Element of (SubstLatt (V,C)) holds a "/\" b = b "/\" a
let a, b be Element of (SubstLatt (V,C)); ::_thesis: a "/\" b = b "/\" a
reconsider a9 = a, b9 = b as Element of SubstitutionSet (V,C) by Def4;
a "/\" b = mi (a9 ^ b9) by Def4
.= mi (b9 ^ a9) by Th3
.= b "/\" a by Def4 ;
hence a "/\" b = b "/\" a ; ::_thesis: verum
end;
Lm11: for V, C being set
for a, b, c being Element of (SubstLatt (V,C)) holds a "/\" (b "/\" c) = (a "/\" b) "/\" c
proof
let V, C be set ; ::_thesis: for a, b, c being Element of (SubstLatt (V,C)) holds a "/\" (b "/\" c) = (a "/\" b) "/\" c
let a, b, c be Element of (SubstLatt (V,C)); ::_thesis: a "/\" (b "/\" c) = (a "/\" b) "/\" c
reconsider a9 = a, b9 = b, c9 = c as Element of SubstitutionSet (V,C) by Def4;
set G = SubstLatt (V,C);
a "/\" (b "/\" c) = the L_meet of (SubstLatt (V,C)) . (a,(mi (b9 ^ c9))) by Def4
.= mi (a9 ^ (mi (b9 ^ c9))) by Def4
.= mi (a9 ^ (b9 ^ c9)) by Th20
.= mi ((a9 ^ b9) ^ c9) by Th21
.= mi ((mi (a9 ^ b9)) ^ c9) by Th19
.= the L_meet of (SubstLatt (V,C)) . ((mi (a9 ^ b9)),c9) by Def4
.= (a "/\" b) "/\" c by Def4 ;
hence a "/\" (b "/\" c) = (a "/\" b) "/\" c ; ::_thesis: verum
end;
Lm12: for V, C being set
for K, L, M being Element of SubstitutionSet (V,C) holds the L_meet of (SubstLatt (V,C)) . (K,( the L_join of (SubstLatt (V,C)) . (L,M))) = the L_join of (SubstLatt (V,C)) . (( the L_meet of (SubstLatt (V,C)) . (K,L)),( the L_meet of (SubstLatt (V,C)) . (K,M)))
proof
let V, C be set ; ::_thesis: for K, L, M being Element of SubstitutionSet (V,C) holds the L_meet of (SubstLatt (V,C)) . (K,( the L_join of (SubstLatt (V,C)) . (L,M))) = the L_join of (SubstLatt (V,C)) . (( the L_meet of (SubstLatt (V,C)) . (K,L)),( the L_meet of (SubstLatt (V,C)) . (K,M)))
let K, L, M be Element of SubstitutionSet (V,C); ::_thesis: the L_meet of (SubstLatt (V,C)) . (K,( the L_join of (SubstLatt (V,C)) . (L,M))) = the L_join of (SubstLatt (V,C)) . (( the L_meet of (SubstLatt (V,C)) . (K,L)),( the L_meet of (SubstLatt (V,C)) . (K,M)))
A1: the L_meet of (SubstLatt (V,C)) . (K,M) = mi (K ^ M) by Def4;
( the L_join of (SubstLatt (V,C)) . (L,M) = mi (L \/ M) & the L_meet of (SubstLatt (V,C)) . (K,L) = mi (K ^ L) ) by Def4;
then reconsider La = the L_join of (SubstLatt (V,C)) . (L,M), Lb = the L_meet of (SubstLatt (V,C)) . (K,L), Lc = the L_meet of (SubstLatt (V,C)) . (K,M) as Element of SubstitutionSet (V,C) by A1;
the L_meet of (SubstLatt (V,C)) . (K,( the L_join of (SubstLatt (V,C)) . (L,M))) = mi (K ^ La) by Def4
.= mi (K ^ (mi (L \/ M))) by Def4
.= mi (K ^ (L \/ M)) by Th20
.= mi ((K ^ L) \/ (K ^ M)) by Th22
.= mi ((mi (K ^ L)) \/ (K ^ M)) by Th13
.= mi ((mi (K ^ L)) \/ (mi (K ^ M))) by Th13
.= mi (Lb \/ (mi (K ^ M))) by Def4
.= mi (Lb \/ Lc) by Def4 ;
hence the L_meet of (SubstLatt (V,C)) . (K,( the L_join of (SubstLatt (V,C)) . (L,M))) = the L_join of (SubstLatt (V,C)) . (( the L_meet of (SubstLatt (V,C)) . (K,L)),( the L_meet of (SubstLatt (V,C)) . (K,M))) by Def4; ::_thesis: verum
end;
Lm13: for V, C being set
for a, b being Element of (SubstLatt (V,C)) holds a "/\" (a "\/" b) = a
proof
let V, C be set ; ::_thesis: for a, b being Element of (SubstLatt (V,C)) holds a "/\" (a "\/" b) = a
let a, b be Element of (SubstLatt (V,C)); ::_thesis: a "/\" (a "\/" b) = a
reconsider a9 = a, b9 = b as Element of SubstitutionSet (V,C) by Def4;
thus a "/\" (a "\/" b) = the L_join of (SubstLatt (V,C)) . (( the L_meet of (SubstLatt (V,C)) . (a9,a9)),( the L_meet of (SubstLatt (V,C)) . (a9,b9))) by Lm12
.= the L_join of (SubstLatt (V,C)) . ((mi (a9 ^ a9)),( the L_meet of (SubstLatt (V,C)) . (a9,b9))) by Def4
.= the L_join of (SubstLatt (V,C)) . ((mi a9),( the L_meet of (SubstLatt (V,C)) . (a9,b9))) by Th24
.= a "\/" (a "/\" b) by Th11
.= (a "/\" b) "\/" a by Lm6
.= (b "/\" a) "\/" a by Lm10
.= a by Lm9 ; ::_thesis: verum
end;
registration
let V, C be set ;
cluster SubstLatt (V,C) -> strict Lattice-like ;
coherence
SubstLatt (V,C) is Lattice-like
proof
set G = SubstLatt (V,C);
thus for u, v being Element of (SubstLatt (V,C)) holds u "\/" v = v "\/" u by Lm6; :: according to LATTICES:def_4,LATTICES:def_10 ::_thesis: ( SubstLatt (V,C) is join-associative & SubstLatt (V,C) is meet-absorbing & SubstLatt (V,C) is meet-commutative & SubstLatt (V,C) is meet-associative & SubstLatt (V,C) is join-absorbing )
thus for u, v, w being Element of (SubstLatt (V,C)) holds u "\/" (v "\/" w) = (u "\/" v) "\/" w by Lm7; :: according to LATTICES:def_5 ::_thesis: ( SubstLatt (V,C) is meet-absorbing & SubstLatt (V,C) is meet-commutative & SubstLatt (V,C) is meet-associative & SubstLatt (V,C) is join-absorbing )
thus for u, v being Element of (SubstLatt (V,C)) holds (u "/\" v) "\/" v = v by Lm9; :: according to LATTICES:def_8 ::_thesis: ( SubstLatt (V,C) is meet-commutative & SubstLatt (V,C) is meet-associative & SubstLatt (V,C) is join-absorbing )
thus for u, v being Element of (SubstLatt (V,C)) holds u "/\" v = v "/\" u by Lm10; :: according to LATTICES:def_6 ::_thesis: ( SubstLatt (V,C) is meet-associative & SubstLatt (V,C) is join-absorbing )
thus for u, v, w being Element of (SubstLatt (V,C)) holds u "/\" (v "/\" w) = (u "/\" v) "/\" w by Lm11; :: according to LATTICES:def_7 ::_thesis: SubstLatt (V,C) is join-absorbing
let u, v be Element of (SubstLatt (V,C)); :: according to LATTICES:def_9 ::_thesis: u "/\" (u "\/" v) = u
thus u "/\" (u "\/" v) = u by Lm13; ::_thesis: verum
end;
end;
registration
let V, C be set ;
cluster SubstLatt (V,C) -> strict distributive bounded ;
coherence
( SubstLatt (V,C) is distributive & SubstLatt (V,C) is bounded )
proof
thus SubstLatt (V,C) is distributive ::_thesis: SubstLatt (V,C) is bounded
proof
let u, v, w be Element of (SubstLatt (V,C)); :: according to LATTICES:def_11 ::_thesis: u "/\" (v "\/" w) = (u "/\" v) "\/" (u "/\" w)
reconsider K = u, L = v, M = w as Element of SubstitutionSet (V,C) by Def4;
thus u "/\" (v "\/" w) = the L_meet of (SubstLatt (V,C)) . (K,( the L_join of (SubstLatt (V,C)) . (L,M)))
.= (u "/\" v) "\/" (u "/\" w) by Lm12 ; ::_thesis: verum
end;
A1: SubstLatt (V,C) is lower-bounded
proof
reconsider E = {} as Element of SubstitutionSet (V,C) by Th1;
set L = SubstLatt (V,C);
reconsider e = E as Element of (SubstLatt (V,C)) by Def4;
take e ; :: according to LATTICES:def_13 ::_thesis: for b1 being Element of the carrier of (SubstLatt (V,C)) holds
( e "/\" b1 = e & b1 "/\" e = e )
let u be Element of (SubstLatt (V,C)); ::_thesis: ( e "/\" u = e & u "/\" e = e )
reconsider K = u as Element of SubstitutionSet (V,C) by Def4;
A2: e "\/" u = mi (E \/ K) by Def4
.= u by Th11 ;
then u "/\" e = e by LATTICES:def_9;
hence ( e "/\" u = e & u "/\" e = e ) by A2, LATTICES:def_9; ::_thesis: verum
end;
SubstLatt (V,C) is upper-bounded
proof
reconsider E = {{}} as Element of SubstitutionSet (V,C) by Th2;
set L = SubstLatt (V,C);
reconsider e = E as Element of (SubstLatt (V,C)) by Def4;
take e ; :: according to LATTICES:def_14 ::_thesis: for b1 being Element of the carrier of (SubstLatt (V,C)) holds
( e "\/" b1 = e & b1 "\/" e = e )
let u be Element of (SubstLatt (V,C)); ::_thesis: ( e "\/" u = e & u "\/" e = e )
reconsider K = u as Element of SubstitutionSet (V,C) by Def4;
A3: e "/\" u = mi (E ^ K) by Def4
.= mi (K ^ E) by Th3
.= mi K by Th4
.= u by Th11 ;
then e "\/" u = e by LATTICES:def_8;
hence ( e "\/" u = e & u "\/" e = e ) by A3, LATTICES:def_8; ::_thesis: verum
end;
hence SubstLatt (V,C) is bounded by A1; ::_thesis: verum
end;
end;
theorem :: SUBSTLAT:26
for V, C being set holds Bottom (SubstLatt (V,C)) = {}
proof
let V, C be set ; ::_thesis: Bottom (SubstLatt (V,C)) = {}
{} in SubstitutionSet (V,C) by Th1;
then reconsider Z = {} as Element of (SubstLatt (V,C)) by Def4;
now__::_thesis:_for_u_being_Element_of_(SubstLatt_(V,C))_holds_Z_"\/"_u_=_u
let u be Element of (SubstLatt (V,C)); ::_thesis: Z "\/" u = u
reconsider z = Z, u9 = u as Element of SubstitutionSet (V,C) by Def4;
thus Z "\/" u = mi (z \/ u9) by Def4
.= u by Th11 ; ::_thesis: verum
end;
hence Bottom (SubstLatt (V,C)) = {} by LATTICE2:14; ::_thesis: verum
end;
theorem :: SUBSTLAT:27
for V, C being set holds Top (SubstLatt (V,C)) = {{}}
proof
let V, C be set ; ::_thesis: Top (SubstLatt (V,C)) = {{}}
{{}} in SubstitutionSet (V,C) by Th2;
then reconsider Z = {{}} as Element of (SubstLatt (V,C)) by Def4;
now__::_thesis:_for_u_being_Element_of_(SubstLatt_(V,C))_holds_Z_"/\"_u_=_u
let u be Element of (SubstLatt (V,C)); ::_thesis: Z "/\" u = u
reconsider z = Z, u9 = u as Element of SubstitutionSet (V,C) by Def4;
thus Z "/\" u = mi (z ^ u9) by Def4
.= mi (u9 ^ z) by Th3
.= mi u9 by Th4
.= u by Th11 ; ::_thesis: verum
end;
hence Top (SubstLatt (V,C)) = {{}} by LATTICE2:16; ::_thesis: verum
end;