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 
|- -. { { (/) } } e. On

Proof

Step Hyp Ref Expression
1 snex 
 |-  { (/) } e. _V
2 1 snid 
 |-  { (/) } e. { { (/) } }
3 2 n0ii 
 |-  -. { { (/) } } = (/)
4 0ex 
 |-  (/) e. _V
5 4 snid 
 |-  (/) e. { (/) }
6 5 n0ii 
 |-  -. { (/) } = (/)
7 eqcom 
 |-  ( (/) = { (/) } <-> { (/) } = (/) )
8 6 7 mtbir 
 |-  -. (/) = { (/) }
9 4 elsn 
 |-  ( (/) e. { { (/) } } <-> (/) = { (/) } )
10 8 9 mtbir 
 |-  -. (/) e. { { (/) } }
11 3 10 pm3.2ni 
 |-  -. ( { { (/) } } = (/) \/ (/) e. { { (/) } } )
12 on0eqel 
 |-  ( { { (/) } } e. On -> ( { { (/) } } = (/) \/ (/) e. { { (/) } } ) )
13 11 12 mto 
 |-  -. { { (/) } } e. On