Existence of Identity Function
Prove: ALL(s):[Set(s) => EXIST(e):ALL(a):[a
s => e(a)=a]]
That is, for any set s, there exists an identity function on s.
Prove: EXIST(e):ALL(a):[as => e(a)=a] given...
1 Set(s)
Premise
Construct the Cartesian Product of s with itself.
Applying the Cartesain Product Axiom....
2 ALL(a1):ALL(a2):[Set(a1) & Set(a2) => EXIST(b):[Set'(b) & ALL(c1):ALL(c2):[(c1,c2)b <=> c1a1 & c2a2]]]
Cart Prod
3 ALL(a2):[Set(s) & Set(a2) => EXIST(b):[Set'(b) & ALL(c1):ALL(c2):[(c1,c2)b <=> c1s & c2a2]]]
U Spec, 2
4 Set(s) & Set(s) => EXIST(b):[Set'(b) & ALL(c1):ALL(c2):[(c1,c2)b <=> c1s & c2s]]
U Spec, 3
5 Set(s) & Set(s)
Join, 1, 1
6 EXIST(b):[Set'(b) & ALL(c1):ALL(c2):[(c1,c2)b <=> c1s & c2s]]
Detach, 4, 5
Define: s2, the Cartesian Product of s with itself
7 Set'(s2) & ALL(c1):ALL(c2):[(c1,c2)s2 <=> c1s & c2s]
E Spec, 6
8 Set'(s2)
Split, 7
9 ALL(c1):ALL(c2):[(c1,c2)s2 <=> c1s & c2s]
Split, 7
Construct f, as subset of s2.
Applying the Subset Axiom...
10 EXIST(f):[Set'(f) & ALL(a):ALL(b):[(a,b)f <=> (a,b)s2 & a=b]]
Subset, 8
Define: f, as subset of s2 such that...
11 Set'(f) & ALL(a):ALL(b):[(a,b)f <=> (a,b)s2 & a=b]
E Spec, 10
12 Set'(f)
Split, 11
13 ALL(a):ALL(b):[(a,b)f <=> (a,b)s2 & a=b]
Split, 11
Applying the defintion of a function of one variable...
14 ALL(f):ALL(a):ALL(b):[Set'(f)
& Set(a) & Set(b)
& ALL(c):[ca => EXIST(d):[db & (c,d)f]]
& ALL(c):ALL(d1):ALL(d2):[ca & d1b & d2b & (c,d1)f & (c,d2)f => d1=d2]
=> ALL(c):ALL(d):[ca & db => [d=f(c) <=> (c,d)f]]]
Function
15 ALL(a):ALL(b):[Set'(f)
& Set(a) & Set(b)
& ALL(c):[ca => EXIST(d):[db & (c,d)f]]
& ALL(c):ALL(d1):ALL(d2):[ca & d1b & d2b & (c,d1)f & (c,d2)f => d1=d2]
=> ALL(c):ALL(d):[ca & db => [d=f(c) <=> (c,d)f]]]
U Spec, 14
16 ALL(b):[Set'(f)
& Set(s) & Set(b)
& ALL(c):[cs => EXIST(d):[db & (c,d)f]]
& ALL(c):ALL(d1):ALL(d2):[cs & d1b & d2b & (c,d1)f & (c,d2)f => d1=d2]
=> ALL(c):ALL(d):[cs & db => [d=f(c) <=> (c,d)f]]]
U Spec, 15
Sufficient: For functionality of f
17 Set'(f)
& Set(s) & Set(s)
& ALL(c):[cs => EXIST(d):[ds & (c,d)f]]
& ALL(c):ALL(d1):ALL(d2):[cs & d1s & d2s & (c,d1)f & (c,d2)f => d1=d2]
=> ALL(c):ALL(d):[cs & ds => [d=f(c) <=> (c,d)f]]
U Spec, 16
Prove: (x,x)f given...
18 xs
Premise
Applying the definition of f...
19 ALL(b):[(x,b)f <=> (x,b)s2 & x=b]
U Spec, 13
20 (x,x)f <=> (x,x)s2 & x=x
U Spec, 19
21 [(x,x)f => (x,x)s2 & x=x]
& [(x,x)s2 & x=x => (x,x)f]
Iff-And, 20
22 (x,x)f => (x,x)s2 & x=x
Split, 21
Sufficient: For (x,x)f
23 (x,x)s2 & x=x => (x,x)f
Split, 21
Prove: (x,x)s2
Applying the defintion of s2...
24 ALL(c2):[(x,c2)s2 <=> xs & c2s]
U Spec, 9
25 (x,x)s2 <=> xs & xs
U Spec, 24
26 [(x,x)s2 => xs & xs] & [xs & xs => (x,x)s2]
Iff-And, 25
27 (x,x)s2 => xs & xs
Split, 26
28 xs & xs => (x,x)s2
Split, 26
29 xs & xs
Join, 18, 18
As Required:
30 (x,x)s2
Detach, 28, 29
31 x=x
Reflex
32 (x,x)s2 & x=x
Join, 30, 31
As Required:
33 (x,x)f
Detach, 23, 32
Joining results...
34 xs & (x,x)f
Join, 18, 33
Generalizing...
35 EXIST(d):[ds & (x,d)f]
E Gen, 34
For arbitrary x...
36 xs => EXIST(d):[ds & (x,d)f]
Conclusion, 18
Generalizing...
37 ALL(c):[cs => EXIST(d):[ds & (c,d)f]]
U Gen, 36
Prove: y1=y2 given...
38 xs & y1s & y2s & (x,y1)f & (x,y2)f
Premise
39 xs
Split, 38
40 y1s
Split, 38
41 y2s
Split, 38
42 (x,y1)f
Split, 38
43 (x,y2)f
Split, 38
Applying the definition of f...
44 ALL(b):[(x,b)f <=> (x,b)s2 & x=b]
U Spec, 13
45 (x,y1)f <=> (x,y1)s2 & x=y1
U Spec, 44
46 [(x,y1)f => (x,y1)s2 & x=y1]
& [(x,y1)s2 & x=y1 => (x,y1)f]
Iff-And, 45
47 (x,y1)f => (x,y1)s2 & x=y1
Split, 46
48 (x,y1)s2 & x=y1 => (x,y1)f
Split, 46
49 (x,y1)s2 & x=y1
Detach, 47, 42
50 (x,y1)s2
Split, 49
51 x=y1
Split, 49
52 (x,y2)f <=> (x,y2)s2 & x=y2
U Spec, 44
53 [(x,y2)f => (x,y2)s2 & x=y2]
& [(x,y2)s2 & x=y2 => (x,y2)f]
Iff-And, 52
54 (x,y2)f => (x,y2)s2 & x=y2
Split, 53
55 (x,y2)s2 & x=y2 => (x,y2)f
Split, 53
56 (x,y2)s2 & x=y2
Detach, 54, 43
57 (x,y2)s2
Split, 56
58 x=y2
Split, 56
As Required:
59 y1=y2
Substitute, 51, 58
For arbitrary x, y1, y2...
60 xs & y1s & y2s & (x,y1)f & (x,y2)f => y1=y2
Conclusion, 38
Generalizing...
61 ALL(d2):[xs & y1s & d2s & (x,y1)f & (x,d2)f => y1=d2]
U Gen, 60
62 ALL(d1):ALL(d2):[xs & d1s & d2s & (x,d1)f & (x,d2)f => d1=d2]
U Gen, 61
63 ALL(c):ALL(d1):ALL(d2):[cs & d1s & d2s & (c,d1)f & (c,d2)f => d1=d2]
U Gen, 62
64 Set'(f) & Set(s)
Join, 12, 1
65 Set'(f) & Set(s) & Set(s)
Join, 64, 1
66 Set'(f) & Set(s) & Set(s)
& ALL(c):[cs => EXIST(d):[ds & (c,d)f]]
Join, 65, 37
67 Set'(f) & Set(s) & Set(s)
& ALL(c):[cs => EXIST(d):[ds & (c,d)f]]
& ALL(c):ALL(d1):ALL(d2):[cs & d1s & d2s & (c,d1)f & (c,d2)f => d1=d2]
Join, 66, 63
As Required: f is a function
68 ALL(c):ALL(d):[cs & ds => [d=f(c) <=> (c,d)f]]
Detach, 17, 67
Prove: x=f(x) given...
69 xs
Premise
70 ALL(d):[xs & ds => [d=f(x) <=> (x,d)f]]
U Spec, 68
71 xs & xs => [x=f(x) <=> (x,x)f]
U Spec, 70
72 xs & xs
Join, 69, 69
73 x=f(x) <=> (x,x)f
Detach, 71, 72
74 [x=f(x) => (x,x)f] & [(x,x)f => x=f(x)]
Iff-And, 73
75 x=f(x) => (x,x)f
Split, 74
76 (x,x)f => x=f(x)
Split, 74
Prove: (x,x)f
Applying the definition of f...
77 ALL(b):[(x,b)f <=> (x,b)s2 & x=b]
U Spec, 13
78 (x,x)f <=> (x,x)s2 & x=x
U Spec, 77
79 [(x,x)f => (x,x)s2 & x=x]
& [(x,x)s2 & x=x => (x,x)f]
Iff-And, 78
80 (x,x)f => (x,x)s2 & x=x
Split, 79
81 (x,x)s2 & x=x => (x,x)f
Split, 79
Prove: (x,x)s2
Applying the definition of s2...
82 ALL(c2):[(x,c2)s2 <=> xs & c2s]
U Spec, 9
83 (x,x)s2 <=> xs & xs
U Spec, 82
84 [(x,x)s2 => xs & xs] & [xs & xs => (x,x)s2]
Iff-And, 83
85 (x,x)s2 => xs & xs
Split, 84
86 xs & xs => (x,x)s2
Split, 84
87 xs & xs
Join, 69, 69
As Required:
88 (x,x)s2
Detach, 86, 87
89 x=x
Reflex
90 (x,x)s2 & x=x
Join, 88, 89
91 (x,x)f
Detach, 81, 90
Applying the functionality of f...
92 ALL(d):[xs & ds => [d=f(x) <=> (x,d)f]]
U Spec, 68
93 xs & xs => [x=f(x) <=> (x,x)f]
U Spec, 92
94 x=f(x) <=> (x,x)f
Detach, 93, 72
95 [x=f(x) => (x,x)f] & [(x,x)f => x=f(x)]
Iff-And, 94
96 x=f(x) => (x,x)f
Split, 95
97 (x,x)f => x=f(x)
Split, 95
As Required:
98 x=f(x)
Detach, 97, 91
For arbitrary x...
99 xs => x=f(x)
Conclusion, 69
Generalizing...
100 ALL(a):[as => a=f(a)]
U Gen, 99
101 EXIST(e):ALL(a):[as => a=e(a)]
E Gen, 100
As Required:
102 EXIST(e):ALL(a):[as => e(a)=a]
Sym, 101
For arbitrary s...
103 Set(s) => EXIST(e):ALL(a):[as => e(a)=a]
Conclusion, 1
As Required:
Generalizing...
104 ALL(s):[Set(s) => EXIST(e):ALL(a):[as => e(a)=a]]
U Gen, 103