Metamath Proof Explorer

Theorem funressnfv

Description: A restriction to a singleton with a function value is a function under certain conditions. (Contributed by Alexander van der Vekens, 25-Jul-2017) (Proof shortened by Peter Mazsa, 2-Oct-2022)

Ref Expression
Assertion funressnfv 
|- ( ( ( X e. dom ( F o. G ) /\ Fun ( ( F o. G ) |` { X } ) ) /\ ( G Fn A /\ X e. A ) ) -> Fun ( F |` { ( G ` X ) } ) )

Proof

Step Hyp Ref Expression
1 relres 
 |-  Rel ( F |` { ( G ` X ) } )
2 1 a1i 
 |-  ( ( ( X e. dom ( F o. G ) /\ Fun ( ( F o. G ) |` { X } ) ) /\ ( G Fn A /\ X e. A ) ) -> Rel ( F |` { ( G ` X ) } ) )
3 dmfco 
 |-  ( ( Fun G /\ X e. dom G ) -> ( X e. dom ( F o. G ) <-> ( G ` X ) e. dom F ) )
4 3 biimpd 
 |-  ( ( Fun G /\ X e. dom G ) -> ( X e. dom ( F o. G ) -> ( G ` X ) e. dom F ) )
5 4 funfni 
 |-  ( ( G Fn A /\ X e. A ) -> ( X e. dom ( F o. G ) -> ( G ` X ) e. dom F ) )
6 dmressnsn 
 |-  ( ( G ` X ) e. dom F -> dom ( F |` { ( G ` X ) } ) = { ( G ` X ) } )
7 eleq2 
 |-  ( dom ( F |` { ( G ` X ) } ) = { ( G ` X ) } -> ( x e. dom ( F |` { ( G ` X ) } ) <-> x e. { ( G ` X ) } ) )
8 velsn 
 |-  ( x e. { ( G ` X ) } <-> x = ( G ` X ) )
9 dmressnsn 
 |-  ( X e. dom ( F o. G ) -> dom ( ( F o. G ) |` { X } ) = { X } )
10 dffun7 
 |-  ( Fun ( ( F o. G ) |` { X } ) <-> ( Rel ( ( F o. G ) |` { X } ) /\ A. x e. dom ( ( F o. G ) |` { X } ) E* y x ( ( F o. G ) |` { X } ) y ) )
11 snidg 
 |-  ( X e. dom ( F o. G ) -> X e. { X } )
12 11 adantl 
 |-  ( ( dom ( ( F o. G ) |` { X } ) = { X } /\ X e. dom ( F o. G ) ) -> X e. { X } )
13 eleq2 
 |-  ( { X } = dom ( ( F o. G ) |` { X } ) -> ( X e. { X } <-> X e. dom ( ( F o. G ) |` { X } ) ) )
14 13 eqcoms 
 |-  ( dom ( ( F o. G ) |` { X } ) = { X } -> ( X e. { X } <-> X e. dom ( ( F o. G ) |` { X } ) ) )
15 14 adantr 
 |-  ( ( dom ( ( F o. G ) |` { X } ) = { X } /\ X e. dom ( F o. G ) ) -> ( X e. { X } <-> X e. dom ( ( F o. G ) |` { X } ) ) )
16 12 15 mpbid 
 |-  ( ( dom ( ( F o. G ) |` { X } ) = { X } /\ X e. dom ( F o. G ) ) -> X e. dom ( ( F o. G ) |` { X } ) )
17 fvex 
 |-  ( G ` X ) e. _V
18 17 isseti 
 |-  E. z z = ( G ` X )
19 eqcom 
 |-  ( z = ( G ` X ) <-> ( G ` X ) = z )
20 fnbrfvb 
 |-  ( ( G Fn A /\ X e. A ) -> ( ( G ` X ) = z <-> X G z ) )
21 19 20 syl5bb 
 |-  ( ( G Fn A /\ X e. A ) -> ( z = ( G ` X ) <-> X G z ) )
22 21 biimpd 
 |-  ( ( G Fn A /\ X e. A ) -> ( z = ( G ` X ) -> X G z ) )
23 breq1 
 |-  ( ( G ` X ) = z -> ( ( G ` X ) F y <-> z F y ) )
24 23 eqcoms 
 |-  ( z = ( G ` X ) -> ( ( G ` X ) F y <-> z F y ) )
