let S be non empty non void ManySortedSign ; :: thesis: for MA being strict non-empty MSAlgebra of S
for F being SubsetFamily of the Sorts of MA st F c= SubSort MA holds
for B being MSSubset of MA st B = meet |:F:| holds
B is opers_closed
let MA be strict non-empty MSAlgebra of S; :: thesis: for F being SubsetFamily of the Sorts of MA st F c= SubSort MA holds
for B being MSSubset of MA st B = meet |:F:| holds
B is opers_closed
let F be SubsetFamily of the Sorts of MA; :: thesis: ( F c= SubSort MA implies for B being MSSubset of MA st B = meet |:F:| holds
B is opers_closed )
assume A1:
F c= SubSort MA
; :: thesis: for B being MSSubset of MA st B = meet |:F:| holds
B is opers_closed
let B be MSSubset of MA; :: thesis: ( B = meet |:F:| implies B is opers_closed )
assume A2:
B = meet |:F:|
; :: thesis: B is opers_closed
per cases
( F = {} or F <> {} )
;
suppose A3:
F = {}
;
:: thesis: B is opers_closed set I = the
carrier of
S;
reconsider FF =
|:F:| as
MSSubsetFamily of the
Sorts of
MA ;
A4:
FF = [0] the
carrier of
S
by A3, CLOSURE2:def 4;
set Q = the
Sorts of
MA;
A5:
the
Sorts of
MA = B
by A2, A4, MSSUBFAM:41;
reconsider Q = the
Sorts of
MA as
MSSubset of
MA by PBOOLE:def 23;
for
o being
OperSymbol of
S holds
Q is_closed_on o
proof
let o be
OperSymbol of
S;
:: thesis: Q is_closed_on o
A7:
( the
Arity of
S . o = the_arity_of o & the
ResultSort of
S . o = the_result_sort_of o )
by MSUALG_1:def 6, MSUALG_1:def 7;
A8:
dom the
Arity of
S = the
carrier' of
S
by FUNCT_2:def 1;
A9:
dom the
ResultSort of
S = the
carrier' of
S
by FUNCT_2:def 1;
A10:
((Q # ) * the Arity of S) . o = (Q # ) . (the_arity_of o)
by A7, A8, FUNCT_1:23;
A11:
(Q * the ResultSort of S) . o = Q . (the_result_sort_of o)
by A7, A9, FUNCT_1:23;
Result o,
MA =
(Q * the ResultSort of S) . o
by MSUALG_1:def 10
.=
Q . (the_result_sort_of o)
by A7, A9, FUNCT_1:23
;
then
rng ((Den o,MA) | ((Q # ) . (the_arity_of o))) c= Q . (the_result_sort_of o)
by RELAT_1:def 19;
hence
Q is_closed_on o
by A10, A11, MSUALG_2:def 6;
:: thesis: verum
end; hence
B is
opers_closed
by A5, MSUALG_2:def 7;
:: thesis: verum end; suppose A12:
F <> {}
;
:: thesis: B is opers_closed set SS =
S;
let o be
OperSymbol of
S;
:: according to MSUALG_2:def 7 :: thesis: B is_closed_on oset i =
the_result_sort_of o;
A14:
( the
Arity of
S . o = the_arity_of o & the
ResultSort of
S . o = the_result_sort_of o )
by MSUALG_1:def 6, MSUALG_1:def 7;
A15:
dom the
Arity of
S = the
carrier' of
S
by FUNCT_2:def 1;
A16:
dom the
ResultSort of
S = the
carrier' of
S
by FUNCT_2:def 1;
A17:
((B # ) * the Arity of S) . o = (B # ) . (the_arity_of o)
by A14, A15, FUNCT_1:23;
A18:
(B * the ResultSort of S) . o = B . (the_result_sort_of o)
by A14, A16, FUNCT_1:23;
Result o,
MA =
(the Sorts of MA * the ResultSort of S) . o
by MSUALG_1:def 10
.=
the
Sorts of
MA . (the_result_sort_of o)
by A14, A16, FUNCT_1:23
;
then A19:
rng ((Den o,MA) | ((B # ) . (the_arity_of o))) c= the
Sorts of
MA . (the_result_sort_of o)
by RELAT_1:def 19;
rng ((Den o,MA) | ((B # ) . (the_arity_of o))) c= B . (the_result_sort_of o)
proof
let v be
set ;
:: according to TARSKI:def 3 :: thesis: ( not v in rng ((Den o,MA) | ((B # ) . (the_arity_of o))) or v in B . (the_result_sort_of o) )
assume A20:
v in rng ((Den o,MA) | ((B # ) . (the_arity_of o)))
;
:: thesis: v in B . (the_result_sort_of o)
then consider p being
set such that A21:
(
p in dom ((Den o,MA) | ((B # ) . (the_arity_of o))) &
v = ((Den o,MA) | ((B # ) . (the_arity_of o))) . p )
by FUNCT_1:def 5;
consider Q being
Subset-Family of
(the Sorts of MA . (the_result_sort_of o)) such that A22:
Q = |:F:| . (the_result_sort_of o)
and A23:
B . (the_result_sort_of o) = Intersect Q
by A2, MSSUBFAM:def 2;
for
Y being
set st
Y in Q holds
v in Y
proof
let Y be
set ;
:: thesis: ( Y in Q implies v in Y )
assume A24:
Y in Q
;
:: thesis: v in Y
|:F:| . (the_result_sort_of o) = { (xx . (the_result_sort_of o)) where xx is Element of Bool the Sorts of MA : xx in F }
by A12, CLOSURE2:15;
then consider xx being
Element of
Bool the
Sorts of
MA such that A25:
(
Y = xx . (the_result_sort_of o) &
xx in F )
by A22, A24;
reconsider xx =
xx as
MSSubset of
MA ;
xx is
opers_closed
by A1, A25, MSUALG_2:15;
then
xx is_closed_on o
by MSUALG_2:def 7;
then A26:
rng ((Den o,MA) | (((xx # ) * the Arity of S) . o)) c= (xx * the ResultSort of S) . o
by MSUALG_2:def 6;
B c= xx
by A2, A25, CLOSURE2:22, MSSUBFAM:43;
then
(Den o,MA) | (((B # ) * the Arity of S) . o) c= (Den o,MA) | (((xx # ) * the Arity of S) . o)
by MSUALG_2:3, RELAT_1:104;
then A27:
dom ((Den o,MA) | (((B # ) * the Arity of S) . o)) c= dom ((Den o,MA) | (((xx # ) * the Arity of S) . o))
by RELAT_1:25;
A28:
v = (Den o,MA) . p
by A21, FUNCT_1:70;
then
v = ((Den o,MA) | (((xx # ) * the Arity of S) . o)) . p
by A17, A21, A27, FUNCT_1:70;
then
v in rng ((Den o,MA) | (((xx # ) * the Arity of S) . o))
by A17, A21, A27, FUNCT_1:def 5;
then
(Den o,MA) . p in (xx * the ResultSort of S) . o
by A26, A28;
then
(Den o,MA) . p in xx . (the ResultSort of S . o)
by A16, FUNCT_1:23;
then
(Den o,MA) . p in xx . (the_result_sort_of o)
by MSUALG_1:def 7;
hence
v in Y
by A21, A25, FUNCT_1:70;
:: thesis: verum
end;
hence
v in B . (the_result_sort_of o)
by A19, A20, A23, SETFAM_1:58;
:: thesis: verum
end; hence
B is_closed_on o
by A17, A18, MSUALG_2:def 6;
:: thesis: verum end;