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 F:AB2ndF:FB

Proof

Step Hyp Ref Expression
1 f2ndres 2ndA×B:A×BB
2 fssxp F:ABFA×B
3 fssres 2ndA×B:A×BBFA×B2ndA×BF:FB
4 1 2 3 sylancr F:AB2ndA×BF:FB
5 2 resabs1d F:AB2ndA×BF=2ndF
6 5 eqcomd F:AB2ndF=2ndA×BF
7 6 feq1d F:AB2ndF:FB2ndA×BF:FB
8 4 7 mpbird F:AB2ndF:FB