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 
|- 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 biimtrrid 
 |-  ( ( 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 )