natoppfb

Description: A natural transformation is natural between opposite functors, and vice versa. (Contributed by Zhi Wang, 18-Nov-2025)

	Ref	Expression
Hypotheses	natoppf.o	⊢ 𝑂 = ( oppCat ‘ 𝐶 )
	natoppf.p	⊢ 𝑃 = ( oppCat ‘ 𝐷 )
	natoppf.n	⊢ 𝑁 = ( 𝐶 Nat 𝐷 )
	natoppf.m	⊢ 𝑀 = ( 𝑂 Nat 𝑃 )
	natoppfb.k	⊢ ( 𝜑 → 𝐾 = ( oppFunc ‘ 𝐹 ) )
	natoppfb.l	⊢ ( 𝜑 → 𝐿 = ( oppFunc ‘ 𝐺 ) )
	natoppfb.c	⊢ ( 𝜑 → 𝐶 ∈ 𝑉 )
	natoppfb.d	⊢ ( 𝜑 → 𝐷 ∈ 𝑊 )
Assertion	natoppfb	⊢ ( 𝜑 → ( 𝐹 𝑁 𝐺 ) = ( 𝐿 𝑀 𝐾 ) )

Proof

Step	Hyp	Ref	Expression
1		natoppf.o	⊢ 𝑂 = ( oppCat ‘ 𝐶 )
2		natoppf.p	⊢ 𝑃 = ( oppCat ‘ 𝐷 )
3		natoppf.n	⊢ 𝑁 = ( 𝐶 Nat 𝐷 )
4		natoppf.m	⊢ 𝑀 = ( 𝑂 Nat 𝑃 )
5		natoppfb.k	⊢ ( 𝜑 → 𝐾 = ( oppFunc ‘ 𝐹 ) )
6		natoppfb.l	⊢ ( 𝜑 → 𝐿 = ( oppFunc ‘ 𝐺 ) )
7		natoppfb.c	⊢ ( 𝜑 → 𝐶 ∈ 𝑉 )
8		natoppfb.d	⊢ ( 𝜑 → 𝐷 ∈ 𝑊 )
9	5	adantr	⊢ ( ( 𝜑 ∧ 𝑥 ∈ ( 𝐹 𝑁 𝐺 ) ) → 𝐾 = ( oppFunc ‘ 𝐹 ) )
10	6	adantr	⊢ ( ( 𝜑 ∧ 𝑥 ∈ ( 𝐹 𝑁 𝐺 ) ) → 𝐿 = ( oppFunc ‘ 𝐺 ) )
11		simpr	⊢ ( ( 𝜑 ∧ 𝑥 ∈ ( 𝐹 𝑁 𝐺 ) ) → 𝑥 ∈ ( 𝐹 𝑁 𝐺 ) )
12	1 2 3 4 9 10 11	natoppf2	⊢ ( ( 𝜑 ∧ 𝑥 ∈ ( 𝐹 𝑁 𝐺 ) ) → 𝑥 ∈ ( 𝐿 𝑀 𝐾 ) )
13		eqid	⊢ ( oppCat ‘ 𝑂 ) = ( oppCat ‘ 𝑂 )
14		eqid	⊢ ( oppCat ‘ 𝑃 ) = ( oppCat ‘ 𝑃 )
15		eqid	⊢ ( ( oppCat ‘ 𝑂 ) Nat ( oppCat ‘ 𝑃 ) ) = ( ( oppCat ‘ 𝑂 ) Nat ( oppCat ‘ 𝑃 ) )
16	6	adantr	⊢ ( ( 𝜑 ∧ 𝑥 ∈ ( 𝐿 𝑀 𝐾 ) ) → 𝐿 = ( oppFunc ‘ 𝐺 ) )
17	16	fveq2d	⊢ ( ( 𝜑 ∧ 𝑥 ∈ ( 𝐿 𝑀 𝐾 ) ) → ( oppFunc ‘ 𝐿 ) = ( oppFunc ‘ ( oppFunc ‘ 𝐺 ) ) )
18	4	natrcl	⊢ ( 𝑥 ∈ ( 𝐿 𝑀 𝐾 ) → ( 𝐿 ∈ ( 𝑂 Func 𝑃 ) ∧ 𝐾 ∈ ( 𝑂 Func 𝑃 ) ) )
19	18	adantl	⊢ ( ( 𝜑 ∧ 𝑥 ∈ ( 𝐿 𝑀 𝐾 ) ) → ( 𝐿 ∈ ( 𝑂 Func 𝑃 ) ∧ 𝐾 ∈ ( 𝑂 Func 𝑃 ) ) )
20	19	simpld	⊢ ( ( 𝜑 ∧ 𝑥 ∈ ( 𝐿 𝑀 𝐾 ) ) → 𝐿 ∈ ( 𝑂 Func 𝑃 ) )
21	16 20	eqeltrrd	⊢ ( ( 𝜑 ∧ 𝑥 ∈ ( 𝐿 𝑀 𝐾 ) ) → ( oppFunc ‘ 𝐺 ) ∈ ( 𝑂 Func 𝑃 ) )
22		relfunc	⊢ Rel ( 𝑂 Func 𝑃 )
23		eqid	⊢ ( oppFunc ‘ 𝐺 ) = ( oppFunc ‘ 𝐺 )
24	21 22 23	2oppf	⊢ ( ( 𝜑 ∧ 𝑥 ∈ ( 𝐿 𝑀 𝐾 ) ) → ( oppFunc ‘ ( oppFunc ‘ 𝐺 ) ) = 𝐺 )
25	17 24	eqtr2d	⊢ ( ( 𝜑 ∧ 𝑥 ∈ ( 𝐿 𝑀 𝐾 ) ) → 𝐺 = ( oppFunc ‘ 𝐿 ) )
26	5	adantr	⊢ ( ( 𝜑 ∧ 𝑥 ∈ ( 𝐿 𝑀 𝐾 ) ) → 𝐾 = ( oppFunc ‘ 𝐹 ) )
27	26	fveq2d	⊢ ( ( 𝜑 ∧ 𝑥 ∈ ( 𝐿 𝑀 𝐾 ) ) → ( oppFunc ‘ 𝐾 ) = ( oppFunc ‘ ( oppFunc ‘ 𝐹 ) ) )
28	19	simprd	⊢ ( ( 𝜑 ∧ 𝑥 ∈ ( 𝐿 𝑀 𝐾 ) ) → 𝐾 ∈ ( 𝑂 Func 𝑃 ) )
29	26 28	eqeltrrd	⊢ ( ( 𝜑 ∧ 𝑥 ∈ ( 𝐿 𝑀 𝐾 ) ) → ( oppFunc ‘ 𝐹 ) ∈ ( 𝑂 Func 𝑃 ) )
30		eqid	⊢ ( oppFunc ‘ 𝐹 ) = ( oppFunc ‘ 𝐹 )
31	29 22 30	2oppf	⊢ ( ( 𝜑 ∧ 𝑥 ∈ ( 𝐿 𝑀 𝐾 ) ) → ( oppFunc ‘ ( oppFunc ‘ 𝐹 ) ) = 𝐹 )
32	27 31	eqtr2d	⊢ ( ( 𝜑 ∧ 𝑥 ∈ ( 𝐿 𝑀 𝐾 ) ) → 𝐹 = ( oppFunc ‘ 𝐾 ) )
33		simpr	⊢ ( ( 𝜑 ∧ 𝑥 ∈ ( 𝐿 𝑀 𝐾 ) ) → 𝑥 ∈ ( 𝐿 𝑀 𝐾 ) )
34	13 14 4 15 25 32 33	natoppf2	⊢ ( ( 𝜑 ∧ 𝑥 ∈ ( 𝐿 𝑀 𝐾 ) ) → 𝑥 ∈ ( 𝐹 ( ( oppCat ‘ 𝑂 ) Nat ( oppCat ‘ 𝑃 ) ) 𝐺 ) )
35	1	2oppchomf	⊢ ( Hom_f ‘ 𝐶 ) = ( Hom_f ‘ ( oppCat ‘ 𝑂 ) )
36	35	a1i	⊢ ( ( 𝜑 ∧ 𝑥 ∈ ( 𝐿 𝑀 𝐾 ) ) → ( Hom_f ‘ 𝐶 ) = ( Hom_f ‘ ( oppCat ‘ 𝑂 ) ) )
37	1	2oppccomf	⊢ ( comp_f ‘ 𝐶 ) = ( comp_f ‘ ( oppCat ‘ 𝑂 ) )
38	37	a1i	⊢ ( ( 𝜑 ∧ 𝑥 ∈ ( 𝐿 𝑀 𝐾 ) ) → ( comp_f ‘ 𝐶 ) = ( comp_f ‘ ( oppCat ‘ 𝑂 ) ) )
39	2	2oppchomf	⊢ ( Hom_f ‘ 𝐷 ) = ( Hom_f ‘ ( oppCat ‘ 𝑃 ) )
40	39	a1i	⊢ ( ( 𝜑 ∧ 𝑥 ∈ ( 𝐿 𝑀 𝐾 ) ) → ( Hom_f ‘ 𝐷 ) = ( Hom_f ‘ ( oppCat ‘ 𝑃 ) ) )
41	2	2oppccomf	⊢ ( comp_f ‘ 𝐷 ) = ( comp_f ‘ ( oppCat ‘ 𝑃 ) )
42	41	a1i	⊢ ( ( 𝜑 ∧ 𝑥 ∈ ( 𝐿 𝑀 𝐾 ) ) → ( comp_f ‘ 𝐷 ) = ( comp_f ‘ ( oppCat ‘ 𝑃 ) ) )
43	7	adantr	⊢ ( ( 𝜑 ∧ 𝑥 ∈ ( 𝐿 𝑀 𝐾 ) ) → 𝐶 ∈ 𝑉 )
44	8	adantr	⊢ ( ( 𝜑 ∧ 𝑥 ∈ ( 𝐿 𝑀 𝐾 ) ) → 𝐷 ∈ 𝑊 )
45	1 2 43 44 29	funcoppc5	⊢ ( ( 𝜑 ∧ 𝑥 ∈ ( 𝐿 𝑀 𝐾 ) ) → 𝐹 ∈ ( 𝐶 Func 𝐷 ) )
46	45	func1st2nd	⊢ ( ( 𝜑 ∧ 𝑥 ∈ ( 𝐿 𝑀 𝐾 ) ) → ( 1^st ‘ 𝐹 ) ( 𝐶 Func 𝐷 ) ( 2^nd ‘ 𝐹 ) )
47	46	funcrcl2	⊢ ( ( 𝜑 ∧ 𝑥 ∈ ( 𝐿 𝑀 𝐾 ) ) → 𝐶 ∈ Cat )
48	1	oppccat	⊢ ( 𝐶 ∈ Cat → 𝑂 ∈ Cat )
49	13	oppccat	⊢ ( 𝑂 ∈ Cat → ( oppCat ‘ 𝑂 ) ∈ Cat )
50	47 48 49	3syl	⊢ ( ( 𝜑 ∧ 𝑥 ∈ ( 𝐿 𝑀 𝐾 ) ) → ( oppCat ‘ 𝑂 ) ∈ Cat )
51	46	funcrcl3	⊢ ( ( 𝜑 ∧ 𝑥 ∈ ( 𝐿 𝑀 𝐾 ) ) → 𝐷 ∈ Cat )
52	2	oppccat	⊢ ( 𝐷 ∈ Cat → 𝑃 ∈ Cat )
53	14	oppccat	⊢ ( 𝑃 ∈ Cat → ( oppCat ‘ 𝑃 ) ∈ Cat )
54	51 52 53	3syl	⊢ ( ( 𝜑 ∧ 𝑥 ∈ ( 𝐿 𝑀 𝐾 ) ) → ( oppCat ‘ 𝑃 ) ∈ Cat )
55	36 38 40 42 47 50 51 54	natpropd	⊢ ( ( 𝜑 ∧ 𝑥 ∈ ( 𝐿 𝑀 𝐾 ) ) → ( 𝐶 Nat 𝐷 ) = ( ( oppCat ‘ 𝑂 ) Nat ( oppCat ‘ 𝑃 ) ) )
56	3 55	eqtrid	⊢ ( ( 𝜑 ∧ 𝑥 ∈ ( 𝐿 𝑀 𝐾 ) ) → 𝑁 = ( ( oppCat ‘ 𝑂 ) Nat ( oppCat ‘ 𝑃 ) ) )
57	56	oveqd	⊢ ( ( 𝜑 ∧ 𝑥 ∈ ( 𝐿 𝑀 𝐾 ) ) → ( 𝐹 𝑁 𝐺 ) = ( 𝐹 ( ( oppCat ‘ 𝑂 ) Nat ( oppCat ‘ 𝑃 ) ) 𝐺 ) )
58	34 57	eleqtrrd	⊢ ( ( 𝜑 ∧ 𝑥 ∈ ( 𝐿 𝑀 𝐾 ) ) → 𝑥 ∈ ( 𝐹 𝑁 𝐺 ) )
59	12 58	impbida	⊢ ( 𝜑 → ( 𝑥 ∈ ( 𝐹 𝑁 𝐺 ) ↔ 𝑥 ∈ ( 𝐿 𝑀 𝐾 ) ) )
60	59	eqrdv	⊢ ( 𝜑 → ( 𝐹 𝑁 𝐺 ) = ( 𝐿 𝑀 𝐾 ) )

Metamath Proof Explorer

Theorem natoppfb

Proof