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

Metamath Proof Explorer

Theorem onnev

Description: The class of ordinal numbers is not equal to the universe. (Contributed by NM, 16-Jun-2007) (Proof shortened by Mario Carneiro, 10-Jan-2013) (Proof shortened by Wolf Lammen, 27-May-2024)

		Ref	Expression
	Assertion	onnev	⊢ On ≠ V

Proof

Step	Hyp	Ref	Expression
1		snsn0non	⊢ ¬ { { ∅ } } ∈ On
2		snex	⊢ { { ∅ } } ∈ V
3		id	⊢ ( On = V → On = V )
4	2 3	eleqtrrid	⊢ ( On = V → { { ∅ } } ∈ On )
5	1 4	mto	⊢ ¬ On = V
6	5	neir	⊢ On ≠ V