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

Theorem eltopss 22900
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 4945 . . 3 (𝐴𝐽𝐴 𝐽)
2 1open.1 . . 3 𝑋 = 𝐽
31, 2sseqtrrdi 4031 . 2 (𝐴𝐽𝐴𝑋)
43adantl 480 1 ((𝐽 ∈ Top ∧ 𝐴𝐽) → 𝐴𝑋)
Colors of variables: wff setvar class
Syntax hints:  wi 4  wa 394   = wceq 1534  wcel 2099  wss 3947   cuni 4913  Topctop 22886
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1790  ax-4 1804  ax-5 1906  ax-6 1964  ax-7 2004  ax-8 2101  ax-9 2109  ax-ext 2697
This theorem depends on definitions:  df-bi 206  df-an 395  df-tru 1537  df-ex 1775  df-sb 2061  df-clab 2704  df-cleq 2718  df-clel 2803  df-v 3464  df-ss 3964  df-uni 4914
This theorem is referenced by:  riinopn  22901  opncld  23028  ntrval2  23046  ntrss3  23055  cmclsopn  23057  opncldf1  23079  opnneissb  23109  opnssneib  23110  opnneiss  23113  neitr  23175  restntr  23177  cnpnei  23259  imasnopn  23685  cnextcn  24062  utopreg  24248  ist0cld  33648  opnregcld  36042  ptrecube  37321  poimirlem29  37350  poimir  37354  seposep  48259  iscnrm3rlem7  48280
  Copyright terms: Public domain W3C validator