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 ⊢FdefAtA∧A∈B→F↾B''''A=F''''A

Proof

Step Hyp Ref Expression
1 df-dfat ⊢FdefAtA↔A∈dom⁡F∧Fun⁡F↾A
2 elin ⊢A∈B∩dom⁡F↔A∈B∧A∈dom⁡F
3 2 biimpri ⊢A∈B∧A∈dom⁡F→A∈B∩dom⁡F
4 dmres ⊢dom⁡F↾B=B∩dom⁡F
5 3 4 eleqtrrdi ⊢A∈B∧A∈dom⁡F→A∈dom⁡F↾B
6 5 ex ⊢A∈B→A∈dom⁡F→A∈dom⁡F↾B
7 snssi ⊢A∈B→A⊆B
8 7 resabs1d ⊢A∈B→F↾B↾A=F↾A
9 8 eqcomd ⊢A∈B→F↾A=F↾B↾A
10 9 funeqd ⊢A∈B→Fun⁡F↾A↔Fun⁡F↾B↾A
11 10 biimpd ⊢A∈B→Fun⁡F↾A→Fun⁡F↾B↾A
12 6 11 anim12d ⊢A∈B→A∈dom⁡F∧Fun⁡F↾A→A∈dom⁡F↾B∧Fun⁡F↾B↾A
13 12 com12 ⊢A∈dom⁡F∧Fun⁡F↾A→A∈B→A∈dom⁡F↾B∧Fun⁡F↾B↾A
14 1 13 sylbi ⊢FdefAtA→A∈B→A∈dom⁡F↾B∧Fun⁡F↾B↾A
15 14 imp ⊢FdefAtA∧A∈B→A∈dom⁡F↾B∧Fun⁡F↾B↾A
16 df-dfat ⊢F↾BdefAtA↔A∈dom⁡F↾B∧Fun⁡F↾B↾A
17 dfatafv2iota ⊢F↾BdefAtA→F↾B''''A=ιx|AF↾Bx
18 16 17 sylbir ⊢A∈dom⁡F↾B∧Fun⁡F↾B↾A→F↾B''''A=ιx|AF↾Bx
19 15 18 syl ⊢FdefAtA∧A∈B→F↾B''''A=ιx|AF↾Bx
20 vex ⊢x∈V
21 20 brresi ⊢AF↾Bx↔A∈B∧AFx
22 21 baib ⊢A∈B→AF↾Bx↔AFx
23 22 iotabidv ⊢A∈B→ιx|AF↾Bx=ιx|AFx
24 23 adantl ⊢FdefAtA∧A∈B→ιx|AF↾Bx=ιx|AFx
25 dfatafv2iota ⊢FdefAtA→F''''A=ιx|AFx
26 25 eqcomd ⊢FdefAtA→ιx|AFx=F''''A
27 26 adantr ⊢FdefAtA∧A∈B→ιx|AFx=F''''A
28 19 24 27 3eqtrd ⊢FdefAtA∧A∈B→F↾B''''A=F''''A