Theorem toptopon2 22862

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

Syntax hints:   ↔ wb 206   ∈ wcel 2113  ∪ cuni 4863  ‘cfv 6492  Topctop 22837  TopOnctopon 22854

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1796  ax-4 1810  ax-5 1911  ax-6 1968  ax-7 2009  ax-8 2115  ax-9 2123  ax-10 2146  ax-11 2162  ax-12 2184  ax-ext 2708  ax-sep 5241  ax-nul 5251  ax-pow 5310  ax-pr 5377  ax-un 7680

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 848  df-3an 1088  df-tru 1544  df-fal 1554  df-ex 1781  df-nf 1785  df-sb 2068  df-mo 2539  df-eu 2569  df-clab 2715  df-cleq 2728  df-clel 2811  df-nfc 2885  df-ne 2933  df-ral 3052  df-rex 3061  df-rab 3400  df-v 3442  df-dif 3904  df-un 3906  df-in 3908  df-ss 3918  df-nul 4286  df-if 4480  df-pw 4556  df-sn 4581  df-pr 4583  df-op 4587  df-uni 4864  df-br 5099  df-opab 5161  df-mpt 5180  df-id 5519  df-xp 5630  df-rel 5631  df-cnv 5632  df-co 5633  df-dm 5634  df-iota 6448  df-fun 6494  df-fv 6500  df-topon 22855

This theorem is referenced by:  topontopon  22863  toprntopon  22869  neiptopreu  23077  lmcvg  23206  cnss1  23220  cnss2  23221  cnrest2  23230  cnrest2r  23231  lmss  23242  lmcnp  23248  lmcn  23249  t1t0  23292  haust1  23296  restcnrm  23306  resthauslem  23307  lmmo  23324  rncmp  23340  connima  23369  conncn  23370  kgeni  23481  kgenftop  23484  kgenss  23487  kgenhaus  23488  kgencmp2  23490  kgenidm  23491  1stckgen  23498  kgencn3  23502  kgen2cn  23503  dfac14  23562  ptcnplem  23565  ptcnp  23566  txcnmpt  23568  ptcn  23571  txdis1cn  23579  lmcn2  23593  txkgen  23596  xkohaus  23597  xkopt  23599  cnmpt11  23607  cnmpt11f  23608  cnmpt1t  23609  cnmpt12  23611  cnmpt21  23615  cnmpt21f  23616  cnmpt2t  23617  cnmpt22  23618  cnmpt22f  23619  cnmptcom  23622  cnmptkp  23624  cnmpt2k  23632  txconn  23633  qtopss  23659  qtopeu  23660  qtopomap  23662  qtopcmap  23663  kqtop  23689  kqt0  23690  nrmr0reg  23693  regr1  23694  kqreg  23695  kqnrm  23696  hmeoqtop  23719  hmphref  23725  xpstopnlem1  23753  ptcmpfi  23757  xkocnv  23758  xkohmeo  23759  kqhmph  23763  flimsncls  23930  cnpflfi  23943  flfcnp  23948  flfcnp2  23951  cnpfcfi  23984  cnextucn  24246  cnmpopc  24878  htpyco1  24933  htpyco2  24934  phtpyco2  24945  pcopt  24978  pcopt2  24979  pcorevlem  24982  pi1cof  25015  pi1coghm  25017  cvxsconn  35437  clduni  49156