Theorem toponss 22949

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 4942	. . 3 ⊢ (𝐴 ∈ 𝐽 → 𝐴 ⊆ ∪ 𝐽)
2	1	adantl 481	. 2 ⊢ ((𝐽 ∈ (TopOn‘𝑋) ∧ 𝐴 ∈ 𝐽) → 𝐴 ⊆ ∪ 𝐽)
3		toponuni 22936	. . 3 ⊢ (𝐽 ∈ (TopOn‘𝑋) → 𝑋 = ∪ 𝐽)
4	3	adantr 480	. 2 ⊢ ((𝐽 ∈ (TopOn‘𝑋) ∧ 𝐴 ∈ 𝐽) → 𝑋 = ∪ 𝐽)
5	2, 4	sseqtrrd 4037	1 ⊢ ((𝐽 ∈ (TopOn‘𝑋) ∧ 𝐴 ∈ 𝐽) → 𝐴 ⊆ 𝑋)

Syntax hints:   → wi 4   ∧ wa 395   = wceq 1537   ∈ wcel 2106   ⊆ wss 3963  ∪ cuni 4912  ‘cfv 6563  TopOnctopon 22932

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1792  ax-4 1806  ax-5 1908  ax-6 1965  ax-7 2005  ax-8 2108  ax-9 2116  ax-10 2139  ax-11 2155  ax-12 2175  ax-ext 2706  ax-sep 5302  ax-nul 5312  ax-pow 5371  ax-pr 5438  ax-un 7754

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 848  df-3an 1088  df-tru 1540  df-fal 1550  df-ex 1777  df-nf 1781  df-sb 2063  df-mo 2538  df-eu 2567  df-clab 2713  df-cleq 2727  df-clel 2814  df-nfc 2890  df-ral 3060  df-rex 3069  df-rab 3434  df-v 3480  df-dif 3966  df-un 3968  df-in 3970  df-ss 3980  df-nul 4340  df-if 4532  df-pw 4607  df-sn 4632  df-pr 4634  df-op 4638  df-uni 4913  df-br 5149  df-opab 5211  df-mpt 5232  df-id 5583  df-xp 5695  df-rel 5696  df-cnv 5697  df-co 5698  df-dm 5699  df-iota 6516  df-fun 6565  df-fv 6571  df-topon 22933

This theorem is referenced by:  en2top  23008  neiptopreu  23157  iscnp3  23268  cnntr  23299  cncnp  23304  isreg2  23401  connsub  23445  iunconnlem  23451  conncompclo  23459  1stccnp  23486  kgenidm  23571  tx1cn  23633  tx2cn  23634  xkoccn  23643  txcnp  23644  ptcnplem  23645  xkoinjcn  23711  idqtop  23730  qtopss  23739  kqfvima  23754  kqsat  23755  kqreglem1  23765  kqreglem2  23766  qtopf1  23840  fbflim  24000  flimcf  24006  flimrest  24007  isflf  24017  fclscf  24049  subgntr  24131  ghmcnp  24139  qustgpopn  24144  qustgplem  24145  tsmsxplem1  24177  tsmsxp  24179  ressusp  24289  mopnss  24472  xrtgioo  24842  lebnumlem2  25008  cfilfcls  25322  iscmet3lem2  25340  dvres3a  25964  dvmptfsum  26028  dvcnvlem  26029  dvcnv  26030  efopn  26715  txomap  33795  cnllysconn  35230  cvmlift2lem9a  35288  icccncfext  45843  dvmptconst  45871  dvmptidg  45873  qndenserrnopnlem  46253  opnvonmbllem2  46589