oprab2co

Description: Composition of operator abstractions. (Contributed by Jeff Madsen, 2-Sep-2009) (Revised by David Abernethy, 23-Apr-2013)

Step	Hyp	Ref	Expression
1		oprab2co.1	$⊢ (x \in A \land y \in B) \to C \in R$
2		oprab2co.2	$⊢ (x \in A \land y \in B) \to D \in S$
3		oprab2co.3	$⊢ F = (x \in A, y \in B ⟼ ⟨C, D⟩)$
4		oprab2co.4	$⊢ G = (x \in A, y \in B ⟼ C M D)$
5	1 2	opelxpd	$⊢ (x \in A \land y \in B) \to ⟨C, D⟩ \in (R \times S)$
6		df-ov	$⊢ C M D = M (⟨C, D⟩)$
7	6	a1i	$⊢ (x \in A \land y \in B) \to C M D = M (⟨C, D⟩)$
8	7	mpoeq3ia	$⊢ (x \in A, y \in B ⟼ C M D) = (x \in A, y \in B ⟼ M (⟨C, D⟩))$
9	4 8	eqtri	$⊢ G = (x \in A, y \in B ⟼ M (⟨C, D⟩))$
10	5 3 9	oprabco	$⊢ M Fn (R \times S) \to G = M \circ F$

Metamath Proof Explorer