Theorem topopn 22408

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 4005	. . 3 ⊢ 𝐽 ⊆ 𝐽
3		uniopn 22399	. . 3 ⊢ ((𝐽 ∈ Top ∧ 𝐽 ⊆ 𝐽) → ∪ 𝐽 ∈ 𝐽)
4	2, 3	mpan2 690	. 2 ⊢ (𝐽 ∈ Top → ∪ 𝐽 ∈ 𝐽)
5	1, 4	eqeltrid 2838	1 ⊢ (𝐽 ∈ Top → 𝑋 ∈ 𝐽)

Syntax hints:   → wi 4   = wceq 1542   ∈ wcel 2107   ⊆ wss 3949  ∪ cuni 4909  Topctop 22395

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1798  ax-4 1812  ax-5 1914  ax-6 1972  ax-7 2012  ax-8 2109  ax-9 2117  ax-ext 2704  ax-sep 5300

This theorem depends on definitions:  df-bi 206  df-an 398  df-tru 1545  df-ex 1783  df-sb 2069  df-clab 2711  df-cleq 2725  df-clel 2811  df-ral 3063  df-rex 3072  df-rab 3434  df-v 3477  df-in 3956  df-ss 3966  df-pw 4605  df-uni 4910  df-top 22396

This theorem is referenced by:  riinopn  22410  toponmax  22428  cldval  22527  ntrfval  22528  clsfval  22529  iscld  22531  ntrval  22540  clsval  22541  0cld  22542  clsval2  22554  ntrtop  22574  toponmre  22597  neifval  22603  neif  22604  neival  22606  isnei  22607  tpnei  22625  lpfval  22642  lpval  22643  restcld  22676  restcls  22685  restntr  22686  cnrest  22789  cmpsub  22904  hauscmplem  22910  cmpfi  22912  isconn2  22918  connsubclo  22928  1stcfb  22949  1stcelcls  22965  islly2  22988  lly1stc  23000  islocfin  23021  finlocfin  23024  cmpkgen  23055  llycmpkgen  23056  ptbasid  23079  ptpjpre2  23084  ptopn2  23088  xkoopn  23093  xkouni  23103  txcld  23107  txcn  23130  ptrescn  23143  txtube  23144  txhaus  23151  xkoptsub  23158  xkopt  23159  xkopjcn  23160  qtoptop  23204  qtopuni  23206  opnfbas  23346  flimval  23467  flimfil  23473  hausflim  23485  hauspwpwf1  23491  hauspwpwdom  23492  flimfnfcls  23532  cnpfcfi  23544  bcthlem5  24845  dvply1  25797  cldssbrsiga  33216  dya2iocucvr  33314  kur14lem7  34234  kur14lem9  34236  connpconn  34257  cvmliftmolem1  34303  ordtop  35369  pibt2  36346  ntrelmap  42924  clselmap  42926  dssmapntrcls  42927  dssmapclsntr  42928  toprestsubel  43896  reopn  44047  toplatglb0  47672