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 ⊢ 𝐵 = ( Base ‘ 𝑅 )
Assertion isnumbasgrplem1 ( ( 𝑅 ∈ Abel ∧ 𝐶 ≈ 𝐵 ) → 𝐶 ∈ ( Base “ Abel ) )

Proof

Step Hyp Ref Expression
1 isnumbasgrplem1.b ⊢ 𝐵 = ( Base ‘ 𝑅 )
2 ensymb ⊢ ( 𝐶 ≈ 𝐵 ↔ 𝐵 ≈ 𝐶 )
3 bren ⊢ ( 𝐵 ≈ 𝐶 ↔ ∃ 𝑓 𝑓 : 𝐵 –1-1-onto→ 𝐶 )
4 2 3 bitri ⊢ ( 𝐶 ≈ 𝐵 ↔ ∃ 𝑓 𝑓 : 𝐵 –1-1-onto→ 𝐶 )
5 eqidd ⊢ ( ( 𝑓 : 𝐵 –1-1-onto→ 𝐶 ∧ 𝑅 ∈ Abel ) → ( 𝑓 “s 𝑅 ) = ( 𝑓 “s 𝑅 ) )
6 1 a1i ⊢ ( ( 𝑓 : 𝐵 –1-1-onto→ 𝐶 ∧ 𝑅 ∈ Abel ) → 𝐵 = ( Base ‘ 𝑅 ) )
7 f1ofo ⊢ ( 𝑓 : 𝐵 –1-1-onto→ 𝐶 → 𝑓 : 𝐵 –onto→ 𝐶 )
8 7 adantr ⊢ ( ( 𝑓 : 𝐵 –1-1-onto→ 𝐶 ∧ 𝑅 ∈ Abel ) → 𝑓 : 𝐵 –onto→ 𝐶 )
9 simpr ⊢ ( ( 𝑓 : 𝐵 –1-1-onto→ 𝐶 ∧ 𝑅 ∈ Abel ) → 𝑅 ∈ Abel )
10 5 6 8 9 imasbas ⊢ ( ( 𝑓 : 𝐵 –1-1-onto→ 𝐶 ∧ 𝑅 ∈ Abel ) → 𝐶 = ( Base ‘ ( 𝑓 “s 𝑅 ) ) )
11 simpl ⊢ ( ( 𝑓 : 𝐵 –1-1-onto→ 𝐶 ∧ 𝑅 ∈ Abel ) → 𝑓 : 𝐵 –1-1-onto→ 𝐶 )
12 ablgrp ⊢ ( 𝑅 ∈ Abel → 𝑅 ∈ Grp )
13 12 adantl ⊢ ( ( 𝑓 : 𝐵 –1-1-onto→ 𝐶 ∧ 𝑅 ∈ Abel ) → 𝑅 ∈ Grp )
14 5 6 11 13 imasgim ⊢ ( ( 𝑓 : 𝐵 –1-1-onto→ 𝐶 ∧ 𝑅 ∈ Abel ) → 𝑓 ∈ ( 𝑅 GrpIso ( 𝑓 “s 𝑅 ) ) )
15 brgici ⊢ ( 𝑓 ∈ ( 𝑅 GrpIso ( 𝑓 “s 𝑅 ) ) → 𝑅 ≃𝑔 ( 𝑓 “s 𝑅 ) )
16 gicabl ⊢ ( 𝑅 ≃𝑔 ( 𝑓 “s 𝑅 ) → ( 𝑅 ∈ Abel ↔ ( 𝑓 “s 𝑅 ) ∈ Abel ) )
17 14 15 16 3syl ⊢ ( ( 𝑓 : 𝐵 –1-1-onto→ 𝐶 ∧ 𝑅 ∈ Abel ) → ( 𝑅 ∈ Abel ↔ ( 𝑓 “s 𝑅 ) ∈ Abel ) )
18 9 17 mpbid ⊢ ( ( 𝑓 : 𝐵 –1-1-onto→ 𝐶 ∧ 𝑅 ∈ Abel ) → ( 𝑓 “s 𝑅 ) ∈ Abel )
19 basfn ⊢ Base Fn V
20 ssv ⊢ Abel ⊆ V
21 fnfvima ⊢ ( ( Base Fn V ∧ Abel ⊆ V ∧ ( 𝑓 “s 𝑅 ) ∈ Abel ) → ( Base ‘ ( 𝑓 “s 𝑅 ) ) ∈ ( Base “ Abel ) )
22 19 20 21 mp3an12 ⊢ ( ( 𝑓 “s 𝑅 ) ∈ Abel → ( Base ‘ ( 𝑓 “s 𝑅 ) ) ∈ ( Base “ Abel ) )
23 18 22 syl ⊢ ( ( 𝑓 : 𝐵 –1-1-onto→ 𝐶 ∧ 𝑅 ∈ Abel ) → ( Base ‘ ( 𝑓 “s 𝑅 ) ) ∈ ( Base “ Abel ) )
24 10 23 eqeltrd ⊢ ( ( 𝑓 : 𝐵 –1-1-onto→ 𝐶 ∧ 𝑅 ∈ Abel ) → 𝐶 ∈ ( Base “ Abel ) )
25 24 ex ⊢ ( 𝑓 : 𝐵 –1-1-onto→ 𝐶 → ( 𝑅 ∈ Abel → 𝐶 ∈ ( Base “ Abel ) ) )
26 25 exlimiv ⊢ ( ∃ 𝑓 𝑓 : 𝐵 –1-1-onto→ 𝐶 → ( 𝑅 ∈ Abel → 𝐶 ∈ ( Base “ Abel ) ) )
27 26 impcom ⊢ ( ( 𝑅 ∈ Abel ∧ ∃ 𝑓 𝑓 : 𝐵 –1-1-onto→ 𝐶 ) → 𝐶 ∈ ( Base “ Abel ) )
28 4 27 sylan2b ⊢ ( ( 𝑅 ∈ Abel ∧ 𝐶 ≈ 𝐵 ) → 𝐶 ∈ ( Base “ Abel ) )