THEOREM
*******
Let s be a non-empty set with function f: s --> s. There exists a subset n of s and x0 e n such that the Induction Principle holds on n with x0 being the "first" element of n and f being the successor function.
COROLLARY
*********
Let x be a non-empty set. Then there exists a subset n of x, x0 e n and f: n --> n such that the Induction Principle holds on n with x0 being the "first" element of n and f being the successor function.
Lines
-----
7-10 Construct n using Subset Axiom
11-18 Prove n is a subset of s
19-29 Prove x0 e n
30-62 Prove f is closed on n
63-89 Prove induction principle holds on n
90-94 Generalize
95-111 Prove corollary
This formal proof was written and machine-verified with the aid of the author's DC Proof 2.0 software available at http://www.dcproof.com
PREVIOUS RESULT
***************
Let s be a set. Then there exists a function f on s such that f(x)=x. Used for corollary. PROOF
1 ALL(s):[Set(s) => EXIST(f):ALL(a):[a e s => f(a)=a]]
Axiom
PROOF OF THEOREM
****************
Let s be a non-empty set with function f: s --> s
2 Set(s) & EXIST(a):a e s & ALL(a):[a e s => f(a) e s]
Premise
3 Set(s)
Split, 2
4 EXIST(a):a e s
Split, 2
5 ALL(a):[a e s => f(a) e s]
Split, 2
Define: x0
6 x0 e s
E Spec, 4
Construct set n
Apply Subset Axiom
7 EXIST(sub):[Set(sub) & ALL(a):[a e sub <=> a e s & ALL(b):[Set(b) & ALL(c):[c e b => c e s]
=> [x0 e b & ALL(c):[c e b => f(c) e b] => a e b]]]]
Subset, 3
8 Set(n) & ALL(a):[a e n <=> a e s & ALL(b):[Set(b) & ALL(c):[c e b => c e s]
=> [x0 e b & ALL(c):[c e b => f(c) e b] => a e b]]]
E Spec, 7
Define: n
9 Set(n)
Split, 8
10 ALL(a):[a e n <=> a e s & ALL(b):[Set(b) & ALL(c):[c e b => c e s]
=> [x0 e b & ALL(c):[c e b => f(c) e b] => a e b]]]
Split, 8
Prove: n is a subset of s
Suppose...
11 x e n
Premise
Apply definition of n
12 x e n <=> x e s & ALL(b):[Set(b) & ALL(c):[c e b => c e s]
=> [x0 e b & ALL(c):[c e b => f(c) e b] => x e b]]
U Spec, 10
13 [x e n => x e s & ALL(b):[Set(b) & ALL(c):[c e b => c e s]
=> [x0 e b & ALL(c):[c e b => f(c) e b] => x e b]]]
& [x e s & ALL(b):[Set(b) & ALL(c):[c e b => c e s]
=> [x0 e b & ALL(c):[c e b => f(c) e b] => x e b]] => x e n]
Iff-And, 12
14 x e n => x e s & ALL(b):[Set(b) & ALL(c):[c e b => c e s]
=> [x0 e b & ALL(c):[c e b => f(c) e b] => x e b]]
Split, 13
15 x e s & ALL(b):[Set(b) & ALL(c):[c e b => c e s]
=> [x0 e b & ALL(c):[c e b => f(c) e b] => x e b]] => x e n
Split, 13
16 x e s & ALL(b):[Set(b) & ALL(c):[c e b => c e s]
=> [x0 e b & ALL(c):[c e b => f(c) e b] => x e b]]
Detach, 14, 11
17 x e s
Split, 16
As Required:
18 ALL(a):[a e n => a e s]
4 Conclusion, 11
Prove that the set n has the required properties. Show that n = {x0, f(x0), f(f(x0)), ...}
Prove: x0 e n
Apply definition of n
19 x0 e n <=> x0 e s & ALL(b):[Set(b) & ALL(c):[c e b => c e s]
=> [x0 e b & ALL(c):[c e b => f(c) e b] => x0 e b]]
U Spec, 10
20 [x0 e n => x0 e s & ALL(b):[Set(b) & ALL(c):[c e b => c e s]
=> [x0 e b & ALL(c):[c e b => f(c) e b] => x0 e b]]]
& [x0 e s & ALL(b):[Set(b) & ALL(c):[c e b => c e s]
=> [x0 e b & ALL(c):[c e b => f(c) e b] => x0 e b]] => x0 e n]
Iff-And, 19
21 x0 e n => x0 e s & ALL(b):[Set(b) & ALL(c):[c e b => c e s]
=> [x0 e b & ALL(c):[c e b => f(c) e b] => x0 e b]]
Split, 20
Sufficient: For x0 e n
22 x0 e s & ALL(b):[Set(b) & ALL(c):[c e b => c e s]
=> [x0 e b & ALL(c):[c e b => f(c) e b] => x0 e b]] => x0 e n
Split, 20
Prove: ALL(b):[Set(b) & ALL(c):[c e b => c e s]
=> [x0 e b & ALL(c):[c e b => f(c) e b] => x0 e b]]
Suppose...
23 Set(q) & ALL(c):[c e q => c e s]
Premise
Prove: x0 e q & ALL(c):[c e q => f(c) e q] => x0 e q => x0 eq
Suppose...
24 x0 e q & ALL(c):[c e q => f(c) e q]
Premise
25 x0 e q
Split, 24
As Required:
26 x0 e q & ALL(c):[c e q => f(c) e q] => x0 e q
4 Conclusion, 24
As Required:
27 ALL(b):[Set(b) & ALL(c):[c e b => c e s]
=> [x0 e b & ALL(c):[c e b => f(c) e b] => x0 e b]]
4 Conclusion, 23
28 x0 e s
& ALL(b):[Set(b) & ALL(c):[c e b => c e s]
=> [x0 e b & ALL(c):[c e b => f(c) e b] => x0 e b]]
Join, 6, 27
As Required:
29 x0 e n
Detach, 22, 28
Prove: f is closed on n
Suppose...
30 x e n
Premise
Apply definition of n
31 x e n <=> x e s & ALL(b):[Set(b) & ALL(c):[c e b => c e s]
=> [x0 e b & ALL(c):[c e b => f(c) e b] => x e b]]
U Spec, 10
32 [x e n => x e s & ALL(b):[Set(b) & ALL(c):[c e b => c e s]
=> [x0 e b & ALL(c):[c e b => f(c) e b] => x e b]]]
& [x e s & ALL(b):[Set(b) & ALL(c):[c e b => c e s]
=> [x0 e b & ALL(c):[c e b => f(c) e b] => x e b]] => x e n]
Iff-And, 31
33 x e n => x e s & ALL(b):[Set(b) & ALL(c):[c e b => c e s]
=> [x0 e b & ALL(c):[c e b => f(c) e b] => x e b]]
Split, 32
34 x e s & ALL(b):[Set(b) & ALL(c):[c e b => c e s]
=> [x0 e b & ALL(c):[c e b => f(c) e b] => x e b]] => x e n
Split, 32
35 x e s & ALL(b):[Set(b) & ALL(c):[c e b => c e s]
=> [x0 e b & ALL(c):[c e b => f(c) e b] => x e b]]
Detach, 33, 30
36 x e s
Split, 35
37 ALL(b):[Set(b) & ALL(c):[c e b => c e s]
=> [x0 e b & ALL(c):[c e b => f(c) e b] => x e b]]
Split, 35
Apply the definition of n
38 f(x) e n <=> f(x) e s & ALL(b):[Set(b) & ALL(c):[c e b => c e s]
=> [x0 e b & ALL(c):[c e b => f(c) e b] => f(x) e b]]
U Spec, 10
39 [f(x) e n => f(x) e s & ALL(b):[Set(b) & ALL(c):[c e b => c e s]
=> [x0 e b & ALL(c):[c e b => f(c) e b] => f(x) e b]]]
& [f(x) e s & ALL(b):[Set(b) & ALL(c):[c e b => c e s]
=> [x0 e b & ALL(c):[c e b => f(c) e b] => f(x) e b]] => f(x) e n]
Iff-And, 38
40 f(x) e n => f(x) e s & ALL(b):[Set(b) & ALL(c):[c e b => c e s]
=> [x0 e b & ALL(c):[c e b => f(c) e b] => f(x) e b]]
Split, 39
Sufficient: For f(x) e n
41 f(x) e s & ALL(b):[Set(b) & ALL(c):[c e b => c e s]
=> [x0 e b & ALL(c):[c e b => f(c) e b] => f(x) e b]] => f(x) e n
Split, 39
Prove: f(x) e s
Apply previous result
42 x e n => x e s
U Spec, 18
43 x e s
Detach, 42, 30
Apply the definition of f
44 x e s => f(x) e s
U Spec, 5
As Required:
45 f(x) e s
Detach, 44, 43
Prove: ALL(b):[Set(b) & ALL(c):[c e b => c e s]
=> [x0 e b & ALL(c):[c e b => f(c) e b] => f(x) e b]]
Suppose...
46 Set(q) & ALL(c):[c e q => c e s]
Premise
47 Set(q)
Split, 46
48 ALL(c):[c e q => c e s]
Split, 46
Prove: x0 e q & ALL(c):[c e q => f(c) e q] => f(x) e q
Suppose...
49 x0 e q & ALL(c):[c e q => f(c) e q]
Premise
50 x0 e q
Split, 49
51 ALL(c):[c e q => f(c) e q]
Split, 49
Sufficient: For f(x) e q
52 x e q => f(x) e q
U Spec, 51
Prove: x e q
Apply previous result
53 Set(q) & ALL(c):[c e q => c e s]
=> [x0 e q & ALL(c):[c e q => f(c) e q] => x e q]
U Spec, 37
Sufficient: For x e q
54 x0 e q & ALL(c):[c e q => f(c) e q] => x e q
Detach, 53, 46
55 x0 e q & ALL(c):[c e q => f(c) e q]
Join, 50, 51
As Required:
56 x e q
Detach, 54, 55
As Required:
57 f(x) e q
Detach, 52, 56
As Required:
58 x0 e q & ALL(c):[c e q => f(c) e q] => f(x) e q
4 Conclusion, 49
As Required:
59 ALL(b):[Set(b) & ALL(c):[c e b => c e s]
=> [x0 e b & ALL(c):[c e b => f(c) e b] => f(x) e b]]
4 Conclusion, 46
60 f(x) e s
& ALL(b):[Set(b) & ALL(c):[c e b => c e s]
=> [x0 e b & ALL(c):[c e b => f(c) e b] => f(x) e b]]
Join, 45, 59
As Required:
61 f(x) e n
Detach, 41, 60
As Required:
62 ALL(a):[a e n => f(a) e n]
4 Conclusion, 30
Induction Principle
*******************
Prove: 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(c):[c e n => c e a]]]
Suppose...
63 Set(p) & ALL(b):[b e p => b e n]
Premise
64 Set(p)
Split, 63
p is a subset of n
65 ALL(b):[b e p => b e n]
Split, 63
Prove: x0 e p & ALL(b):[b e p => f(b) e a]
=> ALL(c):[c e n => c e p]
Suppose...
66 x0 e p & ALL(b):[b e p => f(b) e p]
Premise
67 x0 e p
Split, 66
68 ALL(b):[b e p => f(b) e p]
Split, 66
Prove: ALL(c):[c e n => c e p]
Suppose...
69 x e n
Premise
Apply definition of n
70 x e n <=> x e s & ALL(b):[Set(b) & ALL(c):[c e b => c e s]
=> [x0 e b & ALL(c):[c e b => f(c) e b] => x e b]]
U Spec, 10
71 [x e n => x e s & ALL(b):[Set(b) & ALL(c):[c e b => c e s]
=> [x0 e b & ALL(c):[c e b => f(c) e b] => x e b]]]
& [x e s & ALL(b):[Set(b) & ALL(c):[c e b => c e s]
=> [x0 e b & ALL(c):[c e b => f(c) e b] => x e b]] => x e n]
Iff-And, 70
72 x e n => x e s & ALL(b):[Set(b) & ALL(c):[c e b => c e s]
=> [x0 e b & ALL(c):[c e b => f(c) e b] => x e b]]
Split, 71
73 x e s & ALL(b):[Set(b) & ALL(c):[c e b => c e s]
=> [x0 e b & ALL(c):[c e b => f(c) e b] => x e b]] => x e n
Split, 71
74 x e s & ALL(b):[Set(b) & ALL(c):[c e b => c e s]
=> [x0 e b & ALL(c):[c e b => f(c) e b] => x e b]]
Detach, 72, 69
75 x e s
Split, 74
76 ALL(b):[Set(b) & ALL(c):[c e b => c e s]
=> [x0 e b & ALL(c):[c e b => f(c) e b] => x e b]]
Split, 74
77 Set(p) & ALL(c):[c e p => c e s]
=> [x0 e p & ALL(c):[c e p => f(c) e p] => x e p]
U Spec, 76
Prove: ALL(c):[c e p => c e s]
Suppose...
78 y e p
Premise
Apply definition of p
79 y e p => y e n
U Spec, 65
80 y e n
Detach, 79, 78
Apply previous result
81 y e n => y e s
U Spec, 18
82 y e s
Detach, 81, 80
As Required:
83 ALL(c):[c e p => c e s]
4 Conclusion, 78
84 Set(p) & ALL(c):[c e p => c e s]
Join, 64, 83
85 x0 e p & ALL(c):[c e p => f(c) e p] => x e p
Detach, 77, 84
86 x e p
Detach, 85, 66
As Required:
87 ALL(c):[c e n => c e p]
4 Conclusion, 69
88 x0 e p & ALL(b):[b e p => f(b) e p]
=> ALL(c):[c e n => c e p]
4 Conclusion, 66
As Required:
89 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(c):[c e n => c e a]]]
4 Conclusion, 63
90 Set(n) & ALL(a):[a e n => a e s]
Join, 9, 18
91 Set(n) & ALL(a):[a e n => a e s] & x0 e n
Join, 90, 29
92 Set(n) & ALL(a):[a e n => a e s] & x0 e n
& ALL(a):[a e n => f(a) e n]
Join, 91, 62
93 Set(n) & ALL(a):[a e n => a e s] & x0 e n
& ALL(a):[a e n => f(a) e n]
& 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(c):[c e n => c e a]]]
Join, 92, 89
As Required:
94 ALL(s):ALL(f):[Set(s) & EXIST(a):a e s & ALL(a):[a e s => f(a) e s]
=> EXIST(n):EXIST(x0):[Set(n) & ALL(a):[a e n => a e s] & x0 e n
& ALL(a):[a e n => f(a) e n]
& 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(c):[c e n => c e a]]]]]
4 Conclusion, 2
PROOF OF COROLLARY
******************
Suppose...
95 Set(x) & EXIST(a):a e x
Premise
96 Set(x)
Split, 95
97 EXIST(a):a e x
Split, 95
Define: x0
98 x0 e x
E Spec, 97
Apply previous result
99 Set(x) => EXIST(f):ALL(a):[a e x => f(a)=a]
U Spec, 1
100 EXIST(f):ALL(a):[a e x => f(a)=a]
Detach, 99, 96
Define: f
101 ALL(a):[a e x => f(a)=a]
E Spec, 100
Apply theorem
102 ALL(f):[Set(x) & EXIST(a):a e x & ALL(a):[a e x => f(a) e x]
=> EXIST(n):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):[Set(a) & ALL(b):[b e a => b e n]
=> [x0 e a & ALL(b):[b e a => f(b) e a]
=> ALL(c):[c e n => c e a]]]]]
U Spec, 94
103 Set(x) & EXIST(a):a e x & ALL(a):[a e x => f(a) e x]
=> EXIST(n):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):[Set(a) & ALL(b):[b e a => b e n]
=> [x0 e a & ALL(b):[b e a => f(b) e a]
=> ALL(c):[c e n => c e a]]]]
U Spec, 102
Prove: ALL(a):[a e x => f(a) e x]
Suppose...
104 y e x
Premise
105 y e x => f(y)=y
U Spec, 101
106 f(y)=y
Detach, 105, 104
107 f(y) e x
Substitute, 106, 104
As Required:
108 ALL(a):[a e x => f(a) e x]
4 Conclusion, 104
109 Set(x) & EXIST(a):a e x
& ALL(a):[a e x => f(a) e x]
Join, 95, 108
110 EXIST(n):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):[Set(a) & ALL(b):[b e a => b e n]
=> [x0 e a & ALL(b):[b e a => f(b) e a]
=> ALL(c):[c e n => c e a]]]]
Detach, 103, 109
As Required:
111 ALL(x):[Set(x) & EXIST(a):a e x
=> EXIST(f):EXIST(n):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):[Set(a) & ALL(b):[b e a => b e n]
=> [x0 e a & ALL(b):[b e a => f(b) e a]
=> ALL(c):[c e n => c e a]]]]]
4 Conclusion, 95