Theorem toptopon 20770

Description: Alternative definition of Top in terms of TopOn. (Contributed by Mario Carneiro, 13-Aug-2015.)

Hypothesis

Ref	Expression
toptopon.1	⊢ 𝑋 = ∪ 𝐽

Assertion

Ref	Expression
toptopon	⊢ (𝐽 ∈ Top ↔ 𝐽 ∈ (TopOn‘𝑋))

Proof of Theorem toptopon

Step	Hyp	Ref	Expression
1		toptopon.1	. . 3 ⊢ 𝑋 = ∪ 𝐽
2		istopon 20765	. . 3 ⊢ (𝐽 ∈ (TopOn‘𝑋) ↔ (𝐽 ∈ Top ∧ 𝑋 = ∪ 𝐽))
3	1, 2	mpbiran2 974	. 2 ⊢ (𝐽 ∈ (TopOn‘𝑋) ↔ 𝐽 ∈ Top)
4	3	bicomi 214	1 ⊢ (𝐽 ∈ Top ↔ 𝐽 ∈ (TopOn‘𝑋))

Syntax hints:   ↔ wb 196   = wceq 1523   ∈ wcel 2030  ∪ cuni 4468  ‘cfv 5926  Topctop 20746  TopOnctopon 20763

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1762  ax-4 1777  ax-5 1879  ax-6 1945  ax-7 1981  ax-8 2032  ax-9 2039  ax-10 2059  ax-11 2074  ax-12 2087  ax-13 2282  ax-ext 2631  ax-sep 4814  ax-nul 4822  ax-pow 4873  ax-pr 4936  ax-un 6991

This theorem depends on definitions:  df-bi 197  df-or 384  df-an 385  df-3an 1056  df-tru 1526  df-ex 1745  df-nf 1750  df-sb 1938  df-eu 2502  df-mo 2503  df-clab 2638  df-cleq 2644  df-clel 2647  df-nfc 2782  df-ne 2824  df-ral 2946  df-rex 2947  df-rab 2950  df-v 3233  df-sbc 3469  df-dif 3610  df-un 3612  df-in 3614  df-ss 3621  df-nul 3949  df-if 4120  df-pw 4193  df-sn 4211  df-pr 4213  df-op 4217  df-uni 4469  df-br 4686  df-opab 4746  df-mpt 4763  df-id 5053  df-xp 5149  df-rel 5150  df-cnv 5151  df-co 5152  df-dm 5153  df-iota 5889  df-fun 5928  df-fv 5934  df-topon 20764

This theorem is referenced by:  toptopon2  20771  eltpsi  20796  neiptopreu  20985  restuni  21014  stoig  21015  restlp  21035  restperf  21036  perfopn  21037  iscn2  21090  iscnp2  21091  lmcvg  21114  cnss1  21128  cnss2  21129  cncnpi  21130  cncnp2  21133  cnnei  21134  cnrest  21137  cnrest2  21138  cnrest2r  21139  cnpresti  21140  cnprest  21141  cnprest2  21142  paste  21146  lmss  21150  lmcnp  21156  lmcn  21157  t1t0  21200  haust1  21204  restcnrm  21214  resthauslem  21215  t1sep2  21221  sshauslem  21224  lmmo  21232  rncmp  21247  connima  21276  conncn  21277  1stcelcls  21312  kgeni  21388  kgenuni  21390  kgenftop  21391  kgenss  21394  kgenhaus  21395  kgencmp2  21397  kgenidm  21398  iskgen3  21400  1stckgen  21405  kgencn3  21409  kgen2cn  21410  txuni  21443  ptuniconst  21449  dfac14  21469  ptcnplem  21472  ptcnp  21473  txcnmpt  21475  txcn  21477  ptcn  21478  txindis  21485  txdis1cn  21486  ptrescn  21490  txcmpb  21495  lmcn2  21500  txkgen  21503  xkohaus  21504  xkoptsub  21505  xkopt  21506  cnmpt11  21514  cnmpt11f  21515  cnmpt1t  21516  cnmpt12  21518  cnmpt21  21522  cnmpt21f  21523  cnmpt2t  21524  cnmpt22  21525  cnmpt22f  21526  cnmptcom  21529  cnmptkp  21531  xkofvcn  21535  cnmpt2k  21539  txconn  21540  imasnopn  21541  imasncld  21542  imasncls  21543  qtopcmplem  21558  qtopkgen  21561  qtopss  21566  qtopeu  21567  qtopomap  21569  qtopcmap  21570  kqtop  21596  kqt0  21597  nrmr0reg  21600  regr1  21601  kqreg  21602  kqnrm  21603  hmeof1o  21615  hmeores  21622  hmeoqtop  21626  hmphref  21632  hmphindis  21648  cmphaushmeo  21651  txhmeo  21654  ptunhmeo  21659  xpstopnlem1  21660  ptcmpfi  21664  xkocnv  21665  xkohmeo  21666  kqhmph  21670  hausflim  21832  flimsncls  21837  flfneii  21843  hausflf  21848  cnpflfi  21850  flfcnp  21855  flfcnp2  21858  flimfnfcls  21879  cnpfcfi  21891  flfcntr  21894  cnextfun  21915  cnextfvval  21916  cnextf  21917  cnextcn  21918  cnextfres1  21919  cnextucn  22154  retopon  22614  cnmpt2pc  22774  evth  22805  evth2  22806  htpyco1  22824  htpyco2  22825  phtpyco2  22836  pcopt  22868  pcopt2  22869  pcorevlem  22872  pi1cof  22905  pi1coghm  22907  qtophaus  30031  rrhre  30193  pconnconn  31339  connpconn  31343  pconnpi1  31345  sconnpi1  31347  txsconnlem  31348  txsconn  31349  cvxsconn  31351  cvmsf1o  31380  cvmliftmolem1  31389  cvmliftlem8  31400  cvmlift2lem9a  31411  cvmlift2lem9  31419  cvmlift2lem11  31421  cvmlift2lem12  31422  cvmliftphtlem  31425  cvmlift3lem6  31432  cvmlift3lem8  31434  cvmlift3lem9  31435  cnres2  33692  cnresima  33693  hausgraph  38107  ntrf2  38739  fcnre  39498