Theorem hfstructcan

Description: Two HFStructs are equal if and only if their converted forms are equal. (Contributed by Eric Schmidt, 29-Sep-2026)

	Ref	Expression
Assertion	hfstructcan	Could not format assertion : No typesetting found for |- ( ( F e. HFStruct /\ G e. HFStruct ) -> ( ( F o. ( # |` _om ) ) = ( G o. ( # |` _om ) ) <-> F = G ) ) with typecode |-

Proof

Step	Hyp	Ref	Expression
1		hashomf1o	$$⊢\left({\left|.\right|\upharpoonright }_{\mathrm{\omega }}\right):\mathrm{\omega }\underset{1-1\; onto}{⟶}{\mathbb{N}}_0$$
2		f1ofun	$$⊢\left({\left|.\right|\upharpoonright }_{\mathrm{\omega }}\right):\mathrm{\omega }\underset{1-1\; onto}{⟶}{\mathbb{N}}_0\to \mathrm{Fun}\left({\left|.\right|\upharpoonright }_{\mathrm{\omega }}\right)$$
3	1 2	mp1i	Could not format ( ( F e. HFStruct /\ G e. HFStruct ) -> Fun ( # |` _om ) ) : No typesetting found for |- ( ( F e. HFStruct /\ G e. HFStruct ) -> Fun ( # |` _om ) ) with typecode |-
4		hfstructfun	Could not format ( F e. HFStruct -> Fun F ) : No typesetting found for |- ( F e. HFStruct -> Fun F ) with typecode |-
5		funrel	$$⊢\mathrm{Fun}F\to \mathrm{Rel}F$$
6	4 5	syl	Could not format ( F e. HFStruct -> Rel F ) : No typesetting found for |- ( F e. HFStruct -> Rel F ) with typecode |-
7	6	adantr	Could not format ( ( F e. HFStruct /\ G e. HFStruct ) -> Rel F ) : No typesetting found for |- ( ( F e. HFStruct /\ G e. HFStruct ) -> Rel F ) with typecode |-
8		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 |-
9		dmstructnn	$$⊢F\mathrm{Struct}x\to \mathrm{dom}F\subseteq \mathbb{N}$$
10		nnssnn0	$$⊢\mathbb{N}\subseteq {\mathbb{N}}_0$$
11	9 10	sstrdi	$$⊢F\mathrm{Struct}x\to \mathrm{dom}F\subseteq {\mathbb{N}}_0$$
12		dff1o5	$$⊢\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{1-1}{⟶}{\mathbb{N}}_0\wedge \mathrm{ran}\left({\left|.\right|\upharpoonright }_{\mathrm{\omega }}\right)={\mathbb{N}}_0\right)$$
13	1 12	mpbi	$$⊢\left(\left({\left|.\right|\upharpoonright }_{\mathrm{\omega }}\right):\mathrm{\omega }\underset{1-1}{⟶}{\mathbb{N}}_0\wedge \mathrm{ran}\left({\left|.\right|\upharpoonright }_{\mathrm{\omega }}\right)={\mathbb{N}}_0\right)$$
14	13	simpri	$$⊢\mathrm{ran}\left({\left|.\right|\upharpoonright }_{\mathrm{\omega }}\right)={\mathbb{N}}_0$$
15	11 14	sseqtrrdi	$$⊢F\mathrm{Struct}x\to \mathrm{dom}F\subseteq \mathrm{ran}\left({\left|.\right|\upharpoonright }_{\mathrm{\omega }}\right)$$
16	15	exlimiv	$$⊢\exists xF\mathrm{Struct}x\to \mathrm{dom}F\subseteq \mathrm{ran}\left({\left|.\right|\upharpoonright }_{\mathrm{\omega }}\right)$$
17	8 16	syl	Could not format ( F e. HFStruct -> dom F C_ ran ( # |` _om ) ) : No typesetting found for |- ( F e. HFStruct -> dom F C_ ran ( # |` _om ) ) with typecode |-
18	17	adantr	Could not format ( ( F e. HFStruct /\ G e. HFStruct ) -> dom F C_ ran ( # |` _om ) ) : No typesetting found for |- ( ( F e. HFStruct /\ G e. HFStruct ) -> dom F C_ ran ( # |` _om ) ) with typecode |-
19		hfstructfun	Could not format ( G e. HFStruct -> Fun G ) : No typesetting found for |- ( G e. HFStruct -> Fun G ) with typecode |-
20		funrel	$$⊢\mathrm{Fun}G\to \mathrm{Rel}G$$
21	19 20	syl	Could not format ( G e. HFStruct -> Rel G ) : No typesetting found for |- ( G e. HFStruct -> Rel G ) with typecode |-
22	21	adantl	Could not format ( ( F e. HFStruct /\ G e. HFStruct ) -> Rel G ) : No typesetting found for |- ( ( F e. HFStruct /\ G e. HFStruct ) -> Rel G ) with typecode |-
23		hfstructstruct	Could not format ( G e. HFStruct -> E. x G Struct x ) : No typesetting found for |- ( G e. HFStruct -> E. x G Struct x ) with typecode |-
24		dmstructnn	$$⊢G\mathrm{Struct}x\to \mathrm{dom}G\subseteq \mathbb{N}$$
25	24 10	sstrdi	$$⊢G\mathrm{Struct}x\to \mathrm{dom}G\subseteq {\mathbb{N}}_0$$
26	25 14	sseqtrrdi	$$⊢G\mathrm{Struct}x\to \mathrm{dom}G\subseteq \mathrm{ran}\left({\left|.\right|\upharpoonright }_{\mathrm{\omega }}\right)$$
27	26	exlimiv	$$⊢\exists xG\mathrm{Struct}x\to \mathrm{dom}G\subseteq \mathrm{ran}\left({\left|.\right|\upharpoonright }_{\mathrm{\omega }}\right)$$
28	23 27	syl	Could not format ( G e. HFStruct -> dom G C_ ran ( # |` _om ) ) : No typesetting found for |- ( G e. HFStruct -> dom G C_ ran ( # |` _om ) ) with typecode |-
29	28	adantl	Could not format ( ( F e. HFStruct /\ G e. HFStruct ) -> dom G C_ ran ( # |` _om ) ) : No typesetting found for |- ( ( F e. HFStruct /\ G e. HFStruct ) -> dom G C_ ran ( # |` _om ) ) with typecode |-
30	3 7 18 22 29	cocan2g	Could not format ( ( F e. HFStruct /\ G e. HFStruct ) -> ( ( F o. ( # |` _om ) ) = ( G o. ( # |` _om ) ) <-> F = G ) ) : No typesetting found for |- ( ( F e. HFStruct /\ G e. HFStruct ) -> ( ( F o. ( # |` _om ) ) = ( G o. ( # |` _om ) ) <-> F = G ) ) with typecode |-