This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

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 e. RR -> ( A [,) +oo ) e. ( Clsd ` ( topGen ` ran (,) ) ) )

Proof

Step Hyp Ref Expression
1 mnfxr 
 |-  -oo e. RR*
2 1 a1i 
 |-  ( A e. RR -> -oo e. RR* )
3 rexr 
 |-  ( A e. RR -> A e. RR* )
4 pnfxr 
 |-  +oo e. RR*
5 4 a1i 
 |-  ( A e. RR -> +oo e. RR* )
6 mnflt 
 |-  ( A e. RR -> -oo < A )
7 ltpnf 
 |-  ( A e. RR -> A < +oo )
8 df-ioo 
 |-  (,) = ( x e. RR* , y e. RR* |-> { z e. RR* | ( x < z /\ z < y ) } )
9 df-ico 
 |-  [,) = ( x e. RR* , y e. RR* |-> { z e. RR* | ( x <_ z /\ z < y ) } )
10 xrlenlt 
 |-  ( ( A e. RR* /\ w e. RR* ) -> ( A <_ w <-> -. w < A ) )
11 xrlttr 
 |-  ( ( w e. RR* /\ A e. RR* /\ +oo e. RR* ) -> ( ( w < A /\ A < +oo ) -> w < +oo ) )
12 xrltletr 
 |-  ( ( -oo e. RR* /\ A e. RR* /\ w e. RR* ) -> ( ( -oo < A /\ A <_ w ) -> -oo < w ) )
13 8 9 10 8 11 12 ixxun 
 |-  ( ( ( -oo e. RR* /\ A e. RR* /\ +oo e. RR* ) /\ ( -oo < A /\ A < +oo ) ) -> ( ( -oo (,) A ) u. ( A [,) +oo ) ) = ( -oo (,) +oo ) )
14 2 3 5 6 7 13 syl32anc 
 |-  ( A e. RR -> ( ( -oo (,) A ) u. ( A [,) +oo ) ) = ( -oo (,) +oo ) )
15 ioomax 
 |-  ( -oo (,) +oo ) = RR
16 14 15 eqtrdi 
 |-  ( A e. RR -> ( ( -oo (,) A ) u. ( A [,) +oo ) ) = RR )
17 ioossre 
 |-  ( -oo (,) A ) C_ RR
18 8 9 10 ixxdisj 
 |-  ( ( -oo e. RR* /\ A e. RR* /\ +oo e. RR* ) -> ( ( -oo (,) A ) i^i ( A [,) +oo ) ) = (/) )
19 1 3 5 18 mp3an2i 
 |-  ( A e. RR -> ( ( -oo (,) A ) i^i ( A [,) +oo ) ) = (/) )
20 uneqdifeq 
 |-  ( ( ( -oo (,) A ) C_ RR /\ ( ( -oo (,) A ) i^i ( A [,) +oo ) ) = (/) ) -> ( ( ( -oo (,) A ) u. ( A [,) +oo ) ) = RR <-> ( RR \ ( -oo (,) A ) ) = ( A [,) +oo ) ) )
21 17 19 20 sylancr 
 |-  ( A e. RR -> ( ( ( -oo (,) A ) u. ( A [,) +oo ) ) = RR <-> ( RR \ ( -oo (,) A ) ) = ( A [,) +oo ) ) )
22 16 21 mpbid 
 |-  ( A e. RR -> ( RR \ ( -oo (,) A ) ) = ( A [,) +oo ) )
23 retop 
 |-  ( topGen ` ran (,) ) e. Top
24 iooretop 
 |-  ( -oo (,) A ) e. ( topGen ` ran (,) )
25 uniretop 
 |-  RR = U. ( topGen ` ran (,) )
26 25 opncld 
 |-  ( ( ( topGen ` ran (,) ) e. Top /\ ( -oo (,) A ) e. ( topGen ` ran (,) ) ) -> ( RR \ ( -oo (,) A ) ) e. ( Clsd ` ( topGen ` ran (,) ) ) )
27 23 24 26 mp2an 
 |-  ( RR \ ( -oo (,) A ) ) e. ( Clsd ` ( topGen ` ran (,) ) )
28 22 27 eqeltrrdi 
 |-  ( A e. RR -> ( A [,) +oo ) e. ( Clsd ` ( topGen ` ran (,) ) ) )