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 )