cofuswapf1

Description: The object 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	⊢ ( 𝜑 → 𝑌 ∈ 𝐵 )
Assertion	cofuswapf1	⊢ ( 𝜑 → ( 𝑋 ( 1^st ‘ 𝐺 ) 𝑌 ) = ( 𝑌 ( 1^st ‘ 𝐹 ) 𝑋 ) )

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		df-ov	⊢ ( 𝑋 ( 1^st ‘ 𝐺 ) 𝑌 ) = ( ( 1^st ‘ 𝐺 ) ‘ ⟨ 𝑋 , 𝑌 ⟩ )
10	4	fveq2d	⊢ ( 𝜑 → ( 1^st ‘ 𝐺 ) = ( 1^st ‘ ( 𝐹 ∘_func ( 𝐶 swap_F 𝐷 ) ) ) )
11	10	fveq1d	⊢ ( 𝜑 → ( ( 1^st ‘ 𝐺 ) ‘ ⟨ 𝑋 , 𝑌 ⟩ ) = ( ( 1^st ‘ ( 𝐹 ∘_func ( 𝐶 swap_F 𝐷 ) ) ) ‘ ⟨ 𝑋 , 𝑌 ⟩ ) )
12	9 11	eqtrid	⊢ ( 𝜑 → ( 𝑋 ( 1^st ‘ 𝐺 ) 𝑌 ) = ( ( 1^st ‘ ( 𝐹 ∘_func ( 𝐶 swap_F 𝐷 ) ) ) ‘ ⟨ 𝑋 , 𝑌 ⟩ ) )
13		eqid	⊢ ( 𝐶 ×_c 𝐷 ) = ( 𝐶 ×_c 𝐷 )
14	13 5 6	xpcbas	⊢ ( 𝐴 × 𝐵 ) = ( Base ‘ ( 𝐶 ×_c 𝐷 ) )
15		eqid	⊢ ( 𝐷 ×_c 𝐶 ) = ( 𝐷 ×_c 𝐶 )
16	1 2 13 15	swapffunca	⊢ ( 𝜑 → ( 𝐶 swap_F 𝐷 ) ∈ ( ( 𝐶 ×_c 𝐷 ) Func ( 𝐷 ×_c 𝐶 ) ) )
17	7 8	opelxpd	⊢ ( 𝜑 → ⟨ 𝑋 , 𝑌 ⟩ ∈ ( 𝐴 × 𝐵 ) )
18	14 16 3 17	cofu1	⊢ ( 𝜑 → ( ( 1^st ‘ ( 𝐹 ∘_func ( 𝐶 swap_F 𝐷 ) ) ) ‘ ⟨ 𝑋 , 𝑌 ⟩ ) = ( ( 1^st ‘ 𝐹 ) ‘ ( ( 1^st ‘ ( 𝐶 swap_F 𝐷 ) ) ‘ ⟨ 𝑋 , 𝑌 ⟩ ) ) )
19		df-ov	⊢ ( 𝑋 ( 1^st ‘ ( 𝐶 swap_F 𝐷 ) ) 𝑌 ) = ( ( 1^st ‘ ( 𝐶 swap_F 𝐷 ) ) ‘ ⟨ 𝑋 , 𝑌 ⟩ )
20	1 2	swapfelvv	⊢ ( 𝜑 → ( 𝐶 swap_F 𝐷 ) ∈ ( V × V ) )
21		1st2nd2	⊢ ( ( 𝐶 swap_F 𝐷 ) ∈ ( V × V ) → ( 𝐶 swap_F 𝐷 ) = ⟨ ( 1^st ‘ ( 𝐶 swap_F 𝐷 ) ) , ( 2^nd ‘ ( 𝐶 swap_F 𝐷 ) ) ⟩ )
22	20 21	syl	⊢ ( 𝜑 → ( 𝐶 swap_F 𝐷 ) = ⟨ ( 1^st ‘ ( 𝐶 swap_F 𝐷 ) ) , ( 2^nd ‘ ( 𝐶 swap_F 𝐷 ) ) ⟩ )
23	7 5	eleqtrdi	⊢ ( 𝜑 → 𝑋 ∈ ( Base ‘ 𝐶 ) )
24	8 6	eleqtrdi	⊢ ( 𝜑 → 𝑌 ∈ ( Base ‘ 𝐷 ) )
25	22 23 24	swapf1	⊢ ( 𝜑 → ( 𝑋 ( 1^st ‘ ( 𝐶 swap_F 𝐷 ) ) 𝑌 ) = ⟨ 𝑌 , 𝑋 ⟩ )
26	19 25	eqtr3id	⊢ ( 𝜑 → ( ( 1^st ‘ ( 𝐶 swap_F 𝐷 ) ) ‘ ⟨ 𝑋 , 𝑌 ⟩ ) = ⟨ 𝑌 , 𝑋 ⟩ )
27	26	fveq2d	⊢ ( 𝜑 → ( ( 1^st ‘ 𝐹 ) ‘ ( ( 1^st ‘ ( 𝐶 swap_F 𝐷 ) ) ‘ ⟨ 𝑋 , 𝑌 ⟩ ) ) = ( ( 1^st ‘ 𝐹 ) ‘ ⟨ 𝑌 , 𝑋 ⟩ ) )
28	12 18 27	3eqtrd	⊢ ( 𝜑 → ( 𝑋 ( 1^st ‘ 𝐺 ) 𝑌 ) = ( ( 1^st ‘ 𝐹 ) ‘ ⟨ 𝑌 , 𝑋 ⟩ ) )
29		df-ov	⊢ ( 𝑌 ( 1^st ‘ 𝐹 ) 𝑋 ) = ( ( 1^st ‘ 𝐹 ) ‘ ⟨ 𝑌 , 𝑋 ⟩ )
30	28 29	eqtr4di	⊢ ( 𝜑 → ( 𝑋 ( 1^st ‘ 𝐺 ) 𝑌 ) = ( 𝑌 ( 1^st ‘ 𝐹 ) 𝑋 ) )

Metamath Proof Explorer

Theorem cofuswapf1

Proof