This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

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 )