Theorem
-------
ALL(a):[a e u => P(a)] & EXIST(b):Q(b)
<=> ALL(a):[a e u => EXIST(b):[P(a) & Q(b)]]
where u is a non-empty set.
By Dan Christensen
Axiom
-----
Let u be a non-empty set, the domain of quantification here.
1 EXIST(a):a e u
Axiom
Proof
-----
'=>'
Prove: ALL(a):[a e u => P(a)] & EXIST(b):Q(b)
=> ALL(a):[a e u => EXIST(b):[P(a) & Q(b)]]
Suppose...
2 ALL(a):[a e u => P(a)] & EXIST(b):Q(b)
Premise
Splitting this premise...
3 ALL(a):[a e u => P(a)]
Split, 2
4 EXIST(b):Q(b)
Split, 2
Prove: ALL(a):[a e u => EXIST(b):[P(a) & Q(b)]]
Suppose...
5 x e u
Premise
Apply premise
6 x e u => P(x)
U Spec, 3
7 P(x)
Detach, 6, 5
Let y be such that...
8 Q(y)
E Spec, 4
Joining results...
9 P(x) & Q(y)
Join, 7, 8
Apply existential generalization on y
10 EXIST(b):[P(x) & Q(b)]
E Gen, 9
As Required:
11 ALL(a):[a e u => EXIST(b):[P(a) & Q(b)]]
4 Conclusion, 5
As Required:
12 ALL(a):[a e u => P(a)] & EXIST(b):Q(b)
=> ALL(a):[a e u => EXIST(b):[P(a) & Q(b)]]
4 Conclusion, 2
'<='
Prove: ALL(a):[a e u => EXIST(b):[P(a) & Q(b)]]
=> ALL(a):[a e u => P(a)] & EXIST(b):Q(b)
Suppose...
13 ALL(a):[a e u => EXIST(b):[P(a) & Q(b)]]
Premise
Prove: ALL(a):[a e u => P(a)]
Suppose...
14 v e u
Premise
Apply premise
15 v e u => EXIST(b):[P(v) & Q(b)]
U Spec, 13
16 EXIST(b):[P(v) & Q(b)]
Detach, 15, 14
17 P(v) & Q(w)
E Spec, 16
18 P(v)
Split, 17
As Required:
19 ALL(a):[a e u => P(a)]
4 Conclusion, 14
Prove: EXIST(b):Q(b)
Apply axiom
20 z e u
E Spec, 1
Apply premise
21 z e u => EXIST(b):[P(z) & Q(b)]
U Spec, 13
22 EXIST(b):[P(z) & Q(b)]
Detach, 21, 20
23 P(z) & Q(t)
E Spec, 22
24 P(z)
Split, 23
25 Q(t)
Split, 23
Apply existential generalization
As Required:
26 EXIST(b):Q(b)
E Gen, 25
Joining results...
27 ALL(a):[a e u => P(a)] & EXIST(b):Q(b)
Join, 19, 26
As Required:
28 ALL(a):[a e u => EXIST(b):[P(a) & Q(b)]]
=> ALL(a):[a e u => P(a)] & EXIST(b):Q(b)
4 Conclusion, 13
Joining results...
29 [ALL(a):[a e u => P(a)] & EXIST(b):Q(b)
=> ALL(a):[a e u => EXIST(b):[P(a) & Q(b)]]]
& [ALL(a):[a e u => EXIST(b):[P(a) & Q(b)]]
=> ALL(a):[a e u => P(a)] & EXIST(b):Q(b)]
Join, 12, 28
As Required:
30 ALL(a):[a e u => P(a)] & EXIST(b):Q(b)
<=> ALL(a):[a e u => EXIST(b):[P(a) & Q(b)]]
Iff-And, 29