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