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

Metamath Proof Explorer

Theorem homacd

Description: The codomain of an arrow with known domain and codomain. (Contributed by Mario Carneiro, 11-Jan-2017)

Ref Expression
Hypothesis homahom.h 
|- H = ( HomA ` C )
Assertion homacd 
|- ( F e. ( X H Y ) -> ( codA ` F ) = Y )

Proof

Step Hyp Ref Expression
1 homahom.h 
 |-  H = ( HomA ` C )
2 df-coda 
 |-  codA = ( 2nd o. 1st )
3 2 fveq1i 
 |-  ( codA ` F ) = ( ( 2nd o. 1st ) ` F )
4 fo1st 
 |-  1st : _V -onto-> _V
5 fof 
 |-  ( 1st : _V -onto-> _V -> 1st : _V --> _V )
6 4 5 ax-mp 
 |-  1st : _V --> _V
7 elex 
 |-  ( F e. ( X H Y ) -> F e. _V )
8 fvco3 
 |-  ( ( 1st : _V --> _V /\ F e. _V ) -> ( ( 2nd o. 1st ) ` F ) = ( 2nd ` ( 1st ` F ) ) )
9 6 7 8 sylancr 
 |-  ( F e. ( X H Y ) -> ( ( 2nd o. 1st ) ` F ) = ( 2nd ` ( 1st ` F ) ) )
10 3 9 eqtrid 
 |-  ( F e. ( X H Y ) -> ( codA ` F ) = ( 2nd ` ( 1st ` F ) ) )
11 1 homarel 
 |-  Rel ( X H Y )
12 1st2ndbr 
 |-  ( ( Rel ( X H Y ) /\ F e. ( X H Y ) ) -> ( 1st ` F ) ( X H Y ) ( 2nd ` F ) )
13 11 12 mpan 
 |-  ( F e. ( X H Y ) -> ( 1st ` F ) ( X H Y ) ( 2nd ` F ) )
14 1 homa1 
 |-  ( ( 1st ` F ) ( X H Y ) ( 2nd ` F ) -> ( 1st ` F ) = <. X , Y >. )
15 13 14 syl 
 |-  ( F e. ( X H Y ) -> ( 1st ` F ) = <. X , Y >. )
16 15 fveq2d 
 |-  ( F e. ( X H Y ) -> ( 2nd ` ( 1st ` F ) ) = ( 2nd ` <. X , Y >. ) )
17 eqid 
 |-  ( Base ` C ) = ( Base ` C )
18 1 17 homarcl2 
 |-  ( F e. ( X H Y ) -> ( X e. ( Base ` C ) /\ Y e. ( Base ` C ) ) )
19 op2ndg 
 |-  ( ( X e. ( Base ` C ) /\ Y e. ( Base ` C ) ) -> ( 2nd ` <. X , Y >. ) = Y )
20 18 19 syl 
 |-  ( F e. ( X H Y ) -> ( 2nd ` <. X , Y >. ) = Y )
21 10 16 20 3eqtrd 
 |-  ( F e. ( X H Y ) -> ( codA ` F ) = Y )