Theorem topopn 22963

Description: The underlying set of a topology is an open set. (Contributed by NM, 17-Jul-2006.)

Hypothesis

Ref	Expression
1open.1	⊢ 𝑋 = ∪ 𝐽

Assertion

Ref	Expression
topopn	⊢ (𝐽 ∈ Top → 𝑋 ∈ 𝐽)

Proof of Theorem topopn

Step	Hyp	Ref	Expression
1		1open.1	. 2 ⊢ 𝑋 = ∪ 𝐽
2		ssid 3958	. . 3 ⊢ 𝐽 ⊆ 𝐽
3		uniopn 22954	. . 3 ⊢ ((𝐽 ∈ Top ∧ 𝐽 ⊆ 𝐽) → ∪ 𝐽 ∈ 𝐽)
4	2, 3	mpan2 701	. 2 ⊢ (𝐽 ∈ Top → ∪ 𝐽 ∈ 𝐽)
5	1, 4	eqeltrid 2866	1 ⊢ (𝐽 ∈ Top → 𝑋 ∈ 𝐽)

Syntax hints:   → wi 4   = wceq 1560   ∈ wcel 2142   ⊆ wss 3904  ∪ cuni 4865  Topctop 22950

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1815  ax-4 1829  ax-5 1930  ax-6 1987  ax-7 2028  ax-8 2144  ax-9 2152  ax-ext 2734  ax-sep 5246

This theorem depends on definitions:  df-bi 209  df-an 400  df-3an 1100  df-tru 1563  df-ex 1800  df-sb 2091  df-clab 2741  df-cleq 2754  df-clel 2837  df-ral 3077  df-rex 3087  df-rab 3415  df-v 3456  df-in 3911  df-ss 3921  df-pw 4557  df-uni 4866  df-top 22951

This theorem is referenced by:  riinopn  22965  toponmax  22983  cldval  23080  ntrfval  23081  clsfval  23082  iscld  23084  ntrval  23093  clsval  23094  0cld  23095  clsval2  23107  ntrtop  23127  toponmre  23150  neifval  23156  neif  23157  neival  23159  isnei  23160  tpnei  23178  lpfval  23195  lpval  23196  restcld  23229  restcls  23238  restntr  23239  cnrest  23342  cmpsub  23457  hauscmplem  23463  cmpfi  23465  isconn2  23471  connsubclo  23481  1stcfb  23502  1stcelcls  23518  islly2  23541  lly1stc  23553  islocfin  23574  finlocfin  23577  cmpkgen  23608  llycmpkgen  23609  ptbasid  23632  ptpjpre2  23637  ptopn2  23641  xkoopn  23646  xkouni  23656  txcld  23660  txcn  23683  ptrescn  23696  txtube  23697  txhaus  23704  xkoptsub  23711  xkopt  23712  xkopjcn  23713  qtoptop  23757  qtopuni  23759  opnfbas  23899  flimval  24020  flimfil  24026  hausflim  24038  hauspwpwf1  24044  hauspwpwdom  24045  flimfnfcls  24085  cnpfcfi  24097  bcthlem5  25387  dvply1  26345  cldssbrsiga  34481  dya2iocucvr  34578  kur14lem7  35559  kur14lem9  35561  connpconn  35582  cvmliftmolem1  35628  ordtop  36793  pibt2  37908  ntrelmap  44698  clselmap  44700  dssmapntrcls  44701  dssmapclsntr  44702  toprestsubel  45729  reopn  45865  toplatglb0  49617