Theorem toptopon 22426

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

Syntax hints:   ↔ wb 205   = wceq 1541   ∈ wcel 2106  ∪ cuni 4908  ‘cfv 6543  Topctop 22402  TopOnctopon 22419

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1797  ax-4 1811  ax-5 1913  ax-6 1971  ax-7 2011  ax-8 2108  ax-9 2116  ax-10 2137  ax-11 2154  ax-12 2171  ax-ext 2703  ax-sep 5299  ax-nul 5306  ax-pow 5363  ax-pr 5427  ax-un 7727

This theorem depends on definitions:  df-bi 206  df-an 397  df-or 846  df-3an 1089  df-tru 1544  df-fal 1554  df-ex 1782  df-nf 1786  df-sb 2068  df-mo 2534  df-eu 2563  df-clab 2710  df-cleq 2724  df-clel 2810  df-nfc 2885  df-ral 3062  df-rex 3071  df-rab 3433  df-v 3476  df-dif 3951  df-un 3953  df-in 3955  df-ss 3965  df-nul 4323  df-if 4529  df-pw 4604  df-sn 4629  df-pr 4631  df-op 4635  df-uni 4909  df-br 5149  df-opab 5211  df-mpt 5232  df-id 5574  df-xp 5682  df-rel 5683  df-cnv 5684  df-co 5685  df-dm 5686  df-iota 6495  df-fun 6545  df-fv 6551  df-topon 22420

This theorem is referenced by:  toptopon2  22427  eltpsi  22454  restuni  22673  stoig  22674  restlp  22694  restperf  22695  perfopn  22696  iscn2  22749  iscnp2  22750  cncnpi  22789  cncnp2  22792  cnnei  22793  cnrest  22796  cnpresti  22799  cnprest  22800  cnprest2  22801  paste  22805  t1sep2  22880  sshauslem  22883  1stcelcls  22972  kgenuni  23050  iskgen3  23060  txuni  23103  ptuniconst  23109  txcnmpt  23135  txcn  23137  txindis  23145  ptrescn  23150  txcmpb  23155  xkoptsub  23165  xkofvcn  23195  imasnopn  23201  imasncld  23202  imasncls  23203  qtopcmplem  23218  qtopkgen  23221  hmeof1o  23275  hmeores  23282  hmphindis  23308  cmphaushmeo  23311  txhmeo  23314  ptunhmeo  23319  hausflim  23492  flfneii  23503  hausflf  23508  flimfnfcls  23539  flfcntr  23554  cnextfun  23575  cnextfvval  23576  cnextf  23577  cnextcn  23578  cnextfres1  23579  retopon  24287  evth  24482  evth2  24483  qtophaus  32885  rrhre  33070  pconnconn  34291  connpconn  34295  pconnpi1  34297  sconnpi1  34299  txsconnlem  34300  txsconn  34301  cvxsconn  34303  cvmsf1o  34332  cvmliftmolem1  34341  cvmliftlem8  34352  cvmlift2lem9a  34363  cvmlift2lem9  34371  cvmlift2lem11  34373  cvmlift2lem12  34374  cvmliftphtlem  34377  cvmlift3lem6  34384  cvmlift3lem8  34386  cvmlift3lem9  34387  cnres2  36717  cnresima  36718  hausgraph  42036  ntrf2  42957  fcnre  43791