This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

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 ∩ B

Proof

Step Hyp Ref Expression
1 fnresin1 ⊢ F Fn A → F ↾ A ∩ B Fn A ∩ B
2 resindi ⊢ F ↾ A ∩ B = F ↾ A ∩ F ↾ B
3 fnresdm ⊢ F Fn A → F ↾ A = F
4 3 ineq1d ⊢ F Fn A → F ↾ A ∩ F ↾ B = F ∩ F ↾ B
5 incom ⊢ F ↾ B ∩ F = F ∩ F ↾ B
6 resss ⊢ F ↾ B ⊆ F
7 dfss2 ⊢ F ↾ B ⊆ F ↔ F ↾ B ∩ F = F ↾ B
8 6 7 mpbi ⊢ F ↾ B ∩ F = F ↾ B
9 5 8 eqtr3i ⊢ F ∩ F ↾ B = F ↾ B
10 4 9 eqtrdi ⊢ F Fn A → F ↾ A ∩ F ↾ B = F ↾ B
11 2 10 eqtrid ⊢ F Fn A → F ↾ A ∩ B = F ↾ B
12 11 fneq1d ⊢ F Fn A → F ↾ A ∩ B Fn A ∩ B ↔ F ↾ B Fn A ∩ B
13 1 12 mpbid ⊢ F Fn A → F ↾ B Fn A ∩ B