Theorem toptopon2 23127

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

This proof depends on syntax axioms:   ↔ wb 209   ∈ wcel 2146  ∪ cuni 4874  ‘cfv 6540  Topctop 23102  TopOnctopon 23119

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 1943  ax-6 2000  ax-7 2041  ax-8 2148  ax-9 2156  ax-10 2179  ax-11 2195  ax-12 2216  ax-ext 2737  ax-sep 5259  ax-nul 5271  ax-pow 5338  ax-pr 5406  ax-un 7742

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 2100  df-mo 2569  df-eu 2599  df-clab 2744  df-cleq 2757  df-clel 2840  df-nfc 2914  df-ne 2961  df-ral 3082  df-rex 3092  df-rab 3419  df-v 3459  df-dif 3909  df-un 3911  df-in 3913  df-ss 3923  df-nul 4287  df-if 4490  df-pw 4566  df-sn 4592  df-pr 4594  df-op 4598  df-uni 4875  df-br 5112  df-opab 5176  df-mpt 5195  df-id 5558  df-xp 5669  df-rel 5670  df-cnv 5671  df-co 5672  df-dm 5673  df-iota 6496  df-fun 6542  df-fv 6548  df-topon 23120

This theorem is used by:  topontopon  23128  toprntopon  23134  neiptopreu  23342  lmcvg  23471  cnss1  23485  cnss2  23486  cnrest2  23495  cnrest2r  23496  lmss  23507  lmcnp  23513  lmcn  23514  t1t0  23557  haust1  23561  restcnrm  23571  resthauslem  23572  lmmo  23589  rncmp  23605  connima  23634  conncn  23635  kgeni  23747  kgenftop  23750  kgenss  23753  kgenhaus  23754  kgencmp2  23756  kgenidm  23757  1stckgen  23764  kgencn3  23768  kgen2cn  23769  dfac14  23828  ptcnplem  23831  ptcnp  23832  txcnmpt  23834  ptcn  23837  txdis1cn  23845  lmcn2  23859  txkgen  23862  xkohaus  23863  xkopt  23865  cnmpt11  23873  cnmpt11f  23874  cnmpt1t  23875  cnmpt12  23877  cnmpt21  23881  cnmpt21f  23882  cnmpt2t  23883  cnmpt22  23884  cnmpt22f  23885  cnmptcom  23888  cnmptkp  23890  cnmpt2k  23898  txconn  23899  qtopss  23925  qtopeu  23926  qtopomap  23928  qtopcmap  23929  kqtop  23955  kqt0  23956  nrmr0reg  23959  regr1  23960  kqreg  23961  kqnrm  23962  hmeoqtop  23985  hmphref  23991  xpstopnlem1  24019  ptcmpfi  24023  xkocnv  24024  xkohmeo  24025  kqhmph  24029  flimsncls  24196  cnpflfi  24209  flfcnp  24214  flfcnp2  24217  cnpfcfi  24250  cnextucn  24512  cnmpopc  25140  htpyco1  25190  htpyco2  25191  phtpyco2  25202  pcopt  25234  pcopt2  25235  pcorevlem  25238  pi1cof  25271  pi1coghm  25273  cvxsconn  35774  clduni  49738