:: Certain Facts about Families of Subsets of Many Sorted Sets
:: by Artur Korni{\l}owicz
::
:: Received October 27, 1995
:: Copyright (c) 1995-2012 Association of Mizar Users


begin

registration
let I be set ;
let F be ManySortedFunction of I;
cluster doms F -> I -defined ;
coherence
 doms F is I -defined
proofend;
cluster rngs F -> I -defined ;
coherence
 rngs F is I -defined
proofend;
end;

registration
let I be set ;
let F be ManySortedFunction of I;
cluster doms F -> I -defined total for I -defined Function;
coherence
 for b1 being I -defined Function st b1 = doms F holds
b1 is total
proofend;
cluster rngs F -> I -defined total for I -defined Function;
coherence
 for b1 being I -defined Function st b1 = rngs F holds
b1 is total
proofend;
end;

scheme :: MSSUBFAM:sch 1
MSFExFunc{ F1() ->  set , F2() ->  ManySortedSet of F1(), F3() ->  ManySortedSet of F1(), P1[ set , set , set ] } :
 ex F being ManySortedFunction of F2(),F3() st
for i being set st i in F1() holds
ex f being Function of (F2() . i),(F3() . i) st
( f = F . i & ( for x being set st x in F2() . i holds
P1[f . x,x,i] ) )
provided
A1: for i being set st i in F1() holds
for x being set st x in F2() . i holds
ex y being set st
( y in F3() . i & P1[y,x,i] )
proofend;

theorem :: MSSUBFAM:1
for I being set
for sf being Subset-Family of I st sf <> {} holds
Intersect sf c= union sf
proofend;

theorem :: MSSUBFAM:2
for I, G being set
for sf being Subset-Family of I st G in sf holds
Intersect sf c= G
proofend;

theorem :: MSSUBFAM:3
for I being set
for sf being Subset-Family of I st {} in sf holds
Intersect sf = {}
proofend;

theorem :: MSSUBFAM:4
for I being set
for sf being Subset-Family of I
for Z being Subset of I st ( for Z1 being set st Z1 in sf holds
Z c= Z1 ) holds
Z c= Intersect sf
proofend;

theorem :: MSSUBFAM:5
for I, G being set
for sf being Subset-Family of I st sf <> {} &amp; ( for Z1 being set st Z1 in sf holds
G c= Z1 ) holds
G c= Intersect sf
proofend;

theorem :: MSSUBFAM:6
for I, G, H being set
for sf being Subset-Family of I st G in sf &amp; G c= H holds
Intersect sf c= H
proofend;

theorem :: MSSUBFAM:7
for I, G, H being set
for sf being Subset-Family of I st G in sf &amp; G misses H holds
Intersect sf misses H
proofend;

theorem :: MSSUBFAM:8
for I being set
for sh, sf, sg being Subset-Family of I st sh = sf \/ sg holds
Intersect sh = (Intersect sf) /\ (Intersect sg)
proofend;

theorem :: MSSUBFAM:9
for I being set
for sf being Subset-Family of I
for v being Subset of I st sf = {v} holds
Intersect sf = v
proofend;

theorem :: MSSUBFAM:10
for I being set
for sf being Subset-Family of I
for v, w being Subset of I st sf = {v,w} holds
Intersect sf = v /\ w
proofend;

theorem :: MSSUBFAM:11
for I being set
for A, B being ManySortedSet of I st A in B holds
A is Element of B
proofend;

theorem :: MSSUBFAM:12
for I being set
for A being ManySortedSet of I
for B being V8() ManySortedSet of I st A is Element of B holds
A in B
proofend;

theorem Th13: :: MSSUBFAM:13
for i, I being set
for F being ManySortedFunction of I
for f being Function st i in I &amp; f = F . i holds
(rngs F) . i = rng f
proofend;

theorem Th14: :: MSSUBFAM:14
for i, I being set
for F being ManySortedFunction of I
for f being Function st i in I &amp; f = F . i holds
(doms F) . i = dom f
proofend;

