THEOREM

*******

ALL(x):ALL(z):[Set(x) & ALL(a):[a e x <=> a=z]

=> EXIST(fs):[Set(fs) & ALL(f):[f e fs <=> ALL(d):[d e x => f(d) e x]]

& ALL(f):[f e fs <=> f(z)=z]]]

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]]]]

Premise

Suppose...

2 Set(x) & ALL(a):[a e x <=> a=z]

Premise

3 Set(x)

Split, 2

4 ALL(a):[a e x <=> a=z]

Split, 2

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

U Spec, 1

6 Set(x) & EXIST(c):c e x & Set(x) => EXIST(c):[Set(c) & ALL(f):[f e c <=> ALL(d):[d e x => f(d) e x]]]

U Spec, 5

7 z e x <=> z=z

U Spec, 4

8 [z e x => z=z] & [z=z => z e x]

Iff-And, 7

9 z=z => z e x

Split, 8

10 z=z

Reflex

11 z e x

Detach, 9, 10

12 EXIST(c):c e x

E Gen, 11

13 Set(x) & EXIST(c):c e x

Join, 3, 12

14 Set(x) & EXIST(c):c e x & Set(x)

Join, 13, 3

15 EXIST(c):[Set(c) & ALL(f):[f e c <=> ALL(d):[d e x => f(d) e x]]]

Detach, 6, 14

16 Set(fs) & ALL(f):[f e fs <=> ALL(d):[d e x => f(d) e x]]

E Spec, 15

17 Set(fs)

Split, 16

18 ALL(f):[f e fs <=> ALL(d):[d e x => f(d) e x]]

Split, 16

Prove: ALL(f):[f e fs => f(z)=z]

Suppose...

19 f e fs

Premise

20 f e fs <=> ALL(d):[d e x => f(d) e x]

U Spec, 18

21 [f e fs => ALL(d):[d e x => f(d) e x]]

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

Iff-And, 20

22 f e fs => ALL(d):[d e x => f(d) e x]

Split, 21

23 ALL(d):[d e x => f(d) e x]

Detach, 22, 19

24 z e x => f(z) e x

U Spec, 23

25 f(z) e x

Detach, 24, 11

26 f(z) e x <=> f(z)=z

U Spec, 4, 25

27 [f(z) e x => f(z)=z] & [f(z)=z => f(z) e x]

Iff-And, 26

28 f(z) e x => f(z)=z

Split, 27

29 f(z)=z

Detach, 28, 25

As Required:

30 ALL(f):[f e fs => f(z)=z]

4 Conclusion, 19

Prove: ALL(f):[f(z)=z => f e fs]

Suppose...

31 f(z)=z

Premise

32 f e fs <=> ALL(d):[d e x => f(d) e x]

U Spec, 18

33 [f e fs => ALL(d):[d e x => f(d) e x]]

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

Iff-And, 32

34 ALL(d):[d e x => f(d) e x] => f e fs

Split, 33

Prove: ALL(d):[d e x => f(d) e x]

Suppose...

35 t e x

Premise

36 t e x <=> t=z

U Spec, 4

37 [t e x => t=z] & [t=z => t e x]

Iff-And, 36

38 t e x => t=z

Split, 37

39 t=z

Detach, 38, 35

40 f(t)=t

Substitute, 39, 31

41 f(t) e x

Substitute, 40, 35

As Required:

42 ALL(d):[d e x => f(d) e x]

4 Conclusion, 35

43 f e fs

Detach, 34, 42

As Required:

44 ALL(f):[f(z)=z => f e fs]

4 Conclusion, 31

45 ALL(f):[[f e fs => f(z)=z] & [f(z)=z => f e fs]]

Join, 30, 44

46 ALL(f):[f e fs <=> f(z)=z]

Iff-And, 45

47 Set(fs) & ALL(f):[f e fs <=> ALL(d):[d e x => f(d) e x]]

& ALL(f):[f e fs <=> f(z)=z]

Join, 16, 46

As Required:

48 ALL(x):ALL(z):[Set(x) & ALL(a):[a e x <=> a=z]

=> EXIST(fs):[Set(fs) & ALL(f):[f e fs <=> ALL(d):[d e x => f(d) e x]]

& ALL(f):[f e fs <=> f(z)=z]]]

4 Conclusion, 2