Theorem toptopon2 22812

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

Syntax hints:   ↔ wb 206   ∈ wcel 2109  ∪ cuni 4874  ‘cfv 6514  Topctop 22787  TopOnctopon 22804

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 2702  ax-sep 5254  ax-nul 5264  ax-pow 5323  ax-pr 5390  ax-un 7714

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 2534  df-eu 2563  df-clab 2709  df-cleq 2722  df-clel 2804  df-nfc 2879  df-ral 3046  df-rex 3055  df-rab 3409  df-v 3452  df-dif 3920  df-un 3922  df-in 3924  df-ss 3934  df-nul 4300  df-if 4492  df-pw 4568  df-sn 4593  df-pr 4595  df-op 4599  df-uni 4875  df-br 5111  df-opab 5173  df-mpt 5192  df-id 5536  df-xp 5647  df-rel 5648  df-cnv 5649  df-co 5650  df-dm 5651  df-iota 6467  df-fun 6516  df-fv 6522  df-topon 22805

This theorem is referenced by:  topontopon  22813  toprntopon  22819  neiptopreu  23027  lmcvg  23156  cnss1  23170  cnss2  23171  cnrest2  23180  cnrest2r  23181  lmss  23192  lmcnp  23198  lmcn  23199  t1t0  23242  haust1  23246  restcnrm  23256  resthauslem  23257  lmmo  23274  rncmp  23290  connima  23319  conncn  23320  kgeni  23431  kgenftop  23434  kgenss  23437  kgenhaus  23438  kgencmp2  23440  kgenidm  23441  1stckgen  23448  kgencn3  23452  kgen2cn  23453  dfac14  23512  ptcnplem  23515  ptcnp  23516  txcnmpt  23518  ptcn  23521  txdis1cn  23529  lmcn2  23543  txkgen  23546  xkohaus  23547  xkopt  23549  cnmpt11  23557  cnmpt11f  23558  cnmpt1t  23559  cnmpt12  23561  cnmpt21  23565  cnmpt21f  23566  cnmpt2t  23567  cnmpt22  23568  cnmpt22f  23569  cnmptcom  23572  cnmptkp  23574  cnmpt2k  23582  txconn  23583  qtopss  23609  qtopeu  23610  qtopomap  23612  qtopcmap  23613  kqtop  23639  kqt0  23640  nrmr0reg  23643  regr1  23644  kqreg  23645  kqnrm  23646  hmeoqtop  23669  hmphref  23675  xpstopnlem1  23703  ptcmpfi  23707  xkocnv  23708  xkohmeo  23709  kqhmph  23713  flimsncls  23880  cnpflfi  23893  flfcnp  23898  flfcnp2  23901  cnpfcfi  23934  cnextucn  24197  cnmpopc  24829  htpyco1  24884  htpyco2  24885  phtpyco2  24896  pcopt  24929  pcopt2  24930  pcorevlem  24933  pi1cof  24966  pi1coghm  24968  cvxsconn  35237  clduni  48893