THEOREM
*******
On any non-empty set x there exists a unique identity function id: x --> x
ALL(x):[Set(x) & EXIST(a):a e x
=> EXIST(id):[ALL(a):[a e x => id(a)=a]
& ALL(id'):[ALL(a):[a e x => id'(a)=a] => id=id']]]
By Dan Christensen
2022-04-15
PROOF
*****
Suppose...
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 (Cartesian product)
10 Set'(x2)
Split, 9
11 ALL(c1):ALL(c2):[(c1,c2) e x2 <=> c1 e x & c2 e x]
Split, 9
12 EXIST(sub):[Set'(sub) & ALL(a):ALL(b):[(a,b) e sub <=> (a,b) e x2 & a=b]]
Subset, 10
13 Set'(g) & ALL(a):ALL(b):[(a,b) e g <=> (a,b) e x2 & a=b]
E Spec, 12
Define: g (graph set)
14 Set'(g)
Split, 13
15 ALL(a):ALL(b):[(a,b) e g <=> (a,b) e x2 & a=b]
Split, 13
Apply Function Axiom
16 ALL(dom):ALL(cod):ALL(gra):[Set(dom) & Set(cod) & Set'(gra)
& EXIST(a1):a1 e dom & EXIST(a1):a1 e cod
=> [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) & Set(cod) & Set'(gra)
& EXIST(a1):a1 e x & EXIST(a1):a1 e cod
=> [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) & Set(x) & Set'(gra)
& EXIST(a1):a1 e x & EXIST(a1):a1 e x
=> [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) & Set(x) & Set'(g)
& EXIST(a1):a1 e x & EXIST(a1):a1 e x
=> [ALL(a1):ALL(b):[(a1,b) e g => a1 e x & b e x]
& ALL(a1):[a1 e x => EXIST(b):[b e x & (a1,b) e g]]
& ALL(a1):ALL(b1):ALL(b2):[a1 e x & b1 e x & b2 e x
=> [(a1,b1) e g & (a1,b2) e g => b1=b2]]
=> EXIST(fun):ALL(a1):ALL(b):[a1 e x & b e x
=> [fun(a1)=b <=> (a1,b) e g]]]
U Spec, 18
20 Set(x) & Set(x) & Set'(g)
Join, 7, 14
21 Set(x) & Set(x) & Set'(g) & EXIST(a):a e x
Join, 20, 3
22 Set(x) & Set(x) & Set'(g) & EXIST(a):a e x
& EXIST(a):a e x
Join, 21, 3
Sufficient: For functionality of graph g
23 ALL(a1):ALL(b):[(a1,b) e g => a1 e x & b e x]
& ALL(a1):[a1 e x => EXIST(b):[b e x & (a1,b) e g]]
& ALL(a1):ALL(b1):ALL(b2):[a1 e x & b1 e x & b2 e x
=> [(a1,b1) e g & (a1,b2) e g => b1=b2]]
=> EXIST(fun):ALL(a1):ALL(b):[a1 e x & b e x
=> [fun(a1)=b <=> (a1,b) e g]]
Detach, 19, 22
Prove: ALL(a1):ALL(b):[(a1,b) e g => a1 e x & b e x]
Suppose...
24 (t,u) e g
Premise
25 ALL(b):[(t,b) e g <=> (t,b) e x2 & t=b]
U Spec, 15
26 (t,u) e g <=> (t,u) e x2 & t=u
U Spec, 25
27 [(t,u) e g => (t,u) e x2 & t=u]
& [(t,u) e x2 & t=u => (t,u) e g]
Iff-And, 26
28 (t,u) e g => (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
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
Step 1
As Required:
36 ALL(a1):ALL(b):[(a1,b) e g => a1 e x & b e x]
4 Conclusion, 24
Prove: ALL(a1):[a1 e x => EXIST(b):[b e x & (a1,b) e g]]
Suppose...
37 t e x
Premise
38 ALL(b):[(t,b) e g <=> (t,b) e x2 & t=b]
U Spec, 15
39 (t,t) e g <=> (t,t) e x2 & t=t
U Spec, 38
40 [(t,t) e g => (t,t) e x2 & t=t]
& [(t,t) e x2 & t=t => (t,t) e g]
Iff-And, 39
41 (t,t) e x2 & t=t => (t,t) e g
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 g
Detach, 41, 49
51 t e x & (t,t) e g
Join, 37, 50
52 EXIST(b):[b e x & (t,b) e g]
E Gen, 51
Step 2
As Required:
53 ALL(a1):[a1 e x => EXIST(b):[b e x & (a1,b) e g]]
4 Conclusion, 37
Prove: ALL(a1):ALL(b1):ALL(b2):[a1 e x & b1 e x & b2 e x
=> [(a1,b1) e g & (a1,b2) e g => b1=b2]]
Suppose...
54 t e x & u1 e x & u2 e x
Premise
55 t e x
Split, 54
56 u1 e x
Split, 54
57 u2 e x
Split, 54
Prove: (t,u1) e g & (t,u2) e g => u1=u2
Suppose...
58 (t,u1) e g & (t,u2) e g
Premise
59 (t,u1) e g
Split, 58
60 (t,u2) e g
Split, 58
61 ALL(b):[(t,b) e g <=> (t,b) e x2 & t=b]
U Spec, 15
62 (t,u1) e g <=> (t,u1) e x2 & t=u1
U Spec, 61
63 [(t,u1) e g => (t,u1) e x2 & t=u1]
& [(t,u1) e x2 & t=u1 => (t,u1) e g]
Iff-And, 62
64 (t,u1) e g => (t,u1) e x2 & t=u1
Split, 63
65 (t,u1) e x2 & t=u1
Detach, 64, 59
66 t=u1
Split, 65
67 (t,u2) e g <=> (t,u2) e x2 & t=u2
U Spec, 61
68 [(t,u2) e g => (t,u2) e x2 & t=u2]
& [(t,u2) e x2 & t=u2 => (t,u2) e g]
Iff-And, 67
69 (t,u2) e g => (t,u2) e x2 & t=u2
Split, 68
70 (t,u2) e x2 & t=u2
Detach, 69, 60
71 t=u2
Split, 70
72 u1=u2
Substitute, 66, 71
As Required:
73 (t,u1) e g & (t,u2) e g => u1=u2
4 Conclusion, 58
Step 3
As Required:
74 ALL(a1):ALL(b1):ALL(b2):[a1 e x & b1 e x & b2 e x
=> [(a1,b1) e g & (a1,b2) e g => b1=b2]]
4 Conclusion, 54
75 ALL(a1):ALL(b):[(a1,b) e g => a1 e x & b e x]
& ALL(a1):[a1 e x => EXIST(b):[b e x & (a1,b) e g]]
Join, 36, 53
76 ALL(a1):ALL(b):[(a1,b) e g => a1 e x & b e x]
& ALL(a1):[a1 e x => EXIST(b):[b e x & (a1,b) e g]]
& ALL(a1):ALL(b1):ALL(b2):[a1 e x & b1 e x & b2 e x
=> [(a1,b1) e g & (a1,b2) e g => b1=b2]]
Join, 75, 74
77 EXIST(fun):ALL(a1):ALL(b):[a1 e x & b e x
=> [fun(a1)=b <=> (a1,b) e g]]
Detach, 23, 76
Define: Identity function id in terms of g
78 ALL(a1):ALL(b):[a1 e x & b e x
=> [id(a1)=b <=> (a1,b) e g]]
E Spec, 77
Prove: ALL(a):[a e x => id(a)=a]
Suppose...
79 t e x
Premise
80 t e x => EXIST(b):[b e x & (t,b) e g]
U Spec, 53
81 EXIST(b):[b e x & (t,b) e g]
Detach, 80, 79
82 u e x & (t,u) e g
E Spec, 81
83 u e x
Split, 82
84 (t,u) e g
Split, 82
85 ALL(b):[(t,b) e g <=> (t,b) e x2 & t=b]
U Spec, 15
86 (t,u) e g <=> (t,u) e x2 & t=u
U Spec, 85
87 [(t,u) e g => (t,u) e x2 & t=u]
& [(t,u) e x2 & t=u => (t,u) e g]
Iff-And, 86
88 (t,u) e g => (t,u) e x2 & t=u
Split, 87
89 (t,u) e x2 & t=u
Detach, 88, 84
90 (t,u) e x2
Split, 89
91 t=u
Split, 89
92 ALL(b):[t e x & b e x
=> [id(t)=b <=> (t,b) e g]]
U Spec, 78
93 t e x & u e x
=> [id(t)=u <=> (t,u) e g]
U Spec, 92
94 t e x & u e x
Join, 79, 83
95 id(t)=u <=> (t,u) e g
Detach, 93, 94
96 [id(t)=u => (t,u) e g] & [(t,u) e g => id(t)=u]
Iff-And, 95
97 (t,u) e g => id(t)=u
Split, 96
98 id(t)=u
Detach, 97, 84
99 id(t)=t
Substitute, 91, 98
As Required:
100 ALL(a):[a e x => id(a)=a]
4 Conclusion, 79
Prove: ALL(id'):[ALL(a):[a e x => id'(a)=a] => id=id']
Suppose...
101 ALL(a):[a e x => id'(a)=a]
Premise
Prove: ALL(a):[a e x => id'(a)=id(a)]
Suppose...
102 t e x
Premise
103 t e x => id(t)=t
U Spec, 100
104 id(t)=t
Detach, 103, 102
105 t e x => id'(t)=t
U Spec, 101
106 id'(t)=t
Detach, 105, 102
107 id'(t)=id(t)
Substitute, 104, 106
As Required:
108 ALL(a):[a e x => id'(a)=id(a)]
4 Conclusion, 102
109 ALL(dom):ALL(cod):ALL(f1):ALL(f2):[Set(dom) & Set(cod)
& EXIST(a):a e dom & EXIST(a):a e cod
& ALL(a):[a e dom => f1(a) e cod]
& ALL(a):[a e dom => f2(a) e cod]
=> [f1=f2 <=> ALL(a):[a e dom => f1(a)=f2(a)]]]
Fn Equality
110 ALL(cod):ALL(f1):ALL(f2):[Set(x) & Set(cod)
& EXIST(a):a e x & EXIST(a):a e cod
& ALL(a):[a e x => f1(a) e cod]
& ALL(a):[a e x => f2(a) e cod]
=> [f1=f2 <=> ALL(a):[a e x => f1(a)=f2(a)]]]
U Spec, 109
111 ALL(f1):ALL(f2):[Set(x) & Set(x)
& EXIST(a):a e x & EXIST(a):a e x
& ALL(a):[a e x => f1(a) e x]
& ALL(a):[a e x => f2(a) e x]
=> [f1=f2 <=> ALL(a):[a e x => f1(a)=f2(a)]]]
U Spec, 110
112 ALL(f2):[Set(x) & Set(x)
& EXIST(a):a e x & EXIST(a):a e x
& ALL(a):[a e x => id(a) e x]
& ALL(a):[a e x => f2(a) e x]
=> [id=f2 <=> ALL(a):[a e x => id(a)=f2(a)]]]
U Spec, 111
113 Set(x) & Set(x)
& EXIST(a):a e x & EXIST(a):a e x
& ALL(a):[a e x => id(a) e x]
& ALL(a):[a e x => id'(a) e x]
=> [id=id' <=> ALL(a):[a e x => id(a)=id'(a)]]
U Spec, 112
Prove: ALL(a):[a e x => id(a) e x]
Suppose...
114 t e x
Premise
115 t e x => id(t)=t
U Spec, 100
116 id(t)=t
Detach, 115, 114
117 id(t) e x
Substitute, 116, 114
As Required:
118 ALL(a):[a e x => id(a) e x]
4 Conclusion, 114
Prove: ALL(a):[a e x => id'(a) e x]
Suppose...
119 t e x
Premise
120 t e x => id'(t)=t
U Spec, 101
121 id'(t)=t
Detach, 120, 119
122 id'(t) e x
Substitute, 121, 119
As Required:
123 ALL(a):[a e x => id'(a) e x]
4 Conclusion, 119
124 Set(x) & Set(x)
Join, 2, 2
125 Set(x) & Set(x) & EXIST(a):a e x
Join, 124, 3
126 Set(x) & Set(x) & EXIST(a):a e x & EXIST(a):a e x
Join, 125, 3
127 Set(x) & Set(x) & EXIST(a):a e x & EXIST(a):a e x
& ALL(a):[a e x => id(a) e x]
Join, 126, 118
128 Set(x) & Set(x) & EXIST(a):a e x & EXIST(a):a e x
& ALL(a):[a e x => id(a) e x]
& ALL(a):[a e x => id'(a) e x]
Join, 127, 123
129 id=id' <=> ALL(a):[a e x => id(a)=id'(a)]
Detach, 113, 128
130 [id=id' => ALL(a):[a e x => id(a)=id'(a)]]
& [ALL(a):[a e x => id(a)=id'(a)] => id=id']
Iff-And, 129
131 ALL(a):[a e x => id(a)=id'(a)] => id=id'
Split, 130
132 ALL(a):[a e x => id'(a)=id(a)] => id=id'
Sym, 131
133 id=id'
Detach, 132, 108
As Required:
134 ALL(id'):[ALL(a):[a e x => id'(a)=a] => id=id']
4 Conclusion, 101
135 ALL(a):[a e x => id(a)=a]
& ALL(id'):[ALL(a):[a e x => id'(a)=a] => id=id']
Join, 100, 134
As Required:
136 ALL(x):[Set(x) & EXIST(a):a e x
=> EXIST(id):[ALL(a):[a e x => id(a)=a]
& ALL(id'):[ALL(a):[a e x => id'(a)=a] => id=id']]]
4 Conclusion, 1