Theorem eltopss 22845

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

Syntax hints:   → wi 4   ∧ wa 395   = wceq 1540   ∈ wcel 2108   ⊆ wss 3926  ∪ cuni 4883  Topctop 22831

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 2707

This theorem depends on definitions:  df-bi 207  df-an 396  df-tru 1543  df-ex 1780  df-sb 2065  df-clab 2714  df-cleq 2727  df-clel 2809  df-v 3461  df-ss 3943  df-uni 4884

This theorem is referenced by:  riinopn  22846  opncld  22971  ntrval2  22989  ntrss3  22998  cmclsopn  23000  opncldf1  23022  opnneissb  23052  opnssneib  23053  opnneiss  23056  neitr  23118  restntr  23120  cnpnei  23202  imasnopn  23628  cnextcn  24005  utopreg  24191  ist0cld  33864  opnregcld  36348  ptrecube  37644  poimirlem29  37673  poimir  37677  seposep  48900  iscnrm3rlem7  48920