Theorem topopn 22848

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

Syntax hints:   → wi 4   = wceq 1541   ∈ wcel 2113   ⊆ wss 3899  ∪ cuni 4861  Topctop 22835

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1796  ax-4 1810  ax-5 1911  ax-6 1968  ax-7 2009  ax-8 2115  ax-9 2123  ax-ext 2706  ax-sep 5239

This theorem depends on definitions:  df-bi 207  df-an 396  df-3an 1088  df-tru 1544  df-ex 1781  df-sb 2068  df-clab 2713  df-cleq 2726  df-clel 2809  df-ral 3050  df-rex 3059  df-rab 3398  df-v 3440  df-in 3906  df-ss 3916  df-pw 4554  df-uni 4862  df-top 22836

This theorem is referenced by:  riinopn  22850  toponmax  22868  cldval  22965  ntrfval  22966  clsfval  22967  iscld  22969  ntrval  22978  clsval  22979  0cld  22980  clsval2  22992  ntrtop  23012  toponmre  23035  neifval  23041  neif  23042  neival  23044  isnei  23045  tpnei  23063  lpfval  23080  lpval  23081  restcld  23114  restcls  23123  restntr  23124  cnrest  23227  cmpsub  23342  hauscmplem  23348  cmpfi  23350  isconn2  23356  connsubclo  23366  1stcfb  23387  1stcelcls  23403  islly2  23426  lly1stc  23438  islocfin  23459  finlocfin  23462  cmpkgen  23493  llycmpkgen  23494  ptbasid  23517  ptpjpre2  23522  ptopn2  23526  xkoopn  23531  xkouni  23541  txcld  23545  txcn  23568  ptrescn  23581  txtube  23582  txhaus  23589  xkoptsub  23596  xkopt  23597  xkopjcn  23598  qtoptop  23642  qtopuni  23644  opnfbas  23784  flimval  23905  flimfil  23911  hausflim  23923  hauspwpwf1  23929  hauspwpwdom  23930  flimfnfcls  23970  cnpfcfi  23982  bcthlem5  25282  dvply1  26245  cldssbrsiga  34293  dya2iocucvr  34390  kur14lem7  35355  kur14lem9  35357  connpconn  35378  cvmliftmolem1  35424  ordtop  36579  pibt2  37561  ntrelmap  44308  clselmap  44310  dssmapntrcls  44311  dssmapclsntr  44312  toprestsubel  45340  reopn  45479  toplatglb0  49186