Theorem topopn 22793

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 3969	. . 3 ⊢ 𝐽 ⊆ 𝐽
3		uniopn 22784	. . 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 3914  ∪ cuni 4871  Topctop 22780

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 5251

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 3406  df-v 3449  df-in 3921  df-ss 3931  df-pw 4565  df-uni 4872  df-top 22781

This theorem is referenced by:  riinopn  22795  toponmax  22813  cldval  22910  ntrfval  22911  clsfval  22912  iscld  22914  ntrval  22923  clsval  22924  0cld  22925  clsval2  22937  ntrtop  22957  toponmre  22980  neifval  22986  neif  22987  neival  22989  isnei  22990  tpnei  23008  lpfval  23025  lpval  23026  restcld  23059  restcls  23068  restntr  23069  cnrest  23172  cmpsub  23287  hauscmplem  23293  cmpfi  23295  isconn2  23301  connsubclo  23311  1stcfb  23332  1stcelcls  23348  islly2  23371  lly1stc  23383  islocfin  23404  finlocfin  23407  cmpkgen  23438  llycmpkgen  23439  ptbasid  23462  ptpjpre2  23467  ptopn2  23471  xkoopn  23476  xkouni  23486  txcld  23490  txcn  23513  ptrescn  23526  txtube  23527  txhaus  23534  xkoptsub  23541  xkopt  23542  xkopjcn  23543  qtoptop  23587  qtopuni  23589  opnfbas  23729  flimval  23850  flimfil  23856  hausflim  23868  hauspwpwf1  23874  hauspwpwdom  23875  flimfnfcls  23915  cnpfcfi  23927  bcthlem5  25228  dvply1  26191  cldssbrsiga  34177  dya2iocucvr  34275  kur14lem7  35199  kur14lem9  35201  connpconn  35222  cvmliftmolem1  35268  ordtop  36424  pibt2  37405  ntrelmap  44114  clselmap  44116  dssmapntrcls  44117  dssmapclsntr  44118  toprestsubel  45148  reopn  45287  toplatglb0  48987