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

Metamath Proof Explorer

Theorem basresprsfo

Description: The base function restricted to the class of preordered sets maps the class of preordered sets onto the universal class. (Contributed by Zhi Wang, 20-Oct-2025)

Ref Expression
Assertion basresprsfo 
|- ( Base |` Proset ) : Proset -onto-> _V

Proof

Step Hyp Ref Expression
1 basfn 
 |-  Base Fn _V
2 fvexd 
 |-  ( k e. Proset -> ( Base ` k ) e. _V )
3 eqid 
 |-  { <. ( Base ` ndx ) , b >. , <. ( le ` ndx ) , ( _I |` b ) >. } = { <. ( Base ` ndx ) , b >. , <. ( le ` ndx ) , ( _I |` b ) >. }
4 3 resipos 
 |-  ( b e. _V -> { <. ( Base ` ndx ) , b >. , <. ( le ` ndx ) , ( _I |` b ) >. } e. Poset )
5 posprs 
 |-  ( { <. ( Base ` ndx ) , b >. , <. ( le ` ndx ) , ( _I |` b ) >. } e. Poset -> { <. ( Base ` ndx ) , b >. , <. ( le ` ndx ) , ( _I |` b ) >. } e. Proset )
6 4 5 syl 
 |-  ( b e. _V -> { <. ( Base ` ndx ) , b >. , <. ( le ` ndx ) , ( _I |` b ) >. } e. Proset )
7 3 resiposbas 
 |-  ( b e. _V -> b = ( Base ` { <. ( Base ` ndx ) , b >. , <. ( le ` ndx ) , ( _I |` b ) >. } ) )
8 1 2 6 7 slotresfo 
 |-  ( Base |` Proset ) : Proset -onto-> _V