Metamath Proof Explorer

Theorem icc0

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

Ref Expression
Assertion icc0 ( ( 𝐴 ∈ ℝ* ∧ 𝐵 ∈ ℝ* ) → ( ( 𝐴 [,] 𝐵 ) = ∅ ↔ 𝐵 < 𝐴 ) )

Proof

Step Hyp Ref Expression
1 iccval ⊢ ( ( 𝐴 ∈ ℝ* ∧ 𝐵 ∈ ℝ* ) → ( 𝐴 [,] 𝐵 ) = { 𝑥 ∈ ℝ* ∣ ( 𝐴 ≤ 𝑥 ∧ 𝑥 ≤ 𝐵 ) } )
2 1 eqeq1d ⊢ ( ( 𝐴 ∈ ℝ* ∧ 𝐵 ∈ ℝ* ) → ( ( 𝐴 [,] 𝐵 ) = ∅ ↔ { 𝑥 ∈ ℝ* ∣ ( 𝐴 ≤ 𝑥 ∧ 𝑥 ≤ 𝐵 ) } = ∅ ) )
3 df-ne ⊢ ( { 𝑥 ∈ ℝ* ∣ ( 𝐴 ≤ 𝑥 ∧ 𝑥 ≤ 𝐵 ) } ≠ ∅ ↔ ¬ { 𝑥 ∈ ℝ* ∣ ( 𝐴 ≤ 𝑥 ∧ 𝑥 ≤ 𝐵 ) } = ∅ )
4 rabn0 ⊢ ( { 𝑥 ∈ ℝ* ∣ ( 𝐴 ≤ 𝑥 ∧ 𝑥 ≤ 𝐵 ) } ≠ ∅ ↔ ∃ 𝑥 ∈ ℝ* ( 𝐴 ≤ 𝑥 ∧ 𝑥 ≤ 𝐵 ) )
5 3 4 bitr3i ⊢ ( ¬ { 𝑥 ∈ ℝ* ∣ ( 𝐴 ≤ 𝑥 ∧ 𝑥 ≤ 𝐵 ) } = ∅ ↔ ∃ 𝑥 ∈ ℝ* ( 𝐴 ≤ 𝑥 ∧ 𝑥 ≤ 𝐵 ) )
6 xrletr ⊢ ( ( 𝐴 ∈ ℝ* ∧ 𝑥 ∈ ℝ* ∧ 𝐵 ∈ ℝ* ) → ( ( 𝐴 ≤ 𝑥 ∧ 𝑥 ≤ 𝐵 ) → 𝐴 ≤ 𝐵 ) )
7 6 3com23 ⊢ ( ( 𝐴 ∈ ℝ* ∧ 𝐵 ∈ ℝ* ∧ 𝑥 ∈ ℝ* ) → ( ( 𝐴 ≤ 𝑥 ∧ 𝑥 ≤ 𝐵 ) → 𝐴 ≤ 𝐵 ) )
8 7 3expa ⊢ ( ( ( 𝐴 ∈ ℝ* ∧ 𝐵 ∈ ℝ* ) ∧ 𝑥 ∈ ℝ* ) → ( ( 𝐴 ≤ 𝑥 ∧ 𝑥 ≤ 𝐵 ) → 𝐴 ≤ 𝐵 ) )
9 8 rexlimdva ⊢ ( ( 𝐴 ∈ ℝ* ∧ 𝐵 ∈ ℝ* ) → ( ∃ 𝑥 ∈ ℝ* ( 𝐴 ≤ 𝑥 ∧ 𝑥 ≤ 𝐵 ) → 𝐴 ≤ 𝐵 ) )
10 simp2 ⊢ ( ( 𝐴 ∈ ℝ* ∧ 𝐵 ∈ ℝ* ∧ 𝐴 ≤ 𝐵 ) → 𝐵 ∈ ℝ* )
11 simp3 ⊢ ( ( 𝐴 ∈ ℝ* ∧ 𝐵 ∈ ℝ* ∧ 𝐴 ≤ 𝐵 ) → 𝐴 ≤ 𝐵 )
12 xrleid ⊢ ( 𝐵 ∈ ℝ* → 𝐵 ≤ 𝐵 )
13 12 3ad2ant2 ⊢ ( ( 𝐴 ∈ ℝ* ∧ 𝐵 ∈ ℝ* ∧ 𝐴 ≤ 𝐵 ) → 𝐵 ≤ 𝐵 )
14 breq2 ⊢ ( 𝑥 = 𝐵 → ( 𝐴 ≤ 𝑥 ↔ 𝐴 ≤ 𝐵 ) )
15 breq1 ⊢ ( 𝑥 = 𝐵 → ( 𝑥 ≤ 𝐵 ↔ 𝐵 ≤ 𝐵 ) )
16 14 15 anbi12d ⊢ ( 𝑥 = 𝐵 → ( ( 𝐴 ≤ 𝑥 ∧ 𝑥 ≤ 𝐵 ) ↔ ( 𝐴 ≤ 𝐵 ∧ 𝐵 ≤ 𝐵 ) ) )
17 16 rspcev ⊢ ( ( 𝐵 ∈ ℝ* ∧ ( 𝐴 ≤ 𝐵 ∧ 𝐵 ≤ 𝐵 ) ) → ∃ 𝑥 ∈ ℝ* ( 𝐴 ≤ 𝑥 ∧ 𝑥 ≤ 𝐵 ) )
18 10 11 13 17 syl12anc ⊢ ( ( 𝐴 ∈ ℝ* ∧ 𝐵 ∈ ℝ* ∧ 𝐴 ≤ 𝐵 ) → ∃ 𝑥 ∈ ℝ* ( 𝐴 ≤ 𝑥 ∧ 𝑥 ≤ 𝐵 ) )
19 18 3expia ⊢ ( ( 𝐴 ∈ ℝ* ∧ 𝐵 ∈ ℝ* ) → ( 𝐴 ≤ 𝐵 → ∃ 𝑥 ∈ ℝ* ( 𝐴 ≤ 𝑥 ∧ 𝑥 ≤ 𝐵 ) ) )
20 9 19 impbid ⊢ ( ( 𝐴 ∈ ℝ* ∧ 𝐵 ∈ ℝ* ) → ( ∃ 𝑥 ∈ ℝ* ( 𝐴 ≤ 𝑥 ∧ 𝑥 ≤ 𝐵 ) ↔ 𝐴 ≤ 𝐵 ) )
21 5 20 bitrid ⊢ ( ( 𝐴 ∈ ℝ* ∧ 𝐵 ∈ ℝ* ) → ( ¬ { 𝑥 ∈ ℝ* ∣ ( 𝐴 ≤ 𝑥 ∧ 𝑥 ≤ 𝐵 ) } = ∅ ↔ 𝐴 ≤ 𝐵 ) )
22 xrlenlt ⊢ ( ( 𝐴 ∈ ℝ* ∧ 𝐵 ∈ ℝ* ) → ( 𝐴 ≤ 𝐵 ↔ ¬ 𝐵 < 𝐴 ) )
23 21 22 bitrd ⊢ ( ( 𝐴 ∈ ℝ* ∧ 𝐵 ∈ ℝ* ) → ( ¬ { 𝑥 ∈ ℝ* ∣ ( 𝐴 ≤ 𝑥 ∧ 𝑥 ≤ 𝐵 ) } = ∅ ↔ ¬ 𝐵 < 𝐴 ) )
24 23 con4bid ⊢ ( ( 𝐴 ∈ ℝ* ∧ 𝐵 ∈ ℝ* ) → ( { 𝑥 ∈ ℝ* ∣ ( 𝐴 ≤ 𝑥 ∧ 𝑥 ≤ 𝐵 ) } = ∅ ↔ 𝐵 < 𝐴 ) )
25 2 24 bitrd ⊢ ( ( 𝐴 ∈ ℝ* ∧ 𝐵 ∈ ℝ* ) → ( ( 𝐴 [,] 𝐵 ) = ∅ ↔ 𝐵 < 𝐴 ) )