let S be 1-sorted ; for D being MSClosureSystem of S holds ClOp->ClSys (ClSys->ClOp D) = MSClosureStr(# the Sorts of D,the Family of D #)
let D be MSClosureSystem of S; ClOp->ClSys (ClSys->ClOp D) = MSClosureStr(# the Sorts of D,the Family of D #)
set M = the Sorts of D;
set F = the Family of D;
set I = the carrier of S;
consider X1 being ManySortedSet of the carrier of S such that
A1:
X1 in bool the Sorts of D
by PBOOLE:146;
the Family of D = MSFixPoints (ClSys->ClOp D)
proof
thus
the
Family of
D c= MSFixPoints (ClSys->ClOp D)
PBOOLE:def 13 MSFixPoints (ClSys->ClOp D) c= the Family of Dproof
A2:
dom (ClSys->ClOp D) = the
carrier of
S
by PARTFUN1:def 4;
let i be
set ;
PBOOLE:def 5 ( not i in the carrier of S or the Family of D . i c= (MSFixPoints (ClSys->ClOp D)) . i )
assume A3:
i in the
carrier of
S
;
the Family of D . i c= (MSFixPoints (ClSys->ClOp D)) . i
reconsider f =
(ClSys->ClOp D) . i as
Function of
((bool the Sorts of D) . i),
((bool the Sorts of D) . i) by A3, PBOOLE:def 18;
reconsider Fi = the
Family of
D . i as non
empty set by A3;
let x be
set ;
TARSKI:def 3 ( not x in the Family of D . i or x in (MSFixPoints (ClSys->ClOp D)) . i )
assume A4:
x in the
Family of
D . i
;
x in (MSFixPoints (ClSys->ClOp D)) . i
dom (X1 +* (i .--> x)) = the
carrier of
S
by A3, PZFMISC1:1;
then reconsider X =
X1 +* (i .--> x) as
ManySortedSet of the
carrier of
S by PARTFUN1:def 4, RELAT_1:def 18;
A5:
dom (i .--> x) = {i}
by FUNCOP_1:19;
the
Family of
D c= bool the
Sorts of
D
by PBOOLE:def 23;
then A6:
the
Family of
D . i c= (bool the Sorts of D) . i
by A3, PBOOLE:def 5;
then
x in (bool the Sorts of D) . i
by A4;
then A7:
x in dom f
by FUNCT_2:def 1;
i in {i}
by TARSKI:def 1;
then A8:
X . i =
(i .--> x) . i
by A5, FUNCT_4:14
.=
x
by FUNCOP_1:87
;
X is
Element of
bool the
Sorts of
D
then reconsider X =
X as
Element of
bool the
Sorts of
D ;
consider SF being
V8()
MSSubsetFamily of the
Sorts of
D such that A10:
for
Y being
ManySortedSet of the
carrier of
S holds
(
Y in SF iff (
Y in the
Family of
D &
X c= Y ) )
by Th31;
consider Q being
Subset-Family of
(the Sorts of D . i) such that A11:
Q = SF . i
and A12:
(meet SF) . i = Intersect Q
by A3, MSSUBFAM:def 2;
A13:
SF . i = { z where z is Element of Fi : X . i c= z }
by A3, A10, Th32;
then A14:
x c= Intersect Q
by A3, A11, MSSUBFAM:5;
x in { B where B is Element of Fi : x c= B }
by A4;
then
Intersect Q c= x
by A8, A11, A13, MSSUBFAM:2;
then A15:
Intersect Q = x
by A14, XBOOLE_0:def 10;
(ClSys->ClOp D) .. X = meet SF
by A10, Def15;
then
f . x = x
by A3, A8, A12, A15, A2, PRALG_1:def 17;
hence
x in (MSFixPoints (ClSys->ClOp D)) . i
by A3, A7, Def13;
verum
end;
let i be
set ;
PBOOLE:def 5 ( not i in the carrier of S or (MSFixPoints (ClSys->ClOp D)) . i c= the Family of D . i )
assume A16:
i in the
carrier of
S
;
(MSFixPoints (ClSys->ClOp D)) . i c= the Family of D . i
let x be
set ;
TARSKI:def 3 ( not x in (MSFixPoints (ClSys->ClOp D)) . i or x in the Family of D . i )
assume A17:
x in (MSFixPoints (ClSys->ClOp D)) . i
;
x in the Family of D . i
then A18:
ex
f being
Function st
(
f = (ClSys->ClOp D) . i &
x in dom f &
f . x = x )
by A16, Def13;
dom (X1 +* (i .--> x)) = the
carrier of
S
by A16, PZFMISC1:1;
then reconsider X =
X1 +* (i .--> x) as
ManySortedSet of the
carrier of
S by PARTFUN1:def 4, RELAT_1:def 18;
A19:
dom (i .--> x) = {i}
by FUNCOP_1:19;
i in {i}
by TARSKI:def 1;
then A20:
X . i =
(i .--> x) . i
by A19, FUNCT_4:14
.=
x
by FUNCOP_1:87
;
MSFixPoints (ClSys->ClOp D) c= bool the
Sorts of
D
by PBOOLE:def 23;
then A21:
(MSFixPoints (ClSys->ClOp D)) . i c= (bool the Sorts of D) . i
by A16, PBOOLE:def 5;
X is
Element of
bool the
Sorts of
D
then reconsider X =
X as
Element of
bool the
Sorts of
D ;
defpred S1[
ManySortedSet of the
carrier of
S]
means X c= $1;
consider SF being
V8()
MSSubsetFamily of the
Sorts of
D such that A23:
for
Y being
ManySortedSet of the
carrier of
S holds
(
Y in SF iff (
Y in the
Family of
D &
X c= Y ) )
by Th31;
A24:
dom (ClSys->ClOp D) = the
carrier of
S
by PARTFUN1:def 4;
( ( for
Y being
ManySortedSet of the
carrier of
S holds
(
Y in SF iff (
Y in the
Family of
D &
S1[
Y] ) ) ) implies
SF c= the
Family of
D )
from CLOSURE1:sch 1();
then A25:
meet SF in the
Family of
D
by A23, MSSUBFAM:def 6;
(meet SF) . i =
((ClSys->ClOp D) .. X) . i
by A23, Def15
.=
x
by A16, A18, A20, A24, PRALG_1:def 17
;
hence
x in the
Family of
D . i
by A16, A25, PBOOLE:def 4;
verum
end;
hence
ClOp->ClSys (ClSys->ClOp D) = MSClosureStr(# the Sorts of D,the Family of D #)
by Def14; verum