THEOREM
*******
For any family of sets there
exists a union and intersection of that family. If that family is empty, then
so are its union and intersection.
ALL(fam):[Set(fam)
& ALL(a):[a e fam => Set(a)]
=> EXIST(ufam):EXIST(ifam):[Set(ufam) & ALL(b):[b e ufam <=> EXIST(c):[c e fam & b e c]]
& [Set(ifam) & ALL(a):[a e ifam <=> a e ufam & ALL(b):[b e fam => a e b]]]
& [ALL(a):~a e fam => ALL(a):~a e ufam & ALL(a):~a e ifam]]]
Where
fam = family of sets
(possibly empty)
ufam
= union of f
ifam
= intersection of f
This proof makes use of basic
set theory: Arbitrary Union Axiom (line 4), Subset Axiom (line 10)
By Dan Christensen
2024-06-06
2024-06-14
Let fam be a family of sets (possibly
empty)
1 Set(fam) &
ALL(a):[a e fam => Set(a)]
Premise
2 Set(fam)
Split, 1
3 ALL(a):[a e fam => Set(a)]
Split, 1
Construct ufam (union of fam)
Apply Union Axiom
4 ALL(f):[Set(f) &
ALL(a):[a e f => Set(a)]
=>
EXIST(a):[Set(a) & ALL(b):[b e a <=> EXIST(c):[c e f & b e c]]]]
Arb Union
Define: ufam (union of fam)
7 Set(ufam) &
ALL(b):[b e ufam <=>
EXIST(c):[c e fam & b e c]]
E Spec, 6
8 Set(ufam)
Split, 7
9 ALL(b):[b e ufam <=>
EXIST(c):[c e fam & b e c]]
Split, 7
Construct ifam (intersection of
fam)
Apply Subset Axiom
10 EXIST(sub):[Set(sub) & ALL(a):[a e sub <=> a e ufam & ALL(b):[b e fam => a e b]]]
Subset, 8
Define: ifam (intersection of
fam)
11 Set(ifam) &
ALL(a):[a e ifam <=> a e ufam & ALL(b):[b e fam => a e b]]
E Spec, 10
12 Set(ifam)
Split, 11
13 ALL(a):[a e ifam <=> a e ufam & ALL(b):[b e fam => a e b]]
Split, 11
Prove: ALL(a):~a e fam => ALL(a):~a e fam &
ALL(a):~a e ufam
Suppose...
14 ALL(a):~a e fam
Premise
Prove: ~EXIST(a):a e ufam
Suppose to the contrary...
15 x e ufam
Premise
20 y e fam & x e y
E Spec, 19
21 y e fam
Split, 20
As Required:
24 ~EXIST(a):a e ufam
4 Conclusion, 15
ufam (the
union of fam) is empty
26 ALL(a):~a e ufam
Rem DNeg, 25
Prove: ~EXIST(a):a e ifam
Suppose to the contrary...
27 x e ifam
Premise
As Required:
35 ~EXIST(a):a e ifam
4 Conclusion, 27
ifam (the
intersection of fam) is empty
37 ALL(a):~a e ifam
Rem DNeg, 36
As Required:
39 ALL(a):~a e fam
=>
ALL(a):~a e ufam & ALL(a):~a e ifam
4 Conclusion, 14
As Required:
42 ALL(fam):[Set(fam) & ALL(a):[a e fam => Set(a)]
=>
EXIST(ufam):EXIST(ifam):[Set(ufam) & ALL(b):[b e ufam <=>
EXIST(c):[c e fam & b e c]]
&
[Set(ifam) & ALL(a):[a e ifam <=> a e ufam & ALL(b):[b e fam => a e b]]]
&
[ALL(a):~a e fam
=>
ALL(a):~a e ufam & ALL(a):~a e ifam]]]
4 Conclusion, 1