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 
|- B = ( Base ` G )
fingrphf.2 
|- ( ph -> G e. Grp )
fingrphf.3 
|- ( ph -> B e. Fin )
Assertion fingrphf 
|- ( ph -> E. h e. HFStruct G ~=g h )

Proof

Step Hyp Ref Expression
1 fingrphf.1 
 |-  B = ( Base ` G )
2 fingrphf.2 
 |-  ( ph -> G e. Grp )
3 fingrphf.3 
 |-  ( ph -> B e. Fin )
4 ficardid 
 |-  ( B e. Fin -> ( card ` B ) ~~ B )
5 4 ensymd 
 |-  ( B e. Fin -> B ~~ ( card ` B ) )
6 bren 
 |-  ( B ~~ ( card ` B ) <-> E. f f : B -1-1-onto-> ( card ` B ) )
7 5 6 sylib 
 |-  ( B e. Fin -> E. f f : B -1-1-onto-> ( card ` B ) )
8 3 7 syl 
 |-  ( ph -> E. f f : B -1-1-onto-> ( card ` B ) )
9 breq2 
 |-  ( h = { <. ( Base ` ndx ) , ( Base ` ( f "s G ) ) >. , <. ( +g ` ndx ) , ( +f ` ( f "s G ) ) >. } -> ( G ~=g h <-> G ~=g { <. ( Base ` ndx ) , ( Base ` ( f "s G ) ) >. , <. ( +g ` ndx ) , ( +f ` ( f "s G ) ) >. } ) )
