Metamath Proof Explorer

Theorem fingrphf

Description: Every finite group is isomorphic to a group with hereditarily finite components. (Contributed by Eric Schmidt, 24-Oct-2026)

Ref Expression
Hypotheses fingrphf.1 ⊢ 𝐵 = ( Base ‘ 𝐺 )
fingrphf.2 ⊢ ( 𝜑 → 𝐺 ∈ Grp )
fingrphf.3 ⊢ ( 𝜑 → 𝐵 ∈ Fin )
Assertion fingrphf ( 𝜑 → ∃ ℎ ∈ HFStruct 𝐺 ≃𝑔 ℎ )

Proof

Step Hyp Ref Expression
1 fingrphf.1 ⊢ 𝐵 = ( Base ‘ 𝐺 )
2 fingrphf.2 ⊢ ( 𝜑 → 𝐺 ∈ Grp )
3 fingrphf.3 ⊢ ( 𝜑 → 𝐵 ∈ Fin )
4 ficardid ⊢ ( 𝐵 ∈ Fin → ( card ‘ 𝐵 ) ≈ 𝐵 )
5 4 ensymd ⊢ ( 𝐵 ∈ Fin → 𝐵 ≈ ( card ‘ 𝐵 ) )
6 bren ⊢ ( 𝐵 ≈ ( card ‘ 𝐵 ) ↔ ∃ 𝑓 𝑓 : 𝐵 ⟶1-1onto ( card ‘ 𝐵 ) )
7 5 6 sylib ⊢ ( 𝐵 ∈ Fin → ∃ 𝑓 𝑓 : 𝐵 ⟶1-1onto ( card ‘ 𝐵 ) )
8 3 7 syl ⊢ ( 𝜑 → ∃ 𝑓 𝑓 : 𝐵 ⟶1-1onto ( card ‘ 𝐵 ) )
9 breq2 ⊢ ( ℎ = { ⟨ ( Base ‘ ndx ) , ( Base ‘ ( 𝑓 “s 𝐺 ) ) ⟩ , ⟨ ( +g ‘ ndx ) , ( +𝑓 ‘ ( 𝑓 “s 𝐺 ) ) ⟩ } → ( 𝐺 ≃𝑔 ℎ ↔ 𝐺 ≃𝑔 { ⟨ ( Base ‘ ndx ) , ( Base ‘ ( 𝑓 “s 𝐺 ) ) ⟩ , ⟨ ( +g ‘ ndx ) , ( +𝑓 ‘ ( 𝑓 “s 𝐺 ) ) ⟩ } ) )
10 eqid ⊢ ( Base ‘ ( 𝑓 “s 𝐺 ) ) = ( Base ‘ ( 𝑓 “s 𝐺 ) )
11 eqid ⊢ ( +𝑓 ‘ ( 𝑓 “s 𝐺 ) ) = ( +𝑓 ‘ ( 𝑓 “s 𝐺 ) )
12 eqid ⊢ { ⟨ ( Base ‘ ndx ) , ( Base ‘ ( 𝑓 “s 𝐺 ) ) ⟩ , ⟨ ( +g ‘ ndx ) , ( +𝑓 ‘ ( 𝑓 “s 𝐺 ) ) ⟩ } = { ⟨ ( Base ‘ ndx ) , ( Base ‘ ( 𝑓 “s 𝐺 ) ) ⟩ , ⟨ ( +g ‘ ndx ) , ( +𝑓 ‘ ( 𝑓 “s 𝐺 ) ) ⟩ }
13 eqidd ⊢ ( ( 𝐺 ∈ Grp ∧ 𝑓 : 𝐵 ⟶1-1onto ( card ‘ 𝐵 ) ) → ( 𝑓 “s 𝐺 ) = ( 𝑓 “s 𝐺 ) )
14 1 a1i ⊢ ( ( 𝐺 ∈ Grp ∧ 𝑓 : 𝐵 ⟶1-1onto ( card ‘ 𝐵 ) ) → 𝐵 = ( Base ‘ 𝐺 ) )
15 simpr ⊢ ( ( 𝐺 ∈ Grp ∧ 𝑓 : 𝐵 ⟶1-1onto ( card ‘ 𝐵 ) ) → 𝑓 : 𝐵 ⟶1-1onto ( card ‘ 𝐵 ) )
16 simpl ⊢ ( ( 𝐺 ∈ Grp ∧ 𝑓 : 𝐵 ⟶1-1onto ( card ‘ 𝐵 ) ) → 𝐺 ∈ Grp )
17 fvex ⊢ ( card ‘ 𝐵 ) ∈ V
18 13 14 15 16 17 imasgimw ⊢ ( ( 𝐺 ∈ Grp ∧ 𝑓 : 𝐵 ⟶1-1onto ( card ‘ 𝐵 ) ) → 𝑓 ∈ ( 𝐺 GrpIso ( 𝑓 “s 𝐺 ) ) )
19 gimghm ⊢ ( 𝑓 ∈ ( 𝐺 GrpIso ( 𝑓 “s 𝐺 ) ) → 𝑓 ∈ ( 𝐺 GrpHom ( 𝑓 “s 𝐺 ) ) )
20 ghmgrp2 ⊢ ( 𝑓 ∈ ( 𝐺 GrpHom ( 𝑓 “s 𝐺 ) ) → ( 𝑓 “s 𝐺 ) ∈ Grp )
21 18 19 20 3syl ⊢ ( ( 𝐺 ∈ Grp ∧ 𝑓 : 𝐵 ⟶1-1onto ( card ‘ 𝐵 ) ) → ( 𝑓 “s 𝐺 ) ∈ Grp )
22 2 21 sylan ⊢ ( ( 𝜑 ∧ 𝑓 : 𝐵 ⟶1-1onto ( card ‘ 𝐵 ) ) → ( 𝑓 “s 𝐺 ) ∈ Grp )
23 eqidd ⊢ ( ( 𝜑 ∧ 𝑓 : 𝐵 ⟶1-1onto ( card ‘ 𝐵 ) ) → ( 𝑓 “s 𝐺 ) = ( 𝑓 “s 𝐺 ) )
24 1 a1i ⊢ ( ( 𝜑 ∧ 𝑓 : 𝐵 ⟶1-1onto ( card ‘ 𝐵 ) ) → 𝐵 = ( Base ‘ 𝐺 ) )
25 f1ofo ⊢ ( 𝑓 : 𝐵 ⟶1-1onto ( card ‘ 𝐵 ) → 𝑓 : 𝐵 ⟶onto ( card ‘ 𝐵 ) )
26 25 adantl ⊢ ( ( 𝜑 ∧ 𝑓 : 𝐵 ⟶1-1onto ( card ‘ 𝐵 ) ) → 𝑓 : 𝐵 ⟶onto ( card ‘ 𝐵 ) )
27 2 adantr ⊢ ( ( 𝜑 ∧ 𝑓 : 𝐵 ⟶1-1onto ( card ‘ 𝐵 ) ) → 𝐺 ∈ Grp )
28 23 24 26 27 imasbas ⊢ ( ( 𝜑 ∧ 𝑓 : 𝐵 ⟶1-1onto ( card ‘ 𝐵 ) ) → ( card ‘ 𝐵 ) = ( Base ‘ ( 𝑓 “s 𝐺 ) ) )
29 ficardom ⊢ ( 𝐵 ∈ Fin → ( card ‘ 𝐵 ) ∈ ω )
30 omhf ⊢ ( ( card ‘ 𝐵 ) ∈ ω → ( card ‘ 𝐵 ) ∈ HF )
31 3 29 30 3syl ⊢ ( 𝜑 → ( card ‘ 𝐵 ) ∈ HF )
32 31 adantr ⊢ ( ( 𝜑 ∧ 𝑓 : 𝐵 ⟶1-1onto ( card ‘ 𝐵 ) ) → ( card ‘ 𝐵 ) ∈ HF )
33 28 32 eqeltrrd ⊢ ( ( 𝜑 ∧ 𝑓 : 𝐵 ⟶1-1onto ( card ‘ 𝐵 ) ) → ( Base ‘ ( 𝑓 “s 𝐺 ) ) ∈ HF )
34 10 11 12 22 33 grpcanonhfstruct ⊢ ( ( 𝜑 ∧ 𝑓 : 𝐵 ⟶1-1onto ( card ‘ 𝐵 ) ) → { ⟨ ( Base ‘ ndx ) , ( Base ‘ ( 𝑓 “s 𝐺 ) ) ⟩ , ⟨ ( +g ‘ ndx ) , ( +𝑓 ‘ ( 𝑓 “s 𝐺 ) ) ⟩ } ∈ HFStruct )
35 10 11 12 grpgimcanon ⊢ ( ( 𝑓 “s 𝐺 ) ∈ Grp → ( I ↾ ( Base ‘ ( 𝑓 “s 𝐺 ) ) ) ∈ ( ( 𝑓 “s 𝐺 ) GrpIso { ⟨ ( Base ‘ ndx ) , ( Base ‘ ( 𝑓 “s 𝐺 ) ) ⟩ , ⟨ ( +g ‘ ndx ) , ( +𝑓 ‘ ( 𝑓 “s 𝐺 ) ) ⟩ } ) )
36 21 35 syl ⊢ ( ( 𝐺 ∈ Grp ∧ 𝑓 : 𝐵 ⟶1-1onto ( card ‘ 𝐵 ) ) → ( I ↾ ( Base ‘ ( 𝑓 “s 𝐺 ) ) ) ∈ ( ( 𝑓 “s 𝐺 ) GrpIso { ⟨ ( Base ‘ ndx ) , ( Base ‘ ( 𝑓 “s 𝐺 ) ) ⟩ , ⟨ ( +g ‘ ndx ) , ( +𝑓 ‘ ( 𝑓 “s 𝐺 ) ) ⟩ } ) )
37 gimco ⊢ ( ( ( I ↾ ( Base ‘ ( 𝑓 “s 𝐺 ) ) ) ∈ ( ( 𝑓 “s 𝐺 ) GrpIso { ⟨ ( Base ‘ ndx ) , ( Base ‘ ( 𝑓 “s 𝐺 ) ) ⟩ , ⟨ ( +g ‘ ndx ) , ( +𝑓 ‘ ( 𝑓 “s 𝐺 ) ) ⟩ } ) ∧ 𝑓 ∈ ( 𝐺 GrpIso ( 𝑓 “s 𝐺 ) ) ) → ( ( I ↾ ( Base ‘ ( 𝑓 “s 𝐺 ) ) ) ∘ 𝑓 ) ∈ ( 𝐺 GrpIso { ⟨ ( Base ‘ ndx ) , ( Base ‘ ( 𝑓 “s 𝐺 ) ) ⟩ , ⟨ ( +g ‘ ndx ) , ( +𝑓 ‘ ( 𝑓 “s 𝐺 ) ) ⟩ } ) )
38 36 18 37 syl2anc ⊢ ( ( 𝐺 ∈ Grp ∧ 𝑓 : 𝐵 ⟶1-1onto ( card ‘ 𝐵 ) ) → ( ( I ↾ ( Base ‘ ( 𝑓 “s 𝐺 ) ) ) ∘ 𝑓 ) ∈ ( 𝐺 GrpIso { ⟨ ( Base ‘ ndx ) , ( Base ‘ ( 𝑓 “s 𝐺 ) ) ⟩ , ⟨ ( +g ‘ ndx ) , ( +𝑓 ‘ ( 𝑓 “s 𝐺 ) ) ⟩ } ) )
39 brgici ⊢ ( ( ( I ↾ ( Base ‘ ( 𝑓 “s 𝐺 ) ) ) ∘ 𝑓 ) ∈ ( 𝐺 GrpIso { ⟨ ( Base ‘ ndx ) , ( Base ‘ ( 𝑓 “s 𝐺 ) ) ⟩ , ⟨ ( +g ‘ ndx ) , ( +𝑓 ‘ ( 𝑓 “s 𝐺 ) ) ⟩ } ) → 𝐺 ≃𝑔 { ⟨ ( Base ‘ ndx ) , ( Base ‘ ( 𝑓 “s 𝐺 ) ) ⟩ , ⟨ ( +g ‘ ndx ) , ( +𝑓 ‘ ( 𝑓 “s 𝐺 ) ) ⟩ } )
40 38 39 syl ⊢ ( ( 𝐺 ∈ Grp ∧ 𝑓 : 𝐵 ⟶1-1onto ( card ‘ 𝐵 ) ) → 𝐺 ≃𝑔 { ⟨ ( Base ‘ ndx ) , ( Base ‘ ( 𝑓 “s 𝐺 ) ) ⟩ , ⟨ ( +g ‘ ndx ) , ( +𝑓 ‘ ( 𝑓 “s 𝐺 ) ) ⟩ } )
41 2 40 sylan ⊢ ( ( 𝜑 ∧ 𝑓 : 𝐵 ⟶1-1onto ( card ‘ 𝐵 ) ) → 𝐺 ≃𝑔 { ⟨ ( Base ‘ ndx ) , ( Base ‘ ( 𝑓 “s 𝐺 ) ) ⟩ , ⟨ ( +g ‘ ndx ) , ( +𝑓 ‘ ( 𝑓 “s 𝐺 ) ) ⟩ } )
42 9 34 41 rspcedvdw ⊢ ( ( 𝜑 ∧ 𝑓 : 𝐵 ⟶1-1onto ( card ‘ 𝐵 ) ) → ∃ ℎ ∈ HFStruct 𝐺 ≃𝑔 ℎ )
43 8 42 exlimddv ⊢ ( 𝜑 → ∃ ℎ ∈ HFStruct 𝐺 ≃𝑔 ℎ )