This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

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 ⊢ ( 𝜑 → 𝑋 = 𝑌 )