Theorem opropabco

Description: Composition of an operator with a function abstraction. (Contributed by Jeff Madsen, 11-Jun-2010)

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

Proof

Step	Hyp	Ref	Expression
1		opropabco.1	$$⊢x\in A\to B\in R$$
2		opropabco.2	$$⊢x\in A\to C\in S$$
3		opropabco.3	$$⊢F=\left\{⟨x,y⟩|\left(x\in A\wedge y=⟨B,C⟩\right)\right\}$$
4		opropabco.4	$$⊢G=\left\{⟨x,y⟩|\left(x\in A\wedge y=BMC\right)\right\}$$
5		opelxpi	$$⊢\left(B\in R\wedge C\in S\right)\to ⟨B,C⟩\in \left(R\times S\right)$$
6	1 2 5	syl2anc	$$⊢x\in A\to ⟨B,C⟩\in \left(R\times S\right)$$
7		df-ov	$$⊢BMC=M\left(⟨B,C⟩\right)$$
8	7	eqeq2i	$$⊢y=BMC\leftrightarrow y=M\left(⟨B,C⟩\right)$$
9	8	anbi2i	$$⊢\left(x\in A\wedge y=BMC\right)\leftrightarrow \left(x\in A\wedge y=M\left(⟨B,C⟩\right)\right)$$
10	9	opabbii	$$⊢\left\{⟨x,y⟩|\left(x\in A\wedge y=BMC\right)\right\}=\left\{⟨x,y⟩|\left(x\in A\wedge y=M\left(⟨B,C⟩\right)\right)\right\}$$
11	4 10	eqtri	$$⊢G=\left\{⟨x,y⟩|\left(x\in A\wedge y=M\left(⟨B,C⟩\right)\right)\right\}$$
12	6 3 11	fnopabco	$$⊢MFn\left(R\times S\right)\to G=M\circ F$$