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 ( ( 𝐴 ∈ ℝ*𝐵 ∈ ℝ*𝐴𝐵 ) → ( { 𝐴 } ∪ ( 𝐴 (,] 𝐵 ) ) = ( 𝐴 [,] 𝐵 ) )