Metamath Proof Explorer

Theorem hsmexlem7

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 hsmexlem7 
|- ( H ` (/) ) = ( har ` ~P X )

Proof

Step Hyp Ref Expression
1 hsmexlem7.h 
 |-  H = ( rec ( ( z e. _V |-> ( har ` ~P ( X X. z ) ) ) , ( har ` ~P X ) ) |` _om )
2 1 fveq1i 
 |-  ( H ` (/) ) = ( ( rec ( ( z e. _V |-> ( har ` ~P ( X X. z ) ) ) , ( har ` ~P X ) ) |` _om ) ` (/) )
3 fvex 
 |-  ( har ` ~P X ) e. _V
4 fr0g 
 |-  ( ( har ` ~P X ) e. _V -> ( ( rec ( ( z e. _V |-> ( har ` ~P ( X X. z ) ) ) , ( har ` ~P X ) ) |` _om ) ` (/) ) = ( har ` ~P X ) )
5 3 4 ax-mp 
 |-  ( ( rec ( ( z e. _V |-> ( har ` ~P ( X X. z ) ) ) , ( har ` ~P X ) ) |` _om ) ` (/) ) = ( har ` ~P X )
6 2 5 eqtri 
 |-  ( H ` (/) ) = ( har ` ~P X )