Theorem topopn 21514

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

Syntax hints:   → wi 4   = wceq 1537   ∈ wcel 2114   ⊆ wss 3936  ∪ cuni 4838  Topctop 21501

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1796  ax-4 1810  ax-5 1911  ax-6 1970  ax-7 2015  ax-8 2116  ax-9 2124  ax-10 2145  ax-11 2161  ax-12 2177  ax-ext 2793  ax-sep 5203

This theorem depends on definitions:  df-bi 209  df-an 399  df-or 844  df-tru 1540  df-ex 1781  df-nf 1785  df-sb 2070  df-clab 2800  df-cleq 2814  df-clel 2893  df-nfc 2963  df-ral 3143  df-rab 3147  df-v 3496  df-in 3943  df-ss 3952  df-pw 4541  df-uni 4839  df-top 21502

This theorem is referenced by:  riinopn  21516  toponmax  21534  cldval  21631  ntrfval  21632  clsfval  21633  iscld  21635  ntrval  21644  clsval  21645  0cld  21646  clsval2  21658  ntrtop  21678  toponmre  21701  neifval  21707  neif  21708  neival  21710  isnei  21711  tpnei  21729  lpfval  21746  lpval  21747  restcld  21780  restcls  21789  restntr  21790  cnrest  21893  cmpsub  22008  hauscmplem  22014  cmpfi  22016  isconn2  22022  connsubclo  22032  1stcfb  22053  1stcelcls  22069  islly2  22092  lly1stc  22104  islocfin  22125  finlocfin  22128  cmpkgen  22159  llycmpkgen  22160  ptbasid  22183  ptpjpre2  22188  ptopn2  22192  xkoopn  22197  xkouni  22207  txcld  22211  txcn  22234  ptrescn  22247  txtube  22248  txhaus  22255  xkoptsub  22262  xkopt  22263  xkopjcn  22264  qtoptop  22308  qtopuni  22310  opnfbas  22450  flimval  22571  flimfil  22577  hausflim  22589  hauspwpwf1  22595  hauspwpwdom  22596  flimfnfcls  22636  cnpfcfi  22648  bcthlem5  23931  dvply1  24873  cldssbrsiga  31446  dya2iocucvr  31542  kur14lem7  32459  kur14lem9  32461  connpconn  32482  cvmliftmolem1  32528  ordtop  33784  pibt2  34701  ntrelmap  40495  clselmap  40497  dssmapntrcls  40498  dssmapclsntr  40499  reopn  41575