Description: (/) is not a surreal sign. (Contributed by Scott Fenton, 16-Jun-2011)
Ref | Expression | ||
---|---|---|---|
Assertion | nosgnn0 | ⊢ ¬ ∅ ∈ { 1o , 2o } |
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 } |