Metamath Proof Explorer |
< Previous
Next >
Nearby theorems |
||
Mirrors > Home > MPE Home > Th. List > letopon | Structured version Visualization version GIF version |
Description: The topology of the extended reals. (Contributed by Mario Carneiro, 3-Sep-2015.) |
Ref | Expression |
---|---|
letopon | ⊢ (ordTop‘ ≤ ) ∈ (TopOn‘ℝ*) |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | letsr 18132 | . 2 ⊢ ≤ ∈ TosetRel | |
2 | ledm 18129 | . . 3 ⊢ ℝ* = dom ≤ | |
3 | 2 | ordttopon 22122 | . 2 ⊢ ( ≤ ∈ TosetRel → (ordTop‘ ≤ ) ∈ (TopOn‘ℝ*)) |
4 | 1, 3 | ax-mp 5 | 1 ⊢ (ordTop‘ ≤ ) ∈ (TopOn‘ℝ*) |
Colors of variables: wff setvar class |
Syntax hints: ∈ wcel 2112 ‘cfv 6401 ℝ*cxr 10896 ≤ cle 10898 ordTopcordt 17037 TosetRel ctsr 18104 TopOnctopon 21839 |
This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1803 ax-4 1817 ax-5 1918 ax-6 1976 ax-7 2016 ax-8 2114 ax-9 2122 ax-10 2143 ax-11 2160 ax-12 2177 ax-ext 2710 ax-sep 5209 ax-nul 5216 ax-pow 5275 ax-pr 5339 ax-un 7545 ax-cnex 10815 ax-resscn 10816 ax-pre-lttri 10833 ax-pre-lttrn 10834 |
This theorem depends on definitions: df-bi 210 df-an 400 df-or 848 df-3or 1090 df-3an 1091 df-tru 1546 df-fal 1556 df-ex 1788 df-nf 1792 df-sb 2073 df-mo 2541 df-eu 2570 df-clab 2717 df-cleq 2731 df-clel 2818 df-nfc 2889 df-ne 2944 df-nel 3050 df-ral 3069 df-rex 3070 df-reu 3071 df-rab 3073 df-v 3425 df-sbc 3712 df-csb 3829 df-dif 3886 df-un 3888 df-in 3890 df-ss 3900 df-pss 3902 df-nul 4255 df-if 4457 df-pw 4532 df-sn 4559 df-pr 4561 df-tp 4563 df-op 4565 df-uni 4837 df-int 4877 df-br 5071 df-opab 5133 df-mpt 5153 df-tr 5179 df-id 5472 df-eprel 5478 df-po 5486 df-so 5487 df-fr 5527 df-we 5529 df-xp 5575 df-rel 5576 df-cnv 5577 df-co 5578 df-dm 5579 df-rn 5580 df-res 5581 df-ima 5582 df-ord 6237 df-on 6238 df-lim 6239 df-suc 6240 df-iota 6359 df-fun 6403 df-fn 6404 df-f 6405 df-f1 6406 df-fo 6407 df-f1o 6408 df-fv 6409 df-om 7667 df-1o 8226 df-er 8415 df-en 8651 df-dom 8652 df-sdom 8653 df-fin 8654 df-fi 9057 df-pnf 10899 df-mnf 10900 df-xr 10901 df-ltxr 10902 df-le 10903 df-topgen 16981 df-ordt 17039 df-ps 18105 df-tsr 18106 df-top 21823 df-topon 21840 df-bases 21875 |
This theorem is referenced by: letop 22135 letopuni 22136 xrstopn 22137 xrstps 22138 xmetdcn 23767 metdcn2 23768 xrlimcnp 25883 xrge0pluscn 31636 xrge0mulc1cn 31637 lmlimxrge0 31644 pnfneige0 31647 lmxrge0 31648 esumcvg 31798 xlimres 43083 xlimcl 43084 xlimconst 43087 xlimbr 43089 xlimmnfvlem1 43094 xlimmnfvlem2 43095 xlimpnfvlem1 43098 xlimpnfvlem2 43099 |
Copyright terms: Public domain | W3C validator |