Theorem toptopon 22938

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

Syntax hints:   ↔ wb 206   = wceq 1536   ∈ wcel 2105  ∪ cuni 4911  ‘cfv 6562  Topctop 22914  TopOnctopon 22931

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1791  ax-4 1805  ax-5 1907  ax-6 1964  ax-7 2004  ax-8 2107  ax-9 2115  ax-10 2138  ax-11 2154  ax-12 2174  ax-ext 2705  ax-sep 5301  ax-nul 5311  ax-pow 5370  ax-pr 5437  ax-un 7753

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 848  df-3an 1088  df-tru 1539  df-fal 1549  df-ex 1776  df-nf 1780  df-sb 2062  df-mo 2537  df-eu 2566  df-clab 2712  df-cleq 2726  df-clel 2813  df-nfc 2889  df-ral 3059  df-rex 3068  df-rab 3433  df-v 3479  df-dif 3965  df-un 3967  df-in 3969  df-ss 3979  df-nul 4339  df-if 4531  df-pw 4606  df-sn 4631  df-pr 4633  df-op 4637  df-uni 4912  df-br 5148  df-opab 5210  df-mpt 5231  df-id 5582  df-xp 5694  df-rel 5695  df-cnv 5696  df-co 5697  df-dm 5698  df-iota 6515  df-fun 6564  df-fv 6570  df-topon 22932

This theorem is referenced by:  toptopon2  22939  eltpsi  22966  restuni  23185  stoig  23186  restlp  23206  restperf  23207  perfopn  23208  iscn2  23261  iscnp2  23262  cncnpi  23301  cncnp2  23304  cnnei  23305  cnrest  23308  cnpresti  23311  cnprest  23312  cnprest2  23313  paste  23317  t1sep2  23392  sshauslem  23395  1stcelcls  23484  kgenuni  23562  iskgen3  23572  txuni  23615  ptuniconst  23621  txcnmpt  23647  txcn  23649  txindis  23657  ptrescn  23662  txcmpb  23667  xkoptsub  23677  xkofvcn  23707  imasnopn  23713  imasncld  23714  imasncls  23715  qtopcmplem  23730  qtopkgen  23733  hmeof1o  23787  hmeores  23794  hmphindis  23820  cmphaushmeo  23823  txhmeo  23826  ptunhmeo  23831  hausflim  24004  flfneii  24015  hausflf  24020  flimfnfcls  24051  flfcntr  24066  cnextfun  24087  cnextfvval  24088  cnextf  24089  cnextcn  24090  cnextfres1  24091  retopon  24799  evth  25004  evth2  25005  qtophaus  33796  rrhre  33983  pconnconn  35215  connpconn  35219  pconnpi1  35221  sconnpi1  35223  txsconnlem  35224  txsconn  35225  cvmsf1o  35256  cvmliftmolem1  35265  cvmliftlem8  35276  cvmlift2lem9a  35287  cvmlift2lem9  35295  cvmlift2lem11  35297  cvmlift2lem12  35298  cvmliftphtlem  35301  cvmlift3lem6  35308  cvmlift3lem8  35310  cvmlift3lem9  35311  cnres2  37749  cnresima  37750  hausgraph  43193  ntrf2  44113  fcnre  44962