This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

Theorem cygctb

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

Ref Expression
Hypothesis cygctb.1 ⊢ 𝐵 = ( Base ‘ 𝐺 )
Assertion cygctb ( 𝐺 ∈ CycGrp → 𝐵 ≼ ω )

Proof

Step Hyp Ref Expression
1 cygctb.1 ⊢ 𝐵 = ( Base ‘ 𝐺 )
2 eqid ⊢ ( .g ‘ 𝐺 ) = ( .g ‘ 𝐺 )
3 1 2 iscyg ⊢ ( 𝐺 ∈ CycGrp ↔ ( 𝐺 ∈ Grp ∧ ∃ 𝑥 ∈ 𝐵 ran ( 𝑛 ∈ ℤ ↦ ( 𝑛 ( .g ‘ 𝐺 ) 𝑥 ) ) = 𝐵 ) )
4 3 simprbi ⊢ ( 𝐺 ∈ CycGrp → ∃ 𝑥 ∈ 𝐵 ran ( 𝑛 ∈ ℤ ↦ ( 𝑛 ( .g ‘ 𝐺 ) 𝑥 ) ) = 𝐵 )
5 ovex ⊢ ( 𝑛 ( .g ‘ 𝐺 ) 𝑥 ) ∈ V
6 eqid ⊢ ( 𝑛 ∈ ℤ ↦ ( 𝑛 ( .g ‘ 𝐺 ) 𝑥 ) ) = ( 𝑛 ∈ ℤ ↦ ( 𝑛 ( .g ‘ 𝐺 ) 𝑥 ) )
7 5 6 fnmpti ⊢ ( 𝑛 ∈ ℤ ↦ ( 𝑛 ( .g ‘ 𝐺 ) 𝑥 ) ) Fn ℤ
8 df-fo ⊢ ( ( 𝑛 ∈ ℤ ↦ ( 𝑛 ( .g ‘ 𝐺 ) 𝑥 ) ) : ℤ –onto→ 𝐵 ↔ ( ( 𝑛 ∈ ℤ ↦ ( 𝑛 ( .g ‘ 𝐺 ) 𝑥 ) ) Fn ℤ ∧ ran ( 𝑛 ∈ ℤ ↦ ( 𝑛 ( .g ‘ 𝐺 ) 𝑥 ) ) = 𝐵 ) )
9 7 8 mpbiran ⊢ ( ( 𝑛 ∈ ℤ ↦ ( 𝑛 ( .g ‘ 𝐺 ) 𝑥 ) ) : ℤ –onto→ 𝐵 ↔ ran ( 𝑛 ∈ ℤ ↦ ( 𝑛 ( .g ‘ 𝐺 ) 𝑥 ) ) = 𝐵 )
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 → ( ( 𝑛 ∈ ℤ ↦ ( 𝑛 ( .g ‘ 𝐺 ) 𝑥 ) ) : ℤ –onto→ 𝐵 → 𝐵 ≼ ℤ ) )
20 18 19 mp1i ⊢ ( ( 𝐺 ∈ CycGrp ∧ 𝑥 ∈ 𝐵 ) → ( ( 𝑛 ∈ ℤ ↦ ( 𝑛 ( .g ‘ 𝐺 ) 𝑥 ) ) : ℤ –onto→ 𝐵 → 𝐵 ≼ ℤ ) )
21 domentr ⊢ ( ( 𝐵 ≼ ℤ ∧ ℤ ≈ ω ) → 𝐵 ≼ ω )
22 15 21 mpan2 ⊢ ( 𝐵 ≼ ℤ → 𝐵 ≼ ω )
23 20 22 syl6 ⊢ ( ( 𝐺 ∈ CycGrp ∧ 𝑥 ∈ 𝐵 ) → ( ( 𝑛 ∈ ℤ ↦ ( 𝑛 ( .g ‘ 𝐺 ) 𝑥 ) ) : ℤ –onto→ 𝐵 → 𝐵 ≼ ω ) )
24 9 23 biimtrrid ⊢ ( ( 𝐺 ∈ CycGrp ∧ 𝑥 ∈ 𝐵 ) → ( ran ( 𝑛 ∈ ℤ ↦ ( 𝑛 ( .g ‘ 𝐺 ) 𝑥 ) ) = 𝐵 → 𝐵 ≼ ω ) )
25 24 rexlimdva ⊢ ( 𝐺 ∈ CycGrp → ( ∃ 𝑥 ∈ 𝐵 ran ( 𝑛 ∈ ℤ ↦ ( 𝑛 ( .g ‘ 𝐺 ) 𝑥 ) ) = 𝐵 → 𝐵 ≼ ω ) )
26 4 25 mpd ⊢ ( 𝐺 ∈ CycGrp → 𝐵 ≼ ω )