Theorem topopn 21511

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 3937	. . 3 ⊢ 𝐽 ⊆ 𝐽
3		uniopn 21502	. . 3 ⊢ ((𝐽 ∈ Top ∧ 𝐽 ⊆ 𝐽) → ∪ 𝐽 ∈ 𝐽)
4	2, 3	mpan2 690	. 2 ⊢ (𝐽 ∈ Top → ∪ 𝐽 ∈ 𝐽)
5	1, 4	eqeltrid 2894	1 ⊢ (𝐽 ∈ Top → 𝑋 ∈ 𝐽)

Syntax hints:   → wi 4   = wceq 1538   ∈ wcel 2111   ⊆ wss 3881  ∪ cuni 4800  Topctop 21498

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 1911  ax-6 1970  ax-7 2015  ax-8 2113  ax-9 2121  ax-10 2142  ax-11 2158  ax-12 2175  ax-ext 2770  ax-sep 5167

This theorem depends on definitions:  df-bi 210  df-an 400  df-or 845  df-tru 1541  df-ex 1782  df-nf 1786  df-sb 2070  df-clab 2777  df-cleq 2791  df-clel 2870  df-nfc 2938  df-ral 3111  df-rab 3115  df-v 3443  df-in 3888  df-ss 3898  df-pw 4499  df-uni 4801  df-top 21499

This theorem is referenced by:  riinopn  21513  toponmax  21531  cldval  21628  ntrfval  21629  clsfval  21630  iscld  21632  ntrval  21641  clsval  21642  0cld  21643  clsval2  21655  ntrtop  21675  toponmre  21698  neifval  21704  neif  21705  neival  21707  isnei  21708  tpnei  21726  lpfval  21743  lpval  21744  restcld  21777  restcls  21786  restntr  21787  cnrest  21890  cmpsub  22005  hauscmplem  22011  cmpfi  22013  isconn2  22019  connsubclo  22029  1stcfb  22050  1stcelcls  22066  islly2  22089  lly1stc  22101  islocfin  22122  finlocfin  22125  cmpkgen  22156  llycmpkgen  22157  ptbasid  22180  ptpjpre2  22185  ptopn2  22189  xkoopn  22194  xkouni  22204  txcld  22208  txcn  22231  ptrescn  22244  txtube  22245  txhaus  22252  xkoptsub  22259  xkopt  22260  xkopjcn  22261  qtoptop  22305  qtopuni  22307  opnfbas  22447  flimval  22568  flimfil  22574  hausflim  22586  hauspwpwf1  22592  hauspwpwdom  22593  flimfnfcls  22633  cnpfcfi  22645  bcthlem5  23932  dvply1  24880  cldssbrsiga  31556  dya2iocucvr  31652  kur14lem7  32572  kur14lem9  32574  connpconn  32595  cvmliftmolem1  32641  ordtop  33897  pibt2  34834  ntrelmap  40828  clselmap  40830  dssmapntrcls  40831  dssmapclsntr  40832  reopn  41920