Theorem eltopss 22947

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

Syntax hints:   → wi 4   ∧ wa 399   = wceq 1559   ∈ wcel 2141   ⊆ wss 3904  ∪ cuni 4864  Topctop 22933

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1814  ax-4 1828  ax-5 1929  ax-6 1986  ax-7 2027  ax-8 2143  ax-9 2151  ax-ext 2733

This theorem depends on definitions:  df-bi 209  df-an 400  df-tru 1562  df-ex 1799  df-sb 2090  df-clab 2740  df-cleq 2753  df-clel 2836  df-v 3455  df-ss 3921  df-uni 4865

This theorem is referenced by:  riinopn  22948  opncld  23073  ntrval2  23091  ntrss3  23100  cmclsopn  23102  opncldf1  23124  opnneissb  23154  opnssneib  23155  opnneiss  23158  neitr  23220  restntr  23222  cnpnei  23304  imasnopn  23730  cnextcn  24107  utopreg  24292  ist0cld  34091  opnregcld  36654  ptrecube  38083  poimirlem29  38112  poimir  38116  seposep  49511  iscnrm3rlem7  49531