Theorem termcbas2

Description: The base of a terminal category is given by its object. (Contributed by Zhi Wang, 20-Oct-2025)

	Ref	Expression
Hypotheses	termcbas.c	No typesetting found for |- ( ph -> C e. TermCat ) with typecode |-
	termcbas.b	$$⊢B={\mathrm{Base}}_C$$
	termcbasmo.x	$$⊢\phi \to X\in B$$
Assertion	termcbas2	$$⊢\phi \to B=\left\{X\right\}$$

Proof

Step	Hyp	Ref	Expression
1		termcbas.c	Could not format ( ph -> C e. TermCat ) : No typesetting found for |- ( ph -> C e. TermCat ) with typecode |-
2		termcbas.b	$$⊢B={\mathrm{Base}}_C$$
3		termcbasmo.x	$$⊢\phi \to X\in B$$
4	1 2	termcbas	$$⊢\phi \to \exists xB=\left\{x\right\}$$
5		simpr	$$⊢\left(\phi \wedge B=\left\{x\right\}\right)\to B=\left\{x\right\}$$
6	3	adantr	$$⊢\left(\phi \wedge B=\left\{x\right\}\right)\to X\in B$$
7	6 5	eleqtrd	$$⊢\left(\phi \wedge B=\left\{x\right\}\right)\to X\in \left\{x\right\}$$
8		elsni	$$⊢X\in \left\{x\right\}\to X=x$$
9	8	sneqd	$$⊢X\in \left\{x\right\}\to \left\{X\right\}=\left\{x\right\}$$
10	7 9	syl	$$⊢\left(\phi \wedge B=\left\{x\right\}\right)\to \left\{X\right\}=\left\{x\right\}$$
11	5 10	eqtr4d	$$⊢\left(\phi \wedge B=\left\{x\right\}\right)\to B=\left\{X\right\}$$
12	4 11	exlimddv	$$⊢\phi \to B=\left\{X\right\}$$