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

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 e. RR -> ( -oo (,] A ) 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-ioc 
 |-  (,] = ( x e. RR* , y e. RR* |-> { z e. RR* | ( x < z /\ z <_ y ) } )
9 df-ioo 
 |-  (,) = ( x e. RR* , y e. RR* |-> { z e. RR* | ( x < z /\ z < y ) } )
10 xrltnle 
 |-  ( ( A e. RR* /\ w e. RR* ) -> ( A < w <-> -. w <_ A ) )
11 xrlelttr 
 |-  ( ( w e. RR* /\ A e. RR* /\ +oo e. RR* ) -> ( ( w <_ A /\ A < +oo ) -> w < +oo ) )
12 xrlttr 
 |-  ( ( -oo e. RR* /\ A e. RR* /\ w e. RR* ) -> ( ( -oo < A /\ A < w ) -> -oo < w ) )
13 8 9 10 9 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 iocssre 
 |-  ( ( -oo e. RR* /\ A e. RR ) -> ( -oo (,] A ) C_ RR )
18 1 17 mpan 
 |-  ( A e. RR -> ( -oo (,] A ) C_ RR )
19 8 9 10 ixxdisj 
 |-  ( ( -oo e. RR* /\ A e. RR* /\ +oo e. RR* ) -> ( ( -oo (,] A ) i^i ( A (,) +oo ) ) = (/) )
20 1 3 5 19 mp3an2i 
 |-  ( A e. RR -> ( ( -oo (,] A ) i^i ( A (,) +oo ) ) = (/) )
21 uneqdifeq 
 |-  ( ( ( -oo (,] A ) C_ RR /\ ( ( -oo (,] A ) i^i ( A (,) +oo ) ) = (/) ) -> ( ( ( -oo (,] A ) u. ( A (,) +oo ) ) = RR <-> ( RR \ ( -oo (,] A ) ) = ( A (,) +oo ) ) )
22 18 20 21 syl2anc 
 |-  ( A e. RR -> ( ( ( -oo (,] A ) u. ( A (,) +oo ) ) = RR <-> ( RR \ ( -oo (,] A ) ) = ( A (,) +oo ) ) )
23 16 22 mpbid 
 |-  ( A e. RR -> ( RR \ ( -oo (,] A ) ) = ( A (,) +oo ) )
24 iooretop 
 |-  ( A (,) +oo ) e. ( topGen ` ran (,) )
25 23 24 eqeltrdi 
 |-  ( A e. RR -> ( RR \ ( -oo (,] A ) ) e. ( topGen ` ran (,) ) )
26 retop 
 |-  ( topGen ` ran (,) ) e. Top
27 uniretop 
 |-  RR = U. ( topGen ` ran (,) )
28 27 iscld2 
 |-  ( ( ( topGen ` ran (,) ) e. Top /\ ( -oo (,] A ) C_ RR ) -> ( ( -oo (,] A ) e. ( Clsd ` ( topGen ` ran (,) ) ) <-> ( RR \ ( -oo (,] A ) ) e. ( topGen ` ran (,) ) ) )
29 26 18 28 sylancr 
 |-  ( A e. RR -> ( ( -oo (,] A ) e. ( Clsd ` ( topGen ` ran (,) ) ) <-> ( RR \ ( -oo (,] A ) ) e. ( topGen ` ran (,) ) ) )
30 25 29 mpbird 
 |-  ( A e. RR -> ( -oo (,] A ) e. ( Clsd ` ( topGen ` ran (,) ) ) )