Metamath Proof Explorer

Theorem diag2

Description: Value of the diagonal functor at a morphism. (Contributed by Mario Carneiro, 7-Jan-2017)

Ref Expression
Hypotheses diag2.l 
|- L = ( C DiagFunc D )
diag2.a 
|- A = ( Base ` C )
diag2.b 
|- B = ( Base ` D )
diag2.h 
|- H = ( Hom ` C )
diag2.c 
|- ( ph -> C e. Cat )
diag2.d 
|- ( ph -> D e. Cat )
diag2.x 
|- ( ph -> X e. A )
diag2.y 
|- ( ph -> Y e. A )
diag2.f 
|- ( ph -> F e. ( X H Y ) )
Assertion diag2 
|- ( ph -> ( ( X ( 2nd ` L ) Y ) ` F ) = ( B X. { F } ) )

Proof

Step Hyp Ref Expression
1 diag2.l 
 |-  L = ( C DiagFunc D )
2 diag2.a 
 |-  A = ( Base ` C )
3 diag2.b 
 |-  B = ( Base ` D )
4 diag2.h 
 |-  H = ( Hom ` C )
5 diag2.c 
 |-  ( ph -> C e. Cat )
6 diag2.d 
 |-  ( ph -> D e. Cat )
7 diag2.x 
 |-  ( ph -> X e. A )
8 diag2.y 
 |-  ( ph -> Y e. A )
9 diag2.f 
 |-  ( ph -> F e. ( X H Y ) )
10 1 5 6 diagval 
 |-  ( ph -> L = ( <. C , D >. curryF ( C 1stF D ) ) )
11 10 fveq2d 
 |-  ( ph -> ( 2nd ` L ) = ( 2nd ` ( <. C , D >. curryF ( C 1stF D ) ) ) )
12 11 oveqd 
 |-  ( ph -> ( X ( 2nd ` L ) Y ) = ( X ( 2nd ` ( <. C , D >. curryF ( C 1stF D ) ) ) Y ) )
