Theorem toptopon2 22838

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

Syntax hints:   ↔ wb 206   ∈ wcel 2109  ∪ cuni 4867  ‘cfv 6499  Topctop 22813  TopOnctopon 22830

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 5246  ax-nul 5256  ax-pow 5315  ax-pr 5382  ax-un 7691

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 3403  df-v 3446  df-dif 3914  df-un 3916  df-in 3918  df-ss 3928  df-nul 4293  df-if 4485  df-pw 4561  df-sn 4586  df-pr 4588  df-op 4592  df-uni 4868  df-br 5103  df-opab 5165  df-mpt 5184  df-id 5526  df-xp 5637  df-rel 5638  df-cnv 5639  df-co 5640  df-dm 5641  df-iota 6452  df-fun 6501  df-fv 6507  df-topon 22831

This theorem is referenced by:  topontopon  22839  toprntopon  22845  neiptopreu  23053  lmcvg  23182  cnss1  23196  cnss2  23197  cnrest2  23206  cnrest2r  23207  lmss  23218  lmcnp  23224  lmcn  23225  t1t0  23268  haust1  23272  restcnrm  23282  resthauslem  23283  lmmo  23300  rncmp  23316  connima  23345  conncn  23346  kgeni  23457  kgenftop  23460  kgenss  23463  kgenhaus  23464  kgencmp2  23466  kgenidm  23467  1stckgen  23474  kgencn3  23478  kgen2cn  23479  dfac14  23538  ptcnplem  23541  ptcnp  23542  txcnmpt  23544  ptcn  23547  txdis1cn  23555  lmcn2  23569  txkgen  23572  xkohaus  23573  xkopt  23575  cnmpt11  23583  cnmpt11f  23584  cnmpt1t  23585  cnmpt12  23587  cnmpt21  23591  cnmpt21f  23592  cnmpt2t  23593  cnmpt22  23594  cnmpt22f  23595  cnmptcom  23598  cnmptkp  23600  cnmpt2k  23608  txconn  23609  qtopss  23635  qtopeu  23636  qtopomap  23638  qtopcmap  23639  kqtop  23665  kqt0  23666  nrmr0reg  23669  regr1  23670  kqreg  23671  kqnrm  23672  hmeoqtop  23695  hmphref  23701  xpstopnlem1  23729  ptcmpfi  23733  xkocnv  23734  xkohmeo  23735  kqhmph  23739  flimsncls  23906  cnpflfi  23919  flfcnp  23924  flfcnp2  23927  cnpfcfi  23960  cnextucn  24223  cnmpopc  24855  htpyco1  24910  htpyco2  24911  phtpyco2  24922  pcopt  24955  pcopt2  24956  pcorevlem  24959  pi1cof  24992  pi1coghm  24994  cvxsconn  35223  clduni  48882