25 24 biimpcd 
 |-  ( ( G ` X ) F y -> ( z = ( G ` X ) -> z F y ) )
26 22 25 anim12ii 
 |-  ( ( ( G Fn A /\ X e. A ) /\ ( G ` X ) F y ) -> ( z = ( G ` X ) -> ( X G z /\ z F y ) ) )
27 26 eximdv 
 |-  ( ( ( G Fn A /\ X e. A ) /\ ( G ` X ) F y ) -> ( E. z z = ( G ` X ) -> E. z ( X G z /\ z F y ) ) )
28 18 27 mpi 
 |-  ( ( ( G Fn A /\ X e. A ) /\ ( G ` X ) F y ) -> E. z ( X G z /\ z F y ) )
29 simpr 
 |-  ( ( G Fn A /\ X e. A ) -> X e. A )
30 vex 
 |-  y e. _V
31 brcog 
 |-  ( ( X e. A /\ y e. _V ) -> ( X ( F o. G ) y <-> E. z ( X G z /\ z F y ) ) )
32 29 30 31 sylancl 
 |-  ( ( G Fn A /\ X e. A ) -> ( X ( F o. G ) y <-> E. z ( X G z /\ z F y ) ) )
33 32 adantr 
 |-  ( ( ( G Fn A /\ X e. A ) /\ ( G ` X ) F y ) -> ( X ( F o. G ) y <-> E. z ( X G z /\ z F y ) ) )
34 28 33 mpbird 
 |-  ( ( ( G Fn A /\ X e. A ) /\ ( G ` X ) F y ) -> X ( F o. G ) y )
35 30 brresi 
 |-  ( X ( ( F o. G ) |` { X } ) y <-> ( X e. { X } /\ X ( F o. G ) y ) )
36 snidg 
 |-  ( X e. A -> X e. { X } )
37 36 biantrurd 
 |-  ( X e. A -> ( X ( F o. G ) y <-> ( X e. { X } /\ X ( F o. G ) y ) ) )
38 35 37 bitr4id 
 |-  ( X e. A -> ( X ( ( F o. G ) |` { X } ) y <-> X ( F o. G ) y ) )
39 38 ad2antlr 
 |-  ( ( ( G Fn A /\ X e. A ) /\ ( G ` X ) F y ) -> ( X ( ( F o. G ) |` { X } ) y <-> X ( F o. G ) y ) )
40 34 39 mpbird 
 |-  ( ( ( G Fn A /\ X e. A ) /\ ( G ` X ) F y ) -> X ( ( F o. G ) |` { X } ) y )
41 40 ex 
 |-  ( ( G Fn A /\ X e. A ) -> ( ( G ` X ) F y -> X ( ( F o. G ) |` { X } ) y ) )
42 41 adantl 
 |-  ( ( ( ( dom ( ( F o. G ) |` { X } ) = { X } /\ X e. dom ( F o. G ) ) /\ x = X ) /\ ( G Fn A /\ X e. A ) ) -> ( ( G ` X ) F y -> X ( ( F o. G ) |` { X } ) y ) )
43 breq1 
 |-  ( X = x -> ( X ( ( F o. G ) |` { X } ) y <-> x ( ( F o. G ) |` { X } ) y ) )
44 43 eqcoms 
 |-  ( x = X -> ( X ( ( F o. G ) |` { X } ) y <-> x ( ( F o. G ) |` { X } ) y ) )
