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