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 ( ( 𝐴 ∈ ℝ*𝐵 ∈ ℝ* ) → ( 𝐶 ∈ ( 𝐴 (,) 𝐵 ) ↔ ( 𝐶 ∈ ℝ ∧ 𝐴 < 𝐶𝐶 < 𝐵 ) ) )