45 44 ad2antlr 
 |-  ( ( ( ( dom ( ( F o. G ) |` { X } ) = { X } /\ X e. dom ( F o. G ) ) /\ x = X ) /\ ( G Fn A /\ X e. A ) ) -> ( X ( ( F o. G ) |` { X } ) y <-> x ( ( F o. G ) |` { X } ) y ) )
46 42 45 sylibd 
 |-  ( ( ( ( dom ( ( F o. G ) |` { X } ) = { X } /\ X e. dom ( F o. G ) ) /\ x = X ) /\ ( G Fn A /\ X e. A ) ) -> ( ( G ` X ) F y -> x ( ( F o. G ) |` { X } ) y ) )
47 46 moimdv 
 |-  ( ( ( ( dom ( ( F o. G ) |` { X } ) = { X } /\ X e. dom ( F o. G ) ) /\ x = X ) /\ ( G Fn A /\ X e. A ) ) -> ( E* y x ( ( F o. G ) |` { X } ) y -> E* y ( G ` X ) F y ) )
48 47 ex 
 |-  ( ( ( dom ( ( F o. G ) |` { X } ) = { X } /\ X e. dom ( F o. G ) ) /\ x = X ) -> ( ( G Fn A /\ X e. A ) -> ( E* y x ( ( F o. G ) |` { X } ) y -> E* y ( G ` X ) F y ) ) )
49 48 com23 
 |-  ( ( ( dom ( ( F o. G ) |` { X } ) = { X } /\ X e. dom ( F o. G ) ) /\ x = X ) -> ( E* y x ( ( F o. G ) |` { X } ) y -> ( ( G Fn A /\ X e. A ) -> E* y ( G ` X ) F y ) ) )
50 16 49 rspcimdv 
 |-  ( ( dom ( ( F o. G ) |` { X } ) = { X } /\ X e. dom ( F o. G ) ) -> ( A. x e. dom ( ( F o. G ) |` { X } ) E* y x ( ( F o. G ) |` { X } ) y -> ( ( G Fn A /\ X e. A ) -> E* y ( G ` X ) F y ) ) )
51 50 ex 
 |-  ( dom ( ( F o. G ) |` { X } ) = { X } -> ( X e. dom ( F o. G ) -> ( A. x e. dom ( ( F o. G ) |` { X } ) E* y x ( ( F o. G ) |` { X } ) y -> ( ( G Fn A /\ X e. A ) -> E* y ( G ` X ) F y ) ) ) )
52 51 com13 
 |-  ( A. x e. dom ( ( F o. G ) |` { X } ) E* y x ( ( F o. G ) |` { X } ) y -> ( X e. dom ( F o. G ) -> ( dom ( ( F o. G ) |` { X } ) = { X } -> ( ( G Fn A /\ X e. A ) -> E* y ( G ` X ) F y ) ) ) )
53 10 52 simplbiim 
 |-  ( Fun ( ( F o. G ) |` { X } ) -> ( X e. dom ( F o. G ) -> ( dom ( ( F o. G ) |` { X } ) = { X } -> ( ( G Fn A /\ X e. A ) -> E* y ( G ` X ) F y ) ) ) )
54 53 com13 
 |-  ( dom ( ( F o. G ) |` { X } ) = { X } -> ( X e. dom ( F o. G ) -> ( Fun ( ( F o. G ) |` { X } ) -> ( ( G Fn A /\ X e. A ) -> E* y ( G ` X ) F y ) ) ) )
55 9 54 mpcom 
 |-  ( X e. dom ( F o. G ) -> ( Fun ( ( F o. G ) |` { X } ) -> ( ( G Fn A /\ X e. A ) -> E* y ( G ` X ) F y ) ) )
56 55 imp31 
 |-  ( ( ( X e. dom ( F o. G ) /\ Fun ( ( F o. G ) |` { X } ) ) /\ ( G Fn A /\ X e. A ) ) -> E* y ( G ` X ) F y )
57 17 snid 
 |-  ( G ` X ) e. { ( G ` X ) }
58 57 biantrur 
 |-  ( ( G ` X ) F y <-> ( ( G ` X ) e. { ( G ` X ) } /\ ( G ` X ) F y ) )
59 58 a1i 
 |-  ( ( ( X e. dom ( F o. G ) /\ Fun ( ( F o. G ) |` { X } ) ) /\ ( G Fn A /\ X e. A ) ) -> ( ( G ` X ) F y <-> ( ( G ` X ) e. { ( G ` X ) } /\ ( G ` X ) F y ) ) )
60 59 mobidv 
 |-  ( ( ( X e. dom ( F o. G ) /\ Fun ( ( F o. G ) |` { X } ) ) /\ ( G Fn A /\ X e. A ) ) -> ( E* y ( G ` X ) F y <-> E* y ( ( G ` X ) e. { ( G ` X ) } /\ ( G ` X ) F y ) ) )
61 56 60 mpbid 
 |-  ( ( ( X e. dom ( F o. G ) /\ Fun ( ( F o. G ) |` { X } ) ) /\ ( G Fn A /\ X e. A ) ) -> E* y ( ( G ` X ) e. { ( G ` X ) } /\ ( G ` X ) F y ) )
62 61 adantl 
 |-  ( ( x = ( G ` X ) /\ ( ( X e. dom ( F o. G ) /\ Fun ( ( F o. G ) |` { X } ) ) /\ ( G Fn A /\ X e. A ) ) ) -> E* y ( ( G ` X ) e. { ( G ` X ) } /\ ( G ` X ) F y ) )
63 breq1 
 |-  ( x = ( G ` X ) -> ( x ( F |` { ( G ` X ) } ) y <-> ( G ` X ) ( F |` { ( G ` X ) } ) y ) )
64 30 brresi 
 |-  ( ( G ` X ) ( F |` { ( G ` X ) } ) y <-> ( ( G ` X ) e. { ( G ` X ) } /\ ( G ` X ) F y ) )
65 63 64 bitr2di 
 |-  ( x = ( G ` X ) -> ( ( ( G ` X ) e. { ( G ` X ) } /\ ( G ` X ) F y ) <-> x ( F |` { ( G ` X ) } ) y ) )
66 65 adantr 
 |-  ( ( x = ( G ` X ) /\ ( ( X e. dom ( F o. G ) /\ Fun ( ( F o. G ) |` { X } ) ) /\ ( G Fn A /\ X e. A ) ) ) -> ( ( ( G ` X ) e. { ( G ` X ) } /\ ( G ` X ) F y ) <-> x ( F |` { ( G ` X ) } ) y ) )
67 66 mobidv 
 |-  ( ( x = ( G ` X ) /\ ( ( X e. dom ( F o. G ) /\ Fun ( ( F o. G ) |` { X } ) ) /\ ( G Fn A /\ X e. A ) ) ) -> ( E* y ( ( G ` X ) e. { ( G ` X ) } /\ ( G ` X ) F y ) <-> E* y x ( F |` { ( G ` X ) } ) y ) )
68 62 67 mpbid 
 |-  ( ( x = ( G ` X ) /\ ( ( X e. dom ( F o. G ) /\ Fun ( ( F o. G ) |` { X } ) ) /\ ( G Fn A /\ X e. A ) ) ) -> E* y x ( F |` { ( G ` X ) } ) y )
69 68 ex 
 |-  ( x = ( G ` X ) -> ( ( ( X e. dom ( F o. G ) /\ Fun ( ( F o. G ) |` { X } ) ) /\ ( G Fn A /\ X e. A ) ) -> E* y x ( F |` { ( G ` X ) } ) y ) )
