Metamath Proof Explorer

Theorem swapfcoa

Description: Composition in the source category is mapped to composition in the target. ( ph -> C e. Cat ) and ( ph -> D e. Cat ) can be replaced by a weaker hypothesis ( ph -> S e. Cat ) . (Contributed by Zhi Wang, 8-Oct-2025)

Ref Expression
Hypotheses swapfid.c 
|- ( ph -> C e. Cat )
swapfid.d 
|- ( ph -> D e. Cat )
swapfid.s 
|- S = ( C Xc. D )
swapfid.t 
|- T = ( D Xc. C )
swapfid.o 
|- ( ph -> ( C swapF D ) = <. O , P >. )
swapfida.b 
|- B = ( Base ` S )
swapfida.x 
|- ( ph -> X e. B )
swapfcoa.y 
|- ( ph -> Y e. B )
swapfcoa.z 
|- ( ph -> Z e. B )
swapfcoa.h 
|- H = ( Hom ` S )
swapfcoa.m 
|- ( ph -> M e. ( X H Y ) )
swapfcoa.n 
|- ( ph -> N e. ( Y H Z ) )
swapfcoa.os 
|- .x. = ( comp ` S )
swapfcoa.ot 
|- .xb = ( comp ` T )
Assertion swapfcoa 
|- ( ph -> ( ( X P Z ) ` ( N ( <. X , Y >. .x. Z ) M ) ) = ( ( ( Y P Z ) ` N ) ( <. ( O ` X ) , ( O ` Y ) >. .xb ( O ` Z ) ) ( ( X P Y ) ` M ) ) )

Proof

Step Hyp Ref Expression
1 swapfid.c 
 |-  ( ph -> C e. Cat )
2 swapfid.d 
 |-  ( ph -> D e. Cat )
3 swapfid.s 
 |-  S = ( C Xc. D )
4 swapfid.t 
 |-  T = ( D Xc. C )
5 swapfid.o 
 |-  ( ph -> ( C swapF D ) = <. O , P >. )
6 swapfida.b 
 |-  B = ( Base ` S )
7 swapfida.x 
 |-  ( ph -> X e. B )
8 swapfcoa.y 
 |-  ( ph -> Y e. B )
9 swapfcoa.z 
 |-  ( ph -> Z e. B )
10 swapfcoa.h 
 |-  H = ( Hom ` S )
11 swapfcoa.m 
 |-  ( ph -> M e. ( X H Y ) )
12 swapfcoa.n 
 |-  ( ph -> N e. ( Y H Z ) )
13 swapfcoa.os 
 |-  .x. = ( comp ` S )
14 swapfcoa.ot 
 |-  .xb = ( comp ` T )
15 5 3 6 7 swapf1a 
 |-  ( ph -> ( O ` X ) = <. ( 2nd ` X ) , ( 1st ` X ) >. )
16 15 fveq2d 
 |-  ( ph -> ( 1st ` ( O ` X ) ) = ( 1st ` <. ( 2nd ` X ) , ( 1st ` X ) >. ) )
17 fvex 
 |-  ( 2nd ` X ) e. _V
18 fvex 
 |-  ( 1st ` X ) e. _V
19 17 18 op1st 
 |-  ( 1st ` <. ( 2nd ` X ) , ( 1st ` X ) >. ) = ( 2nd ` X )
20 16 19 eqtrdi 
 |-  ( ph -> ( 1st ` ( O ` X ) ) = ( 2nd ` X ) )
21 5 3 6 8 swapf1a 
 |-  ( ph -> ( O ` Y ) = <. ( 2nd ` Y ) , ( 1st ` Y ) >. )
22 21 fveq2d 
 |-  ( ph -> ( 1st ` ( O ` Y ) ) = ( 1st ` <. ( 2nd ` Y ) , ( 1st ` Y ) >. ) )
23 fvex 
 |-  ( 2nd ` Y ) e. _V
24 fvex 
 |-  ( 1st ` Y ) e. _V
25 23 24 op1st 
 |-  ( 1st ` <. ( 2nd ` Y ) , ( 1st ` Y ) >. ) = ( 2nd ` Y )
26 22 25 eqtrdi 
 |-  ( ph -> ( 1st ` ( O ` Y ) ) = ( 2nd ` Y ) )
