Theorem eltopss 8872

Description: A member of a topology is a subset of its underlying set.

Hypothesis

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

Assertion

Ref	Expression
eltopss	|- ((J e. Top /\ A e. J) -> A C_ X)

Proof of Theorem eltopss

Step	Hyp	Ref	Expression
1		elssuni 3206	. . 3 |- (A e. J -> A C_ U.J)
2		1open.1	. . 3 |- X = U.J
3	1, 2	syl6ssr 2664	. 2 |- (A e. J -> A C_ X)
4	3	adantl 424	1 |- ((J e. Top /\ A e. J) -> A C_ X)

Syntax hints:   -> wi 3   /\ wa 240   = wceq 1298   e. wcel 1300   C_ wss 2593  U.cuni 3177  Topctop 8857

This theorem is referenced by:  txuni 8935  opncld 8950  clsval2 8961  ntrval2 8962  ntrss3 8968  cmclsopn 8969  opnneissb 9004  opnssneib 9005  opnneiss 9008  islp2 9023  iscnp2 9037  idcn 9042  cnpnei 9043  tx1cn 10223  tx2cn 10224  subspid 10249  fbaslim 10322  usinuniop 10341  homcard 14893  opncldf1 15402  opnregcld 15415  cnntr 15420  subntr 15425  dfcon2 15442  connsub 15443  cnconn 15444  topmtcl 15525  topjoin 15527  ist1-2 15542  isnrm2 15552  neifg 15559  ufcondr 15581  fcluscf 15612  flimfnfcls 15615

This theorem was proved from axioms:  ax-1 4  ax-2 5  ax-3 6  ax-mp 7  ax-7 1304  ax-gen 1305  ax-8 1306  ax-9 1307  ax-10 1308  ax-11 1309  ax-12 1310  ax-17 1317  ax-4 1319  ax-5o 1321  ax-6o 1324  ax-9o 1481  ax-10o 1500  ax-16 1580  ax-11o 1588  ax-ext 1865

This theorem depends on definitions:  df-bi 164  df-or 241  df-an 242  df-ex 1327  df-sb 1536  df-clab 1872  df-cleq 1877  df-clel 1880  df-v 2294  df-in 2603  df-ss 2605  df-uni 3178

Copyright terms: Public domain