Metamath Proof Explorer

Theorem iccdifprioo

Description: An open interval is the closed interval without the bounds. (Contributed by Glauco Siliprandi, 11-Dec-2019)

Ref Expression
Assertion iccdifprioo ( ( 𝐴 ∈ ℝ* ∧ 𝐵 ∈ ℝ* ) → ( ( 𝐴 [,] 𝐵 ) ∖ { 𝐴 , 𝐵 } ) = ( 𝐴 (,) 𝐵 ) )

Proof

Step Hyp Ref Expression
1 prunioo ⊢ ( ( 𝐴 ∈ ℝ* ∧ 𝐵 ∈ ℝ* ∧ 𝐴 ≤ 𝐵 ) → ( ( 𝐴 (,) 𝐵 ) ∪ { 𝐴 , 𝐵 } ) = ( 𝐴 [,] 𝐵 ) )
2 1 eqcomd ⊢ ( ( 𝐴 ∈ ℝ* ∧ 𝐵 ∈ ℝ* ∧ 𝐴 ≤ 𝐵 ) → ( 𝐴 [,] 𝐵 ) = ( ( 𝐴 (,) 𝐵 ) ∪ { 𝐴 , 𝐵 } ) )
3 2 difeq1d ⊢ ( ( 𝐴 ∈ ℝ* ∧ 𝐵 ∈ ℝ* ∧ 𝐴 ≤ 𝐵 ) → ( ( 𝐴 [,] 𝐵 ) ∖ { 𝐴 , 𝐵 } ) = ( ( ( 𝐴 (,) 𝐵 ) ∪ { 𝐴 , 𝐵 } ) ∖ { 𝐴 , 𝐵 } ) )
4 difun2 ⊢ ( ( ( 𝐴 (,) 𝐵 ) ∪ { 𝐴 , 𝐵 } ) ∖ { 𝐴 , 𝐵 } ) = ( ( 𝐴 (,) 𝐵 ) ∖ { 𝐴 , 𝐵 } )
5 iooinlbub ⊢ ( ( 𝐴 (,) 𝐵 ) ∩ { 𝐴 , 𝐵 } ) = ∅
6 disj3 ⊢ ( ( ( 𝐴 (,) 𝐵 ) ∩ { 𝐴 , 𝐵 } ) = ∅ ↔ ( 𝐴 (,) 𝐵 ) = ( ( 𝐴 (,) 𝐵 ) ∖ { 𝐴 , 𝐵 } ) )
7 5 6 mpbi ⊢ ( 𝐴 (,) 𝐵 ) = ( ( 𝐴 (,) 𝐵 ) ∖ { 𝐴 , 𝐵 } )
8 4 7 eqtr4i ⊢ ( ( ( 𝐴 (,) 𝐵 ) ∪ { 𝐴 , 𝐵 } ) ∖ { 𝐴 , 𝐵 } ) = ( 𝐴 (,) 𝐵 )
9 3 8 eqtrdi ⊢ ( ( 𝐴 ∈ ℝ* ∧ 𝐵 ∈ ℝ* ∧ 𝐴 ≤ 𝐵 ) → ( ( 𝐴 [,] 𝐵 ) ∖ { 𝐴 , 𝐵 } ) = ( 𝐴 (,) 𝐵 ) )
10 9 3expa ⊢ ( ( ( 𝐴 ∈ ℝ* ∧ 𝐵 ∈ ℝ* ) ∧ 𝐴 ≤ 𝐵 ) → ( ( 𝐴 [,] 𝐵 ) ∖ { 𝐴 , 𝐵 } ) = ( 𝐴 (,) 𝐵 ) )
11 difssd ⊢ ( ( ( 𝐴 ∈ ℝ* ∧ 𝐵 ∈ ℝ* ) ∧ ¬ 𝐴 ≤ 𝐵 ) → ( ( 𝐴 [,] 𝐵 ) ∖ { 𝐴 , 𝐵 } ) ⊆ ( 𝐴 [,] 𝐵 ) )
12 simpr ⊢ ( ( ( 𝐴 ∈ ℝ* ∧ 𝐵 ∈ ℝ* ) ∧ ¬ 𝐴 ≤ 𝐵 ) → ¬ 𝐴 ≤ 𝐵 )
13 xrlenlt ⊢ ( ( 𝐴 ∈ ℝ* ∧ 𝐵 ∈ ℝ* ) → ( 𝐴 ≤ 𝐵 ↔ ¬ 𝐵 < 𝐴 ) )
14 13 adantr ⊢ ( ( ( 𝐴 ∈ ℝ* ∧ 𝐵 ∈ ℝ* ) ∧ ¬ 𝐴 ≤ 𝐵 ) → ( 𝐴 ≤ 𝐵 ↔ ¬ 𝐵 < 𝐴 ) )
15 12 14 mtbid ⊢ ( ( ( 𝐴 ∈ ℝ* ∧ 𝐵 ∈ ℝ* ) ∧ ¬ 𝐴 ≤ 𝐵 ) → ¬ ¬ 𝐵 < 𝐴 )
16 15 notnotrd ⊢ ( ( ( 𝐴 ∈ ℝ* ∧ 𝐵 ∈ ℝ* ) ∧ ¬ 𝐴 ≤ 𝐵 ) → 𝐵 < 𝐴 )
17 icc0 ⊢ ( ( 𝐴 ∈ ℝ* ∧ 𝐵 ∈ ℝ* ) → ( ( 𝐴 [,] 𝐵 ) = ∅ ↔ 𝐵 < 𝐴 ) )
18 17 adantr ⊢ ( ( ( 𝐴 ∈ ℝ* ∧ 𝐵 ∈ ℝ* ) ∧ ¬ 𝐴 ≤ 𝐵 ) → ( ( 𝐴 [,] 𝐵 ) = ∅ ↔ 𝐵 < 𝐴 ) )
19 16 18 mpbird ⊢ ( ( ( 𝐴 ∈ ℝ* ∧ 𝐵 ∈ ℝ* ) ∧ ¬ 𝐴 ≤ 𝐵 ) → ( 𝐴 [,] 𝐵 ) = ∅ )
20 11 19 sseqtrd ⊢ ( ( ( 𝐴 ∈ ℝ* ∧ 𝐵 ∈ ℝ* ) ∧ ¬ 𝐴 ≤ 𝐵 ) → ( ( 𝐴 [,] 𝐵 ) ∖ { 𝐴 , 𝐵 } ) ⊆ ∅ )
21 ss0 ⊢ ( ( ( 𝐴 [,] 𝐵 ) ∖ { 𝐴 , 𝐵 } ) ⊆ ∅ → ( ( 𝐴 [,] 𝐵 ) ∖ { 𝐴 , 𝐵 } ) = ∅ )
22 20 21 syl ⊢ ( ( ( 𝐴 ∈ ℝ* ∧ 𝐵 ∈ ℝ* ) ∧ ¬ 𝐴 ≤ 𝐵 ) → ( ( 𝐴 [,] 𝐵 ) ∖ { 𝐴 , 𝐵 } ) = ∅ )
23 simplr ⊢ ( ( ( 𝐴 ∈ ℝ* ∧ 𝐵 ∈ ℝ* ) ∧ ¬ 𝐴 ≤ 𝐵 ) → 𝐵 ∈ ℝ* )
24 simpll ⊢ ( ( ( 𝐴 ∈ ℝ* ∧ 𝐵 ∈ ℝ* ) ∧ ¬ 𝐴 ≤ 𝐵 ) → 𝐴 ∈ ℝ* )
25 23 24 16 xrltled ⊢ ( ( ( 𝐴 ∈ ℝ* ∧ 𝐵 ∈ ℝ* ) ∧ ¬ 𝐴 ≤ 𝐵 ) → 𝐵 ≤ 𝐴 )
26 ioo0 ⊢ ( ( 𝐴 ∈ ℝ* ∧ 𝐵 ∈ ℝ* ) → ( ( 𝐴 (,) 𝐵 ) = ∅ ↔ 𝐵 ≤ 𝐴 ) )
27 26 adantr ⊢ ( ( ( 𝐴 ∈ ℝ* ∧ 𝐵 ∈ ℝ* ) ∧ ¬ 𝐴 ≤ 𝐵 ) → ( ( 𝐴 (,) 𝐵 ) = ∅ ↔ 𝐵 ≤ 𝐴 ) )
28 25 27 mpbird ⊢ ( ( ( 𝐴 ∈ ℝ* ∧ 𝐵 ∈ ℝ* ) ∧ ¬ 𝐴 ≤ 𝐵 ) → ( 𝐴 (,) 𝐵 ) = ∅ )
29 22 28 eqtr4d ⊢ ( ( ( 𝐴 ∈ ℝ* ∧ 𝐵 ∈ ℝ* ) ∧ ¬ 𝐴 ≤ 𝐵 ) → ( ( 𝐴 [,] 𝐵 ) ∖ { 𝐴 , 𝐵 } ) = ( 𝐴 (,) 𝐵 ) )
30 10 29 pm2.61dan ⊢ ( ( 𝐴 ∈ ℝ* ∧ 𝐵 ∈ ℝ* ) → ( ( 𝐴 [,] 𝐵 ) ∖ { 𝐴 , 𝐵 } ) = ( 𝐴 (,) 𝐵 ) )