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	⊢ ( 𝜑 → 𝐶 ∈ Cat )
	swapfid.d	⊢ ( 𝜑 → 𝐷 ∈ Cat )
	swapfid.s	⊢ 𝑆 = ( 𝐶 ×_c 𝐷 )
	swapfid.t	⊢ 𝑇 = ( 𝐷 ×_c 𝐶 )
	swapfid.o	⊢ ( 𝜑 → ( 𝐶 swap_F 𝐷 ) = ⟨ 𝑂 , 𝑃 ⟩ )
	swapfida.b	⊢ 𝐵 = ( Base ‘ 𝑆 )
	swapfida.x	⊢ ( 𝜑 → 𝑋 ∈ 𝐵 )
	swapfcoa.y	⊢ ( 𝜑 → 𝑌 ∈ 𝐵 )
	swapfcoa.z	⊢ ( 𝜑 → 𝑍 ∈ 𝐵 )
	swapfcoa.h	⊢ 𝐻 = ( Hom ‘ 𝑆 )
	swapfcoa.m	⊢ ( 𝜑 → 𝑀 ∈ ( 𝑋 𝐻 𝑌 ) )
	swapfcoa.n	⊢ ( 𝜑 → 𝑁 ∈ ( 𝑌 𝐻 𝑍 ) )
	swapfcoa.os	⊢ · = ( comp ‘ 𝑆 )
	swapfcoa.ot	⊢ ∙ = ( comp ‘ 𝑇 )
Assertion	swapfcoa	⊢ ( 𝜑 → ( ( 𝑋 𝑃 𝑍 ) ‘ ( 𝑁 ( ⟨ 𝑋 , 𝑌 ⟩ · 𝑍 ) 𝑀 ) ) = ( ( ( 𝑌 𝑃 𝑍 ) ‘ 𝑁 ) ( ⟨ ( 𝑂 ‘ 𝑋 ) , ( 𝑂 ‘ 𝑌 ) ⟩ ∙ ( 𝑂 ‘ 𝑍 ) ) ( ( 𝑋 𝑃 𝑌 ) ‘ 𝑀 ) ) )

Proof

