THEOREM

*******

ALL(x):ALL(y):ALL(fs):[Set(x) & Set(y) & Set(fs)

& EXIST(a):a e x

& ALL(f):[f e fs <=> ALL(a):[a e x => f(a) e y]]

& ~EXIST(a):a e y

=> ~EXIST(f):f e fs]

By Dan Christensen

2022-01-16

This machine-verified, formal proof was written with the aid of the author's DC Proof 2.0 software available at http://www.dcproof.com

PROOF

*****

Proposed Function Space axiom (functions of one variable)

1 ALL(a):ALL(b):[Set(a) & EXIST(c):c e a & Set(b) => EXIST(c):[Set(c) & ALL(f):[f e c <=> ALL(d):[d e a => f(d) e b]]]]

Axiom

Suppose...

2 Set(x) & Set(y) & Set(fs)

& EXIST(a):a e x

& ALL(f):[f e fs <=> ALL(a):[a e x => f(a) e y]]

& ~EXIST(a):a e y

Premise

3 Set(x)

Split, 2

4 Set(y)

Split, 2

5 Set(fs)

Split, 2

6 EXIST(a):a e x

Split, 2

7 ALL(f):[f e fs <=> ALL(a):[a e x => f(a) e y]]

Split, 2

8 ~EXIST(a):a e y

Split, 2

9 z e x

E Spec, 6

10 ~~ALL(a):~a e y

Quant, 8

11 ALL(a):~a e y

Rem DNeg, 10

Prove: ~EXIST(f):f e fs

Suppose to the contrary...

12 f e fs

Premise

13 f e fs <=> ALL(a):[a e x => f(a) e y]

U Spec, 7

14 [f e fs => ALL(a):[a e x => f(a) e y]]

& [ALL(a):[a e x => f(a) e y] => f e fs]

Iff-And, 13

15 f e fs => ALL(a):[a e x => f(a) e y]

Split, 14

16 ALL(a):[a e x => f(a) e y]

Detach, 15, 12

17 z e x => f(z) e y

U Spec, 16

18 f(z) e y

Detach, 17, 9

19 ~f(z) e y

U Spec, 11, 18

20 f(z) e y & ~f(z) e y

Join, 18, 19

As Required:

21 ~EXIST(f):f e fs

4 Conclusion, 12

As Required:

22 ALL(x):ALL(y):ALL(fs):[Set(x) & Set(y) & Set(fs)

& EXIST(a):a e x

& ALL(f):[f e fs <=> ALL(a):[a e x => f(a) e y]]

& ~EXIST(a):a e y

=> ~EXIST(f):f e fs]

4 Conclusion, 2