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

Metamath Proof Explorer

Theorem elioo2

Description: Membership in an open interval of extended reals. (Contributed by NM, 6-Feb-2007)

Ref Expression
Assertion elioo2 ( ( 𝐴 ∈ ℝ* ∧ 𝐵 ∈ ℝ* ) → ( 𝐶 ∈ ( 𝐴 (,) 𝐵 ) ↔ ( 𝐶 ∈ ℝ ∧ 𝐴 < 𝐶 ∧ 𝐶 < 𝐵 ) ) )

Proof

Step Hyp Ref Expression
1 iooval2 ⊢ ( ( 𝐴 ∈ ℝ* ∧ 𝐵 ∈ ℝ* ) → ( 𝐴 (,) 𝐵 ) = { 𝑥 ∈ ℝ ∣ ( 𝐴 < 𝑥 ∧ 𝑥 < 𝐵 ) } )
2 1 eleq2d ⊢ ( ( 𝐴 ∈ ℝ* ∧ 𝐵 ∈ ℝ* ) → ( 𝐶 ∈ ( 𝐴 (,) 𝐵 ) ↔ 𝐶 ∈ { 𝑥 ∈ ℝ ∣ ( 𝐴 < 𝑥 ∧ 𝑥 < 𝐵 ) } ) )
3 breq2 ⊢ ( 𝑥 = 𝐶 → ( 𝐴 < 𝑥 ↔ 𝐴 < 𝐶 ) )
4 breq1 ⊢ ( 𝑥 = 𝐶 → ( 𝑥 < 𝐵 ↔ 𝐶 < 𝐵 ) )
5 3 4 anbi12d ⊢ ( 𝑥 = 𝐶 → ( ( 𝐴 < 𝑥 ∧ 𝑥 < 𝐵 ) ↔ ( 𝐴 < 𝐶 ∧ 𝐶 < 𝐵 ) ) )
6 5 elrab ⊢ ( 𝐶 ∈ { 𝑥 ∈ ℝ ∣ ( 𝐴 < 𝑥 ∧ 𝑥 < 𝐵 ) } ↔ ( 𝐶 ∈ ℝ ∧ ( 𝐴 < 𝐶 ∧ 𝐶 < 𝐵 ) ) )
7 3anass ⊢ ( ( 𝐶 ∈ ℝ ∧ 𝐴 < 𝐶 ∧ 𝐶 < 𝐵 ) ↔ ( 𝐶 ∈ ℝ ∧ ( 𝐴 < 𝐶 ∧ 𝐶 < 𝐵 ) ) )
8 6 7 bitr4i ⊢ ( 𝐶 ∈ { 𝑥 ∈ ℝ ∣ ( 𝐴 < 𝑥 ∧ 𝑥 < 𝐵 ) } ↔ ( 𝐶 ∈ ℝ ∧ 𝐴 < 𝐶 ∧ 𝐶 < 𝐵 ) )
9 2 8 bitrdi ⊢ ( ( 𝐴 ∈ ℝ* ∧ 𝐵 ∈ ℝ* ) → ( 𝐶 ∈ ( 𝐴 (,) 𝐵 ) ↔ ( 𝐶 ∈ ℝ ∧ 𝐴 < 𝐶 ∧ 𝐶 < 𝐵 ) ) )