Metamath Proof Explorer


Theorem resfunexg

Description: The restriction of a function to a set exists. Compare Proposition 6.17 of TakeutiZaring p. 28. (Contributed by NM, 7-Apr-1995) (Revised by Mario Carneiro, 22-Jun-2013)

Ref Expression
Assertion resfunexg
|- ( ( Fun A /\ B e. C ) -> ( A |` B ) e. _V )

Proof

Step Hyp Ref Expression
1 funres
 |-  ( Fun A -> Fun ( A |` B ) )
2 1 adantr
 |-  ( ( Fun A /\ B e. C ) -> Fun ( A |` B ) )
3 2 funfnd
 |-  ( ( Fun A /\ B e. C ) -> ( A |` B ) Fn dom ( A |` B ) )
4 dffn5
 |-  ( ( A |` B ) Fn dom ( A |` B ) <-> ( A |` B ) = ( x e. dom ( A |` B ) |-> ( ( A |` B ) ` x ) ) )
5 3 4 sylib
 |-  ( ( Fun A /\ B e. C ) -> ( A |` B ) = ( x e. dom ( A |` B ) |-> ( ( A |` B ) ` x ) ) )
6 fvex
 |-  ( ( A |` B ) ` x ) e. _V
7 6 fnasrn
 |-  ( x e. dom ( A |` B ) |-> ( ( A |` B ) ` x ) ) = ran ( x e. dom ( A |` B ) |-> <. x , ( ( A |` B ) ` x ) >. )
8 5 7 eqtrdi
 |-  ( ( Fun A /\ B e. C ) -> ( A |` B ) = ran ( x e. dom ( A |` B ) |-> <. x , ( ( A |` B ) ` x ) >. ) )
9 opex
 |-  <. x , ( ( A |` B ) ` x ) >. e. _V
10 eqid
 |-  ( x e. dom ( A |` B ) |-> <. x , ( ( A |` B ) ` x ) >. ) = ( x e. dom ( A |` B ) |-> <. x , ( ( A |` B ) ` x ) >. )
11 9 10 dmmpti
 |-  dom ( x e. dom ( A |` B ) |-> <. x , ( ( A |` B ) ` x ) >. ) = dom ( A |` B )
12 11 imaeq2i
 |-  ( ( x e. dom ( A |` B ) |-> <. x , ( ( A |` B ) ` x ) >. ) " dom ( x e. dom ( A |` B ) |-> <. x , ( ( A |` B ) ` x ) >. ) ) = ( ( x e. dom ( A |` B ) |-> <. x , ( ( A |` B ) ` x ) >. ) " dom ( A |` B ) )
13 imadmrn
 |-  ( ( x e. dom ( A |` B ) |-> <. x , ( ( A |` B ) ` x ) >. ) " dom ( x e. dom ( A |` B ) |-> <. x , ( ( A |` B ) ` x ) >. ) ) = ran ( x e. dom ( A |` B ) |-> <. x , ( ( A |` B ) ` x ) >. )
14 12 13 eqtr3i
 |-  ( ( x e. dom ( A |` B ) |-> <. x , ( ( A |` B ) ` x ) >. ) " dom ( A |` B ) ) = ran ( x e. dom ( A |` B ) |-> <. x , ( ( A |` B ) ` x ) >. )
15 8 14 eqtr4di
 |-  ( ( Fun A /\ B e. C ) -> ( A |` B ) = ( ( x e. dom ( A |` B ) |-> <. x , ( ( A |` B ) ` x ) >. ) " dom ( A |` B ) ) )
16 funmpt
 |-  Fun ( x e. dom ( A |` B ) |-> <. x , ( ( A |` B ) ` x ) >. )
17 dmresexg
 |-  ( B e. C -> dom ( A |` B ) e. _V )
18 17 adantl
 |-  ( ( Fun A /\ B e. C ) -> dom ( A |` B ) e. _V )
19 funimaexg
 |-  ( ( Fun ( x e. dom ( A |` B ) |-> <. x , ( ( A |` B ) ` x ) >. ) /\ dom ( A |` B ) e. _V ) -> ( ( x e. dom ( A |` B ) |-> <. x , ( ( A |` B ) ` x ) >. ) " dom ( A |` B ) ) e. _V )
20 16 18 19 sylancr
 |-  ( ( Fun A /\ B e. C ) -> ( ( x e. dom ( A |` B ) |-> <. x , ( ( A |` B ) ` x ) >. ) " dom ( A |` B ) ) e. _V )
21 15 20 eqeltrd
 |-  ( ( Fun A /\ B e. C ) -> ( A |` B ) e. _V )