Theorem topopn 20930

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 3773	. . 3 ⊢ 𝐽 ⊆ 𝐽
3		uniopn 20921	. . 3 ⊢ ((𝐽 ∈ Top ∧ 𝐽 ⊆ 𝐽) → ∪ 𝐽 ∈ 𝐽)
4	2, 3	mpan2 671	. 2 ⊢ (𝐽 ∈ Top → ∪ 𝐽 ∈ 𝐽)
5	1, 4	syl5eqel 2854	1 ⊢ (𝐽 ∈ Top → 𝑋 ∈ 𝐽)

Syntax hints:   → wi 4   = wceq 1631   ∈ wcel 2145   ⊆ wss 3723  ∪ cuni 4575  Topctop 20917

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1870  ax-4 1885  ax-5 1991  ax-6 2057  ax-7 2093  ax-9 2154  ax-10 2174  ax-11 2190  ax-12 2203  ax-13 2408  ax-ext 2751  ax-sep 4916

This theorem depends on definitions:  df-bi 197  df-an 383  df-or 837  df-tru 1634  df-ex 1853  df-nf 1858  df-sb 2050  df-clab 2758  df-cleq 2764  df-clel 2767  df-nfc 2902  df-ral 3066  df-rex 3067  df-v 3353  df-in 3730  df-ss 3737  df-pw 4300  df-uni 4576  df-top 20918

This theorem is referenced by:  riinopn  20932  toponmax  20950  cldval  21047  ntrfval  21048  clsfval  21049  iscld  21051  ntrval  21060  clsval  21061  0cld  21062  clsval2  21074  ntrtop  21094  toponmre  21117  neifval  21123  neif  21124  neival  21126  isnei  21127  tpnei  21145  lpfval  21162  lpval  21163  restcld  21196  restcls  21205  restntr  21206  cnrest  21309  cmpsub  21423  hauscmplem  21429  cmpfi  21431  isconn2  21437  connsubclo  21447  1stcfb  21468  1stcelcls  21484  islly2  21507  lly1stc  21519  islocfin  21540  finlocfin  21543  cmpkgen  21574  llycmpkgen  21575  ptbasid  21598  ptpjpre2  21603  ptopn2  21607  xkoopn  21612  xkouni  21622  txcld  21626  txcn  21649  ptrescn  21662  txtube  21663  txhaus  21670  xkoptsub  21677  xkopt  21678  xkopjcn  21679  qtoptop  21723  qtopuni  21725  opnfbas  21865  flimval  21986  flimfil  21992  hausflim  22004  hauspwpwf1  22010  hauspwpwdom  22011  flimfnfcls  22051  cnpfcfi  22063  bcthlem5  23343  dvply1  24258  cldssbrsiga  30589  dya2iocucvr  30685  kur14lem7  31531  kur14lem9  31533  connpconn  31554  cvmliftmolem1  31600  ordtop  32771  ntrelmap  38949  clselmap  38951  dssmapntrcls  38952  dssmapclsntr  38953  reopn  40016