Theorem topopn 21118

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 3841	. . 3 ⊢ 𝐽 ⊆ 𝐽
3		uniopn 21109	. . 3 ⊢ ((𝐽 ∈ Top ∧ 𝐽 ⊆ 𝐽) → ∪ 𝐽 ∈ 𝐽)
4	2, 3	mpan2 681	. 2 ⊢ (𝐽 ∈ Top → ∪ 𝐽 ∈ 𝐽)
5	1, 4	syl5eqel 2862	1 ⊢ (𝐽 ∈ Top → 𝑋 ∈ 𝐽)

Syntax hints:   → wi 4   = wceq 1601   ∈ wcel 2106   ⊆ wss 3791  ∪ cuni 4671  Topctop 21105

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1839  ax-4 1853  ax-5 1953  ax-6 2021  ax-7 2054  ax-9 2115  ax-10 2134  ax-11 2149  ax-12 2162  ax-ext 2753  ax-sep 5017

This theorem depends on definitions:  df-bi 199  df-an 387  df-or 837  df-tru 1605  df-ex 1824  df-nf 1828  df-sb 2012  df-clab 2763  df-cleq 2769  df-clel 2773  df-nfc 2920  df-ral 3094  df-rex 3095  df-v 3399  df-in 3798  df-ss 3805  df-pw 4380  df-uni 4672  df-top 21106

This theorem is referenced by:  riinopn  21120  toponmax  21138  cldval  21235  ntrfval  21236  clsfval  21237  iscld  21239  ntrval  21248  clsval  21249  0cld  21250  clsval2  21262  ntrtop  21282  toponmre  21305  neifval  21311  neif  21312  neival  21314  isnei  21315  tpnei  21333  lpfval  21350  lpval  21351  restcld  21384  restcls  21393  restntr  21394  cnrest  21497  cmpsub  21612  hauscmplem  21618  cmpfi  21620  isconn2  21626  connsubclo  21636  1stcfb  21657  1stcelcls  21673  islly2  21696  lly1stc  21708  islocfin  21729  finlocfin  21732  cmpkgen  21763  llycmpkgen  21764  ptbasid  21787  ptpjpre2  21792  ptopn2  21796  xkoopn  21801  xkouni  21811  txcld  21815  txcn  21838  ptrescn  21851  txtube  21852  txhaus  21859  xkoptsub  21866  xkopt  21867  xkopjcn  21868  qtoptop  21912  qtopuni  21914  opnfbas  22054  flimval  22175  flimfil  22181  hausflim  22193  hauspwpwf1  22199  hauspwpwdom  22200  flimfnfcls  22240  cnpfcfi  22252  bcthlem5  23534  dvply1  24476  cldssbrsiga  30848  dya2iocucvr  30944  kur14lem7  31793  kur14lem9  31795  connpconn  31816  cvmliftmolem1  31862  ordtop  33018  ntrelmap  39361  clselmap  39363  dssmapntrcls  39364  dssmapclsntr  39365  reopn  40393