Theorem ishfstruct

Description: Conditions that imply that F is an HFStruct. (Contributed by Eric Schmidt, 29-Sep-2026)

	Ref	Expression
Assertion	ishfstruct	Could not format assertion : No typesetting found for |- ( ( F Struct X /\ Rel F /\ ran F C_ HF ) -> F e. HFStruct ) with typecode |-

Proof

Step	Hyp	Ref	Expression
1		brstruct	$$⊢\mathrm{Rel}\mathrm{Struct}$$
2	1	releldmi	$$⊢F\mathrm{Struct}X\to F\in \mathrm{dom}\mathrm{Struct}$$
3	2	3ad2ant1	Could not format ( ( F Struct X /\ Rel F /\ ran F C_ HF ) -> F e. dom Struct ) : No typesetting found for |- ( ( F Struct X /\ Rel F /\ ran F C_ HF ) -> F e. dom Struct ) with typecode |-
4		structex	$$⊢F\mathrm{Struct}X\to F\in \mathrm{V}$$
5	4	3ad2ant1	Could not format ( ( F Struct X /\ Rel F /\ ran F C_ HF ) -> F e. _V ) : No typesetting found for |- ( ( F Struct X /\ Rel F /\ ran F C_ HF ) -> F e. _V ) with typecode |-
6		relssdmrn	$$⊢\mathrm{Rel}F\to F\subseteq \mathrm{dom}F\times \mathrm{ran}F$$
7	6	3ad2ant2	Could not format ( ( F Struct X /\ Rel F /\ ran F C_ HF ) -> F C_ ( dom F X. ran F ) ) : No typesetting found for |- ( ( F Struct X /\ Rel F /\ ran F C_ HF ) -> F C_ ( dom F X. ran F ) ) with typecode |-
8		ssv	$$⊢\mathrm{dom}F\subseteq \mathrm{V}$$
9		xpss12	Could not format ( ( dom F C_ _V /\ ran F C_ HF ) -> ( dom F X. ran F ) C_ ( _V X. HF ) ) : No typesetting found for |- ( ( dom F C_ _V /\ ran F C_ HF ) -> ( dom F X. ran F ) C_ ( _V X. HF ) ) with typecode |-
10	8 9	mpan	Could not format ( ran F C_ HF -> ( dom F X. ran F ) C_ ( _V X. HF ) ) : No typesetting found for |- ( ran F C_ HF -> ( dom F X. ran F ) C_ ( _V X. HF ) ) with typecode |-
11	10	3ad2ant3	Could not format ( ( F Struct X /\ Rel F /\ ran F C_ HF ) -> ( dom F X. ran F ) C_ ( _V X. HF ) ) : No typesetting found for |- ( ( F Struct X /\ Rel F /\ ran F C_ HF ) -> ( dom F X. ran F ) C_ ( _V X. HF ) ) with typecode |-
12	7 11	sstrd	Could not format ( ( F Struct X /\ Rel F /\ ran F C_ HF ) -> F C_ ( _V X. HF ) ) : No typesetting found for |- ( ( F Struct X /\ Rel F /\ ran F C_ HF ) -> F C_ ( _V X. HF ) ) with typecode |-
13	5 12	elpwd	Could not format ( ( F Struct X /\ Rel F /\ ran F C_ HF ) -> F e. ~P ( _V X. HF ) ) : No typesetting found for |- ( ( F Struct X /\ Rel F /\ ran F C_ HF ) -> F e. ~P ( _V X. HF ) ) with typecode |-
14	3 13	elind	Could not format ( ( F Struct X /\ Rel F /\ ran F C_ HF ) -> F e. ( dom Struct i^i ~P ( _V X. HF ) ) ) : No typesetting found for |- ( ( F Struct X /\ Rel F /\ ran F C_ HF ) -> F e. ( dom Struct i^i ~P ( _V X. HF ) ) ) with typecode |-
15		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 |-
16	14 15	eleqtrrdi	Could not format ( ( F Struct X /\ Rel F /\ ran F C_ HF ) -> F e. HFStruct ) : No typesetting found for |- ( ( F Struct X /\ Rel F /\ ran F C_ HF ) -> F e. HFStruct ) with typecode |-