Theorem toptopon 22855

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

Syntax hints:   ↔ wb 206   = wceq 1540   ∈ wcel 2108  ∪ cuni 4883  ‘cfv 6531  Topctop 22831  TopOnctopon 22848

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1795  ax-4 1809  ax-5 1910  ax-6 1967  ax-7 2007  ax-8 2110  ax-9 2118  ax-10 2141  ax-11 2157  ax-12 2177  ax-ext 2707  ax-sep 5266  ax-nul 5276  ax-pow 5335  ax-pr 5402  ax-un 7729

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 848  df-3an 1088  df-tru 1543  df-fal 1553  df-ex 1780  df-nf 1784  df-sb 2065  df-mo 2539  df-eu 2568  df-clab 2714  df-cleq 2727  df-clel 2809  df-nfc 2885  df-ral 3052  df-rex 3061  df-rab 3416  df-v 3461  df-dif 3929  df-un 3931  df-in 3933  df-ss 3943  df-nul 4309  df-if 4501  df-pw 4577  df-sn 4602  df-pr 4604  df-op 4608  df-uni 4884  df-br 5120  df-opab 5182  df-mpt 5202  df-id 5548  df-xp 5660  df-rel 5661  df-cnv 5662  df-co 5663  df-dm 5664  df-iota 6484  df-fun 6533  df-fv 6539  df-topon 22849

This theorem is referenced by:  toptopon2  22856  eltpsi  22882  restuni  23100  stoig  23101  restlp  23121  restperf  23122  perfopn  23123  iscn2  23176  iscnp2  23177  cncnpi  23216  cncnp2  23219  cnnei  23220  cnrest  23223  cnpresti  23226  cnprest  23227  cnprest2  23228  paste  23232  t1sep2  23307  sshauslem  23310  1stcelcls  23399  kgenuni  23477  iskgen3  23487  txuni  23530  ptuniconst  23536  txcnmpt  23562  txcn  23564  txindis  23572  ptrescn  23577  txcmpb  23582  xkoptsub  23592  xkofvcn  23622  imasnopn  23628  imasncld  23629  imasncls  23630  qtopcmplem  23645  qtopkgen  23648  hmeof1o  23702  hmeores  23709  hmphindis  23735  cmphaushmeo  23738  txhmeo  23741  ptunhmeo  23746  hausflim  23919  flfneii  23930  hausflf  23935  flimfnfcls  23966  flfcntr  23981  cnextfun  24002  cnextfvval  24003  cnextf  24004  cnextcn  24005  cnextfres1  24006  retopon  24702  evth  24909  evth2  24910  qtophaus  33867  rrhre  34052  pconnconn  35253  connpconn  35257  pconnpi1  35259  sconnpi1  35261  txsconnlem  35262  txsconn  35263  cvmsf1o  35294  cvmliftmolem1  35303  cvmliftlem8  35314  cvmlift2lem9a  35325  cvmlift2lem9  35333  cvmlift2lem11  35335  cvmlift2lem12  35336  cvmliftphtlem  35339  cvmlift3lem6  35346  cvmlift3lem8  35348  cvmlift3lem9  35349  cnres2  37787  cnresima  37788  hausgraph  43229  ntrf2  44148  fcnre  45049