| Step |
Hyp |
Ref |
Expression |
| 1 |
|
alephfplem.1 |
|- H = ( rec ( aleph , _om ) |` _om ) |
| 2 |
|
omex |
|- _om e. _V |
| 3 |
|
fr0g |
|- ( _om e. _V -> ( ( rec ( aleph , _om ) |` _om ) ` (/) ) = _om ) |
| 4 |
2 3
|
ax-mp |
|- ( ( rec ( aleph , _om ) |` _om ) ` (/) ) = _om |
| 5 |
1
|
fveq1i |
|- ( H ` (/) ) = ( ( rec ( aleph , _om ) |` _om ) ` (/) ) |
| 6 |
|
aleph0 |
|- ( aleph ` (/) ) = _om |
| 7 |
4 5 6
|
3eqtr4i |
|- ( H ` (/) ) = ( aleph ` (/) ) |
| 8 |
|
alephfnon |
|- aleph Fn On |
| 9 |
|
0elon |
|- (/) e. On |
| 10 |
|
fnfvelrn |
|- ( ( aleph Fn On /\ (/) e. On ) -> ( aleph ` (/) ) e. ran aleph ) |
| 11 |
8 9 10
|
mp2an |
|- ( aleph ` (/) ) e. ran aleph |
| 12 |
7 11
|
eqeltri |
|- ( H ` (/) ) e. ran aleph |