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

Metamath Proof Explorer

Theorem opco1

Description: Value of an operation precomposed with the projection on the first component. (Contributed by Mario Carneiro, 28-May-2014) Generalize to closed form. (Revised by BJ, 27-Oct-2024)

		Ref	Expression
	Hypotheses	opco1.exa	⊢ ( 𝜑 → 𝐴 ∈ 𝑉 )
		opco1.exb	⊢ ( 𝜑 → 𝐵 ∈ 𝑊 )
	Assertion	opco1	⊢ ( 𝜑 → ( 𝐴 ( 𝐹 ∘ 1^st ) 𝐵 ) = ( 𝐹 ‘ 𝐴 ) )

Proof

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