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

Theorem elrestr 15265
Description: Sufficient condition for being an open set in a subspace. (Contributed by Jeff Hankins, 11-Jul-2009.) (Revised by Mario Carneiro, 15-Dec-2013.)
Assertion
Ref Expression
elrestr  |-  ( ( J  e.  V  /\  S  e.  W  /\  A  e.  J )  ->  ( A  i^i  S
)  e.  ( Jt  S ) )

Proof of Theorem elrestr
Dummy variable  x is distinct from all other variables.
StepHypRef Expression
1 eqid 2423 . . . 4  |-  ( A  i^i  S )  =  ( A  i^i  S
)
2 ineq1 3595 . . . . . 6  |-  ( x  =  A  ->  (
x  i^i  S )  =  ( A  i^i  S ) )
32eqeq2d 2433 . . . . 5  |-  ( x  =  A  ->  (
( A  i^i  S
)  =  ( x  i^i  S )  <->  ( A  i^i  S )  =  ( A  i^i  S ) ) )
43rspcev 3120 . . . 4  |-  ( ( A  e.  J  /\  ( A  i^i  S )  =  ( A  i^i  S ) )  ->  E. x  e.  J  ( A  i^i  S )  =  ( x  i^i  S ) )
51, 4mpan2 675 . . 3  |-  ( A  e.  J  ->  E. x  e.  J  ( A  i^i  S )  =  ( x  i^i  S ) )
6 elrest 15264 . . 3  |-  ( ( J  e.  V  /\  S  e.  W )  ->  ( ( A  i^i  S )  e.  ( Jt  S )  <->  E. x  e.  J  ( A  i^i  S )  =  ( x  i^i 
S ) ) )
75, 6syl5ibr 224 . 2  |-  ( ( J  e.  V  /\  S  e.  W )  ->  ( A  e.  J  ->  ( A  i^i  S
)  e.  ( Jt  S ) ) )
873impia 1202 1  |-  ( ( J  e.  V  /\  S  e.  W  /\  A  e.  J )  ->  ( A  i^i  S
)  e.  ( Jt  S ) )
Colors of variables: wff setvar class
Syntax hints:    -> wi 4    /\ wa 370    /\ w3a 982    = wceq 1437    e. wcel 1872   E.wrex 2710    i^i cin 3373  (class class class)co 6244   ↾t crest 15257
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1663  ax-4 1676  ax-5 1752  ax-6 1798  ax-7 1843  ax-8 1874  ax-9 1876  ax-10 1891  ax-11 1896  ax-12 1909  ax-13 2058  ax-ext 2403  ax-rep 4474  ax-sep 4484  ax-nul 4493  ax-pr 4598  ax-un 6536
This theorem depends on definitions:  df-bi 188  df-or 371  df-an 372  df-3an 984  df-tru 1440  df-ex 1658  df-nf 1662  df-sb 1791  df-eu 2275  df-mo 2276  df-clab 2410  df-cleq 2416  df-clel 2419  df-nfc 2553  df-ne 2596  df-ral 2714  df-rex 2715  df-reu 2716  df-rab 2718  df-v 3019  df-sbc 3238  df-csb 3334  df-dif 3377  df-un 3379  df-in 3381  df-ss 3388  df-nul 3700  df-if 3850  df-sn 3937  df-pr 3939  df-op 3943  df-uni 4158  df-iun 4239  df-br 4362  df-opab 4421  df-mpt 4422  df-id 4706  df-xp 4797  df-rel 4798  df-cnv 4799  df-co 4800  df-dm 4801  df-rn 4802  df-res 4803  df-ima 4804  df-iota 5503  df-fun 5541  df-fn 5542  df-f 5543  df-f1 5544  df-fo 5545  df-f1o 5546  df-fv 5547  df-ov 6247  df-oprab 6248  df-mpt2 6249  df-rest 15259
This theorem is referenced by:  firest  15269  restbas  20111  tgrest  20112  resttopon  20114  restcld  20125  restfpw  20132  neitr  20133  restntr  20135  ordtrest  20155  cnrest  20238  lmss  20251  consubclo  20376  restnlly  20434  islly2  20436  cldllycmp  20447  lly1stc  20448  kgenss  20495  xkococnlem  20611  xkoinjcn  20639  qtoprest  20669  trfbas2  20795  trfil1  20838  trfil2  20839  fgtr  20842  trfg  20843  uzrest  20849  trufil  20862  flimrest  20935  cnextcn  21019  trust  21181  restutop  21189  trcfilu  21246  cfiluweak  21247  xrsmopn  21767  zdis  21771  xrge0tsms  21789  cnheibor  21920  cfilres  22203  lhop2  22904  psercn  23318  xrlimcnp  23831  xrge0tsmsd  28495  ordtrestNEW  28674  pnfneige0  28704  lmxrge0  28705  rrhre  28772  cvmscld  29943  cvmopnlem  29948  cvmliftmolem1  29951  poimirlem30  31877  subspopn  31988  iocopn  37513  icoopn  37518  limcresiooub  37606  limcresioolb  37607  fourierdlem32  37885  fourierdlem33  37886  fourierdlem48  37901  fourierdlem49  37902
  Copyright terms: Public domain W3C validator