10 eqid 
 |-  ( Base ` ( f "s G ) ) = ( Base ` ( f "s G ) )
11 eqid 
 |-  ( +f ` ( f "s G ) ) = ( +f ` ( f "s G ) )
12 eqid 
 |-  { <. ( Base ` ndx ) , ( Base ` ( f "s G ) ) >. , <. ( +g ` ndx ) , ( +f ` ( f "s G ) ) >. } = { <. ( Base ` ndx ) , ( Base ` ( f "s G ) ) >. , <. ( +g ` ndx ) , ( +f ` ( f "s G ) ) >. }
13 eqidd 
 |-  ( ( G e. Grp /\ f : B -1-1-onto-> ( card ` B ) ) -> ( f "s G ) = ( f "s G ) )
14 1 a1i 
 |-  ( ( G e. Grp /\ f : B -1-1-onto-> ( card ` B ) ) -> B = ( Base ` G ) )
15 simpr 
 |-  ( ( G e. Grp /\ f : B -1-1-onto-> ( card ` B ) ) -> f : B -1-1-onto-> ( card ` B ) )
16 simpl 
 |-  ( ( G e. Grp /\ f : B -1-1-onto-> ( card ` B ) ) -> G e. Grp )
17 fvex 
 |-  ( card ` B ) e. _V
18 13 14 15 16 17 imasgimw 
 |-  ( ( G e. Grp /\ f : B -1-1-onto-> ( card ` B ) ) -> f e. ( G GrpIso ( f "s G ) ) )
19 gimghm 
 |-  ( f e. ( G GrpIso ( f "s G ) ) -> f e. ( G GrpHom ( f "s G ) ) )
20 ghmgrp2 
 |-  ( f e. ( G GrpHom ( f "s G ) ) -> ( f "s G ) e. Grp )
21 18 19 20 3syl 
 |-  ( ( G e. Grp /\ f : B -1-1-onto-> ( card ` B ) ) -> ( f "s G ) e. Grp )
22 2 21 sylan 
 |-  ( ( ph /\ f : B -1-1-onto-> ( card ` B ) ) -> ( f "s G ) e. Grp )
23 eqidd 
 |-  ( ( ph /\ f : B -1-1-onto-> ( card ` B ) ) -> ( f "s G ) = ( f "s G ) )
24 1 a1i 
 |-  ( ( ph /\ f : B -1-1-onto-> ( card ` B ) ) -> B = ( Base ` G ) )
25 f1ofo 
 |-  ( f : B -1-1-onto-> ( card ` B ) -> f : B -onto-> ( card ` B ) )
26 25 adantl 
 |-  ( ( ph /\ f : B -1-1-onto-> ( card ` B ) ) -> f : B -onto-> ( card ` B ) )
27 2 adantr 
 |-  ( ( ph /\ f : B -1-1-onto-> ( card ` B ) ) -> G e. Grp )
28 23 24 26 27 imasbas 
 |-  ( ( ph /\ f : B -1-1-onto-> ( card ` B ) ) -> ( card ` B ) = ( Base ` ( f "s G ) ) )
29 ficardom 
 |-  ( B e. Fin -> ( card ` B ) e. _om )
30 omhf 
 |-  ( ( card ` B ) e. _om -> ( card ` B ) e. HF )
31 3 29 30 3syl 
 |-  ( ph -> ( card ` B ) e. HF )
32 31 adantr 
 |-  ( ( ph /\ f : B -1-1-onto-> ( card ` B ) ) -> ( card ` B ) e. HF )
33 28 32 eqeltrrd 
 |-  ( ( ph /\ f : B -1-1-onto-> ( card ` B ) ) -> ( Base ` ( f "s G ) ) e. HF )
34 10 11 12 22 33 grpcanonhfstruct 
 |-  ( ( ph /\ f : B -1-1-onto-> ( card ` B ) ) -> { <. ( Base ` ndx ) , ( Base ` ( f "s G ) ) >. , <. ( +g ` ndx ) , ( +f ` ( f "s G ) ) >. } e. HFStruct )
35 10 11 12 grpgimcanon 
 |-  ( ( f "s G ) e. Grp -> ( _I |` ( Base ` ( f "s G ) ) ) e. ( ( f "s G ) GrpIso { <. ( Base ` ndx ) , ( Base ` ( f "s G ) ) >. , <. ( +g ` ndx ) , ( +f ` ( f "s G ) ) >. } ) )
36 21 35 syl 
 |-  ( ( G e. Grp /\ f : B -1-1-onto-> ( card ` B ) ) -> ( _I |` ( Base ` ( f "s G ) ) ) e. ( ( f "s G ) GrpIso { <. ( Base ` ndx ) , ( Base ` ( f "s G ) ) >. , <. ( +g ` ndx ) , ( +f ` ( f "s G ) ) >. } ) )
37 gimco 
 |-  ( ( ( _I |` ( Base ` ( f "s G ) ) ) e. ( ( f "s G ) GrpIso { <. ( Base ` ndx ) , ( Base ` ( f "s G ) ) >. , <. ( +g ` ndx ) , ( +f ` ( f "s G ) ) >. } ) /\ f e. ( G GrpIso ( f "s G ) ) ) -> ( ( _I |` ( Base ` ( f "s G ) ) ) o. f ) e. ( G GrpIso { <. ( Base ` ndx ) , ( Base ` ( f "s G ) ) >. , <. ( +g ` ndx ) , ( +f ` ( f "s G ) ) >. } ) )
38 36 18 37 syl2anc 
 |-  ( ( G e. Grp /\ f : B -1-1-onto-> ( card ` B ) ) -> ( ( _I |` ( Base ` ( f "s G ) ) ) o. f ) e. ( G GrpIso { <. ( Base ` ndx ) , ( Base ` ( f "s G ) ) >. , <. ( +g ` ndx ) , ( +f ` ( f "s G ) ) >. } ) )
39 brgici 
 |-  ( ( ( _I |` ( Base ` ( f "s G ) ) ) o. f ) e. ( G GrpIso { <. ( Base ` ndx ) , ( Base ` ( f "s G ) ) >. , <. ( +g ` ndx ) , ( +f ` ( f "s G ) ) >. } ) -> G ~=g { <. ( Base ` ndx ) , ( Base ` ( f "s G ) ) >. , <. ( +g ` ndx ) , ( +f ` ( f "s G ) ) >. } )
40 38 39 syl 
 |-  ( ( G e. Grp /\ f : B -1-1-onto-> ( card ` B ) ) -> G ~=g { <. ( Base ` ndx ) , ( Base ` ( f "s G ) ) >. , <. ( +g ` ndx ) , ( +f ` ( f "s G ) ) >. } )
41 2 40 sylan 
 |-  ( ( ph /\ f : B -1-1-onto-> ( card ` B ) ) -> G ~=g { <. ( Base ` ndx ) , ( Base ` ( f "s G ) ) >. , <. ( +g ` ndx ) , ( +f ` ( f "s G ) ) >. } )
42 9 34 41 rspcedvdw 
 |-  ( ( ph /\ f : B -1-1-onto-> ( card ` B ) ) -> E. h e. HFStruct G ~=g h )
43 8 42 exlimddv 
 |-  ( ph -> E. h e. HFStruct G ~=g h )