Metamath Proof Explorer

Theorem hfstructhf

Description: A converted HFStruct is a hereditarily finite set. (Contributed by Eric Schmidt, 29-Sep-2026)

Ref Expression
Assertion hfstructhf 
|- ( F e. HFStruct -> ( F o. ( # |` _om ) ) e. HF )

Proof

Step Hyp Ref Expression
1 dmco 
 |-  dom ( F o. ( # |` _om ) ) = ( `' ( # |` _om ) " dom F )
2 hashomf1o 
 |-  ( # |` _om ) : _om -1-1-onto-> NN0
3 dff1o3 
 |-  ( ( # |` _om ) : _om -1-1-onto-> NN0 <-> ( ( # |` _om ) : _om -onto-> NN0 /\ Fun `' ( # |` _om ) ) )
4 2 3 mpbi 
 |-  ( ( # |` _om ) : _om -onto-> NN0 /\ Fun `' ( # |` _om ) )
5 4 simpri 
 |-  Fun `' ( # |` _om )
6 hfstructstruct 
 |-  ( F e. HFStruct -> E. x F Struct x )
7 dmstructfi 
 |-  ( F Struct x -> dom F e. Fin )
8 7 exlimiv 
 |-  ( E. x F Struct x -> dom F e. Fin )
9 6 8 syl 
 |-  ( F e. HFStruct -> dom F e. Fin )
10 imafi 
 |-  ( ( Fun `' ( # |` _om ) /\ dom F e. Fin ) -> ( `' ( # |` _om ) " dom F ) e. Fin )
11 5 9 10 sylancr 
 |-  ( F e. HFStruct -> ( `' ( # |` _om ) " dom F ) e. Fin )
12 1 11 eqeltrid 
 |-  ( F e. HFStruct -> dom ( F o. ( # |` _om ) ) e. Fin )
13 dmcoss 
 |-  dom ( F o. ( # |` _om ) ) C_ dom ( # |` _om )
14 dmhashres 
 |-  dom ( # |` _om ) = _om
15 13 14 sseqtri 
 |-  dom ( F o. ( # |` _om ) ) C_ _om
16 omsshf 
 |-  _om C_ HF
17 15 16 sstri 
 |-  dom ( F o. ( # |` _om ) ) C_ HF
18 elhf3 
 |-  ( dom ( F o. ( # |` _om ) ) e. HF <-> ( dom ( F o. ( # |` _om ) ) e. Fin /\ dom ( F o. ( # |` _om ) ) C_ HF ) )
19 12 17 18 sylanblrc 
 |-  ( F e. HFStruct -> dom ( F o. ( # |` _om ) ) e. HF )
20 rncoss 
 |-  ran ( F o. ( # |` _om ) ) C_ ran F
21 rnhfstructhf 
 |-  ( F e. HFStruct -> ran F e. HF )
22 hfsshf 
 |-  ( ( ran ( F o. ( # |` _om ) ) C_ ran F /\ ran F e. HF ) -> ran ( F o. ( # |` _om ) ) e. HF )
23 20 21 22 sylancr 
 |-  ( F e. HFStruct -> ran ( F o. ( # |` _om ) ) e. HF )
24 relco 
 |-  Rel ( F o. ( # |` _om ) )
25 hfrel 
 |-  ( Rel ( F o. ( # |` _om ) ) -> ( ( F o. ( # |` _om ) ) e. HF <-> ( dom ( F o. ( # |` _om ) ) e. HF /\ ran ( F o. ( # |` _om ) ) e. HF ) ) )
26 24 25 ax-mp 
 |-  ( ( F o. ( # |` _om ) ) e. HF <-> ( dom ( F o. ( # |` _om ) ) e. HF /\ ran ( F o. ( # |` _om ) ) e. HF ) )
27 19 23 26 sylanbrc 
 |-  ( F e. HFStruct -> ( F o. ( # |` _om ) ) e. HF )