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 ( 𝐹 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 dfss2 ⊢ ( ( 𝐹 ↾ 𝐵 ) ⊆ 𝐹 ↔ ( ( 𝐹 ↾ 𝐵 ) ∩ 𝐹 ) = ( 𝐹 ↾ 𝐵 ) )
8 6 7 mpbi ⊢ ( ( 𝐹 ↾ 𝐵 ) ∩ 𝐹 ) = ( 𝐹 ↾ 𝐵 )
9 5 8 eqtr3i ⊢ ( 𝐹 ∩ ( 𝐹 ↾ 𝐵 ) ) = ( 𝐹 ↾ 𝐵 )
10 4 9 eqtrdi ⊢ ( 𝐹 Fn 𝐴 → ( ( 𝐹 ↾ 𝐴 ) ∩ ( 𝐹 ↾ 𝐵 ) ) = ( 𝐹 ↾ 𝐵 ) )
11 2 10 eqtrid ⊢ ( 𝐹 Fn 𝐴 → ( 𝐹 ↾ ( 𝐴 ∩ 𝐵 ) ) = ( 𝐹 ↾ 𝐵 ) )
12 11 fneq1d ⊢ ( 𝐹 Fn 𝐴 → ( ( 𝐹 ↾ ( 𝐴 ∩ 𝐵 ) ) Fn ( 𝐴 ∩ 𝐵 ) ↔ ( 𝐹 ↾ 𝐵 ) Fn ( 𝐴 ∩ 𝐵 ) ) )
13 1 12 mpbid ⊢ ( 𝐹 Fn 𝐴 → ( 𝐹 ↾ 𝐵 ) Fn ( 𝐴 ∩ 𝐵 ) )