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 funres 
 |-  ( Fun F -> Fun ( F |` B ) )
15 13 14 syl 
 |-  ( F Fn dom F -> Fun ( F |` B ) )
16 dmres 
 |-  dom ( F |` B ) = ( B i^i dom F )
17 df-fn 
 |-  ( ( F |` B ) Fn ( B i^i dom F ) <-> ( Fun ( F |` B ) /\ dom ( F |` B ) = ( B i^i dom F ) ) )
18 15 16 17 sylanblrc 
 |-  ( F Fn dom F -> ( F |` B ) Fn ( B i^i dom F ) )
19 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 ) ) )
20 18 19 syl 
 |-  ( F Fn dom F -> ( x e. ( `' ( F |` B ) " A ) <-> ( x e. ( B i^i dom F ) /\ ( ( F |` B ) ` x ) e. A ) ) )
21 elin 
 |-  ( x e. ( ( `' F " A ) i^i B ) <-> ( x e. ( `' F " A ) /\ x e. B ) )
22 elpreima 
 |-  ( F Fn dom F -> ( x e. ( `' F " A ) <-> ( x e. dom F /\ ( F ` x ) e. A ) ) )
23 22 anbi1d 
 |-  ( F Fn dom F -> ( ( x e. ( `' F " A ) /\ x e. B ) <-> ( ( x e. dom F /\ ( F ` x ) e. A ) /\ x e. B ) ) )
24 21 23 syl5bb 
 |-  ( F Fn dom F -> ( x e. ( ( `' F " A ) i^i B ) <-> ( ( x e. dom F /\ ( F ` x ) e. A ) /\ x e. B ) ) )
25 12 20 24 3bitr4d 
 |-  ( F Fn dom F -> ( x e. ( `' ( F |` B ) " A ) <-> x e. ( ( `' F " A ) i^i B ) ) )
26 1 25 sylbi 
 |-  ( Fun F -> ( x e. ( `' ( F |` B ) " A ) <-> x e. ( ( `' F " A ) i^i B ) ) )
27 26 eqrdv 
 |-  ( Fun F -> ( `' ( F |` B ) " A ) = ( ( `' F " A ) i^i B ) )