Theorem toponss 21535

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

Syntax hints:   → wi 4   ∧ wa 398   = wceq 1537   ∈ wcel 2114   ⊆ wss 3936  ∪ cuni 4838  ‘cfv 6355  TopOnctopon 21518

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1796  ax-4 1810  ax-5 1911  ax-6 1970  ax-7 2015  ax-8 2116  ax-9 2124  ax-10 2145  ax-11 2161  ax-12 2177  ax-ext 2793  ax-sep 5203  ax-nul 5210  ax-pow 5266  ax-pr 5330  ax-un 7461

This theorem depends on definitions:  df-bi 209  df-an 399  df-or 844  df-3an 1085  df-tru 1540  df-ex 1781  df-nf 1785  df-sb 2070  df-mo 2622  df-eu 2654  df-clab 2800  df-cleq 2814  df-clel 2893  df-nfc 2963  df-ral 3143  df-rex 3144  df-rab 3147  df-v 3496  df-sbc 3773  df-dif 3939  df-un 3941  df-in 3943  df-ss 3952  df-nul 4292  df-if 4468  df-pw 4541  df-sn 4568  df-pr 4570  df-op 4574  df-uni 4839  df-br 5067  df-opab 5129  df-mpt 5147  df-id 5460  df-xp 5561  df-rel 5562  df-cnv 5563  df-co 5564  df-dm 5565  df-iota 6314  df-fun 6357  df-fv 6363  df-topon 21519

This theorem is referenced by:  en2top  21593  neiptopreu  21741  iscnp3  21852  cnntr  21883  cncnp  21888  isreg2  21985  connsub  22029  iunconnlem  22035  conncompclo  22043  1stccnp  22070  kgenidm  22155  tx1cn  22217  tx2cn  22218  xkoccn  22227  txcnp  22228  ptcnplem  22229  xkoinjcn  22295  idqtop  22314  qtopss  22323  kqfvima  22338  kqsat  22339  kqreglem1  22349  kqreglem2  22350  qtopf1  22424  fbflim  22584  flimcf  22590  flimrest  22591  isflf  22601  fclscf  22633  subgntr  22715  ghmcnp  22723  qustgpopn  22728  qustgplem  22729  tsmsxplem1  22761  tsmsxp  22763  ressusp  22874  mopnss  23056  xrtgioo  23414  lebnumlem2  23566  cfilfcls  23877  iscmet3lem2  23895  dvres3a  24512  dvmptfsum  24572  dvcnvlem  24573  dvcnv  24574  efopn  25241  txomap  31098  cnllysconn  32492  cvmlift2lem9a  32550  icccncfext  42190  dvmptconst  42219  dvmptidg  42221  qndenserrnopnlem  42602  opnvonmbllem2  42935