Theorem toptopon2 22641

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 2731	. 2 ⊢ ∪ 𝐽 = ∪ 𝐽
2	1	toptopon 22640	1 ⊢ (𝐽 ∈ Top ↔ 𝐽 ∈ (TopOn‘∪ 𝐽))

Syntax hints:   ↔ wb 205   ∈ wcel 2105  ∪ cuni 4908  ‘cfv 6543  Topctop 22616  TopOnctopon 22633

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1796  ax-4 1810  ax-5 1912  ax-6 1970  ax-7 2010  ax-8 2107  ax-9 2115  ax-10 2136  ax-11 2153  ax-12 2170  ax-ext 2702  ax-sep 5299  ax-nul 5306  ax-pow 5363  ax-pr 5427  ax-un 7729

This theorem depends on definitions:  df-bi 206  df-an 396  df-or 845  df-3an 1088  df-tru 1543  df-fal 1553  df-ex 1781  df-nf 1785  df-sb 2067  df-mo 2533  df-eu 2562  df-clab 2709  df-cleq 2723  df-clel 2809  df-nfc 2884  df-ral 3061  df-rex 3070  df-rab 3432  df-v 3475  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 22634

This theorem is referenced by:  topontopon  22642  toprntopon  22648  neiptopreu  22858  lmcvg  22987  cnss1  23001  cnss2  23002  cnrest2  23011  cnrest2r  23012  lmss  23023  lmcnp  23029  lmcn  23030  t1t0  23073  haust1  23077  restcnrm  23087  resthauslem  23088  lmmo  23105  rncmp  23121  connima  23150  conncn  23151  kgeni  23262  kgenftop  23265  kgenss  23268  kgenhaus  23269  kgencmp2  23271  kgenidm  23272  1stckgen  23279  kgencn3  23283  kgen2cn  23284  dfac14  23343  ptcnplem  23346  ptcnp  23347  txcnmpt  23349  ptcn  23352  txdis1cn  23360  lmcn2  23374  txkgen  23377  xkohaus  23378  xkopt  23380  cnmpt11  23388  cnmpt11f  23389  cnmpt1t  23390  cnmpt12  23392  cnmpt21  23396  cnmpt21f  23397  cnmpt2t  23398  cnmpt22  23399  cnmpt22f  23400  cnmptcom  23403  cnmptkp  23405  cnmpt2k  23413  txconn  23414  qtopss  23440  qtopeu  23441  qtopomap  23443  qtopcmap  23444  kqtop  23470  kqt0  23471  nrmr0reg  23474  regr1  23475  kqreg  23476  kqnrm  23477  hmeoqtop  23500  hmphref  23506  xpstopnlem1  23534  ptcmpfi  23538  xkocnv  23539  xkohmeo  23540  kqhmph  23544  flimsncls  23711  cnpflfi  23724  flfcnp  23729  flfcnp2  23732  cnpfcfi  23765  cnextucn  24029  cnmpopc  24670  htpyco1  24725  htpyco2  24726  phtpyco2  24737  pcopt  24770  pcopt2  24771  pcorevlem  24774  pi1cof  24807  pi1coghm  24809  clduni  47621