Theorem toptopon 21133

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 21128	. . 3 ⊢ (𝐽 ∈ (TopOn‘𝑋) ↔ (𝐽 ∈ Top ∧ 𝑋 = ∪ 𝐽))
3	1, 2	mpbiran2 700	. 2 ⊢ (𝐽 ∈ (TopOn‘𝑋) ↔ 𝐽 ∈ Top)
4	3	bicomi 216	1 ⊢ (𝐽 ∈ Top ↔ 𝐽 ∈ (TopOn‘𝑋))

Syntax hints:   ↔ wb 198   = wceq 1601   ∈ wcel 2107  ∪ cuni 4673  ‘cfv 6137  Topctop 21109  TopOnctopon 21126

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1839  ax-4 1853  ax-5 1953  ax-6 2021  ax-7 2055  ax-8 2109  ax-9 2116  ax-10 2135  ax-11 2150  ax-12 2163  ax-13 2334  ax-ext 2754  ax-sep 5019  ax-nul 5027  ax-pow 5079  ax-pr 5140  ax-un 7228

This theorem depends on definitions:  df-bi 199  df-an 387  df-or 837  df-3an 1073  df-tru 1605  df-ex 1824  df-nf 1828  df-sb 2012  df-mo 2551  df-eu 2587  df-clab 2764  df-cleq 2770  df-clel 2774  df-nfc 2921  df-ral 3095  df-rex 3096  df-rab 3099  df-v 3400  df-sbc 3653  df-dif 3795  df-un 3797  df-in 3799  df-ss 3806  df-nul 4142  df-if 4308  df-pw 4381  df-sn 4399  df-pr 4401  df-op 4405  df-uni 4674  df-br 4889  df-opab 4951  df-mpt 4968  df-id 5263  df-xp 5363  df-rel 5364  df-cnv 5365  df-co 5366  df-dm 5367  df-iota 6101  df-fun 6139  df-fv 6145  df-topon 21127

This theorem is referenced by:  toptopon2  21134  eltpsi  21160  neiptopreu  21349  restuni  21378  stoig  21379  restlp  21399  restperf  21400  perfopn  21401  iscn2  21454  iscnp2  21455  lmcvg  21478  cnss1  21492  cnss2  21493  cncnpi  21494  cncnp2  21497  cnnei  21498  cnrest  21501  cnrest2  21502  cnrest2r  21503  cnpresti  21504  cnprest  21505  cnprest2  21506  paste  21510  lmss  21514  lmcnp  21520  lmcn  21521  t1t0  21564  haust1  21568  restcnrm  21578  resthauslem  21579  t1sep2  21585  sshauslem  21588  lmmo  21596  rncmp  21612  connima  21641  conncn  21642  1stcelcls  21677  kgeni  21753  kgenuni  21755  kgenftop  21756  kgenss  21759  kgenhaus  21760  kgencmp2  21762  kgenidm  21763  iskgen3  21765  1stckgen  21770  kgencn3  21774  kgen2cn  21775  txuni  21808  ptuniconst  21814  dfac14  21834  ptcnplem  21837  ptcnp  21838  txcnmpt  21840  txcn  21842  ptcn  21843  txindis  21850  txdis1cn  21851  ptrescn  21855  txcmpb  21860  lmcn2  21865  txkgen  21868  xkohaus  21869  xkoptsub  21870  xkopt  21871  cnmpt11  21879  cnmpt11f  21880  cnmpt1t  21881  cnmpt12  21883  cnmpt21  21887  cnmpt21f  21888  cnmpt2t  21889  cnmpt22  21890  cnmpt22f  21891  cnmptcom  21894  cnmptkp  21896  xkofvcn  21900  cnmpt2k  21904  txconn  21905  imasnopn  21906  imasncld  21907  imasncls  21908  qtopcmplem  21923  qtopkgen  21926  qtopss  21931  qtopeu  21932  qtopomap  21934  qtopcmap  21935  kqtop  21961  kqt0  21962  nrmr0reg  21965  regr1  21966  kqreg  21967  kqnrm  21968  hmeof1o  21980  hmeores  21987  hmeoqtop  21991  hmphref  21997  hmphindis  22013  cmphaushmeo  22016  txhmeo  22019  ptunhmeo  22024  xpstopnlem1  22025  ptcmpfi  22029  xkocnv  22030  xkohmeo  22031  kqhmph  22035  hausflim  22197  flimsncls  22202  flfneii  22208  hausflf  22213  cnpflfi  22215  flfcnp  22220  flfcnp2  22223  flimfnfcls  22244  cnpfcfi  22256  flfcntr  22259  cnextfun  22280  cnextfvval  22281  cnextf  22282  cnextcn  22283  cnextfres1  22284  cnextucn  22519  retopon  22979  cnmpt2pc  23139  evth  23170  evth2  23171  htpyco1  23189  htpyco2  23190  phtpyco2  23201  pcopt  23233  pcopt2  23234  pcorevlem  23237  pi1cof  23270  pi1coghm  23272  qtophaus  30505  rrhre  30667  pconnconn  31816  connpconn  31820  pconnpi1  31822  sconnpi1  31824  txsconnlem  31825  txsconn  31826  cvxsconn  31828  cvmsf1o  31857  cvmliftmolem1  31866  cvmliftlem8  31877  cvmlift2lem9a  31888  cvmlift2lem9  31896  cvmlift2lem11  31898  cvmlift2lem12  31899  cvmliftphtlem  31902  cvmlift3lem6  31909  cvmlift3lem8  31911  cvmlift3lem9  31912  cnres2  34191  cnresima  34192  hausgraph  38759  ntrf2  39388  fcnre  40127