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 \neq V$

Proof

Step	Hyp	Ref	Expression
1		snsn0non	$⊢ \neg \{\{\emptyset\}\} \in On$
2		snex	$⊢ \{\{\emptyset\}\} \in V$
3		id	$⊢ On = V \to On = V$
4	2 3	eleqtrrid	$⊢ On = V \to \{\{\emptyset\}\} \in On$
5	1 4	mto	$⊢ \neg On = V$
6	5	neir	$⊢ On \neq V$