Theorem hfstructfun

Description: An HFStruct is a function. (Contributed by Eric Schmidt, 29-Sep-2026)

	Ref	Expression
Assertion	hfstructfun	Could not format assertion : No typesetting found for |- ( F e. HFStruct -> Fun F ) with typecode |-

Proof

Step	Hyp	Ref	Expression
1		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 |-
2		structfung	$$⊢F\mathrm{Struct}x\to \mathrm{Fun}{F^{-1}}^{-1}$$
3	2	exlimiv	$$⊢\exists xF\mathrm{Struct}x\to \mathrm{Fun}{F^{-1}}^{-1}$$
4	1 3	syl	Could not format ( F e. HFStruct -> Fun `' `' F ) : No typesetting found for |- ( F e. HFStruct -> Fun `' `' F ) with typecode |-
5		elinel2	Could not format ( F e. ( dom Struct i^i ~P ( _V X. HF ) ) -> F e. ~P ( _V X. HF ) ) : No typesetting found for |- ( F e. ( dom Struct i^i ~P ( _V X. HF ) ) -> F e. ~P ( _V X. HF ) ) with typecode |-
6	5	elpwid	Could not format ( F e. ( dom Struct i^i ~P ( _V X. HF ) ) -> F C_ ( _V X. HF ) ) : No typesetting found for |- ( F e. ( dom Struct i^i ~P ( _V X. HF ) ) -> F C_ ( _V X. HF ) ) with typecode |-
7		df-hfstruct	Could not format HFStruct = ( dom Struct i^i ~P ( _V X. HF ) ) : No typesetting found for |- HFStruct = ( dom Struct i^i ~P ( _V X. HF ) ) with typecode |-
8	6 7	eleq2s	Could not format ( F e. HFStruct -> F C_ ( _V X. HF ) ) : No typesetting found for |- ( F e. HFStruct -> F C_ ( _V X. HF ) ) with typecode |-
9		relxp	Could not format Rel ( _V X. HF ) : No typesetting found for |- Rel ( _V X. HF ) with typecode |-
10		relss	Could not format ( F C_ ( _V X. HF ) -> ( Rel ( _V X. HF ) -> Rel F ) ) : No typesetting found for |- ( F C_ ( _V X. HF ) -> ( Rel ( _V X. HF ) -> Rel F ) ) with typecode |-
11	8 9 10	mpisyl	Could not format ( F e. HFStruct -> Rel F ) : No typesetting found for |- ( F e. HFStruct -> Rel F ) with typecode |-
12		dfrel2	$$⊢\mathrm{Rel}F\leftrightarrow {F^{-1}}^{-1}=F$$
13	12	biimpi	$$⊢\mathrm{Rel}F\to {F^{-1}}^{-1}=F$$
14	13	funeqd	$$⊢\mathrm{Rel}F\to \left(\mathrm{Fun}{F^{-1}}^{-1}\leftrightarrow \mathrm{Fun}F\right)$$
15	11 14	syl	Could not format ( F e. HFStruct -> ( Fun `' `' F <-> Fun F ) ) : No typesetting found for |- ( F e. HFStruct -> ( Fun `' `' F <-> Fun F ) ) with typecode |-
16	4 15	mpbid	Could not format ( F e. HFStruct -> Fun F ) : No typesetting found for |- ( F e. HFStruct -> Fun F ) with typecode |-