MPE Home Metamath Proof Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >  letopon Structured version   Visualization version   GIF version

Theorem letopon 22134
Description: The topology of the extended reals. (Contributed by Mario Carneiro, 3-Sep-2015.)
Assertion
Ref Expression
letopon (ordTop‘ ≤ ) ∈ (TopOn‘ℝ*)

Proof of Theorem letopon
StepHypRef Expression
1 letsr 18132 . 2 ≤ ∈ TosetRel
2 ledm 18129 . . 3 * = dom ≤
32ordttopon 22122 . 2 ( ≤ ∈ TosetRel → (ordTop‘ ≤ ) ∈ (TopOn‘ℝ*))
41, 3ax-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