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 
|- ( ph -> C = ( MndToCat ` M ) )
mndtcbas.m 
|- ( ph -> M e. Mnd )
mndtcbas.b 
|- ( ph -> B = ( Base ` C ) )
mndtchom.x 
|- ( ph -> X e. B )
mndtchom.y 
|- ( ph -> Y e. B )
Assertion mndtcbas2 
|- ( ph -> X = Y )

Proof

Step Hyp Ref Expression
1 mndtcbas.c 
 |-  ( ph -> C = ( MndToCat ` M ) )
2 mndtcbas.m 
 |-  ( ph -> M e. Mnd )
3 mndtcbas.b 
 |-  ( ph -> B = ( Base ` C ) )
4 mndtchom.x 
 |-  ( ph -> X e. B )
5 mndtchom.y 
 |-  ( ph -> Y e. B )
6 1 2 3 mndtcbas 
 |-  ( ph -> E! x x e. B )
7 eumo 
 |-  ( E! x x e. B -> E* x x e. B )
8 moel 
 |-  ( E* x x e. B <-> A. x e. B A. y e. B x = y )
9 8 biimpi 
 |-  ( E* x x e. B -> A. x e. B A. y e. B x = y )
10 6 7 9 3syl 
 |-  ( ph -> A. x e. B A. y e. B x = y )
11 eqeq12 
 |-  ( ( x = X /\ y = Y ) -> ( x = y <-> X = Y ) )
12 11 rspc2gv 
 |-  ( ( X e. B /\ Y e. B ) -> ( A. x e. B A. y e. B x = y -> X = Y ) )
13 4 5 12 syl2anc 
 |-  ( ph -> ( A. x e. B A. y e. B x = y -> X = Y ) )
14 10 13 mpd 
 |-  ( ph -> X = Y )