Theorem termcbasmo

Description: Two objects in a terminal category are identical. (Contributed by Zhi Wang, 16-Oct-2025)

	Ref	Expression
Hypotheses	termcbas.c	⊢ ( 𝜑 → 𝐶 ∈ TermCat )
	termcbas.b	⊢ 𝐵 = ( Base ‘ 𝐶 )
	termcbasmo.x	⊢ ( 𝜑 → 𝑋 ∈ 𝐵 )
	termcbasmo.y	⊢ ( 𝜑 → 𝑌 ∈ 𝐵 )
Assertion	termcbasmo	⊢ ( 𝜑 → 𝑋 = 𝑌 )

Proof

Step	Hyp	Ref	Expression
1		termcbas.c	⊢ ( 𝜑 → 𝐶 ∈ TermCat )
2		termcbas.b	⊢ 𝐵 = ( Base ‘ 𝐶 )
3		termcbasmo.x	⊢ ( 𝜑 → 𝑋 ∈ 𝐵 )
4		termcbasmo.y	⊢ ( 𝜑 → 𝑌 ∈ 𝐵 )
5		eqeq1	⊢ ( 𝑥 = 𝑋 → ( 𝑥 = 𝑦 ↔ 𝑋 = 𝑦 ) )
6		eqeq2	⊢ ( 𝑦 = 𝑌 → ( 𝑋 = 𝑦 ↔ 𝑋 = 𝑌 ) )
7	1 2	termcbas	⊢ ( 𝜑 → ∃ 𝑧 𝐵 = { 𝑧 } )
8		mosn	⊢ ( 𝐵 = { 𝑧 } → ∃* 𝑥 𝑥 ∈ 𝐵 )
9	8	exlimiv	⊢ ( ∃ 𝑧 𝐵 = { 𝑧 } → ∃* 𝑥 𝑥 ∈ 𝐵 )
10	7 9	syl	⊢ ( 𝜑 → ∃* 𝑥 𝑥 ∈ 𝐵 )
11		moel	⊢ ( ∃* 𝑥 𝑥 ∈ 𝐵 ↔ ∀ 𝑥 ∈ 𝐵 ∀ 𝑦 ∈ 𝐵 𝑥 = 𝑦 )
12	10 11	sylib	⊢ ( 𝜑 → ∀ 𝑥 ∈ 𝐵 ∀ 𝑦 ∈ 𝐵 𝑥 = 𝑦 )
13	5 6 12 3 4	rspc2dv	⊢ ( 𝜑 → 𝑋 = 𝑌 )