Metamath Proof Explorer

Theorem mhmrcl1

Description: Reverse closure of a monoid homomorphism. (Contributed by Mario Carneiro, 7-Mar-2015)

		Ref	Expression
	Assertion	mhmrcl1	\|- ( F e. ( S MndHom T ) -> S e. Mnd )

Proof

Step	Hyp	Ref	Expression
1		df-mhm	\|- MndHom = ( s e. Mnd , t e. Mnd \|-> { f e. ( ( Base ` t ) ^m ( Base ` s ) ) \| ( A. x e. ( Base ` s ) A. y e. ( Base ` s ) ( f ` ( x ( +g ` s ) y ) ) = ( ( f ` x ) ( +g ` t ) ( f ` y ) ) /\ ( f ` ( 0g ` s ) ) = ( 0g ` t ) ) } )
2	1	elmpocl1	\|- ( F e. ( S MndHom T ) -> S e. Mnd )

Step

Hyp

Ref

Expression

df-mhm

 |-  MndHom = ( s e. Mnd , t e. Mnd |-> { f e. ( ( Base ` t ) ^m ( Base ` s ) ) | ( A. x e. ( Base ` s ) A. y e. ( Base ` s ) ( f ` ( x ( +g ` s ) y ) ) = ( ( f ` x ) ( +g ` t ) ( f ` y ) ) /\ ( f ` ( 0g ` s ) ) = ( 0g ` t ) ) } )

elmpocl1

 |-  ( F e. ( S MndHom T ) -> S e. Mnd )