Theorem topopn 22884

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 3945	. . 3 ⊢ 𝐽 ⊆ 𝐽
3		uniopn 22875	. . 3 ⊢ ((𝐽 ∈ Top ∧ 𝐽 ⊆ 𝐽) → ∪ 𝐽 ∈ 𝐽)
4	2, 3	mpan2 692	. 2 ⊢ (𝐽 ∈ Top → ∪ 𝐽 ∈ 𝐽)
5	1, 4	eqeltrid 2841	1 ⊢ (𝐽 ∈ Top → 𝑋 ∈ 𝐽)

Syntax hints:   → wi 4   = wceq 1542   ∈ wcel 2114   ⊆ wss 3890  ∪ cuni 4851  Topctop 22871

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1797  ax-4 1811  ax-5 1912  ax-6 1969  ax-7 2010  ax-8 2116  ax-9 2124  ax-ext 2709  ax-sep 5232

This theorem depends on definitions:  df-bi 207  df-an 396  df-3an 1089  df-tru 1545  df-ex 1782  df-sb 2069  df-clab 2716  df-cleq 2729  df-clel 2812  df-ral 3053  df-rex 3063  df-rab 3391  df-v 3432  df-in 3897  df-ss 3907  df-pw 4544  df-uni 4852  df-top 22872

This theorem is referenced by:  riinopn  22886  toponmax  22904  cldval  23001  ntrfval  23002  clsfval  23003  iscld  23005  ntrval  23014  clsval  23015  0cld  23016  clsval2  23028  ntrtop  23048  toponmre  23071  neifval  23077  neif  23078  neival  23080  isnei  23081  tpnei  23099  lpfval  23116  lpval  23117  restcld  23150  restcls  23159  restntr  23160  cnrest  23263  cmpsub  23378  hauscmplem  23384  cmpfi  23386  isconn2  23392  connsubclo  23402  1stcfb  23423  1stcelcls  23439  islly2  23462  lly1stc  23474  islocfin  23495  finlocfin  23498  cmpkgen  23529  llycmpkgen  23530  ptbasid  23553  ptpjpre2  23558  ptopn2  23562  xkoopn  23567  xkouni  23577  txcld  23581  txcn  23604  ptrescn  23617  txtube  23618  txhaus  23625  xkoptsub  23632  xkopt  23633  xkopjcn  23634  qtoptop  23678  qtopuni  23680  opnfbas  23820  flimval  23941  flimfil  23947  hausflim  23959  hauspwpwf1  23965  hauspwpwdom  23966  flimfnfcls  24006  cnpfcfi  24018  bcthlem5  25308  dvply1  26263  cldssbrsiga  34350  dya2iocucvr  34447  kur14lem7  35413  kur14lem9  35415  connpconn  35436  cvmliftmolem1  35482  ordtop  36637  pibt2  37750  ntrelmap  44573  clselmap  44575  dssmapntrcls  44576  dssmapclsntr  44577  toprestsubel  45605  reopn  45743  toplatglb0  49489