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 𝐴 ∧ ¬ 𝐴 ∈ V ) → 𝐴 = On )

Proof

Step	Hyp	Ref	Expression
1		ordeleqon	⊢ ( Ord 𝐴 ↔ ( 𝐴 ∈ On ∨ 𝐴 = On ) )
2	1	birani	⊢ ( ( Ord 𝐴 ∧ ¬ 𝐴 ∈ V ) → ( 𝐴 ∈ On ∨ 𝐴 = On ) )
3		prcnel	⊢ ( ¬ 𝐴 ∈ V → ¬ 𝐴 ∈ On )
4	3	adantl	⊢ ( ( Ord 𝐴 ∧ ¬ 𝐴 ∈ V ) → ¬ 𝐴 ∈ On )
5	2 4	orcnd	⊢ ( ( Ord 𝐴 ∧ ¬ 𝐴 ∈ V ) → 𝐴 = On )