THEOREM
*******
For any set x and proposition
P, EXIST(a):[a e x => P]]
is always true.
ALL(a):[Set(x) => EXIST(a):[a e x => P]]
Dan Christensen
2023-04-24
PROOF
*****
Lemma: From Russel's Paradox (Proof: http://dcproof.com/UniversalSet.htm)
1 ALL(a):[Set(a) =>
EXIST(b):~b e a]
Axiom
Let x be a set
2 Set(x)
Premise
Apply lemma
3 Set(x) => EXIST(b):~b e x
U Spec, 1
4 EXIST(b):~b e x
Detach, 3, 2
5 ~y e x
E Spec, 4
6 ~y e x | P
Arb Or, 5
7 ~~y e x => P
Imply-Or, 6
8 y e x => P
Rem DNeg, 7
As Required:
9 ALL(a):[Set(x) =>
EXIST(a):[a e x => P]]
4 Conclusion, 2