This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

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 )