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 ) )`
` |-  ( ( -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 )`
` |-  ( ( ( 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 ) ) )`