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	Could not format assertion : No typesetting found for |- ( Base |` TermCat ) : TermCat -onto-> { b | E. x b = { x } } with typecode |-

Proof

Step	Hyp	Ref	Expression
1		basfn	$$⊢\mathrm{Base}Fn\mathrm{V}$$
2		id	Could not format ( c e. TermCat -> c e. TermCat ) : No typesetting found for |- ( c e. TermCat -> c e. TermCat ) with typecode |-
3		eqid	$$⊢{\mathrm{Base}}_c={\mathrm{Base}}_c$$
4	2 3	termcbas	Could not format ( c e. TermCat -> E. x ( Base ` c ) = { x } ) : No typesetting found for |- ( c e. TermCat -> E. x ( Base ` c ) = { x } ) with typecode |-
5		discsntermlem	$$⊢\exists x{\mathrm{Base}}_c=\left\{x\right\}\to {\mathrm{Base}}_c\in \left\{b|\exists xb=\left\{x\right\}\right\}$$
6	4 5	syl	Could not format ( c e. TermCat -> ( Base ` c ) e. { b | E. x b = { x } } ) : No typesetting found for |- ( c e. TermCat -> ( Base ` c ) e. { b | E. x b = { x } } ) with typecode |-
7		basrestermcfolem	$$⊢a\in \left\{b|\exists xb=\left\{x\right\}\right\}\to \exists xa=\left\{x\right\}$$
8		eqid	$$⊢\left\{⟨{\mathrm{Base}}_{\mathrm{ndx}},a⟩,⟨{\le }_{\mathrm{ndx}},{\mathrm{I}\upharpoonright }_a⟩\right\}=\left\{⟨{\mathrm{Base}}_{\mathrm{ndx}},a⟩,⟨{\le }_{\mathrm{ndx}},{\mathrm{I}\upharpoonright }_a⟩\right\}$$
9		eqid	$$⊢\mathrm{ProsetToCat}\left(\left\{⟨{\mathrm{Base}}_{\mathrm{ndx}},a⟩,⟨{\le }_{\mathrm{ndx}},{\mathrm{I}\upharpoonright }_a⟩\right\}\right)=\mathrm{ProsetToCat}\left(\left\{⟨{\mathrm{Base}}_{\mathrm{ndx}},a⟩,⟨{\le }_{\mathrm{ndx}},{\mathrm{I}\upharpoonright }_a⟩\right\}\right)$$
10	8 9	discsnterm	Could not format ( E. x a = { x } -> ( ProsetToCat ` { <. ( Base ` ndx ) , a >. , <. ( le ` ndx ) , ( _I |` a ) >. } ) e. TermCat ) : No typesetting found for |- ( E. x a = { x } -> ( ProsetToCat ` { <. ( Base ` ndx ) , a >. , <. ( le ` ndx ) , ( _I |` a ) >. } ) e. TermCat ) with typecode |-
11	7 10	syl	Could not format ( a e. { b | E. x b = { x } } -> ( ProsetToCat ` { <. ( Base ` ndx ) , a >. , <. ( le ` ndx ) , ( _I |` a ) >. } ) e. TermCat ) : No typesetting found for |- ( a e. { b | E. x b = { x } } -> ( ProsetToCat ` { <. ( Base ` ndx ) , a >. , <. ( le ` ndx ) , ( _I |` a ) >. } ) e. TermCat ) with typecode |-
12	8 9	discbas	$$⊢a\in \left\{b|\exists xb=\left\{x\right\}\right\}\to a={\mathrm{Base}}_{\mathrm{ProsetToCat}\left(\left\{⟨{\mathrm{Base}}_{\mathrm{ndx}},a⟩,⟨{\le }_{\mathrm{ndx}},{\mathrm{I}\upharpoonright }_a⟩\right\}\right)}$$
13	1 6 11 12	slotresfo	Could not format ( Base |` TermCat ) : TermCat -onto-> { b | E. x b = { x } } : No typesetting found for |- ( Base |` TermCat ) : TermCat -onto-> { b | E. x b = { x } } with typecode |-