# Metamath Proof Explorer

## Theorem ioo0

Description: An empty open interval of extended reals. (Contributed by NM, 6-Feb-2007)

Ref Expression
Assertion ioo0 ${⊢}\left({A}\in {ℝ}^{*}\wedge {B}\in {ℝ}^{*}\right)\to \left(\left({A},{B}\right)=\varnothing ↔{B}\le {A}\right)$

### Proof

Step Hyp Ref Expression
1 iooval ${⊢}\left({A}\in {ℝ}^{*}\wedge {B}\in {ℝ}^{*}\right)\to \left({A},{B}\right)=\left\{{x}\in {ℝ}^{*}|\left({A}<{x}\wedge {x}<{B}\right)\right\}$
2 1 eqeq1d ${⊢}\left({A}\in {ℝ}^{*}\wedge {B}\in {ℝ}^{*}\right)\to \left(\left({A},{B}\right)=\varnothing ↔\left\{{x}\in {ℝ}^{*}|\left({A}<{x}\wedge {x}<{B}\right)\right\}=\varnothing \right)$
3 df-ne ${⊢}\left\{{x}\in {ℝ}^{*}|\left({A}<{x}\wedge {x}<{B}\right)\right\}\ne \varnothing ↔¬\left\{{x}\in {ℝ}^{*}|\left({A}<{x}\wedge {x}<{B}\right)\right\}=\varnothing$
4 rabn0 ${⊢}\left\{{x}\in {ℝ}^{*}|\left({A}<{x}\wedge {x}<{B}\right)\right\}\ne \varnothing ↔\exists {x}\in {ℝ}^{*}\phantom{\rule{.4em}{0ex}}\left({A}<{x}\wedge {x}<{B}\right)$
5 3 4 bitr3i ${⊢}¬\left\{{x}\in {ℝ}^{*}|\left({A}<{x}\wedge {x}<{B}\right)\right\}=\varnothing ↔\exists {x}\in {ℝ}^{*}\phantom{\rule{.4em}{0ex}}\left({A}<{x}\wedge {x}<{B}\right)$
6 xrlttr ${⊢}\left({A}\in {ℝ}^{*}\wedge {x}\in {ℝ}^{*}\wedge {B}\in {ℝ}^{*}\right)\to \left(\left({A}<{x}\wedge {x}<{B}\right)\to {A}<{B}\right)$
7 6 3com23 ${⊢}\left({A}\in {ℝ}^{*}\wedge {B}\in {ℝ}^{*}\wedge {x}\in {ℝ}^{*}\right)\to \left(\left({A}<{x}\wedge {x}<{B}\right)\to {A}<{B}\right)$
8 7 3expa ${⊢}\left(\left({A}\in {ℝ}^{*}\wedge {B}\in {ℝ}^{*}\right)\wedge {x}\in {ℝ}^{*}\right)\to \left(\left({A}<{x}\wedge {x}<{B}\right)\to {A}<{B}\right)$
9 8 rexlimdva ${⊢}\left({A}\in {ℝ}^{*}\wedge {B}\in {ℝ}^{*}\right)\to \left(\exists {x}\in {ℝ}^{*}\phantom{\rule{.4em}{0ex}}\left({A}<{x}\wedge {x}<{B}\right)\to {A}<{B}\right)$
10 qbtwnxr ${⊢}\left({A}\in {ℝ}^{*}\wedge {B}\in {ℝ}^{*}\wedge {A}<{B}\right)\to \exists {x}\in ℚ\phantom{\rule{.4em}{0ex}}\left({A}<{x}\wedge {x}<{B}\right)$
11 qre ${⊢}{x}\in ℚ\to {x}\in ℝ$
12 11 rexrd ${⊢}{x}\in ℚ\to {x}\in {ℝ}^{*}$
13 12 anim1i ${⊢}\left({x}\in ℚ\wedge \left({A}<{x}\wedge {x}<{B}\right)\right)\to \left({x}\in {ℝ}^{*}\wedge \left({A}<{x}\wedge {x}<{B}\right)\right)$
14 13 reximi2 ${⊢}\exists {x}\in ℚ\phantom{\rule{.4em}{0ex}}\left({A}<{x}\wedge {x}<{B}\right)\to \exists {x}\in {ℝ}^{*}\phantom{\rule{.4em}{0ex}}\left({A}<{x}\wedge {x}<{B}\right)$
15 10 14 syl ${⊢}\left({A}\in {ℝ}^{*}\wedge {B}\in {ℝ}^{*}\wedge {A}<{B}\right)\to \exists {x}\in {ℝ}^{*}\phantom{\rule{.4em}{0ex}}\left({A}<{x}\wedge {x}<{B}\right)$
16 15 3expia ${⊢}\left({A}\in {ℝ}^{*}\wedge {B}\in {ℝ}^{*}\right)\to \left({A}<{B}\to \exists {x}\in {ℝ}^{*}\phantom{\rule{.4em}{0ex}}\left({A}<{x}\wedge {x}<{B}\right)\right)$
17 9 16 impbid ${⊢}\left({A}\in {ℝ}^{*}\wedge {B}\in {ℝ}^{*}\right)\to \left(\exists {x}\in {ℝ}^{*}\phantom{\rule{.4em}{0ex}}\left({A}<{x}\wedge {x}<{B}\right)↔{A}<{B}\right)$
18 5 17 syl5bb ${⊢}\left({A}\in {ℝ}^{*}\wedge {B}\in {ℝ}^{*}\right)\to \left(¬\left\{{x}\in {ℝ}^{*}|\left({A}<{x}\wedge {x}<{B}\right)\right\}=\varnothing ↔{A}<{B}\right)$
19 xrltnle ${⊢}\left({A}\in {ℝ}^{*}\wedge {B}\in {ℝ}^{*}\right)\to \left({A}<{B}↔¬{B}\le {A}\right)$
20 18 19 bitrd ${⊢}\left({A}\in {ℝ}^{*}\wedge {B}\in {ℝ}^{*}\right)\to \left(¬\left\{{x}\in {ℝ}^{*}|\left({A}<{x}\wedge {x}<{B}\right)\right\}=\varnothing ↔¬{B}\le {A}\right)$
21 20 con4bid ${⊢}\left({A}\in {ℝ}^{*}\wedge {B}\in {ℝ}^{*}\right)\to \left(\left\{{x}\in {ℝ}^{*}|\left({A}<{x}\wedge {x}<{B}\right)\right\}=\varnothing ↔{B}\le {A}\right)$
22 2 21 bitrd ${⊢}\left({A}\in {ℝ}^{*}\wedge {B}\in {ℝ}^{*}\right)\to \left(\left({A},{B}\right)=\varnothing ↔{B}\le {A}\right)$