Theorem toptopon2 22874

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

Syntax hints:   ↔ wb 206   ∈ wcel 2114  ∪ cuni 4865  ‘cfv 6500  Topctop 22849  TopOnctopon 22866

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 5243  ax-nul 5253  ax-pow 5312  ax-pr 5379  ax-un 7690

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 3402  df-v 3444  df-dif 3906  df-un 3908  df-in 3910  df-ss 3920  df-nul 4288  df-if 4482  df-pw 4558  df-sn 4583  df-pr 4585  df-op 4589  df-uni 4866  df-br 5101  df-opab 5163  df-mpt 5182  df-id 5527  df-xp 5638  df-rel 5639  df-cnv 5640  df-co 5641  df-dm 5642  df-iota 6456  df-fun 6502  df-fv 6508  df-topon 22867

This theorem is referenced by:  topontopon  22875  toprntopon  22881  neiptopreu  23089  lmcvg  23218  cnss1  23232  cnss2  23233  cnrest2  23242  cnrest2r  23243  lmss  23254  lmcnp  23260  lmcn  23261  t1t0  23304  haust1  23308  restcnrm  23318  resthauslem  23319  lmmo  23336  rncmp  23352  connima  23381  conncn  23382  kgeni  23493  kgenftop  23496  kgenss  23499  kgenhaus  23500  kgencmp2  23502  kgenidm  23503  1stckgen  23510  kgencn3  23514  kgen2cn  23515  dfac14  23574  ptcnplem  23577  ptcnp  23578  txcnmpt  23580  ptcn  23583  txdis1cn  23591  lmcn2  23605  txkgen  23608  xkohaus  23609  xkopt  23611  cnmpt11  23619  cnmpt11f  23620  cnmpt1t  23621  cnmpt12  23623  cnmpt21  23627  cnmpt21f  23628  cnmpt2t  23629  cnmpt22  23630  cnmpt22f  23631  cnmptcom  23634  cnmptkp  23636  cnmpt2k  23644  txconn  23645  qtopss  23671  qtopeu  23672  qtopomap  23674  qtopcmap  23675  kqtop  23701  kqt0  23702  nrmr0reg  23705  regr1  23706  kqreg  23707  kqnrm  23708  hmeoqtop  23731  hmphref  23737  xpstopnlem1  23765  ptcmpfi  23769  xkocnv  23770  xkohmeo  23771  kqhmph  23775  flimsncls  23942  cnpflfi  23955  flfcnp  23960  flfcnp2  23963  cnpfcfi  23996  cnextucn  24258  cnmpopc  24890  htpyco1  24945  htpyco2  24946  phtpyco2  24957  pcopt  24990  pcopt2  24991  pcorevlem  24994  pi1cof  25027  pi1coghm  25029  cvxsconn  35459  clduni  49260