Metamath Proof Explorer

Theorem afv2res

Description: The value of a restricted function for an argument at which the function is defined. Analog to fvres . (Contributed by AV, 5-Sep-2022)

Ref Expression
Assertion afv2res 
|- ( ( F defAt A /\ A e. B ) -> ( ( F |` B ) '''' A ) = ( F '''' A ) )

Proof

Step Hyp Ref Expression
1 df-dfat 
 |-  ( F defAt A <-> ( A e. dom F /\ Fun ( F |` { A } ) ) )
2 elin 
 |-  ( A e. ( B i^i dom F ) <-> ( A e. B /\ A e. dom F ) )
3 2 biimpri 
 |-  ( ( A e. B /\ A e. dom F ) -> A e. ( B i^i dom F ) )
4 dmres 
 |-  dom ( F |` B ) = ( B i^i dom F )
5 3 4 eleqtrrdi 
 |-  ( ( A e. B /\ A e. dom F ) -> A e. dom ( F |` B ) )
6 5 ex 
 |-  ( A e. B -> ( A e. dom F -> A e. dom ( F |` B ) ) )
7 snssi 
 |-  ( A e. B -> { A } C_ B )
8 7 resabs1d 
 |-  ( A e. B -> ( ( F |` B ) |` { A } ) = ( F |` { A } ) )
9 8 eqcomd 
 |-  ( A e. B -> ( F |` { A } ) = ( ( F |` B ) |` { A } ) )
10 9 funeqd 
 |-  ( A e. B -> ( Fun ( F |` { A } ) <-> Fun ( ( F |` B ) |` { A } ) ) )
11 10 biimpd 
 |-  ( A e. B -> ( Fun ( F |` { A } ) -> Fun ( ( F |` B ) |` { A } ) ) )
12 6 11 anim12d 
 |-  ( A e. B -> ( ( A e. dom F /\ Fun ( F |` { A } ) ) -> ( A e. dom ( F |` B ) /\ Fun ( ( F |` B ) |` { A } ) ) ) )
13 12 com12 
 |-  ( ( A e. dom F /\ Fun ( F |` { A } ) ) -> ( A e. B -> ( A e. dom ( F |` B ) /\ Fun ( ( F |` B ) |` { A } ) ) ) )
14 1 13 sylbi 
 |-  ( F defAt A -> ( A e. B -> ( A e. dom ( F |` B ) /\ Fun ( ( F |` B ) |` { A } ) ) ) )
15 14 imp 
 |-  ( ( F defAt A /\ A e. B ) -> ( A e. dom ( F |` B ) /\ Fun ( ( F |` B ) |` { A } ) ) )
16 df-dfat 
 |-  ( ( F |` B ) defAt A <-> ( A e. dom ( F |` B ) /\ Fun ( ( F |` B ) |` { A } ) ) )
17 dfatafv2iota 
 |-  ( ( F |` B ) defAt A -> ( ( F |` B ) '''' A ) = ( iota x A ( F |` B ) x ) )
18 16 17 sylbir 
 |-  ( ( A e. dom ( F |` B ) /\ Fun ( ( F |` B ) |` { A } ) ) -> ( ( F |` B ) '''' A ) = ( iota x A ( F |` B ) x ) )
19 15 18 syl 
 |-  ( ( F defAt A /\ A e. B ) -> ( ( F |` B ) '''' A ) = ( iota x A ( F |` B ) x ) )
20 vex 
 |-  x e. _V
21 20 brresi 
 |-  ( A ( F |` B ) x <-> ( A e. B /\ A F x ) )
22 21 baib 
 |-  ( A e. B -> ( A ( F |` B ) x <-> A F x ) )
23 22 iotabidv 
 |-  ( A e. B -> ( iota x A ( F |` B ) x ) = ( iota x A F x ) )
24 23 adantl 
 |-  ( ( F defAt A /\ A e. B ) -> ( iota x A ( F |` B ) x ) = ( iota x A F x ) )
25 dfatafv2iota 
 |-  ( F defAt A -> ( F '''' A ) = ( iota x A F x ) )
26 25 eqcomd 
 |-  ( F defAt A -> ( iota x A F x ) = ( F '''' A ) )
27 26 adantr 
 |-  ( ( F defAt A /\ A e. B ) -> ( iota x A F x ) = ( F '''' A ) )
28 19 24 27 3eqtrd 
 |-  ( ( F defAt A /\ A e. B ) -> ( ( F |` B ) '''' A ) = ( F '''' A ) )