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 
 |-  y e. _V
2 1 opelresi 
 |-  ( <. x , y >. e. ( F |` dom G ) <-> ( x e. dom G /\ <. x , y >. e. F ) )
3 vex 
 |-  x e. _V
4 3 1 opeldm 
 |-  ( <. x , y >. e. G -> x e. dom G )
5 4 a1i 
 |-  ( G C_ F -> ( <. x , y >. e. G -> x e. dom G ) )
6 ssel 
 |-  ( G C_ F -> ( <. x , y >. e. G -> <. x , y >. e. F ) )
7 5 6 jcad 
 |-  ( G C_ F -> ( <. x , y >. e. G -> ( x e. dom G /\ <. x , y >. e. F ) ) )
8 7 adantl 
 |-  ( ( Fun F /\ G C_ F ) -> ( <. x , y >. e. G -> ( x e. dom G /\ <. x , y >. e. F ) ) )
9 funeu2 
 |-  ( ( Fun F /\ <. x , y >. e. F ) -> E! y <. x , y >. e. F )
10 3 eldm2 
 |-  ( x e. dom G <-> E. y <. x , y >. e. G )
11 6 ancrd 
 |-  ( G C_ F -> ( <. x , y >. e. G -> ( <. x , y >. e. F /\ <. x , y >. e. G ) ) )
12 11 eximdv 
 |-  ( G C_ F -> ( E. y <. x , y >. e. G -> E. y ( <. x , y >. e. F /\ <. x , y >. e. G ) ) )
13 10 12 syl5bi 
 |-  ( G C_ F -> ( x e. dom G -> E. y ( <. x , y >. e. F /\ <. x , y >. e. G ) ) )
14 13 imp 
 |-  ( ( G C_ F /\ x e. dom G ) -> E. y ( <. x , y >. e. F /\ <. x , y >. e. G ) )
15 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 ) )
16 9 14 15 syl2an 
 |-  ( ( ( Fun F /\ <. x , y >. e. F ) /\ ( G C_ F /\ x e. dom G ) ) -> ( <. x , y >. e. F -> <. x , y >. e. G ) )
17 16 exp43 
 |-  ( Fun F -> ( <. x , y >. e. F -> ( G C_ F -> ( x e. dom G -> ( <. x , y >. e. F -> <. x , y >. e. G ) ) ) ) )
18 17 com23 
 |-  ( Fun F -> ( G C_ F -> ( <. x , y >. e. F -> ( x e. dom G -> ( <. x , y >. e. F -> <. x , y >. e. G ) ) ) ) )
19 18 imp 
 |-  ( ( Fun F /\ G C_ F ) -> ( <. x , y >. e. F -> ( x e. dom G -> ( <. x , y >. e. F -> <. x , y >. e. G ) ) ) )
20 19 com34 
 |-  ( ( Fun F /\ G C_ F ) -> ( <. x , y >. e. F -> ( <. x , y >. e. F -> ( x e. dom G -> <. x , y >. e. G ) ) ) )
21 20 pm2.43d 
 |-  ( ( Fun F /\ G C_ F ) -> ( <. x , y >. e. F -> ( x e. dom G -> <. x , y >. e. G ) ) )
22 21 impcomd 
 |-  ( ( Fun F /\ G C_ F ) -> ( ( x e. dom G /\ <. x , y >. e. F ) -> <. x , y >. e. G ) )
23 8 22 impbid 
 |-  ( ( Fun F /\ G C_ F ) -> ( <. x , y >. e. G <-> ( x e. dom G /\ <. x , y >. e. F ) ) )
24 2 23 bitr4id 
 |-  ( ( 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 )