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 |
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 |