Theorem toptopon2 22896

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

Syntax hints:   ↔ wb 206   ∈ wcel 2114  ∪ cuni 4851  ‘cfv 6493  Topctop 22871  TopOnctopon 22888

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 1969  ax-7 2010  ax-8 2116  ax-9 2124  ax-10 2147  ax-11 2163  ax-12 2185  ax-ext 2709  ax-sep 5232  ax-nul 5242  ax-pow 5303  ax-pr 5371  ax-un 7683

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 849  df-3an 1089  df-tru 1545  df-fal 1555  df-ex 1782  df-nf 1786  df-sb 2069  df-mo 2540  df-eu 2570  df-clab 2716  df-cleq 2729  df-clel 2812  df-nfc 2886  df-ne 2934  df-ral 3053  df-rex 3063  df-rab 3391  df-v 3432  df-dif 3893  df-un 3895  df-in 3897  df-ss 3907  df-nul 4275  df-if 4468  df-pw 4544  df-sn 4569  df-pr 4571  df-op 4575  df-uni 4852  df-br 5087  df-opab 5149  df-mpt 5168  df-id 5520  df-xp 5631  df-rel 5632  df-cnv 5633  df-co 5634  df-dm 5635  df-iota 6449  df-fun 6495  df-fv 6501  df-topon 22889

This theorem is referenced by:  topontopon  22897  toprntopon  22903  neiptopreu  23111  lmcvg  23240  cnss1  23254  cnss2  23255  cnrest2  23264  cnrest2r  23265  lmss  23276  lmcnp  23282  lmcn  23283  t1t0  23326  haust1  23330  restcnrm  23340  resthauslem  23341  lmmo  23358  rncmp  23374  connima  23403  conncn  23404  kgeni  23515  kgenftop  23518  kgenss  23521  kgenhaus  23522  kgencmp2  23524  kgenidm  23525  1stckgen  23532  kgencn3  23536  kgen2cn  23537  dfac14  23596  ptcnplem  23599  ptcnp  23600  txcnmpt  23602  ptcn  23605  txdis1cn  23613  lmcn2  23627  txkgen  23630  xkohaus  23631  xkopt  23633  cnmpt11  23641  cnmpt11f  23642  cnmpt1t  23643  cnmpt12  23645  cnmpt21  23649  cnmpt21f  23650  cnmpt2t  23651  cnmpt22  23652  cnmpt22f  23653  cnmptcom  23656  cnmptkp  23658  cnmpt2k  23666  txconn  23667  qtopss  23693  qtopeu  23694  qtopomap  23696  qtopcmap  23697  kqtop  23723  kqt0  23724  nrmr0reg  23727  regr1  23728  kqreg  23729  kqnrm  23730  hmeoqtop  23753  hmphref  23759  xpstopnlem1  23787  ptcmpfi  23791  xkocnv  23792  xkohmeo  23793  kqhmph  23797  flimsncls  23964  cnpflfi  23977  flfcnp  23982  flfcnp2  23985  cnpfcfi  24018  cnextucn  24280  cnmpopc  24908  htpyco1  24958  htpyco2  24959  phtpyco2  24970  pcopt  25002  pcopt2  25003  pcorevlem  25006  pi1cof  25039  pi1coghm  25041  cvxsconn  35444  clduni  49391