Theorem toptopon 22780

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 22775	. . 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 2109  ∪ cuni 4867  ‘cfv 6499  Topctop 22756  TopOnctopon 22773

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 2008  ax-8 2111  ax-9 2119  ax-10 2142  ax-11 2158  ax-12 2178  ax-ext 2701  ax-sep 5246  ax-nul 5256  ax-pow 5315  ax-pr 5382  ax-un 7691

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 848  df-3an 1088  df-tru 1543  df-fal 1553  df-ex 1780  df-nf 1784  df-sb 2066  df-mo 2533  df-eu 2562  df-clab 2708  df-cleq 2721  df-clel 2803  df-nfc 2878  df-ral 3045  df-rex 3054  df-rab 3403  df-v 3446  df-dif 3914  df-un 3916  df-in 3918  df-ss 3928  df-nul 4293  df-if 4485  df-pw 4561  df-sn 4586  df-pr 4588  df-op 4592  df-uni 4868  df-br 5103  df-opab 5165  df-mpt 5184  df-id 5526  df-xp 5637  df-rel 5638  df-cnv 5639  df-co 5640  df-dm 5641  df-iota 6452  df-fun 6501  df-fv 6507  df-topon 22774

This theorem is referenced by:  toptopon2  22781  eltpsi  22807  restuni  23025  stoig  23026  restlp  23046  restperf  23047  perfopn  23048  iscn2  23101  iscnp2  23102  cncnpi  23141  cncnp2  23144  cnnei  23145  cnrest  23148  cnpresti  23151  cnprest  23152  cnprest2  23153  paste  23157  t1sep2  23232  sshauslem  23235  1stcelcls  23324  kgenuni  23402  iskgen3  23412  txuni  23455  ptuniconst  23461  txcnmpt  23487  txcn  23489  txindis  23497  ptrescn  23502  txcmpb  23507  xkoptsub  23517  xkofvcn  23547  imasnopn  23553  imasncld  23554  imasncls  23555  qtopcmplem  23570  qtopkgen  23573  hmeof1o  23627  hmeores  23634  hmphindis  23660  cmphaushmeo  23663  txhmeo  23666  ptunhmeo  23671  hausflim  23844  flfneii  23855  hausflf  23860  flimfnfcls  23891  flfcntr  23906  cnextfun  23927  cnextfvval  23928  cnextf  23929  cnextcn  23930  cnextfres1  23931  retopon  24627  evth  24834  evth2  24835  qtophaus  33799  rrhre  33984  pconnconn  35191  connpconn  35195  pconnpi1  35197  sconnpi1  35199  txsconnlem  35200  txsconn  35201  cvmsf1o  35232  cvmliftmolem1  35241  cvmliftlem8  35252  cvmlift2lem9a  35263  cvmlift2lem9  35271  cvmlift2lem11  35273  cvmlift2lem12  35274  cvmliftphtlem  35277  cvmlift3lem6  35284  cvmlift3lem8  35286  cvmlift3lem9  35287  cnres2  37730  cnresima  37731  hausgraph  43167  ntrf2  44086  fcnre  44992