Theorem toptopon2 21230

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

Syntax hints:   ↔ wb 198   ∈ wcel 2050  ∪ cuni 4712  ‘cfv 6188  Topctop 21205  TopOnctopon 21222

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1758  ax-4 1772  ax-5 1869  ax-6 1928  ax-7 1965  ax-8 2052  ax-9 2059  ax-10 2079  ax-11 2093  ax-12 2106  ax-13 2301  ax-ext 2751  ax-sep 5060  ax-nul 5067  ax-pow 5119  ax-pr 5186  ax-un 7279

This theorem depends on definitions:  df-bi 199  df-an 388  df-or 834  df-3an 1070  df-tru 1510  df-ex 1743  df-nf 1747  df-sb 2016  df-mo 2547  df-eu 2584  df-clab 2760  df-cleq 2772  df-clel 2847  df-nfc 2919  df-ral 3094  df-rex 3095  df-rab 3098  df-v 3418  df-sbc 3683  df-dif 3833  df-un 3835  df-in 3837  df-ss 3844  df-nul 4180  df-if 4351  df-pw 4424  df-sn 4442  df-pr 4444  df-op 4448  df-uni 4713  df-br 4930  df-opab 4992  df-mpt 5009  df-id 5312  df-xp 5413  df-rel 5414  df-cnv 5415  df-co 5416  df-dm 5417  df-iota 6152  df-fun 6190  df-fv 6196  df-topon 21223

This theorem is referenced by:  topontopon  21231  toprntopon  21237  neiptopreu  21445  lmcvg  21574  cnss1  21588  cnss2  21589  cnrest2  21598  cnrest2r  21599  lmss  21610  lmcnp  21616  lmcn  21617  t1t0  21660  haust1  21664  restcnrm  21674  resthauslem  21675  lmmo  21692  rncmp  21708  connima  21737  conncn  21738  kgeni  21849  kgenftop  21852  kgenss  21855  kgenhaus  21856  kgencmp2  21858  kgenidm  21859  1stckgen  21866  kgencn3  21870  kgen2cn  21871  dfac14  21930  ptcnplem  21933  ptcnp  21934  txcnmpt  21936  ptcn  21939  txdis1cn  21947  lmcn2  21961  txkgen  21964  xkohaus  21965  xkopt  21967  cnmpt11  21975  cnmpt11f  21976  cnmpt1t  21977  cnmpt12  21979  cnmpt21  21983  cnmpt21f  21984  cnmpt2t  21985  cnmpt22  21986  cnmpt22f  21987  cnmptcom  21990  cnmptkp  21992  cnmpt2k  22000  txconn  22001  qtopss  22027  qtopeu  22028  qtopomap  22030  qtopcmap  22031  kqtop  22057  kqt0  22058  nrmr0reg  22061  regr1  22062  kqreg  22063  kqnrm  22064  hmeoqtop  22087  hmphref  22093  xpstopnlem1  22121  ptcmpfi  22125  xkocnv  22126  xkohmeo  22127  kqhmph  22131  flimsncls  22298  cnpflfi  22311  flfcnp  22316  flfcnp2  22319  cnpfcfi  22352  cnextucn  22615  cnmpopc  23235  htpyco1  23285  htpyco2  23286  phtpyco2  23297  pcopt  23329  pcopt2  23330  pcorevlem  23333  pi1cof  23366  pi1coghm  23368