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 ⊢A∈ℝ*∧B∈ℝ*∧A≤B→AB∪AB=AB

Proof

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