THEOREM
*******
Given any non-empty set x,
there exists a unique identity function idx: x -->
x.
ALL(x):[Set(x) &
EXIST(a):a e x
=> EXIST(idx):[ALL(a):[a e x => idx(a) e x] <-- Existence
& ALL(a):[a e x => idx(a)=a]
& ALL(idx'):[ALL(a):[a e x => idx'(a)=a]
<-- Uniqueness
=> ALL(a):[a e x => idx'(a)=idx(a)]]]]
By Dan Christensen
2022-02-01
This machine-verified, formal
proof was written with the aid of the author's DC Proof 2.0 freeware available
at http://www.dcproof.com
PROOF
*****
Let x be non-empty set
1 Set(x) & EXIST(a):a e x
Premise
2 Set(x)
Split, 1
3 EXIST(a):a e x
Split, 1
Apply Cartesian Product Axiom
4 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
5 ALL(a2):[Set(x) & Set(a2) => EXIST(b):[Set'(b) &
ALL(c1):ALL(c2):[(c1,c2) e b <=> c1 e x & c2 e a2]]]
U Spec, 4
6 Set(x) & Set(x) => EXIST(b):[Set'(b) &
ALL(c1):ALL(c2):[(c1,c2) e b <=> c1 e x & c2 e x]]
U Spec, 5
7 Set(x) & Set(x)
Join, 2, 2
8 EXIST(b):[Set'(b)
& ALL(c1):ALL(c2):[(c1,c2) e b <=> c1 e x & c2 e x]]
Detach, 6, 7
9 Set'(x2) & ALL(c1):ALL(c2):[(c1,c2) e x2 <=> c1 e x & c2 e x]
E Spec, 8
Define: x2
10 Set'(x2)
Split, 9
11 ALL(c1):ALL(c2):[(c1,c2) e x2 <=> c1 e x & c2 e x]
Split, 9
Apply Subset Axiom
12 EXIST(sub):[Set'(sub) & ALL(a):ALL(b):[(a,b) e sub <=> (a,b) e x2 & a=b]]
Subset, 10
13 Set'(eqx) & ALL(a):ALL(b):[(a,b) e eqx <=> (a,b) e x2 & a=b]
E Spec, 12
Define: eqx (equality relation
on x)
14 Set'(eqx)
Split, 13
15 ALL(a):ALL(b):[(a,b) e eqx <=> (a,b) e x2 & a=b]
Split, 13
Apply Function Axiom
16 ALL(dom):ALL(cod):ALL(gra):[Set(dom) & EXIST(a1):a1 e dom
&
Set(cod) & EXIST(a):a e cod & Set'(gra)
=>
[ALL(a1):ALL(b):[(a1,b) e gra => a1 e dom & b e cod]
&
ALL(a1):[a1 e dom => EXIST(b):[b e cod & (a1,b) e gra]]
&
ALL(a1):ALL(b1):ALL(b2):[a1 e dom & b1 e cod & b2 e cod
=>
[(a1,b1) e gra & (a1,b2) e gra => b1=b2]]
=>
EXIST(fun):ALL(a1):ALL(b):[a1 e dom & b e cod
=>
[fun(a1)=b <=> (a1,b) e gra]]]]
Function
17 ALL(cod):ALL(gra):[Set(x) &
EXIST(a1):a1 e x
&
Set(cod) & EXIST(a):a e cod & Set'(gra)
=>
[ALL(a1):ALL(b):[(a1,b) e gra => a1 e x & b e cod]
&
ALL(a1):[a1 e x =>
EXIST(b):[b e cod & (a1,b) e gra]]
&
ALL(a1):ALL(b1):ALL(b2):[a1 e x & b1 e cod & b2 e cod
=>
[(a1,b1) e gra & (a1,b2) e gra => b1=b2]]
=>
EXIST(fun):ALL(a1):ALL(b):[a1 e x & b e cod
=>
[fun(a1)=b <=> (a1,b) e gra]]]]
U Spec, 16
18 ALL(gra):[Set(x) &
EXIST(a1):a1 e x
&
Set(x) & EXIST(a):a e x & Set'(gra)
=>
[ALL(a1):ALL(b):[(a1,b) e gra => a1 e x & b e x]
&
ALL(a1):[a1 e x =>
EXIST(b):[b e x & (a1,b) e gra]]
&
ALL(a1):ALL(b1):ALL(b2):[a1 e x & b1 e x & b2 e x
=>
[(a1,b1) e gra & (a1,b2) e gra => b1=b2]]
=>
EXIST(fun):ALL(a1):ALL(b):[a1 e x & b e x
=>
[fun(a1)=b <=> (a1,b) e gra]]]]
U Spec, 17
19 Set(x) & EXIST(a1):a1 e x
&
Set(x) & EXIST(a):a e x & Set'(eqx)
=>
[ALL(a1):ALL(b):[(a1,b) e eqx => a1 e x & b e x]
&
ALL(a1):[a1 e x =>
EXIST(b):[b e x & (a1,b) e eqx]]
&
ALL(a1):ALL(b1):ALL(b2):[a1 e x & b1 e x & b2 e x
=>
[(a1,b1) e eqx & (a1,b2) e eqx => b1=b2]]
=>
EXIST(fun):ALL(a1):ALL(b):[a1 e x & b e x
=>
[fun(a1)=b <=> (a1,b) e eqx]]]
U Spec, 18
20 Set(x) & EXIST(a):a e x & Set(x)
Join, 1, 2
21 Set(x) & EXIST(a):a e x & Set(x) & EXIST(a):a e x
Join, 20, 3
22 Set(x) & EXIST(a):a e x & Set(x) & EXIST(a):a e x
&
Set'(eqx)
Join, 21, 14
Sufficient: For existence of function on x
23 ALL(a1):ALL(b):[(a1,b) e eqx => a1 e x & b e x]
&
ALL(a1):[a1 e x =>
EXIST(b):[b e x & (a1,b) e eqx]]
&
ALL(a1):ALL(b1):ALL(b2):[a1 e x & b1 e x & b2 e x
=>
[(a1,b1) e eqx & (a1,b2) e eqx => b1=b2]]
=>
EXIST(fun):ALL(a1):ALL(b):[a1 e x & b e x
=>
[fun(a1)=b <=> (a1,b) e eqx]]
Detach, 19, 22
Part 1
Prove: ALL(a1):ALL(b):[(a1,b) e eqx => a1 e x & b e x]
Suppose...
24 (t,u) e eqx
Premise
Apply definition of eqx
25 ALL(b):[(t,b) e eqx <=> (t,b) e x2 & t=b]
U Spec, 15
26 (t,u) e eqx <=> (t,u) e x2 & t=u
U Spec, 25
27 [(t,u) e eqx => (t,u) e x2 & t=u]
&
[(t,u) e x2 & t=u => (t,u) e eqx]
Iff-And, 26
28 (t,u) e eqx => (t,u) e x2 & t=u
Split, 27
29 (t,u) e x2 & t=u
Detach, 28, 24
30 (t,u) e x2
Split, 29
Apply definition of x2
31 ALL(c2):[(t,c2) e x2 <=> t e x & c2 e x]
U Spec, 11
32 (t,u) e x2 <=> t e x & u e x
U Spec, 31
33 [(t,u) e x2 => t e x & u e x]
&
[t e x & u e x => (t,u) e x2]
Iff-And, 32
34 (t,u) e x2 => t e x & u e x
Split, 33
35 t e x & u e x
Detach, 34, 30
Part 1
As Required:
36 ALL(a1):ALL(b):[(a1,b) e eqx => a1 e x & b e x]
4 Conclusion, 24
Part 2
Prove: ALL(a1):[a1 e x => EXIST(b):[b e x &
(a1,b) e eqx]]
Suppose...
37 t e x
Premise
Apply definiton of eqx
38 ALL(b):[(t,b) e eqx <=> (t,b) e x2 & t=b]
U Spec, 15
39 (t,t) e eqx <=> (t,t) e x2 & t=t
U Spec, 38
40 [(t,t) e eqx => (t,t) e x2 & t=t]
&
[(t,t) e x2 & t=t => (t,t) e eqx]
Iff-And, 39
41 (t,t) e x2 & t=t => (t,t) e eqx
Split, 40
42 ALL(c2):[(t,c2) e x2 <=> t e x & c2 e x]
U Spec, 11
43 (t,t) e x2 <=> t e x & t e x
U Spec, 42
44 [(t,t) e x2 => t e x & t e x]
&
[t e x & t e x => (t,t) e x2]
Iff-And, 43
45 t e x & t e x => (t,t) e x2
Split, 44
46 t e x & t e x
Join, 37, 37
47 (t,t) e x2
Detach, 45, 46
48 t=t
Reflex
49 (t,t) e x2 & t=t
Join, 47, 48
50 (t,t) e eqx
Detach, 41, 49
51 t e x & (t,t) e eqx
Join, 37, 50
52 EXIST(b):[b e x & (t,b) e eqx]
E Gen, 51
Part 2
As Required:
53 ALL(a1):[a1 e x =>
EXIST(b):[b e x & (a1,b) e eqx]]
4 Conclusion, 37
Part 3
Prove: ALL(a1):ALL(b1):ALL(b2):[a1 e x & b1 e x & b2 e x
=> [(a1,b1) e eqx &
(a1,b2) e eqx => b1=b2]]
Suppose...
54 t e x & u e x & v e x
Premise
55 t e x
Split, 54
56 u e x
Split, 54
57 v e x
Split, 54
Prove: (t,u)
e eqx & (t,v)
e eqx => u=v
Suppose...
58 (t,u) e eqx & (t,v) e eqx
Premise
59 (t,u) e eqx
Split, 58
60 (t,v) e eqx
Split, 58
Apply definiton of eqx
61 ALL(b):[(t,b) e eqx <=> (t,b) e x2 & t=b]
U Spec, 15
62 (t,u) e eqx <=> (t,u) e x2 & t=u
U Spec, 61
63 [(t,u) e eqx => (t,u) e x2 & t=u]
&
[(t,u) e x2 & t=u => (t,u) e eqx]
Iff-And, 62
64 (t,u) e eqx => (t,u) e x2 & t=u
Split, 63
65 (t,u) e x2 & t=u
Detach, 64, 59
66 t=u
Split, 65
67 (t,v) e eqx <=> (t,v) e x2 & t=v
U Spec, 61
68 [(t,v) e eqx => (t,v) e x2 & t=v]
&
[(t,v) e x2 & t=v => (t,v) e eqx]
Iff-And, 67
69 (t,v) e eqx => (t,v) e x2 & t=v
Split, 68
70 (t,v) e x2 & t=v
Detach, 69, 60
71 t=v
Split, 70
72 u=v
Substitute, 66,
71
As Required:
73 (t,u) e eqx & (t,v) e eqx => u=v
4 Conclusion, 58
Part 3
As Required:
74 ALL(a1):ALL(b1):ALL(b2):[a1 e x & b1 e x & b2 e x
=>
[(a1,b1) e eqx & (a1,b2) e eqx => b1=b2]]
4 Conclusion, 54
75 ALL(a1):ALL(b):[(a1,b) e eqx => a1 e x & b e x]
&
ALL(a1):[a1 e x =>
EXIST(b):[b e x & (a1,b) e eqx]]
Join, 36, 53
76 ALL(a1):ALL(b):[(a1,b) e eqx => a1 e x & b e x]
&
ALL(a1):[a1 e x =>
EXIST(b):[b e x & (a1,b) e eqx]]
&
ALL(a1):ALL(b1):ALL(b2):[a1 e x & b1 e x & b2 e x
=>
[(a1,b1) e eqx & (a1,b2) e eqx => b1=b2]]
Join, 75, 74
77 EXIST(fun):ALL(a1):ALL(b):[a1 e x & b e x
=>
[fun(a1)=b <=> (a1,b) e eqx]]
Detach, 23, 76
Define: idx (identity function
on x)
78 ALL(a1):ALL(b):[a1 e x & b e x
=>
[idx(a1)=b <=> (a1,b) e eqx]]
E Spec, 77
Prove: ALL(a):[a e x => idx(a) e x]
Suppose...
79 t e x
Premise
Apply definiton of eqx
80 t e x => EXIST(b):[b e x & (t,b) e eqx]
U Spec, 53
81 EXIST(b):[b e x & (t,b) e eqx]
Detach, 80, 79
82 u e x & (t,u) e eqx
E Spec, 81
83 u e x
Split, 82
84 (t,u) e eqx
Split, 82
Apply definition of idx
85 ALL(b):[t e x & b e x
=>
[idx(t)=b <=> (t,b) e eqx]]
U Spec, 78
86 t e x & u e x
=>
[idx(t)=u <=> (t,u) e eqx]
U Spec, 85
87 t e x & u e x
Join, 79, 83
88 idx(t)=u <=> (t,u) e eqx
Detach, 86, 87
89 [idx(t)=u => (t,u) e eqx] & [(t,u) e eqx => idx(t)=u]
Iff-And, 88
90 (t,u) e eqx => idx(t)=u
Split, 89
91 idx(t)=u
Detach, 90, 84
92 idx(t) e x
Substitute, 91,
83
As Required:
93 ALL(a):[a e x => idx(a) e x]
4 Conclusion, 79
Prove: ALL(a):[a e x => idx(a)=a]
Suppose...
94 t e x
Premise
95 t e x => EXIST(b):[b e x & (t,b) e eqx]
U Spec, 53
96 EXIST(b):[b e x & (t,b) e eqx]
Detach, 95, 94
97 u e x & (t,u) e eqx
E Spec, 96
98 u e x
Split, 97
99 (t,u) e eqx
Split, 97
100 ALL(b):[t e x & b e x
=>
[idx(t)=b <=> (t,b) e eqx]]
U Spec, 78
101 t e x & u e x
=>
[idx(t)=u <=> (t,u) e eqx]
U Spec, 100
102 t e x & u e x
Join, 94, 98
103 idx(t)=u <=> (t,u) e eqx
Detach, 101, 102
104 [idx(t)=u => (t,u) e eqx] & [(t,u) e eqx => idx(t)=u]
Iff-And, 103
105 (t,u) e eqx => idx(t)=u
Split, 104
106 idx(t)=u
Detach, 105, 99
107 ALL(b):[(t,b) e eqx <=> (t,b) e x2 & t=b]
U Spec, 15
108 (t,u) e eqx <=> (t,u) e x2 & t=u
U Spec, 107
109 [(t,u) e eqx => (t,u) e x2 & t=u]
&
[(t,u) e x2 & t=u => (t,u) e eqx]
Iff-And, 108
110 (t,u) e eqx => (t,u) e x2 & t=u
Split, 109
111 (t,u) e x2 & t=u
Detach, 110, 99
112 t=u
Split, 111
113 idx(t)=t
Substitute, 112,
106
As Required:
114 ALL(a):[a e x => idx(a)=a]
4 Conclusion, 94
Prove: idx is a unique function on
set x
Let idx' be a function like idx such that...
115 ALL(a):[a e x => idx'(a)=a]
Premise
Prove: ALL(a):[a e x => idx'(a)=idx(a)]
Suppose...
116 t e x
Premise
117 t e x => idx(t)=t
U Spec, 114
118 idx(t)=t
Detach, 117, 116
119 t e x => idx'(t)=t
U Spec, 115
120 idx'(t)=t
Detach, 119, 116
121 idx'(t)=idx(t)
Substitute, 118,
120
As Required:
122 ALL(a):[a e x => idx'(a)=idx(a)]
4 Conclusion, 116
As Required:
idx is a
unique function on set x
123 ALL(idx'):[ALL(a):[a e x => idx'(a)=a]
=>
ALL(a):[a e x => idx'(a)=idx(a)]]
4 Conclusion, 115
Joining results...
124 ALL(a):[a e x => idx(a) e x]
&
ALL(a):[a e x => idx(a)=a]
Join, 93, 114
125 ALL(a):[a e x => idx(a) e x]
&
ALL(a):[a e x => idx(a)=a]
&
ALL(idx'):[ALL(a):[a e x => idx'(a)=a]
=>
ALL(a):[a e x => idx'(a)=idx(a)]]
Join, 124, 123
As Required:
126 ALL(x):[Set(x) & EXIST(a):a e x
=>
EXIST(idx):[ALL(a):[a e x => idx(a) e x]
&
ALL(a):[a e x => idx(a)=a]
&
ALL(idx'):[ALL(a):[a e x => idx'(a)=a]
=>
ALL(a):[a e x => idx'(a)=idx(a)]]]]
4 Conclusion, 1