Theorem toptopon2 22805

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

Syntax hints:   ↔ wb 206   ∈ wcel 2109  ∪ cuni 4871  ‘cfv 6511  Topctop 22780  TopOnctopon 22797

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 5251  ax-nul 5261  ax-pow 5320  ax-pr 5387  ax-un 7711

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 3406  df-v 3449  df-dif 3917  df-un 3919  df-in 3921  df-ss 3931  df-nul 4297  df-if 4489  df-pw 4565  df-sn 4590  df-pr 4592  df-op 4596  df-uni 4872  df-br 5108  df-opab 5170  df-mpt 5189  df-id 5533  df-xp 5644  df-rel 5645  df-cnv 5646  df-co 5647  df-dm 5648  df-iota 6464  df-fun 6513  df-fv 6519  df-topon 22798

This theorem is referenced by:  topontopon  22806  toprntopon  22812  neiptopreu  23020  lmcvg  23149  cnss1  23163  cnss2  23164  cnrest2  23173  cnrest2r  23174  lmss  23185  lmcnp  23191  lmcn  23192  t1t0  23235  haust1  23239  restcnrm  23249  resthauslem  23250  lmmo  23267  rncmp  23283  connima  23312  conncn  23313  kgeni  23424  kgenftop  23427  kgenss  23430  kgenhaus  23431  kgencmp2  23433  kgenidm  23434  1stckgen  23441  kgencn3  23445  kgen2cn  23446  dfac14  23505  ptcnplem  23508  ptcnp  23509  txcnmpt  23511  ptcn  23514  txdis1cn  23522  lmcn2  23536  txkgen  23539  xkohaus  23540  xkopt  23542  cnmpt11  23550  cnmpt11f  23551  cnmpt1t  23552  cnmpt12  23554  cnmpt21  23558  cnmpt21f  23559  cnmpt2t  23560  cnmpt22  23561  cnmpt22f  23562  cnmptcom  23565  cnmptkp  23567  cnmpt2k  23575  txconn  23576  qtopss  23602  qtopeu  23603  qtopomap  23605  qtopcmap  23606  kqtop  23632  kqt0  23633  nrmr0reg  23636  regr1  23637  kqreg  23638  kqnrm  23639  hmeoqtop  23662  hmphref  23668  xpstopnlem1  23696  ptcmpfi  23700  xkocnv  23701  xkohmeo  23702  kqhmph  23706  flimsncls  23873  cnpflfi  23886  flfcnp  23891  flfcnp2  23894  cnpfcfi  23927  cnextucn  24190  cnmpopc  24822  htpyco1  24877  htpyco2  24878  phtpyco2  24889  pcopt  24922  pcopt2  24923  pcorevlem  24926  pi1cof  24959  pi1coghm  24961  cvxsconn  35230  clduni  48889