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∈ℤ∧I∈0..^N−1→I∈0..^N

Proof

Step Hyp Ref Expression
1 fzossrbm1 ⊢N∈ℤ→0..^N−1⊆0..^N
2 1 sselda ⊢N∈ℤ∧I∈0..^N−1→I∈0..^N