Theorem oprab2co

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

	Ref	Expression
Hypotheses	oprab2co.1	$$⊢\left(x\in A\wedge y\in B\right)\to C\in R$$
	oprab2co.2	$$⊢\left(x\in A\wedge y\in B\right)\to D\in S$$
	oprab2co.3	$$⊢F=\left(x\in A,y\in B⟼⟨C,D⟩\right)$$
	oprab2co.4	$$⊢G=\left(x\in A,y\in B⟼CMD\right)$$
Assertion	oprab2co	$$⊢MFn\left(R\times S\right)\to G=M\circ F$$

Proof

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