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 φAV
opco1.exb φBW
Assertion opco2 φAF2ndB=FB

Proof

Step Hyp Ref Expression
1 opco1.exa φAV
2 opco1.exb φBW
3 df-ov AF2ndB=F2ndAB
4 3 a1i φAF2ndB=F2ndAB
5 fo2nd 2nd:VontoV
6 fof 2nd:VontoV2nd:VV
7 5 6 mp1i φ2nd:VV
8 opex ABV
9 8 a1i φABV
10 7 9 fvco3d φF2ndAB=F2ndAB
11 op2ndg AVBW2ndAB=B
12 1 2 11 syl2anc φ2ndAB=B
13 12 fveq2d φF2ndAB=FB
14 4 10 13 3eqtrd φAF2ndB=FB