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 ( 𝐹 : 𝐴𝐵 → ( 𝐹𝑋 ) : ( 𝐴𝑋 ) ⟶ 𝐵 )