Theorem toptopon 23244

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

This proof depends on syntax axioms:   ↔ wb 209   = wceq 1569   ∈ wcel 2144  ∪ cuni 4866  ‘cfv 6543  Topctop 23220  TopOnctopon 23237

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1827  ax-4 1841  ax-5 1942  ax-6 1999  ax-7 2040  ax-8 2146  ax-9 2154  ax-10 2177  ax-11 2193  ax-12 2212  ax-ext 2732  ax-sep 5248  ax-nul 5259  ax-pow 5327  ax-pr 5391  ax-un 7755

This proof depends on definitions:  df-bi 210  df-an 402  df-or 862  df-3an 1105  df-tru 1572  df-fal 1582  df-ex 1812  df-nf 1816  df-sb 2099  df-mo 2564  df-eu 2594  df-clab 2739  df-cleq 2752  df-clel 2835  df-nfc 2909  df-ne 2956  df-ral 3077  df-rex 3087  df-rab 3413  df-v 3452  df-ss 3897  df-dif 4046  df-in 4090  df-un 4150  df-nul 4278  df-if 4482  df-pw 4558  df-sn 4585  df-pr 4587  df-op 4835  df-uni 4867  df-br 5103  df-opab 5167  df-mpt 5186  df-id 5546  df-xp 5657  df-rel 5658  df-cnv 5659  df-co 5660  df-dm 5661  df-iota 6497  df-fun 6545  df-fv 6551  df-topon 23238

This theorem is used by:  toptopon2  23245  eltpsi  23271  restuni  23489  stoig  23490  restlp  23510  restperf  23511  perfopn  23512  iscn2  23565  iscnp2  23566  cncnpi  23605  cncnp2  23608  cnnei  23609  cnrest  23612  cnpresti  23615  cnprest  23616  cnprest2  23617  paste  23621  t1sep2  23696  sshauslem  23699  1stcelcls  23789  kgenuni  23867  iskgen3  23877  txuni  23920  ptuniconst  23926  txcnmpt  23952  txcn  23954  txindis  23962  ptrescn  23967  txcmpb  23972  xkoptsub  23982  xkofvcn  24012  imasnopn  24018  imasncld  24019  imasncls  24020  qtopcmplem  24035  qtopkgen  24038  hmeof1o  24092  hmeores  24099  hmphindis  24125  cmphaushmeo  24128  txhmeo  24131  ptunhmeo  24136  hausflim  24309  flfneii  24320  hausflf  24325  flimfnfcls  24356  flfcntr  24371  cnextfun  24392  cnextfvval  24393  cnextf  24394  cnextcn  24395  cnextfres1  24396  retopon  25091  evth  25289  evth2  25290  qtophaus  34518  rrhre  34703  pconnconn  36114  connpconn  36118  pconnpi1  36120  sconnpi1  36122  txsconnlem  36123  txsconn  36124  cvmsf1o  36155  cvmliftmolem1  36164  cvmliftlem8  36175  cvmlift2lem9a  36186  cvmlift2lem9  36194  cvmlift2lem11  36196  cvmlift2lem12  36197  cvmliftphtlem  36200  cvmlift3lem6  36207  cvmlift3lem8  36209  cvmlift3lem9  36210  cnres2  38834  cnresima  38835  hausgraph  44344  ntrf2  45261  fcnre  46178