Theorem toptopon2 23044

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

Syntax hints:   ↔ wb 209   ∈ wcel 2149  ∪ cuni 4876  ‘cfv 6537  Topctop 23019  TopOnctopon 23036

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1822  ax-4 1836  ax-5 1937  ax-6 1994  ax-7 2035  ax-8 2151  ax-9 2159  ax-10 2182  ax-11 2198  ax-12 2219  ax-ext 2741  ax-sep 5261  ax-nul 5271  ax-pow 5337  ax-pr 5405  ax-un 7733

This theorem depends on definitions:  df-bi 210  df-an 401  df-or 861  df-3an 1103  df-tru 1570  df-fal 1580  df-ex 1807  df-nf 1811  df-sb 2098  df-mo 2573  df-eu 2603  df-clab 2748  df-cleq 2761  df-clel 2844  df-nfc 2918  df-ne 2965  df-ral 3086  df-rex 3096  df-rab 3424  df-v 3465  df-dif 3916  df-un 3918  df-in 3920  df-ss 3930  df-nul 4295  df-if 4493  df-pw 4569  df-sn 4595  df-pr 4597  df-op 4601  df-uni 4877  df-br 5114  df-opab 5178  df-mpt 5197  df-id 5557  df-xp 5668  df-rel 5669  df-cnv 5670  df-co 5671  df-dm 5672  df-iota 6493  df-fun 6539  df-fv 6545  df-topon 23037

This theorem is referenced by:  topontopon  23045  toprntopon  23051  neiptopreu  23259  lmcvg  23388  cnss1  23402  cnss2  23403  cnrest2  23412  cnrest2r  23413  lmss  23424  lmcnp  23430  lmcn  23431  t1t0  23474  haust1  23478  restcnrm  23488  resthauslem  23489  lmmo  23506  rncmp  23522  connima  23551  conncn  23552  kgeni  23663  kgenftop  23666  kgenss  23669  kgenhaus  23670  kgencmp2  23672  kgenidm  23673  1stckgen  23680  kgencn3  23684  kgen2cn  23685  dfac14  23744  ptcnplem  23747  ptcnp  23748  txcnmpt  23750  ptcn  23753  txdis1cn  23761  lmcn2  23775  txkgen  23778  xkohaus  23779  xkopt  23781  cnmpt11  23789  cnmpt11f  23790  cnmpt1t  23791  cnmpt12  23793  cnmpt21  23797  cnmpt21f  23798  cnmpt2t  23799  cnmpt22  23800  cnmpt22f  23801  cnmptcom  23804  cnmptkp  23806  cnmpt2k  23814  txconn  23815  qtopss  23841  qtopeu  23842  qtopomap  23844  qtopcmap  23845  kqtop  23871  kqt0  23872  nrmr0reg  23875  regr1  23876  kqreg  23877  kqnrm  23878  hmeoqtop  23901  hmphref  23907  xpstopnlem1  23935  ptcmpfi  23939  xkocnv  23940  xkohmeo  23941  kqhmph  23945  flimsncls  24112  cnpflfi  24125  flfcnp  24130  flfcnp2  24133  cnpfcfi  24166  cnextucn  24428  cnmpopc  25056  htpyco1  25106  htpyco2  25107  phtpyco2  25118  pcopt  25150  pcopt2  25151  pcorevlem  25154  pi1cof  25187  pi1coghm  25189  cvxsconn  35634  clduni  49564