Metamath Proof Explorer

Theorem afvres

Description: The value of a restricted function, analogous to fvres . (Contributed by Alexander van der Vekens, 22-Jul-2017)

Ref Expression
Assertion afvres 
|- ( A e. B -> ( ( F |` B ) ''' A ) = ( F ''' A ) )

Proof

Step Hyp Ref Expression
1 elin 
 |-  ( A e. ( B i^i dom F ) <-> ( A e. B /\ A e. dom F ) )
2 1 biimpri 
 |-  ( ( A e. B /\ A e. dom F ) -> A e. ( B i^i dom F ) )
3 dmres 
 |-  dom ( F |` B ) = ( B i^i dom F )
4 2 3 eleqtrrdi 
 |-  ( ( A e. B /\ A e. dom F ) -> A e. dom ( F |` B ) )
5 4 ex 
 |-  ( A e. B -> ( A e. dom F -> A e. dom ( F |` B ) ) )
6 snssi 
 |-  ( A e. B -> { A } C_ B )
7 6 resabs1d 
 |-  ( A e. B -> ( ( F |` B ) |` { A } ) = ( F |` { A } ) )
8 7 eqcomd 
 |-  ( A e. B -> ( F |` { A } ) = ( ( F |` B ) |` { A } ) )
9 8 funeqd 
 |-  ( A e. B -> ( Fun ( F |` { A } ) <-> Fun ( ( F |` B ) |` { A } ) ) )
10 9 biimpd 
 |-  ( A e. B -> ( Fun ( F |` { A } ) -> Fun ( ( F |` B ) |` { A } ) ) )
11 5 10 anim12d 
 |-  ( A e. B -> ( ( A e. dom F /\ Fun ( F |` { A } ) ) -> ( A e. dom ( F |` B ) /\ Fun ( ( F |` B ) |` { A } ) ) ) )
12 11 impcom 
 |-  ( ( ( A e. dom F /\ Fun ( F |` { A } ) ) /\ A e. B ) -> ( A e. dom ( F |` B ) /\ Fun ( ( F |` B ) |` { A } ) ) )
13 df-dfat 
 |-  ( ( F |` B ) defAt A <-> ( A e. dom ( F |` B ) /\ Fun ( ( F |` B ) |` { A } ) ) )
14 afvfundmfveq 
 |-  ( ( F |` B ) defAt A -> ( ( F |` B ) ''' A ) = ( ( F |` B ) ` A ) )
15 13 14 sylbir 
 |-  ( ( A e. dom ( F |` B ) /\ Fun ( ( F |` B ) |` { A } ) ) -> ( ( F |` B ) ''' A ) = ( ( F |` B ) ` A ) )
16 12 15 syl 
 |-  ( ( ( A e. dom F /\ Fun ( F |` { A } ) ) /\ A e. B ) -> ( ( F |` B ) ''' A ) = ( ( F |` B ) ` A ) )
17 fvres 
 |-  ( A e. B -> ( ( F |` B ) ` A ) = ( F ` A ) )
18 17 adantl 
 |-  ( ( ( A e. dom F /\ Fun ( F |` { A } ) ) /\ A e. B ) -> ( ( F |` B ) ` A ) = ( F ` A ) )
19 df-dfat 
 |-  ( F defAt A <-> ( A e. dom F /\ Fun ( F |` { A } ) ) )
20 afvfundmfveq 
 |-  ( F defAt A -> ( F ''' A ) = ( F ` A ) )
21 19 20 sylbir 
 |-  ( ( A e. dom F /\ Fun ( F |` { A } ) ) -> ( F ''' A ) = ( F ` A ) )
22 21 eqcomd 
 |-  ( ( A e. dom F /\ Fun ( F |` { A } ) ) -> ( F ` A ) = ( F ''' A ) )
23 22 adantr 
 |-  ( ( ( A e. dom F /\ Fun ( F |` { A } ) ) /\ A e. B ) -> ( F ` A ) = ( F ''' A ) )
24 16 18 23 3eqtrd 
 |-  ( ( ( A e. dom F /\ Fun ( F |` { A } ) ) /\ A e. B ) -> ( ( F |` B ) ''' A ) = ( F ''' A ) )
25 pm3.4 
 |-  ( ( A e. B /\ A e. dom F ) -> ( A e. B -> A e. dom F ) )
26 1 25 sylbi 
 |-  ( A e. ( B i^i dom F ) -> ( A e. B -> A e. dom F ) )
27 26 3 eleq2s 
 |-  ( A e. dom ( F |` B ) -> ( A e. B -> A e. dom F ) )
28 27 com12 
 |-  ( A e. B -> ( A e. dom ( F |` B ) -> A e. dom F ) )
29 7 funeqd 
 |-  ( A e. B -> ( Fun ( ( F |` B ) |` { A } ) <-> Fun ( F |` { A } ) ) )
30 29 biimpd 
 |-  ( A e. B -> ( Fun ( ( F |` B ) |` { A } ) -> Fun ( F |` { A } ) ) )
31 28 30 anim12d 
 |-  ( A e. B -> ( ( A e. dom ( F |` B ) /\ Fun ( ( F |` B ) |` { A } ) ) -> ( A e. dom F /\ Fun ( F |` { A } ) ) ) )
32 31 con3d 
 |-  ( A e. B -> ( -. ( A e. dom F /\ Fun ( F |` { A } ) ) -> -. ( A e. dom ( F |` B ) /\ Fun ( ( F |` B ) |` { A } ) ) ) )
33 32 impcom 
 |-  ( ( -. ( A e. dom F /\ Fun ( F |` { A } ) ) /\ A e. B ) -> -. ( A e. dom ( F |` B ) /\ Fun ( ( F |` B ) |` { A } ) ) )
34 afvnfundmuv 
 |-  ( -. ( F |` B ) defAt A -> ( ( F |` B ) ''' A ) = _V )
35 13 34 sylnbir 
 |-  ( -. ( A e. dom ( F |` B ) /\ Fun ( ( F |` B ) |` { A } ) ) -> ( ( F |` B ) ''' A ) = _V )
36 33 35 syl 
 |-  ( ( -. ( A e. dom F /\ Fun ( F |` { A } ) ) /\ A e. B ) -> ( ( F |` B ) ''' A ) = _V )
37 afvnfundmuv 
 |-  ( -. F defAt A -> ( F ''' A ) = _V )
38 19 37 sylnbir 
 |-  ( -. ( A e. dom F /\ Fun ( F |` { A } ) ) -> ( F ''' A ) = _V )
39 38 eqcomd 
 |-  ( -. ( A e. dom F /\ Fun ( F |` { A } ) ) -> _V = ( F ''' A ) )
40 39 adantr 
 |-  ( ( -. ( A e. dom F /\ Fun ( F |` { A } ) ) /\ A e. B ) -> _V = ( F ''' A ) )
41 36 40 eqtrd 
 |-  ( ( -. ( A e. dom F /\ Fun ( F |` { A } ) ) /\ A e. B ) -> ( ( F |` B ) ''' A ) = ( F ''' A ) )
42 24 41 pm2.61ian 
 |-  ( A e. B -> ( ( F |` B ) ''' A ) = ( F ''' A ) )