Metamath Proof Explorer


Theorem respreima

Description: The preimage of a restricted function. (Contributed by Jeff Madsen, 2-Sep-2009)

Ref Expression
Assertion respreima ( Fun 𝐹 → ( ( 𝐹𝐵 ) “ 𝐴 ) = ( ( 𝐹𝐴 ) ∩ 𝐵 ) )

Proof

Step Hyp Ref Expression
1 funfn ( Fun 𝐹𝐹 Fn dom 𝐹 )
2 elin ( 𝑥 ∈ ( 𝐵 ∩ dom 𝐹 ) ↔ ( 𝑥𝐵𝑥 ∈ dom 𝐹 ) )
3 2 biancomi ( 𝑥 ∈ ( 𝐵 ∩ dom 𝐹 ) ↔ ( 𝑥 ∈ dom 𝐹𝑥𝐵 ) )
4 3 anbi1i ( ( 𝑥 ∈ ( 𝐵 ∩ dom 𝐹 ) ∧ ( ( 𝐹𝐵 ) ‘ 𝑥 ) ∈ 𝐴 ) ↔ ( ( 𝑥 ∈ dom 𝐹𝑥𝐵 ) ∧ ( ( 𝐹𝐵 ) ‘ 𝑥 ) ∈ 𝐴 ) )
5 fvres ( 𝑥𝐵 → ( ( 𝐹𝐵 ) ‘ 𝑥 ) = ( 𝐹𝑥 ) )
6 5 eleq1d ( 𝑥𝐵 → ( ( ( 𝐹𝐵 ) ‘ 𝑥 ) ∈ 𝐴 ↔ ( 𝐹𝑥 ) ∈ 𝐴 ) )
7 6 adantl ( ( 𝑥 ∈ dom 𝐹𝑥𝐵 ) → ( ( ( 𝐹𝐵 ) ‘ 𝑥 ) ∈ 𝐴 ↔ ( 𝐹𝑥 ) ∈ 𝐴 ) )
8 7 pm5.32i ( ( ( 𝑥 ∈ dom 𝐹𝑥𝐵 ) ∧ ( ( 𝐹𝐵 ) ‘ 𝑥 ) ∈ 𝐴 ) ↔ ( ( 𝑥 ∈ dom 𝐹𝑥𝐵 ) ∧ ( 𝐹𝑥 ) ∈ 𝐴 ) )
9 4 8 bitri ( ( 𝑥 ∈ ( 𝐵 ∩ dom 𝐹 ) ∧ ( ( 𝐹𝐵 ) ‘ 𝑥 ) ∈ 𝐴 ) ↔ ( ( 𝑥 ∈ dom 𝐹𝑥𝐵 ) ∧ ( 𝐹𝑥 ) ∈ 𝐴 ) )
10 9 a1i ( 𝐹 Fn dom 𝐹 → ( ( 𝑥 ∈ ( 𝐵 ∩ dom 𝐹 ) ∧ ( ( 𝐹𝐵 ) ‘ 𝑥 ) ∈ 𝐴 ) ↔ ( ( 𝑥 ∈ dom 𝐹𝑥𝐵 ) ∧ ( 𝐹𝑥 ) ∈ 𝐴 ) ) )
11 an32 ( ( ( 𝑥 ∈ dom 𝐹𝑥𝐵 ) ∧ ( 𝐹𝑥 ) ∈ 𝐴 ) ↔ ( ( 𝑥 ∈ dom 𝐹 ∧ ( 𝐹𝑥 ) ∈ 𝐴 ) ∧ 𝑥𝐵 ) )
12 10 11 bitrdi ( 𝐹 Fn dom 𝐹 → ( ( 𝑥 ∈ ( 𝐵 ∩ dom 𝐹 ) ∧ ( ( 𝐹𝐵 ) ‘ 𝑥 ) ∈ 𝐴 ) ↔ ( ( 𝑥 ∈ dom 𝐹 ∧ ( 𝐹𝑥 ) ∈ 𝐴 ) ∧ 𝑥𝐵 ) ) )
13 fnfun ( 𝐹 Fn dom 𝐹 → Fun 𝐹 )
14 13 funresd ( 𝐹 Fn dom 𝐹 → Fun ( 𝐹𝐵 ) )
15 dmres dom ( 𝐹𝐵 ) = ( 𝐵 ∩ dom 𝐹 )
16 df-fn ( ( 𝐹𝐵 ) Fn ( 𝐵 ∩ dom 𝐹 ) ↔ ( Fun ( 𝐹𝐵 ) ∧ dom ( 𝐹𝐵 ) = ( 𝐵 ∩ dom 𝐹 ) ) )
17 14 15 16 sylanblrc ( 𝐹 Fn dom 𝐹 → ( 𝐹𝐵 ) Fn ( 𝐵 ∩ dom 𝐹 ) )
18 elpreima ( ( 𝐹𝐵 ) Fn ( 𝐵 ∩ dom 𝐹 ) → ( 𝑥 ∈ ( ( 𝐹𝐵 ) “ 𝐴 ) ↔ ( 𝑥 ∈ ( 𝐵 ∩ dom 𝐹 ) ∧ ( ( 𝐹𝐵 ) ‘ 𝑥 ) ∈ 𝐴 ) ) )
19 17 18 syl ( 𝐹 Fn dom 𝐹 → ( 𝑥 ∈ ( ( 𝐹𝐵 ) “ 𝐴 ) ↔ ( 𝑥 ∈ ( 𝐵 ∩ dom 𝐹 ) ∧ ( ( 𝐹𝐵 ) ‘ 𝑥 ) ∈ 𝐴 ) ) )
20 elin ( 𝑥 ∈ ( ( 𝐹𝐴 ) ∩ 𝐵 ) ↔ ( 𝑥 ∈ ( 𝐹𝐴 ) ∧ 𝑥𝐵 ) )
21 elpreima ( 𝐹 Fn dom 𝐹 → ( 𝑥 ∈ ( 𝐹𝐴 ) ↔ ( 𝑥 ∈ dom 𝐹 ∧ ( 𝐹𝑥 ) ∈ 𝐴 ) ) )
22 21 anbi1d ( 𝐹 Fn dom 𝐹 → ( ( 𝑥 ∈ ( 𝐹𝐴 ) ∧ 𝑥𝐵 ) ↔ ( ( 𝑥 ∈ dom 𝐹 ∧ ( 𝐹𝑥 ) ∈ 𝐴 ) ∧ 𝑥𝐵 ) ) )
23 20 22 syl5bb ( 𝐹 Fn dom 𝐹 → ( 𝑥 ∈ ( ( 𝐹𝐴 ) ∩ 𝐵 ) ↔ ( ( 𝑥 ∈ dom 𝐹 ∧ ( 𝐹𝑥 ) ∈ 𝐴 ) ∧ 𝑥𝐵 ) ) )
24 12 19 23 3bitr4d ( 𝐹 Fn dom 𝐹 → ( 𝑥 ∈ ( ( 𝐹𝐵 ) “ 𝐴 ) ↔ 𝑥 ∈ ( ( 𝐹𝐴 ) ∩ 𝐵 ) ) )
25 1 24 sylbi ( Fun 𝐹 → ( 𝑥 ∈ ( ( 𝐹𝐵 ) “ 𝐴 ) ↔ 𝑥 ∈ ( ( 𝐹𝐴 ) ∩ 𝐵 ) ) )
26 25 eqrdv ( Fun 𝐹 → ( ( 𝐹𝐵 ) “ 𝐴 ) = ( ( 𝐹𝐴 ) ∩ 𝐵 ) )