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 No typesetting found for |- ( ph -> C e. TermCat ) with typecode |-
termcbas.b ⊢ B = Base C
termcbasmo.x ⊢ φ → X ∈ B
termcbasmo.y ⊢ φ → Y ∈ B
Assertion termcbasmo ⊢ φ → X = Y

Proof

Step Hyp Ref Expression
1 termcbas.c Could not format ( ph -> C e. TermCat ) : No typesetting found for |- ( ph -> C e. TermCat ) with typecode |-
2 termcbas.b ⊢ B = Base C
3 termcbasmo.x ⊢ φ → X ∈ B
4 termcbasmo.y ⊢ φ → Y ∈ B
5 eqeq1 ⊢ x = X → x = y ↔ X = y
6 eqeq2 ⊢ y = Y → X = y ↔ X = Y
7 1 2 termcbas ⊢ φ → ∃ z B = z
8 mosn ⊢ B = z → ∃* x x ∈ B
9 8 exlimiv ⊢ ∃ z B = z → ∃* x x ∈ B
10 7 9 syl ⊢ φ → ∃* x x ∈ B
11 moel ⊢ ∃* x x ∈ B ↔ ∀ x ∈ B ∀ y ∈ B x = y
12 10 11 sylib ⊢ φ → ∀ x ∈ B ∀ y ∈ B x = y
13 5 6 12 3 4 rspc2dv ⊢ φ → X = Y