Theorem toptopon2 22427

Description: A topology is the same thing as a topology on the union of its open sets. (Contributed by BJ, 27-Apr-2021.)

Assertion

Ref	Expression
toptopon2	⊢ (𝐽 ∈ Top ↔ 𝐽 ∈ (TopOn‘∪ 𝐽))

Proof of Theorem toptopon2

Step	Hyp	Ref	Expression
1		eqid 2732	. 2 ⊢ ∪ 𝐽 = ∪ 𝐽
2	1	toptopon 22426	1 ⊢ (𝐽 ∈ Top ↔ 𝐽 ∈ (TopOn‘∪ 𝐽))

Syntax hints:   ↔ wb 205   ∈ wcel 2106  ∪ cuni 4908  ‘cfv 6543  Topctop 22402  TopOnctopon 22419

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1797  ax-4 1811  ax-5 1913  ax-6 1971  ax-7 2011  ax-8 2108  ax-9 2116  ax-10 2137  ax-11 2154  ax-12 2171  ax-ext 2703  ax-sep 5299  ax-nul 5306  ax-pow 5363  ax-pr 5427  ax-un 7727

This theorem depends on definitions:  df-bi 206  df-an 397  df-or 846  df-3an 1089  df-tru 1544  df-fal 1554  df-ex 1782  df-nf 1786  df-sb 2068  df-mo 2534  df-eu 2563  df-clab 2710  df-cleq 2724  df-clel 2810  df-nfc 2885  df-ral 3062  df-rex 3071  df-rab 3433  df-v 3476  df-dif 3951  df-un 3953  df-in 3955  df-ss 3965  df-nul 4323  df-if 4529  df-pw 4604  df-sn 4629  df-pr 4631  df-op 4635  df-uni 4909  df-br 5149  df-opab 5211  df-mpt 5232  df-id 5574  df-xp 5682  df-rel 5683  df-cnv 5684  df-co 5685  df-dm 5686  df-iota 6495  df-fun 6545  df-fv 6551  df-topon 22420

This theorem is referenced by:  topontopon  22428  toprntopon  22434  neiptopreu  22644  lmcvg  22773  cnss1  22787  cnss2  22788  cnrest2  22797  cnrest2r  22798  lmss  22809  lmcnp  22815  lmcn  22816  t1t0  22859  haust1  22863  restcnrm  22873  resthauslem  22874  lmmo  22891  rncmp  22907  connima  22936  conncn  22937  kgeni  23048  kgenftop  23051  kgenss  23054  kgenhaus  23055  kgencmp2  23057  kgenidm  23058  1stckgen  23065  kgencn3  23069  kgen2cn  23070  dfac14  23129  ptcnplem  23132  ptcnp  23133  txcnmpt  23135  ptcn  23138  txdis1cn  23146  lmcn2  23160  txkgen  23163  xkohaus  23164  xkopt  23166  cnmpt11  23174  cnmpt11f  23175  cnmpt1t  23176  cnmpt12  23178  cnmpt21  23182  cnmpt21f  23183  cnmpt2t  23184  cnmpt22  23185  cnmpt22f  23186  cnmptcom  23189  cnmptkp  23191  cnmpt2k  23199  txconn  23200  qtopss  23226  qtopeu  23227  qtopomap  23229  qtopcmap  23230  kqtop  23256  kqt0  23257  nrmr0reg  23260  regr1  23261  kqreg  23262  kqnrm  23263  hmeoqtop  23286  hmphref  23292  xpstopnlem1  23320  ptcmpfi  23324  xkocnv  23325  xkohmeo  23326  kqhmph  23330  flimsncls  23497  cnpflfi  23510  flfcnp  23515  flfcnp2  23518  cnpfcfi  23551  cnextucn  23815  cnmpopc  24451  htpyco1  24501  htpyco2  24502  phtpyco2  24513  pcopt  24545  pcopt2  24546  pcorevlem  24549  pi1cof  24582  pi1coghm  24584  clduni  47611