:: Families of Sets
:: by Beata Padlewska
::
:: Received April 5, 1989
:: Copyright (c) 1990-2017 Association of Mizar Users
:: (Stowarzyszenie Uzytkownikow Mizara, Bialystok, Poland).
:: This code can be distributed under the GNU General Public Licence
:: version 3.0 or later, or the Creative Commons Attribution-ShareAlike
:: License version 3.0 or later, subject to the binding interpretation
:: detailed in file COPYING.interpretation.
:: See COPYING.GPL and COPYING.CC-BY-SA for the full text of these
:: licenses, or see http://www.gnu.org/licenses/gpl.html and
:: http://creativecommons.org/licenses/by-sa/3.0/.
environ
vocabularies XBOOLE_0, TARSKI, SUBSET_1, ZFMISC_1, SETFAM_1;
notations TARSKI, XBOOLE_0, ENUMSET1, ZFMISC_1, SUBSET_1;
constructors TARSKI, ENUMSET1, SUBSET_1;
registrations XBOOLE_0, SUBSET_1;
requirements SUBSET, BOOLE;
definitions TARSKI, XBOOLE_0;
equalities SUBSET_1;
expansions TARSKI, XBOOLE_0;
theorems TARSKI, XBOOLE_0, ZFMISC_1, ENUMSET1, XBOOLE_1;
schemes XBOOLE_0, SUBSET_1, XFAMILY;
begin
reserve X,Y,Z,Z1,Z2,D for set,x,y for object;
definition
let X;
func meet X -> set means
:Def1:
for x being object holds x in it iff
for Y holds Y in X implies x in Y if X <> {}
otherwise it = {};
existence
proof
thus X <> {} implies ex Z1 st
for x being object holds x in Z1 iff for Z st Z in X
holds x in Z
proof
defpred X[object] means for Z st Z in X holds $1 in Z;
assume
A1: X <> {};
consider Y such that
A2: for x being object holds x in Y iff x in union X & X[x]
from XBOOLE_0:sch 1;
take Y;
for x being object holds (for Z st Z in X holds x in Z) implies x in Y
proof
set y = the Element of X;
let x being object such that
A3: for Z st Z in X holds x in Z;
x in y by A1,A3;
then x in union X by A1,TARSKI:def 4;
hence thesis by A2,A3;
end;
hence thesis by A2;
end;
thus thesis;
end;
uniqueness
proof
let Z1,Z2;
now
assume that
X <> {} and
A4: for x being object holds x in Z1 iff
for Y holds Y in X implies x in Y and
A5: for x being object holds x in Z2 iff
for Y holds Y in X implies x in Y;
now
let x be object;
x in Z1 iff for Y holds Y in X implies x in Y by A4;
hence x in Z1 iff x in Z2 by A5;
end;
hence Z1 = Z2 by TARSKI:2;
end;
hence thesis;
end;
consistency;
end;
:: Intersection of families of sets
theorem
meet {} = {} by Def1;
theorem Th2:
meet X c= union X
proof
A1: now
assume
A2: X <> {};
now
set y = the Element of X;
let x be object;
assume x in meet X;
then x in y by A2,Def1;
hence x in union X by A2,TARSKI:def 4;
end;
hence thesis;
end;
X = {} implies thesis by Def1;
hence thesis by A1;
end;
theorem Th3:
Z in X implies meet X c= Z
by Def1;
theorem
{} in X implies meet X = {} by Th3,XBOOLE_1:3;
theorem
X <> {} & (for Z1 st Z1 in X holds Z c= Z1) implies Z c= meet X
proof
assume that
A1: X <> {} and
A2: for Z1 st Z1 in X holds Z c= Z1;
thus Z c= meet X
proof
let x be object such that
A3: x in Z;
for Y st Y in X holds x in Y
proof
let Y;
assume Y in X;
then Z c= Y by A2;
hence thesis by A3;
end;
hence thesis by A1,Def1;
end;
end;
theorem Th6:
X <> {} & X c= Y implies meet Y c= meet X
proof
assume that
A1: X <> {} and
A2: X c= Y;
let x be object;
assume x in meet Y;
then for Z st Z in X holds x in Z by A2,Def1;
hence thesis by A1,Def1;
end;
theorem
X in Y & X c= Z implies meet Y c= Z
proof
assume that
A1: X in Y and
A2: X c= Z;
meet Y c= X by A1,Th3;
hence thesis by A2;
end;
theorem
X in Y & X misses Z implies meet Y misses Z by Th3,XBOOLE_1:63;
theorem
X <> {} & Y <> {} implies meet (X \/ Y) = meet X /\ meet Y
proof
assume that
A1: X <> {} and
A2: Y <> {};
A3: meet X /\ meet Y c= meet (X \/ Y)
proof
let x be object;
assume x in meet X /\ meet Y;
then
A4: x in meet X & x in meet Y by XBOOLE_0:def 4;
now
let Z;
assume Z in X \/ Y;
then Z in X or Z in Y by XBOOLE_0:def 3;
hence x in Z by A4,Def1;
end;
hence thesis by A1,Def1;
end;
meet (X \/ Y) c= meet X & meet (X \/ Y) c= meet Y by A1,A2,Th6,XBOOLE_1:7;
then meet (X \/ Y) c= meet X /\ meet Y by XBOOLE_1:19;
hence thesis by A3;
end;
theorem
meet {X} = X
proof
A1: X c= meet {X}
proof
let y be object;
assume y in X;
then for Z st Z in {X} holds y in Z by TARSKI:def 1;
hence thesis by Def1;
end;
X in {X} by TARSKI:def 1;
then meet {X} c= X by Th3;
hence thesis by A1;
end;
theorem
meet {X,Y} = X /\ Y
proof
A1: X in {X,Y} & Y in {X,Y} by TARSKI:def 2;
for x being object holds x in meet {X,Y} iff x in X & x in Y
proof let x be object;
thus x in meet {X,Y} implies x in X & x in Y by A1,Def1;
assume x in X & x in Y;
then for Z holds Z in {X,Y} implies x in Z by TARSKI:def 2;
hence thesis by Def1;
end;
hence thesis by XBOOLE_0:def 4;
end;
reserve SFX,SFY,SFZ for set;
definition
let SFX,SFY;
pred SFX is_finer_than SFY means
for X st X in SFX ex Y st Y in SFY & X c= Y;
reflexivity;
pred SFY is_coarser_than SFX means
for Y st Y in SFY ex X st X in SFX & X c= Y;
reflexivity;
end;
theorem
SFX c= SFY implies SFX is_finer_than SFY;
theorem
SFX is_finer_than SFY implies union SFX c= union SFY
proof
assume
A1: for X st X in SFX ex Y st Y in SFY & X c= Y;
thus union SFX c= union SFY
proof
let x be object;
assume x in union SFX;
then consider Y such that
A2: x in Y and
A3: Y in SFX by TARSKI:def 4;
ex Z st Z in SFY & Y c= Z by A1,A3;
hence thesis by A2,TARSKI:def 4;
end;
end;
theorem
SFY <> {} & SFY is_coarser_than SFX implies meet SFX c= meet SFY
proof
assume that
A1: SFY <> {} and
A2: for Z2 st Z2 in SFY ex Z1 st Z1 in SFX & Z1 c= Z2;
meet SFX c= meet SFY
proof
let x be object such that
A3: x in meet SFX;
for Z st Z in SFY holds x in Z
proof
let Z;
assume Z in SFY;
then consider Z1 such that
A4: Z1 in SFX and
A5: Z1 c= Z by A2;
x in Z1 by A3,A4,Def1;
hence thesis by A5;
end;
hence thesis by A1,Def1;
end;
hence thesis;
end;
theorem
{} is_finer_than SFX;
theorem
SFX is_finer_than {} implies SFX = {}
proof
assume
A1: for X st X in SFX ex Y st Y in {} & X c= Y;
set x = the Element of SFX;
assume not thesis;
then ex Y st Y in {} & x c= Y by A1;
hence contradiction;
end;
theorem
SFX is_finer_than SFY & SFY is_finer_than SFZ implies SFX is_finer_than SFZ
proof
assume that
A1: for X st X in SFX ex Y st Y in SFY & X c= Y and
A2: for X st X in SFY ex Y st Y in SFZ & X c= Y;
let X;
assume X in SFX;
then consider Y such that
A3: Y in SFY and
A4: X c= Y by A1;
consider Z such that
A5: Z in SFZ & Y c= Z by A2,A3;
take Z;
thus thesis by A4,A5;
end;
theorem
SFX is_finer_than {Y} implies for X st X in SFX holds X c= Y
proof
assume
A1: for X st X in SFX ex Z st Z in {Y} & X c= Z;
let X;
assume X in SFX;
then ex Z st Z in {Y} & X c= Z by A1;
hence thesis by TARSKI:def 1;
end;
theorem
SFX is_finer_than {X,Y} implies for Z st Z in SFX holds Z c= X or Z c= Y
proof
assume
A1: for Z1 st Z1 in SFX ex Z2 st Z2 in {X,Y} & Z1 c= Z2;
let Z;
assume Z in SFX;
then consider Z2 such that
A2: Z2 in {X,Y} and
A3: Z c= Z2 by A1;
{X,Y} = {X} \/ {Y} by ENUMSET1:1;
then Z2 in {X} or Z2 in {Y} by A2,XBOOLE_0:def 3;
hence thesis by A3,TARSKI:def 1;
end;
definition
let SFX,SFY;
func UNION (SFX,SFY) -> set means
:Def4:
Z in it iff ex X,Y st X in SFX & Y in SFY & Z = X \/ Y;
existence
proof
defpred X[set] means
ex Z being set st $1 = Z & ex X,Y st X in SFX & Y in
SFY & Z = X \/ Y;
consider XX being set such that
A1: for x being set
holds x in XX iff x in bool(union SFX \/ union SFY) & X[x]
from XFAMILY:sch 1;
take XX;
for Z holds Z in XX iff ex X,Y st X in SFX & Y in SFY & Z = X \/ Y
proof
let Z;
A2: now
given X,Y such that
A3: X in SFX & Y in SFY and
A4: Z = X \/ Y;
X c= union SFX & Y c= union SFY by A3,ZFMISC_1:74;
then Z c= union SFX \/ union SFY by A4,XBOOLE_1:13;
hence Z in XX by A1,A3,A4;
end;
now
assume Z in XX;
then ex Z1 st Z = Z1 & ex X,Y st X in SFX & Y in SFY & Z1 = X \/ Y by
A1;
hence ex X,Y st X in SFX & Y in SFY & Z = X \/ Y;
end;
hence thesis by A2;
end;
hence thesis;
end;
uniqueness
proof
let Z1,Z2 be set;
assume that
A5: for Z holds Z in Z1 iff ex X,Y st X in SFX & Y in SFY & Z = X \/ Y and
A6: for Z holds Z in Z2 iff ex X,Y st X in SFX & Y in SFY & Z = X \/ Y;
now
let Z be object;
Z in Z1 iff ex X,Y st X in SFX & Y in SFY & Z = X \/ Y by A5;
hence Z in Z1 iff Z in Z2 by A6;
end;
hence thesis by TARSKI:2;
end;
commutativity
proof
let SFZ,SFX,SFY;
assume
A7: for Z holds Z in SFZ iff ex X,Y st X in SFX & Y in SFY & Z = X \/ Y;
let Z;
hereby
assume Z in SFZ;
then ex X,Y st X in SFX & Y in SFY & Z = X \/ Y by A7;
hence ex Y,X st Y in SFY & X in SFX & Z = Y \/ X;
end;
thus thesis by A7;
end;
func INTERSECTION (SFX,SFY) -> set means
:Def5:
Z in it iff ex X,Y st X in SFX & Y in SFY & Z = X /\ Y;
existence
proof
defpred X[set] means ex Z being set st $1 = Z & ex X,Y st X in SFX & Y in
SFY & Z = X /\ Y;
consider XX being set such that
A8: for x being set holds x in XX iff x in bool(union SFX /\ union SFY) & X[x]
from XFAMILY:sch 1;
take XX;
for Z holds Z in XX iff ex X,Y st X in SFX & Y in SFY & Z = X /\ Y
proof
let Z;
A9: now
given X,Y such that
A10: X in SFX & Y in SFY and
A11: Z = X /\ Y;
X c= union SFX & Y c= union SFY by A10,ZFMISC_1:74;
then Z c= union SFX /\ union SFY by A11,XBOOLE_1:27;
hence Z in XX by A8,A10,A11;
end;
now
assume Z in XX;
then ex Z1 st Z = Z1 & ex X,Y st X in SFX & Y in SFY & Z1 = X /\ Y by
A8;
hence ex X,Y st X in SFX & Y in SFY & Z = X /\ Y;
end;
hence thesis by A9;
end;
hence thesis;
end;
uniqueness
proof
let Z1,Z2 be set;
assume that
A12: for Z holds Z in Z1 iff ex X,Y st X in SFX & Y in SFY & Z = X /\ Y and
A13: for Z holds Z in Z2 iff ex X,Y st X in SFX & Y in SFY & Z = X /\ Y;
now
let Z be object;
Z in Z1 iff ex X,Y st X in SFX & Y in SFY & Z = X /\ Y by A12;
hence Z in Z1 iff Z in Z2 by A13;
end;
hence thesis by TARSKI:2;
end;
commutativity
proof
let SFZ,SFX,SFY;
assume
A14: for Z holds Z in SFZ iff ex X,Y st X in SFX & Y in SFY & Z = X /\ Y;
let Z;
hereby
assume Z in SFZ;
then ex X,Y st X in SFX & Y in SFY & Z = X /\ Y by A14;
hence ex Y,X st Y in SFY & X in SFX & Z = Y /\ X;
end;
thus thesis by A14;
end;
func DIFFERENCE (SFX,SFY) -> set means
:Def6:
Z in it iff ex X,Y st X in SFX & Y in SFY & Z = X \ Y;
existence
proof
defpred X[set] means ex Z being set st $1 = Z & ex X,Y st X in SFX & Y in
SFY & Z = X \ Y;
consider XX being set such that
A15: for x being set holds x in XX iff x in bool union SFX & X[x] from XFAMILY:
sch 1;
take XX;
for Z holds Z in XX iff ex X,Y st X in SFX & Y in SFY & Z = X \ Y
proof
let Z;
A16: now
given X,Y such that
A17: X in SFX and
A18: Y in SFY and
A19: Z = X \ Y;
X c= union SFX by A17,ZFMISC_1:74;
then Z c= union SFX by A19;
hence Z in XX by A15,A17,A18,A19;
end;
now
assume Z in XX;
then ex Z1 st Z = Z1 & ex X,Y st X in SFX & Y in SFY & Z1 = X \ Y by
A15;
hence ex X,Y st X in SFX & Y in SFY & Z = X \ Y;
end;
hence thesis by A16;
end;
hence thesis;
end;
uniqueness
proof
let Z1,Z2 be set;
assume that
A20: for Z holds Z in Z1 iff ex X,Y st X in SFX & Y in SFY & Z = X \ Y and
A21: for Z holds Z in Z2 iff ex X,Y st X in SFX & Y in SFY & Z = X \ Y;
now
let Z be object;
Z in Z1 iff ex X,Y st X in SFX & Y in SFY & Z = X \ Y by A20;
hence Z in Z1 iff Z in Z2 by A21;
end;
hence thesis by TARSKI:2;
end;
end;
theorem
SFX is_finer_than UNION(SFX,SFX)
proof
let X such that
A1: X in SFX;
take X;
X = X \/ X;
hence thesis by A1,Def4;
end;
theorem
INTERSECTION(SFX,SFX) is_finer_than SFX
proof
let X;
assume X in INTERSECTION(SFX,SFX);
then consider Z1,Z2 such that
A1: Z1 in SFX and
Z2 in SFX and
A2: X = Z1 /\ Z2 by Def5;
take Z1;
thus thesis by A1,A2,XBOOLE_1:17;
end;
theorem
DIFFERENCE(SFX,SFX) is_finer_than SFX
proof
let X;
assume X in DIFFERENCE(SFX,SFX);
then consider Z1,Z2 such that
A1: Z1 in SFX and
Z2 in SFX and
A2: X = Z1 \ Z2 by Def6;
take Z1;
thus thesis by A1,A2;
end;
theorem
SFX meets SFY implies meet SFX /\ meet SFY = meet INTERSECTION(SFX,SFY )
proof
set y = the Element of SFX /\ SFY;
assume
A1: SFX /\ SFY <> {};
then
A2: SFY <> {};
A3: y in SFX by A1,XBOOLE_0:def 4;
A4: y in SFY by A1,XBOOLE_0:def 4;
A5: SFX <> {} by A1;
A6: meet INTERSECTION(SFX,SFY) c= meet SFX /\ meet SFY
proof
let x be object such that
A7: x in meet INTERSECTION(SFX,SFY);
for Z st Z in SFY holds x in Z
proof
let Z;
assume Z in SFY;
then y /\ Z in INTERSECTION(SFX,SFY) by A3,Def5;
then x in y /\ Z by A7,Def1;
hence thesis by XBOOLE_0:def 4;
end;
then
A8: x in meet SFY by A2,Def1;
for Z st Z in SFX holds x in Z
proof
let Z;
assume Z in SFX;
then Z /\ y in INTERSECTION(SFX,SFY) by A4,Def5;
then x in Z /\ y by A7,Def1;
hence thesis by XBOOLE_0:def 4;
end;
then x in meet SFX by A5,Def1;
hence thesis by A8,XBOOLE_0:def 4;
end;
A9: y /\ y in INTERSECTION(SFX,SFY) by A3,A4,Def5;
meet SFX /\ meet SFY c= meet INTERSECTION(SFX,SFY)
proof
let x be object;
assume x in meet SFX /\ meet SFY;
then
A10: x in meet SFX & x in meet SFY by XBOOLE_0:def 4;
for Z st Z in INTERSECTION(SFX,SFY) holds x in Z
proof
let Z;
assume Z in INTERSECTION(SFX,SFY);
then consider Z1,Z2 such that
A11: Z1 in SFX & Z2 in SFY and
A12: Z = Z1 /\ Z2 by Def5;
x in Z1 & x in Z2 by A10,A11,Def1;
hence thesis by A12,XBOOLE_0:def 4;
end;
hence thesis by A9,Def1;
end;
hence thesis by A6;
end;
theorem
SFY <> {} implies X \/ meet SFY = meet UNION({X},SFY)
proof
assume
A1: SFY <> {};
set y = the Element of SFY;
X in {X} by TARSKI:def 1;
then
A2: X \/ y in UNION({X},SFY) by A1,Def4;
A3: X \/ meet SFY c= meet UNION({X},SFY)
proof
let x be object;
assume x in X \/ meet SFY;
then
A4: x in X or x in meet SFY by XBOOLE_0:def 3;
for Z st Z in UNION({X},SFY) holds x in Z
proof
let Z;
assume Z in UNION({X},SFY);
then consider Z1,Z2 such that
A5: Z1 in {X} & Z2 in SFY and
A6: Z = Z1 \/ Z2 by Def4;
x in Z1 or x in Z2 by A4,A5,Def1,TARSKI:def 1;
hence thesis by A6,XBOOLE_0:def 3;
end;
hence thesis by A2,Def1;
end;
meet UNION({X},SFY) c= X \/ meet SFY
proof
let x be object;
assume
A7: x in meet UNION({X},SFY);
assume
A8: not x in X \/ meet SFY;
then
A9: not x in X by XBOOLE_0:def 3;
not x in meet SFY by A8,XBOOLE_0:def 3;
then consider Z such that
A10: Z in SFY and
A11: not x in Z by A1,Def1;
X in {X} by TARSKI:def 1;
then X \/ Z in UNION({X},SFY) by A10,Def4;
then x in X \/ Z by A7,Def1;
hence contradiction by A9,A11,XBOOLE_0:def 3;
end;
hence thesis by A3;
end;
theorem
X /\ union SFY = union INTERSECTION({X},SFY)
proof
A1: union INTERSECTION({X},SFY) c= X /\ union SFY
proof
let x be object;
assume x in union INTERSECTION({X},SFY);
then consider Z such that
A2: x in Z and
A3: Z in INTERSECTION({X},SFY) by TARSKI:def 4;
consider X1,X2 be set such that
A4: X1 in {X} and
A5: X2 in SFY and
A6: Z = X1 /\ X2 by A3,Def5;
x in X2 by A2,A6,XBOOLE_0:def 4;
then
A7: x in union SFY by A5,TARSKI:def 4;
X1 = X by A4,TARSKI:def 1;
then x in X by A2,A6,XBOOLE_0:def 4;
hence thesis by A7,XBOOLE_0:def 4;
end;
X /\ union SFY c= union INTERSECTION({X},SFY)
proof
let x be object;
assume
A8: x in X /\ union SFY;
then x in union SFY by XBOOLE_0:def 4;
then consider Y such that
A9: x in Y and
A10: Y in SFY by TARSKI:def 4;
x in X by A8,XBOOLE_0:def 4;
then
A11: x in X /\ Y by A9,XBOOLE_0:def 4;
X in {X} by TARSKI:def 1;
then X /\ Y in INTERSECTION({X},SFY) by A10,Def5;
hence thesis by A11,TARSKI:def 4;
end;
hence thesis by A1;
end;
theorem
SFY <> {} implies X \ union SFY = meet DIFFERENCE({X},SFY)
proof
set y = the Element of SFY;
A1: X in {X} by TARSKI:def 1;
assume SFY <> {};
then
A2: X \ y in DIFFERENCE({X},SFY) by A1,Def6;
A3: meet DIFFERENCE({X},SFY) c= X \ union SFY
proof
let x be object;
assume
A4: x in meet DIFFERENCE({X},SFY);
for Z st Z in SFY holds not x in Z
proof
let Z;
assume Z in SFY;
then X \ Z in DIFFERENCE({X},SFY) by A1,Def6;
then x in X \ Z by A4,Def1;
hence thesis by XBOOLE_0:def 5;
end;
then for Z st x in Z holds not Z in SFY;
then
A5: not x in union SFY by TARSKI:def 4;
x in X \ y by A2,A4,Def1;
hence thesis by A5,XBOOLE_0:def 5;
end;
X \ union SFY c= meet DIFFERENCE({X},SFY)
proof
let x be object;
assume x in X \ union SFY;
then
A6: x in X & not x in union SFY by XBOOLE_0:def 5;
for Z st Z in DIFFERENCE({X},SFY) holds x in Z
proof
let Z;
assume Z in DIFFERENCE({X},SFY);
then consider Z1,Z2 such that
A7: Z1 in {X} & Z2 in SFY and
A8: Z = Z1 \ Z2 by Def6;
x in Z1 & not x in Z2 by A6,A7,TARSKI:def 1,def 4;
hence thesis by A8,XBOOLE_0:def 5;
end;
hence thesis by A2,Def1;
end;
hence thesis by A3;
end;
theorem
SFY <> {} implies X \ meet SFY = union DIFFERENCE ({X},SFY)
proof
A1: X in {X} by TARSKI:def 1;
A2: union DIFFERENCE({X},SFY) c= X \ meet SFY
proof
let x be object;
assume x in union DIFFERENCE({X},SFY);
then consider Z such that
A3: x in Z and
A4: Z in DIFFERENCE({X},SFY) by TARSKI:def 4;
consider Z1,Z2 such that
A5: Z1 in {X} and
A6: Z2 in SFY and
A7: Z = Z1 \ Z2 by A4,Def6;
not x in Z2 by A3,A7,XBOOLE_0:def 5;
then
A8: not x in meet SFY by A6,Def1;
Z1 = X by A5,TARSKI:def 1;
hence thesis by A3,A7,A8,XBOOLE_0:def 5;
end;
assume
A9: SFY <> {};
X \ meet SFY c= union DIFFERENCE({X},SFY)
proof
let x be object;
assume
A10: x in X \ meet SFY;
then not x in meet SFY by XBOOLE_0:def 5;
then consider Z such that
A11: Z in SFY and
A12: not x in Z by A9,Def1;
A13: x in X \ Z by A10,A12,XBOOLE_0:def 5;
X \ Z in DIFFERENCE({X},SFY) by A1,A11,Def6;
hence thesis by A13,TARSKI:def 4;
end;
hence thesis by A2;
end;
theorem
union INTERSECTION (SFX,SFY) = union SFX /\ union SFY
proof
thus union INTERSECTION(SFX,SFY) c= union SFX /\ union SFY
proof
let x be object;
assume x in union INTERSECTION(SFX,SFY);
then consider Z such that
A1: x in Z and
A2: Z in INTERSECTION(SFX,SFY) by TARSKI:def 4;
consider X,Y such that
A3: X in SFX and
A4: Y in SFY and
A5: Z = X /\ Y by A2,Def5;
x in Y by A1,A5,XBOOLE_0:def 4;
then
A6: x in union SFY by A4,TARSKI:def 4;
x in X by A1,A5,XBOOLE_0:def 4;
then x in union SFX by A3,TARSKI:def 4;
hence thesis by A6,XBOOLE_0:def 4;
end;
let x be object;
assume
A7: x in union SFX /\ union SFY;
then x in union SFX by XBOOLE_0:def 4;
then consider X0 being set such that
A8: x in X0 & X0 in SFX by TARSKI:def 4;
x in union SFY by A7,XBOOLE_0:def 4;
then consider Y0 being set such that
A9: x in Y0 & Y0 in SFY by TARSKI:def 4;
X0 /\ Y0 in INTERSECTION(SFX,SFY) & x in X0 /\ Y0 by A8,A9,Def5,
XBOOLE_0:def 4;
hence thesis by TARSKI:def 4;
end;
theorem
SFX <> {} & SFY <> {} implies meet SFX \/ meet SFY c= meet UNION (SFX, SFY)
proof
set y = the Element of SFX;
set z = the Element of SFY;
assume SFX <> {} & SFY <> {};
then
A1: y \/ z in UNION(SFX,SFY) by Def4;
let x be object;
assume x in meet SFX \/ meet SFY;
then
A2: x in meet SFX or x in meet SFY by XBOOLE_0:def 3;
for Z st Z in UNION(SFX,SFY) holds x in Z
proof
let Z;
assume Z in UNION(SFX,SFY);
then consider X,Y such that
A3: X in SFX & Y in SFY and
A4: Z = X \/ Y by Def4;
x in X or x in Y by A2,A3,Def1;
hence thesis by A4,XBOOLE_0:def 3;
end;
hence thesis by A1,Def1;
end;
theorem
meet DIFFERENCE (SFX,SFY) c= meet SFX \ meet SFY
proof
per cases;
suppose
A1: SFX = {} or SFY = {};
now
assume DIFFERENCE (SFX,SFY) <> {};
then consider e being object such that
A2: e in DIFFERENCE (SFX,SFY) by XBOOLE_0:def 1;
ex X,Y st X in SFX & Y in SFY & e = X \ Y by A2,Def6;
hence contradiction by A1;
end;
then meet DIFFERENCE (SFX,SFY) = {} by Def1;
hence thesis;
end;
suppose
A3: SFX <> {} & SFY <> {};
set z = the Element of SFX;
set y = the Element of SFY;
let x be object such that
A4: x in meet DIFFERENCE (SFX,SFY);
for Z st Z in SFX holds x in Z
proof
let Z;
assume Z in SFX;
then Z \ y in DIFFERENCE (SFX,SFY) by A3,Def6;
then x in Z \ y by A4,Def1;
hence thesis;
end;
then
A5: x in meet SFX by A3,Def1;
z \ y in DIFFERENCE(SFX,SFY) by A3,Def6;
then x in z \ y by A4,Def1;
then not x in y by XBOOLE_0:def 5;
then not x in meet SFY by A3,Def1;
hence thesis by A5,XBOOLE_0:def 5;
end;
end;
:: Family of subsets of a set
definition
let D be set;
mode Subset-Family of D is Subset of bool D;
end;
reserve F,G for Subset-Family of D;
reserve P for Subset of D;
definition
let D,F;
redefine func union F -> Subset of D;
coherence
proof
union F c= D
proof
let x be object;
assume x in union F;
then ex Z st x in Z & Z in F by TARSKI:def 4;
hence thesis;
end;
hence thesis;
end;
end;
definition
let D,F;
redefine func meet F -> Subset of D;
coherence
proof
meet F c= D
proof
A1: meet F c= union F by Th2;
let x be object;
assume x in meet F;
then x in union F by A1;
hence thesis;
end;
hence thesis;
end;
end;
theorem Th31:
(for P holds P in F iff P in G) implies F=G
proof
assume
A1: for P holds P in F iff P in G;
thus F c= G
by A1;
let x be object;
assume x in G;
hence thesis by A1;
end;
definition
let D,F;
func COMPLEMENT(F) -> Subset-Family of D means
:Def7:
for P being Subset of D holds P in it iff P` in F;
existence
proof
defpred X[Subset of D] means $1` in F;
thus ex G being Subset-Family of D st for P being Subset of D holds P in G
iff X[P] from SUBSET_1:sch 3;
end;
uniqueness
proof
let G,H be Subset-Family of D;
assume that
A1: for P holds P in G iff P` in F and
A2: for P holds P in H iff P` in F;
now
let P;
P in G iff P` in F by A1;
hence P in G iff P in H by A2;
end;
hence thesis by Th31;
end;
involutiveness
proof
let F,G such that
A3: for P being Subset of D holds P in F iff P` in G;
let P be Subset of D;
P`` = P;
hence thesis by A3;
end;
end;
theorem Th32:
F <> {} implies COMPLEMENT(F) <> {}
proof
set X = the Element of F;
assume
A1: F <> {};
then reconsider X as Subset of D by TARSKI:def 3;
X`` = X;
hence thesis by A1,Def7;
end;
theorem
F <> {} implies [#] D \ union F = meet (COMPLEMENT(F))
proof
A1: for x st x in D holds (for X st X in F holds not x in X) iff for Y st Y
in COMPLEMENT(F) holds x in Y
proof
let x such that
A2: x in D;
thus (for X st X in F holds not x in X) implies for Y st Y in COMPLEMENT(F
) holds x in Y
proof
assume
A3: for X st X in F holds not x in X;
let Y;
assume
A4: Y in COMPLEMENT(F);
then reconsider Y as Subset of D;
Y` in F by A4,Def7;
then not x in Y` by A3;
hence thesis by A2,XBOOLE_0:def 5;
end;
assume
A5: for Y st Y in COMPLEMENT(F) holds x in Y;
let X;
assume
A6: X in F;
then reconsider X as Subset of D;
X`` = X;
then X` in COMPLEMENT(F) by A6,Def7;
then x in X` by A5;
hence thesis by XBOOLE_0:def 5;
end;
assume F <> {};
then
A7: COMPLEMENT(F) <> {} by Th32;
A8: [#] D \ union F c= meet COMPLEMENT(F)
proof
let x be object;
assume
A9: x in [#] D \ union F;
then not x in union F by XBOOLE_0:def 5;
then for X st X in F holds not x in X by TARSKI:def 4;
then for Y st Y in COMPLEMENT(F) holds x in Y by A1,A9;
hence thesis by A7,Def1;
end;
meet COMPLEMENT(F) c= [#] D \ union F
proof
let x be object;
assume
A10: x in meet COMPLEMENT(F);
then for X holds X in COMPLEMENT(F) implies x in X by Def1;
then for Y st x in Y holds not Y in F by A1;
then not x in union F by TARSKI:def 4;
hence thesis by A10,XBOOLE_0:def 5;
end;
hence thesis by A8;
end;
theorem
F <> {} implies union COMPLEMENT(F) = [#] D \ meet F
proof
assume
A1: F <> {};
A2: [#] D \ meet F c= union COMPLEMENT(F)
proof
let x be object;
assume
A3: x in [#] D \ meet F;
then not x in meet F by XBOOLE_0:def 5;
then consider X such that
A4: X in F and
A5: not x in X by A1,Def1;
reconsider X as Subset of D by A4;
reconsider XX=X` as set;
A6: X`` = X;
ex Y st x in Y & Y in COMPLEMENT(F)
proof
take XX;
thus thesis by A3,A4,A5,A6,Def7,XBOOLE_0:def 5;
end;
hence thesis by TARSKI:def 4;
end;
union COMPLEMENT(F) c= [#] D \ meet F
proof
let x be object;
assume
A7: x in union COMPLEMENT(F);
then consider X such that
A8: x in X and
A9: X in COMPLEMENT(F) by TARSKI:def 4;
reconsider X as Subset of D by A9;
reconsider XX=X` as set;
ex Y st Y in F & not x in Y
proof
take Y = XX;
thus Y in F by A9,Def7;
thus thesis by A8,XBOOLE_0:def 5;
end;
then not x in meet F by Def1;
hence thesis by A7,XBOOLE_0:def 5;
end;
hence thesis by A2;
end;
begin :: Addendum
:: from YELLOW_8, 2004.07.25
theorem
for X being set, F being Subset-Family of X for P being Subset of X
holds P` in COMPLEMENT F iff P in F
proof
let X be set, F be Subset-Family of X;
let P be Subset of X;
P = P``;
hence thesis by Def7;
end;
theorem Th36:
for X being set, F,G being Subset-Family of X st COMPLEMENT F c=
COMPLEMENT G holds F c= G
proof
let X be set, F,G be Subset-Family of X such that
A1: COMPLEMENT F c= COMPLEMENT G;
let x be object;
assume
A2: x in F;
then reconsider A = x as Subset of X;
A in COMPLEMENT COMPLEMENT F by A2;
then A` in COMPLEMENT F by Def7;
then A`` in G by A1,Def7;
hence thesis;
end;
theorem
for X being set, F,G being Subset-Family of X holds COMPLEMENT F c= G
iff F c= COMPLEMENT G
proof
let X be set, F,G be Subset-Family of X;
hereby
assume COMPLEMENT F c= G;
then COMPLEMENT F c= COMPLEMENT COMPLEMENT G;
hence F c= COMPLEMENT G by Th36;
end;
assume F c= COMPLEMENT G;
then COMPLEMENT COMPLEMENT F c= COMPLEMENT G;
hence thesis by Th36;
end;
theorem
for X being set, F,G being Subset-Family of X st COMPLEMENT F =
COMPLEMENT G holds F = G
proof
let X be set, F,G be Subset-Family of X;
assume COMPLEMENT F = COMPLEMENT G;
hence F = COMPLEMENT COMPLEMENT G .= G;
end;
theorem
for X being set, F,G being Subset-Family of X holds COMPLEMENT(F \/ G)
= COMPLEMENT F \/ COMPLEMENT G
proof
let X be set, F,G be Subset-Family of X;
for P being Subset of X holds P in COMPLEMENT F \/ COMPLEMENT G iff P`
in F \/ G
proof
let P be Subset of X;
P in COMPLEMENT F or P in COMPLEMENT G iff P` in F or P` in G by Def7;
hence thesis by XBOOLE_0:def 3;
end;
hence thesis by Def7;
end;
theorem
for X being set, F being Subset-Family of X st F = {X} holds
COMPLEMENT F = {{}}
proof
let X be set, F be Subset-Family of X such that
A1: F = {X};
{} c= X;
then reconsider G = {{}} as Subset-Family of X by ZFMISC_1:31;
reconsider G as Subset-Family of X;
for P being Subset of X holds P in G iff P` in F
proof
let P be Subset of X;
hereby
assume P in G;
then P = {}X by TARSKI:def 1;
hence P` in F by A1,TARSKI:def 1;
end;
assume P` in F;
then
A2: P` = [#]X by A1,TARSKI:def 1;
P = P`` .= {} by A2,XBOOLE_1:37;
hence thesis by TARSKI:def 1;
end;
hence thesis by Def7;
end;
registration
let X be set, F be empty Subset-Family of X;
cluster COMPLEMENT F -> empty;
coherence
by Def7;
end;
:: from AMI_1
definition
let IT be set;
attr IT is with_non-empty_elements means
:Def8:
not {} in IT;
end;
registration
cluster non empty with_non-empty_elements for set;
existence
proof
take {{{}}};
thus {{{}}} is non empty;
assume {} in {{{}}};
hence contradiction by TARSKI:def 1;
end;
end;
registration
let A be non empty set;
cluster { A } -> with_non-empty_elements;
coherence
by TARSKI:def 1;
let B be non empty set;
cluster { A, B } -> with_non-empty_elements;
coherence
by TARSKI:def 2;
let C be non empty set;
cluster { A, B, C } -> with_non-empty_elements;
coherence
by ENUMSET1:def 1;
let D be non empty set;
cluster { A, B, C, D } -> with_non-empty_elements;
coherence
by ENUMSET1:def 2;
let E be non empty set;
cluster { A, B, C, D, E } -> with_non-empty_elements;
coherence
by ENUMSET1:def 3;
let F be non empty set;
cluster { A, B, C, D, E, F } -> with_non-empty_elements;
coherence
by ENUMSET1:def 4;
let G be non empty set;
cluster { A, B, C, D, E, F, G } -> with_non-empty_elements;
coherence
by ENUMSET1:def 5;
let H be non empty set;
cluster { A, B, C, D, E, F, G, H } -> with_non-empty_elements;
coherence
by ENUMSET1:def 6;
let I be non empty set;
cluster { A, B, C, D, E, F, G, H, I } -> with_non-empty_elements;
coherence
by ENUMSET1:def 7;
let J be non empty set;
cluster { A, B, C, D, E, F, G, H, I, J } -> with_non-empty_elements;
coherence
by ENUMSET1:def 8;
end;
registration
let A,B be with_non-empty_elements set;
cluster A \/ B -> with_non-empty_elements;
coherence
proof
( not {} in A)& not {} in B by Def8;
then not {} in A \/ B by XBOOLE_0:def 3;
hence thesis;
end;
end;
:: from LATTICE4
theorem
union Y c= Z & X in Y implies X c= Z
proof
assume that
A1: union Y c= Z and
A2: X in Y;
thus X c= Z
proof
let x be object;
assume x in X;
then x in union Y by A2,TARSKI:def 4;
hence thesis by A1;
end;
end;
:: from LOPCLSET
theorem
for A,B,X being set holds ( X c= union (A \/ B) & for Y being set st Y
in B holds Y misses X ) implies X c= union A
proof
let A,B,X be set;
assume X c= union (A \/ B);
then X c= union (A \/ B) /\ X by XBOOLE_1:19;
then X c= (union A \/ union B) /\ X by ZFMISC_1:78;
then
A1: X c= (union A /\ X) \/ (union B /\ X) by XBOOLE_1:23;
assume for Y st Y in B holds Y misses X;
then union B misses X by ZFMISC_1:80;
then
A2: union B /\ X = {};
union A /\ X c= union A by XBOOLE_1:17;
hence thesis by A2,A1;
end;
:: from CANTOR_1
definition
let M be set;
let B be Subset-Family of M;
func Intersect B -> Subset of M equals
:Def9:
meet B if B <> {} otherwise M;
coherence
proof
M c= M;
hence thesis;
end;
consistency;
end;
theorem Th43:
for X, x being set, 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
proof
let X, x be set, R be Subset-Family of X;
assume
A1: x in X;
hereby
assume
A2: x in Intersect R;
let Y be set;
assume
A3: Y in R;
then Intersect R = meet R by Def9;
hence x in Y by A2,A3,Def1;
end;
assume
A4: for Y being set st Y in R holds x in Y;
per cases;
suppose
A5: R <> {};
then x in meet R by A4,Def1;
hence thesis by A5,Def9;
end;
suppose
R = {};
hence thesis by A1,Def9;
end;
end;
theorem
for X being set for H, J being Subset-Family of X st H c= J holds
Intersect J c= Intersect H
proof
let X be set;
let H, J be Subset-Family of X such that
A1: H c= J;
let x be object;
assume
A2: x in Intersect J;
then for Y be set st Y in H holds x in Y by A1,Th43;
hence thesis by A2,Th43;
end;
:: 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 by Def8;
end;
:: from ABIAN, 2005.08.22, A.T
reserve E for set;
definition
let E;
attr E is empty-membered means
:Def10:
not ex x being non empty set st x in E;
end;
notation
let E;
antonym E is with_non-empty_element for E is empty-membered;
end;
registration
cluster with_non-empty_element for set;
existence
proof
take {{{}}}, {{}};
thus thesis by TARSKI:def 1;
end;
end;
registration
cluster with_non-empty_element -> non empty for set;
coherence;
end;
:: from TRIANG_1, 2005.08.22
registration
let X be with_non-empty_element set;
cluster non empty for Element of X;
existence
proof
ex x being non empty set st x in X by Def10;
hence thesis;
end;
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
proof
set d = the Element of D;
d c= union D by ZFMISC_1:74;
hence thesis;
end;
end;
:: missing, 2007.03.09, A.T.
registration
cluster non empty with_non-empty_elements -> with_non-empty_element for set;
coherence;
end;
:: the concept of a cover, 2008.03.08, A.T.
definition
let X be set;
mode Cover of X -> set means
:Def11:
X c= union it;
existence
proof
take {X};
thus thesis by ZFMISC_1:25;
end;
end;
theorem
for X being set, F being Subset-Family of X holds F is Cover of X iff
union F = X
by Def11;
:: from MEASURE1, 2008.06.08, A.T.
theorem Th46:
{{}} is Subset-Family of X
proof
{} c= X;
hence thesis by ZFMISC_1:31;
end;
:: from BORSUK_5 (generalized), 2008.06.08, A.T.
definition
let X be set;
let F be Subset-Family of X;
attr F is with_proper_subsets means
:Def12:
not X in F;
end;
theorem
for TS being set, F, G being Subset-Family of TS st F is
with_proper_subsets & G c= F holds G is with_proper_subsets;
registration
let TS be non empty set;
cluster with_proper_subsets for Subset-Family of TS;
existence
proof
reconsider F = { {} } as Subset-Family of TS by Th46;
take F;
assume TS in F;
hence thesis by TARSKI:def 1;
end;
end;
theorem
for TS being non empty set, A, B being with_proper_subsets
Subset-Family of TS holds A \/ B is with_proper_subsets
proof
let TS be non empty set, A, B be with_proper_subsets Subset-Family of TS;
assume TS in A \/ B;
then TS in A or TS in B by XBOOLE_0:def 3;
hence thesis by Def12;
end;
:: from YELLOW21, 2008.09.10, A.T.
registration
cluster non trivial -> with_non-empty_element for set;
coherence
proof
let W be set;
assume W is non trivial;
then consider w1,w2 being object such that
A1: w1 in W & w2 in W and
A2: w1 <> w2 by ZFMISC_1:def 10;
w1 <> {} or w2 <> {} by A2;
hence thesis by A1;
end;
end;
:: from PCOMPS_1, 2010.02.26, A.T.
definition
let X be set;
redefine func bool X -> Subset-Family of X;
coherence by ZFMISC_1:def 1;
end;
:: from HAHNBAN, 2011.04.26., A.T.
theorem
for A being non empty set, b being object st A <> {b}
ex a being Element of A st a <> b
proof
let A be non empty set, b be object such that
A1: A <> {b};
assume
A2: for a being Element of A holds a = b;
now
set a0 = the Element of A;
let a be object;
thus a in A implies a = b by A2;
assume
A3: a = b;
a0 = b by A2;
hence a in A by A3;
end;
hence contradiction by A1,TARSKI:def 1;
end;