Theorem
-------
If x and y are sets and xy is the Cartesian product of x and y, then
~EXIST(a):EXIST(b):(a,b) e xy <=> ~EXIST(a):a e x | ~EXIST(a):a e y
Note: This proof was written with the aid of DC Proof 2.0. Download at http://www.dcproof.com
Notation
--------
~ = NOT-operator
& = AND-operator
| = OR-operator
=> = IMPLIES-operator
<=> = IF-AND-ONLY-IF-operator
ALL = Universal quantifier
EXIST = Existential quantifier
Set = "is a set" predicate
Set' = "is a set of ordered pairs" predicate
Let x be a set
1 Set(x)
Axiom
Let y be a set
2 Set(y)
Axiom
Construct the Cartesian product of x and y
3 ALL(a1):ALL(a2):[Set(a1) & Set(a2) => EXIST(b):[Set'(b) & ALL(c1):ALL(c2):[(c1,c2) e b <=> c1 e a1 & c2 e a2]]]
Cart Prod
Apply Universal Specification
4 ALL(a2):[Set(x) & Set(a2) => EXIST(b):[Set'(b) & ALL(c1):ALL(c2):[(c1,c2) e b <=> c1 e x & c2 e a2]]]
U Spec, 3
5 Set(x) & Set(y) => EXIST(b):[Set'(b) & ALL(c1):ALL(c2):[(c1,c2) e b <=> c1 e x & c2 e y]]
U Spec, 4
Join lines 1 and 2
6 Set(x) & Set(y)
Join, 1, 2
Apply Detachment Rule
7 EXIST(b):[Set'(b) & ALL(c1):ALL(c2):[(c1,c2) e b <=> c1 e x & c2 e y]]
Detach, 5, 6
Define: xy, the Cartesian product of x and y
8 Set'(xy) & ALL(c1):ALL(c2):[(c1,c2) e xy <=> c1 e x & c2 e y]
E Spec, 7
xy is a set of ordered pairs
9 Set'(xy)
Split, 8
10 ALL(c1):ALL(c2):[(c1,c2) e xy <=> c1 e x & c2 e y]
Split, 8
Proof
-----
'=>'
Prove: ~EXIST(a):EXIST(b):(a,b) e xy
=> ~EXIST(a):a e x | ~EXIST(a):a e y
Suppose...
11 ~EXIST(a):EXIST(b):(a,b) e xy
Premise
Prove: ~EXIST(a):a e x | ~EXIST(a):a e y
Suppose to contrary...
12 ~[~EXIST(a):a e x | ~EXIST(a):a e y]
Premise
Apply De Morgan's Law
13 ~~[~~EXIST(a):a e x & ~~EXIST(a):a e y]
DeMorgan, 12
14 ~~EXIST(a):a e x & ~~EXIST(a):a e y
Rem DNeg, 13
15 EXIST(a):a e x & ~~EXIST(a):a e y
Rem DNeg, 14
16 EXIST(a):a e x & EXIST(a):a e y
Rem DNeg, 15
17 EXIST(a):a e x
Split, 16
18 EXIST(a):a e y
Split, 16
Define: p
19 p e x
E Spec, 17
Define: q
20 q e y
E Spec, 18
Apply definition of xy
21 ALL(c2):[(p,c2) e xy <=> p e x & c2 e y]
U Spec, 10
22 (p,q) e xy <=> p e x & q e y
U Spec, 21
23 [(p,q) e xy => p e x & q e y]
& [p e x & q e y => (p,q) e xy]
Iff-And, 22
24 (p,q) e xy => p e x & q e y
Split, 23
25 p e x & q e y => (p,q) e xy
Split, 23
26 p e x & q e y
Join, 19, 20
27 (p,q) e xy
Detach, 25, 26
Apply Existential Generalization
28 EXIST(b):(p,b) e xy
E Gen, 27
29 EXIST(a):EXIST(b):(a,b) e xy
E Gen, 28
Obtain the contradiction...
30 EXIST(a):EXIST(b):(a,b) e xy
& ~EXIST(a):EXIST(b):(a,b) e xy
Join, 29, 11
Apply Conclusion Rule
31 ~~[~EXIST(a):a e x | ~EXIST(a):a e y]
4 Conclusion, 12
As Required:
32 ~EXIST(a):a e x | ~EXIST(a):a e y
Rem DNeg, 31
'=>'
As Required:
33 ~EXIST(a):EXIST(b):(a,b) e xy
=> ~EXIST(a):a e x | ~EXIST(a):a e y
4 Conclusion, 11
'<='
Prove: ~EXIST(a):a e x | ~EXIST(a):a e y
=> ~EXIST(a):EXIST(b):(a,b) e xy
Suppose...
34 ~EXIST(a):a e x | ~EXIST(a):a e y
Premise
Case 1
Prove: ~EXIST(a):a e x => ~EXIST(a):EXIST(b):(a,b) e xy
Suppose...
35 ~EXIST(a):a e x
Premise
Prove: ~EXIST(a):EXIST(b):(a,b) e xy
Suppose to the contrary...
36 (p,q) e xy
Premise
Apply definition of xy
37 ALL(c2):[(p,c2) e xy <=> p e x & c2 e y]
U Spec, 10
38 (p,q) e xy <=> p e x & q e y
U Spec, 37
39 [(p,q) e xy => p e x & q e y]
& [p e x & q e y => (p,q) e xy]
Iff-And, 38
40 (p,q) e xy => p e x & q e y
Split, 39
41 p e x & q e y => (p,q) e xy
Split, 39
42 p e x & q e y
Detach, 40, 36
43 p e x
Split, 42
44 q e y
Split, 42
Apply Existential Generalization
45 EXIST(a):a e x
E Gen, 43
Obtain the contradiction...
46 EXIST(a):a e x & ~EXIST(a):a e x
Join, 45, 35
As Required:
47 ~EXIST(a):EXIST(b):(a,b) e xy
4 Conclusion, 36
Case 1
As Required:
48 ~EXIST(a):a e x => ~EXIST(a):EXIST(b):(a,b) e xy
4 Conclusion, 35
Case 2
Prove: ~EXIST(a):a e y => ~EXIST(a):EXIST(b):(a,b) e xy
Suppose...
49 ~EXIST(a):a e y
Premise
Prove: ~EXIST(a):EXIST(b):(a,b) e xy
Suppose to the contrary...
50 (p,q) e xy
Premise
Apply definition of xy
51 ALL(c2):[(p,c2) e xy <=> p e x & c2 e y]
U Spec, 10
52 (p,q) e xy <=> p e x & q e y
U Spec, 51
53 [(p,q) e xy => p e x & q e y]
& [p e x & q e y => (p,q) e xy]
Iff-And, 52
54 (p,q) e xy => p e x & q e y
Split, 53
55 p e x & q e y => (p,q) e xy
Split, 53
56 p e x & q e y
Detach, 54, 50
57 p e x
Split, 56
58 q e y
Split, 56
Apply Existential Generalization
59 EXIST(a):a e y
E Gen, 58
Obtain the contradiction...
60 EXIST(a):a e y & ~EXIST(a):a e y
Join, 59, 49
As Required:
61 ~EXIST(a):EXIST(b):(a,b) e xy
4 Conclusion, 50
Case 2
As Required:
62 ~EXIST(a):a e y => ~EXIST(a):EXIST(b):(a,b) e xy
4 Conclusion, 49
Join previous results
63 [~EXIST(a):a e x => ~EXIST(a):EXIST(b):(a,b) e xy]
& [~EXIST(a):a e y => ~EXIST(a):EXIST(b):(a,b) e xy]
Join, 48, 62
Apply Cases Rule
64 ~EXIST(a):EXIST(b):(a,b) e xy
Cases, 34, 63
'<='
As Required:
65 ~EXIST(a):a e x | ~EXIST(a):a e y
=> ~EXIST(a):EXIST(b):(a,b) e xy
4 Conclusion, 34
Join previous results
66 [~EXIST(a):EXIST(b):(a,b) e xy
=> ~EXIST(a):a e x | ~EXIST(a):a e y]
& [~EXIST(a):a e x | ~EXIST(a):a e y
=> ~EXIST(a):EXIST(b):(a,b) e xy]
Join, 33, 65
Apply Iff-And Rule
As Required:
67 ~EXIST(a):EXIST(b):(a,b) e xy
<=> ~EXIST(a):a e x | ~EXIST(a):a e y
Iff-And, 66