Metamath Proof Explorer


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 }