Theorem topopn 23279

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

This proof depends on syntax axioms:   → wi 4   = wceq 1570   ∈ wcel 2147   ⊆ wss 3900  ∪ cuni 4872  Topctop 23266

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 1945  ax-6 2002  ax-7 2043  ax-8 2149  ax-9 2157  ax-ext 2735  ax-sep 5255

This proof depends on definitions:  df-bi 210  df-an 402  df-3an 1105  df-tru 1573  df-ex 1813  df-sb 2102  df-clab 2742  df-cleq 2755  df-clel 2839  df-ral 3081  df-rex 3091  df-rab 3417  df-v 3456  df-ss 3901  df-in 4094  df-pw 4562  df-uni 4873  df-top 23267

This theorem is used by:  riinopn  23281  toponmax  23299  cldval  23396  ntrfval  23397  clsfval  23398  iscld  23400  ntrval  23409  clsval  23410  0cld  23411  clsval2  23423  ntrtop  23443  toponmre  23466  neifval  23472  neif  23473  neival  23475  isnei  23476  tpnei  23494  lpfval  23511  lpval  23512  restcld  23545  restcls  23554  restntr  23555  cnrest  23658  cmpsub  23773  hauscmplem  23779  cmpfi  23781  isconn2  23787  connsubclo  23797  1stcfb  23818  1stcelcls  23835  islly2  23858  lly1stc  23870  islocfin  23891  finlocfin  23894  cmpkgen  23925  llycmpkgen  23926  ptbasid  23949  ptpjpre2  23954  ptopn2  23958  xkoopn  23963  xkouni  23973  txcld  23977  txcn  24000  ptrescn  24013  txtube  24014  txhaus  24021  xkoptsub  24028  xkopt  24029  xkopjcn  24030  qtoptop  24074  qtopuni  24076  opnfbas  24216  flimval  24337  flimfil  24343  hausflim  24355  hauspwpwf1  24361  hauspwpwdom  24362  flimfnfcls  24402  cnpfcfi  24414  bcthlem5  25704  dvply1  26660  cldssbrsiga  34931  dya2iocucvr  35027  kur14lem7  36185  kur14lem9  36187  connpconn  36208  cvmliftmolem1  36254  ordtop  37439  pibt2  38608  ntrelmap  45386  clselmap  45388  dssmapntrcls  45389  dssmapclsntr  45390  toprestsubel  46442  reopn  46578  toplatglb0  50444