:: Families of Sets
:: by Beata Padlewska
::
:: Received April 5, 1989
:: Copyright (c) 1990-2012 Association of Mizar Users


begin

definition
let X be set ;
func meet X ->  set  means :Def1: :: SETFAM_1:def 1
 for x being set holds
( x in it iff for Y being set st Y in X holds
x in Y ) if X <> {}
otherwise it = {} ;
existence
 ( ( X <> {} implies ex b1 being set st
for x being set holds
( x in b1 iff for Y being set st Y in X holds
x in Y ) ) &amp; ( not X <> {} implies ex b1 being set st b1 = {} ) )
proofend;
uniqueness
 for b1, b2 being set holds
( ( X <> {} &amp; ( for x being set holds
( x in b1 iff for Y being set st Y in X holds
x in Y ) ) &amp; ( for x being set holds
( x in b2 iff for Y being set st Y in X holds
x in Y ) ) implies b1 = b2 ) &amp; ( not X <> {} &amp; b1 = {} &amp; b2 = {} implies b1 = b2 ) )
proofend;
consistency
 for b1 being set holds verum ;
end;

:: deftheorem Def1 defines meet SETFAM_1:def_1_:_
 for X being set
for b2 being set holds
( ( X <> {} implies ( b2 = meet X iff for x being set holds
( x in b2 iff for Y being set st Y in X holds
x in Y ) ) ) &amp; ( not X <> {} implies ( b2 = meet X iff b2 = {} ) ) );

:: Intersection of families of sets
theorem :: SETFAM_1:1
meet {} = {} by Def1;

theorem Th2: :: SETFAM_1:2
for X being set holds meet X c= union X
proofend;

theorem Th3: :: SETFAM_1:3
for Z, X being set st Z in X holds
meet X c= Z
proofend;

theorem :: SETFAM_1:4
for X being set st {} in X holds
meet X = {} by Th3, XBOOLE_1:3;

theorem :: SETFAM_1:5
for X, Z being set st X <> {} &amp; ( for Z1 being set st Z1 in X holds
Z c= Z1 ) holds
Z c= meet X
proofend;

theorem Th6: :: SETFAM_1:6
for X, Y being set st X <> {} &amp; X c= Y holds
meet Y c= meet X
proofend;

theorem :: SETFAM_1:7
for X, Y, Z being set st X in Y &amp; X c= Z holds
meet Y c= Z
proofend;

theorem :: SETFAM_1:8
for X, Y, Z being set st X in Y &amp; X misses Z holds
meet Y misses Z by Th3, XBOOLE_1:63;

theorem :: SETFAM_1:9
for X, Y being set st X <> {} &amp; Y <> {} holds
meet (X \/ Y) = (meet X) /\ (meet Y)
proofend;

theorem :: SETFAM_1:10
for x being set holds meet {x} = x
proofend;

theorem :: SETFAM_1:11
for X, Y being set holds meet {X,Y} = X /\ Y
proofend;

definition
let SFX, SFY be set ;
predSFX is_finer_than SFY means :: SETFAM_1:def 2
 for X being set st X in SFX holds
ex Y being set st
( Y in SFY &amp; X c= Y );
reflexivity
 for SFX, X being set st X in SFX holds
ex Y being set st
( Y in SFX &amp; X c= Y ) ;
predSFY is_coarser_than SFX means :: SETFAM_1:def 3
 for Y being set st Y in SFY holds
ex X being set st
( X in SFX &amp; X c= Y );
reflexivity
 for SFY, Y being set st Y in SFY holds
ex X being set st
( X in SFY &amp; X c= Y ) ;
end;

:: deftheorem  defines is_finer_than SETFAM_1:def_2_:_
 for SFX, SFY being set holds
( SFX is_finer_than SFY iff for X being set st X in SFX holds
ex Y being set st
( Y in SFY &amp; X c= Y ) );

