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	⊢ ( ( 𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐵 ) → 𝐶 ∈ 𝐷 )
	oprabco.2	⊢ 𝐹 = ( 𝑥 ∈ 𝐴 , 𝑦 ∈ 𝐵 ↦ 𝐶 )
	oprabco.3	⊢ 𝐺 = ( 𝑥 ∈ 𝐴 , 𝑦 ∈ 𝐵 ↦ ( 𝐻 ‘ 𝐶 ) )
Assertion	oprabco	⊢ ( 𝐻 Fn 𝐷 → 𝐺 = ( 𝐻 ∘ 𝐹 ) )

Proof

Step	Hyp	Ref	Expression
1		oprabco.1	⊢ ( ( 𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐵 ) → 𝐶 ∈ 𝐷 )
2		oprabco.2	⊢ 𝐹 = ( 𝑥 ∈ 𝐴 , 𝑦 ∈ 𝐵 ↦ 𝐶 )
3		oprabco.3	⊢ 𝐺 = ( 𝑥 ∈ 𝐴 , 𝑦 ∈ 𝐵 ↦ ( 𝐻 ‘ 𝐶 ) )
4	1	adantl	⊢ ( ( 𝐻 Fn 𝐷 ∧ ( 𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐵 ) ) → 𝐶 ∈ 𝐷 )
5	2	a1i	⊢ ( 𝐻 Fn 𝐷 → 𝐹 = ( 𝑥 ∈ 𝐴 , 𝑦 ∈ 𝐵 ↦ 𝐶 ) )
6		dffn5	⊢ ( 𝐻 Fn 𝐷 ↔ 𝐻 = ( 𝑧 ∈ 𝐷 ↦ ( 𝐻 ‘ 𝑧 ) ) )
7	6	biimpi	⊢ ( 𝐻 Fn 𝐷 → 𝐻 = ( 𝑧 ∈ 𝐷 ↦ ( 𝐻 ‘ 𝑧 ) ) )
8		fveq2	⊢ ( 𝑧 = 𝐶 → ( 𝐻 ‘ 𝑧 ) = ( 𝐻 ‘ 𝐶 ) )
9	4 5 7 8	fmpoco	⊢ ( 𝐻 Fn 𝐷 → ( 𝐻 ∘ 𝐹 ) = ( 𝑥 ∈ 𝐴 , 𝑦 ∈ 𝐵 ↦ ( 𝐻 ‘ 𝐶 ) ) )
10	3 9	eqtr4id	⊢ ( 𝐻 Fn 𝐷 → 𝐺 = ( 𝐻 ∘ 𝐹 ) )