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 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 bitrid 
 |-  ( 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 ) )