Theorem topopn 22769

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 3966	. . 3 ⊢ 𝐽 ⊆ 𝐽
3		uniopn 22760	. . 3 ⊢ ((𝐽 ∈ Top ∧ 𝐽 ⊆ 𝐽) → ∪ 𝐽 ∈ 𝐽)
4	2, 3	mpan2 691	. 2 ⊢ (𝐽 ∈ Top → ∪ 𝐽 ∈ 𝐽)
5	1, 4	eqeltrid 2832	1 ⊢ (𝐽 ∈ Top → 𝑋 ∈ 𝐽)

Syntax hints:   → wi 4   = wceq 1540   ∈ wcel 2109   ⊆ wss 3911  ∪ cuni 4867  Topctop 22756

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-ext 2701  ax-sep 5246

This theorem depends on definitions:  df-bi 207  df-an 396  df-3an 1088  df-tru 1543  df-ex 1780  df-sb 2066  df-clab 2708  df-cleq 2721  df-clel 2803  df-ral 3045  df-rex 3054  df-rab 3403  df-v 3446  df-in 3918  df-ss 3928  df-pw 4561  df-uni 4868  df-top 22757

This theorem is referenced by:  riinopn  22771  toponmax  22789  cldval  22886  ntrfval  22887  clsfval  22888  iscld  22890  ntrval  22899  clsval  22900  0cld  22901  clsval2  22913  ntrtop  22933  toponmre  22956  neifval  22962  neif  22963  neival  22965  isnei  22966  tpnei  22984  lpfval  23001  lpval  23002  restcld  23035  restcls  23044  restntr  23045  cnrest  23148  cmpsub  23263  hauscmplem  23269  cmpfi  23271  isconn2  23277  connsubclo  23287  1stcfb  23308  1stcelcls  23324  islly2  23347  lly1stc  23359  islocfin  23380  finlocfin  23383  cmpkgen  23414  llycmpkgen  23415  ptbasid  23438  ptpjpre2  23443  ptopn2  23447  xkoopn  23452  xkouni  23462  txcld  23466  txcn  23489  ptrescn  23502  txtube  23503  txhaus  23510  xkoptsub  23517  xkopt  23518  xkopjcn  23519  qtoptop  23563  qtopuni  23565  opnfbas  23705  flimval  23826  flimfil  23832  hausflim  23844  hauspwpwf1  23850  hauspwpwdom  23851  flimfnfcls  23891  cnpfcfi  23903  bcthlem5  25204  dvply1  26167  cldssbrsiga  34150  dya2iocucvr  34248  kur14lem7  35172  kur14lem9  35174  connpconn  35195  cvmliftmolem1  35241  ordtop  36397  pibt2  37378  ntrelmap  44087  clselmap  44089  dssmapntrcls  44090  dssmapclsntr  44091  toprestsubel  45121  reopn  45260  toplatglb0  48960