Theorem cntzcmnf

Description: Discharge the centralizer assumption in a commutative monoid. (Contributed by Mario Carneiro, 24-Apr-2016)

	Ref	Expression
Hypotheses	cntzcmnf.b	⊢ 𝐵 = ( Base ‘ 𝐺 )
	cntzcmnf.z	⊢ 𝑍 = ( Cntz ‘ 𝐺 )
	cntzcmnf.g	⊢ ( 𝜑 → 𝐺 ∈ CMnd )
	cntzcmnf.f	⊢ ( 𝜑 → 𝐹 : 𝐴 ⟶ 𝐵 )
Assertion	cntzcmnf	⊢ ( 𝜑 → ran 𝐹 ⊆ ( 𝑍 ‘ ran 𝐹 ) )

Proof

Step	Hyp	Ref	Expression
1		cntzcmnf.b	⊢ 𝐵 = ( Base ‘ 𝐺 )
2		cntzcmnf.z	⊢ 𝑍 = ( Cntz ‘ 𝐺 )
3		cntzcmnf.g	⊢ ( 𝜑 → 𝐺 ∈ CMnd )
4		cntzcmnf.f	⊢ ( 𝜑 → 𝐹 : 𝐴 ⟶ 𝐵 )
5	4	frnd	⊢ ( 𝜑 → ran 𝐹 ⊆ 𝐵 )
6	1 2	cntzcmn	⊢ ( ( 𝐺 ∈ CMnd ∧ ran 𝐹 ⊆ 𝐵 ) → ( 𝑍 ‘ ran 𝐹 ) = 𝐵 )
7	3 5 6	syl2anc	⊢ ( 𝜑 → ( 𝑍 ‘ ran 𝐹 ) = 𝐵 )
8	5 7	sseqtrrd	⊢ ( 𝜑 → ran 𝐹 ⊆ ( 𝑍 ‘ ran 𝐹 ) )