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

Metamath Proof Explorer

Theorem prunioo

Proof