fvovco

Description: Value of the composition of an operator, with a given function. (Contributed by Glauco Siliprandi, 11-Oct-2020)

Step	Hyp	Ref	Expression
1		fvovco.1	$⊢ φ \to F : X ⟶ V \times W$
2		fvovco.2	$⊢ φ \to Y \in X$
3	1 2	ffvelcdmd	$⊢ φ \to F (Y) \in (V \times W)$
4		1st2nd2	$⊢ F (Y) \in (V \times W) \to F (Y) = ⟨1^{st} (F (Y)), 2^{nd} (F (Y))⟩$
5	3 4	syl	$⊢ φ \to F (Y) = ⟨1^{st} (F (Y)), 2^{nd} (F (Y))⟩$
6	5	fveq2d	$⊢ φ \to O (F (Y)) = O (⟨1^{st} (F (Y)), 2^{nd} (F (Y))⟩)$
7		fvco3	$⊢ (F : X ⟶ V \times W \land Y \in X) \to (O \circ F) (Y) = O (F (Y))$
8	1 2 7	syl2anc	$⊢ φ \to (O \circ F) (Y) = O (F (Y))$
9		df-ov	$⊢ 1^{st} (F (Y)) O 2^{nd} (F (Y)) = O (⟨1^{st} (F (Y)), 2^{nd} (F (Y))⟩)$
10	9	a1i	$⊢ φ \to 1^{st} (F (Y)) O 2^{nd} (F (Y)) = O (⟨1^{st} (F (Y)), 2^{nd} (F (Y))⟩)$
11	6 8 10	3eqtr4d	$⊢ φ \to (O \circ F) (Y) = 1^{st} (F (Y)) O 2^{nd} (F (Y))$

Metamath Proof Explorer