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	⊢ ( 𝜑 → 𝐶 ∈ TermCat )
	termcbas.b	⊢ 𝐵 = ( Base ‘ 𝐶 )
	termcbasmo.x	⊢ ( 𝜑 → 𝑋 ∈ 𝐵 )
Assertion	termcbas2	⊢ ( 𝜑 → 𝐵 = { 𝑋 } )

Proof

Step	Hyp	Ref	Expression
1		termcbas.c	⊢ ( 𝜑 → 𝐶 ∈ TermCat )
2		termcbas.b	⊢ 𝐵 = ( Base ‘ 𝐶 )
3		termcbasmo.x	⊢ ( 𝜑 → 𝑋 ∈ 𝐵 )
4	1 2	termcbas	⊢ ( 𝜑 → ∃ 𝑥 𝐵 = { 𝑥 } )
5		simpr	⊢ ( ( 𝜑 ∧ 𝐵 = { 𝑥 } ) → 𝐵 = { 𝑥 } )
6	3	adantr	⊢ ( ( 𝜑 ∧ 𝐵 = { 𝑥 } ) → 𝑋 ∈ 𝐵 )
7	6 5	eleqtrd	⊢ ( ( 𝜑 ∧ 𝐵 = { 𝑥 } ) → 𝑋 ∈ { 𝑥 } )
8		elsni	⊢ ( 𝑋 ∈ { 𝑥 } → 𝑋 = 𝑥 )
9	8	sneqd	⊢ ( 𝑋 ∈ { 𝑥 } → { 𝑋 } = { 𝑥 } )
10	7 9	syl	⊢ ( ( 𝜑 ∧ 𝐵 = { 𝑥 } ) → { 𝑋 } = { 𝑥 } )
11	5 10	eqtr4d	⊢ ( ( 𝜑 ∧ 𝐵 = { 𝑥 } ) → 𝐵 = { 𝑋 } )
12	4 11	exlimddv	⊢ ( 𝜑 → 𝐵 = { 𝑋 } )