This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

Theorem snunioc

Description: The closure of the open end of a left-open real interval. (Contributed by Thierry Arnoux, 28-Mar-2017)

Ref Expression
Assertion snunioc ( ( 𝐴 ∈ ℝ* ∧ 𝐵 ∈ ℝ* ∧ 𝐴 ≤ 𝐵 ) → ( { 𝐴 } ∪ ( 𝐴 (,] 𝐵 ) ) = ( 𝐴 [,] 𝐵 ) )

Proof

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