Metamath Proof Explorer


Theorem iocopn

Description: A left-open right-closed interval is an open set of the standard topology restricted to an interval that contains the original interval and has the same upper bound. (Contributed by Glauco Siliprandi, 11-Dec-2019)

Ref Expression
Hypotheses iocopn.a φ A *
iocopn.c φ C *
iocopn.b φ B
iocopn.k K = topGen ran .
iocopn.j J = K 𝑡 A B
iocopn.alec φ A C
iocopn.6 φ B
Assertion iocopn φ C B J

Proof

Step Hyp Ref Expression
1 iocopn.a φ A *
2 iocopn.c φ C *
3 iocopn.b φ B
4 iocopn.k K = topGen ran .
5 iocopn.j J = K 𝑡 A B
6 iocopn.alec φ A C
7 iocopn.6 φ B
8 retop topGen ran . Top
9 4 8 eqeltri K Top
10 9 a1i φ K Top
11 ovexd φ A B V
12 iooretop C +∞ topGen ran .
13 12 4 eleqtrri C +∞ K
14 13 a1i φ C +∞ K
15 elrestr K Top A B V C +∞ K C +∞ A B K 𝑡 A B
16 10 11 14 15 syl3anc φ C +∞ A B K 𝑡 A B
17 2 adantr φ x C +∞ A B C *
18 3 rexrd φ B *
19 18 adantr φ x C +∞ A B B *
20 elinel1 x C +∞ A B x C +∞
21 elioore x C +∞ x
22 20 21 syl x C +∞ A B x
23 22 rexrd x C +∞ A B x *
24 23 adantl φ x C +∞ A B x *
25 pnfxr +∞ *
26 25 a1i φ x C +∞ A B +∞ *
27 20 adantl φ x C +∞ A B x C +∞
28 ioogtlb C * +∞ * x C +∞ C < x
29 17 26 27 28 syl3anc φ x C +∞ A B C < x
30 1 adantr φ x C +∞ A B A *
31 elinel2 x C +∞ A B x A B
32 31 adantl φ x C +∞ A B x A B
33 iocleub A * B * x A B x B
34 30 19 32 33 syl3anc φ x C +∞ A B x B
35 17 19 24 29 34 eliocd φ x C +∞ A B x C B
36 2 adantr φ x C B C *
37 25 a1i φ x C B +∞ *
38 iocssre C * B C B
39 2 7 38 syl2anc φ C B
40 39 sselda φ x C B x
41 18 adantr φ x C B B *
42 simpr φ x C B x C B
43 iocgtlb C * B * x C B C < x
44 36 41 42 43 syl3anc φ x C B C < x
45 40 ltpnfd φ x C B x < +∞
46 36 37 40 44 45 eliood φ x C B x C +∞
47 1 adantr φ x C B A *
48 40 rexrd φ x C B x *
49 6 adantr φ x C B A C
50 47 36 48 49 44 xrlelttrd φ x C B A < x
51 iocleub C * B * x C B x B
52 36 41 42 51 syl3anc φ x C B x B
53 47 41 48 50 52 eliocd φ x C B x A B
54 46 53 elind φ x C B x C +∞ A B
55 35 54 impbida φ x C +∞ A B x C B
56 55 eqrdv φ C +∞ A B = C B
57 5 eqcomi K 𝑡 A B = J
58 57 a1i φ K 𝑡 A B = J
59 16 56 58 3eltr3d φ C B J