theorem :: MSSUBFAM:15
for I being set
for F, G being ManySortedFunction of I holds G ** F is ManySortedFunction of I
proofend;

theorem :: MSSUBFAM:16
for I being set
for A being V8() ManySortedSet of I
for F being ManySortedFunction of A, [[0]] I holds F = [[0]] I
proofend;

theorem :: MSSUBFAM:17
for I being set
for A, B being ManySortedSet of I
for F being ManySortedFunction of I st A is_transformable_to B &amp; F is ManySortedFunction of A,B holds
( doms F = A &amp; rngs F c= B )
proofend;

begin

registration
let I be set ;
cluster Relation-like V9() I -defined Function-like total  -> V36() for set ;
coherence
 for b1 being ManySortedSet of I st b1 is V9() holds
b1 is V36()
proofend;
end;

registration
let I be set ;
cluster [[0]] I -> V9() V36() ;
coherence
 ( [[0]] I is empty-yielding &amp; [[0]] I is finite-yielding ) ;
end;

registration
let I be set ;
let A be ManySortedSet of I;
cluster Relation-like V9() I -defined Function-like total V36() for ManySortedSubset of A;
existence
 ex b1 being ManySortedSubset of A st
( b1 is V9() &amp; b1 is V36() )
proofend;
end;

theorem Th18: :: MSSUBFAM:18
for I being set
for A, B being ManySortedSet of I st A c= B &amp; B is V36() holds
A is V36()
proofend;

registration
let I be set ;
let A be V36() ManySortedSet of I;
cluster  -> V36() for ManySortedSubset of A;
coherence
 for b1 being ManySortedSubset of A holds b1 is V36()
proofend;
end;

registration
let I be set ;
let A, B be V36() ManySortedSet of I;
clusterA \/ B -> V36() ;
coherence
 A \/ B is finite-yielding
proofend;
end;

registration
let I be set ;
let A be ManySortedSet of I;
let B be V36() ManySortedSet of I;
clusterA /\ B -> V36() ;
coherence
 A /\ B is finite-yielding
proofend;
end;

registration
let I be set ;
let B be ManySortedSet of I;
let A be V36() ManySortedSet of I;
clusterA /\ B -> V36() ;
coherence
 A /\ B is finite-yielding ;
end;

registration
let I be set ;
let B be ManySortedSet of I;
let A be V36() ManySortedSet of I;
clusterA \ B -> V36() ;
coherence
 A \ B is finite-yielding
proofend;
end;

registration
let I be set ;
let F be ManySortedFunction of I;
let A be V36() ManySortedSet of I;
clusterF .:.: A -> V36() ;
coherence
 F .:.: A is finite-yielding
proofend;
end;

registration
let I be set ;
let A, B be V36() ManySortedSet of I;
cluster[|A,B|] -> V36() ;
coherence
 [|A,B|] is finite-yielding
proofend;
end;

theorem :: MSSUBFAM:19
for I being set
for B, A being ManySortedSet of I st B is V8() &amp; [|A,B|] is V36() holds
A is V36()
proofend;

theorem :: MSSUBFAM:20
for I being set
for A, B being ManySortedSet of I st A is V8() &amp; [|A,B|] is V36() holds
B is V36()
proofend;

theorem Th21: :: MSSUBFAM:21
for I being set
for A being ManySortedSet of I holds
( A is V36() iff bool A is V36() )
proofend;

registration
let I be set ;
let M be V36() ManySortedSet of I;
cluster bool M -> V36() ;
coherence
 bool M is finite-yielding by Th21;
end;

theorem :: MSSUBFAM:22
for I being set
for A being V8() ManySortedSet of I st A is V36() &amp; ( for M being ManySortedSet of I st M in A holds
M is V36() ) holds
union A is V36()
proofend;

theorem :: MSSUBFAM:23
for I being set
for A being ManySortedSet of I st union A is V36() holds
( A is V36() &amp; ( for M being ManySortedSet of I st M in A holds
M is V36() ) )
proofend;

