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 ) 𝐵 ) = ( 𝐹 ‘ 𝐵 ) )