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

Theorem toptopon 19879
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 19871 . . 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 1870   U.cuni 4222   ` cfv 5601   Topctop 19848  TopOnctopon 19849
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1665  ax-4 1678  ax-5 1751  ax-6 1797  ax-7 1841  ax-8 1872  ax-9 1874  ax-10 1889  ax-11 1894  ax-12 1907  ax-13 2055  ax-ext 2407  ax-sep 4548  ax-nul 4556  ax-pow 4603  ax-pr 4661  ax-un 6597
This theorem depends on definitions:  df-bi 188  df-or 371  df-an 372  df-3an 984  df-tru 1440  df-ex 1660  df-nf 1664  df-sb 1790  df-eu 2270  df-mo 2271  df-clab 2415  df-cleq 2421  df-clel 2424  df-nfc 2579  df-ne 2627  df-ral 2787  df-rex 2788  df-rab 2791  df-v 3089  df-sbc 3306  df-dif 3445  df-un 3447  df-in 3449  df-ss 3456  df-nul 3768  df-if 3916  df-pw 3987  df-sn 4003  df-pr 4005  df-op 4009  df-uni 4223  df-br 4427  df-opab 4485  df-mpt 4486  df-id 4769  df-xp 4860  df-rel 4861  df-cnv 4862  df-co 4863  df-dm 4864  df-iota 5565  df-fun 5603  df-fv 5609  df-topon 19854
This theorem is referenced by:  eltpsi  19892  neiptopreu  20080  restuni  20109  stoig  20110  restlp  20130  restperf  20131  perfopn  20132  iscn2  20185  iscnp2  20186  lmcvg  20209  cnss1  20223  cnss2  20224  cncnpi  20225  cncnp2  20228  cnnei  20229  cnrest  20232  cnrest2  20233  cnrest2r  20234  cnpresti  20235  cnprest  20236  cnprest2  20237  paste  20241  lmss  20245  lmcnp  20251  lmcn  20252  t1t0  20295  haust1  20299  restcnrm  20309  resthauslem  20310  t1sep2  20316  sshauslem  20319  lmmo  20327  rncmp  20342  conima  20371  concn  20372  1stcelcls  20407  kgeni  20483  kgenuni  20485  kgenftop  20486  kgenss  20489  kgenhaus  20490  kgencmp2  20492  kgenidm  20493  iskgen3  20495  1stckgen  20500  kgencn3  20504  kgen2cn  20505  txuni  20538  ptuniconst  20544  dfac14  20564  ptcnplem  20567  ptcnp  20568  txcnmpt  20570  txcn  20572  ptcn  20573  txindis  20580  txdis1cn  20581  ptrescn  20585  txcmpb  20590  lmcn2  20595  txkgen  20598  xkohaus  20599  xkoptsub  20600  xkopt  20601  cnmpt11  20609  cnmpt11f  20610  cnmpt1t  20611  cnmpt12  20613  cnmpt21  20617  cnmpt21f  20618  cnmpt2t  20619  cnmpt22  20620  cnmpt22f  20621  cnmptcom  20624  cnmptkp  20626  xkofvcn  20630  cnmpt2k  20634  txcon  20635  imasnopn  20636  imasncld  20637  imasncls  20638  qtopcmplem  20653  qtopkgen  20656  qtopss  20661  qtopeu  20662  qtopomap  20664  qtopcmap  20665  kqtop  20691  kqt0  20692  nrmr0reg  20695  regr1  20696  kqreg  20697  kqnrm  20698  hmeof1o  20710  hmeores  20717  hmeoqtop  20721  hmphref  20727  hmphindis  20743  cmphaushmeo  20746  txhmeo  20749  ptunhmeo  20754  xpstopnlem1  20755  ptcmpfi  20759  xkocnv  20760  xkohmeo  20761  kqhmph  20765  hausflim  20927  flimsncls  20932  flfneii  20938  hausflf  20943  cnpflfi  20945  flfcnp  20950  flfcnp2  20953  flimfnfcls  20974  cnpfcfi  20986  flfcntr  20989  cnextfun  21010  cnextfvval  21011  cnextf  21012  cnextcn  21013  cnextfres1  21014  cnextucn  21249  retopon  21695  cnmpt2pc  21852  evth  21883  evth2  21884  htpyco1  21902  htpyco2  21903  phtpyco2  21914  pcopt  21946  pcopt2  21947  pcorevlem  21950  pi1cof  21983  pi1coghm  21985  qtophaus  28502  rrhre  28664  pconcon  29742  conpcon  29746  pconpi1  29748  sconpi1  29750  txsconlem  29751  txscon  29752  cvxscon  29754  cvmsf1o  29783  cvmliftmolem1  29792  cvmliftlem8  29803  cvmlift2lem9a  29814  cvmlift2lem9  29822  cvmlift2lem11  29824  cvmlift2lem12  29825  cvmliftphtlem  29828  cvmlift3lem6  29835  cvmlift3lem8  29837  cvmlift3lem9  29838  cnres2  31798  cnresima  31799  hausgraph  35787  fcnre  36985
  Copyright terms: Public domain W3C validator