Metamath Proof Explorer

Theorem prsnex

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

Ref Expression
Assertion prsnex 
|- Proset e/ _V

Proof

Step Hyp Ref Expression
1 vprc 
 |-  -. _V e. _V
2 1 nelir 
 |-  _V e/ _V
3 basresprsfo 
 |-  ( Base |` Proset ) : Proset -onto-> _V
4 2 3 fonex 
 |-  Proset e/ _V