Metamath Proof Explorer

Theorem cofuswapf2

Description: The morphism part of a bifunctor pre-composed with a swap functor. (Contributed by Zhi Wang, 9-Oct-2025)

Ref Expression
Hypotheses cofuswapf1.c 
|- ( ph -> C e. Cat )
cofuswapf1.d 
|- ( ph -> D e. Cat )
cofuswapf1.f 
|- ( ph -> F e. ( ( D Xc. C ) Func E ) )
cofuswapf1.g 
|- ( ph -> G = ( F o.func ( C swapF D ) ) )
cofuswapf1.a 
|- A = ( Base ` C )
cofuswapf1.b 
|- B = ( Base ` D )
cofuswapf1.x 
|- ( ph -> X e. A )
cofuswapf1.y 
|- ( ph -> Y e. B )
cofuswapf2.z 
|- ( ph -> Z e. A )
cofuswapf2.w 
|- ( ph -> W e. B )
cofuswapf2.h 
|- H = ( Hom ` C )
cofuswapf2.j 
|- J = ( Hom ` D )
cofuswapf2.m 
|- ( ph -> M e. ( X H Z ) )
cofuswapf2.n 
|- ( ph -> N e. ( Y J W ) )
Assertion cofuswapf2 
|- ( ph -> ( M ( <. X , Y >. ( 2nd ` G ) <. Z , W >. ) N ) = ( N ( <. Y , X >. ( 2nd ` F ) <. W , Z >. ) M ) )

Proof

Step Hyp Ref Expression
1 cofuswapf1.c 
 |-  ( ph -> C e. Cat )
2 cofuswapf1.d 
 |-  ( ph -> D e. Cat )
3 cofuswapf1.f 
 |-  ( ph -> F e. ( ( D Xc. C ) Func E ) )
4 cofuswapf1.g 
 |-  ( ph -> G = ( F o.func ( C swapF D ) ) )
5 cofuswapf1.a 
 |-  A = ( Base ` C )
6 cofuswapf1.b 
 |-  B = ( Base ` D )
7 cofuswapf1.x 
 |-  ( ph -> X e. A )
8 cofuswapf1.y 
 |-  ( ph -> Y e. B )
9 cofuswapf2.z 
 |-  ( ph -> Z e. A )
10 cofuswapf2.w 
 |-  ( ph -> W e. B )
11 cofuswapf2.h 
 |-  H = ( Hom ` C )
12 cofuswapf2.j 
 |-  J = ( Hom ` D )
13 cofuswapf2.m 
 |-  ( ph -> M e. ( X H Z ) )
14 cofuswapf2.n 
 |-  ( ph -> N e. ( Y J W ) )
15 4 fveq2d 
 |-  ( ph -> ( 2nd ` G ) = ( 2nd ` ( F o.func ( C swapF D ) ) ) )
16 15 oveqd 
 |-  ( ph -> ( <. X , Y >. ( 2nd ` G ) <. Z , W >. ) = ( <. X , Y >. ( 2nd ` ( F o.func ( C swapF D ) ) ) <. Z , W >. ) )
17 16 oveqd 
 |-  ( ph -> ( M ( <. X , Y >. ( 2nd ` G ) <. Z , W >. ) N ) = ( M ( <. X , Y >. ( 2nd ` ( F o.func ( C swapF D ) ) ) <. Z , W >. ) N ) )
18 df-ov 
 |-  ( M ( <. X , Y >. ( 2nd ` ( F o.func ( C swapF D ) ) ) <. Z , W >. ) N ) = ( ( <. X , Y >. ( 2nd ` ( F o.func ( C swapF D ) ) ) <. Z , W >. ) ` <. M , N >. )
19 eqid 
 |-  ( C Xc. D ) = ( C Xc. D )
20 19 5 6 xpcbas 
 |-  ( A X. B ) = ( Base ` ( C Xc. D ) )
21 eqid 
 |-  ( D Xc. C ) = ( D Xc. C )
22 1 2 19 21 swapffunca 
 |-  ( ph -> ( C swapF D ) e. ( ( C Xc. D ) Func ( D Xc. C ) ) )
23 7 8 opelxpd 
 |-  ( ph -> <. X , Y >. e. ( A X. B ) )
24 9 10 opelxpd 
 |-  ( ph -> <. Z , W >. e. ( A X. B ) )
25 eqid 
 |-  ( Hom ` ( C Xc. D ) ) = ( Hom ` ( C Xc. D ) )
26 13 14 opelxpd 
 |-  ( ph -> <. M , N >. e. ( ( X H Z ) X. ( Y J W ) ) )
27 19 5 6 11 12 7 8 9 10 25 xpchom2 
 |-  ( ph -> ( <. X , Y >. ( Hom ` ( C Xc. D ) ) <. Z , W >. ) = ( ( X H Z ) X. ( Y J W ) ) )
28 26 27 eleqtrrd 
 |-  ( ph -> <. M , N >. e. ( <. X , Y >. ( Hom ` ( C Xc. D ) ) <. Z , W >. ) )
