Metamath Proof Explorer

Theorem ishfstruct

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

Ref Expression
Assertion ishfstruct 
|- ( ( F Struct X /\ Rel F /\ ran F C_ HF ) -> F e. HFStruct )

Proof

Step Hyp Ref Expression
1 brstruct 
 |-  Rel Struct
2 1 releldmi 
 |-  ( F Struct X -> F e. dom Struct )
3 2 3ad2ant1 
 |-  ( ( F Struct X /\ Rel F /\ ran F C_ HF ) -> F e. dom Struct )
4 structex 
 |-  ( F Struct X -> F e. _V )
5 4 3ad2ant1 
 |-  ( ( F Struct X /\ Rel F /\ ran F C_ HF ) -> F e. _V )
6 relssdmrn 
 |-  ( Rel F -> F C_ ( dom F X. ran F ) )
7 6 3ad2ant2 
 |-  ( ( F Struct X /\ Rel F /\ ran F C_ HF ) -> F C_ ( dom F X. ran F ) )
8 ssv 
 |-  dom F C_ _V
9 xpss12 
 |-  ( ( dom F C_ _V /\ ran F C_ HF ) -> ( dom F X. ran F ) C_ ( _V X. HF ) )
10 8 9 mpan 
 |-  ( ran F C_ HF -> ( dom F X. ran F ) C_ ( _V X. HF ) )
11 10 3ad2ant3 
 |-  ( ( F Struct X /\ Rel F /\ ran F C_ HF ) -> ( dom F X. ran F ) C_ ( _V X. HF ) )
12 7 11 sstrd 
 |-  ( ( F Struct X /\ Rel F /\ ran F C_ HF ) -> F C_ ( _V X. HF ) )
13 5 12 elpwd 
 |-  ( ( F Struct X /\ Rel F /\ ran F C_ HF ) -> F e. ~P ( _V X. HF ) )
14 3 13 elind 
 |-  ( ( F Struct X /\ Rel F /\ ran F C_ HF ) -> F e. ( dom Struct i^i ~P ( _V X. HF ) ) )
15 df-hfstruct 
 |-  HFStruct = ( dom Struct i^i ~P ( _V X. HF ) )
16 14 15 eleqtrrdi 
 |-  ( ( F Struct X /\ Rel F /\ ran F C_ HF ) -> F e. HFStruct )