Metamath Proof Explorer

Theorem hfstructfun

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

Ref Expression
Assertion hfstructfun 
|- ( F e. HFStruct -> Fun F )

Proof

Step Hyp Ref Expression
1 hfstructstruct 
 |-  ( F e. HFStruct -> E. x F Struct x )
2 structfung 
 |-  ( F Struct x -> Fun `' `' F )
3 2 exlimiv 
 |-  ( E. x F Struct x -> Fun `' `' F )
4 1 3 syl 
 |-  ( F e. HFStruct -> Fun `' `' F )
5 elinel2 
 |-  ( F e. ( dom Struct i^i ~P ( _V X. HF ) ) -> F e. ~P ( _V X. HF ) )
6 5 elpwid 
 |-  ( F e. ( dom Struct i^i ~P ( _V X. HF ) ) -> F C_ ( _V X. HF ) )
7 df-hfstruct 
 |-  HFStruct = ( dom Struct i^i ~P ( _V X. HF ) )
8 6 7 eleq2s 
 |-  ( F e. HFStruct -> F C_ ( _V X. HF ) )
9 relxp 
 |-  Rel ( _V X. HF )
10 relss 
 |-  ( F C_ ( _V X. HF ) -> ( Rel ( _V X. HF ) -> Rel F ) )
11 8 9 10 mpisyl 
 |-  ( F e. HFStruct -> Rel F )
12 dfrel2 
 |-  ( Rel F <-> `' `' F = F )
13 12 biimpi 
 |-  ( Rel F -> `' `' F = F )
14 13 funeqd 
 |-  ( Rel F -> ( Fun `' `' F <-> Fun F ) )
15 11 14 syl 
 |-  ( F e. HFStruct -> ( Fun `' `' F <-> Fun F ) )
16 4 15 mpbid 
 |-  ( F e. HFStruct -> Fun F )