Theorem toptopon 22839

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

Syntax hints:   ↔ wb 205   = wceq 1533   ∈ wcel 2098  ∪ cuni 4912  ‘cfv 6553  Topctop 22815  TopOnctopon 22832

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1789  ax-4 1803  ax-5 1905  ax-6 1963  ax-7 2003  ax-8 2100  ax-9 2108  ax-10 2129  ax-11 2146  ax-12 2166  ax-ext 2699  ax-sep 5303  ax-nul 5310  ax-pow 5369  ax-pr 5433  ax-un 7746

This theorem depends on definitions:  df-bi 206  df-an 395  df-or 846  df-3an 1086  df-tru 1536  df-fal 1546  df-ex 1774  df-nf 1778  df-sb 2060  df-mo 2529  df-eu 2558  df-clab 2706  df-cleq 2720  df-clel 2806  df-nfc 2881  df-ral 3059  df-rex 3068  df-rab 3431  df-v 3475  df-dif 3952  df-un 3954  df-in 3956  df-ss 3966  df-nul 4327  df-if 4533  df-pw 4608  df-sn 4633  df-pr 4635  df-op 4639  df-uni 4913  df-br 5153  df-opab 5215  df-mpt 5236  df-id 5580  df-xp 5688  df-rel 5689  df-cnv 5690  df-co 5691  df-dm 5692  df-iota 6505  df-fun 6555  df-fv 6561  df-topon 22833

This theorem is referenced by:  toptopon2  22840  eltpsi  22867  restuni  23086  stoig  23087  restlp  23107  restperf  23108  perfopn  23109  iscn2  23162  iscnp2  23163  cncnpi  23202  cncnp2  23205  cnnei  23206  cnrest  23209  cnpresti  23212  cnprest  23213  cnprest2  23214  paste  23218  t1sep2  23293  sshauslem  23296  1stcelcls  23385  kgenuni  23463  iskgen3  23473  txuni  23516  ptuniconst  23522  txcnmpt  23548  txcn  23550  txindis  23558  ptrescn  23563  txcmpb  23568  xkoptsub  23578  xkofvcn  23608  imasnopn  23614  imasncld  23615  imasncls  23616  qtopcmplem  23631  qtopkgen  23634  hmeof1o  23688  hmeores  23695  hmphindis  23721  cmphaushmeo  23724  txhmeo  23727  ptunhmeo  23732  hausflim  23905  flfneii  23916  hausflf  23921  flimfnfcls  23952  flfcntr  23967  cnextfun  23988  cnextfvval  23989  cnextf  23990  cnextcn  23991  cnextfres1  23992  retopon  24700  evth  24905  evth2  24906  qtophaus  33470  rrhre  33655  pconnconn  34874  connpconn  34878  pconnpi1  34880  sconnpi1  34882  txsconnlem  34883  txsconn  34884  cvmsf1o  34915  cvmliftmolem1  34924  cvmliftlem8  34935  cvmlift2lem9a  34946  cvmlift2lem9  34954  cvmlift2lem11  34956  cvmlift2lem12  34957  cvmliftphtlem  34960  cvmlift3lem6  34967  cvmlift3lem8  34969  cvmlift3lem9  34970  cnres2  37269  cnresima  37270  hausgraph  42664  ntrf2  43585  fcnre  44418