Theorem topopn 21963

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 3939	. . 3 ⊢ 𝐽 ⊆ 𝐽
3		uniopn 21954	. . 3 ⊢ ((𝐽 ∈ Top ∧ 𝐽 ⊆ 𝐽) → ∪ 𝐽 ∈ 𝐽)
4	2, 3	mpan2 687	. 2 ⊢ (𝐽 ∈ Top → ∪ 𝐽 ∈ 𝐽)
5	1, 4	eqeltrid 2843	1 ⊢ (𝐽 ∈ Top → 𝑋 ∈ 𝐽)

Syntax hints:   → wi 4   = wceq 1539   ∈ wcel 2108   ⊆ wss 3883  ∪ cuni 4836  Topctop 21950

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1799  ax-4 1813  ax-5 1914  ax-6 1972  ax-7 2012  ax-8 2110  ax-9 2118  ax-ext 2709  ax-sep 5218

This theorem depends on definitions:  df-bi 206  df-an 396  df-tru 1542  df-ex 1784  df-sb 2069  df-clab 2716  df-cleq 2730  df-clel 2817  df-ral 3068  df-rab 3072  df-v 3424  df-in 3890  df-ss 3900  df-pw 4532  df-uni 4837  df-top 21951

This theorem is referenced by:  riinopn  21965  toponmax  21983  cldval  22082  ntrfval  22083  clsfval  22084  iscld  22086  ntrval  22095  clsval  22096  0cld  22097  clsval2  22109  ntrtop  22129  toponmre  22152  neifval  22158  neif  22159  neival  22161  isnei  22162  tpnei  22180  lpfval  22197  lpval  22198  restcld  22231  restcls  22240  restntr  22241  cnrest  22344  cmpsub  22459  hauscmplem  22465  cmpfi  22467  isconn2  22473  connsubclo  22483  1stcfb  22504  1stcelcls  22520  islly2  22543  lly1stc  22555  islocfin  22576  finlocfin  22579  cmpkgen  22610  llycmpkgen  22611  ptbasid  22634  ptpjpre2  22639  ptopn2  22643  xkoopn  22648  xkouni  22658  txcld  22662  txcn  22685  ptrescn  22698  txtube  22699  txhaus  22706  xkoptsub  22713  xkopt  22714  xkopjcn  22715  qtoptop  22759  qtopuni  22761  opnfbas  22901  flimval  23022  flimfil  23028  hausflim  23040  hauspwpwf1  23046  hauspwpwdom  23047  flimfnfcls  23087  cnpfcfi  23099  bcthlem5  24397  dvply1  25349  cldssbrsiga  32055  dya2iocucvr  32151  kur14lem7  33074  kur14lem9  33076  connpconn  33097  cvmliftmolem1  33143  ordtop  34552  pibt2  35515  ntrelmap  41624  clselmap  41626  dssmapntrcls  41627  dssmapclsntr  41628  reopn  42717  toplatglb0  46173