Metamath Proof Explorer

Theorem snunioo1

Description: The closure of one end of an open real interval. (Contributed by Glauco Siliprandi, 11-Dec-2019)

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

Proof

Step Hyp Ref Expression
1 uncom ⊢ ( ( 𝐴 (,) 𝐵 ) ∪ ( 𝐴 [,] 𝐴 ) ) = ( ( 𝐴 [,] 𝐴 ) ∪ ( 𝐴 (,) 𝐵 ) )
2 iccid ⊢ ( 𝐴 ∈ ℝ* → ( 𝐴 [,] 𝐴 ) = { 𝐴 } )
3 2 3ad2ant1 ⊢ ( ( 𝐴 ∈ ℝ* ∧ 𝐵 ∈ ℝ* ∧ 𝐴 < 𝐵 ) → ( 𝐴 [,] 𝐴 ) = { 𝐴 } )
4 3 uneq2d ⊢ ( ( 𝐴 ∈ ℝ* ∧ 𝐵 ∈ ℝ* ∧ 𝐴 < 𝐵 ) → ( ( 𝐴 (,) 𝐵 ) ∪ ( 𝐴 [,] 𝐴 ) ) = ( ( 𝐴 (,) 𝐵 ) ∪ { 𝐴 } ) )
5 simp1 ⊢ ( ( 𝐴 ∈ ℝ* ∧ 𝐵 ∈ ℝ* ∧ 𝐴 < 𝐵 ) → 𝐴 ∈ ℝ* )
6 simp2 ⊢ ( ( 𝐴 ∈ ℝ* ∧ 𝐵 ∈ ℝ* ∧ 𝐴 < 𝐵 ) → 𝐵 ∈ ℝ* )
7 xrleid ⊢ ( 𝐴 ∈ ℝ* → 𝐴 ≤ 𝐴 )
8 7 3ad2ant1 ⊢ ( ( 𝐴 ∈ ℝ* ∧ 𝐵 ∈ ℝ* ∧ 𝐴 < 𝐵 ) → 𝐴 ≤ 𝐴 )
9 simp3 ⊢ ( ( 𝐴 ∈ ℝ* ∧ 𝐵 ∈ ℝ* ∧ 𝐴 < 𝐵 ) → 𝐴 < 𝐵 )
10 df-icc ⊢ [,] = ( 𝑥 ∈ ℝ* , 𝑦 ∈ ℝ* ↦ { 𝑧 ∈ ℝ* ∣ ( 𝑥 ≤ 𝑧 ∧ 𝑧 ≤ 𝑦 ) } )
11 df-ioo ⊢ (,) = ( 𝑥 ∈ ℝ* , 𝑦 ∈ ℝ* ↦ { 𝑧 ∈ ℝ* ∣ ( 𝑥 < 𝑧 ∧ 𝑧 < 𝑦 ) } )
12 xrltnle ⊢ ( ( 𝐴 ∈ ℝ* ∧ 𝑤 ∈ ℝ* ) → ( 𝐴 < 𝑤 ↔ ¬ 𝑤 ≤ 𝐴 ) )
13 df-ico ⊢ [,) = ( 𝑥 ∈ ℝ* , 𝑦 ∈ ℝ* ↦ { 𝑧 ∈ ℝ* ∣ ( 𝑥 ≤ 𝑧 ∧ 𝑧 < 𝑦 ) } )
14 xrlelttr ⊢ ( ( 𝑤 ∈ ℝ* ∧ 𝐴 ∈ ℝ* ∧ 𝐵 ∈ ℝ* ) → ( ( 𝑤 ≤ 𝐴 ∧ 𝐴 < 𝐵 ) → 𝑤 < 𝐵 ) )
15 simpl1 ⊢ ( ( ( 𝐴 ∈ ℝ* ∧ 𝐴 ∈ ℝ* ∧ 𝑤 ∈ ℝ* ) ∧ ( 𝐴 ≤ 𝐴 ∧ 𝐴 < 𝑤 ) ) → 𝐴 ∈ ℝ* )
16 simpl3 ⊢ ( ( ( 𝐴 ∈ ℝ* ∧ 𝐴 ∈ ℝ* ∧ 𝑤 ∈ ℝ* ) ∧ ( 𝐴 ≤ 𝐴 ∧ 𝐴 < 𝑤 ) ) → 𝑤 ∈ ℝ* )
17 simprr ⊢ ( ( ( 𝐴 ∈ ℝ* ∧ 𝐴 ∈ ℝ* ∧ 𝑤 ∈ ℝ* ) ∧ ( 𝐴 ≤ 𝐴 ∧ 𝐴 < 𝑤 ) ) → 𝐴 < 𝑤 )
18 15 16 17 xrltled ⊢ ( ( ( 𝐴 ∈ ℝ* ∧ 𝐴 ∈ ℝ* ∧ 𝑤 ∈ ℝ* ) ∧ ( 𝐴 ≤ 𝐴 ∧ 𝐴 < 𝑤 ) ) → 𝐴 ≤ 𝑤 )
19 18 ex ⊢ ( ( 𝐴 ∈ ℝ* ∧ 𝐴 ∈ ℝ* ∧ 𝑤 ∈ ℝ* ) → ( ( 𝐴 ≤ 𝐴 ∧ 𝐴 < 𝑤 ) → 𝐴 ≤ 𝑤 ) )
20 10 11 12 13 14 19 ixxun ⊢ ( ( ( 𝐴 ∈ ℝ* ∧ 𝐴 ∈ ℝ* ∧ 𝐵 ∈ ℝ* ) ∧ ( 𝐴 ≤ 𝐴 ∧ 𝐴 < 𝐵 ) ) → ( ( 𝐴 [,] 𝐴 ) ∪ ( 𝐴 (,) 𝐵 ) ) = ( 𝐴 [,) 𝐵 ) )
21 5 5 6 8 9 20 syl32anc ⊢ ( ( 𝐴 ∈ ℝ* ∧ 𝐵 ∈ ℝ* ∧ 𝐴 < 𝐵 ) → ( ( 𝐴 [,] 𝐴 ) ∪ ( 𝐴 (,) 𝐵 ) ) = ( 𝐴 [,) 𝐵 ) )
22 1 4 21 3eqtr3a ⊢ ( ( 𝐴 ∈ ℝ* ∧ 𝐵 ∈ ℝ* ∧ 𝐴 < 𝐵 ) → ( ( 𝐴 (,) 𝐵 ) ∪ { 𝐴 } ) = ( 𝐴 [,) 𝐵 ) )