Metamath Proof Explorer

Theorem posnex

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

Ref Expression
Assertion posnex 
|- Poset e/ _V

Proof

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