Theorem iscyg2

Description: A cyclic group is a group which contains a generator. (Contributed by Mario Carneiro, 21-Apr-2016)

	Ref	Expression
Hypotheses	iscyg.1	⊢ 𝐵 = ( Base ‘ 𝐺 )
	iscyg.2	⊢ · = ( .g ‘ 𝐺 )
	iscyg3.e	⊢ 𝐸 = { 𝑥 ∈ 𝐵 ∣ ran ( 𝑛 ∈ ℤ ↦ ( 𝑛 · 𝑥 ) ) = 𝐵 }
Assertion	iscyg2	⊢ ( 𝐺 ∈ CycGrp ↔ ( 𝐺 ∈ Grp ∧ 𝐸 ≠ ∅ ) )

Proof

Step	Hyp	Ref	Expression
1		iscyg.1	⊢ 𝐵 = ( Base ‘ 𝐺 )
2		iscyg.2	⊢ · = ( .g ‘ 𝐺 )
3		iscyg3.e	⊢ 𝐸 = { 𝑥 ∈ 𝐵 ∣ ran ( 𝑛 ∈ ℤ ↦ ( 𝑛 · 𝑥 ) ) = 𝐵 }
4	1 2	iscyg	⊢ ( 𝐺 ∈ CycGrp ↔ ( 𝐺 ∈ Grp ∧ ∃ 𝑥 ∈ 𝐵 ran ( 𝑛 ∈ ℤ ↦ ( 𝑛 · 𝑥 ) ) = 𝐵 ) )
5	3	neeq1i	⊢ ( 𝐸 ≠ ∅ ↔ { 𝑥 ∈ 𝐵 ∣ ran ( 𝑛 ∈ ℤ ↦ ( 𝑛 · 𝑥 ) ) = 𝐵 } ≠ ∅ )
6		rabn0	⊢ ( { 𝑥 ∈ 𝐵 ∣ ran ( 𝑛 ∈ ℤ ↦ ( 𝑛 · 𝑥 ) ) = 𝐵 } ≠ ∅ ↔ ∃ 𝑥 ∈ 𝐵 ran ( 𝑛 ∈ ℤ ↦ ( 𝑛 · 𝑥 ) ) = 𝐵 )
7	5 6	bitri	⊢ ( 𝐸 ≠ ∅ ↔ ∃ 𝑥 ∈ 𝐵 ran ( 𝑛 ∈ ℤ ↦ ( 𝑛 · 𝑥 ) ) = 𝐵 )
8	7	anbi2i	⊢ ( ( 𝐺 ∈ Grp ∧ 𝐸 ≠ ∅ ) ↔ ( 𝐺 ∈ Grp ∧ ∃ 𝑥 ∈ 𝐵 ran ( 𝑛 ∈ ℤ ↦ ( 𝑛 · 𝑥 ) ) = 𝐵 ) )
9	4 8	bitr4i	⊢ ( 𝐺 ∈ CycGrp ↔ ( 𝐺 ∈ Grp ∧ 𝐸 ≠ ∅ ) )