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=BaseR
Assertion isnumbasgrplem1 ⊢R∈Abel∧C≈B→C∈BaseAbel

Proof

Step Hyp Ref Expression
1 isnumbasgrplem1.b ⊢B=BaseR
2 ensymb ⊢C≈B↔B≈C
3 bren ⊢B≈C↔∃ff:B⟶1-1 ontoC
4 2 3 bitri ⊢C≈B↔∃ff:B⟶1-1 ontoC
5 eqidd ⊢f:B⟶1-1 ontoC∧R∈Abel→f“𝑠R=f“𝑠R
6 1 a1i ⊢f:B⟶1-1 ontoC∧R∈Abel→B=BaseR
7 f1ofo ⊢f:B⟶1-1 ontoC→f:B⟶ontoC
8 7 adantr ⊢f:B⟶1-1 ontoC∧R∈Abel→f:B⟶ontoC
9 simpr ⊢f:B⟶1-1 ontoC∧R∈Abel→R∈Abel
10 5 6 8 9 imasbas ⊢f:B⟶1-1 ontoC∧R∈Abel→C=Basef“𝑠R
11 simpl ⊢f:B⟶1-1 ontoC∧R∈Abel→f:B⟶1-1 ontoC
12 ablgrp ⊢R∈Abel→R∈Grp
13 12 adantl ⊢f:B⟶1-1 ontoC∧R∈Abel→R∈Grp
14 5 6 11 13 imasgim ⊢f:B⟶1-1 ontoC∧R∈Abel→f∈RGrpIsof“𝑠R
15 brgici ⊢f∈RGrpIsof“𝑠R→R≃𝑔f“𝑠R
16 gicabl ⊢R≃𝑔f“𝑠R→R∈Abel↔f“𝑠R∈Abel
17 14 15 16 3syl ⊢f:B⟶1-1 ontoC∧R∈Abel→R∈Abel↔f“𝑠R∈Abel
18 9 17 mpbid ⊢f:B⟶1-1 ontoC∧R∈Abel→f“𝑠R∈Abel
19 basfn ⊢BaseFnV
20 ssv ⊢Abel⊆V
21 fnfvima ⊢BaseFnV∧Abel⊆V∧f“𝑠R∈Abel→Basef“𝑠R∈BaseAbel
22 19 20 21 mp3an12 ⊢f“𝑠R∈Abel→Basef“𝑠R∈BaseAbel
23 18 22 syl ⊢f:B⟶1-1 ontoC∧R∈Abel→Basef“𝑠R∈BaseAbel
24 10 23 eqeltrd ⊢f:B⟶1-1 ontoC∧R∈Abel→C∈BaseAbel
25 24 ex ⊢f:B⟶1-1 ontoC→R∈Abel→C∈BaseAbel
26 25 exlimiv ⊢∃ff:B⟶1-1 ontoC→R∈Abel→C∈BaseAbel
27 26 impcom ⊢R∈Abel∧∃ff:B⟶1-1 ontoC→C∈BaseAbel
28 4 27 sylan2b ⊢R∈Abel∧C≈B→C∈BaseAbel