:: deftheorem  defines is_coarser_than SETFAM_1:def_3_:_
 for SFX, SFY being set holds
( SFY is_coarser_than SFX iff for Y being set st Y in SFY holds
ex X being set st
( X in SFX &amp; X c= Y ) );

theorem :: SETFAM_1:12
for SFX, SFY being set st SFX c= SFY holds
SFX is_finer_than SFY
proofend;

theorem :: SETFAM_1:13
for SFX, SFY being set st SFX is_finer_than SFY holds
union SFX c= union SFY
proofend;

theorem :: SETFAM_1:14
for SFY, SFX being set st SFY <> {} &amp; SFY is_coarser_than SFX holds
meet SFX c= meet SFY
proofend;

theorem :: SETFAM_1:15
for SFX being set holds {} is_finer_than SFX
proofend;

theorem :: SETFAM_1:16
for SFX being set st SFX is_finer_than {} holds
SFX = {}
proofend;

theorem :: SETFAM_1:17
for SFX, SFY, SFZ being set st SFX is_finer_than SFY &amp; SFY is_finer_than SFZ holds
SFX is_finer_than SFZ
proofend;

theorem :: SETFAM_1:18
for Y, SFX being set st SFX is_finer_than {Y} holds
for X being set st X in SFX holds
X c= Y
proofend;

theorem :: SETFAM_1:19
for X, Y, SFX being set st SFX is_finer_than {X,Y} holds
for Z being set holds
( not Z in SFX or Z c= X or Z c= Y )
proofend;

definition
let SFX, SFY be set ;
func UNION (SFX,SFY) ->  set  means :Def4: :: SETFAM_1:def 4
 for Z being set holds
( Z in it iff ex X, Y being set st
( X in SFX &amp; Y in SFY &amp; Z = X \/ Y ) );
existence
 ex b1 being set st
for Z being set holds
( Z in b1 iff ex X, Y being set st
( X in SFX &amp; Y in SFY &amp; Z = X \/ Y ) )
proofend;
uniqueness
 for b1, b2 being set st ( for Z being set holds
( Z in b1 iff ex X, Y being set st
( X in SFX &amp; Y in SFY &amp; Z = X \/ Y ) ) ) &amp; ( for Z being set holds
( Z in b2 iff ex X, Y being set st
( X in SFX &amp; Y in SFY &amp; Z = X \/ Y ) ) ) holds
b1 = b2
proofend;
commutativity
 for b1 being set
for SFX, SFY being set st ( for Z being set holds
( Z in b1 iff ex X, Y being set st
( X in SFX &amp; Y in SFY &amp; Z = X \/ Y ) ) ) holds
for Z being set holds
( Z in b1 iff ex X, Y being set st
( X in SFY &amp; Y in SFX &amp; Z = X \/ Y ) )
proofend;
func INTERSECTION (SFX,SFY) ->  set  means :Def5: :: SETFAM_1:def 5
 for Z being set holds
( Z in it iff ex X, Y being set st
( X in SFX &amp; Y in SFY &amp; Z = X /\ Y ) );
existence
 ex b1 being set st
for Z being set holds
( Z in b1 iff ex X, Y being set st
( X in SFX &amp; Y in SFY &amp; Z = X /\ Y ) )
proofend;
uniqueness
 for b1, b2 being set st ( for Z being set holds
( Z in b1 iff ex X, Y being set st
( X in SFX &amp; Y in SFY &amp; Z = X /\ Y ) ) ) &amp; ( for Z being set holds
( Z in b2 iff ex X, Y being set st
( X in SFX &amp; Y in SFY &amp; Z = X /\ Y ) ) ) holds
b1 = b2
proofend;
commutativity
 for b1 being set
