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

Theorem toptopon 18560
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 18552 . . 3  |-  ( J  e.  (TopOn `  X
)  <->  ( J  e. 
Top  /\  X  =  U. J ) )
31, 2mpbiran2 910 . 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 1369    e. wcel 1756   U.cuni 4112   ` cfv 5439   Topctop 18520  TopOnctopon 18521
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1591  ax-4 1602  ax-5 1670  ax-6 1708  ax-7 1728  ax-8 1758  ax-9 1760  ax-10 1775  ax-11 1780  ax-12 1792  ax-13 1943  ax-ext 2423  ax-sep 4434  ax-nul 4442  ax-pow 4491  ax-pr 4552  ax-un 6393
This theorem depends on definitions:  df-bi 185  df-or 370  df-an 371  df-3an 967  df-tru 1372  df-ex 1587  df-nf 1590  df-sb 1701  df-eu 2257  df-mo 2258  df-clab 2430  df-cleq 2436  df-clel 2439  df-nfc 2577  df-ne 2622  df-ral 2741  df-rex 2742  df-rab 2745  df-v 2995  df-sbc 3208  df-dif 3352  df-un 3354  df-in 3356  df-ss 3363  df-nul 3659  df-if 3813  df-pw 3883  df-sn 3899  df-pr 3901  df-op 3905  df-uni 4113  df-br 4314  df-opab 4372  df-mpt 4373  df-id 4657  df-xp 4867  df-rel 4868  df-cnv 4869  df-co 4870  df-dm 4871  df-iota 5402  df-fun 5441  df-fv 5447  df-topon 18528
This theorem is referenced by:  eltpsi  18573  neiptopreu  18759  restuni  18788  stoig  18789  restlp  18809  restperf  18810  perfopn  18811  iscn2  18864  iscnp2  18865  lmcvg  18888  cnss1  18902  cnss2  18903  cncnpi  18904  cncnp2  18907  cnnei  18908  cnrest  18911  cnrest2  18912  cnrest2r  18913  cnpresti  18914  cnprest  18915  cnprest2  18916  paste  18920  lmss  18924  lmcnp  18930  lmcn  18931  t1t0  18974  haust1  18978  restcnrm  18988  resthauslem  18989  t1sep2  18995  sshauslem  18998  lmmo  19006  rncmp  19021  conima  19051  concn  19052  1stcelcls  19087  kgeni  19132  kgenuni  19134  kgenftop  19135  kgenss  19138  kgenhaus  19139  kgencmp2  19141  kgenidm  19142  iskgen3  19144  1stckgen  19149  kgencn3  19153  kgen2cn  19154  txuni  19187  ptuniconst  19193  dfac14  19213  ptcnplem  19216  ptcnp  19217  txcnmpt  19219  txcn  19221  ptcn  19222  txindis  19229  txdis1cn  19230  ptrescn  19234  txcmpb  19239  lmcn2  19244  txkgen  19247  xkohaus  19248  xkoptsub  19249  xkopt  19250  cnmpt11  19258  cnmpt11f  19259  cnmpt1t  19260  cnmpt12  19262  cnmpt21  19266  cnmpt21f  19267  cnmpt2t  19268  cnmpt22  19269  cnmpt22f  19270  cnmptcom  19273  cnmptkp  19275  xkofvcn  19279  cnmpt2k  19283  txcon  19284  imasnopn  19285  imasncld  19286  imasncls  19287  qtopcmplem  19302  qtopkgen  19305  qtopss  19310  qtopeu  19311  qtopomap  19313  qtopcmap  19314  kqtop  19340  kqt0  19341  nrmr0reg  19344  regr1  19345  kqreg  19346  kqnrm  19347  hmeof1o  19359  hmeores  19366  hmeoqtop  19370  hmphref  19376  hmphindis  19392  cmphaushmeo  19395  txhmeo  19398  ptunhmeo  19403  xpstopnlem1  19404  ptcmpfi  19408  xkocnv  19409  xkohmeo  19410  kqhmph  19414  hausflim  19576  flimsncls  19581  flfneii  19587  hausflf  19592  cnpflfi  19594  flfcnp  19599  flfcnp2  19602  flimfnfcls  19623  cnpfcfi  19635  cnextfun  19658  cnextfvval  19659  cnextf  19660  cnextcn  19661  cnextfres  19662  cnextucn  19900  retopon  20364  cnmpt2pc  20522  evth  20553  evth2  20554  htpyco1  20572  htpyco2  20573  phtpyco2  20584  pcopt  20616  pcopt2  20617  pcorevlem  20620  pi1cof  20653  pi1coghm  20655  rrhre  26469  pconcon  27142  conpcon  27146  pconpi1  27148  sconpi1  27150  txsconlem  27151  txscon  27152  cvxscon  27154  cvmsf1o  27183  cvmliftmolem1  27192  cvmliftlem8  27203  cvmlift2lem9a  27214  cvmlift2lem9  27222  cvmlift2lem11  27224  cvmlift2lem12  27225  cvmliftphtlem  27228  cvmlift3lem6  27235  cvmlift3lem8  27237  cvmlift3lem9  27238  cnres2  28688  cnresima  28689  hausgraph  29606  fcnre  29773
  Copyright terms: Public domain W3C validator