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 ⊢ ( 𝜑 → 𝐶 = ( MndToCat ‘ 𝑀 ) )
mndtcbas.m ⊢ ( 𝜑 → 𝑀 ∈ Mnd )
mndtcbas.b ⊢ ( 𝜑 → 𝐵 = ( Base ‘ 𝐶 ) )
mndtchom.x ⊢ ( 𝜑 → 𝑋 ∈ 𝐵 )
mndtchom.y ⊢ ( 𝜑 → 𝑌 ∈ 𝐵 )
Assertion mndtcbas2 ( 𝜑 → 𝑋 = 𝑌 )

Proof

Step Hyp Ref Expression
1 mndtcbas.c ⊢ ( 𝜑 → 𝐶 = ( MndToCat ‘ 𝑀 ) )
2 mndtcbas.m ⊢ ( 𝜑 → 𝑀 ∈ Mnd )
3 mndtcbas.b ⊢ ( 𝜑 → 𝐵 = ( Base ‘ 𝐶 ) )
4 mndtchom.x ⊢ ( 𝜑 → 𝑋 ∈ 𝐵 )
5 mndtchom.y ⊢ ( 𝜑 → 𝑌 ∈ 𝐵 )
6 1 2 3 mndtcbas ⊢ ( 𝜑 → ∃! 𝑥 𝑥 ∈ 𝐵 )
7 eumo ⊢ ( ∃! 𝑥 𝑥 ∈ 𝐵 → ∃* 𝑥 𝑥 ∈ 𝐵 )
8 moel ⊢ ( ∃* 𝑥 𝑥 ∈ 𝐵 ↔ ∀ 𝑥 ∈ 𝐵 ∀ 𝑦 ∈ 𝐵 𝑥 = 𝑦 )
9 8 biimpi ⊢ ( ∃* 𝑥 𝑥 ∈ 𝐵 → ∀ 𝑥 ∈ 𝐵 ∀ 𝑦 ∈ 𝐵 𝑥 = 𝑦 )
10 6 7 9 3syl ⊢ ( 𝜑 → ∀ 𝑥 ∈ 𝐵 ∀ 𝑦 ∈ 𝐵 𝑥 = 𝑦 )
11 eqeq12 ⊢ ( ( 𝑥 = 𝑋 ∧ 𝑦 = 𝑌 ) → ( 𝑥 = 𝑦 ↔ 𝑋 = 𝑌 ) )
12 11 rspc2gv ⊢ ( ( 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵 ) → ( ∀ 𝑥 ∈ 𝐵 ∀ 𝑦 ∈ 𝐵 𝑥 = 𝑦 → 𝑋 = 𝑌 ) )
13 4 5 12 syl2anc ⊢ ( 𝜑 → ( ∀ 𝑥 ∈ 𝐵 ∀ 𝑦 ∈ 𝐵 𝑥 = 𝑦 → 𝑋 = 𝑌 ) )
14 10 13 mpd ⊢ ( 𝜑 → 𝑋 = 𝑌 )