Theorem oppc2ndf

Description: The opposite functor of the second projection functor is the second projection functor of opposite categories. (Contributed by Zhi Wang, 19-Nov-2025)

	Ref	Expression
Hypotheses	oppc1stf.o	⊢ 𝑂 = ( oppCat ‘ 𝐶 )
	oppc1stf.p	⊢ 𝑃 = ( oppCat ‘ 𝐷 )
	oppc1stf.c	⊢ ( 𝜑 → 𝐶 ∈ 𝑉 )
	oppc1stf.d	⊢ ( 𝜑 → 𝐷 ∈ 𝑊 )
Assertion	oppc2ndf	⊢ ( 𝜑 → ( oppFunc ‘ ( 𝐶 2ndF 𝐷 ) ) = ( 𝑂 2ndF 𝑃 ) )

Proof

Step	Hyp	Ref	Expression
1		oppc1stf.o	⊢ 𝑂 = ( oppCat ‘ 𝐶 )
2		oppc1stf.p	⊢ 𝑃 = ( oppCat ‘ 𝐷 )
3		oppc1stf.c	⊢ ( 𝜑 → 𝐶 ∈ 𝑉 )
4		oppc1stf.d	⊢ ( 𝜑 → 𝐷 ∈ 𝑊 )
5		eqid	⊢ ( 𝑥 ∈ ( ( Base ‘ 𝐶 ) × ( Base ‘ 𝐷 ) ) , 𝑦 ∈ ( ( Base ‘ 𝐶 ) × ( Base ‘ 𝐷 ) ) ↦ ( 2nd ↾ ( 𝑥 ( Hom ‘ ( 𝐶 ×c 𝐷 ) ) 𝑦 ) ) ) = ( 𝑥 ∈ ( ( Base ‘ 𝐶 ) × ( Base ‘ 𝐷 ) ) , 𝑦 ∈ ( ( Base ‘ 𝐶 ) × ( Base ‘ 𝐷 ) ) ↦ ( 2nd ↾ ( 𝑥 ( Hom ‘ ( 𝐶 ×c 𝐷 ) ) 𝑦 ) ) )
6	5	tposmpo	⊢ tpos ( 𝑥 ∈ ( ( Base ‘ 𝐶 ) × ( Base ‘ 𝐷 ) ) , 𝑦 ∈ ( ( Base ‘ 𝐶 ) × ( Base ‘ 𝐷 ) ) ↦ ( 2nd ↾ ( 𝑥 ( Hom ‘ ( 𝐶 ×c 𝐷 ) ) 𝑦 ) ) ) = ( 𝑦 ∈ ( ( Base ‘ 𝐶 ) × ( Base ‘ 𝐷 ) ) , 𝑥 ∈ ( ( Base ‘ 𝐶 ) × ( Base ‘ 𝐷 ) ) ↦ ( 2nd ↾ ( 𝑥 ( Hom ‘ ( 𝐶 ×c 𝐷 ) ) 𝑦 ) ) )
7		eqid	⊢ ( Hom ‘ 𝐶 ) = ( Hom ‘ 𝐶 )
8	7 1	oppchom	⊢ ( ( 1st ‘ 𝑦 ) ( Hom ‘ 𝑂 ) ( 1st ‘ 𝑥 ) ) = ( ( 1st ‘ 𝑥 ) ( Hom ‘ 𝐶 ) ( 1st ‘ 𝑦 ) )
9		eqid	⊢ ( Hom ‘ 𝐷 ) = ( Hom ‘ 𝐷 )
10	9 2	oppchom	⊢ ( ( 2nd ‘ 𝑦 ) ( Hom ‘ 𝑃 ) ( 2nd ‘ 𝑥 ) ) = ( ( 2nd ‘ 𝑥 ) ( Hom ‘ 𝐷 ) ( 2nd ‘ 𝑦 ) )
11	8 10	xpeq12i	⊢ ( ( ( 1st ‘ 𝑦 ) ( Hom ‘ 𝑂 ) ( 1st ‘ 𝑥 ) ) × ( ( 2nd ‘ 𝑦 ) ( Hom ‘ 𝑃 ) ( 2nd ‘ 𝑥 ) ) ) = ( ( ( 1st ‘ 𝑥 ) ( Hom ‘ 𝐶 ) ( 1st ‘ 𝑦 ) ) × ( ( 2nd ‘ 𝑥 ) ( Hom ‘ 𝐷 ) ( 2nd ‘ 𝑦 ) ) )
12		eqid	⊢ ( 𝑂 ×c 𝑃 ) = ( 𝑂 ×c 𝑃 )
13		eqid	⊢ ( Base ‘ 𝐶 ) = ( Base ‘ 𝐶 )
14	1 13	oppcbas	⊢ ( Base ‘ 𝐶 ) = ( Base ‘ 𝑂 )
15		eqid	⊢ ( Base ‘ 𝐷 ) = ( Base ‘ 𝐷 )
16	2 15	oppcbas	⊢ ( Base ‘ 𝐷 ) = ( Base ‘ 𝑃 )
17	12 14 16	xpcbas	⊢ ( ( Base ‘ 𝐶 ) × ( Base ‘ 𝐷 ) ) = ( Base ‘ ( 𝑂 ×c 𝑃 ) )
18		eqid	⊢ ( Hom ‘ 𝑂 ) = ( Hom ‘ 𝑂 )
19		eqid	⊢ ( Hom ‘ 𝑃 ) = ( Hom ‘ 𝑃 )
20		eqid	⊢ ( Hom ‘ ( 𝑂 ×c 𝑃 ) ) = ( Hom ‘ ( 𝑂 ×c 𝑃 ) )
21		simp2	⊢ ( ( ( 𝜑 ∧ ( 𝐶 ∈ Cat ∧ 𝐷 ∈ Cat ) ) ∧ 𝑦 ∈ ( ( Base ‘ 𝐶 ) × ( Base ‘ 𝐷 ) ) ∧ 𝑥 ∈ ( ( Base ‘ 𝐶 ) × ( Base ‘ 𝐷 ) ) ) → 𝑦 ∈ ( ( Base ‘ 𝐶 ) × ( Base ‘ 𝐷 ) ) )
22		simp3	⊢ ( ( ( 𝜑 ∧ ( 𝐶 ∈ Cat ∧ 𝐷 ∈ Cat ) ) ∧ 𝑦 ∈ ( ( Base ‘ 𝐶 ) × ( Base ‘ 𝐷 ) ) ∧ 𝑥 ∈ ( ( Base ‘ 𝐶 ) × ( Base ‘ 𝐷 ) ) ) → 𝑥 ∈ ( ( Base ‘ 𝐶 ) × ( Base ‘ 𝐷 ) ) )
23	12 17 18 19 20 21 22	xpchom	⊢ ( ( ( 𝜑 ∧ ( 𝐶 ∈ Cat ∧ 𝐷 ∈ Cat ) ) ∧ 𝑦 ∈ ( ( Base ‘ 𝐶 ) × ( Base ‘ 𝐷 ) ) ∧ 𝑥 ∈ ( ( Base ‘ 𝐶 ) × ( Base ‘ 𝐷 ) ) ) → ( 𝑦 ( Hom ‘ ( 𝑂 ×c 𝑃 ) ) 𝑥 ) = ( ( ( 1st ‘ 𝑦 ) ( Hom ‘ 𝑂 ) ( 1st ‘ 𝑥 ) ) × ( ( 2nd ‘ 𝑦 ) ( Hom ‘ 𝑃 ) ( 2nd ‘ 𝑥 ) ) ) )
24		eqid	⊢ ( 𝐶 ×c 𝐷 ) = ( 𝐶 ×c 𝐷 )
25	24 13 15	xpcbas	⊢ ( ( Base ‘ 𝐶 ) × ( Base ‘ 𝐷 ) ) = ( Base ‘ ( 𝐶 ×c 𝐷 ) )
26		eqid	⊢ ( Hom ‘ ( 𝐶 ×c 𝐷 ) ) = ( Hom ‘ ( 𝐶 ×c 𝐷 ) )
27	24 25 7 9 26 22 21	xpchom	⊢ ( ( ( 𝜑 ∧ ( 𝐶 ∈ Cat ∧ 𝐷 ∈ Cat ) ) ∧ 𝑦 ∈ ( ( Base ‘ 𝐶 ) × ( Base ‘ 𝐷 ) ) ∧ 𝑥 ∈ ( ( Base ‘ 𝐶 ) × ( Base ‘ 𝐷 ) ) ) → ( 𝑥 ( Hom ‘ ( 𝐶 ×c 𝐷 ) ) 𝑦 ) = ( ( ( 1st ‘ 𝑥 ) ( Hom ‘ 𝐶 ) ( 1st ‘ 𝑦 ) ) × ( ( 2nd ‘ 𝑥 ) ( Hom ‘ 𝐷 ) ( 2nd ‘ 𝑦 ) ) ) )
28	11 23 27	3eqtr4a	⊢ ( ( ( 𝜑 ∧ ( 𝐶 ∈ Cat ∧ 𝐷 ∈ Cat ) ) ∧ 𝑦 ∈ ( ( Base ‘ 𝐶 ) × ( Base ‘ 𝐷 ) ) ∧ 𝑥 ∈ ( ( Base ‘ 𝐶 ) × ( Base ‘ 𝐷 ) ) ) → ( 𝑦 ( Hom ‘ ( 𝑂 ×c 𝑃 ) ) 𝑥 ) = ( 𝑥 ( Hom ‘ ( 𝐶 ×c 𝐷 ) ) 𝑦 ) )
29	28	reseq2d	⊢ ( ( ( 𝜑 ∧ ( 𝐶 ∈ Cat ∧ 𝐷 ∈ Cat ) ) ∧ 𝑦 ∈ ( ( Base ‘ 𝐶 ) × ( Base ‘ 𝐷 ) ) ∧ 𝑥 ∈ ( ( Base ‘ 𝐶 ) × ( Base ‘ 𝐷 ) ) ) → ( 2nd ↾ ( 𝑦 ( Hom ‘ ( 𝑂 ×c 𝑃 ) ) 𝑥 ) ) = ( 2nd ↾ ( 𝑥 ( Hom ‘ ( 𝐶 ×c 𝐷 ) ) 𝑦 ) ) )
30	29	mpoeq3dva	⊢ ( ( 𝜑 ∧ ( 𝐶 ∈ Cat ∧ 𝐷 ∈ Cat ) ) → ( 𝑦 ∈ ( ( Base ‘ 𝐶 ) × ( Base ‘ 𝐷 ) ) , 𝑥 ∈ ( ( Base ‘ 𝐶 ) × ( Base ‘ 𝐷 ) ) ↦ ( 2nd ↾ ( 𝑦 ( Hom ‘ ( 𝑂 ×c 𝑃 ) ) 𝑥 ) ) ) = ( 𝑦 ∈ ( ( Base ‘ 𝐶 ) × ( Base ‘ 𝐷 ) ) , 𝑥 ∈ ( ( Base ‘ 𝐶 ) × ( Base ‘ 𝐷 ) ) ↦ ( 2nd ↾ ( 𝑥 ( Hom ‘ ( 𝐶 ×c 𝐷 ) ) 𝑦 ) ) ) )
31	6 30	eqtr4id	⊢ ( ( 𝜑 ∧ ( 𝐶 ∈ Cat ∧ 𝐷 ∈ Cat ) ) → tpos ( 𝑥 ∈ ( ( Base ‘ 𝐶 ) × ( Base ‘ 𝐷 ) ) , 𝑦 ∈ ( ( Base ‘ 𝐶 ) × ( Base ‘ 𝐷 ) ) ↦ ( 2nd ↾ ( 𝑥 ( Hom ‘ ( 𝐶 ×c 𝐷 ) ) 𝑦 ) ) ) = ( 𝑦 ∈ ( ( Base ‘ 𝐶 ) × ( Base ‘ 𝐷 ) ) , 𝑥 ∈ ( ( Base ‘ 𝐶 ) × ( Base ‘ 𝐷 ) ) ↦ ( 2nd ↾ ( 𝑦 ( Hom ‘ ( 𝑂 ×c 𝑃 ) ) 𝑥 ) ) ) )
32	31	opeq2d	⊢ ( ( 𝜑 ∧ ( 𝐶 ∈ Cat ∧ 𝐷 ∈ Cat ) ) → ⟨ ( 2nd ↾ ( ( Base ‘ 𝐶 ) × ( Base ‘ 𝐷 ) ) ) , tpos ( 𝑥 ∈ ( ( Base ‘ 𝐶 ) × ( Base ‘ 𝐷 ) ) , 𝑦 ∈ ( ( Base ‘ 𝐶 ) × ( Base ‘ 𝐷 ) ) ↦ ( 2nd ↾ ( 𝑥 ( Hom ‘ ( 𝐶 ×c 𝐷 ) ) 𝑦 ) ) ) ⟩ = ⟨ ( 2nd ↾ ( ( Base ‘ 𝐶 ) × ( Base ‘ 𝐷 ) ) ) , ( 𝑦 ∈ ( ( Base ‘ 𝐶 ) × ( Base ‘ 𝐷 ) ) , 𝑥 ∈ ( ( Base ‘ 𝐶 ) × ( Base ‘ 𝐷 ) ) ↦ ( 2nd ↾ ( 𝑦 ( Hom ‘ ( 𝑂 ×c 𝑃 ) ) 𝑥 ) ) ) ⟩ )
33		simprl	⊢ ( ( 𝜑 ∧ ( 𝐶 ∈ Cat ∧ 𝐷 ∈ Cat ) ) → 𝐶 ∈ Cat )
34		simprr	⊢ ( ( 𝜑 ∧ ( 𝐶 ∈ Cat ∧ 𝐷 ∈ Cat ) ) → 𝐷 ∈ Cat )
35		eqid	⊢ ( 𝐶 2ndF 𝐷 ) = ( 𝐶 2ndF 𝐷 )
36	24 25 26 33 34 35	2ndfval	⊢ ( ( 𝜑 ∧ ( 𝐶 ∈ Cat ∧ 𝐷 ∈ Cat ) ) → ( 𝐶 2ndF 𝐷 ) = ⟨ ( 2nd ↾ ( ( Base ‘ 𝐶 ) × ( Base ‘ 𝐷 ) ) ) , ( 𝑥 ∈ ( ( Base ‘ 𝐶 ) × ( Base ‘ 𝐷 ) ) , 𝑦 ∈ ( ( Base ‘ 𝐶 ) × ( Base ‘ 𝐷 ) ) ↦ ( 2nd ↾ ( 𝑥 ( Hom ‘ ( 𝐶 ×c 𝐷 ) ) 𝑦 ) ) ) ⟩ )
37	24 33 34 35	2ndfcl	⊢ ( ( 𝜑 ∧ ( 𝐶 ∈ Cat ∧ 𝐷 ∈ Cat ) ) → ( 𝐶 2ndF 𝐷 ) ∈ ( ( 𝐶 ×c 𝐷 ) Func 𝐷 ) )
38	36 37	oppfval3	⊢ ( ( 𝜑 ∧ ( 𝐶 ∈ Cat ∧ 𝐷 ∈ Cat ) ) → ( oppFunc ‘ ( 𝐶 2ndF 𝐷 ) ) = ⟨ ( 2nd ↾ ( ( Base ‘ 𝐶 ) × ( Base ‘ 𝐷 ) ) ) , tpos ( 𝑥 ∈ ( ( Base ‘ 𝐶 ) × ( Base ‘ 𝐷 ) ) , 𝑦 ∈ ( ( Base ‘ 𝐶 ) × ( Base ‘ 𝐷 ) ) ↦ ( 2nd ↾ ( 𝑥 ( Hom ‘ ( 𝐶 ×c 𝐷 ) ) 𝑦 ) ) ) ⟩ )
39	1	oppccat	⊢ ( 𝐶 ∈ Cat → 𝑂 ∈ Cat )
40	33 39	syl	⊢ ( ( 𝜑 ∧ ( 𝐶 ∈ Cat ∧ 𝐷 ∈ Cat ) ) → 𝑂 ∈ Cat )
41	2	oppccat	⊢ ( 𝐷 ∈ Cat → 𝑃 ∈ Cat )
42	34 41	syl	⊢ ( ( 𝜑 ∧ ( 𝐶 ∈ Cat ∧ 𝐷 ∈ Cat ) ) → 𝑃 ∈ Cat )
43		eqid	⊢ ( 𝑂 2ndF 𝑃 ) = ( 𝑂 2ndF 𝑃 )
44	12 17 20 40 42 43	2ndfval	⊢ ( ( 𝜑 ∧ ( 𝐶 ∈ Cat ∧ 𝐷 ∈ Cat ) ) → ( 𝑂 2ndF 𝑃 ) = ⟨ ( 2nd ↾ ( ( Base ‘ 𝐶 ) × ( Base ‘ 𝐷 ) ) ) , ( 𝑦 ∈ ( ( Base ‘ 𝐶 ) × ( Base ‘ 𝐷 ) ) , 𝑥 ∈ ( ( Base ‘ 𝐶 ) × ( Base ‘ 𝐷 ) ) ↦ ( 2nd ↾ ( 𝑦 ( Hom ‘ ( 𝑂 ×c 𝑃 ) ) 𝑥 ) ) ) ⟩ )
45	32 38 44	3eqtr4d	⊢ ( ( 𝜑 ∧ ( 𝐶 ∈ Cat ∧ 𝐷 ∈ Cat ) ) → ( oppFunc ‘ ( 𝐶 2ndF 𝐷 ) ) = ( 𝑂 2ndF 𝑃 ) )
46		df-2ndf	⊢ 2ndF = ( 𝑐 ∈ Cat , 𝑑 ∈ Cat ↦ ⦋ ( ( Base ‘ 𝑐 ) × ( Base ‘ 𝑑 ) ) / 𝑏 ⦌ ⟨ ( 2nd ↾ 𝑏 ) , ( 𝑥 ∈ 𝑏 , 𝑦 ∈ 𝑏 ↦ ( 2nd ↾ ( 𝑥 ( Hom ‘ ( 𝑐 ×c 𝑑 ) ) 𝑦 ) ) ) ⟩ )
47	1 2 3 4 45 46	oppc1stflem	⊢ ( 𝜑 → ( oppFunc ‘ ( 𝐶 2ndF 𝐷 ) ) = ( 𝑂 2ndF 𝑃 ) )