Step |
Hyp |
Ref |
Expression |
1 |
|
hashf |
|- # : _V --> ( NN0 u. { +oo } ) |
2 |
1
|
a1i |
|- ( M e. V -> # : _V --> ( NN0 u. { +oo } ) ) |
3 |
|
elex |
|- ( M e. V -> M e. _V ) |
4 |
2 3
|
ffvelrnd |
|- ( M e. V -> ( # ` M ) e. ( NN0 u. { +oo } ) ) |
5 |
|
elun |
|- ( ( # ` M ) e. ( NN0 u. { +oo } ) <-> ( ( # ` M ) e. NN0 \/ ( # ` M ) e. { +oo } ) ) |
6 |
|
elsni |
|- ( ( # ` M ) e. { +oo } -> ( # ` M ) = +oo ) |
7 |
6
|
orim2i |
|- ( ( ( # ` M ) e. NN0 \/ ( # ` M ) e. { +oo } ) -> ( ( # ` M ) e. NN0 \/ ( # ` M ) = +oo ) ) |
8 |
5 7
|
sylbi |
|- ( ( # ` M ) e. ( NN0 u. { +oo } ) -> ( ( # ` M ) e. NN0 \/ ( # ` M ) = +oo ) ) |
9 |
4 8
|
syl |
|- ( M e. V -> ( ( # ` M ) e. NN0 \/ ( # ` M ) = +oo ) ) |