Theorem toptopon 21528

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

Syntax hints:   ↔ wb 208   = wceq 1536   ∈ wcel 2113  ∪ cuni 4841  ‘cfv 6358  Topctop 21504  TopOnctopon 21521

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 1969  ax-7 2014  ax-8 2115  ax-9 2123  ax-10 2144  ax-11 2160  ax-12 2176  ax-ext 2796  ax-sep 5206  ax-nul 5213  ax-pow 5269  ax-pr 5333  ax-un 7464

This theorem depends on definitions:  df-bi 209  df-an 399  df-or 844  df-3an 1085  df-tru 1539  df-ex 1780  df-nf 1784  df-sb 2069  df-mo 2621  df-eu 2653  df-clab 2803  df-cleq 2817  df-clel 2896  df-nfc 2966  df-ral 3146  df-rex 3147  df-rab 3150  df-v 3499  df-sbc 3776  df-dif 3942  df-un 3944  df-in 3946  df-ss 3955  df-nul 4295  df-if 4471  df-pw 4544  df-sn 4571  df-pr 4573  df-op 4577  df-uni 4842  df-br 5070  df-opab 5132  df-mpt 5150  df-id 5463  df-xp 5564  df-rel 5565  df-cnv 5566  df-co 5567  df-dm 5568  df-iota 6317  df-fun 6360  df-fv 6366  df-topon 21522

This theorem is referenced by:  toptopon2  21529  eltpsi  21555  restuni  21773  stoig  21774  restlp  21794  restperf  21795  perfopn  21796  iscn2  21849  iscnp2  21850  cncnpi  21889  cncnp2  21892  cnnei  21893  cnrest  21896  cnpresti  21899  cnprest  21900  cnprest2  21901  paste  21905  t1sep2  21980  sshauslem  21983  1stcelcls  22072  kgenuni  22150  iskgen3  22160  txuni  22203  ptuniconst  22209  txcnmpt  22235  txcn  22237  txindis  22245  ptrescn  22250  txcmpb  22255  xkoptsub  22265  xkofvcn  22295  imasnopn  22301  imasncld  22302  imasncls  22303  qtopcmplem  22318  qtopkgen  22321  hmeof1o  22375  hmeores  22382  hmphindis  22408  cmphaushmeo  22411  txhmeo  22414  ptunhmeo  22419  hausflim  22592  flfneii  22603  hausflf  22608  flimfnfcls  22639  flfcntr  22654  cnextfun  22675  cnextfvval  22676  cnextf  22677  cnextcn  22678  cnextfres1  22679  retopon  23375  evth  23566  evth2  23567  qtophaus  31104  rrhre  31266  pconnconn  32482  connpconn  32486  pconnpi1  32488  sconnpi1  32490  txsconnlem  32491  txsconn  32492  cvxsconn  32494  cvmsf1o  32523  cvmliftmolem1  32532  cvmliftlem8  32543  cvmlift2lem9a  32554  cvmlift2lem9  32562  cvmlift2lem11  32564  cvmlift2lem12  32565  cvmliftphtlem  32568  cvmlift3lem6  32575  cvmlift3lem8  32577  cvmlift3lem9  32578  cnres2  35045  cnresima  35046  hausgraph  39818  ntrf2  40480  fcnre  41288