Theorem topopn 22800

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 3972	. . 3 ⊢ 𝐽 ⊆ 𝐽
3		uniopn 22791	. . 3 ⊢ ((𝐽 ∈ Top ∧ 𝐽 ⊆ 𝐽) → ∪ 𝐽 ∈ 𝐽)
4	2, 3	mpan2 691	. 2 ⊢ (𝐽 ∈ Top → ∪ 𝐽 ∈ 𝐽)
5	1, 4	eqeltrid 2833	1 ⊢ (𝐽 ∈ Top → 𝑋 ∈ 𝐽)

Syntax hints:   → wi 4   = wceq 1540   ∈ wcel 2109   ⊆ wss 3917  ∪ cuni 4874  Topctop 22787

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1795  ax-4 1809  ax-5 1910  ax-6 1967  ax-7 2008  ax-8 2111  ax-9 2119  ax-ext 2702  ax-sep 5254

This theorem depends on definitions:  df-bi 207  df-an 396  df-3an 1088  df-tru 1543  df-ex 1780  df-sb 2066  df-clab 2709  df-cleq 2722  df-clel 2804  df-ral 3046  df-rex 3055  df-rab 3409  df-v 3452  df-in 3924  df-ss 3934  df-pw 4568  df-uni 4875  df-top 22788

This theorem is referenced by:  riinopn  22802  toponmax  22820  cldval  22917  ntrfval  22918  clsfval  22919  iscld  22921  ntrval  22930  clsval  22931  0cld  22932  clsval2  22944  ntrtop  22964  toponmre  22987  neifval  22993  neif  22994  neival  22996  isnei  22997  tpnei  23015  lpfval  23032  lpval  23033  restcld  23066  restcls  23075  restntr  23076  cnrest  23179  cmpsub  23294  hauscmplem  23300  cmpfi  23302  isconn2  23308  connsubclo  23318  1stcfb  23339  1stcelcls  23355  islly2  23378  lly1stc  23390  islocfin  23411  finlocfin  23414  cmpkgen  23445  llycmpkgen  23446  ptbasid  23469  ptpjpre2  23474  ptopn2  23478  xkoopn  23483  xkouni  23493  txcld  23497  txcn  23520  ptrescn  23533  txtube  23534  txhaus  23541  xkoptsub  23548  xkopt  23549  xkopjcn  23550  qtoptop  23594  qtopuni  23596  opnfbas  23736  flimval  23857  flimfil  23863  hausflim  23875  hauspwpwf1  23881  hauspwpwdom  23882  flimfnfcls  23922  cnpfcfi  23934  bcthlem5  25235  dvply1  26198  cldssbrsiga  34184  dya2iocucvr  34282  kur14lem7  35206  kur14lem9  35208  connpconn  35229  cvmliftmolem1  35275  ordtop  36431  pibt2  37412  ntrelmap  44121  clselmap  44123  dssmapntrcls  44124  dssmapclsntr  44125  toprestsubel  45155  reopn  45294  toplatglb0  48991