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 e. _V |-> ( har ` ~P ( X X. z ) ) ) , ( har ` ~P X ) ) |` _om )
Assertion hsmexlem9 
|- ( a e. _om -> ( H ` a ) e. On )

Proof

Step Hyp Ref Expression
1 hsmexlem7.h 
 |-  H = ( rec ( ( z e. _V |-> ( har ` ~P ( X X. z ) ) ) , ( har ` ~P X ) ) |` _om )
2 nn0suc 
 |-  ( a e. _om -> ( a = (/) \/ E. b e. _om a = suc b ) )
3 fveq2 
 |-  ( a = (/) -> ( H ` a ) = ( H ` (/) ) )
4 1 hsmexlem7 
 |-  ( H ` (/) ) = ( har ` ~P X )
5 harcl 
 |-  ( har ` ~P X ) e. On
6 4 5 eqeltri 
 |-  ( H ` (/) ) e. On
7 3 6 eqeltrdi 
 |-  ( a = (/) -> ( H ` a ) e. On )
8 1 hsmexlem8 
 |-  ( b e. _om -> ( H ` suc b ) = ( har ` ~P ( X X. ( H ` b ) ) ) )
9 harcl 
 |-  ( har ` ~P ( X X. ( H ` b ) ) ) e. On
10 8 9 eqeltrdi 
 |-  ( b e. _om -> ( H ` suc b ) e. On )
11 fveq2 
 |-  ( a = suc b -> ( H ` a ) = ( H ` suc b ) )
12 11 eleq1d 
 |-  ( a = suc b -> ( ( H ` a ) e. On <-> ( H ` suc b ) e. On ) )
13 10 12 syl5ibrcom 
 |-  ( b e. _om -> ( a = suc b -> ( H ` a ) e. On ) )
14 13 rexlimiv 
 |-  ( E. b e. _om a = suc b -> ( H ` a ) e. On )
15 7 14 jaoi 
 |-  ( ( a = (/) \/ E. b e. _om a = suc b ) -> ( H ` a ) e. On )
16 2 15 syl 
 |-  ( a e. _om -> ( H ` a ) e. On )