```Recursion Theorem

Prove:

ALL(a):ALL(b):ALL(g):[Set(a)
& b ε a
& ALL(c):ALL(d):[c ε n & d ε a => g(c,d) ε a]
=> EXIST(f):[f(1)=b & ALL(c):[c ε n => f(c+1)=g(c+1,f(c))]]]

Axioms
------

1	Set(n)
Axiom

2	1 ε n
Axiom

3	ALL(a):ALL(b):[a ε n & b ε n => a+b ε n]
Axiom

4	ALL(a):[a ε n => ~a+1=1]
Axiom

5	ALL(a):ALL(b):[a ε n & b ε n & a+1=b+1 => a=b]
Axiom

6	ALL(a):ALL(b):[a ε n & b ε n => a+(b+1)=a+b+1]
Axiom

7	ALL(a):[Set(a) & 1 ε a & ALL(b):[b ε n & b ε a => b+1 ε a] => ALL(b):[b ε n => b ε a]]
Axiom

Prove:

ALL(a):ALL(b):ALL(g):[Set(a)
& b ε a
& ALL(c):ALL(d):[c ε n & d ε a => g(c,d) ε a]
=> EXIST(g):[ALL(c):[c ε n => g(c) ε a]
& g(1)=b
& ALL(c):f(c+1)=g(c+1,f(c))]]

Suppose...

8	Set(m)
& m1 ε m
& ALL(c):ALL(d):[c ε n & d ε m => g(c,d) ε m]
Premise

9	Set(m)
Split, 8

10	m1 ε m
Split, 8

11	ALL(c):ALL(d):[c ε n & d ε m => g(c,d) ε m]
Split, 8

Apply the Cartesian Product Axiom to construct nm  (n x m)

12	ALL(a1):ALL(a2):[Set(a1) & Set(a2) => EXIST(b):[Set'(b) & ALL(c1):ALL(c2):[(c1,c2) ε b <=> c1 ε a1 & c2 ε a2]]]
Cart Prod

13	ALL(a2):[Set(n) & Set(a2) => EXIST(b):[Set'(b) & ALL(c1):ALL(c2):[(c1,c2) ε b <=> c1 ε n & c2 ε a2]]]
U Spec, 12

14	Set(n) & Set(m) => EXIST(b):[Set'(b) & ALL(c1):ALL(c2):[(c1,c2) ε b <=> c1 ε n & c2 ε m]]
U Spec, 13

15	Set(n) & Set(m)
Join, 1, 9

16	EXIST(b):[Set'(b) & ALL(c1):ALL(c2):[(c1,c2) ε b <=> c1 ε n & c2 ε m]]
Detach, 14, 15

17	Set'(nm) & ALL(c1):ALL(c2):[(c1,c2) ε nm <=> c1 ε n & c2 ε m]
E Spec, 16

Define: nm   (n x m)

18	Set'(nm)
Split, 17

19	ALL(c1):ALL(c2):[(c1,c2) ε nm <=> c1 ε n & c2 ε m]
Split, 17

Apply the Power Set Axiom to construct pnm

20	ALL(a):[Set'(a) => EXIST(b):[Set(b)
& ALL(c):[c ε b <=> Set'(c) & ALL(d1):ALL(d2):[(d1,d2) ε c => (d1,d2) ε a]]]]
Power Set

21	Set'(nm) => EXIST(b):[Set(b)
& ALL(c):[c ε b <=> Set'(c) & ALL(d1):ALL(d2):[(d1,d2) ε c => (d1,d2) ε nm]]]
U Spec, 20

22	EXIST(b):[Set(b)
& ALL(c):[c ε b <=> Set'(c) & ALL(d1):ALL(d2):[(d1,d2) ε c => (d1,d2) ε nm]]]
Detach, 21, 18

23	Set(pnm)
& ALL(c):[c ε pnm <=> Set'(c) & ALL(d1):ALL(d2):[(d1,d2) ε c => (d1,d2) ε nm]]
E Spec, 22

Define: pnm   (power set of nm)

24	Set(pnm)
Split, 23

25	ALL(c):[c ε pnm <=> Set'(c) & ALL(d1):ALL(d2):[(d1,d2) ε c => (d1,d2) ε nm]]
Split, 23

Apply the Subset Axiom to construct s

26	EXIST(sub):[Set(sub) & ALL(a):[a ε sub <=> a ε pnm & [(1,m1) ε a & ALL(b):ALL(c):[(b,c) ε a => (b+1,g(b+1,c)) ε a]]]]
Subset, 24

27	Set(s) & ALL(a):[a ε s <=> a ε pnm & [(1,m1) ε a & ALL(b):ALL(c):[(b,c) ε a => (b+1,g(b+1,c)) ε a]]]
E Spec, 26

Define: s

28	Set(s)
Split, 27

29	ALL(a):[a ε s <=> a ε pnm & [(1,m1) ε a & ALL(b):ALL(c):[(b,c) ε a => (b+1,g(b+1,c)) ε a]]]
Split, 27

Apply the Subset Axiom to construct f

30	EXIST(sub):[Set'(sub) & ALL(a):ALL(b):[(a,b) ε sub <=> (a,b) ε nm & ALL(c):[c ε s => (a,b) ε c]]]
Subset, 18

31	Set'(f) & ALL(a):ALL(b):[(a,b) ε f <=> (a,b) ε nm & ALL(c):[c ε s => (a,b) ε c]]
E Spec, 30

Define: f

32	Set'(f)
Split, 31

33	ALL(a):ALL(b):[(a,b) ε f <=> (a,b) ε nm & ALL(c):[c ε s => (a,b) ε c]]
Split, 31

34	ALL(f):ALL(a):ALL(b):[ALL(c):ALL(d):[(c,d) ε f => c ε a & d ε b]
& ALL(c):[c ε a => EXIST(d):[d ε b & (c,d) ε f]]
& ALL(c):ALL(d1):ALL(d2):[(c,d1) ε f & (c,d2) ε f => d1=d2]
=> ALL(c):ALL(d):[d=f(c) <=> (c,d) ε f]]
Function

35	ALL(a):ALL(b):[ALL(c):ALL(d):[(c,d) ε f => c ε a & d ε b]
& ALL(c):[c ε a => EXIST(d):[d ε b & (c,d) ε f]]
& ALL(c):ALL(d1):ALL(d2):[(c,d1) ε f & (c,d2) ε f => d1=d2]
=> ALL(c):ALL(d):[d=f(c) <=> (c,d) ε f]]
U Spec, 34

36	ALL(b):[ALL(c):ALL(d):[(c,d) ε f => c ε n & d ε b]
& ALL(c):[c ε n => EXIST(d):[d ε b & (c,d) ε f]]
& ALL(c):ALL(d1):ALL(d2):[(c,d1) ε f & (c,d2) ε f => d1=d2]
=> ALL(c):ALL(d):[d=f(c) <=> (c,d) ε f]]
U Spec, 35

Sufficient: Functionality of f

37	ALL(c):ALL(d):[(c,d) ε f => c ε n & d ε m]
& ALL(c):[c ε n => EXIST(d):[d ε m & (c,d) ε f]]
& ALL(c):ALL(d1):ALL(d2):[(c,d1) ε f & (c,d2) ε f => d1=d2]
=> ALL(c):ALL(d):[d=f(c) <=> (c,d) ε f]
U Spec, 36

38	(x,y) ε f
Premise

39	ALL(b):[(x,b) ε f <=> (x,b) ε nm & ALL(c):[c ε s => (x,b) ε c]]
U Spec, 33

40	(x,y) ε f <=> (x,y) ε nm & ALL(c):[c ε s => (x,y) ε c]
U Spec, 39

41	[(x,y) ε f => (x,y) ε nm & ALL(c):[c ε s => (x,y) ε c]]
& [(x,y) ε nm & ALL(c):[c ε s => (x,y) ε c] => (x,y) ε f]
Iff-And, 40

42	(x,y) ε f => (x,y) ε nm & ALL(c):[c ε s => (x,y) ε c]
Split, 41

43	(x,y) ε nm & ALL(c):[c ε s => (x,y) ε c] => (x,y) ε f
Split, 41

44	(x,y) ε nm & ALL(c):[c ε s => (x,y) ε c]
Detach, 42, 38

45	(x,y) ε nm
Split, 44

Functionality, Part 1

As Required:

46	ALL(c):ALL(d):[(c,d) ε f => (c,d) ε nm]
Conclusion, 38
Sufficient: For Functionality, Part 2

47	EXIST(d):[d ε m & (1,d) ε f]
& ALL(c):[c ε n & EXIST(d):[d ε m & (c,d) ε f] => EXIST(d):[d ε m & (c+1,d) ε f]]
=> ALL(c):[c ε n => EXIST(d):[d ε m & (c,d) ε f]]
Induction

48	ALL(b):[(1,b) ε f <=> (1,b) ε nm & ALL(c):[c ε s => (1,b) ε c]]
U Spec, 33

49	(1,m1) ε f <=> (1,m1) ε nm & ALL(c):[c ε s => (1,m1) ε c]
U Spec, 48

50	[(1,m1) ε f => (1,m1) ε nm & ALL(c):[c ε s => (1,m1) ε c]]
& [(1,m1) ε nm & ALL(c):[c ε s => (1,m1) ε c] => (1,m1) ε f]
Iff-And, 49

51	(1,m1) ε f => (1,m1) ε nm & ALL(c):[c ε s => (1,m1) ε c]
Split, 50

Sufficient: (1,m1) ε f

52	(1,m1) ε nm & ALL(c):[c ε s => (1,m1) ε c] => (1,m1) ε f
Split, 50

53	ALL(c2):[(1,c2) ε nm <=> 1 ε n & c2 ε m]
U Spec, 19

54	(1,m1) ε nm <=> 1 ε n & m1 ε m
U Spec, 53

55	[(1,m1) ε nm => 1 ε n & m1 ε m]
& [1 ε n & m1 ε m => (1,m1) ε nm]
Iff-And, 54

56	(1,m1) ε nm => 1 ε n & m1 ε m
Split, 55

57	1 ε n & m1 ε m => (1,m1) ε nm
Split, 55

58	1 ε n & m1 ε m
Join, 2, 10

59	(1,m1) ε nm
Detach, 57, 58

Suppose...

60	t ε s
Premise

61	t ε s <=> t ε pnm & [(1,m1) ε t & ALL(b):ALL(c):[(b,c) ε t => (b+1,g(b+1,c)) ε t]]
U Spec, 29

62	[t ε s => t ε pnm & [(1,m1) ε t & ALL(b):ALL(c):[(b,c) ε t => (b+1,g(b+1,c)) ε t]]]
& [t ε pnm & [(1,m1) ε t & ALL(b):ALL(c):[(b,c) ε t => (b+1,g(b+1,c)) ε t]] => t ε s]
Iff-And, 61

63	t ε s => t ε pnm & [(1,m1) ε t & ALL(b):ALL(c):[(b,c) ε t => (b+1,g(b+1,c)) ε t]]
Split, 62

64	t ε pnm & [(1,m1) ε t & ALL(b):ALL(c):[(b,c) ε t => (b+1,g(b+1,c)) ε t]] => t ε s
Split, 62

65	t ε pnm & [(1,m1) ε t & ALL(b):ALL(c):[(b,c) ε t => (b+1,g(b+1,c)) ε t]]
Detach, 63, 60

66	t ε pnm
Split, 65

67	(1,m1) ε t & ALL(b):ALL(c):[(b,c) ε t => (b+1,g(b+1,c)) ε t]
Split, 65

68	(1,m1) ε t
Split, 67

69	ALL(c):[c ε s => (1,m1) ε c]
Conclusion, 60
70	(1,m1) ε nm & ALL(c):[c ε s => (1,m1) ε c]
Join, 59, 69

71	(1,m1) ε f
Detach, 52, 70

72	m1 ε m & (1,m1) ε f
Join, 10, 71

Base Case
---------

As Required:

73	EXIST(d):[d ε m & (1,d) ε f]
E Gen, 72

Inductive Case
--------------

Suppose...

74	x ε n & EXIST(d):[d ε m & (x,d) ε f]
Premise

75	x ε n
Split, 74

76	EXIST(d):[d ε m & (x,d) ε f]
Split, 74

77	y ε m & (x,y) ε f
E Spec, 76

Define: y

78	y ε m
Split, 77

79	(x,y) ε f
Split, 77

80	ALL(b):[(x,b) ε f <=> (x,b) ε nm & ALL(c):[c ε s => (x,b) ε c]]
U Spec, 33

81	(x,y) ε f <=> (x,y) ε nm & ALL(c):[c ε s => (x,y) ε c]
U Spec, 80

82	[(x,y) ε f => (x,y) ε nm & ALL(c):[c ε s => (x,y) ε c]]
& [(x,y) ε nm & ALL(c):[c ε s => (x,y) ε c] => (x,y) ε f]
Iff-And, 81

83	(x,y) ε f => (x,y) ε nm & ALL(c):[c ε s => (x,y) ε c]
Split, 82

84	(x,y) ε nm & ALL(c):[c ε s => (x,y) ε c] => (x,y) ε f
Split, 82

85	(x,y) ε nm & ALL(c):[c ε s => (x,y) ε c]
Detach, 83, 79

86	(x,y) ε nm
Split, 85

87	ALL(c):[c ε s => (x,y) ε c]
Split, 85

88	ALL(b):[(x+1,b) ε f <=> (x+1,b) ε nm & ALL(c):[c ε s => (x+1,b) ε c]]
U Spec, 33

89	(x+1,g(x+1,y)) ε f <=> (x+1,g(x+1,y)) ε nm & ALL(c):[c ε s => (x+1,g(x+1,y)) ε c]
U Spec, 88

90	[(x+1,g(x+1,y)) ε f => (x+1,g(x+1,y)) ε nm & ALL(c):[c ε s => (x+1,g(x+1,y)) ε c]]
& [(x+1,g(x+1,y)) ε nm & ALL(c):[c ε s => (x+1,g(x+1,y)) ε c] => (x+1,g(x+1,y)) ε f]
Iff-And, 89

91	(x+1,g(x+1,y)) ε f => (x+1,g(x+1,y)) ε nm & ALL(c):[c ε s => (x+1,g(x+1,y)) ε c]
Split, 90

Sufficient: (x+1,g(x+1,y)) ε f

92	(x+1,g(x+1,y)) ε nm & ALL(c):[c ε s => (x+1,g(x+1,y)) ε c] => (x+1,g(x+1,y)) ε f
Split, 90

93	ALL(c2):[(x+1,c2) ε nm <=> x+1 ε n & c2 ε m]
U Spec, 19

94	(x+1,g(x+1,y)) ε nm <=> x+1 ε n & g(x+1,y) ε m
U Spec, 93

95	[(x+1,g(x+1,y)) ε nm => x+1 ε n & g(x+1,y) ε m]
& [x+1 ε n & g(x+1,y) ε m => (x+1,g(x+1,y)) ε nm]
Iff-And, 94

96	(x+1,g(x+1,y)) ε nm => x+1 ε n & g(x+1,y) ε m
Split, 95

97	x+1 ε n & g(x+1,y) ε m => (x+1,g(x+1,y)) ε nm
Split, 95

98	ALL(b):[x ε n & b ε n => x+b ε n]
U Spec, 3

99	x ε n & 1 ε n => x+1 ε n
U Spec, 98

100	x ε n & 1 ε n
Join, 75, 2

101	x+1 ε n
Detach, 99, 100

102	ALL(d):[x+1 ε n & d ε m => g(x+1,d) ε m]
U Spec, 11

103	x+1 ε n & y ε m => g(x+1,y) ε m
U Spec, 102

104	x+1 ε n & y ε m
Join, 101, 78

105	g(x+1,y) ε m
Detach, 103, 104

106	x+1 ε n & g(x+1,y) ε m
Join, 101, 105

107	(x+1,g(x+1,y)) ε nm
Detach, 97, 106

Supppose...

108	t ε s
Premise

109	t ε s <=> t ε pnm & [(1,m1) ε t & ALL(b):ALL(c):[(b,c) ε t => (b+1,g(b+1,c)) ε t]]
U Spec, 29

110	[t ε s => t ε pnm & [(1,m1) ε t & ALL(b):ALL(c):[(b,c) ε t => (b+1,g(b+1,c)) ε t]]]
& [t ε pnm & [(1,m1) ε t & ALL(b):ALL(c):[(b,c) ε t => (b+1,g(b+1,c)) ε t]] => t ε s]
Iff-And, 109

111	t ε s => t ε pnm & [(1,m1) ε t & ALL(b):ALL(c):[(b,c) ε t => (b+1,g(b+1,c)) ε t]]
Split, 110

112	t ε pnm & [(1,m1) ε t & ALL(b):ALL(c):[(b,c) ε t => (b+1,g(b+1,c)) ε t]] => t ε s
Split, 110

113	t ε pnm & [(1,m1) ε t & ALL(b):ALL(c):[(b,c) ε t => (b+1,g(b+1,c)) ε t]]
Detach, 111, 108

114	t ε pnm
Split, 113

115	(1,m1) ε t & ALL(b):ALL(c):[(b,c) ε t => (b+1,g(b+1,c)) ε t]
Split, 113

116	(1,m1) ε t
Split, 115

117	ALL(b):ALL(c):[(b,c) ε t => (b+1,g(b+1,c)) ε t]
Split, 115

118	ALL(c):[(x,c) ε t => (x+1,g(x+1,c)) ε t]
U Spec, 117

119	(x,y) ε t => (x+1,g(x+1,y)) ε t
U Spec, 118

120	t ε s => (x,y) ε t
U Spec, 87

121	(x,y) ε t
Detach, 120, 108

122	(x+1,g(x+1,y)) ε t
Detach, 119, 121

123	ALL(c):[c ε s => (x+1,g(x+1,y)) ε c]
Conclusion, 108
124	(x+1,g(x+1,y)) ε nm
& ALL(c):[c ε s => (x+1,g(x+1,y)) ε c]
Join, 107, 123

125	(x+1,g(x+1,y)) ε f
Detach, 92, 124

126	g(x+1,y) ε m & (x+1,g(x+1,y)) ε f
Join, 105, 125

127	EXIST(d):[d ε m & (x+1,d) ε f]
E Gen, 126

Inductive Case
--------------

As Required:

128	ALL(c):[c ε n & EXIST(d):[d ε m & (c,d) ε f]
=> EXIST(d):[d ε m & (c+1,d) ε f]]
Conclusion, 74
129	EXIST(d):[d ε m & (1,d) ε f]
& ALL(c):[c ε n & EXIST(d):[d ε m & (c,d) ε f]
=> EXIST(d):[d ε m & (c+1,d) ε f]]
Join, 73, 128

Functionality, Part 2

As Required:

130	ALL(c):[c ε n => EXIST(d):[d ε m & (c,d) ε f]]
Detach, 47, 129

Sufficient: For Functionality, Part 3

131	ALL(d1):ALL(d2):[(1,d1) ε f & (1,d2) ε f => d1=d2]
& ALL(c):[c ε n & ALL(d1):ALL(d2):[(c,d1) ε f & (c,d2) ε f => d1=d2] => ALL(d1):ALL(d2):[(c+1,d1) ε f & (c+1,d2) ε f => d1=d2]]
=> ALL(c):[c ε n => ALL(d1):ALL(d2):[(c,d1) ε f & (c,d2) ε f => d1=d2]]
Induction

Suppose to contrary...

132	(1,y) ε f & ~y=m1
Premise

133	(1,y) ε f
Split, 132

134	~y=m1
Split, 132

135	ALL(b):[(1,b) ε f <=> (1,b) ε nm & ALL(c):[c ε s => (1,b) ε c]]
U Spec, 33

136	(1,y) ε f <=> (1,y) ε nm & ALL(c):[c ε s => (1,y) ε c]
U Spec, 135

137	[(1,y) ε f => (1,y) ε nm & ALL(c):[c ε s => (1,y) ε c]]
& [(1,y) ε nm & ALL(c):[c ε s => (1,y) ε c] => (1,y) ε f]
Iff-And, 136

138	(1,y) ε f => (1,y) ε nm & ALL(c):[c ε s => (1,y) ε c]
Split, 137

139	(1,y) ε nm & ALL(c):[c ε s => (1,y) ε c] => (1,y) ε f
Split, 137

140	(1,y) ε nm & ALL(c):[c ε s => (1,y) ε c]
Detach, 138, 133

141	(1,y) ε nm
Split, 140

142	ALL(c):[c ε s => (1,y) ε c]
Split, 140

143	ALL(c2):[(1,c2) ε nm <=> 1 ε n & c2 ε m]
U Spec, 19

144	(1,y) ε nm <=> 1 ε n & y ε m
U Spec, 143

145	[(1,y) ε nm => 1 ε n & y ε m]
& [1 ε n & y ε m => (1,y) ε nm]
Iff-And, 144

146	(1,y) ε nm => 1 ε n & y ε m
Split, 145

147	1 ε n & y ε m => (1,y) ε nm
Split, 145

148	1 ε n & y ε m
Detach, 146, 141

149	1 ε n
Split, 148

150	y ε m
Split, 148

151	~EXIST(c):~[c ε s => (1,y) ε c]
Quant, 142

152	~EXIST(c):~~[c ε s & ~(1,y) ε c]
Imply-And, 151

Obtain a contradiction by constructing a subset f' of n2 that excludes (1,y)
and is an element of s.

153	~EXIST(c):[c ε s & ~(1,y) ε c]
Rem DNeg, 152

154	EXIST(sub):[Set'(sub) & ALL(a):ALL(b):[(a,b) ε sub <=> (a,b) ε nm & ~[a=1 & b=y]]]
Subset, 18

155	Set'(f') & ALL(a):ALL(b):[(a,b) ε f' <=> (a,b) ε nm & ~[a=1 & b=y]]
E Spec, 154

Define: f'

Prove: f' ε s

156	Set'(f')
Split, 155

157	ALL(a):ALL(b):[(a,b) ε f' <=> (a,b) ε nm & ~[a=1 & b=y]]
Split, 155

158	f' ε s <=> f' ε pnm & [(1,m1) ε f' & ALL(b):ALL(c):[(b,c) ε f' => (b+1,g(b+1,c)) ε f']]
U Spec, 29

159	[f' ε s => f' ε pnm & [(1,m1) ε f' & ALL(b):ALL(c):[(b,c) ε f' => (b+1,g(b+1,c)) ε f']]]
& [f' ε pnm & [(1,m1) ε f' & ALL(b):ALL(c):[(b,c) ε f' => (b+1,g(b+1,c)) ε f']] => f' ε s]
Iff-And, 158

160	f' ε s => f' ε pnm & [(1,m1) ε f' & ALL(b):ALL(c):[(b,c) ε f' => (b+1,g(b+1,c)) ε f']]
Split, 159

Sufficient: f' ε s

161	f' ε pnm & [(1,m1) ε f' & ALL(b):ALL(c):[(b,c) ε f' => (b+1,g(b+1,c)) ε f']] => f' ε s
Split, 159

162	f' ε pnm <=> Set'(f') & ALL(d1):ALL(d2):[(d1,d2) ε f' => (d1,d2) ε nm]
U Spec, 25

163	[f' ε pnm => Set'(f') & ALL(d1):ALL(d2):[(d1,d2) ε f' => (d1,d2) ε nm]]
& [Set'(f') & ALL(d1):ALL(d2):[(d1,d2) ε f' => (d1,d2) ε nm] => f' ε pnm]
Iff-And, 162

164	f' ε pnm => Set'(f') & ALL(d1):ALL(d2):[(d1,d2) ε f' => (d1,d2) ε nm]
Split, 163

Sufficient: f' ε pnm

165	Set'(f') & ALL(d1):ALL(d2):[(d1,d2) ε f' => (d1,d2) ε nm] => f' ε pnm
Split, 163

Suppose...

166	(p,q) ε f'
Premise

167	ALL(b):[(p,b) ε f' <=> (p,b) ε nm & ~[p=1 & b=y]]
U Spec, 157

168	(p,q) ε f' <=> (p,q) ε nm & ~[p=1 & q=y]
U Spec, 167

169	[(p,q) ε f' => (p,q) ε nm & ~[p=1 & q=y]]
& [(p,q) ε nm & ~[p=1 & q=y] => (p,q) ε f']
Iff-And, 168

170	(p,q) ε f' => (p,q) ε nm & ~[p=1 & q=y]
Split, 169

171	(p,q) ε nm & ~[p=1 & q=y] => (p,q) ε f'
Split, 169

172	(p,q) ε nm & ~[p=1 & q=y]
Detach, 170, 166

173	(p,q) ε nm
Split, 172

174	ALL(d1):ALL(d2):[(d1,d2) ε f' => (d1,d2) ε nm]
Conclusion, 166
175	Set'(f')
& ALL(d1):ALL(d2):[(d1,d2) ε f' => (d1,d2) ε nm]
Join, 156, 174

176	f' ε pnm
Detach, 165, 175

177	ALL(b):[(1,b) ε f' <=> (1,b) ε nm & ~[1=1 & b=y]]
U Spec, 157

178	(1,m1) ε f' <=> (1,m1) ε nm & ~[1=1 & m1=y]
U Spec, 177

179	[(1,m1) ε f' => (1,m1) ε nm & ~[1=1 & m1=y]]
& [(1,m1) ε nm & ~[1=1 & m1=y] => (1,m1) ε f']
Iff-And, 178

180	(1,m1) ε f' => (1,m1) ε nm & ~[1=1 & m1=y]
Split, 179

181	(1,m1) ε nm & ~[1=1 & m1=y] => (1,m1) ε f'
Split, 179

182	(1,m1) ε nm & ~~[~1=1 | ~m1=y] => (1,m1) ε f'
DeMorgan, 181

Sufficient: (1,m1) ε f'

183	(1,m1) ε nm & [~1=1 | ~m1=y] => (1,m1) ε f'
Rem DNeg, 182

184	ALL(c2):[(1,c2) ε nm <=> 1 ε n & c2 ε m]
U Spec, 19

185	(1,m1) ε nm <=> 1 ε n & m1 ε m
U Spec, 184

186	[(1,m1) ε nm => 1 ε n & m1 ε m]
& [1 ε n & m1 ε m => (1,m1) ε nm]
Iff-And, 185

187	(1,m1) ε nm => 1 ε n & m1 ε m
Split, 186

188	1 ε n & m1 ε m => (1,m1) ε nm
Split, 186

189	1 ε n & m1 ε m
Join, 2, 10

190	(1,m1) ε nm
Detach, 188, 189

191	~m1=y
Sym, 134

192	~1=1 | ~m1=y
Arb Or, 191

193	(1,m1) ε nm & [~1=1 | ~m1=y]
Join, 190, 192

194	(1,m1) ε f'
Detach, 183, 193

Suppose...

195	(p,q) ε f'
Premise

196	ALL(b):[(p,b) ε f' <=> (p,b) ε nm & ~[p=1 & b=y]]
U Spec, 157

197	(p,q) ε f' <=> (p,q) ε nm & ~[p=1 & q=y]
U Spec, 196

198	[(p,q) ε f' => (p,q) ε nm & ~[p=1 & q=y]]
& [(p,q) ε nm & ~[p=1 & q=y] => (p,q) ε f']
Iff-And, 197

199	(p,q) ε f' => (p,q) ε nm & ~[p=1 & q=y]
Split, 198

200	(p,q) ε nm & ~[p=1 & q=y] => (p,q) ε f'
Split, 198

201	(p,q) ε nm & ~[p=1 & q=y]
Detach, 199, 195

202	(p,q) ε nm
Split, 201

203	~[p=1 & q=y]
Split, 201

204	ALL(c2):[(p,c2) ε nm <=> p ε n & c2 ε m]
U Spec, 19

205	(p,q) ε nm <=> p ε n & q ε m
U Spec, 204

206	[(p,q) ε nm => p ε n & q ε m]
& [p ε n & q ε m => (p,q) ε nm]
Iff-And, 205

207	(p,q) ε nm => p ε n & q ε m
Split, 206

208	p ε n & q ε m => (p,q) ε nm
Split, 206

209	p ε n & q ε m
Detach, 207, 202

210	p ε n
Split, 209

211	q ε m
Split, 209

212	ALL(b):[(p+1,b) ε f' <=> (p+1,b) ε nm & ~[p+1=1 & b=y]]
U Spec, 157

213	(p+1,g(p+1,q)) ε f' <=> (p+1,g(p+1,q)) ε nm & ~[p+1=1 & g(p+1,q)=y]
U Spec, 212

214	[(p+1,g(p+1,q)) ε f' => (p+1,g(p+1,q)) ε nm & ~[p+1=1 & g(p+1,q)=y]]
& [(p+1,g(p+1,q)) ε nm & ~[p+1=1 & g(p+1,q)=y] => (p+1,g(p+1,q)) ε f']
Iff-And, 213

215	(p+1,g(p+1,q)) ε f' => (p+1,g(p+1,q)) ε nm & ~[p+1=1 & g(p+1,q)=y]
Split, 214

216	(p+1,g(p+1,q)) ε nm & ~[p+1=1 & g(p+1,q)=y] => (p+1,g(p+1,q)) ε f'
Split, 214

217	(p+1,g(p+1,q)) ε nm & ~~[~p+1=1 | ~g(p+1,q)=y] => (p+1,g(p+1,q)) ε f'
DeMorgan, 216

Sufficient: (p+1,g(p+1,q)) ε f'

218	(p+1,g(p+1,q)) ε nm & [~p+1=1 | ~g(p+1,q)=y] => (p+1,g(p+1,q)) ε f'
Rem DNeg, 217

219	ALL(c2):[(p+1,c2) ε nm <=> p+1 ε n & c2 ε m]
U Spec, 19

220	(p+1,g(p+1,q)) ε nm <=> p+1 ε n & g(p+1,q) ε m
U Spec, 219

221	[(p+1,g(p+1,q)) ε nm => p+1 ε n & g(p+1,q) ε m]
& [p+1 ε n & g(p+1,q) ε m => (p+1,g(p+1,q)) ε nm]
Iff-And, 220

222	(p+1,g(p+1,q)) ε nm => p+1 ε n & g(p+1,q) ε m
Split, 221

Sufficient: (p+1,g(p+1,q)) ε nm

223	p+1 ε n & g(p+1,q) ε m => (p+1,g(p+1,q)) ε nm
Split, 221

224	ALL(b):[p ε n & b ε n => p+b ε n]
U Spec, 3

225	p ε n & 1 ε n => p+1 ε n
U Spec, 224

226	p ε n & 1 ε n
Join, 210, 2

227	p+1 ε n
Detach, 225, 226

228	ALL(d):[p+1 ε n & d ε m => g(p+1,d) ε m]
U Spec, 11

229	p+1 ε n & q ε m => g(p+1,q) ε m
U Spec, 228

230	p+1 ε n & q ε m
Join, 227, 211

231	g(p+1,q) ε m
Detach, 229, 230

232	p+1 ε n & g(p+1,q) ε m
Join, 227, 231

233	(p+1,g(p+1,q)) ε nm
Detach, 223, 232

234	p ε n => ~p+1=1
U Spec, 4

235	~p+1=1
Detach, 234, 210

236	~p+1=1 | ~g(p+1,q)=y
Arb Or, 235

237	(p+1,g(p+1,q)) ε nm & [~p+1=1 | ~g(p+1,q)=y]
Join, 233, 236

238	(p+1,g(p+1,q)) ε f'
Detach, 218, 237

239	ALL(b):ALL(c):[(b,c) ε f' => (b+1,g(b+1,c)) ε f']
Conclusion, 195
240	(1,m1) ε f'
& ALL(b):ALL(c):[(b,c) ε f' => (b+1,g(b+1,c)) ε f']
Join, 194, 239

241	f' ε pnm
& [(1,m1) ε f'
& ALL(b):ALL(c):[(b,c) ε f' => (b+1,g(b+1,c)) ε f']]
Join, 176, 240

242	f' ε s
Detach, 161, 241

243	ALL(b):[(1,b) ε f' <=> (1,b) ε nm & ~[1=1 & b=y]]
U Spec, 157

244	(1,y) ε f' <=> (1,y) ε nm & ~[1=1 & y=y]
U Spec, 243

245	[(1,y) ε f' => (1,y) ε nm & ~[1=1 & y=y]]
& [(1,y) ε nm & ~[1=1 & y=y] => (1,y) ε f']
Iff-And, 244

246	(1,y) ε f' => (1,y) ε nm & ~[1=1 & y=y]
Split, 245

247	(1,y) ε nm & ~[1=1 & y=y] => (1,y) ε f'
Split, 245

Sufficient: ~(1,y) ε f'  (line 332 in factorial.proof)

248	~[(1,y) ε nm & ~[1=1 & y=y]] => ~(1,y) ε f'
Contra, 246

249	~~[~(1,y) ε nm | ~~[1=1 & y=y]] => ~(1,y) ε f'
DeMorgan, 248

250	~(1,y) ε nm | ~~[1=1 & y=y] => ~(1,y) ε f'
Rem DNeg, 249

251	~(1,y) ε nm | 1=1 & y=y => ~(1,y) ε f'
Rem DNeg, 250

252	1=1
Reflex

253	y=y
Reflex

254	1=1 & y=y
Join, 252, 253

255	~(1,y) ε nm | 1=1 & y=y
Arb Or, 254

256	~(1,y) ε f'
Detach, 251, 255

257	f' ε s & ~(1,y) ε f'
Join, 242, 256

258	EXIST(c):[c ε s & ~(1,y) ε c]
E Gen, 257

259	EXIST(c):[c ε s & ~(1,y) ε c]
& ~EXIST(c):[c ε s & ~(1,y) ε c]
Join, 258, 153

260	ALL(b):~[(1,b) ε f & ~b=m1]
Conclusion, 132
261	ALL(b):~~[(1,b) ε f => ~~b=m1]
Imply-And, 260

262	ALL(b):[(1,b) ε f => ~~b=m1]
Rem DNeg, 261

263	ALL(b):[(1,b) ε f => b=m1]
Rem DNeg, 262

Suppose...

264	(1,y) ε f & (1,y') ε f
Premise

265	(1,y) ε f
Split, 264

266	(1,y') ε f
Split, 264

267	(1,y) ε f => y=m1
U Spec, 263

268	y=m1
Detach, 267, 265

269	(1,y') ε f => y'=m1
U Spec, 263

270	y'=m1
Detach, 269, 266

271	y=y'
Substitute, 270, 268

Base Step
---------

As Required:

272	ALL(d1):ALL(d2):[(1,d1) ε f & (1,d2) ε f => d1=d2]
Conclusion, 264
Inductive Step
--------------

Suppose...

273	x ε n & ALL(d1):ALL(d2):[(x,d1) ε f & (x,d2) ε f => d1=d2]
Premise

274	x ε n
Split, 273

275	ALL(d1):ALL(d2):[(x,d1) ε f & (x,d2) ε f => d1=d2]
Split, 273

Prove: ALL(a):[(x,a) ε f => ALL(b):[(x+1,b) ε f => b=g(x+1,a)]]  (line 357 of factorial.proof)

Suppose...

276	(x,y) ε f
Premise

277	ALL(b):[(x,b) ε f <=> (x,b) ε nm & ALL(c):[c ε s => (x,b) ε c]]
U Spec, 33

278	(x,y) ε f <=> (x,y) ε nm & ALL(c):[c ε s => (x,y) ε c]
U Spec, 277

279	[(x,y) ε f => (x,y) ε nm & ALL(c):[c ε s => (x,y) ε c]]
& [(x,y) ε nm & ALL(c):[c ε s => (x,y) ε c] => (x,y) ε f]
Iff-And, 278

280	(x,y) ε f => (x,y) ε nm & ALL(c):[c ε s => (x,y) ε c]
Split, 279

281	(x,y) ε nm & ALL(c):[c ε s => (x,y) ε c] => (x,y) ε f
Split, 279

282	(x,y) ε nm & ALL(c):[c ε s => (x,y) ε c]
Detach, 280, 276

283	(x,y) ε nm
Split, 282

284	ALL(c):[c ε s => (x,y) ε c]
Split, 282

285	ALL(c2):[(x,c2) ε nm <=> x ε n & c2 ε m]
U Spec, 19

286	(x,y) ε nm <=> x ε n & y ε m
U Spec, 285

287	[(x,y) ε nm => x ε n & y ε m]
& [x ε n & y ε m => (x,y) ε nm]
Iff-And, 286

288	(x,y) ε nm => x ε n & y ε m
Split, 287

289	x ε n & y ε m => (x,y) ε nm
Split, 287

290	x ε n & y ε m
Detach, 288, 283

291	x ε n
Split, 290

292	y ε m
Split, 290

Suppose...

293	(x+1,y') ε f & ~y'=g(x+1,y)
Premise

294	(x+1,y') ε f
Split, 293

295	~y'=g(x+1,y)
Split, 293

296	ALL(b):[(x+1,b) ε f <=> (x+1,b) ε nm & ALL(c):[c ε s => (x+1,b) ε c]]
U Spec, 33

297	(x+1,y') ε f <=> (x+1,y') ε nm & ALL(c):[c ε s => (x+1,y') ε c]
U Spec, 296

298	[(x+1,y') ε f => (x+1,y') ε nm & ALL(c):[c ε s => (x+1,y') ε c]]
& [(x+1,y') ε nm & ALL(c):[c ε s => (x+1,y') ε c] => (x+1,y') ε f]
Iff-And, 297

299	(x+1,y') ε f => (x+1,y') ε nm & ALL(c):[c ε s => (x+1,y') ε c]
Split, 298

300	(x+1,y') ε nm & ALL(c):[c ε s => (x+1,y') ε c] => (x+1,y') ε f
Split, 298

301	(x+1,y') ε nm & ALL(c):[c ε s => (x+1,y') ε c]
Detach, 299, 294

302	(x+1,y') ε nm
Split, 301

303	ALL(c):[c ε s => (x+1,y') ε c]
Split, 301

304	ALL(c2):[(x+1,c2) ε nm <=> x+1 ε n & c2 ε m]
U Spec, 19

305	(x+1,y') ε nm <=> x+1 ε n & y' ε m
U Spec, 304

306	[(x+1,y') ε nm => x+1 ε n & y' ε m]
& [x+1 ε n & y' ε m => (x+1,y') ε nm]
Iff-And, 305

307	(x+1,y') ε nm => x+1 ε n & y' ε m
Split, 306

308	x+1 ε n & y' ε m => (x+1,y') ε nm
Split, 306

309	x+1 ε n & y' ε m
Detach, 307, 302

310	x+1 ε n
Split, 309

311	y' ε m
Split, 309

312	~EXIST(c):~[c ε s => (x+1,y') ε c]
Quant, 303

313	~EXIST(c):~~[c ε s & ~(x+1,y') ε c]
Imply-And, 312

Obtain a contradiction by proving to the contrary that EXIST(c):[c ε s & ~(x+1,y') ε c]

314	~EXIST(c):[c ε s & ~(x+1,y') ε c]
Rem DNeg, 313

315	EXIST(sub):[Set'(sub) & ALL(a):ALL(b):[(a,b) ε sub <=> (a,b) ε f & ~[a=x+1 & b=y']]]
Subset, 32

316	Set'(f') & ALL(a):ALL(b):[(a,b) ε f' <=> (a,b) ε f & ~[a=x+1 & b=y']]
E Spec, 315

Define: f'

Prove: f' ε s

317	Set'(f')
Split, 316

318	ALL(a):ALL(b):[(a,b) ε f' <=> (a,b) ε f & ~[a=x+1 & b=y']]
Split, 316

319	f' ε s <=> f' ε pnm & [(1,m1) ε f' & ALL(b):ALL(c):[(b,c) ε f' => (b+1,g(b+1,c)) ε f']]
U Spec, 29

320	[f' ε s => f' ε pnm & [(1,m1) ε f' & ALL(b):ALL(c):[(b,c) ε f' => (b+1,g(b+1,c)) ε f']]]
& [f' ε pnm & [(1,m1) ε f' & ALL(b):ALL(c):[(b,c) ε f' => (b+1,g(b+1,c)) ε f']] => f' ε s]
Iff-And, 319

321	f' ε s => f' ε pnm & [(1,m1) ε f' & ALL(b):ALL(c):[(b,c) ε f' => (b+1,g(b+1,c)) ε f']]
Split, 320

Sufficient: f' ε s

322	f' ε pnm & [(1,m1) ε f' & ALL(b):ALL(c):[(b,c) ε f' => (b+1,g(b+1,c)) ε f']] => f' ε s
Split, 320

323	f' ε pnm <=> Set'(f') & ALL(d1):ALL(d2):[(d1,d2) ε f' => (d1,d2) ε nm]
U Spec, 25

324	[f' ε pnm => Set'(f') & ALL(d1):ALL(d2):[(d1,d2) ε f' => (d1,d2) ε nm]]
& [Set'(f') & ALL(d1):ALL(d2):[(d1,d2) ε f' => (d1,d2) ε nm] => f' ε pnm]
Iff-And, 323

325	f' ε pnm => Set'(f') & ALL(d1):ALL(d2):[(d1,d2) ε f' => (d1,d2) ε nm]
Split, 324

Sufficient: f' ε pnm

326	Set'(f') & ALL(d1):ALL(d2):[(d1,d2) ε f' => (d1,d2) ε nm] => f' ε pnm
Split, 324

Suppose...

327	(p,q) ε f'
Premise

328	ALL(b):[(p,b) ε f' <=> (p,b) ε f & ~[p=x+1 & b=y']]
U Spec, 318

329	(p,q) ε f' <=> (p,q) ε f & ~[p=x+1 & q=y']
U Spec, 328

330	[(p,q) ε f' => (p,q) ε f & ~[p=x+1 & q=y']]
& [(p,q) ε f & ~[p=x+1 & q=y'] => (p,q) ε f']
Iff-And, 329

331	(p,q) ε f' => (p,q) ε f & ~[p=x+1 & q=y']
Split, 330

332	(p,q) ε f & ~[p=x+1 & q=y'] => (p,q) ε f'
Split, 330

333	(p,q) ε f & ~[p=x+1 & q=y']
Detach, 331, 327

334	(p,q) ε f
Split, 333

335	~[p=x+1 & q=y']
Split, 333

336	ALL(b):[(p,b) ε f <=> (p,b) ε nm & ALL(c):[c ε s => (p,b) ε c]]
U Spec, 33

337	(p,q) ε f <=> (p,q) ε nm & ALL(c):[c ε s => (p,q) ε c]
U Spec, 336

338	[(p,q) ε f => (p,q) ε nm & ALL(c):[c ε s => (p,q) ε c]]
& [(p,q) ε nm & ALL(c):[c ε s => (p,q) ε c] => (p,q) ε f]
Iff-And, 337

339	(p,q) ε f => (p,q) ε nm & ALL(c):[c ε s => (p,q) ε c]
Split, 338

340	(p,q) ε nm & ALL(c):[c ε s => (p,q) ε c] => (p,q) ε f
Split, 338

341	(p,q) ε nm & ALL(c):[c ε s => (p,q) ε c]
Detach, 339, 334

342	(p,q) ε nm
Split, 341

343	ALL(d1):ALL(d2):[(d1,d2) ε f' => (d1,d2) ε nm]
Conclusion, 327
344	Set'(f')
& ALL(d1):ALL(d2):[(d1,d2) ε f' => (d1,d2) ε nm]
Join, 317, 343

345	f' ε pnm
Detach, 326, 344

346	ALL(b):[(1,b) ε f' <=> (1,b) ε f & ~[1=x+1 & b=y']]
U Spec, 318

347	(1,m1) ε f' <=> (1,m1) ε f & ~[1=x+1 & m1=y']
U Spec, 346

348	[(1,m1) ε f' => (1,m1) ε f & ~[1=x+1 & m1=y']]
& [(1,m1) ε f & ~[1=x+1 & m1=y'] => (1,m1) ε f']
Iff-And, 347

349	(1,m1) ε f' => (1,m1) ε f & ~[1=x+1 & m1=y']
Split, 348

350	(1,m1) ε f & ~[1=x+1 & m1=y'] => (1,m1) ε f'
Split, 348

351	(1,m1) ε f & ~~[~1=x+1 | ~m1=y'] => (1,m1) ε f'
DeMorgan, 350

Sufficient: (1,m1) ε f'

352	(1,m1) ε f & [~1=x+1 | ~m1=y'] => (1,m1) ε f'
Rem DNeg, 351

353	ALL(b):[(1,b) ε f <=> (1,b) ε nm & ALL(c):[c ε s => (1,b) ε c]]
U Spec, 33

354	(1,m1) ε f <=> (1,m1) ε nm & ALL(c):[c ε s => (1,m1) ε c]
U Spec, 353

355	[(1,m1) ε f => (1,m1) ε nm & ALL(c):[c ε s => (1,m1) ε c]]
& [(1,m1) ε nm & ALL(c):[c ε s => (1,m1) ε c] => (1,m1) ε f]
Iff-And, 354

356	(1,m1) ε f => (1,m1) ε nm & ALL(c):[c ε s => (1,m1) ε c]
Split, 355

Sufficient: (1,m1) ε f

357	(1,m1) ε nm & ALL(c):[c ε s => (1,m1) ε c] => (1,m1) ε f
Split, 355

358	ALL(c2):[(1,c2) ε nm <=> 1 ε n & c2 ε m]
U Spec, 19

359	(1,m1) ε nm <=> 1 ε n & m1 ε m
U Spec, 358

360	[(1,m1) ε nm => 1 ε n & m1 ε m]
& [1 ε n & m1 ε m => (1,m1) ε nm]
Iff-And, 359

361	(1,m1) ε nm => 1 ε n & m1 ε m
Split, 360

362	1 ε n & m1 ε m => (1,m1) ε nm
Split, 360

363	1 ε n & m1 ε m
Join, 2, 10

364	(1,m1) ε nm
Detach, 362, 363

365	t ε s
Premise

366	t ε s <=> t ε pnm & [(1,m1) ε t & ALL(b):ALL(c):[(b,c) ε t => (b+1,g(b+1,c)) ε t]]
U Spec, 29

367	[t ε s => t ε pnm & [(1,m1) ε t & ALL(b):ALL(c):[(b,c) ε t => (b+1,g(b+1,c)) ε t]]]
& [t ε pnm & [(1,m1) ε t & ALL(b):ALL(c):[(b,c) ε t => (b+1,g(b+1,c)) ε t]] => t ε s]
Iff-And, 366

368	t ε s => t ε pnm & [(1,m1) ε t & ALL(b):ALL(c):[(b,c) ε t => (b+1,g(b+1,c)) ε t]]
Split, 367

369	t ε pnm & [(1,m1) ε t & ALL(b):ALL(c):[(b,c) ε t => (b+1,g(b+1,c)) ε t]] => t ε s
Split, 367

370	t ε pnm & [(1,m1) ε t & ALL(b):ALL(c):[(b,c) ε t => (b+1,g(b+1,c)) ε t]]
Detach, 368, 365

371	t ε pnm
Split, 370

372	(1,m1) ε t & ALL(b):ALL(c):[(b,c) ε t => (b+1,g(b+1,c)) ε t]
Split, 370

373	(1,m1) ε t
Split, 372

374	ALL(c):[c ε s => (1,m1) ε c]
Conclusion, 365
375	(1,m1) ε nm & ALL(c):[c ε s => (1,m1) ε c]
Join, 364, 374

376	(1,m1) ε f
Detach, 357, 375

377	x ε n => ~x+1=1
U Spec, 4

378	~x+1=1
Detach, 377, 274

379	~1=x+1
Sym, 378

380	~1=x+1 | ~m1=y'
Arb Or, 379

381	(1,m1) ε f & [~1=x+1 | ~m1=y']
Join, 376, 380

382	(1,m1) ε f'
Detach, 352, 381

383	(p,q) ε f'
Premise

384	ALL(b):[(p,b) ε f' <=> (p,b) ε f & ~[p=x+1 & b=y']]
U Spec, 318

385	(p,q) ε f' <=> (p,q) ε f & ~[p=x+1 & q=y']
U Spec, 384

386	[(p,q) ε f' => (p,q) ε f & ~[p=x+1 & q=y']]
& [(p,q) ε f & ~[p=x+1 & q=y'] => (p,q) ε f']
Iff-And, 385

387	(p,q) ε f' => (p,q) ε f & ~[p=x+1 & q=y']
Split, 386

388	(p,q) ε f & ~[p=x+1 & q=y'] => (p,q) ε f'
Split, 386

389	(p,q) ε f & ~[p=x+1 & q=y']
Detach, 387, 383

390	(p,q) ε f
Split, 389

391	~[p=x+1 & q=y']
Split, 389

392	ALL(b):[(p,b) ε f <=> (p,b) ε nm & ALL(c):[c ε s => (p,b) ε c]]
U Spec, 33

393	(p,q) ε f <=> (p,q) ε nm & ALL(c):[c ε s => (p,q) ε c]
U Spec, 392

394	[(p,q) ε f => (p,q) ε nm & ALL(c):[c ε s => (p,q) ε c]]
& [(p,q) ε nm & ALL(c):[c ε s => (p,q) ε c] => (p,q) ε f]
Iff-And, 393

395	(p,q) ε f => (p,q) ε nm & ALL(c):[c ε s => (p,q) ε c]
Split, 394

396	(p,q) ε nm & ALL(c):[c ε s => (p,q) ε c] => (p,q) ε f
Split, 394

397	(p,q) ε nm & ALL(c):[c ε s => (p,q) ε c]
Detach, 395, 390

398	(p,q) ε nm
Split, 397

399	ALL(c):[c ε s => (p,q) ε c]
Split, 397

400	ALL(c2):[(p,c2) ε nm <=> p ε n & c2 ε m]
U Spec, 19

401	(p,q) ε nm <=> p ε n & q ε m
U Spec, 400

402	[(p,q) ε nm => p ε n & q ε m]
& [p ε n & q ε m => (p,q) ε nm]
Iff-And, 401

403	(p,q) ε nm => p ε n & q ε m
Split, 402

404	p ε n & q ε m => (p,q) ε nm
Split, 402

405	p ε n & q ε m
Detach, 403, 398

406	p ε n
Split, 405

407	q ε m
Split, 405

408	ALL(b):[(p,b) ε f' <=> (p,b) ε f & ~[p=x+1 & b=y']]
U Spec, 318

409	(p,q) ε f' <=> (p,q) ε f & ~[p=x+1 & q=y']
U Spec, 408

410	[(p,q) ε f' => (p,q) ε f & ~[p=x+1 & q=y']]
& [(p,q) ε f & ~[p=x+1 & q=y'] => (p,q) ε f']
Iff-And, 409

411	(p,q) ε f' => (p,q) ε f & ~[p=x+1 & q=y']
Split, 410

412	(p,q) ε f & ~[p=x+1 & q=y'] => (p,q) ε f'
Split, 410

413	(p,q) ε f & ~[p=x+1 & q=y']
Detach, 411, 383

414	(p,q) ε f
Split, 413

415	~[p=x+1 & q=y']
Split, 413

416	ALL(b):[(p+1,b) ε f' <=> (p+1,b) ε f & ~[p+1=x+1 & b=y']]
U Spec, 318

417	(p+1,g(p+1,q)) ε f' <=> (p+1,g(p+1,q)) ε f & ~[p+1=x+1 & g(p+1,q)=y']
U Spec, 416

418	[(p+1,g(p+1,q)) ε f' => (p+1,g(p+1,q)) ε f & ~[p+1=x+1 & g(p+1,q)=y']]
& [(p+1,g(p+1,q)) ε f & ~[p+1=x+1 & g(p+1,q)=y'] => (p+1,g(p+1,q)) ε f']
Iff-And, 417

419	(p+1,g(p+1,q)) ε f' => (p+1,g(p+1,q)) ε f & ~[p+1=x+1 & g(p+1,q)=y']
Split, 418

Sufficient: (p+1,g(p+1,q)) ε f'

420	(p+1,g(p+1,q)) ε f & ~[p+1=x+1 & g(p+1,q)=y'] => (p+1,g(p+1,q)) ε f'
Split, 418

421	ALL(b):[(p+1,b) ε f <=> (p+1,b) ε nm & ALL(c):[c ε s => (p+1,b) ε c]]
U Spec, 33

422	(p+1,g(p+1,q)) ε f <=> (p+1,g(p+1,q)) ε nm & ALL(c):[c ε s => (p+1,g(p+1,q)) ε c]
U Spec, 421

423	[(p+1,g(p+1,q)) ε f => (p+1,g(p+1,q)) ε nm & ALL(c):[c ε s => (p+1,g(p+1,q)) ε c]]
& [(p+1,g(p+1,q)) ε nm & ALL(c):[c ε s => (p+1,g(p+1,q)) ε c] => (p+1,g(p+1,q)) ε f]
Iff-And, 422

424	(p+1,g(p+1,q)) ε f => (p+1,g(p+1,q)) ε nm & ALL(c):[c ε s => (p+1,g(p+1,q)) ε c]
Split, 423

Sufficient: (p+1,g(p+1,q)) ε f

425	(p+1,g(p+1,q)) ε nm & ALL(c):[c ε s => (p+1,g(p+1,q)) ε c] => (p+1,g(p+1,q)) ε f
Split, 423

426	ALL(c2):[(p+1,c2) ε nm <=> p+1 ε n & c2 ε m]
U Spec, 19

427	(p+1,g(p+1,q)) ε nm <=> p+1 ε n & g(p+1,q) ε m
U Spec, 426

428	[(p+1,g(p+1,q)) ε nm => p+1 ε n & g(p+1,q) ε m]
& [p+1 ε n & g(p+1,q) ε m => (p+1,g(p+1,q)) ε nm]
Iff-And, 427

429	(p+1,g(p+1,q)) ε nm => p+1 ε n & g(p+1,q) ε m
Split, 428

430	p+1 ε n & g(p+1,q) ε m => (p+1,g(p+1,q)) ε nm
Split, 428

431	ALL(d):[p+1 ε n & d ε m => g(p+1,d) ε m]
U Spec, 11

432	p+1 ε n & q ε m => g(p+1,q) ε m
U Spec, 431

433	ALL(b):[p ε n & b ε n => p+b ε n]
U Spec, 3

434	p ε n & 1 ε n => p+1 ε n
U Spec, 433

435	p ε n & 1 ε n
Join, 406, 2

436	p+1 ε n
Detach, 434, 435

437	p+1 ε n & q ε m
Join, 436, 407

438	g(p+1,q) ε m
Detach, 432, 437

439	p+1 ε n & g(p+1,q) ε m
Join, 436, 438

440	(p+1,g(p+1,q)) ε nm
Detach, 430, 439

Suppose...

441	t ε s
Premise

442	t ε s <=> t ε pnm & [(1,m1) ε t & ALL(b):ALL(c):[(b,c) ε t => (b+1,g(b+1,c)) ε t]]
U Spec, 29

443	[t ε s => t ε pnm & [(1,m1) ε t & ALL(b):ALL(c):[(b,c) ε t => (b+1,g(b+1,c)) ε t]]]
& [t ε pnm & [(1,m1) ε t & ALL(b):ALL(c):[(b,c) ε t => (b+1,g(b+1,c)) ε t]] => t ε s]
Iff-And, 442

444	t ε s => t ε pnm & [(1,m1) ε t & ALL(b):ALL(c):[(b,c) ε t => (b+1,g(b+1,c)) ε t]]
Split, 443

445	t ε pnm & [(1,m1) ε t & ALL(b):ALL(c):[(b,c) ε t => (b+1,g(b+1,c)) ε t]] => t ε s
Split, 443

446	t ε pnm & [(1,m1) ε t & ALL(b):ALL(c):[(b,c) ε t => (b+1,g(b+1,c)) ε t]]
Detach, 444, 441

447	t ε pnm
Split, 446

448	(1,m1) ε t & ALL(b):ALL(c):[(b,c) ε t => (b+1,g(b+1,c)) ε t]
Split, 446

449	(1,m1) ε t
Split, 448

450	ALL(b):ALL(c):[(b,c) ε t => (b+1,g(b+1,c)) ε t]
Split, 448

451	ALL(c):[(p,c) ε t => (p+1,g(p+1,c)) ε t]
U Spec, 450

452	(p,q) ε t => (p+1,g(p+1,q)) ε t
U Spec, 451

453	t ε s => (p,q) ε t
U Spec, 399

454	(p,q) ε t
Detach, 453, 441

455	(p+1,g(p+1,q)) ε t
Detach, 452, 454

456	ALL(c):[c ε s => (p+1,g(p+1,q)) ε c]
Conclusion, 441
457	(p+1,g(p+1,q)) ε nm
& ALL(c):[c ε s => (p+1,g(p+1,q)) ε c]
Join, 440, 456

458	(p+1,g(p+1,q)) ε f
Detach, 425, 457

459	p+1=x+1
Premise

460	ALL(b):[p ε n & b ε n & p+1=b+1 => p=b]
U Spec, 5

461	p ε n & x ε n & p+1=x+1 => p=x
U Spec, 460

462	p ε n & x ε n
Join, 406, 274

463	p ε n & x ε n & p+1=x+1
Join, 462, 459

464	p=x
Detach, 461, 463

465	(x,q) ε f
Substitute, 464, 414

466	ALL(d2):[(x,q) ε f & (x,d2) ε f => q=d2]
U Spec, 275

467	(x,q) ε f & (x,y) ε f => q=y
U Spec, 466

468	(x,q) ε f & (x,y) ε f
Join, 465, 276

469	q=y
Detach, 467, 468

470	~y'=g(x+1,q)
Substitute, 469, 295

471	~y'=g(p+1,q)
Substitute, 464, 470

472	~g(p+1,q)=y'
Sym, 471

473	p+1=x+1 => ~g(p+1,q)=y'
Conclusion, 459
474	~[p+1=x+1 & ~~g(p+1,q)=y']
Imply-And, 473

475	~[p+1=x+1 & g(p+1,q)=y']
Rem DNeg, 474

476	(p+1,g(p+1,q)) ε f & ~[p+1=x+1 & g(p+1,q)=y']
Join, 458, 475

477	(p+1,g(p+1,q)) ε f'
Detach, 420, 476

478	ALL(b):ALL(c):[(b,c) ε f' => (b+1,g(b+1,c)) ε f']
Conclusion, 383
479	(1,m1) ε f'
& ALL(b):ALL(c):[(b,c) ε f' => (b+1,g(b+1,c)) ε f']
Join, 382, 478

480	f' ε pnm
& [(1,m1) ε f'
& ALL(b):ALL(c):[(b,c) ε f' => (b+1,g(b+1,c)) ε f']]
Join, 345, 479

line 546 in factorial.proof

481	f' ε s
Detach, 322, 480

482	ALL(b):[(x+1,b) ε f' <=> (x+1,b) ε f & ~[x+1=x+1 & b=y']]
U Spec, 318

483	(x+1,y') ε f' <=> (x+1,y') ε f & ~[x+1=x+1 & y'=y']
U Spec, 482

484	[(x+1,y') ε f' => (x+1,y') ε f & ~[x+1=x+1 & y'=y']]
& [(x+1,y') ε f & ~[x+1=x+1 & y'=y'] => (x+1,y') ε f']
Iff-And, 483

485	(x+1,y') ε f' => (x+1,y') ε f & ~[x+1=x+1 & y'=y']
Split, 484

486	(x+1,y') ε f & ~[x+1=x+1 & y'=y'] => (x+1,y') ε f'
Split, 484

Sufficient: ~(x+1,y') ε f'

487	~[(x+1,y') ε f & ~[x+1=x+1 & y'=y']] => ~(x+1,y') ε f'
Contra, 485

488	~~[~(x+1,y') ε f | ~~[x+1=x+1 & y'=y']] => ~(x+1,y') ε f'
DeMorgan, 487

489	~(x+1,y') ε f | ~~[x+1=x+1 & y'=y'] => ~(x+1,y') ε f'
Rem DNeg, 488

490	~(x+1,y') ε f | x+1=x+1 & y'=y' => ~(x+1,y') ε f'
Rem DNeg, 489

491	x+1=x+1
Reflex

492	y'=y'
Reflex

493	x+1=x+1 & y'=y'
Join, 491, 492

494	~(x+1,y') ε f | x+1=x+1 & y'=y'
Arb Or, 493

495	~(x+1,y') ε f'
Detach, 490, 494

496	f' ε s & ~(x+1,y') ε f'
Join, 481, 495

497	EXIST(c):[c ε s & ~(x+1,y') ε c]
E Gen, 496

498	EXIST(c):[c ε s & ~(x+1,y') ε c]
& ~EXIST(c):[c ε s & ~(x+1,y') ε c]
Join, 497, 314

499	ALL(b):~[(x+1,b) ε f & ~b=g(x+1,y)]
Conclusion, 293
500	ALL(b):~~[(x+1,b) ε f => ~~b=g(x+1,y)]
Imply-And, 499

501	ALL(b):[(x+1,b) ε f => ~~b=g(x+1,y)]
Rem DNeg, 500

502	ALL(b):[(x+1,b) ε f => b=g(x+1,y)]
Rem DNeg, 501

503	ALL(a):[(x,a) ε f => ALL(b):[(x+1,b) ε f => b=g(x+1,a)]]
Conclusion, 276
504	x ε n => EXIST(d):[d ε m & (x,d) ε f]
U Spec, 130

505	EXIST(d):[d ε m & (x,d) ε f]
Detach, 504, 274

506	y ε m & (x,y) ε f
E Spec, 505

Define: y

507	y ε m
Split, 506

508	(x,y) ε f
Split, 506

509	(x,y) ε f => ALL(b):[(x+1,b) ε f => b=g(x+1,y)]
U Spec, 503

510	ALL(b):[(x+1,b) ε f => b=g(x+1,y)]
Detach, 509, 508

Suppose...

511	(x+1,y') ε f & (x+1,y'') ε f
Premise

512	(x+1,y') ε f
Split, 511

513	(x+1,y'') ε f
Split, 511

514	(x+1,y') ε f => y'=g(x+1,y)
U Spec, 510

515	y'=g(x+1,y)
Detach, 514, 512

516	(x+1,y'') ε f => y''=g(x+1,y)
U Spec, 510

517	y''=g(x+1,y)
Detach, 516, 513

518	y'=y''
Substitute, 517, 515

519	ALL(d1):ALL(d2):[(x+1,d1) ε f & (x+1,d2) ε f => d1=d2]
Conclusion, 511
Inductive Step
--------------

As Required:

520	ALL(c):[c ε n & ALL(d1):ALL(d2):[(c,d1) ε f & (c,d2) ε f => d1=d2]
=> ALL(d1):ALL(d2):[(c+1,d1) ε f & (c+1,d2) ε f => d1=d2]]
Conclusion, 273
521	ALL(d1):ALL(d2):[(1,d1) ε f & (1,d2) ε f => d1=d2]
& ALL(c):[c ε n & ALL(d1):ALL(d2):[(c,d1) ε f & (c,d2) ε f => d1=d2]
=> ALL(d1):ALL(d2):[(c+1,d1) ε f & (c+1,d2) ε f => d1=d2]]
Join, 272, 520

By induction...

522	ALL(c):[c ε n => ALL(d1):ALL(d2):[(c,d1) ε f & (c,d2) ε f => d1=d2]]
Detach, 131, 521

Suppose...

523	(x,y) ε f & (x,y') ε f
Premise

524	(x,y) ε f
Split, 523

525	(x,y') ε f
Split, 523

526	ALL(b):[(x,b) ε f <=> (x,b) ε nm & ALL(c):[c ε s => (x,b) ε c]]
U Spec, 33

527	(x,y) ε f <=> (x,y) ε nm & ALL(c):[c ε s => (x,y) ε c]
U Spec, 526

528	[(x,y) ε f => (x,y) ε nm & ALL(c):[c ε s => (x,y) ε c]]
& [(x,y) ε nm & ALL(c):[c ε s => (x,y) ε c] => (x,y) ε f]
Iff-And, 527

529	(x,y) ε f => (x,y) ε nm & ALL(c):[c ε s => (x,y) ε c]
Split, 528

530	(x,y) ε nm & ALL(c):[c ε s => (x,y) ε c] => (x,y) ε f
Split, 528

531	(x,y) ε nm & ALL(c):[c ε s => (x,y) ε c]
Detach, 529, 524

532	(x,y) ε nm
Split, 531

533	ALL(c):[c ε s => (x,y) ε c]
Split, 531

534	ALL(c2):[(x,c2) ε nm <=> x ε n & c2 ε m]
U Spec, 19

535	(x,y) ε nm <=> x ε n & y ε m
U Spec, 534

536	[(x,y) ε nm => x ε n & y ε m]
& [x ε n & y ε m => (x,y) ε nm]
Iff-And, 535

537	(x,y) ε nm => x ε n & y ε m
Split, 536

538	x ε n & y ε m => (x,y) ε nm
Split, 536

539	x ε n & y ε m
Detach, 537, 532

540	x ε n
Split, 539

541	y ε m
Split, 539

542	x ε n => ALL(d1):ALL(d2):[(x,d1) ε f & (x,d2) ε f => d1=d2]
U Spec, 522

543	ALL(d1):ALL(d2):[(x,d1) ε f & (x,d2) ε f => d1=d2]
Detach, 542, 540

544	ALL(d2):[(x,y) ε f & (x,d2) ε f => y=d2]
U Spec, 543

545	(x,y) ε f & (x,y') ε f => y=y'
U Spec, 544

546	(x,y) ε f & (x,y') ε f
Join, 524, 525

547	y=y'
Detach, 545, 546

Functionality, Part 3

As Required:

548	ALL(c):ALL(d1):ALL(d2):[(c,d1) ε f & (c,d2) ε f => d1=d2]
Conclusion, 523
549	ALL(c):ALL(d):[(c,d) ε f => (c,d) ε nm]
& ALL(c):[c ε n => EXIST(d):[d ε m & (c,d) ε f]]
Join, 46, 130

550	ALL(c):ALL(d):[(c,d) ε f => (c,d) ε nm]
& ALL(c):[c ε n => EXIST(d):[d ε m & (c,d) ε f]]
& ALL(c):ALL(d1):ALL(d2):[(c,d1) ε f & (c,d2) ε f => d1=d2]
Join, 549, 548

551	(x,y) ε f
Premise

552	ALL(b):[(x,b) ε f <=> (x,b) ε nm & ALL(c):[c ε s => (x,b) ε c]]
U Spec, 33

553	(x,y) ε f <=> (x,y) ε nm & ALL(c):[c ε s => (x,y) ε c]
U Spec, 552

554	[(x,y) ε f => (x,y) ε nm & ALL(c):[c ε s => (x,y) ε c]]
& [(x,y) ε nm & ALL(c):[c ε s => (x,y) ε c] => (x,y) ε f]
Iff-And, 553

555	(x,y) ε f => (x,y) ε nm & ALL(c):[c ε s => (x,y) ε c]
Split, 554

556	(x,y) ε nm & ALL(c):[c ε s => (x,y) ε c] => (x,y) ε f
Split, 554

557	(x,y) ε nm & ALL(c):[c ε s => (x,y) ε c]
Detach, 555, 551

558	(x,y) ε nm
Split, 557

559	ALL(c):[c ε s => (x,y) ε c]
Split, 557

560	ALL(c2):[(x,c2) ε nm <=> x ε n & c2 ε m]
U Spec, 19

561	(x,y) ε nm <=> x ε n & y ε m
U Spec, 560

562	[(x,y) ε nm => x ε n & y ε m]
& [x ε n & y ε m => (x,y) ε nm]
Iff-And, 561

563	(x,y) ε nm => x ε n & y ε m
Split, 562

564	x ε n & y ε m => (x,y) ε nm
Split, 562

565	x ε n & y ε m
Detach, 563, 558

Functionality, Part 1

566	ALL(c):ALL(d):[(c,d) ε f => c ε n & d ε m]
Conclusion, 551
567	ALL(c):ALL(d):[(c,d) ε f => c ε n & d ε m]
& ALL(c):[c ε n => EXIST(d):[d ε m & (c,d) ε f]]
Join, 566, 130

568	ALL(c):ALL(d):[(c,d) ε f => c ε n & d ε m]
& ALL(c):[c ε n => EXIST(d):[d ε m & (c,d) ε f]]
& ALL(c):ALL(d1):ALL(d2):[(c,d1) ε f & (c,d2) ε f => d1=d2]
Join, 567, 548

f is a function

569	ALL(c):ALL(d):[d=f(c) <=> (c,d) ε f]
Detach, 37, 568

570	ALL(d):[d=f(1) <=> (1,d) ε f]
U Spec, 569

571	m1=f(1) <=> (1,m1) ε f
U Spec, 570

572	[m1=f(1) => (1,m1) ε f] & [(1,m1) ε f => m1=f(1)]
Iff-And, 571

573	m1=f(1) => (1,m1) ε f
Split, 572

574	(1,m1) ε f => m1=f(1)
Split, 572

575	ALL(b):[(1,b) ε f <=> (1,b) ε nm & ALL(c):[c ε s => (1,b) ε c]]
U Spec, 33

576	(1,m1) ε f <=> (1,m1) ε nm & ALL(c):[c ε s => (1,m1) ε c]
U Spec, 575

577	[(1,m1) ε f => (1,m1) ε nm & ALL(c):[c ε s => (1,m1) ε c]]
& [(1,m1) ε nm & ALL(c):[c ε s => (1,m1) ε c] => (1,m1) ε f]
Iff-And, 576

578	(1,m1) ε f => (1,m1) ε nm & ALL(c):[c ε s => (1,m1) ε c]
Split, 577

Sufficient: (1,m1) ε f

579	(1,m1) ε nm & ALL(c):[c ε s => (1,m1) ε c] => (1,m1) ε f
Split, 577

580	ALL(c2):[(1,c2) ε nm <=> 1 ε n & c2 ε m]
U Spec, 19

581	(1,m1) ε nm <=> 1 ε n & m1 ε m
U Spec, 580

582	[(1,m1) ε nm => 1 ε n & m1 ε m]
& [1 ε n & m1 ε m => (1,m1) ε nm]
Iff-And, 581

583	(1,m1) ε nm => 1 ε n & m1 ε m
Split, 582

584	1 ε n & m1 ε m => (1,m1) ε nm
Split, 582

585	1 ε n & m1 ε m
Join, 2, 10

586	(1,m1) ε nm
Detach, 584, 585

587	t ε s
Premise

588	t ε s <=> t ε pnm & [(1,m1) ε t & ALL(b):ALL(c):[(b,c) ε t => (b+1,g(b+1,c)) ε t]]
U Spec, 29

589	[t ε s => t ε pnm & [(1,m1) ε t & ALL(b):ALL(c):[(b,c) ε t => (b+1,g(b+1,c)) ε t]]]
& [t ε pnm & [(1,m1) ε t & ALL(b):ALL(c):[(b,c) ε t => (b+1,g(b+1,c)) ε t]] => t ε s]
Iff-And, 588

590	t ε s => t ε pnm & [(1,m1) ε t & ALL(b):ALL(c):[(b,c) ε t => (b+1,g(b+1,c)) ε t]]
Split, 589

591	t ε pnm & [(1,m1) ε t & ALL(b):ALL(c):[(b,c) ε t => (b+1,g(b+1,c)) ε t]] => t ε s
Split, 589

592	t ε pnm & [(1,m1) ε t & ALL(b):ALL(c):[(b,c) ε t => (b+1,g(b+1,c)) ε t]]
Detach, 590, 587

593	t ε pnm
Split, 592

594	(1,m1) ε t & ALL(b):ALL(c):[(b,c) ε t => (b+1,g(b+1,c)) ε t]
Split, 592

595	(1,m1) ε t
Split, 594

596	ALL(c):[c ε s => (1,m1) ε c]
Conclusion, 587
597	(1,m1) ε nm & ALL(c):[c ε s => (1,m1) ε c]
Join, 586, 596

598	(1,m1) ε f
Detach, 579, 597

599	m1=f(1)
Detach, 574, 598

600	f(1)=m1
Sym, 599

Prove: ALL(a):[a ε n => f(a+1)=g(a+1,f(a))]

Suppose...

601	x ε n
Premise

602	x ε n => EXIST(d):[d ε m & (x,d) ε f]
U Spec, 130

603	EXIST(d):[d ε m & (x,d) ε f]
Detach, 602, 601

604	y ε m & (x,y) ε f
E Spec, 603

Define: y

605	y ε m
Split, 604

606	(x,y) ε f
Split, 604

607	ALL(b):[(x,b) ε f <=> (x,b) ε nm & ALL(c):[c ε s => (x,b) ε c]]
U Spec, 33

608	(x,y) ε f <=> (x,y) ε nm & ALL(c):[c ε s => (x,y) ε c]
U Spec, 607

609	[(x,y) ε f => (x,y) ε nm & ALL(c):[c ε s => (x,y) ε c]]
& [(x,y) ε nm & ALL(c):[c ε s => (x,y) ε c] => (x,y) ε f]
Iff-And, 608

610	(x,y) ε f => (x,y) ε nm & ALL(c):[c ε s => (x,y) ε c]
Split, 609

611	(x,y) ε nm & ALL(c):[c ε s => (x,y) ε c] => (x,y) ε f
Split, 609

612	(x,y) ε nm & ALL(c):[c ε s => (x,y) ε c]
Detach, 610, 606

613	(x,y) ε nm
Split, 612

614	ALL(c):[c ε s => (x,y) ε c]
Split, 612

615	ALL(b):[(x+1,b) ε f <=> (x+1,b) ε nm & ALL(c):[c ε s => (x+1,b) ε c]]
U Spec, 33

616	(x+1,g(x+1,y)) ε f <=> (x+1,g(x+1,y)) ε nm & ALL(c):[c ε s => (x+1,g(x+1,y)) ε c]
U Spec, 615

617	[(x+1,g(x+1,y)) ε f => (x+1,g(x+1,y)) ε nm & ALL(c):[c ε s => (x+1,g(x+1,y)) ε c]]
& [(x+1,g(x+1,y)) ε nm & ALL(c):[c ε s => (x+1,g(x+1,y)) ε c] => (x+1,g(x+1,y)) ε f]
Iff-And, 616

618	(x+1,g(x+1,y)) ε f => (x+1,g(x+1,y)) ε nm & ALL(c):[c ε s => (x+1,g(x+1,y)) ε c]
Split, 617

Sufficient: (x+1,g(x+1,y)) ε f

619	(x+1,g(x+1,y)) ε nm & ALL(c):[c ε s => (x+1,g(x+1,y)) ε c] => (x+1,g(x+1,y)) ε f
Split, 617

620	ALL(c2):[(x+1,c2) ε nm <=> x+1 ε n & c2 ε m]
U Spec, 19

621	(x+1,g(x+1,y)) ε nm <=> x+1 ε n & g(x+1,y) ε m
U Spec, 620

622	[(x+1,g(x+1,y)) ε nm => x+1 ε n & g(x+1,y) ε m]
& [x+1 ε n & g(x+1,y) ε m => (x+1,g(x+1,y)) ε nm]
Iff-And, 621

623	(x+1,g(x+1,y)) ε nm => x+1 ε n & g(x+1,y) ε m
Split, 622

Sufficient: (x+1,g(x+1,y)) ε nm

624	x+1 ε n & g(x+1,y) ε m => (x+1,g(x+1,y)) ε nm
Split, 622

625	ALL(b):[x ε n & b ε n => x+b ε n]
U Spec, 3

626	x ε n & 1 ε n => x+1 ε n
U Spec, 625

627	x ε n & 1 ε n
Join, 601, 2

628	x+1 ε n
Detach, 626, 627

629	ALL(d):[x+1 ε n & d ε m => g(x+1,d) ε m]
U Spec, 11

630	x+1 ε n & y ε m => g(x+1,y) ε m
U Spec, 629

631	x+1 ε n & y ε m
Join, 628, 605

632	g(x+1,y) ε m
Detach, 630, 631

633	x+1 ε n & g(x+1,y) ε m
Join, 628, 632

634	(x+1,g(x+1,y)) ε nm
Detach, 624, 633

Suppose...

635	t ε s
Premise

636	t ε s <=> t ε pnm & [(1,m1) ε t & ALL(b):ALL(c):[(b,c) ε t => (b+1,g(b+1,c)) ε t]]
U Spec, 29

637	[t ε s => t ε pnm & [(1,m1) ε t & ALL(b):ALL(c):[(b,c) ε t => (b+1,g(b+1,c)) ε t]]]
& [t ε pnm & [(1,m1) ε t & ALL(b):ALL(c):[(b,c) ε t => (b+1,g(b+1,c)) ε t]] => t ε s]
Iff-And, 636

638	t ε s => t ε pnm & [(1,m1) ε t & ALL(b):ALL(c):[(b,c) ε t => (b+1,g(b+1,c)) ε t]]
Split, 637

639	t ε pnm & [(1,m1) ε t & ALL(b):ALL(c):[(b,c) ε t => (b+1,g(b+1,c)) ε t]] => t ε s
Split, 637

640	t ε pnm & [(1,m1) ε t & ALL(b):ALL(c):[(b,c) ε t => (b+1,g(b+1,c)) ε t]]
Detach, 638, 635

641	t ε pnm
Split, 640

642	(1,m1) ε t & ALL(b):ALL(c):[(b,c) ε t => (b+1,g(b+1,c)) ε t]
Split, 640

643	(1,m1) ε t
Split, 642

644	ALL(b):ALL(c):[(b,c) ε t => (b+1,g(b+1,c)) ε t]
Split, 642

645	ALL(c):[(x,c) ε t => (x+1,g(x+1,c)) ε t]
U Spec, 644

646	(x,y) ε t => (x+1,g(x+1,y)) ε t
U Spec, 645

647	t ε s => (x,y) ε t
U Spec, 614

648	(x,y) ε t
Detach, 647, 635

649	(x+1,g(x+1,y)) ε t
Detach, 646, 648

650	ALL(c):[c ε s => (x+1,g(x+1,y)) ε c]
Conclusion, 635
651	(x+1,g(x+1,y)) ε nm
& ALL(c):[c ε s => (x+1,g(x+1,y)) ε c]
Join, 634, 650

652	(x+1,g(x+1,y)) ε f
Detach, 619, 651

653	ALL(d):[d=f(x) <=> (x,d) ε f]
U Spec, 569

654	y=f(x) <=> (x,y) ε f
U Spec, 653

655	[y=f(x) => (x,y) ε f] & [(x,y) ε f => y=f(x)]
Iff-And, 654

656	y=f(x) => (x,y) ε f
Split, 655

657	(x,y) ε f => y=f(x)
Split, 655

658	y=f(x)
Detach, 657, 606

659	ALL(d):[d=f(x+1) <=> (x+1,d) ε f]
U Spec, 569

660	g(x+1,y)=f(x+1) <=> (x+1,g(x+1,y)) ε f
U Spec, 659

661	[g(x+1,y)=f(x+1) => (x+1,g(x+1,y)) ε f]
& [(x+1,g(x+1,y)) ε f => g(x+1,y)=f(x+1)]
Iff-And, 660

662	g(x+1,y)=f(x+1) => (x+1,g(x+1,y)) ε f
Split, 661

663	(x+1,g(x+1,y)) ε f => g(x+1,y)=f(x+1)
Split, 661

664	g(x+1,y)=f(x+1)
Detach, 663, 652

665	g(x+1,f(x))=f(x+1)
Substitute, 658, 664

666	f(x+1)=g(x+1,f(x))
Sym, 665

667	ALL(c):[c ε n => f(c+1)=g(c+1,f(c))]
Conclusion, 601
668	f(1)=m1 & ALL(c):[c ε n => f(c+1)=g(c+1,f(c))]
Join, 600, 667

As Required:

669	ALL(a):ALL(b):ALL(g):[Set(a)
& b ε a
& ALL(c):ALL(d):[c ε n & d ε a => g(c,d) ε a]
=> EXIST(f):[f(1)=b & ALL(c):[c ε n => f(c+1)=g(c+1,f(c))]]]
Conclusion, 8
```