Theorem toponss 22883

Description: A member of a topology is a subset of its underlying set. (Contributed by Mario Carneiro, 21-Aug-2015.)

Assertion

Ref	Expression
toponss	⊢ ((𝐽 ∈ (TopOn‘𝑋) ∧ 𝐴 ∈ 𝐽) → 𝐴 ⊆ 𝑋)

Proof of Theorem toponss

Step	Hyp	Ref	Expression
1		elssuni 4896	. . 3 ⊢ (𝐴 ∈ 𝐽 → 𝐴 ⊆ ∪ 𝐽)
2	1	adantl 481	. 2 ⊢ ((𝐽 ∈ (TopOn‘𝑋) ∧ 𝐴 ∈ 𝐽) → 𝐴 ⊆ ∪ 𝐽)
3		toponuni 22870	. . 3 ⊢ (𝐽 ∈ (TopOn‘𝑋) → 𝑋 = ∪ 𝐽)
4	3	adantr 480	. 2 ⊢ ((𝐽 ∈ (TopOn‘𝑋) ∧ 𝐴 ∈ 𝐽) → 𝑋 = ∪ 𝐽)
5	2, 4	sseqtrrd 3973	1 ⊢ ((𝐽 ∈ (TopOn‘𝑋) ∧ 𝐴 ∈ 𝐽) → 𝐴 ⊆ 𝑋)

Syntax hints:   → wi 4   ∧ wa 395   = wceq 1542   ∈ wcel 2114   ⊆ wss 3903  ∪ cuni 4865  ‘cfv 6500  TopOnctopon 22866

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1797  ax-4 1811  ax-5 1912  ax-6 1969  ax-7 2010  ax-8 2116  ax-9 2124  ax-10 2147  ax-11 2163  ax-12 2185  ax-ext 2709  ax-sep 5243  ax-nul 5253  ax-pow 5312  ax-pr 5379  ax-un 7690

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 849  df-3an 1089  df-tru 1545  df-fal 1555  df-ex 1782  df-nf 1786  df-sb 2069  df-mo 2540  df-eu 2570  df-clab 2716  df-cleq 2729  df-clel 2812  df-nfc 2886  df-ne 2934  df-ral 3053  df-rex 3063  df-rab 3402  df-v 3444  df-dif 3906  df-un 3908  df-in 3910  df-ss 3920  df-nul 4288  df-if 4482  df-pw 4558  df-sn 4583  df-pr 4585  df-op 4589  df-uni 4866  df-br 5101  df-opab 5163  df-mpt 5182  df-id 5527  df-xp 5638  df-rel 5639  df-cnv 5640  df-co 5641  df-dm 5642  df-iota 6456  df-fun 6502  df-fv 6508  df-topon 22867

This theorem is referenced by:  en2top  22941  neiptopreu  23089  iscnp3  23200  cnntr  23231  cncnp  23236  isreg2  23333  connsub  23377  iunconnlem  23383  conncompclo  23391  1stccnp  23418  kgenidm  23503  tx1cn  23565  tx2cn  23566  xkoccn  23575  txcnp  23576  ptcnplem  23577  xkoinjcn  23643  idqtop  23662  qtopss  23671  kqfvima  23686  kqsat  23687  kqreglem1  23697  kqreglem2  23698  qtopf1  23772  fbflim  23932  flimcf  23938  flimrest  23939  isflf  23949  fclscf  23981  subgntr  24063  ghmcnp  24071  qustgpopn  24076  qustgplem  24077  tsmsxplem1  24109  tsmsxp  24111  ressusp  24220  mopnss  24402  xrtgioo  24763  lebnumlem2  24929  cfilfcls  25242  iscmet3lem2  25260  dvres3a  25883  dvmptfsum  25947  dvcnvlem  25948  dvcnv  25949  efopn  26635  txomap  34012  cnllysconn  35461  cvmlift2lem9a  35519  icccncfext  46245  dvmptconst  46273  dvmptidg  46275  qndenserrnopnlem  46655  opnvonmbllem2  46991