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

Theorem toptopon 16727
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 16719 . . 3  |-  ( J  e.  (TopOn `  X
)  <->  ( J  e. 
Top  /\  X  =  U. J ) )
31, 2mpbiran2 885 . 2  |-  ( J  e.  (TopOn `  X
)  <->  J  e.  Top )
43bicomi 193 1  |-  ( J  e.  Top  <->  J  e.  (TopOn `  X ) )
Colors of variables: wff set class
Syntax hints:    <-> wb 176    = wceq 1633    e. wcel 1701   U.cuni 3864   ` cfv 5292   Topctop 16687  TopOnctopon 16688
This theorem is referenced by:  eltpsi  16740  restuni  16949  stoig  16950  restlp  16969  restperf  16970  perfopn  16971  iscn2  17024  iscnp2  17025  lmcvg  17048  cnss1  17061  cnss2  17062  cncnpi  17063  cncnp2  17066  cnrest  17069  cnrest2  17070  cnrest2r  17071  cnpresti  17072  cnprest  17073  cnprest2  17074  paste  17078  lmss  17082  lmcnp  17088  lmcn  17089  t1t0  17132  haust1  17136  restcnrm  17146  resthauslem  17147  t1sep2  17153  sshauslem  17156  lmmo  17164  rncmp  17179  conima  17207  concn  17208  1stcelcls  17243  kgeni  17288  kgenuni  17290  kgenftop  17291  kgenss  17294  kgenhaus  17295  kgencmp2  17297  kgenidm  17298  iskgen3  17300  1stckgen  17305  kgencn3  17309  kgen2cn  17310  txuni  17343  ptuniconst  17349  dfac14  17368  ptcnplem  17371  ptcnp  17372  txcnmpt  17374  txcn  17376  ptcn  17377  txindis  17384  txdis1cn  17385  ptrescn  17389  txcmpb  17394  lmcn2  17399  txkgen  17402  xkohaus  17403  xkoptsub  17404  xkopt  17405  cnmpt11  17413  cnmpt11f  17414  cnmpt1t  17415  cnmpt12  17417  cnmpt21  17421  cnmpt21f  17422  cnmpt2t  17423  cnmpt22  17424  cnmpt22f  17425  cnmptcom  17428  cnmptkp  17430  xkofvcn  17434  cnmpt2k  17438  txcon  17439  qtopcmplem  17454  qtopkgen  17457  qtopss  17462  qtopeu  17463  qtopomap  17465  qtopcmap  17466  kqtop  17492  kqt0  17493  nrmr0reg  17496  regr1  17497  kqreg  17498  kqnrm  17499  hmeof1o  17511  hmeores  17518  hmeoqtop  17522  hmphref  17528  hmphindis  17544  cmphaushmeo  17547  txhmeo  17550  ptunhmeo  17555  xpstopnlem1  17556  ptcmpfi  17560  xkocnv  17561  xkohmeo  17562  kqhmph  17566  hausflim  17728  flimsncls  17733  flfneii  17739  hausflf  17744  cnpflfi  17746  flfcnp  17751  flfcnp2  17754  flimfnfcls  17775  cnpfcfi  17787  retopon  18324  cnmpt2pc  18479  evth  18510  evth2  18511  htpyco1  18529  htpyco2  18530  phtpyco2  18541  pcopt  18573  pcopt2  18574  pcorevlem  18577  pi1cof  18610  pi1coghm  18612  cnextfun  23414  cnextfvval  23415  pconcon  24046  conpcon  24050  pconpi1  24052  sconpi1  24054  txsconlem  24055  txscon  24056  cvxscon  24058  cvmsf1o  24087  cvmliftmolem1  24096  cvmliftlem8  24107  cvmlift2lem9a  24118  cvmlift2lem9  24126  cvmlift2lem11  24128  cvmlift2lem12  24129  cvmliftphtlem  24132  cvmlift3lem6  24139  cvmlift3lem8  24141  cvmlift3lem9  24142  dfcon2OLD  25402  connsubOLD  25403  cnres2  25631  cnresima  25632  hausgraph  26679  fcnre  26844
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-3 7  ax-mp 8  ax-gen 1537  ax-5 1548  ax-17 1607  ax-9 1645  ax-8 1666  ax-13 1703  ax-14 1705  ax-6 1720  ax-7 1725  ax-11 1732  ax-12 1897  ax-ext 2297  ax-sep 4178  ax-nul 4186  ax-pow 4225  ax-pr 4251  ax-un 4549
This theorem depends on definitions:  df-bi 177  df-or 359  df-an 360  df-3an 936  df-tru 1310  df-ex 1533  df-nf 1536  df-sb 1640  df-eu 2180  df-mo 2181  df-clab 2303  df-cleq 2309  df-clel 2312  df-nfc 2441  df-ne 2481  df-ral 2582  df-rex 2583  df-rab 2586  df-v 2824  df-sbc 3026  df-dif 3189  df-un 3191  df-in 3193  df-ss 3200  df-nul 3490  df-if 3600  df-pw 3661  df-sn 3680  df-pr 3681  df-op 3683  df-uni 3865  df-br 4061  df-opab 4115  df-mpt 4116  df-id 4346  df-xp 4732  df-rel 4733  df-cnv 4734  df-co 4735  df-dm 4736  df-iota 5256  df-fun 5294  df-fv 5300  df-topon 16695
  Copyright terms: Public domain W3C validator