Metamath Proof Explorer

Theorem nosgnn0

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

Ref Expression
Assertion nosgnn0 
|- -. (/) e. { 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 
 |-  (/) e. _V
12 11 elpr 
 |-  ( (/) e. { 1o , 2o } <-> ( (/) = 1o \/ (/) = 2o ) )
13 10 12 mtbir 
 |-  -. (/) e. { 1o , 2o }