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

Theorem toptopon 19883
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 19875 . . 3  |-  ( J  e.  (TopOn `  X
)  <->  ( J  e. 
Top  /\  X  =  U. J ) )
31, 2mpbiran2 927 . 2  |-  ( J  e.  (TopOn `  X
)  <->  J  e.  Top )
43bicomi 205 1  |-  ( J  e.  Top  <->  J  e.  (TopOn `  X ) )
Colors of variables: wff setvar class
Syntax hints:    <-> wb 187    = wceq 1437    e. wcel 1872   U.cuni 4155   ` cfv 5537   Topctop 19852  TopOnctopon 19853
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1663  ax-4 1676  ax-5 1752  ax-6 1798  ax-7 1843  ax-8 1874  ax-9 1876  ax-10 1891  ax-11 1896  ax-12 1909  ax-13 2058  ax-ext 2402  ax-sep 4482  ax-nul 4491  ax-pow 4538  ax-pr 4596  ax-un 6534
This theorem depends on definitions:  df-bi 188  df-or 371  df-an 372  df-3an 984  df-tru 1440  df-ex 1658  df-nf 1662  df-sb 1791  df-eu 2274  df-mo 2275  df-clab 2409  df-cleq 2415  df-clel 2418  df-nfc 2552  df-ne 2595  df-ral 2713  df-rex 2714  df-rab 2717  df-v 3018  df-sbc 3236  df-dif 3375  df-un 3377  df-in 3379  df-ss 3386  df-nul 3698  df-if 3848  df-pw 3919  df-sn 3935  df-pr 3937  df-op 3941  df-uni 4156  df-br 4360  df-opab 4419  df-mpt 4420  df-id 4704  df-xp 4795  df-rel 4796  df-cnv 4797  df-co 4798  df-dm 4799  df-iota 5501  df-fun 5539  df-fv 5545  df-topon 19858
This theorem is referenced by:  eltpsi  19896  neiptopreu  20084  restuni  20113  stoig  20114  restlp  20134  restperf  20135  perfopn  20136  iscn2  20189  iscnp2  20190  lmcvg  20213  cnss1  20227  cnss2  20228  cncnpi  20229  cncnp2  20232  cnnei  20233  cnrest  20236  cnrest2  20237  cnrest2r  20238  cnpresti  20239  cnprest  20240  cnprest2  20241  paste  20245  lmss  20249  lmcnp  20255  lmcn  20256  t1t0  20299  haust1  20303  restcnrm  20313  resthauslem  20314  t1sep2  20320  sshauslem  20323  lmmo  20331  rncmp  20346  conima  20375  concn  20376  1stcelcls  20411  kgeni  20487  kgenuni  20489  kgenftop  20490  kgenss  20493  kgenhaus  20494  kgencmp2  20496  kgenidm  20497  iskgen3  20499  1stckgen  20504  kgencn3  20508  kgen2cn  20509  txuni  20542  ptuniconst  20548  dfac14  20568  ptcnplem  20571  ptcnp  20572  txcnmpt  20574  txcn  20576  ptcn  20577  txindis  20584  txdis1cn  20585  ptrescn  20589  txcmpb  20594  lmcn2  20599  txkgen  20602  xkohaus  20603  xkoptsub  20604  xkopt  20605  cnmpt11  20613  cnmpt11f  20614  cnmpt1t  20615  cnmpt12  20617  cnmpt21  20621  cnmpt21f  20622  cnmpt2t  20623  cnmpt22  20624  cnmpt22f  20625  cnmptcom  20628  cnmptkp  20630  xkofvcn  20634  cnmpt2k  20638  txcon  20639  imasnopn  20640  imasncld  20641  imasncls  20642  qtopcmplem  20657  qtopkgen  20660  qtopss  20665  qtopeu  20666  qtopomap  20668  qtopcmap  20669  kqtop  20695  kqt0  20696  nrmr0reg  20699  regr1  20700  kqreg  20701  kqnrm  20702  hmeof1o  20714  hmeores  20721  hmeoqtop  20725  hmphref  20731  hmphindis  20747  cmphaushmeo  20750  txhmeo  20753  ptunhmeo  20758  xpstopnlem1  20759  ptcmpfi  20763  xkocnv  20764  xkohmeo  20765  kqhmph  20769  hausflim  20931  flimsncls  20936  flfneii  20942  hausflf  20947  cnpflfi  20949  flfcnp  20954  flfcnp2  20957  flimfnfcls  20978  cnpfcfi  20990  flfcntr  20993  cnextfun  21014  cnextfvval  21015  cnextf  21016  cnextcn  21017  cnextfres1  21018  cnextucn  21253  retopon  21719  cnmpt2pc  21891  evth  21922  evth2  21923  htpyco1  21944  htpyco2  21945  phtpyco2  21956  pcopt  21988  pcopt2  21989  pcorevlem  21992  pi1cof  22025  pi1coghm  22027  qtophaus  28608  rrhre  28770  pconcon  29899  conpcon  29903  pconpi1  29905  sconpi1  29907  txsconlem  29908  txscon  29909  cvxscon  29911  cvmsf1o  29940  cvmliftmolem1  29949  cvmliftlem8  29960  cvmlift2lem9a  29971  cvmlift2lem9  29979  cvmlift2lem11  29981  cvmlift2lem12  29982  cvmliftphtlem  29985  cvmlift3lem6  29992  cvmlift3lem8  29994  cvmlift3lem9  29995  cnres2  31996  cnresima  31997  hausgraph  35996  fcnre  37256
  Copyright terms: Public domain W3C validator