This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

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