Theorem topopn 22862

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

Syntax hints:   → wi 4   = wceq 1542   ∈ wcel 2114   ⊆ wss 3903  ∪ cuni 4865  Topctop 22849

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1797  ax-4 1811  ax-5 1912  ax-6 1969  ax-7 2010  ax-8 2116  ax-9 2124  ax-ext 2709  ax-sep 5243

This theorem depends on definitions:  df-bi 207  df-an 396  df-3an 1089  df-tru 1545  df-ex 1782  df-sb 2069  df-clab 2716  df-cleq 2729  df-clel 2812  df-ral 3053  df-rex 3063  df-rab 3402  df-v 3444  df-in 3910  df-ss 3920  df-pw 4558  df-uni 4866  df-top 22850

This theorem is referenced by:  riinopn  22864  toponmax  22882  cldval  22979  ntrfval  22980  clsfval  22981  iscld  22983  ntrval  22992  clsval  22993  0cld  22994  clsval2  23006  ntrtop  23026  toponmre  23049  neifval  23055  neif  23056  neival  23058  isnei  23059  tpnei  23077  lpfval  23094  lpval  23095  restcld  23128  restcls  23137  restntr  23138  cnrest  23241  cmpsub  23356  hauscmplem  23362  cmpfi  23364  isconn2  23370  connsubclo  23380  1stcfb  23401  1stcelcls  23417  islly2  23440  lly1stc  23452  islocfin  23473  finlocfin  23476  cmpkgen  23507  llycmpkgen  23508  ptbasid  23531  ptpjpre2  23536  ptopn2  23540  xkoopn  23545  xkouni  23555  txcld  23559  txcn  23582  ptrescn  23595  txtube  23596  txhaus  23603  xkoptsub  23610  xkopt  23611  xkopjcn  23612  qtoptop  23656  qtopuni  23658  opnfbas  23798  flimval  23919  flimfil  23925  hausflim  23937  hauspwpwf1  23943  hauspwpwdom  23944  flimfnfcls  23984  cnpfcfi  23996  bcthlem5  25296  dvply1  26259  cldssbrsiga  34365  dya2iocucvr  34462  kur14lem7  35428  kur14lem9  35430  connpconn  35451  cvmliftmolem1  35497  ordtop  36652  pibt2  37672  ntrelmap  44481  clselmap  44483  dssmapntrcls  44484  dssmapclsntr  44485  toprestsubel  45513  reopn  45651  toplatglb0  49358