Theorem toptopon2 21975

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 21974	1 ⊢ (𝐽 ∈ Top ↔ 𝐽 ∈ (TopOn‘∪ 𝐽))

Syntax hints:   ↔ wb 205   ∈ wcel 2108  ∪ cuni 4836  ‘cfv 6418  Topctop 21950  TopOnctopon 21967

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1799  ax-4 1813  ax-5 1914  ax-6 1972  ax-7 2012  ax-8 2110  ax-9 2118  ax-10 2139  ax-11 2156  ax-12 2173  ax-ext 2709  ax-sep 5218  ax-nul 5225  ax-pow 5283  ax-pr 5347  ax-un 7566

This theorem depends on definitions:  df-bi 206  df-an 396  df-or 844  df-3an 1087  df-tru 1542  df-fal 1552  df-ex 1784  df-nf 1788  df-sb 2069  df-mo 2540  df-eu 2569  df-clab 2716  df-cleq 2730  df-clel 2817  df-nfc 2888  df-ne 2943  df-ral 3068  df-rex 3069  df-rab 3072  df-v 3424  df-dif 3886  df-un 3888  df-in 3890  df-ss 3900  df-nul 4254  df-if 4457  df-pw 4532  df-sn 4559  df-pr 4561  df-op 4565  df-uni 4837  df-br 5071  df-opab 5133  df-mpt 5154  df-id 5480  df-xp 5586  df-rel 5587  df-cnv 5588  df-co 5589  df-dm 5590  df-iota 6376  df-fun 6420  df-fv 6426  df-topon 21968

This theorem is referenced by:  topontopon  21976  toprntopon  21982  neiptopreu  22192  lmcvg  22321  cnss1  22335  cnss2  22336  cnrest2  22345  cnrest2r  22346  lmss  22357  lmcnp  22363  lmcn  22364  t1t0  22407  haust1  22411  restcnrm  22421  resthauslem  22422  lmmo  22439  rncmp  22455  connima  22484  conncn  22485  kgeni  22596  kgenftop  22599  kgenss  22602  kgenhaus  22603  kgencmp2  22605  kgenidm  22606  1stckgen  22613  kgencn3  22617  kgen2cn  22618  dfac14  22677  ptcnplem  22680  ptcnp  22681  txcnmpt  22683  ptcn  22686  txdis1cn  22694  lmcn2  22708  txkgen  22711  xkohaus  22712  xkopt  22714  cnmpt11  22722  cnmpt11f  22723  cnmpt1t  22724  cnmpt12  22726  cnmpt21  22730  cnmpt21f  22731  cnmpt2t  22732  cnmpt22  22733  cnmpt22f  22734  cnmptcom  22737  cnmptkp  22739  cnmpt2k  22747  txconn  22748  qtopss  22774  qtopeu  22775  qtopomap  22777  qtopcmap  22778  kqtop  22804  kqt0  22805  nrmr0reg  22808  regr1  22809  kqreg  22810  kqnrm  22811  hmeoqtop  22834  hmphref  22840  xpstopnlem1  22868  ptcmpfi  22872  xkocnv  22873  xkohmeo  22874  kqhmph  22878  flimsncls  23045  cnpflfi  23058  flfcnp  23063  flfcnp2  23066  cnpfcfi  23099  cnextucn  23363  cnmpopc  23997  htpyco1  24047  htpyco2  24048  phtpyco2  24059  pcopt  24091  pcopt2  24092  pcorevlem  24095  pi1cof  24128  pi1coghm  24130  clduni  46082