| Step |
Hyp |
Ref |
Expression |
| 1 |
|
alephfplem.1 |
|- H = ( rec ( aleph , _om ) |` _om ) |
| 2 |
|
frfnom |
|- ( rec ( aleph , _om ) |` _om ) Fn _om |
| 3 |
1
|
fneq1i |
|- ( H Fn _om <-> ( rec ( aleph , _om ) |` _om ) Fn _om ) |
| 4 |
2 3
|
mpbir |
|- H Fn _om |
| 5 |
1
|
alephfplem3 |
|- ( z e. _om -> ( H ` z ) e. ran aleph ) |
| 6 |
5
|
rgen |
|- A. z e. _om ( H ` z ) e. ran aleph |
| 7 |
|
ffnfv |
|- ( H : _om --> ran aleph <-> ( H Fn _om /\ A. z e. _om ( H ` z ) e. ran aleph ) ) |
| 8 |
4 6 7
|
mpbir2an |
|- H : _om --> ran aleph |
| 9 |
|
ssun2 |
|- ran aleph C_ ( _om u. ran aleph ) |
| 10 |
|
fss |
|- ( ( H : _om --> ran aleph /\ ran aleph C_ ( _om u. ran aleph ) ) -> H : _om --> ( _om u. ran aleph ) ) |
| 11 |
8 9 10
|
mp2an |
|- H : _om --> ( _om u. ran aleph ) |
| 12 |
|
peano1 |
|- (/) e. _om |
| 13 |
1
|
alephfplem1 |
|- ( H ` (/) ) e. ran aleph |
| 14 |
|
fveq2 |
|- ( z = (/) -> ( H ` z ) = ( H ` (/) ) ) |
| 15 |
14
|
eleq1d |
|- ( z = (/) -> ( ( H ` z ) e. ran aleph <-> ( H ` (/) ) e. ran aleph ) ) |
| 16 |
15
|
rspcev |
|- ( ( (/) e. _om /\ ( H ` (/) ) e. ran aleph ) -> E. z e. _om ( H ` z ) e. ran aleph ) |
| 17 |
12 13 16
|
mp2an |
|- E. z e. _om ( H ` z ) e. ran aleph |
| 18 |
|
omex |
|- _om e. _V |
| 19 |
|
cardinfima |
|- ( _om e. _V -> ( ( H : _om --> ( _om u. ran aleph ) /\ E. z e. _om ( H ` z ) e. ran aleph ) -> U. ( H " _om ) e. ran aleph ) ) |
| 20 |
18 19
|
ax-mp |
|- ( ( H : _om --> ( _om u. ran aleph ) /\ E. z e. _om ( H ` z ) e. ran aleph ) -> U. ( H " _om ) e. ran aleph ) |
| 21 |
11 17 20
|
mp2an |
|- U. ( H " _om ) e. ran aleph |