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

Theorem icomnfordt 17285
 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
icomnfordt ordTop

Proof of Theorem icomnfordt
Dummy variables are mutually distinct and distinct from all other variables.
StepHypRef Expression
1 eqid 2438 . . . . . . . . 9
2 eqid 2438 . . . . . . . . 9
3 eqid 2438 . . . . . . . . 9
41, 2, 3leordtval 17282 . . . . . . . 8 ordTop
5 letop 17275 . . . . . . . 8 ordTop
64, 5eqeltrri 2509 . . . . . . 7
7 tgclb 17040 . . . . . . 7
86, 7mpbir 202 . . . . . 6
9 bastg 17036 . . . . . 6
108, 9ax-mp 5 . . . . 5
1110, 4sseqtr4i 3383 . . . 4 ordTop
12 ssun1 3512 . . . . 5
13 ssun2 3513 . . . . . 6
14 eqid 2438 . . . . . . . 8
15 oveq2 6092 . . . . . . . . . 10
1615eqeq2d 2449 . . . . . . . . 9
1716rspcev 3054 . . . . . . . 8
1814, 17mpan2 654 . . . . . . 7
19 eqid 2438 . . . . . . . 8
20 ovex 6109 . . . . . . . 8
2119, 20elrnmpti 5124 . . . . . . 7
2218, 21sylibr 205 . . . . . 6
2313, 22sseldi 3348 . . . . 5
2412, 23sseldi 3348 . . . 4
2511, 24sseldi 3348 . . 3 ordTop