Theorem fnopabco

Description: Composition of a function with a function abstraction. (Contributed by Jeff Madsen, 2-Sep-2009) (Revised by Mario Carneiro, 27-Dec-2014)

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

Proof

Step	Hyp	Ref	Expression
1		fnopabco.1	|- ( x e. A -> B e. C )
2		fnopabco.2	|- F = { <. x , y >. | ( x e. A /\ y = B ) }
3		fnopabco.3	|- G = { <. x , y >. | ( x e. A /\ y = ( H ` B ) ) }
4		df-mpt	|- ( x e. A |-> ( H ` B ) ) = { <. x , y >. | ( x e. A /\ y = ( H ` B ) ) }
5	3 4	eqtr4i	|- G = ( x e. A |-> ( H ` B ) )
6	1	adantl	|- ( ( H Fn C /\ x e. A ) -> B e. C )
7		df-mpt	|- ( x e. A |-> B ) = { <. x , y >. | ( x e. A /\ y = B ) }
8	2 7	eqtr4i	|- F = ( x e. A |-> B )
9	8	a1i	|- ( H Fn C -> F = ( x e. A |-> B ) )
10		dffn5	|- ( H Fn C <-> H = ( y e. C |-> ( H ` y ) ) )
11	10	biimpi	|- ( H Fn C -> H = ( y e. C |-> ( H ` y ) ) )
12		fveq2	|- ( y = B -> ( H ` y ) = ( H ` B ) )
13	6 9 11 12	fmptco	|- ( H Fn C -> ( H o. F ) = ( x e. A |-> ( H ` B ) ) )
14	5 13	eqtr4id	|- ( H Fn C -> G = ( H o. F ) )