Metamath Proof Explorer

Theorem ioc0

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

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

Proof

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