Theorem topopn 23233

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 3931	. . 3 ⊢ 𝐽 ⊆ 𝐽
3		uniopn 23224	. . 3 ⊢ ((𝐽 ∈ Top ∧ 𝐽 ⊆ 𝐽) → ∪ 𝐽 ∈ 𝐽)
4	2, 3	mpan2 704	. 2 ⊢ (𝐽 ∈ Top → ∪ 𝐽 ∈ 𝐽)
5	1, 4	eqeltrid 2864	1 ⊢ (𝐽 ∈ Top → 𝑋 ∈ 𝐽)

This proof depends on syntax axioms:   → wi 4   = wceq 1569   ∈ wcel 2144   ⊆ wss 3896  ∪ cuni 4866  Topctop 23220

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1827  ax-4 1841  ax-5 1942  ax-6 1999  ax-7 2040  ax-8 2146  ax-9 2154  ax-ext 2732  ax-sep 5248

This proof depends on definitions:  df-bi 210  df-an 402  df-3an 1105  df-tru 1572  df-ex 1812  df-sb 2099  df-clab 2739  df-cleq 2752  df-clel 2835  df-ral 3077  df-rex 3087  df-rab 3413  df-v 3452  df-ss 3897  df-in 4090  df-pw 4558  df-uni 4867  df-top 23221

This theorem is used by:  riinopn  23235  toponmax  23253  cldval  23350  ntrfval  23351  clsfval  23352  iscld  23354  ntrval  23363  clsval  23364  0cld  23365  clsval2  23377  ntrtop  23397  toponmre  23420  neifval  23426  neif  23427  neival  23429  isnei  23430  tpnei  23448  lpfval  23465  lpval  23466  restcld  23499  restcls  23508  restntr  23509  cnrest  23612  cmpsub  23727  hauscmplem  23733  cmpfi  23735  isconn2  23741  connsubclo  23751  1stcfb  23772  1stcelcls  23789  islly2  23812  lly1stc  23824  islocfin  23845  finlocfin  23848  cmpkgen  23879  llycmpkgen  23880  ptbasid  23903  ptpjpre2  23908  ptopn2  23912  xkoopn  23917  xkouni  23927  txcld  23931  txcn  23954  ptrescn  23967  txtube  23968  txhaus  23975  xkoptsub  23982  xkopt  23983  xkopjcn  23984  qtoptop  24028  qtopuni  24030  opnfbas  24170  flimval  24291  flimfil  24297  hausflim  24309  hauspwpwf1  24315  hauspwpwdom  24316  flimfnfcls  24356  cnpfcfi  24368  bcthlem5  25658  dvply1  26614  cldssbrsiga  34870  dya2iocucvr  34966  kur14lem7  36095  kur14lem9  36097  connpconn  36118  cvmliftmolem1  36164  ordtop  37348  pibt2  38477  ntrelmap  45262  clselmap  45264  dssmapntrcls  45265  dssmapclsntr  45266  toprestsubel  46305  reopn  46441  toplatglb0  50249