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

Theorem eltopss 18361
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 4109 . . 3  |-  ( A  e.  J  ->  A  C_ 
U. J )
2 1open.1 . . 3  |-  X  = 
U. J
31, 2syl6sseqr 3391 . 2  |-  ( A  e.  J  ->  A  C_  X )
43adantl 463 1  |-  ( ( J  e.  Top  /\  A  e.  J )  ->  A  C_  X )
Colors of variables: wff setvar class
Syntax hints:    -> wi 4    /\ wa 369    = wceq 1362    e. wcel 1755    C_ wss 3316   U.cuni 4079   Topctop 18339
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1594  ax-4 1605  ax-5 1669  ax-6 1707  ax-7 1727  ax-10 1774  ax-11 1779  ax-12 1791  ax-13 1942  ax-ext 2414
This theorem depends on definitions:  df-bi 185  df-or 370  df-an 371  df-tru 1365  df-ex 1590  df-nf 1593  df-sb 1700  df-clab 2420  df-cleq 2426  df-clel 2429  df-nfc 2558  df-v 2964  df-in 3323  df-ss 3330  df-uni 4080
This theorem is referenced by:  riinopn  18362  opncld  18478  ntrval2  18496  ntrss3  18505  cmclsopn  18507  opncldf1  18529  opnneissb  18559  opnssneib  18560  opnneiss  18563  neitr  18625  restntr  18627  cnpnei  18709  imasnopn  19104  cnextcn  19480  utopreg  19668  opnregcld  28366
  Copyright terms: Public domain W3C validator