MPE Home Metamath Proof Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >  ntrss2 Structured version   Unicode version

Theorem ntrss2 18661
Description: A subset includes its interior. (Contributed by NM, 3-Oct-2007.) (Revised by Mario Carneiro, 11-Nov-2013.)
Hypothesis
Ref Expression
clscld.1  |-  X  = 
U. J
Assertion
Ref Expression
ntrss2  |-  ( ( J  e.  Top  /\  S  C_  X )  -> 
( ( int `  J
) `  S )  C_  S )

Proof of Theorem ntrss2
StepHypRef Expression
1 clscld.1 . . 3  |-  X  = 
U. J
21ntrval 18640 . 2  |-  ( ( J  e.  Top  /\  S  C_  X )  -> 
( ( int `  J
) `  S )  =  U. ( J  i^i  ~P S ) )
3 inss2 3571 . . . 4  |-  ( J  i^i  ~P S ) 
C_  ~P S
43unissi 4114 . . 3  |-  U. ( J  i^i  ~P S ) 
C_  U. ~P S
5 unipw 4542 . . 3  |-  U. ~P S  =  S
64, 5sseqtri 3388 . 2  |-  U. ( J  i^i  ~P S ) 
C_  S
72, 6syl6eqss 3406 1  |-  ( ( J  e.  Top  /\  S  C_  X )  -> 
( ( int `  J
) `  S )  C_  S )
Colors of variables: wff setvar class
Syntax hints:    -> wi 4    /\ wa 369    = wceq 1369    e. wcel 1756    i^i cin 3327    C_ wss 3328   ~Pcpw 3860   U.cuni 4091   ` cfv 5418   Topctop 18498   intcnt 18621
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1591  ax-4 1602  ax-5 1670  ax-6 1708  ax-7 1728  ax-8 1758  ax-9 1760  ax-10 1775  ax-11 1780  ax-12 1792  ax-13 1943  ax-ext 2423  ax-rep 4403  ax-sep 4413  ax-nul 4421  ax-pow 4470  ax-pr 4531  ax-un 6372
This theorem depends on definitions:  df-bi 185  df-or 370  df-an 371  df-3an 967  df-tru 1372  df-ex 1587  df-nf 1590  df-sb 1701  df-eu 2257  df-mo 2258  df-clab 2430  df-cleq 2436  df-clel 2439  df-nfc 2568  df-ne 2608  df-ral 2720  df-rex 2721  df-reu 2722  df-rab 2724  df-v 2974  df-sbc 3187  df-csb 3289  df-dif 3331  df-un 3333  df-in 3335  df-ss 3342  df-nul 3638  df-if 3792  df-pw 3862  df-sn 3878  df-pr 3880  df-op 3884  df-uni 4092  df-iun 4173  df-br 4293  df-opab 4351  df-mpt 4352  df-id 4636  df-xp 4846  df-rel 4847  df-cnv 4848  df-co 4849  df-dm 4850  df-rn 4851  df-res 4852  df-ima 4853  df-iota 5381  df-fun 5420  df-fn 5421  df-f 5422  df-f1 5423  df-fo 5424  df-f1o 5425  df-fv 5426  df-top 18503  df-ntr 18624
This theorem is referenced by:  ntrin  18665  neiint  18708  opnnei  18724  topssnei  18728  maxlp  18751  restntr  18786  iscnp4  18867  cnntri  18875  cnntr  18879  cnprest  18893  llycmpkgen2  19123  xkococnlem  19232  flimopn  19548  fclsneii  19590  fcfnei  19608  subgntr  19677  iccntr  20398  rectbntr0  20409  bcthlem5  20839  limcflf  21356  dvbss  21376  perfdvf  21378  dvreslem  21384  dvcnp2  21394  dvnres  21405  dvaddbr  21412  dvcmulf  21419  dvmptres2  21436  dvmptcmul  21438  dvmptntr  21445  dvcnvre  21491  taylthlem1  21838  taylthlem2  21839  ulmdvlem3  21867  ubthlem1  24271  lgamucov2  27025  kur14lem6  27099  cvmlift2lem12  27203  opnbnd  28520  opnregcld  28525  cldregopn  28526
  Copyright terms: Public domain W3C validator