Theorem posnex

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

	Ref	Expression
Assertion	posnex	⊢ Poset ∉ V

Proof

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