Theorem toptopon 23235

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 23230	. . 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 1570   ∈ wcel 2145  ∪ cuni 4867  ‘cfv 6538  Topctop 23211  TopOnctopon 23228

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1828  ax-4 1842  ax-5 1943  ax-6 2000  ax-7 2041  ax-8 2147  ax-9 2155  ax-10 2178  ax-11 2194  ax-12 2213  ax-ext 2733  ax-sep 5249  ax-nul 5260  ax-pow 5327  ax-pr 5391  ax-un 7751

This proof depends on definitions:  df-bi 210  df-an 402  df-or 862  df-3an 1105  df-tru 1573  df-fal 1583  df-ex 1813  df-nf 1817  df-sb 2100  df-mo 2565  df-eu 2595  df-clab 2740  df-cleq 2753  df-clel 2836  df-nfc 2910  df-ne 2957  df-ral 3078  df-rex 3088  df-rab 3414  df-v 3453  df-dif 3902  df-un 3904  df-in 3906  df-ss 3916  df-nul 4280  df-if 4483  df-pw 4559  df-sn 4585  df-pr 4587  df-op 4591  df-uni 4868  df-br 5104  df-opab 5168  df-mpt 5187  df-id 5546  df-xp 5657  df-rel 5658  df-cnv 5659  df-co 5660  df-dm 5661  df-iota 6494  df-fun 6540  df-fv 6546  df-topon 23229

This theorem is used by:  toptopon2  23236  eltpsi  23262  restuni  23480  stoig  23481  restlp  23501  restperf  23502  perfopn  23503  iscn2  23556  iscnp2  23557  cncnpi  23596  cncnp2  23599  cnnei  23600  cnrest  23603  cnpresti  23606  cnprest  23607  cnprest2  23608  paste  23612  t1sep2  23687  sshauslem  23690  1stcelcls  23780  kgenuni  23858  iskgen3  23868  txuni  23911  ptuniconst  23917  txcnmpt  23943  txcn  23945  txindis  23953  ptrescn  23958  txcmpb  23963  xkoptsub  23973  xkofvcn  24003  imasnopn  24009  imasncld  24010  imasncls  24011  qtopcmplem  24026  qtopkgen  24029  hmeof1o  24083  hmeores  24090  hmphindis  24116  cmphaushmeo  24119  txhmeo  24122  ptunhmeo  24127  hausflim  24300  flfneii  24311  hausflf  24316  flimfnfcls  24347  flfcntr  24362  cnextfun  24383  cnextfvval  24384  cnextf  24385  cnextcn  24386  cnextfres1  24387  retopon  25082  evth  25280  evth2  25281  qtophaus  34468  rrhre  34653  pconnconn  35996  connpconn  36000  pconnpi1  36002  sconnpi1  36004  txsconnlem  36005  txsconn  36006  cvmsf1o  36037  cvmliftmolem1  36046  cvmliftlem8  36057  cvmlift2lem9a  36068  cvmlift2lem9  36076  cvmlift2lem11  36078  cvmlift2lem12  36079  cvmliftphtlem  36082  cvmlift3lem6  36089  cvmlift3lem8  36091  cvmlift3lem9  36092  cnres2  38697  cnresima  38698  hausgraph  44206  ntrf2  45123  fcnre  46041