Theorem topopn 22064

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 3944	. . 3 ⊢ 𝐽 ⊆ 𝐽
3		uniopn 22055	. . 3 ⊢ ((𝐽 ∈ Top ∧ 𝐽 ⊆ 𝐽) → ∪ 𝐽 ∈ 𝐽)
4	2, 3	mpan2 688	. 2 ⊢ (𝐽 ∈ Top → ∪ 𝐽 ∈ 𝐽)
5	1, 4	eqeltrid 2844	1 ⊢ (𝐽 ∈ Top → 𝑋 ∈ 𝐽)

Syntax hints:   → wi 4   = wceq 1539   ∈ wcel 2107   ⊆ wss 3888  ∪ cuni 4840  Topctop 22051

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1798  ax-4 1812  ax-5 1914  ax-6 1972  ax-7 2012  ax-8 2109  ax-9 2117  ax-ext 2710  ax-sep 5224

This theorem depends on definitions:  df-bi 206  df-an 397  df-tru 1542  df-ex 1783  df-sb 2069  df-clab 2717  df-cleq 2731  df-clel 2817  df-ral 3070  df-rab 3074  df-v 3435  df-in 3895  df-ss 3905  df-pw 4536  df-uni 4841  df-top 22052

This theorem is referenced by:  riinopn  22066  toponmax  22084  cldval  22183  ntrfval  22184  clsfval  22185  iscld  22187  ntrval  22196  clsval  22197  0cld  22198  clsval2  22210  ntrtop  22230  toponmre  22253  neifval  22259  neif  22260  neival  22262  isnei  22263  tpnei  22281  lpfval  22298  lpval  22299  restcld  22332  restcls  22341  restntr  22342  cnrest  22445  cmpsub  22560  hauscmplem  22566  cmpfi  22568  isconn2  22574  connsubclo  22584  1stcfb  22605  1stcelcls  22621  islly2  22644  lly1stc  22656  islocfin  22677  finlocfin  22680  cmpkgen  22711  llycmpkgen  22712  ptbasid  22735  ptpjpre2  22740  ptopn2  22744  xkoopn  22749  xkouni  22759  txcld  22763  txcn  22786  ptrescn  22799  txtube  22800  txhaus  22807  xkoptsub  22814  xkopt  22815  xkopjcn  22816  qtoptop  22860  qtopuni  22862  opnfbas  23002  flimval  23123  flimfil  23129  hausflim  23141  hauspwpwf1  23147  hauspwpwdom  23148  flimfnfcls  23188  cnpfcfi  23200  bcthlem5  24501  dvply1  25453  cldssbrsiga  32164  dya2iocucvr  32260  kur14lem7  33183  kur14lem9  33185  connpconn  33206  cvmliftmolem1  33252  ordtop  34634  pibt2  35597  ntrelmap  41742  clselmap  41744  dssmapntrcls  41745  dssmapclsntr  41746  reopn  42835  toplatglb0  46296