Theorem topopn 23217

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

This proof depends on syntax axioms:   → wi 4   = wceq 1570   ∈ wcel 2145   ⊆ wss 3899  ∪ cuni 4867  Topctop 23204

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 2733  ax-sep 5249

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 2740  df-cleq 2753  df-clel 2836  df-ral 3078  df-rex 3088  df-rab 3414  df-v 3453  df-in 3906  df-ss 3916  df-pw 4559  df-uni 4868  df-top 23205

This theorem is used by:  riinopn  23219  toponmax  23237  cldval  23334  ntrfval  23335  clsfval  23336  iscld  23338  ntrval  23347  clsval  23348  0cld  23349  clsval2  23361  ntrtop  23381  toponmre  23404  neifval  23410  neif  23411  neival  23413  isnei  23414  tpnei  23432  lpfval  23449  lpval  23450  restcld  23483  restcls  23492  restntr  23493  cnrest  23596  cmpsub  23711  hauscmplem  23717  cmpfi  23719  isconn2  23725  connsubclo  23735  1stcfb  23756  1stcelcls  23773  islly2  23796  lly1stc  23808  islocfin  23829  finlocfin  23832  cmpkgen  23863  llycmpkgen  23864  ptbasid  23887  ptpjpre2  23892  ptopn2  23896  xkoopn  23901  xkouni  23911  txcld  23915  txcn  23938  ptrescn  23951  txtube  23952  txhaus  23959  xkoptsub  23966  xkopt  23967  xkopjcn  23968  qtoptop  24012  qtopuni  24014  opnfbas  24154  flimval  24275  flimfil  24281  hausflim  24293  hauspwpwf1  24299  hauspwpwdom  24300  flimfnfcls  24340  cnpfcfi  24352  bcthlem5  25642  dvply1  26598  cldssbrsiga  34813  dya2iocucvr  34909  kur14lem7  35956  kur14lem9  35958  connpconn  35979  cvmliftmolem1  36025  ordtop  37204  pibt2  38320  ntrelmap  45110  clselmap  45112  dssmapntrcls  45113  dssmapclsntr  45114  toprestsubel  46138  reopn  46274  toplatglb0  50076