This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

Theorem elfz1

Description: Membership in a finite set of sequential integers. (Contributed by NM, 21-Jul-2005)

Ref Expression
Assertion elfz1 ( ( 𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ ) → ( 𝐾 ∈ ( 𝑀 ... 𝑁 ) ↔ ( 𝐾 ∈ ℤ ∧ 𝑀 ≤ 𝐾 ∧ 𝐾 ≤ 𝑁 ) ) )

Proof

Step Hyp Ref Expression
1 fzval ⊢ ( ( 𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ ) → ( 𝑀 ... 𝑁 ) = { 𝑗 ∈ ℤ ∣ ( 𝑀 ≤ 𝑗 ∧ 𝑗 ≤ 𝑁 ) } )
2 1 eleq2d ⊢ ( ( 𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ ) → ( 𝐾 ∈ ( 𝑀 ... 𝑁 ) ↔ 𝐾 ∈ { 𝑗 ∈ ℤ ∣ ( 𝑀 ≤ 𝑗 ∧ 𝑗 ≤ 𝑁 ) } ) )
3 breq2 ⊢ ( 𝑗 = 𝐾 → ( 𝑀 ≤ 𝑗 ↔ 𝑀 ≤ 𝐾 ) )
4 breq1 ⊢ ( 𝑗 = 𝐾 → ( 𝑗 ≤ 𝑁 ↔ 𝐾 ≤ 𝑁 ) )
5 3 4 anbi12d ⊢ ( 𝑗 = 𝐾 → ( ( 𝑀 ≤ 𝑗 ∧ 𝑗 ≤ 𝑁 ) ↔ ( 𝑀 ≤ 𝐾 ∧ 𝐾 ≤ 𝑁 ) ) )
6 5 elrab ⊢ ( 𝐾 ∈ { 𝑗 ∈ ℤ ∣ ( 𝑀 ≤ 𝑗 ∧ 𝑗 ≤ 𝑁 ) } ↔ ( 𝐾 ∈ ℤ ∧ ( 𝑀 ≤ 𝐾 ∧ 𝐾 ≤ 𝑁 ) ) )
7 3anass ⊢ ( ( 𝐾 ∈ ℤ ∧ 𝑀 ≤ 𝐾 ∧ 𝐾 ≤ 𝑁 ) ↔ ( 𝐾 ∈ ℤ ∧ ( 𝑀 ≤ 𝐾 ∧ 𝐾 ≤ 𝑁 ) ) )
8 6 7 bitr4i ⊢ ( 𝐾 ∈ { 𝑗 ∈ ℤ ∣ ( 𝑀 ≤ 𝑗 ∧ 𝑗 ≤ 𝑁 ) } ↔ ( 𝐾 ∈ ℤ ∧ 𝑀 ≤ 𝐾 ∧ 𝐾 ≤ 𝑁 ) )
9 2 8 bitrdi ⊢ ( ( 𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ ) → ( 𝐾 ∈ ( 𝑀 ... 𝑁 ) ↔ ( 𝐾 ∈ ℤ ∧ 𝑀 ≤ 𝐾 ∧ 𝐾 ≤ 𝑁 ) ) )