Metamath Proof Explorer

Theorem elixx1

Description: Membership in an interval of extended reals. (Contributed by Mario Carneiro, 3-Nov-2013)

Ref Expression
Hypothesis ixx.1 ⊢ O = x ∈ ℝ * , y ∈ ℝ * ⟼ z ∈ ℝ * | x R z ∧ z S y
Assertion elixx1 ⊢ A ∈ ℝ * ∧ B ∈ ℝ * → C ∈ A O B ↔ C ∈ ℝ * ∧ A R C ∧ C S B

Proof

Step Hyp Ref Expression
1 ixx.1 ⊢ O = x ∈ ℝ * , y ∈ ℝ * ⟼ z ∈ ℝ * | x R z ∧ z S y
2 1 ixxval ⊢ A ∈ ℝ * ∧ B ∈ ℝ * → A O B = z ∈ ℝ * | A R z ∧ z S B
3 2 eleq2d ⊢ A ∈ ℝ * ∧ B ∈ ℝ * → C ∈ A O B ↔ C ∈ z ∈ ℝ * | A R z ∧ z S B
4 breq2 ⊢ z = C → A R z ↔ A R C
5 breq1 ⊢ z = C → z S B ↔ C S B
6 4 5 anbi12d ⊢ z = C → A R z ∧ z S B ↔ A R C ∧ C S B
7 6 elrab ⊢ C ∈ z ∈ ℝ * | A R z ∧ z S B ↔ C ∈ ℝ * ∧ A R C ∧ C S B
8 3anass ⊢ C ∈ ℝ * ∧ A R C ∧ C S B ↔ C ∈ ℝ * ∧ A R C ∧ C S B
9 7 8 bitr4i ⊢ C ∈ z ∈ ℝ * | A R z ∧ z S B ↔ C ∈ ℝ * ∧ A R C ∧ C S B
10 3 9 bitrdi ⊢ A ∈ ℝ * ∧ B ∈ ℝ * → C ∈ A O B ↔ C ∈ ℝ * ∧ A R C ∧ C S B