Theorem toptopon 23143

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 23138	. . 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 6533  Topctop 23119  TopOnctopon 23136

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 2732  ax-sep 5251  ax-nul 5263  ax-pow 5330  ax-pr 5398  ax-un 7737

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 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-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 5550  df-xp 5661  df-rel 5662  df-cnv 5663  df-co 5664  df-dm 5665  df-iota 6489  df-fun 6535  df-fv 6541  df-topon 23137

This theorem is used by:  toptopon2  23144  eltpsi  23170  restuni  23388  stoig  23389  restlp  23409  restperf  23410  perfopn  23411  iscn2  23464  iscnp2  23465  cncnpi  23504  cncnp2  23507  cnnei  23508  cnrest  23511  cnpresti  23514  cnprest  23515  cnprest2  23516  paste  23520  t1sep2  23595  sshauslem  23598  1stcelcls  23688  kgenuni  23766  iskgen3  23776  txuni  23819  ptuniconst  23825  txcnmpt  23851  txcn  23853  txindis  23861  ptrescn  23866  txcmpb  23871  xkoptsub  23881  xkofvcn  23911  imasnopn  23917  imasncld  23918  imasncls  23919  qtopcmplem  23934  qtopkgen  23937  hmeof1o  23991  hmeores  23998  hmphindis  24024  cmphaushmeo  24027  txhmeo  24030  ptunhmeo  24035  hausflim  24208  flfneii  24219  hausflf  24224  flimfnfcls  24255  flfcntr  24270  cnextfun  24291  cnextfvval  24292  cnextf  24293  cnextcn  24294  cnextfres1  24295  retopon  24990  evth  25188  evth2  25189  qtophaus  34347  rrhre  34532  pconnconn  35811  connpconn  35815  pconnpi1  35817  sconnpi1  35819  txsconnlem  35820  txsconn  35821  cvmsf1o  35852  cvmliftmolem1  35861  cvmliftlem8  35872  cvmlift2lem9a  35883  cvmlift2lem9  35891  cvmlift2lem11  35893  cvmlift2lem12  35894  cvmliftphtlem  35897  cvmlift3lem6  35904  cvmlift3lem8  35906  cvmlift3lem9  35907  cnres2  38514  cnresima  38515  hausgraph  44047  ntrf2  44965  fcnre  45860