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

Theorem eltopss 22056
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 4871 . . 3 (𝐴𝐽𝐴 𝐽)
2 1open.1 . . 3 𝑋 = 𝐽
31, 2sseqtrrdi 3972 . 2 (𝐴𝐽𝐴𝑋)
43adantl 482 1 ((𝐽 ∈ Top ∧ 𝐴𝐽) → 𝐴𝑋)
Colors of variables: wff setvar class
Syntax hints:  wi 4  wa 396   = wceq 1539  wcel 2106  wss 3887   cuni 4839  Topctop 22042
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1798  ax-4 1812  ax-5 1913  ax-6 1971  ax-7 2011  ax-8 2108  ax-9 2116  ax-ext 2709
This theorem depends on definitions:  df-bi 206  df-an 397  df-tru 1542  df-ex 1783  df-sb 2068  df-clab 2716  df-cleq 2730  df-clel 2816  df-v 3434  df-in 3894  df-ss 3904  df-uni 4840
This theorem is referenced by:  riinopn  22057  opncld  22184  ntrval2  22202  ntrss3  22211  cmclsopn  22213  opncldf1  22235  opnneissb  22265  opnssneib  22266  opnneiss  22269  neitr  22331  restntr  22333  cnpnei  22415  imasnopn  22841  cnextcn  23218  utopreg  23404  ist0cld  31783  opnregcld  34519  ptrecube  35777  poimirlem29  35806  poimir  35810  seposep  46219  iscnrm3rlem7  46240
  Copyright terms: Public domain W3C validator