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

Theorem toptopon 21846
Description: Alternative definition of Top in terms of TopOn. (Contributed by Mario Carneiro, 13-Aug-2015.)
Hypothesis
Ref Expression
toptopon.1 𝑋 = 𝐽
Assertion
Ref Expression
toptopon (𝐽 ∈ Top ↔ 𝐽 ∈ (TopOn‘𝑋))

Proof of Theorem toptopon
StepHypRef Expression
1 toptopon.1 . . 3 𝑋 = 𝐽
2 istopon 21841 . . 3 (𝐽 ∈ (TopOn‘𝑋) ↔ (𝐽 ∈ Top ∧ 𝑋 = 𝐽))
31, 2mpbiran2 710 . 2 (𝐽 ∈ (TopOn‘𝑋) ↔ 𝐽 ∈ Top)
43bicomi 227 1 (𝐽 ∈ Top ↔ 𝐽 ∈ (TopOn‘𝑋))
Colors of variables: wff setvar class
Syntax hints:  wb 209   = wceq 1543  wcel 2112   cuni 4836  cfv 6401  Topctop 21822  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
This theorem depends on definitions:  df-bi 210  df-an 400  df-or 848  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-ral 3069  df-rex 3070  df-rab 3073  df-v 3425  df-dif 3886  df-un 3888  df-in 3890  df-ss 3900  df-nul 4255  df-if 4457  df-pw 4532  df-sn 4559  df-pr 4561  df-op 4565  df-uni 4837  df-br 5071  df-opab 5133  df-mpt 5153  df-id 5472  df-xp 5575  df-rel 5576  df-cnv 5577  df-co 5578  df-dm 5579  df-iota 6359  df-fun 6403  df-fv 6409  df-topon 21840
This theorem is referenced by:  toptopon2  21847  eltpsi  21873  restuni  22091  stoig  22092  restlp  22112  restperf  22113  perfopn  22114  iscn2  22167  iscnp2  22168  cncnpi  22207  cncnp2  22210  cnnei  22211  cnrest  22214  cnpresti  22217  cnprest  22218  cnprest2  22219  paste  22223  t1sep2  22298  sshauslem  22301  1stcelcls  22390  kgenuni  22468  iskgen3  22478  txuni  22521  ptuniconst  22527  txcnmpt  22553  txcn  22555  txindis  22563  ptrescn  22568  txcmpb  22573  xkoptsub  22583  xkofvcn  22613  imasnopn  22619  imasncld  22620  imasncls  22621  qtopcmplem  22636  qtopkgen  22639  hmeof1o  22693  hmeores  22700  hmphindis  22726  cmphaushmeo  22729  txhmeo  22732  ptunhmeo  22737  hausflim  22910  flfneii  22921  hausflf  22926  flimfnfcls  22957  flfcntr  22972  cnextfun  22993  cnextfvval  22994  cnextf  22995  cnextcn  22996  cnextfres1  22997  retopon  23693  evth  23888  evth2  23889  qtophaus  31532  rrhre  31715  pconnconn  32937  connpconn  32941  pconnpi1  32943  sconnpi1  32945  txsconnlem  32946  txsconn  32947  cvxsconn  32949  cvmsf1o  32978  cvmliftmolem1  32987  cvmliftlem8  32998  cvmlift2lem9a  33009  cvmlift2lem9  33017  cvmlift2lem11  33019  cvmlift2lem12  33020  cvmliftphtlem  33023  cvmlift3lem6  33030  cvmlift3lem8  33032  cvmlift3lem9  33033  cnres2  35695  cnresima  35696  hausgraph  40788  ntrf2  41459  fcnre  42289
  Copyright terms: Public domain W3C validator