Metamath Proof Explorer


Theorem iocmnfcld

Description: Left-unbounded closed intervals are closed sets of the standard topology on RR . (Contributed by Mario Carneiro, 17-Feb-2015)

Ref Expression
Assertion iocmnfcld A −∞ A Clsd topGen ran .

Proof

Step Hyp Ref Expression
1 mnfxr −∞ *
2 1 a1i A −∞ *
3 rexr A A *
4 pnfxr +∞ *
5 4 a1i A +∞ *
6 mnflt A −∞ < A
7 ltpnf A A < +∞
8 df-ioc . = x * , y * z * | x < z z y
9 df-ioo . = x * , y * z * | x < z z < y
10 xrltnle A * w * A < w ¬ w A
11 xrlelttr w * A * +∞ * w A A < +∞ w < +∞
12 xrlttr −∞ * A * w * −∞ < A A < w −∞ < w
13 8 9 10 9 11 12 ixxun −∞ * A * +∞ * −∞ < A A < +∞ −∞ A A +∞ = −∞ +∞
14 2 3 5 6 7 13 syl32anc A −∞ A A +∞ = −∞ +∞
15 ioomax −∞ +∞ =
16 14 15 eqtrdi A −∞ A A +∞ =
17 iocssre −∞ * A −∞ A
18 1 17 mpan A −∞ A
19 8 9 10 ixxdisj −∞ * A * +∞ * −∞ A A +∞ =
20 1 3 5 19 mp3an2i A −∞ A A +∞ =
21 uneqdifeq −∞ A −∞ A A +∞ = −∞ A A +∞ = −∞ A = A +∞
22 18 20 21 syl2anc A −∞ A A +∞ = −∞ A = A +∞
23 16 22 mpbid A −∞ A = A +∞
24 iooretop A +∞ topGen ran .
25 23 24 eqeltrdi A −∞ A topGen ran .
26 retop topGen ran . Top
27 uniretop = topGen ran .
28 27 iscld2 topGen ran . Top −∞ A −∞ A Clsd topGen ran . −∞ A topGen ran .
29 26 18 28 sylancr A −∞ A Clsd topGen ran . −∞ A topGen ran .
30 25 29 mpbird A −∞ A Clsd topGen ran .