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	⊢ ( 𝜑 → 𝐶 ∈ Cat )
	cofuswapf1.d	⊢ ( 𝜑 → 𝐷 ∈ Cat )
	cofuswapf1.f	⊢ ( 𝜑 → 𝐹 ∈ ( ( 𝐷 ×_c 𝐶 ) Func 𝐸 ) )
	cofuswapf1.g	⊢ ( 𝜑 → 𝐺 = ( 𝐹 ∘_func ( 𝐶 swap_F 𝐷 ) ) )
	cofuswapf1.a	⊢ 𝐴 = ( Base ‘ 𝐶 )
	cofuswapf1.b	⊢ 𝐵 = ( Base ‘ 𝐷 )
	cofuswapf1.x	⊢ ( 𝜑 → 𝑋 ∈ 𝐴 )
	cofuswapf1.y	⊢ ( 𝜑 → 𝑌 ∈ 𝐵 )
	cofuswapf2.z	⊢ ( 𝜑 → 𝑍 ∈ 𝐴 )
	cofuswapf2.w	⊢ ( 𝜑 → 𝑊 ∈ 𝐵 )
	cofuswapf2.h	⊢ 𝐻 = ( Hom ‘ 𝐶 )
	cofuswapf2.j	⊢ 𝐽 = ( Hom ‘ 𝐷 )
	cofuswapf2.m	⊢ ( 𝜑 → 𝑀 ∈ ( 𝑋 𝐻 𝑍 ) )
	cofuswapf2.n	⊢ ( 𝜑 → 𝑁 ∈ ( 𝑌 𝐽 𝑊 ) )
Assertion	cofuswapf2	⊢ ( 𝜑 → ( 𝑀 ( ⟨ 𝑋 , 𝑌 ⟩ ( 2^nd ‘ 𝐺 ) ⟨ 𝑍 , 𝑊 ⟩ ) 𝑁 ) = ( 𝑁 ( ⟨ 𝑌 , 𝑋 ⟩ ( 2^nd ‘ 𝐹 ) ⟨ 𝑊 , 𝑍 ⟩ ) 𝑀 ) )

Proof

