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

Metamath Proof Explorer

Theorem basrestermcfo

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

Ref Expression
Assertion basrestermcfo 
|- ( Base |` TermCat ) : TermCat -onto-> { b | E. x b = { x } }

Proof

Step Hyp Ref Expression
1 basfn 
 |-  Base Fn _V
2 id 
 |-  ( c e. TermCat -> c e. TermCat )
3 eqid 
 |-  ( Base ` c ) = ( Base ` c )
4 2 3 termcbas 
 |-  ( c e. TermCat -> E. x ( Base ` c ) = { x } )
5 discsntermlem 
 |-  ( E. x ( Base ` c ) = { x } -> ( Base ` c ) e. { b | E. x b = { x } } )
6 4 5 syl 
 |-  ( c e. TermCat -> ( Base ` c ) e. { b | E. x b = { x } } )
7 basrestermcfolem 
 |-  ( a e. { b | E. x b = { x } } -> E. x a = { x } )
8 eqid 
 |-  { <. ( Base ` ndx ) , a >. , <. ( le ` ndx ) , ( _I |` a ) >. } = { <. ( Base ` ndx ) , a >. , <. ( le ` ndx ) , ( _I |` a ) >. }
9 eqid 
 |-  ( ProsetToCat ` { <. ( Base ` ndx ) , a >. , <. ( le ` ndx ) , ( _I |` a ) >. } ) = ( ProsetToCat ` { <. ( Base ` ndx ) , a >. , <. ( le ` ndx ) , ( _I |` a ) >. } )
10 8 9 discsnterm 
 |-  ( E. x a = { x } -> ( ProsetToCat ` { <. ( Base ` ndx ) , a >. , <. ( le ` ndx ) , ( _I |` a ) >. } ) e. TermCat )
11 7 10 syl 
 |-  ( a e. { b | E. x b = { x } } -> ( ProsetToCat ` { <. ( Base ` ndx ) , a >. , <. ( le ` ndx ) , ( _I |` a ) >. } ) e. TermCat )
12 8 9 discbas 
 |-  ( a e. { b | E. x b = { x } } -> a = ( Base ` ( ProsetToCat ` { <. ( Base ` ndx ) , a >. , <. ( le ` ndx ) , ( _I |` a ) >. } ) ) )
13 1 6 11 12 slotresfo 
 |-  ( Base |` TermCat ) : TermCat -onto-> { b | E. x b = { x } }