Theorem alephfplem2

Description: Lemma for alephfp . (Contributed by NM, 6-Nov-2004)

	Ref	Expression
Hypothesis	alephfplem.1	|- H = ( rec ( aleph , _om ) |` _om )
Assertion	alephfplem2	|- ( w e. _om -> ( H ` suc w ) = ( aleph ` ( H ` w ) ) )

Proof

Step	Hyp	Ref	Expression
1		alephfplem.1	|- H = ( rec ( aleph , _om ) |` _om )
2		frsuc	|- ( w e. _om -> ( ( rec ( aleph , _om ) |` _om ) ` suc w ) = ( aleph ` ( ( rec ( aleph , _om ) |` _om ) ` w ) ) )
3	1	fveq1i	|- ( H ` suc w ) = ( ( rec ( aleph , _om ) |` _om ) ` suc w )
4	1	fveq1i	|- ( H ` w ) = ( ( rec ( aleph , _om ) |` _om ) ` w )
5	4	fveq2i	|- ( aleph ` ( H ` w ) ) = ( aleph ` ( ( rec ( aleph , _om ) |` _om ) ` w ) )
6	2 3 5	3eqtr4g	|- ( w e. _om -> ( H ` suc w ) = ( aleph ` ( H ` w ) ) )