Theorem toptopon2 22901

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

Syntax hints:   ↔ wb 207   ∈ wcel 2119  ∪ cuni 4838  ‘cfv 6485  Topctop 22876  TopOnctopon 22893

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1802  ax-4 1816  ax-5 1917  ax-6 1974  ax-7 2015  ax-8 2121  ax-9 2129  ax-10 2152  ax-11 2168  ax-12 2189  ax-ext 2711  ax-sep 5218  ax-nul 5228  ax-pow 5294  ax-pr 5362  ax-un 7678

This theorem depends on definitions:  df-bi 208  df-an 397  df-or 854  df-3an 1094  df-tru 1550  df-fal 1560  df-ex 1787  df-nf 1791  df-sb 2074  df-mo 2543  df-eu 2573  df-clab 2718  df-cleq 2731  df-clel 2814  df-nfc 2888  df-ne 2935  df-ral 3054  df-rex 3064  df-rab 3392  df-v 3433  df-dif 3886  df-un 3888  df-in 3890  df-ss 3900  df-nul 4262  df-if 4455  df-pw 4531  df-sn 4556  df-pr 4558  df-op 4562  df-uni 4839  df-br 5073  df-opab 5135  df-mpt 5154  df-id 5513  df-xp 5624  df-rel 5625  df-cnv 5626  df-co 5627  df-dm 5628  df-iota 6441  df-fun 6487  df-fv 6493  df-topon 22894

This theorem is referenced by:  topontopon  22902  toprntopon  22908  neiptopreu  23116  lmcvg  23245  cnss1  23259  cnss2  23260  cnrest2  23269  cnrest2r  23270  lmss  23281  lmcnp  23287  lmcn  23288  t1t0  23331  haust1  23335  restcnrm  23345  resthauslem  23346  lmmo  23363  rncmp  23379  connima  23408  conncn  23409  kgeni  23520  kgenftop  23523  kgenss  23526  kgenhaus  23527  kgencmp2  23529  kgenidm  23530  1stckgen  23537  kgencn3  23541  kgen2cn  23542  dfac14  23601  ptcnplem  23604  ptcnp  23605  txcnmpt  23607  ptcn  23610  txdis1cn  23618  lmcn2  23632  txkgen  23635  xkohaus  23636  xkopt  23638  cnmpt11  23646  cnmpt11f  23647  cnmpt1t  23648  cnmpt12  23650  cnmpt21  23654  cnmpt21f  23655  cnmpt2t  23656  cnmpt22  23657  cnmpt22f  23658  cnmptcom  23661  cnmptkp  23663  cnmpt2k  23671  txconn  23672  qtopss  23698  qtopeu  23699  qtopomap  23701  qtopcmap  23702  kqtop  23728  kqt0  23729  nrmr0reg  23732  regr1  23733  kqreg  23734  kqnrm  23735  hmeoqtop  23758  hmphref  23764  xpstopnlem1  23792  ptcmpfi  23796  xkocnv  23797  xkohmeo  23798  kqhmph  23802  flimsncls  23969  cnpflfi  23982  flfcnp  23987  flfcnp2  23990  cnpfcfi  24023  cnextucn  24285  cnmpopc  24913  htpyco1  24963  htpyco2  24964  phtpyco2  24975  pcopt  25007  pcopt2  25008  pcorevlem  25011  pi1cof  25044  pi1coghm  25046  cvxsconn  35471  clduni  49391