Metamath Proof Explorer

Theorem elfzom1elfzo

Description: Membership in a half-open range of nonnegative integers. (Contributed by Alexander van der Vekens, 18-Jun-2018)

Ref Expression
Assertion elfzom1elfzo 
|- ( ( N e. ZZ /\ I e. ( 0 ..^ ( N - 1 ) ) ) -> I e. ( 0 ..^ N ) )

Proof

Step Hyp Ref Expression
1 fzossrbm1 
 |-  ( N e. ZZ -> ( 0 ..^ ( N - 1 ) ) C_ ( 0 ..^ N ) )
2 1 sselda 
 |-  ( ( N e. ZZ /\ I e. ( 0 ..^ ( N - 1 ) ) ) -> I e. ( 0 ..^ N ) )