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

Theorem toptopon 21520
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 21515 . . 3 (𝐽 ∈ (TopOn‘𝑋) ↔ (𝐽 ∈ Top ∧ 𝑋 = 𝐽))
31, 2mpbiran2 709 . 2 (𝐽 ∈ (TopOn‘𝑋) ↔ 𝐽 ∈ Top)
43bicomi 227 1 (𝐽 ∈ Top ↔ 𝐽 ∈ (TopOn‘𝑋))
Colors of variables: wff setvar class
Syntax hints:  wb 209   = wceq 1538  wcel 2115   cuni 4825  cfv 6344  Topctop 21496  TopOnctopon 21513
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1797  ax-4 1811  ax-5 1912  ax-6 1971  ax-7 2016  ax-8 2117  ax-9 2125  ax-10 2146  ax-11 2162  ax-12 2179  ax-ext 2796  ax-sep 5190  ax-nul 5197  ax-pow 5254  ax-pr 5318  ax-un 7452
This theorem depends on definitions:  df-bi 210  df-an 400  df-or 845  df-3an 1086  df-tru 1541  df-ex 1782  df-nf 1786  df-sb 2071  df-mo 2624  df-eu 2655  df-clab 2803  df-cleq 2817  df-clel 2896  df-nfc 2964  df-ral 3138  df-rex 3139  df-rab 3142  df-v 3482  df-sbc 3759  df-dif 3922  df-un 3924  df-in 3926  df-ss 3936  df-nul 4277  df-if 4451  df-pw 4524  df-sn 4551  df-pr 4553  df-op 4557  df-uni 4826  df-br 5054  df-opab 5116  df-mpt 5134  df-id 5448  df-xp 5549  df-rel 5550  df-cnv 5551  df-co 5552  df-dm 5553  df-iota 6303  df-fun 6346  df-fv 6352  df-topon 21514
This theorem is referenced by:  toptopon2  21521  eltpsi  21547  restuni  21765  stoig  21766  restlp  21786  restperf  21787  perfopn  21788  iscn2  21841  iscnp2  21842  cncnpi  21881  cncnp2  21884  cnnei  21885  cnrest  21888  cnpresti  21891  cnprest  21892  cnprest2  21893  paste  21897  t1sep2  21972  sshauslem  21975  1stcelcls  22064  kgenuni  22142  iskgen3  22152  txuni  22195  ptuniconst  22201  txcnmpt  22227  txcn  22229  txindis  22237  ptrescn  22242  txcmpb  22247  xkoptsub  22257  xkofvcn  22287  imasnopn  22293  imasncld  22294  imasncls  22295  qtopcmplem  22310  qtopkgen  22313  hmeof1o  22367  hmeores  22374  hmphindis  22400  cmphaushmeo  22403  txhmeo  22406  ptunhmeo  22411  hausflim  22584  flfneii  22595  hausflf  22600  flimfnfcls  22631  flfcntr  22646  cnextfun  22667  cnextfvval  22668  cnextf  22669  cnextcn  22670  cnextfres1  22671  retopon  23367  evth  23562  evth2  23563  qtophaus  31130  rrhre  31289  pconnconn  32505  connpconn  32509  pconnpi1  32511  sconnpi1  32513  txsconnlem  32514  txsconn  32515  cvxsconn  32517  cvmsf1o  32546  cvmliftmolem1  32555  cvmliftlem8  32566  cvmlift2lem9a  32577  cvmlift2lem9  32585  cvmlift2lem11  32587  cvmlift2lem12  32588  cvmliftphtlem  32591  cvmlift3lem6  32598  cvmlift3lem8  32600  cvmlift3lem9  32601  cnres2  35113  cnresima  35114  hausgraph  40012  ntrf2  40686  fcnre  41514
  Copyright terms: Public domain W3C validator