Theorem toponss 21778

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 4837	. . 3 ⊢ (𝐴 ∈ 𝐽 → 𝐴 ⊆ ∪ 𝐽)
2	1	adantl 485	. 2 ⊢ ((𝐽 ∈ (TopOn‘𝑋) ∧ 𝐴 ∈ 𝐽) → 𝐴 ⊆ ∪ 𝐽)
3		toponuni 21765	. . 3 ⊢ (𝐽 ∈ (TopOn‘𝑋) → 𝑋 = ∪ 𝐽)
4	3	adantr 484	. 2 ⊢ ((𝐽 ∈ (TopOn‘𝑋) ∧ 𝐴 ∈ 𝐽) → 𝑋 = ∪ 𝐽)
5	2, 4	sseqtrrd 3928	1 ⊢ ((𝐽 ∈ (TopOn‘𝑋) ∧ 𝐴 ∈ 𝐽) → 𝐴 ⊆ 𝑋)

Syntax hints:   → wi 4   ∧ wa 399   = wceq 1543   ∈ wcel 2112   ⊆ wss 3853  ∪ cuni 4805  ‘cfv 6358  TopOnctopon 21761

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1803  ax-4 1817  ax-5 1918  ax-6 1976  ax-7 2018  ax-8 2114  ax-9 2122  ax-10 2143  ax-11 2160  ax-12 2177  ax-ext 2708  ax-sep 5177  ax-nul 5184  ax-pow 5243  ax-pr 5307  ax-un 7501

This theorem depends on definitions:  df-bi 210  df-an 400  df-or 848  df-3an 1091  df-tru 1546  df-fal 1556  df-ex 1788  df-nf 1792  df-sb 2073  df-mo 2539  df-eu 2568  df-clab 2715  df-cleq 2728  df-clel 2809  df-nfc 2879  df-ne 2933  df-ral 3056  df-rex 3057  df-rab 3060  df-v 3400  df-sbc 3684  df-dif 3856  df-un 3858  df-in 3860  df-ss 3870  df-nul 4224  df-if 4426  df-pw 4501  df-sn 4528  df-pr 4530  df-op 4534  df-uni 4806  df-br 5040  df-opab 5102  df-mpt 5121  df-id 5440  df-xp 5542  df-rel 5543  df-cnv 5544  df-co 5545  df-dm 5546  df-iota 6316  df-fun 6360  df-fv 6366  df-topon 21762

This theorem is referenced by:  en2top  21836  neiptopreu  21984  iscnp3  22095  cnntr  22126  cncnp  22131  isreg2  22228  connsub  22272  iunconnlem  22278  conncompclo  22286  1stccnp  22313  kgenidm  22398  tx1cn  22460  tx2cn  22461  xkoccn  22470  txcnp  22471  ptcnplem  22472  xkoinjcn  22538  idqtop  22557  qtopss  22566  kqfvima  22581  kqsat  22582  kqreglem1  22592  kqreglem2  22593  qtopf1  22667  fbflim  22827  flimcf  22833  flimrest  22834  isflf  22844  fclscf  22876  subgntr  22958  ghmcnp  22966  qustgpopn  22971  qustgplem  22972  tsmsxplem1  23004  tsmsxp  23006  ressusp  23116  mopnss  23298  xrtgioo  23657  lebnumlem2  23813  cfilfcls  24125  iscmet3lem2  24143  dvres3a  24765  dvmptfsum  24826  dvcnvlem  24827  dvcnv  24828  efopn  25500  txomap  31452  cnllysconn  32874  cvmlift2lem9a  32932  icccncfext  43046  dvmptconst  43074  dvmptidg  43076  qndenserrnopnlem  43456  opnvonmbllem2  43789