Description: An inverse in the opposite category. (Contributed by Mario Carneiro, 3-Jan-2017)
Ref | Expression | ||
---|---|---|---|
Hypotheses | oppcsect.b | |
|
oppcsect.o | |
||
oppcsect.c | |
||
oppcsect.x | |
||
oppcsect.y | |
||
oppcinv.s | |
||
oppcinv.t | |
||
Assertion | oppcinv | |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | oppcsect.b | |
|
2 | oppcsect.o | |
|
3 | oppcsect.c | |
|
4 | oppcsect.x | |
|
5 | oppcsect.y | |
|
6 | oppcinv.s | |
|
7 | oppcinv.t | |
|
8 | incom | |
|
9 | eqid | |
|
10 | eqid | |
|
11 | 1 2 3 5 4 9 10 | oppcsect2 | |
12 | 11 | cnveqd | |
13 | eqid | |
|
14 | eqid | |
|
15 | eqid | |
|
16 | 1 13 14 15 9 3 5 4 | sectss | |
17 | relxp | |
|
18 | relss | |
|
19 | 16 17 18 | mpisyl | |
20 | dfrel2 | |
|
21 | 19 20 | sylib | |
22 | 12 21 | eqtrd | |
23 | 1 2 3 4 5 9 10 | oppcsect2 | |
24 | 22 23 | ineq12d | |
25 | 8 24 | eqtrid | |
26 | 2 1 | oppcbas | |
27 | 2 | oppccat | |
28 | 3 27 | syl | |
29 | 26 7 28 4 5 10 | invfval | |
30 | 1 6 3 5 4 9 | invfval | |
31 | 25 29 30 | 3eqtr4d | |