Theorem toptopon 20648

Description: Alternative definition of Top in terms of TopOn. (Contributed by Mario Carneiro, 13-Aug-2015.)

Hypothesis

Ref	Expression
toptopon.1	⊢ 𝑋 = ∪ 𝐽

Assertion

Ref	Expression
toptopon	⊢ (𝐽 ∈ Top ↔ 𝐽 ∈ (TopOn‘𝑋))

Proof of Theorem toptopon

Step	Hyp	Ref	Expression
1		toptopon.1	. . 3 ⊢ 𝑋 = ∪ 𝐽
2		istopon 20640	. . 3 ⊢ (𝐽 ∈ (TopOn‘𝑋) ↔ (𝐽 ∈ Top ∧ 𝑋 = ∪ 𝐽))
3	1, 2	mpbiran2 953	. 2 ⊢ (𝐽 ∈ (TopOn‘𝑋) ↔ 𝐽 ∈ Top)
4	3	bicomi 214	1 ⊢ (𝐽 ∈ Top ↔ 𝐽 ∈ (TopOn‘𝑋))

Syntax hints:   ↔ wb 196   = wceq 1480   ∈ wcel 1987  ∪ cuni 4402  ‘cfv 5847  Topctop 20617  TopOnctopon 20618

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1719  ax-4 1734  ax-5 1836  ax-6 1885  ax-7 1932  ax-8 1989  ax-9 1996  ax-10 2016  ax-11 2031  ax-12 2044  ax-13 2245  ax-ext 2601  ax-sep 4741  ax-nul 4749  ax-pow 4803  ax-pr 4867  ax-un 6902

This theorem depends on definitions:  df-bi 197  df-or 385  df-an 386  df-3an 1038  df-tru 1483  df-ex 1702  df-nf 1707  df-sb 1878  df-eu 2473  df-mo 2474  df-clab 2608  df-cleq 2614  df-clel 2617  df-nfc 2750  df-ne 2791  df-ral 2912  df-rex 2913  df-rab 2916  df-v 3188  df-sbc 3418  df-dif 3558  df-un 3560  df-in 3562  df-ss 3569  df-nul 3892  df-if 4059  df-pw 4132  df-sn 4149  df-pr 4151  df-op 4155  df-uni 4403  df-br 4614  df-opab 4674  df-mpt 4675  df-id 4989  df-xp 5080  df-rel 5081  df-cnv 5082  df-co 5083  df-dm 5084  df-iota 5810  df-fun 5849  df-fv 5855  df-topon 20623

This theorem is referenced by:  eltpsi  20661  neiptopreu  20847  restuni  20876  stoig  20877  restlp  20897  restperf  20898  perfopn  20899  iscn2  20952  iscnp2  20953  lmcvg  20976  cnss1  20990  cnss2  20991  cncnpi  20992  cncnp2  20995  cnnei  20996  cnrest  20999  cnrest2  21000  cnrest2r  21001  cnpresti  21002  cnprest  21003  cnprest2  21004  paste  21008  lmss  21012  lmcnp  21018  lmcn  21019  t1t0  21062  haust1  21066  restcnrm  21076  resthauslem  21077  t1sep2  21083  sshauslem  21086  lmmo  21094  rncmp  21109  connima  21138  conncn  21139  1stcelcls  21174  kgeni  21250  kgenuni  21252  kgenftop  21253  kgenss  21256  kgenhaus  21257  kgencmp2  21259  kgenidm  21260  iskgen3  21262  1stckgen  21267  kgencn3  21271  kgen2cn  21272  txuni  21305  ptuniconst  21311  dfac14  21331  ptcnplem  21334  ptcnp  21335  txcnmpt  21337  txcn  21339  ptcn  21340  txindis  21347  txdis1cn  21348  ptrescn  21352  txcmpb  21357  lmcn2  21362  txkgen  21365  xkohaus  21366  xkoptsub  21367  xkopt  21368  cnmpt11  21376  cnmpt11f  21377  cnmpt1t  21378  cnmpt12  21380  cnmpt21  21384  cnmpt21f  21385  cnmpt2t  21386  cnmpt22  21387  cnmpt22f  21388  cnmptcom  21391  cnmptkp  21393  xkofvcn  21397  cnmpt2k  21401  txconn  21402  imasnopn  21403  imasncld  21404  imasncls  21405  qtopcmplem  21420  qtopkgen  21423  qtopss  21428  qtopeu  21429  qtopomap  21431  qtopcmap  21432  kqtop  21458  kqt0  21459  nrmr0reg  21462  regr1  21463  kqreg  21464  kqnrm  21465  hmeof1o  21477  hmeores  21484  hmeoqtop  21488  hmphref  21494  hmphindis  21510  cmphaushmeo  21513  txhmeo  21516  ptunhmeo  21521  xpstopnlem1  21522  ptcmpfi  21526  xkocnv  21527  xkohmeo  21528  kqhmph  21532  hausflim  21695  flimsncls  21700  flfneii  21706  hausflf  21711  cnpflfi  21713  flfcnp  21718  flfcnp2  21721  flimfnfcls  21742  cnpfcfi  21754  flfcntr  21757  cnextfun  21778  cnextfvval  21779  cnextf  21780  cnextcn  21781  cnextfres1  21782  cnextucn  22017  retopon  22477  cnmpt2pc  22635  evth  22666  evth2  22667  htpyco1  22685  htpyco2  22686  phtpyco2  22697  pcopt  22730  pcopt2  22731  pcorevlem  22734  pi1cof  22767  pi1coghm  22769  qtophaus  29682  rrhre  29844  pconnconn  30918  connpconn  30922  pconnpi1  30924  sconnpi1  30926  txsconnlem  30927  txsconn  30928  cvxsconn  30930  cvmsf1o  30959  cvmliftmolem1  30968  cvmliftlem8  30979  cvmlift2lem9a  30990  cvmlift2lem9  30998  cvmlift2lem11  31000  cvmlift2lem12  31001  cvmliftphtlem  31004  cvmlift3lem6  31011  cvmlift3lem8  31013  cvmlift3lem9  31014  bj-toptopon2  32687  cnres2  33191  cnresima  33192  hausgraph  37268  ntrf2  37901  fcnre  38664