Metamath Proof Explorer

Theorem leordtval2

Description: The topology of the extended reals. (Contributed by Mario Carneiro, 3-Sep-2015)

Ref Expression
Hypotheses leordtval.1 
|- A = ran ( x e. RR* |-> ( x (,] +oo ) )
leordtval.2 
|- B = ran ( x e. RR* |-> ( -oo [,) x ) )
Assertion leordtval2 
|- ( ordTop ` <_ ) = ( topGen ` ( fi ` ( A u. B ) ) )

Proof

Step Hyp Ref Expression
1 leordtval.1 
 |-  A = ran ( x e. RR* |-> ( x (,] +oo ) )
2 leordtval.2 
 |-  B = ran ( x e. RR* |-> ( -oo [,) x ) )
3 letsr 
 |-  <_ e. TosetRel
4 ledm 
 |-  RR* = dom <_
5 1 leordtvallem1 
 |-  A = ran ( x e. RR* |-> { y e. RR* | -. y <_ x } )
6 1 2 leordtvallem2 
 |-  B = ran ( x e. RR* |-> { y e. RR* | -. x <_ y } )
7 4 5 6 ordtval 
 |-  ( <_ e. TosetRel -> ( ordTop ` <_ ) = ( topGen ` ( fi ` ( { RR* } u. ( A u. B ) ) ) ) )
