Theorem opropabco

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

	Ref	Expression
Hypotheses	opropabco.1	|- ( x e. A -> B e. R )
	opropabco.2	|- ( x e. A -> C e. S )
	opropabco.3	|- F = { <. x , y >. | ( x e. A /\ y = <. B , C >. ) }
	opropabco.4	|- G = { <. x , y >. | ( x e. A /\ y = ( B M C ) ) }
Assertion	opropabco	|- ( M Fn ( R X. S ) -> G = ( M o. F ) )

Proof

Step	Hyp	Ref	Expression
1		opropabco.1	|- ( x e. A -> B e. R )
2		opropabco.2	|- ( x e. A -> C e. S )
3		opropabco.3	|- F = { <. x , y >. | ( x e. A /\ y = <. B , C >. ) }
4		opropabco.4	|- G = { <. x , y >. | ( x e. A /\ y = ( B M C ) ) }
5		opelxpi	|- ( ( B e. R /\ C e. S ) -> <. B , C >. e. ( R X. S ) )
6	1 2 5	syl2anc	|- ( x e. A -> <. B , C >. e. ( R X. S ) )
7		df-ov	|- ( B M C ) = ( M ` <. B , C >. )
8	7	eqeq2i	|- ( y = ( B M C ) <-> y = ( M ` <. B , C >. ) )
9	8	anbi2i	|- ( ( x e. A /\ y = ( B M C ) ) <-> ( x e. A /\ y = ( M ` <. B , C >. ) ) )
10	9	opabbii	|- { <. x , y >. | ( x e. A /\ y = ( B M C ) ) } = { <. x , y >. | ( x e. A /\ y = ( M ` <. B , C >. ) ) }
11	4 10	eqtri	|- G = { <. x , y >. | ( x e. A /\ y = ( M ` <. B , C >. ) ) }
12	6 3 11	fnopabco	|- ( M Fn ( R X. S ) -> G = ( M o. F ) )