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 ) )