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 xAyBCR
oprab2co.2 xAyBDS
oprab2co.3 F=xA,yBCD
oprab2co.4 G=xA,yBCMD
Assertion oprab2co MFnR×SG=MF

Proof

Step Hyp Ref Expression
1 oprab2co.1 xAyBCR
2 oprab2co.2 xAyBDS
3 oprab2co.3 F=xA,yBCD
4 oprab2co.4 G=xA,yBCMD
5 1 2 opelxpd xAyBCDR×S
6 df-ov CMD=MCD
7 6 a1i xAyBCMD=MCD
8 7 mpoeq3ia xA,yBCMD=xA,yBMCD
9 4 8 eqtri G=xA,yBMCD
10 5 3 9 oprabco MFnR×SG=MF