Metamath Proof Explorer

Theorem ordprcon

Description: If an ordinal class is not a set, then it must be the proper class of all ordinals. (Contributed by BTernaryTau, 9-Jun-2026)

		Ref	Expression
	Assertion	ordprcon	$⊢ (Ord A \land \neg A \in V) \to A = On$

Step	Hyp	Ref	Expression
1		ordeleqon	$⊢ Ord A \leftrightarrow (A \in On \lor A = On)$
2	1	birani	$⊢ (Ord A \land \neg A \in V) \to (A \in On \lor A = On)$
3		prcnel	$⊢ \neg A \in V \to \neg A \in On$
4	3	adantl	$⊢ (Ord A \land \neg A \in V) \to \neg A \in On$
5	2 4	orcnd	$⊢ (Ord A \land \neg A \in V) \to A = On$