Theorem toptopon2 22860

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

Syntax hints:   ↔ wb 206   ∈ wcel 2113  ∪ cuni 4861  ‘cfv 6490  Topctop 22835  TopOnctopon 22852

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 1911  ax-6 1968  ax-7 2009  ax-8 2115  ax-9 2123  ax-10 2146  ax-11 2162  ax-12 2182  ax-ext 2706  ax-sep 5239  ax-nul 5249  ax-pow 5308  ax-pr 5375  ax-un 7678

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 848  df-3an 1088  df-tru 1544  df-fal 1554  df-ex 1781  df-nf 1785  df-sb 2068  df-mo 2537  df-eu 2567  df-clab 2713  df-cleq 2726  df-clel 2809  df-nfc 2883  df-ne 2931  df-ral 3050  df-rex 3059  df-rab 3398  df-v 3440  df-dif 3902  df-un 3904  df-in 3906  df-ss 3916  df-nul 4284  df-if 4478  df-pw 4554  df-sn 4579  df-pr 4581  df-op 4585  df-uni 4862  df-br 5097  df-opab 5159  df-mpt 5178  df-id 5517  df-xp 5628  df-rel 5629  df-cnv 5630  df-co 5631  df-dm 5632  df-iota 6446  df-fun 6492  df-fv 6498  df-topon 22853

This theorem is referenced by:  topontopon  22861  toprntopon  22867  neiptopreu  23075  lmcvg  23204  cnss1  23218  cnss2  23219  cnrest2  23228  cnrest2r  23229  lmss  23240  lmcnp  23246  lmcn  23247  t1t0  23290  haust1  23294  restcnrm  23304  resthauslem  23305  lmmo  23322  rncmp  23338  connima  23367  conncn  23368  kgeni  23479  kgenftop  23482  kgenss  23485  kgenhaus  23486  kgencmp2  23488  kgenidm  23489  1stckgen  23496  kgencn3  23500  kgen2cn  23501  dfac14  23560  ptcnplem  23563  ptcnp  23564  txcnmpt  23566  ptcn  23569  txdis1cn  23577  lmcn2  23591  txkgen  23594  xkohaus  23595  xkopt  23597  cnmpt11  23605  cnmpt11f  23606  cnmpt1t  23607  cnmpt12  23609  cnmpt21  23613  cnmpt21f  23614  cnmpt2t  23615  cnmpt22  23616  cnmpt22f  23617  cnmptcom  23620  cnmptkp  23622  cnmpt2k  23630  txconn  23631  qtopss  23657  qtopeu  23658  qtopomap  23660  qtopcmap  23661  kqtop  23687  kqt0  23688  nrmr0reg  23691  regr1  23692  kqreg  23693  kqnrm  23694  hmeoqtop  23717  hmphref  23723  xpstopnlem1  23751  ptcmpfi  23755  xkocnv  23756  xkohmeo  23757  kqhmph  23761  flimsncls  23928  cnpflfi  23941  flfcnp  23946  flfcnp2  23949  cnpfcfi  23982  cnextucn  24244  cnmpopc  24876  htpyco1  24931  htpyco2  24932  phtpyco2  24943  pcopt  24976  pcopt2  24977  pcorevlem  24980  pi1cof  25013  pi1coghm  25015  cvxsconn  35386  clduni  49088