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	⊢ ( ( 𝐴 ∈ 𝐵 ∧ 𝐵 ∈ HF ) → 𝐴 ∈ HF )

Proof

Step	Hyp	Ref	Expression
1		rankelg	⊢ ( ( 𝐵 ∈ HF ∧ 𝐴 ∈ 𝐵 ) → ( rank ‘ 𝐴 ) ∈ ( rank ‘ 𝐵 ) )
2	1	ancoms	⊢ ( ( 𝐴 ∈ 𝐵 ∧ 𝐵 ∈ HF ) → ( rank ‘ 𝐴 ) ∈ ( rank ‘ 𝐵 ) )
3		elhf2g	⊢ ( 𝐵 ∈ HF → ( 𝐵 ∈ HF ↔ ( rank ‘ 𝐵 ) ∈ ω ) )
4	3	ibi	⊢ ( 𝐵 ∈ HF → ( rank ‘ 𝐵 ) ∈ ω )
5		elnn	⊢ ( ( ( rank ‘ 𝐴 ) ∈ ( rank ‘ 𝐵 ) ∧ ( rank ‘ 𝐵 ) ∈ ω ) → ( rank ‘ 𝐴 ) ∈ ω )
6		elhf2g	⊢ ( 𝐴 ∈ 𝐵 → ( 𝐴 ∈ HF ↔ ( rank ‘ 𝐴 ) ∈ ω ) )
7	5 6	imbitrrid	⊢ ( 𝐴 ∈ 𝐵 → ( ( ( rank ‘ 𝐴 ) ∈ ( rank ‘ 𝐵 ) ∧ ( rank ‘ 𝐵 ) ∈ ω ) → 𝐴 ∈ HF ) )
8	7	expcomd	⊢ ( 𝐴 ∈ 𝐵 → ( ( rank ‘ 𝐵 ) ∈ ω → ( ( rank ‘ 𝐴 ) ∈ ( rank ‘ 𝐵 ) → 𝐴 ∈ HF ) ) )
9	8	imp	⊢ ( ( 𝐴 ∈ 𝐵 ∧ ( rank ‘ 𝐵 ) ∈ ω ) → ( ( rank ‘ 𝐴 ) ∈ ( rank ‘ 𝐵 ) → 𝐴 ∈ HF ) )
10	4 9	sylan2	⊢ ( ( 𝐴 ∈ 𝐵 ∧ 𝐵 ∈ HF ) → ( ( rank ‘ 𝐴 ) ∈ ( rank ‘ 𝐵 ) → 𝐴 ∈ HF ) )
11	2 10	mpd	⊢ ( ( 𝐴 ∈ 𝐵 ∧ 𝐵 ∈ HF ) → 𝐴 ∈ HF )