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 ⊢ φ → A ∈ V
opco1.exb ⊢ φ → B ∈ W
Assertion opco1 ⊢ φ → A F ∘ 1 st B = F ⁡ A

Proof

Step Hyp Ref Expression
1 opco1.exa ⊢ φ → A ∈ V
2 opco1.exb ⊢ φ → B ∈ W
3 df-ov ⊢ A F ∘ 1 st B = F ∘ 1 st ⁡ A B
4 3 a1i ⊢ φ → A F ∘ 1 st B = F ∘ 1 st ⁡ A B
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 ⊢ A B ∈ V
9 8 a1i ⊢ φ → A B ∈ V
10 7 9 fvco3d ⊢ φ → F ∘ 1 st ⁡ A B = F ⁡ 1 st ⁡ A B
11 op1stg ⊢ A ∈ V ∧ B ∈ W → 1 st ⁡ A B = A
12 1 2 11 syl2anc ⊢ φ → 1 st ⁡ A B = A
13 12 fveq2d ⊢ φ → F ⁡ 1 st ⁡ A B = F ⁡ A
14 4 10 13 3eqtrd ⊢ φ → A F ∘ 1 st B = F ⁡ A