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	syl5bir	⊢ ( ( 𝐺 ∈ CycGrp ∧ 𝑥 ∈ 𝐵 ) → ( ran ( 𝑛 ∈ ℤ ↦ ( 𝑛 ( .g ‘ 𝐺 ) 𝑥 ) ) = 𝐵 → 𝐵 ≼ ω ) )
25	24	rexlimdva	⊢ ( 𝐺 ∈ CycGrp → ( ∃ 𝑥 ∈ 𝐵 ran ( 𝑛 ∈ ℤ ↦ ( 𝑛 ( .g ‘ 𝐺 ) 𝑥 ) ) = 𝐵 → 𝐵 ≼ ω ) )
26	4 25	mpd	⊢ ( 𝐺 ∈ CycGrp → 𝐵 ≼ ω )