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