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