Theorem fnresin

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

	Ref	Expression
Assertion	fnresin	⊢ ( 𝐹 Fn 𝐴 → ( 𝐹 ↾ 𝐵 ) Fn ( 𝐴 ∩ 𝐵 ) )

Proof

Step	Hyp	Ref	Expression
1		fnresin1	⊢ ( 𝐹 Fn 𝐴 → ( 𝐹 ↾ ( 𝐴 ∩ 𝐵 ) ) Fn ( 𝐴 ∩ 𝐵 ) )
2		resindi	⊢ ( 𝐹 ↾ ( 𝐴 ∩ 𝐵 ) ) = ( ( 𝐹 ↾ 𝐴 ) ∩ ( 𝐹 ↾ 𝐵 ) )
3		fnresdm	⊢ ( 𝐹 Fn 𝐴 → ( 𝐹 ↾ 𝐴 ) = 𝐹 )
4	3	ineq1d	⊢ ( 𝐹 Fn 𝐴 → ( ( 𝐹 ↾ 𝐴 ) ∩ ( 𝐹 ↾ 𝐵 ) ) = ( 𝐹 ∩ ( 𝐹 ↾ 𝐵 ) ) )
5		incom	⊢ ( ( 𝐹 ↾ 𝐵 ) ∩ 𝐹 ) = ( 𝐹 ∩ ( 𝐹 ↾ 𝐵 ) )
6		resss	⊢ ( 𝐹 ↾ 𝐵 ) ⊆ 𝐹
7		df-ss	⊢ ( ( 𝐹 ↾ 𝐵 ) ⊆ 𝐹 ↔ ( ( 𝐹 ↾ 𝐵 ) ∩ 𝐹 ) = ( 𝐹 ↾ 𝐵 ) )
8	6 7	mpbi	⊢ ( ( 𝐹 ↾ 𝐵 ) ∩ 𝐹 ) = ( 𝐹 ↾ 𝐵 )
9	5 8	eqtr3i	⊢ ( 𝐹 ∩ ( 𝐹 ↾ 𝐵 ) ) = ( 𝐹 ↾ 𝐵 )
10	4 9	eqtrdi	⊢ ( 𝐹 Fn 𝐴 → ( ( 𝐹 ↾ 𝐴 ) ∩ ( 𝐹 ↾ 𝐵 ) ) = ( 𝐹 ↾ 𝐵 ) )
11	2 10	syl5eq	⊢ ( 𝐹 Fn 𝐴 → ( 𝐹 ↾ ( 𝐴 ∩ 𝐵 ) ) = ( 𝐹 ↾ 𝐵 ) )
12	11	fneq1d	⊢ ( 𝐹 Fn 𝐴 → ( ( 𝐹 ↾ ( 𝐴 ∩ 𝐵 ) ) Fn ( 𝐴 ∩ 𝐵 ) ↔ ( 𝐹 ↾ 𝐵 ) Fn ( 𝐴 ∩ 𝐵 ) ) )
13	1 12	mpbid	⊢ ( 𝐹 Fn 𝐴 → ( 𝐹 ↾ 𝐵 ) Fn ( 𝐴 ∩ 𝐵 ) )