Induction Independent of Other Axioms

THEOREM

*******

Let x be an infinte set. There exists a subset n of x, n0 e n, n1 e n, and functions f: n --> n and g: n --> n such that (n,f,n0) satisfies each Peano axiom including induction, and (n,g,n1) satisfies each Peano axiom BUT induction.

In this sense, induction is independent of the other Peano axioms.

PROOF SKETCH

************

Apply a previous result to obtain a set n equivalent to the set of natural numbers {0, 1, 2, ...} with successor function f. Then construct the function g: n --> n such that: g(0)=0, g(1)=2, g(2)=3, g(3)=4 or equivalently, for all x in n, we have:

g(x) = {0 if x=0

{f(x) otherwise

Then each of the Peano axioms BUT induction will hold on n if we use 1 as the "first" element.

Lines

-----

3-7       Apply previous result that in any infite set x, there exists a subset n of x,
          a function f: n --> n and element x0 e n such that (n,f,x0) satisfy the Peano
          axioms (PA1-5)

8-9 Define n

10 Define x0

11 Define f: n --> n

14-21 Construct and define n2, the set of ordered pairs of n

22-25 Construct and define subset g of n2

26-42 Prove (x0,x0) e g

43-65 Prove (x,f(x)) e g for x not equal x0

66-190 Prove g is a function

191-204 PA2: g is closed on n

205-245 Prove: g(x) = {x0 if x=x0

{f(x) otherwise

246-306 PA3: g is injective on n

307-336 PA4: f(x0) has no pre-image in n under g

337-338 PA1: f(x0) e n

338-410 ~PA5: Induction does not hold on n for successor function g and "first" element f(x0)

411-432 Generalizing

This formal proof with written and machine-verified with the aid of the authors DC Proof 2.0 software available at http://www.dcproof.com

PREVIOUS RESULT

***************

Let x be an infinte set. There exists a subset n of x, function f: n --> n and "first" element x0 that satisfies all the Peano axioms, including induction. (Proof)

1 ALL(x):[Set(x) & Infinite(x)

=> EXIST(n):EXIST(f):EXIST(x0):[Set(n) & ALL(a):[a e n => a e x] & x0 e n

& ALL(a):[a e n => f(a) e n]

& ALL(a):ALL(b):[a e n & b e n => [f(a)=f(b) => a=b]]

& ALL(a):[a e n => ~f(a)=x0]

& ALL(a):[Set(a) & ALL(b):[b e a => b e n]

=> [x0 e a & ALL(b):[b e a => f(b) e a]

=> ALL(b):[b e n => b e a]]]]]

Axiom

PROOF

*****

Suppose x is an infinite set

2 Set(x) & Infinite(x)

Premise

Apply previous result

3 Set(x) & Infinite(x)

=> EXIST(n):EXIST(f):EXIST(x0):[Set(n) & ALL(a):[a e n => a e x] & x0 e n

& ALL(a):[a e n => f(a) e n]

& ALL(a):ALL(b):[a e n & b e n => [f(a)=f(b) => a=b]]

& ALL(a):[a e n => ~f(a)=x0]

& ALL(a):[Set(a) & ALL(b):[b e a => b e n]

=> [x0 e a & ALL(b):[b e a => f(b) e a]

=> ALL(b):[b e n => b e a]]]]

U Spec, 1

4 EXIST(n):EXIST(f):EXIST(x0):[Set(n) & ALL(a):[a e n => a e x] & x0 e n

& ALL(a):[a e n => f(a) e n]

& ALL(a):ALL(b):[a e n & b e n => [f(a)=f(b) => a=b]]

& ALL(a):[a e n => ~f(a)=x0]

& ALL(a):[Set(a) & ALL(b):[b e a => b e n]

=> [x0 e a & ALL(b):[b e a => f(b) e a]

=> ALL(b):[b e n => b e a]]]]

Detach, 3, 2

5 EXIST(f):EXIST(x0):[Set(n) & ALL(a):[a e n => a e x] & x0 e n

& ALL(a):[a e n => f(a) e n]

& ALL(a):ALL(b):[a e n & b e n => [f(a)=f(b) => a=b]]

& ALL(a):[a e n => ~f(a)=x0]

& ALL(a):[Set(a) & ALL(b):[b e a => b e n]

=> [x0 e a & ALL(b):[b e a => f(b) e a]

=> ALL(b):[b e n => b e a]]]]

E Spec, 4

6 EXIST(x0):[Set(n) & ALL(a):[a e n => a e x] & x0 e n

& ALL(a):[a e n => f(a) e n]

& ALL(a):ALL(b):[a e n & b e n => [f(a)=f(b) => a=b]]

& ALL(a):[a e n => ~f(a)=x0]

& ALL(a):[Set(a) & ALL(b):[b e a => b e n]

=> [x0 e a & ALL(b):[b e a => f(b) e a]

=> ALL(b):[b e n => b e a]]]]

E Spec, 5

7 Set(n) & ALL(a):[a e n => a e x] & x0 e n

& ALL(a):[a e n => f(a) e n]

& ALL(a):ALL(b):[a e n & b e n => [f(a)=f(b) => a=b]]

& ALL(a):[a e n => ~f(a)=x0]

& ALL(a):[Set(a) & ALL(b):[b e a => b e n]

=> [x0 e a & ALL(b):[b e a => f(b) e a]

=> ALL(b):[b e n => b e a]]]

E Spec, 6

Define: n

8 Set(n)

Split, 7

9 ALL(a):[a e n => a e x]

Split, 7

Define: x0

10 x0 e n

Split, 7

Define: f

11 ALL(a):[a e n => f(a) e n]

Split, 7

f is injective

12 ALL(a):ALL(b):[a e n & b e n => [f(a)=f(b) => a=b]]

Split, 7

x0 has no pre-image under f

13 ALL(a):[a e n => ~f(a)=x0]

Split, 7

14 ALL(a):[Set(a) & ALL(b):[b e a => b e n]

=> [x0 e a & ALL(b):[b e a => f(b) e a]

=> ALL(b):[b e n => b e a]]]

Split, 7

Construct the set n2 of ordered pairs of natural numbers.

Apply the Cartesian Product Axiom

15 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

16 ALL(a2):[Set(n) & Set(a2) => EXIST(b):[Set'(b) & ALL(c1):ALL(c2):[(c1,c2) e b
<=> c1 e n & c2 e a2]]]

U Spec, 15

17 Set(n) & Set(n) => EXIST(b):[Set'(b) & ALL(c1):ALL(c2):[(c1,c2) e b <=> c1 e n & c2 e n]]

U Spec, 16

18 Set(n) & Set(n)

Join, 8, 8

19 EXIST(b):[Set'(b) & ALL(c1):ALL(c2):[(c1,c2) e b <=> c1 e n & c2 e n]]

Detach, 17, 18

20 Set'(n2) & ALL(c1):ALL(c2):[(c1,c2) e n2 <=> c1 e n & c2 e n]

E Spec, 19

Define: n2

21 Set'(n2)

Split, 20

22 ALL(c1):ALL(c2):[(c1,c2) e n2 <=> c1 e n & c2 e n]

Split, 20

The the subset g of n2

Apply the Subset Axiom

23 EXIST(sub):[Set'(sub) & ALL(a):ALL(b):[(a,b) e sub <=> (a,b) e n2
& [a=x0 & b=x0 | ~a=x0 & b=f(a)]]]

Subset, 21

24 Set'(g) & ALL(a):ALL(b):[(a,b) e g <=> (a,b) e n2 & [a=x0 & b=x0 | ~a=x0 & b=f(a)]]

E Spec, 23

Define: g

We will show that g is a function such that: g(x) = {x0 for x = x0

{f(x) otherwise

25 Set'(g)

Split, 24

26 ALL(a):ALL(b):[(a,b) e g <=> (a,b) e n2 & [a=x0 & b=x0 | ~a=x0 & b=f(a)]]

Split, 24

Prove: (x0,x0) e g

Apply definition of g

27 ALL(b):[(x0,b) e g <=> (x0,b) e n2 & [x0=x0 & b=x0 | ~x0=x0 & b=f(x0)]]

U Spec, 26

28 (x0,x0) e g <=> (x0,x0) e n2 & [x0=x0 & x0=x0 | ~x0=x0 & x0=f(x0)]

U Spec, 27

29 [(x0,x0) e g => (x0,x0) e n2 & [x0=x0 & x0=x0 | ~x0=x0 & x0=f(x0)]]

& [(x0,x0) e n2 & [x0=x0 & x0=x0 | ~x0=x0 & x0=f(x0)] => (x0,x0) e g]

Iff-And, 28

30 (x0,x0) e g => (x0,x0) e n2 & [x0=x0 & x0=x0 | ~x0=x0 & x0=f(x0)]

Split, 29

Sufficient: (x0,x0) e g

31 (x0,x0) e n2 & [x0=x0 & x0=x0 | ~x0=x0 & x0=f(x0)] => (x0,x0) e g

Split, 29

Apply definition of n2

32 ALL(c2):[(x0,c2) e n2 <=> x0 e n & c2 e n]

U Spec, 22

33 (x0,x0) e n2 <=> x0 e n & x0 e n

U Spec, 32

34 [(x0,x0) e n2 => x0 e n & x0 e n]

& [x0 e n & x0 e n => (x0,x0) e n2]

Iff-And, 33

35 (x0,x0) e n2 => x0 e n & x0 e n

Split, 34

36 x0 e n & x0 e n => (x0,x0) e n2

Split, 34

37 x0 e n & x0 e n

Join, 10, 10

38 (x0,x0) e n2

Detach, 36, 37

39 x0=x0

Reflex

40 x0=x0 & x0=x0

Join, 39, 39

41 x0=x0 & x0=x0 | ~x0=x0 & x0=f(x0)

Arb Or, 40

42 (x0,x0) e n2 & [x0=x0 & x0=x0 | ~x0=x0 & x0=f(x0)]

Join, 38, 41

As Required:

43 (x0,x0) e g

Detach, 31, 42

Prove: ALL(a):[a e n & ~a=x0 => (a,f(a)) e g]

Suppose...

44 t e n & ~t=x0

Premise

45 t e n

Split, 44

46 ~t=x0

Split, 44

Apply defintion of g

47 ALL(b):[(t,b) e g <=> (t,b) e n2 & [t=x0 & b=x0 | ~t=x0 & b=f(t)]]

U Spec, 26

48 (t,f(t)) e g <=> (t,f(t)) e n2 & [t=x0 & f(t)=x0 | ~t=x0 & f(t)=f(t)]

U Spec, 47

49 [(t,f(t)) e g => (t,f(t)) e n2 & [t=x0 & f(t)=x0 | ~t=x0 & f(t)=f(t)]]

& [(t,f(t)) e n2 & [t=x0 & f(t)=x0 | ~t=x0 & f(t)=f(t)] => (t,f(t)) e g]

Iff-And, 48

50 (t,f(t)) e g => (t,f(t)) e n2 & [t=x0 & f(t)=x0 | ~t=x0 & f(t)=f(t)]

Split, 49

Sufficient: For (t,f(t)) e g

51 (t,f(t)) e n2 & [t=x0 & f(t)=x0 | ~t=x0 & f(t)=f(t)] => (t,f(t)) e g

Split, 49

Apply definition of n2

52 ALL(c2):[(t,c2) e n2 <=> t e n & c2 e n]

U Spec, 22

53 (t,f(t)) e n2 <=> t e n & f(t) e n

U Spec, 52

54 [(t,f(t)) e n2 => t e n & f(t) e n]

& [t e n & f(t) e n => (t,f(t)) e n2]

Iff-And, 53

55 (t,f(t)) e n2 => t e n & f(t) e n

Split, 54

56 t e n & f(t) e n => (t,f(t)) e n2

Split, 54

57 t e n => f(t) e n

U Spec, 11

58 f(t) e n

Detach, 57, 45

59 t e n & f(t) e n

Join, 45, 58

60 (t,f(t)) e n2

Detach, 56, 59

61 f(t)=f(t)

Reflex

62 ~t=x0 & f(t)=f(t)

Join, 46, 61

63 t=x0 & f(t)=x0 | ~t=x0 & f(t)=f(t)

Arb Or, 62

64 (t,f(t)) e n2

& [t=x0 & f(t)=x0 | ~t=x0 & f(t)=f(t)]

Join, 60, 63

65 (t,f(t)) e g

Detach, 51, 64

As Required:

66 ALL(a):[a e n & ~a=x0 => (a,f(a)) e g]

4 Conclusion, 44

Prove: g is a function mapping n to itself

Apply Function Axiom

67 ALL(f):ALL(a):ALL(b):[ALL(c):ALL(d):[(c,d) e f => c e a & d e b]

& ALL(c):[c e a => EXIST(d):[d e b & (c,d) e f]]

& ALL(c):ALL(d1):ALL(d2):[(c,d1) e f & (c,d2) e f => d1=d2]

=> ALL(c):ALL(d):[d=f(c) <=> (c,d) e f]]

Function

68 ALL(a):ALL(b):[ALL(c):ALL(d):[(c,d) e g => c e a & d e b]

& ALL(c):[c e a => EXIST(d):[d e b & (c,d) e g]]

& ALL(c):ALL(d1):ALL(d2):[(c,d1) e g & (c,d2) e g => d1=d2]

=> ALL(c):ALL(d):[d=g(c) <=> (c,d) e g]]

U Spec, 67

69 ALL(b):[ALL(c):ALL(d):[(c,d) e g => c e n & d e b]

& ALL(c):[c e n => EXIST(d):[d e b & (c,d) e g]]

& ALL(c):ALL(d1):ALL(d2):[(c,d1) e g & (c,d2) e g => d1=d2]

=> ALL(c):ALL(d):[d=g(c) <=> (c,d) e g]]

U Spec, 68

Sufficient: For functionality of g

70 ALL(c):ALL(d):[(c,d) e g => c e n & d e n]

& ALL(c):[c e n => EXIST(d):[d e n & (c,d) e g]]

& ALL(c):ALL(d1):ALL(d2):[(c,d1) e g & (c,d2) e g => d1=d2]

=> ALL(c):ALL(d):[d=g(c) <=> (c,d) e g]

U Spec, 69

Prove: ALL(c):ALL(d):[(c,d) e g => c e n & d e n]

Suppose...

71 (u,v) e g

Premise

Apply definition of g

72 ALL(b):[(u,b) e g <=> (u,b) e n2 & [u=x0 & b=x0 | ~u=x0 & b=f(u)]]

U Spec, 26

73 (u,v) e g <=> (u,v) e n2 & [u=x0 & v=x0 | ~u=x0 & v=f(u)]

U Spec, 72

74 [(u,v) e g => (u,v) e n2 & [u=x0 & v=x0 | ~u=x0 & v=f(u)]]

& [(u,v) e n2 & [u=x0 & v=x0 | ~u=x0 & v=f(u)] => (u,v) e g]

Iff-And, 73

75 (u,v) e g => (u,v) e n2 & [u=x0 & v=x0 | ~u=x0 & v=f(u)]

Split, 74

76 (u,v) e n2 & [u=x0 & v=x0 | ~u=x0 & v=f(u)] => (u,v) e g

Split, 74

77 (u,v) e n2 & [u=x0 & v=x0 | ~u=x0 & v=f(u)]

Detach, 75, 71

78 (u,v) e n2

Split, 77

79 u=x0 & v=x0 | ~u=x0 & v=f(u)

Split, 77

Apply definition of n2

80 ALL(c2):[(u,c2) e n2 <=> u e n & c2 e n]

U Spec, 22

81 (u,v) e n2 <=> u e n & v e n

U Spec, 80

82 [(u,v) e n2 => u e n & v e n]

& [u e n & v e n => (u,v) e n2]

Iff-And, 81

83 (u,v) e n2 => u e n & v e n

Split, 82

84 u e n & v e n => (u,v) e n2

Split, 82

85 u e n & v e n

Detach, 83, 78

Functionality, Part 1

86 ALL(c):ALL(d):[(c,d) e g => c e n & d e n]

4 Conclusion, 71

Prove: ALL(c):[c e n => EXIST(d):[d e n & (c,d) e g]]

Suppose...

87 u e n

Premise

Two cases to consider:

88 u=x0 | ~u=x0

Or Not

Case 1

Prove: u=x0 => EXIST(d):[d e n & (u,d) e g]

Suppose...

89 u=x0

Premise

90 (u,x0) e g

Substitute, 89, 43

91 x0 e n & (u,x0) e g

Join, 10, 90

92 EXIST(d):[d e n & (u,d) e g]

E Gen, 91

Case 1

As Required:

93 u=x0 => EXIST(d):[d e n & (u,d) e g]

4 Conclusion, 89

Case 2

Prove: ~u=x0 => EXIST(d):[d e n & (u,d) e g]

Suppose...

94 ~u=x0

Premise

95 u e n & ~u=x0 => (u,f(u)) e g

U Spec, 66

96 u e n & ~u=x0

Join, 87, 94

97 (u,f(u)) e g

Detach, 95, 96

98 u e n => f(u) e n

U Spec, 11

99 f(u) e n

Detach, 98, 87

100 f(u) e n & (u,f(u)) e g

Join, 99, 97

101 EXIST(d):[d e n & (u,d) e g]

E Gen, 100

Case 2

As Required:

102 ~u=x0 => EXIST(d):[d e n & (u,d) e g]

4 Conclusion, 94

103 [u=x0 => EXIST(d):[d e n & (u,d) e g]]

& [~u=x0 => EXIST(d):[d e n & (u,d) e g]]

Join, 93, 102

104 EXIST(d):[d e n & (u,d) e g]

Cases, 88, 103

Functionality, Part 2

105 ALL(c):[c e n => EXIST(d):[d e n & (c,d) e g]]

4 Conclusion, 87

Prove: ALL(c):ALL(d1):ALL(d2):[(c,d1) e g & (c,d2) e g => d1=d2]

Suppose...

106 (u,v1) e g & (u,v2) e g

Premise

107 (u,v1) e g

Split, 106

108 (u,v2) e g

Split, 106

Apply definition of g

109 ALL(b):[(u,b) e g <=> (u,b) e n2 & [u=x0 & b=x0 | ~u=x0 & b=f(u)]]

U Spec, 26

110 (u,v1) e g <=> (u,v1) e n2 & [u=x0 & v1=x0 | ~u=x0 & v1=f(u)]

U Spec, 109

111 [(u,v1) e g => (u,v1) e n2 & [u=x0 & v1=x0 | ~u=x0 & v1=f(u)]]

& [(u,v1) e n2 & [u=x0 & v1=x0 | ~u=x0 & v1=f(u)] => (u,v1) e g]

Iff-And, 110

112 (u,v1) e g => (u,v1) e n2 & [u=x0 & v1=x0 | ~u=x0 & v1=f(u)]

Split, 111

113 (u,v1) e n2 & [u=x0 & v1=x0 | ~u=x0 & v1=f(u)] => (u,v1) e g

Split, 111

114 (u,v1) e n2 & [u=x0 & v1=x0 | ~u=x0 & v1=f(u)]

Detach, 112, 107

115 (u,v1) e n2

Split, 114

116 u=x0 & v1=x0 | ~u=x0 & v1=f(u)

Split, 114

Apply definition of n2

117 ALL(c2):[(u,c2) e n2 <=> u e n & c2 e n]

U Spec, 22

118 (u,v1) e n2 <=> u e n & v1 e n

U Spec, 117

119 [(u,v1) e n2 => u e n & v1 e n]

& [u e n & v1 e n => (u,v1) e n2]

Iff-And, 118

120 (u,v1) e n2 => u e n & v1 e n

Split, 119

121 u e n & v1 e n => (u,v1) e n2

Split, 119

122 u e n & v1 e n

Detach, 120, 115

123 u e n

Split, 122

124 v1 e n

Split, 122

Apply definition of g

125 (u,v2) e g <=> (u,v2) e n2 & [u=x0 & v2=x0 | ~u=x0 & v2=f(u)]

U Spec, 109

126 [(u,v2) e g => (u,v2) e n2 & [u=x0 & v2=x0 | ~u=x0 & v2=f(u)]]

& [(u,v2) e n2 & [u=x0 & v2=x0 | ~u=x0 & v2=f(u)] => (u,v2) e g]

Iff-And, 125

127 (u,v2) e g => (u,v2) e n2 & [u=x0 & v2=x0 | ~u=x0 & v2=f(u)]

Split, 126

128 (u,v2) e n2 & [u=x0 & v2=x0 | ~u=x0 & v2=f(u)] => (u,v2) e g

Split, 126

129 (u,v2) e n2 & [u=x0 & v2=x0 | ~u=x0 & v2=f(u)]

Detach, 127, 108

130 (u,v2) e n2

Split, 129

131 u=x0 & v2=x0 | ~u=x0 & v2=f(u)

Split, 129

Apply definition of n2

132 (u,v2) e n2 <=> u e n & v2 e n

U Spec, 117

133 [(u,v2) e n2 => u e n & v2 e n]

& [u e n & v2 e n => (u,v2) e n2]

Iff-And, 132

134 (u,v2) e n2 => u e n & v2 e n

Split, 133

135 u e n & v2 e n => (u,v2) e n2

Split, 133

136 u e n & v2 e n

Detach, 134, 130

137 u e n

Split, 136

138 v2 e n

Split, 136

Two cases to consider:

139 u=x0 | ~u=x0

Or Not

Case 1

Prove: u=x0 => v1=v2

Suppose...

140 u=x0

Premise

141 ~[u=x0 & v1=x0] => ~u=x0 & v1=f(u)

Imply-Or, 116

142 ~[~u=x0 & v1=f(u)] => ~~[u=x0 & v1=x0]

Contra, 141

143 ~[~u=x0 & v1=f(u)] => u=x0 & v1=x0

Rem DNeg, 142

Prove: ~[~u=x0 & v1=f(u)]

Suppose to the contrary...

144 ~u=x0 & v1=f(u)

Premise

145 ~u=x0

Split, 144

146 v1=f(u)

Split, 144

147 u=x0 & ~u=x0

Join, 140, 145

As Required:

148 ~[~u=x0 & v1=f(u)]

4 Conclusion, 144

149 u=x0 & v1=x0

Detach, 143, 148

150 u=x0

Split, 149

151 v1=x0

Split, 149

152 ~[u=x0 & v2=x0] => ~u=x0 & v2=f(u)

Imply-Or, 131

153 ~[~u=x0 & v2=f(u)] => ~~[u=x0 & v2=x0]

Contra, 152

154 ~[~u=x0 & v2=f(u)] => u=x0 & v2=x0

Rem DNeg, 153

Prove: ~[~u=x0 & v2=f(u)]

Suppose to the contrary...

155 ~u=x0 & v2=f(u)

Premise

156 ~u=x0

Split, 155

157 v2=f(u)

Split, 155

158 u=x0 & ~u=x0

Join, 140, 156

As Required:

159 ~[~u=x0 & v2=f(u)]

4 Conclusion, 155

160 u=x0 & v2=x0

Detach, 154, 159

161 u=x0

Split, 160

162 v2=x0

Split, 160

163 v1=v2

Substitute, 162, 151

Case 1

As Required:

164 u=x0 => v1=v2

4 Conclusion, 140

Case 2

Prove: ~u=x0 => v1=v2

Suppose...

165 ~u=x0

Premise

166 ~[u=x0 & v1=x0] => ~u=x0 & v1=f(u)

Imply-Or, 116

Prove: ~[u=x0 & v1=x0]

Suppose to the contrary...

167 u=x0 & v1=x0

Premise

168 u=x0

Split, 167

169 v1=x0

Split, 167

170 u=x0 & ~u=x0

Join, 168, 165

As Required:

171 ~[u=x0 & v1=x0]

4 Conclusion, 167

172 ~u=x0 & v1=f(u)

Detach, 166, 171

173 ~u=x0

Split, 172

174 v1=f(u)

Split, 172

175 ~[u=x0 & v2=x0] => ~u=x0 & v2=f(u)

Imply-Or, 131

Prove: ~[u=x0 & v2=x0]

Suppose to the contrary...

176 u=x0 & v2=x0

Premise

177 u=x0

Split, 176

178 v2=x0

Split, 176

179 u=x0 & ~u=x0

Join, 177, 165

As Required:

180 ~[u=x0 & v2=x0]

4 Conclusion, 176

181 ~u=x0 & v2=f(u)

Detach, 175, 180

182 ~u=x0

Split, 181

183 v2=f(u)

Split, 181

184 v1=v2

Substitute, 183, 174

Case 2

As Required:

185 ~u=x0 => v1=v2

4 Conclusion, 165

186 [u=x0 => v1=v2] & [~u=x0 => v1=v2]

Join, 164, 185

187 v1=v2

Cases, 139, 186

Functionality, Part 3

188 ALL(c):ALL(d1):ALL(d2):[(c,d1) e g & (c,d2) e g => d1=d2]

4 Conclusion, 106

Joining results...

189 ALL(c):ALL(d):[(c,d) e g => c e n & d e n]

& ALL(c):[c e n => EXIST(d):[d e n & (c,d) e g]]

Join, 86, 105

190 ALL(c):ALL(d):[(c,d) e g => c e n & d e n]

& ALL(c):[c e n => EXIST(d):[d e n & (c,d) e g]]

& ALL(c):ALL(d1):ALL(d2):[(c,d1) e g & (c,d2) e g => d1=d2]

Join, 189, 188

g is a function

As Required:

191 ALL(c):ALL(d):[d=g(c) <=> (c,d) e g]

Detach, 70, 190

Prove: ALL(a):[a e n => g(a) e n] (PA2)

Suppose...

192 u e n

Premise

193 u e n => EXIST(d):[d e n & (u,d) e g]

U Spec, 105

194 EXIST(d):[d e n & (u,d) e g]

Detach, 193, 192

195 v e n & (u,v) e g

E Spec, 194

196 v e n

Split, 195

197 (u,v) e g

Split, 195

198 ALL(d):[d=g(u) <=> (u,d) e g]

U Spec, 191

199 v=g(u) <=> (u,v) e g

U Spec, 198

200 [v=g(u) => (u,v) e g] & [(u,v) e g => v=g(u)]

Iff-And, 199

201 v=g(u) => (u,v) e g

Split, 200

202 (u,v) e g => v=g(u)

Split, 200

203 v=g(u)

Detach, 202, 197

204 g(u) e n

Substitute, 203, 196

PA2

***

205 ALL(a):[a e n => g(a) e n]

4 Conclusion, 192

Prove: ALL(a):[a e n => [a=x0 => g(a)=x0] & [~a=x0 => g(a)=f(a)]] (PA3)

Suppose...

206 u e n

Premise

Prove: u=x0 => g(u)=x0

Suppose...

207 u=x0

Premise

208 (u,x0) e g

Substitute, 207, 43

Apply functionality of g

209 ALL(d):[d=g(u) <=> (u,d) e g]

U Spec, 191

210 x0=g(u) <=> (u,x0) e g

U Spec, 209

211 [x0=g(u) => (u,x0) e g] & [(u,x0) e g => x0=g(u)]

Iff-And, 210

212 x0=g(u) => (u,x0) e g

Split, 211

213 (u,x0) e g => x0=g(u)

Split, 211

214 x0=g(u)

Detach, 213, 208

215 g(u)=x0

Sym, 214

As Required:

216 u=x0 => g(u)=x0

4 Conclusion, 207

Prove: ~u=x0 => g(u)=f(u)

Suppose...

217 ~u=x0

Premise

Apply definition of g

218 ALL(b):[(u,b) e g <=> (u,b) e n2 & [u=x0 & b=x0 | ~u=x0 & b=f(u)]]

U Spec, 26

219 (u,f(u)) e g <=> (u,f(u)) e n2 & [u=x0 & f(u)=x0 | ~u=x0 & f(u)=f(u)]

U Spec, 218

220 [(u,f(u)) e g => (u,f(u)) e n2 & [u=x0 & f(u)=x0 | ~u=x0 & f(u)=f(u)]]

& [(u,f(u)) e n2 & [u=x0 & f(u)=x0 | ~u=x0 & f(u)=f(u)] => (u,f(u)) e g]

Iff-And, 219

221 (u,f(u)) e g => (u,f(u)) e n2 & [u=x0 & f(u)=x0 | ~u=x0 & f(u)=f(u)]

Split, 220

222 (u,f(u)) e n2 & [u=x0 & f(u)=x0 | ~u=x0 & f(u)=f(u)] => (u,f(u)) e g

Split, 220

Apply definition of n2

223 ALL(c2):[(u,c2) e n2 <=> u e n & c2 e n]

U Spec, 22

224 (u,f(u)) e n2 <=> u e n & f(u) e n

U Spec, 223

225 [(u,f(u)) e n2 => u e n & f(u) e n]

& [u e n & f(u) e n => (u,f(u)) e n2]

Iff-And, 224

226 (u,f(u)) e n2 => u e n & f(u) e n

Split, 225

227 u e n & f(u) e n => (u,f(u)) e n2

Split, 225

228 u e n => f(u) e n

U Spec, 11

229 f(u) e n

Detach, 228, 206

230 u e n & f(u) e n

Join, 206, 229

231 (u,f(u)) e n2

Detach, 227, 230

232 f(u)=f(u)

Reflex

233 ~u=x0 & f(u)=f(u)

Join, 217, 232

234 u=x0 & f(u)=x0 | ~u=x0 & f(u)=f(u)

Arb Or, 233

235 (u,f(u)) e n2

& [u=x0 & f(u)=x0 | ~u=x0 & f(u)=f(u)]

Join, 231, 234

236 (u,f(u)) e g

Detach, 222, 235

Apply functionality of g

237 ALL(d):[d=g(u) <=> (u,d) e g]

U Spec, 191

238 f(u)=g(u) <=> (u,f(u)) e g

U Spec, 237

239 [f(u)=g(u) => (u,f(u)) e g]

& [(u,f(u)) e g => f(u)=g(u)]

Iff-And, 238

240 f(u)=g(u) => (u,f(u)) e g

Split, 239

241 (u,f(u)) e g => f(u)=g(u)

Split, 239

242 f(u)=g(u)

Detach, 241, 236

243 g(u)=f(u)

Sym, 242

As Required:

244 ~u=x0 => g(u)=f(u)

4 Conclusion, 217

245 [u=x0 => g(u)=x0] & [~u=x0 => g(u)=f(u)]

Join, 216, 244

As Required:

246 ALL(a):[a e n => [a=x0 => g(a)=x0] & [~a=x0 => g(a)=f(a)]]

4 Conclusion, 206

Prove: ALL(a):ALL(b):[a e n & b e n => [g(a)=g(b) => a=b]] (PA3)

Suppose...

247 u e n & v e n

Premise

248 u e n

Split, 247

249 v e n

Split, 247

Prove: g(u)=g(v) => u=v

Suppose...

250 g(u)=g(v)

Premise

Apply previous result

251 u e n => [u=x0 => g(u)=x0] & [~u=x0 => g(u)=f(u)]

U Spec, 246

252 [u=x0 => g(u)=x0] & [~u=x0 => g(u)=f(u)]

Detach, 251, 248

253 u=x0 => g(u)=x0

Split, 252

254 ~u=x0 => g(u)=f(u)

Split, 252

Apply previous result

255 v e n => [v=x0 => g(v)=x0] & [~v=x0 => g(v)=f(v)]

U Spec, 246

256 [v=x0 => g(v)=x0] & [~v=x0 => g(v)=f(v)]

Detach, 255, 249

257 v=x0 => g(v)=x0

Split, 256

258 ~v=x0 => g(v)=f(v)

Split, 256

Two cases to consider:

259 u=x0 | ~u=x0

Or Not

Two sub-cases to consider:

260 v=x0 | ~v=x0

Or Not

Case 1

Prove: u=x0 => u=v

Suppose...

261 u=x0

Premise

Sub-case 1

Prove: v=x0 => u=v

Suppose...

262 v=x0

Premise

263 u=v

Substitute, 262, 261

Sub-case 1

As Required:

264 v=x0 => u=v

4 Conclusion, 262

Prove: v=x0

Suppose to the contrary...

265 ~v=x0

Premise

266 g(u)=x0

Detach, 253, 261

267 g(v)=f(v)

Detach, 258, 265

268 x0=g(v)

Substitute, 266, 250

269 x0=f(v)

Substitute, 267, 268

270 v e n => ~f(v)=x0

U Spec, 13

271 ~f(v)=x0

Detach, 270, 249

272 f(v)=x0

Sym, 269

273 f(v)=x0 & ~f(v)=x0

Join, 272, 271

274 ~~v=x0

4 Conclusion, 265

As Required:

275 v=x0

Rem DNeg, 274

Sub-case 2

As Required:

276 ~v=x0 => u=v

Arb Cons, 275

277 [v=x0 => u=v] & [~v=x0 => u=v]

Join, 264, 276

278 u=v

Cases, 260, 277

Case 1

As Required:

279 u=x0 => u=v

4 Conclusion, 261

Case 2

Prove: ~u=x0 => u=v

Suppose...

280 ~u=x0

Premise

281 g(u)=f(u)

Detach, 254, 280

Prove: ~v=0

Suppose to the contrary...

282 v=x0

Premise

283 g(v)=x0

Detach, 257, 282

284 f(u)=g(v)

Substitute, 281, 250

285 f(u)=x0

Substitute, 283, 284

Apply previous result

286 u e n => ~f(u)=x0

U Spec, 13

287 ~f(u)=x0

Detach, 286, 248

288 f(u)=x0 & ~f(u)=x0

Join, 285, 287

As Required:

289 ~v=x0

4 Conclusion, 282

290 ~~v=x0 => u=v

Arb Cons, 289

Sub-case 1

As Required:

291 v=x0 => u=v

Rem DNeg, 290

Sub-case 2

Prove: ~v=x0 => u=v

Suppose...

292 ~v=x0

Premise

293 g(v)=f(v)

Detach, 258, 292

294 f(u)=g(v)

Substitute, 281, 250

295 f(u)=f(v)

Substitute, 293, 294

Apply injectivity of f on n

296 ALL(b):[u e n & b e n => [f(u)=f(b) => u=b]]

U Spec, 12

297 u e n & v e n => [f(u)=f(v) => u=v]

U Spec, 296

298 f(u)=f(v) => u=v

Detach, 297, 247

299 u=v

Detach, 298, 295

Sub-case 2

As Required:

300 ~v=x0 => u=v

4 Conclusion, 292

301 [v=x0 => u=v] & [~v=x0 => u=v]

Join, 291, 300

302 u=v

Cases, 260, 301

Case 2

As Required:

303 ~u=x0 => u=v

4 Conclusion, 280

304 [u=x0 => u=v] & [~u=x0 => u=v]

Join, 279, 303

305 u=v

Cases, 259, 304

As Required:

306 g(u)=g(v) => u=v

4 Conclusion, 250

PA3

***

307 ALL(a):ALL(b):[a e n & b e n => [g(a)=g(b) => a=b]]

4 Conclusion, 247

Prove: ALL(a):[aen => ~g(a)=f(x0)] (PA4)

Suppose...

308 u e n

Premise

Apply previous result

309 u e n => [u=x0 => g(u)=x0] & [~u=x0 => g(u)=f(u)]

U Spec, 246

310 [u=x0 => g(u)=x0] & [~u=x0 => g(u)=f(u)]

Detach, 309, 308

311 u=x0 => g(u)=x0

Split, 310

312 ~u=x0 => g(u)=f(u)

Split, 310

Two cases:

313 u=x0 | ~u=x0

Or Not

Case 1

Prove: u=x0 => ~g(u)=f(x0)

Suppose...

314 u=x0

Premise

315 g(u)=x0

Detach, 311, 314

316 x0 e n => ~f(x0)=x0

U Spec, 13

317 ~f(x0)=x0

Detach, 316, 10

318 ~f(x0)=g(u)

Substitute, 315, 317

319 ~g(u)=f(x0)

Sym, 318

Case 1

As Required:

320 u=x0 => ~g(u)=f(x0)

4 Conclusion, 314

Case 2

Prove: ~u=x0 => ~g(u)=f(x0)

Suppose...

321 ~u=x0

Premise

322 g(u)=f(u)

Detach, 312, 321

323 u e n => ~f(u)=x0

U Spec, 13

324 ~f(u)=x0

Detach, 323, 308

Prove: ~g(u)=f(x0)

Suppose to the contrary...

325 g(u)=f(x0)

Premise

326 f(u)=f(x0)

Substitute, 322, 325

Apply injectivity of f

327 ALL(b):[u e n & b e n => [f(u)=f(b) => u=b]]

U Spec, 12

328 u e n & x0 e n => [f(u)=f(x0) => u=x0]

U Spec, 327

329 u e n & x0 e n

Join, 308, 10

330 f(u)=f(x0) => u=x0

Detach, 328, 329

331 u=x0

Detach, 330, 326

332 u=x0 & ~u=x0

Join, 331, 321

As Required:

333 ~g(u)=f(x0)

4 Conclusion, 325

Case 2

As Required:

334 ~u=x0 => ~g(u)=f(x0)

4 Conclusion, 321

335 [u=x0 => ~g(u)=f(x0)] & [~u=x0 => ~g(u)=f(x0)]

Join, 320, 334

336 ~g(u)=f(x0)

Cases, 313, 335

PA4

***

337 ALL(a):[a e n => ~g(a)=f(x0)]

4 Conclusion, 308

Prove: f(x0) e n

338 x0 e n => f(x0) e n

U Spec, 11

PA1

***

339 f(x0) e n

Detach, 338, 10

Suppose to the contrary that induction holds on n with successor function g
and "first" element f(x0)

340 ALL(a):[Set(a) & ALL(b):[b e a => b e n]

=> [f(x0) e a & ALL(b):[b e a => g(b) e a]

=> ALL(b):[b e n => b e a]]]

Premise

Prove by induction that no element of n is its own successor using g as the
successor function. This will be contradicted by the fact that g(x0)=x0.

First, construct the subset p of n

Apply Subset Axiom

341 EXIST(sub):[Set(sub) & ALL(a):[a e sub <=> a e n & ~g(a)=a]]

Subset, 8

342 Set(p) & ALL(a):[a e p <=> a e n & ~g(a)=a]

E Spec, 341

Define: p

343 Set(p)

Split, 342

344 ALL(a):[a e p <=> a e n & ~g(a)=a]

Split, 342

345 Set(p) & ALL(b):[b e p => b e n]

=> [f(x0) e p & ALL(b):[b e p => g(b) e p]

=> ALL(b):[b e n => b e p]]

U Spec, 340

Prove: ALL(b):[b e p => b e n]

Suppose...

346 t e p

Premise

347 t e p <=> t e n & ~g(t)=t

U Spec, 344

348 [t e p => t e n & ~g(t)=t] & [t e n & ~g(t)=t => t e p]

Iff-And, 347

349 t e p => t e n & ~g(t)=t

Split, 348

350 t e n & ~g(t)=t => t e p

Split, 348

351 t e n & ~g(t)=t

Detach, 349, 346

352 t e n

Split, 351

As Required:

353 ALL(b):[b e p => b e n]

4 Conclusion, 346

354 Set(p) & ALL(b):[b e p => b e n]

Join, 343, 353

Sufficient: ALL(b):[b e n => b e p]

355 f(x0) e p & ALL(b):[b e p => g(b) e p]

=> ALL(b):[b e n => b e p]

Detach, 345, 354

356 f(x0) e p <=> f(x0) e n & ~g(f(x0))=f(x0)

U Spec, 344

357 [f(x0) e p => f(x0) e n & ~g(f(x0))=f(x0)]

& [f(x0) e n & ~g(f(x0))=f(x0) => f(x0) e p]

Iff-And, 356

358 f(x0) e p => f(x0) e n & ~g(f(x0))=f(x0)

Split, 357

Sufficient: f(x0) e p

359 f(x0) e n & ~g(f(x0))=f(x0) => f(x0) e p

Split, 357

360 f(x0) e n => ~g(f(x0))=f(x0)

U Spec, 337

361 ~g(f(x0))=f(x0)

Detach, 360, 339

362 f(x0) e n & ~g(f(x0))=f(x0)

Join, 339, 361

As Required:

363 f(x0) e p

Detach, 359, 362

Prove: ALL(b):[b e p => g(b) e p]

Suppose...

364 t e p

Premise

Apply definition of p

365 t e p <=> t e n & ~g(t)=t

U Spec, 344

366 [t e p => t e n & ~g(t)=t] & [t e n & ~g(t)=t => t e p]

Iff-And, 365

367 t e p => t e n & ~g(t)=t

Split, 366

368 t e n & ~g(t)=t => t e p

Split, 366

369 t e n & ~g(t)=t

Detach, 367, 364

370 t e n

Split, 369

371 ~g(t)=t

Split, 369

372 g(t) e p <=> g(t) e n & ~g(g(t))=g(t)

U Spec, 344

373 [g(t) e p => g(t) e n & ~g(g(t))=g(t)]

& [g(t) e n & ~g(g(t))=g(t) => g(t) e p]

Iff-And, 372

374 g(t) e p => g(t) e n & ~g(g(t))=g(t)

Split, 373

Sufficient: g(t) e p

375 g(t) e n & ~g(g(t))=g(t) => g(t) e p

Split, 373

376 t e n => g(t) e n

U Spec, 205

377 g(t) e n

Detach, 376, 370

Prove: ~g(g(t))=g(t)

Suppose to the contrary...

378 g(g(t))=g(t)

Premise

Apply PA3

379 ALL(b):[g(t) e n & b e n => [g(g(t))=g(b) => g(t)=b]]

U Spec, 307

380 g(t) e n & t e n => [g(g(t))=g(t) => g(t)=t]

U Spec, 379

381 g(t) e n & t e n

Join, 377, 370

382 g(g(t))=g(t) => g(t)=t

Detach, 380, 381

383 g(t)=t

Detach, 382, 378

384 g(t)=t & ~g(t)=t

Join, 383, 371

As Required:

385 ~g(g(t))=g(t)

4 Conclusion, 378

386 g(t) e n & ~g(g(t))=g(t)

Join, 377, 385

387 g(t) e p

Detach, 375, 386

As Required:

388 ALL(b):[b e p => g(b) e p]

4 Conclusion, 364

389 f(x0) e p & ALL(b):[b e p => g(b) e p]

Join, 363, 388

390 ALL(b):[b e n => b e p]

Detach, 355, 389

Prove: ALL(a):[a e n => ~g(a)=a]

Suppose...

391 t e n

Premise

392 t e n => t e p

U Spec, 390

393 t e p

Detach, 392, 391

394 t e p <=> t e n & ~g(t)=t

U Spec, 344

395 [t e p => t e n & ~g(t)=t] & [t e n & ~g(t)=t => t e p]

Iff-And, 394

396 t e p => t e n & ~g(t)=t

Split, 395

397 t e n & ~g(t)=t => t e p

Split, 395

398 t e n & ~g(t)=t

Detach, 396, 393

399 t e n

Split, 398

400 ~g(t)=t

Split, 398

As Required:

401 ALL(a):[a e n => ~g(a)=a]

4 Conclusion, 391

402 x0 e n => ~g(x0)=x0

U Spec, 401

403 ~g(x0)=x0

Detach, 402, 10

404 x0 e n => [x0=x0 => g(x0)=x0] & [~x0=x0 => g(x0)=f(x0)]

U Spec, 246

405 [x0=x0 => g(x0)=x0] & [~x0=x0 => g(x0)=f(x0)]

Detach, 404, 10

406 x0=x0 => g(x0)=x0

Split, 405

407 ~x0=x0 => g(x0)=f(x0)

Split, 405

408 x0=x0

Reflex

409 g(x0)=x0

Detach, 406, 408

410 g(x0)=x0 & ~g(x0)=x0

Join, 409, 403

~PA5

****

411 ~ALL(a):[Set(a) & ALL(b):[b e a => b e n]

=> [f(x0) e a & ALL(b):[b e a => g(b) e a]

=> ALL(b):[b e n => b e a]]]

4 Conclusion, 340

412 Set(n) & ALL(a):[a e n => a e x]

Join, 8, 9

413 Set(n) & ALL(a):[a e n => a e x] & x0 e n

Join, 412, 10

414 Set(n) & ALL(a):[a e n => a e x] & x0 e n

& f(x0) e n

Join, 413, 339

415 Set(n) & ALL(a):[a e n => a e x] & x0 e n

& f(x0) e n

& ALL(a):[a e n => f(a) e n]

Join, 414, 11

416 Set(n) & ALL(a):[a e n => a e x] & x0 e n

& f(x0) e n

& ALL(a):[a e n => f(a) e n]

& ALL(a):[a e n => g(a) e n]

Join, 415, 205

417 Set(n) & ALL(a):[a e n => a e x] & x0 e n

& f(x0) e n

& ALL(a):[a e n => f(a) e n]

& ALL(a):[a e n => g(a) e n]

& ALL(a):ALL(b):[a e n & b e n => [f(a)=f(b) => a=b]]

Join, 416, 12

418 Set(n) & ALL(a):[a e n => a e x] & x0 e n

& f(x0) e n

& ALL(a):[a e n => f(a) e n]

& ALL(a):[a e n => g(a) e n]

& ALL(a):ALL(b):[a e n & b e n => [f(a)=f(b) => a=b]]

& ALL(a):ALL(b):[a e n & b e n => [g(a)=g(b) => a=b]]

Join, 417, 307

419 Set(n) & ALL(a):[a e n => a e x] & x0 e n

& f(x0) e n

& ALL(a):[a e n => f(a) e n]

& ALL(a):[a e n => g(a) e n]

& ALL(a):ALL(b):[a e n & b e n => [f(a)=f(b) => a=b]]

& ALL(a):ALL(b):[a e n & b e n => [g(a)=g(b) => a=b]]

& ALL(a):[a e n => ~f(a)=x0]

Join, 418, 13

420 Set(n) & ALL(a):[a e n => a e x] & x0 e n

& f(x0) e n

& ALL(a):[a e n => f(a) e n]

& ALL(a):[a e n => g(a) e n]

& ALL(a):ALL(b):[a e n & b e n => [f(a)=f(b) => a=b]]

& ALL(a):ALL(b):[a e n & b e n => [g(a)=g(b) => a=b]]

& ALL(a):[a e n => ~f(a)=x0]

& ALL(a):[a e n => ~g(a)=f(x0)]

Join, 419, 337

421 Set(n) & ALL(a):[a e n => a e x] & x0 e n

& f(x0) e n

& ALL(a):[a e n => f(a) e n]

& ALL(a):[a e n => g(a) e n]

& ALL(a):ALL(b):[a e n & b e n => [f(a)=f(b) => a=b]]

& ALL(a):ALL(b):[a e n & b e n => [g(a)=g(b) => a=b]]

& ALL(a):[a e n => ~f(a)=x0]

& ALL(a):[a e n => ~g(a)=f(x0)]

& ALL(a):[Set(a) & ALL(b):[b e a => b e n]

=> [x0 e a & ALL(b):[b e a => f(b) e a]

=> ALL(b):[b e n => b e a]]]

Join, 420, 14

422 Set(n) & ALL(a):[a e n => a e x] & x0 e n

& f(x0) e n

& ALL(a):[a e n => f(a) e n]

& ALL(a):[a e n => g(a) e n]

& ALL(a):ALL(b):[a e n & b e n => [f(a)=f(b) => a=b]]

& ALL(a):ALL(b):[a e n & b e n => [g(a)=g(b) => a=b]]

& ALL(a):[a e n => ~f(a)=x0]

& ALL(a):[a e n => ~g(a)=f(x0)]

& ALL(a):[Set(a) & ALL(b):[b e a => b e n]

=> [x0 e a & ALL(b):[b e a => f(b) e a]

=> ALL(b):[b e n => b e a]]]

& ~ALL(a):[Set(a) & ALL(b):[b e a => b e n]

=> [f(x0) e a & ALL(b):[b e a => g(b) e a]

=> ALL(b):[b e n => b e a]]]

Join, 421, 411

423 f(x0)=f(x0)

Reflex

424 EXIST(x1):f(x0)=x1

E Gen, 423

425 f(x0)=x1

E Spec, 424

426 Set(n) & ALL(a):[a e n => a e x] & x0 e n

& x1 e n

& ALL(a):[a e n => f(a) e n]

& ALL(a):[a e n => g(a) e n]

& ALL(a):ALL(b):[a e n & b e n => [f(a)=f(b) => a=b]]

& ALL(a):ALL(b):[a e n & b e n => [g(a)=g(b) => a=b]]

& ALL(a):[a e n => ~f(a)=x0]

& ALL(a):[a e n => ~g(a)=x1]

& ALL(a):[Set(a) & ALL(b):[b e a => b e n]

=> [x0 e a & ALL(b):[b e a => f(b) e a]

=> ALL(b):[b e n => b e a]]]

& ~ALL(a):[Set(a) & ALL(b):[b e a => b e n]

=> [x1 e a & ALL(b):[b e a => g(b) e a]

=> ALL(b):[b e n => b e a]]]

Substitute, 425, 422

427 EXIST(g):[Set(n) & ALL(a):[a e n => a e x] & x0 e n

& x1 e n

& ALL(a):[a e n => f(a) e n]

& ALL(a):[a e n => g(a) e n]

& ALL(a):ALL(b):[a e n & b e n => [f(a)=f(b) => a=b]]

& ALL(a):ALL(b):[a e n & b e n => [g(a)=g(b) => a=b]]

& ALL(a):[a e n => ~f(a)=x0]

& ALL(a):[a e n => ~g(a)=x1]

& ALL(a):[Set(a) & ALL(b):[b e a => b e n]

=> [x0 e a & ALL(b):[b e a => f(b) e a]

=> ALL(b):[b e n => b e a]]]

& ~ALL(a):[Set(a) & ALL(b):[b e a => b e n]

=> [x1 e a & ALL(b):[b e a => g(b) e a]

=> ALL(b):[b e n => b e a]]]]

E Gen, 426

428 EXIST(f):EXIST(g):[Set(n) & ALL(a):[a e n => a e x] & x0 e n

& x1 e n

& ALL(a):[a e n => f(a) e n]

& ALL(a):[a e n => g(a) e n]

& ALL(a):ALL(b):[a e n & b e n => [f(a)=f(b) => a=b]]

& ALL(a):ALL(b):[a e n & b e n => [g(a)=g(b) => a=b]]

& ALL(a):[a e n => ~f(a)=x0]

& ALL(a):[a e n => ~g(a)=x1]

& ALL(a):[Set(a) & ALL(b):[b e a => b e n]

=> [x0 e a & ALL(b):[b e a => f(b) e a]

=> ALL(b):[b e n => b e a]]]

& ~ALL(a):[Set(a) & ALL(b):[b e a => b e n]

=> [x1 e a & ALL(b):[b e a => g(b) e a]

=> ALL(b):[b e n => b e a]]]]

E Gen, 427

429 EXIST(n1):EXIST(f):EXIST(g):[Set(n) & ALL(a):[a e n => a e x] & x0 e n

& n1 e n

& ALL(a):[a e n => f(a) e n]

& ALL(a):[a e n => g(a) e n]

& ALL(a):ALL(b):[a e n & b e n => [f(a)=f(b) => a=b]]

& ALL(a):ALL(b):[a e n & b e n => [g(a)=g(b) => a=b]]

& ALL(a):[a e n => ~f(a)=x0]

& ALL(a):[a e n => ~g(a)=n1]

& ALL(a):[Set(a) & ALL(b):[b e a => b e n]

=> [x0 e a & ALL(b):[b e a => f(b) e a]

=> ALL(b):[b e n => b e a]]]

& ~ALL(a):[Set(a) & ALL(b):[b e a => b e n]

=> [n1 e a & ALL(b):[b e a => g(b) e a]

=> ALL(b):[b e n => b e a]]]]

E Gen, 428

430 EXIST(n0):EXIST(n1):EXIST(f):EXIST(g):[Set(n) & ALL(a):[a e n => a e x] & n0 e n

& n1 e n

& ALL(a):[a e n => f(a) e n]

& ALL(a):[a e n => g(a) e n]

& ALL(a):ALL(b):[a e n & b e n => [f(a)=f(b) => a=b]]

& ALL(a):ALL(b):[a e n & b e n => [g(a)=g(b) => a=b]]

& ALL(a):[a e n => ~f(a)=n0]

& ALL(a):[a e n => ~g(a)=n1]

& ALL(a):[Set(a) & ALL(b):[b e a => b e n]

=> [n0 e a & ALL(b):[b e a => f(b) e a]

=> ALL(b):[b e n => b e a]]]

& ~ALL(a):[Set(a) & ALL(b):[b e a => b e n]

=> [n1 e a & ALL(b):[b e a => g(b) e a]

=> ALL(b):[b e n => b e a]]]]

E Gen, 429

431 EXIST(n):EXIST(n0):EXIST(n1):EXIST(f):EXIST(g):[Set(n) & ALL(a):[a e n => a e x] & n0 e n

& n1 e n

& ALL(a):[a e n => f(a) e n]

& ALL(a):[a e n => g(a) e n]

& ALL(a):ALL(b):[a e n & b e n => [f(a)=f(b) => a=b]]

& ALL(a):ALL(b):[a e n & b e n => [g(a)=g(b) => a=b]]

& ALL(a):[a e n => ~f(a)=n0]

& ALL(a):[a e n => ~g(a)=n1]

& ALL(a):[Set(a) & ALL(b):[b e a => b e n]

=> [n0 e a & ALL(b):[b e a => f(b) e a]

=> ALL(b):[b e n => b e a]]]

& ~ALL(a):[Set(a) & ALL(b):[b e a => b e n]

=> [n1 e a & ALL(b):[b e a => g(b) e a]

=> ALL(b):[b e n => b e a]]]]

E Gen, 430

As Required:

432 ALL(x):[Set(x) & Infinite(x)

=> EXIST(n):EXIST(n0):EXIST(n1):EXIST(f):EXIST(g):[Set(n) & ALL(a):[a e n => a e x] & n0 e n

& n1 e n

& ALL(a):[a e n => f(a) e n]

& ALL(a):[a e n => g(a) e n]

& ALL(a):ALL(b):[a e n & b e n => [f(a)=f(b) => a=b]]

& ALL(a):ALL(b):[a e n & b e n => [g(a)=g(b) => a=b]]

& ALL(a):[a e n => ~f(a)=n0]

& ALL(a):[a e n => ~g(a)=n1]

& ALL(a):[Set(a) & ALL(b):[b e a => b e n]

=> [n0 e a & ALL(b):[b e a => f(b) e a]

=> ALL(b):[b e n => b e a]]]

& ~ALL(a):[Set(a) & ALL(b):[b e a => b e n]

=> [n1 e a & ALL(b):[b e a => g(b) e a]

=> ALL(b):[b e n => b e a]]]]]

4 Conclusion, 2