Metamath Proof Explorer

Theorem cygctb

Description: A cyclic group is countable. (Contributed by Mario Carneiro, 21-Apr-2016)

Ref Expression
Hypothesis cygctb.1 ⊢ B = Base G
Assertion cygctb ⊢ G ∈ CycGrp → B ≼ ω

Proof

Step Hyp Ref Expression
1 cygctb.1 ⊢ B = Base G
2 eqid ⊢ ⋅ G = ⋅ G
3 1 2 iscyg ⊢ G ∈ CycGrp ↔ G ∈ Grp ∧ ∃ x ∈ B ran ⁡ n ∈ ℤ ⟼ n ⋅ G x = B
4 3 simprbi ⊢ G ∈ CycGrp → ∃ x ∈ B ran ⁡ n ∈ ℤ ⟼ n ⋅ G x = B
5 ovex ⊢ n ⋅ G x ∈ V
6 eqid ⊢ n ∈ ℤ ⟼ n ⋅ G x = n ∈ ℤ ⟼ n ⋅ G x
7 5 6 fnmpti ⊢ n ∈ ℤ ⟼ n ⋅ G x Fn ℤ
8 df-fo ⊢ n ∈ ℤ ⟼ n ⋅ G x : ℤ ⟶ onto B ↔ n ∈ ℤ ⟼ n ⋅ G x Fn ℤ ∧ ran ⁡ n ∈ ℤ ⟼ n ⋅ G x = B
9 7 8 mpbiran ⊢ n ∈ ℤ ⟼ n ⋅ G x : ℤ ⟶ onto B ↔ ran ⁡ n ∈ ℤ ⟼ n ⋅ G x = B
10 omelon ⊢ ω ∈ On
11 onenon ⊢ ω ∈ On → ω ∈ dom ⁡ card
12 10 11 ax-mp ⊢ ω ∈ dom ⁡ card
13 znnen ⊢ ℤ ≈ ℕ
14 nnenom ⊢ ℕ ≈ ω
15 13 14 entri ⊢ ℤ ≈ ω
16 ennum ⊢ ℤ ≈ ω → ℤ ∈ dom ⁡ card ↔ ω ∈ dom ⁡ card
17 15 16 ax-mp ⊢ ℤ ∈ dom ⁡ card ↔ ω ∈ dom ⁡ card
18 12 17 mpbir ⊢ ℤ ∈ dom ⁡ card
19 fodomnum ⊢ ℤ ∈ dom ⁡ card → n ∈ ℤ ⟼ n ⋅ G x : ℤ ⟶ onto B → B ≼ ℤ
20 18 19 mp1i ⊢ G ∈ CycGrp ∧ x ∈ B → n ∈ ℤ ⟼ n ⋅ G x : ℤ ⟶ onto B → B ≼ ℤ
21 domentr ⊢ B ≼ ℤ ∧ ℤ ≈ ω → B ≼ ω
22 15 21 mpan2 ⊢ B ≼ ℤ → B ≼ ω
23 20 22 syl6 ⊢ G ∈ CycGrp ∧ x ∈ B → n ∈ ℤ ⟼ n ⋅ G x : ℤ ⟶ onto B → B ≼ ω
24 9 23 biimtrrid ⊢ G ∈ CycGrp ∧ x ∈ B → ran ⁡ n ∈ ℤ ⟼ n ⋅ G x = B → B ≼ ω
25 24 rexlimdva ⊢ G ∈ CycGrp → ∃ x ∈ B ran ⁡ n ∈ ℤ ⟼ n ⋅ G x = B → B ≼ ω
26 4 25 mpd ⊢ G ∈ CycGrp → B ≼ ω