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 )