Metamath Proof Explorer

Theorem alephfplem3

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

Ref Expression
Hypothesis alephfplem.1 
|- H = ( rec ( aleph , _om ) |` _om )
Assertion alephfplem3 
|- ( v e. _om -> ( H ` v ) e. ran aleph )

Proof

Step Hyp Ref Expression
1 alephfplem.1 
 |-  H = ( rec ( aleph , _om ) |` _om )
2 fveq2 
 |-  ( v = (/) -> ( H ` v ) = ( H ` (/) ) )
3 2 eleq1d 
 |-  ( v = (/) -> ( ( H ` v ) e. ran aleph <-> ( H ` (/) ) e. ran aleph ) )
4 fveq2 
 |-  ( v = w -> ( H ` v ) = ( H ` w ) )
5 4 eleq1d 
 |-  ( v = w -> ( ( H ` v ) e. ran aleph <-> ( H ` w ) e. ran aleph ) )
6 fveq2 
 |-  ( v = suc w -> ( H ` v ) = ( H ` suc w ) )
7 6 eleq1d 
 |-  ( v = suc w -> ( ( H ` v ) e. ran aleph <-> ( H ` suc w ) e. ran aleph ) )
8 1 alephfplem1 
 |-  ( H ` (/) ) e. ran aleph
9 alephfnon 
 |-  aleph Fn On
10 alephsson 
 |-  ran aleph C_ On
11 10 sseli 
 |-  ( ( H ` w ) e. ran aleph -> ( H ` w ) e. On )
12 fnfvelrn 
 |-  ( ( aleph Fn On /\ ( H ` w ) e. On ) -> ( aleph ` ( H ` w ) ) e. ran aleph )
13 9 11 12 sylancr 
 |-  ( ( H ` w ) e. ran aleph -> ( aleph ` ( H ` w ) ) e. ran aleph )
14 1 alephfplem2 
 |-  ( w e. _om -> ( H ` suc w ) = ( aleph ` ( H ` w ) ) )
15 14 eleq1d 
 |-  ( w e. _om -> ( ( H ` suc w ) e. ran aleph <-> ( aleph ` ( H ` w ) ) e. ran aleph ) )
16 13 15 syl5ibr 
 |-  ( w e. _om -> ( ( H ` w ) e. ran aleph -> ( H ` suc w ) e. ran aleph ) )
17 3 5 7 8 16 finds1 
 |-  ( v e. _om -> ( H ` v ) e. ran aleph )