Define: f, a function mapping x to y
1 ALL(a):[a
x => f(a)
y]
Premise
Define: finv, the inverse of f
2 ALL(a):[a
x => finv(f(a))=a]
Premise
Suppose we have...
3 p
x
Premise
Applying the definition of f...
4 p
x => f(p)
y
U Spec, 1
5 f(p)
y
Detach, 4, 3
Applying the definition of finv...
6 p
x => finv(f(p))=p
U Spec, 2
7 finv(f(p))=p
Detach, 6, 3
Joining lines 5 and 7...
8 f(p)
y & finv(f(p))=p
Join, 5, 7
As Required:
9 EXIST(b):[b
y & finv(b)=p]
E Gen, 8
10 p
x => EXIST(b):[b
y & finv(b)=p]
Conclusion, 3
Generalizing...
11 ALL(a):[a
x => EXIST(b):[b
y & finv(b)=a]]
U Gen, 10