Theorem hfstructfun

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

	Ref	Expression
Assertion	hfstructfun	⊢ ( 𝐹 ∈ HFStruct → Fun 𝐹 )

Proof

Step	Hyp	Ref	Expression
1		hfstructstruct	⊢ ( 𝐹 ∈ HFStruct → ∃ 𝑥 𝐹 Struct 𝑥 )
2		structfung	⊢ ( 𝐹 Struct 𝑥 → Fun ◡ ◡ 𝐹 )
3	2	exlimiv	⊢ ( ∃ 𝑥 𝐹 Struct 𝑥 → Fun ◡ ◡ 𝐹 )
4	1 3	syl	⊢ ( 𝐹 ∈ HFStruct → Fun ◡ ◡ 𝐹 )
5		elinel2	⊢ ( 𝐹 ∈ ( dom Struct ∩ 𝒫 ( V × HF ) ) → 𝐹 ∈ 𝒫 ( V × HF ) )
6	5	elpwid	⊢ ( 𝐹 ∈ ( dom Struct ∩ 𝒫 ( V × HF ) ) → 𝐹 ⊆ ( V × HF ) )
7		df-hfstruct	⊢ HFStruct = ( dom Struct ∩ 𝒫 ( V × HF ) )
8	6 7	eleq2s	⊢ ( 𝐹 ∈ HFStruct → 𝐹 ⊆ ( V × HF ) )
9		relxp	⊢ Rel ( V × HF )
10		relss	⊢ ( 𝐹 ⊆ ( V × HF ) → ( Rel ( V × HF ) → Rel 𝐹 ) )
11	8 9 10	mpisyl	⊢ ( 𝐹 ∈ HFStruct → Rel 𝐹 )
12		dfrel2	⊢ ( Rel 𝐹 ↔ ◡ ◡ 𝐹 = 𝐹 )
13	12	biimpi	⊢ ( Rel 𝐹 → ◡ ◡ 𝐹 = 𝐹 )
14	13	funeqd	⊢ ( Rel 𝐹 → ( Fun ◡ ◡ 𝐹 ↔ Fun 𝐹 ) )
15	11 14	syl	⊢ ( 𝐹 ∈ HFStruct → ( Fun ◡ ◡ 𝐹 ↔ Fun 𝐹 ) )
16	4 15	mpbid	⊢ ( 𝐹 ∈ HFStruct → Fun 𝐹 )