Theorem topopn 22852

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

Syntax hints:   → wi 4   = wceq 1533   ∈ wcel 2098   ⊆ wss 3944  ∪ cuni 4909  Topctop 22839

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1789  ax-4 1803  ax-5 1905  ax-6 1963  ax-7 2003  ax-8 2100  ax-9 2108  ax-ext 2696  ax-sep 5300

This theorem depends on definitions:  df-bi 206  df-an 395  df-3an 1086  df-tru 1536  df-ex 1774  df-sb 2060  df-clab 2703  df-cleq 2717  df-clel 2802  df-ral 3051  df-rex 3060  df-rab 3419  df-v 3463  df-in 3951  df-ss 3961  df-pw 4606  df-uni 4910  df-top 22840

This theorem is referenced by:  riinopn  22854  toponmax  22872  cldval  22971  ntrfval  22972  clsfval  22973  iscld  22975  ntrval  22984  clsval  22985  0cld  22986  clsval2  22998  ntrtop  23018  toponmre  23041  neifval  23047  neif  23048  neival  23050  isnei  23051  tpnei  23069  lpfval  23086  lpval  23087  restcld  23120  restcls  23129  restntr  23130  cnrest  23233  cmpsub  23348  hauscmplem  23354  cmpfi  23356  isconn2  23362  connsubclo  23372  1stcfb  23393  1stcelcls  23409  islly2  23432  lly1stc  23444  islocfin  23465  finlocfin  23468  cmpkgen  23499  llycmpkgen  23500  ptbasid  23523  ptpjpre2  23528  ptopn2  23532  xkoopn  23537  xkouni  23547  txcld  23551  txcn  23574  ptrescn  23587  txtube  23588  txhaus  23595  xkoptsub  23602  xkopt  23603  xkopjcn  23604  qtoptop  23648  qtopuni  23650  opnfbas  23790  flimval  23911  flimfil  23917  hausflim  23929  hauspwpwf1  23935  hauspwpwdom  23936  flimfnfcls  23976  cnpfcfi  23988  bcthlem5  25300  dvply1  26263  cldssbrsiga  33937  dya2iocucvr  34035  kur14lem7  34953  kur14lem9  34955  connpconn  34976  cvmliftmolem1  35022  ordtop  36051  pibt2  37027  ntrelmap  43697  clselmap  43699  dssmapntrcls  43700  dssmapclsntr  43701  toprestsubel  44664  reopn  44809  toplatglb0  48196