Theorem ntrss2 23041

Description: A subset includes its interior. (Contributed by NM, 3-Oct-2007.) (Revised by Mario Carneiro, 11-Nov-2013.)

Hypothesis

Ref	Expression
clscld.1	⊢ 𝑋 = ∪ 𝐽

Assertion

Ref	Expression
ntrss2	⊢ ((𝐽 ∈ Top ∧ 𝑆 ⊆ 𝑋) → ((int‘𝐽)‘𝑆) ⊆ 𝑆)

Proof of Theorem ntrss2

Step	Hyp	Ref	Expression
1		clscld.1	. . 3 ⊢ 𝑋 = ∪ 𝐽
2	1	ntrval 23020	. 2 ⊢ ((𝐽 ∈ Top ∧ 𝑆 ⊆ 𝑋) → ((int‘𝐽)‘𝑆) = ∪ (𝐽 ∩ 𝒫 𝑆))
3		inss2 4167	. . . 4 ⊢ (𝐽 ∩ 𝒫 𝑆) ⊆ 𝒫 𝑆
4	3	unissi 4848	. . 3 ⊢ ∪ (𝐽 ∩ 𝒫 𝑆) ⊆ ∪ 𝒫 𝑆
5		unipw 5390	. . 3 ⊢ ∪ 𝒫 𝑆 = 𝑆
6	4, 5	sseqtri 3963	. 2 ⊢ ∪ (𝐽 ∩ 𝒫 𝑆) ⊆ 𝑆
7	2, 6	eqsstrdi 3959	1 ⊢ ((𝐽 ∈ Top ∧ 𝑆 ⊆ 𝑋) → ((int‘𝐽)‘𝑆) ⊆ 𝑆)

Syntax hints:   → wi 4   ∧ wa 396   = wceq 1547   ∈ wcel 2119   ∩ cin 3882   ⊆ wss 3883  𝒫 cpw 4530  ∪ cuni 4839  ‘cfv 6486  Topctop 22877  intcnt 23001

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1802  ax-4 1816  ax-5 1917  ax-6 1974  ax-7 2015  ax-8 2121  ax-9 2129  ax-10 2152  ax-11 2168  ax-12 2189  ax-ext 2711  ax-rep 5200  ax-sep 5219  ax-nul 5229  ax-pow 5295  ax-pr 5363  ax-un 7679

This theorem depends on definitions:  df-bi 208  df-an 397  df-or 854  df-3an 1094  df-tru 1550  df-fal 1560  df-ex 1787  df-nf 1791  df-sb 2074  df-mo 2543  df-eu 2573  df-clab 2718  df-cleq 2731  df-clel 2814  df-nfc 2888  df-ne 2935  df-ral 3054  df-rex 3064  df-reu 3345  df-rab 3392  df-v 3433  df-sbc 3724  df-csb 3832  df-dif 3886  df-un 3888  df-in 3890  df-ss 3900  df-nul 4263  df-if 4456  df-pw 4532  df-sn 4557  df-pr 4559  df-op 4563  df-uni 4840  df-iun 4924  df-br 5074  df-opab 5136  df-mpt 5155  df-id 5514  df-xp 5625  df-rel 5626  df-cnv 5627  df-co 5628  df-dm 5629  df-rn 5630  df-res 5631  df-ima 5632  df-iota 6442  df-fun 6488  df-fn 6489  df-f 6490  df-f1 6491  df-fo 6492  df-f1o 6493  df-fv 6494  df-top 22878  df-ntr 23004

This theorem is referenced by:  ntrin  23045  neiint  23088  opnnei  23104  topssnei  23108  maxlp  23131  restntr  23166  iscnp4  23247  cnntri  23255  cnntr  23259  cnprest  23273  llycmpkgen2  23534  xkococnlem  23643  flimopn  23959  fclsneii  24001  fcfnei  24019  subgntr  24091  iccntr  24806  rectbntr0  24817  bcthlem5  25314  limcflf  25867  dvbss  25887  perfdvf  25889  dvreslem  25895  dvcnp2  25906  dvnres  25917  dvaddbr  25924  dvcmulf  25931  dvmptres2  25948  dvmptcmul  25950  dvmptntr  25957  dvcnvre  26005  taylthlem1  26357  taylthlem2  26358  ulmdvlem3  26386  lgamucov2  27021  ubthlem1  30960  kur14lem6  35448  cvmlift2lem12  35551  opnbnd  36562  opnregcld  36567  cldregopn  36568  dvresntr  46369