Theorem toptopon 22895

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

Syntax hints:   ↔ wb 206   = wceq 1542   ∈ wcel 2114  ∪ cuni 4851  ‘cfv 6493  Topctop 22871  TopOnctopon 22888

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 1912  ax-6 1969  ax-7 2010  ax-8 2116  ax-9 2124  ax-10 2147  ax-11 2163  ax-12 2185  ax-ext 2709  ax-sep 5232  ax-nul 5242  ax-pow 5303  ax-pr 5371  ax-un 7683

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 849  df-3an 1089  df-tru 1545  df-fal 1555  df-ex 1782  df-nf 1786  df-sb 2069  df-mo 2540  df-eu 2570  df-clab 2716  df-cleq 2729  df-clel 2812  df-nfc 2886  df-ne 2934  df-ral 3053  df-rex 3063  df-rab 3391  df-v 3432  df-dif 3893  df-un 3895  df-in 3897  df-ss 3907  df-nul 4275  df-if 4468  df-pw 4544  df-sn 4569  df-pr 4571  df-op 4575  df-uni 4852  df-br 5087  df-opab 5149  df-mpt 5168  df-id 5520  df-xp 5631  df-rel 5632  df-cnv 5633  df-co 5634  df-dm 5635  df-iota 6449  df-fun 6495  df-fv 6501  df-topon 22889

This theorem is referenced by:  toptopon2  22896  eltpsi  22922  restuni  23140  stoig  23141  restlp  23161  restperf  23162  perfopn  23163  iscn2  23216  iscnp2  23217  cncnpi  23256  cncnp2  23259  cnnei  23260  cnrest  23263  cnpresti  23266  cnprest  23267  cnprest2  23268  paste  23272  t1sep2  23347  sshauslem  23350  1stcelcls  23439  kgenuni  23517  iskgen3  23527  txuni  23570  ptuniconst  23576  txcnmpt  23602  txcn  23604  txindis  23612  ptrescn  23617  txcmpb  23622  xkoptsub  23632  xkofvcn  23662  imasnopn  23668  imasncld  23669  imasncls  23670  qtopcmplem  23685  qtopkgen  23688  hmeof1o  23742  hmeores  23749  hmphindis  23775  cmphaushmeo  23778  txhmeo  23781  ptunhmeo  23786  hausflim  23959  flfneii  23970  hausflf  23975  flimfnfcls  24006  flfcntr  24021  cnextfun  24042  cnextfvval  24043  cnextf  24044  cnextcn  24045  cnextfres1  24046  retopon  24741  evth  24939  evth2  24940  qtophaus  33999  rrhre  34184  pconnconn  35432  connpconn  35436  pconnpi1  35438  sconnpi1  35440  txsconnlem  35441  txsconn  35442  cvmsf1o  35473  cvmliftmolem1  35482  cvmliftlem8  35493  cvmlift2lem9a  35504  cvmlift2lem9  35512  cvmlift2lem11  35514  cvmlift2lem12  35515  cvmliftphtlem  35518  cvmlift3lem6  35525  cvmlift3lem8  35527  cvmlift3lem9  35528  cnres2  38101  cnresima  38102  hausgraph  43654  ntrf2  44572  fcnre  45477