THEOREM

-------

Let f be an injective (one-to-one) function defined on a set s:

1-1

f: s ---> s

For every element s1 of s with no pre-image in s under f, there exists a unique set n

that is identical in structure to the set of natural numbers (as defined by Peano's axioms)

in which f is the successor function.

INFORMAL OUTLINE

----------------

We construct n = {s1, f(s1), f(f(s1)), ... }

The usual axioms for the natural numbers, with f as the successor function, are shown

here to apply on n:

N1: s1 e n                                               (lines 12-21)

N2: ALL(a):[a e n => f(a) e n]                           (22-48)

N3: ALL(a):ALL(b):[a e n & b e n => [f(a)=f(b) => a=b]]  (49-70)

N4: ALL(a):[a e n => ~f(a)=s1]                           (71-81)

N5: ALL(b):[Set(b)                                       (82-106)

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

& s1 e b

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

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

The remainder of the proof establishes the uniqueness of n

This proof was prepared with the aid of the author's DC Proof 2.0 system

available

PROOF

-----

Let f be an injective (one-to-one) function on s

1     Set(s)

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

& ALL(b):ALL(c):[b e s & c e s => [f(b)=f(c) => b=c]]

Premise

Splitting up this premise...

s is a set

2     Set(s)

Split, 1

f is a function mapping s to s

3     ALL(b):[b e s => f(b) e s]

Split, 1

f is an injective

4     ALL(b):ALL(c):[b e s & c e s => [f(b)=f(c) => b=c]]

Split, 1

Suppose that s1 be an element of s with no pre-image under f

5     s1 e s & ALL(b):[b e s => ~f(b)=s1]

Premise

Splitting up this premise...

s1 is an element of s

6     s1 e s

Split, 5

s1 has no pre-image under f

7     ALL(b):[b e s => ~f(b)=s1]

Split, 5

Construct the set n

Applying the Subset Axiom...

8     EXIST(sub):[Set(sub) & ALL(a):[a e sub <=> a e s & ALL(b):[Set(b)

& s1 e b

& ALL(c):[c e b & c e s => f(c) e b]

=> a e b]]]

Subset, 2

9     Set(n) & ALL(a):[a e n <=> a e s & ALL(b):[Set(b)

& s1 e b

& ALL(c):[c e b & c e s => f(c) e b]

=> a e b]]

E Spec, 8

Define: n

10    Set(n)

Split, 9

11    ALL(a):[a e n <=> a e s & ALL(b):[Set(b)

& s1 e b

& ALL(c):[c e b & c e s => f(c) e b]

=> a e b]]

Split, 9

PROVE N1

--------

Prove: s1 e n

Apply definition of n for s1

12    s1 e n <=> s1 e s & ALL(b):[Set(b)

& s1 e b

& ALL(c):[c e b & c e s => f(c) e b]

=> s1 e b]

U Spec, 11

13    [s1 e n => s1 e s & ALL(b):[Set(b)

& s1 e b

& ALL(c):[c e b & c e s => f(c) e b]

=> s1 e b]]

& [s1 e s & ALL(b):[Set(b)

& s1 e b

& ALL(c):[c e b & c e s => f(c) e b]

=> s1 e b] => s1 e n]

Iff-And, 12

14    s1 e n => s1 e s & ALL(b):[Set(b)

& s1 e b

& ALL(c):[c e b & c e s => f(c) e b]

=> s1 e b]

Split, 13

Sufficient: For s1 e n

15    s1 e s & ALL(b):[Set(b)

& s1 e b

& ALL(c):[c e b & c e s => f(c) e b]

=> s1 e b] => s1 e n

Split, 13

Prove: ALL(b):[Set(b)

& s1 e b

& ALL(c):[c e b & c e s => f(c) e b]

=> s1 e b]

Suppose...

16    Set(p)

& s1 e p

& ALL(c):[c e p & c e s => f(c) e p]

Premise

17    Set(p)

Split, 16

18    s1 e p

Split, 16

As Required:

19    ALL(b):[Set(b)

& s1 e b

& ALL(c):[c e b & c e s => f(c) e b]

=> s1 e b]

4 Conclusion, 16

20    s1 e s

& ALL(b):[Set(b)

& s1 e b

& ALL(c):[c e b & c e s => f(c) e b]

=> s1 e b]

Join, 6, 19

N1:

---

21    s1 e n

Detach, 15, 20

PROVE N2

--------

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

Suppose...

22    x e n

Premise

Apply definition of n for x

23    x e n <=> x e s & ALL(b):[Set(b)

& s1 e b

& ALL(c):[c e b & c e s => f(c) e b]

=> x e b]

U Spec, 11

24    [x e n => x e s & ALL(b):[Set(b)

& s1 e b

& ALL(c):[c e b & c e s => f(c) e b]

=> x e b]]

& [x e s & ALL(b):[Set(b)

& s1 e b

& ALL(c):[c e b & c e s => f(c) e b]

=> x e b] => x e n]

Iff-And, 23

25    x e n => x e s & ALL(b):[Set(b)

& s1 e b

& ALL(c):[c e b & c e s => f(c) e b]

=> x e b]

Split, 24

26    x e s & ALL(b):[Set(b)

& s1 e b

& ALL(c):[c e b & c e s => f(c) e b]

=> x e b] => x e n

Split, 24

27    x e s & ALL(b):[Set(b)

& s1 e b

& ALL(c):[c e b & c e s => f(c) e b]

=> x e b]

Detach, 25, 22

28    x e s

Split, 27

29    ALL(b):[Set(b)

& s1 e b

& ALL(c):[c e b & c e s => f(c) e b]

=> x e b]

Split, 27

Apply definition of n for f(x)

30    f(x) e n <=> f(x) e s & ALL(b):[Set(b)

& s1 e b

& ALL(c):[c e b & c e s => f(c) e b]

=> f(x) e b]

U Spec, 11

31    [f(x) e n => f(x) e s & ALL(b):[Set(b)

& s1 e b

& ALL(c):[c e b & c e s => f(c) e b]

=> f(x) e b]]

& [f(x) e s & ALL(b):[Set(b)

& s1 e b

& ALL(c):[c e b & c e s => f(c) e b]

=> f(x) e b] => f(x) e n]

Iff-And, 30

32    f(x) e n => f(x) e s & ALL(b):[Set(b)

& s1 e b

& ALL(c):[c e b & c e s => f(c) e b]

=> f(x) e b]

Split, 31

Sufficient: For f(x) e n

33    f(x) e s & ALL(b):[Set(b)

& s1 e b

& ALL(c):[c e b & c e s => f(c) e b]

=> f(x) e b] => f(x) e n

Split, 31

34    x e s => f(x) e s

U Spec, 3

35    f(x) e s

Detach, 34, 28

Prove: ALL(b):[Set(b)

& s1 e b

& ALL(c):[c e b & c e s => f(c) e b]

=> f(x) e b]

Suppose...

36    Set(p)

& s1 e p

& ALL(c):[c e p & c e s => f(c) e p]

Premise

37    Set(p)

Split, 36

38    s1 e p

Split, 36

39    ALL(c):[c e p & c e s => f(c) e p]

Split, 36

From previous result

40    Set(p)

& s1 e p

& ALL(c):[c e p & c e s => f(c) e p]

=> x e p

U Spec, 29

41    x e p

Detach, 40, 36

42    x e p & x e s => f(x) e p

U Spec, 39

43    x e p & x e s

Join, 41, 28

44    f(x) e p

Detach, 42, 43

As Required:

45    ALL(b):[Set(b)

& s1 e b

& ALL(c):[c e b & c e s => f(c) e b]

=> f(x) e b]

4 Conclusion, 36

46    f(x) e s

& ALL(b):[Set(b)

& s1 e b

& ALL(c):[c e b & c e s => f(c) e b]

=> f(x) e b]

Join, 35, 45

47    f(x) e n

Detach, 33, 46

N2:

---

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

4 Conclusion, 22

PROVE N3

--------

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

Suppose...

49    x e n & y e n

Premise

50    x e n

Split, 49

51    y e n

Split, 49

Apply premise

52    ALL(c):[x e s & c e s => [f(x)=f(c) => x=c]]

U Spec, 4

53    x e s & y e s => [f(x)=f(y) => x=y]

U Spec, 52

Apply definition of n for x

54    x e n <=> x e s & ALL(b):[Set(b)

& s1 e b

& ALL(c):[c e b & c e s => f(c) e b]

=> x e b]

U Spec, 11

55    [x e n => x e s & ALL(b):[Set(b)

& s1 e b

& ALL(c):[c e b & c e s => f(c) e b]

=> x e b]]

& [x e s & ALL(b):[Set(b)

& s1 e b

& ALL(c):[c e b & c e s => f(c) e b]

=> x e b] => x e n]

Iff-And, 54

56    x e n => x e s & ALL(b):[Set(b)

& s1 e b

& ALL(c):[c e b & c e s => f(c) e b]

=> x e b]

Split, 55

57    x e s & ALL(b):[Set(b)

& s1 e b

& ALL(c):[c e b & c e s => f(c) e b]

=> x e b] => x e n

Split, 55

58    x e s & ALL(b):[Set(b)

& s1 e b

& ALL(c):[c e b & c e s => f(c) e b]

=> x e b]

Detach, 56, 50

59    x e s

Split, 58

60    ALL(b):[Set(b)

& s1 e b

& ALL(c):[c e b & c e s => f(c) e b]

=> x e b]

Split, 58

Apply definition of n for y

61    y e n <=> y e s & ALL(b):[Set(b)

& s1 e b

& ALL(c):[c e b & c e s => f(c) e b]

=> y e b]

U Spec, 11

62    [y e n => y e s & ALL(b):[Set(b)

& s1 e b

& ALL(c):[c e b & c e s => f(c) e b]

=> y e b]]

& [y e s & ALL(b):[Set(b)

& s1 e b

& ALL(c):[c e b & c e s => f(c) e b]

=> y e b] => y e n]

Iff-And, 61

63    y e n => y e s & ALL(b):[Set(b)

& s1 e b

& ALL(c):[c e b & c e s => f(c) e b]

=> y e b]

Split, 62

64    y e s & ALL(b):[Set(b)

& s1 e b

& ALL(c):[c e b & c e s => f(c) e b]

=> y e b] => y e n

Split, 62

65    y e s & ALL(b):[Set(b)

& s1 e b

& ALL(c):[c e b & c e s => f(c) e b]

=> y e b]

Detach, 63, 51

66    y e s

Split, 65

67    ALL(b):[Set(b)

& s1 e b

& ALL(c):[c e b & c e s => f(c) e b]

=> y e b]

Split, 65

68    x e s & y e s

Join, 59, 66

69    f(x)=f(y) => x=y

Detach, 53, 68

N3:

---

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

4 Conclusion, 49

PROVE N4

--------

Prove: ALL(b):[b e n => ~f(b)=s1]

Suppose...

71    x e n

Premise

72    x e s => ~f(x)=s1

U Spec, 7

Apply definition of n for x

73    x e n <=> x e s & ALL(b):[Set(b)

& s1 e b

& ALL(c):[c e b & c e s => f(c) e b]

=> x e b]

U Spec, 11

74    [x e n => x e s & ALL(b):[Set(b)

& s1 e b

& ALL(c):[c e b & c e s => f(c) e b]

=> x e b]]

& [x e s & ALL(b):[Set(b)

& s1 e b

& ALL(c):[c e b & c e s => f(c) e b]

=> x e b] => x e n]

Iff-And, 73

75    x e n => x e s & ALL(b):[Set(b)

& s1 e b

& ALL(c):[c e b & c e s => f(c) e b]

=> x e b]

Split, 74

76    x e s & ALL(b):[Set(b)

& s1 e b

& ALL(c):[c e b & c e s => f(c) e b]

=> x e b] => x e n

Split, 74

77    x e s & ALL(b):[Set(b)

& s1 e b

& ALL(c):[c e b & c e s => f(c) e b]

=> x e b]

Detach, 75, 71

78    x e s

Split, 77

79    ALL(b):[Set(b)

& s1 e b

& ALL(c):[c e b & c e s => f(c) e b]

=> x e b]

Split, 77

80    ~f(x)=s1

Detach, 72, 78

N4:

---

81    ALL(b):[b e n => ~f(b)=s1]

4 Conclusion, 71

PROVE N5

--------

Prove: ALL(b):[Set(b)

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

& s1 e b

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

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

Suppose...

82    Set(p)

& ALL(c):[c e p => c e n]

& s1 e p

& ALL(c):[c e p => f(c) e p]

Premise

83    Set(p)

Split, 82

84    ALL(c):[c e p => c e n]

Split, 82

85    s1 e p

Split, 82

How about ALL(c):[c e p & c e n => f(c) e p] ????

86    ALL(c):[c e p => f(c) e p]

Split, 82

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

Suppose...

87    x e n

Premise

Apply definiton of n for x

88    x e n <=> x e s & ALL(b):[Set(b)

& s1 e b

& ALL(c):[c e b & c e s => f(c) e b]

=> x e b]

U Spec, 11

89    [x e n => x e s & ALL(b):[Set(b)

& s1 e b

& ALL(c):[c e b & c e s => f(c) e b]

=> x e b]]

& [x e s & ALL(b):[Set(b)

& s1 e b

& ALL(c):[c e b & c e s => f(c) e b]

=> x e b] => x e n]

Iff-And, 88

90    x e n => x e s & ALL(b):[Set(b)

& s1 e b

& ALL(c):[c e b & c e s => f(c) e b]

=> x e b]

Split, 89

91    x e s & ALL(b):[Set(b)

& s1 e b

& ALL(c):[c e b & c e s => f(c) e b]

=> x e b] => x e n

Split, 89

92    x e s & ALL(b):[Set(b)

& s1 e b

& ALL(c):[c e b & c e s => f(c) e b]

=> x e b]

Detach, 90, 87

93    x e s

Split, 92

94    ALL(b):[Set(b)

& s1 e b

& ALL(c):[c e b & c e s => f(c) e b]

=> x e b]

Split, 92

Sufficient: For x e p

95    Set(p)

& s1 e p

& ALL(c):[c e p & c e s => f(c) e p]

=> x e p

U Spec, 94

Prove: ALL(c):[c e p & c e s => f(c) e p]

Suppose...

96    y e p & y e s

Premise

97    y e p

Split, 96

98    y e s

Split, 96

Apply previous result

99    y e p => f(y) e p

U Spec, 86

100  f(y) e p

Detach, 99, 97

As Required:

101  ALL(c):[c e p & c e s => f(c) e p]

4 Conclusion, 96

102  Set(p) & s1 e p

Join, 83, 85

103  Set(p) & s1 e p

& ALL(c):[c e p & c e s => f(c) e p]

Join, 102, 101

104  x e p

Detach, 95, 103

As Required:

105  ALL(c):[c e n => c e p]

4 Conclusion, 87

N5:

---

The principle of mathematical induction holds on n

106  ALL(b):[Set(b)

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

& s1 e b

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

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

4 Conclusion, 82

PROVE UNIQUENESS OF n

---------------------

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

Suppose...

107  x e n

Premise

108  x e n <=> x e s & ALL(b):[Set(b)

& s1 e b

& ALL(c):[c e b & c e s => f(c) e b]

=> x e b]

U Spec, 11

109  [x e n => x e s & ALL(b):[Set(b)

& s1 e b

& ALL(c):[c e b & c e s => f(c) e b]

=> x e b]]

& [x e s & ALL(b):[Set(b)

& s1 e b

& ALL(c):[c e b & c e s => f(c) e b]

=> x e b] => x e n]

Iff-And, 108

110  x e n => x e s & ALL(b):[Set(b)

& s1 e b

& ALL(c):[c e b & c e s => f(c) e b]

=> x e b]

Split, 109

111  x e s & ALL(b):[Set(b)

& s1 e b

& ALL(c):[c e b & c e s => f(c) e b]

=> x e b] => x e n

Split, 109

112  x e s & ALL(b):[Set(b)

& s1 e b

& ALL(c):[c e b & c e s => f(c) e b]

=> x e b]

Detach, 110, 107

113  x e s

Split, 112

As Required:

114  ALL(b):[b e n => b e s]

4 Conclusion, 107

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

Join, 10, 114

116  Set(n) & ALL(b):[b e n => b e s] & s1 e n

Join, 115, 21

117  Set(n) & ALL(b):[b e n => b e s] & s1 e n

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

Join, 116, 48

118  Set(n) & ALL(b):[b e n => b e s] & s1 e n

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

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

Join, 117, 70

119  Set(n) & ALL(b):[b e n => b e s] & s1 e n

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

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

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

Join, 118, 81

120  Set(n) & ALL(b):[b e n => b e s] & s1 e n

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

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

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

& ALL(b):[Set(b)

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

& s1 e b

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

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

Join, 119, 106

Prove: n'=n where...

121  Set(n') & ALL(b):[b e n' => b e s] & s1 e n'

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

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

& ALL(b):[b e n' => ~f(b)=s1]

& ALL(b):[Set(b)

& ALL(c):[c e b => c e n']

& s1 e b

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

=> ALL(c):[c e n' => c e b]]

Premise

122  Set(n')

Split, 121

123  ALL(b):[b e n' => b e s]

Split, 121

124  s1 e n'

Split, 121

125  ALL(b):[b e n' => f(b) e n']

Split, 121

126  ALL(b):ALL(c):[b e n' & c e n => [f(b)=f(c) => b=c]]

Split, 121

127  ALL(b):[b e n' => ~f(b)=s1]

Split, 121

128  ALL(b):[Set(b)

& ALL(c):[c e b => c e n']

& s1 e b

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

=> ALL(c):[c e n' => c e b]]

Split, 121

129  Set(n')

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

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

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

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

& ALL(b):[Set(b)

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

& s1 e b

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

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

Join, 122, 120

Apply Set Equality Axiom

130  ALL(a):ALL(b):[Set(a) & Set(b) => [a=b <=> ALL(c):[c e a <=> c e b]]]

Set Equality

131  ALL(b):[Set(n') & Set(b) => [n'=b <=> ALL(c):[c e n' <=> c e b]]]

U Spec, 130

132  Set(n') & Set(n) => [n'=n <=> ALL(c):[c e n' <=> c e n]]

U Spec, 131

133  Set(n') & Set(n)

Join, 122, 10

134  n'=n <=> ALL(c):[c e n' <=> c e n]

Detach, 132, 133

135  [n'=n => ALL(c):[c e n' <=> c e n]]

& [ALL(c):[c e n' <=> c e n] => n'=n]

Iff-And, 134

136  n'=n => ALL(c):[c e n' <=> c e n]

Split, 135

Sufficient: n'=n

137  ALL(c):[c e n' <=> c e n] => n'=n

Split, 135

138  EXIST(sub):[Set(sub) & ALL(a):[a e sub <=> a e n' & a e n]]

Subset, 122

139  Set(p) & ALL(a):[a e p <=> a e n' & a e n]

E Spec, 138

Define: p

140  Set(p)

Split, 139

141  ALL(a):[a e p <=> a e n' & a e n]

Split, 139

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

142  Set(p)

& ALL(c):[c e p => c e n']

& s1 e p

& ALL(c):[c e p => f(c) e p]

=> ALL(c):[c e n' => c e p]

U Spec, 128

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

Suppose...

143  x e p

Premise

144  x e p <=> x e n' & x e n

U Spec, 141

145  [x e p => x e n' & x e n] & [x e n' & x e n => x e p]

Iff-And, 144

146  x e p => x e n' & x e n

Split, 145

147  x e n' & x e n => x e p

Split, 145

148  x e n' & x e n

Detach, 146, 143

149  x e n'

Split, 148

As Required:

150  ALL(c):[c e p => c e n']

4 Conclusion, 143

151  s1 e p <=> s1 e n' & s1 e n

U Spec, 141

152  [s1 e p => s1 e n' & s1 e n]

& [s1 e n' & s1 e n => s1 e p]

Iff-And, 151

153  s1 e p => s1 e n' & s1 e n

Split, 152

Sufficient: s1 e p

154  s1 e n' & s1 e n => s1 e p

Split, 152

155  s1 e n' & s1 e n

Join, 124, 21

As Required:

156  s1 e p

Detach, 154, 155

Prove: ALL(c):[c e p => f(c) e p]

Suppose...

157  x e p

Premise

158  x e p <=> x e n' & x e n

U Spec, 141

159  [x e p => x e n' & x e n] & [x e n' & x e n => x e p]

Iff-And, 158

160  x e p => x e n' & x e n

Split, 159

161  x e n' & x e n => x e p

Split, 159

162  x e n' & x e n

Detach, 160, 157

163  x e n'

Split, 162

164  x e n

Split, 162

165  f(x) e p <=> f(x) e n' & f(x) e n

U Spec, 141

166  [f(x) e p => f(x) e n' & f(x) e n]

& [f(x) e n' & f(x) e n => f(x) e p]

Iff-And, 165

167  f(x) e p => f(x) e n' & f(x) e n

Split, 166

Sufficient: f(x) e p

168  f(x) e n' & f(x) e n => f(x) e p

Split, 166

169  x e n' => f(x) e n'

U Spec, 125

170  f(x) e n'

Detach, 169, 163

171  x e n => f(x) e n

U Spec, 48

172  f(x) e n

Detach, 171, 164

173  f(x) e n' & f(x) e n

Join, 170, 172

174  f(x) e p

Detach, 168, 173

As Required:

175  ALL(c):[c e p => f(c) e p]

4 Conclusion, 157

176  Set(p) & ALL(c):[c e p => c e n']

Join, 140, 150

177  Set(p) & ALL(c):[c e p => c e n'] & s1 e p

Join, 176, 156

178  Set(p) & ALL(c):[c e p => c e n'] & s1 e p

& ALL(c):[c e p => f(c) e p]

Join, 177, 175

179  ALL(c):[c e n' => c e p]

Detach, 142, 178

Prove: ALL(c):[c e n' => c e n]

Suppose...

180  x e n'

Premise

181  x e n' => x e p

U Spec, 179

182  x e p

Detach, 181, 180

183  x e p <=> x e n' & x e n

U Spec, 141

184  [x e p => x e n' & x e n] & [x e n' & x e n => x e p]

Iff-And, 183

185  x e p => x e n' & x e n

Split, 184

186  x e n' & x e n => x e p

Split, 184

187  x e n' & x e n

Detach, 185, 182

188  x e n'

Split, 187

189  x e n

Split, 187

As Required:

190  ALL(c):[c e n' => c e n]

4 Conclusion, 180

191  EXIST(sub):[Set(sub) & ALL(a):[a e sub <=> a e n & a e n']]

Subset, 10

192  Set(p') & ALL(a):[a e p' <=> a e n & a e n']

E Spec, 191

Define: p'

193  Set(p')

Split, 192

194  ALL(a):[a e p' <=> a e n & a e n']

Split, 192

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

195  Set(p')

& ALL(c):[c e p' => c e n]

& s1 e p'

& ALL(c):[c e p' => f(c) e p']

=> ALL(c):[c e n => c e p']

U Spec, 106

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

Suppose...

196  x e p'

Premise

197  x e p' <=> x e n & x e n'

U Spec, 194

198  [x e p' => x e n & x e n'] & [x e n & x e n' => x e p']

Iff-And, 197

199  x e p' => x e n & x e n'

Split, 198

200  x e n & x e n' => x e p'

Split, 198

201  x e n & x e n'

Detach, 199, 196

202  x e n

Split, 201

As Required:

203  ALL(c):[c e p' => c e n]

4 Conclusion, 196

204  s1 e p' <=> s1 e n & s1 e n'

U Spec, 194

205  [s1 e p' => s1 e n & s1 e n']

& [s1 e n & s1 e n' => s1 e p']

Iff-And, 204

206  s1 e p' => s1 e n & s1 e n'

Split, 205

Sufficient: s1 e p'

207  s1 e n & s1 e n' => s1 e p'

Split, 205

208  s1 e n & s1 e n'

Join, 21, 124

As Required:

209  s1 e p'

Detach, 207, 208

Prove: ALL(c):[c e p' => f(c) e p']

Suppose...

210  x e p'

Premise

211  x e p' <=> x e n & x e n'

U Spec, 194

212  [x e p' => x e n & x e n'] & [x e n & x e n' => x e p']

Iff-And, 211

213  x e p' => x e n & x e n'

Split, 212

214  x e n & x e n' => x e p'

Split, 212

215  x e n & x e n'

Detach, 213, 210

216  x e n

Split, 215

217  x e n'

Split, 215

218  f(x) e p' <=> f(x) e n & f(x) e n'

U Spec, 194

219  [f(x) e p' => f(x) e n & f(x) e n']

& [f(x) e n & f(x) e n' => f(x) e p']

Iff-And, 218

220  f(x) e p' => f(x) e n & f(x) e n'

Split, 219

221  f(x) e n & f(x) e n' => f(x) e p'

Split, 219

222  x e n => f(x) e n

U Spec, 48

223  f(x) e n

Detach, 222, 216

224  x e n' => f(x) e n'

U Spec, 125

225  f(x) e n'

Detach, 224, 217

226  f(x) e n & f(x) e n'

Join, 223, 225

227  f(x) e p'

Detach, 221, 226

As Required:

228  ALL(c):[c e p' => f(c) e p']

4 Conclusion, 210

229  Set(p') & ALL(c):[c e p' => c e n]

Join, 193, 203

230  Set(p') & ALL(c):[c e p' => c e n] & s1 e p'

Join, 229, 209

231  Set(p') & ALL(c):[c e p' => c e n] & s1 e p'

& ALL(c):[c e p' => f(c) e p']

Join, 230, 228

As Required:

232  ALL(c):[c e n => c e p']

Detach, 195, 231

Prove: ALL(c):[c e n => c e n']

Suppose...

233  x e n

Premise

234  x e n => x e p'

U Spec, 232

235  x e p'

Detach, 234, 233

236  x e p' <=> x e n & x e n'

U Spec, 194

237  [x e p' => x e n & x e n'] & [x e n & x e n' => x e p']

Iff-And, 236

238  x e p' => x e n & x e n'

Split, 237

239  x e n & x e n' => x e p'

Split, 237

240  x e n & x e n'

Detach, 238, 235

241  x e n

Split, 240

242  x e n'

Split, 240

As Required:

243  ALL(c):[c e n => c e n']

4 Conclusion, 233

244  ALL(c):[[c e n' => c e n] & [c e n => c e n']]

Join, 190, 243

245  ALL(c):[c e n' <=> c e n]

Iff-And, 244

246  n'=n

Detach, 137, 245

n is unique

As Required:

247  ALL(n'):[Set(n') & ALL(b):[b e n' => b e s] & s1 e n'

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

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

& ALL(b):[b e n' => ~f(b)=s1]

& ALL(b):[Set(b)

& ALL(c):[c e b => c e n']

& s1 e b

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

=> ALL(c):[c e n' => c e b]]

=> n'=n]

4 Conclusion, 121