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

Theorem toptopon 19561
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 19553 . . 3  |-  ( J  e.  (TopOn `  X
)  <->  ( J  e. 
Top  /\  X  =  U. J ) )
31, 2mpbiran2 919 . 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 1395    e. wcel 1819   U.cuni 4251   ` cfv 5594   Topctop 19521  TopOnctopon 19522
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1619  ax-4 1632  ax-5 1705  ax-6 1748  ax-7 1791  ax-8 1821  ax-9 1823  ax-10 1838  ax-11 1843  ax-12 1855  ax-13 2000  ax-ext 2435  ax-sep 4578  ax-nul 4586  ax-pow 4634  ax-pr 4695  ax-un 6591
This theorem depends on definitions:  df-bi 185  df-or 370  df-an 371  df-3an 975  df-tru 1398  df-ex 1614  df-nf 1618  df-sb 1741  df-eu 2287  df-mo 2288  df-clab 2443  df-cleq 2449  df-clel 2452  df-nfc 2607  df-ne 2654  df-ral 2812  df-rex 2813  df-rab 2816  df-v 3111  df-sbc 3328  df-dif 3474  df-un 3476  df-in 3478  df-ss 3485  df-nul 3794  df-if 3945  df-pw 4017  df-sn 4033  df-pr 4035  df-op 4039  df-uni 4252  df-br 4457  df-opab 4516  df-mpt 4517  df-id 4804  df-xp 5014  df-rel 5015  df-cnv 5016  df-co 5017  df-dm 5018  df-iota 5557  df-fun 5596  df-fv 5602  df-topon 19529
This theorem is referenced by:  eltpsi  19574  neiptopreu  19761  restuni  19790  stoig  19791  restlp  19811  restperf  19812  perfopn  19813  iscn2  19866  iscnp2  19867  lmcvg  19890  cnss1  19904  cnss2  19905  cncnpi  19906  cncnp2  19909  cnnei  19910  cnrest  19913  cnrest2  19914  cnrest2r  19915  cnpresti  19916  cnprest  19917  cnprest2  19918  paste  19922  lmss  19926  lmcnp  19932  lmcn  19933  t1t0  19976  haust1  19980  restcnrm  19990  resthauslem  19991  t1sep2  19997  sshauslem  20000  lmmo  20008  rncmp  20023  conima  20052  concn  20053  1stcelcls  20088  kgeni  20164  kgenuni  20166  kgenftop  20167  kgenss  20170  kgenhaus  20171  kgencmp2  20173  kgenidm  20174  iskgen3  20176  1stckgen  20181  kgencn3  20185  kgen2cn  20186  txuni  20219  ptuniconst  20225  dfac14  20245  ptcnplem  20248  ptcnp  20249  txcnmpt  20251  txcn  20253  ptcn  20254  txindis  20261  txdis1cn  20262  ptrescn  20266  txcmpb  20271  lmcn2  20276  txkgen  20279  xkohaus  20280  xkoptsub  20281  xkopt  20282  cnmpt11  20290  cnmpt11f  20291  cnmpt1t  20292  cnmpt12  20294  cnmpt21  20298  cnmpt21f  20299  cnmpt2t  20300  cnmpt22  20301  cnmpt22f  20302  cnmptcom  20305  cnmptkp  20307  xkofvcn  20311  cnmpt2k  20315  txcon  20316  imasnopn  20317  imasncld  20318  imasncls  20319  qtopcmplem  20334  qtopkgen  20337  qtopss  20342  qtopeu  20343  qtopomap  20345  qtopcmap  20346  kqtop  20372  kqt0  20373  nrmr0reg  20376  regr1  20377  kqreg  20378  kqnrm  20379  hmeof1o  20391  hmeores  20398  hmeoqtop  20402  hmphref  20408  hmphindis  20424  cmphaushmeo  20427  txhmeo  20430  ptunhmeo  20435  xpstopnlem1  20436  ptcmpfi  20440  xkocnv  20441  xkohmeo  20442  kqhmph  20446  hausflim  20608  flimsncls  20613  flfneii  20619  hausflf  20624  cnpflfi  20626  flfcnp  20631  flfcnp2  20634  flimfnfcls  20655  cnpfcfi  20667  cnextfun  20690  cnextfvval  20691  cnextf  20692  cnextcn  20693  cnextfres  20694  cnextucn  20932  retopon  21396  cnmpt2pc  21554  evth  21585  evth2  21586  htpyco1  21604  htpyco2  21605  phtpyco2  21616  pcopt  21648  pcopt2  21649  pcorevlem  21652  pi1cof  21685  pi1coghm  21687  qtophaus  28000  pconcon  28873  conpcon  28877  pconpi1  28879  sconpi1  28881  txsconlem  28882  txscon  28883  cvxscon  28885  cvmsf1o  28914  cvmliftmolem1  28923  cvmliftlem8  28934  cvmlift2lem9a  28945  cvmlift2lem9  28953  cvmlift2lem11  28955  cvmlift2lem12  28956  cvmliftphtlem  28959  cvmlift3lem6  28966  cvmlift3lem8  28968  cvmlift3lem9  28969  cnres2  30464  cnresima  30465  hausgraph  31376  fcnre  31603
  Copyright terms: Public domain W3C validator