THEOREM

*******

Given:

ALL(a):[a e x <=> a=0 | a=1] (x = {0, 1}, line 3)

ALL(f):[f e fs <=> ALL(d):[d e x => f(d) e x]] (Function space fs, line 24)

f(0)=1 & f(1)=0 (line 25)

Prove:

f e fs

PROOF

*****

Proposed Function Space Axiom (for functions of 1 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

Define: x (x = {0, 1}

2 Set(x)

Axiom

3 ALL(a):[a e x <=> a=0 | a=1]

Axiom

Apply Function Space Axiom

4 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

5 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, 4

Apply definition of x

6 0 e x <=> 0=0 | 0=1

U Spec, 3

7 [0 e x => 0=0 | 0=1] & [0=0 | 0=1 => 0 e x]

Iff-And, 6

8 0=0 | 0=1 => 0 e x

Split, 7

9 0=0

Reflex

10 0=0 | 0=1

Arb Or, 9

11 0 e x

Detach, 8, 10

12 1 e x <=> 1=0 | 1=1

U Spec, 3

13 [1 e x => 1=0 | 1=1] & [1=0 | 1=1 => 1 e x]

Iff-And, 12

14 1=0 | 1=1 => 1 e x

Split, 13

15 1=1

Reflex

16 1=0 | 1=1

Arb Or, 15

17 1 e x

Detach, 14, 16

18 EXIST(c):c e x

E Gen, 11

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

Join, 2, 18

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

Join, 19, 2

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

Detach, 5, 20

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

E Spec, 21

Define: fs (Function space on x)

23 Set(fs)

Split, 22

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

Split, 22

Prove: ALL(f):[f(0)=1 & f(1)=0 => f e fs]

Suppose...

25 f(0)=1 & f(1)=0

Premise

26 f(0)=1

Split, 25

27 f(1)=0

Split, 25

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

U Spec, 24

29 [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, 28

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

Split, 29

Sufficient: For f e fs

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

Split, 29

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

Suppose...

32 t e x

Premise

33 t e x <=> t=0 | t=1

U Spec, 3

34 [t e x => t=0 | t=1] & [t=0 | t=1 => t e x]

Iff-And, 33

35 t e x => t=0 | t=1

Split, 34

Two cases to consider:

36 t=0 | t=1

Detach, 35, 32

Case 1

Prove: t=0 => f(t) e x

Suppose...

37 t=0

Premise

38 f(0) e x

Substitute, 26, 17

39 f(t) e x

Substitute, 37, 38

As Required:

40 t=0 => f(t) e x

4 Conclusion, 37

Case 2

Prove: t=1 => f(t) e x

Suppose...

41 t=1

Premise

42 f(1) e x

Substitute, 27, 11

43 f(t) e x

Substitute, 41, 42

As Required:

44 t=1 => f(t) e x

4 Conclusion, 41

45 [t=0 => f(t) e x] & [t=1 => f(t) e x]

Join, 40, 44

46 f(t) e x

Cases, 36, 45

As Required:

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

4 Conclusion, 32

48 f e fs

Detach, 31, 47

As Required:

49 ALL(f):[f(0)=1 & f(1)=0 => f e fs]

4 Conclusion, 25