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 } }