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 
|- ( ( x e. A /\ y e. B ) -> C e. R )
oprab2co.2 
|- ( ( x e. A /\ y e. B ) -> D e. S )
oprab2co.3 
|- F = ( x e. A , y e. B |-> <. C , D >. )
oprab2co.4 
|- G = ( x e. A , y e. B |-> ( C M D ) )
Assertion oprab2co 
|- ( M Fn ( R X. S ) -> G = ( M o. F ) )

Proof

Step Hyp Ref Expression
1 oprab2co.1 
 |-  ( ( x e. A /\ y e. B ) -> C e. R )
2 oprab2co.2 
 |-  ( ( x e. A /\ y e. B ) -> D e. S )
3 oprab2co.3 
 |-  F = ( x e. A , y e. B |-> <. C , D >. )
4 oprab2co.4 
 |-  G = ( x e. A , y e. B |-> ( C M D ) )
5 1 2 opelxpd 
 |-  ( ( x e. A /\ y e. B ) -> <. C , D >. e. ( R X. S ) )
6 df-ov 
 |-  ( C M D ) = ( M ` <. C , D >. )
7 6 a1i 
 |-  ( ( x e. A /\ y e. B ) -> ( C M D ) = ( M ` <. C , D >. ) )
8 7 mpoeq3ia 
 |-  ( x e. A , y e. B |-> ( C M D ) ) = ( x e. A , y e. B |-> ( M ` <. C , D >. ) )
9 4 8 eqtri 
 |-  G = ( x e. A , y e. B |-> ( M ` <. C , D >. ) )
10 5 3 9 oprabco 
 |-  ( M Fn ( R X. S ) -> G = ( M o. F ) )