Theorem eltopss 22900

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 4945	. . 3 ⊢ (𝐴 ∈ 𝐽 → 𝐴 ⊆ ∪ 𝐽)
2		1open.1	. . 3 ⊢ 𝑋 = ∪ 𝐽
3	1, 2	sseqtrrdi 4031	. 2 ⊢ (𝐴 ∈ 𝐽 → 𝐴 ⊆ 𝑋)
4	3	adantl 480	1 ⊢ ((𝐽 ∈ Top ∧ 𝐴 ∈ 𝐽) → 𝐴 ⊆ 𝑋)

Syntax hints:   → wi 4   ∧ wa 394   = wceq 1534   ∈ wcel 2099   ⊆ wss 3947  ∪ cuni 4913  Topctop 22886

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1790  ax-4 1804  ax-5 1906  ax-6 1964  ax-7 2004  ax-8 2101  ax-9 2109  ax-ext 2697

This theorem depends on definitions:  df-bi 206  df-an 395  df-tru 1537  df-ex 1775  df-sb 2061  df-clab 2704  df-cleq 2718  df-clel 2803  df-v 3464  df-ss 3964  df-uni 4914

This theorem is referenced by:  riinopn  22901  opncld  23028  ntrval2  23046  ntrss3  23055  cmclsopn  23057  opncldf1  23079  opnneissb  23109  opnssneib  23110  opnneiss  23113  neitr  23175  restntr  23177  cnpnei  23259  imasnopn  23685  cnextcn  24062  utopreg  24248  ist0cld  33648  opnregcld  36042  ptrecube  37321  poimirlem29  37350  poimir  37354  seposep  48259  iscnrm3rlem7  48280