Metamath Proof Explorer

Theorem hsmexlem8

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 hsmexlem8 
|- ( a e. _om -> ( H ` suc a ) = ( har ` ~P ( X X. ( H ` a ) ) ) )

Proof

Step Hyp Ref Expression
1 hsmexlem7.h 
 |-  H = ( rec ( ( z e. _V |-> ( har ` ~P ( X X. z ) ) ) , ( har ` ~P X ) ) |` _om )
2 fvex 
 |-  ( har ` ~P ( X X. ( H ` a ) ) ) e. _V
3 xpeq2 
 |-  ( b = z -> ( X X. b ) = ( X X. z ) )
4 3 pweqd 
 |-  ( b = z -> ~P ( X X. b ) = ~P ( X X. z ) )
5 4 fveq2d 
 |-  ( b = z -> ( har ` ~P ( X X. b ) ) = ( har ` ~P ( X X. z ) ) )
6 xpeq2 
 |-  ( b = ( H ` a ) -> ( X X. b ) = ( X X. ( H ` a ) ) )
7 6 pweqd 
 |-  ( b = ( H ` a ) -> ~P ( X X. b ) = ~P ( X X. ( H ` a ) ) )
8 7 fveq2d 
 |-  ( b = ( H ` a ) -> ( har ` ~P ( X X. b ) ) = ( har ` ~P ( X X. ( H ` a ) ) ) )
9 1 5 8 frsucmpt2 
 |-  ( ( a e. _om /\ ( har ` ~P ( X X. ( H ` a ) ) ) e. _V ) -> ( H ` suc a ) = ( har ` ~P ( X X. ( H ` a ) ) ) )
10 2 9 mpan2 
 |-  ( a e. _om -> ( H ` suc a ) = ( har ` ~P ( X X. ( H ` a ) ) ) )