Theorem topopn 23031

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 3967	. . 3 ⊢ 𝐽 ⊆ 𝐽
3		uniopn 23022	. . 3 ⊢ ((𝐽 ∈ Top ∧ 𝐽 ⊆ 𝐽) → ∪ 𝐽 ∈ 𝐽)
4	2, 3	mpan2 703	. 2 ⊢ (𝐽 ∈ Top → ∪ 𝐽 ∈ 𝐽)
5	1, 4	eqeltrid 2873	1 ⊢ (𝐽 ∈ Top → 𝑋 ∈ 𝐽)

Syntax hints:   → wi 4   = wceq 1567   ∈ wcel 2149   ⊆ wss 3913  ∪ cuni 4876  Topctop 23018

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1822  ax-4 1836  ax-5 1937  ax-6 1994  ax-7 2035  ax-8 2151  ax-9 2159  ax-ext 2741  ax-sep 5261

This theorem depends on definitions:  df-bi 210  df-an 401  df-3an 1103  df-tru 1570  df-ex 1807  df-sb 2098  df-clab 2748  df-cleq 2761  df-clel 2844  df-ral 3086  df-rex 3096  df-rab 3424  df-v 3465  df-in 3920  df-ss 3930  df-pw 4569  df-uni 4877  df-top 23019

This theorem is referenced by:  riinopn  23033  toponmax  23051  cldval  23148  ntrfval  23149  clsfval  23150  iscld  23152  ntrval  23161  clsval  23162  0cld  23163  clsval2  23175  ntrtop  23195  toponmre  23218  neifval  23224  neif  23225  neival  23227  isnei  23228  tpnei  23246  lpfval  23263  lpval  23264  restcld  23297  restcls  23306  restntr  23307  cnrest  23410  cmpsub  23525  hauscmplem  23531  cmpfi  23533  isconn2  23539  connsubclo  23549  1stcfb  23570  1stcelcls  23586  islly2  23609  lly1stc  23621  islocfin  23642  finlocfin  23645  cmpkgen  23676  llycmpkgen  23677  ptbasid  23700  ptpjpre2  23705  ptopn2  23709  xkoopn  23714  xkouni  23724  txcld  23728  txcn  23751  ptrescn  23764  txtube  23765  txhaus  23772  xkoptsub  23779  xkopt  23780  xkopjcn  23781  qtoptop  23825  qtopuni  23827  opnfbas  23967  flimval  24088  flimfil  24094  hausflim  24106  hauspwpwf1  24112  hauspwpwdom  24113  flimfnfcls  24153  cnpfcfi  24165  bcthlem5  25455  dvply1  26413  cldssbrsiga  34521  dya2iocucvr  34618  kur14lem7  35602  kur14lem9  35604  connpconn  35625  cvmliftmolem1  35671  ordtop  36835  pibt2  37950  ntrelmap  44742  clselmap  44744  dssmapntrcls  44745  dssmapclsntr  44746  toprestsubel  45763  reopn  45899  toplatglb0  49661