70 8 69 sylbi 
 |-  ( x e. { ( G ` X ) } -> ( ( ( X e. dom ( F o. G ) /\ Fun ( ( F o. G ) |` { X } ) ) /\ ( G Fn A /\ X e. A ) ) -> E* y x ( F |` { ( G ` X ) } ) y ) )
71 7 70 syl6bi 
 |-  ( dom ( F |` { ( G ` X ) } ) = { ( G ` X ) } -> ( x e. dom ( F |` { ( G ` X ) } ) -> ( ( ( X e. dom ( F o. G ) /\ Fun ( ( F o. G ) |` { X } ) ) /\ ( G Fn A /\ X e. A ) ) -> E* y x ( F |` { ( G ` X ) } ) y ) ) )
72 71 com23 
 |-  ( dom ( F |` { ( G ` X ) } ) = { ( G ` X ) } -> ( ( ( X e. dom ( F o. G ) /\ Fun ( ( F o. G ) |` { X } ) ) /\ ( G Fn A /\ X e. A ) ) -> ( x e. dom ( F |` { ( G ` X ) } ) -> E* y x ( F |` { ( G ` X ) } ) y ) ) )
73 6 72 syl 
 |-  ( ( G ` X ) e. dom F -> ( ( ( X e. dom ( F o. G ) /\ Fun ( ( F o. G ) |` { X } ) ) /\ ( G Fn A /\ X e. A ) ) -> ( x e. dom ( F |` { ( G ` X ) } ) -> E* y x ( F |` { ( G ` X ) } ) y ) ) )
