Theorem topopn 22791

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 3958	. . 3 ⊢ 𝐽 ⊆ 𝐽
3		uniopn 22782	. . 3 ⊢ ((𝐽 ∈ Top ∧ 𝐽 ⊆ 𝐽) → ∪ 𝐽 ∈ 𝐽)
4	2, 3	mpan2 691	. 2 ⊢ (𝐽 ∈ Top → ∪ 𝐽 ∈ 𝐽)
5	1, 4	eqeltrid 2832	1 ⊢ (𝐽 ∈ Top → 𝑋 ∈ 𝐽)

Syntax hints:   → wi 4   = wceq 1540   ∈ wcel 2109   ⊆ wss 3903  ∪ cuni 4858  Topctop 22778

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1795  ax-4 1809  ax-5 1910  ax-6 1967  ax-7 2008  ax-8 2111  ax-9 2119  ax-ext 2701  ax-sep 5235

This theorem depends on definitions:  df-bi 207  df-an 396  df-3an 1088  df-tru 1543  df-ex 1780  df-sb 2066  df-clab 2708  df-cleq 2721  df-clel 2803  df-ral 3045  df-rex 3054  df-rab 3395  df-v 3438  df-in 3910  df-ss 3920  df-pw 4553  df-uni 4859  df-top 22779

This theorem is referenced by:  riinopn  22793  toponmax  22811  cldval  22908  ntrfval  22909  clsfval  22910  iscld  22912  ntrval  22921  clsval  22922  0cld  22923  clsval2  22935  ntrtop  22955  toponmre  22978  neifval  22984  neif  22985  neival  22987  isnei  22988  tpnei  23006  lpfval  23023  lpval  23024  restcld  23057  restcls  23066  restntr  23067  cnrest  23170  cmpsub  23285  hauscmplem  23291  cmpfi  23293  isconn2  23299  connsubclo  23309  1stcfb  23330  1stcelcls  23346  islly2  23369  lly1stc  23381  islocfin  23402  finlocfin  23405  cmpkgen  23436  llycmpkgen  23437  ptbasid  23460  ptpjpre2  23465  ptopn2  23469  xkoopn  23474  xkouni  23484  txcld  23488  txcn  23511  ptrescn  23524  txtube  23525  txhaus  23532  xkoptsub  23539  xkopt  23540  xkopjcn  23541  qtoptop  23585  qtopuni  23587  opnfbas  23727  flimval  23848  flimfil  23854  hausflim  23866  hauspwpwf1  23872  hauspwpwdom  23873  flimfnfcls  23913  cnpfcfi  23925  bcthlem5  25226  dvply1  26189  cldssbrsiga  34154  dya2iocucvr  34252  kur14lem7  35185  kur14lem9  35187  connpconn  35208  cvmliftmolem1  35254  ordtop  36410  pibt2  37391  ntrelmap  44098  clselmap  44100  dssmapntrcls  44101  dssmapclsntr  44102  toprestsubel  45132  reopn  45271  toplatglb0  48983