Metamath Proof Explorer

Theorem f2ndf

Description: The 2nd (second component of an ordered pair) function restricted to a function F is a function from F into the codomain of F . (Contributed by Alexander van der Vekens, 4-Feb-2018)

		Ref	Expression
	Assertion	f2ndf	⊢ ( 𝐹 : 𝐴 ⟶ 𝐵 → ( 2^nd ↾ 𝐹 ) : 𝐹 ⟶ 𝐵 )

Proof

Step	Hyp	Ref	Expression
1		f2ndres	⊢ ( 2^nd ↾ ( 𝐴 × 𝐵 ) ) : ( 𝐴 × 𝐵 ) ⟶ 𝐵
2		fssxp	⊢ ( 𝐹 : 𝐴 ⟶ 𝐵 → 𝐹 ⊆ ( 𝐴 × 𝐵 ) )
3		fssres	⊢ ( ( ( 2^nd ↾ ( 𝐴 × 𝐵 ) ) : ( 𝐴 × 𝐵 ) ⟶ 𝐵 ∧ 𝐹 ⊆ ( 𝐴 × 𝐵 ) ) → ( ( 2^nd ↾ ( 𝐴 × 𝐵 ) ) ↾ 𝐹 ) : 𝐹 ⟶ 𝐵 )
4	1 2 3	sylancr	⊢ ( 𝐹 : 𝐴 ⟶ 𝐵 → ( ( 2^nd ↾ ( 𝐴 × 𝐵 ) ) ↾ 𝐹 ) : 𝐹 ⟶ 𝐵 )
5	2	resabs1d	⊢ ( 𝐹 : 𝐴 ⟶ 𝐵 → ( ( 2^nd ↾ ( 𝐴 × 𝐵 ) ) ↾ 𝐹 ) = ( 2^nd ↾ 𝐹 ) )
6	5	eqcomd	⊢ ( 𝐹 : 𝐴 ⟶ 𝐵 → ( 2^nd ↾ 𝐹 ) = ( ( 2^nd ↾ ( 𝐴 × 𝐵 ) ) ↾ 𝐹 ) )
7	6	feq1d	⊢ ( 𝐹 : 𝐴 ⟶ 𝐵 → ( ( 2^nd ↾ 𝐹 ) : 𝐹 ⟶ 𝐵 ↔ ( ( 2^nd ↾ ( 𝐴 × 𝐵 ) ) ↾ 𝐹 ) : 𝐹 ⟶ 𝐵 ) )
8	4 7	mpbird	⊢ ( 𝐹 : 𝐴 ⟶ 𝐵 → ( 2^nd ↾ 𝐹 ) : 𝐹 ⟶ 𝐵 )