This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

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 bitrid ⊢ ( 𝐹 Fn dom 𝐹 → ( 𝑥 ∈ ( ( ◡ 𝐹 “ 𝐴 ) ∩ 𝐵 ) ↔ ( ( 𝑥 ∈ dom 𝐹 ∧ ( 𝐹 ‘ 𝑥 ) ∈ 𝐴 ) ∧ 𝑥 ∈ 𝐵 ) ) )
24 12 19 23 3bitr4d ⊢ ( 𝐹 Fn dom 𝐹 → ( 𝑥 ∈ ( ◡ ( 𝐹 ↾ 𝐵 ) “ 𝐴 ) ↔ 𝑥 ∈ ( ( ◡ 𝐹 “ 𝐴 ) ∩ 𝐵 ) ) )
25 1 24 sylbi ⊢ ( Fun 𝐹 → ( 𝑥 ∈ ( ◡ ( 𝐹 ↾ 𝐵 ) “ 𝐴 ) ↔ 𝑥 ∈ ( ( ◡ 𝐹 “ 𝐴 ) ∩ 𝐵 ) ) )
26 25 eqrdv ⊢ ( Fun 𝐹 → ( ◡ ( 𝐹 ↾ 𝐵 ) “ 𝐴 ) = ( ( ◡ 𝐹 “ 𝐴 ) ∩ 𝐵 ) )