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

Theorem resiexg 6712
Description: The existence of a restricted identity function, proved without using the Axiom of Replacement (unlike resfunexg 6119). (Contributed by NM, 13-Jan-2007.)
Assertion
Ref Expression
resiexg  |-  ( A  e.  V  ->  (  _I  |`  A )  e. 
_V )

Proof of Theorem resiexg
Dummy variables  x  y are mutually distinct and distinct from all other variables.
StepHypRef Expression
1 relres 5294 . . 3  |-  Rel  (  _I  |`  A )
2 simpr 461 . . . . 5  |-  ( ( x  =  y  /\  x  e.  A )  ->  x  e.  A )
3 eleq1 2534 . . . . . 6  |-  ( x  =  y  ->  (
x  e.  A  <->  y  e.  A ) )
43biimpa 484 . . . . 5  |-  ( ( x  =  y  /\  x  e.  A )  ->  y  e.  A )
52, 4jca 532 . . . 4  |-  ( ( x  =  y  /\  x  e.  A )  ->  ( x  e.  A  /\  y  e.  A
) )
6 vex 3111 . . . . . 6  |-  y  e. 
_V
76opelres 5272 . . . . 5  |-  ( <.
x ,  y >.  e.  (  _I  |`  A )  <-> 
( <. x ,  y
>.  e.  _I  /\  x  e.  A ) )
8 df-br 4443 . . . . . . 7  |-  ( x  _I  y  <->  <. x ,  y >.  e.  _I  )
96ideq 5148 . . . . . . 7  |-  ( x  _I  y  <->  x  =  y )
108, 9bitr3i 251 . . . . . 6  |-  ( <.
x ,  y >.  e.  _I  <->  x  =  y
)
1110anbi1i 695 . . . . 5  |-  ( (
<. x ,  y >.  e.  _I  /\  x  e.  A )  <->  ( x  =  y  /\  x  e.  A ) )
127, 11bitri 249 . . . 4  |-  ( <.
x ,  y >.  e.  (  _I  |`  A )  <-> 
( x  =  y  /\  x  e.  A
) )
13 opelxp 5023 . . . 4  |-  ( <.
x ,  y >.  e.  ( A  X.  A
)  <->  ( x  e.  A  /\  y  e.  A ) )
145, 12, 133imtr4i 266 . . 3  |-  ( <.
x ,  y >.  e.  (  _I  |`  A )  ->  <. x ,  y
>.  e.  ( A  X.  A ) )
151, 14relssi 5087 . 2  |-  (  _I  |`  A )  C_  ( A  X.  A )
16 xpexg 6704 . . 3  |-  ( ( A  e.  V  /\  A  e.  V )  ->  ( A  X.  A
)  e.  _V )
1716anidms 645 . 2  |-  ( A  e.  V  ->  ( A  X.  A )  e. 
_V )
18 ssexg 4588 . 2  |-  ( ( (  _I  |`  A ) 
C_  ( A  X.  A )  /\  ( A  X.  A )  e. 
_V )  ->  (  _I  |`  A )  e. 
_V )
1915, 17, 18sylancr 663 1  |-  ( A  e.  V  ->  (  _I  |`  A )  e. 
_V )
Colors of variables: wff setvar class
Syntax hints:    -> wi 4    /\ wa 369    e. wcel 1762   _Vcvv 3108    C_ wss 3471   <.cop 4028   class class class wbr 4442    _I cid 4785    X. cxp 4992    |` cres 4996
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1596  ax-4 1607  ax-5 1675  ax-6 1714  ax-7 1734  ax-8 1764  ax-9 1766  ax-10 1781  ax-11 1786  ax-12 1798  ax-13 1963  ax-ext 2440  ax-sep 4563  ax-nul 4571  ax-pow 4620  ax-pr 4681  ax-un 6569
This theorem depends on definitions:  df-bi 185  df-or 370  df-an 371  df-3an 970  df-tru 1377  df-ex 1592  df-nf 1595  df-sb 1707  df-eu 2274  df-mo 2275  df-clab 2448  df-cleq 2454  df-clel 2457  df-nfc 2612  df-ne 2659  df-ral 2814  df-rex 2815  df-rab 2818  df-v 3110  df-dif 3474  df-un 3476  df-in 3478  df-ss 3485  df-nul 3781  df-if 3935  df-pw 4007  df-sn 4023  df-pr 4025  df-op 4029  df-uni 4241  df-br 4443  df-opab 4501  df-id 4790  df-xp 5000  df-rel 5001  df-res 5006
This theorem is referenced by:  ordiso  7932  wdomref  7989  dfac9  8507  ndxarg  14501  idfu2nd  15095  idfu1st  15097  idfucl  15099  setcid  15262  pf1ind  18157  islinds2  18610  ausisusgra  24020  cusgraexilem1  24130  sizeusglecusg  24150  relexp0  28515  relexpsucr  28516  eldioph2lem1  30286  eldioph2lem2  30287  dib0  35838  dicn0  35866  cdlemn11a  35881  dihord6apre  35930  dihatlat  36008  dihpN  36010
  Copyright terms: Public domain W3C validator