Description: A section in the opposite category. (Contributed by Mario Carneiro, 3-Jan-2017)
Ref | Expression | ||
---|---|---|---|
Hypotheses | oppcsect.b | |
|
oppcsect.o | |
||
oppcsect.c | |
||
oppcsect.x | |
||
oppcsect.y | |
||
oppcsect.s | |
||
oppcsect.t | |
||
Assertion | oppcsect | |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | oppcsect.b | |
|
2 | oppcsect.o | |
|
3 | oppcsect.c | |
|
4 | oppcsect.x | |
|
5 | oppcsect.y | |
|
6 | oppcsect.s | |
|
7 | oppcsect.t | |
|
8 | eqid | |
|
9 | 4 | adantr | |
10 | 5 | adantr | |
11 | 1 8 2 9 10 9 | oppcco | |
12 | 3 | adantr | |
13 | eqid | |
|
14 | 2 13 | oppcid | |
15 | 12 14 | syl | |
16 | 15 | fveq1d | |
17 | 11 16 | eqeq12d | |
18 | 17 | pm5.32da | |
19 | df-3an | |
|
20 | eqid | |
|
21 | 20 2 | oppchom | |
22 | 21 | eleq2i | |
23 | 20 2 | oppchom | |
24 | 23 | eleq2i | |
25 | 22 24 | anbi12ci | |
26 | 25 | anbi1i | |
27 | 19 26 | bitri | |
28 | df-3an | |
|
29 | 18 27 28 | 3bitr4g | |
30 | 2 1 | oppcbas | |
31 | eqid | |
|
32 | eqid | |
|
33 | eqid | |
|
34 | 2 | oppccat | |
35 | 3 34 | syl | |
36 | 30 31 32 33 7 35 4 5 | issect | |
37 | 1 20 8 13 6 3 4 5 | issect | |
38 | 29 36 37 | 3bitr4d | |