Metamath Proof Explorer

Theorem fzon0

Description: A half-open integer interval is nonempty iff it contains its left endpoint. (Contributed by Mario Carneiro, 29-Sep-2015)

Ref Expression
Assertion fzon0 ⊢ M ..^ N ≠ ∅ ↔ M ∈ M ..^ N

Proof

Step Hyp Ref Expression
1 n0 ⊢ M ..^ N ≠ ∅ ↔ ∃ x x ∈ M ..^ N
2 elfzolt3b ⊢ x ∈ M ..^ N → M ∈ M ..^ N
3 2 exlimiv ⊢ ∃ x x ∈ M ..^ N → M ∈ M ..^ N
4 1 3 sylbi ⊢ M ..^ N ≠ ∅ → M ∈ M ..^ N
5 ne0i ⊢ M ∈ M ..^ N → M ..^ N ≠ ∅
6 4 5 impbii ⊢ M ..^ N ≠ ∅ ↔ M ∈ M ..^ N