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

Theorem eltopss 22338
Description: A member of a topology is a subset of its underlying set. (Contributed by NM, 12-Sep-2006.)
Hypothesis
Ref Expression
1open.1 𝑋 = 𝐽
Assertion
Ref Expression
eltopss ((𝐽 ∈ Top ∧ 𝐴𝐽) → 𝐴𝑋)

Proof of Theorem eltopss
StepHypRef Expression
1 elssuni 4934 . . 3 (𝐴𝐽𝐴 𝐽)
2 1open.1 . . 3 𝑋 = 𝐽
31, 2sseqtrrdi 4029 . 2 (𝐴𝐽𝐴𝑋)
43adantl 482 1 ((𝐽 ∈ Top ∧ 𝐴𝐽) → 𝐴𝑋)
Colors of variables: wff setvar class
Syntax hints:  wi 4  wa 396   = wceq 1541  wcel 2106  wss 3944   cuni 4901  Topctop 22324
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1797  ax-4 1811  ax-5 1913  ax-6 1971  ax-7 2011  ax-8 2108  ax-9 2116  ax-ext 2702
This theorem depends on definitions:  df-bi 206  df-an 397  df-tru 1544  df-ex 1782  df-sb 2068  df-clab 2709  df-cleq 2723  df-clel 2809  df-v 3475  df-in 3951  df-ss 3961  df-uni 4902
This theorem is referenced by:  riinopn  22339  opncld  22466  ntrval2  22484  ntrss3  22493  cmclsopn  22495  opncldf1  22517  opnneissb  22547  opnssneib  22548  opnneiss  22551  neitr  22613  restntr  22615  cnpnei  22697  imasnopn  23123  cnextcn  23500  utopreg  23686  ist0cld  32644  opnregcld  35019  ptrecube  36292  poimirlem29  36321  poimir  36325  seposep  47206  iscnrm3rlem7  47227
  Copyright terms: Public domain W3C validator