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	$⊢ φ \to C \in Cat$
	swapfid.d	$⊢ φ \to D \in Cat$
	swapfid.s	$⊢ S = C \times_{c} D$
	swapfid.t	$⊢ T = D \times_{c} C$
	swapfid.o	No typesetting found for \|- ( ph -> ( C swapF D ) = <. O , P >. ) with typecode \|-
	swapfida.b	$⊢ B = {Base}_{S}$
	swapfida.x	$⊢ φ \to X \in B$
	swapfcoa.y	$⊢ φ \to Y \in B$
	swapfcoa.z	$⊢ φ \to Z \in B$
	swapfcoa.h	$⊢ H = Hom (S)$
	swapfcoa.m	$⊢ φ \to M \in (X H Y)$
	swapfcoa.n	$⊢ φ \to N \in (Y H Z)$
	swapfcoa.os	$⊢ \underset{˙}{\cdot} = comp (S)$
	swapfcoa.ot	$⊢ \underset{˙}{∙} = comp (T)$
Assertion	swapfcoa	$⊢ φ \to (X P Z) (N (⟨X, Y⟩ \underset{˙}{\cdot} Z) M) = (Y P Z) (N) (⟨O (X), O (Y)⟩ \underset{˙}{∙} O (Z)) (X P Y) (M)$

Proof

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

Metamath Proof Explorer

Theorem swapfcoa

Proof