for SFX, SFY being set st ( for Z being set holds
( Z in b1 iff ex X, Y being set st
( X in SFX &amp; Y in SFY &amp; Z = X /\ Y ) ) ) holds
for Z being set holds
( Z in b1 iff ex X, Y being set st
( X in SFY &amp; Y in SFX &amp; Z = X /\ Y ) )
proofend;
func DIFFERENCE (SFX,SFY) ->  set  means :Def6: :: SETFAM_1:def 6
 for Z being set holds
( Z in it iff ex X, Y being set st
( X in SFX &amp; Y in SFY &amp; Z = X \ Y ) );
existence
 ex b1 being set st
for Z being set holds
( Z in b1 iff ex X, Y being set st
( X in SFX &amp; Y in SFY &amp; Z = X \ Y ) )
proofend;
uniqueness
 for b1, b2 being set st ( for Z being set holds
( Z in b1 iff ex X, Y being set st
( X in SFX &amp; Y in SFY &amp; Z = X \ Y ) ) ) &amp; ( for Z being set holds
( Z in b2 iff ex X, Y being set st
( X in SFX &amp; Y in SFY &amp; Z = X \ Y ) ) ) holds
b1 = b2
proofend;
end;

:: deftheorem Def4 defines UNION SETFAM_1:def_4_:_
 for SFX, SFY being set
for b3 being set holds
( b3 = UNION (SFX,SFY) iff for Z being set holds
( Z in b3 iff ex X, Y being set st
( X in SFX &amp; Y in SFY &amp; Z = X \/ Y ) ) );

:: deftheorem Def5 defines INTERSECTION SETFAM_1:def_5_:_
 for SFX, SFY being set
for b3 being set holds
( b3 = INTERSECTION (SFX,SFY) iff for Z being set holds
( Z in b3 iff ex X, Y being set st
( X in SFX &amp; Y in SFY &amp; Z = X /\ Y ) ) );

:: deftheorem Def6 defines DIFFERENCE SETFAM_1:def_6_:_
 for SFX, SFY being set
for b3 being set holds
( b3 = DIFFERENCE (SFX,SFY) iff for Z being set holds
( Z in b3 iff ex X, Y being set st
( X in SFX &amp; Y in SFY &amp; Z = X \ Y ) ) );

theorem :: SETFAM_1:20
for SFX being set holds SFX is_finer_than UNION (SFX,SFX)
proofend;

theorem :: SETFAM_1:21
for SFX being set holds INTERSECTION (SFX,SFX) is_finer_than SFX
proofend;

theorem :: SETFAM_1:22
for SFX being set holds DIFFERENCE (SFX,SFX) is_finer_than SFX
proofend;

theorem :: SETFAM_1:23
for SFX, SFY being set st SFX meets SFY holds
(meet SFX) /\ (meet SFY) = meet (INTERSECTION (SFX,SFY))
proofend;

theorem :: SETFAM_1:24
for X, SFY being set st SFY <> {} holds
X \/ (meet SFY) = meet (UNION ({X},SFY))
proofend;

theorem :: SETFAM_1:25
for X, SFY being set holds X /\ (union SFY) = union (INTERSECTION ({X},SFY))
proofend;

theorem :: SETFAM_1:26
for X, SFY being set st SFY <> {} holds
X \ (union SFY) = meet (DIFFERENCE ({X},SFY))
proofend;

theorem :: SETFAM_1:27
for X, SFY being set st SFY <> {} holds
X \ (meet SFY) = union (DIFFERENCE ({X},SFY))
proofend;

theorem :: SETFAM_1:28
for SFX, SFY being set holds union (INTERSECTION (SFX,SFY)) = (union SFX) /\ (union SFY)
proofend;

theorem :: SETFAM_1:29
for SFX, SFY being set st SFX <> {} &amp; SFY <> {} holds
(meet SFX) \/ (meet SFY) c= meet (UNION (SFX,SFY))
proofend;

theorem :: SETFAM_1:30
for SFX, SFY being set holds meet (DIFFERENCE (SFX,SFY)) c= (meet SFX) \ (meet SFY)
proofend;

