Theorem toptopon2 22304

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

Syntax hints:   ↔ wb 205   ∈ wcel 2106  ∪ cuni 4870  ‘cfv 6501  Topctop 22279  TopOnctopon 22296

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 2702  ax-sep 5261  ax-nul 5268  ax-pow 5325  ax-pr 5389  ax-un 7677

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 2533  df-eu 2562  df-clab 2709  df-cleq 2723  df-clel 2809  df-nfc 2884  df-ral 3061  df-rex 3070  df-rab 3406  df-v 3448  df-dif 3916  df-un 3918  df-in 3920  df-ss 3930  df-nul 4288  df-if 4492  df-pw 4567  df-sn 4592  df-pr 4594  df-op 4598  df-uni 4871  df-br 5111  df-opab 5173  df-mpt 5194  df-id 5536  df-xp 5644  df-rel 5645  df-cnv 5646  df-co 5647  df-dm 5648  df-iota 6453  df-fun 6503  df-fv 6509  df-topon 22297

This theorem is referenced by:  topontopon  22305  toprntopon  22311  neiptopreu  22521  lmcvg  22650  cnss1  22664  cnss2  22665  cnrest2  22674  cnrest2r  22675  lmss  22686  lmcnp  22692  lmcn  22693  t1t0  22736  haust1  22740  restcnrm  22750  resthauslem  22751  lmmo  22768  rncmp  22784  connima  22813  conncn  22814  kgeni  22925  kgenftop  22928  kgenss  22931  kgenhaus  22932  kgencmp2  22934  kgenidm  22935  1stckgen  22942  kgencn3  22946  kgen2cn  22947  dfac14  23006  ptcnplem  23009  ptcnp  23010  txcnmpt  23012  ptcn  23015  txdis1cn  23023  lmcn2  23037  txkgen  23040  xkohaus  23041  xkopt  23043  cnmpt11  23051  cnmpt11f  23052  cnmpt1t  23053  cnmpt12  23055  cnmpt21  23059  cnmpt21f  23060  cnmpt2t  23061  cnmpt22  23062  cnmpt22f  23063  cnmptcom  23066  cnmptkp  23068  cnmpt2k  23076  txconn  23077  qtopss  23103  qtopeu  23104  qtopomap  23106  qtopcmap  23107  kqtop  23133  kqt0  23134  nrmr0reg  23137  regr1  23138  kqreg  23139  kqnrm  23140  hmeoqtop  23163  hmphref  23169  xpstopnlem1  23197  ptcmpfi  23201  xkocnv  23202  xkohmeo  23203  kqhmph  23207  flimsncls  23374  cnpflfi  23387  flfcnp  23392  flfcnp2  23395  cnpfcfi  23428  cnextucn  23692  cnmpopc  24328  htpyco1  24378  htpyco2  24379  phtpyco2  24390  pcopt  24422  pcopt2  24423  pcorevlem  24426  pi1cof  24459  pi1coghm  24461  clduni  47053