THEOREM
-------
Suppose:
a) f is an injection defined on s
b) s1 is an element of s with no pre-image under f
c) s2 is an element of s with no pre-image under f
d) n1 is an infinite chain in s starting at s1 with successor function f
e) n2 is an infinite chain in s starting at s2 with successor function f
f) s1 and s2 are distinct
Then n1 and n2 are disjoint
This proof was written with the aid of the author's DC Proof 2.0 software
available at http://www.dcproof.com
PREVIOUS RESULT
---------------
Existence of predecessors
1 ALL(n):ALL(s1):ALL(f):[Set(n)
& 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]]
=> ALL(a):[a e n => [~a=s1 => EXIST(b):[b e n & f(b)=a]]]]
Axiom
PROOF
-----
Suppose:
a) f is an injection defined on s
b) s1 is an element of s with pre-image under f
c) s2 is an element of s with pre-image under f
d) n1 is an infinite chain in s starting at s1
e) n2 is an infinite chain in s starting at s2
f) s1 and s2 are distinct
2 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]]
& s1 e s & ALL(b):[b e s => ~f(b)=s1]
& s2 e s & ALL(b):[b e s => ~f(b)=s2]
& Set(n1)
& ALL(b):[b e n1 => b e s]
& s1 e n1
& ALL(b):[b e n1 => f(b) e n1]
& ALL(b):ALL(c):[b e n1 & c e n1 => [f(b)=f(c) => b=c]]
& ALL(b):[b e n1 => ~f(b)=s1]
& ALL(b):[Set(b)
& ALL(c):[c e b => c e n1]
& s1 e b
& ALL(c):[c e b => f(c) e b]
=> ALL(c):[c e n1 => c e b]]
& Set(n2) & ALL(b):[b e n2 => b e s] & s2 e n2
& ALL(b):[b e n2 => f(b) e n2]
& ALL(b):ALL(c):[b e n2 & c e n2 => [f(b)=f(c) => b=c]]
& ALL(b):[b e n2 => ~f(b)=s2]
& ALL(b):[Set(b)
& ALL(c):[c e b => c e n2]
& s2 e b
& ALL(c):[c e b => f(c) e b]
=> ALL(c):[c e n2 => c e b]]
& ~s1=s2
Premise
Splitting this premise into its component parts...
f is an injection defined on s
3 Set(s)
Split, 2
4 ALL(b):[b e s => f(b) e s]
Split, 2
5 ALL(b):ALL(c):[b e s & c e s => [f(b)=f(c) => b=c]]
Split, 2
s1 is an element of s with no pre-image under f
6 s1 e s
Split, 2
7 ALL(b):[b e s => ~f(b)=s1]
Split, 2
s2 is an element of s with no pre-image under f
8 s2 e s
Split, 2
9 ALL(b):[b e s => ~f(b)=s2]
Split, 2
n1 is an infinite chain of elements of s starting at s1 with successor function f
10 Set(n1)
Split, 2
11 ALL(b):[b e n1 => b e s]
Split, 2
12 s1 e n1
Split, 2
13 ALL(b):[b e n1 => f(b) e n1]
Split, 2
14 ALL(b):ALL(c):[b e n1 & c e n1 => [f(b)=f(c) => b=c]]
Split, 2
15 ALL(b):[b e n1 => ~f(b)=s1]
Split, 2
16 ALL(b):[Set(b)
& ALL(c):[c e b => c e n1]
& s1 e b
& ALL(c):[c e b => f(c) e b]
=> ALL(c):[c e n1 => c e b]]
Split, 2
n2 is an infinite chain of elements of s starting at s2 with successor function f
17 Set(n2)
Split, 2
18 ALL(b):[b e n2 => b e s]
Split, 2
19 s2 e n2
Split, 2
20 ALL(b):[b e n2 => f(b) e n2]
Split, 2
21 ALL(b):ALL(c):[b e n2 & c e n2 => [f(b)=f(c) => b=c]]
Split, 2
22 ALL(b):[b e n2 => ~f(b)=s2]
Split, 2
23 ALL(b):[Set(b)
& ALL(c):[c e b => c e n2]
& s2 e b
& ALL(c):[c e b => f(c) e b]
=> ALL(c):[c e n2 => c e b]]
Split, 2
s1 and s2 are distinct
24 ~s1=s2
Split, 2
Prove: ~EXIST(a):[a e n1 & a e n2] i.e. that n1 and n2 are disjoint sets
Suppose to the contrary...
25 x e n1 & x e n2
Premise
26 x e n1
Split, 25
27 x e n2
Split, 25
Construct the subset of n1 that has no elements in n2
28 EXIST(sub):[Set(sub) & ALL(a):[a e sub <=> a e n1 & ~a e n2]]
Subset, 10
29 Set(p) & ALL(a):[a e p <=> a e n1 & ~a e n2]
E Spec, 28
Define: p
30 Set(p)
Split, 29
31 ALL(a):[a e p <=> a e n1 & ~a e n2]
Split, 29
Apply definition of n1 for set p
32 Set(p)
& ALL(c):[c e p => c e n1]
& s1 e p
& ALL(c):[c e p => f(c) e p]
=> ALL(c):[c e n1 => c e p]
U Spec, 16
Recast previous statement
Prove: Set(p)
& ALL(c):[c e p => c e n1]
& s1 e p
=> [EXIST(c):[c e n1 & ~c e p] => EXIST(c):[c e p & ~f(c) e p]]
Suppose...
33 Set(p)
& ALL(c):[c e p => c e n1]
& s1 e p
Premise
Prove: ALL(c):[c e p => f(c) e p]
=> ALL(c):[c e n1 => c e p]
Suppose...
34 ALL(c):[c e p => f(c) e p]
Premise
35 Set(p)
& ALL(c):[c e p => c e n1]
& s1 e p
& ALL(c):[c e p => f(c) e p]
Join, 33, 34
36 ALL(c):[c e n1 => c e p]
Detach, 32, 35
As Required:
37 ALL(c):[c e p => f(c) e p]
=> ALL(c):[c e n1 => c e p]
4 Conclusion, 34
Apply Contrapositive Rule
38 ~ALL(c):[c e n1 => c e p] => ~ALL(c):[c e p => f(c) e p]
Contra, 37
Apply Quantifier Switch, etc.
39 ~~EXIST(c):~[c e n1 => c e p] => ~ALL(c):[c e p => f(c) e p]
Quant, 38
40 EXIST(c):~[c e n1 => c e p] => ~ALL(c):[c e p => f(c) e p]
Rem DNeg, 39
41 EXIST(c):~~[c e n1 & ~c e p] => ~ALL(c):[c e p => f(c) e p]
Imply-And, 40
42 EXIST(c):[c e n1 & ~c e p] => ~ALL(c):[c e p => f(c) e p]
Rem DNeg, 41
43 EXIST(c):[c e n1 & ~c e p] => ~~EXIST(c):~[c e p => f(c) e p]
Quant, 42
44 EXIST(c):[c e n1 & ~c e p] => EXIST(c):~[c e p => f(c) e p]
Rem DNeg, 43
45 EXIST(c):[c e n1 & ~c e p] => EXIST(c):~~[c e p & ~f(c) e p]
Imply-And, 44
46 EXIST(c):[c e n1 & ~c e p] => EXIST(c):[c e p & ~f(c) e p]
Rem DNeg, 45
Alternative formulation of principle of induction
As Required:
47 Set(p)
& ALL(c):[c e p => c e n1]
& s1 e p
=> [EXIST(c):[c e n1 & ~c e p] => EXIST(c):[c e p & ~f(c) e p]]
4 Conclusion, 33
Prove: ALL(c):[c e p => c e n1]
Suppose...
48 y e p
Premise
Apply definition of p for y
49 y e p <=> y e n1 & ~y e n2
U Spec, 31
50 [y e p => y e n1 & ~y e n2]
& [y e n1 & ~y e n2 => y e p]
Iff-And, 49
51 y e p => y e n1 & ~y e n2
Split, 50
52 y e n1 & ~y e n2 => y e p
Split, 50
53 y e n1 & ~y e n2
Detach, 51, 48
54 y e n1
Split, 53
As Required:
55 ALL(c):[c e p => c e n1]
4 Conclusion, 48
Apply definition of p for s1
56 s1 e p <=> s1 e n1 & ~s1 e n2
U Spec, 31
57 [s1 e p => s1 e n1 & ~s1 e n2]
& [s1 e n1 & ~s1 e n2 => s1 e p]
Iff-And, 56
58 s1 e p => s1 e n1 & ~s1 e n2
Split, 57
Sufficient: s1 e p
59 s1 e n1 & ~s1 e n2 => s1 e p
Split, 57
Prove: ~s1 e n2
Suppose to the contrary...
60 s1 e n2
Premise
Apply previous result
61 ALL(s1):ALL(f):[Set(n2)
& s1 e n2
& ALL(b):[b e n2 => f(b) e n2]
& ALL(b):ALL(c):[b e n2 & c e n2 => [f(b)=f(c) => b=c]]
& ALL(b):[b e n2 => ~f(b)=s1]
& ALL(b):[Set(b)
& ALL(c):[c e b => c e n2]
& s1 e b
& ALL(c):[c e b => f(c) e b]
=> ALL(c):[c e n2 => c e b]]
=> ALL(a):[a e n2 => [~a=s1 => EXIST(b):[b e n2 & f(b)=a]]]]
U Spec, 1
62 ALL(f):[Set(n2)
& s2 e n2
& ALL(b):[b e n2 => f(b) e n2]
& ALL(b):ALL(c):[b e n2 & c e n2 => [f(b)=f(c) => b=c]]
& ALL(b):[b e n2 => ~f(b)=s2]
& ALL(b):[Set(b)
& ALL(c):[c e b => c e n2]
& s2 e b
& ALL(c):[c e b => f(c) e b]
=> ALL(c):[c e n2 => c e b]]
=> ALL(a):[a e n2 => [~a=s2 => EXIST(b):[b e n2 & f(b)=a]]]]
U Spec, 61
63 Set(n2)
& s2 e n2
& ALL(b):[b e n2 => f(b) e n2]
& ALL(b):ALL(c):[b e n2 & c e n2 => [f(b)=f(c) => b=c]]
& ALL(b):[b e n2 => ~f(b)=s2]
& ALL(b):[Set(b)
& ALL(c):[c e b => c e n2]
& s2 e b
& ALL(c):[c e b => f(c) e b]
=> ALL(c):[c e n2 => c e b]]
=> ALL(a):[a e n2 => [~a=s2 => EXIST(b):[b e n2 & f(b)=a]]]
U Spec, 62
64 Set(n2) & s2 e n2
Join, 17, 19
65 Set(n2) & s2 e n2 & ALL(b):[b e n2 => f(b) e n2]
Join, 64, 20
66 Set(n2) & s2 e n2 & ALL(b):[b e n2 => f(b) e n2]
& ALL(b):ALL(c):[b e n2 & c e n2 => [f(b)=f(c) => b=c]]
Join, 65, 21
67 Set(n2) & s2 e n2 & ALL(b):[b e n2 => f(b) e n2]
& ALL(b):ALL(c):[b e n2 & c e n2 => [f(b)=f(c) => b=c]]
& ALL(b):[b e n2 => ~f(b)=s2]
Join, 66, 22
68 Set(n2) & s2 e n2 & ALL(b):[b e n2 => f(b) e n2]
& ALL(b):ALL(c):[b e n2 & c e n2 => [f(b)=f(c) => b=c]]
& ALL(b):[b e n2 => ~f(b)=s2]
& ALL(b):[Set(b)
& ALL(c):[c e b => c e n2]
& s2 e b
& ALL(c):[c e b => f(c) e b]
=> ALL(c):[c e n2 => c e b]]
Join, 67, 23
69 ALL(a):[a e n2 => [~a=s2 => EXIST(b):[b e n2 & f(b)=a]]]
Detach, 63, 68
70 s1 e n2 => [~s1=s2 => EXIST(b):[b e n2 & f(b)=s1]]
U Spec, 69
71 ~s1=s2 => EXIST(b):[b e n2 & f(b)=s1]
Detach, 70, 60
Apply Contrapostive Rule, etc.
72 ~EXIST(b):[b e n2 & f(b)=s1] => ~~s1=s2
Contra, 71
73 ~EXIST(b):[b e n2 & f(b)=s1] => s1=s2
Rem DNeg, 72
74 ~~ALL(b):~[b e n2 & f(b)=s1] => s1=s2
Quant, 73
75 ALL(b):~[b e n2 & f(b)=s1] => s1=s2
Rem DNeg, 74
76 ALL(b):~~[b e n2 => ~f(b)=s1] => s1=s2
Imply-And, 75
77 ALL(b):[b e n2 => ~f(b)=s1] => s1=s2
Rem DNeg, 76
Prove: ALL(b):[b e n2 => ~f(b)=s1]
Suppose...
78 y e n2
Premise
Apply definition of s1
79 y e s => ~f(y)=s1
U Spec, 7
80 y e n2 => y e s
U Spec, 18
81 y e s
Detach, 80, 78
82 ~f(y)=s1
Detach, 79, 81
As Required:
83 ALL(b):[b e n2 => ~f(b)=s1]
4 Conclusion, 78
84 s1=s2
Detach, 77, 83
85 s1=s2 & ~s1=s2
Join, 84, 24
As Required:
86 ~s1 e n2
4 Conclusion, 60
87 s1 e n1 & ~s1 e n2
Join, 12, 86
As Required:
88 s1 e p
Detach, 59, 87
89 Set(p) & ALL(c):[c e p => c e n1]
Join, 30, 55
90 Set(p) & ALL(c):[c e p => c e n1] & s1 e p
Join, 89, 88
91 EXIST(c):[c e n1 & ~c e p] => EXIST(c):[c e p & ~f(c) e p]
Detach, 47, 90
Apply definition of p for x
92 x e p <=> x e n1 & ~x e n2
U Spec, 31
93 [x e p => x e n1 & ~x e n2]
& [x e n1 & ~x e n2 => x e p]
Iff-And, 92
94 x e p => x e n1 & ~x e n2
Split, 93
95 x e n1 & ~x e n2 => x e p
Split, 93
Apply Contrapositive Rule, etc.
96 ~[x e n1 & ~x e n2] => ~x e p
Contra, 94
97 ~~[~x e n1 | ~~x e n2] => ~x e p
DeMorgan, 96
98 ~x e n1 | ~~x e n2 => ~x e p
Rem DNeg, 97
99 ~x e n1 | x e n2 => ~x e p
Rem DNeg, 98
100 ~x e n1 | x e n2
Arb Or, 27
101 ~x e p
Detach, 99, 100
102 x e n1 & ~x e p
Join, 26, 101
103 EXIST(c):[c e n1 & ~c e p]
E Gen, 102
104 EXIST(c):[c e p & ~f(c) e p]
Detach, 91, 103
105 y e p & ~f(y) e p
E Spec, 104
106 y e p
Split, 105
107 ~f(y) e p
Split, 105
Apply definition of p for y
108 y e p <=> y e n1 & ~y e n2
U Spec, 31
109 [y e p => y e n1 & ~y e n2]
& [y e n1 & ~y e n2 => y e p]
Iff-And, 108
110 y e p => y e n1 & ~y e n2
Split, 109
111 y e n1 & ~y e n2 => y e p
Split, 109
112 y e n1 & ~y e n2
Detach, 110, 106
113 y e n1
Split, 112
114 ~y e n2
Split, 112
Apply definition of p for f(y)
115 f(y) e p <=> f(y) e n1 & ~f(y) e n2
U Spec, 31
116 [f(y) e p => f(y) e n1 & ~f(y) e n2]
& [f(y) e n1 & ~f(y) e n2 => f(y) e p]
Iff-And, 115
117 f(y) e p => f(y) e n1 & ~f(y) e n2
Split, 116
118 f(y) e n1 & ~f(y) e n2 => f(y) e p
Split, 116
119 ~f(y) e p => ~[f(y) e n1 & ~f(y) e n2]
Contra, 118
120 ~[f(y) e n1 & ~f(y) e n2]
Detach, 119, 107
121 ~~[f(y) e n1 => ~~f(y) e n2]
Imply-And, 120
122 f(y) e n1 => ~~f(y) e n2
Rem DNeg, 121
123 f(y) e n1 => f(y) e n2
Rem DNeg, 122
Apply definition of f
124 y e n1 => f(y) e n1
U Spec, 13
125 f(y) e n1
Detach, 124, 113
126 f(y) e n2
Detach, 123, 125
Apply previous result
127 ALL(s1):ALL(f):[Set(n2)
& s1 e n2
& ALL(b):[b e n2 => f(b) e n2]
& ALL(b):ALL(c):[b e n2 & c e n2 => [f(b)=f(c) => b=c]]
& ALL(b):[b e n2 => ~f(b)=s1]
& ALL(b):[Set(b)
& ALL(c):[c e b => c e n2]
& s1 e b
& ALL(c):[c e b => f(c) e b]
=> ALL(c):[c e n2 => c e b]]
=> ALL(a):[a e n2 => [~a=s1 => EXIST(b):[b e n2 & f(b)=a]]]]
U Spec, 1
128 ALL(f):[Set(n2)
& s2 e n2
& ALL(b):[b e n2 => f(b) e n2]
& ALL(b):ALL(c):[b e n2 & c e n2 => [f(b)=f(c) => b=c]]
& ALL(b):[b e n2 => ~f(b)=s2]
& ALL(b):[Set(b)
& ALL(c):[c e b => c e n2]
& s2 e b
& ALL(c):[c e b => f(c) e b]
=> ALL(c):[c e n2 => c e b]]
=> ALL(a):[a e n2 => [~a=s2 => EXIST(b):[b e n2 & f(b)=a]]]]
U Spec, 127
129 Set(n2)
& s2 e n2
& ALL(b):[b e n2 => f(b) e n2]
& ALL(b):ALL(c):[b e n2 & c e n2 => [f(b)=f(c) => b=c]]
& ALL(b):[b e n2 => ~f(b)=s2]
& ALL(b):[Set(b)
& ALL(c):[c e b => c e n2]
& s2 e b
& ALL(c):[c e b => f(c) e b]
=> ALL(c):[c e n2 => c e b]]
=> ALL(a):[a e n2 => [~a=s2 => EXIST(b):[b e n2 & f(b)=a]]]
U Spec, 128
130 Set(n2) & s2 e n2
Join, 17, 19
131 Set(n2) & s2 e n2 & ALL(b):[b e n2 => f(b) e n2]
Join, 130, 20
132 Set(n2) & s2 e n2 & ALL(b):[b e n2 => f(b) e n2]
& ALL(b):ALL(c):[b e n2 & c e n2 => [f(b)=f(c) => b=c]]
Join, 131, 21
133 Set(n2) & s2 e n2 & ALL(b):[b e n2 => f(b) e n2]
& ALL(b):ALL(c):[b e n2 & c e n2 => [f(b)=f(c) => b=c]]
& ALL(b):[b e n2 => ~f(b)=s2]
Join, 132, 22
134 Set(n2) & s2 e n2 & ALL(b):[b e n2 => f(b) e n2]
& ALL(b):ALL(c):[b e n2 & c e n2 => [f(b)=f(c) => b=c]]
& ALL(b):[b e n2 => ~f(b)=s2]
& ALL(b):[Set(b)
& ALL(c):[c e b => c e n2]
& s2 e b
& ALL(c):[c e b => f(c) e b]
=> ALL(c):[c e n2 => c e b]]
Join, 133, 23
135 ALL(a):[a e n2 => [~a=s2 => EXIST(b):[b e n2 & f(b)=a]]]
Detach, 129, 134
136 f(y) e n2 => [~f(y)=s2 => EXIST(b):[b e n2 & f(b)=f(y)]]
U Spec, 135
137 ~f(y)=s2 => EXIST(b):[b e n2 & f(b)=f(y)]
Detach, 136, 126
Apply definition of s2
138 y e s => ~f(y)=s2
U Spec, 9
139 y e n1 => y e s
U Spec, 11
140 y e s
Detach, 139, 113
141 ~f(y)=s2
Detach, 138, 140
142 EXIST(b):[b e n2 & f(b)=f(y)]
Detach, 137, 141
143 y' e n2 & f(y')=f(y)
E Spec, 142
144 y' e n2
Split, 143
145 f(y')=f(y)
Split, 143
Apply definition of f
146 ALL(c):[y' e s & c e s => [f(y')=f(c) => y'=c]]
U Spec, 5
147 y' e s & y e s => [f(y')=f(y) => y'=y]
U Spec, 146
148 y' e n2 => y' e s
U Spec, 18
149 y' e s
Detach, 148, 144
150 y' e s & y e s
Join, 149, 140
151 f(y')=f(y) => y'=y
Detach, 147, 150
152 y'=y
Detach, 151, 145
153 y e n2
Substitute, 152, 144
154 y e n2 & ~y e n2
Join, 153, 114
n1 and n2 are disjoint
As Required:
155 ~EXIST(a):[a e n1 & a e n2]
4 Conclusion, 25