Metamath Proof Explorer

Theorem basresposfo

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

Ref Expression
Assertion basresposfo 
|- ( Base |` Poset ) : Poset -onto-> _V

Proof

Step Hyp Ref Expression
1 basfn 
 |-  Base Fn _V
2 ssv 
 |-  Poset C_ _V
3 fnssres 
 |-  ( ( Base Fn _V /\ Poset C_ _V ) -> ( Base |` Poset ) Fn Poset )
4 1 2 3 mp2an 
 |-  ( Base |` Poset ) Fn Poset
5 dffn2 
 |-  ( ( Base |` Poset ) Fn Poset <-> ( Base |` Poset ) : Poset --> _V )
6 4 5 mpbi 
 |-  ( Base |` Poset ) : Poset --> _V
7 exbaspos 
 |-  ( b e. _V -> E. k e. Poset b = ( Base ` k ) )
8 fvres 
 |-  ( k e. Poset -> ( ( Base |` Poset ) ` k ) = ( Base ` k ) )
9 8 eqeq2d 
 |-  ( k e. Poset -> ( b = ( ( Base |` Poset ) ` k ) <-> b = ( Base ` k ) ) )
10 9 rexbiia 
 |-  ( E. k e. Poset b = ( ( Base |` Poset ) ` k ) <-> E. k e. Poset b = ( Base ` k ) )
11 7 10 sylibr 
 |-  ( b e. _V -> E. k e. Poset b = ( ( Base |` Poset ) ` k ) )
12 11 rgen 
 |-  A. b e. _V E. k e. Poset b = ( ( Base |` Poset ) ` k )
13 dffo3 
 |-  ( ( Base |` Poset ) : Poset -onto-> _V <-> ( ( Base |` Poset ) : Poset --> _V /\ A. b e. _V E. k e. Poset b = ( ( Base |` Poset ) ` k ) ) )
14 6 12 13 mpbir2an 
 |-  ( Base |` Poset ) : Poset -onto-> _V