Theorem toptopon2 23236

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

This proof depends on syntax axioms:   ↔ wb 209   ∈ wcel 2145  ∪ cuni 4867  ‘cfv 6538  Topctop 23211  TopOnctopon 23228

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 2733  ax-sep 5249  ax-nul 5260  ax-pow 5327  ax-pr 5391  ax-un 7751

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 2565  df-eu 2595  df-clab 2740  df-cleq 2753  df-clel 2836  df-nfc 2910  df-ne 2957  df-ral 3078  df-rex 3088  df-rab 3414  df-v 3453  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 5546  df-xp 5657  df-rel 5658  df-cnv 5659  df-co 5660  df-dm 5661  df-iota 6494  df-fun 6540  df-fv 6546  df-topon 23229

This theorem is used by:  topontopon  23237  toprntopon  23243  neiptopreu  23451  lmcvg  23580  cnss1  23594  cnss2  23595  cnrest2  23604  cnrest2r  23605  lmss  23616  lmcnp  23622  lmcn  23623  t1t0  23666  haust1  23670  restcnrm  23680  resthauslem  23681  lmmo  23698  rncmp  23714  connima  23743  conncn  23744  kgeni  23856  kgenftop  23859  kgenss  23862  kgenhaus  23863  kgencmp2  23865  kgenidm  23866  1stckgen  23873  kgencn3  23877  kgen2cn  23878  dfac14  23937  ptcnplem  23940  ptcnp  23941  txcnmpt  23943  ptcn  23946  txdis1cn  23954  lmcn2  23968  txkgen  23971  xkohaus  23972  xkopt  23974  cnmpt11  23982  cnmpt11f  23983  cnmpt1t  23984  cnmpt12  23986  cnmpt21  23990  cnmpt21f  23991  cnmpt2t  23992  cnmpt22  23993  cnmpt22f  23994  cnmptcom  23997  cnmptkp  23999  cnmpt2k  24007  txconn  24008  qtopss  24034  qtopeu  24035  qtopomap  24037  qtopcmap  24038  kqtop  24064  kqt0  24065  nrmr0reg  24068  regr1  24069  kqreg  24070  kqnrm  24071  hmeoqtop  24094  hmphref  24100  xpstopnlem1  24128  ptcmpfi  24132  xkocnv  24133  xkohmeo  24134  kqhmph  24138  flimsncls  24305  cnpflfi  24318  flfcnp  24323  flfcnp2  24326  cnpfcfi  24359  cnextucn  24621  cnmpopc  25249  htpyco1  25299  htpyco2  25300  phtpyco2  25311  pcopt  25343  pcopt2  25344  pcorevlem  25347  pi1cof  25380  pi1coghm  25382  cvxsconn  36008  clduni  50008