Metamath Proof Explorer

Theorem fzosplitsni

Description: Membership in a half-open range extended by a singleton. (Contributed by Stefan O'Rear, 23-Aug-2015)

Ref Expression
Assertion fzosplitsni ⊢ B ∈ ℤ ≥ A → C ∈ A ..^ B + 1 ↔ C ∈ A ..^ B ∨ C = B

Proof

Step Hyp Ref Expression
1 fzosplitsn ⊢ B ∈ ℤ ≥ A → A ..^ B + 1 = A ..^ B ∪ B
2 1 eleq2d ⊢ B ∈ ℤ ≥ A → C ∈ A ..^ B + 1 ↔ C ∈ A ..^ B ∪ B
3 elun ⊢ C ∈ A ..^ B ∪ B ↔ C ∈ A ..^ B ∨ C ∈ B
4 elsn2g ⊢ B ∈ ℤ ≥ A → C ∈ B ↔ C = B
5 4 orbi2d ⊢ B ∈ ℤ ≥ A → C ∈ A ..^ B ∨ C ∈ B ↔ C ∈ A ..^ B ∨ C = B
6 3 5 bitrid ⊢ B ∈ ℤ ≥ A → C ∈ A ..^ B ∪ B ↔ C ∈ A ..^ B ∨ C = B
7 2 6 bitrd ⊢ B ∈ ℤ ≥ A → C ∈ A ..^ B + 1 ↔ C ∈ A ..^ B ∨ C = B