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 |