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 )