Metamath Proof Explorer


Theorem snunioo

Description: The closure of one end of an open real interval. (Contributed by Paul Chapman, 15-Mar-2008) (Proof shortened by Mario Carneiro, 16-Jun-2014)

Ref Expression
Assertion snunioo ( ( 𝐴 ∈ ℝ*𝐵 ∈ ℝ*𝐴 < 𝐵 ) → ( { 𝐴 } ∪ ( 𝐴 (,) 𝐵 ) ) = ( 𝐴 [,) 𝐵 ) )

Proof

Step Hyp Ref Expression
1 simp1 ( ( 𝐴 ∈ ℝ*𝐵 ∈ ℝ*𝐴 < 𝐵 ) → 𝐴 ∈ ℝ* )
2 iccid ( 𝐴 ∈ ℝ* → ( 𝐴 [,] 𝐴 ) = { 𝐴 } )
3 1 2 syl ( ( 𝐴 ∈ ℝ*𝐵 ∈ ℝ*𝐴 < 𝐵 ) → ( 𝐴 [,] 𝐴 ) = { 𝐴 } )
4 3 uneq1d ( ( 𝐴 ∈ ℝ*𝐵 ∈ ℝ*𝐴 < 𝐵 ) → ( ( 𝐴 [,] 𝐴 ) ∪ ( 𝐴 (,) 𝐵 ) ) = ( { 𝐴 } ∪ ( 𝐴 (,) 𝐵 ) ) )
5 simp2 ( ( 𝐴 ∈ ℝ*𝐵 ∈ ℝ*𝐴 < 𝐵 ) → 𝐵 ∈ ℝ* )
6 1 xrleidd ( ( 𝐴 ∈ ℝ*𝐵 ∈ ℝ*𝐴 < 𝐵 ) → 𝐴𝐴 )
7 simp3 ( ( 𝐴 ∈ ℝ*𝐵 ∈ ℝ*𝐴 < 𝐵 ) → 𝐴 < 𝐵 )
8 df-icc [,] = ( 𝑥 ∈ ℝ* , 𝑦 ∈ ℝ* ↦ { 𝑧 ∈ ℝ* ∣ ( 𝑥𝑧𝑧𝑦 ) } )
9 df-ioo (,) = ( 𝑥 ∈ ℝ* , 𝑦 ∈ ℝ* ↦ { 𝑧 ∈ ℝ* ∣ ( 𝑥 < 𝑧𝑧 < 𝑦 ) } )
10 xrltnle ( ( 𝐴 ∈ ℝ*𝑤 ∈ ℝ* ) → ( 𝐴 < 𝑤 ↔ ¬ 𝑤𝐴 ) )
11 df-ico [,) = ( 𝑥 ∈ ℝ* , 𝑦 ∈ ℝ* ↦ { 𝑧 ∈ ℝ* ∣ ( 𝑥𝑧𝑧 < 𝑦 ) } )
12 xrlelttr ( ( 𝑤 ∈ ℝ*𝐴 ∈ ℝ*𝐵 ∈ ℝ* ) → ( ( 𝑤𝐴𝐴 < 𝐵 ) → 𝑤 < 𝐵 ) )
13 xrltle ( ( 𝐴 ∈ ℝ*𝑤 ∈ ℝ* ) → ( 𝐴 < 𝑤𝐴𝑤 ) )
14 13 3adant1 ( ( 𝐴 ∈ ℝ*𝐴 ∈ ℝ*𝑤 ∈ ℝ* ) → ( 𝐴 < 𝑤𝐴𝑤 ) )
15 14 adantld ( ( 𝐴 ∈ ℝ*𝐴 ∈ ℝ*𝑤 ∈ ℝ* ) → ( ( 𝐴𝐴𝐴 < 𝑤 ) → 𝐴𝑤 ) )
16 8 9 10 11 12 15 ixxun ( ( ( 𝐴 ∈ ℝ*𝐴 ∈ ℝ*𝐵 ∈ ℝ* ) ∧ ( 𝐴𝐴𝐴 < 𝐵 ) ) → ( ( 𝐴 [,] 𝐴 ) ∪ ( 𝐴 (,) 𝐵 ) ) = ( 𝐴 [,) 𝐵 ) )
17 1 1 5 6 7 16 syl32anc ( ( 𝐴 ∈ ℝ*𝐵 ∈ ℝ*𝐴 < 𝐵 ) → ( ( 𝐴 [,] 𝐴 ) ∪ ( 𝐴 (,) 𝐵 ) ) = ( 𝐴 [,) 𝐵 ) )
18 4 17 eqtr3d ( ( 𝐴 ∈ ℝ*𝐵 ∈ ℝ*𝐴 < 𝐵 ) → ( { 𝐴 } ∪ ( 𝐴 (,) 𝐵 ) ) = ( 𝐴 [,) 𝐵 ) )