MPE Home Metamath Proof Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >  eltopss Structured version   Unicode version

Theorem eltopss 18542
Description: A member of a topology is a subset of its underlying set. (Contributed by NM, 12-Sep-2006.)
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
StepHypRef Expression
1 elssuni 4142 . . 3  |-  ( A  e.  J  ->  A  C_ 
U. J )
2 1open.1 . . 3  |-  X  = 
U. J
31, 2syl6sseqr 3424 . 2  |-  ( A  e.  J  ->  A  C_  X )
43adantl 466 1  |-  ( ( J  e.  Top  /\  A  e.  J )  ->  A  C_  X )
Colors of variables: wff setvar class
Syntax hints:    -> wi 4    /\ wa 369    = wceq 1369    e. wcel 1756    C_ wss 3349   U.cuni 4112   Topctop 18520
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
This theorem depends on definitions:  df-bi 185  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 2577  df-v 2995  df-in 3356  df-ss 3363  df-uni 4113
This theorem is referenced by:  riinopn  18543  opncld  18659  ntrval2  18677  ntrss3  18686  cmclsopn  18688  opncldf1  18710  opnneissb  18740  opnssneib  18741  opnneiss  18744  neitr  18806  restntr  18808  cnpnei  18890  imasnopn  19285  cnextcn  19661  utopreg  19849  opnregcld  28551
  Copyright terms: Public domain W3C validator