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

Theorem iocpnfordt 17233
 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 2404 . . . . . . . . 9
2 eqid 2404 . . . . . . . . 9
3 eqid 2404 . . . . . . . . 9
41, 2, 3leordtval 17231 . . . . . . . 8 ordTop
5 letop 17224 . . . . . . . 8 ordTop
64, 5eqeltrri 2475 . . . . . . 7
7 tgclb 16990 . . . . . . 7
86, 7mpbir 201 . . . . . 6
9 bastg 16986 . . . . . 6
108, 9ax-mp 8 . . . . 5
1110, 4sseqtr4i 3341 . . . 4 ordTop
12 ssun1 3470 . . . . 5
13 ssun1 3470 . . . . . 6
14 eqid 2404 . . . . . . . 8
15 oveq1 6047 . . . . . . . . . 10
1615eqeq2d 2415 . . . . . . . . 9
1716rspcev 3012 . . . . . . . 8
1814, 17mpan2 653 . . . . . . 7
19 eqid 2404 . . . . . . . 8
20 ovex 6065 . . . . . . . 8
2119, 20elrnmpti 5080 . . . . . . 7
2218, 21sylibr 204 . . . . . 6
2313, 22sseldi 3306 . . . . 5
2412, 23sseldi 3306 . . . 4
2511, 24sseldi 3306 . . 3 ordTop