Metamath Proof Explorer


Theorem mhmrcl1

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

Ref Expression
Assertion mhmrcl1 ( 𝐹 ∈ ( 𝑆 MndHom 𝑇 ) → 𝑆 ∈ Mnd )

Proof

Step Hyp Ref Expression
1 df-mhm MndHom = ( 𝑠 ∈ Mnd , 𝑡 ∈ Mnd ↦ { 𝑓 ∈ ( ( Base ‘ 𝑡 ) ↑m ( Base ‘ 𝑠 ) ) ∣ ( ∀ 𝑥 ∈ ( Base ‘ 𝑠 ) ∀ 𝑦 ∈ ( Base ‘ 𝑠 ) ( 𝑓 ‘ ( 𝑥 ( +g𝑠 ) 𝑦 ) ) = ( ( 𝑓𝑥 ) ( +g𝑡 ) ( 𝑓𝑦 ) ) ∧ ( 𝑓 ‘ ( 0g𝑠 ) ) = ( 0g𝑡 ) ) } )
2 1 elmpocl1 ( 𝐹 ∈ ( 𝑆 MndHom 𝑇 ) → 𝑆 ∈ Mnd )