:: CLOSURE2 semantic presentation
begin
notation
let I be set ;
let A, B be ManySortedSet of I;
synonym A in' B for A in B;
end;
notation
let I be set ;
let A, B be ManySortedSet of I;
synonym A c=' B for A c= B;
end;
theorem :: CLOSURE2:1
for M being non empty set
for X, Y being Element of M st X c= Y holds
(id M) . X c= (id M) . Y
proof
let M be non empty set ; ::_thesis: for X, Y being Element of M st X c= Y holds
(id M) . X c= (id M) . Y
let X, Y be Element of M; ::_thesis: ( X c= Y implies (id M) . X c= (id M) . Y )
assume A1: X c= Y ; ::_thesis: (id M) . X c= (id M) . Y
(id M) . X = X by FUNCT_1:18;
hence (id M) . X c= (id M) . Y by A1, FUNCT_1:18; ::_thesis: verum
end;
theorem Th2: :: CLOSURE2:2
for I being non empty set
for A being ManySortedSet of I
for B being ManySortedSubset of A holds rng B c= union (rng (bool A))
proof
let I be non empty set ; ::_thesis: for A being ManySortedSet of I
for B being ManySortedSubset of A holds rng B c= union (rng (bool A))
let A be ManySortedSet of I; ::_thesis: for B being ManySortedSubset of A holds rng B c= union (rng (bool A))
let B be ManySortedSubset of A; ::_thesis: rng B c= union (rng (bool A))
let a be set ; :: according to TARSKI:def_3 ::_thesis: ( not a in rng B or a in union (rng (bool A)) )
assume a in rng B ; ::_thesis: a in union (rng (bool A))
then consider i being set such that
A1: i in I and
A2: a = B . i by PBOOLE:138;
( i in dom (bool A) & bool (A . i) = (bool A) . i ) by A1, MBOOLEAN:def_1, PARTFUN1:def_2;
then A3: bool (A . i) in rng (bool A) by FUNCT_1:def_3;
B c= A by PBOOLE:def_18;
then B in bool A by MBOOLEAN:18;
then B . i in (bool A) . i by A1, PBOOLE:def_1;
then a in bool (A . i) by A1, A2, MBOOLEAN:def_1;
hence a in union (rng (bool A)) by A3, TARSKI:def_4; ::_thesis: verum
end;
begin
definition
let I be set ;
let M be ManySortedSet of I;
defpred S1[ set ] means $1 is ManySortedSubset of M;
func Bool M -> set means :Def1: :: CLOSURE2:def 1
for x being set holds
( x in it iff x is ManySortedSubset of M );
existence
ex b1 being set st
for x being set holds
( x in b1 iff x is ManySortedSubset of M )
proof
percases ( not I is empty or I is empty ) ;
supposeA1: not I is empty ; ::_thesis: ex b1 being set st
for x being set holds
( x in b1 iff x is ManySortedSubset of M )
consider X being set such that
A2: for e being set holds
( e in X iff ( e in Funcs (I,(union (rng (bool M)))) & S1[e] ) ) from XBOOLE_0:sch_1();
take X ; ::_thesis: for x being set holds
( x in X iff x is ManySortedSubset of M )
thus for x being set holds
( x in X iff x is ManySortedSubset of M ) ::_thesis: verum
proof
let x be set ; ::_thesis: ( x in X iff x is ManySortedSubset of M )
thus ( x in X implies x is ManySortedSubset of M ) by A2; ::_thesis: ( x is ManySortedSubset of M implies x in X )
assume A3: x is ManySortedSubset of M ; ::_thesis: x in X
now__::_thesis:_(_x_in_Funcs_(I,(union_(rng_(bool_M))))_&_S1[x]_)
reconsider xx = x as ManySortedSubset of M by A3;
( dom xx = I & rng xx c= union (rng (bool M)) ) by A1, Th2, PARTFUN1:def_2;
hence x in Funcs (I,(union (rng (bool M)))) by FUNCT_2:def_2; ::_thesis: S1[x]
thus S1[x] by A3; ::_thesis: verum
end;
hence x in X by A2; ::_thesis: verum
end;
end;
supposeA4: I is empty ; ::_thesis: ex b1 being set st
for x being set holds
( x in b1 iff x is ManySortedSubset of M )
take {([[0]] {})} ; ::_thesis: for x being set holds
( x in {([[0]] {})} iff x is ManySortedSubset of M )
thus for x being set holds
( x in {([[0]] {})} iff x is ManySortedSubset of M ) ::_thesis: verum
proof
let x be set ; ::_thesis: ( x in {([[0]] {})} iff x is ManySortedSubset of M )
thus ( x in {([[0]] {})} implies x is ManySortedSubset of M ) ::_thesis: ( x is ManySortedSubset of M implies x in {([[0]] {})} )
proof
reconsider M9 = M as ManySortedSet of {} by A4;
assume A6: x in {([[0]] {})} ; ::_thesis: x is ManySortedSubset of M
reconsider y = [[0]] {} as ManySortedSubset of M9 by PBOOLE:def_18;
y is ManySortedSubset of M by A4;
hence x is ManySortedSubset of M by A6, TARSKI:def_1; ::_thesis: verum
end;
assume x is ManySortedSubset of M ; ::_thesis: x in {([[0]] {})}
then consider y being ManySortedSubset of M such that
A7: y = x ;
y = [[0]] {} by A4;
hence x in {([[0]] {})} by A7, TARSKI:def_1; ::_thesis: verum
end;
end;
end;
end;
uniqueness
for b1, b2 being set st ( for x being set holds
( x in b1 iff x is ManySortedSubset of M ) ) & ( for x being set holds
( x in b2 iff x is ManySortedSubset of M ) ) holds
b1 = b2
proof
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 Def1 defines Bool CLOSURE2:def_1_:_
for I being set
for M being ManySortedSet of I
for b3 being set holds
( b3 = Bool M iff for x being set holds
( x in b3 iff x is ManySortedSubset of M ) );
registration
let I be set ;
let M be ManySortedSet of I;
cluster Bool M -> non empty functional with_common_domain ;
coherence
( not Bool M is empty & Bool M is functional & Bool M is with_common_domain )
proof
M is ManySortedSubset of M by PBOOLE:def_18;
hence not Bool M is empty by Def1; ::_thesis: ( Bool M is functional & Bool M is with_common_domain )
thus Bool M is functional ::_thesis: Bool M is with_common_domain
proof
let x be set ; :: according to FUNCT_1:def_13 ::_thesis: ( not x in Bool M or x is set )
assume x in Bool M ; ::_thesis: x is set
hence x is set by Def1; ::_thesis: verum
end;
let f, g be Function; :: according to CARD_3:def_10 ::_thesis: ( not f in Bool M or not g in Bool M or dom f = dom g )
assume that
A1: f in Bool M and
A2: g in Bool M ; ::_thesis: dom f = dom g
A3: g is ManySortedSubset of M by A2, Def1;
f is ManySortedSubset of M by A1, Def1;
hence dom f = I by PARTFUN1:def_2
.= dom g by A3, PARTFUN1:def_2 ;
::_thesis: verum
end;
end;
definition
let I be set ;
let M be ManySortedSet of I;
mode SubsetFamily of M is Subset of (Bool M);
end;
definition
let I be set ;
let M be ManySortedSet of I;
:: original: Bool
redefine func Bool M -> SubsetFamily of M;
coherence
Bool M is SubsetFamily of M
proof
Bool M c= Bool M ;
hence Bool M is SubsetFamily of M ; ::_thesis: verum
end;
end;
registration
let I be set ;
let M be ManySortedSet of I;
cluster non empty functional with_common_domain for Element of bool (Bool M);
existence
ex b1 being SubsetFamily of M st
( not b1 is empty & b1 is functional & b1 is with_common_domain )
proof
take Bool M ; ::_thesis: ( not Bool M is empty & Bool M is functional & Bool M is with_common_domain )
thus ( not Bool M is empty & Bool M is functional & Bool M is with_common_domain ) ; ::_thesis: verum
end;
end;
registration
let I be set ;
let M be ManySortedSet of I;
cluster empty functional finite for Element of bool (Bool M);
existence
ex b1 being SubsetFamily of M st
( b1 is empty & b1 is finite )
proof
reconsider x = {} as SubsetFamily of M by XBOOLE_1:2;
take x ; ::_thesis: ( x is empty & x is finite )
thus ( x is empty & x is finite ) ; ::_thesis: verum
end;
end;
definition
let I be set ;
let M be ManySortedSet of I;
let S be non empty SubsetFamily of M;
:: original: Element
redefine mode Element of S -> ManySortedSubset of M;
coherence
for b1 being Element of S holds b1 is ManySortedSubset of M
proof
let e be Element of S; ::_thesis: e is ManySortedSubset of M
thus e is ManySortedSubset of M by Def1; ::_thesis: verum
end;
end;
theorem Th3: :: CLOSURE2:3
for I being set
for M being ManySortedSet of I
for SF, SG being SubsetFamily of M holds SF \/ SG is SubsetFamily of M ;
theorem :: CLOSURE2:4
for I being set
for M being ManySortedSet of I
for SF, SG being SubsetFamily of M holds SF /\ SG is SubsetFamily of M ;
theorem :: CLOSURE2:5
for I, x being set
for M being ManySortedSet of I
for SF being SubsetFamily of M holds SF \ x is SubsetFamily of M ;
theorem :: CLOSURE2:6
for I being set
for M being ManySortedSet of I
for SF, SG being SubsetFamily of M holds SF \+\ SG is SubsetFamily of M ;
theorem Th7: :: CLOSURE2:7
for I being set
for A, M being ManySortedSet of I st A c= M holds
{A} is SubsetFamily of M
proof
let I be set ; ::_thesis: for A, M being ManySortedSet of I st A c= M holds
{A} is SubsetFamily of M
let A, M be ManySortedSet of I; ::_thesis: ( A c= M implies {A} is SubsetFamily of M )
assume A c= M ; ::_thesis: {A} is SubsetFamily of M
then A is ManySortedSubset of M by PBOOLE:def_18;
then A in Bool M by Def1;
hence {A} is SubsetFamily of M by ZFMISC_1:31; ::_thesis: verum
end;
theorem Th8: :: CLOSURE2:8
for I being set
for A, M, B being ManySortedSet of I st A c= M & B c= M holds
{A,B} is SubsetFamily of M
proof
let I be set ; ::_thesis: for A, M, B being ManySortedSet of I st A c= M & B c= M holds
{A,B} is SubsetFamily of M
let A, M, B be ManySortedSet of I; ::_thesis: ( A c= M & B c= M implies {A,B} is SubsetFamily of M )
assume ( A c= M & B c= M ) ; ::_thesis: {A,B} is SubsetFamily of M
then ( {A} is SubsetFamily of M & {B} is SubsetFamily of M ) by Th7;
then {A} \/ {B} is SubsetFamily of M by Th3;
hence {A,B} is SubsetFamily of M by ENUMSET1:1; ::_thesis: verum
end;
theorem Th9: :: CLOSURE2:9
for I being set
for M being ManySortedSet of I
for E, T being Element of Bool M holds E /\ T in Bool M
proof
let I be set ; ::_thesis: for M being ManySortedSet of I
for E, T being Element of Bool M holds E /\ T in Bool M
let M be ManySortedSet of I; ::_thesis: for E, T being Element of Bool M holds E /\ T in Bool M
let E, T be Element of Bool M; ::_thesis: E /\ T in Bool M
( E c= M & T c= M ) by PBOOLE:def_18;
then E /\ T c= M /\ M by PBOOLE:21;
then E /\ T is ManySortedSubset of M by PBOOLE:def_18;
hence E /\ T in Bool M by Def1; ::_thesis: verum
end;
theorem Th10: :: CLOSURE2:10
for I being set
for M being ManySortedSet of I
for E, T being Element of Bool M holds E \/ T in Bool M
proof
let I be set ; ::_thesis: for M being ManySortedSet of I
for E, T being Element of Bool M holds E \/ T in Bool M
let M be ManySortedSet of I; ::_thesis: for E, T being Element of Bool M holds E \/ T in Bool M
let E, T be Element of Bool M; ::_thesis: E \/ T in Bool M
( E c= M & T c= M ) by PBOOLE:def_18;
then E \/ T c= M \/ M by PBOOLE:20;
then E \/ T is ManySortedSubset of M by PBOOLE:def_18;
hence E \/ T in Bool M by Def1; ::_thesis: verum
end;
theorem :: CLOSURE2:11
for I being set
for A, M being ManySortedSet of I
for E being Element of Bool M holds E \ A in Bool M
proof
let I be set ; ::_thesis: for A, M being ManySortedSet of I
for E being Element of Bool M holds E \ A in Bool M
let A, M be ManySortedSet of I; ::_thesis: for E being Element of Bool M holds E \ A in Bool M
let E be Element of Bool M; ::_thesis: E \ A in Bool M
E c= M by PBOOLE:def_18;
then E \ A c= M by MBOOLEAN:15;
then E \ A is ManySortedSubset of M by PBOOLE:def_18;
hence E \ A in Bool M by Def1; ::_thesis: verum
end;
theorem :: CLOSURE2:12
for I being set
for M being ManySortedSet of I
for E, T being Element of Bool M holds E \+\ T in Bool M
proof
let I be set ; ::_thesis: for M being ManySortedSet of I
for E, T being Element of Bool M holds E \+\ T in Bool M
let M be ManySortedSet of I; ::_thesis: for E, T being Element of Bool M holds E \+\ T in Bool M
let E, T be Element of Bool M; ::_thesis: E \+\ T in Bool M
T c= M by PBOOLE:def_18;
then A1: T \ E c= M by MBOOLEAN:15;
E c= M by PBOOLE:def_18;
then E \ T c= M by MBOOLEAN:15;
then E \+\ T c= M by A1, PBOOLE:91;
then E \+\ T is ManySortedSubset of M by PBOOLE:def_18;
hence E \+\ T in Bool M by Def1; ::_thesis: verum
end;
begin
definition
let S be functional set ;
func|.S.| -> Function means :Def2: :: CLOSURE2:def 2
ex A being non empty functional set st
( A = S & dom it = meet { (dom x) where x is Element of A : verum } & ( for i being set st i in dom it holds
it . i = { (x . i) where x is Element of A : verum } ) ) if S <> {}
otherwise it = {} ;
existence
( ( S <> {} implies ex b1 being Function ex A being non empty functional set st
( A = S & dom b1 = meet { (dom x) where x is Element of A : verum } & ( for i being set st i in dom b1 holds
b1 . i = { (x . i) where x is Element of A : verum } ) ) ) & ( not S <> {} implies ex b1 being Function st b1 = {} ) )
proof
thus ( S <> {} implies ex f being Function ex A being non empty functional set st
( A = S & dom f = meet { (dom x) where x is Element of A : verum } & ( for i being set st i in dom f holds
f . i = { (x . i) where x is Element of A : verum } ) ) ) ::_thesis: ( not S <> {} implies ex b1 being Function st b1 = {} )
proof
assume S <> {} ; ::_thesis: ex f being Function ex A being non empty functional set st
( A = S & dom f = meet { (dom x) where x is Element of A : verum } & ( for i being set st i in dom f holds
f . i = { (x . i) where x is Element of A : verum } ) )
then consider A being non empty functional set such that
A1: A = S ;
deffunc H1( set ) -> set = { (x . $1) where x is Element of A : verum } ;
consider f being Function such that
A2: ( dom f = meet { (dom x) where x is Element of A : verum } & ( for i being set st i in meet { (dom x) where x is Element of A : verum } holds
f . i = H1(i) ) ) from FUNCT_1:sch_3();
take f ; ::_thesis: ex A being non empty functional set st
( A = S & dom f = meet { (dom x) where x is Element of A : verum } & ( for i being set st i in dom f holds
f . i = { (x . i) where x is Element of A : verum } ) )
take A ; ::_thesis: ( A = S & dom f = meet { (dom x) where x is Element of A : verum } & ( for i being set st i in dom f holds
f . i = { (x . i) where x is Element of A : verum } ) )
thus ( A = S & dom f = meet { (dom x) where x is Element of A : verum } & ( for i being set st i in dom f holds
f . i = { (x . i) where x is Element of A : verum } ) ) by A1, A2; ::_thesis: verum
end;
thus ( not S <> {} implies ex b1 being Function st b1 = {} ) ; ::_thesis: verum
end;
uniqueness
for b1, b2 being Function holds
( ( S <> {} & ex A being non empty functional set st
( A = S & dom b1 = meet { (dom x) where x is Element of A : verum } & ( for i being set st i in dom b1 holds
b1 . i = { (x . i) where x is Element of A : verum } ) ) & ex A being non empty functional set st
( A = S & dom b2 = meet { (dom x) where x is Element of A : verum } & ( for i being set st i in dom b2 holds
b2 . i = { (x . i) where x is Element of A : verum } ) ) implies b1 = b2 ) & ( not S <> {} & b1 = {} & b2 = {} implies b1 = b2 ) )
proof
let f, g be Function; ::_thesis: ( ( S <> {} & ex A being non empty functional set st
( A = S & dom f = meet { (dom x) where x is Element of A : verum } & ( for i being set st i in dom f holds
f . i = { (x . i) where x is Element of A : verum } ) ) & ex A being non empty functional set st
( A = S & dom g = meet { (dom x) where x is Element of A : verum } & ( for i being set st i in dom g holds
g . i = { (x . i) where x is Element of A : verum } ) ) implies f = g ) & ( not S <> {} & f = {} & g = {} implies f = g ) )
defpred S1[ Function] means ex A being non empty functional set st
( A = S & dom $1 = meet { (dom x) where x is Element of A : verum } & ( for i being set st i in dom $1 holds
$1 . i = { (x . i) where x is Element of A : verum } ) );
thus ( S <> {} & S1[f] & S1[g] implies f = g ) ::_thesis: ( not S <> {} & f = {} & g = {} implies f = g )
proof
assume that
S <> {} and
A3: S1[f] and
A4: S1[g] ; ::_thesis: f = g
consider A being non empty functional set such that
A5: A = S and
A6: dom f = meet { (dom x) where x is Element of A : verum } and
A7: for i being set st i in dom f holds
f . i = { (x . i) where x is Element of A : verum } by A3;
now__::_thesis:_for_a_being_set_st_a_in_meet__{__(dom_x)_where_x_is_Element_of_A_:_verum__}__holds_
f_._a_=_g_._a
let a be set ; ::_thesis: ( a in meet { (dom x) where x is Element of A : verum } implies f . a = g . a )
assume A8: a in meet { (dom x) where x is Element of A : verum } ; ::_thesis: f . a = g . a
hence f . a = { (x . a) where x is Element of A : verum } by A6, A7
.= g . a by A4, A5, A8 ;
::_thesis: verum
end;
hence f = g by A4, A5, A6, FUNCT_1:2; ::_thesis: verum
end;
thus ( not S <> {} & f = {} & g = {} implies f = g ) ; ::_thesis: verum
end;
consistency
for b1 being Function holds verum ;
end;
:: deftheorem Def2 defines |. CLOSURE2:def_2_:_
for S being functional set
for b2 being Function holds
( ( S <> {} implies ( b2 = |.S.| iff ex A being non empty functional set st
( A = S & dom b2 = meet { (dom x) where x is Element of A : verum } & ( for i being set st i in dom b2 holds
b2 . i = { (x . i) where x is Element of A : verum } ) ) ) ) & ( not S <> {} implies ( b2 = |.S.| iff b2 = {} ) ) );
theorem Th13: :: CLOSURE2:13
for I being set
for M being ManySortedSet of I
for SF being non empty SubsetFamily of M holds dom |.SF.| = I
proof
let I be set ; ::_thesis: for M being ManySortedSet of I
for SF being non empty SubsetFamily of M holds dom |.SF.| = I
let M be ManySortedSet of I; ::_thesis: for SF being non empty SubsetFamily of M holds dom |.SF.| = I
let SF be non empty SubsetFamily of M; ::_thesis: dom |.SF.| = I
consider A being non empty functional set such that
A1: A = SF and
A2: dom |.SF.| = meet { (dom x) where x is Element of A : verum } and
for i being set st i in dom |.SF.| holds
|.SF.| . i = { (x . i) where x is Element of A : verum } by Def2;
{ (dom x) where x is Element of A : verum } = {I}
proof
thus { (dom x) where x is Element of A : verum } c= {I} :: according to XBOOLE_0:def_10 ::_thesis: {I} c= { (dom x) where x is Element of A : verum }
proof
let a be set ; :: according to TARSKI:def_3 ::_thesis: ( not a in { (dom x) where x is Element of A : verum } or a in {I} )
assume a in { (dom x) where x is Element of A : verum } ; ::_thesis: a in {I}
then consider x being Element of A such that
A3: a = dom x ;
x is Element of SF by A1;
then a = I by A3, PARTFUN1:def_2;
hence a in {I} by TARSKI:def_1; ::_thesis: verum
end;
set x = the Element of A;
let a be set ; :: according to TARSKI:def_3 ::_thesis: ( not a in {I} or a in { (dom x) where x is Element of A : verum } )
assume a in {I} ; ::_thesis: a in { (dom x) where x is Element of A : verum }
then A4: a = I by TARSKI:def_1;
the Element of A is Element of SF by A1;
then dom the Element of A = I by PARTFUN1:def_2;
hence a in { (dom x) where x is Element of A : verum } by A4; ::_thesis: verum
end;
hence dom |.SF.| = I by A2, SETFAM_1:10; ::_thesis: verum
end;
registration
let S be empty functional set ;
cluster|.S.| -> empty ;
coherence
|.S.| is empty by Def2;
end;
definition
let I be set ;
let M be ManySortedSet of I;
let S be SubsetFamily of M;
func|:S:| -> ManySortedSet of I equals :Def3: :: CLOSURE2:def 3
|.S.| if S <> {}
otherwise [[0]] I;
coherence
( ( S <> {} implies |.S.| is ManySortedSet of I ) & ( not S <> {} implies [[0]] I is ManySortedSet of I ) )
proof
thus ( S <> {} implies |.S.| is ManySortedSet of I ) ::_thesis: ( not S <> {} implies [[0]] I is ManySortedSet of I )
proof
assume S <> {} ; ::_thesis: |.S.| is ManySortedSet of I
then dom |.S.| = I by Th13;
hence |.S.| is ManySortedSet of I by PARTFUN1:def_2, RELAT_1:def_18; ::_thesis: verum
end;
thus ( not S <> {} implies [[0]] I is ManySortedSet of I ) ; ::_thesis: verum
end;
consistency
for b1 being ManySortedSet of I holds verum ;
end;
:: deftheorem Def3 defines |: CLOSURE2:def_3_:_
for I being set
for M being ManySortedSet of I
for S being SubsetFamily of M holds
( ( S <> {} implies |:S:| = |.S.| ) & ( not S <> {} implies |:S:| = [[0]] I ) );
registration
let I be set ;
let M be ManySortedSet of I;
let S be empty SubsetFamily of M;
cluster|:S:| -> V9() ;
coherence
|:S:| is empty-yielding
proof
|:S:| = [[0]] I by Def3;
hence |:S:| is empty-yielding ; ::_thesis: verum
end;
end;
theorem Th14: :: CLOSURE2:14
for I being set
for M being ManySortedSet of I
for SF being SubsetFamily of M st not SF is empty holds
for i being set st i in I holds
|:SF:| . i = { (x . i) where x is Element of Bool M : x in SF }
proof
let I be set ; ::_thesis: for M being ManySortedSet of I
for SF being SubsetFamily of M st not SF is empty holds
for i being set st i in I holds
|:SF:| . i = { (x . i) where x is Element of Bool M : x in SF }
let M be ManySortedSet of I; ::_thesis: for SF being SubsetFamily of M st not SF is empty holds
for i being set st i in I holds
|:SF:| . i = { (x . i) where x is Element of Bool M : x in SF }
let SF be SubsetFamily of M; ::_thesis: ( not SF is empty implies for i being set st i in I holds
|:SF:| . i = { (x . i) where x is Element of Bool M : x in SF } )
A1: dom |:SF:| = I by PARTFUN1:def_2;
assume A2: not SF is empty ; ::_thesis: for i being set st i in I holds
|:SF:| . i = { (x . i) where x is Element of Bool M : x in SF }
then consider A being non empty functional set such that
A3: A = SF and
dom |.SF.| = meet { (dom x) where x is Element of A : verum } and
A4: for i being set st i in dom |.SF.| holds
|.SF.| . i = { (x . i) where x is Element of A : verum } by Def2;
let i be set ; ::_thesis: ( i in I implies |:SF:| . i = { (x . i) where x is Element of Bool M : x in SF } )
assume A5: i in I ; ::_thesis: |:SF:| . i = { (x . i) where x is Element of Bool M : x in SF }
set K = { (x . i) where x is Element of Bool M : x in SF } ;
set N = { (x . i) where x is Element of A : verum } ;
A6: { (x . i) where x is Element of Bool M : x in SF } = { (x . i) where x is Element of A : verum }
proof
thus { (x . i) where x is Element of Bool M : x in SF } c= { (x . i) where x is Element of A : verum } :: according to XBOOLE_0:def_10 ::_thesis: { (x . i) where x is Element of A : verum } c= { (x . i) where x is Element of Bool M : x in SF }
proof
let q be set ; :: according to TARSKI:def_3 ::_thesis: ( not q in { (x . i) where x is Element of Bool M : x in SF } or q in { (x . i) where x is Element of A : verum } )
assume q in { (x . i) where x is Element of Bool M : x in SF } ; ::_thesis: q in { (x . i) where x is Element of A : verum }
then ex x being Element of Bool M st
( q = x . i & x in SF ) ;
hence q in { (x . i) where x is Element of A : verum } by A3; ::_thesis: verum
end;
let q be set ; :: according to TARSKI:def_3 ::_thesis: ( not q in { (x . i) where x is Element of A : verum } or q in { (x . i) where x is Element of Bool M : x in SF } )
assume q in { (x . i) where x is Element of A : verum } ; ::_thesis: q in { (x . i) where x is Element of Bool M : x in SF }
then consider x being Element of A such that
A7: q = x . i ;
x in SF by A3;
hence q in { (x . i) where x is Element of Bool M : x in SF } by A7; ::_thesis: verum
end;
|:SF:| = |.SF.| by A2, Def3;
hence |:SF:| . i = { (x . i) where x is Element of Bool M : x in SF } by A4, A5, A1, A6; ::_thesis: verum
end;
registration
let I be set ;
let M be ManySortedSet of I;
let SF be non empty SubsetFamily of M;
cluster|:SF:| -> V8() ;
coherence
|:SF:| is non-empty
proof
let i be set ; :: according to PBOOLE:def_13 ::_thesis: ( not i in I or not |:SF:| . i is empty )
assume i in I ; ::_thesis: not |:SF:| . i is empty
then A1: |:SF:| . i = { (x . i) where x is Element of Bool M : x in SF } by Th14;
consider x being set such that
A2: x in SF by XBOOLE_0:def_1;
reconsider x = x as Element of Bool M by A2;
x . i in |:SF:| . i by A1, A2;
hence not |:SF:| . i is empty ; ::_thesis: verum
end;
end;
theorem Th15: :: CLOSURE2:15
for f being Function holds dom |.{f}.| = dom f
proof
let f be Function; ::_thesis: dom |.{f}.| = dom f
consider A being non empty functional set such that
A1: A = {f} and
A2: dom |.{f}.| = meet { (dom x) where x is Element of A : verum } and
for i being set st i in dom |.{f}.| holds
|.{f}.| . i = { (x . i) where x is Element of A : verum } by Def2;
set m = { (dom x) where x is Element of A : verum } ;
{ (dom x) where x is Element of A : verum } = {(dom f)}
proof
thus { (dom x) where x is Element of A : verum } c= {(dom f)} :: according to XBOOLE_0:def_10 ::_thesis: {(dom f)} c= { (dom x) where x is Element of A : verum }
proof
let q be set ; :: according to TARSKI:def_3 ::_thesis: ( not q in { (dom x) where x is Element of A : verum } or q in {(dom f)} )
assume q in { (dom x) where x is Element of A : verum } ; ::_thesis: q in {(dom f)}
then consider x being Element of A such that
A3: q = dom x ;
x = f by A1, TARSKI:def_1;
hence q in {(dom f)} by A3, TARSKI:def_1; ::_thesis: verum
end;
let q be set ; :: according to TARSKI:def_3 ::_thesis: ( not q in {(dom f)} or q in { (dom x) where x is Element of A : verum } )
assume q in {(dom f)} ; ::_thesis: q in { (dom x) where x is Element of A : verum }
then A4: q = dom f by TARSKI:def_1;
f is Element of A by A1, TARSKI:def_1;
hence q in { (dom x) where x is Element of A : verum } by A4; ::_thesis: verum
end;
hence dom |.{f}.| = dom f by A2, SETFAM_1:10; ::_thesis: verum
end;
theorem :: CLOSURE2:16
for f, f1 being Function holds dom |.{f,f1}.| = (dom f) /\ (dom f1)
proof
let f, f1 be Function; ::_thesis: dom |.{f,f1}.| = (dom f) /\ (dom f1)
consider A being non empty functional set such that
A1: A = {f,f1} and
A2: dom |.{f,f1}.| = meet { (dom x) where x is Element of A : verum } and
for i being set st i in dom |.{f,f1}.| holds
|.{f,f1}.| . i = { (x . i) where x is Element of A : verum } by Def2;
set m = { (dom x) where x is Element of A : verum } ;
{ (dom x) where x is Element of A : verum } = {(dom f),(dom f1)}
proof
thus { (dom x) where x is Element of A : verum } c= {(dom f),(dom f1)} :: according to XBOOLE_0:def_10 ::_thesis: {(dom f),(dom f1)} c= { (dom x) where x is Element of A : verum }
proof
let q be set ; :: according to TARSKI:def_3 ::_thesis: ( not q in { (dom x) where x is Element of A : verum } or q in {(dom f),(dom f1)} )
assume q in { (dom x) where x is Element of A : verum } ; ::_thesis: q in {(dom f),(dom f1)}
then consider x being Element of A such that
A3: q = dom x ;
( x = f or x = f1 ) by A1, TARSKI:def_2;
hence q in {(dom f),(dom f1)} by A3, TARSKI:def_2; ::_thesis: verum
end;
let q be set ; :: according to TARSKI:def_3 ::_thesis: ( not q in {(dom f),(dom f1)} or q in { (dom x) where x is Element of A : verum } )
assume q in {(dom f),(dom f1)} ; ::_thesis: q in { (dom x) where x is Element of A : verum }
then A4: ( q = dom f or q = dom f1 ) by TARSKI:def_2;
( f is Element of A & f1 is Element of A ) by A1, TARSKI:def_2;
hence q in { (dom x) where x is Element of A : verum } by A4; ::_thesis: verum
end;
hence dom |.{f,f1}.| = (dom f) /\ (dom f1) by A2, SETFAM_1:11; ::_thesis: verum
end;
theorem Th17: :: CLOSURE2:17
for i being set
for f being Function st i in dom f holds
|.{f}.| . i = {(f . i)}
proof
let i be set ; ::_thesis: for f being Function st i in dom f holds
|.{f}.| . i = {(f . i)}
let f be Function; ::_thesis: ( i in dom f implies |.{f}.| . i = {(f . i)} )
A1: f in {f} by TARSKI:def_1;
consider A being non empty functional set such that
A2: A = {f} and
dom |.{f}.| = meet { (dom x) where x is Element of A : verum } and
A3: for i being set st i in dom |.{f}.| holds
|.{f}.| . i = { (x . i) where x is Element of A : verum } by Def2;
assume i in dom f ; ::_thesis: |.{f}.| . i = {(f . i)}
then i in dom |.{f}.| by Th15;
then A4: |.{f}.| . i = { (x . i) where x is Element of A : verum } by A3;
thus |.{f}.| . i c= {(f . i)} :: according to XBOOLE_0:def_10 ::_thesis: {(f . i)} c= |.{f}.| . i
proof
let q be set ; :: according to TARSKI:def_3 ::_thesis: ( not q in |.{f}.| . i or q in {(f . i)} )
assume q in |.{f}.| . i ; ::_thesis: q in {(f . i)}
then consider x being Element of A such that
A5: q = x . i by A4;
x = f by A2, TARSKI:def_1;
hence q in {(f . i)} by A5, TARSKI:def_1; ::_thesis: verum
end;
let q be set ; :: according to TARSKI:def_3 ::_thesis: ( not q in {(f . i)} or q in |.{f}.| . i )
assume q in {(f . i)} ; ::_thesis: q in |.{f}.| . i
then q = f . i by TARSKI:def_1;
hence q in |.{f}.| . i by A2, A4, A1; ::_thesis: verum
end;
theorem :: CLOSURE2:18
for i, I being set
for M being ManySortedSet of I
for f being Function
for SF being SubsetFamily of M st i in I & SF = {f} holds
|:SF:| . i = {(f . i)}
proof
let i, I be set ; ::_thesis: for M being ManySortedSet of I
for f being Function
for SF being SubsetFamily of M st i in I & SF = {f} holds
|:SF:| . i = {(f . i)}
let M be ManySortedSet of I; ::_thesis: for f being Function
for SF being SubsetFamily of M st i in I & SF = {f} holds
|:SF:| . i = {(f . i)}
let f be Function; ::_thesis: for SF being SubsetFamily of M st i in I & SF = {f} holds
|:SF:| . i = {(f . i)}
let SF be SubsetFamily of M; ::_thesis: ( i in I & SF = {f} implies |:SF:| . i = {(f . i)} )
assume that
A1: i in I and
A2: SF = {f} ; ::_thesis: |:SF:| . i = {(f . i)}
A3: |:SF:| = |.SF.| by A2, Def3;
dom |:SF:| = I by PARTFUN1:def_2;
then i in dom f by A1, A2, A3, Th15;
hence |:SF:| . i = {(f . i)} by A2, A3, Th17; ::_thesis: verum
end;
theorem Th19: :: CLOSURE2:19
for i being set
for f, f1 being Function st i in dom |.{f,f1}.| holds
|.{f,f1}.| . i = {(f . i),(f1 . i)}
proof
let i be set ; ::_thesis: for f, f1 being Function st i in dom |.{f,f1}.| holds
|.{f,f1}.| . i = {(f . i),(f1 . i)}
let f, f1 be Function; ::_thesis: ( i in dom |.{f,f1}.| implies |.{f,f1}.| . i = {(f . i),(f1 . i)} )
A1: ( f in {f,f1} & f1 in {f,f1} ) by TARSKI:def_2;
consider A being non empty functional set such that
A2: A = {f,f1} and
dom |.{f,f1}.| = meet { (dom x) where x is Element of A : verum } and
A3: for i being set st i in dom |.{f,f1}.| holds
|.{f,f1}.| . i = { (x . i) where x is Element of A : verum } by Def2;
assume i in dom |.{f,f1}.| ; ::_thesis: |.{f,f1}.| . i = {(f . i),(f1 . i)}
then A4: |.{f,f1}.| . i = { (x . i) where x is Element of A : verum } by A3;
thus |.{f,f1}.| . i c= {(f . i),(f1 . i)} :: according to XBOOLE_0:def_10 ::_thesis: {(f . i),(f1 . i)} c= |.{f,f1}.| . i
proof
let q be set ; :: according to TARSKI:def_3 ::_thesis: ( not q in |.{f,f1}.| . i or q in {(f . i),(f1 . i)} )
assume q in |.{f,f1}.| . i ; ::_thesis: q in {(f . i),(f1 . i)}
then consider x being Element of A such that
A5: q = x . i by A4;
percases ( x = f or x = f1 ) by A2, TARSKI:def_2;
suppose x = f ; ::_thesis: q in {(f . i),(f1 . i)}
hence q in {(f . i),(f1 . i)} by A5, TARSKI:def_2; ::_thesis: verum
end;
suppose x = f1 ; ::_thesis: q in {(f . i),(f1 . i)}
hence q in {(f . i),(f1 . i)} by A5, TARSKI:def_2; ::_thesis: verum
end;
end;
end;
let q be set ; :: according to TARSKI:def_3 ::_thesis: ( not q in {(f . i),(f1 . i)} or q in |.{f,f1}.| . i )
assume q in {(f . i),(f1 . i)} ; ::_thesis: q in |.{f,f1}.| . i
then ( q = f . i or q = f1 . i ) by TARSKI:def_2;
hence q in |.{f,f1}.| . i by A2, A4, A1; ::_thesis: verum
end;
theorem Th20: :: CLOSURE2:20
for i, I being set
for M being ManySortedSet of I
for f, f1 being Function
for SF being SubsetFamily of M st i in I & SF = {f,f1} holds
|:SF:| . i = {(f . i),(f1 . i)}
proof
let i, I be set ; ::_thesis: for M being ManySortedSet of I
for f, f1 being Function
for SF being SubsetFamily of M st i in I & SF = {f,f1} holds
|:SF:| . i = {(f . i),(f1 . i)}
let M be ManySortedSet of I; ::_thesis: for f, f1 being Function
for SF being SubsetFamily of M st i in I & SF = {f,f1} holds
|:SF:| . i = {(f . i),(f1 . i)}
let f, f1 be Function; ::_thesis: for SF being SubsetFamily of M st i in I & SF = {f,f1} holds
|:SF:| . i = {(f . i),(f1 . i)}
let SF be SubsetFamily of M; ::_thesis: ( i in I & SF = {f,f1} implies |:SF:| . i = {(f . i),(f1 . i)} )
assume that
A1: i in I and
A2: SF = {f,f1} ; ::_thesis: |:SF:| . i = {(f . i),(f1 . i)}
( dom |:SF:| = I & |:SF:| = |.SF.| ) by A2, Def3, PARTFUN1:def_2;
hence |:SF:| . i = {(f . i),(f1 . i)} by A1, A2, Th19; ::_thesis: verum
end;
definition
let I be set ;
let M be ManySortedSet of I;
let SF be SubsetFamily of M;
:: original: |:
redefine func|:SF:| -> MSSubsetFamily of M;
coherence
|:SF:| is MSSubsetFamily of M
proof
percases ( not SF is empty or SF is empty ) ;
supposeA1: not SF is empty ; ::_thesis: |:SF:| is MSSubsetFamily of M
|:SF:| is ManySortedSubset of bool M
proof
let i be set ; :: according to PBOOLE:def_2,PBOOLE:def_18 ::_thesis: ( not i in I or |:SF:| . i c= (bool M) . i )
assume A2: i in I ; ::_thesis: |:SF:| . i c= (bool M) . i
then A3: |:SF:| . i = { (x . i) where x is Element of Bool M : x in SF } by A1, Th14;
thus |:SF:| . i c= (bool M) . i ::_thesis: verum
proof
let x be set ; :: according to TARSKI:def_3 ::_thesis: ( not x in |:SF:| . i or x in (bool M) . i )
assume x in |:SF:| . i ; ::_thesis: x in (bool M) . i
then consider a being Element of Bool M such that
A4: x = a . i and
a in SF by A3;
a c= M by PBOOLE:def_18;
then x c= M . i by A2, A4, PBOOLE:def_2;
then x in bool (M . i) ;
hence x in (bool M) . i by A2, MBOOLEAN:def_1; ::_thesis: verum
end;
end;
hence |:SF:| is MSSubsetFamily of M ; ::_thesis: verum
end;
suppose SF is empty ; ::_thesis: |:SF:| is MSSubsetFamily of M
then |:SF:| = [[0]] I by Def3;
hence |:SF:| is MSSubsetFamily of M by MSSUBFAM:31; ::_thesis: verum
end;
end;
end;
end;
theorem Th21: :: CLOSURE2:21
for I being set
for M, A being ManySortedSet of I
for SF being SubsetFamily of M st A in SF holds
A in' |:SF:|
proof
let I be set ; ::_thesis: for M, A being ManySortedSet of I
for SF being SubsetFamily of M st A in SF holds
A in' |:SF:|
let M, A be ManySortedSet of I; ::_thesis: for SF being SubsetFamily of M st A in SF holds
A in' |:SF:|
let SF be SubsetFamily of M; ::_thesis: ( A in SF implies A in' |:SF:| )
assume A1: A in SF ; ::_thesis: A in' |:SF:|
let i be set ; :: according to PBOOLE:def_1 ::_thesis: ( not i in I or A . i in |:SF:| . i )
assume i in I ; ::_thesis: A . i in |:SF:| . i
then |:SF:| . i = { (x . i) where x is Element of Bool M : x in SF } by A1, Th14;
hence A . i in |:SF:| . i by A1; ::_thesis: verum
end;
theorem Th22: :: CLOSURE2:22
for I being set
for M, A, B being ManySortedSet of I
for SF being SubsetFamily of M st SF = {A,B} holds
union |:SF:| = A \/ B
proof
let I be set ; ::_thesis: for M, A, B being ManySortedSet of I
for SF being SubsetFamily of M st SF = {A,B} holds
union |:SF:| = A \/ B
let M, A, B be ManySortedSet of I; ::_thesis: for SF being SubsetFamily of M st SF = {A,B} holds
union |:SF:| = A \/ B
let SF be SubsetFamily of M; ::_thesis: ( SF = {A,B} implies union |:SF:| = A \/ B )
assume A1: SF = {A,B} ; ::_thesis: union |:SF:| = A \/ B
now__::_thesis:_for_i_being_set_st_i_in_I_holds_
(union_|:SF:|)_._i_=_(A_\/_B)_._i
let i be set ; ::_thesis: ( i in I implies (union |:SF:|) . i = (A \/ B) . i )
assume A2: i in I ; ::_thesis: (union |:SF:|) . i = (A \/ B) . i
hence (union |:SF:|) . i = union (|:SF:| . i) by MBOOLEAN:def_2
.= union {(A . i),(B . i)} by A1, A2, Th20
.= (A . i) \/ (B . i) by ZFMISC_1:75
.= (A \/ B) . i by A2, PBOOLE:def_4 ;
::_thesis: verum
end;
hence union |:SF:| = A \/ B by PBOOLE:3; ::_thesis: verum
end;
theorem Th23: :: CLOSURE2:23
for I being set
for M being ManySortedSet of I
for SF being SubsetFamily of M
for E, T being Element of Bool M st SF = {E,T} holds
meet |:SF:| = E /\ T
proof
let I be set ; ::_thesis: for M being ManySortedSet of I
for SF being SubsetFamily of M
for E, T being Element of Bool M st SF = {E,T} holds
meet |:SF:| = E /\ T
let M be ManySortedSet of I; ::_thesis: for SF being SubsetFamily of M
for E, T being Element of Bool M st SF = {E,T} holds
meet |:SF:| = E /\ T
let SF be SubsetFamily of M; ::_thesis: for E, T being Element of Bool M st SF = {E,T} holds
meet |:SF:| = E /\ T
let E, T be Element of Bool M; ::_thesis: ( SF = {E,T} implies meet |:SF:| = E /\ T )
assume A1: SF = {E,T} ; ::_thesis: meet |:SF:| = E /\ T
now__::_thesis:_for_i_being_set_st_i_in_I_holds_
(meet_|:SF:|)_._i_=_(E_/\_T)_._i
reconsider sf1 = SF as non empty SubsetFamily of M by A1;
let i be set ; ::_thesis: ( i in I implies (meet |:SF:|) . i = (E /\ T) . i )
assume A2: i in I ; ::_thesis: (meet |:SF:|) . i = (E /\ T) . i
ex Q being Subset-Family of (M . i) st
( Q = |:sf1:| . i & (meet |:sf1:|) . i = Intersect Q ) by A2, MSSUBFAM:def_1;
hence (meet |:SF:|) . i = meet (|:sf1:| . i) by A2, SETFAM_1:def_9
.= meet {(E . i),(T . i)} by A1, A2, Th20
.= (E . i) /\ (T . i) by SETFAM_1:11
.= (E /\ T) . i by A2, PBOOLE:def_5 ;
::_thesis: verum
end;
hence meet |:SF:| = E /\ T by PBOOLE:3; ::_thesis: verum
end;
theorem Th24: :: CLOSURE2:24
for I being set
for M being ManySortedSet of I
for SF being SubsetFamily of M
for Z being ManySortedSubset of M st ( for Z1 being ManySortedSet of I st Z1 in SF holds
Z c=' Z1 ) holds
Z c=' meet |:SF:|
proof
let I be set ; ::_thesis: for M being ManySortedSet of I
for SF being SubsetFamily of M
for Z being ManySortedSubset of M st ( for Z1 being ManySortedSet of I st Z1 in SF holds
Z c=' Z1 ) holds
Z c=' meet |:SF:|
let M be ManySortedSet of I; ::_thesis: for SF being SubsetFamily of M
for Z being ManySortedSubset of M st ( for Z1 being ManySortedSet of I st Z1 in SF holds
Z c=' Z1 ) holds
Z c=' meet |:SF:|
let SF be SubsetFamily of M; ::_thesis: for Z being ManySortedSubset of M st ( for Z1 being ManySortedSet of I st Z1 in SF holds
Z c=' Z1 ) holds
Z c=' meet |:SF:|
let Z be ManySortedSubset of M; ::_thesis: ( ( for Z1 being ManySortedSet of I st Z1 in SF holds
Z c=' Z1 ) implies Z c=' meet |:SF:| )
assume A1: for Z1 being ManySortedSet of I st Z1 in SF holds
Z c=' Z1 ; ::_thesis: Z c=' meet |:SF:|
let i be set ; :: according to PBOOLE:def_2 ::_thesis: ( not i in I or Z . i c= (meet |:SF:|) . i )
assume A2: i in I ; ::_thesis: Z . i c= (meet |:SF:|) . i
consider Q being Subset-Family of (M . i) such that
A3: Q = |:SF:| . i and
A4: (meet |:SF:|) . i = Intersect Q by A2, MSSUBFAM:def_1;
A5: now__::_thesis:_for_q_being_set_st_q_in_Q_holds_
Z_._i_c=_q
let q be set ; ::_thesis: ( q in Q implies Z . i c= b1 )
assume A6: q in Q ; ::_thesis: Z . i c= b1
percases ( not SF is empty or SF is empty ) ;
suppose not SF is empty ; ::_thesis: Z . i c= b1
then |:SF:| . i = { (x . i) where x is Element of Bool M : x in SF } by A2, Th14;
then consider a being Element of Bool M such that
A7: q = a . i and
A8: a in SF by A3, A6;
Z c=' a by A1, A8;
hence Z . i c= q by A2, A7, PBOOLE:def_2; ::_thesis: verum
end;
suppose SF is empty ; ::_thesis: Z . i c= b1
then |:SF:| = [[0]] I by Def3;
hence Z . i c= q by A3, A6; ::_thesis: verum
end;
end;
end;
Z c= M by PBOOLE:def_18;
then Z . i is Subset of (M . i) by A2, PBOOLE:def_2;
hence Z . i c= (meet |:SF:|) . i by A4, A5, MSSUBFAM:4; ::_thesis: verum
end;
theorem :: CLOSURE2:25
for I being set
for M being ManySortedSet of I holds |:(Bool M):| = bool M
proof
let I be set ; ::_thesis: for M being ManySortedSet of I holds |:(Bool M):| = bool M
let M be ManySortedSet of I; ::_thesis: |:(Bool M):| = bool M
now__::_thesis:_for_i_being_set_st_i_in_I_holds_
|:(Bool_M):|_._i_=_(bool_M)_._i
let i be set ; ::_thesis: ( i in I implies |:(Bool M):| . i = (bool M) . i )
assume A1: i in I ; ::_thesis: |:(Bool M):| . i = (bool M) . i
then A2: |:(Bool M):| . i = { (x . i) where x is Element of Bool M : x in Bool M } by Th14;
thus |:(Bool M):| . i = (bool M) . i ::_thesis: verum
proof
thus |:(Bool M):| . i c= (bool M) . i :: according to XBOOLE_0:def_10 ::_thesis: (bool M) . i c= |:(Bool M):| . i
proof
let q be set ; :: according to TARSKI:def_3 ::_thesis: ( not q in |:(Bool M):| . i or q in (bool M) . i )
assume q in |:(Bool M):| . i ; ::_thesis: q in (bool M) . i
then consider x being Element of Bool M such that
A3: q = x . i and
x in Bool M by A2;
x c= M by PBOOLE:def_18;
then x . i c= M . i by A1, PBOOLE:def_2;
then x . i in bool (M . i) ;
hence q in (bool M) . i by A1, A3, MBOOLEAN:def_1; ::_thesis: verum
end;
let a be set ; :: according to TARSKI:def_3 ::_thesis: ( not a in (bool M) . i or a in |:(Bool M):| . i )
assume A4: a in (bool M) . i ; ::_thesis: a in |:(Bool M):| . i
dom (([[0]] I) +* (i .--> a)) = I by A1, PZFMISC1:1;
then reconsider X = ([[0]] I) +* (i .--> a) as ManySortedSet of I by PARTFUN1:def_2, RELAT_1:def_18;
A5: dom (i .--> a) = {i} by FUNCOP_1:13;
i in {i} by TARSKI:def_1;
then A6: X . i = (i .--> a) . i by A5, FUNCT_4:13
.= a by FUNCOP_1:72 ;
X is ManySortedSubset of M
proof
let s be set ; :: according to PBOOLE:def_2,PBOOLE:def_18 ::_thesis: ( not s in I or X . s c= M . s )
assume A7: s in I ; ::_thesis: X . s c= M . s
percases ( s = i or s <> i ) ;
supposeA8: s = i ; ::_thesis: X . s c= M . s
then a in bool (M . s) by A4, A7, MBOOLEAN:def_1;
hence X . s c= M . s by A6, A8; ::_thesis: verum
end;
suppose s <> i ; ::_thesis: X . s c= M . s
then not s in dom (i .--> a) by A5, TARSKI:def_1;
then X . s = ([[0]] I) . s by FUNCT_4:11
.= {} ;
hence X . s c= M . s by XBOOLE_1:2; ::_thesis: verum
end;
end;
end;
then X is Element of Bool M by Def1;
hence a in |:(Bool M):| . i by A2, A6; ::_thesis: verum
end;
end;
hence |:(Bool M):| = bool M by PBOOLE:3; ::_thesis: verum
end;
definition
let I be set ;
let M be ManySortedSet of I;
let IT be SubsetFamily of M;
attrIT is additive means :: CLOSURE2:def 4
for A, B being ManySortedSet of I st A in IT & B in IT holds
A \/ B in IT;
attrIT is absolutely-additive means :Def5: :: CLOSURE2:def 5
for F being SubsetFamily of M st F c= IT holds
union |:F:| in IT;
attrIT is multiplicative means :: CLOSURE2:def 6
for A, B being ManySortedSet of I st A in IT & B in IT holds
A /\ B in IT;
attrIT is absolutely-multiplicative means :Def7: :: CLOSURE2:def 7
for F being SubsetFamily of M st F c= IT holds
meet |:F:| in IT;
attrIT is properly-upper-bound means :Def8: :: CLOSURE2:def 8
M in IT;
attrIT is properly-lower-bound means :Def9: :: CLOSURE2:def 9
[[0]] I in IT;
end;
:: deftheorem defines additive CLOSURE2:def_4_:_
for I being set
for M being ManySortedSet of I
for IT being SubsetFamily of M holds
( IT is additive iff for A, B being ManySortedSet of I st A in IT & B in IT holds
A \/ B in IT );
:: deftheorem Def5 defines absolutely-additive CLOSURE2:def_5_:_
for I being set
for M being ManySortedSet of I
for IT being SubsetFamily of M holds
( IT is absolutely-additive iff for F being SubsetFamily of M st F c= IT holds
union |:F:| in IT );
:: deftheorem defines multiplicative CLOSURE2:def_6_:_
for I being set
for M being ManySortedSet of I
for IT being SubsetFamily of M holds
( IT is multiplicative iff for A, B being ManySortedSet of I st A in IT & B in IT holds
A /\ B in IT );
:: deftheorem Def7 defines absolutely-multiplicative CLOSURE2:def_7_:_
for I being set
for M being ManySortedSet of I
for IT being SubsetFamily of M holds
( IT is absolutely-multiplicative iff for F being SubsetFamily of M st F c= IT holds
meet |:F:| in IT );
:: deftheorem Def8 defines properly-upper-bound CLOSURE2:def_8_:_
for I being set
for M being ManySortedSet of I
for IT being SubsetFamily of M holds
( IT is properly-upper-bound iff M in IT );
:: deftheorem Def9 defines properly-lower-bound CLOSURE2:def_9_:_
for I being set
for M being ManySortedSet of I
for IT being SubsetFamily of M holds
( IT is properly-lower-bound iff [[0]] I in IT );
Lm1: for I being set
for M being ManySortedSet of I holds
( Bool M is additive & Bool M is absolutely-additive & Bool M is multiplicative & Bool M is absolutely-multiplicative & Bool M is properly-upper-bound & Bool M is properly-lower-bound )
proof
let I be set ; ::_thesis: for M being ManySortedSet of I holds
( Bool M is additive & Bool M is absolutely-additive & Bool M is multiplicative & Bool M is absolutely-multiplicative & Bool M is properly-upper-bound & Bool M is properly-lower-bound )
let M be ManySortedSet of I; ::_thesis: ( Bool M is additive & Bool M is absolutely-additive & Bool M is multiplicative & Bool M is absolutely-multiplicative & Bool M is properly-upper-bound & Bool M is properly-lower-bound )
thus Bool M is additive ::_thesis: ( Bool M is absolutely-additive & Bool M is multiplicative & Bool M is absolutely-multiplicative & Bool M is properly-upper-bound & Bool M is properly-lower-bound )
proof
let A be ManySortedSet of I; :: according to CLOSURE2:def_4 ::_thesis: for B being ManySortedSet of I st A in Bool M & B in Bool M holds
A \/ B in Bool M
let B be ManySortedSet of I; ::_thesis: ( A in Bool M & B in Bool M implies A \/ B in Bool M )
assume ( A in Bool M & B in Bool M ) ; ::_thesis: A \/ B in Bool M
hence A \/ B in Bool M by Th10; ::_thesis: verum
end;
thus Bool M is absolutely-additive ::_thesis: ( Bool M is multiplicative & Bool M is absolutely-multiplicative & Bool M is properly-upper-bound & Bool M is properly-lower-bound )
proof
let F be SubsetFamily of M; :: according to CLOSURE2:def_5 ::_thesis: ( F c= Bool M implies union |:F:| in Bool M )
assume F c= Bool M ; ::_thesis: union |:F:| in Bool M
union |:F:| c= M by MSSUBFAM:40;
then union |:F:| is ManySortedSubset of M by PBOOLE:def_18;
hence union |:F:| in Bool M by Def1; ::_thesis: verum
end;
thus Bool M is multiplicative ::_thesis: ( Bool M is absolutely-multiplicative & Bool M is properly-upper-bound & Bool M is properly-lower-bound )
proof
let A be ManySortedSet of I; :: according to CLOSURE2:def_6 ::_thesis: for B being ManySortedSet of I st A in Bool M & B in Bool M holds
A /\ B in Bool M
let B be ManySortedSet of I; ::_thesis: ( A in Bool M & B in Bool M implies A /\ B in Bool M )
assume ( A in Bool M & B in Bool M ) ; ::_thesis: A /\ B in Bool M
hence A /\ B in Bool M by Th9; ::_thesis: verum
end;
thus Bool M is absolutely-multiplicative ::_thesis: ( Bool M is properly-upper-bound & Bool M is properly-lower-bound )
proof
let F be SubsetFamily of M; :: according to CLOSURE2:def_7 ::_thesis: ( F c= Bool M implies meet |:F:| in Bool M )
assume F c= Bool M ; ::_thesis: meet |:F:| in Bool M
thus meet |:F:| in Bool M by Def1; ::_thesis: verum
end;
M is ManySortedSubset of M by PBOOLE:def_18;
then M in Bool M by Def1;
hence Bool M is properly-upper-bound by Def8; ::_thesis: Bool M is properly-lower-bound
[[0]] I c= M by PBOOLE:43;
then [[0]] I is ManySortedSubset of M by PBOOLE:def_18;
hence [[0]] I in Bool M by Def1; :: according to CLOSURE2:def_9 ::_thesis: verum
end;
registration
let I be set ;
let M be ManySortedSet of I;
cluster non empty functional with_common_domain additive absolutely-additive multiplicative absolutely-multiplicative properly-upper-bound properly-lower-bound for Element of bool (Bool M);
existence
ex b1 being SubsetFamily of M st
( not b1 is empty & b1 is functional & b1 is with_common_domain & b1 is additive & b1 is absolutely-additive & b1 is multiplicative & b1 is absolutely-multiplicative & b1 is properly-upper-bound & b1 is properly-lower-bound )
proof
take Bool M ; ::_thesis: ( not Bool M is empty & Bool M is functional & Bool M is with_common_domain & Bool M is additive & Bool M is absolutely-additive & Bool M is multiplicative & Bool M is absolutely-multiplicative & Bool M is properly-upper-bound & Bool M is properly-lower-bound )
thus ( not Bool M is empty & Bool M is functional & Bool M is with_common_domain & Bool M is additive & Bool M is absolutely-additive & Bool M is multiplicative & Bool M is absolutely-multiplicative & Bool M is properly-upper-bound & Bool M is properly-lower-bound ) by Lm1; ::_thesis: verum
end;
end;
definition
let I be set ;
let M be ManySortedSet of I;
:: original: Bool
redefine func Bool M -> additive absolutely-additive multiplicative absolutely-multiplicative properly-upper-bound properly-lower-bound SubsetFamily of M;
coherence
Bool M is additive absolutely-additive multiplicative absolutely-multiplicative properly-upper-bound properly-lower-bound SubsetFamily of M by Lm1;
end;
registration
let I be set ;
let M be ManySortedSet of I;
cluster absolutely-additive -> additive for Element of bool (Bool M);
coherence
for b1 being SubsetFamily of M st b1 is absolutely-additive holds
b1 is additive
proof
let SF be SubsetFamily of M; ::_thesis: ( SF is absolutely-additive implies SF is additive )
assume A1: SF is absolutely-additive ; ::_thesis: SF is additive
let A be ManySortedSet of I; :: according to CLOSURE2:def_4 ::_thesis: for B being ManySortedSet of I st A in SF & B in SF holds
A \/ B in SF
let B be ManySortedSet of I; ::_thesis: ( A in SF & B in SF implies A \/ B in SF )
assume that
A2: A in SF and
A3: B in SF ; ::_thesis: A \/ B in SF
B is ManySortedSubset of M by A3, Def1;
then A4: B c= M by PBOOLE:def_18;
A is ManySortedSubset of M by A2, Def1;
then A c= M by PBOOLE:def_18;
then reconsider ab = {A,B} as SubsetFamily of M by A4, Th8;
( {A} c= SF & {B} c= SF ) by A2, A3, ZFMISC_1:31;
then {A} \/ {B} c= SF by XBOOLE_1:8;
then {A,B} c= SF by ENUMSET1:1;
then union |:ab:| in SF by A1, Def5;
hence A \/ B in SF by Th22; ::_thesis: verum
end;
end;
registration
let I be set ;
let M be ManySortedSet of I;
cluster absolutely-multiplicative -> multiplicative for Element of bool (Bool M);
coherence
for b1 being SubsetFamily of M st b1 is absolutely-multiplicative holds
b1 is multiplicative
proof
let SF be SubsetFamily of M; ::_thesis: ( SF is absolutely-multiplicative implies SF is multiplicative )
assume A1: SF is absolutely-multiplicative ; ::_thesis: SF is multiplicative
let A be ManySortedSet of I; :: according to CLOSURE2:def_6 ::_thesis: for B being ManySortedSet of I st A in SF & B in SF holds
A /\ B in SF
let B be ManySortedSet of I; ::_thesis: ( A in SF & B in SF implies A /\ B in SF )
assume that
A2: A in SF and
A3: B in SF ; ::_thesis: A /\ B in SF
B is ManySortedSubset of M by A3, Def1;
then A4: B c= M by PBOOLE:def_18;
A is ManySortedSubset of M by A2, Def1;
then A c= M by PBOOLE:def_18;
then reconsider ab = {A,B} as SubsetFamily of M by A4, Th8;
( {A} c= SF & {B} c= SF ) by A2, A3, ZFMISC_1:31;
then {A} \/ {B} c= SF by XBOOLE_1:8;
then {A,B} c= SF by ENUMSET1:1;
then meet |:ab:| in SF by A1, Def7;
hence A /\ B in SF by A2, A3, Th23; ::_thesis: verum
end;
end;
registration
let I be set ;
let M be ManySortedSet of I;
cluster absolutely-multiplicative -> properly-upper-bound for Element of bool (Bool M);
coherence
for b1 being SubsetFamily of M st b1 is absolutely-multiplicative holds
b1 is properly-upper-bound
proof
reconsider a = {} as SubsetFamily of M by XBOOLE_1:2;
let SF be SubsetFamily of M; ::_thesis: ( SF is absolutely-multiplicative implies SF is properly-upper-bound )
assume A1: SF is absolutely-multiplicative ; ::_thesis: SF is properly-upper-bound
|:a:| = [[0]] I by Def3;
then A2: meet |:a:| = M by MSSUBFAM:41;
a c= SF by XBOOLE_1:2;
hence M in SF by A1, A2, Def7; :: according to CLOSURE2:def_8 ::_thesis: verum
end;
end;
registration
let I be set ;
let M be ManySortedSet of I;
cluster properly-upper-bound -> non empty for Element of bool (Bool M);
coherence
for b1 being SubsetFamily of M st b1 is properly-upper-bound holds
not b1 is empty by Def8;
end;
registration
let I be set ;
let M be ManySortedSet of I;
cluster absolutely-additive -> properly-lower-bound for Element of bool (Bool M);
coherence
for b1 being SubsetFamily of M st b1 is absolutely-additive holds
b1 is properly-lower-bound
proof
reconsider a = {} as SubsetFamily of M by XBOOLE_1:2;
let SF be SubsetFamily of M; ::_thesis: ( SF is absolutely-additive implies SF is properly-lower-bound )
assume A1: SF is absolutely-additive ; ::_thesis: SF is properly-lower-bound
|:a:| = [[0]] I by Def3;
then A2: union |:a:| = [[0]] I by MBOOLEAN:21;
a c= SF by XBOOLE_1:2;
hence [[0]] I in SF by A1, A2, Def5; :: according to CLOSURE2:def_9 ::_thesis: verum
end;
end;
registration
let I be set ;
let M be ManySortedSet of I;
cluster properly-lower-bound -> non empty for Element of bool (Bool M);
coherence
for b1 being SubsetFamily of M st b1 is properly-lower-bound holds
not b1 is empty by Def9;
end;
begin
definition
let I be set ;
let M be ManySortedSet of I;
mode SetOp of M is Function of (Bool M),(Bool M);
end;
definition
let I be set ;
let M be ManySortedSet of I;
let f be SetOp of M;
let x be Element of Bool M;
:: original: .
redefine funcf . x -> Element of Bool M;
coherence
f . x is Element of Bool M
proof
f . x in Bool M ;
hence f . x is Element of Bool M ; ::_thesis: verum
end;
end;
definition
let I be set ;
let M be ManySortedSet of I;
let IT be SetOp of M;
attrIT is reflexive means :Def10: :: CLOSURE2:def 10
for x being Element of Bool M holds x c=' IT . x;
attrIT is monotonic means :Def11: :: CLOSURE2:def 11
for x, y being Element of Bool M st x c=' y holds
IT . x c=' IT . y;
attrIT is idempotent means :Def12: :: CLOSURE2:def 12
for x being Element of Bool M holds IT . x = IT . (IT . x);
attrIT is topological means :Def13: :: CLOSURE2:def 13
for x, y being Element of Bool M holds IT . (x \/ y) = (IT . x) \/ (IT . y);
end;
:: deftheorem Def10 defines reflexive CLOSURE2:def_10_:_
for I being set
for M being ManySortedSet of I
for IT being SetOp of M holds
( IT is reflexive iff for x being Element of Bool M holds x c=' IT . x );
:: deftheorem Def11 defines monotonic CLOSURE2:def_11_:_
for I being set
for M being ManySortedSet of I
for IT being SetOp of M holds
( IT is monotonic iff for x, y being Element of Bool M st x c=' y holds
IT . x c=' IT . y );
:: deftheorem Def12 defines idempotent CLOSURE2:def_12_:_
for I being set
for M being ManySortedSet of I
for IT being SetOp of M holds
( IT is idempotent iff for x being Element of Bool M holds IT . x = IT . (IT . x) );
:: deftheorem Def13 defines topological CLOSURE2:def_13_:_
for I being set
for M being ManySortedSet of I
for IT being SetOp of M holds
( IT is topological iff for x, y being Element of Bool M holds IT . (x \/ y) = (IT . x) \/ (IT . y) );
registration
let I be set ;
let M be ManySortedSet of I;
cluster non empty Relation-like Function-like V17( Bool M) quasi_total reflexive monotonic idempotent topological for Element of bool [:(Bool M),(Bool M):];
existence
ex b1 being SetOp of M st
( b1 is reflexive & b1 is monotonic & b1 is idempotent & b1 is topological )
proof
reconsider f = id (Bool M) as SetOp of M ;
take f ; ::_thesis: ( f is reflexive & f is monotonic & f is idempotent & f is topological )
thus f is reflexive ::_thesis: ( f is monotonic & f is idempotent & f is topological )
proof
let X be Element of Bool M; :: according to CLOSURE2:def_10 ::_thesis: X c=' f . X
thus X c=' f . X by FUNCT_1:18; ::_thesis: verum
end;
thus f is monotonic ::_thesis: ( f is idempotent & f is topological )
proof
let X, Y be Element of Bool M; :: according to CLOSURE2:def_11 ::_thesis: ( X c=' Y implies f . X c=' f . Y )
assume A1: X c= Y ; ::_thesis: f . X c=' f . Y
f . X = X by FUNCT_1:18;
hence f . X c=' f . Y by A1, FUNCT_1:18; ::_thesis: verum
end;
thus f is idempotent ::_thesis: f is topological
proof
let X be Element of Bool M; :: according to CLOSURE2:def_12 ::_thesis: f . X = f . (f . X)
thus f . (f . X) = f . X by FUNCT_1:18; ::_thesis: verum
end;
thus f is topological ::_thesis: verum
proof
let X, Y be Element of Bool M; :: according to CLOSURE2:def_13 ::_thesis: f . (X \/ Y) = (f . X) \/ (f . Y)
( X c= M & Y c= M ) by PBOOLE:def_18;
then X \/ Y c= M by PBOOLE:16;
then X \/ Y is ManySortedSubset of M by PBOOLE:def_18;
then X \/ Y in Bool M by Def1;
hence f . (X \/ Y) = X \/ Y by FUNCT_1:18
.= (f . X) \/ Y by FUNCT_1:18
.= (f . X) \/ (f . Y) by FUNCT_1:18 ;
::_thesis: verum
end;
end;
end;
theorem :: CLOSURE2:26
for I being set
for A being ManySortedSet of I holds id (Bool A) is reflexive SetOp of A
proof
let I be set ; ::_thesis: for A being ManySortedSet of I holds id (Bool A) is reflexive SetOp of A
let A be ManySortedSet of I; ::_thesis: id (Bool A) is reflexive SetOp of A
reconsider f = id (Bool A) as SetOp of A ;
f is reflexive
proof
let X be Element of Bool A; :: according to CLOSURE2:def_10 ::_thesis: X c=' f . X
thus X c=' f . X by FUNCT_1:18; ::_thesis: verum
end;
hence id (Bool A) is reflexive SetOp of A ; ::_thesis: verum
end;
theorem :: CLOSURE2:27
for I being set
for A being ManySortedSet of I holds id (Bool A) is monotonic SetOp of A
proof
let I be set ; ::_thesis: for A being ManySortedSet of I holds id (Bool A) is monotonic SetOp of A
let A be ManySortedSet of I; ::_thesis: id (Bool A) is monotonic SetOp of A
reconsider f = id (Bool A) as SetOp of A ;
f is monotonic
proof
let X, Y be Element of Bool A; :: according to CLOSURE2:def_11 ::_thesis: ( X c=' Y implies f . X c=' f . Y )
assume A1: X c= Y ; ::_thesis: f . X c=' f . Y
f . X = X by FUNCT_1:18;
hence f . X c=' f . Y by A1, FUNCT_1:18; ::_thesis: verum
end;
hence id (Bool A) is monotonic SetOp of A ; ::_thesis: verum
end;
theorem :: CLOSURE2:28
for I being set
for A being ManySortedSet of I holds id (Bool A) is idempotent SetOp of A
proof
let I be set ; ::_thesis: for A being ManySortedSet of I holds id (Bool A) is idempotent SetOp of A
let A be ManySortedSet of I; ::_thesis: id (Bool A) is idempotent SetOp of A
reconsider f = id (Bool A) as SetOp of A ;
f is idempotent
proof
let X be Element of Bool A; :: according to CLOSURE2:def_12 ::_thesis: f . X = f . (f . X)
thus f . (f . X) = f . X by FUNCT_1:18; ::_thesis: verum
end;
hence id (Bool A) is idempotent SetOp of A ; ::_thesis: verum
end;
theorem :: CLOSURE2:29
for I being set
for A being ManySortedSet of I holds id (Bool A) is topological SetOp of A
proof
let I be set ; ::_thesis: for A being ManySortedSet of I holds id (Bool A) is topological SetOp of A
let A be ManySortedSet of I; ::_thesis: id (Bool A) is topological SetOp of A
reconsider f = id (Bool A) as SetOp of A ;
f is topological
proof
let X, Y be Element of Bool A; :: according to CLOSURE2:def_13 ::_thesis: f . (X \/ Y) = (f . X) \/ (f . Y)
( X c= A & Y c= A ) by PBOOLE:def_18;
then X \/ Y c= A by PBOOLE:16;
then X \/ Y is ManySortedSubset of A by PBOOLE:def_18;
then X \/ Y in Bool A by Def1;
hence f . (X \/ Y) = X \/ Y by FUNCT_1:18
.= (f . X) \/ Y by FUNCT_1:18
.= (f . X) \/ (f . Y) by FUNCT_1:18 ;
::_thesis: verum
end;
hence id (Bool A) is topological SetOp of A ; ::_thesis: verum
end;
theorem :: CLOSURE2:30
for I being set
for M being ManySortedSet of I
for E being Element of Bool M
for g being SetOp of M st E = M & g is reflexive holds
E = g . E
proof
let I be set ; ::_thesis: for M being ManySortedSet of I
for E being Element of Bool M
for g being SetOp of M st E = M & g is reflexive holds
E = g . E
let M be ManySortedSet of I; ::_thesis: for E being Element of Bool M
for g being SetOp of M st E = M & g is reflexive holds
E = g . E
let E be Element of Bool M; ::_thesis: for g being SetOp of M st E = M & g is reflexive holds
E = g . E
let g be SetOp of M; ::_thesis: ( E = M & g is reflexive implies E = g . E )
assume A1: E = M ; ::_thesis: ( not g is reflexive or E = g . E )
assume g is reflexive ; ::_thesis: E = g . E
then A2: E c= g . E by Def10;
g . E c= E by A1, PBOOLE:def_18;
hence E = g . E by A2, PBOOLE:146; ::_thesis: verum
end;
theorem :: CLOSURE2:31
for I being set
for M being ManySortedSet of I
for g being SetOp of M st g is reflexive & ( for X being Element of Bool M holds g . X c= X ) holds
g is idempotent
proof
let I be set ; ::_thesis: for M being ManySortedSet of I
for g being SetOp of M st g is reflexive & ( for X being Element of Bool M holds g . X c= X ) holds
g is idempotent
let M be ManySortedSet of I; ::_thesis: for g being SetOp of M st g is reflexive & ( for X being Element of Bool M holds g . X c= X ) holds
g is idempotent
let g be SetOp of M; ::_thesis: ( g is reflexive & ( for X being Element of Bool M holds g . X c= X ) implies g is idempotent )
assume that
A1: g is reflexive and
A2: for X being Element of Bool M holds g . X c= X ; ::_thesis: g is idempotent
let X be Element of Bool M; :: according to CLOSURE2:def_12 ::_thesis: g . X = g . (g . X)
A3: g . X c= g . (g . X) by A1, Def10;
g . (g . X) c= g . X by A2;
hence g . X = g . (g . X) by A3, PBOOLE:146; ::_thesis: verum
end;
theorem :: CLOSURE2:32
for I being set
for M being ManySortedSet of I
for E, T being Element of Bool M
for g being SetOp of M
for A being Element of Bool M st A = E /\ T & g is monotonic holds
g . A c= (g . E) /\ (g . T)
proof
let I be set ; ::_thesis: for M being ManySortedSet of I
for E, T being Element of Bool M
for g being SetOp of M
for A being Element of Bool M st A = E /\ T & g is monotonic holds
g . A c= (g . E) /\ (g . T)
let M be ManySortedSet of I; ::_thesis: for E, T being Element of Bool M
for g being SetOp of M
for A being Element of Bool M st A = E /\ T & g is monotonic holds
g . A c= (g . E) /\ (g . T)
let E, T be Element of Bool M; ::_thesis: for g being SetOp of M
for A being Element of Bool M st A = E /\ T & g is monotonic holds
g . A c= (g . E) /\ (g . T)
let g be SetOp of M; ::_thesis: for A being Element of Bool M st A = E /\ T & g is monotonic holds
g . A c= (g . E) /\ (g . T)
let A be Element of Bool M; ::_thesis: ( A = E /\ T & g is monotonic implies g . A c= (g . E) /\ (g . T) )
assume A1: A = E /\ T ; ::_thesis: ( not g is monotonic or g . A c= (g . E) /\ (g . T) )
assume A2: g is monotonic ; ::_thesis: g . A c= (g . E) /\ (g . T)
E /\ T c= T by PBOOLE:15;
then A3: g . A c= g . T by A1, A2, Def11;
E /\ T c= E by PBOOLE:15;
then g . A c= g . E by A1, A2, Def11;
hence g . A c= (g . E) /\ (g . T) by A3, PBOOLE:17; ::_thesis: verum
end;
registration
let I be set ;
let M be ManySortedSet of I;
cluster Function-like quasi_total topological -> monotonic for Element of bool [:(Bool M),(Bool M):];
coherence
for b1 being SetOp of M st b1 is topological holds
b1 is monotonic
proof
let g be SetOp of M; ::_thesis: ( g is topological implies g is monotonic )
assume A1: g is topological ; ::_thesis: g is monotonic
let X, Y be Element of Bool M; :: according to CLOSURE2:def_11 ::_thesis: ( X c=' Y implies g . X c=' g . Y )
assume A2: X c= Y ; ::_thesis: g . X c=' g . Y
(g . X) \/ (g . Y) = g . (X \/ Y) by A1, Def13
.= g . Y by A2, PBOOLE:22 ;
hence g . X c=' g . Y by PBOOLE:26; ::_thesis: verum
end;
end;
theorem :: CLOSURE2:33
for I being set
for M being ManySortedSet of I
for E, T being Element of Bool M
for g being SetOp of M
for A being Element of Bool M st A = E \ T & g is topological holds
(g . E) \ (g . T) c= g . A
proof
let I be set ; ::_thesis: for M being ManySortedSet of I
for E, T being Element of Bool M
for g being SetOp of M
for A being Element of Bool M st A = E \ T & g is topological holds
(g . E) \ (g . T) c= g . A
let M be ManySortedSet of I; ::_thesis: for E, T being Element of Bool M
for g being SetOp of M
for A being Element of Bool M st A = E \ T & g is topological holds
(g . E) \ (g . T) c= g . A
let E, T be Element of Bool M; ::_thesis: for g being SetOp of M
for A being Element of Bool M st A = E \ T & g is topological holds
(g . E) \ (g . T) c= g . A
let g be SetOp of M; ::_thesis: for A being Element of Bool M st A = E \ T & g is topological holds
(g . E) \ (g . T) c= g . A
let A be Element of Bool M; ::_thesis: ( A = E \ T & g is topological implies (g . E) \ (g . T) c= g . A )
assume A1: A = E \ T ; ::_thesis: ( not g is topological or (g . E) \ (g . T) c= g . A )
assume A2: g is topological ; ::_thesis: (g . E) \ (g . T) c= g . A
then (g . E) \/ (g . T) = g . (E \/ T) by Def13
.= g . ((E \ T) \/ T) by PBOOLE:67
.= (g . A) \/ (g . T) by A1, A2, Def13 ;
then g . E c= (g . A) \/ (g . T) by PBOOLE:14;
then (g . E) \ (g . T) c= ((g . A) \/ (g . T)) \ (g . T) by PBOOLE:53;
then A3: (g . E) \ (g . T) c= (g . A) \ (g . T) by PBOOLE:75;
(g . A) \ (g . T) c= g . A by PBOOLE:56;
hence (g . E) \ (g . T) c= g . A by A3, PBOOLE:13; ::_thesis: verum
end;
definition
let I be set ;
let M be ManySortedSet of I;
let h, g be SetOp of M;
:: original: *
redefine funcg * h -> SetOp of M;
coherence
h * g is SetOp of M
proof
g * h is Function of (Bool M),(Bool M) ;
hence h * g is SetOp of M ; ::_thesis: verum
end;
end;
theorem :: CLOSURE2:34
for I being set
for M being ManySortedSet of I
for g, h being SetOp of M st g is reflexive & h is reflexive holds
g * h is reflexive
proof
let I be set ; ::_thesis: for M being ManySortedSet of I
for g, h being SetOp of M st g is reflexive & h is reflexive holds
g * h is reflexive
let M be ManySortedSet of I; ::_thesis: for g, h being SetOp of M st g is reflexive & h is reflexive holds
g * h is reflexive
let g, h be SetOp of M; ::_thesis: ( g is reflexive & h is reflexive implies g * h is reflexive )
assume A1: ( g is reflexive & h is reflexive ) ; ::_thesis: g * h is reflexive
let X be Element of Bool M; :: according to CLOSURE2:def_10 ::_thesis: X c=' (g * h) . X
( X c= h . X & h . X c= g . (h . X) ) by A1, Def10;
then ( dom h = Bool M & X c= g . (h . X) ) by FUNCT_2:def_1, PBOOLE:13;
hence X c=' (g * h) . X by FUNCT_1:13; ::_thesis: verum
end;
theorem :: CLOSURE2:35
for I being set
for M being ManySortedSet of I
for g, h being SetOp of M st g is monotonic & h is monotonic holds
g * h is monotonic
proof
let I be set ; ::_thesis: for M being ManySortedSet of I
for g, h being SetOp of M st g is monotonic & h is monotonic holds
g * h is monotonic
let M be ManySortedSet of I; ::_thesis: for g, h being SetOp of M st g is monotonic & h is monotonic holds
g * h is monotonic
let g, h be SetOp of M; ::_thesis: ( g is monotonic & h is monotonic implies g * h is monotonic )
assume that
A1: g is monotonic and
A2: h is monotonic ; ::_thesis: g * h is monotonic
A3: dom h = Bool M by FUNCT_2:def_1;
let X, Y be Element of Bool M; :: according to CLOSURE2:def_11 ::_thesis: ( X c=' Y implies (g * h) . X c=' (g * h) . Y )
assume X c= Y ; ::_thesis: (g * h) . X c=' (g * h) . Y
then h . X c= h . Y by A2, Def11;
then g . (h . X) c= g . (h . Y) by A1, Def11;
then g . (h . X) c= (g * h) . Y by A3, FUNCT_1:13;
hence (g * h) . X c=' (g * h) . Y by A3, FUNCT_1:13; ::_thesis: verum
end;
theorem :: CLOSURE2:36
for I being set
for M being ManySortedSet of I
for g, h being SetOp of M st g is idempotent & h is idempotent & g * h = h * g holds
g * h is idempotent
proof
let I be set ; ::_thesis: for M being ManySortedSet of I
for g, h being SetOp of M st g is idempotent & h is idempotent & g * h = h * g holds
g * h is idempotent
let M be ManySortedSet of I; ::_thesis: for g, h being SetOp of M st g is idempotent & h is idempotent & g * h = h * g holds
g * h is idempotent
let g, h be SetOp of M; ::_thesis: ( g is idempotent & h is idempotent & g * h = h * g implies g * h is idempotent )
assume that
A1: g is idempotent and
A2: h is idempotent and
A3: g * h = h * g ; ::_thesis: g * h is idempotent
let X be Element of Bool M; :: according to CLOSURE2:def_12 ::_thesis: (g * h) . X = (g * h) . ((g * h) . X)
A4: dom g = Bool M by FUNCT_2:def_1;
A5: dom h = Bool M by FUNCT_2:def_1;
hence (g * h) . X = g . (h . X) by FUNCT_1:13
.= g . (h . (h . X)) by A2, Def12
.= g . (g . (h . (h . X))) by A1, Def12
.= g . ((h * g) . (h . X)) by A3, A5, FUNCT_1:13
.= g . (h . (g . (h . X))) by A4, FUNCT_1:13
.= g . (h . ((g * h) . X)) by A5, FUNCT_1:13
.= (g * h) . ((g * h) . X) by A5, FUNCT_1:13 ;
::_thesis: verum
end;
theorem :: CLOSURE2:37
for I being set
for M being ManySortedSet of I
for g, h being SetOp of M st g is topological & h is topological holds
g * h is topological
proof
let I be set ; ::_thesis: for M being ManySortedSet of I
for g, h being SetOp of M st g is topological & h is topological holds
g * h is topological
let M be ManySortedSet of I; ::_thesis: for g, h being SetOp of M st g is topological & h is topological holds
g * h is topological
let g, h be SetOp of M; ::_thesis: ( g is topological & h is topological implies g * h is topological )
assume that
A1: g is topological and
A2: h is topological ; ::_thesis: g * h is topological
let X, Y be Element of Bool M; :: according to CLOSURE2:def_13 ::_thesis: (g * h) . (X \/ Y) = ((g * h) . X) \/ ((g * h) . Y)
A3: dom h = Bool M by FUNCT_2:def_1;
hence (g * h) . (X \/ Y) = g . (h . (X \/ Y)) by Th10, FUNCT_1:13
.= g . ((h . X) \/ (h . Y)) by A2, Def13
.= (g . (h . X)) \/ (g . (h . Y)) by A1, Def13
.= ((g * h) . X) \/ (g . (h . Y)) by A3, FUNCT_1:13
.= ((g * h) . X) \/ ((g * h) . Y) by A3, FUNCT_1:13 ;
::_thesis: verum
end;
begin
definition
let S be 1-sorted ;
attrc2 is strict ;
struct ClosureStr over S -> many-sorted over S;
aggrClosureStr(# Sorts, Family #) -> ClosureStr over S;
sel Family c2 -> SubsetFamily of the Sorts of c2;
end;
definition
let S be 1-sorted ;
let IT be ClosureStr over S;
attrIT is additive means :Def14: :: CLOSURE2:def 14
the Family of IT is additive ;
attrIT is absolutely-additive means :Def15: :: CLOSURE2:def 15
the Family of IT is absolutely-additive ;
attrIT is multiplicative means :Def16: :: CLOSURE2:def 16
the Family of IT is multiplicative ;
attrIT is absolutely-multiplicative means :Def17: :: CLOSURE2:def 17
the Family of IT is absolutely-multiplicative ;
attrIT is properly-upper-bound means :Def18: :: CLOSURE2:def 18
the Family of IT is properly-upper-bound ;
attrIT is properly-lower-bound means :Def19: :: CLOSURE2:def 19
the Family of IT is properly-lower-bound ;
end;
:: deftheorem Def14 defines additive CLOSURE2:def_14_:_
for S being 1-sorted
for IT being ClosureStr over S holds
( IT is additive iff the Family of IT is additive );
:: deftheorem Def15 defines absolutely-additive CLOSURE2:def_15_:_
for S being 1-sorted
for IT being ClosureStr over S holds
( IT is absolutely-additive iff the Family of IT is absolutely-additive );
:: deftheorem Def16 defines multiplicative CLOSURE2:def_16_:_
for S being 1-sorted
for IT being ClosureStr over S holds
( IT is multiplicative iff the Family of IT is multiplicative );
:: deftheorem Def17 defines absolutely-multiplicative CLOSURE2:def_17_:_
for S being 1-sorted
for IT being ClosureStr over S holds
( IT is absolutely-multiplicative iff the Family of IT is absolutely-multiplicative );
:: deftheorem Def18 defines properly-upper-bound CLOSURE2:def_18_:_
for S being 1-sorted
for IT being ClosureStr over S holds
( IT is properly-upper-bound iff the Family of IT is properly-upper-bound );
:: deftheorem Def19 defines properly-lower-bound CLOSURE2:def_19_:_
for S being 1-sorted
for IT being ClosureStr over S holds
( IT is properly-lower-bound iff the Family of IT is properly-lower-bound );
definition
let S be 1-sorted ;
let MS be many-sorted over S;
func Full MS -> ClosureStr over S equals :: CLOSURE2:def 20
ClosureStr(# the Sorts of MS,(Bool the Sorts of MS) #);
correctness
coherence
ClosureStr(# the Sorts of MS,(Bool the Sorts of MS) #) is ClosureStr over S;
;
end;
:: deftheorem defines Full CLOSURE2:def_20_:_
for S being 1-sorted
for MS being many-sorted over S holds Full MS = ClosureStr(# the Sorts of MS,(Bool the Sorts of MS) #);
registration
let S be 1-sorted ;
let MS be many-sorted over S;
cluster Full MS -> strict additive absolutely-additive multiplicative absolutely-multiplicative properly-upper-bound properly-lower-bound ;
coherence
( Full MS is strict & Full MS is additive & Full MS is absolutely-additive & Full MS is multiplicative & Full MS is absolutely-multiplicative & Full MS is properly-upper-bound & Full MS is properly-lower-bound )
proof
thus Full MS is strict ; ::_thesis: ( Full MS is additive & Full MS is absolutely-additive & Full MS is multiplicative & Full MS is absolutely-multiplicative & Full MS is properly-upper-bound & Full MS is properly-lower-bound )
thus ( the Family of (Full MS) is additive & the Family of (Full MS) is absolutely-additive & the Family of (Full MS) is multiplicative & the Family of (Full MS) is absolutely-multiplicative & the Family of (Full MS) is properly-upper-bound & the Family of (Full MS) is properly-lower-bound ) ; :: according to CLOSURE2:def_14,CLOSURE2:def_15,CLOSURE2:def_16,CLOSURE2:def_17,CLOSURE2:def_18,CLOSURE2:def_19 ::_thesis: verum
end;
end;
registration
let S be 1-sorted ;
let MS be non-empty many-sorted over S;
cluster Full MS -> non-empty ;
coherence
Full MS is non-empty by MSUALG_1:def_3;
end;
registration
let S be 1-sorted ;
cluster non-empty strict additive absolutely-additive multiplicative absolutely-multiplicative properly-upper-bound properly-lower-bound for ClosureStr over S;
existence
ex b1 being ClosureStr over S st
( b1 is strict & b1 is non-empty & b1 is additive & b1 is absolutely-additive & b1 is multiplicative & b1 is absolutely-multiplicative & b1 is properly-upper-bound & b1 is properly-lower-bound )
proof
set a = the non-empty many-sorted over S;
take Full the non-empty many-sorted over S ; ::_thesis: ( Full the non-empty many-sorted over S is strict & Full the non-empty many-sorted over S is non-empty & Full the non-empty many-sorted over S is additive & Full the non-empty many-sorted over S is absolutely-additive & Full the non-empty many-sorted over S is multiplicative & Full the non-empty many-sorted over S is absolutely-multiplicative & Full the non-empty many-sorted over S is properly-upper-bound & Full the non-empty many-sorted over S is properly-lower-bound )
thus ( Full the non-empty many-sorted over S is strict & Full the non-empty many-sorted over S is non-empty & Full the non-empty many-sorted over S is additive & Full the non-empty many-sorted over S is absolutely-additive & Full the non-empty many-sorted over S is multiplicative & Full the non-empty many-sorted over S is absolutely-multiplicative & Full the non-empty many-sorted over S is properly-upper-bound & Full the non-empty many-sorted over S is properly-lower-bound ) ; ::_thesis: verum
end;
end;
registration
let S be 1-sorted ;
let CS be additive ClosureStr over S;
cluster the Family of CS -> additive ;
coherence
the Family of CS is additive by Def14;
end;
registration
let S be 1-sorted ;
let CS be absolutely-additive ClosureStr over S;
cluster the Family of CS -> absolutely-additive ;
coherence
the Family of CS is absolutely-additive by Def15;
end;
registration
let S be 1-sorted ;
let CS be multiplicative ClosureStr over S;
cluster the Family of CS -> multiplicative ;
coherence
the Family of CS is multiplicative by Def16;
end;
registration
let S be 1-sorted ;
let CS be absolutely-multiplicative ClosureStr over S;
cluster the Family of CS -> absolutely-multiplicative ;
coherence
the Family of CS is absolutely-multiplicative by Def17;
end;
registration
let S be 1-sorted ;
let CS be properly-upper-bound ClosureStr over S;
cluster the Family of CS -> properly-upper-bound ;
coherence
the Family of CS is properly-upper-bound by Def18;
end;
registration
let S be 1-sorted ;
let CS be properly-lower-bound ClosureStr over S;
cluster the Family of CS -> properly-lower-bound ;
coherence
the Family of CS is properly-lower-bound by Def19;
end;
registration
let S be 1-sorted ;
let M be V8() ManySortedSet of the carrier of S;
let F be SubsetFamily of M;
cluster ClosureStr(# M,F #) -> non-empty ;
coherence
ClosureStr(# M,F #) is non-empty
proof
thus the Sorts of ClosureStr(# M,F #) is V8() ; :: according to MSUALG_1:def_3 ::_thesis: verum
end;
end;
registration
let S be 1-sorted ;
let MS be many-sorted over S;
let F be additive SubsetFamily of the Sorts of MS;
cluster ClosureStr(# the Sorts of MS,F #) -> additive ;
coherence
ClosureStr(# the Sorts of MS,F #) is additive by Def14;
end;
registration
let S be 1-sorted ;
let MS be many-sorted over S;
let F be absolutely-additive SubsetFamily of the Sorts of MS;
cluster ClosureStr(# the Sorts of MS,F #) -> absolutely-additive ;
coherence
ClosureStr(# the Sorts of MS,F #) is absolutely-additive by Def15;
end;
registration
let S be 1-sorted ;
let MS be many-sorted over S;
let F be multiplicative SubsetFamily of the Sorts of MS;
cluster ClosureStr(# the Sorts of MS,F #) -> multiplicative ;
coherence
ClosureStr(# the Sorts of MS,F #) is multiplicative by Def16;
end;
registration
let S be 1-sorted ;
let MS be many-sorted over S;
let F be absolutely-multiplicative SubsetFamily of the Sorts of MS;
cluster ClosureStr(# the Sorts of MS,F #) -> absolutely-multiplicative ;
coherence
ClosureStr(# the Sorts of MS,F #) is absolutely-multiplicative by Def17;
end;
registration
let S be 1-sorted ;
let MS be many-sorted over S;
let F be properly-upper-bound SubsetFamily of the Sorts of MS;
cluster ClosureStr(# the Sorts of MS,F #) -> properly-upper-bound ;
coherence
ClosureStr(# the Sorts of MS,F #) is properly-upper-bound by Def18;
end;
registration
let S be 1-sorted ;
let MS be many-sorted over S;
let F be properly-lower-bound SubsetFamily of the Sorts of MS;
cluster ClosureStr(# the Sorts of MS,F #) -> properly-lower-bound ;
coherence
ClosureStr(# the Sorts of MS,F #) is properly-lower-bound by Def19;
end;
registration
let S be 1-sorted ;
cluster absolutely-additive -> additive for ClosureStr over S;
coherence
for b1 being ClosureStr over S st b1 is absolutely-additive holds
b1 is additive
proof
let CS be ClosureStr over S; ::_thesis: ( CS is absolutely-additive implies CS is additive )
assume CS is absolutely-additive ; ::_thesis: CS is additive
hence the Family of CS is additive ; :: according to CLOSURE2:def_14 ::_thesis: verum
end;
end;
registration
let S be 1-sorted ;
cluster absolutely-multiplicative -> multiplicative for ClosureStr over S;
coherence
for b1 being ClosureStr over S st b1 is absolutely-multiplicative holds
b1 is multiplicative
proof
let CS be ClosureStr over S; ::_thesis: ( CS is absolutely-multiplicative implies CS is multiplicative )
assume CS is absolutely-multiplicative ; ::_thesis: CS is multiplicative
hence the Family of CS is multiplicative ; :: according to CLOSURE2:def_16 ::_thesis: verum
end;
end;
registration
let S be 1-sorted ;
cluster absolutely-multiplicative -> properly-upper-bound for ClosureStr over S;
coherence
for b1 being ClosureStr over S st b1 is absolutely-multiplicative holds
b1 is properly-upper-bound
proof
let CS be ClosureStr over S; ::_thesis: ( CS is absolutely-multiplicative implies CS is properly-upper-bound )
assume CS is absolutely-multiplicative ; ::_thesis: CS is properly-upper-bound
hence the Family of CS is properly-upper-bound ; :: according to CLOSURE2:def_18 ::_thesis: verum
end;
end;
registration
let S be 1-sorted ;
cluster absolutely-additive -> properly-lower-bound for ClosureStr over S;
coherence
for b1 being ClosureStr over S st b1 is absolutely-additive holds
b1 is properly-lower-bound
proof
let CS be ClosureStr over S; ::_thesis: ( CS is absolutely-additive implies CS is properly-lower-bound )
assume CS is absolutely-additive ; ::_thesis: CS is properly-lower-bound
hence the Family of CS is properly-lower-bound ; :: according to CLOSURE2:def_19 ::_thesis: verum
end;
end;
definition
let S be 1-sorted ;
mode ClosureSystem of S is absolutely-multiplicative ClosureStr over S;
end;
definition
let I be set ;
let M be ManySortedSet of I;
mode ClosureOperator of M is reflexive monotonic idempotent SetOp of M;
end;
definition
let S be 1-sorted ;
let A be ManySortedSet of the carrier of S;
let g be ClosureOperator of A;
func ClOp->ClSys g -> strict ClosureStr over S means :Def21: :: CLOSURE2:def 21
( the Sorts of it = A & the Family of it = { x where x is Element of Bool A : g . x = x } );
existence
ex b1 being strict ClosureStr over S st
( the Sorts of b1 = A & the Family of b1 = { x where x is Element of Bool A : g . x = x } )
proof
defpred S1[ set ] means g . $1 = $1;
set SF = { x where x is Element of Bool A : S1[x] } ;
{ x where x is Element of Bool A : S1[x] } is Subset of (Bool A) from DOMAIN_1:sch_7();
then reconsider D = { x where x is Element of Bool A : S1[x] } as SubsetFamily of A ;
take ClosureStr(# A,D #) ; ::_thesis: ( the Sorts of ClosureStr(# A,D #) = A & the Family of ClosureStr(# A,D #) = { x where x is Element of Bool A : g . x = x } )
thus ( the Sorts of ClosureStr(# A,D #) = A & the Family of ClosureStr(# A,D #) = { x where x is Element of Bool A : g . x = x } ) ; ::_thesis: verum
end;
uniqueness
for b1, b2 being strict ClosureStr over S st the Sorts of b1 = A & the Family of b1 = { x where x is Element of Bool A : g . x = x } & the Sorts of b2 = A & the Family of b2 = { x where x is Element of Bool A : g . x = x } holds
b1 = b2 ;
end;
:: deftheorem Def21 defines ClOp->ClSys CLOSURE2:def_21_:_
for S being 1-sorted
for A being ManySortedSet of the carrier of S
for g being ClosureOperator of A
for b4 being strict ClosureStr over S holds
( b4 = ClOp->ClSys g iff ( the Sorts of b4 = A & the Family of b4 = { x where x is Element of Bool A : g . x = x } ) );
registration
let S be 1-sorted ;
let A be ManySortedSet of the carrier of S;
let g be ClosureOperator of A;
cluster ClOp->ClSys g -> strict absolutely-multiplicative ;
coherence
ClOp->ClSys g is absolutely-multiplicative
proof
A1: the Sorts of (ClOp->ClSys g) = A by Def21;
defpred S1[ set ] means g . S = S;
set SF = { x where x is Element of Bool A : S1[x] } ;
A2: { x where x is Element of Bool A : S1[x] } = the Family of (ClOp->ClSys g) by Def21;
{ x where x is Element of Bool A : S1[x] } is Subset of (Bool A) from DOMAIN_1:sch_7();
then reconsider D = { x where x is Element of Bool A : S1[x] } as SubsetFamily of A ;
A3: ClOp->ClSys g = ClosureStr(# A,D #) by A1, A2;
D is absolutely-multiplicative
proof
let F be SubsetFamily of A; :: according to CLOSURE2:def_7 ::_thesis: ( F c= D implies meet |:F:| in D )
assume A4: F c= D ; ::_thesis: meet |:F:| in D
reconsider mf = meet |:F:| as Element of Bool A by Def1;
now__::_thesis:_for_Z1_being_ManySortedSet_of_the_carrier_of_S_st_Z1_in_F_holds_
g_._mf_c='_Z1
let Z1 be ManySortedSet of the carrier of S; ::_thesis: ( Z1 in F implies g . mf c=' Z1 )
assume A5: Z1 in F ; ::_thesis: g . mf c=' Z1
then reconsider y1 = Z1 as Element of Bool A ;
Z1 in D by A4, A5;
then A6: ex a being Element of Bool A st
( Z1 = a & g . a = a ) ;
mf c=' y1 by A5, Th21, MSSUBFAM:43;
hence g . mf c=' Z1 by A6, Def11; ::_thesis: verum
end;
then A7: g . mf c=' mf by Th24;
mf c=' g . mf by Def10;
then g . mf = mf by A7, PBOOLE:146;
hence meet |:F:| in D ; ::_thesis: verum
end;
hence ClOp->ClSys g is absolutely-multiplicative by A3; ::_thesis: verum
end;
end;
definition
let S be 1-sorted ;
let A be ClosureSystem of S;
let C be ManySortedSubset of the Sorts of A;
func Cl C -> Element of Bool the Sorts of A means :Def22: :: CLOSURE2:def 22
ex F being SubsetFamily of the Sorts of A st
( it = meet |:F:| & F = { X where X is Element of Bool the Sorts of A : ( C c=' X & X in the Family of A ) } );
existence
ex b1 being Element of Bool the Sorts of A ex F being SubsetFamily of the Sorts of A st
( b1 = meet |:F:| & F = { X where X is Element of Bool the Sorts of A : ( C c=' X & X in the Family of A ) } )
proof
defpred S1[ Element of Bool the Sorts of A] means ( C c= $1 & $1 in the Family of A );
{ X where X is Element of Bool the Sorts of A : S1[X] } is Subset of (Bool the Sorts of A) from DOMAIN_1:sch_7();
then reconsider F = { X where X is Element of Bool the Sorts of A : ( C c= X & X in the Family of A ) } as SubsetFamily of the Sorts of A ;
reconsider IT = meet |:F:| as Element of Bool the Sorts of A by Def1;
take IT ; ::_thesis: ex F being SubsetFamily of the Sorts of A st
( IT = meet |:F:| & F = { X where X is Element of Bool the Sorts of A : ( C c=' X & X in the Family of A ) } )
take F ; ::_thesis: ( IT = meet |:F:| & F = { X where X is Element of Bool the Sorts of A : ( C c=' X & X in the Family of A ) } )
thus ( IT = meet |:F:| & F = { X where X is Element of Bool the Sorts of A : ( C c=' X & X in the Family of A ) } ) ; ::_thesis: verum
end;
uniqueness
for b1, b2 being Element of Bool the Sorts of A st ex F being SubsetFamily of the Sorts of A st
( b1 = meet |:F:| & F = { X where X is Element of Bool the Sorts of A : ( C c=' X & X in the Family of A ) } ) & ex F being SubsetFamily of the Sorts of A st
( b2 = meet |:F:| & F = { X where X is Element of Bool the Sorts of A : ( C c=' X & X in the Family of A ) } ) holds
b1 = b2 ;
end;
:: deftheorem Def22 defines Cl CLOSURE2:def_22_:_
for S being 1-sorted
for A being ClosureSystem of S
for C being ManySortedSubset of the Sorts of A
for b4 being Element of Bool the Sorts of A holds
( b4 = Cl C iff ex F being SubsetFamily of the Sorts of A st
( b4 = meet |:F:| & F = { X where X is Element of Bool the Sorts of A : ( C c=' X & X in the Family of A ) } ) );
theorem Th38: :: CLOSURE2:38
for S being 1-sorted
for D being ClosureSystem of S
for a being Element of Bool the Sorts of D
for f being SetOp of the Sorts of D st a in the Family of D & ( for x being Element of Bool the Sorts of D holds f . x = Cl x ) holds
f . a = a
proof
let S be 1-sorted ; ::_thesis: for D being ClosureSystem of S
for a being Element of Bool the Sorts of D
for f being SetOp of the Sorts of D st a in the Family of D & ( for x being Element of Bool the Sorts of D holds f . x = Cl x ) holds
f . a = a
let D be ClosureSystem of S; ::_thesis: for a being Element of Bool the Sorts of D
for f being SetOp of the Sorts of D st a in the Family of D & ( for x being Element of Bool the Sorts of D holds f . x = Cl x ) holds
f . a = a
let a be Element of Bool the Sorts of D; ::_thesis: for f being SetOp of the Sorts of D st a in the Family of D & ( for x being Element of Bool the Sorts of D holds f . x = Cl x ) holds
f . a = a
let f be SetOp of the Sorts of D; ::_thesis: ( a in the Family of D & ( for x being Element of Bool the Sorts of D holds f . x = Cl x ) implies f . a = a )
assume that
A1: a in the Family of D and
A2: for x being Element of Bool the Sorts of D holds f . x = Cl x ; ::_thesis: f . a = a
consider F being SubsetFamily of the Sorts of D such that
A3: Cl a = meet |:F:| and
A4: F = { X where X is Element of Bool the Sorts of D : ( a c=' X & X in the Family of D ) } by Def22;
A5: f . a = meet |:F:| by A2, A3;
a in F by A1, A4;
then A6: f . a c= a by A5, Th21, MSSUBFAM:43;
for Z1 being ManySortedSet of the carrier of S st Z1 in F holds
a c=' Z1
proof
let Z1 be ManySortedSet of the carrier of S; ::_thesis: ( Z1 in F implies a c=' Z1 )
assume Z1 in F ; ::_thesis: a c=' Z1
then ex b being Element of Bool the Sorts of D st
( Z1 = b & a c=' b & b in the Family of D ) by A4;
hence a c=' Z1 ; ::_thesis: verum
end;
then a c= f . a by A5, Th24;
hence f . a = a by A6, PBOOLE:146; ::_thesis: verum
end;
theorem :: CLOSURE2:39
for S being 1-sorted
for D being ClosureSystem of S
for a being Element of Bool the Sorts of D
for f being SetOp of the Sorts of D st f . a = a & ( for x being Element of Bool the Sorts of D holds f . x = Cl x ) holds
a in the Family of D
proof
let S be 1-sorted ; ::_thesis: for D being ClosureSystem of S
for a being Element of Bool the Sorts of D
for f being SetOp of the Sorts of D st f . a = a & ( for x being Element of Bool the Sorts of D holds f . x = Cl x ) holds
a in the Family of D
deffunc H1( set ) -> set = $1;
let D be ClosureSystem of S; ::_thesis: for a being Element of Bool the Sorts of D
for f being SetOp of the Sorts of D st f . a = a & ( for x being Element of Bool the Sorts of D holds f . x = Cl x ) holds
a in the Family of D
let a be Element of Bool the Sorts of D; ::_thesis: for f being SetOp of the Sorts of D st f . a = a & ( for x being Element of Bool the Sorts of D holds f . x = Cl x ) holds
a in the Family of D
let f be SetOp of the Sorts of D; ::_thesis: ( f . a = a & ( for x being Element of Bool the Sorts of D holds f . x = Cl x ) implies a in the Family of D )
assume A1: ( f . a = a & ( for x being Element of Bool the Sorts of D holds f . x = Cl x ) ) ; ::_thesis: a in the Family of D
set F = the Family of D;
set M = the Sorts of D;
defpred S1[ Element of Bool the Sorts of D] means a c=' $1;
defpred S2[ Element of Bool the Sorts of D] means ( a c=' $1 & $1 in the Family of D );
defpred S3[ Element of Bool the Sorts of D] means ( $1 in the Family of D & a c=' $1 );
A2: { H1(w) where w is Element of Bool the Sorts of D : ( H1(w) in the Family of D & S1[w] ) } c= the Family of D from FRAENKEL:sch_17();
A3: for q being Element of Bool the Sorts of D holds
( S2[q] iff S3[q] ) ;
A4: { H1(s) where s is Element of Bool the Sorts of D : S2[s] } = { H1(b) where b is Element of Bool the Sorts of D : S3[b] } from FRAENKEL:sch_3(A3);
consider SF being SubsetFamily of the Sorts of D such that
A5: Cl a = meet |:SF:| and
A6: SF = { X where X is Element of Bool the Sorts of D : ( a c= X & X in the Family of D ) } by Def22;
a = meet |:SF:| by A1, A5;
hence a in the Family of D by A6, A2, A4, Def7; ::_thesis: verum
end;
theorem Th40: :: CLOSURE2:40
for S being 1-sorted
for D being ClosureSystem of S
for f being SetOp of the Sorts of D st ( for x being Element of Bool the Sorts of D holds f . x = Cl x ) holds
( f is reflexive & f is monotonic & f is idempotent )
proof
let S be 1-sorted ; ::_thesis: for D being ClosureSystem of S
for f being SetOp of the Sorts of D st ( for x being Element of Bool the Sorts of D holds f . x = Cl x ) holds
( f is reflexive & f is monotonic & f is idempotent )
let D be ClosureSystem of S; ::_thesis: for f being SetOp of the Sorts of D st ( for x being Element of Bool the Sorts of D holds f . x = Cl x ) holds
( f is reflexive & f is monotonic & f is idempotent )
let f be SetOp of the Sorts of D; ::_thesis: ( ( for x being Element of Bool the Sorts of D holds f . x = Cl x ) implies ( f is reflexive & f is monotonic & f is idempotent ) )
assume A1: for x being Element of Bool the Sorts of D holds f . x = Cl x ; ::_thesis: ( f is reflexive & f is monotonic & f is idempotent )
set M = the Sorts of D;
A2: f is reflexive
proof
let x be Element of Bool the Sorts of D; :: according to CLOSURE2:def_10 ::_thesis: x c=' f . x
consider F being SubsetFamily of the Sorts of D such that
A3: Cl x = meet |:F:| and
A4: F = { X where X is Element of Bool the Sorts of D : ( x c=' X & X in the Family of D ) } by Def22;
A5: for Z1 being ManySortedSet of the carrier of S st Z1 in F holds
x c=' Z1
proof
let Z1 be ManySortedSet of the carrier of S; ::_thesis: ( Z1 in F implies x c=' Z1 )
assume Z1 in F ; ::_thesis: x c=' Z1
then ex a being Element of Bool the Sorts of D st
( Z1 = a & x c=' a & a in the Family of D ) by A4;
hence x c=' Z1 ; ::_thesis: verum
end;
f . x = meet |:F:| by A1, A3;
hence x c=' f . x by A5, Th24; ::_thesis: verum
end;
A6: f is monotonic
proof
let x, y be Element of Bool the Sorts of D; :: according to CLOSURE2:def_11 ::_thesis: ( x c=' y implies f . x c=' f . y )
assume A7: x c=' y ; ::_thesis: f . x c=' f . y
consider Fy being SubsetFamily of the Sorts of D such that
A8: Cl y = meet |:Fy:| and
A9: Fy = { X where X is Element of Bool the Sorts of D : ( y c=' X & X in the Family of D ) } by Def22;
consider Fx being SubsetFamily of the Sorts of D such that
A10: Cl x = meet |:Fx:| and
A11: Fx = { X where X is Element of Bool the Sorts of D : ( x c=' X & X in the Family of D ) } by Def22;
|:Fy:| c=' |:Fx:|
proof
let i be set ; :: according to PBOOLE:def_2 ::_thesis: ( not i in the carrier of S or |:Fy:| . i c= |:Fx:| . i )
assume A12: i in the carrier of S ; ::_thesis: |:Fy:| . i c= |:Fx:| . i
thus |:Fy:| . i c= |:Fx:| . i ::_thesis: verum
proof
let q be set ; :: according to TARSKI:def_3 ::_thesis: ( not q in |:Fy:| . i or q in |:Fx:| . i )
assume A13: q in |:Fy:| . i ; ::_thesis: q in |:Fx:| . i
percases ( Fy is empty or not Fy is empty ) ;
suppose Fy is empty ; ::_thesis: q in |:Fx:| . i
then reconsider Fy9 = Fy as empty SubsetFamily of the Sorts of D ;
|:Fy9:| . i is empty ;
hence q in |:Fx:| . i by A13; ::_thesis: verum
end;
suppose not Fy is empty ; ::_thesis: q in |:Fx:| . i
then |:Fy:| . i = { (e . i) where e is Element of Bool the Sorts of D : e in Fy } by A12, Th14;
then consider w being Element of Bool the Sorts of D such that
A14: q = w . i and
A15: w in Fy by A13;
A16: ex r being Element of Bool the Sorts of D st
( r = w & y c=' r & r in the Family of D ) by A9, A15;
then x c=' w by A7, PBOOLE:13;
then A17: w in Fx by A11, A16;
then |:Fx:| . i = { (e . i) where e is Element of Bool the Sorts of D : e in Fx } by A12, Th14;
hence q in |:Fx:| . i by A14, A17; ::_thesis: verum
end;
end;
end;
end;
then meet |:Fx:| c=' meet |:Fy:| by MSSUBFAM:46;
then meet |:Fx:| c=' f . y by A1, A8;
hence f . x c=' f . y by A1, A10; ::_thesis: verum
end;
f is idempotent
proof
let x be Element of Bool the Sorts of D; :: according to CLOSURE2:def_12 ::_thesis: f . x = f . (f . x)
consider F being SubsetFamily of the Sorts of D such that
A18: Cl x = meet |:F:| and
A19: F = { X where X is Element of Bool the Sorts of D : ( x c=' X & X in the Family of D ) } by Def22;
F c= the Family of D
proof
let k be set ; :: according to TARSKI:def_3 ::_thesis: ( not k in F or k in the Family of D )
assume k in F ; ::_thesis: k in the Family of D
then ex q being Element of Bool the Sorts of D st
( k = q & x c=' q & q in the Family of D ) by A19;
hence k in the Family of D ; ::_thesis: verum
end;
then A20: meet |:F:| in the Family of D by Def7;
thus f . x = meet |:F:| by A1, A18
.= f . (meet |:F:|) by A1, A20, Th38
.= f . (f . x) by A1, A18 ; ::_thesis: verum
end;
hence ( f is reflexive & f is monotonic & f is idempotent ) by A2, A6; ::_thesis: verum
end;
definition
let S be 1-sorted ;
let D be ClosureSystem of S;
func ClSys->ClOp D -> ClosureOperator of the Sorts of D means :Def23: :: CLOSURE2:def 23
for x being Element of Bool the Sorts of D holds it . x = Cl x;
existence
ex b1 being ClosureOperator of the Sorts of D st
for x being Element of Bool the Sorts of D holds b1 . x = Cl x
proof
set M = the Sorts of D;
deffunc H1( Element of Bool the Sorts of D) -> Element of Bool the Sorts of D = Cl $1;
consider f being Function of (Bool the Sorts of D),(Bool the Sorts of D) such that
A1: for x being Element of Bool the Sorts of D holds f . x = H1(x) from FUNCT_2:sch_4();
reconsider f = f as SetOp of the Sorts of D ;
reconsider f = f as ClosureOperator of the Sorts of D by A1, Th40;
take f ; ::_thesis: for x being Element of Bool the Sorts of D holds f . x = Cl x
thus for x being Element of Bool the Sorts of D holds f . x = Cl x by A1; ::_thesis: verum
end;
uniqueness
for b1, b2 being ClosureOperator of the Sorts of D st ( for x being Element of Bool the Sorts of D holds b1 . x = Cl x ) & ( for x being Element of Bool the Sorts of D holds b2 . x = Cl x ) holds
b1 = b2
proof
let f, g be ClosureOperator of the Sorts of D; ::_thesis: ( ( for x being Element of Bool the Sorts of D holds f . x = Cl x ) & ( for x being Element of Bool the Sorts of D holds g . x = Cl x ) implies f = g )
assume that
A2: for x being Element of Bool the Sorts of D holds f . x = Cl x and
A3: for x being Element of Bool the Sorts of D holds g . x = Cl x ; ::_thesis: f = g
now__::_thesis:_(_Bool_the_Sorts_of_D_=_dom_f_&_Bool_the_Sorts_of_D_=_dom_g_&_(_for_x_being_set_st_x_in_Bool_the_Sorts_of_D_holds_
f_._x_=_g_._x_)_)
set X = Bool the Sorts of D;
thus Bool the Sorts of D = dom f by FUNCT_2:def_1; ::_thesis: ( Bool the Sorts of D = dom g & ( for x being set st x in Bool the Sorts of D holds
f . x = g . x ) )
thus Bool the Sorts of D = dom g by FUNCT_2:def_1; ::_thesis: for x being set st x in Bool the Sorts of D holds
f . x = g . x
let x be set ; ::_thesis: ( x in Bool the Sorts of D implies f . x = g . x )
assume x in Bool the Sorts of D ; ::_thesis: f . x = g . x
then reconsider x1 = x as Element of Bool the Sorts of D ;
thus f . x = Cl x1 by A2
.= g . x by A3 ; ::_thesis: verum
end;
hence f = g by FUNCT_1:2; ::_thesis: verum
end;
end;
:: deftheorem Def23 defines ClSys->ClOp CLOSURE2:def_23_:_
for S being 1-sorted
for D being ClosureSystem of S
for b3 being ClosureOperator of the Sorts of D holds
( b3 = ClSys->ClOp D iff for x being Element of Bool the Sorts of D holds b3 . x = Cl x );
theorem :: CLOSURE2:41
for S being 1-sorted
for A being ManySortedSet of the carrier of S
for f being ClosureOperator of A holds ClSys->ClOp (ClOp->ClSys f) = f
proof
let S be 1-sorted ; ::_thesis: for A being ManySortedSet of the carrier of S
for f being ClosureOperator of A holds ClSys->ClOp (ClOp->ClSys f) = f
let A be ManySortedSet of the carrier of S; ::_thesis: for f being ClosureOperator of A holds ClSys->ClOp (ClOp->ClSys f) = f
let f be ClosureOperator of A; ::_thesis: ClSys->ClOp (ClOp->ClSys f) = f
set D = ClOp->ClSys f;
set M = the Sorts of (ClOp->ClSys f);
set f1 = ClSys->ClOp (ClOp->ClSys f);
A1: A = the Sorts of (ClOp->ClSys f) by Def21;
then reconsider ff = f as reflexive monotonic idempotent SetOp of the Sorts of (ClOp->ClSys f) ;
for x being set st x in Bool A holds
(ClSys->ClOp (ClOp->ClSys f)) . x = ff . x
proof
let x be set ; ::_thesis: ( x in Bool A implies (ClSys->ClOp (ClOp->ClSys f)) . x = ff . x )
assume x in Bool A ; ::_thesis: (ClSys->ClOp (ClOp->ClSys f)) . x = ff . x
then reconsider x1 = x as Element of Bool the Sorts of (ClOp->ClSys f) by Def21;
consider F being SubsetFamily of the Sorts of (ClOp->ClSys f) such that
A2: Cl x1 = meet |:F:| and
A3: F = { X where X is Element of Bool the Sorts of (ClOp->ClSys f) : ( x1 c=' X & X in the Family of (ClOp->ClSys f) ) } by Def22;
A4: now__::_thesis:_for_i_being_set_st_i_in_the_carrier_of_S_holds_
(meet_|:F:|)_._i_=_(ff_._x1)_._i
A5: x1 c=' ff . x1 by Def10;
( x1 c=' the Sorts of (ClOp->ClSys f) & the Sorts of (ClOp->ClSys f) in the Family of (ClOp->ClSys f) ) by Def8, PBOOLE:def_18;
then the Sorts of (ClOp->ClSys f) in F by A3;
then reconsider F9 = F as non empty SubsetFamily of the Sorts of (ClOp->ClSys f) ;
let i be set ; ::_thesis: ( i in the carrier of S implies (meet |:F:|) . i = (ff . x1) . i )
assume A6: i in the carrier of S ; ::_thesis: (meet |:F:|) . i = (ff . x1) . i
then consider Q being Subset-Family of ( the Sorts of (ClOp->ClSys f) . i) such that
A7: Q = |:F:| . i and
A8: (meet |:F:|) . i = Intersect Q by MSSUBFAM:def_1;
A9: Q = { (q . i) where q is Element of Bool the Sorts of (ClOp->ClSys f) : q in F9 } by A6, A7, Th14;
A10: the Family of (ClOp->ClSys f) = { q where q is Element of Bool the Sorts of (ClOp->ClSys f) : ff . q = q } by A1, Def21;
A11: now__::_thesis:_for_z_being_set_st_z_in_Q_holds_
(ff_._x1)_._i_c=_z
let z be set ; ::_thesis: ( z in Q implies (ff . x1) . i c= z )
assume z in Q ; ::_thesis: (ff . x1) . i c= z
then consider q being Element of Bool the Sorts of (ClOp->ClSys f) such that
A12: z = q . i and
A13: q in F9 by A9;
consider X being Element of Bool the Sorts of (ClOp->ClSys f) such that
A14: q = X and
A15: ( x1 c=' X & X in the Family of (ClOp->ClSys f) ) by A3, A13;
( ex t being Element of Bool the Sorts of (ClOp->ClSys f) st
( X = t & ff . t = t ) & ff . x1 c=' ff . X ) by A10, A15, Def11;
hence (ff . x1) . i c= z by A6, A12, A14, PBOOLE:def_2; ::_thesis: verum
end;
ff . (ff . x1) = ff . x1 by Def12;
then ff . x1 in the Family of (ClOp->ClSys f) by A10;
then ff . x1 in F9 by A3, A5;
then (ff . x1) . i in Q by A9;
then A16: (meet |:F:|) . i c= (ff . x1) . i by A8, MSSUBFAM:2;
Q = |:F9:| . i by A7;
then (ff . x1) . i c= (meet |:F:|) . i by A6, A8, A11, MSSUBFAM:5;
hence (meet |:F:|) . i = (ff . x1) . i by A16, XBOOLE_0:def_10; ::_thesis: verum
end;
thus (ClSys->ClOp (ClOp->ClSys f)) . x = Cl x1 by Def23
.= ff . x by A2, A4, PBOOLE:3 ; ::_thesis: verum
end;
hence ClSys->ClOp (ClOp->ClSys f) = f by A1, FUNCT_2:12; ::_thesis: verum
end;
deffunc H1( set ) -> set = $1;
theorem :: CLOSURE2:42
for S being 1-sorted
for D being ClosureSystem of S holds ClOp->ClSys (ClSys->ClOp D) = ClosureStr(# the Sorts of D, the Family of D #)
proof
let S be 1-sorted ; ::_thesis: for D being ClosureSystem of S holds ClOp->ClSys (ClSys->ClOp D) = ClosureStr(# the Sorts of D, the Family of D #)
let D be ClosureSystem of S; ::_thesis: ClOp->ClSys (ClSys->ClOp D) = ClosureStr(# the Sorts of D, the Family of D #)
set M = the Sorts of D;
set F = the Family of D;
set d = the Family of (ClOp->ClSys (ClSys->ClOp D));
set f = ClSys->ClOp D;
A1: the Family of (ClOp->ClSys (ClSys->ClOp D)) = { x where x is Element of Bool the Sorts of D : (ClSys->ClOp D) . x = x } by Def21;
the Family of D = the Family of (ClOp->ClSys (ClSys->ClOp D))
proof
thus the Family of D c= the Family of (ClOp->ClSys (ClSys->ClOp D)) :: according to XBOOLE_0:def_10 ::_thesis: the Family of (ClOp->ClSys (ClSys->ClOp D)) c= the Family of D
proof
let q be set ; :: according to TARSKI:def_3 ::_thesis: ( not q in the Family of D or q in the Family of (ClOp->ClSys (ClSys->ClOp D)) )
assume A2: q in the Family of D ; ::_thesis: q in the Family of (ClOp->ClSys (ClSys->ClOp D))
then reconsider q1 = q as Element of Bool the Sorts of D ;
consider SF being SubsetFamily of the Sorts of D such that
A3: Cl q1 = meet |:SF:| and
A4: SF = { X where X is Element of Bool the Sorts of D : ( q1 c= X & X in the Family of D ) } by Def22;
( q1 c=' the Sorts of D & the Sorts of D in the Family of D ) by Def8, PBOOLE:def_18;
then the Sorts of D in SF by A4;
then reconsider SF9 = SF as non empty SubsetFamily of the Sorts of D ;
now__::_thesis:_for_i_being_set_st_i_in_the_carrier_of_S_holds_
((ClSys->ClOp_D)_._q1)_._i_=_q1_._i
let i be set ; ::_thesis: ( i in the carrier of S implies ((ClSys->ClOp D) . q1) . i = q1 . i )
assume A5: i in the carrier of S ; ::_thesis: ((ClSys->ClOp D) . q1) . i = q1 . i
then consider Q being Subset-Family of ( the Sorts of D . i) such that
A6: Q = |:SF9:| . i and
A7: (meet |:SF9:|) . i = Intersect Q by MSSUBFAM:def_1;
A8: Q = { (x . i) where x is Element of Bool the Sorts of D : x in SF9 } by A5, A6, Th14;
q1 in SF9 by A2, A4;
then A9: q1 . i in Q by A8;
then A10: Intersect Q c= q1 . i by MSSUBFAM:2;
now__::_thesis:_for_z_being_set_st_z_in_Q_holds_
q1_._i_c=_z
let z be set ; ::_thesis: ( z in Q implies q1 . i c= z )
assume z in Q ; ::_thesis: q1 . i c= z
then consider x being Element of Bool the Sorts of D such that
A11: z = x . i and
A12: x in SF9 by A8;
ex xx being Element of Bool the Sorts of D st
( xx = x & q1 c=' xx & xx in the Family of D ) by A4, A12;
hence q1 . i c= z by A5, A11, PBOOLE:def_2; ::_thesis: verum
end;
then q1 . i c= Intersect Q by A9, MSSUBFAM:5;
then Intersect Q = q1 . i by A10, XBOOLE_0:def_10;
hence ((ClSys->ClOp D) . q1) . i = q1 . i by A3, A7, Def23; ::_thesis: verum
end;
then (ClSys->ClOp D) . q1 = q1 by PBOOLE:3;
hence q in the Family of (ClOp->ClSys (ClSys->ClOp D)) by A1; ::_thesis: verum
end;
let q be set ; :: according to TARSKI:def_3 ::_thesis: ( not q in the Family of (ClOp->ClSys (ClSys->ClOp D)) or q in the Family of D )
assume q in the Family of (ClOp->ClSys (ClSys->ClOp D)) ; ::_thesis: q in the Family of D
then consider x being Element of Bool the Sorts of D such that
A13: ( q = x & (ClSys->ClOp D) . x = x ) by A1;
defpred S1[ Element of Bool the Sorts of D] means ( $1 in the Family of D & x c=' $1 );
defpred S2[ Element of Bool the Sorts of D] means ( x c=' $1 & $1 in the Family of D );
defpred S3[ Element of Bool the Sorts of D] means x c=' $1;
A14: { H1(w) where w is Element of Bool the Sorts of D : ( H1(w) in the Family of D & S3[w] ) } c= the Family of D from FRAENKEL:sch_17();
A15: for a being Element of Bool the Sorts of D holds
( S2[a] iff S1[a] ) ;
A16: { H1(a) where a is Element of Bool the Sorts of D : S2[a] } = { H1(b) where b is Element of Bool the Sorts of D : S1[b] } from FRAENKEL:sch_3(A15);
consider SF being SubsetFamily of the Sorts of D such that
A17: Cl x = meet |:SF:| and
A18: SF = { X where X is Element of Bool the Sorts of D : ( x c=' X & X in the Family of D ) } by Def22;
meet |:SF:| = q by A13, A17, Def23;
hence q in the Family of D by A18, A14, A16, Def7; ::_thesis: verum
end;
hence ClOp->ClSys (ClSys->ClOp D) = ClosureStr(# the Sorts of D, the Family of D #) by Def21; ::_thesis: verum
end;