Theorem topopn 18522

Description: The underlying set of a topology is an open set. (Contributed by NM, 17-Jul-2006.)

Hypothesis

Ref	Expression
1open.1	|- X = U. J

Assertion

Ref	Expression
topopn	|- ( J e. Top -> X e. J )

Proof of Theorem topopn

Step	Hyp	Ref	Expression
1		1open.1	. 2 |- X = U. J
2		ssid 3378	. . 3 |- J C_ J
3		uniopn 18513	. . 3 |- ( ( J e. Top /\ J C_ J ) -> U. J e. J )
4	2, 3	mpan2 671	. 2 |- ( J e. Top -> U. J e. J )
5	1, 4	syl5eqel 2527	1 |- ( J e. Top -> X e. J )

Syntax hints:   -> wi 4   = wceq 1369   e. wcel 1756   C_ wss 3331   U.cuni 4094   Topctop 18501

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1591  ax-4 1602  ax-5 1670  ax-6 1708  ax-7 1728  ax-10 1775  ax-11 1780  ax-12 1792  ax-13 1943  ax-ext 2423  ax-sep 4416

This theorem depends on definitions:  df-bi 185  df-or 370  df-an 371  df-tru 1372  df-ex 1587  df-nf 1590  df-sb 1701  df-clab 2430  df-cleq 2436  df-clel 2439  df-nfc 2571  df-ral 2723  df-rex 2724  df-v 2977  df-in 3338  df-ss 3345  df-pw 3865  df-uni 4095  df-top 18506

This theorem is referenced by:  riinopn  18524  istps2OLD  18529  toponmax  18536  cldval  18630  ntrfval  18631  clsfval  18632  iscld  18634  ntrval  18643  clsval  18644  0cld  18645  clsval2  18657  ntrtop  18677  toponmre  18700  neifval  18706  neif  18707  neival  18709  isnei  18710  tpnei  18728  lpfval  18745  lpval  18746  restcld  18779  restcls  18788  restntr  18789  cnrest  18892  cmpsub  19006  hauscmplem  19012  cmpfi  19014  iscon2  19021  consubclo  19031  1stcfb  19052  1stcelcls  19068  islly2  19091  lly1stc  19103  cmpkgen  19127  llycmpkgen  19128  ptbasid  19151  ptpjpre2  19156  ptopn2  19160  xkoopn  19165  xkouni  19175  txcld  19179  txcn  19202  ptrescn  19215  txtube  19216  txhaus  19223  xkoptsub  19230  xkopt  19231  xkopjcn  19232  qtoptop  19276  qtopuni  19278  opnfbas  19418  flimval  19539  flimfil  19545  hausflim  19557  hauspwpwf1  19563  hauspwpwdom  19564  flimfnfcls  19604  cnpfcfi  19616  bcthlem5  20842  dvply1  21753  cldssbrsiga  26604  dya2iocucvr  26702  kur14lem7  27103  kur14lem9  27105  conpcon  27127  cvmliftmolem1  27173  ordtop  28285  islocfin  28571  finlocfin  28574