This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

Theorem snsn0non

Description: The singleton of the singleton of the empty set is not an ordinal (nor a natural number by omsson ). It can be used to represent an "undefined" value for a partial operation on natural or ordinal numbers. See also onxpdisj . (Contributed by NM, 21-May-2004) (Proof shortened by Andrew Salmon, 12-Aug-2011)

Ref Expression
Assertion snsn0non ⊢ ¬ ∅ ∈ On

Proof

Step Hyp Ref Expression
1 snex ⊢ ∅ ∈ V
2 1 snid ⊢ ∅ ∈ ∅
3 2 n0ii ⊢ ¬ ∅ = ∅
4 0ex ⊢ ∅ ∈ V
5 4 snid ⊢ ∅ ∈ ∅
6 5 n0ii ⊢ ¬ ∅ = ∅
7 eqcom ⊢ ∅ = ∅ ↔ ∅ = ∅
8 6 7 mtbir ⊢ ¬ ∅ = ∅
9 4 elsn ⊢ ∅ ∈ ∅ ↔ ∅ = ∅
10 8 9 mtbir ⊢ ¬ ∅ ∈ ∅
11 3 10 pm3.2ni ⊢ ¬ ∅ = ∅ ∨ ∅ ∈ ∅
12 on0eqel ⊢ ∅ ∈ On → ∅ = ∅ ∨ ∅ ∈ ∅
13 11 12 mto ⊢ ¬ ∅ ∈ On