Metamath Proof Explorer

Theorem oppcsect

Description: A section in the opposite category. (Contributed by Mario Carneiro, 3-Jan-2017)

Ref Expression
Hypotheses oppcsect.b 
|- B = ( Base ` C )
oppcsect.o 
|- O = ( oppCat ` C )
oppcsect.c 
|- ( ph -> C e. Cat )
oppcsect.x 
|- ( ph -> X e. B )
oppcsect.y 
|- ( ph -> Y e. B )
oppcsect.s 
|- S = ( Sect ` C )
oppcsect.t 
|- T = ( Sect ` O )
Assertion oppcsect 
|- ( ph -> ( F ( X T Y ) G <-> G ( X S Y ) F ) )

Proof

Step Hyp Ref Expression
1 oppcsect.b 
 |-  B = ( Base ` C )
2 oppcsect.o 
 |-  O = ( oppCat ` C )
3 oppcsect.c 
 |-  ( ph -> C e. Cat )
4 oppcsect.x 
 |-  ( ph -> X e. B )
5 oppcsect.y 
 |-  ( ph -> Y e. B )
6 oppcsect.s 
 |-  S = ( Sect ` C )
7 oppcsect.t 
 |-  T = ( Sect ` O )
8 eqid 
 |-  ( comp ` C ) = ( comp ` C )
9 4 adantr 
 |-  ( ( ph /\ ( G e. ( X ( Hom ` C ) Y ) /\ F e. ( Y ( Hom ` C ) X ) ) ) -> X e. B )
10 5 adantr 
 |-  ( ( ph /\ ( G e. ( X ( Hom ` C ) Y ) /\ F e. ( Y ( Hom ` C ) X ) ) ) -> Y e. B )
11 1 8 2 9 10 9 oppcco 
 |-  ( ( ph /\ ( G e. ( X ( Hom ` C ) Y ) /\ F e. ( Y ( Hom ` C ) X ) ) ) -> ( G ( <. X , Y >. ( comp ` O ) X ) F ) = ( F ( <. X , Y >. ( comp ` C ) X ) G ) )
12 3 adantr 
 |-  ( ( ph /\ ( G e. ( X ( Hom ` C ) Y ) /\ F e. ( Y ( Hom ` C ) X ) ) ) -> C e. Cat )
13 eqid 
 |-  ( Id ` C ) = ( Id ` C )
14 2 13 oppcid 
 |-  ( C e. Cat -> ( Id ` O ) = ( Id ` C ) )
15 12 14 syl 
 |-  ( ( ph /\ ( G e. ( X ( Hom ` C ) Y ) /\ F e. ( Y ( Hom ` C ) X ) ) ) -> ( Id ` O ) = ( Id ` C ) )
