Theorem topopn 22844

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

Syntax hints:   → wi 4   = wceq 1540   ∈ wcel 2108   ⊆ wss 3926  ∪ cuni 4883  Topctop 22831

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 2707  ax-sep 5266

This theorem depends on definitions:  df-bi 207  df-an 396  df-3an 1088  df-tru 1543  df-ex 1780  df-sb 2065  df-clab 2714  df-cleq 2727  df-clel 2809  df-ral 3052  df-rex 3061  df-rab 3416  df-v 3461  df-in 3933  df-ss 3943  df-pw 4577  df-uni 4884  df-top 22832

This theorem is referenced by:  riinopn  22846  toponmax  22864  cldval  22961  ntrfval  22962  clsfval  22963  iscld  22965  ntrval  22974  clsval  22975  0cld  22976  clsval2  22988  ntrtop  23008  toponmre  23031  neifval  23037  neif  23038  neival  23040  isnei  23041  tpnei  23059  lpfval  23076  lpval  23077  restcld  23110  restcls  23119  restntr  23120  cnrest  23223  cmpsub  23338  hauscmplem  23344  cmpfi  23346  isconn2  23352  connsubclo  23362  1stcfb  23383  1stcelcls  23399  islly2  23422  lly1stc  23434  islocfin  23455  finlocfin  23458  cmpkgen  23489  llycmpkgen  23490  ptbasid  23513  ptpjpre2  23518  ptopn2  23522  xkoopn  23527  xkouni  23537  txcld  23541  txcn  23564  ptrescn  23577  txtube  23578  txhaus  23585  xkoptsub  23592  xkopt  23593  xkopjcn  23594  qtoptop  23638  qtopuni  23640  opnfbas  23780  flimval  23901  flimfil  23907  hausflim  23919  hauspwpwf1  23925  hauspwpwdom  23926  flimfnfcls  23966  cnpfcfi  23978  bcthlem5  25280  dvply1  26243  cldssbrsiga  34218  dya2iocucvr  34316  kur14lem7  35234  kur14lem9  35236  connpconn  35257  cvmliftmolem1  35303  ordtop  36454  pibt2  37435  ntrelmap  44149  clselmap  44151  dssmapntrcls  44152  dssmapclsntr  44153  toprestsubel  45178  reopn  45318  toplatglb0  48973