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 \in CycGrp \to B ≼ ω$

Proof

Step	Hyp	Ref	Expression
1		cygctb.1	$⊢ B = {Base}_{G}$
2		eqid	$⊢ \cdot_{G} = \cdot_{G}$
3	1 2	iscyg	$⊢ G \in CycGrp \leftrightarrow (G \in Grp \land \exists x \in B ran (n \in ℤ ⟼ n \cdot_{G} x) = B)$
4	3	simprbi	$⊢ G \in CycGrp \to \exists x \in B ran (n \in ℤ ⟼ n \cdot_{G} x) = B$
5		ovex	$⊢ n \cdot_{G} x \in V$
6		eqid	$⊢ (n \in ℤ ⟼ n \cdot_{G} x) = (n \in ℤ ⟼ n \cdot_{G} x)$
7	5 6	fnmpti	$⊢ (n \in ℤ ⟼ n \cdot_{G} x) Fn ℤ$
8		df-fo	$⊢ (n \in ℤ ⟼ n \cdot_{G} x) : ℤ \underset{onto}{⟶} B \leftrightarrow ((n \in ℤ ⟼ n \cdot_{G} x) Fn ℤ \land ran (n \in ℤ ⟼ n \cdot_{G} x) = B)$
9	7 8	mpbiran	$⊢ (n \in ℤ ⟼ n \cdot_{G} x) : ℤ \underset{onto}{⟶} B \leftrightarrow ran (n \in ℤ ⟼ n \cdot_{G} x) = B$
10		omelon	$⊢ ω \in On$
11		onenon	$⊢ ω \in On \to ω \in dom card$
12	10 11	ax-mp	$⊢ ω \in dom card$
13		znnen	$⊢ ℤ \approx ℕ$
14		nnenom	$⊢ ℕ \approx ω$
15	13 14	entri	$⊢ ℤ \approx ω$
16		ennum	$⊢ ℤ \approx ω \to (ℤ \in dom card \leftrightarrow ω \in dom card)$
17	15 16	ax-mp	$⊢ ℤ \in dom card \leftrightarrow ω \in dom card$
18	12 17	mpbir	$⊢ ℤ \in dom card$
19		fodomnum	$⊢ ℤ \in dom card \to ((n \in ℤ ⟼ n \cdot_{G} x) : ℤ \underset{onto}{⟶} B \to B ≼ ℤ)$
20	18 19	mp1i	$⊢ (G \in CycGrp \land x \in B) \to ((n \in ℤ ⟼ n \cdot_{G} x) : ℤ \underset{onto}{⟶} B \to B ≼ ℤ)$
21		domentr	$⊢ (B ≼ ℤ \land ℤ \approx ω) \to B ≼ ω$
22	15 21	mpan2	$⊢ B ≼ ℤ \to B ≼ ω$
23	20 22	syl6	$⊢ (G \in CycGrp \land x \in B) \to ((n \in ℤ ⟼ n \cdot_{G} x) : ℤ \underset{onto}{⟶} B \to B ≼ ω)$
24	9 23	biimtrrid	$⊢ (G \in CycGrp \land x \in B) \to (ran (n \in ℤ ⟼ n \cdot_{G} x) = B \to B ≼ ω)$
25	24	rexlimdva	$⊢ G \in CycGrp \to (\exists x \in B ran (n \in ℤ ⟼ n \cdot_{G} x) = B \to B ≼ ω)$
26	4 25	mpd	$⊢ G \in CycGrp \to B ≼ ω$

Metamath Proof Explorer

Theorem cygctb

Proof