Theorem toptopon 22837

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 22832	. . 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 4867  ‘cfv 6499  Topctop 22813  TopOnctopon 22830

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 5246  ax-nul 5256  ax-pow 5315  ax-pr 5382  ax-un 7691

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 3403  df-v 3446  df-dif 3914  df-un 3916  df-in 3918  df-ss 3928  df-nul 4293  df-if 4485  df-pw 4561  df-sn 4586  df-pr 4588  df-op 4592  df-uni 4868  df-br 5103  df-opab 5165  df-mpt 5184  df-id 5526  df-xp 5637  df-rel 5638  df-cnv 5639  df-co 5640  df-dm 5641  df-iota 6452  df-fun 6501  df-fv 6507  df-topon 22831

This theorem is referenced by:  toptopon2  22838  eltpsi  22864  restuni  23082  stoig  23083  restlp  23103  restperf  23104  perfopn  23105  iscn2  23158  iscnp2  23159  cncnpi  23198  cncnp2  23201  cnnei  23202  cnrest  23205  cnpresti  23208  cnprest  23209  cnprest2  23210  paste  23214  t1sep2  23289  sshauslem  23292  1stcelcls  23381  kgenuni  23459  iskgen3  23469  txuni  23512  ptuniconst  23518  txcnmpt  23544  txcn  23546  txindis  23554  ptrescn  23559  txcmpb  23564  xkoptsub  23574  xkofvcn  23604  imasnopn  23610  imasncld  23611  imasncls  23612  qtopcmplem  23627  qtopkgen  23630  hmeof1o  23684  hmeores  23691  hmphindis  23717  cmphaushmeo  23720  txhmeo  23723  ptunhmeo  23728  hausflim  23901  flfneii  23912  hausflf  23917  flimfnfcls  23948  flfcntr  23963  cnextfun  23984  cnextfvval  23985  cnextf  23986  cnextcn  23987  cnextfres1  23988  retopon  24684  evth  24891  evth2  24892  qtophaus  33819  rrhre  34004  pconnconn  35211  connpconn  35215  pconnpi1  35217  sconnpi1  35219  txsconnlem  35220  txsconn  35221  cvmsf1o  35252  cvmliftmolem1  35261  cvmliftlem8  35272  cvmlift2lem9a  35283  cvmlift2lem9  35291  cvmlift2lem11  35293  cvmlift2lem12  35294  cvmliftphtlem  35297  cvmlift3lem6  35304  cvmlift3lem8  35306  cvmlift3lem9  35307  cnres2  37750  cnresima  37751  hausgraph  43187  ntrf2  44106  fcnre  45012