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	⊢ 𝐻 = ( rec ( ( 𝑧 ∈ V ↦ ( har ‘ 𝒫 ( 𝑋 × 𝑧 ) ) ) , ( har ‘ 𝒫 𝑋 ) ) ↾ ω )
Assertion	hsmexlem9	⊢ ( 𝑎 ∈ ω → ( 𝐻 ‘ 𝑎 ) ∈ On )

Proof

Step	Hyp	Ref	Expression
1		hsmexlem7.h	⊢ 𝐻 = ( rec ( ( 𝑧 ∈ V ↦ ( har ‘ 𝒫 ( 𝑋 × 𝑧 ) ) ) , ( har ‘ 𝒫 𝑋 ) ) ↾ ω )
2		nn0suc	⊢ ( 𝑎 ∈ ω → ( 𝑎 = ∅ ∨ ∃ 𝑏 ∈ ω 𝑎 = suc 𝑏 ) )
3		fveq2	⊢ ( 𝑎 = ∅ → ( 𝐻 ‘ 𝑎 ) = ( 𝐻 ‘ ∅ ) )
4	1	hsmexlem7	⊢ ( 𝐻 ‘ ∅ ) = ( har ‘ 𝒫 𝑋 )
5		harcl	⊢ ( har ‘ 𝒫 𝑋 ) ∈ On
6	4 5	eqeltri	⊢ ( 𝐻 ‘ ∅ ) ∈ On
7	3 6	eqeltrdi	⊢ ( 𝑎 = ∅ → ( 𝐻 ‘ 𝑎 ) ∈ On )
8	1	hsmexlem8	⊢ ( 𝑏 ∈ ω → ( 𝐻 ‘ suc 𝑏 ) = ( har ‘ 𝒫 ( 𝑋 × ( 𝐻 ‘ 𝑏 ) ) ) )
9		harcl	⊢ ( har ‘ 𝒫 ( 𝑋 × ( 𝐻 ‘ 𝑏 ) ) ) ∈ On
10	8 9	eqeltrdi	⊢ ( 𝑏 ∈ ω → ( 𝐻 ‘ suc 𝑏 ) ∈ On )
11		fveq2	⊢ ( 𝑎 = suc 𝑏 → ( 𝐻 ‘ 𝑎 ) = ( 𝐻 ‘ suc 𝑏 ) )
12	11	eleq1d	⊢ ( 𝑎 = suc 𝑏 → ( ( 𝐻 ‘ 𝑎 ) ∈ On ↔ ( 𝐻 ‘ suc 𝑏 ) ∈ On ) )
13	10 12	syl5ibrcom	⊢ ( 𝑏 ∈ ω → ( 𝑎 = suc 𝑏 → ( 𝐻 ‘ 𝑎 ) ∈ On ) )
14	13	rexlimiv	⊢ ( ∃ 𝑏 ∈ ω 𝑎 = suc 𝑏 → ( 𝐻 ‘ 𝑎 ) ∈ On )
15	7 14	jaoi	⊢ ( ( 𝑎 = ∅ ∨ ∃ 𝑏 ∈ ω 𝑎 = suc 𝑏 ) → ( 𝐻 ‘ 𝑎 ) ∈ On )
16	2 15	syl	⊢ ( 𝑎 ∈ ω → ( 𝐻 ‘ 𝑎 ) ∈ On )