27 20 26 opeq12d 
 |-  ( ph -> <. ( 1st ` ( O ` X ) ) , ( 1st ` ( O ` Y ) ) >. = <. ( 2nd ` X ) , ( 2nd ` Y ) >. )
28 5 3 6 9 swapf1a 
 |-  ( ph -> ( O ` Z ) = <. ( 2nd ` Z ) , ( 1st ` Z ) >. )
29 28 fveq2d 
 |-  ( ph -> ( 1st ` ( O ` Z ) ) = ( 1st ` <. ( 2nd ` Z ) , ( 1st ` Z ) >. ) )
30 fvex 
 |-  ( 2nd ` Z ) e. _V
31 fvex 
 |-  ( 1st ` Z ) e. _V
32 30 31 op1st 
 |-  ( 1st ` <. ( 2nd ` Z ) , ( 1st ` Z ) >. ) = ( 2nd ` Z )
33 29 32 eqtrdi 
 |-  ( ph -> ( 1st ` ( O ` Z ) ) = ( 2nd ` Z ) )
34 27 33 oveq12d 
 |-  ( ph -> ( <. ( 1st ` ( O ` X ) ) , ( 1st ` ( O ` Y ) ) >. ( comp ` D ) ( 1st ` ( O ` Z ) ) ) = ( <. ( 2nd ` X ) , ( 2nd ` Y ) >. ( comp ` D ) ( 2nd ` Z ) ) )
35 10 a1i 
 |-  ( ph -> H = ( Hom ` S ) )
36 5 3 6 8 9 35 12 swapf2a 
 |-  ( ph -> ( ( Y P Z ) ` N ) = <. ( 2nd ` N ) , ( 1st ` N ) >. )
37 36 fveq2d 
 |-  ( ph -> ( 1st ` ( ( Y P Z ) ` N ) ) = ( 1st ` <. ( 2nd ` N ) , ( 1st ` N ) >. ) )
38 fvex 
 |-  ( 2nd ` N ) e. _V
39 fvex 
 |-  ( 1st ` N ) e. _V
40 38 39 op1st 
 |-  ( 1st ` <. ( 2nd ` N ) , ( 1st ` N ) >. ) = ( 2nd ` N )
41 37 40 eqtrdi 
 |-  ( ph -> ( 1st ` ( ( Y P Z ) ` N ) ) = ( 2nd ` N ) )
42 5 3 6 7 8 35 11 swapf2a 
 |-  ( ph -> ( ( X P Y ) ` M ) = <. ( 2nd ` M ) , ( 1st ` M ) >. )
43 42 fveq2d 
 |-  ( ph -> ( 1st ` ( ( X P Y ) ` M ) ) = ( 1st ` <. ( 2nd ` M ) , ( 1st ` M ) >. ) )
44 fvex 
 |-  ( 2nd ` M ) e. _V
45 fvex 
 |-  ( 1st ` M ) e. _V
46 44 45 op1st 
 |-  ( 1st ` <. ( 2nd ` M ) , ( 1st ` M ) >. ) = ( 2nd ` M )
47 43 46 eqtrdi 
 |-  ( ph -> ( 1st ` ( ( X P Y ) ` M ) ) = ( 2nd ` M ) )
48 34 41 47 oveq123d 
 |-  ( ph -> ( ( 1st ` ( ( Y P Z ) ` N ) ) ( <. ( 1st ` ( O ` X ) ) , ( 1st ` ( O ` Y ) ) >. ( comp ` D ) ( 1st ` ( O ` Z ) ) ) ( 1st ` ( ( X P Y ) ` M ) ) ) = ( ( 2nd ` N ) ( <. ( 2nd ` X ) , ( 2nd ` Y ) >. ( comp ` D ) ( 2nd ` Z ) ) ( 2nd ` M ) ) )
49 15 fveq2d 
 |-  ( ph -> ( 2nd ` ( O ` X ) ) = ( 2nd ` <. ( 2nd ` X ) , ( 1st ` X ) >. ) )
50 17 18 op2nd 
 |-  ( 2nd ` <. ( 2nd ` X ) , ( 1st ` X ) >. ) = ( 1st ` X )
51 49 50 eqtrdi 
 |-  ( ph -> ( 2nd ` ( O ` X ) ) = ( 1st ` X ) )
