Theorem toptopon2 22924

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 22923	1 ⊢ (𝐽 ∈ Top ↔ 𝐽 ∈ (TopOn‘∪ 𝐽))

Syntax hints:   ↔ wb 206   ∈ wcel 2108  ∪ cuni 4907  ‘cfv 6561  Topctop 22899  TopOnctopon 22916

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1795  ax-4 1809  ax-5 1910  ax-6 1967  ax-7 2007  ax-8 2110  ax-9 2118  ax-10 2141  ax-11 2157  ax-12 2177  ax-ext 2708  ax-sep 5296  ax-nul 5306  ax-pow 5365  ax-pr 5432  ax-un 7755

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 849  df-3an 1089  df-tru 1543  df-fal 1553  df-ex 1780  df-nf 1784  df-sb 2065  df-mo 2540  df-eu 2569  df-clab 2715  df-cleq 2729  df-clel 2816  df-nfc 2892  df-ral 3062  df-rex 3071  df-rab 3437  df-v 3482  df-dif 3954  df-un 3956  df-in 3958  df-ss 3968  df-nul 4334  df-if 4526  df-pw 4602  df-sn 4627  df-pr 4629  df-op 4633  df-uni 4908  df-br 5144  df-opab 5206  df-mpt 5226  df-id 5578  df-xp 5691  df-rel 5692  df-cnv 5693  df-co 5694  df-dm 5695  df-iota 6514  df-fun 6563  df-fv 6569  df-topon 22917

This theorem is referenced by:  topontopon  22925  toprntopon  22931  neiptopreu  23141  lmcvg  23270  cnss1  23284  cnss2  23285  cnrest2  23294  cnrest2r  23295  lmss  23306  lmcnp  23312  lmcn  23313  t1t0  23356  haust1  23360  restcnrm  23370  resthauslem  23371  lmmo  23388  rncmp  23404  connima  23433  conncn  23434  kgeni  23545  kgenftop  23548  kgenss  23551  kgenhaus  23552  kgencmp2  23554  kgenidm  23555  1stckgen  23562  kgencn3  23566  kgen2cn  23567  dfac14  23626  ptcnplem  23629  ptcnp  23630  txcnmpt  23632  ptcn  23635  txdis1cn  23643  lmcn2  23657  txkgen  23660  xkohaus  23661  xkopt  23663  cnmpt11  23671  cnmpt11f  23672  cnmpt1t  23673  cnmpt12  23675  cnmpt21  23679  cnmpt21f  23680  cnmpt2t  23681  cnmpt22  23682  cnmpt22f  23683  cnmptcom  23686  cnmptkp  23688  cnmpt2k  23696  txconn  23697  qtopss  23723  qtopeu  23724  qtopomap  23726  qtopcmap  23727  kqtop  23753  kqt0  23754  nrmr0reg  23757  regr1  23758  kqreg  23759  kqnrm  23760  hmeoqtop  23783  hmphref  23789  xpstopnlem1  23817  ptcmpfi  23821  xkocnv  23822  xkohmeo  23823  kqhmph  23827  flimsncls  23994  cnpflfi  24007  flfcnp  24012  flfcnp2  24015  cnpfcfi  24048  cnextucn  24312  cnmpopc  24955  htpyco1  25010  htpyco2  25011  phtpyco2  25022  pcopt  25055  pcopt2  25056  pcorevlem  25059  pi1cof  25092  pi1coghm  25094  cvxsconn  35248  clduni  48798