Peano Thm 3

THEOREM 3

*********

The bijective mapping from n to n' preserves the successor relations on n and n'

Outline

*******

Line 1 Previous result from Theorem 2

Lines 2 - 14 Initial assumptions

Lines 15 - 164 Prove successor relations are preserved under f

Lines 165 - 167 Generalizing

This proof was written with the aid of the author's DC Proof 2.0 software available free at http://www.dcproof.com

PREVIOUS RESULT

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

From Theorem 2, the mapping from n to n' is bijective

1 ALL(n1):ALL(z1):ALL(next1):ALL(n2):ALL(z2):ALL(next2):[Set(n1)

& z1 e n1

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

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

& ALL(a):[a e n1 => ~next1(a)=z1]

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

=> [z1 e a & ALL(b):[b e a => next1(b) e a]

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

& Set(n2)

& z2 e n2

& ALL(a):[a e n2 => next2(a) e n2]

& ALL(a):ALL(b):[a e n2 & b e n2 => [next2(a)=next2(b) => a=b]]

& ALL(a):[a e n2 => ~next2(a)=z2]

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

=> [z2 e a & ALL(b):[b e a => next2(b) e a]

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

=> ALL(f):[ALL(a):[a e n1 => f(a) e n2]

& f(z1)=z2

& ALL(a):[a e n1 => f(next1(a))=next2(f(a))]

=> ALL(a):[a e n2 => EXIST(b):[b e n1 & f(b)=a]]

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

Axiom

PROOF

*****

Suppose we have Peano systems (n,0,next) and (n',0',next')

2 Set(n)

& 0 e n

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

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

& ALL(a):[a e n => ~next(a)=0]

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

=> [0 e a & ALL(b):[b e a => next(b) e a]

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

& Set(n')

& 0' e n'

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

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

& ALL(a):[a e n' => ~next'(a)=0']

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

=> [0' e a & ALL(b):[b e a => next'(b) e a]

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

Premise

Peano's Axioms (n,0,next)

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

3 Set(n)

Split, 2

4 0 e n

Split, 2

5 ALL(a):[a e n => next(a) e n]

Split, 2

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

Split, 2

7 ALL(a):[a e n => ~next(a)=0]

Split, 2

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

=> [0 e a & ALL(b):[b e a => next(b) e a]

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

Split, 2

Peano's Axioms (n',0',next')

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

9 Set(n')

Split, 2

10 0' e n'

Split, 2

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

Split, 2

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

Split, 2

13 ALL(a):[a e n' => ~next'(a)=0']

Split, 2

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

=> [0' e a & ALL(b):[b e a => next'(b) e a]

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

Split, 2

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

& f(0)=0'

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

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

Suppose...

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

& f(0)=0'

Premise

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

Split, 15

17 f(0)=0'

Split, 15

'=>'

Prove: ALL(a):[a e n => f(next(a))=next'(f(a))]

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

Suppose...

18 ALL(a):[a e n => f(next(a))=next'(f(a))]

Premise

Prove: ALL(a):ALL(b):[a e n & b e n => [next(a)=b <=> next'(f(a))=f(b)]]

Suppose...

19 x e n & y e n

Premise

20 x e n

Split, 19

21 y e n

Split, 19

Prove: next(x)=y => next'(f(x))=f(y)

Suppose...

22 next(x)=y

Premise

23 next'(f(x))=next'(f(x))

Reflex

24 x e n => f(next(x))=next'(f(x))

U Spec, 18

25 f(next(x))=next'(f(x))

Detach, 24, 20

26 next'(f(x))=f(next(x))

Substitute, 25, 23

27 next'(f(x))=f(y)

Substitute, 22, 26

As Required:

28 next(x)=y => next'(f(x))=f(y)

4 Conclusion, 22

'<='

Prove: next'(f(x))=f(y) => next(x)=y

Suppose...

29 next'(f(x))=f(y)

Premise

30 x e n => f(next(x))=next'(f(x))

U Spec, 18

31 f(next(x))=next'(f(x))

Detach, 30, 20

32 f(next(x))=f(y)

Substitute, 29, 31

Apply Theorem 2

33 ALL(z1):ALL(next1):ALL(n2):ALL(z2):ALL(next2):[Set(n)

& z1 e n

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

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

& ALL(a):[a e n => ~next1(a)=z1]

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

=> [z1 e a & ALL(b):[b e a => next1(b) e a]

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

& Set(n2)

& z2 e n2

& ALL(a):[a e n2 => next2(a) e n2]

& ALL(a):ALL(b):[a e n2 & b e n2 => [next2(a)=next2(b) => a=b]]

& ALL(a):[a e n2 => ~next2(a)=z2]

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

=> [z2 e a & ALL(b):[b e a => next2(b) e a]

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

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

& f(z1)=z2

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

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

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

U Spec, 1

34 ALL(next1):ALL(n2):ALL(z2):ALL(next2):[Set(n)

& 0 e n

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

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

& ALL(a):[a e n => ~next1(a)=0]

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

=> [0 e a & ALL(b):[b e a => next1(b) e a]

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

& Set(n2)

& z2 e n2

& ALL(a):[a e n2 => next2(a) e n2]

& ALL(a):ALL(b):[a e n2 & b e n2 => [next2(a)=next2(b) => a=b]]

& ALL(a):[a e n2 => ~next2(a)=z2]

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

=> [z2 e a & ALL(b):[b e a => next2(b) e a]

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

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

& f(0)=z2

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

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

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

U Spec, 33

35 ALL(n2):ALL(z2):ALL(next2):[Set(n)

& 0 e n

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

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

& ALL(a):[a e n => ~next(a)=0]

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

=> [0 e a & ALL(b):[b e a => next(b) e a]

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

& Set(n2)

& z2 e n2

& ALL(a):[a e n2 => next2(a) e n2]

& ALL(a):ALL(b):[a e n2 & b e n2 => [next2(a)=next2(b) => a=b]]

& ALL(a):[a e n2 => ~next2(a)=z2]

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

=> [z2 e a & ALL(b):[b e a => next2(b) e a]

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

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

& f(0)=z2

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

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

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

U Spec, 34

36 ALL(z2):ALL(next2):[Set(n)

& 0 e n

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

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

& ALL(a):[a e n => ~next(a)=0]

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

=> [0 e a & ALL(b):[b e a => next(b) e a]

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

& Set(n')

& z2 e n'

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

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

& ALL(a):[a e n' => ~next2(a)=z2]

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

=> [z2 e a & ALL(b):[b e a => next2(b) e a]

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

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

& f(0)=z2

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

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

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

U Spec, 35

37 ALL(next2):[Set(n)

& 0 e n

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

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

& ALL(a):[a e n => ~next(a)=0]

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

=> [0 e a & ALL(b):[b e a => next(b) e a]

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

& Set(n')

& 0' e n'

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

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

& ALL(a):[a e n' => ~next2(a)=0']

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

=> [0' e a & ALL(b):[b e a => next2(b) e a]

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

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

& f(0)=0'

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

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

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

U Spec, 36

38 Set(n)

& 0 e n

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

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

& ALL(a):[a e n => ~next(a)=0]

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

=> [0 e a & ALL(b):[b e a => next(b) e a]

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

& Set(n')

& 0' e n'

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

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

& ALL(a):[a e n' => ~next'(a)=0']

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

=> [0' e a & ALL(b):[b e a => next'(b) e a]

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

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

& f(0)=0'

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

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

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

U Spec, 37

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

& f(0)=0'

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

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

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

Detach, 38, 2

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

& f(0)=0'

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

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

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

U Spec, 39

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

& f(0)=0'

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

Join, 15, 18

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

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

Detach, 40, 41

f is surjective

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

Split, 42

f is injective

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

Split, 42

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

U Spec, 44

46 next(x) e n & y e n => [f(next(x))=f(y) => next(x)=y]

U Spec, 45

47 x e n => next(x) e n

U Spec, 5

48 next(x) e n

Detach, 47, 20

49 next(x) e n & y e n

Join, 48, 21

50 f(next(x))=f(y) => next(x)=y

Detach, 46, 49

51 next(x)=y

Detach, 50, 32

As Required:

52 next'(f(x))=f(y) => next(x)=y

4 Conclusion, 29

53 [next(x)=y => next'(f(x))=f(y)]

& [next'(f(x))=f(y) => next(x)=y]

Join, 28, 52

54 next(x)=y <=> next'(f(x))=f(y)

Iff-And, 53

As Required:

55 ALL(a):ALL(b):[a e n & b e n => [next(a)=b <=> next'(f(a))=f(b)]]

4 Conclusion, 19

As Required:

56 ALL(a):[a e n => f(next(a))=next'(f(a))]

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

4 Conclusion, 18

'<='

Prove: ALL(a):ALL(b):[a e n & b e n => [next(a)=b <=> next'(f(a))=f(b)]]

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

Suppose...

57 ALL(a):ALL(b):[a e n & b e n => [next(a)=b <=> next'(f(a))=f(b)]]

Premise

Apply Subset Axiom for proof by induction

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

Subset, 3

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

E Spec, 58

Define: p

60 Set(p)

Split, 59

61 ALL(a):[a e p <=> a e n & f(next(a))=next'(f(a))]

Split, 59

Apply PMI for n

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

=> [0 e p & ALL(b):[b e p => next(b) e p]

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

U Spec, 8

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

Suppose...

63 x e p

Premise

Apply defintion of p

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

U Spec, 61

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

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

Iff-And, 64

66 x e p => x e n & f(next(x))=next'(f(x))

Split, 65

67 x e n & f(next(x))=next'(f(x)) => x e p

Split, 65

68 x e n & f(next(x))=next'(f(x))

Detach, 66, 63

69 x e n

Split, 68

As Required:

70 ALL(a):[a e p => a e n]

4 Conclusion, 63

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

Join, 60, 70

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

72 0 e p & ALL(b):[b e p => next(b) e p]

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

Detach, 62, 71

BASE CASE

*********

Prove: 0 e p

Apply definition of p

73 0 e p <=> 0 e n & f(next(0))=next'(f(0))

U Spec, 61

74 [0 e p => 0 e n & f(next(0))=next'(f(0))]

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

Iff-And, 73

75 0 e p => 0 e n & f(next(0))=next'(f(0))

Split, 74

Sufficient: 0 e p

76 0 e n & f(next(0))=next'(f(0)) => 0 e p

Split, 74

77 ALL(b):[0 e n & b e n => [next(0)=b <=> next'(f(0))=f(b)]]

U Spec, 57

78 0 e n & next(0) e n => [next(0)=next(0) <=> next'(f(0))=f(next(0))]

U Spec, 77

79 0 e n => next(0) e n

U Spec, 5

80 next(0) e n

Detach, 79, 4

81 0 e n & next(0) e n

Join, 4, 80

82 next(0)=next(0) <=> next'(f(0))=f(next(0))

Detach, 78, 81

83 [next(0)=next(0) => next'(f(0))=f(next(0))]

& [next'(f(0))=f(next(0)) => next(0)=next(0)]

Iff-And, 82

84 next(0)=next(0) => next'(f(0))=f(next(0))

Split, 83

85 next'(f(0))=f(next(0)) => next(0)=next(0)

Split, 83

86 next(0)=next(0)

Reflex

87 next'(f(0))=f(next(0))

Detach, 84, 86

88 f(next(0))=next'(f(0))

Sym, 87

89 0 e n & f(next(0))=next'(f(0))

Join, 4, 88

As Required:

90 0 e p

Detach, 76, 89

INDUCTIVE STEP

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

Prove: ALL(a):[a e p => next(a) e p]

Suppose...

91 x e p

Premise

Apply defintion of p

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

U Spec, 61

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

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

Iff-And, 92

94 x e p => x e n & f(next(x))=next'(f(x))

Split, 93

95 x e n & f(next(x))=next'(f(x)) => x e p

Split, 93

96 x e n & f(next(x))=next'(f(x))

Detach, 94, 91

97 x e n

Split, 96

98 f(next(x))=next'(f(x))

Split, 96

Apply definition of p

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

U Spec, 61

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

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

Iff-And, 99

101 next(x) e p => next(x) e n & f(next(next(x)))=next'(f(next(x)))

Split, 100

Sufficient: For next(x) e p

102 next(x) e n & f(next(next(x)))=next'(f(next(x))) => next(x) e p

Split, 100

103 x e n => next(x) e n

U Spec, 5

104 next(x) e n

Detach, 103, 97

105 ALL(b):[next(x) e n & b e n => [next(next(x))=b <=> next'(f(next(x)))=f(b)]]

U Spec, 57

106 next(x) e n & next(next(x)) e n => [next(next(x))=next(next(x)) <=> next'(f(next(x)))=f(next(next(x)))]

U Spec, 105

107 next(x) e n => next(next(x)) e n

U Spec, 5

108 next(next(x)) e n

Detach, 107, 104

109 next(x) e n & next(next(x)) e n

Join, 104, 108

110 next(next(x))=next(next(x)) <=> next'(f(next(x)))=f(next(next(x)))

Detach, 106, 109

111 [next(next(x))=next(next(x)) => next'(f(next(x)))=f(next(next(x)))]

& [next'(f(next(x)))=f(next(next(x))) => next(next(x))=next(next(x))]

Iff-And, 110

112 next(next(x))=next(next(x)) => next'(f(next(x)))=f(next(next(x)))

Split, 111

113 next'(f(next(x)))=f(next(next(x))) => next(next(x))=next(next(x))

Split, 111

114 next(next(x))=next(next(x))

Reflex

115 next'(f(next(x)))=f(next(next(x)))

Detach, 112, 114

116 f(next(next(x)))=next'(f(next(x)))

Sym, 115

117 next(x) e n & f(next(next(x)))=next'(f(next(x)))

Join, 104, 116

118 next(x) e p

Detach, 102, 117

As Required:

119 ALL(a):[a e p => next(a) e p]

4 Conclusion, 91

120 0 e p & ALL(a):[a e p => next(a) e p]

Join, 90, 119

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

Detach, 72, 120

Prove: ALL(a):[a e n => f(next(a))=next'(f(a))]

Suppose...

122 x e n

Premise

123 x e n => x e p

U Spec, 121

124 x e p

Detach, 123, 122

Apply definition of p

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

U Spec, 61

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

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

Iff-And, 125

127 x e p => x e n & f(next(x))=next'(f(x))

Split, 126

128 x e n & f(next(x))=next'(f(x)) => x e p

Split, 126

129 x e n & f(next(x))=next'(f(x))

Detach, 127, 124

130 x e n

Split, 129

131 f(next(x))=next'(f(x))

Split, 129

As Required:

132 ALL(a):[a e n => f(next(a))=next'(f(a))]

4 Conclusion, 122

As Required:

133 ALL(a):ALL(b):[a e n & b e n => [next(a)=b <=> next'(f(a))=f(b)]]

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

4 Conclusion, 57

134 [ALL(a):[a e n => f(next(a))=next'(f(a))]

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

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

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

Join, 56, 133

135 ALL(a):[a e n => f(next(a))=next'(f(a))]

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

Iff-And, 134

As Required:

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

& f(0)=0'

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

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

4 Conclusion, 15

'=>'

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

& f(0)=0'

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

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

& f(0)=0'

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

Suppose...

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

& f(0)=0'

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

Premise

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

Split, 137

139 f(0)=0'

Split, 137

140 ALL(a):[a e n => f(next(a))=next'(f(a))]

Split, 137

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

& f(0)=0'

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

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

U Spec, 136

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

Join, 138, 139

143 ALL(a):[a e n => f(next(a))=next'(f(a))]

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

Detach, 141, 142

144 [ALL(a):[a e n => f(next(a))=next'(f(a))] => ALL(a):ALL(b):[a e n & b e n => [next(a)=b <=> next'(f(a))=f(b)]]]

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

Iff-And, 143

145 ALL(a):[a e n => f(next(a))=next'(f(a))] => ALL(a):ALL(b):[a e n & b e n => [next(a)=b <=> next'(f(a))=f(b)]]

Split, 144

146 ALL(a):ALL(b):[a e n & b e n => [next(a)=b <=> next'(f(a))=f(b)]] => ALL(a):[a e n => f(next(a))=next'(f(a))]

Split, 144

147 ALL(a):ALL(b):[a e n & b e n => [next(a)=b <=> next'(f(a))=f(b)]]

Detach, 145, 140

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

Join, 138, 139

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

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

Join, 148, 147

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

& f(0)=0'

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

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

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

4 Conclusion, 137

'<='

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

& f(0)=0'

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

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

& f(0)=0'

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

Suppose...

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

& f(0)=0'

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

Premise

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

Split, 151

153 f(0)=0'

Split, 151

154 ALL(a):ALL(b):[a e n & b e n => [next(a)=b <=> next'(f(a))=f(b)]]

Split, 151

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

& f(0)=0'

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

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

U Spec, 136

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

Join, 152, 153

157 ALL(a):[a e n => f(next(a))=next'(f(a))]

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

Detach, 155, 156

158 [ALL(a):[a e n => f(next(a))=next'(f(a))] => ALL(a):ALL(b):[a e n & b e n => [next(a)=b <=> next'(f(a))=f(b)]]]

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

Iff-And, 157

159 ALL(a):[a e n => f(next(a))=next'(f(a))] => ALL(a):ALL(b):[a e n & b e n => [next(a)=b <=> next'(f(a))=f(b)]]

Split, 158

160 ALL(a):ALL(b):[a e n & b e n => [next(a)=b <=> next'(f(a))=f(b)]] => ALL(a):[a e n => f(next(a))=next'(f(a))]

Split, 158

161 ALL(a):[a e n => f(next(a))=next'(f(a))]

Detach, 160, 154

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

Join, 152, 153

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

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

Join, 162, 161

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

& f(0)=0'

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

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

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

4 Conclusion, 151

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

& f(0)=0'

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

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

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

& f(0)=0'

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

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

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

Join, 150, 164

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

& f(0)=0'

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

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

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

Iff-And, 165

Successor relations are preserved

As Required:

167 ALL(n1):ALL(z1):ALL(next1):ALL(n2):ALL(z2):ALL(next2):[Set(n1)

& z1 e n1

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

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

& ALL(a):[a e n1 => ~next1(a)=z1]

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

=> [z1 e a & ALL(b):[b e a => next1(b) e a]

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

& Set(n2)

& z2 e n2

& ALL(a):[a e n2 => next2(a) e n2]

& ALL(a):ALL(b):[a e n2 & b e n2 => [next2(a)=next2(b) => a=b]]

& ALL(a):[a e n2 => ~next2(a)=z2]

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

=> [z2 e a & ALL(b):[b e a => next2(b) e a]

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

=> ALL(f):[ALL(a):[a e n1 => f(a) e n2]

& f(z1)=z2

& ALL(a):[a e n1 => f(next1(a))=next2(f(a))]

<=> ALL(a):[a e n1 => f(a) e n2] & f(z1)=z2

& ALL(a):ALL(b):[a e n1 & b e n1 => [next1(a)=b <=> next2(f(a))=f(b)]]]]

4 Conclusion, 2