52 21 fveq2d 
 |-  ( ph -> ( 2nd ` ( O ` Y ) ) = ( 2nd ` <. ( 2nd ` Y ) , ( 1st ` Y ) >. ) )
53 23 24 op2nd 
 |-  ( 2nd ` <. ( 2nd ` Y ) , ( 1st ` Y ) >. ) = ( 1st ` Y )
54 52 53 eqtrdi 
 |-  ( ph -> ( 2nd ` ( O ` Y ) ) = ( 1st ` Y ) )
55 51 54 opeq12d 
 |-  ( ph -> <. ( 2nd ` ( O ` X ) ) , ( 2nd ` ( O ` Y ) ) >. = <. ( 1st ` X ) , ( 1st ` Y ) >. )
56 28 fveq2d 
 |-  ( ph -> ( 2nd ` ( O ` Z ) ) = ( 2nd ` <. ( 2nd ` Z ) , ( 1st ` Z ) >. ) )
57 30 31 op2nd 
 |-  ( 2nd ` <. ( 2nd ` Z ) , ( 1st ` Z ) >. ) = ( 1st ` Z )
58 56 57 eqtrdi 
 |-  ( ph -> ( 2nd ` ( O ` Z ) ) = ( 1st ` Z ) )
59 55 58 oveq12d 
 |-  ( ph -> ( <. ( 2nd ` ( O ` X ) ) , ( 2nd ` ( O ` Y ) ) >. ( comp ` C ) ( 2nd ` ( O ` Z ) ) ) = ( <. ( 1st ` X ) , ( 1st ` Y ) >. ( comp ` C ) ( 1st ` Z ) ) )
60 36 fveq2d 
 |-  ( ph -> ( 2nd ` ( ( Y P Z ) ` N ) ) = ( 2nd ` <. ( 2nd ` N ) , ( 1st ` N ) >. ) )
61 38 39 op2nd 
 |-  ( 2nd ` <. ( 2nd ` N ) , ( 1st ` N ) >. ) = ( 1st ` N )
62 60 61 eqtrdi 
 |-  ( ph -> ( 2nd ` ( ( Y P Z ) ` N ) ) = ( 1st ` N ) )
63 42 fveq2d 
 |-  ( ph -> ( 2nd ` ( ( X P Y ) ` M ) ) = ( 2nd ` <. ( 2nd ` M ) , ( 1st ` M ) >. ) )
64 44 45 op2nd 
 |-  ( 2nd ` <. ( 2nd ` M ) , ( 1st ` M ) >. ) = ( 1st ` M )
65 63 64 eqtrdi 
 |-  ( ph -> ( 2nd ` ( ( X P Y ) ` M ) ) = ( 1st ` M ) )
66 59 62 65 oveq123d 
 |-  ( ph -> ( ( 2nd ` ( ( Y P Z ) ` N ) ) ( <. ( 2nd ` ( O ` X ) ) , ( 2nd ` ( O ` Y ) ) >. ( comp ` C ) ( 2nd ` ( O ` Z ) ) ) ( 2nd ` ( ( X P Y ) ` M ) ) ) = ( ( 1st ` N ) ( <. ( 1st ` X ) , ( 1st ` Y ) >. ( comp ` C ) ( 1st ` Z ) ) ( 1st ` M ) ) )
67 48 66 opeq12d 
 |-  ( ph -> <. ( ( 1st ` ( ( Y P Z ) ` N ) ) ( <. ( 1st ` ( O ` X ) ) , ( 1st ` ( O ` Y ) ) >. ( comp ` D ) ( 1st ` ( O ` Z ) ) ) ( 1st ` ( ( X P Y ) ` M ) ) ) , ( ( 2nd ` ( ( Y P Z ) ` N ) ) ( <. ( 2nd ` ( O ` X ) ) , ( 2nd ` ( O ` Y ) ) >. ( comp ` C ) ( 2nd ` ( O ` Z ) ) ) ( 2nd ` ( ( X P Y ) ` M ) ) ) >. = <. ( ( 2nd ` N ) ( <. ( 2nd ` X ) , ( 2nd ` Y ) >. ( comp ` D ) ( 2nd ` Z ) ) ( 2nd ` M ) ) , ( ( 1st ` N ) ( <. ( 1st ` X ) , ( 1st ` Y ) >. ( comp ` C ) ( 1st ` Z ) ) ( 1st ` M ) ) >. )
