Theorem toptopon2 23291

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

This proof depends on syntax axioms:   ↔ wb 209   ∈ wcel 2147  ∪ cuni 4872  ‘cfv 6566  Topctop 23266  TopOnctopon 23283

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1828  ax-4 1842  ax-5 1945  ax-6 2002  ax-7 2043  ax-8 2149  ax-9 2157  ax-10 2180  ax-11 2197  ax-12 2216  ax-ext 2735  ax-sep 5255  ax-nul 5266  ax-pow 5334  ax-pr 5398  ax-un 7783

This proof depends on definitions:  df-bi 210  df-an 402  df-or 862  df-3an 1105  df-tru 1573  df-fal 1583  df-ex 1813  df-nf 1817  df-sb 2102  df-mo 2567  df-eu 2597  df-clab 2742  df-cleq 2755  df-clel 2839  df-nfc 2913  df-ne 2960  df-ral 3081  df-rex 3091  df-rab 3417  df-v 3456  df-ss 3901  df-dif 4050  df-in 4094  df-un 4154  df-nul 4282  df-if 4486  df-pw 4562  df-sn 4589  df-pr 4591  df-op 4841  df-uni 4873  df-br 5109  df-opab 5174  df-mpt 5193  df-id 5553  df-xp 5664  df-rel 5665  df-cnv 5666  df-co 5667  df-dm 5668  df-iota 6520  df-fun 6568  df-fv 6574  df-topon 23284

This theorem is used by:  topontopon  23292  toprntopon  23298  neiptopreu  23506  lmcvg  23635  cnss1  23649  cnss2  23650  cnrest2  23659  cnrest2r  23660  lmss  23671  lmcnp  23677  lmcn  23678  t1t0  23721  haust1  23725  restcnrm  23735  resthauslem  23736  lmmo  23753  rncmp  23769  connima  23798  conncn  23799  kgeni  23911  kgenftop  23914  kgenss  23917  kgenhaus  23918  kgencmp2  23920  kgenidm  23921  1stckgen  23928  kgencn3  23932  kgen2cn  23933  dfac14  23992  ptcnplem  23995  ptcnp  23996  txcnmpt  23998  ptcn  24001  txdis1cn  24009  lmcn2  24023  txkgen  24026  xkohaus  24027  xkopt  24029  cnmpt11  24037  cnmpt11f  24038  cnmpt1t  24039  cnmpt12  24041  cnmpt21  24045  cnmpt21f  24046  cnmpt2t  24047  cnmpt22  24048  cnmpt22f  24049  cnmptcom  24052  cnmptkp  24054  cnmpt2k  24062  txconn  24063  qtopss  24089  qtopeu  24090  qtopomap  24092  qtopcmap  24093  kqtop  24119  kqt0  24120  nrmr0reg  24123  regr1  24124  kqreg  24125  kqnrm  24126  hmeoqtop  24149  hmphref  24155  xpstopnlem1  24183  ptcmpfi  24187  xkocnv  24188  xkohmeo  24189  kqhmph  24193  flimsncls  24360  cnpflfi  24373  flfcnp  24378  flfcnp2  24381  cnpfcfi  24414  cnextucn  24676  cnmpopc  25304  htpyco1  25354  htpyco2  25355  phtpyco2  25366  pcopt  25398  pcopt2  25399  pcorevlem  25402  pi1cof  25435  pi1coghm  25437  cvxsconn  36216  clduni  50346