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

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

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

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