Theorem toponss 22812

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

Syntax hints:   → wi 4   ∧ wa 395   = wceq 1540   ∈ wcel 2109   ⊆ wss 3903  ∪ cuni 4858  ‘cfv 6482  TopOnctopon 22795

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1795  ax-4 1809  ax-5 1910  ax-6 1967  ax-7 2008  ax-8 2111  ax-9 2119  ax-10 2142  ax-11 2158  ax-12 2178  ax-ext 2701  ax-sep 5235  ax-nul 5245  ax-pow 5304  ax-pr 5371  ax-un 7671

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 848  df-3an 1088  df-tru 1543  df-fal 1553  df-ex 1780  df-nf 1784  df-sb 2066  df-mo 2533  df-eu 2562  df-clab 2708  df-cleq 2721  df-clel 2803  df-nfc 2878  df-ral 3045  df-rex 3054  df-rab 3395  df-v 3438  df-dif 3906  df-un 3908  df-in 3910  df-ss 3920  df-nul 4285  df-if 4477  df-pw 4553  df-sn 4578  df-pr 4580  df-op 4584  df-uni 4859  df-br 5093  df-opab 5155  df-mpt 5174  df-id 5514  df-xp 5625  df-rel 5626  df-cnv 5627  df-co 5628  df-dm 5629  df-iota 6438  df-fun 6484  df-fv 6490  df-topon 22796

This theorem is referenced by:  en2top  22870  neiptopreu  23018  iscnp3  23129  cnntr  23160  cncnp  23165  isreg2  23262  connsub  23306  iunconnlem  23312  conncompclo  23320  1stccnp  23347  kgenidm  23432  tx1cn  23494  tx2cn  23495  xkoccn  23504  txcnp  23505  ptcnplem  23506  xkoinjcn  23572  idqtop  23591  qtopss  23600  kqfvima  23615  kqsat  23616  kqreglem1  23626  kqreglem2  23627  qtopf1  23701  fbflim  23861  flimcf  23867  flimrest  23868  isflf  23878  fclscf  23910  subgntr  23992  ghmcnp  24000  qustgpopn  24005  qustgplem  24006  tsmsxplem1  24038  tsmsxp  24040  ressusp  24150  mopnss  24332  xrtgioo  24693  lebnumlem2  24859  cfilfcls  25172  iscmet3lem2  25190  dvres3a  25813  dvmptfsum  25877  dvcnvlem  25878  dvcnv  25879  efopn  26565  txomap  33801  cnllysconn  35218  cvmlift2lem9a  35276  icccncfext  45868  dvmptconst  45896  dvmptidg  45898  qndenserrnopnlem  46278  opnvonmbllem2  46614