Theorem grpcanonhfstruct

Description: A group defined on a hereditarily finite set is an HFStruct. (Contributed by Eric Schmidt, 24-Oct-2026)

	Ref	Expression
Hypotheses	grpcanonhfstruct.1	$$⊢B={\mathrm{Base}}_G$$
	grpcanonhfstruct.2	$$⊢\underset{\dot{}}{⨣}={+}_{𝑓}\left(G\right)$$
	grpcanonhfstruct.3	$$⊢H=\left\{⟨{\mathrm{Base}}_{\mathrm{ndx}},B⟩,⟨{+}_{\mathrm{ndx}},\underset{\dot{}}{⨣}⟩\right\}$$
	grpcanonhfstruct.4	$$⊢\phi \to G\in \mathrm{Grp}$$
	grpcanonhfstruct.5	No typesetting found for |- ( ph -> B e. HF ) with typecode |-
Assertion	grpcanonhfstruct	Could not format assertion : No typesetting found for |- ( ph -> H e. HFStruct ) with typecode |-

Proof

Step	Hyp	Ref	Expression
1		grpcanonhfstruct.1	$$⊢B={\mathrm{Base}}_G$$
2		grpcanonhfstruct.2	$$⊢\underset{\dot{}}{⨣}={+}_{𝑓}\left(G\right)$$
3		grpcanonhfstruct.3	$$⊢H=\left\{⟨{\mathrm{Base}}_{\mathrm{ndx}},B⟩,⟨{+}_{\mathrm{ndx}},\underset{\dot{}}{⨣}⟩\right\}$$
4		grpcanonhfstruct.4	$$⊢\phi \to G\in \mathrm{Grp}$$
5		grpcanonhfstruct.5	Could not format ( ph -> B e. HF ) : No typesetting found for |- ( ph -> B e. HF ) with typecode |-
6	3	grpstr	$$⊢H\mathrm{Struct}⟨{\mathrm{Base}}_{\mathrm{ndx}},{+}_{\mathrm{ndx}}⟩$$
7	1 2	grpplusf	$$⊢G\in \mathrm{Grp}\to \underset{\dot{}}{⨣}:B\times B⟶B$$
8		fssxp	$$⊢\underset{\dot{}}{⨣}:B\times B⟶B\to \underset{\dot{}}{⨣}\subseteq \left(B\times B\right)\times B$$
9	4 7 8	3syl	$$⊢\phi \to \underset{\dot{}}{⨣}\subseteq \left(B\times B\right)\times B$$
10		hfxp	Could not format ( ( B e. HF /\ B e. HF ) -> ( B X. B ) e. HF ) : No typesetting found for |- ( ( B e. HF /\ B e. HF ) -> ( B X. B ) e. HF ) with typecode |-
11	5 5 10	syl2anc	Could not format ( ph -> ( B X. B ) e. HF ) : No typesetting found for |- ( ph -> ( B X. B ) e. HF ) with typecode |-
12		hfxp	Could not format ( ( ( B X. B ) e. HF /\ B e. HF ) -> ( ( B X. B ) X. B ) e. HF ) : No typesetting found for |- ( ( ( B X. B ) e. HF /\ B e. HF ) -> ( ( B X. B ) X. B ) e. HF ) with typecode |-
13	11 5 12	syl2anc	Could not format ( ph -> ( ( B X. B ) X. B ) e. HF ) : No typesetting found for |- ( ph -> ( ( B X. B ) X. B ) e. HF ) with typecode |-
14		hfsshf	Could not format ( ( .+^ C_ ( ( B X. B ) X. B ) /\ ( ( B X. B ) X. B ) e. HF ) -> .+^ e. HF ) : No typesetting found for |- ( ( .+^ C_ ( ( B X. B ) X. B ) /\ ( ( B X. B ) X. B ) e. HF ) -> .+^ e. HF ) with typecode |-
15	9 13 14	syl2anc	Could not format ( ph -> .+^ e. HF ) : No typesetting found for |- ( ph -> .+^ e. HF ) with typecode |-
16		fvex	$$⊢{+}_{\mathrm{ndx}}\in \mathrm{V}$$
17		fvex	$$⊢{\mathrm{Base}}_{\mathrm{ndx}}\in \mathrm{V}$$
18		relpropg	Could not format ( ( ( ( Base ` ndx ) e. _V /\ B e. HF ) /\ ( ( +g ` ndx ) e. _V /\ .+^ e. HF ) ) -> Rel { <. ( Base ` ndx ) , B >. , <. ( +g ` ndx ) , .+^ >. } ) : No typesetting found for |- ( ( ( ( Base ` ndx ) e. _V /\ B e. HF ) /\ ( ( +g ` ndx ) e. _V /\ .+^ e. HF ) ) -> Rel { <. ( Base ` ndx ) , B >. , <. ( +g ` ndx ) , .+^ >. } ) with typecode |-
19	17 18	mpanl1	Could not format ( ( B e. HF /\ ( ( +g ` ndx ) e. _V /\ .+^ e. HF ) ) -> Rel { <. ( Base ` ndx ) , B >. , <. ( +g ` ndx ) , .+^ >. } ) : No typesetting found for |- ( ( B e. HF /\ ( ( +g ` ndx ) e. _V /\ .+^ e. HF ) ) -> Rel { <. ( Base ` ndx ) , B >. , <. ( +g ` ndx ) , .+^ >. } ) with typecode |-
20	16 19	mpanr1	Could not format ( ( B e. HF /\ .+^ e. HF ) -> Rel { <. ( Base ` ndx ) , B >. , <. ( +g ` ndx ) , .+^ >. } ) : No typesetting found for |- ( ( B e. HF /\ .+^ e. HF ) -> Rel { <. ( Base ` ndx ) , B >. , <. ( +g ` ndx ) , .+^ >. } ) with typecode |-
21	5 15 20	syl2anc	$$⊢\phi \to \mathrm{Rel}\left\{⟨{\mathrm{Base}}_{\mathrm{ndx}},B⟩,⟨{+}_{\mathrm{ndx}},\underset{\dot{}}{⨣}⟩\right\}$$
22	3	releqi	$$⊢\mathrm{Rel}H\leftrightarrow \mathrm{Rel}\left\{⟨{\mathrm{Base}}_{\mathrm{ndx}},B⟩,⟨{+}_{\mathrm{ndx}},\underset{\dot{}}{⨣}⟩\right\}$$
23	21 22	sylibr	$$⊢\phi \to \mathrm{Rel}H$$
24	3	rneqi	$$⊢\mathrm{ran}H=\mathrm{ran}\left\{⟨{\mathrm{Base}}_{\mathrm{ndx}},B⟩,⟨{+}_{\mathrm{ndx}},\underset{\dot{}}{⨣}⟩\right\}$$
25		rnpropg	$$⊢\left({\mathrm{Base}}_{\mathrm{ndx}}\in \mathrm{V}\wedge {+}_{\mathrm{ndx}}\in \mathrm{V}\right)\to \mathrm{ran}\left\{⟨{\mathrm{Base}}_{\mathrm{ndx}},B⟩,⟨{+}_{\mathrm{ndx}},\underset{\dot{}}{⨣}⟩\right\}=\left\{B,\underset{\dot{}}{⨣}\right\}$$
26	17 16 25	mp2an	$$⊢\mathrm{ran}\left\{⟨{\mathrm{Base}}_{\mathrm{ndx}},B⟩,⟨{+}_{\mathrm{ndx}},\underset{\dot{}}{⨣}⟩\right\}=\left\{B,\underset{\dot{}}{⨣}\right\}$$
27	24 26	eqtri	$$⊢\mathrm{ran}H=\left\{B,\underset{\dot{}}{⨣}\right\}$$
28	5 15	prssd	Could not format ( ph -> { B , .+^ } C_ HF ) : No typesetting found for |- ( ph -> { B , .+^ } C_ HF ) with typecode |-
29	27 28	eqsstrid	Could not format ( ph -> ran H C_ HF ) : No typesetting found for |- ( ph -> ran H C_ HF ) with typecode |-
30		ishfstruct	Could not format ( ( H Struct <. ( Base ` ndx ) , ( +g ` ndx ) >. /\ Rel H /\ ran H C_ HF ) -> H e. HFStruct ) : No typesetting found for |- ( ( H Struct <. ( Base ` ndx ) , ( +g ` ndx ) >. /\ Rel H /\ ran H C_ HF ) -> H e. HFStruct ) with typecode |-
31	6 23 29 30	mp3an2i	Could not format ( ph -> H e. HFStruct ) : No typesetting found for |- ( ph -> H e. HFStruct ) with typecode |-