Step	Hyp	Ref	Expression
1		swapfid.c	⊢ ( 𝜑 → 𝐶 ∈ Cat )
2		swapfid.d	⊢ ( 𝜑 → 𝐷 ∈ Cat )
3		swapfid.s	⊢ 𝑆 = ( 𝐶 ×_c 𝐷 )
4		swapfid.t	⊢ 𝑇 = ( 𝐷 ×_c 𝐶 )
5		swapfid.o	⊢ ( 𝜑 → ( 𝐶 swap_F 𝐷 ) = ⟨ 𝑂 , 𝑃 ⟩ )
6		swapfida.b	⊢ 𝐵 = ( Base ‘ 𝑆 )
7		swapfida.x	⊢ ( 𝜑 → 𝑋 ∈ 𝐵 )
8		swapfcoa.y	⊢ ( 𝜑 → 𝑌 ∈ 𝐵 )
9		swapfcoa.z	⊢ ( 𝜑 → 𝑍 ∈ 𝐵 )
10		swapfcoa.h	⊢ 𝐻 = ( Hom ‘ 𝑆 )
11		swapfcoa.m	⊢ ( 𝜑 → 𝑀 ∈ ( 𝑋 𝐻 𝑌 ) )
12		swapfcoa.n	⊢ ( 𝜑 → 𝑁 ∈ ( 𝑌 𝐻 𝑍 ) )
13		swapfcoa.os	⊢ · = ( comp ‘ 𝑆 )
14		swapfcoa.ot	⊢ ∙ = ( comp ‘ 𝑇 )
15	5 3 6 7	swapf1a	⊢ ( 𝜑 → ( 𝑂 ‘ 𝑋 ) = ⟨ ( 2^nd ‘ 𝑋 ) , ( 1^st ‘ 𝑋 ) ⟩ )
16	15	fveq2d	⊢ ( 𝜑 → ( 1^st ‘ ( 𝑂 ‘ 𝑋 ) ) = ( 1^st ‘ ⟨ ( 2^nd ‘ 𝑋 ) , ( 1^st ‘ 𝑋 ) ⟩ ) )
17		fvex	⊢ ( 2^nd ‘ 𝑋 ) ∈ V
18		fvex	⊢ ( 1^st ‘ 𝑋 ) ∈ V
19	17 18	op1st	⊢ ( 1^st ‘ ⟨ ( 2^nd ‘ 𝑋 ) , ( 1^st ‘ 𝑋 ) ⟩ ) = ( 2^nd ‘ 𝑋 )
20	16 19	eqtrdi	⊢ ( 𝜑 → ( 1^st ‘ ( 𝑂 ‘ 𝑋 ) ) = ( 2^nd ‘ 𝑋 ) )
21	5 3 6 8	swapf1a	⊢ ( 𝜑 → ( 𝑂 ‘ 𝑌 ) = ⟨ ( 2^nd ‘ 𝑌 ) , ( 1^st ‘ 𝑌 ) ⟩ )
22	21	fveq2d	⊢ ( 𝜑 → ( 1^st ‘ ( 𝑂 ‘ 𝑌 ) ) = ( 1^st ‘ ⟨ ( 2^nd ‘ 𝑌 ) , ( 1^st ‘ 𝑌 ) ⟩ ) )
23		fvex	⊢ ( 2^nd ‘ 𝑌 ) ∈ V
24		fvex	⊢ ( 1^st ‘ 𝑌 ) ∈ V
25	23 24	op1st	⊢ ( 1^st ‘ ⟨ ( 2^nd ‘ 𝑌 ) , ( 1^st ‘ 𝑌 ) ⟩ ) = ( 2^nd ‘ 𝑌 )
26	22 25	eqtrdi	⊢ ( 𝜑 → ( 1^st ‘ ( 𝑂 ‘ 𝑌 ) ) = ( 2^nd ‘ 𝑌 ) )
27	20 26	opeq12d	⊢ ( 𝜑 → ⟨ ( 1^st ‘ ( 𝑂 ‘ 𝑋 ) ) , ( 1^st ‘ ( 𝑂 ‘ 𝑌 ) ) ⟩ = ⟨ ( 2^nd ‘ 𝑋 ) , ( 2^nd ‘ 𝑌 ) ⟩ )
28	5 3 6 9	swapf1a	⊢ ( 𝜑 → ( 𝑂 ‘ 𝑍 ) = ⟨ ( 2^nd ‘ 𝑍 ) , ( 1^st ‘ 𝑍 ) ⟩ )
29	28	fveq2d	⊢ ( 𝜑 → ( 1^st ‘ ( 𝑂 ‘ 𝑍 ) ) = ( 1^st ‘ ⟨ ( 2^nd ‘ 𝑍 ) , ( 1^st ‘ 𝑍 ) ⟩ ) )
30		fvex	⊢ ( 2^nd ‘ 𝑍 ) ∈ V
31		fvex	⊢ ( 1^st ‘ 𝑍 ) ∈ V
32	30 31	op1st	⊢ ( 1^st ‘ ⟨ ( 2^nd ‘ 𝑍 ) , ( 1^st ‘ 𝑍 ) ⟩ ) = ( 2^nd ‘ 𝑍 )
33	29 32	eqtrdi	⊢ ( 𝜑 → ( 1^st ‘ ( 𝑂 ‘ 𝑍 ) ) = ( 2^nd ‘ 𝑍 ) )
34	27 33	oveq12d	⊢ ( 𝜑 → ( ⟨ ( 1^st ‘ ( 𝑂 ‘ 𝑋 ) ) , ( 1^st ‘ ( 𝑂 ‘ 𝑌 ) ) ⟩ ( comp ‘ 𝐷 ) ( 1^st ‘ ( 𝑂 ‘ 𝑍 ) ) ) = ( ⟨ ( 2^nd ‘ 𝑋 ) , ( 2^nd ‘ 𝑌 ) ⟩ ( comp ‘ 𝐷 ) ( 2^nd ‘ 𝑍 ) ) )
35	10	a1i	⊢ ( 𝜑 → 𝐻 = ( Hom ‘ 𝑆 ) )
36	5 3 6 8 9 35 12	swapf2a	⊢ ( 𝜑 → ( ( 𝑌 𝑃 𝑍 ) ‘ 𝑁 ) = ⟨ ( 2^nd ‘ 𝑁 ) , ( 1^st ‘ 𝑁 ) ⟩ )
37	36	fveq2d	⊢ ( 𝜑 → ( 1^st ‘ ( ( 𝑌 𝑃 𝑍 ) ‘ 𝑁 ) ) = ( 1^st ‘ ⟨ ( 2^nd ‘ 𝑁 ) , ( 1^st ‘ 𝑁 ) ⟩ ) )
38		fvex	⊢ ( 2^nd ‘ 𝑁 ) ∈ V
39		fvex	⊢ ( 1^st ‘ 𝑁 ) ∈ V
40	38 39	op1st	⊢ ( 1^st ‘ ⟨ ( 2^nd ‘ 𝑁 ) , ( 1^st ‘ 𝑁 ) ⟩ ) = ( 2^nd ‘ 𝑁 )
41	37 40	eqtrdi	⊢ ( 𝜑 → ( 1^st ‘ ( ( 𝑌 𝑃 𝑍 ) ‘ 𝑁 ) ) = ( 2^nd ‘ 𝑁 ) )
42	5 3 6 7 8 35 11	swapf2a	⊢ ( 𝜑 → ( ( 𝑋 𝑃 𝑌 ) ‘ 𝑀 ) = ⟨ ( 2^nd ‘ 𝑀 ) , ( 1^st ‘ 𝑀 ) ⟩ )
43	42	fveq2d	⊢ ( 𝜑 → ( 1^st ‘ ( ( 𝑋 𝑃 𝑌 ) ‘ 𝑀 ) ) = ( 1^st ‘ ⟨ ( 2^nd ‘ 𝑀 ) , ( 1^st ‘ 𝑀 ) ⟩ ) )
44		fvex	⊢ ( 2^nd ‘ 𝑀 ) ∈ V
45		fvex	⊢ ( 1^st ‘ 𝑀 ) ∈ V
46	44 45	op1st	⊢ ( 1^st ‘ ⟨ ( 2^nd ‘ 𝑀 ) , ( 1^st ‘ 𝑀 ) ⟩ ) = ( 2^nd ‘ 𝑀 )
47	43 46	eqtrdi	⊢ ( 𝜑 → ( 1^st ‘ ( ( 𝑋 𝑃 𝑌 ) ‘ 𝑀 ) ) = ( 2^nd ‘ 𝑀 ) )
48	34 41 47	oveq123d	⊢ ( 𝜑 → ( ( 1^st ‘ ( ( 𝑌 𝑃 𝑍 ) ‘ 𝑁 ) ) ( ⟨ ( 1^st ‘ ( 𝑂 ‘ 𝑋 ) ) , ( 1^st ‘ ( 𝑂 ‘ 𝑌 ) ) ⟩ ( comp ‘ 𝐷 ) ( 1^st ‘ ( 𝑂 ‘ 𝑍 ) ) ) ( 1^st ‘ ( ( 𝑋 𝑃 𝑌 ) ‘ 𝑀 ) ) ) = ( ( 2^nd ‘ 𝑁 ) ( ⟨ ( 2^nd ‘ 𝑋 ) , ( 2^nd ‘ 𝑌 ) ⟩ ( comp ‘ 𝐷 ) ( 2^nd ‘ 𝑍 ) ) ( 2^nd ‘ 𝑀 ) ) )
49	15	fveq2d	⊢ ( 𝜑 → ( 2^nd ‘ ( 𝑂 ‘ 𝑋 ) ) = ( 2^nd ‘ ⟨ ( 2^nd ‘ 𝑋 ) , ( 1^st ‘ 𝑋 ) ⟩ ) )
50	17 18	op2nd	⊢ ( 2^nd ‘ ⟨ ( 2^nd ‘ 𝑋 ) , ( 1^st ‘ 𝑋 ) ⟩ ) = ( 1^st ‘ 𝑋 )
51	49 50	eqtrdi	⊢ ( 𝜑 → ( 2^nd ‘ ( 𝑂 ‘ 𝑋 ) ) = ( 1^st ‘ 𝑋 ) )
52	21	fveq2d	⊢ ( 𝜑 → ( 2^nd ‘ ( 𝑂 ‘ 𝑌 ) ) = ( 2^nd ‘ ⟨ ( 2^nd ‘ 𝑌 ) , ( 1^st ‘ 𝑌 ) ⟩ ) )
53	23 24	op2nd	⊢ ( 2^nd ‘ ⟨ ( 2^nd ‘ 𝑌 ) , ( 1^st ‘ 𝑌 ) ⟩ ) = ( 1^st ‘ 𝑌 )
54	52 53	eqtrdi	⊢ ( 𝜑 → ( 2^nd ‘ ( 𝑂 ‘ 𝑌 ) ) = ( 1^st ‘ 𝑌 ) )
55	51 54	opeq12d	⊢ ( 𝜑 → ⟨ ( 2^nd ‘ ( 𝑂 ‘ 𝑋 ) ) , ( 2^nd ‘ ( 𝑂 ‘ 𝑌 ) ) ⟩ = ⟨ ( 1^st ‘ 𝑋 ) , ( 1^st ‘ 𝑌 ) ⟩ )
56	28	fveq2d	⊢ ( 𝜑 → ( 2^nd ‘ ( 𝑂 ‘ 𝑍 ) ) = ( 2^nd ‘ ⟨ ( 2^nd ‘ 𝑍 ) , ( 1^st ‘ 𝑍 ) ⟩ ) )
57	30 31	op2nd	⊢ ( 2^nd ‘ ⟨ ( 2^nd ‘ 𝑍 ) , ( 1^st ‘ 𝑍 ) ⟩ ) = ( 1^st ‘ 𝑍 )
58	56 57	eqtrdi	⊢ ( 𝜑 → ( 2^nd ‘ ( 𝑂 ‘ 𝑍 ) ) = ( 1^st ‘ 𝑍 ) )
59	55 58	oveq12d	⊢ ( 𝜑 → ( ⟨ ( 2^nd ‘ ( 𝑂 ‘ 𝑋 ) ) , ( 2^nd ‘ ( 𝑂 ‘ 𝑌 ) ) ⟩ ( comp ‘ 𝐶 ) ( 2^nd ‘ ( 𝑂 ‘ 𝑍 ) ) ) = ( ⟨ ( 1^st ‘ 𝑋 ) , ( 1^st ‘ 𝑌 ) ⟩ ( comp ‘ 𝐶 ) ( 1^st ‘ 𝑍 ) ) )
60	36	fveq2d	⊢ ( 𝜑 → ( 2^nd ‘ ( ( 𝑌 𝑃 𝑍 ) ‘ 𝑁 ) ) = ( 2^nd ‘ ⟨ ( 2^nd ‘ 𝑁 ) , ( 1^st ‘ 𝑁 ) ⟩ ) )
61	38 39	op2nd	⊢ ( 2^nd ‘ ⟨ ( 2^nd ‘ 𝑁 ) , ( 1^st ‘ 𝑁 ) ⟩ ) = ( 1^st ‘ 𝑁 )
62	60 61	eqtrdi	⊢ ( 𝜑 → ( 2^nd ‘ ( ( 𝑌 𝑃 𝑍 ) ‘ 𝑁 ) ) = ( 1^st ‘ 𝑁 ) )
63	42	fveq2d	⊢ ( 𝜑 → ( 2^nd ‘ ( ( 𝑋 𝑃 𝑌 ) ‘ 𝑀 ) ) = ( 2^nd ‘ ⟨ ( 2^nd ‘ 𝑀 ) , ( 1^st ‘ 𝑀 ) ⟩ ) )
64	44 45	op2nd	⊢ ( 2^nd ‘ ⟨ ( 2^nd ‘ 𝑀 ) , ( 1^st ‘ 𝑀 ) ⟩ ) = ( 1^st ‘ 𝑀 )
65	63 64	eqtrdi	⊢ ( 𝜑 → ( 2^nd ‘ ( ( 𝑋 𝑃 𝑌 ) ‘ 𝑀 ) ) = ( 1^st ‘ 𝑀 ) )
66	59 62 65	oveq123d	⊢ ( 𝜑 → ( ( 2^nd ‘ ( ( 𝑌 𝑃 𝑍 ) ‘ 𝑁 ) ) ( ⟨ ( 2^nd ‘ ( 𝑂 ‘ 𝑋 ) ) , ( 2^nd ‘ ( 𝑂 ‘ 𝑌 ) ) ⟩ ( comp ‘ 𝐶 ) ( 2^nd ‘ ( 𝑂 ‘ 𝑍 ) ) ) ( 2^nd ‘ ( ( 𝑋 𝑃 𝑌 ) ‘ 𝑀 ) ) ) = ( ( 1^st ‘ 𝑁 ) ( ⟨ ( 1^st ‘ 𝑋 ) , ( 1^st ‘ 𝑌 ) ⟩ ( comp ‘ 𝐶 ) ( 1^st ‘ 𝑍 ) ) ( 1^st ‘ 𝑀 ) ) )
67	48 66	opeq12d	⊢ ( 𝜑 → ⟨ ( ( 1^st ‘ ( ( 𝑌 𝑃 𝑍 ) ‘ 𝑁 ) ) ( ⟨ ( 1^st ‘ ( 𝑂 ‘ 𝑋 ) ) , ( 1^st ‘ ( 𝑂 ‘ 𝑌 ) ) ⟩ ( comp ‘ 𝐷 ) ( 1^st ‘ ( 𝑂 ‘ 𝑍 ) ) ) ( 1^st ‘ ( ( 𝑋 𝑃 𝑌 ) ‘ 𝑀 ) ) ) , ( ( 2^nd ‘ ( ( 𝑌 𝑃 𝑍 ) ‘ 𝑁 ) ) ( ⟨ ( 2^nd ‘ ( 𝑂 ‘ 𝑋 ) ) , ( 2^nd ‘ ( 𝑂 ‘ 𝑌 ) ) ⟩ ( comp ‘ 𝐶 ) ( 2^nd ‘ ( 𝑂 ‘ 𝑍 ) ) ) ( 2^nd ‘ ( ( 𝑋 𝑃 𝑌 ) ‘ 𝑀 ) ) ) ⟩ = ⟨ ( ( 2^nd ‘ 𝑁 ) ( ⟨ ( 2^nd ‘ 𝑋 ) , ( 2^nd ‘ 𝑌 ) ⟩ ( comp ‘ 𝐷 ) ( 2^nd ‘ 𝑍 ) ) ( 2^nd ‘ 𝑀 ) ) , ( ( 1^st ‘ 𝑁 ) ( ⟨ ( 1^st ‘ 𝑋 ) , ( 1^st ‘ 𝑌 ) ⟩ ( comp ‘ 𝐶 ) ( 1^st ‘ 𝑍 ) ) ( 1^st ‘ 𝑀 ) ) ⟩ )
68		eqid	⊢ ( Base ‘ 𝑇 ) = ( Base ‘ 𝑇 )
69		eqid	⊢ ( Hom ‘ 𝑇 ) = ( Hom ‘ 𝑇 )
70		eqid	⊢ ( comp ‘ 𝐷 ) = ( comp ‘ 𝐷 )
71		eqid	⊢ ( comp ‘ 𝐶 ) = ( comp ‘ 𝐶 )
72	5 3 4 1 2 6 68	swapf1f1o	⊢ ( 𝜑 → 𝑂 : 𝐵 –1-1-onto→ ( Base ‘ 𝑇 ) )
73		f1of	⊢ ( 𝑂 : 𝐵 –1-1-onto→ ( Base ‘ 𝑇 ) → 𝑂 : 𝐵 ⟶ ( Base ‘ 𝑇 ) )
74	72 73	syl	⊢ ( 𝜑 → 𝑂 : 𝐵 ⟶ ( Base ‘ 𝑇 ) )
75	74 7	ffvelcdmd	⊢ ( 𝜑 → ( 𝑂 ‘ 𝑋 ) ∈ ( Base ‘ 𝑇 ) )
76	74 8	ffvelcdmd	⊢ ( 𝜑 → ( 𝑂 ‘ 𝑌 ) ∈ ( Base ‘ 𝑇 ) )
77	74 9	ffvelcdmd	⊢ ( 𝜑 → ( 𝑂 ‘ 𝑍 ) ∈ ( Base ‘ 𝑇 ) )
78	5 3 4 10 69 6 7 8	swapf2f1oa	⊢ ( 𝜑 → ( 𝑋 𝑃 𝑌 ) : ( 𝑋 𝐻 𝑌 ) –1-1-onto→ ( ( 𝑂 ‘ 𝑋 ) ( Hom ‘ 𝑇 ) ( 𝑂 ‘ 𝑌 ) ) )
79		f1of	⊢ ( ( 𝑋 𝑃 𝑌 ) : ( 𝑋 𝐻 𝑌 ) –1-1-onto→ ( ( 𝑂 ‘ 𝑋 ) ( Hom ‘ 𝑇 ) ( 𝑂 ‘ 𝑌 ) ) → ( 𝑋 𝑃 𝑌 ) : ( 𝑋 𝐻 𝑌 ) ⟶ ( ( 𝑂 ‘ 𝑋 ) ( Hom ‘ 𝑇 ) ( 𝑂 ‘ 𝑌 ) ) )
80	78 79	syl	⊢ ( 𝜑 → ( 𝑋 𝑃 𝑌 ) : ( 𝑋 𝐻 𝑌 ) ⟶ ( ( 𝑂 ‘ 𝑋 ) ( Hom ‘ 𝑇 ) ( 𝑂 ‘ 𝑌 ) ) )
81	80 11	ffvelcdmd	⊢ ( 𝜑 → ( ( 𝑋 𝑃 𝑌 ) ‘ 𝑀 ) ∈ ( ( 𝑂 ‘ 𝑋 ) ( Hom ‘ 𝑇 ) ( 𝑂 ‘ 𝑌 ) ) )
82	5 3 4 10 69 6 8 9	swapf2f1oa	⊢ ( 𝜑 → ( 𝑌 𝑃 𝑍 ) : ( 𝑌 𝐻 𝑍 ) –1-1-onto→ ( ( 𝑂 ‘ 𝑌 ) ( Hom ‘ 𝑇 ) ( 𝑂 ‘ 𝑍 ) ) )
83		f1of	⊢ ( ( 𝑌 𝑃 𝑍 ) : ( 𝑌 𝐻 𝑍 ) –1-1-onto→ ( ( 𝑂 ‘ 𝑌 ) ( Hom ‘ 𝑇 ) ( 𝑂 ‘ 𝑍 ) ) → ( 𝑌 𝑃 𝑍 ) : ( 𝑌 𝐻 𝑍 ) ⟶ ( ( 𝑂 ‘ 𝑌 ) ( Hom ‘ 𝑇 ) ( 𝑂 ‘ 𝑍 ) ) )
84	82 83	syl	⊢ ( 𝜑 → ( 𝑌 𝑃 𝑍 ) : ( 𝑌 𝐻 𝑍 ) ⟶ ( ( 𝑂 ‘ 𝑌 ) ( Hom ‘ 𝑇 ) ( 𝑂 ‘ 𝑍 ) ) )
85	84 12	ffvelcdmd	⊢ ( 𝜑 → ( ( 𝑌 𝑃 𝑍 ) ‘ 𝑁 ) ∈ ( ( 𝑂 ‘ 𝑌 ) ( Hom ‘ 𝑇 ) ( 𝑂 ‘ 𝑍 ) ) )
86	4 68 69 70 71 14 75 76 77 81 85	xpcco	⊢ ( 𝜑 → ( ( ( 𝑌 𝑃 𝑍 ) ‘ 𝑁 ) ( ⟨ ( 𝑂 ‘ 𝑋 ) , ( 𝑂 ‘ 𝑌 ) ⟩ ∙ ( 𝑂 ‘ 𝑍 ) ) ( ( 𝑋 𝑃 𝑌 ) ‘ 𝑀 ) ) = ⟨ ( ( 1^st ‘ ( ( 𝑌 𝑃 𝑍 ) ‘ 𝑁 ) ) ( ⟨ ( 1^st ‘ ( 𝑂 ‘ 𝑋 ) ) , ( 1^st ‘ ( 𝑂 ‘ 𝑌 ) ) ⟩ ( comp ‘ 𝐷 ) ( 1^st ‘ ( 𝑂 ‘ 𝑍 ) ) ) ( 1^st ‘ ( ( 𝑋 𝑃 𝑌 ) ‘ 𝑀 ) ) ) , ( ( 2^nd ‘ ( ( 𝑌 𝑃 𝑍 ) ‘ 𝑁 ) ) ( ⟨ ( 2^nd ‘ ( 𝑂 ‘ 𝑋 ) ) , ( 2^nd ‘ ( 𝑂 ‘ 𝑌 ) ) ⟩ ( comp ‘ 𝐶 ) ( 2^nd ‘ ( 𝑂 ‘ 𝑍 ) ) ) ( 2^nd ‘ ( ( 𝑋 𝑃 𝑌 ) ‘ 𝑀 ) ) ) ⟩ )
87	3 6 10 71 70 13 7 8 9 11 12	xpcco	⊢ ( 𝜑 → ( 𝑁 ( ⟨ 𝑋 , 𝑌 ⟩ · 𝑍 ) 𝑀 ) = ⟨ ( ( 1^st ‘ 𝑁 ) ( ⟨ ( 1^st ‘ 𝑋 ) , ( 1^st ‘ 𝑌 ) ⟩ ( comp ‘ 𝐶 ) ( 1^st ‘ 𝑍 ) ) ( 1^st ‘ 𝑀 ) ) , ( ( 2^nd ‘ 𝑁 ) ( ⟨ ( 2^nd ‘ 𝑋 ) , ( 2^nd ‘ 𝑌 ) ⟩ ( comp ‘ 𝐷 ) ( 2^nd ‘ 𝑍 ) ) ( 2^nd ‘ 𝑀 ) ) ⟩ )
88	87	fveq2d	⊢ ( 𝜑 → ( ( 𝑋 𝑃 𝑍 ) ‘ ( 𝑁 ( ⟨ 𝑋 , 𝑌 ⟩ · 𝑍 ) 𝑀 ) ) = ( ( 𝑋 𝑃 𝑍 ) ‘ ⟨ ( ( 1^st ‘ 𝑁 ) ( ⟨ ( 1^st ‘ 𝑋 ) , ( 1^st ‘ 𝑌 ) ⟩ ( comp ‘ 𝐶 ) ( 1^st ‘ 𝑍 ) ) ( 1^st ‘ 𝑀 ) ) , ( ( 2^nd ‘ 𝑁 ) ( ⟨ ( 2^nd ‘ 𝑋 ) , ( 2^nd ‘ 𝑌 ) ⟩ ( comp ‘ 𝐷 ) ( 2^nd ‘ 𝑍 ) ) ( 2^nd ‘ 𝑀 ) ) ⟩ ) )
89	3 1 2	xpccat	⊢ ( 𝜑 → 𝑆 ∈ Cat )
90	6 10 13 89 7 8 9 11 12	catcocl	⊢ ( 𝜑 → ( 𝑁 ( ⟨ 𝑋 , 𝑌 ⟩ · 𝑍 ) 𝑀 ) ∈ ( 𝑋 𝐻 𝑍 ) )
91	87 90	eqeltrrd	⊢ ( 𝜑 → ⟨ ( ( 1^st ‘ 𝑁 ) ( ⟨ ( 1^st ‘ 𝑋 ) , ( 1^st ‘ 𝑌 ) ⟩ ( comp ‘ 𝐶 ) ( 1^st ‘ 𝑍 ) ) ( 1^st ‘ 𝑀 ) ) , ( ( 2^nd ‘ 𝑁 ) ( ⟨ ( 2^nd ‘ 𝑋 ) , ( 2^nd ‘ 𝑌 ) ⟩ ( comp ‘ 𝐷 ) ( 2^nd ‘ 𝑍 ) ) ( 2^nd ‘ 𝑀 ) ) ⟩ ∈ ( 𝑋 𝐻 𝑍 ) )
92	5 3 6 7 9 35 91	swapf2a	⊢ ( 𝜑 → ( ( 𝑋 𝑃 𝑍 ) ‘ ⟨ ( ( 1^st ‘ 𝑁 ) ( ⟨ ( 1^st ‘ 𝑋 ) , ( 1^st ‘ 𝑌 ) ⟩ ( comp ‘ 𝐶 ) ( 1^st ‘ 𝑍 ) ) ( 1^st ‘ 𝑀 ) ) , ( ( 2^nd ‘ 𝑁 ) ( ⟨ ( 2^nd ‘ 𝑋 ) , ( 2^nd ‘ 𝑌 ) ⟩ ( comp ‘ 𝐷 ) ( 2^nd ‘ 𝑍 ) ) ( 2^nd ‘ 𝑀 ) ) ⟩ ) = ⟨ ( 2^nd ‘ ⟨ ( ( 1^st ‘ 𝑁 ) ( ⟨ ( 1^st ‘ 𝑋 ) , ( 1^st ‘ 𝑌 ) ⟩ ( comp ‘ 𝐶 ) ( 1^st ‘ 𝑍 ) ) ( 1^st ‘ 𝑀 ) ) , ( ( 2^nd ‘ 𝑁 ) ( ⟨ ( 2^nd ‘ 𝑋 ) , ( 2^nd ‘ 𝑌 ) ⟩ ( comp ‘ 𝐷 ) ( 2^nd ‘ 𝑍 ) ) ( 2^nd ‘ 𝑀 ) ) ⟩ ) , ( 1^st ‘ ⟨ ( ( 1^st ‘ 𝑁 ) ( ⟨ ( 1^st ‘ 𝑋 ) , ( 1^st ‘ 𝑌 ) ⟩ ( comp ‘ 𝐶 ) ( 1^st ‘ 𝑍 ) ) ( 1^st ‘ 𝑀 ) ) , ( ( 2^nd ‘ 𝑁 ) ( ⟨ ( 2^nd ‘ 𝑋 ) , ( 2^nd ‘ 𝑌 ) ⟩ ( comp ‘ 𝐷 ) ( 2^nd ‘ 𝑍 ) ) ( 2^nd ‘ 𝑀 ) ) ⟩ ) ⟩ )
93		ovex	⊢ ( ( 1^st ‘ 𝑁 ) ( ⟨ ( 1^st ‘ 𝑋 ) , ( 1^st ‘ 𝑌 ) ⟩ ( comp ‘ 𝐶 ) ( 1^st ‘ 𝑍 ) ) ( 1^st ‘ 𝑀 ) ) ∈ V
94		ovex	⊢ ( ( 2^nd ‘ 𝑁 ) ( ⟨ ( 2^nd ‘ 𝑋 ) , ( 2^nd ‘ 𝑌 ) ⟩ ( comp ‘ 𝐷 ) ( 2^nd ‘ 𝑍 ) ) ( 2^nd ‘ 𝑀 ) ) ∈ V
95	93 94	op2nd	⊢ ( 2^nd ‘ ⟨ ( ( 1^st ‘ 𝑁 ) ( ⟨ ( 1^st ‘ 𝑋 ) , ( 1^st ‘ 𝑌 ) ⟩ ( comp ‘ 𝐶 ) ( 1^st ‘ 𝑍 ) ) ( 1^st ‘ 𝑀 ) ) , ( ( 2^nd ‘ 𝑁 ) ( ⟨ ( 2^nd ‘ 𝑋 ) , ( 2^nd ‘ 𝑌 ) ⟩ ( comp ‘ 𝐷 ) ( 2^nd ‘ 𝑍 ) ) ( 2^nd ‘ 𝑀 ) ) ⟩ ) = ( ( 2^nd ‘ 𝑁 ) ( ⟨ ( 2^nd ‘ 𝑋 ) , ( 2^nd ‘ 𝑌 ) ⟩ ( comp ‘ 𝐷 ) ( 2^nd ‘ 𝑍 ) ) ( 2^nd ‘ 𝑀 ) )
96	93 94	op1st	⊢ ( 1^st ‘ ⟨ ( ( 1^st ‘ 𝑁 ) ( ⟨ ( 1^st ‘ 𝑋 ) , ( 1^st ‘ 𝑌 ) ⟩ ( comp ‘ 𝐶 ) ( 1^st ‘ 𝑍 ) ) ( 1^st ‘ 𝑀 ) ) , ( ( 2^nd ‘ 𝑁 ) ( ⟨ ( 2^nd ‘ 𝑋 ) , ( 2^nd ‘ 𝑌 ) ⟩ ( comp ‘ 𝐷 ) ( 2^nd ‘ 𝑍 ) ) ( 2^nd ‘ 𝑀 ) ) ⟩ ) = ( ( 1^st ‘ 𝑁 ) ( ⟨ ( 1^st ‘ 𝑋 ) , ( 1^st ‘ 𝑌 ) ⟩ ( comp ‘ 𝐶 ) ( 1^st ‘ 𝑍 ) ) ( 1^st ‘ 𝑀 ) )
97	95 96	opeq12i	⊢ ⟨ ( 2^nd ‘ ⟨ ( ( 1^st ‘ 𝑁 ) ( ⟨ ( 1^st ‘ 𝑋 ) , ( 1^st ‘ 𝑌 ) ⟩ ( comp ‘ 𝐶 ) ( 1^st ‘ 𝑍 ) ) ( 1^st ‘ 𝑀 ) ) , ( ( 2^nd ‘ 𝑁 ) ( ⟨ ( 2^nd ‘ 𝑋 ) , ( 2^nd ‘ 𝑌 ) ⟩ ( comp ‘ 𝐷 ) ( 2^nd ‘ 𝑍 ) ) ( 2^nd ‘ 𝑀 ) ) ⟩ ) , ( 1^st ‘ ⟨ ( ( 1^st ‘ 𝑁 ) ( ⟨ ( 1^st ‘ 𝑋 ) , ( 1^st ‘ 𝑌 ) ⟩ ( comp ‘ 𝐶 ) ( 1^st ‘ 𝑍 ) ) ( 1^st ‘ 𝑀 ) ) , ( ( 2^nd ‘ 𝑁 ) ( ⟨ ( 2^nd ‘ 𝑋 ) , ( 2^nd ‘ 𝑌 ) ⟩ ( comp ‘ 𝐷 ) ( 2^nd ‘ 𝑍 ) ) ( 2^nd ‘ 𝑀 ) ) ⟩ ) ⟩ = ⟨ ( ( 2^nd ‘ 𝑁 ) ( ⟨ ( 2^nd ‘ 𝑋 ) , ( 2^nd ‘ 𝑌 ) ⟩ ( comp ‘ 𝐷 ) ( 2^nd ‘ 𝑍 ) ) ( 2^nd ‘ 𝑀 ) ) , ( ( 1^st ‘ 𝑁 ) ( ⟨ ( 1^st ‘ 𝑋 ) , ( 1^st ‘ 𝑌 ) ⟩ ( comp ‘ 𝐶 ) ( 1^st ‘ 𝑍 ) ) ( 1^st ‘ 𝑀 ) ) ⟩
98	92 97	eqtrdi	⊢ ( 𝜑 → ( ( 𝑋 𝑃 𝑍 ) ‘ ⟨ ( ( 1^st ‘ 𝑁 ) ( ⟨ ( 1^st ‘ 𝑋 ) , ( 1^st ‘ 𝑌 ) ⟩ ( comp ‘ 𝐶 ) ( 1^st ‘ 𝑍 ) ) ( 1^st ‘ 𝑀 ) ) , ( ( 2^nd ‘ 𝑁 ) ( ⟨ ( 2^nd ‘ 𝑋 ) , ( 2^nd ‘ 𝑌 ) ⟩ ( comp ‘ 𝐷 ) ( 2^nd ‘ 𝑍 ) ) ( 2^nd ‘ 𝑀 ) ) ⟩ ) = ⟨ ( ( 2^nd ‘ 𝑁 ) ( ⟨ ( 2^nd ‘ 𝑋 ) , ( 2^nd ‘ 𝑌 ) ⟩ ( comp ‘ 𝐷 ) ( 2^nd ‘ 𝑍 ) ) ( 2^nd ‘ 𝑀 ) ) , ( ( 1^st ‘ 𝑁 ) ( ⟨ ( 1^st ‘ 𝑋 ) , ( 1^st ‘ 𝑌 ) ⟩ ( comp ‘ 𝐶 ) ( 1^st ‘ 𝑍 ) ) ( 1^st ‘ 𝑀 ) ) ⟩ )
99	88 98	eqtrd	⊢ ( 𝜑 → ( ( 𝑋 𝑃 𝑍 ) ‘ ( 𝑁 ( ⟨ 𝑋 , 𝑌 ⟩ · 𝑍 ) 𝑀 ) ) = ⟨ ( ( 2^nd ‘ 𝑁 ) ( ⟨ ( 2^nd ‘ 𝑋 ) , ( 2^nd ‘ 𝑌 ) ⟩ ( comp ‘ 𝐷 ) ( 2^nd ‘ 𝑍 ) ) ( 2^nd ‘ 𝑀 ) ) , ( ( 1^st ‘ 𝑁 ) ( ⟨ ( 1^st ‘ 𝑋 ) , ( 1^st ‘ 𝑌 ) ⟩ ( comp ‘ 𝐶 ) ( 1^st ‘ 𝑍 ) ) ( 1^st ‘ 𝑀 ) ) ⟩ )
100	67 86 99	3eqtr4rd	⊢ ( 𝜑 → ( ( 𝑋 𝑃 𝑍 ) ‘ ( 𝑁 ( ⟨ 𝑋 , 𝑌 ⟩ · 𝑍 ) 𝑀 ) ) = ( ( ( 𝑌 𝑃 𝑍 ) ‘ 𝑁 ) ( ⟨ ( 𝑂 ‘ 𝑋 ) , ( 𝑂 ‘ 𝑌 ) ⟩ ∙ ( 𝑂 ‘ 𝑍 ) ) ( ( 𝑋 𝑃 𝑌 ) ‘ 𝑀 ) ) )

Metamath Proof Explorer

Theorem swapfcoa

Proof