Theorem cntzcmnf

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

	Ref	Expression
Hypotheses	cntzcmnf.b	|- B = ( Base ` G )
	cntzcmnf.z	|- Z = ( Cntz ` G )
	cntzcmnf.g	|- ( ph -> G e. CMnd )
	cntzcmnf.f	|- ( ph -> F : A --> B )
Assertion	cntzcmnf	|- ( ph -> ran F C_ ( Z ` ran F ) )

Proof

Step	Hyp	Ref	Expression
1		cntzcmnf.b	|- B = ( Base ` G )
2		cntzcmnf.z	|- Z = ( Cntz ` G )
3		cntzcmnf.g	|- ( ph -> G e. CMnd )
4		cntzcmnf.f	|- ( ph -> F : A --> B )
5	4	frnd	|- ( ph -> ran F C_ B )
6	1 2	cntzcmn	|- ( ( G e. CMnd /\ ran F C_ B ) -> ( Z ` ran F ) = B )
7	3 5 6	syl2anc	|- ( ph -> ( Z ` ran F ) = B )
8	5 7	sseqtrrd	|- ( ph -> ran F C_ ( Z ` ran F ) )