Metamath Proof Explorer


Theorem mhmrcl2

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

Ref Expression
Assertion mhmrcl2
|- ( F e. ( S MndHom T ) -> T 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 elmpocl2
 |-  ( F e. ( S MndHom T ) -> T e. Mnd )