Theorem hfelhfOLD

Description: Obsolete version of elhf3 as of 17-Sep-2026. (Contributed by Scott Fenton, 16-Jul-2015) (Proof modification is discouraged.) (New usage is discouraged.)

	Ref	Expression
Assertion	hfelhfOLD	|- ( ( 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 )