Step |
Hyp |
Ref |
Expression |
1 |
|
simpr |
|- ( ( ( A e. V /\ A =/= (/) ) /\ A e. Fin ) -> A e. Fin ) |
2 |
|
simplr |
|- ( ( ( A e. V /\ A =/= (/) ) /\ A e. Fin ) -> A =/= (/) ) |
3 |
|
hashnncl |
|- ( A e. Fin -> ( ( # ` A ) e. NN <-> A =/= (/) ) ) |
4 |
3
|
biimpar |
|- ( ( A e. Fin /\ A =/= (/) ) -> ( # ` A ) e. NN ) |
5 |
1 2 4
|
syl2anc |
|- ( ( ( A e. V /\ A =/= (/) ) /\ A e. Fin ) -> ( # ` A ) e. NN ) |
6 |
5
|
nnge1d |
|- ( ( ( A e. V /\ A =/= (/) ) /\ A e. Fin ) -> 1 <_ ( # ` A ) ) |
7 |
|
1xr |
|- 1 e. RR* |
8 |
|
pnfge |
|- ( 1 e. RR* -> 1 <_ +oo ) |
9 |
7 8
|
ax-mp |
|- 1 <_ +oo |
10 |
|
hashinf |
|- ( ( A e. V /\ -. A e. Fin ) -> ( # ` A ) = +oo ) |
11 |
10
|
adantlr |
|- ( ( ( A e. V /\ A =/= (/) ) /\ -. A e. Fin ) -> ( # ` A ) = +oo ) |
12 |
9 11
|
breqtrrid |
|- ( ( ( A e. V /\ A =/= (/) ) /\ -. A e. Fin ) -> 1 <_ ( # ` A ) ) |
13 |
6 12
|
pm2.61dan |
|- ( ( A e. V /\ A =/= (/) ) -> 1 <_ ( # ` A ) ) |