Theorem nosgnn0

Description: (/) is not a surreal sign. (Contributed by Scott Fenton, 16-Jun-2011)

	Ref	Expression
Assertion	nosgnn0	⊢ ¬ ∅ ∈ { 1o , 2o }

Proof

Step	Hyp	Ref	Expression
1		1n0	⊢ 1o ≠ ∅
2	1	nesymi	⊢ ¬ ∅ = 1o
3		nsuceq0	⊢ suc 1o ≠ ∅
4		necom	⊢ ( suc 1o ≠ ∅ ↔ ∅ ≠ suc 1o )
5		df-2o	⊢ 2o = suc 1o
6	5	neeq2i	⊢ ( ∅ ≠ 2o ↔ ∅ ≠ suc 1o )
7	4 6	bitr4i	⊢ ( suc 1o ≠ ∅ ↔ ∅ ≠ 2o )
8	3 7	mpbi	⊢ ∅ ≠ 2o
9	8	neii	⊢ ¬ ∅ = 2o
10	2 9	pm3.2ni	⊢ ¬ ( ∅ = 1o ∨ ∅ = 2o )
11		0ex	⊢ ∅ ∈ V
12	11	elpr	⊢ ( ∅ ∈ { 1o , 2o } ↔ ( ∅ = 1o ∨ ∅ = 2o ) )
13	10 12	mtbir	⊢ ¬ ∅ ∈ { 1o , 2o }