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

Theorem eltopss 22409
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 4942 . . 3 (𝐴𝐽𝐴 𝐽)
2 1open.1 . . 3 𝑋 = 𝐽
31, 2sseqtrrdi 4034 . 2 (𝐴𝐽𝐴𝑋)
43adantl 483 1 ((𝐽 ∈ Top ∧ 𝐴𝐽) → 𝐴𝑋)
Colors of variables: wff setvar class
Syntax hints:  wi 4  wa 397   = wceq 1542  wcel 2107  wss 3949   cuni 4909  Topctop 22395
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 1914  ax-6 1972  ax-7 2012  ax-8 2109  ax-9 2117  ax-ext 2704
This theorem depends on definitions:  df-bi 206  df-an 398  df-tru 1545  df-ex 1783  df-sb 2069  df-clab 2711  df-cleq 2725  df-clel 2811  df-v 3477  df-in 3956  df-ss 3966  df-uni 4910
This theorem is referenced by:  riinopn  22410  opncld  22537  ntrval2  22555  ntrss3  22564  cmclsopn  22566  opncldf1  22588  opnneissb  22618  opnssneib  22619  opnneiss  22622  neitr  22684  restntr  22686  cnpnei  22768  imasnopn  23194  cnextcn  23571  utopreg  23757  ist0cld  32813  opnregcld  35215  ptrecube  36488  poimirlem29  36517  poimir  36521  seposep  47558  iscnrm3rlem7  47579
  Copyright terms: Public domain W3C validator