Theorem termco

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

	Ref	Expression
Hypotheses	termcbas.c	|- ( ph -> C e. TermCat )
	termcbas.b	|- B = ( Base ` C )
Assertion	termco	|- ( ph -> U. B e. B )

Proof

Step	Hyp	Ref	Expression
1		termcbas.c	|- ( ph -> C e. TermCat )
2		termcbas.b	|- B = ( Base ` C )
3	1 2	termcbas	|- ( ph -> E. x B = { x } )
4		unieq	|- ( B = { x } -> U. B = U. { x } )
5		unisnv	|- U. { x } = x
6	4 5	eqtrdi	|- ( B = { x } -> U. B = x )
7		vsnid	|- x e. { x }
8	6 7	eqeltrdi	|- ( B = { x } -> U. B e. { x } )
9		id	|- ( B = { x } -> B = { x } )
10	8 9	eleqtrrd	|- ( B = { x } -> U. B e. B )
11	10	exlimiv	|- ( E. x B = { x } -> U. B e. B )
12	3 11	syl	|- ( ph -> U. B e. B )