theorem :: MSSUBFAM:24
for I being set
for F being ManySortedFunction of I st doms F is V36() holds
rngs F is V36()
proofend;

theorem :: MSSUBFAM:25
for I being set
for A being ManySortedSet of I
for F being ManySortedFunction of I st A c= rngs F &amp; ( for i being set
for f being Function st i in I &amp; f = F . i holds
f " (A . i) is finite ) holds
A is V36()
proofend;

registration
let I be set ;
let A, B be V36() ManySortedSet of I;
cluster (Funcs) (A,B) -> V36() ;
coherence
 (Funcs) (A,B) is finite-yielding
proofend;
end;

registration
let I be set ;
let A, B be V36() ManySortedSet of I;
clusterA \+\ B -> V36() ;
coherence
 A \+\ B is finite-yielding ;
end;

theorem :: MSSUBFAM:26
for I being set
for X, Y, Z being ManySortedSet of I st X is V36() &amp; X c= [|Y,Z|] holds
ex A, B being ManySortedSet of I st
( A is V36() &amp; A c= Y &amp; B is V36() &amp; B c= Z &amp; X c= [|A,B|] )
proofend;

theorem :: MSSUBFAM:27
for I being set
for X, Y, Z being ManySortedSet of I st X is V36() &amp; X c= [|Y,Z|] holds
ex A being ManySortedSet of I st
( A is V36() &amp; A c= Y &amp; X c= [|A,Z|] )
proofend;

theorem :: MSSUBFAM:28
for I being set
for M being V8() V36() ManySortedSet of I st ( for A, B being ManySortedSet of I st A in M &amp; B in M &amp; not A c= B holds
B c= A ) holds
ex m being ManySortedSet of I st
( m in M &amp; ( for K being ManySortedSet of I st K in M holds
m c= K ) )
proofend;

theorem :: MSSUBFAM:29
for I being set
for M being V8() V36() ManySortedSet of I st ( for A, B being ManySortedSet of I st A in M &amp; B in M &amp; not A c= B holds
B c= A ) holds
ex m being ManySortedSet of I st
( m in M &amp; ( for K being ManySortedSet of I st K in M holds
K c= m ) )
proofend;

theorem :: MSSUBFAM:30
for I being set
for F being ManySortedFunction of I
for Z being ManySortedSet of I st Z is V36() &amp; Z c= rngs F holds
ex Y being ManySortedSet of I st
( Y c= doms F &amp; Y is V36() &amp; F .:.: Y = Z )
proofend;

begin

definition
let I be set ;
let M be ManySortedSet of I;
mode MSSubsetFamily of M is ManySortedSubset of bool M;
end;

registration
let I be set ;
let M be ManySortedSet of I;
cluster Relation-like V8() I -defined Function-like total for ManySortedSubset of bool M;
existence
 not for b1 being MSSubsetFamily of M holds b1 is V8()
proofend;
end;

definition
let I be set ;
let M be ManySortedSet of I;
:: original:bool
redefine func bool M ->  MSSubsetFamily of M;
coherence
 bool M is MSSubsetFamily of M by PBOOLE:def_18;
end;

registration
let I be set ;
let M be ManySortedSet of I;
cluster Relation-like V9() I -defined Function-like total V36() for ManySortedSubset of bool M;
existence
 ex b1 being MSSubsetFamily of M st
( b1 is V9() &amp; b1 is V36() )
proofend;
end;

theorem :: MSSUBFAM:31
for I being set
for M being ManySortedSet of I holds [[0]] I is V9() V36() MSSubsetFamily of M
proofend;

registration
let I be set ;
let M be V36() ManySortedSet of I;
cluster Relation-like V8() I -defined Function-like total V36() for ManySortedSubset of bool M;
existence
 ex b1 being MSSubsetFamily of M st
( b1 is V8() &amp; b1 is V36() )
proofend;
end;

definition
let I be non empty set ;
let M be ManySortedSet of I;
let SF be MSSubsetFamily of M;
let i be Element of I;
:: original:.
redefine funcSF . i ->  Subset-Family of (M . i);
coherence
 SF . i is Subset-Family of (M . i)
proofend;
end;

theorem Th32: :: MSSUBFAM:32
for i, I being set
for M being ManySortedSet of I
for SF being MSSubsetFamily of M st i in I holds
SF . i is Subset-Family of (M . i)
proofend;

theorem Th33: :: MSSUBFAM:33
for I being set
for A, M being ManySortedSet of I
for SF being MSSubsetFamily of M st A in SF holds
A is ManySortedSubset of M
proofend;

theorem Th34: :: MSSUBFAM:34
for I being set
for M being ManySortedSet of I
for SF, SG being MSSubsetFamily of M holds SF \/ SG is MSSubsetFamily of M
proofend;

theorem :: MSSUBFAM:35
for I being set
for M being ManySortedSet of I
for SF, SG being MSSubsetFamily of M holds SF /\ SG is MSSubsetFamily of M
proofend;

theorem Th36: :: MSSUBFAM:36
for I being set
for A, M being ManySortedSet of I
for SF being MSSubsetFamily of M holds SF \ A is MSSubsetFamily of M
proofend;

theorem :: MSSUBFAM:37
for I being set
for M being ManySortedSet of I
for SF, SG being MSSubsetFamily of M holds SF \+\ SG is MSSubsetFamily of M
proofend;

theorem Th38: :: MSSUBFAM:38
for I being set
for A, M being ManySortedSet of I st A c= M holds
{A} is MSSubsetFamily of M
proofend;

theorem Th39: :: MSSUBFAM:39
for I being set
for A, M, B being ManySortedSet of I st A c= M &amp; B c= M holds
{A,B} is MSSubsetFamily of M
proofend;

theorem Th40: :: MSSUBFAM:40
for I being set
for M being ManySortedSet of I
for SF being MSSubsetFamily of M holds union SF c= M
proofend;

begin

definition
let I be set ;
let M be ManySortedSet of I;
let SF be MSSubsetFamily of M;
func meet SF ->  ManySortedSet of I means :Def1: :: MSSUBFAM:def 1
 for i being set st i in I holds
ex Q being Subset-Family of (M . i) st
( Q = SF . i &amp; it . i = Intersect Q );
existence
 ex b1 being ManySortedSet of I st
for i being set st i in I holds
ex Q being Subset-Family of (M . i) st
( Q = SF . i &amp; b1 . i = Intersect Q )
proofend;
uniqueness
 for b1, b2 being ManySortedSet of I st ( for i being set st i in I holds
ex Q being Subset-Family of (M . i) st
( Q = SF . i &amp; b1 . i = Intersect Q ) ) &amp; ( for i being set st i in I holds
ex Q being Subset-Family of (M . i) st
( Q = SF . i &amp; b2 . i = Intersect Q ) ) holds
b1 = b2
proofend;
end;

:: deftheorem Def1 defines meet MSSUBFAM:def_1_:_
 for I being set
for M being ManySortedSet of I
for SF being MSSubsetFamily of M
for b4 being ManySortedSet of I holds
( b4 = meet SF iff for i being set st i in I holds
ex Q being Subset-Family of (M . i) st
( Q = SF . i &amp; b4 . i = Intersect Q ) );

definition
let I be set ;
let M be ManySortedSet of I;
let SF be MSSubsetFamily of M;
:: original:meet
redefine func meet SF ->  ManySortedSubset of M;
coherence
 meet SF is ManySortedSubset of M
proofend;
end;

theorem Th41: :: MSSUBFAM:41
for I being set
for M being ManySortedSet of I
for SF being MSSubsetFamily of M st SF = [[0]] I holds
meet SF = M
proofend;

theorem :: MSSUBFAM:42
for I being set
for M being ManySortedSet of I
for SFe being V8() MSSubsetFamily of M holds meet SFe c= union SFe
proofend;

theorem :: MSSUBFAM:43
for I being set
for M, A being ManySortedSet of I
for SF being MSSubsetFamily of M st A in SF holds
meet SF c= A
proofend;

theorem :: MSSUBFAM:44
for I being set
for M being ManySortedSet of I
for SF being MSSubsetFamily of M st [[0]] I in SF holds
meet SF = [[0]] I
proofend;

theorem :: MSSUBFAM:45
for I being set
for Z, M being ManySortedSet of I
for SF being V8() MSSubsetFamily of M st ( for Z1 being ManySortedSet of I st Z1 in SF holds
Z c= Z1 ) holds
Z c= meet SF
proofend;

theorem :: MSSUBFAM:46
for I being set
for M being ManySortedSet of I
for SF, SG being MSSubsetFamily of M st SF c= SG holds
meet SG c= meet SF
proofend;

theorem :: MSSUBFAM:47
for I being set
for M, A, B being ManySortedSet of I
for SF being MSSubsetFamily of M st A in SF &amp; A c= B holds
meet SF c= B
proofend;

theorem :: MSSUBFAM:48
for I being set
for M, A, B being ManySortedSet of I
for SF being MSSubsetFamily of M st A in SF &amp; A /\ B = [[0]] I holds
(meet SF) /\ B = [[0]] I
proofend;

theorem :: MSSUBFAM:49
for I being set
for M being ManySortedSet of I
for SH, SF, SG being MSSubsetFamily of M st SH = SF \/ SG holds
meet SH = (meet SF) /\ (meet SG)
proofend;

theorem :: MSSUBFAM:50
for I being set
for M being ManySortedSet of I
for SF being MSSubsetFamily of M
for V being ManySortedSubset of M st SF = {V} holds
meet SF = V
proofend;

theorem Th51: :: MSSUBFAM:51
for I being set
for M being ManySortedSet of I
for SF being MSSubsetFamily of M
for V, W being ManySortedSubset of M st SF = {V,W} holds
meet SF = V /\ W
proofend;

theorem :: MSSUBFAM:52
for I being set
for M, A being ManySortedSet of I
for SF being MSSubsetFamily of M st A in meet SF holds
for B being ManySortedSet of I st B in SF holds
A in B
proofend;

theorem :: MSSUBFAM:53
for I being set
for A, M being ManySortedSet of I
for SF being V8() MSSubsetFamily of M st A in M &amp; ( for B being ManySortedSet of I st B in SF holds
A in B ) holds
A in meet SF
proofend;

definition
let I be set ;
let M be ManySortedSet of I;
let IT be MSSubsetFamily of M;
attrIT is additive  means :: MSSUBFAM:def 2
 for A, B being ManySortedSet of I st A in IT &amp; B in IT holds
A \/ B in IT;
attrIT is absolutely-additive  means :Def3: :: MSSUBFAM:def 3
 for F being MSSubsetFamily of M st F c= IT holds
union F in IT;
attrIT is multiplicative  means :: MSSUBFAM:def 4
 for A, B being ManySortedSet of I st A in IT &amp; B in IT holds
A /\ B in IT;
attrIT is absolutely-multiplicative  means :Def5: :: MSSUBFAM:def 5
 for F being MSSubsetFamily of M st F c= IT holds
meet F in IT;
attrIT is properly-upper-bound  means :Def6: :: MSSUBFAM:def 6
M in IT;
attrIT is properly-lower-bound  means :Def7: :: MSSUBFAM:def 7
 [[0]] I in IT;
end;

:: deftheorem  defines additive MSSUBFAM:def_2_:_
 for I being set
for M being ManySortedSet of I
for IT being MSSubsetFamily of M holds
( IT is additive iff for A, B being ManySortedSet of I st A in IT &amp; B in IT holds
A \/ B in IT );

:: deftheorem Def3 defines absolutely-additive MSSUBFAM:def_3_:_
 for I being set
for M being ManySortedSet of I
for IT being MSSubsetFamily of M holds
( IT is absolutely-additive iff for F being MSSubsetFamily of M st F c= IT holds
union F in IT );

:: deftheorem  defines multiplicative MSSUBFAM:def_4_:_
 for I being set
for M being ManySortedSet of I
for IT being MSSubsetFamily of M holds
( IT is multiplicative iff for A, B being ManySortedSet of I st A in IT &amp; B in IT holds
A /\ B in IT );

:: deftheorem Def5 defines absolutely-multiplicative MSSUBFAM:def_5_:_
 for I being set
for M being ManySortedSet of I
for IT being MSSubsetFamily of M holds
( IT is absolutely-multiplicative iff for F being MSSubsetFamily of M st F c= IT holds
meet F in IT );

:: deftheorem Def6 defines properly-upper-bound MSSUBFAM:def_6_:_
 for I being set
for M being ManySortedSet of I
for IT being MSSubsetFamily of M holds
( IT is properly-upper-bound iff M in IT );

:: deftheorem Def7 defines properly-lower-bound MSSUBFAM:def_7_:_
 for I being set
for M being ManySortedSet of I
for IT being MSSubsetFamily 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 &amp; bool M is absolutely-additive &amp; bool M is multiplicative &amp; bool M is absolutely-multiplicative &amp; bool M is properly-upper-bound &amp; bool M is properly-lower-bound )
proofend;

