Theorem topopn 22826

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

Syntax hints:   → wi 4   = wceq 1540   ∈ wcel 2109   ⊆ wss 3911  ∪ cuni 4867  Topctop 22813

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 2701  ax-sep 5246

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 2708  df-cleq 2721  df-clel 2803  df-ral 3045  df-rex 3054  df-rab 3403  df-v 3446  df-in 3918  df-ss 3928  df-pw 4561  df-uni 4868  df-top 22814

This theorem is referenced by:  riinopn  22828  toponmax  22846  cldval  22943  ntrfval  22944  clsfval  22945  iscld  22947  ntrval  22956  clsval  22957  0cld  22958  clsval2  22970  ntrtop  22990  toponmre  23013  neifval  23019  neif  23020  neival  23022  isnei  23023  tpnei  23041  lpfval  23058  lpval  23059  restcld  23092  restcls  23101  restntr  23102  cnrest  23205  cmpsub  23320  hauscmplem  23326  cmpfi  23328  isconn2  23334  connsubclo  23344  1stcfb  23365  1stcelcls  23381  islly2  23404  lly1stc  23416  islocfin  23437  finlocfin  23440  cmpkgen  23471  llycmpkgen  23472  ptbasid  23495  ptpjpre2  23500  ptopn2  23504  xkoopn  23509  xkouni  23519  txcld  23523  txcn  23546  ptrescn  23559  txtube  23560  txhaus  23567  xkoptsub  23574  xkopt  23575  xkopjcn  23576  qtoptop  23620  qtopuni  23622  opnfbas  23762  flimval  23883  flimfil  23889  hausflim  23901  hauspwpwf1  23907  hauspwpwdom  23908  flimfnfcls  23948  cnpfcfi  23960  bcthlem5  25261  dvply1  26224  cldssbrsiga  34170  dya2iocucvr  34268  kur14lem7  35192  kur14lem9  35194  connpconn  35215  cvmliftmolem1  35261  ordtop  36417  pibt2  37398  ntrelmap  44107  clselmap  44109  dssmapntrcls  44110  dssmapclsntr  44111  toprestsubel  45141  reopn  45280  toplatglb0  48980