Description: 1 is an element of the finite set of sequential nonnegative integers bounded by the size of a nonempty finite set. (Contributed by AV, 9-May-2020)
Ref | Expression | ||
---|---|---|---|
Assertion | 1elfz0hash | |- ( ( A e. Fin /\ A =/= (/) ) -> 1 e. ( 0 ... ( # ` A ) ) ) |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | 1nn0 | |- 1 e. NN0 |
|
2 | 1 | a1i | |- ( ( A e. Fin /\ A =/= (/) ) -> 1 e. NN0 ) |
3 | hashcl | |- ( A e. Fin -> ( # ` A ) e. NN0 ) |
|
4 | 3 | adantr | |- ( ( A e. Fin /\ A =/= (/) ) -> ( # ` A ) e. NN0 ) |
5 | hashge1 | |- ( ( A e. Fin /\ A =/= (/) ) -> 1 <_ ( # ` A ) ) |
|
6 | elfz2nn0 | |- ( 1 e. ( 0 ... ( # ` A ) ) <-> ( 1 e. NN0 /\ ( # ` A ) e. NN0 /\ 1 <_ ( # ` A ) ) ) |
|
7 | 2 4 5 6 | syl3anbrc | |- ( ( A e. Fin /\ A =/= (/) ) -> 1 e. ( 0 ... ( # ` A ) ) ) |