Metamath Proof Explorer


Theorem icopnfcld

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

Ref Expression
Assertion icopnfcld 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-ioo . = x * , y * z * | x < z z < y
9 df-ico . = x * , y * z * | x z z < y
10 xrlenlt A * w * A w ¬ w < A
11 xrlttr w * A * +∞ * w < A A < +∞ w < +∞
12 xrltletr −∞ * A * w * −∞ < A A w −∞ < w
13 8 9 10 8 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 ioossre −∞ A
18 8 9 10 ixxdisj −∞ * A * +∞ * −∞ A A +∞ =
19 1 3 5 18 mp3an2i A −∞ A A +∞ =
20 uneqdifeq −∞ A −∞ A A +∞ = −∞ A A +∞ = −∞ A = A +∞
21 17 19 20 sylancr A −∞ A A +∞ = −∞ A = A +∞
22 16 21 mpbid A −∞ A = A +∞
23 retop topGen ran . Top
24 iooretop −∞ A topGen ran .
25 uniretop = topGen ran .
26 25 opncld topGen ran . Top −∞ A topGen ran . −∞ A Clsd topGen ran .
27 23 24 26 mp2an −∞ A Clsd topGen ran .
28 22 27 eqeltrrdi A A +∞ Clsd topGen ran .