Metamath Proof Explorer


Theorem 1elfz0hash

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 ) ) )

Proof

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 ) ) )