13 12 fveq1d 
 |-  ( ph -> ( ( X ( 2nd ` L ) Y ) ` F ) = ( ( X ( 2nd ` ( <. C , D >. curryF ( C 1stF D ) ) ) Y ) ` F ) )
14 eqid 
 |-  ( <. C , D >. curryF ( C 1stF D ) ) = ( <. C , D >. curryF ( C 1stF D ) )
15 eqid 
 |-  ( C Xc. D ) = ( C Xc. D )
16 eqid 
 |-  ( C 1stF D ) = ( C 1stF D )
17 15 5 6 16 1stfcl 
 |-  ( ph -> ( C 1stF D ) e. ( ( C Xc. D ) Func C ) )
18 eqid 
 |-  ( Id ` D ) = ( Id ` D )
19 eqid 
 |-  ( ( X ( 2nd ` ( <. C , D >. curryF ( C 1stF D ) ) ) Y ) ` F ) = ( ( X ( 2nd ` ( <. C , D >. curryF ( C 1stF D ) ) ) Y ) ` F )
20 14 2 5 6 17 3 4 18 7 8 9 19 curf2 
 |-  ( ph -> ( ( X ( 2nd ` ( <. C , D >. curryF ( C 1stF D ) ) ) Y ) ` F ) = ( x e. B |-> ( F ( <. X , x >. ( 2nd ` ( C 1stF D ) ) <. Y , x >. ) ( ( Id ` D ) ` x ) ) ) )
21 15 2 3 xpcbas 
 |-  ( A X. B ) = ( Base ` ( C Xc. D ) )
22 eqid 
 |-  ( Hom ` ( C Xc. D ) ) = ( Hom ` ( C Xc. D ) )
23 5 adantr 
 |-  ( ( ph /\ x e. B ) -> C e. Cat )
24 6 adantr 
 |-  ( ( ph /\ x e. B ) -> D e. Cat )
25 opelxpi 
 |-  ( ( X e. A /\ x e. B ) -> <. X , x >. e. ( A X. B ) )
26 7 25 sylan 
 |-  ( ( ph /\ x e. B ) -> <. X , x >. e. ( A X. B ) )
27 opelxpi 
 |-  ( ( Y e. A /\ x e. B ) -> <. Y , x >. e. ( A X. B ) )
28 8 27 sylan 
 |-  ( ( ph /\ x e. B ) -> <. Y , x >. e. ( A X. B ) )
29 15 21 22 23 24 16 26 28 1stf2 
 |-  ( ( ph /\ x e. B ) -> ( <. X , x >. ( 2nd ` ( C 1stF D ) ) <. Y , x >. ) = ( 1st |` ( <. X , x >. ( Hom ` ( C Xc. D ) ) <. Y , x >. ) ) )
30 29 oveqd 
 |-  ( ( ph /\ x e. B ) -> ( F ( <. X , x >. ( 2nd ` ( C 1stF D ) ) <. Y , x >. ) ( ( Id ` D ) ` x ) ) = ( F ( 1st |` ( <. X , x >. ( Hom ` ( C Xc. D ) ) <. Y , x >. ) ) ( ( Id ` D ) ` x ) ) )
31 df-ov 
 |-  ( F ( 1st |` ( <. X , x >. ( Hom ` ( C Xc. D ) ) <. Y , x >. ) ) ( ( Id ` D ) ` x ) ) = ( ( 1st |` ( <. X , x >. ( Hom ` ( C Xc. D ) ) <. Y , x >. ) ) ` <. F , ( ( Id ` D ) ` x ) >. )
32 9 adantr 
 |-  ( ( ph /\ x e. B ) -> F e. ( X H Y ) )
33 eqid 
 |-  ( Hom ` D ) = ( Hom ` D )
34 simpr 
 |-  ( ( ph /\ x e. B ) -> x e. B )
35 3 33 18 24 34 catidcl 
 |-  ( ( ph /\ x e. B ) -> ( ( Id ` D ) ` x ) e. ( x ( Hom ` D ) x ) )
36 32 35 opelxpd 
 |-  ( ( ph /\ x e. B ) -> <. F , ( ( Id ` D ) ` x ) >. e. ( ( X H Y ) X. ( x ( Hom ` D ) x ) ) )
37 7 adantr 
 |-  ( ( ph /\ x e. B ) -> X e. A )
38 8 adantr 
 |-  ( ( ph /\ x e. B ) -> Y e. A )
39 15 2 3 4 33 37 34 38 34 22 xpchom2 
 |-  ( ( ph /\ x e. B ) -> ( <. X , x >. ( Hom ` ( C Xc. D ) ) <. Y , x >. ) = ( ( X H Y ) X. ( x ( Hom ` D ) x ) ) )
40 36 39 eleqtrrd 
 |-  ( ( ph /\ x e. B ) -> <. F , ( ( Id ` D ) ` x ) >. e. ( <. X , x >. ( Hom ` ( C Xc. D ) ) <. Y , x >. ) )
41 40 fvresd 
 |-  ( ( ph /\ x e. B ) -> ( ( 1st |` ( <. X , x >. ( Hom ` ( C Xc. D ) ) <. Y , x >. ) ) ` <. F , ( ( Id ` D ) ` x ) >. ) = ( 1st ` <. F , ( ( Id ` D ) ` x ) >. ) )
42 31 41 eqtrid 
 |-  ( ( ph /\ x e. B ) -> ( F ( 1st |` ( <. X , x >. ( Hom ` ( C Xc. D ) ) <. Y , x >. ) ) ( ( Id ` D ) ` x ) ) = ( 1st ` <. F , ( ( Id ` D ) ` x ) >. ) )
43 op1stg 
 |-  ( ( F e. ( X H Y ) /\ ( ( Id ` D ) ` x ) e. ( x ( Hom ` D ) x ) ) -> ( 1st ` <. F , ( ( Id ` D ) ` x ) >. ) = F )
44 9 35 43 syl2an2r 
 |-  ( ( ph /\ x e. B ) -> ( 1st ` <. F , ( ( Id ` D ) ` x ) >. ) = F )
45 30 42 44 3eqtrd 
 |-  ( ( ph /\ x e. B ) -> ( F ( <. X , x >. ( 2nd ` ( C 1stF D ) ) <. Y , x >. ) ( ( Id ` D ) ` x ) ) = F )
46 45 mpteq2dva 
 |-  ( ph -> ( x e. B |-> ( F ( <. X , x >. ( 2nd ` ( C 1stF D ) ) <. Y , x >. ) ( ( Id ` D ) ` x ) ) ) = ( x e. B |-> F ) )
47 fconstmpt 
 |-  ( B X. { F } ) = ( x e. B |-> F )
48 46 47 eqtr4di 
 |-  ( ph -> ( x e. B |-> ( F ( <. X , x >. ( 2nd ` ( C 1stF D ) ) <. Y , x >. ) ( ( Id ` D ) ` x ) ) ) = ( B X. { F } ) )
49 13 20 48 3eqtrd 
 |-  ( ph -> ( ( X ( 2nd ` L ) Y ) ` F ) = ( B X. { F } ) )