Theorem toptopon 21519

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

Syntax hints:   ↔ wb 208   = wceq 1533   ∈ wcel 2110  ∪ cuni 4831  ‘cfv 6349  Topctop 21495  TopOnctopon 21512

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1792  ax-4 1806  ax-5 1907  ax-6 1966  ax-7 2011  ax-8 2112  ax-9 2120  ax-10 2141  ax-11 2157  ax-12 2173  ax-ext 2793  ax-sep 5195  ax-nul 5202  ax-pow 5258  ax-pr 5321  ax-un 7455

This theorem depends on definitions:  df-bi 209  df-an 399  df-or 844  df-3an 1085  df-tru 1536  df-ex 1777  df-nf 1781  df-sb 2066  df-mo 2618  df-eu 2650  df-clab 2800  df-cleq 2814  df-clel 2893  df-nfc 2963  df-ral 3143  df-rex 3144  df-rab 3147  df-v 3496  df-sbc 3772  df-dif 3938  df-un 3940  df-in 3942  df-ss 3951  df-nul 4291  df-if 4467  df-pw 4540  df-sn 4561  df-pr 4563  df-op 4567  df-uni 4832  df-br 5059  df-opab 5121  df-mpt 5139  df-id 5454  df-xp 5555  df-rel 5556  df-cnv 5557  df-co 5558  df-dm 5559  df-iota 6308  df-fun 6351  df-fv 6357  df-topon 21513

This theorem is referenced by:  toptopon2  21520  eltpsi  21546  restuni  21764  stoig  21765  restlp  21785  restperf  21786  perfopn  21787  iscn2  21840  iscnp2  21841  cncnpi  21880  cncnp2  21883  cnnei  21884  cnrest  21887  cnpresti  21890  cnprest  21891  cnprest2  21892  paste  21896  t1sep2  21971  sshauslem  21974  1stcelcls  22063  kgenuni  22141  iskgen3  22151  txuni  22194  ptuniconst  22200  txcnmpt  22226  txcn  22228  txindis  22236  ptrescn  22241  txcmpb  22246  xkoptsub  22256  xkofvcn  22286  imasnopn  22292  imasncld  22293  imasncls  22294  qtopcmplem  22309  qtopkgen  22312  hmeof1o  22366  hmeores  22373  hmphindis  22399  cmphaushmeo  22402  txhmeo  22405  ptunhmeo  22410  hausflim  22583  flfneii  22594  hausflf  22599  flimfnfcls  22630  flfcntr  22645  cnextfun  22666  cnextfvval  22667  cnextf  22668  cnextcn  22669  cnextfres1  22670  retopon  23366  evth  23557  evth2  23558  qtophaus  31095  rrhre  31257  pconnconn  32473  connpconn  32477  pconnpi1  32479  sconnpi1  32481  txsconnlem  32482  txsconn  32483  cvxsconn  32485  cvmsf1o  32514  cvmliftmolem1  32523  cvmliftlem8  32534  cvmlift2lem9a  32545  cvmlift2lem9  32553  cvmlift2lem11  32555  cvmlift2lem12  32556  cvmliftphtlem  32559  cvmlift3lem6  32566  cvmlift3lem8  32568  cvmlift3lem9  32569  cnres2  35035  cnresima  35036  hausgraph  39805  ntrf2  40467  fcnre  41275