Theorem fnresin

Description: Restriction of a function with a subclass of its domain. (Contributed by Thierry Arnoux, 10-Oct-2017)

	Ref	Expression
Assertion	fnresin	|- ( F Fn A -> ( F |` B ) Fn ( A i^i B ) )

Proof

Step	Hyp	Ref	Expression
1		fnresin1	|- ( F Fn A -> ( F |` ( A i^i B ) ) Fn ( A i^i B ) )
2		resindi	|- ( F |` ( A i^i B ) ) = ( ( F |` A ) i^i ( F |` B ) )
3		fnresdm	|- ( F Fn A -> ( F |` A ) = F )
4	3	ineq1d	|- ( F Fn A -> ( ( F |` A ) i^i ( F |` B ) ) = ( F i^i ( F |` B ) ) )
5		incom	|- ( ( F |` B ) i^i F ) = ( F i^i ( F |` B ) )
6		resss	|- ( F |` B ) C_ F
7		dfss2	|- ( ( F |` B ) C_ F <-> ( ( F |` B ) i^i F ) = ( F |` B ) )
8	6 7	mpbi	|- ( ( F |` B ) i^i F ) = ( F |` B )
9	5 8	eqtr3i	|- ( F i^i ( F |` B ) ) = ( F |` B )
10	4 9	eqtrdi	|- ( F Fn A -> ( ( F |` A ) i^i ( F |` B ) ) = ( F |` B ) )
11	2 10	eqtrid	|- ( F Fn A -> ( F |` ( A i^i B ) ) = ( F |` B ) )
12	11	fneq1d	|- ( F Fn A -> ( ( F |` ( A i^i B ) ) Fn ( A i^i B ) <-> ( F |` B ) Fn ( A i^i B ) ) )
13	1 12	mpbid	|- ( F Fn A -> ( F |` B ) Fn ( A i^i B ) )