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	⊢ 𝐵 = ( Base ‘ 𝐺 )
	grpcanonhfstruct.2	⊢ ⨣ = ( +𝑓 ‘ 𝐺 )
	grpcanonhfstruct.3	⊢ 𝐻 = { ⟨ ( Base ‘ ndx ) , 𝐵 ⟩ , ⟨ ( +g ‘ ndx ) , ⨣ ⟩ }
	grpcanonhfstruct.4	⊢ ( 𝜑 → 𝐺 ∈ Grp )
	grpcanonhfstruct.5	⊢ ( 𝜑 → 𝐵 ∈ HF )
Assertion	grpcanonhfstruct	⊢ ( 𝜑 → 𝐻 ∈ HFStruct )

Proof

Step	Hyp	Ref	Expression
1		grpcanonhfstruct.1	⊢ 𝐵 = ( Base ‘ 𝐺 )
2		grpcanonhfstruct.2	⊢ ⨣ = ( +𝑓 ‘ 𝐺 )
3		grpcanonhfstruct.3	⊢ 𝐻 = { ⟨ ( Base ‘ ndx ) , 𝐵 ⟩ , ⟨ ( +g ‘ ndx ) , ⨣ ⟩ }
4		grpcanonhfstruct.4	⊢ ( 𝜑 → 𝐺 ∈ Grp )
5		grpcanonhfstruct.5	⊢ ( 𝜑 → 𝐵 ∈ HF )
6	3	grpstr	⊢ 𝐻 Struct ⟨ ( Base ‘ ndx ) , ( +g ‘ ndx ) ⟩
7	1 2	grpplusf	⊢ ( 𝐺 ∈ Grp → ⨣ : ( 𝐵 × 𝐵 ) ⟶ 𝐵 )
8		fssxp	⊢ ( ⨣ : ( 𝐵 × 𝐵 ) ⟶ 𝐵 → ⨣ ⊆ ( ( 𝐵 × 𝐵 ) × 𝐵 ) )
9	4 7 8	3syl	⊢ ( 𝜑 → ⨣ ⊆ ( ( 𝐵 × 𝐵 ) × 𝐵 ) )
10		hfxp	⊢ ( ( 𝐵 ∈ HF ∧ 𝐵 ∈ HF ) → ( 𝐵 × 𝐵 ) ∈ HF )
11	5 5 10	syl2anc	⊢ ( 𝜑 → ( 𝐵 × 𝐵 ) ∈ HF )
12		hfxp	⊢ ( ( ( 𝐵 × 𝐵 ) ∈ HF ∧ 𝐵 ∈ HF ) → ( ( 𝐵 × 𝐵 ) × 𝐵 ) ∈ HF )
13	11 5 12	syl2anc	⊢ ( 𝜑 → ( ( 𝐵 × 𝐵 ) × 𝐵 ) ∈ HF )
14		hfsshf	⊢ ( ( ⨣ ⊆ ( ( 𝐵 × 𝐵 ) × 𝐵 ) ∧ ( ( 𝐵 × 𝐵 ) × 𝐵 ) ∈ HF ) → ⨣ ∈ HF )
15	9 13 14	syl2anc	⊢ ( 𝜑 → ⨣ ∈ HF )
16		fvex	⊢ ( +g ‘ ndx ) ∈ V
17		fvex	⊢ ( Base ‘ ndx ) ∈ V
18		relpropg	⊢ ( ( ( ( Base ‘ ndx ) ∈ V ∧ 𝐵 ∈ HF ) ∧ ( ( +g ‘ ndx ) ∈ V ∧ ⨣ ∈ HF ) ) → Rel { ⟨ ( Base ‘ ndx ) , 𝐵 ⟩ , ⟨ ( +g ‘ ndx ) , ⨣ ⟩ } )
19	17 18	mpanl1	⊢ ( ( 𝐵 ∈ HF ∧ ( ( +g ‘ ndx ) ∈ V ∧ ⨣ ∈ HF ) ) → Rel { ⟨ ( Base ‘ ndx ) , 𝐵 ⟩ , ⟨ ( +g ‘ ndx ) , ⨣ ⟩ } )
20	16 19	mpanr1	⊢ ( ( 𝐵 ∈ HF ∧ ⨣ ∈ HF ) → Rel { ⟨ ( Base ‘ ndx ) , 𝐵 ⟩ , ⟨ ( +g ‘ ndx ) , ⨣ ⟩ } )
21	5 15 20	syl2anc	⊢ ( 𝜑 → Rel { ⟨ ( Base ‘ ndx ) , 𝐵 ⟩ , ⟨ ( +g ‘ ndx ) , ⨣ ⟩ } )
22	3	releqi	⊢ ( Rel 𝐻 ↔ Rel { ⟨ ( Base ‘ ndx ) , 𝐵 ⟩ , ⟨ ( +g ‘ ndx ) , ⨣ ⟩ } )
23	21 22	sylibr	⊢ ( 𝜑 → Rel 𝐻 )
24	3	rneqi	⊢ ran 𝐻 = ran { ⟨ ( Base ‘ ndx ) , 𝐵 ⟩ , ⟨ ( +g ‘ ndx ) , ⨣ ⟩ }
25		rnpropg	⊢ ( ( ( Base ‘ ndx ) ∈ V ∧ ( +g ‘ ndx ) ∈ V ) → ran { ⟨ ( Base ‘ ndx ) , 𝐵 ⟩ , ⟨ ( +g ‘ ndx ) , ⨣ ⟩ } = { 𝐵 , ⨣ } )
26	17 16 25	mp2an	⊢ ran { ⟨ ( Base ‘ ndx ) , 𝐵 ⟩ , ⟨ ( +g ‘ ndx ) , ⨣ ⟩ } = { 𝐵 , ⨣ }
27	24 26	eqtri	⊢ ran 𝐻 = { 𝐵 , ⨣ }
28	5 15	prssd	⊢ ( 𝜑 → { 𝐵 , ⨣ } ⊆ HF )
29	27 28	eqsstrid	⊢ ( 𝜑 → ran 𝐻 ⊆ HF )
30		ishfstruct	⊢ ( ( 𝐻 Struct ⟨ ( Base ‘ ndx ) , ( +g ‘ ndx ) ⟩ ∧ Rel 𝐻 ∧ ran 𝐻 ⊆ HF ) → 𝐻 ∈ HFStruct )
31	6 23 29 30	mp3an2i	⊢ ( 𝜑 → 𝐻 ∈ HFStruct )