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

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 ⊢ ( 𝜑 → 𝐴 ∈ 𝑉 )
opco1.exb ⊢ ( 𝜑 → 𝐵 ∈ 𝑊 )
Assertion opco2 ( 𝜑 → ( 𝐴 ( 𝐹 ∘ 2nd ) 𝐵 ) = ( 𝐹 ‘ 𝐵 ) )

Proof

Step Hyp Ref Expression
1 opco1.exa ⊢ ( 𝜑 → 𝐴 ∈ 𝑉 )
2 opco1.exb ⊢ ( 𝜑 → 𝐵 ∈ 𝑊 )
3 df-ov ⊢ ( 𝐴 ( 𝐹 ∘ 2nd ) 𝐵 ) = ( ( 𝐹 ∘ 2nd ) ‘ ⟨ 𝐴 , 𝐵 ⟩ )
4 3 a1i ⊢ ( 𝜑 → ( 𝐴 ( 𝐹 ∘ 2nd ) 𝐵 ) = ( ( 𝐹 ∘ 2nd ) ‘ ⟨ 𝐴 , 𝐵 ⟩ ) )
5 fo2nd ⊢ 2nd : V –onto→ V
6 fof ⊢ ( 2nd : V –onto→ V → 2nd : V ⟶ V )
7 5 6 mp1i ⊢ ( 𝜑 → 2nd : V ⟶ V )
8 opex ⊢ ⟨ 𝐴 , 𝐵 ⟩ ∈ V
9 8 a1i ⊢ ( 𝜑 → ⟨ 𝐴 , 𝐵 ⟩ ∈ V )
10 7 9 fvco3d ⊢ ( 𝜑 → ( ( 𝐹 ∘ 2nd ) ‘ ⟨ 𝐴 , 𝐵 ⟩ ) = ( 𝐹 ‘ ( 2nd ‘ ⟨ 𝐴 , 𝐵 ⟩ ) ) )
11 op2ndg ⊢ ( ( 𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑊 ) → ( 2nd ‘ ⟨ 𝐴 , 𝐵 ⟩ ) = 𝐵 )
12 1 2 11 syl2anc ⊢ ( 𝜑 → ( 2nd ‘ ⟨ 𝐴 , 𝐵 ⟩ ) = 𝐵 )
13 12 fveq2d ⊢ ( 𝜑 → ( 𝐹 ‘ ( 2nd ‘ ⟨ 𝐴 , 𝐵 ⟩ ) ) = ( 𝐹 ‘ 𝐵 ) )
14 4 10 13 3eqtrd ⊢ ( 𝜑 → ( 𝐴 ( 𝐹 ∘ 2nd ) 𝐵 ) = ( 𝐹 ‘ 𝐵 ) )