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

Proof

Step Hyp Ref Expression
1 df-dfat ⊢ ( 𝐹 defAt 𝐴 ↔ ( 𝐴 ∈ dom 𝐹 ∧ Fun ( 𝐹 ↾ { 𝐴 } ) ) )
2 elin ⊢ ( 𝐴 ∈ ( 𝐵 ∩ dom 𝐹 ) ↔ ( 𝐴 ∈ 𝐵 ∧ 𝐴 ∈ dom 𝐹 ) )
3 2 biimpri ⊢ ( ( 𝐴 ∈ 𝐵 ∧ 𝐴 ∈ dom 𝐹 ) → 𝐴 ∈ ( 𝐵 ∩ dom 𝐹 ) )
4 dmres ⊢ dom ( 𝐹 ↾ 𝐵 ) = ( 𝐵 ∩ dom 𝐹 )
5 3 4 eleqtrrdi ⊢ ( ( 𝐴 ∈ 𝐵 ∧ 𝐴 ∈ dom 𝐹 ) → 𝐴 ∈ dom ( 𝐹 ↾ 𝐵 ) )
6 5 ex ⊢ ( 𝐴 ∈ 𝐵 → ( 𝐴 ∈ dom 𝐹 → 𝐴 ∈ dom ( 𝐹 ↾ 𝐵 ) ) )
7 snssi ⊢ ( 𝐴 ∈ 𝐵 → { 𝐴 } ⊆ 𝐵 )
8 7 resabs1d ⊢ ( 𝐴 ∈ 𝐵 → ( ( 𝐹 ↾ 𝐵 ) ↾ { 𝐴 } ) = ( 𝐹 ↾ { 𝐴 } ) )
9 8 eqcomd ⊢ ( 𝐴 ∈ 𝐵 → ( 𝐹 ↾ { 𝐴 } ) = ( ( 𝐹 ↾ 𝐵 ) ↾ { 𝐴 } ) )
10 9 funeqd ⊢ ( 𝐴 ∈ 𝐵 → ( Fun ( 𝐹 ↾ { 𝐴 } ) ↔ Fun ( ( 𝐹 ↾ 𝐵 ) ↾ { 𝐴 } ) ) )
11 10 biimpd ⊢ ( 𝐴 ∈ 𝐵 → ( Fun ( 𝐹 ↾ { 𝐴 } ) → Fun ( ( 𝐹 ↾ 𝐵 ) ↾ { 𝐴 } ) ) )
12 6 11 anim12d ⊢ ( 𝐴 ∈ 𝐵 → ( ( 𝐴 ∈ dom 𝐹 ∧ Fun ( 𝐹 ↾ { 𝐴 } ) ) → ( 𝐴 ∈ dom ( 𝐹 ↾ 𝐵 ) ∧ Fun ( ( 𝐹 ↾ 𝐵 ) ↾ { 𝐴 } ) ) ) )
13 12 com12 ⊢ ( ( 𝐴 ∈ dom 𝐹 ∧ Fun ( 𝐹 ↾ { 𝐴 } ) ) → ( 𝐴 ∈ 𝐵 → ( 𝐴 ∈ dom ( 𝐹 ↾ 𝐵 ) ∧ Fun ( ( 𝐹 ↾ 𝐵 ) ↾ { 𝐴 } ) ) ) )
14 1 13 sylbi ⊢ ( 𝐹 defAt 𝐴 → ( 𝐴 ∈ 𝐵 → ( 𝐴 ∈ dom ( 𝐹 ↾ 𝐵 ) ∧ Fun ( ( 𝐹 ↾ 𝐵 ) ↾ { 𝐴 } ) ) ) )
15 14 imp ⊢ ( ( 𝐹 defAt 𝐴 ∧ 𝐴 ∈ 𝐵 ) → ( 𝐴 ∈ dom ( 𝐹 ↾ 𝐵 ) ∧ Fun ( ( 𝐹 ↾ 𝐵 ) ↾ { 𝐴 } ) ) )
16 df-dfat ⊢ ( ( 𝐹 ↾ 𝐵 ) defAt 𝐴 ↔ ( 𝐴 ∈ dom ( 𝐹 ↾ 𝐵 ) ∧ Fun ( ( 𝐹 ↾ 𝐵 ) ↾ { 𝐴 } ) ) )
17 dfatafv2iota ⊢ ( ( 𝐹 ↾ 𝐵 ) defAt 𝐴 → ( ( 𝐹 ↾ 𝐵 ) '''' 𝐴 ) = ( ℩ 𝑥 𝐴 ( 𝐹 ↾ 𝐵 ) 𝑥 ) )
18 16 17 sylbir ⊢ ( ( 𝐴 ∈ dom ( 𝐹 ↾ 𝐵 ) ∧ Fun ( ( 𝐹 ↾ 𝐵 ) ↾ { 𝐴 } ) ) → ( ( 𝐹 ↾ 𝐵 ) '''' 𝐴 ) = ( ℩ 𝑥 𝐴 ( 𝐹 ↾ 𝐵 ) 𝑥 ) )
19 15 18 syl ⊢ ( ( 𝐹 defAt 𝐴 ∧ 𝐴 ∈ 𝐵 ) → ( ( 𝐹 ↾ 𝐵 ) '''' 𝐴 ) = ( ℩ 𝑥 𝐴 ( 𝐹 ↾ 𝐵 ) 𝑥 ) )
20 vex ⊢ 𝑥 ∈ V
21 20 brresi ⊢ ( 𝐴 ( 𝐹 ↾ 𝐵 ) 𝑥 ↔ ( 𝐴 ∈ 𝐵 ∧ 𝐴 𝐹 𝑥 ) )
22 21 baib ⊢ ( 𝐴 ∈ 𝐵 → ( 𝐴 ( 𝐹 ↾ 𝐵 ) 𝑥 ↔ 𝐴 𝐹 𝑥 ) )
23 22 iotabidv ⊢ ( 𝐴 ∈ 𝐵 → ( ℩ 𝑥 𝐴 ( 𝐹 ↾ 𝐵 ) 𝑥 ) = ( ℩ 𝑥 𝐴 𝐹 𝑥 ) )
24 23 adantl ⊢ ( ( 𝐹 defAt 𝐴 ∧ 𝐴 ∈ 𝐵 ) → ( ℩ 𝑥 𝐴 ( 𝐹 ↾ 𝐵 ) 𝑥 ) = ( ℩ 𝑥 𝐴 𝐹 𝑥 ) )
25 dfatafv2iota ⊢ ( 𝐹 defAt 𝐴 → ( 𝐹 '''' 𝐴 ) = ( ℩ 𝑥 𝐴 𝐹 𝑥 ) )
26 25 eqcomd ⊢ ( 𝐹 defAt 𝐴 → ( ℩ 𝑥 𝐴 𝐹 𝑥 ) = ( 𝐹 '''' 𝐴 ) )
27 26 adantr ⊢ ( ( 𝐹 defAt 𝐴 ∧ 𝐴 ∈ 𝐵 ) → ( ℩ 𝑥 𝐴 𝐹 𝑥 ) = ( 𝐹 '''' 𝐴 ) )
28 19 24 27 3eqtrd ⊢ ( ( 𝐹 defAt 𝐴 ∧ 𝐴 ∈ 𝐵 ) → ( ( 𝐹 ↾ 𝐵 ) '''' 𝐴 ) = ( 𝐹 '''' 𝐴 ) )