Theorem toptopon2 22803

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

Syntax hints:   ↔ wb 206   ∈ wcel 2109  ∪ cuni 4858  ‘cfv 6482  Topctop 22778  TopOnctopon 22795

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1795  ax-4 1809  ax-5 1910  ax-6 1967  ax-7 2008  ax-8 2111  ax-9 2119  ax-10 2142  ax-11 2158  ax-12 2178  ax-ext 2701  ax-sep 5235  ax-nul 5245  ax-pow 5304  ax-pr 5371  ax-un 7671

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 848  df-3an 1088  df-tru 1543  df-fal 1553  df-ex 1780  df-nf 1784  df-sb 2066  df-mo 2533  df-eu 2562  df-clab 2708  df-cleq 2721  df-clel 2803  df-nfc 2878  df-ral 3045  df-rex 3054  df-rab 3395  df-v 3438  df-dif 3906  df-un 3908  df-in 3910  df-ss 3920  df-nul 4285  df-if 4477  df-pw 4553  df-sn 4578  df-pr 4580  df-op 4584  df-uni 4859  df-br 5093  df-opab 5155  df-mpt 5174  df-id 5514  df-xp 5625  df-rel 5626  df-cnv 5627  df-co 5628  df-dm 5629  df-iota 6438  df-fun 6484  df-fv 6490  df-topon 22796

This theorem is referenced by:  topontopon  22804  toprntopon  22810  neiptopreu  23018  lmcvg  23147  cnss1  23161  cnss2  23162  cnrest2  23171  cnrest2r  23172  lmss  23183  lmcnp  23189  lmcn  23190  t1t0  23233  haust1  23237  restcnrm  23247  resthauslem  23248  lmmo  23265  rncmp  23281  connima  23310  conncn  23311  kgeni  23422  kgenftop  23425  kgenss  23428  kgenhaus  23429  kgencmp2  23431  kgenidm  23432  1stckgen  23439  kgencn3  23443  kgen2cn  23444  dfac14  23503  ptcnplem  23506  ptcnp  23507  txcnmpt  23509  ptcn  23512  txdis1cn  23520  lmcn2  23534  txkgen  23537  xkohaus  23538  xkopt  23540  cnmpt11  23548  cnmpt11f  23549  cnmpt1t  23550  cnmpt12  23552  cnmpt21  23556  cnmpt21f  23557  cnmpt2t  23558  cnmpt22  23559  cnmpt22f  23560  cnmptcom  23563  cnmptkp  23565  cnmpt2k  23573  txconn  23574  qtopss  23600  qtopeu  23601  qtopomap  23603  qtopcmap  23604  kqtop  23630  kqt0  23631  nrmr0reg  23634  regr1  23635  kqreg  23636  kqnrm  23637  hmeoqtop  23660  hmphref  23666  xpstopnlem1  23694  ptcmpfi  23698  xkocnv  23699  xkohmeo  23700  kqhmph  23704  flimsncls  23871  cnpflfi  23884  flfcnp  23889  flfcnp2  23892  cnpfcfi  23925  cnextucn  24188  cnmpopc  24820  htpyco1  24875  htpyco2  24876  phtpyco2  24887  pcopt  24920  pcopt2  24921  pcorevlem  24924  pi1cof  24957  pi1coghm  24959  cvxsconn  35220  clduni  48889