Theorem toptopon2 22978

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

Syntax hints:   ↔ wb 208   ∈ wcel 2142  ∪ cuni 4865  ‘cfv 6521  Topctop 22953  TopOnctopon 22970

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1815  ax-4 1829  ax-5 1930  ax-6 1987  ax-7 2028  ax-8 2144  ax-9 2152  ax-10 2175  ax-11 2191  ax-12 2212  ax-ext 2734  ax-sep 5246  ax-nul 5256  ax-pow 5322  ax-pr 5390  ax-un 7718

This theorem depends on definitions:  df-bi 209  df-an 400  df-or 859  df-3an 1100  df-tru 1563  df-fal 1573  df-ex 1800  df-nf 1804  df-sb 2091  df-mo 2566  df-eu 2596  df-clab 2741  df-cleq 2754  df-clel 2837  df-nfc 2911  df-ne 2958  df-ral 3077  df-rex 3087  df-rab 3415  df-v 3456  df-dif 3907  df-un 3909  df-in 3911  df-ss 3921  df-nul 4286  df-if 4481  df-pw 4557  df-sn 4583  df-pr 4585  df-op 4589  df-uni 4866  df-br 5101  df-opab 5163  df-mpt 5182  df-id 5542  df-xp 5653  df-rel 5654  df-cnv 5655  df-co 5656  df-dm 5657  df-iota 6477  df-fun 6523  df-fv 6529  df-topon 22971

This theorem is referenced by:  topontopon  22979  toprntopon  22985  neiptopreu  23193  lmcvg  23322  cnss1  23336  cnss2  23337  cnrest2  23346  cnrest2r  23347  lmss  23358  lmcnp  23364  lmcn  23365  t1t0  23408  haust1  23412  restcnrm  23422  resthauslem  23423  lmmo  23440  rncmp  23456  connima  23485  conncn  23486  kgeni  23597  kgenftop  23600  kgenss  23603  kgenhaus  23604  kgencmp2  23606  kgenidm  23607  1stckgen  23614  kgencn3  23618  kgen2cn  23619  dfac14  23678  ptcnplem  23681  ptcnp  23682  txcnmpt  23684  ptcn  23687  txdis1cn  23695  lmcn2  23709  txkgen  23712  xkohaus  23713  xkopt  23715  cnmpt11  23723  cnmpt11f  23724  cnmpt1t  23725  cnmpt12  23727  cnmpt21  23731  cnmpt21f  23732  cnmpt2t  23733  cnmpt22  23734  cnmpt22f  23735  cnmptcom  23738  cnmptkp  23740  cnmpt2k  23748  txconn  23749  qtopss  23775  qtopeu  23776  qtopomap  23778  qtopcmap  23779  kqtop  23805  kqt0  23806  nrmr0reg  23809  regr1  23810  kqreg  23811  kqnrm  23812  hmeoqtop  23835  hmphref  23841  xpstopnlem1  23869  ptcmpfi  23873  xkocnv  23874  xkohmeo  23875  kqhmph  23879  flimsncls  24046  cnpflfi  24059  flfcnp  24064  flfcnp2  24067  cnpfcfi  24100  cnextucn  24362  cnmpopc  24990  htpyco1  25040  htpyco2  25041  phtpyco2  25052  pcopt  25084  pcopt2  25085  pcorevlem  25088  pi1cof  25121  pi1coghm  25123  cvxsconn  35593  clduni  49522