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 e. CycGrp -> B ~<_ _om )

Proof

Step	Hyp	Ref	Expression
1		cygctb.1	|- B = ( Base ` G )
2		eqid	|- ( .g ` G ) = ( .g ` G )
3	1 2	iscyg	|- ( G e. CycGrp <-> ( G e. Grp /\ E. x e. B ran ( n e. ZZ |-> ( n ( .g ` G ) x ) ) = B ) )
4	3	simprbi	|- ( G e. CycGrp -> E. x e. B ran ( n e. ZZ |-> ( n ( .g ` G ) x ) ) = B )
5		ovex	|- ( n ( .g ` G ) x ) e. _V
6		eqid	|- ( n e. ZZ |-> ( n ( .g ` G ) x ) ) = ( n e. ZZ |-> ( n ( .g ` G ) x ) )
7	5 6	fnmpti	|- ( n e. ZZ |-> ( n ( .g ` G ) x ) ) Fn ZZ
8		df-fo	|- ( ( n e. ZZ |-> ( n ( .g ` G ) x ) ) : ZZ -onto-> B <-> ( ( n e. ZZ |-> ( n ( .g ` G ) x ) ) Fn ZZ /\ ran ( n e. ZZ |-> ( n ( .g ` G ) x ) ) = B ) )
9	7 8	mpbiran	|- ( ( n e. ZZ |-> ( n ( .g ` G ) x ) ) : ZZ -onto-> B <-> ran ( n e. ZZ |-> ( n ( .g ` G ) x ) ) = B )
10		omelon	|- _om e. On
11		onenon	|- ( _om e. On -> _om e. dom card )
12	10 11	ax-mp	|- _om e. dom card
13		znnen	|- ZZ ~~ NN
14		nnenom	|- NN ~~ _om
15	13 14	entri	|- ZZ ~~ _om
16		ennum	|- ( ZZ ~~ _om -> ( ZZ e. dom card <-> _om e. dom card ) )
17	15 16	ax-mp	|- ( ZZ e. dom card <-> _om e. dom card )
18	12 17	mpbir	|- ZZ e. dom card
19		fodomnum	|- ( ZZ e. dom card -> ( ( n e. ZZ |-> ( n ( .g ` G ) x ) ) : ZZ -onto-> B -> B ~<_ ZZ ) )
20	18 19	mp1i	|- ( ( G e. CycGrp /\ x e. B ) -> ( ( n e. ZZ |-> ( n ( .g ` G ) x ) ) : ZZ -onto-> B -> B ~<_ ZZ ) )
21		domentr	|- ( ( B ~<_ ZZ /\ ZZ ~~ _om ) -> B ~<_ _om )
22	15 21	mpan2	|- ( B ~<_ ZZ -> B ~<_ _om )
23	20 22	syl6	|- ( ( G e. CycGrp /\ x e. B ) -> ( ( n e. ZZ |-> ( n ( .g ` G ) x ) ) : ZZ -onto-> B -> B ~<_ _om ) )
24	9 23	syl5bir	|- ( ( G e. CycGrp /\ x e. B ) -> ( ran ( n e. ZZ |-> ( n ( .g ` G ) x ) ) = B -> B ~<_ _om ) )
25	24	rexlimdva	|- ( G e. CycGrp -> ( E. x e. B ran ( n e. ZZ |-> ( n ( .g ` G ) x ) ) = B -> B ~<_ _om ) )
26	4 25	mpd	|- ( G e. CycGrp -> B ~<_ _om )