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	⊢ ( 𝑥 ∈ 𝐴 → 𝐵 ∈ 𝐶 )
	fnopabco.2	⊢ 𝐹 = { ⟨ 𝑥 , 𝑦 ⟩ ∣ ( 𝑥 ∈ 𝐴 ∧ 𝑦 = 𝐵 ) }
	fnopabco.3	⊢ 𝐺 = { ⟨ 𝑥 , 𝑦 ⟩ ∣ ( 𝑥 ∈ 𝐴 ∧ 𝑦 = ( 𝐻 ‘ 𝐵 ) ) }
Assertion	fnopabco	⊢ ( 𝐻 Fn 𝐶 → 𝐺 = ( 𝐻 ∘ 𝐹 ) )

Proof

Step	Hyp	Ref	Expression
1		fnopabco.1	⊢ ( 𝑥 ∈ 𝐴 → 𝐵 ∈ 𝐶 )
2		fnopabco.2	⊢ 𝐹 = { ⟨ 𝑥 , 𝑦 ⟩ ∣ ( 𝑥 ∈ 𝐴 ∧ 𝑦 = 𝐵 ) }
3		fnopabco.3	⊢ 𝐺 = { ⟨ 𝑥 , 𝑦 ⟩ ∣ ( 𝑥 ∈ 𝐴 ∧ 𝑦 = ( 𝐻 ‘ 𝐵 ) ) }
4		df-mpt	⊢ ( 𝑥 ∈ 𝐴 ↦ ( 𝐻 ‘ 𝐵 ) ) = { ⟨ 𝑥 , 𝑦 ⟩ ∣ ( 𝑥 ∈ 𝐴 ∧ 𝑦 = ( 𝐻 ‘ 𝐵 ) ) }
5	3 4	eqtr4i	⊢ 𝐺 = ( 𝑥 ∈ 𝐴 ↦ ( 𝐻 ‘ 𝐵 ) )
6	1	adantl	⊢ ( ( 𝐻 Fn 𝐶 ∧ 𝑥 ∈ 𝐴 ) → 𝐵 ∈ 𝐶 )
7		df-mpt	⊢ ( 𝑥 ∈ 𝐴 ↦ 𝐵 ) = { ⟨ 𝑥 , 𝑦 ⟩ ∣ ( 𝑥 ∈ 𝐴 ∧ 𝑦 = 𝐵 ) }
8	2 7	eqtr4i	⊢ 𝐹 = ( 𝑥 ∈ 𝐴 ↦ 𝐵 )
9	8	a1i	⊢ ( 𝐻 Fn 𝐶 → 𝐹 = ( 𝑥 ∈ 𝐴 ↦ 𝐵 ) )
10		dffn5	⊢ ( 𝐻 Fn 𝐶 ↔ 𝐻 = ( 𝑦 ∈ 𝐶 ↦ ( 𝐻 ‘ 𝑦 ) ) )
11	10	biimpi	⊢ ( 𝐻 Fn 𝐶 → 𝐻 = ( 𝑦 ∈ 𝐶 ↦ ( 𝐻 ‘ 𝑦 ) ) )
12		fveq2	⊢ ( 𝑦 = 𝐵 → ( 𝐻 ‘ 𝑦 ) = ( 𝐻 ‘ 𝐵 ) )
13	6 9 11 12	fmptco	⊢ ( 𝐻 Fn 𝐶 → ( 𝐻 ∘ 𝐹 ) = ( 𝑥 ∈ 𝐴 ↦ ( 𝐻 ‘ 𝐵 ) ) )
14	5 13	eqtr4id	⊢ ( 𝐻 Fn 𝐶 → 𝐺 = ( 𝐻 ∘ 𝐹 ) )