natoppf

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

	Ref	Expression
Hypotheses	natoppf.o	$⊢ O = oppCat (C)$
	natoppf.p	$⊢ P = oppCat (D)$
	natoppf.n	$⊢ N = C Nat D$
	natoppf.m	$⊢ M = O Nat P$
	natoppf.a	$⊢ φ \to A \in (⟨F, G⟩ N ⟨K, L⟩)$
Assertion	natoppf	$⊢ φ \to A \in (⟨K, tpos L⟩ M ⟨F, tpos G⟩)$

Proof

Step	Hyp	Ref	Expression
1		natoppf.o	$⊢ O = oppCat (C)$
2		natoppf.p	$⊢ P = oppCat (D)$
3		natoppf.n	$⊢ N = C Nat D$
4		natoppf.m	$⊢ M = O Nat P$
5		natoppf.a	$⊢ φ \to A \in (⟨F, G⟩ N ⟨K, L⟩)$
6		eqid	$⊢ {Base}_{C} = {Base}_{C}$
7	1 6	oppcbas	$⊢ {Base}_{C} = {Base}_{O}$
8		eqid	$⊢ Hom (O) = Hom (O)$
9		eqid	$⊢ Hom (P) = Hom (P)$
10		eqid	$⊢ comp (P) = comp (P)$
11	3 5	natrcl3	$⊢ φ \to K (C Func D) L$
12	1 2 11	funcoppc	$⊢ φ \to K (O Func P) tpos L$
13	3 5	natrcl2	$⊢ φ \to F (C Func D) G$
14	1 2 13	funcoppc	$⊢ φ \to F (O Func P) tpos G$
15	3 5 6	natfn	$⊢ φ \to A Fn {Base}_{C}$
16	5	adantr	$⊢ (φ \land x \in {Base}_{C}) \to A \in (⟨F, G⟩ N ⟨K, L⟩)$
17		eqid	$⊢ Hom (D) = Hom (D)$
18		simpr	$⊢ (φ \land x \in {Base}_{C}) \to x \in {Base}_{C}$
19	3 16 6 17 18	natcl	$⊢ (φ \land x \in {Base}_{C}) \to A (x) \in (F (x) Hom (D) K (x))$
20	17 2	oppchom	$⊢ K (x) Hom (P) F (x) = F (x) Hom (D) K (x)$
21	19 20	eleqtrrdi	$⊢ (φ \land x \in {Base}_{C}) \to A (x) \in (K (x) Hom (P) F (x))$
22	5	ad2antrr	$⊢ ((φ \land (x \in {Base}_{C} \land y \in {Base}_{C})) \land m \in (x Hom (O) y)) \to A \in (⟨F, G⟩ N ⟨K, L⟩)$
23		eqid	$⊢ Hom (C) = Hom (C)$
24		eqid	$⊢ comp (D) = comp (D)$
25		simplrr	$⊢ ((φ \land (x \in {Base}_{C} \land y \in {Base}_{C})) \land m \in (x Hom (O) y)) \to y \in {Base}_{C}$
26		simplrl	$⊢ ((φ \land (x \in {Base}_{C} \land y \in {Base}_{C})) \land m \in (x Hom (O) y)) \to x \in {Base}_{C}$
27		simpr	$⊢ ((φ \land (x \in {Base}_{C} \land y \in {Base}_{C})) \land m \in (x Hom (O) y)) \to m \in (x Hom (O) y)$
28	23 1	oppchom	$⊢ x Hom (O) y = y Hom (C) x$
29	27 28	eleqtrdi	$⊢ ((φ \land (x \in {Base}_{C} \land y \in {Base}_{C})) \land m \in (x Hom (O) y)) \to m \in (y Hom (C) x)$
30	3 22 6 23 24 25 26 29	nati	$⊢ ((φ \land (x \in {Base}_{C} \land y \in {Base}_{C})) \land m \in (x Hom (O) y)) \to A (x) (⟨F (y), F (x)⟩ comp (D) K (x)) (y G x) (m) = (y L x) (m) (⟨F (y), K (y)⟩ comp (D) K (x)) A (y)$
31		eqid	$⊢ {Base}_{D} = {Base}_{D}$
32	6 31 11	funcf1	$⊢ φ \to K : {Base}_{C} ⟶ {Base}_{D}$
33	32	ad2antrr	$⊢ ((φ \land (x \in {Base}_{C} \land y \in {Base}_{C})) \land m \in (x Hom (O) y)) \to K : {Base}_{C} ⟶ {Base}_{D}$
34	33 26	ffvelcdmd	$⊢ ((φ \land (x \in {Base}_{C} \land y \in {Base}_{C})) \land m \in (x Hom (O) y)) \to K (x) \in {Base}_{D}$
35	6 31 13	funcf1	$⊢ φ \to F : {Base}_{C} ⟶ {Base}_{D}$
36	35	ad2antrr	$⊢ ((φ \land (x \in {Base}_{C} \land y \in {Base}_{C})) \land m \in (x Hom (O) y)) \to F : {Base}_{C} ⟶ {Base}_{D}$
37	36 26	ffvelcdmd	$⊢ ((φ \land (x \in {Base}_{C} \land y \in {Base}_{C})) \land m \in (x Hom (O) y)) \to F (x) \in {Base}_{D}$
38	36 25	ffvelcdmd	$⊢ ((φ \land (x \in {Base}_{C} \land y \in {Base}_{C})) \land m \in (x Hom (O) y)) \to F (y) \in {Base}_{D}$
39	31 24 2 34 37 38	oppcco	$⊢ ((φ \land (x \in {Base}_{C} \land y \in {Base}_{C})) \land m \in (x Hom (O) y)) \to (y G x) (m) (⟨K (x), F (x)⟩ comp (P) F (y)) A (x) = A (x) (⟨F (y), F (x)⟩ comp (D) K (x)) (y G x) (m)$
40	33 25	ffvelcdmd	$⊢ ((φ \land (x \in {Base}_{C} \land y \in {Base}_{C})) \land m \in (x Hom (O) y)) \to K (y) \in {Base}_{D}$
41	31 24 2 34 40 38	oppcco	$⊢ ((φ \land (x \in {Base}_{C} \land y \in {Base}_{C})) \land m \in (x Hom (O) y)) \to A (y) (⟨K (x), K (y)⟩ comp (P) F (y)) (y L x) (m) = (y L x) (m) (⟨F (y), K (y)⟩ comp (D) K (x)) A (y)$
42	30 39 41	3eqtr4rd	$⊢ ((φ \land (x \in {Base}_{C} \land y \in {Base}_{C})) \land m \in (x Hom (O) y)) \to A (y) (⟨K (x), K (y)⟩ comp (P) F (y)) (y L x) (m) = (y G x) (m) (⟨K (x), F (x)⟩ comp (P) F (y)) A (x)$
43		ovtpos	$⊢ x tpos L y = y L x$
44	43	fveq1i	$⊢ (x tpos L y) (m) = (y L x) (m)$
45	44	oveq2i	$⊢ A (y) (⟨K (x), K (y)⟩ comp (P) F (y)) (x tpos L y) (m) = A (y) (⟨K (x), K (y)⟩ comp (P) F (y)) (y L x) (m)$
46		ovtpos	$⊢ x tpos G y = y G x$
47	46	fveq1i	$⊢ (x tpos G y) (m) = (y G x) (m)$
48	47	oveq1i	$⊢ (x tpos G y) (m) (⟨K (x), F (x)⟩ comp (P) F (y)) A (x) = (y G x) (m) (⟨K (x), F (x)⟩ comp (P) F (y)) A (x)$
49	42 45 48	3eqtr4g	$⊢ ((φ \land (x \in {Base}_{C} \land y \in {Base}_{C})) \land m \in (x Hom (O) y)) \to A (y) (⟨K (x), K (y)⟩ comp (P) F (y)) (x tpos L y) (m) = (x tpos G y) (m) (⟨K (x), F (x)⟩ comp (P) F (y)) A (x)$
50	4 7 8 9 10 12 14 15 21 49	isnatd	$⊢ φ \to A \in (⟨K, tpos L⟩ M ⟨F, tpos G⟩)$

Metamath Proof Explorer

Theorem natoppf

Proof