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

Metamath Proof Explorer

Theorem elfzp1

Description: Append an element to a finite set of sequential integers. (Contributed by NM, 19-Sep-2005) (Proof shortened by Mario Carneiro, 28-Apr-2015)

Ref Expression
Assertion elfzp1 ⊢ N ∈ ℤ ≥ M → K ∈ M … N + 1 ↔ K ∈ M … N ∨ K = N + 1

Proof

Step Hyp Ref Expression
1 fzsuc ⊢ N ∈ ℤ ≥ M → M … N + 1 = M … N ∪ N + 1
2 1 eleq2d ⊢ N ∈ ℤ ≥ M → K ∈ M … N + 1 ↔ K ∈ M … N ∪ N + 1
3 elun ⊢ K ∈ M … N ∪ N + 1 ↔ K ∈ M … N ∨ K ∈ N + 1
4 ovex ⊢ N + 1 ∈ V
5 4 elsn2 ⊢ K ∈ N + 1 ↔ K = N + 1
6 5 orbi2i ⊢ K ∈ M … N ∨ K ∈ N + 1 ↔ K ∈ M … N ∨ K = N + 1
7 3 6 bitri ⊢ K ∈ M … N ∪ N + 1 ↔ K ∈ M … N ∨ K = N + 1
8 2 7 bitrdi ⊢ N ∈ ℤ ≥ M → K ∈ M … N + 1 ↔ K ∈ M … N ∨ K = N + 1