16 15 fveq1d 
 |-  ( ( ph /\ ( G e. ( X ( Hom ` C ) Y ) /\ F e. ( Y ( Hom ` C ) X ) ) ) -> ( ( Id ` O ) ` X ) = ( ( Id ` C ) ` X ) )
17 11 16 eqeq12d 
 |-  ( ( ph /\ ( G e. ( X ( Hom ` C ) Y ) /\ F e. ( Y ( Hom ` C ) X ) ) ) -> ( ( G ( <. X , Y >. ( comp ` O ) X ) F ) = ( ( Id ` O ) ` X ) <-> ( F ( <. X , Y >. ( comp ` C ) X ) G ) = ( ( Id ` C ) ` X ) ) )
18 17 pm5.32da 
 |-  ( ph -> ( ( ( G e. ( X ( Hom ` C ) Y ) /\ F e. ( Y ( Hom ` C ) X ) ) /\ ( G ( <. X , Y >. ( comp ` O ) X ) F ) = ( ( Id ` O ) ` X ) ) <-> ( ( G e. ( X ( Hom ` C ) Y ) /\ F e. ( Y ( Hom ` C ) X ) ) /\ ( F ( <. X , Y >. ( comp ` C ) X ) G ) = ( ( Id ` C ) ` X ) ) ) )
19 df-3an 
 |-  ( ( F e. ( X ( Hom ` O ) Y ) /\ G e. ( Y ( Hom ` O ) X ) /\ ( G ( <. X , Y >. ( comp ` O ) X ) F ) = ( ( Id ` O ) ` X ) ) <-> ( ( F e. ( X ( Hom ` O ) Y ) /\ G e. ( Y ( Hom ` O ) X ) ) /\ ( G ( <. X , Y >. ( comp ` O ) X ) F ) = ( ( Id ` O ) ` X ) ) )
20 eqid 
 |-  ( Hom ` C ) = ( Hom ` C )
21 20 2 oppchom 
 |-  ( X ( Hom ` O ) Y ) = ( Y ( Hom ` C ) X )
22 21 eleq2i 
 |-  ( F e. ( X ( Hom ` O ) Y ) <-> F e. ( Y ( Hom ` C ) X ) )
23 20 2 oppchom 
 |-  ( Y ( Hom ` O ) X ) = ( X ( Hom ` C ) Y )
24 23 eleq2i 
 |-  ( G e. ( Y ( Hom ` O ) X ) <-> G e. ( X ( Hom ` C ) Y ) )
25 22 24 anbi12ci 
 |-  ( ( F e. ( X ( Hom ` O ) Y ) /\ G e. ( Y ( Hom ` O ) X ) ) <-> ( G e. ( X ( Hom ` C ) Y ) /\ F e. ( Y ( Hom ` C ) X ) ) )
26 25 anbi1i 
 |-  ( ( ( F e. ( X ( Hom ` O ) Y ) /\ G e. ( Y ( Hom ` O ) X ) ) /\ ( G ( <. X , Y >. ( comp ` O ) X ) F ) = ( ( Id ` O ) ` X ) ) <-> ( ( G e. ( X ( Hom ` C ) Y ) /\ F e. ( Y ( Hom ` C ) X ) ) /\ ( G ( <. X , Y >. ( comp ` O ) X ) F ) = ( ( Id ` O ) ` X ) ) )
27 19 26 bitri 
 |-  ( ( F e. ( X ( Hom ` O ) Y ) /\ G e. ( Y ( Hom ` O ) X ) /\ ( G ( <. X , Y >. ( comp ` O ) X ) F ) = ( ( Id ` O ) ` X ) ) <-> ( ( G e. ( X ( Hom ` C ) Y ) /\ F e. ( Y ( Hom ` C ) X ) ) /\ ( G ( <. X , Y >. ( comp ` O ) X ) F ) = ( ( Id ` O ) ` X ) ) )
28 df-3an 
 |-  ( ( G e. ( X ( Hom ` C ) Y ) /\ F e. ( Y ( Hom ` C ) X ) /\ ( F ( <. X , Y >. ( comp ` C ) X ) G ) = ( ( Id ` C ) ` X ) ) <-> ( ( G e. ( X ( Hom ` C ) Y ) /\ F e. ( Y ( Hom ` C ) X ) ) /\ ( F ( <. X , Y >. ( comp ` C ) X ) G ) = ( ( Id ` C ) ` X ) ) )
29 18 27 28 3bitr4g 
 |-  ( ph -> ( ( F e. ( X ( Hom ` O ) Y ) /\ G e. ( Y ( Hom ` O ) X ) /\ ( G ( <. X , Y >. ( comp ` O ) X ) F ) = ( ( Id ` O ) ` X ) ) <-> ( G e. ( X ( Hom ` C ) Y ) /\ F e. ( Y ( Hom ` C ) X ) /\ ( F ( <. X , Y >. ( comp ` C ) X ) G ) = ( ( Id ` C ) ` X ) ) ) )
30 2 1 oppcbas 
 |-  B = ( Base ` O )
31 eqid 
 |-  ( Hom ` O ) = ( Hom ` O )
32 eqid 
 |-  ( comp ` O ) = ( comp ` O )
33 eqid 
 |-  ( Id ` O ) = ( Id ` O )
34 2 oppccat 
 |-  ( C e. Cat -> O e. Cat )
35 3 34 syl 
 |-  ( ph -> O e. Cat )
36 30 31 32 33 7 35 4 5 issect 
 |-  ( ph -> ( F ( X T Y ) G <-> ( F e. ( X ( Hom ` O ) Y ) /\ G e. ( Y ( Hom ` O ) X ) /\ ( G ( <. X , Y >. ( comp ` O ) X ) F ) = ( ( Id ` O ) ` X ) ) ) )
37 1 20 8 13 6 3 4 5 issect 
 |-  ( ph -> ( G ( X S Y ) F <-> ( G e. ( X ( Hom ` C ) Y ) /\ F e. ( Y ( Hom ` C ) X ) /\ ( F ( <. X , Y >. ( comp ` C ) X ) G ) = ( ( Id ` C ) ` X ) ) ) )
38 29 36 37 3bitr4d 
 |-  ( ph -> ( F ( X T Y ) G <-> G ( X S Y ) F ) )