Theorem topopn 23113

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 3960	. . 3 ⊢ 𝐽 ⊆ 𝐽
3		uniopn 23104	. . 3 ⊢ ((𝐽 ∈ Top ∧ 𝐽 ⊆ 𝐽) → ∪ 𝐽 ∈ 𝐽)
4	2, 3	mpan2 704	. 2 ⊢ (𝐽 ∈ Top → ∪ 𝐽 ∈ 𝐽)
5	1, 4	eqeltrid 2869	1 ⊢ (𝐽 ∈ Top → 𝑋 ∈ 𝐽)

This proof depends on syntax axioms:   → wi 4   = wceq 1570   ∈ wcel 2146   ⊆ wss 3906  ∪ cuni 4874  Topctop 23100

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1828  ax-4 1842  ax-5 1943  ax-6 2000  ax-7 2041  ax-8 2148  ax-9 2156  ax-ext 2737  ax-sep 5259

This proof depends on definitions:  df-bi 210  df-an 402  df-3an 1105  df-tru 1573  df-ex 1813  df-sb 2100  df-clab 2744  df-cleq 2757  df-clel 2840  df-ral 3082  df-rex 3092  df-rab 3419  df-v 3459  df-in 3913  df-ss 3923  df-pw 4566  df-uni 4875  df-top 23101

This theorem is used by:  riinopn  23115  toponmax  23133  cldval  23230  ntrfval  23231  clsfval  23232  iscld  23234  ntrval  23243  clsval  23244  0cld  23245  clsval2  23257  ntrtop  23277  toponmre  23300  neifval  23306  neif  23307  neival  23309  isnei  23310  tpnei  23328  lpfval  23345  lpval  23346  restcld  23379  restcls  23388  restntr  23389  cnrest  23492  cmpsub  23607  hauscmplem  23613  cmpfi  23615  isconn2  23621  connsubclo  23631  1stcfb  23652  1stcelcls  23669  islly2  23692  lly1stc  23704  islocfin  23725  finlocfin  23728  cmpkgen  23759  llycmpkgen  23760  ptbasid  23783  ptpjpre2  23788  ptopn2  23792  xkoopn  23797  xkouni  23807  txcld  23811  txcn  23834  ptrescn  23847  txtube  23848  txhaus  23855  xkoptsub  23862  xkopt  23863  xkopjcn  23864  qtoptop  23908  qtopuni  23910  opnfbas  24050  flimval  24171  flimfil  24177  hausflim  24189  hauspwpwf1  24195  hauspwpwdom  24196  flimfnfcls  24236  cnpfcfi  24248  bcthlem5  25538  dvply1  26496  cldssbrsiga  34642  dya2iocucvr  34739  kur14lem7  35741  kur14lem9  35743  connpconn  35764  cvmliftmolem1  35810  ordtop  37004  pibt2  38120  ntrelmap  44909  clselmap  44911  dssmapntrcls  44912  dssmapclsntr  44913  toprestsubel  45930  reopn  46066  toplatglb0  49834