Metamath Proof Explorer

Theorem opco2

Description: Value of an operation precomposed with the projection on the second component. (Contributed by BJ, 27-Oct-2024)

Ref Expression
Hypotheses opco1.exa 
|- ( ph -> A e. V )
opco1.exb 
|- ( ph -> B e. W )
Assertion opco2 
|- ( ph -> ( A ( F o. 2nd ) B ) = ( F ` B ) )

Proof

Step Hyp Ref Expression
1 opco1.exa 
 |-  ( ph -> A e. V )
2 opco1.exb 
 |-  ( ph -> B e. W )
3 df-ov 
 |-  ( A ( F o. 2nd ) B ) = ( ( F o. 2nd ) ` <. A , B >. )
4 3 a1i 
 |-  ( ph -> ( A ( F o. 2nd ) B ) = ( ( F o. 2nd ) ` <. A , B >. ) )
5 fo2nd 
 |-  2nd : _V -onto-> _V
6 fof 
 |-  ( 2nd : _V -onto-> _V -> 2nd : _V --> _V )
7 5 6 mp1i 
 |-  ( ph -> 2nd : _V --> _V )
8 opex 
 |-  <. A , B >. e. _V
9 8 a1i 
 |-  ( ph -> <. A , B >. e. _V )
10 7 9 fvco3d 
 |-  ( ph -> ( ( F o. 2nd ) ` <. A , B >. ) = ( F ` ( 2nd ` <. A , B >. ) ) )
11 op2ndg 
 |-  ( ( A e. V /\ B e. W ) -> ( 2nd ` <. A , B >. ) = B )
12 1 2 11 syl2anc 
 |-  ( ph -> ( 2nd ` <. A , B >. ) = B )
13 12 fveq2d 
 |-  ( ph -> ( F ` ( 2nd ` <. A , B >. ) ) = ( F ` B ) )
14 4 10 13 3eqtrd 
 |-  ( ph -> ( A ( F o. 2nd ) B ) = ( F ` B ) )