Metamath Proof Explorer

Theorem ioo0

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

Ref Expression
Assertion ioo0 ( ( 𝐴 ∈ ℝ* ∧ 𝐵 ∈ ℝ* ) → ( ( 𝐴 (,) 𝐵 ) = ∅ ↔ 𝐵 ≤ 𝐴 ) )

Proof

Step Hyp Ref Expression
1 iooval ⊢ ( ( 𝐴 ∈ ℝ* ∧ 𝐵 ∈ ℝ* ) → ( 𝐴 (,) 𝐵 ) = { 𝑥 ∈ ℝ* ∣ ( 𝐴 < 𝑥 ∧ 𝑥 < 𝐵 ) } )
2 1 eqeq1d ⊢ ( ( 𝐴 ∈ ℝ* ∧ 𝐵 ∈ ℝ* ) → ( ( 𝐴 (,) 𝐵 ) = ∅ ↔ { 𝑥 ∈ ℝ* ∣ ( 𝐴 < 𝑥 ∧ 𝑥 < 𝐵 ) } = ∅ ) )
3 df-ne ⊢ ( { 𝑥 ∈ ℝ* ∣ ( 𝐴 < 𝑥 ∧ 𝑥 < 𝐵 ) } ≠ ∅ ↔ ¬ { 𝑥 ∈ ℝ* ∣ ( 𝐴 < 𝑥 ∧ 𝑥 < 𝐵 ) } = ∅ )
4 rabn0 ⊢ ( { 𝑥 ∈ ℝ* ∣ ( 𝐴 < 𝑥 ∧ 𝑥 < 𝐵 ) } ≠ ∅ ↔ ∃ 𝑥 ∈ ℝ* ( 𝐴 < 𝑥 ∧ 𝑥 < 𝐵 ) )
5 3 4 bitr3i ⊢ ( ¬ { 𝑥 ∈ ℝ* ∣ ( 𝐴 < 𝑥 ∧ 𝑥 < 𝐵 ) } = ∅ ↔ ∃ 𝑥 ∈ ℝ* ( 𝐴 < 𝑥 ∧ 𝑥 < 𝐵 ) )
6 xrlttr ⊢ ( ( 𝐴 ∈ ℝ* ∧ 𝑥 ∈ ℝ* ∧ 𝐵 ∈ ℝ* ) → ( ( 𝐴 < 𝑥 ∧ 𝑥 < 𝐵 ) → 𝐴 < 𝐵 ) )
7 6 3com23 ⊢ ( ( 𝐴 ∈ ℝ* ∧ 𝐵 ∈ ℝ* ∧ 𝑥 ∈ ℝ* ) → ( ( 𝐴 < 𝑥 ∧ 𝑥 < 𝐵 ) → 𝐴 < 𝐵 ) )
8 7 3expa ⊢ ( ( ( 𝐴 ∈ ℝ* ∧ 𝐵 ∈ ℝ* ) ∧ 𝑥 ∈ ℝ* ) → ( ( 𝐴 < 𝑥 ∧ 𝑥 < 𝐵 ) → 𝐴 < 𝐵 ) )
9 8 rexlimdva ⊢ ( ( 𝐴 ∈ ℝ* ∧ 𝐵 ∈ ℝ* ) → ( ∃ 𝑥 ∈ ℝ* ( 𝐴 < 𝑥 ∧ 𝑥 < 𝐵 ) → 𝐴 < 𝐵 ) )
10 qbtwnxr ⊢ ( ( 𝐴 ∈ ℝ* ∧ 𝐵 ∈ ℝ* ∧ 𝐴 < 𝐵 ) → ∃ 𝑥 ∈ ℚ ( 𝐴 < 𝑥 ∧ 𝑥 < 𝐵 ) )
11 qre ⊢ ( 𝑥 ∈ ℚ → 𝑥 ∈ ℝ )
12 11 rexrd ⊢ ( 𝑥 ∈ ℚ → 𝑥 ∈ ℝ* )
13 12 anim1i ⊢ ( ( 𝑥 ∈ ℚ ∧ ( 𝐴 < 𝑥 ∧ 𝑥 < 𝐵 ) ) → ( 𝑥 ∈ ℝ* ∧ ( 𝐴 < 𝑥 ∧ 𝑥 < 𝐵 ) ) )
14 13 reximi2 ⊢ ( ∃ 𝑥 ∈ ℚ ( 𝐴 < 𝑥 ∧ 𝑥 < 𝐵 ) → ∃ 𝑥 ∈ ℝ* ( 𝐴 < 𝑥 ∧ 𝑥 < 𝐵 ) )
15 10 14 syl ⊢ ( ( 𝐴 ∈ ℝ* ∧ 𝐵 ∈ ℝ* ∧ 𝐴 < 𝐵 ) → ∃ 𝑥 ∈ ℝ* ( 𝐴 < 𝑥 ∧ 𝑥 < 𝐵 ) )
16 15 3expia ⊢ ( ( 𝐴 ∈ ℝ* ∧ 𝐵 ∈ ℝ* ) → ( 𝐴 < 𝐵 → ∃ 𝑥 ∈ ℝ* ( 𝐴 < 𝑥 ∧ 𝑥 < 𝐵 ) ) )
17 9 16 impbid ⊢ ( ( 𝐴 ∈ ℝ* ∧ 𝐵 ∈ ℝ* ) → ( ∃ 𝑥 ∈ ℝ* ( 𝐴 < 𝑥 ∧ 𝑥 < 𝐵 ) ↔ 𝐴 < 𝐵 ) )
18 5 17 syl5bb ⊢ ( ( 𝐴 ∈ ℝ* ∧ 𝐵 ∈ ℝ* ) → ( ¬ { 𝑥 ∈ ℝ* ∣ ( 𝐴 < 𝑥 ∧ 𝑥 < 𝐵 ) } = ∅ ↔ 𝐴 < 𝐵 ) )
19 xrltnle ⊢ ( ( 𝐴 ∈ ℝ* ∧ 𝐵 ∈ ℝ* ) → ( 𝐴 < 𝐵 ↔ ¬ 𝐵 ≤ 𝐴 ) )
20 18 19 bitrd ⊢ ( ( 𝐴 ∈ ℝ* ∧ 𝐵 ∈ ℝ* ) → ( ¬ { 𝑥 ∈ ℝ* ∣ ( 𝐴 < 𝑥 ∧ 𝑥 < 𝐵 ) } = ∅ ↔ ¬ 𝐵 ≤ 𝐴 ) )
21 20 con4bid ⊢ ( ( 𝐴 ∈ ℝ* ∧ 𝐵 ∈ ℝ* ) → ( { 𝑥 ∈ ℝ* ∣ ( 𝐴 < 𝑥 ∧ 𝑥 < 𝐵 ) } = ∅ ↔ 𝐵 ≤ 𝐴 ) )
22 2 21 bitrd ⊢ ( ( 𝐴 ∈ ℝ* ∧ 𝐵 ∈ ℝ* ) → ( ( 𝐴 (,) 𝐵 ) = ∅ ↔ 𝐵 ≤ 𝐴 ) )