Metamath Proof Explorer


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 ( 𝑅 × 𝑆 ) → 𝐺 = ( 𝑀𝐹 ) )