Metamath Proof Explorer


Theorem alephfplem2

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

Ref Expression
Hypothesis alephfplem.1 H = rec ω ω
Assertion alephfplem2 w ω H suc w = H w

Proof

Step Hyp Ref Expression
1 alephfplem.1 H = rec ω ω
2 frsuc w ω rec ω ω suc w = rec ω ω w
3 1 fveq1i H suc w = rec ω ω suc w
4 1 fveq1i H w = rec ω ω w
5 4 fveq2i H w = rec ω ω w
6 2 3 5 3eqtr4g w ω H suc w = H w