Metamath Proof Explorer


Theorem respreima

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

Ref Expression
Assertion respreima
|- ( Fun F -> ( `' ( F |` B ) " A ) = ( ( `' F " A ) i^i B ) )

Proof

Step Hyp Ref Expression
1 funfn
 |-  ( Fun F <-> F Fn dom F )
2 elin
 |-  ( x e. ( B i^i dom F ) <-> ( x e. B /\ x e. dom F ) )
3 2 biancomi
 |-  ( x e. ( B i^i dom F ) <-> ( x e. dom F /\ x e. B ) )
4 3 anbi1i
 |-  ( ( x e. ( B i^i dom F ) /\ ( ( F |` B ) ` x ) e. A ) <-> ( ( x e. dom F /\ x e. B ) /\ ( ( F |` B ) ` x ) e. A ) )
5 fvres
 |-  ( x e. B -> ( ( F |` B ) ` x ) = ( F ` x ) )
6 5 eleq1d
 |-  ( x e. B -> ( ( ( F |` B ) ` x ) e. A <-> ( F ` x ) e. A ) )
7 6 adantl
 |-  ( ( x e. dom F /\ x e. B ) -> ( ( ( F |` B ) ` x ) e. A <-> ( F ` x ) e. A ) )
8 7 pm5.32i
 |-  ( ( ( x e. dom F /\ x e. B ) /\ ( ( F |` B ) ` x ) e. A ) <-> ( ( x e. dom F /\ x e. B ) /\ ( F ` x ) e. A ) )
9 4 8 bitri
 |-  ( ( x e. ( B i^i dom F ) /\ ( ( F |` B ) ` x ) e. A ) <-> ( ( x e. dom F /\ x e. B ) /\ ( F ` x ) e. A ) )
10 9 a1i
 |-  ( F Fn dom F -> ( ( x e. ( B i^i dom F ) /\ ( ( F |` B ) ` x ) e. A ) <-> ( ( x e. dom F /\ x e. B ) /\ ( F ` x ) e. A ) ) )
11 an32
 |-  ( ( ( x e. dom F /\ x e. B ) /\ ( F ` x ) e. A ) <-> ( ( x e. dom F /\ ( F ` x ) e. A ) /\ x e. B ) )
12 10 11 bitrdi
 |-  ( F Fn dom F -> ( ( x e. ( B i^i dom F ) /\ ( ( F |` B ) ` x ) e. A ) <-> ( ( x e. dom F /\ ( F ` x ) e. A ) /\ x e. B ) ) )
13 fnfun
 |-  ( F Fn dom F -> Fun F )
14 13 funresd
 |-  ( F Fn dom F -> Fun ( F |` B ) )
15 dmres
 |-  dom ( F |` B ) = ( B i^i dom F )
16 df-fn
 |-  ( ( F |` B ) Fn ( B i^i dom F ) <-> ( Fun ( F |` B ) /\ dom ( F |` B ) = ( B i^i dom F ) ) )
17 14 15 16 sylanblrc
 |-  ( F Fn dom F -> ( F |` B ) Fn ( B i^i dom F ) )
18 elpreima
 |-  ( ( F |` B ) Fn ( B i^i dom F ) -> ( x e. ( `' ( F |` B ) " A ) <-> ( x e. ( B i^i dom F ) /\ ( ( F |` B ) ` x ) e. A ) ) )
19 17 18 syl
 |-  ( F Fn dom F -> ( x e. ( `' ( F |` B ) " A ) <-> ( x e. ( B i^i dom F ) /\ ( ( F |` B ) ` x ) e. A ) ) )
20 elin
 |-  ( x e. ( ( `' F " A ) i^i B ) <-> ( x e. ( `' F " A ) /\ x e. B ) )
21 elpreima
 |-  ( F Fn dom F -> ( x e. ( `' F " A ) <-> ( x e. dom F /\ ( F ` x ) e. A ) ) )
22 21 anbi1d
 |-  ( F Fn dom F -> ( ( x e. ( `' F " A ) /\ x e. B ) <-> ( ( x e. dom F /\ ( F ` x ) e. A ) /\ x e. B ) ) )
23 20 22 syl5bb
 |-  ( F Fn dom F -> ( x e. ( ( `' F " A ) i^i B ) <-> ( ( x e. dom F /\ ( F ` x ) e. A ) /\ x e. B ) ) )
24 12 19 23 3bitr4d
 |-  ( F Fn dom F -> ( x e. ( `' ( F |` B ) " A ) <-> x e. ( ( `' F " A ) i^i B ) ) )
25 1 24 sylbi
 |-  ( Fun F -> ( x e. ( `' ( F |` B ) " A ) <-> x e. ( ( `' F " A ) i^i B ) ) )
26 25 eqrdv
 |-  ( Fun F -> ( `' ( F |` B ) " A ) = ( ( `' F " A ) i^i B ) )