Metamath Proof Explorer

Theorem prunioo

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

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

Proof

Step Hyp Ref Expression
1 simp3 ⊢ ( ( 𝐴 ∈ ℝ* ∧ 𝐵 ∈ ℝ* ∧ 𝐴 ≤ 𝐵 ) → 𝐴 ≤ 𝐵 )
2 xrleloe ⊢ ( ( 𝐴 ∈ ℝ* ∧ 𝐵 ∈ ℝ* ) → ( 𝐴 ≤ 𝐵 ↔ ( 𝐴 < 𝐵 ∨ 𝐴 = 𝐵 ) ) )
3 2 3adant3 ⊢ ( ( 𝐴 ∈ ℝ* ∧ 𝐵 ∈ ℝ* ∧ 𝐴 ≤ 𝐵 ) → ( 𝐴 ≤ 𝐵 ↔ ( 𝐴 < 𝐵 ∨ 𝐴 = 𝐵 ) ) )
4 df-pr ⊢ { 𝐴 , 𝐵 } = ( { 𝐴 } ∪ { 𝐵 } )
5 4 uneq2i ⊢ ( ( 𝐴 (,) 𝐵 ) ∪ { 𝐴 , 𝐵 } ) = ( ( 𝐴 (,) 𝐵 ) ∪ ( { 𝐴 } ∪ { 𝐵 } ) )
6 unass ⊢ ( ( ( 𝐴 (,) 𝐵 ) ∪ { 𝐴 } ) ∪ { 𝐵 } ) = ( ( 𝐴 (,) 𝐵 ) ∪ ( { 𝐴 } ∪ { 𝐵 } ) )
7 5 6 eqtr4i ⊢ ( ( 𝐴 (,) 𝐵 ) ∪ { 𝐴 , 𝐵 } ) = ( ( ( 𝐴 (,) 𝐵 ) ∪ { 𝐴 } ) ∪ { 𝐵 } )
8 uncom ⊢ ( ( 𝐴 (,) 𝐵 ) ∪ { 𝐴 } ) = ( { 𝐴 } ∪ ( 𝐴 (,) 𝐵 ) )
9 snunioo ⊢ ( ( 𝐴 ∈ ℝ* ∧ 𝐵 ∈ ℝ* ∧ 𝐴 < 𝐵 ) → ( { 𝐴 } ∪ ( 𝐴 (,) 𝐵 ) ) = ( 𝐴 [,) 𝐵 ) )
10 8 9 eqtrid ⊢ ( ( 𝐴 ∈ ℝ* ∧ 𝐵 ∈ ℝ* ∧ 𝐴 < 𝐵 ) → ( ( 𝐴 (,) 𝐵 ) ∪ { 𝐴 } ) = ( 𝐴 [,) 𝐵 ) )
11 10 uneq1d ⊢ ( ( 𝐴 ∈ ℝ* ∧ 𝐵 ∈ ℝ* ∧ 𝐴 < 𝐵 ) → ( ( ( 𝐴 (,) 𝐵 ) ∪ { 𝐴 } ) ∪ { 𝐵 } ) = ( ( 𝐴 [,) 𝐵 ) ∪ { 𝐵 } ) )
12 7 11 eqtrid ⊢ ( ( 𝐴 ∈ ℝ* ∧ 𝐵 ∈ ℝ* ∧ 𝐴 < 𝐵 ) → ( ( 𝐴 (,) 𝐵 ) ∪ { 𝐴 , 𝐵 } ) = ( ( 𝐴 [,) 𝐵 ) ∪ { 𝐵 } ) )
13 12 3expa ⊢ ( ( ( 𝐴 ∈ ℝ* ∧ 𝐵 ∈ ℝ* ) ∧ 𝐴 < 𝐵 ) → ( ( 𝐴 (,) 𝐵 ) ∪ { 𝐴 , 𝐵 } ) = ( ( 𝐴 [,) 𝐵 ) ∪ { 𝐵 } ) )
14 13 3adantl3 ⊢ ( ( ( 𝐴 ∈ ℝ* ∧ 𝐵 ∈ ℝ* ∧ 𝐴 ≤ 𝐵 ) ∧ 𝐴 < 𝐵 ) → ( ( 𝐴 (,) 𝐵 ) ∪ { 𝐴 , 𝐵 } ) = ( ( 𝐴 [,) 𝐵 ) ∪ { 𝐵 } ) )
15 snunico ⊢ ( ( 𝐴 ∈ ℝ* ∧ 𝐵 ∈ ℝ* ∧ 𝐴 ≤ 𝐵 ) → ( ( 𝐴 [,) 𝐵 ) ∪ { 𝐵 } ) = ( 𝐴 [,] 𝐵 ) )
16 15 adantr ⊢ ( ( ( 𝐴 ∈ ℝ* ∧ 𝐵 ∈ ℝ* ∧ 𝐴 ≤ 𝐵 ) ∧ 𝐴 < 𝐵 ) → ( ( 𝐴 [,) 𝐵 ) ∪ { 𝐵 } ) = ( 𝐴 [,] 𝐵 ) )
17 14 16 eqtrd ⊢ ( ( ( 𝐴 ∈ ℝ* ∧ 𝐵 ∈ ℝ* ∧ 𝐴 ≤ 𝐵 ) ∧ 𝐴 < 𝐵 ) → ( ( 𝐴 (,) 𝐵 ) ∪ { 𝐴 , 𝐵 } ) = ( 𝐴 [,] 𝐵 ) )
18 17 ex ⊢ ( ( 𝐴 ∈ ℝ* ∧ 𝐵 ∈ ℝ* ∧ 𝐴 ≤ 𝐵 ) → ( 𝐴 < 𝐵 → ( ( 𝐴 (,) 𝐵 ) ∪ { 𝐴 , 𝐵 } ) = ( 𝐴 [,] 𝐵 ) ) )
19 iccid ⊢ ( 𝐴 ∈ ℝ* → ( 𝐴 [,] 𝐴 ) = { 𝐴 } )
20 19 3ad2ant1 ⊢ ( ( 𝐴 ∈ ℝ* ∧ 𝐵 ∈ ℝ* ∧ 𝐴 ≤ 𝐵 ) → ( 𝐴 [,] 𝐴 ) = { 𝐴 } )
21 20 eqcomd ⊢ ( ( 𝐴 ∈ ℝ* ∧ 𝐵 ∈ ℝ* ∧ 𝐴 ≤ 𝐵 ) → { 𝐴 } = ( 𝐴 [,] 𝐴 ) )
22 uncom ⊢ ( ∅ ∪ { 𝐴 } ) = ( { 𝐴 } ∪ ∅ )
23 un0 ⊢ ( { 𝐴 } ∪ ∅ ) = { 𝐴 }
24 22 23 eqtri ⊢ ( ∅ ∪ { 𝐴 } ) = { 𝐴 }
25 iooid ⊢ ( 𝐴 (,) 𝐴 ) = ∅
26 oveq2 ⊢ ( 𝐴 = 𝐵 → ( 𝐴 (,) 𝐴 ) = ( 𝐴 (,) 𝐵 ) )
27 25 26 eqtr3id ⊢ ( 𝐴 = 𝐵 → ∅ = ( 𝐴 (,) 𝐵 ) )
28 dfsn2 ⊢ { 𝐴 } = { 𝐴 , 𝐴 }
29 preq2 ⊢ ( 𝐴 = 𝐵 → { 𝐴 , 𝐴 } = { 𝐴 , 𝐵 } )
30 28 29 eqtrid ⊢ ( 𝐴 = 𝐵 → { 𝐴 } = { 𝐴 , 𝐵 } )
31 27 30 uneq12d ⊢ ( 𝐴 = 𝐵 → ( ∅ ∪ { 𝐴 } ) = ( ( 𝐴 (,) 𝐵 ) ∪ { 𝐴 , 𝐵 } ) )
32 24 31 eqtr3id ⊢ ( 𝐴 = 𝐵 → { 𝐴 } = ( ( 𝐴 (,) 𝐵 ) ∪ { 𝐴 , 𝐵 } ) )
33 oveq2 ⊢ ( 𝐴 = 𝐵 → ( 𝐴 [,] 𝐴 ) = ( 𝐴 [,] 𝐵 ) )
34 32 33 eqeq12d ⊢ ( 𝐴 = 𝐵 → ( { 𝐴 } = ( 𝐴 [,] 𝐴 ) ↔ ( ( 𝐴 (,) 𝐵 ) ∪ { 𝐴 , 𝐵 } ) = ( 𝐴 [,] 𝐵 ) ) )
35 21 34 syl5ibcom ⊢ ( ( 𝐴 ∈ ℝ* ∧ 𝐵 ∈ ℝ* ∧ 𝐴 ≤ 𝐵 ) → ( 𝐴 = 𝐵 → ( ( 𝐴 (,) 𝐵 ) ∪ { 𝐴 , 𝐵 } ) = ( 𝐴 [,] 𝐵 ) ) )
36 18 35 jaod ⊢ ( ( 𝐴 ∈ ℝ* ∧ 𝐵 ∈ ℝ* ∧ 𝐴 ≤ 𝐵 ) → ( ( 𝐴 < 𝐵 ∨ 𝐴 = 𝐵 ) → ( ( 𝐴 (,) 𝐵 ) ∪ { 𝐴 , 𝐵 } ) = ( 𝐴 [,] 𝐵 ) ) )
37 3 36 sylbid ⊢ ( ( 𝐴 ∈ ℝ* ∧ 𝐵 ∈ ℝ* ∧ 𝐴 ≤ 𝐵 ) → ( 𝐴 ≤ 𝐵 → ( ( 𝐴 (,) 𝐵 ) ∪ { 𝐴 , 𝐵 } ) = ( 𝐴 [,] 𝐵 ) ) )
38 1 37 mpd ⊢ ( ( 𝐴 ∈ ℝ* ∧ 𝐵 ∈ ℝ* ∧ 𝐴 ≤ 𝐵 ) → ( ( 𝐴 (,) 𝐵 ) ∪ { 𝐴 , 𝐵 } ) = ( 𝐴 [,] 𝐵 ) )