Metamath Proof Explorer

Theorem hsmexlem9

Description: Lemma for hsmex . Properties of the recurrent sequence of ordinals. (Contributed by Stefan O'Rear, 14-Feb-2015)

Ref Expression
Hypothesis hsmexlem7.h ⊢ H = rec ⁡ z ∈ V ⟼ har ⁡ 𝒫 X × z har ⁡ 𝒫 X ↾ ω
Assertion hsmexlem9 ⊢ a ∈ ω → H ⁡ a ∈ On

Proof

Step Hyp Ref Expression
1 hsmexlem7.h ⊢ H = rec ⁡ z ∈ V ⟼ har ⁡ 𝒫 X × z har ⁡ 𝒫 X ↾ ω
2 nn0suc ⊢ a ∈ ω → a = ∅ ∨ ∃ b ∈ ω a = suc ⁡ b
3 fveq2 ⊢ a = ∅ → H ⁡ a = H ⁡ ∅
4 1 hsmexlem7 ⊢ H ⁡ ∅ = har ⁡ 𝒫 X
5 harcl ⊢ har ⁡ 𝒫 X ∈ On
6 4 5 eqeltri ⊢ H ⁡ ∅ ∈ On
7 3 6 eqeltrdi ⊢ a = ∅ → H ⁡ a ∈ On
8 1 hsmexlem8 ⊢ b ∈ ω → H ⁡ suc ⁡ b = har ⁡ 𝒫 X × H ⁡ b
9 harcl ⊢ har ⁡ 𝒫 X × H ⁡ b ∈ On
10 8 9 eqeltrdi ⊢ b ∈ ω → H ⁡ suc ⁡ b ∈ On
11 fveq2 ⊢ a = suc ⁡ b → H ⁡ a = H ⁡ suc ⁡ b
12 11 eleq1d ⊢ a = suc ⁡ b → H ⁡ a ∈ On ↔ H ⁡ suc ⁡ b ∈ On
13 10 12 syl5ibrcom ⊢ b ∈ ω → a = suc ⁡ b → H ⁡ a ∈ On
14 13 rexlimiv ⊢ ∃ b ∈ ω a = suc ⁡ b → H ⁡ a ∈ On
15 7 14 jaoi ⊢ a = ∅ ∨ ∃ b ∈ ω a = suc ⁡ b → H ⁡ a ∈ On
16 2 15 syl ⊢ a ∈ ω → H ⁡ a ∈ On