Theorem oprab2co

Description: Composition of operator abstractions. (Contributed by Jeff Madsen, 2-Sep-2009) (Revised by David Abernethy, 23-Apr-2013)

	Ref	Expression
Hypotheses	oprab2co.1	⊢ ( ( 𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐵 ) → 𝐶 ∈ 𝑅 )
	oprab2co.2	⊢ ( ( 𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐵 ) → 𝐷 ∈ 𝑆 )
	oprab2co.3	⊢ 𝐹 = ( 𝑥 ∈ 𝐴 , 𝑦 ∈ 𝐵 ↦ ⟨ 𝐶 , 𝐷 ⟩ )
	oprab2co.4	⊢ 𝐺 = ( 𝑥 ∈ 𝐴 , 𝑦 ∈ 𝐵 ↦ ( 𝐶 𝑀 𝐷 ) )
Assertion	oprab2co	⊢ ( 𝑀 Fn ( 𝑅 × 𝑆 ) → 𝐺 = ( 𝑀 ∘ 𝐹 ) )

Proof

Step	Hyp	Ref	Expression
1		oprab2co.1	⊢ ( ( 𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐵 ) → 𝐶 ∈ 𝑅 )
2		oprab2co.2	⊢ ( ( 𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐵 ) → 𝐷 ∈ 𝑆 )
3		oprab2co.3	⊢ 𝐹 = ( 𝑥 ∈ 𝐴 , 𝑦 ∈ 𝐵 ↦ ⟨ 𝐶 , 𝐷 ⟩ )
4		oprab2co.4	⊢ 𝐺 = ( 𝑥 ∈ 𝐴 , 𝑦 ∈ 𝐵 ↦ ( 𝐶 𝑀 𝐷 ) )
5	1 2	opelxpd	⊢ ( ( 𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐵 ) → ⟨ 𝐶 , 𝐷 ⟩ ∈ ( 𝑅 × 𝑆 ) )
6		df-ov	⊢ ( 𝐶 𝑀 𝐷 ) = ( 𝑀 ‘ ⟨ 𝐶 , 𝐷 ⟩ )
7	6	a1i	⊢ ( ( 𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐵 ) → ( 𝐶 𝑀 𝐷 ) = ( 𝑀 ‘ ⟨ 𝐶 , 𝐷 ⟩ ) )
8	7	mpoeq3ia	⊢ ( 𝑥 ∈ 𝐴 , 𝑦 ∈ 𝐵 ↦ ( 𝐶 𝑀 𝐷 ) ) = ( 𝑥 ∈ 𝐴 , 𝑦 ∈ 𝐵 ↦ ( 𝑀 ‘ ⟨ 𝐶 , 𝐷 ⟩ ) )
9	4 8	eqtri	⊢ 𝐺 = ( 𝑥 ∈ 𝐴 , 𝑦 ∈ 𝐵 ↦ ( 𝑀 ‘ ⟨ 𝐶 , 𝐷 ⟩ ) )
10	5 3 9	oprabco	⊢ ( 𝑀 Fn ( 𝑅 × 𝑆 ) → 𝐺 = ( 𝑀 ∘ 𝐹 ) )