Theorem topopn 22889

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 22880	. . 3 ⊢ ((𝐽 ∈ Top ∧ 𝐽 ⊆ 𝐽) → ∪ 𝐽 ∈ 𝐽)
4	2, 3	mpan2 697	. 2 ⊢ (𝐽 ∈ Top → ∪ 𝐽 ∈ 𝐽)
5	1, 4	eqeltrid 2843	1 ⊢ (𝐽 ∈ Top → 𝑋 ∈ 𝐽)

Syntax hints:   → wi 4   = wceq 1547   ∈ wcel 2119   ⊆ wss 3883  ∪ cuni 4838  Topctop 22876

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 1974  ax-7 2015  ax-8 2121  ax-9 2129  ax-ext 2711  ax-sep 5218

This theorem depends on definitions:  df-bi 208  df-an 397  df-3an 1094  df-tru 1550  df-ex 1787  df-sb 2074  df-clab 2718  df-cleq 2731  df-clel 2814  df-ral 3054  df-rex 3064  df-rab 3392  df-v 3433  df-in 3890  df-ss 3900  df-pw 4531  df-uni 4839  df-top 22877

This theorem is referenced by:  riinopn  22891  toponmax  22909  cldval  23006  ntrfval  23007  clsfval  23008  iscld  23010  ntrval  23019  clsval  23020  0cld  23021  clsval2  23033  ntrtop  23053  toponmre  23076  neifval  23082  neif  23083  neival  23085  isnei  23086  tpnei  23104  lpfval  23121  lpval  23122  restcld  23155  restcls  23164  restntr  23165  cnrest  23268  cmpsub  23383  hauscmplem  23389  cmpfi  23391  isconn2  23397  connsubclo  23407  1stcfb  23428  1stcelcls  23444  islly2  23467  lly1stc  23479  islocfin  23500  finlocfin  23503  cmpkgen  23534  llycmpkgen  23535  ptbasid  23558  ptpjpre2  23563  ptopn2  23567  xkoopn  23572  xkouni  23582  txcld  23586  txcn  23609  ptrescn  23622  txtube  23623  txhaus  23630  xkoptsub  23637  xkopt  23638  xkopjcn  23639  qtoptop  23683  qtopuni  23685  opnfbas  23825  flimval  23946  flimfil  23952  hausflim  23964  hauspwpwf1  23970  hauspwpwdom  23971  flimfnfcls  24011  cnpfcfi  24023  bcthlem5  25313  dvply1  26268  cldssbrsiga  34371  dya2iocucvr  34468  kur14lem7  35440  kur14lem9  35442  connpconn  35463  cvmliftmolem1  35509  ordtop  36664  pibt2  37779  ntrelmap  44569  clselmap  44571  dssmapntrcls  44572  dssmapclsntr  44573  toprestsubel  45601  reopn  45737  toplatglb0  49489