8 3 7 ax-mp 
 |-  ( ordTop ` <_ ) = ( topGen ` ( fi ` ( { RR* } u. ( A u. B ) ) ) )
9 snex 
 |-  { RR* } e. _V
10 xrex 
 |-  RR* e. _V
11 10 pwex 
 |-  ~P RR* e. _V
12 eqid 
 |-  ( x e. RR* |-> ( x (,] +oo ) ) = ( x e. RR* |-> ( x (,] +oo ) )
13 iocssxr 
 |-  ( x (,] +oo ) C_ RR*
14 10 13 elpwi2 
 |-  ( x (,] +oo ) e. ~P RR*
15 14 a1i 
 |-  ( x e. RR* -> ( x (,] +oo ) e. ~P RR* )
16 12 15 fmpti 
 |-  ( x e. RR* |-> ( x (,] +oo ) ) : RR* --> ~P RR*
17 frn 
 |-  ( ( x e. RR* |-> ( x (,] +oo ) ) : RR* --> ~P RR* -> ran ( x e. RR* |-> ( x (,] +oo ) ) C_ ~P RR* )
18 16 17 ax-mp 
 |-  ran ( x e. RR* |-> ( x (,] +oo ) ) C_ ~P RR*
19 1 18 eqsstri 
 |-  A C_ ~P RR*
20 eqid 
 |-  ( x e. RR* |-> ( -oo [,) x ) ) = ( x e. RR* |-> ( -oo [,) x ) )
21 icossxr 
 |-  ( -oo [,) x ) C_ RR*
22 10 21 elpwi2 
 |-  ( -oo [,) x ) e. ~P RR*
23 22 a1i 
 |-  ( x e. RR* -> ( -oo [,) x ) e. ~P RR* )
24 20 23 fmpti 
 |-  ( x e. RR* |-> ( -oo [,) x ) ) : RR* --> ~P RR*
25 frn 
 |-  ( ( x e. RR* |-> ( -oo [,) x ) ) : RR* --> ~P RR* -> ran ( x e. RR* |-> ( -oo [,) x ) ) C_ ~P RR* )
26 24 25 ax-mp 
 |-  ran ( x e. RR* |-> ( -oo [,) x ) ) C_ ~P RR*
27 2 26 eqsstri 
 |-  B C_ ~P RR*
28 19 27 unssi 
 |-  ( A u. B ) C_ ~P RR*
29 11 28 ssexi 
 |-  ( A u. B ) e. _V
30 9 29 unex 
 |-  ( { RR* } u. ( A u. B ) ) e. _V
31 ssun2 
 |-  ( A u. B ) C_ ( { RR* } u. ( A u. B ) )
32 fiss 
 |-  ( ( ( { RR* } u. ( A u. B ) ) e. _V /\ ( A u. B ) C_ ( { RR* } u. ( A u. B ) ) ) -> ( fi ` ( A u. B ) ) C_ ( fi ` ( { RR* } u. ( A u. B ) ) ) )
33 30 31 32 mp2an 
 |-  ( fi ` ( A u. B ) ) C_ ( fi ` ( { RR* } u. ( A u. B ) ) )
34 fvex 
 |-  ( topGen ` ( fi ` ( A u. B ) ) ) e. _V
35 ovex 
 |-  ( 0 (,] +oo ) e. _V
36 ovex 
 |-  ( -oo [,) 1 ) e. _V
37 35 36 unipr 
 |-  U. { ( 0 (,] +oo ) , ( -oo [,) 1 ) } = ( ( 0 (,] +oo ) u. ( -oo [,) 1 ) )
38 iocssxr 
 |-  ( 0 (,] +oo ) C_ RR*
39 icossxr 
 |-  ( -oo [,) 1 ) C_ RR*
40 38 39 unssi 
 |-  ( ( 0 (,] +oo ) u. ( -oo [,) 1 ) ) C_ RR*
41 mnfxr 
 |-  -oo e. RR*
42 0xr 
 |-  0 e. RR*
43 pnfxr 
 |-  +oo e. RR*
44 mnflt0 
 |-  -oo < 0
45 0lepnf 
 |-  0 <_ +oo
46 df-icc 
 |-  [,] = ( x e. RR* , y e. RR* |-> { z e. RR* | ( x <_ z /\ z <_ y ) } )
47 df-ioc 
 |-  (,] = ( x e. RR* , y e. RR* |-> { z e. RR* | ( x < z /\ z <_ y ) } )
48 xrltnle 
 |-  ( ( 0 e. RR* /\ w e. RR* ) -> ( 0 < w <-> -. w <_ 0 ) )
49 xrletr 
 |-  ( ( w e. RR* /\ 0 e. RR* /\ +oo e. RR* ) -> ( ( w <_ 0 /\ 0 <_ +oo ) -> w <_ +oo ) )
50 xrlttr 
 |-  ( ( -oo e. RR* /\ 0 e. RR* /\ w e. RR* ) -> ( ( -oo < 0 /\ 0 < w ) -> -oo < w ) )
51 xrltle 
 |-  ( ( -oo e. RR* /\ w e. RR* ) -> ( -oo < w -> -oo <_ w ) )
52 51 3adant2 
 |-  ( ( -oo e. RR* /\ 0 e. RR* /\ w e. RR* ) -> ( -oo < w -> -oo <_ w ) )
53 50 52 syld 
 |-  ( ( -oo e. RR* /\ 0 e. RR* /\ w e. RR* ) -> ( ( -oo < 0 /\ 0 < w ) -> -oo <_ w ) )
54 46 47 48 46 49 53 ixxun 
 |-  ( ( ( -oo e. RR* /\ 0 e. RR* /\ +oo e. RR* ) /\ ( -oo < 0 /\ 0 <_ +oo ) ) -> ( ( -oo [,] 0 ) u. ( 0 (,] +oo ) ) = ( -oo [,] +oo ) )
55 44 45 54 mpanr12 
 |-  ( ( -oo e. RR* /\ 0 e. RR* /\ +oo e. RR* ) -> ( ( -oo [,] 0 ) u. ( 0 (,] +oo ) ) = ( -oo [,] +oo ) )
56 41 42 43 55 mp3an 
 |-  ( ( -oo [,] 0 ) u. ( 0 (,] +oo ) ) = ( -oo [,] +oo )
57 1xr 
 |-  1 e. RR*
58 0lt1 
 |-  0 < 1
59 df-ico 
 |-  [,) = ( x e. RR* , y e. RR* |-> { z e. RR* | ( x <_ z /\ z < y ) } )
60 xrlelttr 
 |-  ( ( w e. RR* /\ 0 e. RR* /\ 1 e. RR* ) -> ( ( w <_ 0 /\ 0 < 1 ) -> w < 1 ) )
61 59 46 60 ixxss2 
 |-  ( ( 1 e. RR* /\ 0 < 1 ) -> ( -oo [,] 0 ) C_ ( -oo [,) 1 ) )
62 57 58 61 mp2an 
 |-  ( -oo [,] 0 ) C_ ( -oo [,) 1 )
63 unss1 
 |-  ( ( -oo [,] 0 ) C_ ( -oo [,) 1 ) -> ( ( -oo [,] 0 ) u. ( 0 (,] +oo ) ) C_ ( ( -oo [,) 1 ) u. ( 0 (,] +oo ) ) )
64 62 63 ax-mp 
 |-  ( ( -oo [,] 0 ) u. ( 0 (,] +oo ) ) C_ ( ( -oo [,) 1 ) u. ( 0 (,] +oo ) )
65 56 64 eqsstrri 
 |-  ( -oo [,] +oo ) C_ ( ( -oo [,) 1 ) u. ( 0 (,] +oo ) )
66 iccmax 
 |-  ( -oo [,] +oo ) = RR*
67 uncom 
 |-  ( ( -oo [,) 1 ) u. ( 0 (,] +oo ) ) = ( ( 0 (,] +oo ) u. ( -oo [,) 1 ) )
68 65 66 67 3sstr3i 
 |-  RR* C_ ( ( 0 (,] +oo ) u. ( -oo [,) 1 ) )
69 40 68 eqssi 
 |-  ( ( 0 (,] +oo ) u. ( -oo [,) 1 ) ) = RR*
70 37 69 eqtri 
 |-  U. { ( 0 (,] +oo ) , ( -oo [,) 1 ) } = RR*
71 fvex 
 |-  ( fi ` ( A u. B ) ) e. _V
72 ssun1 
 |-  A C_ ( A u. B )
73 eqid 
 |-  ( 0 (,] +oo ) = ( 0 (,] +oo )
74 oveq1 
 |-  ( x = 0 -> ( x (,] +oo ) = ( 0 (,] +oo ) )
75 74 rspceeqv 
 |-  ( ( 0 e. RR* /\ ( 0 (,] +oo ) = ( 0 (,] +oo ) ) -> E. x e. RR* ( 0 (,] +oo ) = ( x (,] +oo ) )
76 42 73 75 mp2an 
 |-  E. x e. RR* ( 0 (,] +oo ) = ( x (,] +oo )
77 ovex 
 |-  ( x (,] +oo ) e. _V
78 12 77 elrnmpti 
 |-  ( ( 0 (,] +oo ) e. ran ( x e. RR* |-> ( x (,] +oo ) ) <-> E. x e. RR* ( 0 (,] +oo ) = ( x (,] +oo ) )
79 76 78 mpbir 
 |-  ( 0 (,] +oo ) e. ran ( x e. RR* |-> ( x (,] +oo ) )
80 79 1 eleqtrri 
 |-  ( 0 (,] +oo ) e. A
81 72 80 sselii 
 |-  ( 0 (,] +oo ) e. ( A u. B )
82 ssun2 
 |-  B C_ ( A u. B )
83 eqid 
 |-  ( -oo [,) 1 ) = ( -oo [,) 1 )
84 oveq2 
 |-  ( x = 1 -> ( -oo [,) x ) = ( -oo [,) 1 ) )
85 84 rspceeqv 
 |-  ( ( 1 e. RR* /\ ( -oo [,) 1 ) = ( -oo [,) 1 ) ) -> E. x e. RR* ( -oo [,) 1 ) = ( -oo [,) x ) )
86 57 83 85 mp2an 
 |-  E. x e. RR* ( -oo [,) 1 ) = ( -oo [,) x )
87 ovex 
 |-  ( -oo [,) x ) e. _V
88 20 87 elrnmpti 
 |-  ( ( -oo [,) 1 ) e. ran ( x e. RR* |-> ( -oo [,) x ) ) <-> E. x e. RR* ( -oo [,) 1 ) = ( -oo [,) x ) )
89 86 88 mpbir 
 |-  ( -oo [,) 1 ) e. ran ( x e. RR* |-> ( -oo [,) x ) )
90 89 2 eleqtrri 
 |-  ( -oo [,) 1 ) e. B
91 82 90 sselii 
 |-  ( -oo [,) 1 ) e. ( A u. B )
92 prssi 
 |-  ( ( ( 0 (,] +oo ) e. ( A u. B ) /\ ( -oo [,) 1 ) e. ( A u. B ) ) -> { ( 0 (,] +oo ) , ( -oo [,) 1 ) } C_ ( A u. B ) )
93 81 91 92 mp2an 
 |-  { ( 0 (,] +oo ) , ( -oo [,) 1 ) } C_ ( A u. B )
94 ssfii 
 |-  ( ( A u. B ) e. _V -> ( A u. B ) C_ ( fi ` ( A u. B ) ) )
95 29 94 ax-mp 
 |-  ( A u. B ) C_ ( fi ` ( A u. B ) )
96 93 95 sstri 
 |-  { ( 0 (,] +oo ) , ( -oo [,) 1 ) } C_ ( fi ` ( A u. B ) )
97 eltg3i 
 |-  ( ( ( fi ` ( A u. B ) ) e. _V /\ { ( 0 (,] +oo ) , ( -oo [,) 1 ) } C_ ( fi ` ( A u. B ) ) ) -> U. { ( 0 (,] +oo ) , ( -oo [,) 1 ) } e. ( topGen ` ( fi ` ( A u. B ) ) ) )
98 71 96 97 mp2an 
 |-  U. { ( 0 (,] +oo ) , ( -oo [,) 1 ) } e. ( topGen ` ( fi ` ( A u. B ) ) )
99 70 98 eqeltrri 
 |-  RR* e. ( topGen ` ( fi ` ( A u. B ) ) )
100 snssi 
 |-  ( RR* e. ( topGen ` ( fi ` ( A u. B ) ) ) -> { RR* } C_ ( topGen ` ( fi ` ( A u. B ) ) ) )
101 99 100 ax-mp 
 |-  { RR* } C_ ( topGen ` ( fi ` ( A u. B ) ) )
102 bastg 
 |-  ( ( fi ` ( A u. B ) ) e. _V -> ( fi ` ( A u. B ) ) C_ ( topGen ` ( fi ` ( A u. B ) ) ) )
103 71 102 ax-mp 
 |-  ( fi ` ( A u. B ) ) C_ ( topGen ` ( fi ` ( A u. B ) ) )
104 95 103 sstri 
 |-  ( A u. B ) C_ ( topGen ` ( fi ` ( A u. B ) ) )
105 101 104 unssi 
 |-  ( { RR* } u. ( A u. B ) ) C_ ( topGen ` ( fi ` ( A u. B ) ) )
106 fiss 
 |-  ( ( ( topGen ` ( fi ` ( A u. B ) ) ) e. _V /\ ( { RR* } u. ( A u. B ) ) C_ ( topGen ` ( fi ` ( A u. B ) ) ) ) -> ( fi ` ( { RR* } u. ( A u. B ) ) ) C_ ( fi ` ( topGen ` ( fi ` ( A u. B ) ) ) ) )
107 34 105 106 mp2an 
 |-  ( fi ` ( { RR* } u. ( A u. B ) ) ) C_ ( fi ` ( topGen ` ( fi ` ( A u. B ) ) ) )
108 fibas 
 |-  ( fi ` ( A u. B ) ) e. TopBases
109 tgcl 
 |-  ( ( fi ` ( A u. B ) ) e. TopBases -> ( topGen ` ( fi ` ( A u. B ) ) ) e. Top )
110 fitop 
 |-  ( ( topGen ` ( fi ` ( A u. B ) ) ) e. Top -> ( fi ` ( topGen ` ( fi ` ( A u. B ) ) ) ) = ( topGen ` ( fi ` ( A u. B ) ) ) )
111 108 109 110 mp2b 
 |-  ( fi ` ( topGen ` ( fi ` ( A u. B ) ) ) ) = ( topGen ` ( fi ` ( A u. B ) ) )
112 107 111 sseqtri 
 |-  ( fi ` ( { RR* } u. ( A u. B ) ) ) C_ ( topGen ` ( fi ` ( A u. B ) ) )
113 2basgen 
 |-  ( ( ( fi ` ( A u. B ) ) C_ ( fi ` ( { RR* } u. ( A u. B ) ) ) /\ ( fi ` ( { RR* } u. ( A u. B ) ) ) C_ ( topGen ` ( fi ` ( A u. B ) ) ) ) -> ( topGen ` ( fi ` ( A u. B ) ) ) = ( topGen ` ( fi ` ( { RR* } u. ( A u. B ) ) ) ) )
114 33 112 113 mp2an 
 |-  ( topGen ` ( fi ` ( A u. B ) ) ) = ( topGen ` ( fi ` ( { RR* } u. ( A u. B ) ) ) )
115 8 114 eqtr4i 
 |-  ( ordTop ` <_ ) = ( topGen ` ( fi ` ( A u. B ) ) )