Theorem termco

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

	Ref	Expression
Hypotheses	termcbas.c	⊢ ( 𝜑 → 𝐶 ∈ TermCat )
	termcbas.b	⊢ 𝐵 = ( Base ‘ 𝐶 )
Assertion	termco	⊢ ( 𝜑 → ∪ 𝐵 ∈ 𝐵 )

Proof

Step	Hyp	Ref	Expression
1		termcbas.c	⊢ ( 𝜑 → 𝐶 ∈ TermCat )
2		termcbas.b	⊢ 𝐵 = ( Base ‘ 𝐶 )
3	1 2	termcbas	⊢ ( 𝜑 → ∃ 𝑥 𝐵 = { 𝑥 } )
4		unieq	⊢ ( 𝐵 = { 𝑥 } → ∪ 𝐵 = ∪ { 𝑥 } )
5		unisnv	⊢ ∪ { 𝑥 } = 𝑥
6	4 5	eqtrdi	⊢ ( 𝐵 = { 𝑥 } → ∪ 𝐵 = 𝑥 )
7		vsnid	⊢ 𝑥 ∈ { 𝑥 }
8	6 7	eqeltrdi	⊢ ( 𝐵 = { 𝑥 } → ∪ 𝐵 ∈ { 𝑥 } )
9		id	⊢ ( 𝐵 = { 𝑥 } → 𝐵 = { 𝑥 } )
10	8 9	eleqtrrd	⊢ ( 𝐵 = { 𝑥 } → ∪ 𝐵 ∈ 𝐵 )
11	10	exlimiv	⊢ ( ∃ 𝑥 𝐵 = { 𝑥 } → ∪ 𝐵 ∈ 𝐵 )
12	3 11	syl	⊢ ( 𝜑 → ∪ 𝐵 ∈ 𝐵 )