Theorem toptopon 22066

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

Syntax hints:   ↔ wb 205   = wceq 1539   ∈ wcel 2106  ∪ cuni 4839  ‘cfv 6433  Topctop 22042  TopOnctopon 22059

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1798  ax-4 1812  ax-5 1913  ax-6 1971  ax-7 2011  ax-8 2108  ax-9 2116  ax-10 2137  ax-11 2154  ax-12 2171  ax-ext 2709  ax-sep 5223  ax-nul 5230  ax-pow 5288  ax-pr 5352  ax-un 7588

This theorem depends on definitions:  df-bi 206  df-an 397  df-or 845  df-3an 1088  df-tru 1542  df-fal 1552  df-ex 1783  df-nf 1787  df-sb 2068  df-mo 2540  df-eu 2569  df-clab 2716  df-cleq 2730  df-clel 2816  df-nfc 2889  df-ral 3069  df-rex 3070  df-rab 3073  df-v 3434  df-dif 3890  df-un 3892  df-in 3894  df-ss 3904  df-nul 4257  df-if 4460  df-pw 4535  df-sn 4562  df-pr 4564  df-op 4568  df-uni 4840  df-br 5075  df-opab 5137  df-mpt 5158  df-id 5489  df-xp 5595  df-rel 5596  df-cnv 5597  df-co 5598  df-dm 5599  df-iota 6391  df-fun 6435  df-fv 6441  df-topon 22060

This theorem is referenced by:  toptopon2  22067  eltpsi  22094  restuni  22313  stoig  22314  restlp  22334  restperf  22335  perfopn  22336  iscn2  22389  iscnp2  22390  cncnpi  22429  cncnp2  22432  cnnei  22433  cnrest  22436  cnpresti  22439  cnprest  22440  cnprest2  22441  paste  22445  t1sep2  22520  sshauslem  22523  1stcelcls  22612  kgenuni  22690  iskgen3  22700  txuni  22743  ptuniconst  22749  txcnmpt  22775  txcn  22777  txindis  22785  ptrescn  22790  txcmpb  22795  xkoptsub  22805  xkofvcn  22835  imasnopn  22841  imasncld  22842  imasncls  22843  qtopcmplem  22858  qtopkgen  22861  hmeof1o  22915  hmeores  22922  hmphindis  22948  cmphaushmeo  22951  txhmeo  22954  ptunhmeo  22959  hausflim  23132  flfneii  23143  hausflf  23148  flimfnfcls  23179  flfcntr  23194  cnextfun  23215  cnextfvval  23216  cnextf  23217  cnextcn  23218  cnextfres1  23219  retopon  23927  evth  24122  evth2  24123  qtophaus  31786  rrhre  31971  pconnconn  33193  connpconn  33197  pconnpi1  33199  sconnpi1  33201  txsconnlem  33202  txsconn  33203  cvxsconn  33205  cvmsf1o  33234  cvmliftmolem1  33243  cvmliftlem8  33254  cvmlift2lem9a  33265  cvmlift2lem9  33273  cvmlift2lem11  33275  cvmlift2lem12  33276  cvmliftphtlem  33279  cvmlift3lem6  33286  cvmlift3lem8  33288  cvmlift3lem9  33289  cnres2  35921  cnresima  35922  hausgraph  41037  ntrf2  41734  fcnre  42568