Theorem hfstructhf

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

	Ref	Expression
Assertion	hfstructhf	Could not format assertion : No typesetting found for |- ( F e. HFStruct -> ( F o. ( # |` _om ) ) e. HF ) with typecode |-

Proof

Step	Hyp	Ref	Expression
1		dmco	$$⊢\mathrm{dom}\left(F\circ \left({\left|.\right|\upharpoonright }_{\mathrm{\omega }}\right)\right)={\left({\left|.\right|\upharpoonright }_{\mathrm{\omega }}\right)}^{-1}\left[\mathrm{dom}F\right]$$
2		hashomf1o	$$⊢\left({\left|.\right|\upharpoonright }_{\mathrm{\omega }}\right):\mathrm{\omega }\underset{1-1\; onto}{⟶}{\mathbb{N}}_0$$
3		dff1o3	$$⊢\left({\left|.\right|\upharpoonright }_{\mathrm{\omega }}\right):\mathrm{\omega }\underset{1-1\; onto}{⟶}{\mathbb{N}}_0\leftrightarrow \left(\left({\left|.\right|\upharpoonright }_{\mathrm{\omega }}\right):\mathrm{\omega }\underset{onto}{⟶}{\mathbb{N}}_0\wedge \mathrm{Fun}{\left({\left|.\right|\upharpoonright }_{\mathrm{\omega }}\right)}^{-1}\right)$$
4	2 3	mpbi	$$⊢\left(\left({\left|.\right|\upharpoonright }_{\mathrm{\omega }}\right):\mathrm{\omega }\underset{onto}{⟶}{\mathbb{N}}_0\wedge \mathrm{Fun}{\left({\left|.\right|\upharpoonright }_{\mathrm{\omega }}\right)}^{-1}\right)$$
5	4	simpri	$$⊢\mathrm{Fun}{\left({\left|.\right|\upharpoonright }_{\mathrm{\omega }}\right)}^{-1}$$
6		hfstructstruct	Could not format ( F e. HFStruct -> E. x F Struct x ) : No typesetting found for |- ( F e. HFStruct -> E. x F Struct x ) with typecode |-
7		dmstructfi	$$⊢F\mathrm{Struct}x\to \mathrm{dom}F\in \mathrm{Fin}$$
8	7	exlimiv	$$⊢\exists xF\mathrm{Struct}x\to \mathrm{dom}F\in \mathrm{Fin}$$
9	6 8	syl	Could not format ( F e. HFStruct -> dom F e. Fin ) : No typesetting found for |- ( F e. HFStruct -> dom F e. Fin ) with typecode |-
10		imafi	$$⊢\left(\mathrm{Fun}{\left({\left|.\right|\upharpoonright }_{\mathrm{\omega }}\right)}^{-1}\wedge \mathrm{dom}F\in \mathrm{Fin}\right)\to {\left({\left|.\right|\upharpoonright }_{\mathrm{\omega }}\right)}^{-1}\left[\mathrm{dom}F\right]\in \mathrm{Fin}$$
11	5 9 10	sylancr	Could not format ( F e. HFStruct -> ( `' ( # |` _om ) " dom F ) e. Fin ) : No typesetting found for |- ( F e. HFStruct -> ( `' ( # |` _om ) " dom F ) e. Fin ) with typecode |-
12	1 11	eqeltrid	Could not format ( F e. HFStruct -> dom ( F o. ( # |` _om ) ) e. Fin ) : No typesetting found for |- ( F e. HFStruct -> dom ( F o. ( # |` _om ) ) e. Fin ) with typecode |-
13		dmcoss	$$⊢\mathrm{dom}\left(F\circ \left({\left|.\right|\upharpoonright }_{\mathrm{\omega }}\right)\right)\subseteq \mathrm{dom}\left({\left|.\right|\upharpoonright }_{\mathrm{\omega }}\right)$$
14		dmhashres	$$⊢\mathrm{dom}\left({\left|.\right|\upharpoonright }_{\mathrm{\omega }}\right)=\mathrm{\omega }$$
15	13 14	sseqtri	$$⊢\mathrm{dom}\left(F\circ \left({\left|.\right|\upharpoonright }_{\mathrm{\omega }}\right)\right)\subseteq \mathrm{\omega }$$
16		omsshf	Could not format _om C_ HF : No typesetting found for |- _om C_ HF with typecode |-
17	15 16	sstri	Could not format dom ( F o. ( # |` _om ) ) C_ HF : No typesetting found for |- dom ( F o. ( # |` _om ) ) C_ HF with typecode |-
18		elhf3	Could not format ( dom ( F o. ( # |` _om ) ) e. HF <-> ( dom ( F o. ( # |` _om ) ) e. Fin /\ dom ( F o. ( # |` _om ) ) C_ HF ) ) : No typesetting found for |- ( dom ( F o. ( # |` _om ) ) e. HF <-> ( dom ( F o. ( # |` _om ) ) e. Fin /\ dom ( F o. ( # |` _om ) ) C_ HF ) ) with typecode |-
19	12 17 18	sylanblrc	Could not format ( F e. HFStruct -> dom ( F o. ( # |` _om ) ) e. HF ) : No typesetting found for |- ( F e. HFStruct -> dom ( F o. ( # |` _om ) ) e. HF ) with typecode |-
20		rncoss	$$⊢\mathrm{ran}\left(F\circ \left({\left|.\right|\upharpoonright }_{\mathrm{\omega }}\right)\right)\subseteq \mathrm{ran}F$$
21		rnhfstructhf	Could not format ( F e. HFStruct -> ran F e. HF ) : No typesetting found for |- ( F e. HFStruct -> ran F e. HF ) with typecode |-
22		hfsshf	Could not format ( ( ran ( F o. ( # |` _om ) ) C_ ran F /\ ran F e. HF ) -> ran ( F o. ( # |` _om ) ) e. HF ) : No typesetting found for |- ( ( ran ( F o. ( # |` _om ) ) C_ ran F /\ ran F e. HF ) -> ran ( F o. ( # |` _om ) ) e. HF ) with typecode |-
23	20 21 22	sylancr	Could not format ( F e. HFStruct -> ran ( F o. ( # |` _om ) ) e. HF ) : No typesetting found for |- ( F e. HFStruct -> ran ( F o. ( # |` _om ) ) e. HF ) with typecode |-
24		relco	$$⊢\mathrm{Rel}\left(F\circ \left({\left|.\right|\upharpoonright }_{\mathrm{\omega }}\right)\right)$$
25		hfrel	Could not format ( Rel ( F o. ( # |` _om ) ) -> ( ( F o. ( # |` _om ) ) e. HF <-> ( dom ( F o. ( # |` _om ) ) e. HF /\ ran ( F o. ( # |` _om ) ) e. HF ) ) ) : No typesetting found for |- ( Rel ( F o. ( # |` _om ) ) -> ( ( F o. ( # |` _om ) ) e. HF <-> ( dom ( F o. ( # |` _om ) ) e. HF /\ ran ( F o. ( # |` _om ) ) e. HF ) ) ) with typecode |-
26	24 25	ax-mp	Could not format ( ( F o. ( # |` _om ) ) e. HF <-> ( dom ( F o. ( # |` _om ) ) e. HF /\ ran ( F o. ( # |` _om ) ) e. HF ) ) : No typesetting found for |- ( ( F o. ( # |` _om ) ) e. HF <-> ( dom ( F o. ( # |` _om ) ) e. HF /\ ran ( F o. ( # |` _om ) ) e. HF ) ) with typecode |-
27	19 23 26	sylanbrc	Could not format ( F e. HFStruct -> ( F o. ( # |` _om ) ) e. HF ) : No typesetting found for |- ( F e. HFStruct -> ( F o. ( # |` _om ) ) e. HF ) with typecode |-