Metamath Proof Explorer


Theorem cycsubg

Description: The cyclic group generated by A is the smallest 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 cycsubg G Grp A X ran F = s SubGrp G | A s

Proof

Step Hyp Ref Expression
1 cycsubg.x X = Base G
2 cycsubg.t · ˙ = G
3 cycsubg.f F = x x · ˙ A
4 ssintab ran F s | s SubGrp G A s s s SubGrp G A s ran F s
5 1 2 3 cycsubgss s SubGrp G A s ran F s
6 4 5 mpgbir ran F s | s SubGrp G A s
7 df-rab s SubGrp G | A s = s | s SubGrp G A s
8 7 inteqi s SubGrp G | A s = s | s SubGrp G A s
9 6 8 sseqtrri ran F s SubGrp G | A s
10 9 a1i G Grp A X ran F s SubGrp G | A s
11 1 2 3 cycsubgcl G Grp A X ran F SubGrp G A ran F
12 eleq2 s = ran F A s A ran F
13 12 elrab ran F s SubGrp G | A s ran F SubGrp G A ran F
14 11 13 sylibr G Grp A X ran F s SubGrp G | A s
15 intss1 ran F s SubGrp G | A s s SubGrp G | A s ran F
16 14 15 syl G Grp A X s SubGrp G | A s ran F
17 10 16 eqssd G Grp A X ran F = s SubGrp G | A s