THEOREM
*******
Given: s0={0}, f:s0-->s0, ~1=0
We have: f(0)=0 and f(1) is indeterminate (undefined)
By Dan Christensen
2021-12-03
PROOF
*****
Assumptions:
1 ALL(a):[a e s0 <=> a=0]
Axiom
2 ALL(a):[a e s0 => f(a) e s0]
Axiom
3 ~1=0
Axiom
Prove: 0 e s0
4 0 e s0 => f(0) e s0
U Spec, 2
5 0 e s0 <=> 0=0
U Spec, 1
6 [0 e s0 => 0=0] & [0=0 => 0 e s0]
Iff-And, 5
7 0=0 => 0 e s0
Split, 6
8 0=0
Reflex
As Required:
9 0 e s0
Detach, 7, 8
Prove: ~1 e s0
10 1 e s0 <=> 1=0
U Spec, 1
11 [1 e s0 => 1=0] & [1=0 => 1 e s0]
Iff-And, 10
12 1 e s0 => 1=0
Split, 11
13 ~1=0 => ~1 e s0
Contra, 12
As Required:
14 ~1 e s0
Detach, 13, 3
Prove: f(0)=0
15 f(0) e s0
Detach, 4, 9
16 f(0) e s0 <=> f(0)=0
U Spec, 1, 15
17 [f(0) e s0 => f(0)=0] & [f(0)=0 => f(0) e s0]
Iff-And, 16
18 f(0) e s0 => f(0)=0
Split, 17
19 f(0)=0 => f(0) e s0
Split, 17
As Required:
20 f(0)=0
Detach, 18, 15
Prove: 1 e s0 => f(1) e s0
21 1 e s0 => f(1) e s0
U Spec, 2
Prove: 1 e s0 => ~f(1) e s0 (vacuously true)
22 ~~1 e s0 => ~f(1) e s0
Arb Cons, 14
As Required:
23 1 e s0 => ~f(1) e s0
Rem DNeg, 22