Theorem toptopon 20548

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 20540	. . 3 ⊢ (𝐽 ∈ (TopOn‘𝑋) ↔ (𝐽 ∈ Top ∧ 𝑋 = ∪ 𝐽))
3	1, 2	mpbiran2 956	. 2 ⊢ (𝐽 ∈ (TopOn‘𝑋) ↔ 𝐽 ∈ Top)
4	3	bicomi 213	1 ⊢ (𝐽 ∈ Top ↔ 𝐽 ∈ (TopOn‘𝑋))

Syntax hints:   ↔ wb 195   = wceq 1475   ∈ wcel 1977  ∪ cuni 4372  ‘cfv 5804  Topctop 20517  TopOnctopon 20518

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1713  ax-4 1728  ax-5 1827  ax-6 1875  ax-7 1922  ax-8 1979  ax-9 1986  ax-10 2006  ax-11 2021  ax-12 2034  ax-13 2234  ax-ext 2590  ax-sep 4709  ax-nul 4717  ax-pow 4769  ax-pr 4833  ax-un 6847

This theorem depends on definitions:  df-bi 196  df-or 384  df-an 385  df-3an 1033  df-tru 1478  df-ex 1696  df-nf 1701  df-sb 1868  df-eu 2462  df-mo 2463  df-clab 2597  df-cleq 2603  df-clel 2606  df-nfc 2740  df-ne 2782  df-ral 2901  df-rex 2902  df-rab 2905  df-v 3175  df-sbc 3403  df-dif 3543  df-un 3545  df-in 3547  df-ss 3554  df-nul 3875  df-if 4037  df-pw 4110  df-sn 4126  df-pr 4128  df-op 4132  df-uni 4373  df-br 4584  df-opab 4644  df-mpt 4645  df-id 4953  df-xp 5044  df-rel 5045  df-cnv 5046  df-co 5047  df-dm 5048  df-iota 5768  df-fun 5806  df-fv 5812  df-topon 20523

This theorem is referenced by:  eltpsi  20561  neiptopreu  20747  restuni  20776  stoig  20777  restlp  20797  restperf  20798  perfopn  20799  iscn2  20852  iscnp2  20853  lmcvg  20876  cnss1  20890  cnss2  20891  cncnpi  20892  cncnp2  20895  cnnei  20896  cnrest  20899  cnrest2  20900  cnrest2r  20901  cnpresti  20902  cnprest  20903  cnprest2  20904  paste  20908  lmss  20912  lmcnp  20918  lmcn  20919  t1t0  20962  haust1  20966  restcnrm  20976  resthauslem  20977  t1sep2  20983  sshauslem  20986  lmmo  20994  rncmp  21009  conima  21038  concn  21039  1stcelcls  21074  kgeni  21150  kgenuni  21152  kgenftop  21153  kgenss  21156  kgenhaus  21157  kgencmp2  21159  kgenidm  21160  iskgen3  21162  1stckgen  21167  kgencn3  21171  kgen2cn  21172  txuni  21205  ptuniconst  21211  dfac14  21231  ptcnplem  21234  ptcnp  21235  txcnmpt  21237  txcn  21239  ptcn  21240  txindis  21247  txdis1cn  21248  ptrescn  21252  txcmpb  21257  lmcn2  21262  txkgen  21265  xkohaus  21266  xkoptsub  21267  xkopt  21268  cnmpt11  21276  cnmpt11f  21277  cnmpt1t  21278  cnmpt12  21280  cnmpt21  21284  cnmpt21f  21285  cnmpt2t  21286  cnmpt22  21287  cnmpt22f  21288  cnmptcom  21291  cnmptkp  21293  xkofvcn  21297  cnmpt2k  21301  txcon  21302  imasnopn  21303  imasncld  21304  imasncls  21305  qtopcmplem  21320  qtopkgen  21323  qtopss  21328  qtopeu  21329  qtopomap  21331  qtopcmap  21332  kqtop  21358  kqt0  21359  nrmr0reg  21362  regr1  21363  kqreg  21364  kqnrm  21365  hmeof1o  21377  hmeores  21384  hmeoqtop  21388  hmphref  21394  hmphindis  21410  cmphaushmeo  21413  txhmeo  21416  ptunhmeo  21421  xpstopnlem1  21422  ptcmpfi  21426  xkocnv  21427  xkohmeo  21428  kqhmph  21432  hausflim  21595  flimsncls  21600  flfneii  21606  hausflf  21611  cnpflfi  21613  flfcnp  21618  flfcnp2  21621  flimfnfcls  21642  cnpfcfi  21654  flfcntr  21657  cnextfun  21678  cnextfvval  21679  cnextf  21680  cnextcn  21681  cnextfres1  21682  cnextucn  21917  retopon  22377  cnmpt2pc  22535  evth  22566  evth2  22567  htpyco1  22585  htpyco2  22586  phtpyco2  22597  pcopt  22630  pcopt2  22631  pcorevlem  22634  pi1cof  22667  pi1coghm  22669  qtophaus  29231  rrhre  29393  pconcon  30467  conpcon  30471  pconpi1  30473  sconpi1  30475  txsconlem  30476  txscon  30477  cvxscon  30479  cvmsf1o  30508  cvmliftmolem1  30517  cvmliftlem8  30528  cvmlift2lem9a  30539  cvmlift2lem9  30547  cvmlift2lem11  30549  cvmlift2lem12  30550  cvmliftphtlem  30553  cvmlift3lem6  30560  cvmlift3lem8  30562  cvmlift3lem9  30563  bj-toptopon2  32234  cnres2  32732  cnresima  32733  hausgraph  36809  ntrf2  37442  fcnre  38207