Theorem toptopon2 22067

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

Syntax hints:   ↔ wb 205   ∈ wcel 2106  ∪ cuni 4839  ‘cfv 6433  Topctop 22042  TopOnctopon 22059

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1798  ax-4 1812  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 2709  ax-sep 5223  ax-nul 5230  ax-pow 5288  ax-pr 5352  ax-un 7588

This theorem depends on definitions:  df-bi 206  df-an 397  df-or 845  df-3an 1088  df-tru 1542  df-fal 1552  df-ex 1783  df-nf 1787  df-sb 2068  df-mo 2540  df-eu 2569  df-clab 2716  df-cleq 2730  df-clel 2816  df-nfc 2889  df-ral 3069  df-rex 3070  df-rab 3073  df-v 3434  df-dif 3890  df-un 3892  df-in 3894  df-ss 3904  df-nul 4257  df-if 4460  df-pw 4535  df-sn 4562  df-pr 4564  df-op 4568  df-uni 4840  df-br 5075  df-opab 5137  df-mpt 5158  df-id 5489  df-xp 5595  df-rel 5596  df-cnv 5597  df-co 5598  df-dm 5599  df-iota 6391  df-fun 6435  df-fv 6441  df-topon 22060

This theorem is referenced by:  topontopon  22068  toprntopon  22074  neiptopreu  22284  lmcvg  22413  cnss1  22427  cnss2  22428  cnrest2  22437  cnrest2r  22438  lmss  22449  lmcnp  22455  lmcn  22456  t1t0  22499  haust1  22503  restcnrm  22513  resthauslem  22514  lmmo  22531  rncmp  22547  connima  22576  conncn  22577  kgeni  22688  kgenftop  22691  kgenss  22694  kgenhaus  22695  kgencmp2  22697  kgenidm  22698  1stckgen  22705  kgencn3  22709  kgen2cn  22710  dfac14  22769  ptcnplem  22772  ptcnp  22773  txcnmpt  22775  ptcn  22778  txdis1cn  22786  lmcn2  22800  txkgen  22803  xkohaus  22804  xkopt  22806  cnmpt11  22814  cnmpt11f  22815  cnmpt1t  22816  cnmpt12  22818  cnmpt21  22822  cnmpt21f  22823  cnmpt2t  22824  cnmpt22  22825  cnmpt22f  22826  cnmptcom  22829  cnmptkp  22831  cnmpt2k  22839  txconn  22840  qtopss  22866  qtopeu  22867  qtopomap  22869  qtopcmap  22870  kqtop  22896  kqt0  22897  nrmr0reg  22900  regr1  22901  kqreg  22902  kqnrm  22903  hmeoqtop  22926  hmphref  22932  xpstopnlem1  22960  ptcmpfi  22964  xkocnv  22965  xkohmeo  22966  kqhmph  22970  flimsncls  23137  cnpflfi  23150  flfcnp  23155  flfcnp2  23158  cnpfcfi  23191  cnextucn  23455  cnmpopc  24091  htpyco1  24141  htpyco2  24142  phtpyco2  24153  pcopt  24185  pcopt2  24186  pcorevlem  24189  pi1cof  24222  pi1coghm  24224  clduni  46194