:: OSALG_2 semantic presentation
begin
theorem Th1: :: OSALG_2:1
for R being non empty Poset
for X, Y being OrderSortedSet of R holds X /\ Y is OrderSortedSet of R
proof
let R be non empty Poset; ::_thesis: for X, Y being OrderSortedSet of R holds X /\ Y is OrderSortedSet of R
let X, Y be OrderSortedSet of R; ::_thesis: X /\ Y is OrderSortedSet of R
reconsider M = X /\ Y as ManySortedSet of R ;
M is order-sorted
proof
let s1, s2 be Element of R; :: according to OSALG_1:def_16 ::_thesis: ( not s1 <= s2 or M . s1 c= M . s2 )
assume s1 <= s2 ; ::_thesis: M . s1 c= M . s2
then A1: ( X . s1 c= X . s2 & Y . s1 c= Y . s2 ) by OSALG_1:def_16;
( (X /\ Y) . s1 = (X . s1) /\ (Y . s1) & (X /\ Y) . s2 = (X . s2) /\ (Y . s2) ) by PBOOLE:def_5;
hence M . s1 c= M . s2 by A1, XBOOLE_1:27; ::_thesis: verum
end;
hence X /\ Y is OrderSortedSet of R ; ::_thesis: verum
end;
theorem Th2: :: OSALG_2:2
for R being non empty Poset
for X, Y being OrderSortedSet of R holds X \/ Y is OrderSortedSet of R
proof
let R be non empty Poset; ::_thesis: for X, Y being OrderSortedSet of R holds X \/ Y is OrderSortedSet of R
let X, Y be OrderSortedSet of R; ::_thesis: X \/ Y is OrderSortedSet of R
reconsider M = X \/ Y as ManySortedSet of R ;
M is order-sorted
proof
let s1, s2 be Element of R; :: according to OSALG_1:def_16 ::_thesis: ( not s1 <= s2 or M . s1 c= M . s2 )
assume s1 <= s2 ; ::_thesis: M . s1 c= M . s2
then A1: ( X . s1 c= X . s2 & Y . s1 c= Y . s2 ) by OSALG_1:def_16;
( (X \/ Y) . s1 = (X . s1) \/ (Y . s1) & (X \/ Y) . s2 = (X . s2) \/ (Y . s2) ) by PBOOLE:def_4;
hence M . s1 c= M . s2 by A1, XBOOLE_1:13; ::_thesis: verum
end;
hence X \/ Y is OrderSortedSet of R ; ::_thesis: verum
end;
definition
let R be non empty Poset;
let M be OrderSortedSet of R;
mode OrderSortedSubset of M -> ManySortedSubset of M means :Def1: :: OSALG_2:def 1
it is OrderSortedSet of R;
existence
ex b1 being ManySortedSubset of M st b1 is OrderSortedSet of R
proof
reconsider X = M as ManySortedSubset of M by PBOOLE:def_18;
take X ; ::_thesis: X is OrderSortedSet of R
thus X is OrderSortedSet of R ; ::_thesis: verum
end;
end;
:: deftheorem Def1 defines OrderSortedSubset OSALG_2:def_1_:_
for R being non empty Poset
for M being OrderSortedSet of R
for b3 being ManySortedSubset of M holds
( b3 is OrderSortedSubset of M iff b3 is OrderSortedSet of R );
registration
let R be non empty Poset;
let M be V8() OrderSortedSet of R;
cluster non empty Relation-like V8() the carrier of R -defined Function-like V17( the carrier of R) for OrderSortedSubset of M;
existence
not for b1 being OrderSortedSubset of M holds b1 is V8()
proof
reconsider N = M as ManySortedSubset of M by PBOOLE:def_18;
reconsider N1 = N as OrderSortedSubset of M by Def1;
take N1 ; ::_thesis: N1 is V8()
thus N1 is V8() ; ::_thesis: verum
end;
end;
begin
definition
let S be OrderSortedSign;
let U0 be OSAlgebra of S;
mode OSSubset of U0 -> ManySortedSubset of the Sorts of U0 means :Def2: :: OSALG_2:def 2
it is OrderSortedSet of S;
existence
ex b1 being ManySortedSubset of the Sorts of U0 st b1 is OrderSortedSet of S
proof
reconsider B = the Sorts of U0 as MSSubset of U0 by PBOOLE:def_18;
take B ; ::_thesis: B is OrderSortedSet of S
thus B is OrderSortedSet of S by OSALG_1:17; ::_thesis: verum
end;
end;
:: deftheorem Def2 defines OSSubset OSALG_2:def_2_:_
for S being OrderSortedSign
for U0 being OSAlgebra of S
for b3 being ManySortedSubset of the Sorts of U0 holds
( b3 is OSSubset of U0 iff b3 is OrderSortedSet of S );
registration
let S be OrderSortedSign;
cluster strict non-empty order-sorted monotone for MSAlgebra over S;
existence
ex b1 being OSAlgebra of S st
( b1 is monotone & b1 is strict & b1 is non-empty )
proof
set z1 = the Element of {{}};
take TrivialOSA (S,{{}}, the Element of {{}}) ; ::_thesis: ( TrivialOSA (S,{{}}, the Element of {{}}) is monotone & TrivialOSA (S,{{}}, the Element of {{}}) is strict & TrivialOSA (S,{{}}, the Element of {{}}) is non-empty )
thus ( TrivialOSA (S,{{}}, the Element of {{}}) is monotone & TrivialOSA (S,{{}}, the Element of {{}}) is strict & TrivialOSA (S,{{}}, the Element of {{}}) is non-empty ) ; ::_thesis: verum
end;
end;
registration
let S be OrderSortedSign;
let U0 be non-empty OSAlgebra of S;
cluster non empty Relation-like V8() the carrier of S -defined Function-like V17( the carrier of S) for OSSubset of U0;
existence
not for b1 being OSSubset of U0 holds b1 is V8()
proof
reconsider N = the Sorts of U0 as MSSubset of U0 by PBOOLE:def_18;
the Sorts of U0 is OrderSortedSet of S by OSALG_1:17;
then reconsider M = N as OSSubset of U0 by Def2;
take M ; ::_thesis: M is V8()
thus M is V8() ; ::_thesis: verum
end;
end;
theorem Th3: :: OSALG_2:3
for S0 being non empty non void strict all-with_const_op ManySortedSign holds OSSign S0 is all-with_const_op
proof
let S0 be non empty non void strict all-with_const_op ManySortedSign ; ::_thesis: OSSign S0 is all-with_const_op
let s be Element of (OSSign S0); :: according to MSUALG_2:def_2 ::_thesis: s is with_const_op
reconsider s1 = s as Element of S0 by OSALG_1:def_5;
s1 is with_const_op by MSUALG_2:def_2;
then consider o being Element of the carrier' of S0 such that
A1: ( the Arity of S0 . o = {} & the ResultSort of S0 . o = s1 ) by MSUALG_2:def_1;
A2: o is Element of the carrier' of (OSSign S0) by OSALG_1:def_5;
( the Arity of (OSSign S0) . o = {} & the ResultSort of (OSSign S0) . o = s1 ) by A1, OSALG_1:def_5;
hence s is with_const_op by A2, MSUALG_2:def_1; ::_thesis: verum
end;
registration
cluster non empty non void V52() all-with_const_op V99() V100() V101() strict order-sorted discernable for OverloadedRSSign ;
existence
ex b1 being OrderSortedSign st
( b1 is all-with_const_op & b1 is strict )
proof
set S0 = the non empty non void strict all-with_const_op ManySortedSign ;
take OSSign the non empty non void strict all-with_const_op ManySortedSign ; ::_thesis: ( OSSign the non empty non void strict all-with_const_op ManySortedSign is all-with_const_op & OSSign the non empty non void strict all-with_const_op ManySortedSign is strict )
thus ( OSSign the non empty non void strict all-with_const_op ManySortedSign is all-with_const_op & OSSign the non empty non void strict all-with_const_op ManySortedSign is strict ) by Th3; ::_thesis: verum
end;
end;
begin
theorem Th4: :: OSALG_2:4
for S being OrderSortedSign
for U0 being OSAlgebra of S holds MSAlgebra(# the Sorts of U0, the Charact of U0 #) is order-sorted
proof
let S be OrderSortedSign; ::_thesis: for U0 being OSAlgebra of S holds MSAlgebra(# the Sorts of U0, the Charact of U0 #) is order-sorted
let U0 be OSAlgebra of S; ::_thesis: MSAlgebra(# the Sorts of U0, the Charact of U0 #) is order-sorted
the Sorts of U0 is OrderSortedSet of S by OSALG_1:17;
hence MSAlgebra(# the Sorts of U0, the Charact of U0 #) is order-sorted by OSALG_1:17; ::_thesis: verum
end;
registration
let S be OrderSortedSign;
let U0 be OSAlgebra of S;
cluster order-sorted for MSSubAlgebra of U0;
existence
ex b1 being MSSubAlgebra of U0 st b1 is order-sorted
proof
reconsider U1 = MSAlgebra(# the Sorts of U0, the Charact of U0 #) as strict MSSubAlgebra of U0 by MSUALG_2:37;
take U1 ; ::_thesis: U1 is order-sorted
thus U1 is order-sorted by Th4; ::_thesis: verum
end;
end;
definition
let S be OrderSortedSign;
let U0 be OSAlgebra of S;
mode OSSubAlgebra of U0 is order-sorted MSSubAlgebra of U0;
end;
registration
let S be OrderSortedSign;
let U0 be OSAlgebra of S;
cluster strict order-sorted for MSSubAlgebra of U0;
existence
ex b1 being OSSubAlgebra of U0 st b1 is strict
proof
reconsider U1 = MSAlgebra(# the Sorts of U0, the Charact of U0 #) as order-sorted MSSubAlgebra of U0 by Th4, MSUALG_2:37;
take U1 ; ::_thesis: U1 is strict
thus U1 is strict ; ::_thesis: verum
end;
end;
registration
let S be OrderSortedSign;
let U0 be non-empty OSAlgebra of S;
cluster strict non-empty order-sorted for MSSubAlgebra of U0;
existence
ex b1 being OSSubAlgebra of U0 st
( b1 is non-empty & b1 is strict )
proof
set U1 = MSAlgebra(# the Sorts of U0, the Charact of U0 #);
the Sorts of U0 is OrderSortedSet of S by OSALG_1:17;
then reconsider U1 = MSAlgebra(# the Sorts of U0, the Charact of U0 #) as strict OSSubAlgebra of U0 by MSUALG_2:37, OSALG_1:17;
take U1 ; ::_thesis: ( U1 is non-empty & U1 is strict )
thus ( U1 is non-empty & U1 is strict ) ; ::_thesis: verum
end;
end;
theorem Th5: :: OSALG_2:5
for S being OrderSortedSign
for U0 being OSAlgebra of S
for U1 being MSAlgebra over S holds
( U1 is OSSubAlgebra of U0 iff ( the Sorts of U1 is OSSubset of U0 & ( for B being OSSubset of U0 st B = the Sorts of U1 holds
( B is opers_closed & the Charact of U1 = Opers (U0,B) ) ) ) )
proof
let S be OrderSortedSign; ::_thesis: for U0 being OSAlgebra of S
for U1 being MSAlgebra over S holds
( U1 is OSSubAlgebra of U0 iff ( the Sorts of U1 is OSSubset of U0 & ( for B being OSSubset of U0 st B = the Sorts of U1 holds
( B is opers_closed & the Charact of U1 = Opers (U0,B) ) ) ) )
let U0 be OSAlgebra of S; ::_thesis: for U1 being MSAlgebra over S holds
( U1 is OSSubAlgebra of U0 iff ( the Sorts of U1 is OSSubset of U0 & ( for B being OSSubset of U0 st B = the Sorts of U1 holds
( B is opers_closed & the Charact of U1 = Opers (U0,B) ) ) ) )
let U1 be MSAlgebra over S; ::_thesis: ( U1 is OSSubAlgebra of U0 iff ( the Sorts of U1 is OSSubset of U0 & ( for B being OSSubset of U0 st B = the Sorts of U1 holds
( B is opers_closed & the Charact of U1 = Opers (U0,B) ) ) ) )
hereby ::_thesis: ( the Sorts of U1 is OSSubset of U0 & ( for B being OSSubset of U0 st B = the Sorts of U1 holds
( B is opers_closed & the Charact of U1 = Opers (U0,B) ) ) implies U1 is OSSubAlgebra of U0 )
assume A1: U1 is OSSubAlgebra of U0 ; ::_thesis: ( the Sorts of U1 is OSSubset of U0 & ( for B being OSSubset of U0 st B = the Sorts of U1 holds
( B is opers_closed & the Charact of U1 = Opers (U0,B) ) ) )
then ( the Sorts of U1 is OrderSortedSet of S & the Sorts of U1 is MSSubset of U0 ) by MSUALG_2:def_9, OSALG_1:17;
hence the Sorts of U1 is OSSubset of U0 by Def2; ::_thesis: for B being OSSubset of U0 st B = the Sorts of U1 holds
( B is opers_closed & the Charact of U1 = Opers (U0,B) )
let B be OSSubset of U0; ::_thesis: ( B = the Sorts of U1 implies ( B is opers_closed & the Charact of U1 = Opers (U0,B) ) )
assume B = the Sorts of U1 ; ::_thesis: ( B is opers_closed & the Charact of U1 = Opers (U0,B) )
hence ( B is opers_closed & the Charact of U1 = Opers (U0,B) ) by A1, MSUALG_2:def_9; ::_thesis: verum
end;
assume A2: the Sorts of U1 is OSSubset of U0 ; ::_thesis: ( ex B being OSSubset of U0 st
( B = the Sorts of U1 & not ( B is opers_closed & the Charact of U1 = Opers (U0,B) ) ) or U1 is OSSubAlgebra of U0 )
assume A3: for B being OSSubset of U0 st B = the Sorts of U1 holds
( B is opers_closed & the Charact of U1 = Opers (U0,B) ) ; ::_thesis: U1 is OSSubAlgebra of U0
A4: U1 is MSSubAlgebra of U0
proof
thus the Sorts of U1 is MSSubset of U0 by A2; :: according to MSUALG_2:def_9 ::_thesis: for b1 being ManySortedSubset of the Sorts of U0 holds
( not b1 = the Sorts of U1 or ( b1 is opers_closed & the Charact of U1 = Opers (U0,b1) ) )
let B be MSSubset of U0; ::_thesis: ( not B = the Sorts of U1 or ( B is opers_closed & the Charact of U1 = Opers (U0,B) ) )
assume A5: B = the Sorts of U1 ; ::_thesis: ( B is opers_closed & the Charact of U1 = Opers (U0,B) )
reconsider B1 = B as OSSubset of U0 by A2, A5;
B1 is opers_closed by A3, A5;
hence ( B is opers_closed & the Charact of U1 = Opers (U0,B) ) by A3, A5; ::_thesis: verum
end;
the Sorts of U1 is OrderSortedSet of S by A2, Def2;
hence U1 is OSSubAlgebra of U0 by A4, OSALG_1:17; ::_thesis: verum
end;
definition
let S1 be OrderSortedSign;
let OU0 be OSAlgebra of S1;
let s be SortSymbol of S1;
func OSConstants (OU0,s) -> Subset of ( the Sorts of OU0 . s) equals :: OSALG_2:def 3
union { (Constants (OU0,s2)) where s2 is SortSymbol of S1 : s2 <= s } ;
coherence
union { (Constants (OU0,s2)) where s2 is SortSymbol of S1 : s2 <= s } is Subset of ( the Sorts of OU0 . s)
proof
set Cs = { (Constants (OU0,s2)) where s2 is SortSymbol of S1 : s2 <= s } ;
for X being set st X in { (Constants (OU0,s2)) where s2 is SortSymbol of S1 : s2 <= s } holds
X c= the Sorts of OU0 . s
proof
let X be set ; ::_thesis: ( X in { (Constants (OU0,s2)) where s2 is SortSymbol of S1 : s2 <= s } implies X c= the Sorts of OU0 . s )
assume X in { (Constants (OU0,s2)) where s2 is SortSymbol of S1 : s2 <= s } ; ::_thesis: X c= the Sorts of OU0 . s
then consider s2 being SortSymbol of S1 such that
A1: X = Constants (OU0,s2) and
A2: s2 <= s ;
the Sorts of OU0 . s2 c= the Sorts of OU0 . s by A2, OSALG_1:def_17;
hence X c= the Sorts of OU0 . s by A1, XBOOLE_1:1; ::_thesis: verum
end;
hence union { (Constants (OU0,s2)) where s2 is SortSymbol of S1 : s2 <= s } is Subset of ( the Sorts of OU0 . s) by ZFMISC_1:76; ::_thesis: verum
end;
end;
:: deftheorem defines OSConstants OSALG_2:def_3_:_
for S1 being OrderSortedSign
for OU0 being OSAlgebra of S1
for s being SortSymbol of S1 holds OSConstants (OU0,s) = union { (Constants (OU0,s2)) where s2 is SortSymbol of S1 : s2 <= s } ;
theorem Th6: :: OSALG_2:6
for S1 being OrderSortedSign
for OU0 being OSAlgebra of S1
for s being SortSymbol of S1 holds Constants (OU0,s) c= OSConstants (OU0,s)
proof
let S1 be OrderSortedSign; ::_thesis: for OU0 being OSAlgebra of S1
for s being SortSymbol of S1 holds Constants (OU0,s) c= OSConstants (OU0,s)
let OU0 be OSAlgebra of S1; ::_thesis: for s being SortSymbol of S1 holds Constants (OU0,s) c= OSConstants (OU0,s)
let s be SortSymbol of S1; ::_thesis: Constants (OU0,s) c= OSConstants (OU0,s)
Constants (OU0,s) in { (Constants (OU0,s2)) where s2 is SortSymbol of S1 : s2 <= s } ;
hence Constants (OU0,s) c= OSConstants (OU0,s) by ZFMISC_1:74; ::_thesis: verum
end;
definition
let S1 be OrderSortedSign;
let M be ManySortedSet of the carrier of S1;
func OSCl M -> OrderSortedSet of S1 means :Def4: :: OSALG_2:def 4
for s being SortSymbol of S1 holds it . s = union { (M . s1) where s1 is SortSymbol of S1 : s1 <= s } ;
existence
ex b1 being OrderSortedSet of S1 st
for s being SortSymbol of S1 holds b1 . s = union { (M . s1) where s1 is SortSymbol of S1 : s1 <= s }
proof
deffunc H1( Element of S1) -> set = union { (M . s1) where s1 is SortSymbol of S1 : s1 <= $1 } ;
consider f being Function such that
A1: ( dom f = the carrier of S1 & ( for d being Element of S1 holds f . d = H1(d) ) ) from FUNCT_1:sch_4();
reconsider f = f as ManySortedSet of the carrier of S1 by A1, PARTFUN1:def_2, RELAT_1:def_18;
reconsider f1 = f as ManySortedSet of S1 ;
f1 is order-sorted
proof
let r1, r2 be Element of S1; :: according to OSALG_1:def_16 ::_thesis: ( not r1 <= r2 or f1 . r1 c= f1 . r2 )
assume A2: r1 <= r2 ; ::_thesis: f1 . r1 c= f1 . r2
let x be set ; :: according to TARSKI:def_3 ::_thesis: ( not x in f1 . r1 or x in f1 . r2 )
assume x in f1 . r1 ; ::_thesis: x in f1 . r2
then x in union { (M . s2) where s2 is SortSymbol of S1 : s2 <= r1 } by A1;
then consider y being set such that
A3: ( x in y & y in { (M . s2) where s2 is SortSymbol of S1 : s2 <= r1 } ) by TARSKI:def_4;
consider s3 being SortSymbol of S1 such that
A4: y = M . s3 and
A5: s3 <= r1 by A3;
s3 <= r2 by A2, A5, ORDERS_2:3;
then y in { (M . s2) where s2 is SortSymbol of S1 : s2 <= r2 } by A4;
then x in union { (M . s2) where s2 is SortSymbol of S1 : s2 <= r2 } by A3, TARSKI:def_4;
hence x in f1 . r2 by A1; ::_thesis: verum
end;
then reconsider f2 = f1 as OrderSortedSet of S1 ;
take f2 ; ::_thesis: for s being SortSymbol of S1 holds f2 . s = union { (M . s1) where s1 is SortSymbol of S1 : s1 <= s }
thus for s being SortSymbol of S1 holds f2 . s = union { (M . s1) where s1 is SortSymbol of S1 : s1 <= s } by A1; ::_thesis: verum
end;
uniqueness
for b1, b2 being OrderSortedSet of S1 st ( for s being SortSymbol of S1 holds b1 . s = union { (M . s1) where s1 is SortSymbol of S1 : s1 <= s } ) & ( for s being SortSymbol of S1 holds b2 . s = union { (M . s1) where s1 is SortSymbol of S1 : s1 <= s } ) holds
b1 = b2
proof
let W1, W2 be OrderSortedSet of S1; ::_thesis: ( ( for s being SortSymbol of S1 holds W1 . s = union { (M . s1) where s1 is SortSymbol of S1 : s1 <= s } ) & ( for s being SortSymbol of S1 holds W2 . s = union { (M . s1) where s1 is SortSymbol of S1 : s1 <= s } ) implies W1 = W2 )
assume A6: for s being SortSymbol of S1 holds W1 . s = union { (M . s1) where s1 is SortSymbol of S1 : s1 <= s } ; ::_thesis: ( ex s being SortSymbol of S1 st not W2 . s = union { (M . s1) where s1 is SortSymbol of S1 : s1 <= s } or W1 = W2 )
assume A7: for s being SortSymbol of S1 holds W2 . s = union { (M . s1) where s1 is SortSymbol of S1 : s1 <= s } ; ::_thesis: W1 = W2
for s being set st s in the carrier of S1 holds
W1 . s = W2 . s
proof
let s be set ; ::_thesis: ( s in the carrier of S1 implies W1 . s = W2 . s )
assume s in the carrier of S1 ; ::_thesis: W1 . s = W2 . s
then reconsider t = s as SortSymbol of S1 ;
W1 . s = union { (M . s1) where s1 is SortSymbol of S1 : s1 <= t } by A6
.= W2 . s by A7 ;
hence W1 . s = W2 . s ; ::_thesis: verum
end;
hence W1 = W2 by PBOOLE:3; ::_thesis: verum
end;
end;
:: deftheorem Def4 defines OSCl OSALG_2:def_4_:_
for S1 being OrderSortedSign
for M being ManySortedSet of the carrier of S1
for b3 being OrderSortedSet of S1 holds
( b3 = OSCl M iff for s being SortSymbol of S1 holds b3 . s = union { (M . s1) where s1 is SortSymbol of S1 : s1 <= s } );
theorem Th7: :: OSALG_2:7
for S1 being OrderSortedSign
for M being ManySortedSet of the carrier of S1 holds M c= OSCl M
proof
let S1 be OrderSortedSign; ::_thesis: for M being ManySortedSet of the carrier of S1 holds M c= OSCl M
let M be ManySortedSet of the carrier of S1; ::_thesis: M c= OSCl M
let i be set ; :: according to PBOOLE:def_2 ::_thesis: ( not i in the carrier of S1 or M . i c= (OSCl M) . i )
assume i in the carrier of S1 ; ::_thesis: M . i c= (OSCl M) . i
then reconsider s = i as SortSymbol of S1 ;
M . s in { (M . s1) where s1 is SortSymbol of S1 : s1 <= s } ;
then M . s c= union { (M . s1) where s1 is SortSymbol of S1 : s1 <= s } by ZFMISC_1:74;
hence M . i c= (OSCl M) . i by Def4; ::_thesis: verum
end;
theorem Th8: :: OSALG_2:8
for S1 being OrderSortedSign
for M being ManySortedSet of the carrier of S1
for A being OrderSortedSet of S1 st M c= A holds
OSCl M c= A
proof
let S1 be OrderSortedSign; ::_thesis: for M being ManySortedSet of the carrier of S1
for A being OrderSortedSet of S1 st M c= A holds
OSCl M c= A
let M be ManySortedSet of the carrier of S1; ::_thesis: for A being OrderSortedSet of S1 st M c= A holds
OSCl M c= A
let A be OrderSortedSet of S1; ::_thesis: ( M c= A implies OSCl M c= A )
assume A1: M c= A ; ::_thesis: OSCl M c= A
assume not OSCl M c= A ; ::_thesis: contradiction
then consider i being set such that
A2: i in the carrier of S1 and
A3: not (OSCl M) . i c= A . i by PBOOLE:def_2;
reconsider s = i as SortSymbol of S1 by A2;
consider x being set such that
A4: x in (OSCl M) . i and
A5: not x in A . i by A3, TARSKI:def_3;
(OSCl M) . s = union { (M . s2) where s2 is SortSymbol of S1 : s2 <= s } by Def4;
then consider X1 being set such that
A6: x in X1 and
A7: X1 in { (M . s2) where s2 is SortSymbol of S1 : s2 <= s } by A4, TARSKI:def_4;
consider s1 being SortSymbol of S1 such that
A8: X1 = M . s1 and
A9: s1 <= s by A7;
M . s1 c= A . s1 by A1, PBOOLE:def_2;
then A10: x in A . s1 by A6, A8;
A . s1 c= A . s by A9, OSALG_1:def_16;
hence contradiction by A5, A10; ::_thesis: verum
end;
theorem :: OSALG_2:9
for S being OrderSortedSign
for X being OrderSortedSet of S holds OSCl X = X
proof
let S be OrderSortedSign; ::_thesis: for X being OrderSortedSet of S holds OSCl X = X
let X be OrderSortedSet of S; ::_thesis: OSCl X = X
( X c= OSCl X & OSCl X c= X ) by Th7, Th8;
hence OSCl X = X by PBOOLE:146; ::_thesis: verum
end;
definition
let S1 be OrderSortedSign;
let OU0 be OSAlgebra of S1;
func OSConstants OU0 -> OSSubset of OU0 means :Def5: :: OSALG_2:def 5
for s being SortSymbol of S1 holds it . s = OSConstants (OU0,s);
existence
ex b1 being OSSubset of OU0 st
for s being SortSymbol of S1 holds b1 . s = OSConstants (OU0,s)
proof
deffunc H1( Element of S1) -> set = union { (Constants (OU0,s1)) where s1 is SortSymbol of S1 : s1 <= $1 } ;
consider f being Function such that
A1: ( dom f = the carrier of S1 & ( for d being Element of S1 holds f . d = H1(d) ) ) from FUNCT_1:sch_4();
reconsider f = f as ManySortedSet of the carrier of S1 by A1, PARTFUN1:def_2, RELAT_1:def_18;
f c= the Sorts of OU0
proof
let s be set ; :: according to PBOOLE:def_2 ::_thesis: ( not s in the carrier of S1 or f . s c= the Sorts of OU0 . s )
assume s in the carrier of S1 ; ::_thesis: f . s c= the Sorts of OU0 . s
then reconsider s1 = s as SortSymbol of S1 ;
f . s1 = OSConstants (OU0,s1) by A1;
hence f . s c= the Sorts of OU0 . s ; ::_thesis: verum
end;
then reconsider f = f as MSSubset of OU0 by PBOOLE:def_18;
take f ; ::_thesis: ( f is OSSubset of OU0 & ( for s being SortSymbol of S1 holds f . s = OSConstants (OU0,s) ) )
reconsider f1 = f as ManySortedSet of S1 ;
f1 is order-sorted
proof
let r1, r2 be Element of S1; :: according to OSALG_1:def_16 ::_thesis: ( not r1 <= r2 or f1 . r1 c= f1 . r2 )
assume A2: r1 <= r2 ; ::_thesis: f1 . r1 c= f1 . r2
let x be set ; :: according to TARSKI:def_3 ::_thesis: ( not x in f1 . r1 or x in f1 . r2 )
assume x in f1 . r1 ; ::_thesis: x in f1 . r2
then x in union { (Constants (OU0,s2)) where s2 is SortSymbol of S1 : s2 <= r1 } by A1;
then consider y being set such that
A3: ( x in y & y in { (Constants (OU0,s2)) where s2 is SortSymbol of S1 : s2 <= r1 } ) by TARSKI:def_4;
consider s3 being SortSymbol of S1 such that
A4: y = Constants (OU0,s3) and
A5: s3 <= r1 by A3;
s3 <= r2 by A2, A5, ORDERS_2:3;
then y in { (Constants (OU0,s2)) where s2 is SortSymbol of S1 : s2 <= r2 } by A4;
then x in union { (Constants (OU0,s2)) where s2 is SortSymbol of S1 : s2 <= r2 } by A3, TARSKI:def_4;
hence x in f1 . r2 by A1; ::_thesis: verum
end;
hence f is OSSubset of OU0 by Def2; ::_thesis: for s being SortSymbol of S1 holds f . s = OSConstants (OU0,s)
thus for s being SortSymbol of S1 holds f . s = OSConstants (OU0,s) by A1; ::_thesis: verum
end;
uniqueness
for b1, b2 being OSSubset of OU0 st ( for s being SortSymbol of S1 holds b1 . s = OSConstants (OU0,s) ) & ( for s being SortSymbol of S1 holds b2 . s = OSConstants (OU0,s) ) holds
b1 = b2
proof
let W1, W2 be OSSubset of OU0; ::_thesis: ( ( for s being SortSymbol of S1 holds W1 . s = OSConstants (OU0,s) ) & ( for s being SortSymbol of S1 holds W2 . s = OSConstants (OU0,s) ) implies W1 = W2 )
assume that
A6: for s being SortSymbol of S1 holds W1 . s = OSConstants (OU0,s) and
A7: for s being SortSymbol of S1 holds W2 . s = OSConstants (OU0,s) ; ::_thesis: W1 = W2
for s being set st s in the carrier of S1 holds
W1 . s = W2 . s
proof
let s be set ; ::_thesis: ( s in the carrier of S1 implies W1 . s = W2 . s )
assume s in the carrier of S1 ; ::_thesis: W1 . s = W2 . s
then reconsider t = s as SortSymbol of S1 ;
W1 . t = OSConstants (OU0,t) by A6;
hence W1 . s = W2 . s by A7; ::_thesis: verum
end;
hence W1 = W2 by PBOOLE:3; ::_thesis: verum
end;
end;
:: deftheorem Def5 defines OSConstants OSALG_2:def_5_:_
for S1 being OrderSortedSign
for OU0 being OSAlgebra of S1
for b3 being OSSubset of OU0 holds
( b3 = OSConstants OU0 iff for s being SortSymbol of S1 holds b3 . s = OSConstants (OU0,s) );
theorem Th10: :: OSALG_2:10
for S1 being OrderSortedSign
for OU0 being OSAlgebra of S1 holds Constants OU0 c= OSConstants OU0
proof
let S1 be OrderSortedSign; ::_thesis: for OU0 being OSAlgebra of S1 holds Constants OU0 c= OSConstants OU0
let OU0 be OSAlgebra of S1; ::_thesis: Constants OU0 c= OSConstants OU0
let i be set ; :: according to PBOOLE:def_2 ::_thesis: ( not i in the carrier of S1 or (Constants OU0) . i c= (OSConstants OU0) . i )
assume i in the carrier of S1 ; ::_thesis: (Constants OU0) . i c= (OSConstants OU0) . i
then reconsider s = i as SortSymbol of S1 ;
( (Constants OU0) . s = Constants (OU0,s) & (OSConstants OU0) . s = OSConstants (OU0,s) ) by Def5, MSUALG_2:def_4;
hence (Constants OU0) . i c= (OSConstants OU0) . i by Th6; ::_thesis: verum
end;
theorem Th11: :: OSALG_2:11
for S1 being OrderSortedSign
for OU0 being OSAlgebra of S1
for A being OSSubset of OU0 st Constants OU0 c= A holds
OSConstants OU0 c= A
proof
let S1 be OrderSortedSign; ::_thesis: for OU0 being OSAlgebra of S1
for A being OSSubset of OU0 st Constants OU0 c= A holds
OSConstants OU0 c= A
let OU0 be OSAlgebra of S1; ::_thesis: for A being OSSubset of OU0 st Constants OU0 c= A holds
OSConstants OU0 c= A
let A be OSSubset of OU0; ::_thesis: ( Constants OU0 c= A implies OSConstants OU0 c= A )
assume A1: Constants OU0 c= A ; ::_thesis: OSConstants OU0 c= A
assume not OSConstants OU0 c= A ; ::_thesis: contradiction
then consider i being set such that
A2: i in the carrier of S1 and
A3: not (OSConstants OU0) . i c= A . i by PBOOLE:def_2;
reconsider s = i as SortSymbol of S1 by A2;
consider x being set such that
A4: x in (OSConstants OU0) . i and
A5: not x in A . i by A3, TARSKI:def_3;
(OSConstants OU0) . s = OSConstants (OU0,s) by Def5
.= union { (Constants (OU0,s2)) where s2 is SortSymbol of S1 : s2 <= s } ;
then consider X1 being set such that
A6: x in X1 and
A7: X1 in { (Constants (OU0,s2)) where s2 is SortSymbol of S1 : s2 <= s } by A4, TARSKI:def_4;
consider s1 being SortSymbol of S1 such that
A8: X1 = Constants (OU0,s1) and
A9: s1 <= s by A7;
A10: (Constants OU0) . s1 c= A . s1 by A1, PBOOLE:def_2;
x in (Constants OU0) . s1 by A6, A8, MSUALG_2:def_4;
then A11: x in A . s1 by A10;
A is OrderSortedSet of S1 by Def2;
then A . s1 c= A . s by A9, OSALG_1:def_16;
hence contradiction by A5, A11; ::_thesis: verum
end;
theorem :: OSALG_2:12
for S1 being OrderSortedSign
for OU0 being OSAlgebra of S1
for A being OSSubset of OU0 holds OSConstants OU0 = OSCl (Constants OU0)
proof
let S1 be OrderSortedSign; ::_thesis: for OU0 being OSAlgebra of S1
for A being OSSubset of OU0 holds OSConstants OU0 = OSCl (Constants OU0)
let OU0 be OSAlgebra of S1; ::_thesis: for A being OSSubset of OU0 holds OSConstants OU0 = OSCl (Constants OU0)
let A be OSSubset of OU0; ::_thesis: OSConstants OU0 = OSCl (Constants OU0)
A1: now__::_thesis:_for_i_being_set_st_i_in_the_carrier_of_S1_holds_
(OSConstants_OU0)_._i_=_(OSCl_(Constants_OU0))_._i
let i be set ; ::_thesis: ( i in the carrier of S1 implies (OSConstants OU0) . i = (OSCl (Constants OU0)) . i )
assume i in the carrier of S1 ; ::_thesis: (OSConstants OU0) . i = (OSCl (Constants OU0)) . i
then reconsider s = i as SortSymbol of S1 ;
set c1 = { ((Constants OU0) . s1) where s1 is SortSymbol of S1 : s1 <= s } ;
set c2 = { (Constants (OU0,s1)) where s1 is SortSymbol of S1 : s1 <= s } ;
for x being set holds
( x in { ((Constants OU0) . s1) where s1 is SortSymbol of S1 : s1 <= s } iff x in { (Constants (OU0,s1)) where s1 is SortSymbol of S1 : s1 <= s } )
proof
let x be set ; ::_thesis: ( x in { ((Constants OU0) . s1) where s1 is SortSymbol of S1 : s1 <= s } iff x in { (Constants (OU0,s1)) where s1 is SortSymbol of S1 : s1 <= s } )
hereby ::_thesis: ( x in { (Constants (OU0,s1)) where s1 is SortSymbol of S1 : s1 <= s } implies x in { ((Constants OU0) . s1) where s1 is SortSymbol of S1 : s1 <= s } )
assume x in { ((Constants OU0) . s1) where s1 is SortSymbol of S1 : s1 <= s } ; ::_thesis: x in { (Constants (OU0,s1)) where s1 is SortSymbol of S1 : s1 <= s }
then consider s1 being SortSymbol of S1 such that
A2: x = (Constants OU0) . s1 and
A3: s1 <= s ;
x = Constants (OU0,s1) by A2, MSUALG_2:def_4;
hence x in { (Constants (OU0,s1)) where s1 is SortSymbol of S1 : s1 <= s } by A3; ::_thesis: verum
end;
assume x in { (Constants (OU0,s1)) where s1 is SortSymbol of S1 : s1 <= s } ; ::_thesis: x in { ((Constants OU0) . s1) where s1 is SortSymbol of S1 : s1 <= s }
then consider s1 being SortSymbol of S1 such that
A4: x = Constants (OU0,s1) and
A5: s1 <= s ;
x = (Constants OU0) . s1 by A4, MSUALG_2:def_4;
hence x in { ((Constants OU0) . s1) where s1 is SortSymbol of S1 : s1 <= s } by A5; ::_thesis: verum
end;
then A6: { ((Constants OU0) . s1) where s1 is SortSymbol of S1 : s1 <= s } = { (Constants (OU0,s1)) where s1 is SortSymbol of S1 : s1 <= s } by TARSKI:1;
(OSConstants OU0) . s = OSConstants (OU0,s) by Def5
.= (OSCl (Constants OU0)) . s by A6, Def4 ;
hence (OSConstants OU0) . i = (OSCl (Constants OU0)) . i ; ::_thesis: verum
end;
then for i being set st i in the carrier of S1 holds
(OSCl (Constants OU0)) . i c= (OSConstants OU0) . i ;
then A7: OSCl (Constants OU0) c= OSConstants OU0 by PBOOLE:def_2;
for i being set st i in the carrier of S1 holds
(OSConstants OU0) . i c= (OSCl (Constants OU0)) . i by A1;
then OSConstants OU0 c= OSCl (Constants OU0) by PBOOLE:def_2;
hence OSConstants OU0 = OSCl (Constants OU0) by A7, PBOOLE:146; ::_thesis: verum
end;
theorem Th13: :: OSALG_2:13
for S1 being OrderSortedSign
for OU0 being OSAlgebra of S1
for OU1 being OSSubAlgebra of OU0 holds OSConstants OU0 is OSSubset of OU1
proof
let S1 be OrderSortedSign; ::_thesis: for OU0 being OSAlgebra of S1
for OU1 being OSSubAlgebra of OU0 holds OSConstants OU0 is OSSubset of OU1
let OU0 be OSAlgebra of S1; ::_thesis: for OU1 being OSSubAlgebra of OU0 holds OSConstants OU0 is OSSubset of OU1
let OU1 be OSSubAlgebra of OU0; ::_thesis: OSConstants OU0 is OSSubset of OU1
OSConstants OU0 c= the Sorts of OU1
proof
let i be set ; :: according to PBOOLE:def_2 ::_thesis: ( not i in the carrier of S1 or (OSConstants OU0) . i c= the Sorts of OU1 . i )
assume i in the carrier of S1 ; ::_thesis: (OSConstants OU0) . i c= the Sorts of OU1 . i
then reconsider s = i as SortSymbol of S1 ;
Constants OU0 is MSSubset of OU1 by MSUALG_2:10;
then A1: Constants OU0 c= the Sorts of OU1 by PBOOLE:def_18;
A2: for s2, s3 being SortSymbol of S1 st s2 <= s3 holds
(Constants OU0) . s2 c= the Sorts of OU1 . s3
proof
let s2, s3 be SortSymbol of S1; ::_thesis: ( s2 <= s3 implies (Constants OU0) . s2 c= the Sorts of OU1 . s3 )
assume s2 <= s3 ; ::_thesis: (Constants OU0) . s2 c= the Sorts of OU1 . s3
then A3: the Sorts of OU1 . s2 c= the Sorts of OU1 . s3 by OSALG_1:def_17;
(Constants OU0) . s2 c= the Sorts of OU1 . s2 by A1, PBOOLE:def_2;
hence (Constants OU0) . s2 c= the Sorts of OU1 . s3 by A3, XBOOLE_1:1; ::_thesis: verum
end;
A4: for X being set st X in { (Constants (OU0,s1)) where s1 is SortSymbol of S1 : s1 <= s } holds
X c= the Sorts of OU1 . s
proof
let X be set ; ::_thesis: ( X in { (Constants (OU0,s1)) where s1 is SortSymbol of S1 : s1 <= s } implies X c= the Sorts of OU1 . s )
assume X in { (Constants (OU0,s1)) where s1 is SortSymbol of S1 : s1 <= s } ; ::_thesis: X c= the Sorts of OU1 . s
then consider s4 being SortSymbol of S1 such that
A5: ( X = Constants (OU0,s4) & s4 <= s ) ;
Constants (OU0,s4) = (Constants OU0) . s4 by MSUALG_2:def_4;
hence X c= the Sorts of OU1 . s by A2, A5; ::_thesis: verum
end;
(OSConstants OU0) . i = OSConstants (OU0,s) by Def5
.= union { (Constants (OU0,s1)) where s1 is SortSymbol of S1 : s1 <= s } ;
hence (OSConstants OU0) . i c= the Sorts of OU1 . i by A4, ZFMISC_1:76; ::_thesis: verum
end;
then A6: OSConstants OU0 is ManySortedSubset of the Sorts of OU1 by PBOOLE:def_18;
OSConstants OU0 is OrderSortedSet of S1 by Def2;
hence OSConstants OU0 is OSSubset of OU1 by A6, Def2; ::_thesis: verum
end;
theorem :: OSALG_2:14
for S being all-with_const_op OrderSortedSign
for OU0 being non-empty OSAlgebra of S
for OU1 being non-empty OSSubAlgebra of OU0 holds OSConstants OU0 is V8() OSSubset of OU1
proof
let S be all-with_const_op OrderSortedSign; ::_thesis: for OU0 being non-empty OSAlgebra of S
for OU1 being non-empty OSSubAlgebra of OU0 holds OSConstants OU0 is V8() OSSubset of OU1
let OU0 be non-empty OSAlgebra of S; ::_thesis: for OU1 being non-empty OSSubAlgebra of OU0 holds OSConstants OU0 is V8() OSSubset of OU1
let OU1 be non-empty OSSubAlgebra of OU0; ::_thesis: OSConstants OU0 is V8() OSSubset of OU1
Constants OU0 c= OSConstants OU0 by Th10;
hence OSConstants OU0 is V8() OSSubset of OU1 by Th13, PBOOLE:131; ::_thesis: verum
end;
begin
theorem Th15: :: OSALG_2:15
for I being set
for M being ManySortedSet of I
for x being set holds
( x is ManySortedSubset of M iff x in product (bool M) )
proof
let I be set ; ::_thesis: for M being ManySortedSet of I
for x being set holds
( x is ManySortedSubset of M iff x in product (bool M) )
let M be ManySortedSet of I; ::_thesis: for x being set holds
( x is ManySortedSubset of M iff x in product (bool M) )
let x be set ; ::_thesis: ( x is ManySortedSubset of M iff x in product (bool M) )
A1: I = dom (bool M) by PARTFUN1:def_2;
hereby ::_thesis: ( x in product (bool M) implies x is ManySortedSubset of M )
assume x is ManySortedSubset of M ; ::_thesis: x in product (bool M)
then reconsider x1 = x as ManySortedSubset of M ;
A2: for i being set st i in dom (bool M) holds
x1 . i in (bool M) . i
proof
let i be set ; ::_thesis: ( i in dom (bool M) implies x1 . i in (bool M) . i )
assume A3: i in dom (bool M) ; ::_thesis: x1 . i in (bool M) . i
x1 c= M by PBOOLE:def_18;
then x1 . i c= M . i by A1, A3, PBOOLE:def_2;
then x1 . i in bool (M . i) ;
hence x1 . i in (bool M) . i by A1, A3, MBOOLEAN:def_1; ::_thesis: verum
end;
dom x1 = I by PARTFUN1:def_2
.= dom (bool M) by PARTFUN1:def_2 ;
hence x in product (bool M) by A2, CARD_3:def_5; ::_thesis: verum
end;
assume x in product (bool M) ; ::_thesis: x is ManySortedSubset of M
then consider x1 being Function such that
A4: x = x1 and
A5: dom x1 = dom (bool M) and
A6: for i being set st i in dom (bool M) holds
x1 . i in (bool M) . i by CARD_3:def_5;
dom x1 = I by A5, PARTFUN1:def_2;
then reconsider x2 = x1 as ManySortedSet of I by PARTFUN1:def_2, RELAT_1:def_18;
x2 c= M
proof
let i be set ; :: according to PBOOLE:def_2 ::_thesis: ( not i in I or x2 . i c= M . i )
assume A7: i in I ; ::_thesis: x2 . i c= M . i
x2 . i in (bool M) . i by A1, A6, A7;
then x2 . i in bool (M . i) by A7, MBOOLEAN:def_1;
hence x2 . i c= M . i ; ::_thesis: verum
end;
hence x is ManySortedSubset of M by A4, PBOOLE:def_18; ::_thesis: verum
end;
definition
let R be non empty Poset;
let M be OrderSortedSet of R;
func OSbool M -> set means :: OSALG_2:def 6
for x being set holds
( x in it iff x is OrderSortedSubset of M );
existence
ex b1 being set st
for x being set holds
( x in b1 iff x is OrderSortedSubset of M )
proof
defpred S1[ set ] means $1 is OrderSortedSubset of M;
set f = product (bool M);
consider X being set such that
A1: for y being set holds
( y in X iff ( y in product (bool M) & S1[y] ) ) from XBOOLE_0:sch_1();
take X ; ::_thesis: for x being set holds
( x in X iff x is OrderSortedSubset of M )
let y be set ; ::_thesis: ( y in X iff y is OrderSortedSubset of M )
thus ( y in X implies y is OrderSortedSubset of M ) by A1; ::_thesis: ( y is OrderSortedSubset of M implies y in X )
assume A2: y is OrderSortedSubset of M ; ::_thesis: y in X
then y in product (bool M) by Th15;
hence y in X by A1, A2; ::_thesis: verum
end;
uniqueness
for b1, b2 being set st ( for x being set holds
( x in b1 iff x is OrderSortedSubset of M ) ) & ( for x being set holds
( x in b2 iff x is OrderSortedSubset of M ) ) holds
b1 = b2
proof
defpred S1[ set ] means $1 is OrderSortedSubset of M;
thus for X1, X2 being set st ( for x being set holds
( x in X1 iff S1[x] ) ) & ( for x being set holds
( x in X2 iff S1[x] ) ) holds
X1 = X2 from XBOOLE_0:sch_3(); ::_thesis: verum
end;
end;
:: deftheorem defines OSbool OSALG_2:def_6_:_
for R being non empty Poset
for M being OrderSortedSet of R
for b3 being set holds
( b3 = OSbool M iff for x being set holds
( x in b3 iff x is OrderSortedSubset of M ) );
definition
let S be OrderSortedSign;
let U0 be OSAlgebra of S;
let A be OSSubset of U0;
func OSSubSort A -> set equals :: OSALG_2:def 7
{ x where x is Element of SubSort A : x is OrderSortedSet of S } ;
correctness
coherence
{ x where x is Element of SubSort A : x is OrderSortedSet of S } is set ;
;
end;
:: deftheorem defines OSSubSort OSALG_2:def_7_:_
for S being OrderSortedSign
for U0 being OSAlgebra of S
for A being OSSubset of U0 holds OSSubSort A = { x where x is Element of SubSort A : x is OrderSortedSet of S } ;
theorem Th16: :: OSALG_2:16
for S1 being OrderSortedSign
for OU0 being OSAlgebra of S1
for A being OSSubset of OU0 holds OSSubSort A c= SubSort A
proof
let S1 be OrderSortedSign; ::_thesis: for OU0 being OSAlgebra of S1
for A being OSSubset of OU0 holds OSSubSort A c= SubSort A
let OU0 be OSAlgebra of S1; ::_thesis: for A being OSSubset of OU0 holds OSSubSort A c= SubSort A
let A be OSSubset of OU0; ::_thesis: OSSubSort A c= SubSort A
let x be set ; :: according to TARSKI:def_3 ::_thesis: ( not x in OSSubSort A or x in SubSort A )
assume x in OSSubSort A ; ::_thesis: x in SubSort A
then ex y being Element of SubSort A st
( x = y & y is OrderSortedSet of S1 ) ;
hence x in SubSort A ; ::_thesis: verum
end;
theorem Th17: :: OSALG_2:17
for S1 being OrderSortedSign
for OU0 being OSAlgebra of S1
for A being OSSubset of OU0 holds the Sorts of OU0 in OSSubSort A
proof
let S1 be OrderSortedSign; ::_thesis: for OU0 being OSAlgebra of S1
for A being OSSubset of OU0 holds the Sorts of OU0 in OSSubSort A
let OU0 be OSAlgebra of S1; ::_thesis: for A being OSSubset of OU0 holds the Sorts of OU0 in OSSubSort A
let A be OSSubset of OU0; ::_thesis: the Sorts of OU0 in OSSubSort A
reconsider X = the Sorts of OU0 as Element of SubSort A by MSUALG_2:38;
the Sorts of OU0 is OrderSortedSet of S1 by OSALG_1:17;
then X in { x where x is Element of SubSort A : x is OrderSortedSet of S1 } ;
hence the Sorts of OU0 in OSSubSort A ; ::_thesis: verum
end;
registration
let S1 be OrderSortedSign;
let OU0 be OSAlgebra of S1;
let A be OSSubset of OU0;
cluster OSSubSort A -> non empty ;
coherence
not OSSubSort A is empty by Th17;
end;
definition
let S1 be OrderSortedSign;
let OU0 be OSAlgebra of S1;
func OSSubSort OU0 -> set equals :: OSALG_2:def 8
{ x where x is Element of SubSort OU0 : x is OrderSortedSet of S1 } ;
correctness
coherence
{ x where x is Element of SubSort OU0 : x is OrderSortedSet of S1 } is set ;
;
end;
:: deftheorem defines OSSubSort OSALG_2:def_8_:_
for S1 being OrderSortedSign
for OU0 being OSAlgebra of S1 holds OSSubSort OU0 = { x where x is Element of SubSort OU0 : x is OrderSortedSet of S1 } ;
theorem Th18: :: OSALG_2:18
for S1 being OrderSortedSign
for OU0 being OSAlgebra of S1
for A being OSSubset of OU0 holds OSSubSort A c= OSSubSort OU0
proof
let S1 be OrderSortedSign; ::_thesis: for OU0 being OSAlgebra of S1
for A being OSSubset of OU0 holds OSSubSort A c= OSSubSort OU0
let OU0 be OSAlgebra of S1; ::_thesis: for A being OSSubset of OU0 holds OSSubSort A c= OSSubSort OU0
let A be OSSubset of OU0; ::_thesis: OSSubSort A c= OSSubSort OU0
let x be set ; :: according to TARSKI:def_3 ::_thesis: ( not x in OSSubSort A or x in OSSubSort OU0 )
assume x in OSSubSort A ; ::_thesis: x in OSSubSort OU0
then consider x1 being Element of SubSort A such that
A1: x1 = x and
A2: x1 is OrderSortedSet of S1 ;
( x1 in SubSort A & SubSort A c= SubSort OU0 ) by MSUALG_2:39;
then reconsider x2 = x1 as Element of SubSort OU0 ;
x2 in { y where y is Element of SubSort OU0 : y is OrderSortedSet of S1 } by A2;
hence x in OSSubSort OU0 by A1; ::_thesis: verum
end;
registration
let S1 be OrderSortedSign;
let OU0 be OSAlgebra of S1;
cluster OSSubSort OU0 -> non empty ;
coherence
not OSSubSort OU0 is empty
proof
set A = the OSSubset of OU0;
OSSubSort the OSSubset of OU0 c= OSSubSort OU0 by Th18;
hence not OSSubSort OU0 is empty ; ::_thesis: verum
end;
end;
definition
let S1 be OrderSortedSign;
let OU0 be OSAlgebra of S1;
let e be Element of OSSubSort OU0;
func @ e -> OSSubset of OU0 equals :: OSALG_2:def 9
e;
coherence
e is OSSubset of OU0
proof
e in { x where x is Element of SubSort OU0 : x is OrderSortedSet of S1 } ;
then consider e1 being Element of SubSort OU0 such that
A1: e = e1 and
A2: e1 is OrderSortedSet of S1 ;
reconsider e2 = @ e1 as OSSubset of OU0 by A2, Def2;
e2 = e by A1;
hence e is OSSubset of OU0 ; ::_thesis: verum
end;
end;
:: deftheorem defines @ OSALG_2:def_9_:_
for S1 being OrderSortedSign
for OU0 being OSAlgebra of S1
for e being Element of OSSubSort OU0 holds @ e = e;
theorem Th19: :: OSALG_2:19
for S1 being OrderSortedSign
for OU0 being OSAlgebra of S1
for A, B being OSSubset of OU0 holds
( B in OSSubSort A iff ( B is opers_closed & OSConstants OU0 c= B & A c= B ) )
proof
let S1 be OrderSortedSign; ::_thesis: for OU0 being OSAlgebra of S1
for A, B being OSSubset of OU0 holds
( B in OSSubSort A iff ( B is opers_closed & OSConstants OU0 c= B & A c= B ) )
let OU0 be OSAlgebra of S1; ::_thesis: for A, B being OSSubset of OU0 holds
( B in OSSubSort A iff ( B is opers_closed & OSConstants OU0 c= B & A c= B ) )
let A, B be OSSubset of OU0; ::_thesis: ( B in OSSubSort A iff ( B is opers_closed & OSConstants OU0 c= B & A c= B ) )
thus ( B in OSSubSort A implies ( B is opers_closed & OSConstants OU0 c= B & A c= B ) ) ::_thesis: ( B is opers_closed & OSConstants OU0 c= B & A c= B implies B in OSSubSort A )
proof
assume B in OSSubSort A ; ::_thesis: ( B is opers_closed & OSConstants OU0 c= B & A c= B )
then A1: ex B1 being Element of SubSort A st
( B1 = B & B1 is OrderSortedSet of S1 ) ;
then Constants OU0 c= B by MSUALG_2:13;
hence ( B is opers_closed & OSConstants OU0 c= B & A c= B ) by A1, Th11, MSUALG_2:13; ::_thesis: verum
end;
assume that
A2: B is opers_closed and
A3: OSConstants OU0 c= B and
A4: A c= B ; ::_thesis: B in OSSubSort A
Constants OU0 c= OSConstants OU0 by Th10;
then Constants OU0 c= B by A3, PBOOLE:13;
then A5: B in SubSort A by A2, A4, MSUALG_2:13;
B is OrderSortedSet of S1 by Def2;
hence B in OSSubSort A by A5; ::_thesis: verum
end;
theorem Th20: :: OSALG_2:20
for S1 being OrderSortedSign
for OU0 being OSAlgebra of S1
for B being OSSubset of OU0 holds
( B in OSSubSort OU0 iff B is opers_closed )
proof
let S1 be OrderSortedSign; ::_thesis: for OU0 being OSAlgebra of S1
for B being OSSubset of OU0 holds
( B in OSSubSort OU0 iff B is opers_closed )
let OU0 be OSAlgebra of S1; ::_thesis: for B being OSSubset of OU0 holds
( B in OSSubSort OU0 iff B is opers_closed )
let B be OSSubset of OU0; ::_thesis: ( B in OSSubSort OU0 iff B is opers_closed )
A1: ( B in SubSort OU0 iff B is opers_closed ) by MSUALG_2:14;
thus ( B in OSSubSort OU0 implies B is opers_closed ) ::_thesis: ( B is opers_closed implies B in OSSubSort OU0 )
proof
assume B in OSSubSort OU0 ; ::_thesis: B is opers_closed
then ex B1 being Element of SubSort OU0 st
( B1 = B & B1 is OrderSortedSet of S1 ) ;
hence B is opers_closed by MSUALG_2:14; ::_thesis: verum
end;
assume A2: B is opers_closed ; ::_thesis: B in OSSubSort OU0
B is OrderSortedSet of S1 by Def2;
hence B in OSSubSort OU0 by A1, A2; ::_thesis: verum
end;
definition
let S1 be OrderSortedSign;
let OU0 be OSAlgebra of S1;
let A be OSSubset of OU0;
let s be Element of S1;
func OSSubSort (A,s) -> set means :Def10: :: OSALG_2:def 10
for x being set holds
( x in it iff ex B being OSSubset of OU0 st
( B in OSSubSort A & x = B . s ) );
existence
ex b1 being set st
for x being set holds
( x in b1 iff ex B being OSSubset of OU0 st
( B in OSSubSort A & x = B . s ) )
proof
defpred S1[ set ] means ex B being OSSubset of OU0 st
( B in OSSubSort A & $1 = B . s );
set C = bool (Union the Sorts of OU0);
consider X being set such that
A1: for x being set holds
( x in X iff ( x in bool (Union the Sorts of OU0) & S1[x] ) ) from XBOOLE_0:sch_1();
take X ; ::_thesis: for x being set holds
( x in X iff ex B being OSSubset of OU0 st
( B in OSSubSort A & x = B . s ) )
A2: bool (Union the Sorts of OU0) = bool (union (rng the Sorts of OU0)) by CARD_3:def_4;
for x being set holds
( x in X iff ex B being OSSubset of OU0 st
( B in OSSubSort A & x = B . s ) )
proof
dom the Sorts of OU0 = the carrier of S1 by PARTFUN1:def_2;
then the Sorts of OU0 . s in rng the Sorts of OU0 by FUNCT_1:def_3;
then A3: the Sorts of OU0 . s c= union (rng the Sorts of OU0) by ZFMISC_1:74;
let x be set ; ::_thesis: ( x in X iff ex B being OSSubset of OU0 st
( B in OSSubSort A & x = B . s ) )
thus ( x in X implies ex B being OSSubset of OU0 st
( B in OSSubSort A & x = B . s ) ) by A1; ::_thesis: ( ex B being OSSubset of OU0 st
( B in OSSubSort A & x = B . s ) implies x in X )
given B being OSSubset of OU0 such that A4: B in OSSubSort A and
A5: x = B . s ; ::_thesis: x in X
B c= the Sorts of OU0 by PBOOLE:def_18;
then B . s c= the Sorts of OU0 . s by PBOOLE:def_2;
then x c= union (rng the Sorts of OU0) by A5, A3, XBOOLE_1:1;
hence x in X by A2, A1, A4, A5; ::_thesis: verum
end;
hence for x being set holds
( x in X iff ex B being OSSubset of OU0 st
( B in OSSubSort A & x = B . s ) ) ; ::_thesis: verum
end;
uniqueness
for b1, b2 being set st ( for x being set holds
( x in b1 iff ex B being OSSubset of OU0 st
( B in OSSubSort A & x = B . s ) ) ) & ( for x being set holds
( x in b2 iff ex B being OSSubset of OU0 st
( B in OSSubSort A & x = B . s ) ) ) holds
b1 = b2
proof
defpred S1[ set ] means ex B being OSSubset of OU0 st
( B in OSSubSort A & $1 = B . s );
thus for X1, X2 being set st ( for x being set holds
( x in X1 iff S1[x] ) ) & ( for x being set holds
( x in X2 iff S1[x] ) ) holds
X1 = X2 from XBOOLE_0:sch_3(); ::_thesis: verum
end;
end;
:: deftheorem Def10 defines OSSubSort OSALG_2:def_10_:_
for S1 being OrderSortedSign
for OU0 being OSAlgebra of S1
for A being OSSubset of OU0
for s being Element of S1
for b5 being set holds
( b5 = OSSubSort (A,s) iff for x being set holds
( x in b5 iff ex B being OSSubset of OU0 st
( B in OSSubSort A & x = B . s ) ) );
theorem Th21: :: OSALG_2:21
for S1 being OrderSortedSign
for OU0 being OSAlgebra of S1
for A being OSSubset of OU0
for s1, s2 being SortSymbol of S1 st s1 <= s2 holds
OSSubSort (A,s2) is_coarser_than OSSubSort (A,s1)
proof
let S1 be OrderSortedSign; ::_thesis: for OU0 being OSAlgebra of S1
for A being OSSubset of OU0
for s1, s2 being SortSymbol of S1 st s1 <= s2 holds
OSSubSort (A,s2) is_coarser_than OSSubSort (A,s1)
let OU0 be OSAlgebra of S1; ::_thesis: for A being OSSubset of OU0
for s1, s2 being SortSymbol of S1 st s1 <= s2 holds
OSSubSort (A,s2) is_coarser_than OSSubSort (A,s1)
let A be OSSubset of OU0; ::_thesis: for s1, s2 being SortSymbol of S1 st s1 <= s2 holds
OSSubSort (A,s2) is_coarser_than OSSubSort (A,s1)
let s1, s2 be SortSymbol of S1; ::_thesis: ( s1 <= s2 implies OSSubSort (A,s2) is_coarser_than OSSubSort (A,s1) )
assume A1: s1 <= s2 ; ::_thesis: OSSubSort (A,s2) is_coarser_than OSSubSort (A,s1)
for Y being set st Y in OSSubSort (A,s2) holds
ex X being set st
( X in OSSubSort (A,s1) & X c= Y )
proof
let x be set ; ::_thesis: ( x in OSSubSort (A,s2) implies ex X being set st
( X in OSSubSort (A,s1) & X c= x ) )
assume x in OSSubSort (A,s2) ; ::_thesis: ex X being set st
( X in OSSubSort (A,s1) & X c= x )
then consider B being OSSubset of OU0 such that
A2: ( B in OSSubSort A & x = B . s2 ) by Def10;
take B . s1 ; ::_thesis: ( B . s1 in OSSubSort (A,s1) & B . s1 c= x )
B is OrderSortedSet of S1 by Def2;
hence ( B . s1 in OSSubSort (A,s1) & B . s1 c= x ) by A1, A2, Def10, OSALG_1:def_16; ::_thesis: verum
end;
hence OSSubSort (A,s2) is_coarser_than OSSubSort (A,s1) by SETFAM_1:def_3; ::_thesis: verum
end;
theorem Th22: :: OSALG_2:22
for S1 being OrderSortedSign
for OU0 being OSAlgebra of S1
for A being OSSubset of OU0
for s being SortSymbol of S1 holds OSSubSort (A,s) c= SubSort (A,s)
proof
let S1 be OrderSortedSign; ::_thesis: for OU0 being OSAlgebra of S1
for A being OSSubset of OU0
for s being SortSymbol of S1 holds OSSubSort (A,s) c= SubSort (A,s)
let OU0 be OSAlgebra of S1; ::_thesis: for A being OSSubset of OU0
for s being SortSymbol of S1 holds OSSubSort (A,s) c= SubSort (A,s)
let A be OSSubset of OU0; ::_thesis: for s being SortSymbol of S1 holds OSSubSort (A,s) c= SubSort (A,s)
let s be SortSymbol of S1; ::_thesis: OSSubSort (A,s) c= SubSort (A,s)
let x be set ; :: according to TARSKI:def_3 ::_thesis: ( not x in OSSubSort (A,s) or x in SubSort (A,s) )
assume x in OSSubSort (A,s) ; ::_thesis: x in SubSort (A,s)
then A1: ex B being OSSubset of OU0 st
( B in OSSubSort A & x = B . s ) by Def10;
OSSubSort A c= SubSort A by Th16;
hence x in SubSort (A,s) by A1, MSUALG_2:def_13; ::_thesis: verum
end;
theorem Th23: :: OSALG_2:23
for S1 being OrderSortedSign
for OU0 being OSAlgebra of S1
for A being OSSubset of OU0
for s being SortSymbol of S1 holds the Sorts of OU0 . s in OSSubSort (A,s)
proof
let S1 be OrderSortedSign; ::_thesis: for OU0 being OSAlgebra of S1
for A being OSSubset of OU0
for s being SortSymbol of S1 holds the Sorts of OU0 . s in OSSubSort (A,s)
let OU0 be OSAlgebra of S1; ::_thesis: for A being OSSubset of OU0
for s being SortSymbol of S1 holds the Sorts of OU0 . s in OSSubSort (A,s)
let A be OSSubset of OU0; ::_thesis: for s being SortSymbol of S1 holds the Sorts of OU0 . s in OSSubSort (A,s)
let s be SortSymbol of S1; ::_thesis: the Sorts of OU0 . s in OSSubSort (A,s)
( the Sorts of OU0 is ManySortedSubset of the Sorts of OU0 & the Sorts of OU0 is OrderSortedSet of S1 ) by OSALG_1:17, PBOOLE:def_18;
then reconsider B = the Sorts of OU0 as OSSubset of OU0 by Def2;
the Sorts of OU0 in OSSubSort A by Th17;
then B . s in OSSubSort (A,s) by Def10;
hence the Sorts of OU0 . s in OSSubSort (A,s) ; ::_thesis: verum
end;
registration
let S1 be OrderSortedSign;
let OU0 be OSAlgebra of S1;
let A be OSSubset of OU0;
let s be SortSymbol of S1;
cluster OSSubSort (A,s) -> non empty ;
coherence
not OSSubSort (A,s) is empty by Th23;
end;
definition
let S1 be OrderSortedSign;
let OU0 be OSAlgebra of S1;
let A be OSSubset of OU0;
func OSMSubSort A -> OSSubset of OU0 means :Def11: :: OSALG_2:def 11
for s being SortSymbol of S1 holds it . s = meet (OSSubSort (A,s));
existence
ex b1 being OSSubset of OU0 st
for s being SortSymbol of S1 holds b1 . s = meet (OSSubSort (A,s))
proof
deffunc H1( Element of S1) -> set = meet (OSSubSort (A,$1));
consider f being Function such that
A1: ( dom f = the carrier of S1 & ( for s being Element of S1 holds f . s = H1(s) ) ) from FUNCT_1:sch_4();
reconsider f = f as ManySortedSet of the carrier of S1 by A1, PARTFUN1:def_2, RELAT_1:def_18;
f c= the Sorts of OU0
proof
reconsider u0 = the Sorts of OU0 as MSSubset of OU0 by PBOOLE:def_18;
let x be set ; :: according to PBOOLE:def_2 ::_thesis: ( not x in the carrier of S1 or f . x c= the Sorts of OU0 . x )
assume x in the carrier of S1 ; ::_thesis: f . x c= the Sorts of OU0 . x
then reconsider s = x as SortSymbol of S1 ;
A2: f . s = meet (OSSubSort (A,s)) by A1;
u0 is OrderSortedSet of S1 by OSALG_1:17;
then A3: u0 is OSSubset of OU0 by Def2;
u0 in OSSubSort A by Th17;
then the Sorts of OU0 . s in OSSubSort (A,s) by A3, Def10;
hence f . x c= the Sorts of OU0 . x by A2, SETFAM_1:3; ::_thesis: verum
end;
then reconsider f = f as MSSubset of OU0 by PBOOLE:def_18;
take f ; ::_thesis: ( f is OSSubset of OU0 & ( for s being SortSymbol of S1 holds f . s = meet (OSSubSort (A,s)) ) )
reconsider f1 = f as ManySortedSet of S1 ;
for s1, s2 being Element of S1 st s1 <= s2 holds
f1 . s1 c= f1 . s2
proof
let s1, s2 be Element of S1; ::_thesis: ( s1 <= s2 implies f1 . s1 c= f1 . s2 )
assume s1 <= s2 ; ::_thesis: f1 . s1 c= f1 . s2
then A4: meet (OSSubSort (A,s1)) c= meet (OSSubSort (A,s2)) by Th21, SETFAM_1:14;
f1 . s1 = meet (OSSubSort (A,s1)) by A1;
hence f1 . s1 c= f1 . s2 by A1, A4; ::_thesis: verum
end;
then f is OrderSortedSet of S1 by OSALG_1:def_16;
hence ( f is OSSubset of OU0 & ( for s being SortSymbol of S1 holds f . s = meet (OSSubSort (A,s)) ) ) by A1, Def2; ::_thesis: verum
end;
uniqueness
for b1, b2 being OSSubset of OU0 st ( for s being SortSymbol of S1 holds b1 . s = meet (OSSubSort (A,s)) ) & ( for s being SortSymbol of S1 holds b2 . s = meet (OSSubSort (A,s)) ) holds
b1 = b2
proof
let W1, W2 be OSSubset of OU0; ::_thesis: ( ( for s being SortSymbol of S1 holds W1 . s = meet (OSSubSort (A,s)) ) & ( for s being SortSymbol of S1 holds W2 . s = meet (OSSubSort (A,s)) ) implies W1 = W2 )
assume that
A5: for s being SortSymbol of S1 holds W1 . s = meet (OSSubSort (A,s)) and
A6: for s being SortSymbol of S1 holds W2 . s = meet (OSSubSort (A,s)) ; ::_thesis: W1 = W2
for s being set st s in the carrier of S1 holds
W1 . s = W2 . s
proof
let s be set ; ::_thesis: ( s in the carrier of S1 implies W1 . s = W2 . s )
assume s in the carrier of S1 ; ::_thesis: W1 . s = W2 . s
then reconsider s = s as SortSymbol of S1 ;
W1 . s = meet (OSSubSort (A,s)) by A5;
hence W1 . s = W2 . s by A6; ::_thesis: verum
end;
hence W1 = W2 by PBOOLE:3; ::_thesis: verum
end;
end;
:: deftheorem Def11 defines OSMSubSort OSALG_2:def_11_:_
for S1 being OrderSortedSign
for OU0 being OSAlgebra of S1
for A, b4 being OSSubset of OU0 holds
( b4 = OSMSubSort A iff for s being SortSymbol of S1 holds b4 . s = meet (OSSubSort (A,s)) );
registration
let S1 be OrderSortedSign;
let OU0 be OSAlgebra of S1;
cluster non empty Relation-like the carrier of S1 -defined Function-like V17( the carrier of S1) opers_closed for OSSubset of OU0;
existence
ex b1 being OSSubset of OU0 st b1 is opers_closed
proof
set x = the Element of OSSubSort OU0;
the Element of OSSubSort OU0 in { y where y is Element of SubSort OU0 : y is OrderSortedSet of S1 } ;
then consider x1 being Element of SubSort OU0 such that
the Element of OSSubSort OU0 = x1 and
A1: x1 is OrderSortedSet of S1 ;
reconsider x2 = x1 as MSSubset of OU0 by MSUALG_2:def_11;
reconsider x3 = x2 as OSSubset of OU0 by A1, Def2;
take x3 ; ::_thesis: x3 is opers_closed
thus x3 is opers_closed by MSUALG_2:def_11; ::_thesis: verum
end;
end;
theorem Th24: :: OSALG_2:24
for S1 being OrderSortedSign
for OU0 being OSAlgebra of S1
for A being OSSubset of OU0 holds (OSConstants OU0) \/ A c= OSMSubSort A
proof
let S1 be OrderSortedSign; ::_thesis: for OU0 being OSAlgebra of S1
for A being OSSubset of OU0 holds (OSConstants OU0) \/ A c= OSMSubSort A
let OU0 be OSAlgebra of S1; ::_thesis: for A being OSSubset of OU0 holds (OSConstants OU0) \/ A c= OSMSubSort A
let A be OSSubset of OU0; ::_thesis: (OSConstants OU0) \/ A c= OSMSubSort A
let i be set ; :: according to PBOOLE:def_2 ::_thesis: ( not i in the carrier of S1 or ((OSConstants OU0) \/ A) . i c= (OSMSubSort A) . i )
assume i in the carrier of S1 ; ::_thesis: ((OSConstants OU0) \/ A) . i c= (OSMSubSort A) . i
then reconsider s = i as SortSymbol of S1 ;
A1: for Z being set st Z in OSSubSort (A,s) holds
((OSConstants OU0) \/ A) . s c= Z
proof
let Z be set ; ::_thesis: ( Z in OSSubSort (A,s) implies ((OSConstants OU0) \/ A) . s c= Z )
assume Z in OSSubSort (A,s) ; ::_thesis: ((OSConstants OU0) \/ A) . s c= Z
then consider B being OSSubset of OU0 such that
A2: B in OSSubSort A and
A3: Z = B . s by Def10;
( OSConstants OU0 c= B & A c= B ) by A2, Th19;
then (OSConstants OU0) \/ A c= B by PBOOLE:16;
hence ((OSConstants OU0) \/ A) . s c= Z by A3, PBOOLE:def_2; ::_thesis: verum
end;
(OSMSubSort A) . s = meet (OSSubSort (A,s)) by Def11;
hence ((OSConstants OU0) \/ A) . i c= (OSMSubSort A) . i by A1, SETFAM_1:5; ::_thesis: verum
end;
theorem :: OSALG_2:25
for S1 being OrderSortedSign
for OU0 being OSAlgebra of S1
for A being OSSubset of OU0 st (OSConstants OU0) \/ A is V8() holds
OSMSubSort A is V8()
proof
let S1 be OrderSortedSign; ::_thesis: for OU0 being OSAlgebra of S1
for A being OSSubset of OU0 st (OSConstants OU0) \/ A is V8() holds
OSMSubSort A is V8()
let OU0 be OSAlgebra of S1; ::_thesis: for A being OSSubset of OU0 st (OSConstants OU0) \/ A is V8() holds
OSMSubSort A is V8()
let A be OSSubset of OU0; ::_thesis: ( (OSConstants OU0) \/ A is V8() implies OSMSubSort A is V8() )
assume A1: (OSConstants OU0) \/ A is V8() ; ::_thesis: OSMSubSort A is V8()
now__::_thesis:_for_i_being_set_st_i_in_the_carrier_of_S1_holds_
not_(OSMSubSort_A)_._i_is_empty
let i be set ; ::_thesis: ( i in the carrier of S1 implies not (OSMSubSort A) . i is empty )
assume i in the carrier of S1 ; ::_thesis: not (OSMSubSort A) . i is empty
then reconsider s = i as SortSymbol of S1 ;
for Z being set st Z in OSSubSort (A,s) holds
((OSConstants OU0) \/ A) . s c= Z
proof
let Z be set ; ::_thesis: ( Z in OSSubSort (A,s) implies ((OSConstants OU0) \/ A) . s c= Z )
assume Z in OSSubSort (A,s) ; ::_thesis: ((OSConstants OU0) \/ A) . s c= Z
then consider B being OSSubset of OU0 such that
A2: B in OSSubSort A and
A3: Z = B . s by Def10;
( OSConstants OU0 c= B & A c= B ) by A2, Th19;
then (OSConstants OU0) \/ A c= B by PBOOLE:16;
hence ((OSConstants OU0) \/ A) . s c= Z by A3, PBOOLE:def_2; ::_thesis: verum
end;
then A4: ((OSConstants OU0) \/ A) . s c= meet (OSSubSort (A,s)) by SETFAM_1:5;
ex x being set st x in ((OSConstants OU0) \/ A) . s by A1, XBOOLE_0:def_1;
hence not (OSMSubSort A) . i is empty by A4, Def11; ::_thesis: verum
end;
hence OSMSubSort A is V8() by PBOOLE:def_13; ::_thesis: verum
end;
theorem Th26: :: OSALG_2:26
for S1 being OrderSortedSign
for OU0 being OSAlgebra of S1
for o being OperSymbol of S1
for A, B being OSSubset of OU0 st B in OSSubSort A holds
(((OSMSubSort A) #) * the Arity of S1) . o c= ((B #) * the Arity of S1) . o
proof
let S1 be OrderSortedSign; ::_thesis: for OU0 being OSAlgebra of S1
for o being OperSymbol of S1
for A, B being OSSubset of OU0 st B in OSSubSort A holds
(((OSMSubSort A) #) * the Arity of S1) . o c= ((B #) * the Arity of S1) . o
let OU0 be OSAlgebra of S1; ::_thesis: for o being OperSymbol of S1
for A, B being OSSubset of OU0 st B in OSSubSort A holds
(((OSMSubSort A) #) * the Arity of S1) . o c= ((B #) * the Arity of S1) . o
let o be OperSymbol of S1; ::_thesis: for A, B being OSSubset of OU0 st B in OSSubSort A holds
(((OSMSubSort A) #) * the Arity of S1) . o c= ((B #) * the Arity of S1) . o
let A, B be OSSubset of OU0; ::_thesis: ( B in OSSubSort A implies (((OSMSubSort A) #) * the Arity of S1) . o c= ((B #) * the Arity of S1) . o )
assume A1: B in OSSubSort A ; ::_thesis: (((OSMSubSort A) #) * the Arity of S1) . o c= ((B #) * the Arity of S1) . o
OSMSubSort A c= B
proof
let i be set ; :: according to PBOOLE:def_2 ::_thesis: ( not i in the carrier of S1 or (OSMSubSort A) . i c= B . i )
assume i in the carrier of S1 ; ::_thesis: (OSMSubSort A) . i c= B . i
then reconsider s = i as SortSymbol of S1 ;
( (OSMSubSort A) . s = meet (OSSubSort (A,s)) & B . s in OSSubSort (A,s) ) by A1, Def10, Def11;
hence (OSMSubSort A) . i c= B . i by SETFAM_1:3; ::_thesis: verum
end;
hence (((OSMSubSort A) #) * the Arity of S1) . o c= ((B #) * the Arity of S1) . o by MSUALG_2:2; ::_thesis: verum
end;
theorem Th27: :: OSALG_2:27
for S1 being OrderSortedSign
for OU0 being OSAlgebra of S1
for o being OperSymbol of S1
for A, B being OSSubset of OU0 st B in OSSubSort A holds
rng ((Den (o,OU0)) | ((((OSMSubSort A) #) * the Arity of S1) . o)) c= (B * the ResultSort of S1) . o
proof
let S1 be OrderSortedSign; ::_thesis: for OU0 being OSAlgebra of S1
for o being OperSymbol of S1
for A, B being OSSubset of OU0 st B in OSSubSort A holds
rng ((Den (o,OU0)) | ((((OSMSubSort A) #) * the Arity of S1) . o)) c= (B * the ResultSort of S1) . o
let OU0 be OSAlgebra of S1; ::_thesis: for o being OperSymbol of S1
for A, B being OSSubset of OU0 st B in OSSubSort A holds
rng ((Den (o,OU0)) | ((((OSMSubSort A) #) * the Arity of S1) . o)) c= (B * the ResultSort of S1) . o
let o be OperSymbol of S1; ::_thesis: for A, B being OSSubset of OU0 st B in OSSubSort A holds
rng ((Den (o,OU0)) | ((((OSMSubSort A) #) * the Arity of S1) . o)) c= (B * the ResultSort of S1) . o
let A, B be OSSubset of OU0; ::_thesis: ( B in OSSubSort A implies rng ((Den (o,OU0)) | ((((OSMSubSort A) #) * the Arity of S1) . o)) c= (B * the ResultSort of S1) . o )
set m = (((OSMSubSort A) #) * the Arity of S1) . o;
set b = ((B #) * the Arity of S1) . o;
set d = Den (o,OU0);
assume A1: B in OSSubSort A ; ::_thesis: rng ((Den (o,OU0)) | ((((OSMSubSort A) #) * the Arity of S1) . o)) c= (B * the ResultSort of S1) . o
then B is opers_closed by Th19;
then B is_closed_on o by MSUALG_2:def_6;
then A2: rng ((Den (o,OU0)) | (((B #) * the Arity of S1) . o)) c= (B * the ResultSort of S1) . o by MSUALG_2:def_5;
(((B #) * the Arity of S1) . o) /\ ((((OSMSubSort A) #) * the Arity of S1) . o) = (((OSMSubSort A) #) * the Arity of S1) . o by A1, Th26, XBOOLE_1:28;
then (Den (o,OU0)) | ((((OSMSubSort A) #) * the Arity of S1) . o) = ((Den (o,OU0)) | (((B #) * the Arity of S1) . o)) | ((((OSMSubSort A) #) * the Arity of S1) . o) by RELAT_1:71;
then rng ((Den (o,OU0)) | ((((OSMSubSort A) #) * the Arity of S1) . o)) c= rng ((Den (o,OU0)) | (((B #) * the Arity of S1) . o)) by RELAT_1:70;
hence rng ((Den (o,OU0)) | ((((OSMSubSort A) #) * the Arity of S1) . o)) c= (B * the ResultSort of S1) . o by A2, XBOOLE_1:1; ::_thesis: verum
end;
theorem Th28: :: OSALG_2:28
for S1 being OrderSortedSign
for OU0 being OSAlgebra of S1
for o being OperSymbol of S1
for A being OSSubset of OU0 holds rng ((Den (o,OU0)) | ((((OSMSubSort A) #) * the Arity of S1) . o)) c= ((OSMSubSort A) * the ResultSort of S1) . o
proof
let S1 be OrderSortedSign; ::_thesis: for OU0 being OSAlgebra of S1
for o being OperSymbol of S1
for A being OSSubset of OU0 holds rng ((Den (o,OU0)) | ((((OSMSubSort A) #) * the Arity of S1) . o)) c= ((OSMSubSort A) * the ResultSort of S1) . o
let OU0 be OSAlgebra of S1; ::_thesis: for o being OperSymbol of S1
for A being OSSubset of OU0 holds rng ((Den (o,OU0)) | ((((OSMSubSort A) #) * the Arity of S1) . o)) c= ((OSMSubSort A) * the ResultSort of S1) . o
let o be OperSymbol of S1; ::_thesis: for A being OSSubset of OU0 holds rng ((Den (o,OU0)) | ((((OSMSubSort A) #) * the Arity of S1) . o)) c= ((OSMSubSort A) * the ResultSort of S1) . o
let A be OSSubset of OU0; ::_thesis: rng ((Den (o,OU0)) | ((((OSMSubSort A) #) * the Arity of S1) . o)) c= ((OSMSubSort A) * the ResultSort of S1) . o
let x be set ; :: according to TARSKI:def_3 ::_thesis: ( not x in rng ((Den (o,OU0)) | ((((OSMSubSort A) #) * the Arity of S1) . o)) or x in ((OSMSubSort A) * the ResultSort of S1) . o )
assume that
A1: x in rng ((Den (o,OU0)) | ((((OSMSubSort A) #) * the Arity of S1) . o)) and
A2: not x in ((OSMSubSort A) * the ResultSort of S1) . o ; ::_thesis: contradiction
set r = the_result_sort_of o;
A3: ( the_result_sort_of o = the ResultSort of S1 . o & dom the ResultSort of S1 = the carrier' of S1 ) by FUNCT_2:def_1, MSUALG_1:def_2;
then ((OSMSubSort A) * the ResultSort of S1) . o = (OSMSubSort A) . (the_result_sort_of o) by FUNCT_1:13
.= meet (OSSubSort (A,(the_result_sort_of o))) by Def11 ;
then consider X being set such that
A4: X in OSSubSort (A,(the_result_sort_of o)) and
A5: not x in X by A2, SETFAM_1:def_1;
consider B being OSSubset of OU0 such that
A6: B in OSSubSort A and
A7: B . (the_result_sort_of o) = X by A4, Def10;
rng ((Den (o,OU0)) | ((((OSMSubSort A) #) * the Arity of S1) . o)) c= (B * the ResultSort of S1) . o by A6, Th27;
then x in (B * the ResultSort of S1) . o by A1;
hence contradiction by A3, A5, A7, FUNCT_1:13; ::_thesis: verum
end;
theorem Th29: :: OSALG_2:29
for S1 being OrderSortedSign
for OU0 being OSAlgebra of S1
for A being OSSubset of OU0 holds
( OSMSubSort A is opers_closed & A c= OSMSubSort A )
proof
let S1 be OrderSortedSign; ::_thesis: for OU0 being OSAlgebra of S1
for A being OSSubset of OU0 holds
( OSMSubSort A is opers_closed & A c= OSMSubSort A )
let OU0 be OSAlgebra of S1; ::_thesis: for A being OSSubset of OU0 holds
( OSMSubSort A is opers_closed & A c= OSMSubSort A )
let A be OSSubset of OU0; ::_thesis: ( OSMSubSort A is opers_closed & A c= OSMSubSort A )
thus OSMSubSort A is opers_closed ::_thesis: A c= OSMSubSort A
proof
let o1 be Element of the carrier' of S1; :: according to MSUALG_2:def_6 ::_thesis: OSMSubSort A is_closed_on o1
reconsider o = o1 as OperSymbol of S1 ;
rng ((Den (o,OU0)) | ((((OSMSubSort A) #) * the Arity of S1) . o)) c= ((OSMSubSort A) * the ResultSort of S1) . o by Th28;
hence OSMSubSort A is_closed_on o1 by MSUALG_2:def_5; ::_thesis: verum
end;
( A c= (OSConstants OU0) \/ A & (OSConstants OU0) \/ A c= OSMSubSort A ) by Th24, PBOOLE:14;
hence A c= OSMSubSort A by PBOOLE:13; ::_thesis: verum
end;
registration
let S1 be OrderSortedSign;
let OU0 be OSAlgebra of S1;
let A be OSSubset of OU0;
cluster OSMSubSort A -> opers_closed ;
coherence
OSMSubSort A is opers_closed by Th29;
end;
begin
registration
let S1 be OrderSortedSign;
let OU0 be OSAlgebra of S1;
let A be opers_closed OSSubset of OU0;
clusterOU0 | A -> order-sorted ;
coherence
OU0 | A is order-sorted
proof
set M = MSAlgebra(# A,(Opers (OU0,A)) #);
( OU0 | A = MSAlgebra(# A,(Opers (OU0,A)) #) & A is OrderSortedSet of S1 ) by Def2, MSUALG_2:def_15;
hence OU0 | A is order-sorted by OSALG_1:17; ::_thesis: verum
end;
end;
registration
let S1 be OrderSortedSign;
let OU0 be OSAlgebra of S1;
let OU1, OU2 be OSSubAlgebra of OU0;
clusterOU1 /\ OU2 -> order-sorted ;
coherence
OU1 /\ OU2 is order-sorted
proof
reconsider M1 = the Sorts of OU1, M2 = the Sorts of OU2 as OrderSortedSet of S1 by OSALG_1:17;
M1 /\ M2 is OrderSortedSet of S1 by Th1;
then the Sorts of (OU1 /\ OU2) is OrderSortedSet of S1 by MSUALG_2:def_16;
hence OU1 /\ OU2 is order-sorted by OSALG_1:17; ::_thesis: verum
end;
end;
definition
let S1 be OrderSortedSign;
let OU0 be OSAlgebra of S1;
let A be OSSubset of OU0;
func GenOSAlg A -> strict OSSubAlgebra of OU0 means :Def12: :: OSALG_2:def 12
( A is OSSubset of it & ( for OU1 being OSSubAlgebra of OU0 st A is OSSubset of OU1 holds
it is OSSubAlgebra of OU1 ) );
existence
ex b1 being strict OSSubAlgebra of OU0 st
( A is OSSubset of b1 & ( for OU1 being OSSubAlgebra of OU0 st A is OSSubset of OU1 holds
b1 is OSSubAlgebra of OU1 ) )
proof
set a = OSMSubSort A;
reconsider u1 = OU0 | (OSMSubSort A) as strict OSSubAlgebra of OU0 ;
take u1 ; ::_thesis: ( A is OSSubset of u1 & ( for OU1 being OSSubAlgebra of OU0 st A is OSSubset of OU1 holds
u1 is OSSubAlgebra of OU1 ) )
A1: u1 = MSAlgebra(# (OSMSubSort A),(Opers (OU0,(OSMSubSort A))) #) by MSUALG_2:def_15;
A2: A is OrderSortedSet of S1 by Def2;
A c= OSMSubSort A by Th29;
then A is MSSubset of u1 by A1, PBOOLE:def_18;
hence A is OSSubset of u1 by A2, Def2; ::_thesis: for OU1 being OSSubAlgebra of OU0 st A is OSSubset of OU1 holds
u1 is OSSubAlgebra of OU1
let U2 be OSSubAlgebra of OU0; ::_thesis: ( A is OSSubset of U2 implies u1 is OSSubAlgebra of U2 )
reconsider B1 = the Sorts of U2 as MSSubset of OU0 by MSUALG_2:def_9;
B1 is OrderSortedSet of S1 by OSALG_1:17;
then reconsider B = B1 as OSSubset of OU0 by Def2;
assume A is OSSubset of U2 ; ::_thesis: u1 is OSSubAlgebra of U2
then A3: ( B is opers_closed & A c= B ) by MSUALG_2:def_9, PBOOLE:def_18;
OSConstants OU0 is OSSubset of U2 by Th13;
then OSConstants OU0 c= B by PBOOLE:def_18;
then A4: B in OSSubSort A by A3, Th19;
the Sorts of u1 c= the Sorts of U2
proof
let i be set ; :: according to PBOOLE:def_2 ::_thesis: ( not i in the carrier of S1 or the Sorts of u1 . i c= the Sorts of U2 . i )
assume i in the carrier of S1 ; ::_thesis: the Sorts of u1 . i c= the Sorts of U2 . i
then reconsider s = i as SortSymbol of S1 ;
( the Sorts of u1 . s = meet (OSSubSort (A,s)) & B . s in OSSubSort (A,s) ) by A1, A4, Def10, Def11;
hence the Sorts of u1 . i c= the Sorts of U2 . i by SETFAM_1:3; ::_thesis: verum
end;
hence u1 is OSSubAlgebra of U2 by MSUALG_2:8; ::_thesis: verum
end;
uniqueness
for b1, b2 being strict OSSubAlgebra of OU0 st A is OSSubset of b1 & ( for OU1 being OSSubAlgebra of OU0 st A is OSSubset of OU1 holds
b1 is OSSubAlgebra of OU1 ) & A is OSSubset of b2 & ( for OU1 being OSSubAlgebra of OU0 st A is OSSubset of OU1 holds
b2 is OSSubAlgebra of OU1 ) holds
b1 = b2
proof
let W1, W2 be strict OSSubAlgebra of OU0; ::_thesis: ( A is OSSubset of W1 & ( for OU1 being OSSubAlgebra of OU0 st A is OSSubset of OU1 holds
W1 is OSSubAlgebra of OU1 ) & A is OSSubset of W2 & ( for OU1 being OSSubAlgebra of OU0 st A is OSSubset of OU1 holds
W2 is OSSubAlgebra of OU1 ) implies W1 = W2 )
assume ( A is OSSubset of W1 & ( for U1 being OSSubAlgebra of OU0 st A is OSSubset of U1 holds
W1 is OSSubAlgebra of U1 ) & A is OSSubset of W2 & ( for U2 being OSSubAlgebra of OU0 st A is OSSubset of U2 holds
W2 is OSSubAlgebra of U2 ) ) ; ::_thesis: W1 = W2
then ( W1 is strict OSSubAlgebra of W2 & W2 is strict OSSubAlgebra of W1 ) ;
hence W1 = W2 by MSUALG_2:7; ::_thesis: verum
end;
end;
:: deftheorem Def12 defines GenOSAlg OSALG_2:def_12_:_
for S1 being OrderSortedSign
for OU0 being OSAlgebra of S1
for A being OSSubset of OU0
for b4 being strict OSSubAlgebra of OU0 holds
( b4 = GenOSAlg A iff ( A is OSSubset of b4 & ( for OU1 being OSSubAlgebra of OU0 st A is OSSubset of OU1 holds
b4 is OSSubAlgebra of OU1 ) ) );
theorem Th30: :: OSALG_2:30
for S1 being OrderSortedSign
for OU0 being OSAlgebra of S1
for A being OSSubset of OU0 holds
( GenOSAlg A = OU0 | (OSMSubSort A) & the Sorts of (GenOSAlg A) = OSMSubSort A )
proof
let S1 be OrderSortedSign; ::_thesis: for OU0 being OSAlgebra of S1
for A being OSSubset of OU0 holds
( GenOSAlg A = OU0 | (OSMSubSort A) & the Sorts of (GenOSAlg A) = OSMSubSort A )
let OU0 be OSAlgebra of S1; ::_thesis: for A being OSSubset of OU0 holds
( GenOSAlg A = OU0 | (OSMSubSort A) & the Sorts of (GenOSAlg A) = OSMSubSort A )
let A be OSSubset of OU0; ::_thesis: ( GenOSAlg A = OU0 | (OSMSubSort A) & the Sorts of (GenOSAlg A) = OSMSubSort A )
set a = OSMSubSort A;
reconsider u1 = OU0 | (OSMSubSort A) as strict OSSubAlgebra of OU0 ;
A1: u1 = MSAlgebra(# (OSMSubSort A),(Opers (OU0,(OSMSubSort A))) #) by MSUALG_2:def_15;
A2: A c= OSMSubSort A by Th29;
A3: A is OrderSortedSet of S1 by Def2;
A4: ( A is OSSubset of u1 & ( for OU1 being OSSubAlgebra of OU0 st A is OSSubset of OU1 holds
u1 is OSSubAlgebra of OU1 ) )
proof
A is MSSubset of u1 by A2, A1, PBOOLE:def_18;
hence A is OSSubset of u1 by A3, Def2; ::_thesis: for OU1 being OSSubAlgebra of OU0 st A is OSSubset of OU1 holds
u1 is OSSubAlgebra of OU1
let U2 be OSSubAlgebra of OU0; ::_thesis: ( A is OSSubset of U2 implies u1 is OSSubAlgebra of U2 )
reconsider B1 = the Sorts of U2 as MSSubset of OU0 by MSUALG_2:def_9;
B1 is OrderSortedSet of S1 by OSALG_1:17;
then reconsider B = B1 as OSSubset of OU0 by Def2;
assume A is OSSubset of U2 ; ::_thesis: u1 is OSSubAlgebra of U2
then A5: ( B is opers_closed & A c= B ) by MSUALG_2:def_9, PBOOLE:def_18;
OSConstants OU0 is OSSubset of U2 by Th13;
then OSConstants OU0 c= B by PBOOLE:def_18;
then A6: B in OSSubSort A by A5, Th19;
the Sorts of u1 c= the Sorts of U2
proof
let i be set ; :: according to PBOOLE:def_2 ::_thesis: ( not i in the carrier of S1 or the Sorts of u1 . i c= the Sorts of U2 . i )
assume i in the carrier of S1 ; ::_thesis: the Sorts of u1 . i c= the Sorts of U2 . i
then reconsider s = i as SortSymbol of S1 ;
( the Sorts of u1 . s = meet (OSSubSort (A,s)) & B . s in OSSubSort (A,s) ) by A1, A6, Def10, Def11;
hence the Sorts of u1 . i c= the Sorts of U2 . i by SETFAM_1:3; ::_thesis: verum
end;
hence u1 is OSSubAlgebra of U2 by MSUALG_2:8; ::_thesis: verum
end;
hence GenOSAlg A = OU0 | (OSMSubSort A) by Def12; ::_thesis: the Sorts of (GenOSAlg A) = OSMSubSort A
thus the Sorts of (GenOSAlg A) = OSMSubSort A by A1, A4, Def12; ::_thesis: verum
end;
theorem Th31: :: OSALG_2:31
for S being non empty non void ManySortedSign
for U0 being MSAlgebra over S
for A being MSSubset of U0 holds
( GenMSAlg A = U0 | (MSSubSort A) & the Sorts of (GenMSAlg A) = MSSubSort A )
proof
let S be non empty non void ManySortedSign ; ::_thesis: for U0 being MSAlgebra over S
for A being MSSubset of U0 holds
( GenMSAlg A = U0 | (MSSubSort A) & the Sorts of (GenMSAlg A) = MSSubSort A )
let U0 be MSAlgebra over S; ::_thesis: for A being MSSubset of U0 holds
( GenMSAlg A = U0 | (MSSubSort A) & the Sorts of (GenMSAlg A) = MSSubSort A )
let A be MSSubset of U0; ::_thesis: ( GenMSAlg A = U0 | (MSSubSort A) & the Sorts of (GenMSAlg A) = MSSubSort A )
set a = MSSubSort A;
reconsider u1 = U0 | (MSSubSort A) as strict MSSubAlgebra of U0 ;
A1: u1 = MSAlgebra(# (MSSubSort A),(Opers (U0,(MSSubSort A))) #) by MSUALG_2:20, MSUALG_2:def_15;
A2: A c= MSSubSort A by MSUALG_2:20;
A3: ( A is MSSubset of u1 & ( for U1 being MSSubAlgebra of U0 st A is MSSubset of U1 holds
u1 is MSSubAlgebra of U1 ) )
proof
thus A is MSSubset of u1 by A2, A1, PBOOLE:def_18; ::_thesis: for U1 being MSSubAlgebra of U0 st A is MSSubset of U1 holds
u1 is MSSubAlgebra of U1
let U2 be MSSubAlgebra of U0; ::_thesis: ( A is MSSubset of U2 implies u1 is MSSubAlgebra of U2 )
reconsider B = the Sorts of U2 as MSSubset of U0 by MSUALG_2:def_9;
Constants U0 is MSSubset of U2 by MSUALG_2:10;
then A4: Constants U0 c= B by PBOOLE:def_18;
assume A is MSSubset of U2 ; ::_thesis: u1 is MSSubAlgebra of U2
then ( B is opers_closed & A c= B ) by MSUALG_2:def_9, PBOOLE:def_18;
then A5: B in SubSort A by A4, MSUALG_2:13;
the Sorts of u1 c= the Sorts of U2
proof
let i be set ; :: according to PBOOLE:def_2 ::_thesis: ( not i in the carrier of S or the Sorts of u1 . i c= the Sorts of U2 . i )
assume i in the carrier of S ; ::_thesis: the Sorts of u1 . i c= the Sorts of U2 . i
then reconsider s = i as SortSymbol of S ;
( the Sorts of u1 . s = meet (SubSort (A,s)) & B . s in SubSort (A,s) ) by A1, A5, MSUALG_2:def_13, MSUALG_2:def_14;
hence the Sorts of u1 . i c= the Sorts of U2 . i by SETFAM_1:3; ::_thesis: verum
end;
hence u1 is MSSubAlgebra of U2 by MSUALG_2:8; ::_thesis: verum
end;
hence GenMSAlg A = U0 | (MSSubSort A) by MSUALG_2:def_17; ::_thesis: the Sorts of (GenMSAlg A) = MSSubSort A
thus the Sorts of (GenMSAlg A) = MSSubSort A by A1, A3, MSUALG_2:def_17; ::_thesis: verum
end;
theorem Th32: :: OSALG_2:32
for S1 being OrderSortedSign
for OU0 being OSAlgebra of S1
for A being OSSubset of OU0 holds the Sorts of (GenMSAlg A) c= the Sorts of (GenOSAlg A)
proof
let S1 be OrderSortedSign; ::_thesis: for OU0 being OSAlgebra of S1
for A being OSSubset of OU0 holds the Sorts of (GenMSAlg A) c= the Sorts of (GenOSAlg A)
let OU0 be OSAlgebra of S1; ::_thesis: for A being OSSubset of OU0 holds the Sorts of (GenMSAlg A) c= the Sorts of (GenOSAlg A)
let A be OSSubset of OU0; ::_thesis: the Sorts of (GenMSAlg A) c= the Sorts of (GenOSAlg A)
set GM = GenMSAlg A;
set GO = GenOSAlg A;
let i be set ; :: according to PBOOLE:def_2 ::_thesis: ( not i in the carrier of S1 or the Sorts of (GenMSAlg A) . i c= the Sorts of (GenOSAlg A) . i )
assume i in the carrier of S1 ; ::_thesis: the Sorts of (GenMSAlg A) . i c= the Sorts of (GenOSAlg A) . i
then reconsider s = i as SortSymbol of S1 ;
the Sorts of (GenMSAlg A) = MSSubSort A by Th31;
then A1: the Sorts of (GenMSAlg A) . s = meet (SubSort (A,s)) by MSUALG_2:def_14;
the Sorts of (GenOSAlg A) = OSMSubSort A by Th30;
then the Sorts of (GenOSAlg A) . s = meet (OSSubSort (A,s)) by Def11;
hence the Sorts of (GenMSAlg A) . i c= the Sorts of (GenOSAlg A) . i by A1, Th22, SETFAM_1:6; ::_thesis: verum
end;
theorem :: OSALG_2:33
for S1 being OrderSortedSign
for OU0 being OSAlgebra of S1
for A being OSSubset of OU0 holds GenMSAlg A is MSSubAlgebra of GenOSAlg A by Th32, MSUALG_2:8;
theorem Th34: :: OSALG_2:34
for S1 being OrderSortedSign
for OU0 being strict OSAlgebra of S1
for B being OSSubset of OU0 st B = the Sorts of OU0 holds
GenOSAlg B = OU0
proof
let S1 be OrderSortedSign; ::_thesis: for OU0 being strict OSAlgebra of S1
for B being OSSubset of OU0 st B = the Sorts of OU0 holds
GenOSAlg B = OU0
let OU0 be strict OSAlgebra of S1; ::_thesis: for B being OSSubset of OU0 st B = the Sorts of OU0 holds
GenOSAlg B = OU0
let B be OSSubset of OU0; ::_thesis: ( B = the Sorts of OU0 implies GenOSAlg B = OU0 )
assume B = the Sorts of OU0 ; ::_thesis: GenOSAlg B = OU0
then A1: GenMSAlg B = OU0 by MSUALG_2:21;
GenMSAlg B is strict MSSubAlgebra of GenOSAlg B by Th32, MSUALG_2:8;
hence GenOSAlg B = OU0 by A1, MSUALG_2:7; ::_thesis: verum
end;
theorem Th35: :: OSALG_2:35
for S1 being OrderSortedSign
for OU0 being OSAlgebra of S1
for OU1 being strict OSSubAlgebra of OU0
for B being OSSubset of OU0 st B = the Sorts of OU1 holds
GenOSAlg B = OU1
proof
let S1 be OrderSortedSign; ::_thesis: for OU0 being OSAlgebra of S1
for OU1 being strict OSSubAlgebra of OU0
for B being OSSubset of OU0 st B = the Sorts of OU1 holds
GenOSAlg B = OU1
let OU0 be OSAlgebra of S1; ::_thesis: for OU1 being strict OSSubAlgebra of OU0
for B being OSSubset of OU0 st B = the Sorts of OU1 holds
GenOSAlg B = OU1
let OU1 be strict OSSubAlgebra of OU0; ::_thesis: for B being OSSubset of OU0 st B = the Sorts of OU1 holds
GenOSAlg B = OU1
let B be OSSubset of OU0; ::_thesis: ( B = the Sorts of OU1 implies GenOSAlg B = OU1 )
set W = GenOSAlg B;
assume A1: B = the Sorts of OU1 ; ::_thesis: GenOSAlg B = OU1
then A2: B is MSSubset of OU1 by PBOOLE:def_18;
B is OSSubset of GenOSAlg B by Def12;
then the Sorts of OU1 c= the Sorts of (GenOSAlg B) by A1, PBOOLE:def_18;
then A3: OU1 is strict MSSubAlgebra of GenOSAlg B by MSUALG_2:8;
B is OrderSortedSet of S1 by Def2;
then B is OSSubset of OU1 by A2, Def2;
then GenOSAlg B is strict OSSubAlgebra of OU1 by Def12;
hence GenOSAlg B = OU1 by A3, MSUALG_2:7; ::_thesis: verum
end;
theorem Th36: :: OSALG_2:36
for S1 being OrderSortedSign
for U0 being non-empty OSAlgebra of S1
for U1 being OSSubAlgebra of U0 holds (GenOSAlg (OSConstants U0)) /\ U1 = GenOSAlg (OSConstants U0)
proof
let S1 be OrderSortedSign; ::_thesis: for U0 being non-empty OSAlgebra of S1
for U1 being OSSubAlgebra of U0 holds (GenOSAlg (OSConstants U0)) /\ U1 = GenOSAlg (OSConstants U0)
let U0 be non-empty OSAlgebra of S1; ::_thesis: for U1 being OSSubAlgebra of U0 holds (GenOSAlg (OSConstants U0)) /\ U1 = GenOSAlg (OSConstants U0)
let U1 be OSSubAlgebra of U0; ::_thesis: (GenOSAlg (OSConstants U0)) /\ U1 = GenOSAlg (OSConstants U0)
set C = OSConstants U0;
set G = GenOSAlg (OSConstants U0);
OSConstants U0 is OSSubset of U1 by Th13;
then GenOSAlg (OSConstants U0) is strict OSSubAlgebra of U1 by Def12;
then the Sorts of (GenOSAlg (OSConstants U0)) is MSSubset of U1 by MSUALG_2:def_9;
then ( the Sorts of ((GenOSAlg (OSConstants U0)) /\ U1) = the Sorts of (GenOSAlg (OSConstants U0)) /\ the Sorts of U1 & the Sorts of (GenOSAlg (OSConstants U0)) c= the Sorts of U1 ) by MSUALG_2:def_16, PBOOLE:def_18;
then the Sorts of ((GenOSAlg (OSConstants U0)) /\ U1) = the Sorts of (GenOSAlg (OSConstants U0)) by PBOOLE:23;
hence (GenOSAlg (OSConstants U0)) /\ U1 = GenOSAlg (OSConstants U0) by MSUALG_2:9; ::_thesis: verum
end;
definition
let S1 be OrderSortedSign;
let U0 be non-empty OSAlgebra of S1;
let U1, U2 be OSSubAlgebra of U0;
funcU1 "\/"_os U2 -> strict OSSubAlgebra of U0 means :Def13: :: OSALG_2:def 13
for A being OSSubset of U0 st A = the Sorts of U1 \/ the Sorts of U2 holds
it = GenOSAlg A;
existence
ex b1 being strict OSSubAlgebra of U0 st
for A being OSSubset of U0 st A = the Sorts of U1 \/ the Sorts of U2 holds
b1 = GenOSAlg A
proof
set B = the Sorts of U1 \/ the Sorts of U2;
the Sorts of U2 is MSSubset of U0 by MSUALG_2:def_9;
then A1: the Sorts of U2 c= the Sorts of U0 by PBOOLE:def_18;
the Sorts of U1 is MSSubset of U0 by MSUALG_2:def_9;
then the Sorts of U1 c= the Sorts of U0 by PBOOLE:def_18;
then the Sorts of U1 \/ the Sorts of U2 c= the Sorts of U0 by A1, PBOOLE:16;
then reconsider B = the Sorts of U1 \/ the Sorts of U2 as MSSubset of U0 by PBOOLE:def_18;
reconsider B1 = the Sorts of U1, B2 = the Sorts of U2 as OrderSortedSet of S1 by OSALG_1:17;
B = B1 \/ B2 ;
then B is OrderSortedSet of S1 by Th2;
then reconsider B0 = B as OSSubset of U0 by Def2;
take GenOSAlg B0 ; ::_thesis: for A being OSSubset of U0 st A = the Sorts of U1 \/ the Sorts of U2 holds
GenOSAlg B0 = GenOSAlg A
thus for A being OSSubset of U0 st A = the Sorts of U1 \/ the Sorts of U2 holds
GenOSAlg B0 = GenOSAlg A ; ::_thesis: verum
end;
uniqueness
for b1, b2 being strict OSSubAlgebra of U0 st ( for A being OSSubset of U0 st A = the Sorts of U1 \/ the Sorts of U2 holds
b1 = GenOSAlg A ) & ( for A being OSSubset of U0 st A = the Sorts of U1 \/ the Sorts of U2 holds
b2 = GenOSAlg A ) holds
b1 = b2
proof
reconsider B1 = the Sorts of U1, B2 = the Sorts of U2 as OrderSortedSet of S1 by OSALG_1:17;
set B = the Sorts of U1 \/ the Sorts of U2;
the Sorts of U2 is MSSubset of U0 by MSUALG_2:def_9;
then A2: the Sorts of U2 c= the Sorts of U0 by PBOOLE:def_18;
the Sorts of U1 is MSSubset of U0 by MSUALG_2:def_9;
then the Sorts of U1 c= the Sorts of U0 by PBOOLE:def_18;
then the Sorts of U1 \/ the Sorts of U2 c= the Sorts of U0 by A2, PBOOLE:16;
then reconsider B = the Sorts of U1 \/ the Sorts of U2 as MSSubset of U0 by PBOOLE:def_18;
let W1, W2 be strict OSSubAlgebra of U0; ::_thesis: ( ( for A being OSSubset of U0 st A = the Sorts of U1 \/ the Sorts of U2 holds
W1 = GenOSAlg A ) & ( for A being OSSubset of U0 st A = the Sorts of U1 \/ the Sorts of U2 holds
W2 = GenOSAlg A ) implies W1 = W2 )
assume that
A3: for A being OSSubset of U0 st A = the Sorts of U1 \/ the Sorts of U2 holds
W1 = GenOSAlg A and
A4: for A being OSSubset of U0 st A = the Sorts of U1 \/ the Sorts of U2 holds
W2 = GenOSAlg A ; ::_thesis: W1 = W2
B = B1 \/ B2 ;
then B is OrderSortedSet of S1 by Th2;
then reconsider B0 = B as OSSubset of U0 by Def2;
W1 = GenOSAlg B0 by A3;
hence W1 = W2 by A4; ::_thesis: verum
end;
end;
:: deftheorem Def13 defines "\/"_os OSALG_2:def_13_:_
for S1 being OrderSortedSign
for U0 being non-empty OSAlgebra of S1
for U1, U2 being OSSubAlgebra of U0
for b5 being strict OSSubAlgebra of U0 holds
( b5 = U1 "\/"_os U2 iff for A being OSSubset of U0 st A = the Sorts of U1 \/ the Sorts of U2 holds
b5 = GenOSAlg A );
theorem Th37: :: OSALG_2:37
for S1 being OrderSortedSign
for U0 being non-empty OSAlgebra of S1
for U1 being OSSubAlgebra of U0
for A, B being OSSubset of U0 st B = A \/ the Sorts of U1 holds
(GenOSAlg A) "\/"_os U1 = GenOSAlg B
proof
let S1 be OrderSortedSign; ::_thesis: for U0 being non-empty OSAlgebra of S1
for U1 being OSSubAlgebra of U0
for A, B being OSSubset of U0 st B = A \/ the Sorts of U1 holds
(GenOSAlg A) "\/"_os U1 = GenOSAlg B
let U0 be non-empty OSAlgebra of S1; ::_thesis: for U1 being OSSubAlgebra of U0
for A, B being OSSubset of U0 st B = A \/ the Sorts of U1 holds
(GenOSAlg A) "\/"_os U1 = GenOSAlg B
let U1 be OSSubAlgebra of U0; ::_thesis: for A, B being OSSubset of U0 st B = A \/ the Sorts of U1 holds
(GenOSAlg A) "\/"_os U1 = GenOSAlg B
let A, B be OSSubset of U0; ::_thesis: ( B = A \/ the Sorts of U1 implies (GenOSAlg A) "\/"_os U1 = GenOSAlg B )
assume A1: B = A \/ the Sorts of U1 ; ::_thesis: (GenOSAlg A) "\/"_os U1 = GenOSAlg B
reconsider u1m = the Sorts of U1, am = the Sorts of (GenOSAlg A) as MSSubset of U0 by MSUALG_2:def_9;
A2: ( the Sorts of U1 is OrderSortedSet of S1 & the Sorts of (GenOSAlg A) is OrderSortedSet of S1 ) by OSALG_1:17;
then reconsider u1 = u1m, a = am as OSSubset of U0 by Def2;
( a c= the Sorts of U0 & u1 c= the Sorts of U0 ) by PBOOLE:def_18;
then a \/ u1 c= the Sorts of U0 by PBOOLE:16;
then reconsider b = a \/ u1 as MSSubset of U0 by PBOOLE:def_18;
A3: a \/ u1 is OrderSortedSet of S1 by A2, Th2;
then reconsider b = b as OSSubset of U0 by Def2;
A4: (GenOSAlg A) "\/"_os U1 = GenOSAlg b by Def13;
then a \/ u1 is OSSubset of (GenOSAlg A) "\/"_os U1 by Def12;
then A5: a \/ u1 c= the Sorts of ((GenOSAlg A) "\/"_os U1) by PBOOLE:def_18;
A is OSSubset of GenOSAlg A by Def12;
then A6: A c= the Sorts of (GenOSAlg A) by PBOOLE:def_18;
then A \/ u1 c= a \/ u1 by PBOOLE:20;
then B c= the Sorts of ((GenOSAlg A) "\/"_os U1) by A1, A5, PBOOLE:13;
then A7: B is MSSubset of ((GenOSAlg A) "\/"_os U1) by PBOOLE:def_18;
A8: A is OrderSortedSet of S1 by Def2;
A9: the Sorts of ((GenOSAlg A) /\ (GenOSAlg B)) = the Sorts of (GenOSAlg A) /\ the Sorts of (GenOSAlg B) by MSUALG_2:def_16;
B is OSSubset of GenOSAlg B by Def12;
then A10: B c= the Sorts of (GenOSAlg B) by PBOOLE:def_18;
A c= B by A1, PBOOLE:14;
then A c= the Sorts of (GenOSAlg B) by A10, PBOOLE:13;
then A c= the Sorts of (GenOSAlg A) /\ the Sorts of (GenOSAlg B) by A6, PBOOLE:17;
then A is MSSubset of ((GenOSAlg A) /\ (GenOSAlg B)) by A9, PBOOLE:def_18;
then A is OSSubset of (GenOSAlg A) /\ (GenOSAlg B) by A8, Def2;
then GenOSAlg A is OSSubAlgebra of (GenOSAlg A) /\ (GenOSAlg B) by Def12;
then a is MSSubset of ((GenOSAlg A) /\ (GenOSAlg B)) by MSUALG_2:def_9;
then A11: a c= the Sorts of (GenOSAlg A) /\ the Sorts of (GenOSAlg B) by A9, PBOOLE:def_18;
the Sorts of (GenOSAlg A) /\ the Sorts of (GenOSAlg B) c= a by PBOOLE:15;
then a = the Sorts of (GenOSAlg A) /\ the Sorts of (GenOSAlg B) by A11, PBOOLE:146;
then A12: a c= the Sorts of (GenOSAlg B) by PBOOLE:15;
u1 c= B by A1, PBOOLE:14;
then u1 c= the Sorts of (GenOSAlg B) by A10, PBOOLE:13;
then b c= the Sorts of (GenOSAlg B) by A12, PBOOLE:16;
then b is MSSubset of (GenOSAlg B) by PBOOLE:def_18;
then b is OSSubset of GenOSAlg B by A3, Def2;
then A13: GenOSAlg b is strict OSSubAlgebra of GenOSAlg B by Def12;
B is OrderSortedSet of S1 by Def2;
then B is OSSubset of (GenOSAlg A) "\/"_os U1 by A7, Def2;
then GenOSAlg B is strict OSSubAlgebra of (GenOSAlg A) "\/"_os U1 by Def12;
hence (GenOSAlg A) "\/"_os U1 = GenOSAlg B by A4, A13, MSUALG_2:7; ::_thesis: verum
end;
theorem Th38: :: OSALG_2:38
for S1 being OrderSortedSign
for U0 being non-empty OSAlgebra of S1
for U1 being OSSubAlgebra of U0
for B being OSSubset of U0 st B = the Sorts of U0 holds
(GenOSAlg B) "\/"_os U1 = GenOSAlg B
proof
let S1 be OrderSortedSign; ::_thesis: for U0 being non-empty OSAlgebra of S1
for U1 being OSSubAlgebra of U0
for B being OSSubset of U0 st B = the Sorts of U0 holds
(GenOSAlg B) "\/"_os U1 = GenOSAlg B
let U0 be non-empty OSAlgebra of S1; ::_thesis: for U1 being OSSubAlgebra of U0
for B being OSSubset of U0 st B = the Sorts of U0 holds
(GenOSAlg B) "\/"_os U1 = GenOSAlg B
let U1 be OSSubAlgebra of U0; ::_thesis: for B being OSSubset of U0 st B = the Sorts of U0 holds
(GenOSAlg B) "\/"_os U1 = GenOSAlg B
let B be OSSubset of U0; ::_thesis: ( B = the Sorts of U0 implies (GenOSAlg B) "\/"_os U1 = GenOSAlg B )
A1: the Sorts of U1 is MSSubset of U0 by MSUALG_2:def_9;
assume B = the Sorts of U0 ; ::_thesis: (GenOSAlg B) "\/"_os U1 = GenOSAlg B
then the Sorts of U1 c= B by A1, PBOOLE:def_18;
then B \/ the Sorts of U1 = B by PBOOLE:22;
hence (GenOSAlg B) "\/"_os U1 = GenOSAlg B by Th37; ::_thesis: verum
end;
theorem Th39: :: OSALG_2:39
for S1 being OrderSortedSign
for U0 being non-empty OSAlgebra of S1
for U1, U2 being OSSubAlgebra of U0 holds U1 "\/"_os U2 = U2 "\/"_os U1
proof
let S1 be OrderSortedSign; ::_thesis: for U0 being non-empty OSAlgebra of S1
for U1, U2 being OSSubAlgebra of U0 holds U1 "\/"_os U2 = U2 "\/"_os U1
let U0 be non-empty OSAlgebra of S1; ::_thesis: for U1, U2 being OSSubAlgebra of U0 holds U1 "\/"_os U2 = U2 "\/"_os U1
let U1, U2 be OSSubAlgebra of U0; ::_thesis: U1 "\/"_os U2 = U2 "\/"_os U1
reconsider u1 = the Sorts of U1, u2 = the Sorts of U2 as MSSubset of U0 by MSUALG_2:def_9;
( u1 c= the Sorts of U0 & u2 c= the Sorts of U0 ) by PBOOLE:def_18;
then u1 \/ u2 c= the Sorts of U0 by PBOOLE:16;
then reconsider A1 = u1 \/ u2 as MSSubset of U0 by PBOOLE:def_18;
( u1 is OrderSortedSet of S1 & u2 is OrderSortedSet of S1 ) by OSALG_1:17;
then A1 is OrderSortedSet of S1 by Th2;
then reconsider A = A1 as OSSubset of U0 by Def2;
U1 "\/"_os U2 = GenOSAlg A by Def13;
hence U1 "\/"_os U2 = U2 "\/"_os U1 by Def13; ::_thesis: verum
end;
theorem Th40: :: OSALG_2:40
for S1 being OrderSortedSign
for U0 being non-empty OSAlgebra of S1
for U1, U2 being strict OSSubAlgebra of U0 holds U1 /\ (U1 "\/"_os U2) = U1
proof
let S1 be OrderSortedSign; ::_thesis: for U0 being non-empty OSAlgebra of S1
for U1, U2 being strict OSSubAlgebra of U0 holds U1 /\ (U1 "\/"_os U2) = U1
let U0 be non-empty OSAlgebra of S1; ::_thesis: for U1, U2 being strict OSSubAlgebra of U0 holds U1 /\ (U1 "\/"_os U2) = U1
let U1, U2 be strict OSSubAlgebra of U0; ::_thesis: U1 /\ (U1 "\/"_os U2) = U1
reconsider u1 = the Sorts of U1, u2 = the Sorts of U2 as MSSubset of U0 by MSUALG_2:def_9;
reconsider u112 = the Sorts of (U1 /\ (U1 "\/"_os U2)) as MSSubset of U0 by MSUALG_2:def_9;
A1: the Charact of (U1 /\ (U1 "\/"_os U2)) = Opers (U0,u112) by MSUALG_2:def_16;
( u1 c= the Sorts of U0 & u2 c= the Sorts of U0 ) by PBOOLE:def_18;
then u1 \/ u2 c= the Sorts of U0 by PBOOLE:16;
then reconsider A = u1 \/ u2 as MSSubset of U0 by PBOOLE:def_18;
( u1 is OrderSortedSet of S1 & u2 is OrderSortedSet of S1 ) by OSALG_1:17;
then A is OrderSortedSet of S1 by Th2;
then reconsider A = A as OSSubset of U0 by Def2;
A2: the Sorts of (U1 /\ (U1 "\/"_os U2)) = the Sorts of U1 /\ the Sorts of (U1 "\/"_os U2) by MSUALG_2:def_16;
U1 "\/"_os U2 = GenOSAlg A by Def13;
then A is OSSubset of U1 "\/"_os U2 by Def12;
then A3: A c= the Sorts of (U1 "\/"_os U2) by PBOOLE:def_18;
the Sorts of U1 c= A by PBOOLE:14;
then the Sorts of U1 c= the Sorts of (U1 "\/"_os U2) by A3, PBOOLE:13;
then A4: the Sorts of U1 c= the Sorts of (U1 /\ (U1 "\/"_os U2)) by A2, PBOOLE:17;
the Sorts of (U1 /\ (U1 "\/"_os U2)) c= the Sorts of U1 by A2, PBOOLE:15;
then the Sorts of (U1 /\ (U1 "\/"_os U2)) = the Sorts of U1 by A4, PBOOLE:146;
hence U1 /\ (U1 "\/"_os U2) = U1 by A1, MSUALG_2:def_9; ::_thesis: verum
end;
theorem Th41: :: OSALG_2:41
for S1 being OrderSortedSign
for U0 being non-empty OSAlgebra of S1
for U1, U2 being strict OSSubAlgebra of U0 holds (U1 /\ U2) "\/"_os U2 = U2
proof
let S1 be OrderSortedSign; ::_thesis: for U0 being non-empty OSAlgebra of S1
for U1, U2 being strict OSSubAlgebra of U0 holds (U1 /\ U2) "\/"_os U2 = U2
let U0 be non-empty OSAlgebra of S1; ::_thesis: for U1, U2 being strict OSSubAlgebra of U0 holds (U1 /\ U2) "\/"_os U2 = U2
let U1, U2 be strict OSSubAlgebra of U0; ::_thesis: (U1 /\ U2) "\/"_os U2 = U2
reconsider u12 = the Sorts of (U1 /\ U2), u2 = the Sorts of U2 as MSSubset of U0 by MSUALG_2:def_9;
A1: ( u12 is OrderSortedSet of S1 & u2 is OrderSortedSet of S1 ) by OSALG_1:17;
then reconsider u12 = u12, u2 = u2 as OSSubset of U0 by Def2;
( u12 c= the Sorts of U0 & u2 c= the Sorts of U0 ) by PBOOLE:def_18;
then u12 \/ u2 c= the Sorts of U0 by PBOOLE:16;
then reconsider A = u12 \/ u2 as MSSubset of U0 by PBOOLE:def_18;
A is OrderSortedSet of S1 by A1, Th2;
then reconsider A = u12 \/ u2 as OSSubset of U0 by Def2;
u12 = the Sorts of U1 /\ the Sorts of U2 by MSUALG_2:def_16;
then u12 c= u2 by PBOOLE:15;
then A2: A = u2 by PBOOLE:22;
(U1 /\ U2) "\/"_os U2 = GenOSAlg A by Def13;
hence (U1 /\ U2) "\/"_os U2 = U2 by A2, Th35; ::_thesis: verum
end;
begin
definition
let S1 be OrderSortedSign;
let OU0 be OSAlgebra of S1;
func OSSub OU0 -> set means :Def14: :: OSALG_2:def 14
for x being set holds
( x in it iff x is strict OSSubAlgebra of OU0 );
existence
ex b1 being set st
for x being set holds
( x in b1 iff x is strict OSSubAlgebra of OU0 )
proof
set X = { (GenOSAlg (@ A)) where A is Element of OSSubSort OU0 : verum } ;
take { (GenOSAlg (@ A)) where A is Element of OSSubSort OU0 : verum } ; ::_thesis: for x being set holds
( x in { (GenOSAlg (@ A)) where A is Element of OSSubSort OU0 : verum } iff x is strict OSSubAlgebra of OU0 )
let x be set ; ::_thesis: ( x in { (GenOSAlg (@ A)) where A is Element of OSSubSort OU0 : verum } iff x is strict OSSubAlgebra of OU0 )
thus ( x in { (GenOSAlg (@ A)) where A is Element of OSSubSort OU0 : verum } implies x is strict OSSubAlgebra of OU0 ) ::_thesis: ( x is strict OSSubAlgebra of OU0 implies x in { (GenOSAlg (@ A)) where A is Element of OSSubSort OU0 : verum } )
proof
assume x in { (GenOSAlg (@ A)) where A is Element of OSSubSort OU0 : verum } ; ::_thesis: x is strict OSSubAlgebra of OU0
then ex A being Element of OSSubSort OU0 st x = GenOSAlg (@ A) ;
hence x is strict OSSubAlgebra of OU0 ; ::_thesis: verum
end;
assume x is strict OSSubAlgebra of OU0 ; ::_thesis: x in { (GenOSAlg (@ A)) where A is Element of OSSubSort OU0 : verum }
then reconsider a = x as strict OSSubAlgebra of OU0 ;
reconsider A = the Sorts of a as OSSubset of OU0 by Th5;
A is opers_closed by Th5;
then reconsider h = A as Element of OSSubSort OU0 by Th20;
a = GenOSAlg (@ h) by Th35;
hence x in { (GenOSAlg (@ A)) where A is Element of OSSubSort OU0 : verum } ; ::_thesis: verum
end;
uniqueness
for b1, b2 being set st ( for x being set holds
( x in b1 iff x is strict OSSubAlgebra of OU0 ) ) & ( for x being set holds
( x in b2 iff x is strict OSSubAlgebra of OU0 ) ) holds
b1 = b2
proof
defpred S1[ set ] means $1 is strict OSSubAlgebra of OU0;
thus for X1, X2 being set st ( for x being set holds
( x in X1 iff S1[x] ) ) & ( for x being set holds
( x in X2 iff S1[x] ) ) holds
X1 = X2 from XBOOLE_0:sch_3(); ::_thesis: verum
end;
end;
:: deftheorem Def14 defines OSSub OSALG_2:def_14_:_
for S1 being OrderSortedSign
for OU0 being OSAlgebra of S1
for b3 being set holds
( b3 = OSSub OU0 iff for x being set holds
( x in b3 iff x is strict OSSubAlgebra of OU0 ) );
theorem Th42: :: OSALG_2:42
for S1 being OrderSortedSign
for OU0 being OSAlgebra of S1 holds OSSub OU0 c= MSSub OU0
proof
let S1 be OrderSortedSign; ::_thesis: for OU0 being OSAlgebra of S1 holds OSSub OU0 c= MSSub OU0
let OU0 be OSAlgebra of S1; ::_thesis: OSSub OU0 c= MSSub OU0
let x be set ; :: according to TARSKI:def_3 ::_thesis: ( not x in OSSub OU0 or x in MSSub OU0 )
assume x in OSSub OU0 ; ::_thesis: x in MSSub OU0
then x is strict MSSubAlgebra of OU0 by Def14;
hence x in MSSub OU0 by MSUALG_2:def_19; ::_thesis: verum
end;
registration
let S be OrderSortedSign;
let U0 be OSAlgebra of S;
cluster OSSub U0 -> non empty ;
coherence
not OSSub U0 is empty
proof
set x = the strict OSSubAlgebra of U0;
the strict OSSubAlgebra of U0 in OSSub U0 by Def14;
hence not OSSub U0 is empty ; ::_thesis: verum
end;
end;
definition
let S1 be OrderSortedSign;
let OU0 be OSAlgebra of S1;
:: original: OSSub
redefine func OSSub OU0 -> Subset of (MSSub OU0);
coherence
OSSub OU0 is Subset of (MSSub OU0) by Th42;
end;
definition
let S1 be OrderSortedSign;
let U0 be non-empty OSAlgebra of S1;
func OSAlg_join U0 -> BinOp of (OSSub U0) means :Def15: :: OSALG_2:def 15
for x, y being Element of OSSub U0
for U1, U2 being strict OSSubAlgebra of U0 st x = U1 & y = U2 holds
it . (x,y) = U1 "\/"_os U2;
existence
ex b1 being BinOp of (OSSub U0) st
for x, y being Element of OSSub U0
for U1, U2 being strict OSSubAlgebra of U0 st x = U1 & y = U2 holds
b1 . (x,y) = U1 "\/"_os U2
proof
defpred S1[ Element of OSSub U0, Element of OSSub U0, set ] means for U1, U2 being strict OSSubAlgebra of U0 st $1 = U1 & $2 = U2 holds
$3 = U1 "\/"_os U2;
A1: for x, y being Element of OSSub U0 ex z being Element of OSSub U0 st S1[x,y,z]
proof
let x, y be Element of OSSub U0; ::_thesis: ex z being Element of OSSub U0 st S1[x,y,z]
reconsider U1 = x, U2 = y as strict OSSubAlgebra of U0 by Def14;
reconsider z = U1 "\/"_os U2 as Element of OSSub U0 by Def14;
take z ; ::_thesis: S1[x,y,z]
thus S1[x,y,z] ; ::_thesis: verum
end;
consider o being BinOp of (OSSub U0) such that
A2: for a, b being Element of OSSub U0 holds S1[a,b,o . (a,b)] from BINOP_1:sch_3(A1);
take o ; ::_thesis: for x, y being Element of OSSub U0
for U1, U2 being strict OSSubAlgebra of U0 st x = U1 & y = U2 holds
o . (x,y) = U1 "\/"_os U2
thus for x, y being Element of OSSub U0
for U1, U2 being strict OSSubAlgebra of U0 st x = U1 & y = U2 holds
o . (x,y) = U1 "\/"_os U2 by A2; ::_thesis: verum
end;
uniqueness
for b1, b2 being BinOp of (OSSub U0) st ( for x, y being Element of OSSub U0
for U1, U2 being strict OSSubAlgebra of U0 st x = U1 & y = U2 holds
b1 . (x,y) = U1 "\/"_os U2 ) & ( for x, y being Element of OSSub U0
for U1, U2 being strict OSSubAlgebra of U0 st x = U1 & y = U2 holds
b2 . (x,y) = U1 "\/"_os U2 ) holds
b1 = b2
proof
let o1, o2 be BinOp of (OSSub U0); ::_thesis: ( ( for x, y being Element of OSSub U0
for U1, U2 being strict OSSubAlgebra of U0 st x = U1 & y = U2 holds
o1 . (x,y) = U1 "\/"_os U2 ) & ( for x, y being Element of OSSub U0
for U1, U2 being strict OSSubAlgebra of U0 st x = U1 & y = U2 holds
o2 . (x,y) = U1 "\/"_os U2 ) implies o1 = o2 )
assume that
A3: for x, y being Element of OSSub U0
for U1, U2 being strict OSSubAlgebra of U0 st x = U1 & y = U2 holds
o1 . (x,y) = U1 "\/"_os U2 and
A4: for x, y being Element of OSSub U0
for U1, U2 being strict OSSubAlgebra of U0 st x = U1 & y = U2 holds
o2 . (x,y) = U1 "\/"_os U2 ; ::_thesis: o1 = o2
for x, y being Element of OSSub U0 holds o1 . (x,y) = o2 . (x,y)
proof
let x, y be Element of OSSub U0; ::_thesis: o1 . (x,y) = o2 . (x,y)
reconsider U1 = x, U2 = y as strict OSSubAlgebra of U0 by Def14;
o1 . (x,y) = U1 "\/"_os U2 by A3;
hence o1 . (x,y) = o2 . (x,y) by A4; ::_thesis: verum
end;
hence o1 = o2 by BINOP_1:2; ::_thesis: verum
end;
end;
:: deftheorem Def15 defines OSAlg_join OSALG_2:def_15_:_
for S1 being OrderSortedSign
for U0 being non-empty OSAlgebra of S1
for b3 being BinOp of (OSSub U0) holds
( b3 = OSAlg_join U0 iff for x, y being Element of OSSub U0
for U1, U2 being strict OSSubAlgebra of U0 st x = U1 & y = U2 holds
b3 . (x,y) = U1 "\/"_os U2 );
definition
let S1 be OrderSortedSign;
let U0 be non-empty OSAlgebra of S1;
func OSAlg_meet U0 -> BinOp of (OSSub U0) means :Def16: :: OSALG_2:def 16
for x, y being Element of OSSub U0
for U1, U2 being strict OSSubAlgebra of U0 st x = U1 & y = U2 holds
it . (x,y) = U1 /\ U2;
existence
ex b1 being BinOp of (OSSub U0) st
for x, y being Element of OSSub U0
for U1, U2 being strict OSSubAlgebra of U0 st x = U1 & y = U2 holds
b1 . (x,y) = U1 /\ U2
proof
defpred S1[ Element of OSSub U0, Element of OSSub U0, set ] means for U1, U2 being strict OSSubAlgebra of U0 st $1 = U1 & $2 = U2 holds
$3 = U1 /\ U2;
A1: for x, y being Element of OSSub U0 ex z being Element of OSSub U0 st S1[x,y,z]
proof
let x, y be Element of OSSub U0; ::_thesis: ex z being Element of OSSub U0 st S1[x,y,z]
reconsider U1 = x, U2 = y as strict OSSubAlgebra of U0 by Def14;
reconsider z = U1 /\ U2 as Element of OSSub U0 by Def14;
take z ; ::_thesis: S1[x,y,z]
thus S1[x,y,z] ; ::_thesis: verum
end;
consider o being BinOp of (OSSub U0) such that
A2: for a, b being Element of OSSub U0 holds S1[a,b,o . (a,b)] from BINOP_1:sch_3(A1);
take o ; ::_thesis: for x, y being Element of OSSub U0
for U1, U2 being strict OSSubAlgebra of U0 st x = U1 & y = U2 holds
o . (x,y) = U1 /\ U2
thus for x, y being Element of OSSub U0
for U1, U2 being strict OSSubAlgebra of U0 st x = U1 & y = U2 holds
o . (x,y) = U1 /\ U2 by A2; ::_thesis: verum
end;
uniqueness
for b1, b2 being BinOp of (OSSub U0) st ( for x, y being Element of OSSub U0
for U1, U2 being strict OSSubAlgebra of U0 st x = U1 & y = U2 holds
b1 . (x,y) = U1 /\ U2 ) & ( for x, y being Element of OSSub U0
for U1, U2 being strict OSSubAlgebra of U0 st x = U1 & y = U2 holds
b2 . (x,y) = U1 /\ U2 ) holds
b1 = b2
proof
let o1, o2 be BinOp of (OSSub U0); ::_thesis: ( ( for x, y being Element of OSSub U0
for U1, U2 being strict OSSubAlgebra of U0 st x = U1 & y = U2 holds
o1 . (x,y) = U1 /\ U2 ) & ( for x, y being Element of OSSub U0
for U1, U2 being strict OSSubAlgebra of U0 st x = U1 & y = U2 holds
o2 . (x,y) = U1 /\ U2 ) implies o1 = o2 )
assume that
A3: for x, y being Element of OSSub U0
for U1, U2 being strict OSSubAlgebra of U0 st x = U1 & y = U2 holds
o1 . (x,y) = U1 /\ U2 and
A4: for x, y being Element of OSSub U0
for U1, U2 being strict OSSubAlgebra of U0 st x = U1 & y = U2 holds
o2 . (x,y) = U1 /\ U2 ; ::_thesis: o1 = o2
for x, y being Element of OSSub U0 holds o1 . (x,y) = o2 . (x,y)
proof
let x, y be Element of OSSub U0; ::_thesis: o1 . (x,y) = o2 . (x,y)
reconsider U1 = x, U2 = y as strict OSSubAlgebra of U0 by Def14;
o1 . (x,y) = U1 /\ U2 by A3;
hence o1 . (x,y) = o2 . (x,y) by A4; ::_thesis: verum
end;
hence o1 = o2 by BINOP_1:2; ::_thesis: verum
end;
end;
:: deftheorem Def16 defines OSAlg_meet OSALG_2:def_16_:_
for S1 being OrderSortedSign
for U0 being non-empty OSAlgebra of S1
for b3 being BinOp of (OSSub U0) holds
( b3 = OSAlg_meet U0 iff for x, y being Element of OSSub U0
for U1, U2 being strict OSSubAlgebra of U0 st x = U1 & y = U2 holds
b3 . (x,y) = U1 /\ U2 );
theorem Th43: :: OSALG_2:43
for S1 being OrderSortedSign
for U0 being non-empty OSAlgebra of S1
for x, y being Element of OSSub U0 holds (OSAlg_meet U0) . (x,y) = (MSAlg_meet U0) . (x,y)
proof
let S1 be OrderSortedSign; ::_thesis: for U0 being non-empty OSAlgebra of S1
for x, y being Element of OSSub U0 holds (OSAlg_meet U0) . (x,y) = (MSAlg_meet U0) . (x,y)
let U0 be non-empty OSAlgebra of S1; ::_thesis: for x, y being Element of OSSub U0 holds (OSAlg_meet U0) . (x,y) = (MSAlg_meet U0) . (x,y)
let x, y be Element of OSSub U0; ::_thesis: (OSAlg_meet U0) . (x,y) = (MSAlg_meet U0) . (x,y)
( x is strict OSSubAlgebra of U0 & y is strict OSSubAlgebra of U0 ) by Def14;
then consider U1, U2 being strict OSSubAlgebra of U0 such that
A1: ( x = U1 & y = U2 ) ;
(OSAlg_meet U0) . (x,y) = U1 /\ U2 by A1, Def16
.= (MSAlg_meet U0) . (x,y) by A1, MSUALG_2:def_21 ;
hence (OSAlg_meet U0) . (x,y) = (MSAlg_meet U0) . (x,y) ; ::_thesis: verum
end;
theorem Th44: :: OSALG_2:44
for S1 being OrderSortedSign
for U0 being non-empty OSAlgebra of S1 holds OSAlg_join U0 is commutative
proof
let S1 be OrderSortedSign; ::_thesis: for U0 being non-empty OSAlgebra of S1 holds OSAlg_join U0 is commutative
let U0 be non-empty OSAlgebra of S1; ::_thesis: OSAlg_join U0 is commutative
set o = OSAlg_join U0;
for x, y being Element of OSSub U0 holds (OSAlg_join U0) . (x,y) = (OSAlg_join U0) . (y,x)
proof
let x, y be Element of OSSub U0; ::_thesis: (OSAlg_join U0) . (x,y) = (OSAlg_join U0) . (y,x)
reconsider U1 = x, U2 = y as strict OSSubAlgebra of U0 by Def14;
set B = the Sorts of U1 \/ the Sorts of U2;
the Sorts of U2 is MSSubset of U0 by MSUALG_2:def_9;
then A1: the Sorts of U2 c= the Sorts of U0 by PBOOLE:def_18;
the Sorts of U1 is MSSubset of U0 by MSUALG_2:def_9;
then the Sorts of U1 c= the Sorts of U0 by PBOOLE:def_18;
then the Sorts of U1 \/ the Sorts of U2 c= the Sorts of U0 by A1, PBOOLE:16;
then A2: the Sorts of U1 \/ the Sorts of U2 is MSSubset of U0 by PBOOLE:def_18;
( the Sorts of U1 is OrderSortedSet of S1 & the Sorts of U2 is OrderSortedSet of S1 ) by OSALG_1:17;
then the Sorts of U1 \/ the Sorts of U2 is OrderSortedSet of S1 by Th2;
then reconsider B = the Sorts of U1 \/ the Sorts of U2 as OSSubset of U0 by A2, Def2;
A3: U1 "\/"_os U2 = GenOSAlg B by Def13;
( (OSAlg_join U0) . (x,y) = U1 "\/"_os U2 & (OSAlg_join U0) . (y,x) = U2 "\/"_os U1 ) by Def15;
hence (OSAlg_join U0) . (x,y) = (OSAlg_join U0) . (y,x) by A3, Def13; ::_thesis: verum
end;
hence OSAlg_join U0 is commutative by BINOP_1:def_2; ::_thesis: verum
end;
theorem Th45: :: OSALG_2:45
for S1 being OrderSortedSign
for U0 being non-empty OSAlgebra of S1 holds OSAlg_join U0 is associative
proof
let S1 be OrderSortedSign; ::_thesis: for U0 being non-empty OSAlgebra of S1 holds OSAlg_join U0 is associative
let U0 be non-empty OSAlgebra of S1; ::_thesis: OSAlg_join U0 is associative
set o = OSAlg_join U0;
for x, y, z being Element of OSSub U0 holds (OSAlg_join U0) . (x,((OSAlg_join U0) . (y,z))) = (OSAlg_join U0) . (((OSAlg_join U0) . (x,y)),z)
proof
let x, y, z be Element of OSSub U0; ::_thesis: (OSAlg_join U0) . (x,((OSAlg_join U0) . (y,z))) = (OSAlg_join U0) . (((OSAlg_join U0) . (x,y)),z)
reconsider U1 = x, U2 = y, U3 = z as strict OSSubAlgebra of U0 by Def14;
set B = the Sorts of U1 \/ ( the Sorts of U2 \/ the Sorts of U3);
A1: the Sorts of U2 is OrderSortedSet of S1 by OSALG_1:17;
the Sorts of U2 is MSSubset of U0 by MSUALG_2:def_9;
then A2: the Sorts of U2 c= the Sorts of U0 by PBOOLE:def_18;
the Sorts of U3 is MSSubset of U0 by MSUALG_2:def_9;
then the Sorts of U3 c= the Sorts of U0 by PBOOLE:def_18;
then A3: the Sorts of U2 \/ the Sorts of U3 c= the Sorts of U0 by A2, PBOOLE:16;
then reconsider C1 = the Sorts of U2 \/ the Sorts of U3 as MSSubset of U0 by PBOOLE:def_18;
the Sorts of U3 is OrderSortedSet of S1 by OSALG_1:17;
then A4: the Sorts of U2 \/ the Sorts of U3 is OrderSortedSet of S1 by A1, Th2;
then reconsider C = C1 as OSSubset of U0 by Def2;
A5: the Sorts of U1 is OrderSortedSet of S1 by OSALG_1:17;
then A6: the Sorts of U1 \/ ( the Sorts of U2 \/ the Sorts of U3) is OrderSortedSet of S1 by A4, Th2;
the Sorts of U1 is MSSubset of U0 by MSUALG_2:def_9;
then A7: the Sorts of U1 c= the Sorts of U0 by PBOOLE:def_18;
then the Sorts of U1 \/ the Sorts of U2 c= the Sorts of U0 by A2, PBOOLE:16;
then reconsider D1 = the Sorts of U1 \/ the Sorts of U2 as MSSubset of U0 by PBOOLE:def_18;
(OSAlg_join U0) . (y,z) = U2 "\/"_os U3 by Def15;
then A8: (OSAlg_join U0) . (x,((OSAlg_join U0) . (y,z))) = U1 "\/"_os (U2 "\/"_os U3) by Def15;
the Sorts of U1 \/ the Sorts of U2 is OrderSortedSet of S1 by A5, A1, Th2;
then reconsider D = D1 as OSSubset of U0 by Def2;
A9: (OSAlg_join U0) . (x,y) = U1 "\/"_os U2 by Def15;
the Sorts of U1 \/ ( the Sorts of U2 \/ the Sorts of U3) c= the Sorts of U0 by A7, A3, PBOOLE:16;
then the Sorts of U1 \/ ( the Sorts of U2 \/ the Sorts of U3) is MSSubset of U0 by PBOOLE:def_18;
then reconsider B = the Sorts of U1 \/ ( the Sorts of U2 \/ the Sorts of U3) as OSSubset of U0 by A6, Def2;
A10: B = D \/ the Sorts of U3 by PBOOLE:28;
A11: (U1 "\/"_os U2) "\/"_os U3 = (GenOSAlg D) "\/"_os U3 by Def13
.= GenOSAlg B by A10, Th37 ;
U1 "\/"_os (U2 "\/"_os U3) = U1 "\/"_os (GenOSAlg C) by Def13
.= (GenOSAlg C) "\/"_os U1 by Th39
.= GenOSAlg B by Th37 ;
hence (OSAlg_join U0) . (x,((OSAlg_join U0) . (y,z))) = (OSAlg_join U0) . (((OSAlg_join U0) . (x,y)),z) by A9, A8, A11, Def15; ::_thesis: verum
end;
hence OSAlg_join U0 is associative by BINOP_1:def_3; ::_thesis: verum
end;
theorem Th46: :: OSALG_2:46
for S1 being OrderSortedSign
for U0 being non-empty OSAlgebra of S1 holds OSAlg_meet U0 is commutative
proof
let S1 be OrderSortedSign; ::_thesis: for U0 being non-empty OSAlgebra of S1 holds OSAlg_meet U0 is commutative
let U0 be non-empty OSAlgebra of S1; ::_thesis: OSAlg_meet U0 is commutative
set o = OSAlg_meet U0;
set m = MSAlg_meet U0;
A1: MSAlg_meet U0 is commutative by MSUALG_2:31;
for x, y being Element of OSSub U0 holds (OSAlg_meet U0) . (x,y) = (OSAlg_meet U0) . (y,x)
proof
let x, y be Element of OSSub U0; ::_thesis: (OSAlg_meet U0) . (x,y) = (OSAlg_meet U0) . (y,x)
(OSAlg_meet U0) . (x,y) = (MSAlg_meet U0) . (x,y) by Th43
.= (MSAlg_meet U0) . (y,x) by A1, BINOP_1:def_2
.= (OSAlg_meet U0) . (y,x) by Th43 ;
hence (OSAlg_meet U0) . (x,y) = (OSAlg_meet U0) . (y,x) ; ::_thesis: verum
end;
hence OSAlg_meet U0 is commutative by BINOP_1:def_2; ::_thesis: verum
end;
theorem Th47: :: OSALG_2:47
for S1 being OrderSortedSign
for U0 being non-empty OSAlgebra of S1 holds OSAlg_meet U0 is associative
proof
let S1 be OrderSortedSign; ::_thesis: for U0 being non-empty OSAlgebra of S1 holds OSAlg_meet U0 is associative
let U0 be non-empty OSAlgebra of S1; ::_thesis: OSAlg_meet U0 is associative
set o = OSAlg_meet U0;
set m = MSAlg_meet U0;
A1: MSAlg_meet U0 is associative by MSUALG_2:32;
for x, y, z being Element of OSSub U0 holds (OSAlg_meet U0) . (x,((OSAlg_meet U0) . (y,z))) = (OSAlg_meet U0) . (((OSAlg_meet U0) . (x,y)),z)
proof
let x, y, z be Element of OSSub U0; ::_thesis: (OSAlg_meet U0) . (x,((OSAlg_meet U0) . (y,z))) = (OSAlg_meet U0) . (((OSAlg_meet U0) . (x,y)),z)
A2: (OSAlg_meet U0) . (x,y) = (MSAlg_meet U0) . (x,y) by Th43;
(OSAlg_meet U0) . (y,z) = (MSAlg_meet U0) . (y,z) by Th43;
then (OSAlg_meet U0) . (x,((OSAlg_meet U0) . (y,z))) = (MSAlg_meet U0) . (x,((MSAlg_meet U0) . (y,z))) by Th43
.= (MSAlg_meet U0) . (((MSAlg_meet U0) . (x,y)),z) by A1, BINOP_1:def_3
.= (OSAlg_meet U0) . (((OSAlg_meet U0) . (x,y)),z) by A2, Th43 ;
hence (OSAlg_meet U0) . (x,((OSAlg_meet U0) . (y,z))) = (OSAlg_meet U0) . (((OSAlg_meet U0) . (x,y)),z) ; ::_thesis: verum
end;
hence OSAlg_meet U0 is associative by BINOP_1:def_3; ::_thesis: verum
end;
definition
let S1 be OrderSortedSign;
let U0 be non-empty OSAlgebra of S1;
func OSSubAlLattice U0 -> strict Lattice equals :: OSALG_2:def 17
LattStr(# (OSSub U0),(OSAlg_join U0),(OSAlg_meet U0) #);
coherence
LattStr(# (OSSub U0),(OSAlg_join U0),(OSAlg_meet U0) #) is strict Lattice
proof
set L = LattStr(# (OSSub U0),(OSAlg_join U0),(OSAlg_meet U0) #);
A1: for a, b, c being Element of LattStr(# (OSSub U0),(OSAlg_join U0),(OSAlg_meet U0) #) holds a "\/" (b "\/" c) = (a "\/" b) "\/" c
proof
let a, b, c be Element of LattStr(# (OSSub U0),(OSAlg_join U0),(OSAlg_meet U0) #); ::_thesis: a "\/" (b "\/" c) = (a "\/" b) "\/" c
OSAlg_join U0 is associative by Th45;
hence a "\/" (b "\/" c) = (a "\/" b) "\/" c by BINOP_1:def_3; ::_thesis: verum
end;
A2: for a, b being Element of LattStr(# (OSSub U0),(OSAlg_join U0),(OSAlg_meet U0) #) holds a "/\" b = b "/\" a
proof
let a, b be Element of LattStr(# (OSSub U0),(OSAlg_join U0),(OSAlg_meet U0) #); ::_thesis: a "/\" b = b "/\" a
OSAlg_meet U0 is commutative by Th46;
hence a "/\" b = b "/\" a by BINOP_1:def_2; ::_thesis: verum
end;
A3: for a, b being Element of LattStr(# (OSSub U0),(OSAlg_join U0),(OSAlg_meet U0) #) holds a "/\" (a "\/" b) = a
proof
let a, b be Element of LattStr(# (OSSub U0),(OSAlg_join U0),(OSAlg_meet U0) #); ::_thesis: a "/\" (a "\/" b) = a
reconsider x = a, y = b as Element of OSSub U0 ;
(OSAlg_meet U0) . (x,((OSAlg_join U0) . (x,y))) = x
proof
reconsider U1 = x, U2 = y as strict OSSubAlgebra of U0 by Def14;
(OSAlg_join U0) . (x,y) = U1 "\/"_os U2 by Def15;
hence (OSAlg_meet U0) . (x,((OSAlg_join U0) . (x,y))) = U1 /\ (U1 "\/"_os U2) by Def16
.= x by Th40 ;
::_thesis: verum
end;
hence a "/\" (a "\/" b) = a ; ::_thesis: verum
end;
A4: for a, b being Element of LattStr(# (OSSub U0),(OSAlg_join U0),(OSAlg_meet U0) #) holds (a "/\" b) "\/" b = b
proof
let a, b be Element of LattStr(# (OSSub U0),(OSAlg_join U0),(OSAlg_meet U0) #); ::_thesis: (a "/\" b) "\/" b = b
reconsider x = a, y = b as Element of OSSub U0 ;
(OSAlg_join U0) . (((OSAlg_meet U0) . (x,y)),y) = y
proof
reconsider U1 = x, U2 = y as strict OSSubAlgebra of U0 by Def14;
(OSAlg_meet U0) . (x,y) = U1 /\ U2 by Def16;
hence (OSAlg_join U0) . (((OSAlg_meet U0) . (x,y)),y) = (U1 /\ U2) "\/"_os U2 by Def15
.= y by Th41 ;
::_thesis: verum
end;
hence (a "/\" b) "\/" b = b ; ::_thesis: verum
end;
A5: for a, b, c being Element of LattStr(# (OSSub U0),(OSAlg_join U0),(OSAlg_meet U0) #) holds a "/\" (b "/\" c) = (a "/\" b) "/\" c
proof
let a, b, c be Element of LattStr(# (OSSub U0),(OSAlg_join U0),(OSAlg_meet U0) #); ::_thesis: a "/\" (b "/\" c) = (a "/\" b) "/\" c
OSAlg_meet U0 is associative by Th47;
hence a "/\" (b "/\" c) = (a "/\" b) "/\" c by BINOP_1:def_3; ::_thesis: verum
end;
for a, b being Element of LattStr(# (OSSub U0),(OSAlg_join U0),(OSAlg_meet U0) #) holds a "\/" b = b "\/" a
proof
let a, b be Element of LattStr(# (OSSub U0),(OSAlg_join U0),(OSAlg_meet U0) #); ::_thesis: a "\/" b = b "\/" a
OSAlg_join U0 is commutative by Th44;
hence a "\/" b = b "\/" a by BINOP_1:def_2; ::_thesis: verum
end;
then ( LattStr(# (OSSub U0),(OSAlg_join U0),(OSAlg_meet U0) #) is strict & LattStr(# (OSSub U0),(OSAlg_join U0),(OSAlg_meet U0) #) is join-commutative & LattStr(# (OSSub U0),(OSAlg_join U0),(OSAlg_meet U0) #) is join-associative & LattStr(# (OSSub U0),(OSAlg_join U0),(OSAlg_meet U0) #) is meet-absorbing & LattStr(# (OSSub U0),(OSAlg_join U0),(OSAlg_meet U0) #) is meet-commutative & LattStr(# (OSSub U0),(OSAlg_join U0),(OSAlg_meet U0) #) is meet-associative & LattStr(# (OSSub U0),(OSAlg_join U0),(OSAlg_meet U0) #) is join-absorbing ) by A1, A4, A2, A5, A3, LATTICES:def_4, LATTICES:def_5, LATTICES:def_6, LATTICES:def_7, LATTICES:def_8, LATTICES:def_9;
hence LattStr(# (OSSub U0),(OSAlg_join U0),(OSAlg_meet U0) #) is strict Lattice ; ::_thesis: verum
end;
end;
:: deftheorem defines OSSubAlLattice OSALG_2:def_17_:_
for S1 being OrderSortedSign
for U0 being non-empty OSAlgebra of S1 holds OSSubAlLattice U0 = LattStr(# (OSSub U0),(OSAlg_join U0),(OSAlg_meet U0) #);
theorem Th48: :: OSALG_2:48
for S1 being OrderSortedSign
for U0 being non-empty OSAlgebra of S1 holds OSSubAlLattice U0 is bounded
proof
let S1 be OrderSortedSign; ::_thesis: for U0 being non-empty OSAlgebra of S1 holds OSSubAlLattice U0 is bounded
let U0 be non-empty OSAlgebra of S1; ::_thesis: OSSubAlLattice U0 is bounded
set L = OSSubAlLattice U0;
thus OSSubAlLattice U0 is lower-bounded :: according to LATTICES:def_15 ::_thesis: OSSubAlLattice U0 is upper-bounded
proof
set C = OSConstants U0;
reconsider G = GenOSAlg (OSConstants U0) as Element of OSSub U0 by Def14;
reconsider G1 = G as Element of (OSSubAlLattice U0) ;
take G1 ; :: according to LATTICES:def_13 ::_thesis: for b1 being Element of the carrier of (OSSubAlLattice U0) holds
( G1 "/\" b1 = G1 & b1 "/\" G1 = G1 )
let a be Element of (OSSubAlLattice U0); ::_thesis: ( G1 "/\" a = G1 & a "/\" G1 = G1 )
reconsider a1 = a as Element of OSSub U0 ;
reconsider a2 = a1 as strict OSSubAlgebra of U0 by Def14;
thus G1 "/\" a = (GenOSAlg (OSConstants U0)) /\ a2 by Def16
.= G1 by Th36 ; ::_thesis: a "/\" G1 = G1
hence a "/\" G1 = G1 ; ::_thesis: verum
end;
thus OSSubAlLattice U0 is upper-bounded ::_thesis: verum
proof
reconsider B = the Sorts of U0 as MSSubset of U0 by PBOOLE:def_18;
the Sorts of U0 is OrderSortedSet of S1 by OSALG_1:17;
then reconsider B = B as OSSubset of U0 by Def2;
reconsider G = GenOSAlg B as Element of OSSub U0 by Def14;
reconsider G1 = G as Element of (OSSubAlLattice U0) ;
take G1 ; :: according to LATTICES:def_14 ::_thesis: for b1 being Element of the carrier of (OSSubAlLattice U0) holds
( G1 "\/" b1 = G1 & b1 "\/" G1 = G1 )
let a be Element of (OSSubAlLattice U0); ::_thesis: ( G1 "\/" a = G1 & a "\/" G1 = G1 )
reconsider a1 = a as Element of OSSub U0 ;
reconsider a2 = a1 as strict OSSubAlgebra of U0 by Def14;
thus G1 "\/" a = (GenOSAlg B) "\/"_os a2 by Def15
.= G1 by Th38 ; ::_thesis: a "\/" G1 = G1
hence a "\/" G1 = G1 ; ::_thesis: verum
end;
end;
registration
let S1 be OrderSortedSign;
let U0 be non-empty OSAlgebra of S1;
cluster OSSubAlLattice U0 -> strict bounded ;
coherence
OSSubAlLattice U0 is bounded by Th48;
end;
theorem :: OSALG_2:49
for S1 being OrderSortedSign
for U0 being non-empty OSAlgebra of S1 holds Bottom (OSSubAlLattice U0) = GenOSAlg (OSConstants U0)
proof
let S1 be OrderSortedSign; ::_thesis: for U0 being non-empty OSAlgebra of S1 holds Bottom (OSSubAlLattice U0) = GenOSAlg (OSConstants U0)
let U0 be non-empty OSAlgebra of S1; ::_thesis: Bottom (OSSubAlLattice U0) = GenOSAlg (OSConstants U0)
set C = OSConstants U0;
reconsider G = GenOSAlg (OSConstants U0) as Element of OSSub U0 by Def14;
set L = OSSubAlLattice U0;
reconsider G1 = G as Element of (OSSubAlLattice U0) ;
now__::_thesis:_for_a_being_Element_of_(OSSubAlLattice_U0)_holds_
(_G1_"/\"_a_=_G1_&_a_"/\"_G1_=_G1_)
let a be Element of (OSSubAlLattice U0); ::_thesis: ( G1 "/\" a = G1 & a "/\" G1 = G1 )
reconsider a1 = a as Element of OSSub U0 ;
reconsider a2 = a1 as strict OSSubAlgebra of U0 by Def14;
thus G1 "/\" a = (GenOSAlg (OSConstants U0)) /\ a2 by Def16
.= G1 by Th36 ; ::_thesis: a "/\" G1 = G1
hence a "/\" G1 = G1 ; ::_thesis: verum
end;
hence Bottom (OSSubAlLattice U0) = GenOSAlg (OSConstants U0) by LATTICES:def_16; ::_thesis: verum
end;
theorem Th50: :: OSALG_2:50
for S1 being OrderSortedSign
for U0 being non-empty OSAlgebra of S1
for B being OSSubset of U0 st B = the Sorts of U0 holds
Top (OSSubAlLattice U0) = GenOSAlg B
proof
let S1 be OrderSortedSign; ::_thesis: for U0 being non-empty OSAlgebra of S1
for B being OSSubset of U0 st B = the Sorts of U0 holds
Top (OSSubAlLattice U0) = GenOSAlg B
let U0 be non-empty OSAlgebra of S1; ::_thesis: for B being OSSubset of U0 st B = the Sorts of U0 holds
Top (OSSubAlLattice U0) = GenOSAlg B
let B be OSSubset of U0; ::_thesis: ( B = the Sorts of U0 implies Top (OSSubAlLattice U0) = GenOSAlg B )
reconsider G = GenOSAlg B as Element of OSSub U0 by Def14;
set L = OSSubAlLattice U0;
reconsider G1 = G as Element of (OSSubAlLattice U0) ;
assume A1: B = the Sorts of U0 ; ::_thesis: Top (OSSubAlLattice U0) = GenOSAlg B
now__::_thesis:_for_a_being_Element_of_(OSSubAlLattice_U0)_holds_
(_G1_"\/"_a_=_G1_&_a_"\/"_G1_=_G1_)
let a be Element of (OSSubAlLattice U0); ::_thesis: ( G1 "\/" a = G1 & a "\/" G1 = G1 )
reconsider a1 = a as Element of OSSub U0 ;
reconsider a2 = a1 as strict OSSubAlgebra of U0 by Def14;
thus G1 "\/" a = (GenOSAlg B) "\/"_os a2 by Def15
.= G1 by A1, Th38 ; ::_thesis: a "\/" G1 = G1
hence a "\/" G1 = G1 ; ::_thesis: verum
end;
hence Top (OSSubAlLattice U0) = GenOSAlg B by LATTICES:def_17; ::_thesis: verum
end;
theorem :: OSALG_2:51
for S1 being OrderSortedSign
for U0 being strict non-empty OSAlgebra of S1 holds Top (OSSubAlLattice U0) = U0
proof
let S1 be OrderSortedSign; ::_thesis: for U0 being strict non-empty OSAlgebra of S1 holds Top (OSSubAlLattice U0) = U0
let U0 be strict non-empty OSAlgebra of S1; ::_thesis: Top (OSSubAlLattice U0) = U0
reconsider B = the Sorts of U0 as MSSubset of U0 by PBOOLE:def_18;
B is OrderSortedSet of S1 by OSALG_1:17;
then reconsider B = the Sorts of U0 as OSSubset of U0 by Def2;
thus Top (OSSubAlLattice U0) = GenOSAlg B by Th50
.= U0 by Th34 ; ::_thesis: verum
end;