Metamath Proof Explorer

Theorem funssres

Description: The restriction of a function to the domain of a subclass equals the subclass. (Contributed by NM, 15-Aug-1994)

Ref Expression
Assertion funssres 
|- ( ( Fun F /\ G C_ F ) -> ( F |` dom G ) = G )

Proof

Step Hyp Ref Expression
1 vex 
 |-  x e. _V
2 vex 
 |-  y e. _V
3 1 2 opeldm 
 |-  ( <. x , y >. e. G -> x e. dom G )
4 3 a1i 
 |-  ( G C_ F -> ( <. x , y >. e. G -> x e. dom G ) )
5 ssel 
 |-  ( G C_ F -> ( <. x , y >. e. G -> <. x , y >. e. F ) )
6 4 5 jcad 
 |-  ( G C_ F -> ( <. x , y >. e. G -> ( x e. dom G /\ <. x , y >. e. F ) ) )
7 6 adantl 
 |-  ( ( Fun F /\ G C_ F ) -> ( <. x , y >. e. G -> ( x e. dom G /\ <. x , y >. e. F ) ) )
8 funeu2 
 |-  ( ( Fun F /\ <. x , y >. e. F ) -> E! y <. x , y >. e. F )
9 1 eldm2 
 |-  ( x e. dom G <-> E. y <. x , y >. e. G )
10 5 ancrd 
 |-  ( G C_ F -> ( <. x , y >. e. G -> ( <. x , y >. e. F /\ <. x , y >. e. G ) ) )
11 10 eximdv 
 |-  ( G C_ F -> ( E. y <. x , y >. e. G -> E. y ( <. x , y >. e. F /\ <. x , y >. e. G ) ) )
12 9 11 syl5bi 
 |-  ( G C_ F -> ( x e. dom G -> E. y ( <. x , y >. e. F /\ <. x , y >. e. G ) ) )
13 12 imp 
 |-  ( ( G C_ F /\ x e. dom G ) -> E. y ( <. x , y >. e. F /\ <. x , y >. e. G ) )
14 eupick 
 |-  ( ( E! y <. x , y >. e. F /\ E. y ( <. x , y >. e. F /\ <. x , y >. e. G ) ) -> ( <. x , y >. e. F -> <. x , y >. e. G ) )
15 8 13 14 syl2an 
 |-  ( ( ( Fun F /\ <. x , y >. e. F ) /\ ( G C_ F /\ x e. dom G ) ) -> ( <. x , y >. e. F -> <. x , y >. e. G ) )
16 15 exp43 
 |-  ( Fun F -> ( <. x , y >. e. F -> ( G C_ F -> ( x e. dom G -> ( <. x , y >. e. F -> <. x , y >. e. G ) ) ) ) )
17 16 com23 
 |-  ( Fun F -> ( G C_ F -> ( <. x , y >. e. F -> ( x e. dom G -> ( <. x , y >. e. F -> <. x , y >. e. G ) ) ) ) )
18 17 imp 
 |-  ( ( Fun F /\ G C_ F ) -> ( <. x , y >. e. F -> ( x e. dom G -> ( <. x , y >. e. F -> <. x , y >. e. G ) ) ) )
19 18 com34 
 |-  ( ( Fun F /\ G C_ F ) -> ( <. x , y >. e. F -> ( <. x , y >. e. F -> ( x e. dom G -> <. x , y >. e. G ) ) ) )
20 19 pm2.43d 
 |-  ( ( Fun F /\ G C_ F ) -> ( <. x , y >. e. F -> ( x e. dom G -> <. x , y >. e. G ) ) )
21 20 impcomd 
 |-  ( ( Fun F /\ G C_ F ) -> ( ( x e. dom G /\ <. x , y >. e. F ) -> <. x , y >. e. G ) )
22 7 21 impbid 
 |-  ( ( Fun F /\ G C_ F ) -> ( <. x , y >. e. G <-> ( x e. dom G /\ <. x , y >. e. F ) ) )
23 2 opelresi 
 |-  ( <. x , y >. e. ( F |` dom G ) <-> ( x e. dom G /\ <. x , y >. e. F ) )
24 22 23 syl6rbbr 
 |-  ( ( Fun F /\ G C_ F ) -> ( <. x , y >. e. ( F |` dom G ) <-> <. x , y >. e. G ) )
25 24 alrimivv 
 |-  ( ( Fun F /\ G C_ F ) -> A. x A. y ( <. x , y >. e. ( F |` dom G ) <-> <. x , y >. e. G ) )
26 relres 
 |-  Rel ( F |` dom G )
27 funrel 
 |-  ( Fun F -> Rel F )
28 relss 
 |-  ( G C_ F -> ( Rel F -> Rel G ) )
29 27 28 mpan9 
 |-  ( ( Fun F /\ G C_ F ) -> Rel G )
30 eqrel 
 |-  ( ( Rel ( F |` dom G ) /\ Rel G ) -> ( ( F |` dom G ) = G <-> A. x A. y ( <. x , y >. e. ( F |` dom G ) <-> <. x , y >. e. G ) ) )
31 26 29 30 sylancr 
 |-  ( ( Fun F /\ G C_ F ) -> ( ( F |` dom G ) = G <-> A. x A. y ( <. x , y >. e. ( F |` dom G ) <-> <. x , y >. e. G ) ) )
32 25 31 mpbird 
 |-  ( ( Fun F /\ G C_ F ) -> ( F |` dom G ) = G )