This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

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 )