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:134;
the Family of D = MSFixPoints (ClSys->ClOp D)
proof
let i be
object ;
PBOOLE:def 10 ( not i in the carrier of S or the Family of D . i = (MSFixPoints (ClSys->ClOp D)) . i )
assume A3:
i in the
carrier of
S
;
the Family of D . i = (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 15;
reconsider Fi = the
Family of
D . i as non
empty set by A3;
thus
the
Family of
D . i c= (MSFixPoints (ClSys->ClOp D)) . i
XBOOLE_0:def 10 (MSFixPoints (ClSys->ClOp D)) . i c= the Family of D . iproof
let x be
object ;
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
reconsider xx =
x as
set by TARSKI:1;
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 2, RELAT_1:def 18;
A5:
dom (i .--> x) = {i}
;
the
Family of
D c= bool the
Sorts of
D
by PBOOLE:def 18;
then A6:
the
Family of
D . i c= (bool the Sorts of D) . i
by A3;
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:13
.=
x
by FUNCOP_1:72
;
X is
Element of
bool the
Sorts of
D
then reconsider X =
X as
Element of
bool the
Sorts of
D ;
consider SF being
non-empty 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 1;
A13:
SF . i = { z where z is Element of Fi : X . i c= z }
by A3, A10, Th32;
now for Z1 being set st Z1 in Q holds
xx c= Z1let Z1 be
set ;
( Z1 in Q implies xx c= Z1 )assume
Z1 in Q
;
xx c= Z1then
ex
q being
Element of
Fi st
(
q = Z1 &
X . i c= q )
by A11, A13;
hence
xx c= Z1
by A8;
verum end;
then A14:
xx c= Intersect Q
by A3, A11, MSSUBFAM:5;
x in { B where B is Element of Fi : xx c= B }
by A4;
then
Intersect Q c= xx
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, Def14;
then
f . x = x
by A3, A8, A12, A15, PRALG_1:def 20;
hence
x in (MSFixPoints (ClSys->ClOp D)) . i
by A3, A7, Def12;
verum
end;
let x be
object ;
TARSKI:def 3 ( not x in (MSFixPoints (ClSys->ClOp D)) . i or x in the Family of D . i )
assume A16:
x in (MSFixPoints (ClSys->ClOp D)) . i
;
x in the Family of D . i
then A17:
ex
f being
Function st
(
f = (ClSys->ClOp D) . i &
x in dom f &
f . x = x )
by A3, Def12;
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 2, RELAT_1:def 18;
A18:
dom (i .--> x) = {i}
;
i in {i}
by TARSKI:def 1;
then A19:
X . i =
(i .--> x) . i
by A18, FUNCT_4:13
.=
x
by FUNCOP_1:72
;
MSFixPoints (ClSys->ClOp D) c= bool the
Sorts of
D
by PBOOLE:def 18;
then A20:
(MSFixPoints (ClSys->ClOp D)) . i c= (bool the Sorts of D) . i
by A3;
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
non-empty MSSubsetFamily of the
Sorts of
D such that A22:
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;
( ( 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 A24:
meet SF in the
Family of
D
by A22, MSSUBFAM:def 5;
(meet SF) . i =
((ClSys->ClOp D) .. X) . i
by A22, Def14
.=
x
by A3, A17, A19, PRALG_1:def 20
;
hence
x in the
Family of
D . i
by A3, A24;
verum
end;
hence
ClOp->ClSys (ClSys->ClOp D) = MSClosureStr(# the Sorts of D, the Family of D #)
by Def13; verum