Theorem toptopon 22802

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 22797	. . 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 2109  ∪ cuni 4858  ‘cfv 6482  Topctop 22778  TopOnctopon 22795

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 2008  ax-8 2111  ax-9 2119  ax-10 2142  ax-11 2158  ax-12 2178  ax-ext 2701  ax-sep 5235  ax-nul 5245  ax-pow 5304  ax-pr 5371  ax-un 7671

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 2066  df-mo 2533  df-eu 2562  df-clab 2708  df-cleq 2721  df-clel 2803  df-nfc 2878  df-ral 3045  df-rex 3054  df-rab 3395  df-v 3438  df-dif 3906  df-un 3908  df-in 3910  df-ss 3920  df-nul 4285  df-if 4477  df-pw 4553  df-sn 4578  df-pr 4580  df-op 4584  df-uni 4859  df-br 5093  df-opab 5155  df-mpt 5174  df-id 5514  df-xp 5625  df-rel 5626  df-cnv 5627  df-co 5628  df-dm 5629  df-iota 6438  df-fun 6484  df-fv 6490  df-topon 22796

This theorem is referenced by:  toptopon2  22803  eltpsi  22829  restuni  23047  stoig  23048  restlp  23068  restperf  23069  perfopn  23070  iscn2  23123  iscnp2  23124  cncnpi  23163  cncnp2  23166  cnnei  23167  cnrest  23170  cnpresti  23173  cnprest  23174  cnprest2  23175  paste  23179  t1sep2  23254  sshauslem  23257  1stcelcls  23346  kgenuni  23424  iskgen3  23434  txuni  23477  ptuniconst  23483  txcnmpt  23509  txcn  23511  txindis  23519  ptrescn  23524  txcmpb  23529  xkoptsub  23539  xkofvcn  23569  imasnopn  23575  imasncld  23576  imasncls  23577  qtopcmplem  23592  qtopkgen  23595  hmeof1o  23649  hmeores  23656  hmphindis  23682  cmphaushmeo  23685  txhmeo  23688  ptunhmeo  23693  hausflim  23866  flfneii  23877  hausflf  23882  flimfnfcls  23913  flfcntr  23928  cnextfun  23949  cnextfvval  23950  cnextf  23951  cnextcn  23952  cnextfres1  23953  retopon  24649  evth  24856  evth2  24857  qtophaus  33803  rrhre  33988  pconnconn  35204  connpconn  35208  pconnpi1  35210  sconnpi1  35212  txsconnlem  35213  txsconn  35214  cvmsf1o  35245  cvmliftmolem1  35254  cvmliftlem8  35265  cvmlift2lem9a  35276  cvmlift2lem9  35284  cvmlift2lem11  35286  cvmlift2lem12  35287  cvmliftphtlem  35290  cvmlift3lem6  35297  cvmlift3lem8  35299  cvmlift3lem9  35300  cnres2  37743  cnresima  37744  hausgraph  43178  ntrf2  44097  fcnre  45003