THEOREM
*******
Let fn be the set of functions (as sets of ordered pairs)
that map set n to itself.
Then, for all f, we have f e fn if and only
if
1. For all x in n,
f(x) is also in n, and
2. f is the set of ordered pairs (x, y), x e n and y e n such that (x, y) in f iff f(x)=y
This formal proof was written
and machine verified with the aid of the author's DC Proof 2.0 freeware
available http://www.dcproof.com
Dan Christensen
2021-7-5
AXIOMS
******
Let n be an arbitrary set
1 Set(n)
Axiom
Apply the Cartesian Product Axiom
2 ALL(a1):ALL(a2):[Set(a1)
& Set(a2) => EXIST(b):[Set'(b) & ALL(c1):ALL(c2):[(c1,c2) e b <=> c1 e a1 & c2 e a2]]]
Cart Prod
3 ALL(a2):[Set(n) & Set(a2)
=> EXIST(b):[Set'(b) & ALL(c1):ALL(c2):[(c1,c2) e b <=> c1 e n & c2 e a2]]]
U Spec, 2
4 Set(n) & Set(n) =>
EXIST(b):[Set'(b) & ALL(c1):ALL(c2):[(c1,c2) e b <=> c1 e n & c2 e n]]
U Spec, 3
5 Set(n) & Set(n)
Join, 1, 1
6 EXIST(b):[Set'(b)
& ALL(c1):ALL(c2):[(c1,c2) e b <=> c1 e n & c2 e n]]
Detach, 4, 5
7 Set'(n2) & ALL(c1):ALL(c2):[(c1,c2) e n2 <=> c1 e n & c2 e n]
E Spec, 6
Define: n2 (the Cartesian Product n*n)
8 Set'(n2)
Split, 7
9 ALL(c1):ALL(c2):[(c1,c2) e n2 <=> c1 e n & c2 e n]
Split, 7
Apply the Power Set Axiom
10 ALL(a):[Set'(a)
=> EXIST(b):[Set(b)
&
ALL(c):[c e b <=> Set'(c) & ALL(d1):ALL(d2):[(d1,d2) e c => (d1,d2) e a]]]]
Power Set
11 Set'(n2) => EXIST(b):[Set(b)
&
ALL(c):[c e b <=> Set'(c) & ALL(d1):ALL(d2):[(d1,d2) e c => (d1,d2) e n2]]]
U Spec, 10
12 EXIST(b):[Set(b)
&
ALL(c):[c e b <=> Set'(c) & ALL(d1):ALL(d2):[(d1,d2) e c => (d1,d2) e n2]]]
Detach, 11, 8
13 Set(pn2)
&
ALL(c):[c e pn2 <=> Set'(c) & ALL(d1):ALL(d2):[(d1,d2) e c => (d1,d2) e n2]]
E Spec, 12
Define: pn2 (the power set of n2)
14 Set(pn2)
Split, 13
15 ALL(c):[c e pn2 <=> Set'(c) &
ALL(d1):ALL(d2):[(d1,d2) e c => (d1,d2) e n2]]
Split, 13
Apply the Subset Axiom
16 EXIST(sub):[Set(sub)
& ALL(a):[a e sub <=> a e pn2 & ALL(b):[b e n =>
EXIST(c):[c e n & (b,c) e a & ALL(d):[d e n => [(b,d) e a => d=c]]]]]]
Subset, 14
17 Set(fn) & ALL(a):[a e fn <=> a e pn2 & ALL(b):[b e n =>
EXIST(c):[c e n & (b,c) e a & ALL(d):[d e n => [(b,d) e a => d=c]]]]]
E Spec, 16
Define: fn (set on functions mapping n --> n ?)
18 Set(fn)
Split, 17
19 ALL(a):[a e fn <=> a e pn2 & ALL(b):[b e n =>
EXIST(c):[c e n & (b,c) e a & ALL(d):[d e n => [(b,d) e a => d=c]]]]]
Split, 17
'=>'
Prove: ALL(f):[f e fn
=> ALL(a):[a e n => f(a) e n]
& [Set'(f)
& ALL(a1):ALL(b):[(a1,b) e f => a1 e n & b e n]
& ALL(a1):ALL(b):[a1 e n & b e n => [f(a1)=b <=> (a1,b) e f]]]]
Suppose...
20 f e fn
Premise
21 f e fn <=> f e pn2 & ALL(b):[b e n => EXIST(c):[c e n & (b,c) e f & ALL(d):[d e n => [(b,d) e f => d=c]]]]
U Spec, 19
22 [f e fn => f e pn2 & ALL(b):[b e n => EXIST(c):[c e n & (b,c) e f & ALL(d):[d e n => [(b,d) e f => d=c]]]]]
&
[f e pn2 & ALL(b):[b e n => EXIST(c):[c e n & (b,c) e f & ALL(d):[d e n => [(b,d) e f => d=c]]]] => f e fn]
Iff-And, 21
23 f e fn => f e pn2 & ALL(b):[b e n => EXIST(c):[c e n & (b,c) e f & ALL(d):[d e n => [(b,d) e f => d=c]]]]
Split, 22
24 f e pn2 & ALL(b):[b e n => EXIST(c):[c e n & (b,c) e f & ALL(d):[d e n => [(b,d) e f => d=c]]]]
Detach, 23, 20
25 f e pn2
Split, 24
26 ALL(b):[b e n =>
EXIST(c):[c e n & (b,c) e f & ALL(d):[d e n => [(b,d) e f => d=c]]]]
Split, 24
Apply the Function Axiom to obtain sufficient condtions
of the functionality of f
27 ALL(f):ALL(dom):ALL(cod):[Set'(f) &
Set(dom) & Set(cod)
=>
[ALL(a1):ALL(b):[(a1,b) e f => a1 e dom & b e cod]
&
ALL(a1):[a1 e dom => EXIST(b):[b e cod & (a1,b) e f]]
&
ALL(a1):ALL(b1):ALL(b2):[a1 e dom & b1 e cod & b2 e cod
=>
[(a1,b1) e f & (a1,b2) e f => b1=b2]]
=>
ALL(a1):ALL(b):[a1 e dom & b e cod => [f(a1)=b <=> (a1,b) e f]]]]
Function
28 ALL(dom):ALL(cod):[Set'(f) & Set(dom) & Set(cod)
=>
[ALL(a1):ALL(b):[(a1,b) e f => a1 e dom & b e cod]
&
ALL(a1):[a1 e dom => EXIST(b):[b e cod & (a1,b) e f]]
&
ALL(a1):ALL(b1):ALL(b2):[a1 e dom & b1 e cod & b2 e cod
=>
[(a1,b1) e f & (a1,b2) e f => b1=b2]]
=>
ALL(a1):ALL(b):[a1 e dom & b e cod => [f(a1)=b <=>
(a1,b) e f]]]]
U Spec, 27
29 ALL(cod):[Set'(f) & Set(n) & Set(cod)
=>
[ALL(a1):ALL(b):[(a1,b) e f => a1 e n & b e cod]
&
ALL(a1):[a1 e n =>
EXIST(b):[b e cod & (a1,b) e f]]
&
ALL(a1):ALL(b1):ALL(b2):[a1 e n & b1 e cod & b2 e cod
=>
[(a1,b1) e f & (a1,b2) e f => b1=b2]]
=>
ALL(a1):ALL(b):[a1 e n & b e cod => [f(a1)=b <=> (a1,b) e f]]]]
U Spec, 28
30 Set'(f) & Set(n) & Set(n)
=>
[ALL(a1):ALL(b):[(a1,b) e f => a1 e n & b e n]
&
ALL(a1):[a1 e n =>
EXIST(b):[b e n & (a1,b) e f]]
&
ALL(a1):ALL(b1):ALL(b2):[a1 e n & b1 e n & b2 e n
=>
[(a1,b1) e f & (a1,b2) e f => b1=b2]]
=>
ALL(a1):ALL(b):[a1 e n & b e n => [f(a1)=b <=> (a1,b) e f]]]
U Spec, 29
31 f e pn2 <=> Set'(f) & ALL(d1):ALL(d2):[(d1,d2) e f => (d1,d2) e n2]
U Spec, 15
32 [f e pn2 => Set'(f) & ALL(d1):ALL(d2):[(d1,d2) e f => (d1,d2) e n2]]
&
[Set'(f) & ALL(d1):ALL(d2):[(d1,d2) e f => (d1,d2) e n2] => f e pn2]
Iff-And, 31
33 f e pn2 => Set'(f) & ALL(d1):ALL(d2):[(d1,d2) e f => (d1,d2) e n2]
Split, 32
34 Set'(f) & ALL(d1):ALL(d2):[(d1,d2) e f => (d1,d2) e n2]
Detach, 33, 25
35 Set'(f)
Split, 34
36 ALL(d1):ALL(d2):[(d1,d2) e f => (d1,d2) e n2]
Split, 34
37 Set'(f) & Set(n)
Join, 35, 1
38 Set'(f) & Set(n) & Set(n)
Join, 37, 1
Sufficient: For functionality of f
39 ALL(a1):ALL(b):[(a1,b) e f => a1 e n & b e n]
&
ALL(a1):[a1 e n =>
EXIST(b):[b e n & (a1,b) e f]]
&
ALL(a1):ALL(b1):ALL(b2):[a1 e n & b1 e n & b2 e n
=>
[(a1,b1) e f & (a1,b2) e f => b1=b2]]
=>
ALL(a1):ALL(b):[a1 e n & b e n => [f(a1)=b <=> (a1,b) e f]]
Detach, 30, 38
Prove: ALL(a1):ALL(b):[(a1,b) e f => a1 e n & b e n]
Suppose...
40 (t,u) e f
Premise
41 ALL(d2):[(t,d2) e f => (t,d2) e n2]
U Spec, 36
42 (t,u) e f => (t,u) e n2
U Spec, 41
43 (t,u) e n2
Detach, 42, 40
44 ALL(c2):[(t,c2) e n2 <=> t e n & c2 e n]
U Spec, 9
45 (t,u) e n2 <=> t e n & u e n
U Spec, 44
46 [(t,u) e n2 => t e n & u e n]
&
[t e n & u e n => (t,u) e n2]
Iff-And, 45
47 (t,u) e n2 => t e n & u e n
Split, 46
48 t e n & u e n
Detach, 47, 43
Part 1
49 ALL(a1):ALL(b):[(a1,b) e f => a1 e n & b e n]
4 Conclusion, 40
Prove: ALL(a1):[a1 e n => EXIST(b):[b e n &
(a1,b) e f]]
Suppose...
50 t e n
Premise
51 t e n => EXIST(c):[c e n & (t,c) e f & ALL(d):[d e n => [(t,d) e f => d=c]]]
U Spec, 26
52 EXIST(c):[c e n & (t,c) e f & ALL(d):[d e n => [(t,d) e f => d=c]]]
Detach, 51, 50
53 u e n & (t,u) e f & ALL(d):[d e n => [(t,d) e f => d=u]]
E Spec, 52
54 u e n
Split, 53
55 (t,u) e f
Split, 53
56 u e n & (t,u) e f
Join, 54, 55
Part 2
57 ALL(a1):[a1 e n =>
EXIST(b):[b e n & (a1,b) e f]]
4 Conclusion, 50
Prove: ALL(a1):ALL(b1):ALL(b2):[a1 e n & b1 e n & b2 e n
=> [(a1,b1) e f & (a1,b2) e f => b1=b2]]
Suppose...
58 t e n & u1 e n & u2 e n
Premise
59 t e n
Split, 58
60 u1 e n
Split, 58
61 u2 e n
Split, 58
Prove: (t,u1) e f & (t,u2) e f => u1=u2
Suppose...
62 (t,u1) e f & (t,u2) e f
Premise
63 (t,u1) e f
Split, 62
64 (t,u2) e f
Split, 62
65 t e n => EXIST(c):[c e n & (t,c) e f & ALL(d):[d e n => [(t,d) e f => d=c]]]
U Spec, 26
66 EXIST(c):[c e n & (t,c) e f & ALL(d):[d e n => [(t,d) e f => d=c]]]
Detach, 65, 59
67 u3 e n & (t,u3) e f & ALL(d):[d e n => [(t,d) e f => d=u3]]
E Spec, 66
Define: u3
68 u3 e n
Split, 67
69 (t,u3) e f
Split, 67
70 ALL(d):[d e n => [(t,d) e f => d=u3]]
Split, 67
71 u1 e n => [(t,u1) e f => u1=u3]
U Spec, 70
72 (t,u1) e f => u1=u3
Detach, 71, 60
73 u1=u3
Detach, 72, 63
74 u2 e n => [(t,u2) e f => u2=u3]
U Spec, 70
75 (t,u2) e f => u2=u3
Detach, 74, 61
76 u2=u3
Detach, 75, 64
77 u1=u2
Substitute, 76,
73
As Required:
78 (t,u1) e f & (t,u2) e f => u1=u2
4 Conclusion, 62
Part 3
79 ALL(a1):ALL(b1):ALL(b2):[a1 e n & b1 e n & b2 e n
=>
[(a1,b1) e f & (a1,b2) e f => b1=b2]]
4 Conclusion, 58
80 ALL(a1):ALL(b):[(a1,b) e f => a1 e n & b e n]
&
ALL(a1):[a1 e n =>
EXIST(b):[b e n & (a1,b) e f]]
Join, 49, 57
81 ALL(a1):ALL(b):[(a1,b) e f => a1 e n & b e n]
&
ALL(a1):[a1 e n =>
EXIST(b):[b e n & (a1,b) e f]]
&
ALL(a1):ALL(b1):ALL(b2):[a1 e n & b1 e n & b2 e n
=>
[(a1,b1) e f & (a1,b2) e f => b1=b2]]
Join, 80, 79
f is a function
82 ALL(a1):ALL(b):[a1 e n & b e n => [f(a1)=b <=> (a1,b) e f]]
Detach, 39, 81
Suppose...
83 t e n
Premise
84 t e n => EXIST(b):[b e n & (t,b) e f]
U Spec, 57
85 EXIST(b):[b e n & (t,b) e f]
Detach, 84, 83
86 u e n & (t,u) e f
E Spec, 85
87 u e n
Split, 86
88 (t,u) e f
Split, 86
89 ALL(b):[t e n & b e n => [f(t)=b <=> (t,b) e f]]
U Spec, 82
90 t e n & u e n => [f(t)=u <=> (t,u) e f]
U Spec, 89
91 t e n & u e n
Join, 83, 87
92 f(t)=u <=> (t,u) e f
Detach, 90, 91
93 [f(t)=u => (t,u) e f] & [(t,u) e f => f(t)=u]
Iff-And, 92
94 (t,u) e f => f(t)=u
Split, 93
95 f(t)=u
Detach, 94, 88
96 f(t) e n
Substitute, 95,
87
f: n --> n
97 ALL(a):[a e n => f(a) e n]
4 Conclusion, 83
98 Set'(f)
&
ALL(a1):ALL(b):[(a1,b) e f => a1 e n & b e n]
Join, 35, 49
99 Set'(f)
&
ALL(a1):ALL(b):[(a1,b) e f => a1 e n & b e n]
&
ALL(a1):ALL(b):[a1 e n & b e n => [f(a1)=b <=> (a1,b) e f]]
Join, 98, 82
100 ALL(a):[a e n => f(a) e n]
&
[Set'(f)
&
ALL(a1):ALL(b):[(a1,b) e f => a1 e n & b e n]
&
ALL(a1):ALL(b):[a1 e n & b e n => [f(a1)=b <=> (a1,b) e f]]]
Join, 97, 99
'=>'
As Required:
101 ALL(f):[f e fn
=>
ALL(a):[a e n => f(a) e n]
&
[Set'(f)
&
ALL(a1):ALL(b):[(a1,b) e f => a1 e n & b e n]
&
ALL(a1):ALL(b):[a1 e n & b e n => [f(a1)=b <=> (a1,b) e f]]]]
4 Conclusion, 20
'<='
Prove: ALL(f):[ALL(a):[a e n => f(a) e n]
& [Set'(f)
& ALL(a1):ALL(b):[(a1,b) e f => a1 e n & b e n]
& ALL(a1):ALL(b):[a1
e n & b e n =>
[f(a1)=b <=> (a1,b) e f]]]
=> f e fn]
Suppose...
102 ALL(a):[a e n => f(a) e n]
&
[Set'(f)
&
ALL(a1):ALL(b):[(a1,b) e f => a1 e n & b e n]
&
ALL(a1):ALL(b):[a1 e n & b e n => [f(a1)=b <=> (a1,b) e f]]]
Premise
103 ALL(a):[a e n => f(a) e n]
Split, 102
104 Set'(f)
&
ALL(a1):ALL(b):[(a1,b) e f => a1 e n & b e n]
&
ALL(a1):ALL(b):[a1 e n & b e n => [f(a1)=b <=> (a1,b) e f]]
Split, 102
105 Set'(f)
Split, 104
106 ALL(a1):ALL(b):[(a1,b) e f => a1 e n & b e n]
Split, 104
107 ALL(a1):ALL(b):[a1 e n & b e n => [f(a1)=b <=> (a1,b) e f]]
Split, 104
108 f e fn <=> f e pn2 & ALL(b):[b e n => EXIST(c):[c e n & (b,c) e f & ALL(d):[d e n => [(b,d) e f => d=c]]]]
U Spec, 19
109 [f e fn => f e pn2 & ALL(b):[b e n => EXIST(c):[c e n & (b,c) e f & ALL(d):[d e n => [(b,d) e f => d=c]]]]]
&
[f e pn2 & ALL(b):[b e n => EXIST(c):[c e n & (b,c) e f & ALL(d):[d e n => [(b,d) e f => d=c]]]] => f e fn]
Iff-And, 108
110 f e fn => f e pn2 & ALL(b):[b e n => EXIST(c):[c e n & (b,c) e f & ALL(d):[d e n => [(b,d) e f => d=c]]]]
Split, 109
Sufficient: For f e fn
111 f e pn2 & ALL(b):[b e n => EXIST(c):[c e n & (b,c) e f & ALL(d):[d e n => [(b,d) e f => d=c]]]] => f e fn
Split, 109
112 f e pn2 <=> Set'(f) & ALL(d1):ALL(d2):[(d1,d2) e f => (d1,d2) e n2]
U Spec, 15
113 [f e pn2 => Set'(f) & ALL(d1):ALL(d2):[(d1,d2) e f => (d1,d2) e n2]]
&
[Set'(f) & ALL(d1):ALL(d2):[(d1,d2) e f => (d1,d2) e n2] => f e pn2]
Iff-And, 112
Sufficient: For f e pn2
114 Set'(f) & ALL(d1):ALL(d2):[(d1,d2) e f => (d1,d2) e n2] => f e pn2
Split, 113
Prove: ALL(d1):ALL(d2):[(d1,d2) e f => (d1,d2) e n2]
Suppose...
115 (t,u) e f
Premise
116 ALL(c2):[(t,c2) e n2 <=> t e n & c2 e n]
U Spec, 9
117 (t,u) e n2 <=> t e n & u e n
U Spec, 116
118 [(t,u) e n2 => t e n & u e n]
&
[t e n & u e n => (t,u) e n2]
Iff-And, 117
Sufficient: For (t,u)
e n2
119 t e n & u e n => (t,u) e n2
Split, 118
120 ALL(b):[(t,b) e f => t e n & b e n]
U Spec, 106
121 (t,u) e f => t e n & u e n
U Spec, 120
122 t e n & u e n
Detach, 121, 115
123 (t,u) e n2
Detach, 119, 122
As Required:
124 ALL(d1):ALL(d2):[(d1,d2) e f => (d1,d2) e n2]
4 Conclusion, 115
125 Set'(f)
&
ALL(d1):ALL(d2):[(d1,d2) e f => (d1,d2) e n2]
Join, 105, 124
As Required:
126 f e pn2
Detach, 114, 125
Prove: ALL(b):[b e n
=>
EXIST(c):[c e n & (b,c)
e f
& ALL(d):[d e n => [(b,d) e f => d=c]]]]
Suppose...
127 t e n
Premise
128 t e n => f(t) e n
U Spec, 103
129 f(t) e n
Detach, 128, 127
130 f(t)=f(t)
Reflex, 129
131 f(t) e n & f(t)=f(t)
Join, 129, 130
132 EXIST(a):[a e n & f(t)=a]
E Gen, 131
133 u e n & f(t)=u
E Spec, 132
134 u e n
Split, 133
135 f(t)=u
Split, 133
136 ALL(b):[t e n & b e n => [f(t)=b <=> (t,b) e f]]
U Spec, 107
137 t e n & u e n => [f(t)=u <=> (t,u) e f]
U Spec, 136
138 t e n & u e n
Join, 127, 134
139 f(t)=u <=> (t,u) e f
Detach, 137, 138
140 [f(t)=u => (t,u) e f] & [(t,u) e f => f(t)=u]
Iff-And, 139
141 f(t)=u => (t,u) e f
Split, 140
142 (t,u) e f
Detach, 141, 135
Prove: ALL(d):[d e n => [(t,d) e f => d=u]]
Suppose...
143 v e n
Premise
Prove: (t,v)
e f => v=u
Suppose...
144 (t,v) e f
Premise
145 ALL(b):[t e n & b e n => [f(t)=b <=> (t,b) e f]]
U Spec, 107
146 t e n & v e n => [f(t)=v <=> (t,v) e f]
U Spec, 145
147 t e n & v e n
Join, 127, 143
148 f(t)=v <=> (t,v) e f
Detach, 146, 147
149 [f(t)=v => (t,v) e f] & [(t,v) e f => f(t)=v]
Iff-And, 148
150 (t,v) e f => f(t)=v
Split, 149
151 f(t)=v
Detach, 150, 144
152 v=u
Substitute, 151,
135
As Required:
153 (t,v) e f => v=u
4 Conclusion, 144
As Required:
154 ALL(d):[d e n => [(t,d) e f => d=u]]
4 Conclusion, 143
155 u e n & (t,u) e f
Join, 134, 142
156 u e n & (t,u) e f
&
ALL(d):[d e n => [(t,d) e f => d=u]]
Join, 155, 154
As Required:
157 ALL(b):[b e n
=>
EXIST(c):[c e n & (b,c) e f
&
ALL(d):[d e n => [(b,d) e f => d=c]]]]
4 Conclusion, 127
158 f e pn2
&
ALL(b):[b e n
=>
EXIST(c):[c e n & (b,c) e f
&
ALL(d):[d e n => [(b,d) e f => d=c]]]]
Join, 126, 157
159 f e fn
Detach, 111, 158
'<='
As Required:
160 ALL(f):[ALL(a):[a e n => f(a) e n]
&
[Set'(f)
&
ALL(a1):ALL(b):[(a1,b) e f => a1 e n & b e n]
&
ALL(a1):ALL(b):[a1 e n & b e n => [f(a1)=b <=> (a1,b) e f]]]
=>
f e fn]
4 Conclusion, 102
161 ALL(f):[[f e fn
=>
ALL(a):[a e n => f(a) e n]
&
[Set'(f)
&
ALL(a1):ALL(b):[(a1,b) e f => a1 e n & b e n]
&
ALL(a1):ALL(b):[a1 e n & b e n => [f(a1)=b
<=> (a1,b) e f]]]] & [ALL(a):[a e n => f(a) e n]
&
[Set'(f)
&
ALL(a1):ALL(b):[(a1,b) e f => a1 e n & b e n]
&
ALL(a1):ALL(b):[a1 e n & b e n => [f(a1)=b <=> (a1,b) e f]]]
=>
f e fn]]
Join, 101, 160
As Required:
162 ALL(f):[f e fn
<=>
ALL(a):[a e n => f(a) e n]
&
[Set'(f)
&
ALL(a1):ALL(b):[(a1,b) e f => a1 e n & b e n]
&
ALL(a1):ALL(b):[a1 e n & b e n => [f(a1)=b <=> (a1,b) e f]]]]
Iff-And, 161