THEOREM
*******
EXIST(f):ALL(a):[a e null => f(a) e x] where null
is the empty set and x is an arbitrary function
Updated Function Axiom applied
on line 14
By Dan Christensen
2022-02-15
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
*****
Define: null (empty set)
1 Set(null)
Axiom
2 ALL(a):~a e null
Axiom
Define: x (arbitrary set)
3 Set(x)
Axiom
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(null) & Set(a2)
=> EXIST(b):[Set'(b) & ALL(c1):ALL(c2):[(c1,c2) e b <=> c1 e null & c2 e a2]]]
U Spec, 4
6 Set(null) & Set(x) =>
EXIST(b):[Set'(b) & ALL(c1):ALL(c2):[(c1,c2) e b <=> c1 e null & c2 e x]]
U Spec, 5
7 Set(null) & Set(x)
Join, 1, 3
8 EXIST(b):[Set'(b)
& ALL(c1):ALL(c2):[(c1,c2) e b <=> c1 e null & c2 e x]]
Detach, 6, 7
9 Set'(nx) & ALL(c1):ALL(c2):[(c1,c2) e nx <=> c1 e null & c2 e x]
E Spec, 8
Define: nx
(Cartesian product of sets null and x)
10 Set'(nx)
Split, 9
11 ALL(c1):ALL(c2):[(c1,c2) e nx <=> c1 e null & c2 e x]
Split, 9
12 Set(null) & Set(x)
Join, 1, 3
13 Set(null) & Set(x) & Set'(nx)
Join, 12, 10
Apply updated Function Axiom
14 ALL(dom):ALL(cod):ALL(gra):[Set(dom) & Set(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
15 ALL(cod):ALL(gra):[Set(null) & Set(cod) & Set'(gra)
=>
[ALL(a1):ALL(b):[(a1,b) e gra => a1 e null & b e cod]
&
ALL(a1):[a1 e null =>
EXIST(b):[b e cod & (a1,b) e gra]]
&
ALL(a1):ALL(b1):ALL(b2):[a1 e null & b1 e cod & b2 e cod
=>
[(a1,b1) e gra & (a1,b2) e gra => b1=b2]]
=>
EXIST(fun):ALL(a1):ALL(b):[a1 e null & b e cod
=>
[fun(a1)=b <=> (a1,b) e gra]]]]
U Spec, 14
16 ALL(gra):[Set(null) & Set(x) & Set'(gra)
=>
[ALL(a1):ALL(b):[(a1,b) e gra => a1 e null & b e x]
&
ALL(a1):[a1 e null => EXIST(b):[b e x & (a1,b) e gra]]
&
ALL(a1):ALL(b1):ALL(b2):[a1 e null & b1 e x & b2 e x
=>
[(a1,b1) e gra & (a1,b2) e gra => b1=b2]]
=>
EXIST(fun):ALL(a1):ALL(b):[a1 e null & b e x
=>
[fun(a1)=b <=> (a1,b) e gra]]]]
U Spec, 15
17 Set(null) & Set(x) & Set'(nx)
=>
[ALL(a1):ALL(b):[(a1,b) e nx => a1 e null & b e x]
&
ALL(a1):[a1 e null =>
EXIST(b):[b e x & (a1,b) e nx]]
&
ALL(a1):ALL(b1):ALL(b2):[a1 e null & b1 e x & b2 e x
=>
[(a1,b1) e nx & (a1,b2) e nx => b1=b2]]
=>
EXIST(fun):ALL(a1):ALL(b):[a1 e null & b e x
=>
[fun(a1)=b <=> (a1,b) e nx]]]
U Spec, 16
18 Set(null) & Set(x)
Join, 1, 3
19 Set(null) & Set(x) & Set'(nx)
Join, 18, 10
Sufficient: For functionality
of nx
20 ALL(a1):ALL(b):[(a1,b) e nx => a1 e null & b e x]
&
ALL(a1):[a1 e null =>
EXIST(b):[b e x & (a1,b) e nx]]
&
ALL(a1):ALL(b1):ALL(b2):[a1 e null & b1 e x & b2 e x
=>
[(a1,b1) e nx & (a1,b2) e nx => b1=b2]]
=>
EXIST(fun):ALL(a1):ALL(b):[a1 e null & b e x
=>
[fun(a1)=b <=> (a1,b) e nx]]
Detach, 17, 19
Prove: ALL(a1):ALL(b):[(a1,b) e nx => a1 e null & b e x]
Suppose...
21 (t,u) e nx
Premise
Apply definition of nx
22 ALL(c2):[(t,c2) e nx <=> t e null & c2 e x]
U Spec, 11
23 (t,u) e nx <=> t e null & u e x
U Spec, 22
24 [(t,u) e nx => t e null & u e x]
&
[t e null & u e x => (t,u) e nx]
Iff-And, 23
25 (t,u) e nx => t e null & u e x
Split, 24
26 t e null & u e x
Detach, 25, 21
Part 1
27 ALL(a1):ALL(b):[(a1,b) e nx => a1 e null & b e x]
4 Conclusion, 21
Prove: ALL(a1):[a1 e null => EXIST(b):[b e x &
(a1,b) e nx]]
Suppose...
28 t e null
Premise
Apply definition of null
29 ~t e null
U Spec, 2
Apply vacuous truth
30 ~t e null => EXIST(b):[b e x & (t,b) e nx]
Arb Cons, 28
31 EXIST(b):[b e x & (t,b) e nx]
Detach, 30, 29
Part 2
32 ALL(a1):[a1 e null => EXIST(b):[b e x & (a1,b) e nx]]
4 Conclusion, 28
Prove: ALL(a1):ALL(b1):ALL(b2):[a1 e null & b1 e x & b2 e x
=> [(a1,b1) e nx &
(a1,b2) e nx => b1=b2]]
Suppose...
33 t e null & u e x & v e x
Premise
34 t e null
Split, 33
Apply definition of null
35 ~t e null
U Spec, 2
Apply vacuous truth
36 ~t e null => [(t,u) e nx & (t,v) e nx => u=v]
Arb Cons, 34
37 (t,u) e nx & (t,v) e nx => u=v
Detach, 36, 35
Part 3
38 ALL(a1):ALL(b1):ALL(b2):[a1 e null & b1 e x & b2 e x
=>
[(a1,b1) e nx & (a1,b2) e nx => b1=b2]]
4 Conclusion, 33
Joining results...
39 ALL(a1):ALL(b):[(a1,b) e nx => a1 e null & b e x]
&
ALL(a1):[a1 e null =>
EXIST(b):[b e x & (a1,b) e nx]]
Join, 27, 32
40 ALL(a1):ALL(b):[(a1,b) e nx => a1 e null & b e x]
&
ALL(a1):[a1 e null =>
EXIST(b):[b e x & (a1,b) e nx]]
&
ALL(a1):ALL(b1):ALL(b2):[a1 e null & b1 e x & b2 e x
=>
[(a1,b1) e nx & (a1,b2) e nx => b1=b2]]
Join, 39, 38
41 EXIST(fun):ALL(a1):ALL(b):[a1 e null & b e x
=>
[fun(a1)=b <=> (a1,b) e nx]]
Detach, 20, 40
Define: f (empty function)
42 ALL(a1):ALL(b):[a1 e null & b e x
=>
[f(a1)=b <=> (a1,b) e nx]]
E Spec, 41
Prove: ALL(a):[a e null => f(a) e x]
Suppose...
43 t e null
Premise
Apply Part 2
44 t e null => EXIST(b):[b e x & (t,b) e nx]
U Spec, 32
45 EXIST(b):[b e x & (t,b) e nx]
Detach, 44, 43
46 u e x & (t,u) e nx
E Spec, 45
47 u e x
Split, 46
48 (t,u) e nx
Split, 46
Apply definition of function f
49 ALL(b):[t e null & b e x
=>
[f(t)=b <=> (t,b) e nx]]
U Spec, 42
50 t e null & u e x
=>
[f(t)=u <=> (t,u) e nx]
U Spec, 49
51 t e null & u e x
Join, 43, 47
52 f(t)=u <=> (t,u) e nx
Detach, 50, 51
53 [f(t)=u => (t,u) e nx] & [(t,u) e nx => f(t)=u]
Iff-And, 52
54 (t,u) e nx => f(t)=u
Split, 53
55 f(t)=u
Detach, 54, 48
56 f(t) e x
Substitute, 55,
47
As Required:
57 ALL(a):[a e null => f(a) e x]
4 Conclusion, 43
As Required:
58 EXIST(f):ALL(a):[a e null => f(a) e x]
E Gen, 57