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

Theorem toptopon 18379
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 18371 . . 3  |-  ( J  e.  (TopOn `  X
)  <->  ( J  e. 
Top  /\  X  =  U. J ) )
31, 2mpbiran2 903 . 2  |-  ( J  e.  (TopOn `  X
)  <->  J  e.  Top )
43bicomi 202 1  |-  ( J  e.  Top  <->  J  e.  (TopOn `  X ) )
Colors of variables: wff setvar class
Syntax hints:    <-> wb 184    = wceq 1362    e. wcel 1755   U.cuni 4079   ` cfv 5406   Topctop 18339  TopOnctopon 18340
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1594  ax-4 1605  ax-5 1669  ax-6 1707  ax-7 1727  ax-8 1757  ax-9 1759  ax-10 1774  ax-11 1779  ax-12 1791  ax-13 1942  ax-ext 2414  ax-sep 4401  ax-nul 4409  ax-pow 4458  ax-pr 4519  ax-un 6361
This theorem depends on definitions:  df-bi 185  df-or 370  df-an 371  df-3an 960  df-tru 1365  df-ex 1590  df-nf 1593  df-sb 1700  df-eu 2258  df-mo 2259  df-clab 2420  df-cleq 2426  df-clel 2429  df-nfc 2558  df-ne 2598  df-ral 2710  df-rex 2711  df-rab 2714  df-v 2964  df-sbc 3176  df-dif 3319  df-un 3321  df-in 3323  df-ss 3330  df-nul 3626  df-if 3780  df-pw 3850  df-sn 3866  df-pr 3868  df-op 3872  df-uni 4080  df-br 4281  df-opab 4339  df-mpt 4340  df-id 4623  df-xp 4833  df-rel 4834  df-cnv 4835  df-co 4836  df-dm 4837  df-iota 5369  df-fun 5408  df-fv 5414  df-topon 18347
This theorem is referenced by:  eltpsi  18392  neiptopreu  18578  restuni  18607  stoig  18608  restlp  18628  restperf  18629  perfopn  18630  iscn2  18683  iscnp2  18684  lmcvg  18707  cnss1  18721  cnss2  18722  cncnpi  18723  cncnp2  18726  cnnei  18727  cnrest  18730  cnrest2  18731  cnrest2r  18732  cnpresti  18733  cnprest  18734  cnprest2  18735  paste  18739  lmss  18743  lmcnp  18749  lmcn  18750  t1t0  18793  haust1  18797  restcnrm  18807  resthauslem  18808  t1sep2  18814  sshauslem  18817  lmmo  18825  rncmp  18840  conima  18870  concn  18871  1stcelcls  18906  kgeni  18951  kgenuni  18953  kgenftop  18954  kgenss  18957  kgenhaus  18958  kgencmp2  18960  kgenidm  18961  iskgen3  18963  1stckgen  18968  kgencn3  18972  kgen2cn  18973  txuni  19006  ptuniconst  19012  dfac14  19032  ptcnplem  19035  ptcnp  19036  txcnmpt  19038  txcn  19040  ptcn  19041  txindis  19048  txdis1cn  19049  ptrescn  19053  txcmpb  19058  lmcn2  19063  txkgen  19066  xkohaus  19067  xkoptsub  19068  xkopt  19069  cnmpt11  19077  cnmpt11f  19078  cnmpt1t  19079  cnmpt12  19081  cnmpt21  19085  cnmpt21f  19086  cnmpt2t  19087  cnmpt22  19088  cnmpt22f  19089  cnmptcom  19092  cnmptkp  19094  xkofvcn  19098  cnmpt2k  19102  txcon  19103  imasnopn  19104  imasncld  19105  imasncls  19106  qtopcmplem  19121  qtopkgen  19124  qtopss  19129  qtopeu  19130  qtopomap  19132  qtopcmap  19133  kqtop  19159  kqt0  19160  nrmr0reg  19163  regr1  19164  kqreg  19165  kqnrm  19166  hmeof1o  19178  hmeores  19185  hmeoqtop  19189  hmphref  19195  hmphindis  19211  cmphaushmeo  19214  txhmeo  19217  ptunhmeo  19222  xpstopnlem1  19223  ptcmpfi  19227  xkocnv  19228  xkohmeo  19229  kqhmph  19233  hausflim  19395  flimsncls  19400  flfneii  19406  hausflf  19411  cnpflfi  19413  flfcnp  19418  flfcnp2  19421  flimfnfcls  19442  cnpfcfi  19454  cnextfun  19477  cnextfvval  19478  cnextf  19479  cnextcn  19480  cnextfres  19481  cnextucn  19719  retopon  20183  cnmpt2pc  20341  evth  20372  evth2  20373  htpyco1  20391  htpyco2  20392  phtpyco2  20403  pcopt  20435  pcopt2  20436  pcorevlem  20439  pi1cof  20472  pi1coghm  20474  rrhre  26300  pconcon  26967  conpcon  26971  pconpi1  26973  sconpi1  26975  txsconlem  26976  txscon  26977  cvxscon  26979  cvmsf1o  27008  cvmliftmolem1  27017  cvmliftlem8  27028  cvmlift2lem9a  27039  cvmlift2lem9  27047  cvmlift2lem11  27049  cvmlift2lem12  27050  cvmliftphtlem  27053  cvmlift3lem6  27060  cvmlift3lem8  27062  cvmlift3lem9  27063  cnres2  28503  cnresima  28504  hausgraph  29422  fcnre  29589
  Copyright terms: Public domain W3C validator