Description: The double opposite category has the same composition as the original category. Intended for use with property lemmas such as monpropd . (Contributed by Mario Carneiro, 3-Jan-2017)
Ref | Expression | ||
---|---|---|---|
Hypothesis | oppcbas.1 | |
|
Assertion | 2oppccomf | |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | oppcbas.1 | |
|
2 | eqid | |
|
3 | 1 2 | oppcbas | |
4 | eqid | |
|
5 | eqid | |
|
6 | simpr1 | |
|
7 | simpr2 | |
|
8 | simpr3 | |
|
9 | 3 4 5 6 7 8 | oppcco | |
10 | eqid | |
|
11 | 2 10 1 8 7 6 | oppcco | |
12 | 9 11 | eqtr2d | |
13 | 12 | ralrimivw | |
14 | 13 | ralrimivw | |
15 | 14 | ralrimivvva | |
16 | eqid | |
|
17 | eqid | |
|
18 | eqidd | |
|
19 | 1 2 | 2oppcbas | |
20 | 19 | a1i | |
21 | 1 | 2oppchomf | |
22 | 21 | a1i | |
23 | 10 16 17 18 20 22 | comfeq | |
24 | 15 23 | mpbird | |
25 | 24 | mptru | |