This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

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