Theorem topopn 23063

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 3959	. . 3 ⊢ 𝐽 ⊆ 𝐽
3		uniopn 23054	. . 3 ⊢ ((𝐽 ∈ Top ∧ 𝐽 ⊆ 𝐽) → ∪ 𝐽 ∈ 𝐽)
4	2, 3	mpan2 703	. 2 ⊢ (𝐽 ∈ Top → ∪ 𝐽 ∈ 𝐽)
5	1, 4	eqeltrid 2867	1 ⊢ (𝐽 ∈ Top → 𝑋 ∈ 𝐽)

Syntax hints:   → wi 4   = wceq 1570   ∈ wcel 2143   ⊆ wss 3905  ∪ cuni 4872  Topctop 23050

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1825  ax-4 1839  ax-5 1940  ax-6 1997  ax-7 2038  ax-8 2145  ax-9 2153  ax-ext 2735  ax-sep 5257

This theorem depends on definitions:  df-bi 210  df-an 401  df-3an 1105  df-tru 1573  df-ex 1810  df-sb 2097  df-clab 2742  df-cleq 2755  df-clel 2838  df-ral 3080  df-rex 3090  df-rab 3417  df-v 3457  df-in 3912  df-ss 3922  df-pw 4564  df-uni 4873  df-top 23051

This theorem is referenced by:  riinopn  23065  toponmax  23083  cldval  23180  ntrfval  23181  clsfval  23182  iscld  23184  ntrval  23193  clsval  23194  0cld  23195  clsval2  23207  ntrtop  23227  toponmre  23250  neifval  23256  neif  23257  neival  23259  isnei  23260  tpnei  23278  lpfval  23295  lpval  23296  restcld  23329  restcls  23338  restntr  23339  cnrest  23442  cmpsub  23557  hauscmplem  23563  cmpfi  23565  isconn2  23571  connsubclo  23581  1stcfb  23602  1stcelcls  23618  islly2  23641  lly1stc  23653  islocfin  23674  finlocfin  23677  cmpkgen  23708  llycmpkgen  23709  ptbasid  23732  ptpjpre2  23737  ptopn2  23741  xkoopn  23746  xkouni  23756  txcld  23760  txcn  23783  ptrescn  23796  txtube  23797  txhaus  23804  xkoptsub  23811  xkopt  23812  xkopjcn  23813  qtoptop  23857  qtopuni  23859  opnfbas  23999  flimval  24120  flimfil  24126  hausflim  24138  hauspwpwf1  24144  hauspwpwdom  24145  flimfnfcls  24185  cnpfcfi  24197  bcthlem5  25487  dvply1  26445  cldssbrsiga  34577  dya2iocucvr  34674  kur14lem7  35704  kur14lem9  35706  connpconn  35727  cvmliftmolem1  35773  ordtop  36947  pibt2  38063  ntrelmap  44851  clselmap  44853  dssmapntrcls  44854  dssmapclsntr  44855  toprestsubel  45872  reopn  46008  toplatglb0  49777