Metamath Proof Explorer

Theorem iscyg3

Description: Definition of a cyclic group. (Contributed by Mario Carneiro, 21-Apr-2016)

Ref Expression
Hypotheses iscyg.1 ⊢ B = Base G
iscyg.2 ⊢ · ˙ = ⋅ G
Assertion iscyg3 ⊢ G ∈ CycGrp ↔ G ∈ Grp ∧ ∃ x ∈ B ∀ y ∈ B ∃ n ∈ ℤ y = n · ˙ x

Proof

Step Hyp Ref Expression
1 iscyg.1 ⊢ B = Base G
2 iscyg.2 ⊢ · ˙ = ⋅ G
3 1 2 iscyg ⊢ G ∈ CycGrp ↔ G ∈ Grp ∧ ∃ x ∈ B ran ⁡ n ∈ ℤ ⟼ n · ˙ x = B
4 1 2 mulgcl ⊢ G ∈ Grp ∧ n ∈ ℤ ∧ x ∈ B → n · ˙ x ∈ B
5 4 3expa ⊢ G ∈ Grp ∧ n ∈ ℤ ∧ x ∈ B → n · ˙ x ∈ B
6 5 an32s ⊢ G ∈ Grp ∧ x ∈ B ∧ n ∈ ℤ → n · ˙ x ∈ B
7 6 fmpttd ⊢ G ∈ Grp ∧ x ∈ B → n ∈ ℤ ⟼ n · ˙ x : ℤ ⟶ B
8 frn ⊢ n ∈ ℤ ⟼ n · ˙ x : ℤ ⟶ B → ran ⁡ n ∈ ℤ ⟼ n · ˙ x ⊆ B
9 eqss ⊢ ran ⁡ n ∈ ℤ ⟼ n · ˙ x = B ↔ ran ⁡ n ∈ ℤ ⟼ n · ˙ x ⊆ B ∧ B ⊆ ran ⁡ n ∈ ℤ ⟼ n · ˙ x
10 9 baib ⊢ ran ⁡ n ∈ ℤ ⟼ n · ˙ x ⊆ B → ran ⁡ n ∈ ℤ ⟼ n · ˙ x = B ↔ B ⊆ ran ⁡ n ∈ ℤ ⟼ n · ˙ x
11 7 8 10 3syl ⊢ G ∈ Grp ∧ x ∈ B → ran ⁡ n ∈ ℤ ⟼ n · ˙ x = B ↔ B ⊆ ran ⁡ n ∈ ℤ ⟼ n · ˙ x
12 dfss3 ⊢ B ⊆ ran ⁡ n ∈ ℤ ⟼ n · ˙ x ↔ ∀ y ∈ B y ∈ ran ⁡ n ∈ ℤ ⟼ n · ˙ x
13 eqid ⊢ n ∈ ℤ ⟼ n · ˙ x = n ∈ ℤ ⟼ n · ˙ x
14 ovex ⊢ n · ˙ x ∈ V
15 13 14 elrnmpti ⊢ y ∈ ran ⁡ n ∈ ℤ ⟼ n · ˙ x ↔ ∃ n ∈ ℤ y = n · ˙ x
16 15 ralbii ⊢ ∀ y ∈ B y ∈ ran ⁡ n ∈ ℤ ⟼ n · ˙ x ↔ ∀ y ∈ B ∃ n ∈ ℤ y = n · ˙ x
17 12 16 bitri ⊢ B ⊆ ran ⁡ n ∈ ℤ ⟼ n · ˙ x ↔ ∀ y ∈ B ∃ n ∈ ℤ y = n · ˙ x
18 11 17 bitrdi ⊢ G ∈ Grp ∧ x ∈ B → ran ⁡ n ∈ ℤ ⟼ n · ˙ x = B ↔ ∀ y ∈ B ∃ n ∈ ℤ y = n · ˙ x
19 18 rexbidva ⊢ G ∈ Grp → ∃ x ∈ B ran ⁡ n ∈ ℤ ⟼ n · ˙ x = B ↔ ∃ x ∈ B ∀ y ∈ B ∃ n ∈ ℤ y = n · ˙ x
20 19 pm5.32i ⊢ G ∈ Grp ∧ ∃ x ∈ B ran ⁡ n ∈ ℤ ⟼ n · ˙ x = B ↔ G ∈ Grp ∧ ∃ x ∈ B ∀ y ∈ B ∃ n ∈ ℤ y = n · ˙ x
21 3 20 bitri ⊢ G ∈ CycGrp ↔ G ∈ Grp ∧ ∃ x ∈ B ∀ y ∈ B ∃ n ∈ ℤ y = n · ˙ x