Step |
Hyp |
Ref |
Expression |
1 |
|
hashnn0pnf |
|- ( A e. V -> ( ( # ` A ) e. NN0 \/ ( # ` A ) = +oo ) ) |
2 |
|
nn0re |
|- ( ( # ` A ) e. NN0 -> ( # ` A ) e. RR ) |
3 |
|
nn0ge0 |
|- ( ( # ` A ) e. NN0 -> 0 <_ ( # ` A ) ) |
4 |
|
ne0gt0 |
|- ( ( ( # ` A ) e. RR /\ 0 <_ ( # ` A ) ) -> ( ( # ` A ) =/= 0 <-> 0 < ( # ` A ) ) ) |
5 |
2 3 4
|
syl2anc |
|- ( ( # ` A ) e. NN0 -> ( ( # ` A ) =/= 0 <-> 0 < ( # ` A ) ) ) |
6 |
5
|
bicomd |
|- ( ( # ` A ) e. NN0 -> ( 0 < ( # ` A ) <-> ( # ` A ) =/= 0 ) ) |
7 |
|
breq2 |
|- ( ( # ` A ) = +oo -> ( 0 < ( # ` A ) <-> 0 < +oo ) ) |
8 |
|
0ltpnf |
|- 0 < +oo |
9 |
|
0re |
|- 0 e. RR |
10 |
|
renepnf |
|- ( 0 e. RR -> 0 =/= +oo ) |
11 |
9 10
|
ax-mp |
|- 0 =/= +oo |
12 |
11
|
necomi |
|- +oo =/= 0 |
13 |
8 12
|
2th |
|- ( 0 < +oo <-> +oo =/= 0 ) |
14 |
|
neeq1 |
|- ( ( # ` A ) = +oo -> ( ( # ` A ) =/= 0 <-> +oo =/= 0 ) ) |
15 |
13 14
|
bitr4id |
|- ( ( # ` A ) = +oo -> ( 0 < +oo <-> ( # ` A ) =/= 0 ) ) |
16 |
7 15
|
bitrd |
|- ( ( # ` A ) = +oo -> ( 0 < ( # ` A ) <-> ( # ` A ) =/= 0 ) ) |
17 |
6 16
|
jaoi |
|- ( ( ( # ` A ) e. NN0 \/ ( # ` A ) = +oo ) -> ( 0 < ( # ` A ) <-> ( # ` A ) =/= 0 ) ) |
18 |
1 17
|
syl |
|- ( A e. V -> ( 0 < ( # ` A ) <-> ( # ` A ) =/= 0 ) ) |
19 |
|
hasheq0 |
|- ( A e. V -> ( ( # ` A ) = 0 <-> A = (/) ) ) |
20 |
19
|
necon3bid |
|- ( A e. V -> ( ( # ` A ) =/= 0 <-> A =/= (/) ) ) |
21 |
18 20
|
bitrd |
|- ( A e. V -> ( 0 < ( # ` A ) <-> A =/= (/) ) ) |