Metamath Proof Explorer


Theorem gicen

Description: Isomorphic groups have equinumerous base sets. (Contributed by Stefan O'Rear, 25-Jan-2015)

Ref Expression
Hypotheses gicen.b
|- B = ( Base ` R )
gicen.c
|- C = ( Base ` S )
Assertion gicen
|- ( R ~=g S -> B ~~ C )

Proof

Step Hyp Ref Expression
1 gicen.b
 |-  B = ( Base ` R )
2 gicen.c
 |-  C = ( Base ` S )
3 brgic
 |-  ( R ~=g S <-> ( R GrpIso S ) =/= (/) )
4 n0
 |-  ( ( R GrpIso S ) =/= (/) <-> E. f f e. ( R GrpIso S ) )
5 1 2 gimf1o
 |-  ( f e. ( R GrpIso S ) -> f : B -1-1-onto-> C )
6 1 fvexi
 |-  B e. _V
7 6 f1oen
 |-  ( f : B -1-1-onto-> C -> B ~~ C )
8 5 7 syl
 |-  ( f e. ( R GrpIso S ) -> B ~~ C )
9 8 exlimiv
 |-  ( E. f f e. ( R GrpIso S ) -> B ~~ C )
10 4 9 sylbi
 |-  ( ( R GrpIso S ) =/= (/) -> B ~~ C )
11 3 10 sylbi
 |-  ( R ~=g S -> B ~~ C )