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\in A\to B\in C$$
	fnopabco.2	$$⊢F=\left\{⟨x,y⟩|\left(x\in A\wedge y=B\right)\right\}$$
	fnopabco.3	$$⊢G=\left\{⟨x,y⟩|\left(x\in A\wedge y=H\left(B\right)\right)\right\}$$
Assertion	fnopabco	$$⊢HFnC\to G=H\circ F$$

Proof

Step	Hyp	Ref	Expression
1		fnopabco.1	$$⊢x\in A\to B\in C$$
2		fnopabco.2	$$⊢F=\left\{⟨x,y⟩|\left(x\in A\wedge y=B\right)\right\}$$
3		fnopabco.3	$$⊢G=\left\{⟨x,y⟩|\left(x\in A\wedge y=H\left(B\right)\right)\right\}$$
4		df-mpt	$$⊢\left(x\in A⟼H\left(B\right)\right)=\left\{⟨x,y⟩|\left(x\in A\wedge y=H\left(B\right)\right)\right\}$$
5	3 4	eqtr4i	$$⊢G=\left(x\in A⟼H\left(B\right)\right)$$
6	1	adantl	$$⊢\left(HFnC\wedge x\in A\right)\to B\in C$$
7		df-mpt	$$⊢\left(x\in A⟼B\right)=\left\{⟨x,y⟩|\left(x\in A\wedge y=B\right)\right\}$$
8	2 7	eqtr4i	$$⊢F=\left(x\in A⟼B\right)$$
9	8	a1i	$$⊢HFnC\to F=\left(x\in A⟼B\right)$$
10		dffn5	$$⊢HFnC\leftrightarrow H=\left(y\in C⟼H\left(y\right)\right)$$
11	10	biimpi	$$⊢HFnC\to H=\left(y\in C⟼H\left(y\right)\right)$$
12		fveq2	$$⊢y=B\to H\left(y\right)=H\left(B\right)$$
13	6 9 11 12	fmptco	$$⊢HFnC\to H\circ F=\left(x\in A⟼H\left(B\right)\right)$$
14	5 13	eqtr4id	$$⊢HFnC\to G=H\circ F$$