Theorem topopn 22399

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 4003	. . 3 ⊢ 𝐽 ⊆ 𝐽
3		uniopn 22390	. . 3 ⊢ ((𝐽 ∈ Top ∧ 𝐽 ⊆ 𝐽) → ∪ 𝐽 ∈ 𝐽)
4	2, 3	mpan2 689	. 2 ⊢ (𝐽 ∈ Top → ∪ 𝐽 ∈ 𝐽)
5	1, 4	eqeltrid 2837	1 ⊢ (𝐽 ∈ Top → 𝑋 ∈ 𝐽)

Syntax hints:   → wi 4   = wceq 1541   ∈ wcel 2106   ⊆ wss 3947  ∪ cuni 4907  Topctop 22386

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1797  ax-4 1811  ax-5 1913  ax-6 1971  ax-7 2011  ax-8 2108  ax-9 2116  ax-ext 2703  ax-sep 5298

This theorem depends on definitions:  df-bi 206  df-an 397  df-tru 1544  df-ex 1782  df-sb 2068  df-clab 2710  df-cleq 2724  df-clel 2810  df-ral 3062  df-rex 3071  df-rab 3433  df-v 3476  df-in 3954  df-ss 3964  df-pw 4603  df-uni 4908  df-top 22387

This theorem is referenced by:  riinopn  22401  toponmax  22419  cldval  22518  ntrfval  22519  clsfval  22520  iscld  22522  ntrval  22531  clsval  22532  0cld  22533  clsval2  22545  ntrtop  22565  toponmre  22588  neifval  22594  neif  22595  neival  22597  isnei  22598  tpnei  22616  lpfval  22633  lpval  22634  restcld  22667  restcls  22676  restntr  22677  cnrest  22780  cmpsub  22895  hauscmplem  22901  cmpfi  22903  isconn2  22909  connsubclo  22919  1stcfb  22940  1stcelcls  22956  islly2  22979  lly1stc  22991  islocfin  23012  finlocfin  23015  cmpkgen  23046  llycmpkgen  23047  ptbasid  23070  ptpjpre2  23075  ptopn2  23079  xkoopn  23084  xkouni  23094  txcld  23098  txcn  23121  ptrescn  23134  txtube  23135  txhaus  23142  xkoptsub  23149  xkopt  23150  xkopjcn  23151  qtoptop  23195  qtopuni  23197  opnfbas  23337  flimval  23458  flimfil  23464  hausflim  23476  hauspwpwf1  23482  hauspwpwdom  23483  flimfnfcls  23523  cnpfcfi  23535  bcthlem5  24836  dvply1  25788  cldssbrsiga  33173  dya2iocucvr  33271  kur14lem7  34191  kur14lem9  34193  connpconn  34214  cvmliftmolem1  34260  ordtop  35309  pibt2  36286  ntrelmap  42861  clselmap  42863  dssmapntrcls  42864  dssmapclsntr  42865  toprestsubel  43833  reopn  43985  toplatglb0  47577