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	imbitrrid	|- ( 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 )