Theorem prsnex

Description: The class of preordered sets is a proper class. (Contributed by Zhi Wang, 20-Oct-2025)

	Ref	Expression
Assertion	prsnex	⊢ Proset ∉ V

Proof

Step	Hyp	Ref	Expression
1		vprc	⊢ ¬ V ∈ V
2	1	nelir	⊢ V ∉ V
3		basresprsfo	⊢ ( Base ↾ Proset ) : Proset –onto→ V
4	2 3	fonex	⊢ Proset ∉ V