Metamath Proof Explorer


Theorem icoopn

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

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

Proof

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