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

Metamath Proof Explorer

Theorem mndtcbas2

Description: Two objects in a category built from a monoid are identical. (Contributed by Zhi Wang, 24-Sep-2024)

Ref Expression
Hypotheses mndtcbas.c ⊢ φ → C = MndToCat ⁡ M
mndtcbas.m ⊢ φ → M ∈ Mnd
mndtcbas.b ⊢ φ → B = Base C
mndtchom.x ⊢ φ → X ∈ B
mndtchom.y ⊢ φ → Y ∈ B
Assertion mndtcbas2 ⊢ φ → X = Y

Proof

Step Hyp Ref Expression
1 mndtcbas.c ⊢ φ → C = MndToCat ⁡ M
2 mndtcbas.m ⊢ φ → M ∈ Mnd
3 mndtcbas.b ⊢ φ → B = Base C
4 mndtchom.x ⊢ φ → X ∈ B
5 mndtchom.y ⊢ φ → Y ∈ B
6 1 2 3 mndtcbas ⊢ φ → ∃! x x ∈ B
7 eumo ⊢ ∃! x x ∈ B → ∃* x x ∈ B
8 moel ⊢ ∃* x x ∈ B ↔ ∀ x ∈ B ∀ y ∈ B x = y
9 8 biimpi ⊢ ∃* x x ∈ B → ∀ x ∈ B ∀ y ∈ B x = y
10 6 7 9 3syl ⊢ φ → ∀ x ∈ B ∀ y ∈ B x = y
11 eqeq12 ⊢ x = X ∧ y = Y → x = y ↔ X = Y
12 11 rspc2gv ⊢ X ∈ B ∧ Y ∈ B → ∀ x ∈ B ∀ y ∈ B x = y → X = Y
13 4 5 12 syl2anc ⊢ φ → ∀ x ∈ B ∀ y ∈ B x = y → X = Y
14 10 13 mpd ⊢ φ → X = Y