Step	Hyp	Ref	Expression
1		cofuswapf1.c	⊢ ( 𝜑 → 𝐶 ∈ Cat )
2		cofuswapf1.d	⊢ ( 𝜑 → 𝐷 ∈ Cat )
3		cofuswapf1.f	⊢ ( 𝜑 → 𝐹 ∈ ( ( 𝐷 ×_c 𝐶 ) Func 𝐸 ) )
4		cofuswapf1.g	⊢ ( 𝜑 → 𝐺 = ( 𝐹 ∘_func ( 𝐶 swap_F 𝐷 ) ) )
5		cofuswapf1.a	⊢ 𝐴 = ( Base ‘ 𝐶 )
6		cofuswapf1.b	⊢ 𝐵 = ( Base ‘ 𝐷 )
7		cofuswapf1.x	⊢ ( 𝜑 → 𝑋 ∈ 𝐴 )
8		cofuswapf1.y	⊢ ( 𝜑 → 𝑌 ∈ 𝐵 )
9		cofuswapf2.z	⊢ ( 𝜑 → 𝑍 ∈ 𝐴 )
10		cofuswapf2.w	⊢ ( 𝜑 → 𝑊 ∈ 𝐵 )
11		cofuswapf2.h	⊢ 𝐻 = ( Hom ‘ 𝐶 )
12		cofuswapf2.j	⊢ 𝐽 = ( Hom ‘ 𝐷 )
13		cofuswapf2.m	⊢ ( 𝜑 → 𝑀 ∈ ( 𝑋 𝐻 𝑍 ) )
14		cofuswapf2.n	⊢ ( 𝜑 → 𝑁 ∈ ( 𝑌 𝐽 𝑊 ) )
15	4	fveq2d	⊢ ( 𝜑 → ( 2^nd ‘ 𝐺 ) = ( 2^nd ‘ ( 𝐹 ∘_func ( 𝐶 swap_F 𝐷 ) ) ) )
16	15	oveqd	⊢ ( 𝜑 → ( ⟨ 𝑋 , 𝑌 ⟩ ( 2^nd ‘ 𝐺 ) ⟨ 𝑍 , 𝑊 ⟩ ) = ( ⟨ 𝑋 , 𝑌 ⟩ ( 2^nd ‘ ( 𝐹 ∘_func ( 𝐶 swap_F 𝐷 ) ) ) ⟨ 𝑍 , 𝑊 ⟩ ) )
17	16	oveqd	⊢ ( 𝜑 → ( 𝑀 ( ⟨ 𝑋 , 𝑌 ⟩ ( 2^nd ‘ 𝐺 ) ⟨ 𝑍 , 𝑊 ⟩ ) 𝑁 ) = ( 𝑀 ( ⟨ 𝑋 , 𝑌 ⟩ ( 2^nd ‘ ( 𝐹 ∘_func ( 𝐶 swap_F 𝐷 ) ) ) ⟨ 𝑍 , 𝑊 ⟩ ) 𝑁 ) )
18		df-ov	⊢ ( 𝑀 ( ⟨ 𝑋 , 𝑌 ⟩ ( 2^nd ‘ ( 𝐹 ∘_func ( 𝐶 swap_F 𝐷 ) ) ) ⟨ 𝑍 , 𝑊 ⟩ ) 𝑁 ) = ( ( ⟨ 𝑋 , 𝑌 ⟩ ( 2^nd ‘ ( 𝐹 ∘_func ( 𝐶 swap_F 𝐷 ) ) ) ⟨ 𝑍 , 𝑊 ⟩ ) ‘ ⟨ 𝑀 , 𝑁 ⟩ )
19		eqid	⊢ ( 𝐶 ×_c 𝐷 ) = ( 𝐶 ×_c 𝐷 )
20	19 5 6	xpcbas	⊢ ( 𝐴 × 𝐵 ) = ( Base ‘ ( 𝐶 ×_c 𝐷 ) )
21		eqid	⊢ ( 𝐷 ×_c 𝐶 ) = ( 𝐷 ×_c 𝐶 )
22	1 2 19 21	swapffunca	⊢ ( 𝜑 → ( 𝐶 swap_F 𝐷 ) ∈ ( ( 𝐶 ×_c 𝐷 ) Func ( 𝐷 ×_c 𝐶 ) ) )
23	7 8	opelxpd	⊢ ( 𝜑 → ⟨ 𝑋 , 𝑌 ⟩ ∈ ( 𝐴 × 𝐵 ) )
24	9 10	opelxpd	⊢ ( 𝜑 → ⟨ 𝑍 , 𝑊 ⟩ ∈ ( 𝐴 × 𝐵 ) )
25		eqid	⊢ ( Hom ‘ ( 𝐶 ×_c 𝐷 ) ) = ( Hom ‘ ( 𝐶 ×_c 𝐷 ) )
26	13 14	opelxpd	⊢ ( 𝜑 → ⟨ 𝑀 , 𝑁 ⟩ ∈ ( ( 𝑋 𝐻 𝑍 ) × ( 𝑌 𝐽 𝑊 ) ) )
27	19 5 6 11 12 7 8 9 10 25	xpchom2	⊢ ( 𝜑 → ( ⟨ 𝑋 , 𝑌 ⟩ ( Hom ‘ ( 𝐶 ×_c 𝐷 ) ) ⟨ 𝑍 , 𝑊 ⟩ ) = ( ( 𝑋 𝐻 𝑍 ) × ( 𝑌 𝐽 𝑊 ) ) )
28	26 27	eleqtrrd	⊢ ( 𝜑 → ⟨ 𝑀 , 𝑁 ⟩ ∈ ( ⟨ 𝑋 , 𝑌 ⟩ ( Hom ‘ ( 𝐶 ×_c 𝐷 ) ) ⟨ 𝑍 , 𝑊 ⟩ ) )
29	20 22 3 23 24 25 28	cofu2	⊢ ( 𝜑 → ( ( ⟨ 𝑋 , 𝑌 ⟩ ( 2^nd ‘ ( 𝐹 ∘_func ( 𝐶 swap_F 𝐷 ) ) ) ⟨ 𝑍 , 𝑊 ⟩ ) ‘ ⟨ 𝑀 , 𝑁 ⟩ ) = ( ( ( ( 1^st ‘ ( 𝐶 swap_F 𝐷 ) ) ‘ ⟨ 𝑋 , 𝑌 ⟩ ) ( 2^nd ‘ 𝐹 ) ( ( 1^st ‘ ( 𝐶 swap_F 𝐷 ) ) ‘ ⟨ 𝑍 , 𝑊 ⟩ ) ) ‘ ( ( ⟨ 𝑋 , 𝑌 ⟩ ( 2^nd ‘ ( 𝐶 swap_F 𝐷 ) ) ⟨ 𝑍 , 𝑊 ⟩ ) ‘ ⟨ 𝑀 , 𝑁 ⟩ ) ) )
30	18 29	eqtrid	⊢ ( 𝜑 → ( 𝑀 ( ⟨ 𝑋 , 𝑌 ⟩ ( 2^nd ‘ ( 𝐹 ∘_func ( 𝐶 swap_F 𝐷 ) ) ) ⟨ 𝑍 , 𝑊 ⟩ ) 𝑁 ) = ( ( ( ( 1^st ‘ ( 𝐶 swap_F 𝐷 ) ) ‘ ⟨ 𝑋 , 𝑌 ⟩ ) ( 2^nd ‘ 𝐹 ) ( ( 1^st ‘ ( 𝐶 swap_F 𝐷 ) ) ‘ ⟨ 𝑍 , 𝑊 ⟩ ) ) ‘ ( ( ⟨ 𝑋 , 𝑌 ⟩ ( 2^nd ‘ ( 𝐶 swap_F 𝐷 ) ) ⟨ 𝑍 , 𝑊 ⟩ ) ‘ ⟨ 𝑀 , 𝑁 ⟩ ) ) )
31		df-ov	⊢ ( 𝑋 ( 1^st ‘ ( 𝐶 swap_F 𝐷 ) ) 𝑌 ) = ( ( 1^st ‘ ( 𝐶 swap_F 𝐷 ) ) ‘ ⟨ 𝑋 , 𝑌 ⟩ )
32	1 2	swapfelvv	⊢ ( 𝜑 → ( 𝐶 swap_F 𝐷 ) ∈ ( V × V ) )
33		1st2nd2	⊢ ( ( 𝐶 swap_F 𝐷 ) ∈ ( V × V ) → ( 𝐶 swap_F 𝐷 ) = ⟨ ( 1^st ‘ ( 𝐶 swap_F 𝐷 ) ) , ( 2^nd ‘ ( 𝐶 swap_F 𝐷 ) ) ⟩ )
34	32 33	syl	⊢ ( 𝜑 → ( 𝐶 swap_F 𝐷 ) = ⟨ ( 1^st ‘ ( 𝐶 swap_F 𝐷 ) ) , ( 2^nd ‘ ( 𝐶 swap_F 𝐷 ) ) ⟩ )
35	7 5	eleqtrdi	⊢ ( 𝜑 → 𝑋 ∈ ( Base ‘ 𝐶 ) )
36	8 6	eleqtrdi	⊢ ( 𝜑 → 𝑌 ∈ ( Base ‘ 𝐷 ) )
37	34 35 36	swapf1	⊢ ( 𝜑 → ( 𝑋 ( 1^st ‘ ( 𝐶 swap_F 𝐷 ) ) 𝑌 ) = ⟨ 𝑌 , 𝑋 ⟩ )
38	31 37	eqtr3id	⊢ ( 𝜑 → ( ( 1^st ‘ ( 𝐶 swap_F 𝐷 ) ) ‘ ⟨ 𝑋 , 𝑌 ⟩ ) = ⟨ 𝑌 , 𝑋 ⟩ )
39		df-ov	⊢ ( 𝑍 ( 1^st ‘ ( 𝐶 swap_F 𝐷 ) ) 𝑊 ) = ( ( 1^st ‘ ( 𝐶 swap_F 𝐷 ) ) ‘ ⟨ 𝑍 , 𝑊 ⟩ )
40	9 5	eleqtrdi	⊢ ( 𝜑 → 𝑍 ∈ ( Base ‘ 𝐶 ) )
41	10 6	eleqtrdi	⊢ ( 𝜑 → 𝑊 ∈ ( Base ‘ 𝐷 ) )
42	34 40 41	swapf1	⊢ ( 𝜑 → ( 𝑍 ( 1^st ‘ ( 𝐶 swap_F 𝐷 ) ) 𝑊 ) = ⟨ 𝑊 , 𝑍 ⟩ )
43	39 42	eqtr3id	⊢ ( 𝜑 → ( ( 1^st ‘ ( 𝐶 swap_F 𝐷 ) ) ‘ ⟨ 𝑍 , 𝑊 ⟩ ) = ⟨ 𝑊 , 𝑍 ⟩ )
44	38 43	oveq12d	⊢ ( 𝜑 → ( ( ( 1^st ‘ ( 𝐶 swap_F 𝐷 ) ) ‘ ⟨ 𝑋 , 𝑌 ⟩ ) ( 2^nd ‘ 𝐹 ) ( ( 1^st ‘ ( 𝐶 swap_F 𝐷 ) ) ‘ ⟨ 𝑍 , 𝑊 ⟩ ) ) = ( ⟨ 𝑌 , 𝑋 ⟩ ( 2^nd ‘ 𝐹 ) ⟨ 𝑊 , 𝑍 ⟩ ) )
45		df-ov	⊢ ( 𝑀 ( ⟨ 𝑋 , 𝑌 ⟩ ( 2^nd ‘ ( 𝐶 swap_F 𝐷 ) ) ⟨ 𝑍 , 𝑊 ⟩ ) 𝑁 ) = ( ( ⟨ 𝑋 , 𝑌 ⟩ ( 2^nd ‘ ( 𝐶 swap_F 𝐷 ) ) ⟨ 𝑍 , 𝑊 ⟩ ) ‘ ⟨ 𝑀 , 𝑁 ⟩ )
46	11	oveqi	⊢ ( 𝑋 𝐻 𝑍 ) = ( 𝑋 ( Hom ‘ 𝐶 ) 𝑍 )
47	13 46	eleqtrdi	⊢ ( 𝜑 → 𝑀 ∈ ( 𝑋 ( Hom ‘ 𝐶 ) 𝑍 ) )
48	12	oveqi	⊢ ( 𝑌 𝐽 𝑊 ) = ( 𝑌 ( Hom ‘ 𝐷 ) 𝑊 )
49	14 48	eleqtrdi	⊢ ( 𝜑 → 𝑁 ∈ ( 𝑌 ( Hom ‘ 𝐷 ) 𝑊 ) )
50	34 35 36 40 41 47 49	swapf2	⊢ ( 𝜑 → ( 𝑀 ( ⟨ 𝑋 , 𝑌 ⟩ ( 2^nd ‘ ( 𝐶 swap_F 𝐷 ) ) ⟨ 𝑍 , 𝑊 ⟩ ) 𝑁 ) = ⟨ 𝑁 , 𝑀 ⟩ )
51	45 50	eqtr3id	⊢ ( 𝜑 → ( ( ⟨ 𝑋 , 𝑌 ⟩ ( 2^nd ‘ ( 𝐶 swap_F 𝐷 ) ) ⟨ 𝑍 , 𝑊 ⟩ ) ‘ ⟨ 𝑀 , 𝑁 ⟩ ) = ⟨ 𝑁 , 𝑀 ⟩ )
52	44 51	fveq12d	⊢ ( 𝜑 → ( ( ( ( 1^st ‘ ( 𝐶 swap_F 𝐷 ) ) ‘ ⟨ 𝑋 , 𝑌 ⟩ ) ( 2^nd ‘ 𝐹 ) ( ( 1^st ‘ ( 𝐶 swap_F 𝐷 ) ) ‘ ⟨ 𝑍 , 𝑊 ⟩ ) ) ‘ ( ( ⟨ 𝑋 , 𝑌 ⟩ ( 2^nd ‘ ( 𝐶 swap_F 𝐷 ) ) ⟨ 𝑍 , 𝑊 ⟩ ) ‘ ⟨ 𝑀 , 𝑁 ⟩ ) ) = ( ( ⟨ 𝑌 , 𝑋 ⟩ ( 2^nd ‘ 𝐹 ) ⟨ 𝑊 , 𝑍 ⟩ ) ‘ ⟨ 𝑁 , 𝑀 ⟩ ) )
53	17 30 52	3eqtrd	⊢ ( 𝜑 → ( 𝑀 ( ⟨ 𝑋 , 𝑌 ⟩ ( 2^nd ‘ 𝐺 ) ⟨ 𝑍 , 𝑊 ⟩ ) 𝑁 ) = ( ( ⟨ 𝑌 , 𝑋 ⟩ ( 2^nd ‘ 𝐹 ) ⟨ 𝑊 , 𝑍 ⟩ ) ‘ ⟨ 𝑁 , 𝑀 ⟩ ) )
54		df-ov	⊢ ( 𝑁 ( ⟨ 𝑌 , 𝑋 ⟩ ( 2^nd ‘ 𝐹 ) ⟨ 𝑊 , 𝑍 ⟩ ) 𝑀 ) = ( ( ⟨ 𝑌 , 𝑋 ⟩ ( 2^nd ‘ 𝐹 ) ⟨ 𝑊 , 𝑍 ⟩ ) ‘ ⟨ 𝑁 , 𝑀 ⟩ )
55	53 54	eqtr4di	⊢ ( 𝜑 → ( 𝑀 ( ⟨ 𝑋 , 𝑌 ⟩ ( 2^nd ‘ 𝐺 ) ⟨ 𝑍 , 𝑊 ⟩ ) 𝑁 ) = ( 𝑁 ( ⟨ 𝑌 , 𝑋 ⟩ ( 2^nd ‘ 𝐹 ) ⟨ 𝑊 , 𝑍 ⟩ ) 𝑀 ) )

Metamath Proof Explorer

Theorem cofuswapf2

Proof