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 · ˙ = G
cycsubg.f F = x x · ˙ A
Assertion cycsubgss S SubGrp G A S ran F S

Proof

Step Hyp Ref Expression
1 cycsubg.x X = Base G
2 cycsubg.t · ˙ = G
3 cycsubg.f F = x x · ˙ A
4 2 subgmulgcl S SubGrp G x A S x · ˙ A S
5 4 3expa S SubGrp G x A S x · ˙ A S
6 5 an32s S SubGrp G A S x x · ˙ A S
7 6 3 fmptd S SubGrp G A S F : S
8 7 frnd S SubGrp G A S ran F S