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

Metamath Proof Explorer

Theorem snsn0non

Proof