Metamath Proof Explorer

Theorem ico0

Description: An empty open interval of extended reals. (Contributed by FL, 30-May-2014)

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

Proof

Step Hyp Ref Expression
1 icoval ⊢ ( ( 𝐴 ∈ ℝ* ∧ 𝐵 ∈ ℝ* ) → ( 𝐴 [,) 𝐵 ) = { 𝑥 ∈ ℝ* ∣ ( 𝐴 ≤ 𝑥 ∧ 𝑥 < 𝐵 ) } )
2 1 eqeq1d ⊢ ( ( 𝐴 ∈ ℝ* ∧ 𝐵 ∈ ℝ* ) → ( ( 𝐴 [,) 𝐵 ) = ∅ ↔ { 𝑥 ∈ ℝ* ∣ ( 𝐴 ≤ 𝑥 ∧ 𝑥 < 𝐵 ) } = ∅ ) )
3 df-ne ⊢ ( { 𝑥 ∈ ℝ* ∣ ( 𝐴 ≤ 𝑥 ∧ 𝑥 < 𝐵 ) } ≠ ∅ ↔ ¬ { 𝑥 ∈ ℝ* ∣ ( 𝐴 ≤ 𝑥 ∧ 𝑥 < 𝐵 ) } = ∅ )
4 rabn0 ⊢ ( { 𝑥 ∈ ℝ* ∣ ( 𝐴 ≤ 𝑥 ∧ 𝑥 < 𝐵 ) } ≠ ∅ ↔ ∃ 𝑥 ∈ ℝ* ( 𝐴 ≤ 𝑥 ∧ 𝑥 < 𝐵 ) )
5 3 4 bitr3i ⊢ ( ¬ { 𝑥 ∈ ℝ* ∣ ( 𝐴 ≤ 𝑥 ∧ 𝑥 < 𝐵 ) } = ∅ ↔ ∃ 𝑥 ∈ ℝ* ( 𝐴 ≤ 𝑥 ∧ 𝑥 < 𝐵 ) )
6 xrlelttr ⊢ ( ( 𝐴 ∈ ℝ* ∧ 𝑥 ∈ ℝ* ∧ 𝐵 ∈ ℝ* ) → ( ( 𝐴 ≤ 𝑥 ∧ 𝑥 < 𝐵 ) → 𝐴 < 𝐵 ) )
7 6 3com23 ⊢ ( ( 𝐴 ∈ ℝ* ∧ 𝐵 ∈ ℝ* ∧ 𝑥 ∈ ℝ* ) → ( ( 𝐴 ≤ 𝑥 ∧ 𝑥 < 𝐵 ) → 𝐴 < 𝐵 ) )
8 7 3expa ⊢ ( ( ( 𝐴 ∈ ℝ* ∧ 𝐵 ∈ ℝ* ) ∧ 𝑥 ∈ ℝ* ) → ( ( 𝐴 ≤ 𝑥 ∧ 𝑥 < 𝐵 ) → 𝐴 < 𝐵 ) )
9 8 rexlimdva ⊢ ( ( 𝐴 ∈ ℝ* ∧ 𝐵 ∈ ℝ* ) → ( ∃ 𝑥 ∈ ℝ* ( 𝐴 ≤ 𝑥 ∧ 𝑥 < 𝐵 ) → 𝐴 < 𝐵 ) )
10 qbtwnxr ⊢ ( ( 𝐴 ∈ ℝ* ∧ 𝐵 ∈ ℝ* ∧ 𝐴 < 𝐵 ) → ∃ 𝑥 ∈ ℚ ( 𝐴 < 𝑥 ∧ 𝑥 < 𝐵 ) )
11 qre ⊢ ( 𝑥 ∈ ℚ → 𝑥 ∈ ℝ )
12 11 rexrd ⊢ ( 𝑥 ∈ ℚ → 𝑥 ∈ ℝ* )
13 12 a1i ⊢ ( ( 𝑥 ∈ ℝ* ∧ ( 𝐴 ∈ ℝ* ∧ 𝐵 ∈ ℝ* ∧ 𝐴 < 𝐵 ) ) → ( 𝑥 ∈ ℚ → 𝑥 ∈ ℝ* ) )
14 simpr1 ⊢ ( ( 𝑥 ∈ ℝ* ∧ ( 𝐴 ∈ ℝ* ∧ 𝐵 ∈ ℝ* ∧ 𝐴 < 𝐵 ) ) → 𝐴 ∈ ℝ* )
15 simpl ⊢ ( ( 𝑥 ∈ ℝ* ∧ ( 𝐴 ∈ ℝ* ∧ 𝐵 ∈ ℝ* ∧ 𝐴 < 𝐵 ) ) → 𝑥 ∈ ℝ* )
16 xrltle ⊢ ( ( 𝐴 ∈ ℝ* ∧ 𝑥 ∈ ℝ* ) → ( 𝐴 < 𝑥 → 𝐴 ≤ 𝑥 ) )
17 14 15 16 syl2anc ⊢ ( ( 𝑥 ∈ ℝ* ∧ ( 𝐴 ∈ ℝ* ∧ 𝐵 ∈ ℝ* ∧ 𝐴 < 𝐵 ) ) → ( 𝐴 < 𝑥 → 𝐴 ≤ 𝑥 ) )
18 17 anim1d ⊢ ( ( 𝑥 ∈ ℝ* ∧ ( 𝐴 ∈ ℝ* ∧ 𝐵 ∈ ℝ* ∧ 𝐴 < 𝐵 ) ) → ( ( 𝐴 < 𝑥 ∧ 𝑥 < 𝐵 ) → ( 𝐴 ≤ 𝑥 ∧ 𝑥 < 𝐵 ) ) )
19 13 18 anim12d ⊢ ( ( 𝑥 ∈ ℝ* ∧ ( 𝐴 ∈ ℝ* ∧ 𝐵 ∈ ℝ* ∧ 𝐴 < 𝐵 ) ) → ( ( 𝑥 ∈ ℚ ∧ ( 𝐴 < 𝑥 ∧ 𝑥 < 𝐵 ) ) → ( 𝑥 ∈ ℝ* ∧ ( 𝐴 ≤ 𝑥 ∧ 𝑥 < 𝐵 ) ) ) )
20 19 ex ⊢ ( 𝑥 ∈ ℝ* → ( ( 𝐴 ∈ ℝ* ∧ 𝐵 ∈ ℝ* ∧ 𝐴 < 𝐵 ) → ( ( 𝑥 ∈ ℚ ∧ ( 𝐴 < 𝑥 ∧ 𝑥 < 𝐵 ) ) → ( 𝑥 ∈ ℝ* ∧ ( 𝐴 ≤ 𝑥 ∧ 𝑥 < 𝐵 ) ) ) ) )
21 12 20 syl ⊢ ( 𝑥 ∈ ℚ → ( ( 𝐴 ∈ ℝ* ∧ 𝐵 ∈ ℝ* ∧ 𝐴 < 𝐵 ) → ( ( 𝑥 ∈ ℚ ∧ ( 𝐴 < 𝑥 ∧ 𝑥 < 𝐵 ) ) → ( 𝑥 ∈ ℝ* ∧ ( 𝐴 ≤ 𝑥 ∧ 𝑥 < 𝐵 ) ) ) ) )
22 21 adantr ⊢ ( ( 𝑥 ∈ ℚ ∧ ( 𝐴 < 𝑥 ∧ 𝑥 < 𝐵 ) ) → ( ( 𝐴 ∈ ℝ* ∧ 𝐵 ∈ ℝ* ∧ 𝐴 < 𝐵 ) → ( ( 𝑥 ∈ ℚ ∧ ( 𝐴 < 𝑥 ∧ 𝑥 < 𝐵 ) ) → ( 𝑥 ∈ ℝ* ∧ ( 𝐴 ≤ 𝑥 ∧ 𝑥 < 𝐵 ) ) ) ) )
23 22 pm2.43b ⊢ ( ( 𝐴 ∈ ℝ* ∧ 𝐵 ∈ ℝ* ∧ 𝐴 < 𝐵 ) → ( ( 𝑥 ∈ ℚ ∧ ( 𝐴 < 𝑥 ∧ 𝑥 < 𝐵 ) ) → ( 𝑥 ∈ ℝ* ∧ ( 𝐴 ≤ 𝑥 ∧ 𝑥 < 𝐵 ) ) ) )
24 23 reximdv2 ⊢ ( ( 𝐴 ∈ ℝ* ∧ 𝐵 ∈ ℝ* ∧ 𝐴 < 𝐵 ) → ( ∃ 𝑥 ∈ ℚ ( 𝐴 < 𝑥 ∧ 𝑥 < 𝐵 ) → ∃ 𝑥 ∈ ℝ* ( 𝐴 ≤ 𝑥 ∧ 𝑥 < 𝐵 ) ) )
25 10 24 mpd ⊢ ( ( 𝐴 ∈ ℝ* ∧ 𝐵 ∈ ℝ* ∧ 𝐴 < 𝐵 ) → ∃ 𝑥 ∈ ℝ* ( 𝐴 ≤ 𝑥 ∧ 𝑥 < 𝐵 ) )
26 25 3expia ⊢ ( ( 𝐴 ∈ ℝ* ∧ 𝐵 ∈ ℝ* ) → ( 𝐴 < 𝐵 → ∃ 𝑥 ∈ ℝ* ( 𝐴 ≤ 𝑥 ∧ 𝑥 < 𝐵 ) ) )
27 9 26 impbid ⊢ ( ( 𝐴 ∈ ℝ* ∧ 𝐵 ∈ ℝ* ) → ( ∃ 𝑥 ∈ ℝ* ( 𝐴 ≤ 𝑥 ∧ 𝑥 < 𝐵 ) ↔ 𝐴 < 𝐵 ) )
28 5 27 syl5bb ⊢ ( ( 𝐴 ∈ ℝ* ∧ 𝐵 ∈ ℝ* ) → ( ¬ { 𝑥 ∈ ℝ* ∣ ( 𝐴 ≤ 𝑥 ∧ 𝑥 < 𝐵 ) } = ∅ ↔ 𝐴 < 𝐵 ) )
29 xrltnle ⊢ ( ( 𝐴 ∈ ℝ* ∧ 𝐵 ∈ ℝ* ) → ( 𝐴 < 𝐵 ↔ ¬ 𝐵 ≤ 𝐴 ) )
30 28 29 bitrd ⊢ ( ( 𝐴 ∈ ℝ* ∧ 𝐵 ∈ ℝ* ) → ( ¬ { 𝑥 ∈ ℝ* ∣ ( 𝐴 ≤ 𝑥 ∧ 𝑥 < 𝐵 ) } = ∅ ↔ ¬ 𝐵 ≤ 𝐴 ) )
31 30 con4bid ⊢ ( ( 𝐴 ∈ ℝ* ∧ 𝐵 ∈ ℝ* ) → ( { 𝑥 ∈ ℝ* ∣ ( 𝐴 ≤ 𝑥 ∧ 𝑥 < 𝐵 ) } = ∅ ↔ 𝐵 ≤ 𝐴 ) )
32 2 31 bitrd ⊢ ( ( 𝐴 ∈ ℝ* ∧ 𝐵 ∈ ℝ* ) → ( ( 𝐴 [,) 𝐵 ) = ∅ ↔ 𝐵 ≤ 𝐴 ) )