Metamath Proof Explorer


Theorem hfelhf

Description: Any member of an HF set is itself an HF set. (Contributed by Scott Fenton, 16-Jul-2015)

Ref Expression
Assertion hfelhf
|- ( ( A e. B /\ B e. Hf ) -> A e. Hf )

Proof

Step Hyp Ref Expression
1 rankelg
 |-  ( ( B e. Hf /\ A e. B ) -> ( rank ` A ) e. ( rank ` B ) )
2 1 ancoms
 |-  ( ( A e. B /\ B e. Hf ) -> ( rank ` A ) e. ( rank ` B ) )
3 elhf2g
 |-  ( B e. Hf -> ( B e. Hf <-> ( rank ` B ) e. _om ) )
4 3 ibi
 |-  ( B e. Hf -> ( rank ` B ) e. _om )
5 elnn
 |-  ( ( ( rank ` A ) e. ( rank ` B ) /\ ( rank ` B ) e. _om ) -> ( rank ` A ) e. _om )
6 elhf2g
 |-  ( A e. B -> ( A e. Hf <-> ( rank ` A ) e. _om ) )
7 5 6 syl5ibr
 |-  ( A e. B -> ( ( ( rank ` A ) e. ( rank ` B ) /\ ( rank ` B ) e. _om ) -> A e. Hf ) )
8 7 expcomd
 |-  ( A e. B -> ( ( rank ` B ) e. _om -> ( ( rank ` A ) e. ( rank ` B ) -> A e. Hf ) ) )
9 8 imp
 |-  ( ( A e. B /\ ( rank ` B ) e. _om ) -> ( ( rank ` A ) e. ( rank ` B ) -> A e. Hf ) )
10 4 9 sylan2
 |-  ( ( A e. B /\ B e. Hf ) -> ( ( rank ` A ) e. ( rank ` B ) -> A e. Hf ) )
11 2 10 mpd
 |-  ( ( A e. B /\ B e. Hf ) -> A e. Hf )