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