Theorem cycsubgss

Description: The cyclic subgroup generated by an element A is a subset of any subgroup containing A . (Contributed by Mario Carneiro, 13-Jan-2015)

	Ref	Expression
Hypotheses	cycsubg.x	|- X = ( Base ` G )
	cycsubg.t	|- .x. = ( .g ` G )
	cycsubg.f	|- F = ( x e. ZZ |-> ( x .x. A ) )
Assertion	cycsubgss	|- ( ( S e. ( SubGrp ` G ) /\ A e. S ) -> ran F C_ S )

Proof

Step	Hyp	Ref	Expression
1		cycsubg.x	|- X = ( Base ` G )
2		cycsubg.t	|- .x. = ( .g ` G )
3		cycsubg.f	|- F = ( x e. ZZ |-> ( x .x. A ) )
4	2	subgmulgcl	|- ( ( S e. ( SubGrp ` G ) /\ x e. ZZ /\ A e. S ) -> ( x .x. A ) e. S )
5	4	3expa	|- ( ( ( S e. ( SubGrp ` G ) /\ x e. ZZ ) /\ A e. S ) -> ( x .x. A ) e. S )
6	5	an32s	|- ( ( ( S e. ( SubGrp ` G ) /\ A e. S ) /\ x e. ZZ ) -> ( x .x. A ) e. S )
7	6 3	fmptd	|- ( ( S e. ( SubGrp ` G ) /\ A e. S ) -> F : ZZ --> S )
8	7	frnd	|- ( ( S e. ( SubGrp ` G ) /\ A e. S ) -> ran F C_ S )