Metamath Proof Explorer < Previous   Next > Nearby theorems Mirrors  >  Home  >  MPE Home  >  Th. List  >  iocpnfordt Structured version   Unicode version

Theorem iocpnfordt 17280
 Description: An unbounded above open interval is open in the order topology of the extended reals. (Contributed by Mario Carneiro, 3-Sep-2015.)
Assertion
Ref Expression
iocpnfordt ordTop

Proof of Theorem iocpnfordt
Dummy variables are mutually distinct and distinct from all other variables.
StepHypRef Expression
1 eqid 2437 . . . . . . . . 9
2 eqid 2437 . . . . . . . . 9
3 eqid 2437 . . . . . . . . 9
41, 2, 3leordtval 17278 . . . . . . . 8 ordTop
5 letop 17271 . . . . . . . 8 ordTop
64, 5eqeltrri 2508 . . . . . . 7
7 tgclb 17036 . . . . . . 7
86, 7mpbir 202 . . . . . 6
9 bastg 17032 . . . . . 6
108, 9ax-mp 8 . . . . 5
1110, 4sseqtr4i 3382 . . . 4 ordTop
12 ssun1 3511 . . . . 5
13 ssun1 3511 . . . . . 6
14 eqid 2437 . . . . . . . 8
15 oveq1 6089 . . . . . . . . . 10
1615eqeq2d 2448 . . . . . . . . 9
1716rspcev 3053 . . . . . . . 8
1814, 17mpan2 654 . . . . . . 7
19 eqid 2437 . . . . . . . 8
20 ovex 6107 . . . . . . . 8
2119, 20elrnmpti 5122 . . . . . . 7
2218, 21sylibr 205 . . . . . 6
2313, 22sseldi 3347 . . . . 5
2412, 23sseldi 3347 . . . 4
2511, 24sseldi 3347 . . 3 ordTop