Metamath Proof Explorer

Theorem funcsect

Description: The image of a section under a functor is a section. (Contributed by Mario Carneiro, 2-Jan-2017)

Ref Expression
Hypotheses funcsect.b 
|- B = ( Base ` D )
funcsect.s 
|- S = ( Sect ` D )
funcsect.t 
|- T = ( Sect ` E )
funcsect.f 
|- ( ph -> F ( D Func E ) G )
funcsect.x 
|- ( ph -> X e. B )
funcsect.y 
|- ( ph -> Y e. B )
funcsect.m 
|- ( ph -> M ( X S Y ) N )
Assertion funcsect 
|- ( ph -> ( ( X G Y ) ` M ) ( ( F ` X ) T ( F ` Y ) ) ( ( Y G X ) ` N ) )

Proof

Step Hyp Ref Expression
1 funcsect.b 
 |-  B = ( Base ` D )
2 funcsect.s 
 |-  S = ( Sect ` D )
3 funcsect.t 
 |-  T = ( Sect ` E )
4 funcsect.f 
 |-  ( ph -> F ( D Func E ) G )
5 funcsect.x 
 |-  ( ph -> X e. B )
6 funcsect.y 
 |-  ( ph -> Y e. B )
7 funcsect.m 
 |-  ( ph -> M ( X S Y ) N )
8 eqid 
 |-  ( Hom ` D ) = ( Hom ` D )
9 eqid 
 |-  ( comp ` D ) = ( comp ` D )
10 eqid 
 |-  ( Id ` D ) = ( Id ` D )
11 df-br 
 |-  ( F ( D Func E ) G <-> <. F , G >. e. ( D Func E ) )
12 4 11 sylib 
 |-  ( ph -> <. F , G >. e. ( D Func E ) )
13 funcrcl 
 |-  ( <. F , G >. e. ( D Func E ) -> ( D e. Cat /\ E e. Cat ) )
14 12 13 syl 
 |-  ( ph -> ( D e. Cat /\ E e. Cat ) )
15 14 simpld 
 |-  ( ph -> D e. Cat )
16 1 8 9 10 2 15 5 6 issect 
 |-  ( ph -> ( M ( X S Y ) N <-> ( M e. ( X ( Hom ` D ) Y ) /\ N e. ( Y ( Hom ` D ) X ) /\ ( N ( <. X , Y >. ( comp ` D ) X ) M ) = ( ( Id ` D ) ` X ) ) ) )
17 7 16 mpbid 
 |-  ( ph -> ( M e. ( X ( Hom ` D ) Y ) /\ N e. ( Y ( Hom ` D ) X ) /\ ( N ( <. X , Y >. ( comp ` D ) X ) M ) = ( ( Id ` D ) ` X ) ) )
18 17 simp3d 
 |-  ( ph -> ( N ( <. X , Y >. ( comp ` D ) X ) M ) = ( ( Id ` D ) ` X ) )
19 18 fveq2d 
 |-  ( ph -> ( ( X G X ) ` ( N ( <. X , Y >. ( comp ` D ) X ) M ) ) = ( ( X G X ) ` ( ( Id ` D ) ` X ) ) )
20 eqid 
 |-  ( comp ` E ) = ( comp ` E )
21 17 simp1d 
 |-  ( ph -> M e. ( X ( Hom ` D ) Y ) )
22 17 simp2d 
 |-  ( ph -> N e. ( Y ( Hom ` D ) X ) )
23 1 8 9 20 4 5 6 5 21 22 funcco 
 |-  ( ph -> ( ( X G X ) ` ( N ( <. X , Y >. ( comp ` D ) X ) M ) ) = ( ( ( Y G X ) ` N ) ( <. ( F ` X ) , ( F ` Y ) >. ( comp ` E ) ( F ` X ) ) ( ( X G Y ) ` M ) ) )
24 eqid 
 |-  ( Id ` E ) = ( Id ` E )
25 1 10 24 4 5 funcid 
 |-  ( ph -> ( ( X G X ) ` ( ( Id ` D ) ` X ) ) = ( ( Id ` E ) ` ( F ` X ) ) )
26 19 23 25 3eqtr3d 
 |-  ( ph -> ( ( ( Y G X ) ` N ) ( <. ( F ` X ) , ( F ` Y ) >. ( comp ` E ) ( F ` X ) ) ( ( X G Y ) ` M ) ) = ( ( Id ` E ) ` ( F ` X ) ) )
27 eqid 
 |-  ( Base ` E ) = ( Base ` E )
28 eqid 
 |-  ( Hom ` E ) = ( Hom ` E )
29 14 simprd 
 |-  ( ph -> E e. Cat )
30 1 27 4 funcf1 
 |-  ( ph -> F : B --> ( Base ` E ) )
31 30 5 ffvelrnd 
 |-  ( ph -> ( F ` X ) e. ( Base ` E ) )
32 30 6 ffvelrnd 
 |-  ( ph -> ( F ` Y ) e. ( Base ` E ) )
33 1 8 28 4 5 6 funcf2 
 |-  ( ph -> ( X G Y ) : ( X ( Hom ` D ) Y ) --> ( ( F ` X ) ( Hom ` E ) ( F ` Y ) ) )
34 33 21 ffvelrnd 
 |-  ( ph -> ( ( X G Y ) ` M ) e. ( ( F ` X ) ( Hom ` E ) ( F ` Y ) ) )
35 1 8 28 4 6 5 funcf2 
 |-  ( ph -> ( Y G X ) : ( Y ( Hom ` D ) X ) --> ( ( F ` Y ) ( Hom ` E ) ( F ` X ) ) )
36 35 22 ffvelrnd 
 |-  ( ph -> ( ( Y G X ) ` N ) e. ( ( F ` Y ) ( Hom ` E ) ( F ` X ) ) )
37 27 28 20 24 3 29 31 32 34 36 issect2 
 |-  ( ph -> ( ( ( X G Y ) ` M ) ( ( F ` X ) T ( F ` Y ) ) ( ( Y G X ) ` N ) <-> ( ( ( Y G X ) ` N ) ( <. ( F ` X ) , ( F ` Y ) >. ( comp ` E ) ( F ` X ) ) ( ( X G Y ) ` M ) ) = ( ( Id ` E ) ` ( F ` X ) ) ) )
38 26 37 mpbird 
 |-  ( ph -> ( ( X G Y ) ` M ) ( ( F ` X ) T ( F ` Y ) ) ( ( Y G X ) ` N ) )