let S be 1-sorted ; :: thesis: 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; :: thesis: 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 MS being MSSubsetFamily of the Sorts of D such that
A1:
MS = MSFixPoints (ClSys->ClOp D)
and
A2:
ClOp->ClSys (ClSys->ClOp D) = MSClosureStr(# the Sorts of D,MS #)
by Def14;
consider X1 being ManySortedSet of such that
A3:
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)
:: according to PBOOLE:def 13 :: thesis: MSFixPoints (ClSys->ClOp D) c= the Family of Dproof
let i be
set ;
:: according to PBOOLE:def 5 :: thesis: ( not i in the carrier of S or the Family of D . i c= (MSFixPoints (ClSys->ClOp D)) . i )
assume A4:
i in the
carrier of
S
;
:: thesis: the Family of D . i c= (MSFixPoints (ClSys->ClOp D)) . i
let x be
set ;
:: according to TARSKI:def 3 :: thesis: ( not x in the Family of D . i or x in (MSFixPoints (ClSys->ClOp D)) . i )
assume A5:
x in the
Family of
D . i
;
:: thesis: x in (MSFixPoints (ClSys->ClOp D)) . i
dom (X1 +* (i .--> x)) = the
carrier of
S
by A4, PZFMISC1:1;
then reconsider X =
X1 +* (i .--> x) as
ManySortedSet of
by PARTFUN1:def 4, RELAT_1:def 18;
A6:
dom (i .--> x) = {i}
by FUNCOP_1:19;
i in {i}
by TARSKI:def 1;
then A7:
X . i =
(i .--> x) . i
by A6, FUNCT_4:14
.=
x
by FUNCOP_1:87
;
the
Family of
D c= bool the
Sorts of
D
by PBOOLE:def 23;
then A8:
the
Family of
D . i c= (bool the Sorts of D) . i
by A4, PBOOLE:def 5;
then A9:
x in (bool the Sorts of D) . i
by A5;
X is
Element of
bool the
Sorts of
D
then reconsider X =
X as
Element of
bool the
Sorts of
D ;
reconsider Fi = the
Family of
D . i as non
empty set by A4;
reconsider f =
(ClSys->ClOp D) . i as
Function of
((bool the Sorts of D) . i),
((bool the Sorts of D) . i) by A4, PBOOLE:def 18;
consider SF being
V8()
MSSubsetFamily of the
Sorts of
D such that A11:
for
Y being
ManySortedSet of 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 A12:
Q = SF . i
and A13:
(meet SF) . i = Intersect Q
by A4, MSSUBFAM:def 2;
A14:
x in dom f
by A9, FUNCT_2:def 1;
A15:
SF . i = { z where z is Element of Fi : X . i c= z }
by A4, A11, Th32;
A16:
Intersect Q = x
A19:
(ClSys->ClOp D) .. X = meet SF
by A11, Def15;
dom (ClSys->ClOp D) = the
carrier of
S
by PARTFUN1:def 4;
then
f . x = x
by A4, A7, A13, A16, A19, PRALG_1:def 17;
hence
x in (MSFixPoints (ClSys->ClOp D)) . i
by A4, A14, Def13;
:: thesis: verum
end;
let i be
set ;
:: according to PBOOLE:def 5 :: thesis: ( not i in the carrier of S or (MSFixPoints (ClSys->ClOp D)) . i c= the Family of D . i )
assume A20:
i in the
carrier of
S
;
:: thesis: (MSFixPoints (ClSys->ClOp D)) . i c= the Family of D . i
let x be
set ;
:: according to TARSKI:def 3 :: thesis: ( not x in (MSFixPoints (ClSys->ClOp D)) . i or x in the Family of D . i )
assume A21:
x in (MSFixPoints (ClSys->ClOp D)) . i
;
:: thesis: x in the Family of D . i
then consider f being
Function such that A22:
(
f = (ClSys->ClOp D) . i &
x in dom f &
f . x = x )
by A20, Def13;
dom (X1 +* (i .--> x)) = the
carrier of
S
by A20, PZFMISC1:1;
then reconsider X =
X1 +* (i .--> x) as
ManySortedSet of
by PARTFUN1:def 4, RELAT_1:def 18;
A23:
dom (i .--> x) = {i}
by FUNCOP_1:19;
i in {i}
by TARSKI:def 1;
then A24:
X . i =
(i .--> x) . i
by A23, FUNCT_4:14
.=
x
by FUNCOP_1:87
;
MSFixPoints (ClSys->ClOp D) c= bool the
Sorts of
D
by PBOOLE:def 23;
then A25:
(MSFixPoints (ClSys->ClOp D)) . i c= (bool the Sorts of D) . i
by A20, PBOOLE:def 5;
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 A27:
for
Y being
ManySortedSet of holds
(
Y in SF iff (
Y in the
Family of
D &
X c= Y ) )
by Th31;
A28:
dom (ClSys->ClOp D) = the
carrier of
S
by PARTFUN1:def 4;
A29:
(meet SF) . i =
((ClSys->ClOp D) .. X) . i
by A27, Def15
.=
x
by A20, A22, A24, A28, PRALG_1:def 17
;
defpred S1[
ManySortedSet of ]
means X c= $1;
( ( for
Y being
ManySortedSet of 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
meet SF in the
Family of
D
by A27, MSSUBFAM:def 6;
hence
x in the
Family of
D . i
by A20, A29, PBOOLE:def 4;
:: thesis: verum
end;
hence
ClOp->ClSys (ClSys->ClOp D) = MSClosureStr(# the Sorts of D,the Family of D #)
by A1, A2; :: thesis: verum