Metamath Proof Explorer

Theorem isnumbasgrplem1

Description: A set which is equipollent to the base set of a definable Abelian group is the base set of some (relabeled) Abelian group. (Contributed by Stefan O'Rear, 8-Jul-2015)

Ref Expression
Hypothesis isnumbasgrplem1.b 
|- B = ( Base ` R )
Assertion isnumbasgrplem1 
|- ( ( R e. Abel /\ C ~~ B ) -> C e. ( Base " Abel ) )

Proof

Step Hyp Ref Expression
1 isnumbasgrplem1.b 
 |-  B = ( Base ` R )
2 ensymb 
 |-  ( C ~~ B <-> B ~~ C )
3 bren 
 |-  ( B ~~ C <-> E. f f : B -1-1-onto-> C )
4 2 3 bitri 
 |-  ( C ~~ B <-> E. f f : B -1-1-onto-> C )
5 eqidd 
 |-  ( ( f : B -1-1-onto-> C /\ R e. Abel ) -> ( f "s R ) = ( f "s R ) )
6 1 a1i 
 |-  ( ( f : B -1-1-onto-> C /\ R e. Abel ) -> B = ( Base ` R ) )
7 f1ofo 
 |-  ( f : B -1-1-onto-> C -> f : B -onto-> C )
8 7 adantr 
 |-  ( ( f : B -1-1-onto-> C /\ R e. Abel ) -> f : B -onto-> C )
9 simpr 
 |-  ( ( f : B -1-1-onto-> C /\ R e. Abel ) -> R e. Abel )
10 5 6 8 9 imasbas 
 |-  ( ( f : B -1-1-onto-> C /\ R e. Abel ) -> C = ( Base ` ( f "s R ) ) )
11 simpl 
 |-  ( ( f : B -1-1-onto-> C /\ R e. Abel ) -> f : B -1-1-onto-> C )
12 ablgrp 
 |-  ( R e. Abel -> R e. Grp )
13 12 adantl 
 |-  ( ( f : B -1-1-onto-> C /\ R e. Abel ) -> R e. Grp )
14 5 6 11 13 imasgim 
 |-  ( ( f : B -1-1-onto-> C /\ R e. Abel ) -> f e. ( R GrpIso ( f "s R ) ) )
15 brgici 
 |-  ( f e. ( R GrpIso ( f "s R ) ) -> R ~=g ( f "s R ) )
16 gicabl 
 |-  ( R ~=g ( f "s R ) -> ( R e. Abel <-> ( f "s R ) e. Abel ) )
17 14 15 16 3syl 
 |-  ( ( f : B -1-1-onto-> C /\ R e. Abel ) -> ( R e. Abel <-> ( f "s R ) e. Abel ) )
18 9 17 mpbid 
 |-  ( ( f : B -1-1-onto-> C /\ R e. Abel ) -> ( f "s R ) e. Abel )
19 basfn 
 |-  Base Fn _V
20 ssv 
 |-  Abel C_ _V
21 fnfvima 
 |-  ( ( Base Fn _V /\ Abel C_ _V /\ ( f "s R ) e. Abel ) -> ( Base ` ( f "s R ) ) e. ( Base " Abel ) )
22 19 20 21 mp3an12 
 |-  ( ( f "s R ) e. Abel -> ( Base ` ( f "s R ) ) e. ( Base " Abel ) )
23 18 22 syl 
 |-  ( ( f : B -1-1-onto-> C /\ R e. Abel ) -> ( Base ` ( f "s R ) ) e. ( Base " Abel ) )
24 10 23 eqeltrd 
 |-  ( ( f : B -1-1-onto-> C /\ R e. Abel ) -> C e. ( Base " Abel ) )
25 24 ex 
 |-  ( f : B -1-1-onto-> C -> ( R e. Abel -> C e. ( Base " Abel ) ) )
26 25 exlimiv 
 |-  ( E. f f : B -1-1-onto-> C -> ( R e. Abel -> C e. ( Base " Abel ) ) )
27 26 impcom 
 |-  ( ( R e. Abel /\ E. f f : B -1-1-onto-> C ) -> C e. ( Base " Abel ) )
28 4 27 sylan2b 
 |-  ( ( R e. Abel /\ C ~~ B ) -> C e. ( Base " Abel ) )