Theorem eltopss 23025

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

Step	Hyp	Ref	Expression
1		elssuni 4900	. . 3 ⊢ (𝐴 ∈ 𝐽 → 𝐴 ⊆ ∪ 𝐽)
2		1open.1	. . 3 ⊢ 𝑋 = ∪ 𝐽
3	1, 2	sseqtrrdi 3980	. 2 ⊢ (𝐴 ∈ 𝐽 → 𝐴 ⊆ 𝑋)
4	3	adantl 486	1 ⊢ ((𝐽 ∈ Top ∧ 𝐴 ∈ 𝐽) → 𝐴 ⊆ 𝑋)

Syntax hints:   → wi 4   ∧ wa 400   = wceq 1563   ∈ wcel 2145   ⊆ wss 3907  ∪ cuni 4868  Topctop 23011

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1818  ax-4 1832  ax-5 1933  ax-6 1990  ax-7 2031  ax-8 2147  ax-9 2155  ax-ext 2737

This theorem depends on definitions:  df-bi 210  df-an 401  df-tru 1566  df-ex 1803  df-sb 2094  df-clab 2744  df-cleq 2757  df-clel 2840  df-v 3459  df-ss 3924  df-uni 4869

This theorem is referenced by:  riinopn  23026  opncld  23151  ntrval2  23169  ntrss3  23178  cmclsopn  23180  opncldf1  23202  opnneissb  23232  opnssneib  23233  opnneiss  23236  neitr  23298  restntr  23300  cnpnei  23382  imasnopn  23808  cnextcn  24185  utopreg  24370  ist0cld  34140  opnregcld  36703  ptrecube  38131  poimirlem29  38160  poimir  38164  seposep  49555  iscnrm3rlem7  49575