registration
let I be set ;
let M be ManySortedSet of I;
cluster Relation-like V8() I -defined Function-like total additive absolutely-additive multiplicative absolutely-multiplicative properly-upper-bound properly-lower-bound for ManySortedSubset of bool M;
existence
 ex b1 being MSSubsetFamily of M st
( b1 is V8() &amp; b1 is additive &amp; b1 is absolutely-additive &amp; b1 is multiplicative &amp; b1 is absolutely-multiplicative &amp; b1 is properly-upper-bound &amp; b1 is properly-lower-bound )
proofend;
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 MSSubsetFamily of M;
coherence
 bool M is additive absolutely-additive multiplicative absolutely-multiplicative properly-upper-bound properly-lower-bound MSSubsetFamily of M by Lm1;
end;

registration
let I be set ;
let M be ManySortedSet of I;
cluster absolutely-additive  ->  additive for ManySortedSubset of bool M;
coherence
 for b1 being MSSubsetFamily of M st b1 is absolutely-additive holds
b1 is additive
proofend;
end;

registration
let I be set ;
let M be ManySortedSet of I;
cluster absolutely-multiplicative  ->  multiplicative for ManySortedSubset of bool M;
coherence
 for b1 being MSSubsetFamily of M st b1 is absolutely-multiplicative holds
b1 is multiplicative
proofend;
end;

registration
let I be set ;
let M be ManySortedSet of I;
cluster absolutely-multiplicative  ->  properly-upper-bound for ManySortedSubset of bool M;
coherence
 for b1 being MSSubsetFamily of M st b1 is absolutely-multiplicative holds
b1 is properly-upper-bound
proofend;
end;

registration
let I be set ;
let M be ManySortedSet of I;
cluster properly-upper-bound  -> V8() for ManySortedSubset of bool M;
coherence
 for b1 being MSSubsetFamily of M st b1 is properly-upper-bound holds
b1 is V8()
proofend;
end;

registration
let I be set ;
let M be ManySortedSet of I;
cluster absolutely-additive  ->  properly-lower-bound for ManySortedSubset of bool M;
coherence
 for b1 being MSSubsetFamily of M st b1 is absolutely-additive holds
b1 is properly-lower-bound
proofend;
end;

registration
let I be set ;
let M be ManySortedSet of I;
cluster properly-lower-bound  -> V8() for ManySortedSubset of bool M;
coherence
 for b1 being MSSubsetFamily of M st b1 is properly-lower-bound holds
b1 is V8()
proofend;
end;