Metamath Proof Explorer < Previous   Next > Nearby theorems Mirrors  >  Home  >  MPE Home  >  Th. List  >  toptopon2 Structured version   Visualization version   GIF version

Theorem toptopon2 21529
 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
StepHypRef Expression
1 eqid 2824 . 2 𝐽 = 𝐽
21toptopon 21528 1 (𝐽 ∈ Top ↔ 𝐽 ∈ (TopOn‘ 𝐽))
 Colors of variables: wff setvar class Syntax hints:   ↔ wb 209   ∈ wcel 2115  ∪ cuni 4824  ‘cfv 6343  Topctop 21504  TopOnctopon 21521 This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1797  ax-4 1811  ax-5 1912  ax-6 1971  ax-7 2016  ax-8 2117  ax-9 2125  ax-10 2146  ax-11 2162  ax-12 2179  ax-ext 2796  ax-sep 5189  ax-nul 5196  ax-pow 5253  ax-pr 5317  ax-un 7455 This theorem depends on definitions:  df-bi 210  df-an 400  df-or 845  df-3an 1086  df-tru 1541  df-ex 1782  df-nf 1786  df-sb 2071  df-mo 2624  df-eu 2655  df-clab 2803  df-cleq 2817  df-clel 2896  df-nfc 2964  df-ral 3138  df-rex 3139  df-rab 3142  df-v 3482  df-sbc 3759  df-dif 3922  df-un 3924  df-in 3926  df-ss 3936  df-nul 4277  df-if 4451  df-pw 4524  df-sn 4551  df-pr 4553  df-op 4557  df-uni 4825  df-br 5053  df-opab 5115  df-mpt 5133  df-id 5447  df-xp 5548  df-rel 5549  df-cnv 5550  df-co 5551  df-dm 5552  df-iota 6302  df-fun 6345  df-fv 6351  df-topon 21522 This theorem is referenced by:  topontopon  21530  toprntopon  21536  neiptopreu  21744  lmcvg  21873  cnss1  21887  cnss2  21888  cnrest2  21897  cnrest2r  21898  lmss  21909  lmcnp  21915  lmcn  21916  t1t0  21959  haust1  21963  restcnrm  21973  resthauslem  21974  lmmo  21991  rncmp  22007  connima  22036  conncn  22037  kgeni  22148  kgenftop  22151  kgenss  22154  kgenhaus  22155  kgencmp2  22157  kgenidm  22158  1stckgen  22165  kgencn3  22169  kgen2cn  22170  dfac14  22229  ptcnplem  22232  ptcnp  22233  txcnmpt  22235  ptcn  22238  txdis1cn  22246  lmcn2  22260  txkgen  22263  xkohaus  22264  xkopt  22266  cnmpt11  22274  cnmpt11f  22275  cnmpt1t  22276  cnmpt12  22278  cnmpt21  22282  cnmpt21f  22283  cnmpt2t  22284  cnmpt22  22285  cnmpt22f  22286  cnmptcom  22289  cnmptkp  22291  cnmpt2k  22299  txconn  22300  qtopss  22326  qtopeu  22327  qtopomap  22329  qtopcmap  22330  kqtop  22356  kqt0  22357  nrmr0reg  22360  regr1  22361  kqreg  22362  kqnrm  22363  hmeoqtop  22386  hmphref  22392  xpstopnlem1  22420  ptcmpfi  22424  xkocnv  22425  xkohmeo  22426  kqhmph  22430  flimsncls  22597  cnpflfi  22610  flfcnp  22615  flfcnp2  22618  cnpfcfi  22651  cnextucn  22915  cnmpopc  23539  htpyco1  23589  htpyco2  23590  phtpyco2  23601  pcopt  23633  pcopt2  23634  pcorevlem  23637  pi1cof  23670  pi1coghm  23672
 Copyright terms: Public domain W3C validator