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

Theorem toptopon 16990
Description: Alternative definition of  Top in terms of TopOn. (Contributed by Mario Carneiro, 13-Aug-2015.)
Hypothesis
Ref Expression
toptopon.1  |-  X  = 
U. J
Assertion
Ref Expression
toptopon  |-  ( J  e.  Top  <->  J  e.  (TopOn `  X ) )

Proof of Theorem toptopon
StepHypRef Expression
1 toptopon.1 . . 3  |-  X  = 
U. J
2 istopon 16982 . . 3  |-  ( J  e.  (TopOn `  X
)  <->  ( J  e. 
Top  /\  X  =  U. J ) )
31, 2mpbiran2 886 . 2  |-  ( J  e.  (TopOn `  X
)  <->  J  e.  Top )
43bicomi 194 1  |-  ( J  e.  Top  <->  J  e.  (TopOn `  X ) )
Colors of variables: wff set class
Syntax hints:    <-> wb 177    = wceq 1652    e. wcel 1725   U.cuni 4007   ` cfv 5446   Topctop 16950  TopOnctopon 16951
This theorem is referenced by:  eltpsi  17003  neiptopreu  17189  restuni  17218  stoig  17219  restlp  17239  restperf  17240  perfopn  17241  iscn2  17294  iscnp2  17295  lmcvg  17318  cnss1  17332  cnss2  17333  cncnpi  17334  cncnp2  17337  cnnei  17338  cnrest  17341  cnrest2  17342  cnrest2r  17343  cnpresti  17344  cnprest  17345  cnprest2  17346  paste  17350  lmss  17354  lmcnp  17360  lmcn  17361  t1t0  17404  haust1  17408  restcnrm  17418  resthauslem  17419  t1sep2  17425  sshauslem  17428  lmmo  17436  rncmp  17451  conima  17480  concn  17481  1stcelcls  17516  kgeni  17561  kgenuni  17563  kgenftop  17564  kgenss  17567  kgenhaus  17568  kgencmp2  17570  kgenidm  17571  iskgen3  17573  1stckgen  17578  kgencn3  17582  kgen2cn  17583  txuni  17616  ptuniconst  17622  dfac14  17642  ptcnplem  17645  ptcnp  17646  txcnmpt  17648  txcn  17650  ptcn  17651  txindis  17658  txdis1cn  17659  ptrescn  17663  txcmpb  17668  lmcn2  17673  txkgen  17676  xkohaus  17677  xkoptsub  17678  xkopt  17679  cnmpt11  17687  cnmpt11f  17688  cnmpt1t  17689  cnmpt12  17691  cnmpt21  17695  cnmpt21f  17696  cnmpt2t  17697  cnmpt22  17698  cnmpt22f  17699  cnmptcom  17702  cnmptkp  17704  xkofvcn  17708  cnmpt2k  17712  txcon  17713  imasnopn  17714  imasncld  17715  imasncls  17716  qtopcmplem  17731  qtopkgen  17734  qtopss  17739  qtopeu  17740  qtopomap  17742  qtopcmap  17743  kqtop  17769  kqt0  17770  nrmr0reg  17773  regr1  17774  kqreg  17775  kqnrm  17776  hmeof1o  17788  hmeores  17795  hmeoqtop  17799  hmphref  17805  hmphindis  17821  cmphaushmeo  17824  txhmeo  17827  ptunhmeo  17832  xpstopnlem1  17833  ptcmpfi  17837  xkocnv  17838  xkohmeo  17839  kqhmph  17843  hausflim  18005  flimsncls  18010  flfneii  18016  hausflf  18021  cnpflfi  18023  flfcnp  18028  flfcnp2  18031  flimfnfcls  18052  cnpfcfi  18064  cnextfun  18087  cnextfvval  18088  cnextf  18089  cnextcn  18090  cnextfres  18091  cnextucn  18325  retopon  18789  cnmpt2pc  18945  evth  18976  evth2  18977  htpyco1  18995  htpyco2  18996  phtpyco2  19007  pcopt  19039  pcopt2  19040  pcorevlem  19043  pi1cof  19076  pi1coghm  19078  rrhre  24379  pconcon  24910  conpcon  24914  pconpi1  24916  sconpi1  24918  txsconlem  24919  txscon  24920  cvxscon  24922  cvmsf1o  24951  cvmliftmolem1  24960  cvmliftlem8  24971  cvmlift2lem9a  24982  cvmlift2lem9  24990  cvmlift2lem11  24992  cvmlift2lem12  24993  cvmliftphtlem  24996  cvmlift3lem6  25003  cvmlift3lem8  25005  cvmlift3lem9  25006  cnres2  26463  cnresima  26464  hausgraph  27499  fcnre  27663
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-3 7  ax-mp 8  ax-gen 1555  ax-5 1566  ax-17 1626  ax-9 1666  ax-8 1687  ax-13 1727  ax-14 1729  ax-6 1744  ax-7 1749  ax-11 1761  ax-12 1950  ax-ext 2416  ax-sep 4322  ax-nul 4330  ax-pow 4369  ax-pr 4395  ax-un 4693
This theorem depends on definitions:  df-bi 178  df-or 360  df-an 361  df-3an 938  df-tru 1328  df-ex 1551  df-nf 1554  df-sb 1659  df-eu 2284  df-mo 2285  df-clab 2422  df-cleq 2428  df-clel 2431  df-nfc 2560  df-ne 2600  df-ral 2702  df-rex 2703  df-rab 2706  df-v 2950  df-sbc 3154  df-dif 3315  df-un 3317  df-in 3319  df-ss 3326  df-nul 3621  df-if 3732  df-pw 3793  df-sn 3812  df-pr 3813  df-op 3815  df-uni 4008  df-br 4205  df-opab 4259  df-mpt 4260  df-id 4490  df-xp 4876  df-rel 4877  df-cnv 4878  df-co 4879  df-dm 4880  df-iota 5410  df-fun 5448  df-fv 5454  df-topon 16958
  Copyright terms: Public domain W3C validator