29 20 22 3 23 24 25 28 cofu2 
 |-  ( ph -> ( ( <. X , Y >. ( 2nd ` ( F o.func ( C swapF D ) ) ) <. Z , W >. ) ` <. M , N >. ) = ( ( ( ( 1st ` ( C swapF D ) ) ` <. X , Y >. ) ( 2nd ` F ) ( ( 1st ` ( C swapF D ) ) ` <. Z , W >. ) ) ` ( ( <. X , Y >. ( 2nd ` ( C swapF D ) ) <. Z , W >. ) ` <. M , N >. ) ) )
30 18 29 eqtrid 
 |-  ( ph -> ( M ( <. X , Y >. ( 2nd ` ( F o.func ( C swapF D ) ) ) <. Z , W >. ) N ) = ( ( ( ( 1st ` ( C swapF D ) ) ` <. X , Y >. ) ( 2nd ` F ) ( ( 1st ` ( C swapF D ) ) ` <. Z , W >. ) ) ` ( ( <. X , Y >. ( 2nd ` ( C swapF D ) ) <. Z , W >. ) ` <. M , N >. ) ) )
31 df-ov 
 |-  ( X ( 1st ` ( C swapF D ) ) Y ) = ( ( 1st ` ( C swapF D ) ) ` <. X , Y >. )
32 1 2 swapfelvv 
 |-  ( ph -> ( C swapF D ) e. ( _V X. _V ) )
33 1st2nd2 
 |-  ( ( C swapF D ) e. ( _V X. _V ) -> ( C swapF D ) = <. ( 1st ` ( C swapF D ) ) , ( 2nd ` ( C swapF D ) ) >. )
34 32 33 syl 
 |-  ( ph -> ( C swapF D ) = <. ( 1st ` ( C swapF D ) ) , ( 2nd ` ( C swapF D ) ) >. )
35 7 5 eleqtrdi 
 |-  ( ph -> X e. ( Base ` C ) )
36 8 6 eleqtrdi 
 |-  ( ph -> Y e. ( Base ` D ) )
37 34 35 36 swapf1 
 |-  ( ph -> ( X ( 1st ` ( C swapF D ) ) Y ) = <. Y , X >. )
38 31 37 eqtr3id 
 |-  ( ph -> ( ( 1st ` ( C swapF D ) ) ` <. X , Y >. ) = <. Y , X >. )
39 df-ov 
 |-  ( Z ( 1st ` ( C swapF D ) ) W ) = ( ( 1st ` ( C swapF D ) ) ` <. Z , W >. )
40 9 5 eleqtrdi 
 |-  ( ph -> Z e. ( Base ` C ) )
41 10 6 eleqtrdi 
 |-  ( ph -> W e. ( Base ` D ) )
42 34 40 41 swapf1 
 |-  ( ph -> ( Z ( 1st ` ( C swapF D ) ) W ) = <. W , Z >. )
43 39 42 eqtr3id 
 |-  ( ph -> ( ( 1st ` ( C swapF D ) ) ` <. Z , W >. ) = <. W , Z >. )
44 38 43 oveq12d 
 |-  ( ph -> ( ( ( 1st ` ( C swapF D ) ) ` <. X , Y >. ) ( 2nd ` F ) ( ( 1st ` ( C swapF D ) ) ` <. Z , W >. ) ) = ( <. Y , X >. ( 2nd ` F ) <. W , Z >. ) )
45 df-ov 
 |-  ( M ( <. X , Y >. ( 2nd ` ( C swapF D ) ) <. Z , W >. ) N ) = ( ( <. X , Y >. ( 2nd ` ( C swapF D ) ) <. Z , W >. ) ` <. M , N >. )
46 11 oveqi 
 |-  ( X H Z ) = ( X ( Hom ` C ) Z )
47 13 46 eleqtrdi 
 |-  ( ph -> M e. ( X ( Hom ` C ) Z ) )
48 12 oveqi 
 |-  ( Y J W ) = ( Y ( Hom ` D ) W )
49 14 48 eleqtrdi 
 |-  ( ph -> N e. ( Y ( Hom ` D ) W ) )
50 34 35 36 40 41 47 49 swapf2 
 |-  ( ph -> ( M ( <. X , Y >. ( 2nd ` ( C swapF D ) ) <. Z , W >. ) N ) = <. N , M >. )
51 45 50 eqtr3id 
 |-  ( ph -> ( ( <. X , Y >. ( 2nd ` ( C swapF D ) ) <. Z , W >. ) ` <. M , N >. ) = <. N , M >. )
52 44 51 fveq12d 
 |-  ( ph -> ( ( ( ( 1st ` ( C swapF D ) ) ` <. X , Y >. ) ( 2nd ` F ) ( ( 1st ` ( C swapF D ) ) ` <. Z , W >. ) ) ` ( ( <. X , Y >. ( 2nd ` ( C swapF D ) ) <. Z , W >. ) ` <. M , N >. ) ) = ( ( <. Y , X >. ( 2nd ` F ) <. W , Z >. ) ` <. N , M >. ) )
53 17 30 52 3eqtrd 
 |-  ( ph -> ( M ( <. X , Y >. ( 2nd ` G ) <. Z , W >. ) N ) = ( ( <. Y , X >. ( 2nd ` F ) <. W , Z >. ) ` <. N , M >. ) )
54 df-ov 
 |-  ( N ( <. Y , X >. ( 2nd ` F ) <. W , Z >. ) M ) = ( ( <. Y , X >. ( 2nd ` F ) <. W , Z >. ) ` <. N , M >. )
55 53 54 eqtr4di 
 |-  ( ph -> ( M ( <. X , Y >. ( 2nd ` G ) <. Z , W >. ) N ) = ( N ( <. Y , X >. ( 2nd ` F ) <. W , Z >. ) M ) )