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

Theorem eltopss 22928
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 4941 . . 3 (𝐴𝐽𝐴 𝐽)
2 1open.1 . . 3 𝑋 = 𝐽
31, 2sseqtrrdi 4046 . 2 (𝐴𝐽𝐴𝑋)
43adantl 481 1 ((𝐽 ∈ Top ∧ 𝐴𝐽) → 𝐴𝑋)
Colors of variables: wff setvar class
Syntax hints:  wi 4  wa 395   = wceq 1536  wcel 2105  wss 3962   cuni 4911  Topctop 22914
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1791  ax-4 1805  ax-5 1907  ax-6 1964  ax-7 2004  ax-8 2107  ax-9 2115  ax-ext 2705
This theorem depends on definitions:  df-bi 207  df-an 396  df-tru 1539  df-ex 1776  df-sb 2062  df-clab 2712  df-cleq 2726  df-clel 2813  df-v 3479  df-ss 3979  df-uni 4912
This theorem is referenced by:  riinopn  22929  opncld  23056  ntrval2  23074  ntrss3  23083  cmclsopn  23085  opncldf1  23107  opnneissb  23137  opnssneib  23138  opnneiss  23141  neitr  23203  restntr  23205  cnpnei  23287  imasnopn  23713  cnextcn  24090  utopreg  24276  ist0cld  33793  opnregcld  36312  ptrecube  37606  poimirlem29  37635  poimir  37639  seposep  48721  iscnrm3rlem7  48742
  Copyright terms: Public domain W3C validator