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

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 ( 𝐵 ∈ ( ℤ≥ ‘ 𝐴 ) → ( 𝐶 ∈ ( 𝐴 ..^ ( 𝐵 + 1 ) ) ↔ ( 𝐶 ∈ ( 𝐴 ..^ 𝐵 ) ∨ 𝐶 = 𝐵 ) ) )

Proof

Step Hyp Ref Expression
1 fzosplitsn ⊢ ( 𝐵 ∈ ( ℤ≥ ‘ 𝐴 ) → ( 𝐴 ..^ ( 𝐵 + 1 ) ) = ( ( 𝐴 ..^ 𝐵 ) ∪ { 𝐵 } ) )
2 1 eleq2d ⊢ ( 𝐵 ∈ ( ℤ≥ ‘ 𝐴 ) → ( 𝐶 ∈ ( 𝐴 ..^ ( 𝐵 + 1 ) ) ↔ 𝐶 ∈ ( ( 𝐴 ..^ 𝐵 ) ∪ { 𝐵 } ) ) )
3 elun ⊢ ( 𝐶 ∈ ( ( 𝐴 ..^ 𝐵 ) ∪ { 𝐵 } ) ↔ ( 𝐶 ∈ ( 𝐴 ..^ 𝐵 ) ∨ 𝐶 ∈ { 𝐵 } ) )
4 elsn2g ⊢ ( 𝐵 ∈ ( ℤ≥ ‘ 𝐴 ) → ( 𝐶 ∈ { 𝐵 } ↔ 𝐶 = 𝐵 ) )
5 4 orbi2d ⊢ ( 𝐵 ∈ ( ℤ≥ ‘ 𝐴 ) → ( ( 𝐶 ∈ ( 𝐴 ..^ 𝐵 ) ∨ 𝐶 ∈ { 𝐵 } ) ↔ ( 𝐶 ∈ ( 𝐴 ..^ 𝐵 ) ∨ 𝐶 = 𝐵 ) ) )
6 3 5 bitrid ⊢ ( 𝐵 ∈ ( ℤ≥ ‘ 𝐴 ) → ( 𝐶 ∈ ( ( 𝐴 ..^ 𝐵 ) ∪ { 𝐵 } ) ↔ ( 𝐶 ∈ ( 𝐴 ..^ 𝐵 ) ∨ 𝐶 = 𝐵 ) ) )
7 2 6 bitrd ⊢ ( 𝐵 ∈ ( ℤ≥ ‘ 𝐴 ) → ( 𝐶 ∈ ( 𝐴 ..^ ( 𝐵 + 1 ) ) ↔ ( 𝐶 ∈ ( 𝐴 ..^ 𝐵 ) ∨ 𝐶 = 𝐵 ) ) )