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

Theorem eltopss 22913
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 4937 . . 3 (𝐴𝐽𝐴 𝐽)
2 1open.1 . . 3 𝑋 = 𝐽
31, 2sseqtrrdi 4025 . 2 (𝐴𝐽𝐴𝑋)
43adantl 481 1 ((𝐽 ∈ Top ∧ 𝐴𝐽) → 𝐴𝑋)
Colors of variables: wff setvar class
Syntax hints:  wi 4  wa 395   = wceq 1540  wcel 2108  wss 3951   cuni 4907  Topctop 22899
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1795  ax-4 1809  ax-5 1910  ax-6 1967  ax-7 2007  ax-8 2110  ax-9 2118  ax-ext 2708
This theorem depends on definitions:  df-bi 207  df-an 396  df-tru 1543  df-ex 1780  df-sb 2065  df-clab 2715  df-cleq 2729  df-clel 2816  df-v 3482  df-ss 3968  df-uni 4908
This theorem is referenced by:  riinopn  22914  opncld  23041  ntrval2  23059  ntrss3  23068  cmclsopn  23070  opncldf1  23092  opnneissb  23122  opnssneib  23123  opnneiss  23126  neitr  23188  restntr  23190  cnpnei  23272  imasnopn  23698  cnextcn  24075  utopreg  24261  ist0cld  33832  opnregcld  36331  ptrecube  37627  poimirlem29  37656  poimir  37660  seposep  48823  iscnrm3rlem7  48843
  Copyright terms: Public domain W3C validator