:: Family of subsets of a set
definition
let D be set ;
mode Subset-Family of D is Subset of (bool D);
end;

definition
let D be set ;
let F be Subset-Family of D;
:: original:union
redefine func union F ->  Subset of D;
coherence
 union F is Subset of D
proofend;
end;

definition
let D be set ;
let F be Subset-Family of D;
:: original:meet
redefine func meet F ->  Subset of D;
coherence
 meet F is Subset of D
proofend;
end;

theorem Th31: :: SETFAM_1:31
for D being set
for F, G being Subset-Family of D st ( for P being Subset of D holds
( P in F iff P in G ) ) holds
F = G
proofend;

definition
let D be set ;
let F be Subset-Family of D;
func COMPLEMENT F ->  Subset-Family of D means :Def7: :: SETFAM_1:def 7
 for P being Subset of D holds
( P in it iff P ` in F );
existence
 ex b1 being Subset-Family of D st
for P being Subset of D holds
( P in b1 iff P ` in F )
proofend;
uniqueness
 for b1, b2 being Subset-Family of D st ( for P being Subset of D holds
( P in b1 iff P ` in F ) ) &amp; ( for P being Subset of D holds
( P in b2 iff P ` in F ) ) holds
b1 = b2
proofend;
involutiveness
 for b1, b2 being Subset-Family of D st ( for P being Subset of D holds
( P in b1 iff P ` in b2 ) ) holds
for P being Subset of D holds
( P in b2 iff P ` in b1 )
proofend;
end;

:: deftheorem Def7 defines COMPLEMENT SETFAM_1:def_7_:_
 for D being set
for F, b3 being Subset-Family of D holds
( b3 = COMPLEMENT F iff for P being Subset of D holds
( P in b3 iff P ` in F ) );

theorem Th32: :: SETFAM_1:32
for D being set
for F being Subset-Family of D st F <> {} holds
COMPLEMENT F <> {}
proofend;

theorem :: SETFAM_1:33
for D being set
for F being Subset-Family of D st F <> {} holds
([#] D) \ (union F) = meet (COMPLEMENT F)
proofend;

theorem :: SETFAM_1:34
for D being set
for F being Subset-Family of D st F <> {} holds
union (COMPLEMENT F) = ([#] D) \ (meet F)
proofend;

begin

:: from YELLOW_8, 2004.07.25
theorem :: SETFAM_1:35
for X being set
for F being Subset-Family of X
for P being Subset of X holds
( P ` in COMPLEMENT F iff P in F )
proofend;

theorem Th36: :: SETFAM_1:36
for X being set
for F, G being Subset-Family of X st COMPLEMENT F c= COMPLEMENT G holds
F c= G
proofend;

theorem :: SETFAM_1:37
for X being set
for F, G being Subset-Family of X holds
( COMPLEMENT F c= G iff F c= COMPLEMENT G )
proofend;

theorem :: SETFAM_1:38
for X being set
for F, G being Subset-Family of X st COMPLEMENT F = COMPLEMENT G holds
F = G
proofend;

theorem :: SETFAM_1:39
for X being set
for F, G being Subset-Family of X holds COMPLEMENT (F \/ G) = (COMPLEMENT F) \/ (COMPLEMENT G)
proofend;

theorem :: SETFAM_1:40
for X being set
for F being Subset-Family of X st F = {X} holds
COMPLEMENT F = {{}}
proofend;

registration
let X be set ;
let F be empty Subset-Family of X;
cluster COMPLEMENT F ->  empty ;
coherence
 COMPLEMENT F is empty
proofend;
end;

:: from AMI_1
definition
let IT be set ;
attrIT is with_non-empty_elements  means :Def8: :: SETFAM_1:def 8
 not {} in IT;
end;

:: deftheorem Def8 defines with_non-empty_elements SETFAM_1:def_8_:_
 for IT being set holds
( IT is with_non-empty_elements iff not {} in IT );

registration
cluster non empty with_non-empty_elements for set ;
existence
 ex b1 being set st
( not b1 is empty &amp; b1 is with_non-empty_elements )
proofend;
end;

registration
let A be non empty set ;
cluster{A} ->  with_non-empty_elements ;
coherence
 {A} is with_non-empty_elements
proofend;
let B be non empty set ;
cluster{A,B} ->  with_non-empty_elements ;
coherence
 {A,B} is with_non-empty_elements
proofend;
let C be non empty set ;
cluster{A,B,C} ->  with_non-empty_elements ;
coherence
 {A,B,C} is with_non-empty_elements
proofend;
let D be non empty set ;
cluster{A,B,C,D} ->  with_non-empty_elements ;
coherence
 {A,B,C,D} is with_non-empty_elements
proofend;
let E be non empty set ;
cluster{A,B,C,D,E} ->  with_non-empty_elements ;
coherence
 {A,B,C,D,E} is with_non-empty_elements
proofend;
let F be non empty set ;
cluster{A,B,C,D,E,F} ->  with_non-empty_elements ;
coherence
 {A,B,C,D,E,F} is with_non-empty_elements
proofend;
let G be non empty set ;
cluster{A,B,C,D,E,F,G} ->  with_non-empty_elements ;
coherence
 {A,B,C,D,E,F,G} is with_non-empty_elements
proofend;
let H be non empty set ;
cluster{A,B,C,D,E,F,G,H} ->  with_non-empty_elements ;
coherence
 {A,B,C,D,E,F,G,H} is with_non-empty_elements
proofend;
let I be non empty set ;
cluster{A,B,C,D,E,F,G,H,I} ->  with_non-empty_elements ;
coherence
 {A,B,C,D,E,F,G,H,I} is with_non-empty_elements
proofend;
let J be non empty set ;
cluster{A,B,C,D,E,F,G,H,I,J} ->  with_non-empty_elements ;
coherence
 {A,B,C,D,E,F,G,H,I,J} is with_non-empty_elements
proofend;
end;

registration
let A, B be with_non-empty_elements set ;
clusterA \/ B ->  with_non-empty_elements ;
coherence
 A \/ B is with_non-empty_elements
proofend;
end;

:: from LATTICE4
theorem :: SETFAM_1:41
for Y, Z, X being set st union Y c= Z &amp; X in Y holds
X c= Z
proofend;

:: from LOPCLSET
theorem :: SETFAM_1:42
for A, B, X being set st X c= union (A \/ B) &amp; ( for Y being set st Y in B holds
Y misses X ) holds
X c= union A
proofend;

:: from CANTOR_1
definition
let M be set ;
let B be Subset-Family of M;
func Intersect B ->  Subset of M equals :Def9: :: SETFAM_1:def 9
 meet B if B <> {}
otherwise M;
coherence
 ( ( B <> {} implies meet B is Subset of M ) &amp; ( not B <> {} implies M is Subset of M ) )
proofend;
consistency
 for b1 being Subset of M holds verum ;
end;

:: deftheorem Def9 defines Intersect SETFAM_1:def_9_:_
 for M being set
for B being Subset-Family of M holds
( ( B <> {} implies Intersect B = meet B ) &amp; ( not B <> {} implies Intersect B = M ) );

theorem Th43: :: SETFAM_1:43
for X, x being set
for R being Subset-Family of X st x in X holds
( x in Intersect R iff for Y being set st Y in R holds
x in Y )
proofend;

theorem :: SETFAM_1:44
for X being set
for H, J being Subset-Family of X st H c= J holds
Intersect J c= Intersect H
proofend;

:: from PUA2MSS1, 2005.08.22, A.T
registration
let X be non empty with_non-empty_elements set ;
cluster  ->  non empty for Element of X;
coherence
 for b1 being Element of X holds not b1 is empty by Def8;
end;

definition
let E be set ;
attrE is empty-membered  means :Def10: :: SETFAM_1:def 10
 for x being non empty set holds not x in E;
end;

:: deftheorem Def10 defines empty-membered SETFAM_1:def_10_:_
 for E being set holds
( E is empty-membered iff for x being non empty set holds not x in E );

notation
let E be set ;
antonym  with_non-empty_element E for  empty-membered ;
end;

registration
cluster with_non-empty_element for set ;
existence
 ex b1 being set st b1 is with_non-empty_element
proofend;
end;

registration
cluster with_non-empty_element  ->  non empty for set ;
coherence
 for b1 being set st b1 is with_non-empty_element holds
not b1 is empty
proofend;
end;

:: from TRIANG_1, 2005.08.22
registration
let X be with_non-empty_element set ;
cluster non empty for Element of X;
existence
 not for b1 being Element of X holds b1 is empty
proofend;
end;

:: from MSAFREE1, 2007.03.09, A.T.
registration
let D be non empty with_non-empty_elements set ;
cluster union D ->  non empty ;
coherence
 not union D is empty
proofend;
end;

:: missing, 2007.03.09, A.T.
registration
cluster non empty with_non-empty_elements  ->  with_non-empty_element for set ;
coherence
 for b1 being set st not b1 is empty &amp; b1 is with_non-empty_elements holds
b1 is with_non-empty_element
proofend;
end;

:: the concept of a cover, 2008.03.08, A.T.
definition
let X be set ;
mode Cover of X ->  set  means :Def11: :: SETFAM_1:def 11
X c= union it;
existence
 ex b1 being set st X c= union b1
proofend;
end;

:: deftheorem Def11 defines Cover SETFAM_1:def_11_:_
 for X being set
for b2 being set holds
( b2 is Cover of X iff X c= union b2 );

theorem :: SETFAM_1:45
for X being set
for F being Subset-Family of X holds
( F is Cover of X iff union F = X )
proofend;

:: from MEASURE1, 2008.06.08, A.T.
theorem Th46: :: SETFAM_1:46
for X being set holds {{}} is Subset-Family of X
proofend;

:: from BORSUK_5 (generalized), 2008.06.08, A.T.
definition
let X be set ;
let F be Subset-Family of X;
attrF is with_proper_subsets  means :Def12: :: SETFAM_1:def 12
 not X in F;
end;

:: deftheorem Def12 defines with_proper_subsets SETFAM_1:def_12_:_
 for X being set
for F being Subset-Family of X holds
( F is with_proper_subsets iff not X in F );

theorem :: SETFAM_1:47
for TS being set
for F, G being Subset-Family of TS st F is with_proper_subsets &amp; G c= F holds
G is with_proper_subsets
proofend;

registration
let TS be non empty set ;
cluster with_proper_subsets for Element of bool (bool TS);
existence
 ex b1 being Subset-Family of TS st b1 is with_proper_subsets
proofend;
end;

theorem :: SETFAM_1:48
for TS being non empty set
for A, B being with_proper_subsets Subset-Family of TS holds A \/ B is with_proper_subsets
proofend;

:: from YELLOW21, 2008.09.10, A.T.
registration
cluster non trivial  ->  with_non-empty_element for set ;
coherence
 for b1 being set st not b1 is trivial holds
b1 is with_non-empty_element
proofend;
end;

:: from PCOMPS_1, 2010.02.26, A.T.
definition
let X be set ;
:: original:bool
redefine func bool X ->  Subset-Family of X;
coherence
 bool X is Subset-Family of X by ZFMISC_1:def_1;
end;

:: from HAHNBAN, 2011.04.26., A.T.
theorem :: SETFAM_1:49
for A being non empty set
for b being set st A <> {b} holds
ex a being Element of A st a <> b
proofend;