Metamath Proof Explorer

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 = ( Base ` G )
grpcanonhfstruct.2 
|- .+^ = ( +f ` G )
grpcanonhfstruct.3 
|- H = { <. ( Base ` ndx ) , B >. , <. ( +g ` ndx ) , .+^ >. }
grpcanonhfstruct.4 
|- ( ph -> G e. Grp )
grpcanonhfstruct.5 
|- ( ph -> B e. HF )
Assertion grpcanonhfstruct 
|- ( ph -> H e. HFStruct )

Proof

Step Hyp Ref Expression
1 grpcanonhfstruct.1 
 |-  B = ( Base ` G )
2 grpcanonhfstruct.2 
 |-  .+^ = ( +f ` G )
3 grpcanonhfstruct.3 
 |-  H = { <. ( Base ` ndx ) , B >. , <. ( +g ` ndx ) , .+^ >. }
4 grpcanonhfstruct.4 
 |-  ( ph -> G e. Grp )
5 grpcanonhfstruct.5 
 |-  ( ph -> B e. HF )
6 3 grpstr 
 |-  H Struct <. ( Base ` ndx ) , ( +g ` ndx ) >.
7 1 2 grpplusf 
 |-  ( G e. Grp -> .+^ : ( B X. B ) --> B )
8 fssxp 
 |-  ( .+^ : ( B X. B ) --> B -> .+^ C_ ( ( B X. B ) X. B ) )
9 4 7 8 3syl 
 |-  ( ph -> .+^ C_ ( ( B X. B ) X. B ) )
10 hfxp 
 |-  ( ( B e. HF /\ B e. HF ) -> ( B X. B ) e. HF )
11 5 5 10 syl2anc 
 |-  ( ph -> ( B X. B ) e. HF )
12 hfxp 
 |-  ( ( ( B X. B ) e. HF /\ B e. HF ) -> ( ( B X. B ) X. B ) e. HF )
13 11 5 12 syl2anc 
 |-  ( ph -> ( ( B X. B ) X. B ) e. HF )
14 hfsshf 
 |-  ( ( .+^ C_ ( ( B X. B ) X. B ) /\ ( ( B X. B ) X. B ) e. HF ) -> .+^ e. HF )
15 9 13 14 syl2anc 
 |-  ( ph -> .+^ e. HF )
16 fvex 
 |-  ( +g ` ndx ) e. _V
17 fvex 
 |-  ( Base ` ndx ) e. _V
18 relpropg 
 |-  ( ( ( ( Base ` ndx ) e. _V /\ B e. HF ) /\ ( ( +g ` ndx ) e. _V /\ .+^ e. HF ) ) -> Rel { <. ( Base ` ndx ) , B >. , <. ( +g ` ndx ) , .+^ >. } )
19 17 18 mpanl1 
 |-  ( ( B e. HF /\ ( ( +g ` ndx ) e. _V /\ .+^ e. HF ) ) -> Rel { <. ( Base ` ndx ) , B >. , <. ( +g ` ndx ) , .+^ >. } )
20 16 19 mpanr1 
 |-  ( ( B e. HF /\ .+^ e. HF ) -> Rel { <. ( Base ` ndx ) , B >. , <. ( +g ` ndx ) , .+^ >. } )
21 5 15 20 syl2anc 
 |-  ( ph -> Rel { <. ( Base ` ndx ) , B >. , <. ( +g ` ndx ) , .+^ >. } )
22 3 releqi 
 |-  ( Rel H <-> Rel { <. ( Base ` ndx ) , B >. , <. ( +g ` ndx ) , .+^ >. } )
23 21 22 sylibr 
 |-  ( ph -> Rel H )
24 3 rneqi 
 |-  ran H = ran { <. ( Base ` ndx ) , B >. , <. ( +g ` ndx ) , .+^ >. }
25 rnpropg 
 |-  ( ( ( Base ` ndx ) e. _V /\ ( +g ` ndx ) e. _V ) -> ran { <. ( Base ` ndx ) , B >. , <. ( +g ` ndx ) , .+^ >. } = { B , .+^ } )
26 17 16 25 mp2an 
 |-  ran { <. ( Base ` ndx ) , B >. , <. ( +g ` ndx ) , .+^ >. } = { B , .+^ }
27 24 26 eqtri 
 |-  ran H = { B , .+^ }
28 5 15 prssd 
 |-  ( ph -> { B , .+^ } C_ HF )
29 27 28 eqsstrid 
 |-  ( ph -> ran H C_ HF )
30 ishfstruct 
 |-  ( ( H Struct <. ( Base ` ndx ) , ( +g ` ndx ) >. /\ Rel H /\ ran H C_ HF ) -> H e. HFStruct )
31 6 23 29 30 mp3an2i 
 |-  ( ph -> H e. HFStruct )