68 eqid 
 |-  ( Base ` T ) = ( Base ` T )
69 eqid 
 |-  ( Hom ` T ) = ( Hom ` T )
70 eqid 
 |-  ( comp ` D ) = ( comp ` D )
71 eqid 
 |-  ( comp ` C ) = ( comp ` C )
72 5 3 4 1 2 6 68 swapf1f1o 
 |-  ( ph -> O : B -1-1-onto-> ( Base ` T ) )
73 f1of 
 |-  ( O : B -1-1-onto-> ( Base ` T ) -> O : B --> ( Base ` T ) )
74 72 73 syl 
 |-  ( ph -> O : B --> ( Base ` T ) )
75 74 7 ffvelcdmd 
 |-  ( ph -> ( O ` X ) e. ( Base ` T ) )
76 74 8 ffvelcdmd 
 |-  ( ph -> ( O ` Y ) e. ( Base ` T ) )
77 74 9 ffvelcdmd 
 |-  ( ph -> ( O ` Z ) e. ( Base ` T ) )
78 5 3 4 10 69 6 7 8 swapf2f1oa 
 |-  ( ph -> ( X P Y ) : ( X H Y ) -1-1-onto-> ( ( O ` X ) ( Hom ` T ) ( O ` Y ) ) )
79 f1of 
 |-  ( ( X P Y ) : ( X H Y ) -1-1-onto-> ( ( O ` X ) ( Hom ` T ) ( O ` Y ) ) -> ( X P Y ) : ( X H Y ) --> ( ( O ` X ) ( Hom ` T ) ( O ` Y ) ) )
80 78 79 syl 
 |-  ( ph -> ( X P Y ) : ( X H Y ) --> ( ( O ` X ) ( Hom ` T ) ( O ` Y ) ) )
81 80 11 ffvelcdmd 
 |-  ( ph -> ( ( X P Y ) ` M ) e. ( ( O ` X ) ( Hom ` T ) ( O ` Y ) ) )
82 5 3 4 10 69 6 8 9 swapf2f1oa 
 |-  ( ph -> ( Y P Z ) : ( Y H Z ) -1-1-onto-> ( ( O ` Y ) ( Hom ` T ) ( O ` Z ) ) )
83 f1of 
 |-  ( ( Y P Z ) : ( Y H Z ) -1-1-onto-> ( ( O ` Y ) ( Hom ` T ) ( O ` Z ) ) -> ( Y P Z ) : ( Y H Z ) --> ( ( O ` Y ) ( Hom ` T ) ( O ` Z ) ) )
84 82 83 syl 
 |-  ( ph -> ( Y P Z ) : ( Y H Z ) --> ( ( O ` Y ) ( Hom ` T ) ( O ` Z ) ) )
85 84 12 ffvelcdmd 
 |-  ( ph -> ( ( Y P Z ) ` N ) e. ( ( O ` Y ) ( Hom ` T ) ( O ` Z ) ) )
