Theorem termco

Description: The object of a terminal category. (Contributed by Zhi Wang, 17-Nov-2025)

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

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	1 2	termcbas	$$⊢\phi \to \exists xB=\left\{x\right\}$$
4		unieq	$$⊢B=\left\{x\right\}\to \bigcup B=\bigcup \left\{x\right\}$$
5		unisnv	$$⊢\bigcup \left\{x\right\}=x$$
6	4 5	eqtrdi	$$⊢B=\left\{x\right\}\to \bigcup B=x$$
7		vsnid	$$⊢x\in \left\{x\right\}$$
8	6 7	eqeltrdi	$$⊢B=\left\{x\right\}\to \bigcup B\in \left\{x\right\}$$
9		id	$$⊢B=\left\{x\right\}\to B=\left\{x\right\}$$
10	8 9	eleqtrrd	$$⊢B=\left\{x\right\}\to \bigcup B\in B$$
11	10	exlimiv	$$⊢\exists xB=\left\{x\right\}\to \bigcup B\in B$$
12	3 11	syl	$$⊢\phi \to \bigcup B\in B$$