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