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

Metamath Proof Explorer

Theorem mgmhmf

Description: A magma homomorphism is a function. (Contributed by AV, 25-Feb-2020)

Ref Expression
Hypotheses mgmhmf.b 
|- B = ( Base ` S )
mgmhmf.c 
|- C = ( Base ` T )
Assertion mgmhmf 
|- ( F e. ( S MgmHom T ) -> F : B --> C )

Proof

Step Hyp Ref Expression
1 mgmhmf.b 
 |-  B = ( Base ` S )
2 mgmhmf.c 
 |-  C = ( Base ` T )
3 eqid 
 |-  ( +g ` S ) = ( +g ` S )
4 eqid 
 |-  ( +g ` T ) = ( +g ` T )
5 1 2 3 4 ismgmhm 
 |-  ( F e. ( S MgmHom T ) <-> ( ( S e. Mgm /\ T e. Mgm ) /\ ( F : B --> C /\ A. x e. B A. y e. B ( F ` ( x ( +g ` S ) y ) ) = ( ( F ` x ) ( +g ` T ) ( F ` y ) ) ) ) )
6 simprl 
 |-  ( ( ( S e. Mgm /\ T e. Mgm ) /\ ( F : B --> C /\ A. x e. B A. y e. B ( F ` ( x ( +g ` S ) y ) ) = ( ( F ` x ) ( +g ` T ) ( F ` y ) ) ) ) -> F : B --> C )
7 5 6 sylbi 
 |-  ( F e. ( S MgmHom T ) -> F : B --> C )