Description: The closure of one end of an open real interval. (Contributed by Paul Chapman, 15-Mar-2008) (Proof shortened by Mario Carneiro, 16-Jun-2014)
Ref | Expression | ||
---|---|---|---|
Assertion | snunioo | |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | simp1 | |
|
2 | iccid | |
|
3 | 1 2 | syl | |
4 | 3 | uneq1d | |
5 | simp2 | |
|
6 | 1 | xrleidd | |
7 | simp3 | |
|
8 | df-icc | |
|
9 | df-ioo | |
|
10 | xrltnle | |
|
11 | df-ico | |
|
12 | xrlelttr | |
|
13 | xrltle | |
|
14 | 13 | 3adant1 | |
15 | 14 | adantld | |
16 | 8 9 10 11 12 15 | ixxun | |
17 | 1 1 5 6 7 16 | syl32anc | |
18 | 4 17 | eqtr3d | |