Theorem topopn 22933

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 4031	. . 3 ⊢ 𝐽 ⊆ 𝐽
3		uniopn 22924	. . 3 ⊢ ((𝐽 ∈ Top ∧ 𝐽 ⊆ 𝐽) → ∪ 𝐽 ∈ 𝐽)
4	2, 3	mpan2 690	. 2 ⊢ (𝐽 ∈ Top → ∪ 𝐽 ∈ 𝐽)
5	1, 4	eqeltrid 2848	1 ⊢ (𝐽 ∈ Top → 𝑋 ∈ 𝐽)

Syntax hints:   → wi 4   = wceq 1537   ∈ wcel 2108   ⊆ wss 3976  ∪ cuni 4931  Topctop 22920

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1793  ax-4 1807  ax-5 1909  ax-6 1967  ax-7 2007  ax-8 2110  ax-9 2118  ax-ext 2711  ax-sep 5317

This theorem depends on definitions:  df-bi 207  df-an 396  df-3an 1089  df-tru 1540  df-ex 1778  df-sb 2065  df-clab 2718  df-cleq 2732  df-clel 2819  df-ral 3068  df-rex 3077  df-rab 3444  df-v 3490  df-in 3983  df-ss 3993  df-pw 4624  df-uni 4932  df-top 22921

This theorem is referenced by:  riinopn  22935  toponmax  22953  cldval  23052  ntrfval  23053  clsfval  23054  iscld  23056  ntrval  23065  clsval  23066  0cld  23067  clsval2  23079  ntrtop  23099  toponmre  23122  neifval  23128  neif  23129  neival  23131  isnei  23132  tpnei  23150  lpfval  23167  lpval  23168  restcld  23201  restcls  23210  restntr  23211  cnrest  23314  cmpsub  23429  hauscmplem  23435  cmpfi  23437  isconn2  23443  connsubclo  23453  1stcfb  23474  1stcelcls  23490  islly2  23513  lly1stc  23525  islocfin  23546  finlocfin  23549  cmpkgen  23580  llycmpkgen  23581  ptbasid  23604  ptpjpre2  23609  ptopn2  23613  xkoopn  23618  xkouni  23628  txcld  23632  txcn  23655  ptrescn  23668  txtube  23669  txhaus  23676  xkoptsub  23683  xkopt  23684  xkopjcn  23685  qtoptop  23729  qtopuni  23731  opnfbas  23871  flimval  23992  flimfil  23998  hausflim  24010  hauspwpwf1  24016  hauspwpwdom  24017  flimfnfcls  24057  cnpfcfi  24069  bcthlem5  25381  dvply1  26343  cldssbrsiga  34151  dya2iocucvr  34249  kur14lem7  35180  kur14lem9  35182  connpconn  35203  cvmliftmolem1  35249  ordtop  36402  pibt2  37383  ntrelmap  44087  clselmap  44089  dssmapntrcls  44090  dssmapclsntr  44091  toprestsubel  45059  reopn  45204  toplatglb0  48671