cofuoppf

Description: Composition of opposite functors. (Contributed by Zhi Wang, 26-Nov-2025)

	Ref	Expression
Hypotheses	cofuoppf.k	⊢ ( 𝜑 → ( 𝐺 ∘_func 𝐹 ) = 𝐾 )
	cofuoppf.f	⊢ ( 𝜑 → 𝐹 ∈ ( 𝐶 Func 𝐷 ) )
	cofuoppf.g	⊢ ( 𝜑 → 𝐺 ∈ ( 𝐷 Func 𝐸 ) )
Assertion	cofuoppf	⊢ ( 𝜑 → ( ( oppFunc ‘ 𝐺 ) ∘_func ( oppFunc ‘ 𝐹 ) ) = ( oppFunc ‘ 𝐾 ) )

Proof

Step	Hyp	Ref	Expression
1		cofuoppf.k	⊢ ( 𝜑 → ( 𝐺 ∘_func 𝐹 ) = 𝐾 )
2		cofuoppf.f	⊢ ( 𝜑 → 𝐹 ∈ ( 𝐶 Func 𝐷 ) )
3		cofuoppf.g	⊢ ( 𝜑 → 𝐺 ∈ ( 𝐷 Func 𝐸 ) )
4		eqid	⊢ ( oppCat ‘ 𝐶 ) = ( oppCat ‘ 𝐶 )
5		eqid	⊢ ( Base ‘ 𝐶 ) = ( Base ‘ 𝐶 )
6	4 5	oppcbas	⊢ ( Base ‘ 𝐶 ) = ( Base ‘ ( oppCat ‘ 𝐶 ) )
7		eqid	⊢ ( oppCat ‘ 𝐷 ) = ( oppCat ‘ 𝐷 )
8	2	func1st2nd	⊢ ( 𝜑 → ( 1^st ‘ 𝐹 ) ( 𝐶 Func 𝐷 ) ( 2^nd ‘ 𝐹 ) )
9	4 7 8	funcoppc	⊢ ( 𝜑 → ( 1^st ‘ 𝐹 ) ( ( oppCat ‘ 𝐶 ) Func ( oppCat ‘ 𝐷 ) ) tpos ( 2^nd ‘ 𝐹 ) )
10		eqid	⊢ ( oppCat ‘ 𝐸 ) = ( oppCat ‘ 𝐸 )
11	3	func1st2nd	⊢ ( 𝜑 → ( 1^st ‘ 𝐺 ) ( 𝐷 Func 𝐸 ) ( 2^nd ‘ 𝐺 ) )
12	7 10 11	funcoppc	⊢ ( 𝜑 → ( 1^st ‘ 𝐺 ) ( ( oppCat ‘ 𝐷 ) Func ( oppCat ‘ 𝐸 ) ) tpos ( 2^nd ‘ 𝐺 ) )
13	6 9 12	cofuval2	⊢ ( 𝜑 → ( ⟨ ( 1^st ‘ 𝐺 ) , tpos ( 2^nd ‘ 𝐺 ) ⟩ ∘_func ⟨ ( 1^st ‘ 𝐹 ) , tpos ( 2^nd ‘ 𝐹 ) ⟩ ) = ⟨ ( ( 1^st ‘ 𝐺 ) ∘ ( 1^st ‘ 𝐹 ) ) , ( 𝑦 ∈ ( Base ‘ 𝐶 ) , 𝑥 ∈ ( Base ‘ 𝐶 ) ↦ ( ( ( ( 1^st ‘ 𝐹 ) ‘ 𝑦 ) tpos ( 2^nd ‘ 𝐺 ) ( ( 1^st ‘ 𝐹 ) ‘ 𝑥 ) ) ∘ ( 𝑦 tpos ( 2^nd ‘ 𝐹 ) 𝑥 ) ) ) ⟩ )
14		oppfval2	⊢ ( 𝐺 ∈ ( 𝐷 Func 𝐸 ) → ( oppFunc ‘ 𝐺 ) = ⟨ ( 1^st ‘ 𝐺 ) , tpos ( 2^nd ‘ 𝐺 ) ⟩ )
15	3 14	syl	⊢ ( 𝜑 → ( oppFunc ‘ 𝐺 ) = ⟨ ( 1^st ‘ 𝐺 ) , tpos ( 2^nd ‘ 𝐺 ) ⟩ )
16		oppfval2	⊢ ( 𝐹 ∈ ( 𝐶 Func 𝐷 ) → ( oppFunc ‘ 𝐹 ) = ⟨ ( 1^st ‘ 𝐹 ) , tpos ( 2^nd ‘ 𝐹 ) ⟩ )
17	2 16	syl	⊢ ( 𝜑 → ( oppFunc ‘ 𝐹 ) = ⟨ ( 1^st ‘ 𝐹 ) , tpos ( 2^nd ‘ 𝐹 ) ⟩ )
18	15 17	oveq12d	⊢ ( 𝜑 → ( ( oppFunc ‘ 𝐺 ) ∘_func ( oppFunc ‘ 𝐹 ) ) = ( ⟨ ( 1^st ‘ 𝐺 ) , tpos ( 2^nd ‘ 𝐺 ) ⟩ ∘_func ⟨ ( 1^st ‘ 𝐹 ) , tpos ( 2^nd ‘ 𝐹 ) ⟩ ) )
19	5 2 3	cofuval	⊢ ( 𝜑 → ( 𝐺 ∘_func 𝐹 ) = ⟨ ( ( 1^st ‘ 𝐺 ) ∘ ( 1^st ‘ 𝐹 ) ) , ( 𝑥 ∈ ( Base ‘ 𝐶 ) , 𝑦 ∈ ( Base ‘ 𝐶 ) ↦ ( ( ( ( 1^st ‘ 𝐹 ) ‘ 𝑥 ) ( 2^nd ‘ 𝐺 ) ( ( 1^st ‘ 𝐹 ) ‘ 𝑦 ) ) ∘ ( 𝑥 ( 2^nd ‘ 𝐹 ) 𝑦 ) ) ) ⟩ )
20	1 19	eqtr3d	⊢ ( 𝜑 → 𝐾 = ⟨ ( ( 1^st ‘ 𝐺 ) ∘ ( 1^st ‘ 𝐹 ) ) , ( 𝑥 ∈ ( Base ‘ 𝐶 ) , 𝑦 ∈ ( Base ‘ 𝐶 ) ↦ ( ( ( ( 1^st ‘ 𝐹 ) ‘ 𝑥 ) ( 2^nd ‘ 𝐺 ) ( ( 1^st ‘ 𝐹 ) ‘ 𝑦 ) ) ∘ ( 𝑥 ( 2^nd ‘ 𝐹 ) 𝑦 ) ) ) ⟩ )
21	2 3	cofucl	⊢ ( 𝜑 → ( 𝐺 ∘_func 𝐹 ) ∈ ( 𝐶 Func 𝐸 ) )
22	1 21	eqeltrrd	⊢ ( 𝜑 → 𝐾 ∈ ( 𝐶 Func 𝐸 ) )
23	20 22	oppfval3	⊢ ( 𝜑 → ( oppFunc ‘ 𝐾 ) = ⟨ ( ( 1^st ‘ 𝐺 ) ∘ ( 1^st ‘ 𝐹 ) ) , tpos ( 𝑥 ∈ ( Base ‘ 𝐶 ) , 𝑦 ∈ ( Base ‘ 𝐶 ) ↦ ( ( ( ( 1^st ‘ 𝐹 ) ‘ 𝑥 ) ( 2^nd ‘ 𝐺 ) ( ( 1^st ‘ 𝐹 ) ‘ 𝑦 ) ) ∘ ( 𝑥 ( 2^nd ‘ 𝐹 ) 𝑦 ) ) ) ⟩ )
24		ovtpos	⊢ ( ( ( 1^st ‘ 𝐹 ) ‘ 𝑦 ) tpos ( 2^nd ‘ 𝐺 ) ( ( 1^st ‘ 𝐹 ) ‘ 𝑥 ) ) = ( ( ( 1^st ‘ 𝐹 ) ‘ 𝑥 ) ( 2^nd ‘ 𝐺 ) ( ( 1^st ‘ 𝐹 ) ‘ 𝑦 ) )
25		ovtpos	⊢ ( 𝑦 tpos ( 2^nd ‘ 𝐹 ) 𝑥 ) = ( 𝑥 ( 2^nd ‘ 𝐹 ) 𝑦 )
26	24 25	coeq12i	⊢ ( ( ( ( 1^st ‘ 𝐹 ) ‘ 𝑦 ) tpos ( 2^nd ‘ 𝐺 ) ( ( 1^st ‘ 𝐹 ) ‘ 𝑥 ) ) ∘ ( 𝑦 tpos ( 2^nd ‘ 𝐹 ) 𝑥 ) ) = ( ( ( ( 1^st ‘ 𝐹 ) ‘ 𝑥 ) ( 2^nd ‘ 𝐺 ) ( ( 1^st ‘ 𝐹 ) ‘ 𝑦 ) ) ∘ ( 𝑥 ( 2^nd ‘ 𝐹 ) 𝑦 ) )
27	26	eqcomi	⊢ ( ( ( ( 1^st ‘ 𝐹 ) ‘ 𝑥 ) ( 2^nd ‘ 𝐺 ) ( ( 1^st ‘ 𝐹 ) ‘ 𝑦 ) ) ∘ ( 𝑥 ( 2^nd ‘ 𝐹 ) 𝑦 ) ) = ( ( ( ( 1^st ‘ 𝐹 ) ‘ 𝑦 ) tpos ( 2^nd ‘ 𝐺 ) ( ( 1^st ‘ 𝐹 ) ‘ 𝑥 ) ) ∘ ( 𝑦 tpos ( 2^nd ‘ 𝐹 ) 𝑥 ) )
28	27	a1i	⊢ ( ( 𝑥 ∈ ( Base ‘ 𝐶 ) ∧ 𝑦 ∈ ( Base ‘ 𝐶 ) ) → ( ( ( ( 1^st ‘ 𝐹 ) ‘ 𝑥 ) ( 2^nd ‘ 𝐺 ) ( ( 1^st ‘ 𝐹 ) ‘ 𝑦 ) ) ∘ ( 𝑥 ( 2^nd ‘ 𝐹 ) 𝑦 ) ) = ( ( ( ( 1^st ‘ 𝐹 ) ‘ 𝑦 ) tpos ( 2^nd ‘ 𝐺 ) ( ( 1^st ‘ 𝐹 ) ‘ 𝑥 ) ) ∘ ( 𝑦 tpos ( 2^nd ‘ 𝐹 ) 𝑥 ) ) )
29	28	mpoeq3ia	⊢ ( 𝑥 ∈ ( Base ‘ 𝐶 ) , 𝑦 ∈ ( Base ‘ 𝐶 ) ↦ ( ( ( ( 1^st ‘ 𝐹 ) ‘ 𝑥 ) ( 2^nd ‘ 𝐺 ) ( ( 1^st ‘ 𝐹 ) ‘ 𝑦 ) ) ∘ ( 𝑥 ( 2^nd ‘ 𝐹 ) 𝑦 ) ) ) = ( 𝑥 ∈ ( Base ‘ 𝐶 ) , 𝑦 ∈ ( Base ‘ 𝐶 ) ↦ ( ( ( ( 1^st ‘ 𝐹 ) ‘ 𝑦 ) tpos ( 2^nd ‘ 𝐺 ) ( ( 1^st ‘ 𝐹 ) ‘ 𝑥 ) ) ∘ ( 𝑦 tpos ( 2^nd ‘ 𝐹 ) 𝑥 ) ) )
30	29	tposmpo	⊢ tpos ( 𝑥 ∈ ( Base ‘ 𝐶 ) , 𝑦 ∈ ( Base ‘ 𝐶 ) ↦ ( ( ( ( 1^st ‘ 𝐹 ) ‘ 𝑥 ) ( 2^nd ‘ 𝐺 ) ( ( 1^st ‘ 𝐹 ) ‘ 𝑦 ) ) ∘ ( 𝑥 ( 2^nd ‘ 𝐹 ) 𝑦 ) ) ) = ( 𝑦 ∈ ( Base ‘ 𝐶 ) , 𝑥 ∈ ( Base ‘ 𝐶 ) ↦ ( ( ( ( 1^st ‘ 𝐹 ) ‘ 𝑦 ) tpos ( 2^nd ‘ 𝐺 ) ( ( 1^st ‘ 𝐹 ) ‘ 𝑥 ) ) ∘ ( 𝑦 tpos ( 2^nd ‘ 𝐹 ) 𝑥 ) ) )
31	30	opeq2i	⊢ ⟨ ( ( 1^st ‘ 𝐺 ) ∘ ( 1^st ‘ 𝐹 ) ) , tpos ( 𝑥 ∈ ( Base ‘ 𝐶 ) , 𝑦 ∈ ( Base ‘ 𝐶 ) ↦ ( ( ( ( 1^st ‘ 𝐹 ) ‘ 𝑥 ) ( 2^nd ‘ 𝐺 ) ( ( 1^st ‘ 𝐹 ) ‘ 𝑦 ) ) ∘ ( 𝑥 ( 2^nd ‘ 𝐹 ) 𝑦 ) ) ) ⟩ = ⟨ ( ( 1^st ‘ 𝐺 ) ∘ ( 1^st ‘ 𝐹 ) ) , ( 𝑦 ∈ ( Base ‘ 𝐶 ) , 𝑥 ∈ ( Base ‘ 𝐶 ) ↦ ( ( ( ( 1^st ‘ 𝐹 ) ‘ 𝑦 ) tpos ( 2^nd ‘ 𝐺 ) ( ( 1^st ‘ 𝐹 ) ‘ 𝑥 ) ) ∘ ( 𝑦 tpos ( 2^nd ‘ 𝐹 ) 𝑥 ) ) ) ⟩
32	23 31	eqtrdi	⊢ ( 𝜑 → ( oppFunc ‘ 𝐾 ) = ⟨ ( ( 1^st ‘ 𝐺 ) ∘ ( 1^st ‘ 𝐹 ) ) , ( 𝑦 ∈ ( Base ‘ 𝐶 ) , 𝑥 ∈ ( Base ‘ 𝐶 ) ↦ ( ( ( ( 1^st ‘ 𝐹 ) ‘ 𝑦 ) tpos ( 2^nd ‘ 𝐺 ) ( ( 1^st ‘ 𝐹 ) ‘ 𝑥 ) ) ∘ ( 𝑦 tpos ( 2^nd ‘ 𝐹 ) 𝑥 ) ) ) ⟩ )
33	13 18 32	3eqtr4d	⊢ ( 𝜑 → ( ( oppFunc ‘ 𝐺 ) ∘_func ( oppFunc ‘ 𝐹 ) ) = ( oppFunc ‘ 𝐾 ) )

Metamath Proof Explorer

Theorem cofuoppf

Proof