86 4 68 69 70 71 14 75 76 77 81 85 xpcco 
 |-  ( ph -> ( ( ( Y P Z ) ` N ) ( <. ( O ` X ) , ( O ` Y ) >. .xb ( O ` Z ) ) ( ( X P Y ) ` M ) ) = <. ( ( 1st ` ( ( Y P Z ) ` N ) ) ( <. ( 1st ` ( O ` X ) ) , ( 1st ` ( O ` Y ) ) >. ( comp ` D ) ( 1st ` ( O ` Z ) ) ) ( 1st ` ( ( X P Y ) ` M ) ) ) , ( ( 2nd ` ( ( Y P Z ) ` N ) ) ( <. ( 2nd ` ( O ` X ) ) , ( 2nd ` ( O ` Y ) ) >. ( comp ` C ) ( 2nd ` ( O ` Z ) ) ) ( 2nd ` ( ( X P Y ) ` M ) ) ) >. )
87 3 6 10 71 70 13 7 8 9 11 12 xpcco 
 |-  ( ph -> ( N ( <. X , Y >. .x. Z ) M ) = <. ( ( 1st ` N ) ( <. ( 1st ` X ) , ( 1st ` Y ) >. ( comp ` C ) ( 1st ` Z ) ) ( 1st ` M ) ) , ( ( 2nd ` N ) ( <. ( 2nd ` X ) , ( 2nd ` Y ) >. ( comp ` D ) ( 2nd ` Z ) ) ( 2nd ` M ) ) >. )
88 87 fveq2d 
 |-  ( ph -> ( ( X P Z ) ` ( N ( <. X , Y >. .x. Z ) M ) ) = ( ( X P Z ) ` <. ( ( 1st ` N ) ( <. ( 1st ` X ) , ( 1st ` Y ) >. ( comp ` C ) ( 1st ` Z ) ) ( 1st ` M ) ) , ( ( 2nd ` N ) ( <. ( 2nd ` X ) , ( 2nd ` Y ) >. ( comp ` D ) ( 2nd ` Z ) ) ( 2nd ` M ) ) >. ) )
89 3 1 2 xpccat 
 |-  ( ph -> S e. Cat )
90 6 10 13 89 7 8 9 11 12 catcocl 
 |-  ( ph -> ( N ( <. X , Y >. .x. Z ) M ) e. ( X H Z ) )
91 87 90 eqeltrrd 
 |-  ( ph -> <. ( ( 1st ` N ) ( <. ( 1st ` X ) , ( 1st ` Y ) >. ( comp ` C ) ( 1st ` Z ) ) ( 1st ` M ) ) , ( ( 2nd ` N ) ( <. ( 2nd ` X ) , ( 2nd ` Y ) >. ( comp ` D ) ( 2nd ` Z ) ) ( 2nd ` M ) ) >. e. ( X H Z ) )
92 5 3 6 7 9 35 91 swapf2a 
 |-  ( ph -> ( ( X P Z ) ` <. ( ( 1st ` N ) ( <. ( 1st ` X ) , ( 1st ` Y ) >. ( comp ` C ) ( 1st ` Z ) ) ( 1st ` M ) ) , ( ( 2nd ` N ) ( <. ( 2nd ` X ) , ( 2nd ` Y ) >. ( comp ` D ) ( 2nd ` Z ) ) ( 2nd ` M ) ) >. ) = <. ( 2nd ` <. ( ( 1st ` N ) ( <. ( 1st ` X ) , ( 1st ` Y ) >. ( comp ` C ) ( 1st ` Z ) ) ( 1st ` M ) ) , ( ( 2nd ` N ) ( <. ( 2nd ` X ) , ( 2nd ` Y ) >. ( comp ` D ) ( 2nd ` Z ) ) ( 2nd ` M ) ) >. ) , ( 1st ` <. ( ( 1st ` N ) ( <. ( 1st ` X ) , ( 1st ` Y ) >. ( comp ` C ) ( 1st ` Z ) ) ( 1st ` M ) ) , ( ( 2nd ` N ) ( <. ( 2nd ` X ) , ( 2nd ` Y ) >. ( comp ` D ) ( 2nd ` Z ) ) ( 2nd ` M ) ) >. ) >. )
93 ovex 
 |-  ( ( 1st ` N ) ( <. ( 1st ` X ) , ( 1st ` Y ) >. ( comp ` C ) ( 1st ` Z ) ) ( 1st ` M ) ) e. _V
94 ovex 
 |-  ( ( 2nd ` N ) ( <. ( 2nd ` X ) , ( 2nd ` Y ) >. ( comp ` D ) ( 2nd ` Z ) ) ( 2nd ` M ) ) e. _V
95 93 94 op2nd 
 |-  ( 2nd ` <. ( ( 1st ` N ) ( <. ( 1st ` X ) , ( 1st ` Y ) >. ( comp ` C ) ( 1st ` Z ) ) ( 1st ` M ) ) , ( ( 2nd ` N ) ( <. ( 2nd ` X ) , ( 2nd ` Y ) >. ( comp ` D ) ( 2nd ` Z ) ) ( 2nd ` M ) ) >. ) = ( ( 2nd ` N ) ( <. ( 2nd ` X ) , ( 2nd ` Y ) >. ( comp ` D ) ( 2nd ` Z ) ) ( 2nd ` M ) )
96 93 94 op1st 
 |-  ( 1st ` <. ( ( 1st ` N ) ( <. ( 1st ` X ) , ( 1st ` Y ) >. ( comp ` C ) ( 1st ` Z ) ) ( 1st ` M ) ) , ( ( 2nd ` N ) ( <. ( 2nd ` X ) , ( 2nd ` Y ) >. ( comp ` D ) ( 2nd ` Z ) ) ( 2nd ` M ) ) >. ) = ( ( 1st ` N ) ( <. ( 1st ` X ) , ( 1st ` Y ) >. ( comp ` C ) ( 1st ` Z ) ) ( 1st ` M ) )
97 95 96 opeq12i 
 |-  <. ( 2nd ` <. ( ( 1st ` N ) ( <. ( 1st ` X ) , ( 1st ` Y ) >. ( comp ` C ) ( 1st ` Z ) ) ( 1st ` M ) ) , ( ( 2nd ` N ) ( <. ( 2nd ` X ) , ( 2nd ` Y ) >. ( comp ` D ) ( 2nd ` Z ) ) ( 2nd ` M ) ) >. ) , ( 1st ` <. ( ( 1st ` N ) ( <. ( 1st ` X ) , ( 1st ` Y ) >. ( comp ` C ) ( 1st ` Z ) ) ( 1st ` M ) ) , ( ( 2nd ` N ) ( <. ( 2nd ` X ) , ( 2nd ` Y ) >. ( comp ` D ) ( 2nd ` Z ) ) ( 2nd ` M ) ) >. ) >. = <. ( ( 2nd ` N ) ( <. ( 2nd ` X ) , ( 2nd ` Y ) >. ( comp ` D ) ( 2nd ` Z ) ) ( 2nd ` M ) ) , ( ( 1st ` N ) ( <. ( 1st ` X ) , ( 1st ` Y ) >. ( comp ` C ) ( 1st ` Z ) ) ( 1st ` M ) ) >.
98 92 97 eqtrdi 
 |-  ( ph -> ( ( X P Z ) ` <. ( ( 1st ` N ) ( <. ( 1st ` X ) , ( 1st ` Y ) >. ( comp ` C ) ( 1st ` Z ) ) ( 1st ` M ) ) , ( ( 2nd ` N ) ( <. ( 2nd ` X ) , ( 2nd ` Y ) >. ( comp ` D ) ( 2nd ` Z ) ) ( 2nd ` M ) ) >. ) = <. ( ( 2nd ` N ) ( <. ( 2nd ` X ) , ( 2nd ` Y ) >. ( comp ` D ) ( 2nd ` Z ) ) ( 2nd ` M ) ) , ( ( 1st ` N ) ( <. ( 1st ` X ) , ( 1st ` Y ) >. ( comp ` C ) ( 1st ` Z ) ) ( 1st ` M ) ) >. )
99 88 98 eqtrd 
 |-  ( ph -> ( ( X P Z ) ` ( N ( <. X , Y >. .x. Z ) M ) ) = <. ( ( 2nd ` N ) ( <. ( 2nd ` X ) , ( 2nd ` Y ) >. ( comp ` D ) ( 2nd ` Z ) ) ( 2nd ` M ) ) , ( ( 1st ` N ) ( <. ( 1st ` X ) , ( 1st ` Y ) >. ( comp ` C ) ( 1st ` Z ) ) ( 1st ` M ) ) >. )
100 67 86 99 3eqtr4rd 
 |-  ( ph -> ( ( X P Z ) ` ( N ( <. X , Y >. .x. Z ) M ) ) = ( ( ( Y P Z ) ` N ) ( <. ( O ` X ) , ( O ` Y ) >. .xb ( O ` Z ) ) ( ( X P Y ) ` M ) ) )