Metamath Proof Explorer

Theorem icoiccdif

Description: Left-closed right-open interval gotten by a closed iterval taking away the upper bound. (Contributed by Glauco Siliprandi, 11-Dec-2019)

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

Proof

Step Hyp Ref Expression
1 icossicc ⊢ ( 𝐴 [,) 𝐵 ) ⊆ ( 𝐴 [,] 𝐵 )
2 1 a1i ⊢ ( ( 𝐴 ∈ ℝ* ∧ 𝐵 ∈ ℝ* ) → ( 𝐴 [,) 𝐵 ) ⊆ ( 𝐴 [,] 𝐵 ) )
3 2 sselda ⊢ ( ( ( 𝐴 ∈ ℝ* ∧ 𝐵 ∈ ℝ* ) ∧ 𝑥 ∈ ( 𝐴 [,) 𝐵 ) ) → 𝑥 ∈ ( 𝐴 [,] 𝐵 ) )
4 elico1 ⊢ ( ( 𝐴 ∈ ℝ* ∧ 𝐵 ∈ ℝ* ) → ( 𝑥 ∈ ( 𝐴 [,) 𝐵 ) ↔ ( 𝑥 ∈ ℝ* ∧ 𝐴 ≤ 𝑥 ∧ 𝑥 < 𝐵 ) ) )
5 4 biimpa ⊢ ( ( ( 𝐴 ∈ ℝ* ∧ 𝐵 ∈ ℝ* ) ∧ 𝑥 ∈ ( 𝐴 [,) 𝐵 ) ) → ( 𝑥 ∈ ℝ* ∧ 𝐴 ≤ 𝑥 ∧ 𝑥 < 𝐵 ) )
6 5 simp1d ⊢ ( ( ( 𝐴 ∈ ℝ* ∧ 𝐵 ∈ ℝ* ) ∧ 𝑥 ∈ ( 𝐴 [,) 𝐵 ) ) → 𝑥 ∈ ℝ* )
7 simplr ⊢ ( ( ( 𝐴 ∈ ℝ* ∧ 𝐵 ∈ ℝ* ) ∧ 𝑥 ∈ ( 𝐴 [,) 𝐵 ) ) → 𝐵 ∈ ℝ* )
8 5 simp3d ⊢ ( ( ( 𝐴 ∈ ℝ* ∧ 𝐵 ∈ ℝ* ) ∧ 𝑥 ∈ ( 𝐴 [,) 𝐵 ) ) → 𝑥 < 𝐵 )
9 xrltne ⊢ ( ( 𝑥 ∈ ℝ* ∧ 𝐵 ∈ ℝ* ∧ 𝑥 < 𝐵 ) → 𝐵 ≠ 𝑥 )
10 6 7 8 9 syl3anc ⊢ ( ( ( 𝐴 ∈ ℝ* ∧ 𝐵 ∈ ℝ* ) ∧ 𝑥 ∈ ( 𝐴 [,) 𝐵 ) ) → 𝐵 ≠ 𝑥 )
11 10 necomd ⊢ ( ( ( 𝐴 ∈ ℝ* ∧ 𝐵 ∈ ℝ* ) ∧ 𝑥 ∈ ( 𝐴 [,) 𝐵 ) ) → 𝑥 ≠ 𝐵 )
12 11 neneqd ⊢ ( ( ( 𝐴 ∈ ℝ* ∧ 𝐵 ∈ ℝ* ) ∧ 𝑥 ∈ ( 𝐴 [,) 𝐵 ) ) → ¬ 𝑥 = 𝐵 )
13 velsn ⊢ ( 𝑥 ∈ { 𝐵 } ↔ 𝑥 = 𝐵 )
14 12 13 sylnibr ⊢ ( ( ( 𝐴 ∈ ℝ* ∧ 𝐵 ∈ ℝ* ) ∧ 𝑥 ∈ ( 𝐴 [,) 𝐵 ) ) → ¬ 𝑥 ∈ { 𝐵 } )
15 3 14 eldifd ⊢ ( ( ( 𝐴 ∈ ℝ* ∧ 𝐵 ∈ ℝ* ) ∧ 𝑥 ∈ ( 𝐴 [,) 𝐵 ) ) → 𝑥 ∈ ( ( 𝐴 [,] 𝐵 ) ∖ { 𝐵 } ) )
16 15 ex ⊢ ( ( 𝐴 ∈ ℝ* ∧ 𝐵 ∈ ℝ* ) → ( 𝑥 ∈ ( 𝐴 [,) 𝐵 ) → 𝑥 ∈ ( ( 𝐴 [,] 𝐵 ) ∖ { 𝐵 } ) ) )
17 16 ssrdv ⊢ ( ( 𝐴 ∈ ℝ* ∧ 𝐵 ∈ ℝ* ) → ( 𝐴 [,) 𝐵 ) ⊆ ( ( 𝐴 [,] 𝐵 ) ∖ { 𝐵 } ) )
18 simpll ⊢ ( ( ( 𝐴 ∈ ℝ* ∧ 𝐵 ∈ ℝ* ) ∧ 𝑥 ∈ ( ( 𝐴 [,] 𝐵 ) ∖ { 𝐵 } ) ) → 𝐴 ∈ ℝ* )
19 simplr ⊢ ( ( ( 𝐴 ∈ ℝ* ∧ 𝐵 ∈ ℝ* ) ∧ 𝑥 ∈ ( ( 𝐴 [,] 𝐵 ) ∖ { 𝐵 } ) ) → 𝐵 ∈ ℝ* )
20 eldifi ⊢ ( 𝑥 ∈ ( ( 𝐴 [,] 𝐵 ) ∖ { 𝐵 } ) → 𝑥 ∈ ( 𝐴 [,] 𝐵 ) )
21 eliccxr ⊢ ( 𝑥 ∈ ( 𝐴 [,] 𝐵 ) → 𝑥 ∈ ℝ* )
22 20 21 syl ⊢ ( 𝑥 ∈ ( ( 𝐴 [,] 𝐵 ) ∖ { 𝐵 } ) → 𝑥 ∈ ℝ* )
23 22 adantl ⊢ ( ( ( 𝐴 ∈ ℝ* ∧ 𝐵 ∈ ℝ* ) ∧ 𝑥 ∈ ( ( 𝐴 [,] 𝐵 ) ∖ { 𝐵 } ) ) → 𝑥 ∈ ℝ* )
24 20 adantl ⊢ ( ( ( 𝐴 ∈ ℝ* ∧ 𝐵 ∈ ℝ* ) ∧ 𝑥 ∈ ( ( 𝐴 [,] 𝐵 ) ∖ { 𝐵 } ) ) → 𝑥 ∈ ( 𝐴 [,] 𝐵 ) )
25 elicc1 ⊢ ( ( 𝐴 ∈ ℝ* ∧ 𝐵 ∈ ℝ* ) → ( 𝑥 ∈ ( 𝐴 [,] 𝐵 ) ↔ ( 𝑥 ∈ ℝ* ∧ 𝐴 ≤ 𝑥 ∧ 𝑥 ≤ 𝐵 ) ) )
26 25 adantr ⊢ ( ( ( 𝐴 ∈ ℝ* ∧ 𝐵 ∈ ℝ* ) ∧ 𝑥 ∈ ( ( 𝐴 [,] 𝐵 ) ∖ { 𝐵 } ) ) → ( 𝑥 ∈ ( 𝐴 [,] 𝐵 ) ↔ ( 𝑥 ∈ ℝ* ∧ 𝐴 ≤ 𝑥 ∧ 𝑥 ≤ 𝐵 ) ) )
27 24 26 mpbid ⊢ ( ( ( 𝐴 ∈ ℝ* ∧ 𝐵 ∈ ℝ* ) ∧ 𝑥 ∈ ( ( 𝐴 [,] 𝐵 ) ∖ { 𝐵 } ) ) → ( 𝑥 ∈ ℝ* ∧ 𝐴 ≤ 𝑥 ∧ 𝑥 ≤ 𝐵 ) )
28 27 simp2d ⊢ ( ( ( 𝐴 ∈ ℝ* ∧ 𝐵 ∈ ℝ* ) ∧ 𝑥 ∈ ( ( 𝐴 [,] 𝐵 ) ∖ { 𝐵 } ) ) → 𝐴 ≤ 𝑥 )
29 eldifsni ⊢ ( 𝑥 ∈ ( ( 𝐴 [,] 𝐵 ) ∖ { 𝐵 } ) → 𝑥 ≠ 𝐵 )
30 29 necomd ⊢ ( 𝑥 ∈ ( ( 𝐴 [,] 𝐵 ) ∖ { 𝐵 } ) → 𝐵 ≠ 𝑥 )
31 30 adantl ⊢ ( ( ( 𝐴 ∈ ℝ* ∧ 𝐵 ∈ ℝ* ) ∧ 𝑥 ∈ ( ( 𝐴 [,] 𝐵 ) ∖ { 𝐵 } ) ) → 𝐵 ≠ 𝑥 )
32 27 simp3d ⊢ ( ( ( 𝐴 ∈ ℝ* ∧ 𝐵 ∈ ℝ* ) ∧ 𝑥 ∈ ( ( 𝐴 [,] 𝐵 ) ∖ { 𝐵 } ) ) → 𝑥 ≤ 𝐵 )
33 xrleltne ⊢ ( ( 𝑥 ∈ ℝ* ∧ 𝐵 ∈ ℝ* ∧ 𝑥 ≤ 𝐵 ) → ( 𝑥 < 𝐵 ↔ 𝐵 ≠ 𝑥 ) )
34 23 19 32 33 syl3anc ⊢ ( ( ( 𝐴 ∈ ℝ* ∧ 𝐵 ∈ ℝ* ) ∧ 𝑥 ∈ ( ( 𝐴 [,] 𝐵 ) ∖ { 𝐵 } ) ) → ( 𝑥 < 𝐵 ↔ 𝐵 ≠ 𝑥 ) )
35 31 34 mpbird ⊢ ( ( ( 𝐴 ∈ ℝ* ∧ 𝐵 ∈ ℝ* ) ∧ 𝑥 ∈ ( ( 𝐴 [,] 𝐵 ) ∖ { 𝐵 } ) ) → 𝑥 < 𝐵 )
36 18 19 23 28 35 elicod ⊢ ( ( ( 𝐴 ∈ ℝ* ∧ 𝐵 ∈ ℝ* ) ∧ 𝑥 ∈ ( ( 𝐴 [,] 𝐵 ) ∖ { 𝐵 } ) ) → 𝑥 ∈ ( 𝐴 [,) 𝐵 ) )
37 17 36 eqelssd ⊢ ( ( 𝐴 ∈ ℝ* ∧ 𝐵 ∈ ℝ* ) → ( 𝐴 [,) 𝐵 ) = ( ( 𝐴 [,] 𝐵 ) ∖ { 𝐵 } ) )