THEOREM
*******
Here, we prove the equivalence of two definitions of finite, FiniteA and FiniteB as defined below.
(This proof was written with the aid of the author's DC Proof 2.0 software available at http://www.dcproof.com )
Define: FiniteA
***************
1 ALL(s):[Set(s) => [FiniteA(s)
<=> ALL(x0):ALL(f):[x0 e s
& ALL(a):[a e s => f(a) e s]
=> [Injection(f,s,s) => EXIST(xn):[xn e s & f(xn)=x0]]]]]
Axiom
Define: FiniteB (Dedekind finite)
***************
2 ALL(s):[Set(s) => [FiniteB(s)
<=> ALL(f):[ALL(a):[a e s => f(a) e s]
=> [Injection(f,s,s) => Surjection(f,s,s)]]]]
Axiom
Define: Injection
*****************
3 ALL(f):ALL(a):ALL(b):[Injection(f,a,b)
<=> ALL(c):ALL(d):[c e a & d e a => [f(c)=f(d) => c=d]]]
Axiom
Define: Surjection
******************
4 ALL(f):ALL(a):ALL(b):[Surjection(f,a,b) <=> ALL(c):[c e b => EXIST(d):[d e a & f(d)=c]]]
Axiom
PROOF
*****
ALL(s):[Set(s) => [FiniteA(s) <=> FiniteB(s)]]
Suppose...
5 Set(s)
Premise
'=>'
Prove: FiniteA(s) => FiniteB(s)
Suppose...
6 FiniteA(s)
Premise
Apply definition of FiniteA
7 Set(s) => [FiniteA(s)
<=> ALL(x0):ALL(f):[x0 e s
& ALL(a):[a e s => f(a) e s]
=> [Injection(f,s,s) => EXIST(xn):[xn e s & f(xn)=x0]]]]
U Spec, 1
8 FiniteA(s)
<=> ALL(x0):ALL(f):[x0 e s
& ALL(a):[a e s => f(a) e s]
=> [Injection(f,s,s) => EXIST(xn):[xn e s & f(xn)=x0]]]
Detach, 7, 5
9 [FiniteA(s) => ALL(x0):ALL(f):[x0 e s
& ALL(a):[a e s => f(a) e s]
=> [Injection(f,s,s) => EXIST(xn):[xn e s & f(xn)=x0]]]]
& [ALL(x0):ALL(f):[x0 e s
& ALL(a):[a e s => f(a) e s]
=> [Injection(f,s,s) => EXIST(xn):[xn e s & f(xn)=x0]]] => FiniteA(s)]
Iff-And, 8
10 FiniteA(s) => ALL(x0):ALL(f):[x0 e s
& ALL(a):[a e s => f(a) e s]
=> [Injection(f,s,s) => EXIST(xn):[xn e s & f(xn)=x0]]]
Split, 9
11 ALL(x0):ALL(f):[x0 e s
& ALL(a):[a e s => f(a) e s]
=> [Injection(f,s,s) => EXIST(xn):[xn e s & f(xn)=x0]]] => FiniteA(s)
Split, 9
12 ALL(x0):ALL(f):[x0 e s
& ALL(a):[a e s => f(a) e s]
=> [Injection(f,s,s) => EXIST(xn):[xn e s & f(xn)=x0]]]
Detach, 10, 6
Apply definition of FiniteB
13 Set(s) => [FiniteB(s)
<=> ALL(f):[ALL(a):[a e s => f(a) e s]
=> [Injection(f,s,s) => Surjection(f,s,s)]]]
U Spec, 2
14 FiniteB(s)
<=> ALL(f):[ALL(a):[a e s => f(a) e s]
=> [Injection(f,s,s) => Surjection(f,s,s)]]
Detach, 13, 5
15 [FiniteB(s) => ALL(f):[ALL(a):[a e s => f(a) e s]
=> [Injection(f,s,s) => Surjection(f,s,s)]]]
& [ALL(f):[ALL(a):[a e s => f(a) e s]
=> [Injection(f,s,s) => Surjection(f,s,s)]] => FiniteB(s)]
Iff-And, 14
16 FiniteB(s) => ALL(f):[ALL(a):[a e s => f(a) e s]
=> [Injection(f,s,s) => Surjection(f,s,s)]]
Split, 15
Sufficient: FiniteB(s)
17 ALL(f):[ALL(a):[a e s => f(a) e s]
=> [Injection(f,s,s) => Surjection(f,s,s)]] => FiniteB(s)
Split, 15
Prove: ALL(f):[ALL(a):[a e s => f(a) e s]
=> [Injection(f,s,s) => Surjection(f,s,s)]]
Suppose...
18 ALL(a):[a e s => f(a) e s]
Premise
Prove: Injection(f,s,s) => Surjection(f,s,s)
Suppose...
19 Injection(f,s,s)
Premise
Apply definition of Injection
20 ALL(a):ALL(b):[Injection(f,a,b)
<=> ALL(c):ALL(d):[c e a & d e a => [f(c)=f(d) => c=d]]]
U Spec, 3
21 ALL(b):[Injection(f,s,b)
<=> ALL(c):ALL(d):[c e s & d e s => [f(c)=f(d) => c=d]]]
U Spec, 20
22 Injection(f,s,s)
<=> ALL(c):ALL(d):[c e s & d e s => [f(c)=f(d) => c=d]]
U Spec, 21
23 [Injection(f,s,s) => ALL(c):ALL(d):[c e s & d e s => [f(c)=f(d) => c=d]]]
& [ALL(c):ALL(d):[c e s & d e s => [f(c)=f(d) => c=d]] => Injection(f,s,s)]
Iff-And, 22
24 Injection(f,s,s) => ALL(c):ALL(d):[c e s & d e s => [f(c)=f(d) => c=d]]
Split, 23
25 ALL(c):ALL(d):[c e s & d e s => [f(c)=f(d) => c=d]] => Injection(f,s,s)
Split, 23
26 ALL(c):ALL(d):[c e s & d e s => [f(c)=f(d) => c=d]]
Detach, 24, 19
Apply definition of Surjection
27 ALL(a):ALL(b):[Surjection(f,a,b) <=> ALL(c):[c e b => EXIST(d):[d e a & f(d)=c]]]
U Spec, 4
28 ALL(b):[Surjection(f,s,b) <=> ALL(c):[c e b => EXIST(d):[d e s & f(d)=c]]]
U Spec, 27
29 Surjection(f,s,s) <=> ALL(c):[c e s => EXIST(d):[d e s & f(d)=c]]
U Spec, 28
30 [Surjection(f,s,s) => ALL(c):[c e s => EXIST(d):[d e s & f(d)=c]]]
& [ALL(c):[c e s => EXIST(d):[d e s & f(d)=c]] => Surjection(f,s,s)]
Iff-And, 29
31 Surjection(f,s,s) => ALL(c):[c e s => EXIST(d):[d e s & f(d)=c]]
Split, 30
Sufficient: Surjection(f,s,s)
32 ALL(c):[c e s => EXIST(d):[d e s & f(d)=c]] => Surjection(f,s,s)
Split, 30
Prove: ALL(c):[c e s => EXIST(xn):[xn e s & f(xn)=c]]
Suppose...
33 x0 e s
Premise
Apply premise
34 ALL(f):[x0 e s
& ALL(a):[a e s => f(a) e s]
=> [Injection(f,s,s) => EXIST(xn):[xn e s & f(xn)=x0]]]
U Spec, 12
35 x0 e s
& ALL(a):[a e s => f(a) e s]
=> [Injection(f,s,s) => EXIST(xn):[xn e s & f(xn)=x0]]
U Spec, 34
36 x0 e s & ALL(a):[a e s => f(a) e s]
Join, 33, 18
37 Injection(f,s,s) => EXIST(xn):[xn e s & f(xn)=x0]
Detach, 35, 36
38 EXIST(xn):[xn e s & f(xn)=x0]
Detach, 37, 19
As Required:
39 ALL(c):[c e s => EXIST(xn):[xn e s & f(xn)=c]]
4 Conclusion, 33
40 Surjection(f,s,s)
Detach, 32, 39
As Required:
41 Injection(f,s,s) => Surjection(f,s,s)
4 Conclusion, 19
As Required:
42 ALL(f):[ALL(a):[a e s => f(a) e s]
=> [Injection(f,s,s) => Surjection(f,s,s)]]
4 Conclusion, 18
43 FiniteB(s)
Detach, 17, 42
As Required:
44 FiniteA(s) => FiniteB(s)
4 Conclusion, 6
'<='
Suppose...
45 FiniteB(s)
Premise
Apply definition of FiniteB
46 Set(s) => [FiniteB(s)
<=> ALL(f):[ALL(a):[a e s => f(a) e s]
=> [Injection(f,s,s) => Surjection(f,s,s)]]]
U Spec, 2
47 FiniteB(s)
<=> ALL(f):[ALL(a):[a e s => f(a) e s]
=> [Injection(f,s,s) => Surjection(f,s,s)]]
Detach, 46, 5
48 [FiniteB(s) => ALL(f):[ALL(a):[a e s => f(a) e s]
=> [Injection(f,s,s) => Surjection(f,s,s)]]]
& [ALL(f):[ALL(a):[a e s => f(a) e s]
=> [Injection(f,s,s) => Surjection(f,s,s)]] => FiniteB(s)]
Iff-And, 47
49 FiniteB(s) => ALL(f):[ALL(a):[a e s => f(a) e s]
=> [Injection(f,s,s) => Surjection(f,s,s)]]
Split, 48
50 ALL(f):[ALL(a):[a e s => f(a) e s]
=> [Injection(f,s,s) => Surjection(f,s,s)]] => FiniteB(s)
Split, 48
51 ALL(f):[ALL(a):[a e s => f(a) e s]
=> [Injection(f,s,s) => Surjection(f,s,s)]]
Detach, 49, 45
Apply definition of FiniteA
52 Set(s) => [FiniteA(s)
<=> ALL(x0):ALL(f):[x0 e s
& ALL(a):[a e s => f(a) e s]
=> [Injection(f,s,s) => EXIST(xn):[xn e s & f(xn)=x0]]]]
U Spec, 1
53 FiniteA(s)
<=> ALL(x0):ALL(f):[x0 e s
& ALL(a):[a e s => f(a) e s]
=> [Injection(f,s,s) => EXIST(xn):[xn e s & f(xn)=x0]]]
Detach, 52, 5
54 [FiniteA(s) => ALL(x0):ALL(f):[x0 e s
& ALL(a):[a e s => f(a) e s]
=> [Injection(f,s,s) => EXIST(xn):[xn e s & f(xn)=x0]]]]
& [ALL(x0):ALL(f):[x0 e s
& ALL(a):[a e s => f(a) e s]
=> [Injection(f,s,s) => EXIST(xn):[xn e s & f(xn)=x0]]] => FiniteA(s)]
Iff-And, 53
55 FiniteA(s) => ALL(x0):ALL(f):[x0 e s
& ALL(a):[a e s => f(a) e s]
=> [Injection(f,s,s) => EXIST(xn):[xn e s & f(xn)=x0]]]
Split, 54
Sufficient: FiniteA(s)
56 ALL(x0):ALL(f):[x0 e s
& ALL(a):[a e s => f(a) e s]
=> [Injection(f,s,s) => EXIST(xn):[xn e s & f(xn)=x0]]] => FiniteA(s)
Split, 54
Prove: ALL(x0):ALL(f):[x0 e s
& ALL(a):[a e s => f(a) e s]
=> [Injection(f,s,s) => EXIST(xn):[xn e s & f(xn)=x0]]] => FiniteA(s)
Suppose...
57 x0 e s
& ALL(a):[a e s => f(a) e s]
Premise
58 x0 e s
Split, 57
59 ALL(a):[a e s => f(a) e s]
Split, 57
Prove: Injection(f,s,s) => EXIST(xn):[xn e s & f(xn)=x0]]
Suppose...
60 Injection(f,s,s)
Premise
Apply definition of Injection
61 ALL(a):ALL(b):[Injection(f,a,b)
<=> ALL(c):ALL(d):[c e a & d e a => [f(c)=f(d) => c=d]]]
U Spec, 3
62 ALL(b):[Injection(f,s,b)
<=> ALL(c):ALL(d):[c e s & d e s => [f(c)=f(d) => c=d]]]
U Spec, 61
63 Injection(f,s,s)
<=> ALL(c):ALL(d):[c e s & d e s => [f(c)=f(d) => c=d]]
U Spec, 62
64 [Injection(f,s,s) => ALL(c):ALL(d):[c e s & d e s => [f(c)=f(d) => c=d]]]
& [ALL(c):ALL(d):[c e s & d e s => [f(c)=f(d) => c=d]] => Injection(f,s,s)]
Iff-And, 63
65 Injection(f,s,s) => ALL(c):ALL(d):[c e s & d e s => [f(c)=f(d) => c=d]]
Split, 64
66 ALL(c):ALL(d):[c e s & d e s => [f(c)=f(d) => c=d]] => Injection(f,s,s)
Split, 64
67 ALL(c):ALL(d):[c e s & d e s => [f(c)=f(d) => c=d]]
Detach, 65, 60
Apply premise
68 ALL(a):[a e s => f(a) e s]
=> [Injection(f,s,s) => Surjection(f,s,s)]
U Spec, 51
69 Injection(f,s,s) => Surjection(f,s,s)
Detach, 68, 59
70 Surjection(f,s,s)
Detach, 69, 60
Apply definition of Surjection
71 ALL(a):ALL(b):[Surjection(f,a,b) <=> ALL(c):[c e b => EXIST(d):[d e a & f(d)=c]]]
U Spec, 4
72 ALL(b):[Surjection(f,s,b) <=> ALL(c):[c e b => EXIST(d):[d e s & f(d)=c]]]
U Spec, 71
73 Surjection(f,s,s) <=> ALL(c):[c e s => EXIST(d):[d e s & f(d)=c]]
U Spec, 72
74 [Surjection(f,s,s) => ALL(c):[c e s => EXIST(d):[d e s & f(d)=c]]]
& [ALL(c):[c e s => EXIST(d):[d e s & f(d)=c]] => Surjection(f,s,s)]
Iff-And, 73
75 Surjection(f,s,s) => ALL(c):[c e s => EXIST(d):[d e s & f(d)=c]]
Split, 74
76 ALL(c):[c e s => EXIST(d):[d e s & f(d)=c]] => Surjection(f,s,s)
Split, 74
77 ALL(c):[c e s => EXIST(d):[d e s & f(d)=c]]
Detach, 75, 70
78 x0 e s => EXIST(d):[d e s & f(d)=x0]
U Spec, 77
79 EXIST(d):[d e s & f(d)=x0]
Detach, 78, 58
As Required:
80 Injection(f,s,s) => EXIST(d):[d e s & f(d)=x0]
4 Conclusion, 60
As Required:
81 ALL(x0):ALL(f):[x0 e s
& ALL(a):[a e s => f(a) e s]
=> [Injection(f,s,s) => EXIST(d):[d e s & f(d)=x0]]]
4 Conclusion, 57
82 FiniteA(s)
Detach, 56, 81
As Required:
83 FiniteB(s) => FiniteA(s)
4 Conclusion, 45
84 [FiniteA(s) => FiniteB(s)]
& [FiniteB(s) => FiniteA(s)]
Join, 44, 83
85 FiniteA(s) <=> FiniteB(s)
Iff-And, 84
As Required:
86 ALL(s):[Set(s) => [FiniteA(s) <=> FiniteB(s)]]
4 Conclusion, 5