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