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

Metamath Proof Explorer

Theorem fresin

Description: An identity for the mapping relationship under restriction. (Contributed by Scott Fenton, 4-Sep-2011) (Proof shortened by Mario Carneiro, 26-May-2016)

Ref Expression
Assertion fresin ( 𝐹 : 𝐴 ⟶ 𝐵 → ( 𝐹 ↾ 𝑋 ) : ( 𝐴 ∩ 𝑋 ) ⟶ 𝐵 )

Proof

Step Hyp Ref Expression
1 inss1 ⊢ ( 𝐴 ∩ 𝑋 ) ⊆ 𝐴
2 fssres ⊢ ( ( 𝐹 : 𝐴 ⟶ 𝐵 ∧ ( 𝐴 ∩ 𝑋 ) ⊆ 𝐴 ) → ( 𝐹 ↾ ( 𝐴 ∩ 𝑋 ) ) : ( 𝐴 ∩ 𝑋 ) ⟶ 𝐵 )
3 1 2 mpan2 ⊢ ( 𝐹 : 𝐴 ⟶ 𝐵 → ( 𝐹 ↾ ( 𝐴 ∩ 𝑋 ) ) : ( 𝐴 ∩ 𝑋 ) ⟶ 𝐵 )
4 resres ⊢ ( ( 𝐹 ↾ 𝐴 ) ↾ 𝑋 ) = ( 𝐹 ↾ ( 𝐴 ∩ 𝑋 ) )
5 ffn ⊢ ( 𝐹 : 𝐴 ⟶ 𝐵 → 𝐹 Fn 𝐴 )
6 fnresdm ⊢ ( 𝐹 Fn 𝐴 → ( 𝐹 ↾ 𝐴 ) = 𝐹 )
7 5 6 syl ⊢ ( 𝐹 : 𝐴 ⟶ 𝐵 → ( 𝐹 ↾ 𝐴 ) = 𝐹 )
8 7 reseq1d ⊢ ( 𝐹 : 𝐴 ⟶ 𝐵 → ( ( 𝐹 ↾ 𝐴 ) ↾ 𝑋 ) = ( 𝐹 ↾ 𝑋 ) )
9 4 8 eqtr3id ⊢ ( 𝐹 : 𝐴 ⟶ 𝐵 → ( 𝐹 ↾ ( 𝐴 ∩ 𝑋 ) ) = ( 𝐹 ↾ 𝑋 ) )
10 9 feq1d ⊢ ( 𝐹 : 𝐴 ⟶ 𝐵 → ( ( 𝐹 ↾ ( 𝐴 ∩ 𝑋 ) ) : ( 𝐴 ∩ 𝑋 ) ⟶ 𝐵 ↔ ( 𝐹 ↾ 𝑋 ) : ( 𝐴 ∩ 𝑋 ) ⟶ 𝐵 ) )
11 3 10 mpbid ⊢ ( 𝐹 : 𝐴 ⟶ 𝐵 → ( 𝐹 ↾ 𝑋 ) : ( 𝐴 ∩ 𝑋 ) ⟶ 𝐵 )