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 ( 𝐴 ∈ 𝐵 → ( ( 𝐹 ↾ 𝐵 ) ''' 𝐴 ) = ( 𝐹 ''' 𝐴 ) )

Proof

Step Hyp Ref Expression
1 elin ⊢ ( 𝐴 ∈ ( 𝐵 ∩ dom 𝐹 ) ↔ ( 𝐴 ∈ 𝐵 ∧ 𝐴 ∈ dom 𝐹 ) )
2 1 biimpri ⊢ ( ( 𝐴 ∈ 𝐵 ∧ 𝐴 ∈ dom 𝐹 ) → 𝐴 ∈ ( 𝐵 ∩ dom 𝐹 ) )
3 dmres ⊢ dom ( 𝐹 ↾ 𝐵 ) = ( 𝐵 ∩ dom 𝐹 )
4 2 3 eleqtrrdi ⊢ ( ( 𝐴 ∈ 𝐵 ∧ 𝐴 ∈ dom 𝐹 ) → 𝐴 ∈ dom ( 𝐹 ↾ 𝐵 ) )
5 4 ex ⊢ ( 𝐴 ∈ 𝐵 → ( 𝐴 ∈ dom 𝐹 → 𝐴 ∈ dom ( 𝐹 ↾ 𝐵 ) ) )
6 snssi ⊢ ( 𝐴 ∈ 𝐵 → { 𝐴 } ⊆ 𝐵 )
7 6 resabs1d ⊢ ( 𝐴 ∈ 𝐵 → ( ( 𝐹 ↾ 𝐵 ) ↾ { 𝐴 } ) = ( 𝐹 ↾ { 𝐴 } ) )
8 7 eqcomd ⊢ ( 𝐴 ∈ 𝐵 → ( 𝐹 ↾ { 𝐴 } ) = ( ( 𝐹 ↾ 𝐵 ) ↾ { 𝐴 } ) )
9 8 funeqd ⊢ ( 𝐴 ∈ 𝐵 → ( Fun ( 𝐹 ↾ { 𝐴 } ) ↔ Fun ( ( 𝐹 ↾ 𝐵 ) ↾ { 𝐴 } ) ) )
10 9 biimpd ⊢ ( 𝐴 ∈ 𝐵 → ( Fun ( 𝐹 ↾ { 𝐴 } ) → Fun ( ( 𝐹 ↾ 𝐵 ) ↾ { 𝐴 } ) ) )
11 5 10 anim12d ⊢ ( 𝐴 ∈ 𝐵 → ( ( 𝐴 ∈ dom 𝐹 ∧ Fun ( 𝐹 ↾ { 𝐴 } ) ) → ( 𝐴 ∈ dom ( 𝐹 ↾ 𝐵 ) ∧ Fun ( ( 𝐹 ↾ 𝐵 ) ↾ { 𝐴 } ) ) ) )
12 11 impcom ⊢ ( ( ( 𝐴 ∈ dom 𝐹 ∧ Fun ( 𝐹 ↾ { 𝐴 } ) ) ∧ 𝐴 ∈ 𝐵 ) → ( 𝐴 ∈ dom ( 𝐹 ↾ 𝐵 ) ∧ Fun ( ( 𝐹 ↾ 𝐵 ) ↾ { 𝐴 } ) ) )
13 df-dfat ⊢ ( ( 𝐹 ↾ 𝐵 ) defAt 𝐴 ↔ ( 𝐴 ∈ dom ( 𝐹 ↾ 𝐵 ) ∧ Fun ( ( 𝐹 ↾ 𝐵 ) ↾ { 𝐴 } ) ) )
14 afvfundmfveq ⊢ ( ( 𝐹 ↾ 𝐵 ) defAt 𝐴 → ( ( 𝐹 ↾ 𝐵 ) ''' 𝐴 ) = ( ( 𝐹 ↾ 𝐵 ) ‘ 𝐴 ) )
15 13 14 sylbir ⊢ ( ( 𝐴 ∈ dom ( 𝐹 ↾ 𝐵 ) ∧ Fun ( ( 𝐹 ↾ 𝐵 ) ↾ { 𝐴 } ) ) → ( ( 𝐹 ↾ 𝐵 ) ''' 𝐴 ) = ( ( 𝐹 ↾ 𝐵 ) ‘ 𝐴 ) )
16 12 15 syl ⊢ ( ( ( 𝐴 ∈ dom 𝐹 ∧ Fun ( 𝐹 ↾ { 𝐴 } ) ) ∧ 𝐴 ∈ 𝐵 ) → ( ( 𝐹 ↾ 𝐵 ) ''' 𝐴 ) = ( ( 𝐹 ↾ 𝐵 ) ‘ 𝐴 ) )
17 fvres ⊢ ( 𝐴 ∈ 𝐵 → ( ( 𝐹 ↾ 𝐵 ) ‘ 𝐴 ) = ( 𝐹 ‘ 𝐴 ) )
18 17 adantl ⊢ ( ( ( 𝐴 ∈ dom 𝐹 ∧ Fun ( 𝐹 ↾ { 𝐴 } ) ) ∧ 𝐴 ∈ 𝐵 ) → ( ( 𝐹 ↾ 𝐵 ) ‘ 𝐴 ) = ( 𝐹 ‘ 𝐴 ) )
19 df-dfat ⊢ ( 𝐹 defAt 𝐴 ↔ ( 𝐴 ∈ dom 𝐹 ∧ Fun ( 𝐹 ↾ { 𝐴 } ) ) )
20 afvfundmfveq ⊢ ( 𝐹 defAt 𝐴 → ( 𝐹 ''' 𝐴 ) = ( 𝐹 ‘ 𝐴 ) )
21 19 20 sylbir ⊢ ( ( 𝐴 ∈ dom 𝐹 ∧ Fun ( 𝐹 ↾ { 𝐴 } ) ) → ( 𝐹 ''' 𝐴 ) = ( 𝐹 ‘ 𝐴 ) )
22 21 eqcomd ⊢ ( ( 𝐴 ∈ dom 𝐹 ∧ Fun ( 𝐹 ↾ { 𝐴 } ) ) → ( 𝐹 ‘ 𝐴 ) = ( 𝐹 ''' 𝐴 ) )
23 22 adantr ⊢ ( ( ( 𝐴 ∈ dom 𝐹 ∧ Fun ( 𝐹 ↾ { 𝐴 } ) ) ∧ 𝐴 ∈ 𝐵 ) → ( 𝐹 ‘ 𝐴 ) = ( 𝐹 ''' 𝐴 ) )
24 16 18 23 3eqtrd ⊢ ( ( ( 𝐴 ∈ dom 𝐹 ∧ Fun ( 𝐹 ↾ { 𝐴 } ) ) ∧ 𝐴 ∈ 𝐵 ) → ( ( 𝐹 ↾ 𝐵 ) ''' 𝐴 ) = ( 𝐹 ''' 𝐴 ) )
25 pm3.4 ⊢ ( ( 𝐴 ∈ 𝐵 ∧ 𝐴 ∈ dom 𝐹 ) → ( 𝐴 ∈ 𝐵 → 𝐴 ∈ dom 𝐹 ) )
26 1 25 sylbi ⊢ ( 𝐴 ∈ ( 𝐵 ∩ dom 𝐹 ) → ( 𝐴 ∈ 𝐵 → 𝐴 ∈ dom 𝐹 ) )
27 26 3 eleq2s ⊢ ( 𝐴 ∈ dom ( 𝐹 ↾ 𝐵 ) → ( 𝐴 ∈ 𝐵 → 𝐴 ∈ dom 𝐹 ) )
28 27 com12 ⊢ ( 𝐴 ∈ 𝐵 → ( 𝐴 ∈ dom ( 𝐹 ↾ 𝐵 ) → 𝐴 ∈ dom 𝐹 ) )
29 7 funeqd ⊢ ( 𝐴 ∈ 𝐵 → ( Fun ( ( 𝐹 ↾ 𝐵 ) ↾ { 𝐴 } ) ↔ Fun ( 𝐹 ↾ { 𝐴 } ) ) )
30 29 biimpd ⊢ ( 𝐴 ∈ 𝐵 → ( Fun ( ( 𝐹 ↾ 𝐵 ) ↾ { 𝐴 } ) → Fun ( 𝐹 ↾ { 𝐴 } ) ) )
31 28 30 anim12d ⊢ ( 𝐴 ∈ 𝐵 → ( ( 𝐴 ∈ dom ( 𝐹 ↾ 𝐵 ) ∧ Fun ( ( 𝐹 ↾ 𝐵 ) ↾ { 𝐴 } ) ) → ( 𝐴 ∈ dom 𝐹 ∧ Fun ( 𝐹 ↾ { 𝐴 } ) ) ) )
32 31 con3d ⊢ ( 𝐴 ∈ 𝐵 → ( ¬ ( 𝐴 ∈ dom 𝐹 ∧ Fun ( 𝐹 ↾ { 𝐴 } ) ) → ¬ ( 𝐴 ∈ dom ( 𝐹 ↾ 𝐵 ) ∧ Fun ( ( 𝐹 ↾ 𝐵 ) ↾ { 𝐴 } ) ) ) )
33 32 impcom ⊢ ( ( ¬ ( 𝐴 ∈ dom 𝐹 ∧ Fun ( 𝐹 ↾ { 𝐴 } ) ) ∧ 𝐴 ∈ 𝐵 ) → ¬ ( 𝐴 ∈ dom ( 𝐹 ↾ 𝐵 ) ∧ Fun ( ( 𝐹 ↾ 𝐵 ) ↾ { 𝐴 } ) ) )
34 afvnfundmuv ⊢ ( ¬ ( 𝐹 ↾ 𝐵 ) defAt 𝐴 → ( ( 𝐹 ↾ 𝐵 ) ''' 𝐴 ) = V )
35 13 34 sylnbir ⊢ ( ¬ ( 𝐴 ∈ dom ( 𝐹 ↾ 𝐵 ) ∧ Fun ( ( 𝐹 ↾ 𝐵 ) ↾ { 𝐴 } ) ) → ( ( 𝐹 ↾ 𝐵 ) ''' 𝐴 ) = V )
36 33 35 syl ⊢ ( ( ¬ ( 𝐴 ∈ dom 𝐹 ∧ Fun ( 𝐹 ↾ { 𝐴 } ) ) ∧ 𝐴 ∈ 𝐵 ) → ( ( 𝐹 ↾ 𝐵 ) ''' 𝐴 ) = V )
37 afvnfundmuv ⊢ ( ¬ 𝐹 defAt 𝐴 → ( 𝐹 ''' 𝐴 ) = V )
38 19 37 sylnbir ⊢ ( ¬ ( 𝐴 ∈ dom 𝐹 ∧ Fun ( 𝐹 ↾ { 𝐴 } ) ) → ( 𝐹 ''' 𝐴 ) = V )
39 38 eqcomd ⊢ ( ¬ ( 𝐴 ∈ dom 𝐹 ∧ Fun ( 𝐹 ↾ { 𝐴 } ) ) → V = ( 𝐹 ''' 𝐴 ) )
40 39 adantr ⊢ ( ( ¬ ( 𝐴 ∈ dom 𝐹 ∧ Fun ( 𝐹 ↾ { 𝐴 } ) ) ∧ 𝐴 ∈ 𝐵 ) → V = ( 𝐹 ''' 𝐴 ) )
41 36 40 eqtrd ⊢ ( ( ¬ ( 𝐴 ∈ dom 𝐹 ∧ Fun ( 𝐹 ↾ { 𝐴 } ) ) ∧ 𝐴 ∈ 𝐵 ) → ( ( 𝐹 ↾ 𝐵 ) ''' 𝐴 ) = ( 𝐹 ''' 𝐴 ) )
42 24 41 pm2.61ian ⊢ ( 𝐴 ∈ 𝐵 → ( ( 𝐹 ↾ 𝐵 ) ''' 𝐴 ) = ( 𝐹 ''' 𝐴 ) )