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

Theorem toptopon 17003
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 16995 . . 3  |-  ( J  e.  (TopOn `  X
)  <->  ( J  e. 
Top  /\  X  =  U. J ) )
31, 2mpbiran2 887 . 2  |-  ( J  e.  (TopOn `  X
)  <->  J  e.  Top )
43bicomi 195 1  |-  ( J  e.  Top  <->  J  e.  (TopOn `  X ) )
Colors of variables: wff set class
Syntax hints:    <-> wb 178    = wceq 1653    e. wcel 1726   U.cuni 4017   ` cfv 5457   Topctop 16963  TopOnctopon 16964
This theorem is referenced by:  eltpsi  17016  neiptopreu  17202  restuni  17231  stoig  17232  restlp  17252  restperf  17253  perfopn  17254  iscn2  17307  iscnp2  17308  lmcvg  17331  cnss1  17345  cnss2  17346  cncnpi  17347  cncnp2  17350  cnnei  17351  cnrest  17354  cnrest2  17355  cnrest2r  17356  cnpresti  17357  cnprest  17358  cnprest2  17359  paste  17363  lmss  17367  lmcnp  17373  lmcn  17374  t1t0  17417  haust1  17421  restcnrm  17431  resthauslem  17432  t1sep2  17438  sshauslem  17441  lmmo  17449  rncmp  17464  conima  17493  concn  17494  1stcelcls  17529  kgeni  17574  kgenuni  17576  kgenftop  17577  kgenss  17580  kgenhaus  17581  kgencmp2  17583  kgenidm  17584  iskgen3  17586  1stckgen  17591  kgencn3  17595  kgen2cn  17596  txuni  17629  ptuniconst  17635  dfac14  17655  ptcnplem  17658  ptcnp  17659  txcnmpt  17661  txcn  17663  ptcn  17664  txindis  17671  txdis1cn  17672  ptrescn  17676  txcmpb  17681  lmcn2  17686  txkgen  17689  xkohaus  17690  xkoptsub  17691  xkopt  17692  cnmpt11  17700  cnmpt11f  17701  cnmpt1t  17702  cnmpt12  17704  cnmpt21  17708  cnmpt21f  17709  cnmpt2t  17710  cnmpt22  17711  cnmpt22f  17712  cnmptcom  17715  cnmptkp  17717  xkofvcn  17721  cnmpt2k  17725  txcon  17726  imasnopn  17727  imasncld  17728  imasncls  17729  qtopcmplem  17744  qtopkgen  17747  qtopss  17752  qtopeu  17753  qtopomap  17755  qtopcmap  17756  kqtop  17782  kqt0  17783  nrmr0reg  17786  regr1  17787  kqreg  17788  kqnrm  17789  hmeof1o  17801  hmeores  17808  hmeoqtop  17812  hmphref  17818  hmphindis  17834  cmphaushmeo  17837  txhmeo  17840  ptunhmeo  17845  xpstopnlem1  17846  ptcmpfi  17850  xkocnv  17851  xkohmeo  17852  kqhmph  17856  hausflim  18018  flimsncls  18023  flfneii  18029  hausflf  18034  cnpflfi  18036  flfcnp  18041  flfcnp2  18044  flimfnfcls  18065  cnpfcfi  18077  cnextfun  18100  cnextfvval  18101  cnextf  18102  cnextcn  18103  cnextfres  18104  cnextucn  18338  retopon  18802  cnmpt2pc  18958  evth  18989  evth2  18990  htpyco1  19008  htpyco2  19009  phtpyco2  19020  pcopt  19052  pcopt2  19053  pcorevlem  19056  pi1cof  19089  pi1coghm  19091  rrhre  24392  pconcon  24923  conpcon  24927  pconpi1  24929  sconpi1  24931  txsconlem  24932  txscon  24933  cvxscon  24935  cvmsf1o  24964  cvmliftmolem1  24973  cvmliftlem8  24984  cvmlift2lem9a  24995  cvmlift2lem9  25003  cvmlift2lem11  25005  cvmlift2lem12  25006  cvmliftphtlem  25009  cvmlift3lem6  25016  cvmlift3lem8  25018  cvmlift3lem9  25019  cnres2  26486  cnresima  26487  hausgraph  27522  fcnre  27686
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1556  ax-5 1567  ax-17 1627  ax-9 1667  ax-8 1688  ax-13 1728  ax-14 1730  ax-6 1745  ax-7 1750  ax-11 1762  ax-12 1951  ax-ext 2419  ax-sep 4333  ax-nul 4341  ax-pow 4380  ax-pr 4406  ax-un 4704
This theorem depends on definitions:  df-bi 179  df-or 361  df-an 362  df-3an 939  df-tru 1329  df-ex 1552  df-nf 1555  df-sb 1660  df-eu 2287  df-mo 2288  df-clab 2425  df-cleq 2431  df-clel 2434  df-nfc 2563  df-ne 2603  df-ral 2712  df-rex 2713  df-rab 2716  df-v 2960  df-sbc 3164  df-dif 3325  df-un 3327  df-in 3329  df-ss 3336  df-nul 3631  df-if 3742  df-pw 3803  df-sn 3822  df-pr 3823  df-op 3825  df-uni 4018  df-br 4216  df-opab 4270  df-mpt 4271  df-id 4501  df-xp 4887  df-rel 4888  df-cnv 4889  df-co 4890  df-dm 4891  df-iota 5421  df-fun 5459  df-fv 5465  df-topon 16971
  Copyright terms: Public domain W3C validator