74 5 73 syl6com 
 |-  ( X e. dom ( F o. G ) -> ( ( G Fn A /\ X e. A ) -> ( ( ( X e. dom ( F o. G ) /\ Fun ( ( F o. G ) |` { X } ) ) /\ ( G Fn A /\ X e. A ) ) -> ( x e. dom ( F |` { ( G ` X ) } ) -> E* y x ( F |` { ( G ` X ) } ) y ) ) ) )
75 74 a1d 
 |-  ( X e. dom ( F o. G ) -> ( Fun ( ( F o. G ) |` { X } ) -> ( ( G Fn A /\ X e. A ) -> ( ( ( X e. dom ( F o. G ) /\ Fun ( ( F o. G ) |` { X } ) ) /\ ( G Fn A /\ X e. A ) ) -> ( x e. dom ( F |` { ( G ` X ) } ) -> E* y x ( F |` { ( G ` X ) } ) y ) ) ) ) )
76 75 imp31 
 |-  ( ( ( X e. dom ( F o. G ) /\ Fun ( ( F o. G ) |` { X } ) ) /\ ( G Fn A /\ X e. A ) ) -> ( ( ( X e. dom ( F o. G ) /\ Fun ( ( F o. G ) |` { X } ) ) /\ ( G Fn A /\ X e. A ) ) -> ( x e. dom ( F |` { ( G ` X ) } ) -> E* y x ( F |` { ( G ` X ) } ) y ) ) )
77 76 pm2.43i 
 |-  ( ( ( X e. dom ( F o. G ) /\ Fun ( ( F o. G ) |` { X } ) ) /\ ( G Fn A /\ X e. A ) ) -> ( x e. dom ( F |` { ( G ` X ) } ) -> E* y x ( F |` { ( G ` X ) } ) y ) )
78 77 ralrimiv 
 |-  ( ( ( X e. dom ( F o. G ) /\ Fun ( ( F o. G ) |` { X } ) ) /\ ( G Fn A /\ X e. A ) ) -> A. x e. dom ( F |` { ( G ` X ) } ) E* y x ( F |` { ( G ` X ) } ) y )
79 dffun7 
 |-  ( Fun ( F |` { ( G ` X ) } ) <-> ( Rel ( F |` { ( G ` X ) } ) /\ A. x e. dom ( F |` { ( G ` X ) } ) E* y x ( F |` { ( G ` X ) } ) y ) )
80 2 78 79 sylanbrc 
 |-  ( ( ( X e. dom ( F o. G ) /\ Fun ( ( F o. G ) |` { X } ) ) /\ ( G Fn A /\ X e. A ) ) -> Fun ( F |` { ( G ` X ) } ) )