THEOREM
*******
ALL(x):ALL(y):[Set(x)
& Set(y)
=> EXIST(fxy):[Set(fxy) & ALL(f):[f e fxy <=> ALL(a1):[a1 e x => f(a1) e y]]
& ALL(fxy'):[Set(fxy') & ALL(f):[f e fxy' <=> ALL(a1):[a1 e x => f(a1) e y]] => fxy'=fxy]]]
By Dan Christensen
2022-03-23
PROOF
*****
Suppose x and y are sets
1 Set(x) & Set(y)
Premise
Apply Function Set Axiom (for 1 variable)
2 ALL(dom):ALL(cod):[Set(dom) & Set(cod)
=>
EXIST(fsp):[Set(fsp) & ALL(f):[f e fsp <=> ALL(a1):[a1 e dom => f(a1) e cod]]]]
Fn Space
3 ALL(cod):[Set(x) & Set(cod)
=>
EXIST(fsp):[Set(fsp) & ALL(f):[f e fsp <=> ALL(a1):[a1 e x => f(a1) e cod]]]]
U Spec, 2
4 Set(x) & Set(y)
=>
EXIST(fsp):[Set(fsp) & ALL(f):[f e fsp <=> ALL(a1):[a1 e x => f(a1) e y]]]
U Spec, 3
5 EXIST(fsp):[Set(fsp) & ALL(f):[f e fsp <=> ALL(a1):[a1 e x => f(a1) e y]]]
Detach, 4, 1
6 Set(fxy) &
ALL(f):[f e fxy <=>
ALL(a1):[a1 e x => f(a1) e y]]
E Spec, 5
Define: fxy (Function space of
all functions f: x --> y)
7 Set(fxy)
Split, 6
8 ALL(f):[f e fxy <=>
ALL(a1):[a1 e x => f(a1) e y]]
Split, 6
Define: fxy' (Another function
space of all functions f: x --> y)
9 Set(fxy') &
ALL(f):[f e fxy' <=>
ALL(a1):[a1 e x => f(a1) e y]]
Premise
Define: fxy'
10 Set(fxy')
Split, 9
11 ALL(f):[f e fxy' <=> ALL(a1):[a1 e x => f(a1) e y]]
Split, 9
Sufficient: For fxy'=fxy
18 ALL(c):[c e fxy' <=> c e fxy] => fxy'=fxy
Split, 17
As Required:
28 ALL(f):[f e fxy' => f e fxy]
5 Conclusion, 19
As Required:
38 ALL(f):[f e fxy => f e fxy']
5 Conclusion, 29
40 ALL(f):[f e fxy' <=> f e fxy]
Iff-And, 39
41 fxy'=fxy
Detach, 18, 40
42 ALL(fxy'):[Set(fxy') & ALL(f):[f e fxy' <=> ALL(a1):[a1 e x => f(a1) e y]]
=>
fxy'=fxy]
4 Conclusion, 9
Joining results...
43 Set(fxy) &
ALL(f):[f e fxy <=>
ALL(a1):[a1 e x => f(a1) e y]]
&
ALL(fxy'):[Set(fxy') & ALL(f):[f e fxy' <=> ALL(a1):[a1 e x => f(a1) e y]]
=>
fxy'=fxy]
Join, 6, 42
As Required:
44 ALL(x):ALL(y):[Set(x) & Set(y)
=>
EXIST(fxy):[Set(fxy) & ALL(f):[f e fxy <=> ALL(a1):[a1 e x => f(a1) e y]]
&
ALL(fxy'):[Set(fxy') & ALL(f):[f e fxy' <=> ALL(a1):[a1 e x => f(a1) e y]]
=>
fxy'=fxy]]]
4 Conclusion, 1