Theorem toptopon 23074

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

Syntax hints:   ↔ wb 209   = wceq 1570   ∈ wcel 2143  ∪ cuni 4872  ‘cfv 6536  Topctop 23050  TopOnctopon 23067

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1825  ax-4 1839  ax-5 1940  ax-6 1997  ax-7 2038  ax-8 2145  ax-9 2153  ax-10 2176  ax-11 2192  ax-12 2213  ax-ext 2735  ax-sep 5257  ax-nul 5269  ax-pow 5336  ax-pr 5404  ax-un 7732

This theorem depends on definitions:  df-bi 210  df-an 401  df-or 861  df-3an 1105  df-tru 1573  df-fal 1583  df-ex 1810  df-nf 1814  df-sb 2097  df-mo 2567  df-eu 2597  df-clab 2742  df-cleq 2755  df-clel 2838  df-nfc 2912  df-ne 2959  df-ral 3080  df-rex 3090  df-rab 3417  df-v 3457  df-dif 3908  df-un 3910  df-in 3912  df-ss 3922  df-nul 4287  df-if 4488  df-pw 4564  df-sn 4590  df-pr 4592  df-op 4596  df-uni 4873  df-br 5110  df-opab 5174  df-mpt 5193  df-id 5556  df-xp 5667  df-rel 5668  df-cnv 5669  df-co 5670  df-dm 5671  df-iota 6492  df-fun 6538  df-fv 6544  df-topon 23068

This theorem is referenced by:  toptopon2  23075  eltpsi  23101  restuni  23319  stoig  23320  restlp  23340  restperf  23341  perfopn  23342  iscn2  23395  iscnp2  23396  cncnpi  23435  cncnp2  23438  cnnei  23439  cnrest  23442  cnpresti  23445  cnprest  23446  cnprest2  23447  paste  23451  t1sep2  23526  sshauslem  23529  1stcelcls  23618  kgenuni  23696  iskgen3  23706  txuni  23749  ptuniconst  23755  txcnmpt  23781  txcn  23783  txindis  23791  ptrescn  23796  txcmpb  23801  xkoptsub  23811  xkofvcn  23841  imasnopn  23847  imasncld  23848  imasncls  23849  qtopcmplem  23864  qtopkgen  23867  hmeof1o  23921  hmeores  23928  hmphindis  23954  cmphaushmeo  23957  txhmeo  23960  ptunhmeo  23965  hausflim  24138  flfneii  24149  hausflf  24154  flimfnfcls  24185  flfcntr  24200  cnextfun  24221  cnextfvval  24222  cnextf  24223  cnextcn  24224  cnextfres1  24225  retopon  24920  evth  25118  evth2  25119  qtophaus  34226  rrhre  34411  pconnconn  35723  connpconn  35727  pconnpi1  35729  sconnpi1  35731  txsconnlem  35732  txsconn  35733  cvmsf1o  35764  cvmliftmolem1  35773  cvmliftlem8  35784  cvmlift2lem9a  35795  cvmlift2lem9  35803  cvmlift2lem11  35805  cvmlift2lem12  35806  cvmliftphtlem  35809  cvmlift3lem6  35816  cvmlift3lem8  35818  cvmlift3lem9  35819  cnres2  38414  cnresima  38415  hausgraph  43932  ntrf2  44850  fcnre  45745