Theorem eltopss 21651

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

Syntax hints:   → wi 4   ∧ wa 399   = wceq 1542   ∈ wcel 2113   ⊆ wss 3841  ∪ cuni 4793  Topctop 21637

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1802  ax-4 1816  ax-5 1916  ax-6 1974  ax-7 2019  ax-8 2115  ax-9 2123  ax-ext 2710

This theorem depends on definitions:  df-bi 210  df-an 400  df-tru 1545  df-ex 1787  df-sb 2074  df-clab 2717  df-cleq 2730  df-clel 2811  df-v 3399  df-in 3848  df-ss 3858  df-uni 4794

This theorem is referenced by:  riinopn  21652  opncld  21777  ntrval2  21795  ntrss3  21804  cmclsopn  21806  opncldf1  21828  opnneissb  21858  opnssneib  21859  opnneiss  21862  neitr  21924  restntr  21926  cnpnei  22008  imasnopn  22434  cnextcn  22811  utopreg  22997  ist0cld  31347  opnregcld  34149  ptrecube  35389  poimirlem29  35418  poimir  35422  seposep  45725  iscnrm3rlem7  45746