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 funres ⊢ ( Fun 𝐹 → Fun ( 𝐹 ↾ 𝐵 ) )
15 13 14 syl ⊢ ( 𝐹 Fn dom 𝐹 → Fun ( 𝐹 ↾ 𝐵 ) )
16 dmres ⊢ dom ( 𝐹 ↾ 𝐵 ) = ( 𝐵 ∩ dom 𝐹 )
17 df-fn ⊢ ( ( 𝐹 ↾ 𝐵 ) Fn ( 𝐵 ∩ dom 𝐹 ) ↔ ( Fun ( 𝐹 ↾ 𝐵 ) ∧ dom ( 𝐹 ↾ 𝐵 ) = ( 𝐵 ∩ dom 𝐹 ) ) )
18 15 16 17 sylanblrc ⊢ ( 𝐹 Fn dom 𝐹 → ( 𝐹 ↾ 𝐵 ) Fn ( 𝐵 ∩ dom 𝐹 ) )
19 elpreima ⊢ ( ( 𝐹 ↾ 𝐵 ) Fn ( 𝐵 ∩ dom 𝐹 ) → ( 𝑥 ∈ ( ◡ ( 𝐹 ↾ 𝐵 ) “ 𝐴 ) ↔ ( 𝑥 ∈ ( 𝐵 ∩ dom 𝐹 ) ∧ ( ( 𝐹 ↾ 𝐵 ) ‘ 𝑥 ) ∈ 𝐴 ) ) )
20 18 19 syl ⊢ ( 𝐹 Fn dom 𝐹 → ( 𝑥 ∈ ( ◡ ( 𝐹 ↾ 𝐵 ) “ 𝐴 ) ↔ ( 𝑥 ∈ ( 𝐵 ∩ dom 𝐹 ) ∧ ( ( 𝐹 ↾ 𝐵 ) ‘ 𝑥 ) ∈ 𝐴 ) ) )
21 elin ⊢ ( 𝑥 ∈ ( ( ◡ 𝐹 “ 𝐴 ) ∩ 𝐵 ) ↔ ( 𝑥 ∈ ( ◡ 𝐹 “ 𝐴 ) ∧ 𝑥 ∈ 𝐵 ) )
22 elpreima ⊢ ( 𝐹 Fn dom 𝐹 → ( 𝑥 ∈ ( ◡ 𝐹 “ 𝐴 ) ↔ ( 𝑥 ∈ dom 𝐹 ∧ ( 𝐹 ‘ 𝑥 ) ∈ 𝐴 ) ) )
23 22 anbi1d ⊢ ( 𝐹 Fn dom 𝐹 → ( ( 𝑥 ∈ ( ◡ 𝐹 “ 𝐴 ) ∧ 𝑥 ∈ 𝐵 ) ↔ ( ( 𝑥 ∈ dom 𝐹 ∧ ( 𝐹 ‘ 𝑥 ) ∈ 𝐴 ) ∧ 𝑥 ∈ 𝐵 ) ) )
24 21 23 syl5bb ⊢ ( 𝐹 Fn dom 𝐹 → ( 𝑥 ∈ ( ( ◡ 𝐹 “ 𝐴 ) ∩ 𝐵 ) ↔ ( ( 𝑥 ∈ dom 𝐹 ∧ ( 𝐹 ‘ 𝑥 ) ∈ 𝐴 ) ∧ 𝑥 ∈ 𝐵 ) ) )
25 12 20 24 3bitr4d ⊢ ( 𝐹 Fn dom 𝐹 → ( 𝑥 ∈ ( ◡ ( 𝐹 ↾ 𝐵 ) “ 𝐴 ) ↔ 𝑥 ∈ ( ( ◡ 𝐹 “ 𝐴 ) ∩ 𝐵 ) ) )
26 1 25 sylbi ⊢ ( Fun 𝐹 → ( 𝑥 ∈ ( ◡ ( 𝐹 ↾ 𝐵 ) “ 𝐴 ) ↔ 𝑥 ∈ ( ( ◡ 𝐹 “ 𝐴 ) ∩ 𝐵 ) ) )
27 26 eqrdv ⊢ ( Fun 𝐹 → ( ◡ ( 𝐹 ↾ 𝐵 ) “ 𝐴 ) = ( ( ◡ 𝐹 “ 𝐴 ) ∩ 𝐵 ) )