Theorem topopn 22821

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

Syntax hints:   → wi 4   = wceq 1541   ∈ wcel 2111   ⊆ wss 3897  ∪ cuni 4856  Topctop 22808

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 2113  ax-9 2121  ax-ext 2703  ax-sep 5232

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 2710  df-cleq 2723  df-clel 2806  df-ral 3048  df-rex 3057  df-rab 3396  df-v 3438  df-in 3904  df-ss 3914  df-pw 4549  df-uni 4857  df-top 22809

This theorem is referenced by:  riinopn  22823  toponmax  22841  cldval  22938  ntrfval  22939  clsfval  22940  iscld  22942  ntrval  22951  clsval  22952  0cld  22953  clsval2  22965  ntrtop  22985  toponmre  23008  neifval  23014  neif  23015  neival  23017  isnei  23018  tpnei  23036  lpfval  23053  lpval  23054  restcld  23087  restcls  23096  restntr  23097  cnrest  23200  cmpsub  23315  hauscmplem  23321  cmpfi  23323  isconn2  23329  connsubclo  23339  1stcfb  23360  1stcelcls  23376  islly2  23399  lly1stc  23411  islocfin  23432  finlocfin  23435  cmpkgen  23466  llycmpkgen  23467  ptbasid  23490  ptpjpre2  23495  ptopn2  23499  xkoopn  23504  xkouni  23514  txcld  23518  txcn  23541  ptrescn  23554  txtube  23555  txhaus  23562  xkoptsub  23569  xkopt  23570  xkopjcn  23571  qtoptop  23615  qtopuni  23617  opnfbas  23757  flimval  23878  flimfil  23884  hausflim  23896  hauspwpwf1  23902  hauspwpwdom  23903  flimfnfcls  23943  cnpfcfi  23955  bcthlem5  25255  dvply1  26218  cldssbrsiga  34200  dya2iocucvr  34297  kur14lem7  35256  kur14lem9  35258  connpconn  35279  cvmliftmolem1  35325  ordtop  36478  pibt2  37459  ntrelmap  44166  clselmap  44168  dssmapntrcls  44169  dssmapclsntr  44170  toprestsubel  45199  reopn  45338  toplatglb0  49038