THEOREM
*******
The union of the set of all fison's is the set of natural numbers.
ufisons=n
where
n
= the set of natural numbers
<=
= partial ordering on n
fisons = set of all
FISON's = {{0}, {0,1}, {0,1,2}, ... }
ufisons = union of
fisons
= U {{0}, {0,1}, {0,1,2}, ... }
OUTLINE OF PROOF
****************
Lines
7-21 Construct ufisons:
ALL(b):[b e ufisons <=> EXIST(c):[c e fisons & b e c]]
22-29 Determine sufficient conditions for equality:
ALL(c):[c e ufisons <=> c e n] => ufisons=n
30-49 Prove: ALL(c):[c e ufisons => c e n]
50-108 Prove: ALL(c):[c e n => c e ufisons]
This machine-verified formal
proof was written with the aid of the author’s DC Proof 2.0 proof-checking
software available at http://www.dcproof.com
AXIOMS
******
1 Set(n)
Axiom
Define: <= on n
2 ALL(a):[a e n => a<=a]
Axiom
3 ALL(a):ALL(b):[a e n & b e n => [a<=b & b<=a => a=b]]
Axiom
Define: fisons
(See formal
construction here, lines 5-52)
4 Set(fisons)
&
ALL(a):[a e fisons
<=>
Set(a) & ALL(b):[b e a => b e n]
&
EXIST(b):[b e n & ALL(c):[c e n => [c e a <=> c<=b]]]]
Axiom
5 Set(fisons)
Split, 4
6 ALL(a):[a e fisons
<=>
Set(a) & ALL(b):[b e a => b e n]
&
EXIST(b):[b e n & ALL(c):[c e n => [c e a <=> c<=b]]]]
Split, 4
PROOF
*****
Apply Axiom of Arbitrary Union
7 ALL(f):[Set(f) & ALL(a):[a e f => Set(a)]
=>
EXIST(a):[Set(a) & ALL(b):[b e a <=> EXIST(c):[c e f & b e c]]]]
Arb Union
8 Set(fisons) & ALL(a):[a e fisons => Set(a)]
=>
EXIST(a):[Set(a) & ALL(b):[b e a <=> EXIST(c):[c e fisons & b e c]]]
U Spec, 7
Prove: ALL(a):[a e fisons => Set(a)]
Suppose...
9 x e fisons
Premise
Apply defintion of fisons
10 x e fisons
<=>
Set(x) & ALL(b):[b e x => b e n]
&
EXIST(b):[b e n & ALL(c):[c e n => [c e x <=> c<=b]]]
U Spec, 6
11 [x e fisons => Set(x) & ALL(b):[b e x => b e n]
&
EXIST(b):[b e n & ALL(c):[c e n => [c e x <=> c<=b]]]]
&
[Set(x) & ALL(b):[b e x => b e n]
&
EXIST(b):[b e n & ALL(c):[c e n => [c e x <=> c<=b]]] => x e fisons]
Iff-And, 10
12 x e fisons => Set(x) & ALL(b):[b e x => b e n]
&
EXIST(b):[b e n & ALL(c):[c e n => [c e x <=> c<=b]]]
Split, 11
13 Set(x) & ALL(b):[b e x => b e n]
&
EXIST(b):[b e n & ALL(c):[c e n => [c e x <=> c<=b]]] => x e fisons
Split, 11
14 Set(x) & ALL(b):[b e x => b e n]
&
EXIST(b):[b e n & ALL(c):[c e n => [c e x <=> c<=b]]]
Detach, 12, 9
15 Set(x)
Split, 14
As Required:
16 ALL(a):[a e fisons => Set(a)]
4 Conclusion, 9
17 Set(fisons) & ALL(a):[a e fisons => Set(a)]
Join, 5, 16
18 EXIST(a):[Set(a) & ALL(b):[b e a <=>
EXIST(c):[c e fisons & b e c]]]
Detach, 8, 17
Define: ufisons
19 Set(ufisons) & ALL(b):[b e ufisons <=>
EXIST(c):[c e fisons & b e c]]
E Spec, 18
20 Set(ufisons)
Split, 19
21 ALL(b):[b e ufisons <=> EXIST(c):[c e fisons & b e c]]
Split, 19
Apply Axiom of Set Equality
22 ALL(a):ALL(b):[Set(a) & Set(b) => [a=b <=> ALL(c):[c e a <=> c e b]]]
Set Equality
23 ALL(b):[Set(ufisons) & Set(b)
=> [ufisons=b <=> ALL(c):[c e ufisons <=> c e b]]]
U Spec, 22
24 Set(ufisons) & Set(n) => [ufisons=n <=> ALL(c):[c e ufisons <=> c e n]]
U Spec, 23
25 Set(ufisons) & Set(n)
Join, 20, 1
26 ufisons=n <=> ALL(c):[c e ufisons <=> c e n]
Detach, 24, 25
27 [ufisons=n => ALL(c):[c e ufisons <=> c e n]]
&
[ALL(c):[c e ufisons <=> c e n] => ufisons=n]
Iff-And, 26
28 ufisons=n => ALL(c):[c e ufisons <=> c e n]
Split, 27
Sufficient: For ufisons=n
29 ALL(c):[c e ufisons <=> c e n] => ufisons=n
Split, 27
Prove: ALL(c):[c e ufisons => c e n]
Suppose...
30 x e ufisons
Premise
Apply definition of ufisons
31 x e ufisons <=>
EXIST(c):[c e fisons & x e c]
U Spec, 21
32 [x e ufisons => EXIST(c):[c e fisons & x e c]]
&
[EXIST(c):[c e fisons & x e c] => x e ufisons]
Iff-And, 31
33 x e ufisons => EXIST(c):[c e fisons & x e c]
Split, 32
34 EXIST(c):[c e fisons & x e c] => x e ufisons
Split, 32
35 EXIST(c):[c e fisons & x e c]
Detach, 33, 30
Define: y
36 y e fisons & x e y
E Spec, 35
37 y e fisons
Split, 36
38 x e y
Split, 36
Apply definition of fisons
39 y e fisons
<=>
Set(y) & ALL(b):[b e y => b e n]
&
EXIST(b):[b e n & ALL(c):[c e n => [c e y <=> c<=b]]]
U Spec, 6
40 [y e fisons => Set(y) & ALL(b):[b e y => b e n]
&
EXIST(b):[b e n & ALL(c):[c e n => [c e y <=> c<=b]]]]
&
[Set(y) & ALL(b):[b e y => b e n]
&
EXIST(b):[b e n & ALL(c):[c e n => [c e y <=> c<=b]]] => y e fisons]
Iff-And, 39
41 y e fisons => Set(y) & ALL(b):[b e y => b e n]
&
EXIST(b):[b e n & ALL(c):[c e n => [c e y <=> c<=b]]]
Split, 40
42 Set(y) & ALL(b):[b e y => b e n]
&
EXIST(b):[b e n & ALL(c):[c e n => [c e y <=> c<=b]]] => y e fisons
Split, 40
43 Set(y) & ALL(b):[b e y => b e n]
&
EXIST(b):[b e n & ALL(c):[c e n => [c e y <=> c<=b]]]
Detach, 41, 37
44 Set(y)
Split, 43
45 ALL(b):[b e y => b e n]
Split, 43
46 EXIST(b):[b e n & ALL(c):[c e n => [c e y <=> c<=b]]]
Split, 43
47 x e y => x e n
U Spec, 45
48 x e n
Detach, 47, 38
As Required:
49 ALL(c):[c e ufisons => c e n]
4 Conclusion, 30
Prove: ALL(c):[c e n => c e ufisons]
Suppose...
50 x e n
Premise
Apply definition of ufisons
51 x e ufisons <=>
EXIST(c):[c e fisons & x e c]
U Spec, 21
52 [x e ufisons => EXIST(c):[c e fisons & x e c]]
&
[EXIST(c):[c e fisons & x e c] => x e ufisons]
Iff-And, 51
53 x e ufisons => EXIST(c):[c e fisons & x e c]
Split, 52
Sufficient: For x e ufisons
54 EXIST(c):[c e fisons & x e c] => x e ufisons
Split, 52
Apply Subset Axiom
55 EXIST(sub):[Set(sub) & ALL(a):[a e sub <=> a e n & a<=x]]
Subset, 1
Define: y
56 Set(y) & ALL(a):[a e y <=> a e n & a<=x]
E Spec, 55
57 Set(y)
Split, 56
58 ALL(a):[a e y <=> a e n & a<=x]
Split, 56
Apply definition of fisons
59 y e fisons
<=>
Set(y) & ALL(b):[b e y => b e n]
&
EXIST(b):[b e n & ALL(c):[c e n => [c e y <=> c<=b]]]
U Spec, 6
60 [y e fisons => Set(y) & ALL(b):[b e y => b e n]
&
EXIST(b):[b e n & ALL(c):[c e n => [c e y <=> c<=b]]]]
&
[Set(y) & ALL(b):[b e y => b e n]
&
EXIST(b):[b e n & ALL(c):[c e n => [c e y <=> c<=b]]] => y e fisons]
Iff-And, 59
61 y e fisons => Set(y) & ALL(b):[b e y => b e n]
&
EXIST(b):[b e n & ALL(c):[c e n => [c e y <=> c<=b]]]
Split, 60
Sufficient: For y e fisons
62 Set(y) & ALL(b):[b e y => b e n]
&
EXIST(b):[b e n & ALL(c):[c e n => [c e y <=> c<=b]]] => y e fisons
Split, 60
Prove: ALL(b):[b e y => b e n]
Suppose...
63 z e y
Premise
64 z e y <=> z e n & z<=x
U Spec, 58
65 [z e y => z e n & z<=x] & [z e n & z<=x => z e y]
Iff-And, 64
66 z e y => z e n & z<=x
Split, 65
67 z e n & z<=x => z e y
Split, 65
68 z e n & z<=x
Detach, 66, 63
69 z e n
Split, 68
As Required:
70 ALL(b):[b e y => b e n]
4 Conclusion, 63
Prove: ALL(c):[c e n => [c e y <=>
c<=x]]
Suppose...
71 z e n
Premise
Prove: z e y =>
z<=x
Suppose...
72 z e y
Premise
Apply definition of y
73 z e y <=> z e n & z<=x
U Spec, 58
74 [z e y => z e n & z<=x] & [z e n & z<=x => z e y]
Iff-And, 73
75 z e y => z e n & z<=x
Split, 74
76 z e n & z<=x => z e y
Split, 74
77 z e n & z<=x
Detach, 75, 72
78 z e n
Split, 77
79 z<=x
Split, 77
As Required:
80 z e y => z<=x
4 Conclusion, 72
Prove: z<=x => z e y
Suppose...
81 z<=x
Premise
82 z e y <=> z e n & z<=x
U Spec, 58
83 [z e y => z e n & z<=x] & [z e n & z<=x => z e y]
Iff-And, 82
84 z e y => z e n & z<=x
Split, 83
85 z e n & z<=x => z e y
Split, 83
86 z e n & z<=x
Join, 71, 81
87 z e y
Detach, 85, 86
As Required:
88 z<=x => z e y
4 Conclusion, 81
89 [z e y => z<=x] & [z<=x => z e y]
Join, 80, 88
90 z e y <=> z<=x
Iff-And, 89
As Required:
91 ALL(c):[c e n => [c e y <=> c<=x]]
4 Conclusion, 71
92 x e n & ALL(c):[c e n => [c e y <=> c<=x]]
Join, 50, 91
93 EXIST(b):[b e n & ALL(c):[c e n => [c e y <=> c<=b]]]
E Gen, 92
94 Set(y) & ALL(b):[b e y => b e n]
Join, 57, 70
95 Set(y) & ALL(b):[b e y => b e n]
&
EXIST(b):[b e n & ALL(c):[c e n => [c e y <=> c<=b]]]
Join, 94, 93
96 y e fisons
Detach, 62, 95
97 x e y <=> x e n & x<=x
U Spec, 58
98 [x e y => x e n & x<=x] & [x e n & x<=x => x e y]
Iff-And, 97
99 x e y => x e n & x<=x
Split, 98
Sufficient: For x e y
100 x e n & x<=x => x e y
Split, 98
101 x e n => x<=x
U Spec, 2
102 x<=x
Detach, 101, 50
103 x e n & x<=x
Join, 50, 102
104 x e y
Detach, 100, 103
105 y e fisons & x e y
Join, 96, 104
106 EXIST(c):[c e fisons & x e c]
E Gen, 105
107 x e ufisons
Detach, 54, 106
As Required:
108 ALL(c):[c e n => c e ufisons]
4 Conclusion, 50
109 ALL(c):[[c e ufisons => c e n] & [c e n => c e ufisons]]
Join, 49, 108
110 ALL(c):[c e ufisons <=> c e n]
Iff-And, 109
As Required:
111 ufisons=n
Detach, 29, 110