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 Abel C B C Base Abel

Proof

Step Hyp Ref Expression
1 isnumbasgrplem1.b B = Base R
2 ensymb C B B C
3 bren B C f f : B 1-1 onto C
4 2 3 bitri C B f f : B 1-1 onto C
5 eqidd f : B 1-1 onto C R Abel f 𝑠 R = f 𝑠 R
6 1 a1i f : B 1-1 onto C R 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 Abel f : B onto C
9 simpr f : B 1-1 onto C R Abel R Abel
10 5 6 8 9 imasbas f : B 1-1 onto C R Abel C = Base f 𝑠 R
11 simpl f : B 1-1 onto C R Abel f : B 1-1 onto C
12 ablgrp R Abel R Grp
13 12 adantl f : B 1-1 onto C R Abel R Grp
14 5 6 11 13 imasgim f : B 1-1 onto C R Abel f R GrpIso f 𝑠 R
15 brgici f R GrpIso f 𝑠 R R 𝑔 f 𝑠 R
16 gicabl R 𝑔 f 𝑠 R R Abel f 𝑠 R Abel
17 14 15 16 3syl f : B 1-1 onto C R Abel R Abel f 𝑠 R Abel
18 9 17 mpbid f : B 1-1 onto C R Abel f 𝑠 R Abel
19 basfn Base Fn V
20 ssv Abel V
21 fnfvima Base Fn V Abel V f 𝑠 R Abel Base f 𝑠 R Base Abel
22 19 20 21 mp3an12 f 𝑠 R Abel Base f 𝑠 R Base Abel
23 18 22 syl f : B 1-1 onto C R Abel Base f 𝑠 R Base Abel
24 10 23 eqeltrd f : B 1-1 onto C R Abel C Base Abel
25 24 ex f : B 1-1 onto C R Abel C Base Abel
26 25 exlimiv f f : B 1-1 onto C R Abel C Base Abel
27 26 impcom R Abel f f : B 1-1 onto C C Base Abel
28 4 27 sylan2b R Abel C B C Base Abel