Theorem toptopon2 22861

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

Syntax hints:   ↔ wb 206   ∈ wcel 2114  ∪ cuni 4851  ‘cfv 6490  Topctop 22836  TopOnctopon 22853

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 1912  ax-6 1969  ax-7 2010  ax-8 2116  ax-9 2124  ax-10 2147  ax-11 2163  ax-12 2185  ax-ext 2709  ax-sep 5231  ax-nul 5241  ax-pow 5300  ax-pr 5368  ax-un 7680

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 849  df-3an 1089  df-tru 1545  df-fal 1555  df-ex 1782  df-nf 1786  df-sb 2069  df-mo 2540  df-eu 2570  df-clab 2716  df-cleq 2729  df-clel 2812  df-nfc 2886  df-ne 2934  df-ral 3053  df-rex 3063  df-rab 3391  df-v 3432  df-dif 3893  df-un 3895  df-in 3897  df-ss 3907  df-nul 4275  df-if 4468  df-pw 4544  df-sn 4569  df-pr 4571  df-op 4575  df-uni 4852  df-br 5087  df-opab 5149  df-mpt 5168  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 22854

This theorem is referenced by:  topontopon  22862  toprntopon  22868  neiptopreu  23076  lmcvg  23205  cnss1  23219  cnss2  23220  cnrest2  23229  cnrest2r  23230  lmss  23241  lmcnp  23247  lmcn  23248  t1t0  23291  haust1  23295  restcnrm  23305  resthauslem  23306  lmmo  23323  rncmp  23339  connima  23368  conncn  23369  kgeni  23480  kgenftop  23483  kgenss  23486  kgenhaus  23487  kgencmp2  23489  kgenidm  23490  1stckgen  23497  kgencn3  23501  kgen2cn  23502  dfac14  23561  ptcnplem  23564  ptcnp  23565  txcnmpt  23567  ptcn  23570  txdis1cn  23578  lmcn2  23592  txkgen  23595  xkohaus  23596  xkopt  23598  cnmpt11  23606  cnmpt11f  23607  cnmpt1t  23608  cnmpt12  23610  cnmpt21  23614  cnmpt21f  23615  cnmpt2t  23616  cnmpt22  23617  cnmpt22f  23618  cnmptcom  23621  cnmptkp  23623  cnmpt2k  23631  txconn  23632  qtopss  23658  qtopeu  23659  qtopomap  23661  qtopcmap  23662  kqtop  23688  kqt0  23689  nrmr0reg  23692  regr1  23693  kqreg  23694  kqnrm  23695  hmeoqtop  23718  hmphref  23724  xpstopnlem1  23752  ptcmpfi  23756  xkocnv  23757  xkohmeo  23758  kqhmph  23762  flimsncls  23929  cnpflfi  23942  flfcnp  23947  flfcnp2  23950  cnpfcfi  23983  cnextucn  24245  cnmpopc  24873  htpyco1  24923  htpyco2  24924  phtpyco2  24935  pcopt  24967  pcopt2  24968  pcorevlem  24971  pi1cof  25004  pi1coghm  25006  cvxsconn  35431  clduni  49334