Theorem topopn 23131

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 3953	. . 3 ⊢ 𝐽 ⊆ 𝐽
3		uniopn 23122	. . 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 1570   ∈ wcel 2145   ⊆ wss 3899  ∪ cuni 4867  Topctop 23118

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1828  ax-4 1842  ax-5 1943  ax-6 2000  ax-7 2041  ax-8 2147  ax-9 2155  ax-ext 2732  ax-sep 5251

This proof depends on definitions:  df-bi 210  df-an 402  df-3an 1105  df-tru 1573  df-ex 1813  df-sb 2100  df-clab 2739  df-cleq 2752  df-clel 2835  df-ral 3077  df-rex 3087  df-rab 3413  df-v 3452  df-in 3906  df-ss 3916  df-pw 4559  df-uni 4868  df-top 23119

This theorem is used by:  riinopn  23133  toponmax  23151  cldval  23248  ntrfval  23249  clsfval  23250  iscld  23252  ntrval  23261  clsval  23262  0cld  23263  clsval2  23275  ntrtop  23295  toponmre  23318  neifval  23324  neif  23325  neival  23327  isnei  23328  tpnei  23346  lpfval  23363  lpval  23364  restcld  23397  restcls  23406  restntr  23407  cnrest  23510  cmpsub  23625  hauscmplem  23631  cmpfi  23633  isconn2  23639  connsubclo  23649  1stcfb  23670  1stcelcls  23687  islly2  23710  lly1stc  23722  islocfin  23743  finlocfin  23746  cmpkgen  23777  llycmpkgen  23778  ptbasid  23801  ptpjpre2  23806  ptopn2  23810  xkoopn  23815  xkouni  23825  txcld  23829  txcn  23852  ptrescn  23865  txtube  23866  txhaus  23873  xkoptsub  23880  xkopt  23881  xkopjcn  23882  qtoptop  23926  qtopuni  23928  opnfbas  24068  flimval  24189  flimfil  24195  hausflim  24207  hauspwpwf1  24213  hauspwpwdom  24214  flimfnfcls  24254  cnpfcfi  24266  bcthlem5  25556  dvply1  26514  cldssbrsiga  34698  dya2iocucvr  34795  kur14lem7  35791  kur14lem9  35793  connpconn  35814  cvmliftmolem1  35860  ordtop  37055  pibt2  38171  ntrelmap  44965  clselmap  44967  dssmapntrcls  44968  dssmapclsntr  44969  toprestsubel  45986  reopn  46122  toplatglb0  49925