Theorem onprcALT

Description: Alternate proof of onprc from onprcr . (Contributed by Adrian Ducourtial, 15-Oct-2026) (Proof modification is discouraged.) (New usage is discouraged.)

	Ref	Expression
Assertion	onprcALT	$$⊢\neg \mathrm{On}\in \mathrm{V}$$

Proof

Step	Hyp	Ref	Expression
1		df-on	$$⊢\mathrm{On}=\left\{x|\mathrm{Ord}x\right\}$$
2		rabab	$$⊢\left\{x\in \mathrm{V}|\mathrm{Ord}x\right\}=\left\{x|\mathrm{Ord}x\right\}$$
3	1 2	eqtr4i	$$⊢\mathrm{On}=\left\{x\in \mathrm{V}|\mathrm{Ord}x\right\}$$
4		tron	$$⊢\mathrm{Tr}\mathrm{On}$$
5	3 4	onprcr	$$⊢\neg \mathrm{On}\in \mathrm{V}$$