Theorem topopn 22051

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

Syntax hints:   → wi 4   = wceq 1542   ∈ wcel 2110   ⊆ wss 3892  ∪ cuni 4845  Topctop 22038

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1802  ax-4 1816  ax-5 1917  ax-6 1975  ax-7 2015  ax-8 2112  ax-9 2120  ax-ext 2711  ax-sep 5227

This theorem depends on definitions:  df-bi 206  df-an 397  df-tru 1545  df-ex 1787  df-sb 2072  df-clab 2718  df-cleq 2732  df-clel 2818  df-ral 3071  df-rab 3075  df-v 3433  df-in 3899  df-ss 3909  df-pw 4541  df-uni 4846  df-top 22039

This theorem is referenced by:  riinopn  22053  toponmax  22071  cldval  22170  ntrfval  22171  clsfval  22172  iscld  22174  ntrval  22183  clsval  22184  0cld  22185  clsval2  22197  ntrtop  22217  toponmre  22240  neifval  22246  neif  22247  neival  22249  isnei  22250  tpnei  22268  lpfval  22285  lpval  22286  restcld  22319  restcls  22328  restntr  22329  cnrest  22432  cmpsub  22547  hauscmplem  22553  cmpfi  22555  isconn2  22561  connsubclo  22571  1stcfb  22592  1stcelcls  22608  islly2  22631  lly1stc  22643  islocfin  22664  finlocfin  22667  cmpkgen  22698  llycmpkgen  22699  ptbasid  22722  ptpjpre2  22727  ptopn2  22731  xkoopn  22736  xkouni  22746  txcld  22750  txcn  22773  ptrescn  22786  txtube  22787  txhaus  22794  xkoptsub  22801  xkopt  22802  xkopjcn  22803  qtoptop  22847  qtopuni  22849  opnfbas  22989  flimval  23110  flimfil  23116  hausflim  23128  hauspwpwf1  23134  hauspwpwdom  23135  flimfnfcls  23175  cnpfcfi  23187  bcthlem5  24488  dvply1  25440  cldssbrsiga  32149  dya2iocucvr  32245  kur14lem7  33168  kur14lem9  33170  connpconn  33191  cvmliftmolem1  33237  ordtop  34619  pibt2  35582  ntrelmap  41703  clselmap  41705  dssmapntrcls  41706  dssmapclsntr  41707  reopn  42796  toplatglb0  46252