Theorem toptopon 22923

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

Syntax hints:   ↔ wb 206   = wceq 1540   ∈ wcel 2108  ∪ cuni 4907  ‘cfv 6561  Topctop 22899  TopOnctopon 22916

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 1967  ax-7 2007  ax-8 2110  ax-9 2118  ax-10 2141  ax-11 2157  ax-12 2177  ax-ext 2708  ax-sep 5296  ax-nul 5306  ax-pow 5365  ax-pr 5432  ax-un 7755

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 849  df-3an 1089  df-tru 1543  df-fal 1553  df-ex 1780  df-nf 1784  df-sb 2065  df-mo 2540  df-eu 2569  df-clab 2715  df-cleq 2729  df-clel 2816  df-nfc 2892  df-ral 3062  df-rex 3071  df-rab 3437  df-v 3482  df-dif 3954  df-un 3956  df-in 3958  df-ss 3968  df-nul 4334  df-if 4526  df-pw 4602  df-sn 4627  df-pr 4629  df-op 4633  df-uni 4908  df-br 5144  df-opab 5206  df-mpt 5226  df-id 5578  df-xp 5691  df-rel 5692  df-cnv 5693  df-co 5694  df-dm 5695  df-iota 6514  df-fun 6563  df-fv 6569  df-topon 22917

This theorem is referenced by:  toptopon2  22924  eltpsi  22951  restuni  23170  stoig  23171  restlp  23191  restperf  23192  perfopn  23193  iscn2  23246  iscnp2  23247  cncnpi  23286  cncnp2  23289  cnnei  23290  cnrest  23293  cnpresti  23296  cnprest  23297  cnprest2  23298  paste  23302  t1sep2  23377  sshauslem  23380  1stcelcls  23469  kgenuni  23547  iskgen3  23557  txuni  23600  ptuniconst  23606  txcnmpt  23632  txcn  23634  txindis  23642  ptrescn  23647  txcmpb  23652  xkoptsub  23662  xkofvcn  23692  imasnopn  23698  imasncld  23699  imasncls  23700  qtopcmplem  23715  qtopkgen  23718  hmeof1o  23772  hmeores  23779  hmphindis  23805  cmphaushmeo  23808  txhmeo  23811  ptunhmeo  23816  hausflim  23989  flfneii  24000  hausflf  24005  flimfnfcls  24036  flfcntr  24051  cnextfun  24072  cnextfvval  24073  cnextf  24074  cnextcn  24075  cnextfres1  24076  retopon  24784  evth  24991  evth2  24992  qtophaus  33835  rrhre  34022  pconnconn  35236  connpconn  35240  pconnpi1  35242  sconnpi1  35244  txsconnlem  35245  txsconn  35246  cvmsf1o  35277  cvmliftmolem1  35286  cvmliftlem8  35297  cvmlift2lem9a  35308  cvmlift2lem9  35316  cvmlift2lem11  35318  cvmlift2lem12  35319  cvmliftphtlem  35322  cvmlift3lem6  35329  cvmlift3lem8  35331  cvmlift3lem9  35332  cnres2  37770  cnresima  37771  hausgraph  43217  ntrf2  44137  fcnre  45030