Theorem toptopon2 23144

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

This proof depends on syntax axioms:   ↔ wb 209   ∈ wcel 2145  ∪ cuni 4867  ‘cfv 6533  Topctop 23119  TopOnctopon 23136

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 2147  ax-9 2155  ax-10 2178  ax-11 2194  ax-12 2213  ax-ext 2732  ax-sep 5251  ax-nul 5263  ax-pow 5330  ax-pr 5398  ax-un 7737

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 2564  df-eu 2594  df-clab 2739  df-cleq 2752  df-clel 2835  df-nfc 2909  df-ne 2956  df-ral 3077  df-rex 3087  df-rab 3413  df-v 3452  df-dif 3902  df-un 3904  df-in 3906  df-ss 3916  df-nul 4280  df-if 4483  df-pw 4559  df-sn 4585  df-pr 4587  df-op 4591  df-uni 4868  df-br 5104  df-opab 5168  df-mpt 5187  df-id 5550  df-xp 5661  df-rel 5662  df-cnv 5663  df-co 5664  df-dm 5665  df-iota 6489  df-fun 6535  df-fv 6541  df-topon 23137

This theorem is used by:  topontopon  23145  toprntopon  23151  neiptopreu  23359  lmcvg  23488  cnss1  23502  cnss2  23503  cnrest2  23512  cnrest2r  23513  lmss  23524  lmcnp  23530  lmcn  23531  t1t0  23574  haust1  23578  restcnrm  23588  resthauslem  23589  lmmo  23606  rncmp  23622  connima  23651  conncn  23652  kgeni  23764  kgenftop  23767  kgenss  23770  kgenhaus  23771  kgencmp2  23773  kgenidm  23774  1stckgen  23781  kgencn3  23785  kgen2cn  23786  dfac14  23845  ptcnplem  23848  ptcnp  23849  txcnmpt  23851  ptcn  23854  txdis1cn  23862  lmcn2  23876  txkgen  23879  xkohaus  23880  xkopt  23882  cnmpt11  23890  cnmpt11f  23891  cnmpt1t  23892  cnmpt12  23894  cnmpt21  23898  cnmpt21f  23899  cnmpt2t  23900  cnmpt22  23901  cnmpt22f  23902  cnmptcom  23905  cnmptkp  23907  cnmpt2k  23915  txconn  23916  qtopss  23942  qtopeu  23943  qtopomap  23945  qtopcmap  23946  kqtop  23972  kqt0  23973  nrmr0reg  23976  regr1  23977  kqreg  23978  kqnrm  23979  hmeoqtop  24002  hmphref  24008  xpstopnlem1  24036  ptcmpfi  24040  xkocnv  24041  xkohmeo  24042  kqhmph  24046  flimsncls  24213  cnpflfi  24226  flfcnp  24231  flfcnp2  24234  cnpfcfi  24267  cnextucn  24529  cnmpopc  25157  htpyco1  25207  htpyco2  25208  phtpyco2  25219  pcopt  25251  pcopt2  25252  pcorevlem  25255  pi1cof  25288  pi1coghm  25290  cvxsconn  35823  clduni  49828