Theorem toponss 22182

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 4890	. . 3 ⊢ (𝐴 ∈ 𝐽 → 𝐴 ⊆ ∪ 𝐽)
2	1	adantl 483	. 2 ⊢ ((𝐽 ∈ (TopOn‘𝑋) ∧ 𝐴 ∈ 𝐽) → 𝐴 ⊆ ∪ 𝐽)
3		toponuni 22169	. . 3 ⊢ (𝐽 ∈ (TopOn‘𝑋) → 𝑋 = ∪ 𝐽)
4	3	adantr 482	. 2 ⊢ ((𝐽 ∈ (TopOn‘𝑋) ∧ 𝐴 ∈ 𝐽) → 𝑋 = ∪ 𝐽)
5	2, 4	sseqtrrd 3977	1 ⊢ ((𝐽 ∈ (TopOn‘𝑋) ∧ 𝐴 ∈ 𝐽) → 𝐴 ⊆ 𝑋)

Syntax hints:   → wi 4   ∧ wa 397   = wceq 1541   ∈ wcel 2106   ⊆ wss 3902  ∪ cuni 4857  ‘cfv 6484  TopOnctopon 22165

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 1913  ax-6 1971  ax-7 2011  ax-8 2108  ax-9 2116  ax-10 2137  ax-11 2154  ax-12 2171  ax-ext 2708  ax-sep 5248  ax-nul 5255  ax-pow 5313  ax-pr 5377  ax-un 7655

This theorem depends on definitions:  df-bi 206  df-an 398  df-or 846  df-3an 1089  df-tru 1544  df-fal 1554  df-ex 1782  df-nf 1786  df-sb 2068  df-mo 2539  df-eu 2568  df-clab 2715  df-cleq 2729  df-clel 2815  df-nfc 2887  df-ral 3063  df-rex 3072  df-rab 3405  df-v 3444  df-dif 3905  df-un 3907  df-in 3909  df-ss 3919  df-nul 4275  df-if 4479  df-pw 4554  df-sn 4579  df-pr 4581  df-op 4585  df-uni 4858  df-br 5098  df-opab 5160  df-mpt 5181  df-id 5523  df-xp 5631  df-rel 5632  df-cnv 5633  df-co 5634  df-dm 5635  df-iota 6436  df-fun 6486  df-fv 6492  df-topon 22166

This theorem is referenced by:  en2top  22241  neiptopreu  22390  iscnp3  22501  cnntr  22532  cncnp  22537  isreg2  22634  connsub  22678  iunconnlem  22684  conncompclo  22692  1stccnp  22719  kgenidm  22804  tx1cn  22866  tx2cn  22867  xkoccn  22876  txcnp  22877  ptcnplem  22878  xkoinjcn  22944  idqtop  22963  qtopss  22972  kqfvima  22987  kqsat  22988  kqreglem1  22998  kqreglem2  22999  qtopf1  23073  fbflim  23233  flimcf  23239  flimrest  23240  isflf  23250  fclscf  23282  subgntr  23364  ghmcnp  23372  qustgpopn  23377  qustgplem  23378  tsmsxplem1  23410  tsmsxp  23412  ressusp  23522  mopnss  23705  xrtgioo  24075  lebnumlem2  24231  cfilfcls  24544  iscmet3lem2  24562  dvres3a  25184  dvmptfsum  25245  dvcnvlem  25246  dvcnv  25247  efopn  25919  txomap  32080  cnllysconn  33504  cvmlift2lem9a  33562  icccncfext  43814  dvmptconst  43842  dvmptidg  43844  qndenserrnopnlem  44224  opnvonmbllem2  44558