# Metamath Proof Explorer

## Theorem icoopnst

Description: A half-open interval starting at A is open in the closed interval from A to B . (Contributed by Jeff Madsen, 2-Sep-2009) (Revised by Mario Carneiro, 15-Dec-2013)

Ref Expression
Hypothesis icoopnst.1 ${⊢}{J}=\mathrm{MetOpen}\left({\left(\mathrm{abs}\circ -\right)↾}_{\left(\left[{A},{B}\right]×\left[{A},{B}\right]\right)}\right)$
Assertion icoopnst ${⊢}\left({A}\in ℝ\wedge {B}\in ℝ\right)\to \left({C}\in \left({A},{B}\right]\to \left[{A},{C}\right)\in {J}\right)$

### Proof

Step Hyp Ref Expression
1 icoopnst.1 ${⊢}{J}=\mathrm{MetOpen}\left({\left(\mathrm{abs}\circ -\right)↾}_{\left(\left[{A},{B}\right]×\left[{A},{B}\right]\right)}\right)$
2 iooretop ${⊢}\left({A}-1,{C}\right)\in \mathrm{topGen}\left(\mathrm{ran}\left(.\right)\right)$
3 simp1 ${⊢}\left({v}\in ℝ\wedge {A}\le {v}\wedge {v}<{C}\right)\to {v}\in ℝ$
4 3 a1i ${⊢}\left(\left({A}\in ℝ\wedge {B}\in ℝ\right)\wedge {C}\in \left({A},{B}\right]\right)\to \left(\left({v}\in ℝ\wedge {A}\le {v}\wedge {v}<{C}\right)\to {v}\in ℝ\right)$
5 ltm1 ${⊢}{A}\in ℝ\to {A}-1<{A}$
6 5 adantr ${⊢}\left({A}\in ℝ\wedge {v}\in ℝ\right)\to {A}-1<{A}$
7 peano2rem ${⊢}{A}\in ℝ\to {A}-1\in ℝ$
8 7 adantr ${⊢}\left({A}\in ℝ\wedge {v}\in ℝ\right)\to {A}-1\in ℝ$
9 ltletr ${⊢}\left({A}-1\in ℝ\wedge {A}\in ℝ\wedge {v}\in ℝ\right)\to \left(\left({A}-1<{A}\wedge {A}\le {v}\right)\to {A}-1<{v}\right)$
10 9 3expb ${⊢}\left({A}-1\in ℝ\wedge \left({A}\in ℝ\wedge {v}\in ℝ\right)\right)\to \left(\left({A}-1<{A}\wedge {A}\le {v}\right)\to {A}-1<{v}\right)$
11 8 10 mpancom ${⊢}\left({A}\in ℝ\wedge {v}\in ℝ\right)\to \left(\left({A}-1<{A}\wedge {A}\le {v}\right)\to {A}-1<{v}\right)$
12 6 11 mpand ${⊢}\left({A}\in ℝ\wedge {v}\in ℝ\right)\to \left({A}\le {v}\to {A}-1<{v}\right)$
13 12 impr ${⊢}\left({A}\in ℝ\wedge \left({v}\in ℝ\wedge {A}\le {v}\right)\right)\to {A}-1<{v}$
14 13 3adantr3 ${⊢}\left({A}\in ℝ\wedge \left({v}\in ℝ\wedge {A}\le {v}\wedge {v}<{C}\right)\right)\to {A}-1<{v}$
15 14 ex ${⊢}{A}\in ℝ\to \left(\left({v}\in ℝ\wedge {A}\le {v}\wedge {v}<{C}\right)\to {A}-1<{v}\right)$
16 15 ad2antrr ${⊢}\left(\left({A}\in ℝ\wedge {B}\in ℝ\right)\wedge {C}\in \left({A},{B}\right]\right)\to \left(\left({v}\in ℝ\wedge {A}\le {v}\wedge {v}<{C}\right)\to {A}-1<{v}\right)$
17 simp3 ${⊢}\left({v}\in ℝ\wedge {A}\le {v}\wedge {v}<{C}\right)\to {v}<{C}$
18 17 a1i ${⊢}\left(\left({A}\in ℝ\wedge {B}\in ℝ\right)\wedge {C}\in \left({A},{B}\right]\right)\to \left(\left({v}\in ℝ\wedge {A}\le {v}\wedge {v}<{C}\right)\to {v}<{C}\right)$
19 4 16 18 3jcad ${⊢}\left(\left({A}\in ℝ\wedge {B}\in ℝ\right)\wedge {C}\in \left({A},{B}\right]\right)\to \left(\left({v}\in ℝ\wedge {A}\le {v}\wedge {v}<{C}\right)\to \left({v}\in ℝ\wedge {A}-1<{v}\wedge {v}<{C}\right)\right)$
20 simp2 ${⊢}\left({v}\in ℝ\wedge {A}\le {v}\wedge {v}<{C}\right)\to {A}\le {v}$
21 20 a1i ${⊢}\left(\left({A}\in ℝ\wedge {B}\in ℝ\right)\wedge {C}\in \left({A},{B}\right]\right)\to \left(\left({v}\in ℝ\wedge {A}\le {v}\wedge {v}<{C}\right)\to {A}\le {v}\right)$
22 rexr ${⊢}{A}\in ℝ\to {A}\in {ℝ}^{*}$
23 elioc2 ${⊢}\left({A}\in {ℝ}^{*}\wedge {B}\in ℝ\right)\to \left({C}\in \left({A},{B}\right]↔\left({C}\in ℝ\wedge {A}<{C}\wedge {C}\le {B}\right)\right)$
24 22 23 sylan ${⊢}\left({A}\in ℝ\wedge {B}\in ℝ\right)\to \left({C}\in \left({A},{B}\right]↔\left({C}\in ℝ\wedge {A}<{C}\wedge {C}\le {B}\right)\right)$
25 24 biimpa ${⊢}\left(\left({A}\in ℝ\wedge {B}\in ℝ\right)\wedge {C}\in \left({A},{B}\right]\right)\to \left({C}\in ℝ\wedge {A}<{C}\wedge {C}\le {B}\right)$
26 ltleletr ${⊢}\left({v}\in ℝ\wedge {C}\in ℝ\wedge {B}\in ℝ\right)\to \left(\left({v}<{C}\wedge {C}\le {B}\right)\to {v}\le {B}\right)$
27 26 3expa ${⊢}\left(\left({v}\in ℝ\wedge {C}\in ℝ\right)\wedge {B}\in ℝ\right)\to \left(\left({v}<{C}\wedge {C}\le {B}\right)\to {v}\le {B}\right)$
28 27 an31s ${⊢}\left(\left({B}\in ℝ\wedge {C}\in ℝ\right)\wedge {v}\in ℝ\right)\to \left(\left({v}<{C}\wedge {C}\le {B}\right)\to {v}\le {B}\right)$
29 28 imp ${⊢}\left(\left(\left({B}\in ℝ\wedge {C}\in ℝ\right)\wedge {v}\in ℝ\right)\wedge \left({v}<{C}\wedge {C}\le {B}\right)\right)\to {v}\le {B}$
30 29 ancom2s ${⊢}\left(\left(\left({B}\in ℝ\wedge {C}\in ℝ\right)\wedge {v}\in ℝ\right)\wedge \left({C}\le {B}\wedge {v}<{C}\right)\right)\to {v}\le {B}$
31 30 an4s ${⊢}\left(\left(\left({B}\in ℝ\wedge {C}\in ℝ\right)\wedge {C}\le {B}\right)\wedge \left({v}\in ℝ\wedge {v}<{C}\right)\right)\to {v}\le {B}$
32 31 3adantr2 ${⊢}\left(\left(\left({B}\in ℝ\wedge {C}\in ℝ\right)\wedge {C}\le {B}\right)\wedge \left({v}\in ℝ\wedge {A}\le {v}\wedge {v}<{C}\right)\right)\to {v}\le {B}$
33 32 ex ${⊢}\left(\left({B}\in ℝ\wedge {C}\in ℝ\right)\wedge {C}\le {B}\right)\to \left(\left({v}\in ℝ\wedge {A}\le {v}\wedge {v}<{C}\right)\to {v}\le {B}\right)$
34 33 anasss ${⊢}\left({B}\in ℝ\wedge \left({C}\in ℝ\wedge {C}\le {B}\right)\right)\to \left(\left({v}\in ℝ\wedge {A}\le {v}\wedge {v}<{C}\right)\to {v}\le {B}\right)$
35 34 3adantr2 ${⊢}\left({B}\in ℝ\wedge \left({C}\in ℝ\wedge {A}<{C}\wedge {C}\le {B}\right)\right)\to \left(\left({v}\in ℝ\wedge {A}\le {v}\wedge {v}<{C}\right)\to {v}\le {B}\right)$
36 35 adantll ${⊢}\left(\left({A}\in ℝ\wedge {B}\in ℝ\right)\wedge \left({C}\in ℝ\wedge {A}<{C}\wedge {C}\le {B}\right)\right)\to \left(\left({v}\in ℝ\wedge {A}\le {v}\wedge {v}<{C}\right)\to {v}\le {B}\right)$
37 25 36 syldan ${⊢}\left(\left({A}\in ℝ\wedge {B}\in ℝ\right)\wedge {C}\in \left({A},{B}\right]\right)\to \left(\left({v}\in ℝ\wedge {A}\le {v}\wedge {v}<{C}\right)\to {v}\le {B}\right)$
38 4 21 37 3jcad ${⊢}\left(\left({A}\in ℝ\wedge {B}\in ℝ\right)\wedge {C}\in \left({A},{B}\right]\right)\to \left(\left({v}\in ℝ\wedge {A}\le {v}\wedge {v}<{C}\right)\to \left({v}\in ℝ\wedge {A}\le {v}\wedge {v}\le {B}\right)\right)$
39 19 38 jcad ${⊢}\left(\left({A}\in ℝ\wedge {B}\in ℝ\right)\wedge {C}\in \left({A},{B}\right]\right)\to \left(\left({v}\in ℝ\wedge {A}\le {v}\wedge {v}<{C}\right)\to \left(\left({v}\in ℝ\wedge {A}-1<{v}\wedge {v}<{C}\right)\wedge \left({v}\in ℝ\wedge {A}\le {v}\wedge {v}\le {B}\right)\right)\right)$
40 simpl1 ${⊢}\left(\left({v}\in ℝ\wedge {A}-1<{v}\wedge {v}<{C}\right)\wedge \left({v}\in ℝ\wedge {A}\le {v}\wedge {v}\le {B}\right)\right)\to {v}\in ℝ$
41 simpr2 ${⊢}\left(\left({v}\in ℝ\wedge {A}-1<{v}\wedge {v}<{C}\right)\wedge \left({v}\in ℝ\wedge {A}\le {v}\wedge {v}\le {B}\right)\right)\to {A}\le {v}$
42 simpl3 ${⊢}\left(\left({v}\in ℝ\wedge {A}-1<{v}\wedge {v}<{C}\right)\wedge \left({v}\in ℝ\wedge {A}\le {v}\wedge {v}\le {B}\right)\right)\to {v}<{C}$
43 40 41 42 3jca ${⊢}\left(\left({v}\in ℝ\wedge {A}-1<{v}\wedge {v}<{C}\right)\wedge \left({v}\in ℝ\wedge {A}\le {v}\wedge {v}\le {B}\right)\right)\to \left({v}\in ℝ\wedge {A}\le {v}\wedge {v}<{C}\right)$
44 39 43 impbid1 ${⊢}\left(\left({A}\in ℝ\wedge {B}\in ℝ\right)\wedge {C}\in \left({A},{B}\right]\right)\to \left(\left({v}\in ℝ\wedge {A}\le {v}\wedge {v}<{C}\right)↔\left(\left({v}\in ℝ\wedge {A}-1<{v}\wedge {v}<{C}\right)\wedge \left({v}\in ℝ\wedge {A}\le {v}\wedge {v}\le {B}\right)\right)\right)$
45 simpll ${⊢}\left(\left({A}\in ℝ\wedge {B}\in ℝ\right)\wedge {C}\in \left({A},{B}\right]\right)\to {A}\in ℝ$
46 25 simp1d ${⊢}\left(\left({A}\in ℝ\wedge {B}\in ℝ\right)\wedge {C}\in \left({A},{B}\right]\right)\to {C}\in ℝ$
47 46 rexrd ${⊢}\left(\left({A}\in ℝ\wedge {B}\in ℝ\right)\wedge {C}\in \left({A},{B}\right]\right)\to {C}\in {ℝ}^{*}$
48 elico2 ${⊢}\left({A}\in ℝ\wedge {C}\in {ℝ}^{*}\right)\to \left({v}\in \left[{A},{C}\right)↔\left({v}\in ℝ\wedge {A}\le {v}\wedge {v}<{C}\right)\right)$
49 45 47 48 syl2anc ${⊢}\left(\left({A}\in ℝ\wedge {B}\in ℝ\right)\wedge {C}\in \left({A},{B}\right]\right)\to \left({v}\in \left[{A},{C}\right)↔\left({v}\in ℝ\wedge {A}\le {v}\wedge {v}<{C}\right)\right)$
50 elin ${⊢}{v}\in \left(\left({A}-1,{C}\right)\cap \left[{A},{B}\right]\right)↔\left({v}\in \left({A}-1,{C}\right)\wedge {v}\in \left[{A},{B}\right]\right)$
51 7 rexrd ${⊢}{A}\in ℝ\to {A}-1\in {ℝ}^{*}$
52 51 ad2antrr ${⊢}\left(\left({A}\in ℝ\wedge {B}\in ℝ\right)\wedge {C}\in \left({A},{B}\right]\right)\to {A}-1\in {ℝ}^{*}$
53 elioo2 ${⊢}\left({A}-1\in {ℝ}^{*}\wedge {C}\in {ℝ}^{*}\right)\to \left({v}\in \left({A}-1,{C}\right)↔\left({v}\in ℝ\wedge {A}-1<{v}\wedge {v}<{C}\right)\right)$
54 52 47 53 syl2anc ${⊢}\left(\left({A}\in ℝ\wedge {B}\in ℝ\right)\wedge {C}\in \left({A},{B}\right]\right)\to \left({v}\in \left({A}-1,{C}\right)↔\left({v}\in ℝ\wedge {A}-1<{v}\wedge {v}<{C}\right)\right)$
55 elicc2 ${⊢}\left({A}\in ℝ\wedge {B}\in ℝ\right)\to \left({v}\in \left[{A},{B}\right]↔\left({v}\in ℝ\wedge {A}\le {v}\wedge {v}\le {B}\right)\right)$
56 55 adantr ${⊢}\left(\left({A}\in ℝ\wedge {B}\in ℝ\right)\wedge {C}\in \left({A},{B}\right]\right)\to \left({v}\in \left[{A},{B}\right]↔\left({v}\in ℝ\wedge {A}\le {v}\wedge {v}\le {B}\right)\right)$
57 54 56 anbi12d ${⊢}\left(\left({A}\in ℝ\wedge {B}\in ℝ\right)\wedge {C}\in \left({A},{B}\right]\right)\to \left(\left({v}\in \left({A}-1,{C}\right)\wedge {v}\in \left[{A},{B}\right]\right)↔\left(\left({v}\in ℝ\wedge {A}-1<{v}\wedge {v}<{C}\right)\wedge \left({v}\in ℝ\wedge {A}\le {v}\wedge {v}\le {B}\right)\right)\right)$
58 50 57 syl5bb ${⊢}\left(\left({A}\in ℝ\wedge {B}\in ℝ\right)\wedge {C}\in \left({A},{B}\right]\right)\to \left({v}\in \left(\left({A}-1,{C}\right)\cap \left[{A},{B}\right]\right)↔\left(\left({v}\in ℝ\wedge {A}-1<{v}\wedge {v}<{C}\right)\wedge \left({v}\in ℝ\wedge {A}\le {v}\wedge {v}\le {B}\right)\right)\right)$
59 44 49 58 3bitr4d ${⊢}\left(\left({A}\in ℝ\wedge {B}\in ℝ\right)\wedge {C}\in \left({A},{B}\right]\right)\to \left({v}\in \left[{A},{C}\right)↔{v}\in \left(\left({A}-1,{C}\right)\cap \left[{A},{B}\right]\right)\right)$
60 59 eqrdv ${⊢}\left(\left({A}\in ℝ\wedge {B}\in ℝ\right)\wedge {C}\in \left({A},{B}\right]\right)\to \left[{A},{C}\right)=\left({A}-1,{C}\right)\cap \left[{A},{B}\right]$
61 ineq1 ${⊢}{v}=\left({A}-1,{C}\right)\to {v}\cap \left[{A},{B}\right]=\left({A}-1,{C}\right)\cap \left[{A},{B}\right]$
62 61 rspceeqv ${⊢}\left(\left({A}-1,{C}\right)\in \mathrm{topGen}\left(\mathrm{ran}\left(.\right)\right)\wedge \left[{A},{C}\right)=\left({A}-1,{C}\right)\cap \left[{A},{B}\right]\right)\to \exists {v}\in \mathrm{topGen}\left(\mathrm{ran}\left(.\right)\right)\phantom{\rule{.4em}{0ex}}\left[{A},{C}\right)={v}\cap \left[{A},{B}\right]$
63 2 60 62 sylancr ${⊢}\left(\left({A}\in ℝ\wedge {B}\in ℝ\right)\wedge {C}\in \left({A},{B}\right]\right)\to \exists {v}\in \mathrm{topGen}\left(\mathrm{ran}\left(.\right)\right)\phantom{\rule{.4em}{0ex}}\left[{A},{C}\right)={v}\cap \left[{A},{B}\right]$
64 retop ${⊢}\mathrm{topGen}\left(\mathrm{ran}\left(.\right)\right)\in \mathrm{Top}$
65 ovex ${⊢}\left[{A},{B}\right]\in \mathrm{V}$
66 elrest ${⊢}\left(\mathrm{topGen}\left(\mathrm{ran}\left(.\right)\right)\in \mathrm{Top}\wedge \left[{A},{B}\right]\in \mathrm{V}\right)\to \left(\left[{A},{C}\right)\in \left(\mathrm{topGen}\left(\mathrm{ran}\left(.\right)\right){↾}_{𝑡}\left[{A},{B}\right]\right)↔\exists {v}\in \mathrm{topGen}\left(\mathrm{ran}\left(.\right)\right)\phantom{\rule{.4em}{0ex}}\left[{A},{C}\right)={v}\cap \left[{A},{B}\right]\right)$
67 64 65 66 mp2an ${⊢}\left[{A},{C}\right)\in \left(\mathrm{topGen}\left(\mathrm{ran}\left(.\right)\right){↾}_{𝑡}\left[{A},{B}\right]\right)↔\exists {v}\in \mathrm{topGen}\left(\mathrm{ran}\left(.\right)\right)\phantom{\rule{.4em}{0ex}}\left[{A},{C}\right)={v}\cap \left[{A},{B}\right]$
68 63 67 sylibr ${⊢}\left(\left({A}\in ℝ\wedge {B}\in ℝ\right)\wedge {C}\in \left({A},{B}\right]\right)\to \left[{A},{C}\right)\in \left(\mathrm{topGen}\left(\mathrm{ran}\left(.\right)\right){↾}_{𝑡}\left[{A},{B}\right]\right)$
69 iccssre ${⊢}\left({A}\in ℝ\wedge {B}\in ℝ\right)\to \left[{A},{B}\right]\subseteq ℝ$
70 69 adantr ${⊢}\left(\left({A}\in ℝ\wedge {B}\in ℝ\right)\wedge {C}\in \left({A},{B}\right]\right)\to \left[{A},{B}\right]\subseteq ℝ$
71 eqid ${⊢}\mathrm{topGen}\left(\mathrm{ran}\left(.\right)\right)=\mathrm{topGen}\left(\mathrm{ran}\left(.\right)\right)$
72 71 1 resubmet ${⊢}\left[{A},{B}\right]\subseteq ℝ\to {J}=\mathrm{topGen}\left(\mathrm{ran}\left(.\right)\right){↾}_{𝑡}\left[{A},{B}\right]$
73 70 72 syl ${⊢}\left(\left({A}\in ℝ\wedge {B}\in ℝ\right)\wedge {C}\in \left({A},{B}\right]\right)\to {J}=\mathrm{topGen}\left(\mathrm{ran}\left(.\right)\right){↾}_{𝑡}\left[{A},{B}\right]$
74 68 73 eleqtrrd ${⊢}\left(\left({A}\in ℝ\wedge {B}\in ℝ\right)\wedge {C}\in \left({A},{B}\right]\right)\to \left[{A},{C}\right)\in {J}$
75 74 ex ${⊢}\left({A}\in ℝ\wedge {B}\in ℝ\right)\to \left({C}\in \left({A},{B}\right]\to \left[{A},{C}\right)\in {J}\right)$