Theorem ishfstruct

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

	Ref	Expression
Assertion	ishfstruct	⊢ ( ( 𝐹 Struct 𝑋 ∧ Rel 𝐹 ∧ ran 𝐹 ⊆ HF ) → 𝐹 ∈ HFStruct )

Proof

Step	Hyp	Ref	Expression
1		brstruct	⊢ Rel Struct
2	1	releldmi	⊢ ( 𝐹 Struct 𝑋 → 𝐹 ∈ dom Struct )
3	2	3ad2ant1	⊢ ( ( 𝐹 Struct 𝑋 ∧ Rel 𝐹 ∧ ran 𝐹 ⊆ HF ) → 𝐹 ∈ dom Struct )
4		structex	⊢ ( 𝐹 Struct 𝑋 → 𝐹 ∈ V )
5	4	3ad2ant1	⊢ ( ( 𝐹 Struct 𝑋 ∧ Rel 𝐹 ∧ ran 𝐹 ⊆ HF ) → 𝐹 ∈ V )
6		relssdmrn	⊢ ( Rel 𝐹 → 𝐹 ⊆ ( dom 𝐹 × ran 𝐹 ) )
7	6	3ad2ant2	⊢ ( ( 𝐹 Struct 𝑋 ∧ Rel 𝐹 ∧ ran 𝐹 ⊆ HF ) → 𝐹 ⊆ ( dom 𝐹 × ran 𝐹 ) )
8		ssv	⊢ dom 𝐹 ⊆ V
9		xpss12	⊢ ( ( dom 𝐹 ⊆ V ∧ ran 𝐹 ⊆ HF ) → ( dom 𝐹 × ran 𝐹 ) ⊆ ( V × HF ) )
10	8 9	mpan	⊢ ( ran 𝐹 ⊆ HF → ( dom 𝐹 × ran 𝐹 ) ⊆ ( V × HF ) )
11	10	3ad2ant3	⊢ ( ( 𝐹 Struct 𝑋 ∧ Rel 𝐹 ∧ ran 𝐹 ⊆ HF ) → ( dom 𝐹 × ran 𝐹 ) ⊆ ( V × HF ) )
12	7 11	sstrd	⊢ ( ( 𝐹 Struct 𝑋 ∧ Rel 𝐹 ∧ ran 𝐹 ⊆ HF ) → 𝐹 ⊆ ( V × HF ) )
13	5 12	elpwd	⊢ ( ( 𝐹 Struct 𝑋 ∧ Rel 𝐹 ∧ ran 𝐹 ⊆ HF ) → 𝐹 ∈ 𝒫 ( V × HF ) )
14	3 13	elind	⊢ ( ( 𝐹 Struct 𝑋 ∧ Rel 𝐹 ∧ ran 𝐹 ⊆ HF ) → 𝐹 ∈ ( dom Struct ∩ 𝒫 ( V × HF ) ) )
15		df-hfstruct	⊢ HFStruct = ( dom Struct ∩ 𝒫 ( V × HF ) )
16	14 15	eleqtrrdi	⊢ ( ( 𝐹 Struct 𝑋 ∧ Rel 𝐹 ∧ ran 𝐹 ⊆ HF ) → 𝐹 ∈ HFStruct )