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={\mathrm{Base}}_G$$
	fingrphf.2	$$⊢\phi \to G\in \mathrm{Grp}$$
	fingrphf.3	$$⊢\phi \to B\in \mathrm{Fin}$$
Assertion	fingrphf	Could not format assertion : No typesetting found for |- ( ph -> E. h e. HFStruct G ~=g h ) with typecode |-

Proof

Step	Hyp	Ref	Expression
1		fingrphf.1	$$⊢B={\mathrm{Base}}_G$$
2		fingrphf.2	$$⊢\phi \to G\in \mathrm{Grp}$$
3		fingrphf.3	$$⊢\phi \to B\in \mathrm{Fin}$$
4		ficardid	$$⊢B\in \mathrm{Fin}\to \mathrm{card}\left(B\right)\approx B$$
5	4	ensymd	$$⊢B\in \mathrm{Fin}\to B\approx \mathrm{card}\left(B\right)$$
6		bren	$$⊢B\approx \mathrm{card}\left(B\right)\leftrightarrow \exists ff:B\underset{1-1\; onto}{⟶}\mathrm{card}\left(B\right)$$
7	5 6	sylib	$$⊢B\in \mathrm{Fin}\to \exists ff:B\underset{1-1\; onto}{⟶}\mathrm{card}\left(B\right)$$
8	3 7	syl	$$⊢\phi \to \exists ff:B\underset{1-1\; onto}{⟶}\mathrm{card}\left(B\right)$$
9		breq2	$$⊢h=\left\{⟨{\mathrm{Base}}_{\mathrm{ndx}},{\mathrm{Base}}_{\left(f{“}_{𝑠}G\right)}⟩,⟨{+}_{\mathrm{ndx}},{+}_{𝑓}\left(f{“}_{𝑠}G\right)⟩\right\}\to \left(G{\simeq }_{𝑔}h\leftrightarrow G{\simeq }_{𝑔}\left\{⟨{\mathrm{Base}}_{\mathrm{ndx}},{\mathrm{Base}}_{\left(f{“}_{𝑠}G\right)}⟩,⟨{+}_{\mathrm{ndx}},{+}_{𝑓}\left(f{“}_{𝑠}G\right)⟩\right\}\right)$$
10		eqid	$$⊢{\mathrm{Base}}_{\left(f{“}_{𝑠}G\right)}={\mathrm{Base}}_{\left(f{“}_{𝑠}G\right)}$$
11		eqid	$$⊢{+}_{𝑓}\left(f{“}_{𝑠}G\right)={+}_{𝑓}\left(f{“}_{𝑠}G\right)$$
12		eqid	$$⊢\left\{⟨{\mathrm{Base}}_{\mathrm{ndx}},{\mathrm{Base}}_{\left(f{“}_{𝑠}G\right)}⟩,⟨{+}_{\mathrm{ndx}},{+}_{𝑓}\left(f{“}_{𝑠}G\right)⟩\right\}=\left\{⟨{\mathrm{Base}}_{\mathrm{ndx}},{\mathrm{Base}}_{\left(f{“}_{𝑠}G\right)}⟩,⟨{+}_{\mathrm{ndx}},{+}_{𝑓}\left(f{“}_{𝑠}G\right)⟩\right\}$$
13		eqidd	$$⊢\left(G\in \mathrm{Grp}\wedge f:B\underset{1-1\; onto}{⟶}\mathrm{card}\left(B\right)\right)\to f{“}_{𝑠}G=f{“}_{𝑠}G$$
14	1	a1i	$$⊢\left(G\in \mathrm{Grp}\wedge f:B\underset{1-1\; onto}{⟶}\mathrm{card}\left(B\right)\right)\to B={\mathrm{Base}}_G$$
15		simpr	$$⊢\left(G\in \mathrm{Grp}\wedge f:B\underset{1-1\; onto}{⟶}\mathrm{card}\left(B\right)\right)\to f:B\underset{1-1\; onto}{⟶}\mathrm{card}\left(B\right)$$
16		simpl	$$⊢\left(G\in \mathrm{Grp}\wedge f:B\underset{1-1\; onto}{⟶}\mathrm{card}\left(B\right)\right)\to G\in \mathrm{Grp}$$
17		fvex	$$⊢\mathrm{card}\left(B\right)\in \mathrm{V}$$
18	13 14 15 16 17	imasgimw	$$⊢\left(G\in \mathrm{Grp}\wedge f:B\underset{1-1\; onto}{⟶}\mathrm{card}\left(B\right)\right)\to f\in \left(G\mathrm{GrpIso}\left(f{“}_{𝑠}G\right)\right)$$
19		gimghm	$$⊢f\in \left(G\mathrm{GrpIso}\left(f{“}_{𝑠}G\right)\right)\to f\in \left(G\mathrm{GrpHom}\left(f{“}_{𝑠}G\right)\right)$$
20		ghmgrp2	$$⊢f\in \left(G\mathrm{GrpHom}\left(f{“}_{𝑠}G\right)\right)\to f{“}_{𝑠}G\in \mathrm{Grp}$$
21	18 19 20	3syl	$$⊢\left(G\in \mathrm{Grp}\wedge f:B\underset{1-1\; onto}{⟶}\mathrm{card}\left(B\right)\right)\to f{“}_{𝑠}G\in \mathrm{Grp}$$
22	2 21	sylan	$$⊢\left(\phi \wedge f:B\underset{1-1\; onto}{⟶}\mathrm{card}\left(B\right)\right)\to f{“}_{𝑠}G\in \mathrm{Grp}$$
23		eqidd	$$⊢\left(\phi \wedge f:B\underset{1-1\; onto}{⟶}\mathrm{card}\left(B\right)\right)\to f{“}_{𝑠}G=f{“}_{𝑠}G$$
24	1	a1i	$$⊢\left(\phi \wedge f:B\underset{1-1\; onto}{⟶}\mathrm{card}\left(B\right)\right)\to B={\mathrm{Base}}_G$$
25		f1ofo	$$⊢f:B\underset{1-1\; onto}{⟶}\mathrm{card}\left(B\right)\to f:B\underset{onto}{⟶}\mathrm{card}\left(B\right)$$
26	25	adantl	$$⊢\left(\phi \wedge f:B\underset{1-1\; onto}{⟶}\mathrm{card}\left(B\right)\right)\to f:B\underset{onto}{⟶}\mathrm{card}\left(B\right)$$
27	2	adantr	$$⊢\left(\phi \wedge f:B\underset{1-1\; onto}{⟶}\mathrm{card}\left(B\right)\right)\to G\in \mathrm{Grp}$$
28	23 24 26 27	imasbas	$$⊢\left(\phi \wedge f:B\underset{1-1\; onto}{⟶}\mathrm{card}\left(B\right)\right)\to \mathrm{card}\left(B\right)={\mathrm{Base}}_{\left(f{“}_{𝑠}G\right)}$$
29		ficardom	$$⊢B\in \mathrm{Fin}\to \mathrm{card}\left(B\right)\in \mathrm{\omega }$$
30		omhf	Could not format ( ( card ` B ) e. _om -> ( card ` B ) e. HF ) : No typesetting found for |- ( ( card ` B ) e. _om -> ( card ` B ) e. HF ) with typecode |-
31	3 29 30	3syl	Could not format ( ph -> ( card ` B ) e. HF ) : No typesetting found for |- ( ph -> ( card ` B ) e. HF ) with typecode |-
32	31	adantr	Could not format ( ( ph /\ f : B -1-1-onto-> ( card ` B ) ) -> ( card ` B ) e. HF ) : No typesetting found for |- ( ( ph /\ f : B -1-1-onto-> ( card ` B ) ) -> ( card ` B ) e. HF ) with typecode |-
33	28 32	eqeltrrd	Could not format ( ( ph /\ f : B -1-1-onto-> ( card ` B ) ) -> ( Base ` ( f "s G ) ) e. HF ) : No typesetting found for |- ( ( ph /\ f : B -1-1-onto-> ( card ` B ) ) -> ( Base ` ( f "s G ) ) e. HF ) with typecode |-
34	10 11 12 22 33	grpcanonhfstruct	Could not format ( ( ph /\ f : B -1-1-onto-> ( card ` B ) ) -> { <. ( Base ` ndx ) , ( Base ` ( f "s G ) ) >. , <. ( +g ` ndx ) , ( +f ` ( f "s G ) ) >. } e. HFStruct ) : No typesetting found for |- ( ( ph /\ f : B -1-1-onto-> ( card ` B ) ) -> { <. ( Base ` ndx ) , ( Base ` ( f "s G ) ) >. , <. ( +g ` ndx ) , ( +f ` ( f "s G ) ) >. } e. HFStruct ) with typecode |-
35	10 11 12	grpgimcanon	$$⊢f{“}_{𝑠}G\in \mathrm{Grp}\to {\mathrm{I}\upharpoonright }_{{\mathrm{Base}}_{\left(f{“}_{𝑠}G\right)}}\in \left(\left(f{“}_{𝑠}G\right)\mathrm{GrpIso}\left\{⟨{\mathrm{Base}}_{\mathrm{ndx}},{\mathrm{Base}}_{\left(f{“}_{𝑠}G\right)}⟩,⟨{+}_{\mathrm{ndx}},{+}_{𝑓}\left(f{“}_{𝑠}G\right)⟩\right\}\right)$$
36	21 35	syl	$$⊢\left(G\in \mathrm{Grp}\wedge f:B\underset{1-1\; onto}{⟶}\mathrm{card}\left(B\right)\right)\to {\mathrm{I}\upharpoonright }_{{\mathrm{Base}}_{\left(f{“}_{𝑠}G\right)}}\in \left(\left(f{“}_{𝑠}G\right)\mathrm{GrpIso}\left\{⟨{\mathrm{Base}}_{\mathrm{ndx}},{\mathrm{Base}}_{\left(f{“}_{𝑠}G\right)}⟩,⟨{+}_{\mathrm{ndx}},{+}_{𝑓}\left(f{“}_{𝑠}G\right)⟩\right\}\right)$$
37		gimco	$$⊢\left({\mathrm{I}\upharpoonright }_{{\mathrm{Base}}_{\left(f{“}_{𝑠}G\right)}}\in \left(\left(f{“}_{𝑠}G\right)\mathrm{GrpIso}\left\{⟨{\mathrm{Base}}_{\mathrm{ndx}},{\mathrm{Base}}_{\left(f{“}_{𝑠}G\right)}⟩,⟨{+}_{\mathrm{ndx}},{+}_{𝑓}\left(f{“}_{𝑠}G\right)⟩\right\}\right)\wedge f\in \left(G\mathrm{GrpIso}\left(f{“}_{𝑠}G\right)\right)\right)\to \left({\mathrm{I}\upharpoonright }_{{\mathrm{Base}}_{\left(f{“}_{𝑠}G\right)}}\right)\circ f\in \left(G\mathrm{GrpIso}\left\{⟨{\mathrm{Base}}_{\mathrm{ndx}},{\mathrm{Base}}_{\left(f{“}_{𝑠}G\right)}⟩,⟨{+}_{\mathrm{ndx}},{+}_{𝑓}\left(f{“}_{𝑠}G\right)⟩\right\}\right)$$
38	36 18 37	syl2anc	$$⊢\left(G\in \mathrm{Grp}\wedge f:B\underset{1-1\; onto}{⟶}\mathrm{card}\left(B\right)\right)\to \left({\mathrm{I}\upharpoonright }_{{\mathrm{Base}}_{\left(f{“}_{𝑠}G\right)}}\right)\circ f\in \left(G\mathrm{GrpIso}\left\{⟨{\mathrm{Base}}_{\mathrm{ndx}},{\mathrm{Base}}_{\left(f{“}_{𝑠}G\right)}⟩,⟨{+}_{\mathrm{ndx}},{+}_{𝑓}\left(f{“}_{𝑠}G\right)⟩\right\}\right)$$
39		brgici	$$⊢\left({\mathrm{I}\upharpoonright }_{{\mathrm{Base}}_{\left(f{“}_{𝑠}G\right)}}\right)\circ f\in \left(G\mathrm{GrpIso}\left\{⟨{\mathrm{Base}}_{\mathrm{ndx}},{\mathrm{Base}}_{\left(f{“}_{𝑠}G\right)}⟩,⟨{+}_{\mathrm{ndx}},{+}_{𝑓}\left(f{“}_{𝑠}G\right)⟩\right\}\right)\to G{\simeq }_{𝑔}\left\{⟨{\mathrm{Base}}_{\mathrm{ndx}},{\mathrm{Base}}_{\left(f{“}_{𝑠}G\right)}⟩,⟨{+}_{\mathrm{ndx}},{+}_{𝑓}\left(f{“}_{𝑠}G\right)⟩\right\}$$
40	38 39	syl	$$⊢\left(G\in \mathrm{Grp}\wedge f:B\underset{1-1\; onto}{⟶}\mathrm{card}\left(B\right)\right)\to G{\simeq }_{𝑔}\left\{⟨{\mathrm{Base}}_{\mathrm{ndx}},{\mathrm{Base}}_{\left(f{“}_{𝑠}G\right)}⟩,⟨{+}_{\mathrm{ndx}},{+}_{𝑓}\left(f{“}_{𝑠}G\right)⟩\right\}$$
41	2 40	sylan	$$⊢\left(\phi \wedge f:B\underset{1-1\; onto}{⟶}\mathrm{card}\left(B\right)\right)\to G{\simeq }_{𝑔}\left\{⟨{\mathrm{Base}}_{\mathrm{ndx}},{\mathrm{Base}}_{\left(f{“}_{𝑠}G\right)}⟩,⟨{+}_{\mathrm{ndx}},{+}_{𝑓}\left(f{“}_{𝑠}G\right)⟩\right\}$$
42	9 34 41	rspcedvdw	Could not format ( ( ph /\ f : B -1-1-onto-> ( card ` B ) ) -> E. h e. HFStruct G ~=g h ) : No typesetting found for |- ( ( ph /\ f : B -1-1-onto-> ( card ` B ) ) -> E. h e. HFStruct G ~=g h ) with typecode |-
43	8 42	exlimddv	Could not format ( ph -> E. h e. HFStruct G ~=g h ) : No typesetting found for |- ( ph -> E. h e. HFStruct G ~=g h ) with typecode |-