Theorem oprabco

Description: Composition of a function with an operator abstraction. (Contributed by Jeff Madsen, 2-Sep-2009) (Proof shortened by Mario Carneiro, 26-Sep-2015)

	Ref	Expression
Hypotheses	oprabco.1	|- ( ( x e. A /\ y e. B ) -> C e. D )
	oprabco.2	|- F = ( x e. A , y e. B |-> C )
	oprabco.3	|- G = ( x e. A , y e. B |-> ( H ` C ) )
Assertion	oprabco	|- ( H Fn D -> G = ( H o. F ) )

Proof

Step	Hyp	Ref	Expression
1		oprabco.1	|- ( ( x e. A /\ y e. B ) -> C e. D )
2		oprabco.2	|- F = ( x e. A , y e. B |-> C )
3		oprabco.3	|- G = ( x e. A , y e. B |-> ( H ` C ) )
4	1	adantl	|- ( ( H Fn D /\ ( x e. A /\ y e. B ) ) -> C e. D )
5	2	a1i	|- ( H Fn D -> F = ( x e. A , y e. B |-> C ) )
6		dffn5	|- ( H Fn D <-> H = ( z e. D |-> ( H ` z ) ) )
7	6	biimpi	|- ( H Fn D -> H = ( z e. D |-> ( H ` z ) ) )
8		fveq2	|- ( z = C -> ( H ` z ) = ( H ` C ) )
9	4 5 7 8	fmpoco	|- ( H Fn D -> ( H o. F ) = ( x e. A , y e. B |-> ( H ` C ) ) )
10	3 9	eqtr4id	|- ( H Fn D -> G = ( H o. F ) )