Metamath Proof Explorer

Theorem fthsect

Description: A faithful functor reflects sections. (Contributed by Mario Carneiro, 27-Jan-2017)

Ref Expression
Hypotheses fthsect.b 
|- B = ( Base ` C )
fthsect.h 
|- H = ( Hom ` C )
fthsect.f 
|- ( ph -> F ( C Faith D ) G )
fthsect.x 
|- ( ph -> X e. B )
fthsect.y 
|- ( ph -> Y e. B )
fthsect.m 
|- ( ph -> M e. ( X H Y ) )
fthsect.n 
|- ( ph -> N e. ( Y H X ) )
fthsect.s 
|- S = ( Sect ` C )
fthsect.t 
|- T = ( Sect ` D )
Assertion fthsect 
|- ( ph -> ( M ( X S Y ) N <-> ( ( X G Y ) ` M ) ( ( F ` X ) T ( F ` Y ) ) ( ( Y G X ) ` N ) ) )

Proof

Step Hyp Ref Expression
1 fthsect.b 
 |-  B = ( Base ` C )
2 fthsect.h 
 |-  H = ( Hom ` C )
3 fthsect.f 
 |-  ( ph -> F ( C Faith D ) G )
4 fthsect.x 
 |-  ( ph -> X e. B )
5 fthsect.y 
 |-  ( ph -> Y e. B )
6 fthsect.m 
 |-  ( ph -> M e. ( X H Y ) )
7 fthsect.n 
 |-  ( ph -> N e. ( Y H X ) )
8 fthsect.s 
 |-  S = ( Sect ` C )
9 fthsect.t 
 |-  T = ( Sect ` D )
10 eqid 
 |-  ( Hom ` D ) = ( Hom ` D )
11 eqid 
 |-  ( comp ` C ) = ( comp ` C )
12 fthfunc 
 |-  ( C Faith D ) C_ ( C Func D )
13 12 ssbri 
 |-  ( F ( C Faith D ) G -> F ( C Func D ) G )
14 3 13 syl 
 |-  ( ph -> F ( C Func D ) G )
15 df-br 
 |-  ( F ( C Func D ) G <-> <. F , G >. e. ( C Func D ) )
16 14 15 sylib 
 |-  ( ph -> <. F , G >. e. ( C Func D ) )
17 funcrcl 
 |-  ( <. F , G >. e. ( C Func D ) -> ( C e. Cat /\ D e. Cat ) )
18 16 17 syl 
 |-  ( ph -> ( C e. Cat /\ D e. Cat ) )
19 18 simpld 
 |-  ( ph -> C e. Cat )
20 1 2 11 19 4 5 4 6 7 catcocl 
 |-  ( ph -> ( N ( <. X , Y >. ( comp ` C ) X ) M ) e. ( X H X ) )
21 eqid 
 |-  ( Id ` C ) = ( Id ` C )
22 1 2 21 19 4 catidcl 
 |-  ( ph -> ( ( Id ` C ) ` X ) e. ( X H X ) )
23 1 2 10 3 4 4 20 22 fthi 
 |-  ( ph -> ( ( ( X G X ) ` ( N ( <. X , Y >. ( comp ` C ) X ) M ) ) = ( ( X G X ) ` ( ( Id ` C ) ` X ) ) <-> ( N ( <. X , Y >. ( comp ` C ) X ) M ) = ( ( Id ` C ) ` X ) ) )
24 eqid 
 |-  ( comp ` D ) = ( comp ` D )
25 1 2 11 24 14 4 5 4 6 7 funcco 
 |-  ( ph -> ( ( X G X ) ` ( N ( <. X , Y >. ( comp ` C ) X ) M ) ) = ( ( ( Y G X ) ` N ) ( <. ( F ` X ) , ( F ` Y ) >. ( comp ` D ) ( F ` X ) ) ( ( X G Y ) ` M ) ) )
26 eqid 
 |-  ( Id ` D ) = ( Id ` D )
27 1 21 26 14 4 funcid 
 |-  ( ph -> ( ( X G X ) ` ( ( Id ` C ) ` X ) ) = ( ( Id ` D ) ` ( F ` X ) ) )
28 25 27 eqeq12d 
 |-  ( ph -> ( ( ( X G X ) ` ( N ( <. X , Y >. ( comp ` C ) X ) M ) ) = ( ( X G X ) ` ( ( Id ` C ) ` X ) ) <-> ( ( ( Y G X ) ` N ) ( <. ( F ` X ) , ( F ` Y ) >. ( comp ` D ) ( F ` X ) ) ( ( X G Y ) ` M ) ) = ( ( Id ` D ) ` ( F ` X ) ) ) )
29 23 28 bitr3d 
 |-  ( ph -> ( ( N ( <. X , Y >. ( comp ` C ) X ) M ) = ( ( Id ` C ) ` X ) <-> ( ( ( Y G X ) ` N ) ( <. ( F ` X ) , ( F ` Y ) >. ( comp ` D ) ( F ` X ) ) ( ( X G Y ) ` M ) ) = ( ( Id ` D ) ` ( F ` X ) ) ) )
30 1 2 11 21 8 19 4 5 6 7 issect2 
 |-  ( ph -> ( M ( X S Y ) N <-> ( N ( <. X , Y >. ( comp ` C ) X ) M ) = ( ( Id ` C ) ` X ) ) )
31 eqid 
 |-  ( Base ` D ) = ( Base ` D )
32 18 simprd 
 |-  ( ph -> D e. Cat )
33 1 31 14 funcf1 
 |-  ( ph -> F : B --> ( Base ` D ) )
34 33 4 ffvelrnd 
 |-  ( ph -> ( F ` X ) e. ( Base ` D ) )
35 33 5 ffvelrnd 
 |-  ( ph -> ( F ` Y ) e. ( Base ` D ) )
36 1 2 10 14 4 5 funcf2 
 |-  ( ph -> ( X G Y ) : ( X H Y ) --> ( ( F ` X ) ( Hom ` D ) ( F ` Y ) ) )
37 36 6 ffvelrnd 
 |-  ( ph -> ( ( X G Y ) ` M ) e. ( ( F ` X ) ( Hom ` D ) ( F ` Y ) ) )
38 1 2 10 14 5 4 funcf2 
 |-  ( ph -> ( Y G X ) : ( Y H X ) --> ( ( F ` Y ) ( Hom ` D ) ( F ` X ) ) )
39 38 7 ffvelrnd 
 |-  ( ph -> ( ( Y G X ) ` N ) e. ( ( F ` Y ) ( Hom ` D ) ( F ` X ) ) )
40 31 10 24 26 9 32 34 35 37 39 issect2 
 |-  ( ph -> ( ( ( X G Y ) ` M ) ( ( F ` X ) T ( F ` Y ) ) ( ( Y G X ) ` N ) <-> ( ( ( Y G X ) ` N ) ( <. ( F ` X ) , ( F ` Y ) >. ( comp ` D ) ( F ` X ) ) ( ( X G Y ) ` M ) ) = ( ( Id ` D ) ` ( F ` X ) ) ) )
41 29 30 40 3bitr4d 
 |-  ( ph -> ( M ( X S Y ) N <-> ( ( X G Y ) ` M ) ( ( F ` X ) T ( F ` Y ) ) ( ( Y G X ) ` N ) ) )