Theorem topopn 22912

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

Syntax hints:   → wi 4   = wceq 1540   ∈ wcel 2108   ⊆ wss 3951  ∪ cuni 4907  Topctop 22899

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 2007  ax-8 2110  ax-9 2118  ax-ext 2708  ax-sep 5296

This theorem depends on definitions:  df-bi 207  df-an 396  df-3an 1089  df-tru 1543  df-ex 1780  df-sb 2065  df-clab 2715  df-cleq 2729  df-clel 2816  df-ral 3062  df-rex 3071  df-rab 3437  df-v 3482  df-in 3958  df-ss 3968  df-pw 4602  df-uni 4908  df-top 22900

This theorem is referenced by:  riinopn  22914  toponmax  22932  cldval  23031  ntrfval  23032  clsfval  23033  iscld  23035  ntrval  23044  clsval  23045  0cld  23046  clsval2  23058  ntrtop  23078  toponmre  23101  neifval  23107  neif  23108  neival  23110  isnei  23111  tpnei  23129  lpfval  23146  lpval  23147  restcld  23180  restcls  23189  restntr  23190  cnrest  23293  cmpsub  23408  hauscmplem  23414  cmpfi  23416  isconn2  23422  connsubclo  23432  1stcfb  23453  1stcelcls  23469  islly2  23492  lly1stc  23504  islocfin  23525  finlocfin  23528  cmpkgen  23559  llycmpkgen  23560  ptbasid  23583  ptpjpre2  23588  ptopn2  23592  xkoopn  23597  xkouni  23607  txcld  23611  txcn  23634  ptrescn  23647  txtube  23648  txhaus  23655  xkoptsub  23662  xkopt  23663  xkopjcn  23664  qtoptop  23708  qtopuni  23710  opnfbas  23850  flimval  23971  flimfil  23977  hausflim  23989  hauspwpwf1  23995  hauspwpwdom  23996  flimfnfcls  24036  cnpfcfi  24048  bcthlem5  25362  dvply1  26325  cldssbrsiga  34188  dya2iocucvr  34286  kur14lem7  35217  kur14lem9  35219  connpconn  35240  cvmliftmolem1  35286  ordtop  36437  pibt2  37418  ntrelmap  44138  clselmap  44140  dssmapntrcls  44141  dssmapclsntr  44142  toprestsubel  45159  reopn  45301  toplatglb0  48888