funcoppc

Description: A functor on categories yields a functor on the opposite categories (in the same direction), see definition 3.41 of Adamek p. 39. (Contributed by Mario Carneiro, 4-Jan-2017)

	Ref	Expression
Hypotheses	funcoppc.o	$⊢ O = oppCat (C)$
	funcoppc.p	$⊢ P = oppCat (D)$
	funcoppc.f	$⊢ φ \to F (C Func D) G$
Assertion	funcoppc	$⊢ φ \to F (O Func P) tpos G$

Proof

Step	Hyp	Ref	Expression
1		funcoppc.o	$⊢ O = oppCat (C)$
2		funcoppc.p	$⊢ P = oppCat (D)$
3		funcoppc.f	$⊢ φ \to F (C Func D) G$
4		eqid	$⊢ {Base}_{C} = {Base}_{C}$
5	1 4	oppcbas	$⊢ {Base}_{C} = {Base}_{O}$
6		eqid	$⊢ {Base}_{D} = {Base}_{D}$
7	2 6	oppcbas	$⊢ {Base}_{D} = {Base}_{P}$
8		eqid	$⊢ Hom (O) = Hom (O)$
9		eqid	$⊢ Hom (P) = Hom (P)$
10		eqid	$⊢ Id (O) = Id (O)$
11		eqid	$⊢ Id (P) = Id (P)$
12		eqid	$⊢ comp (O) = comp (O)$
13		eqid	$⊢ comp (P) = comp (P)$
14		df-br	$⊢ F (C Func D) G \leftrightarrow ⟨F, G⟩ \in (C Func D)$
15	3 14	sylib	$⊢ φ \to ⟨F, G⟩ \in (C Func D)$
16		funcrcl	$⊢ ⟨F, G⟩ \in (C Func D) \to (C \in Cat \land D \in Cat)$
17	15 16	syl	$⊢ φ \to (C \in Cat \land D \in Cat)$
18	17	simpld	$⊢ φ \to C \in Cat$
19	1	oppccat	$⊢ C \in Cat \to O \in Cat$
20	18 19	syl	$⊢ φ \to O \in Cat$
21	2	oppccat	$⊢ D \in Cat \to P \in Cat$
22	17 21	simpl2im	$⊢ φ \to P \in Cat$
23	4 6 3	funcf1	$⊢ φ \to F : {Base}_{C} ⟶ {Base}_{D}$
24	4 3	funcfn2	$⊢ φ \to G Fn ({Base}_{C} \times {Base}_{C})$
25		tposfn	$⊢ G Fn ({Base}_{C} \times {Base}_{C}) \to tpos G Fn ({Base}_{C} \times {Base}_{C})$
26	24 25	syl	$⊢ φ \to tpos G Fn ({Base}_{C} \times {Base}_{C})$
27		eqid	$⊢ Hom (C) = Hom (C)$
28		eqid	$⊢ Hom (D) = Hom (D)$
29	3	adantr	$⊢ (φ \land (x \in {Base}_{C} \land y \in {Base}_{C})) \to F (C Func D) G$
30		simprr	$⊢ (φ \land (x \in {Base}_{C} \land y \in {Base}_{C})) \to y \in {Base}_{C}$
31		simprl	$⊢ (φ \land (x \in {Base}_{C} \land y \in {Base}_{C})) \to x \in {Base}_{C}$
32	4 27 28 29 30 31	funcf2	$⊢ (φ \land (x \in {Base}_{C} \land y \in {Base}_{C})) \to (y G x) : y Hom (C) x ⟶ F (y) Hom (D) F (x)$
33		ovtpos	$⊢ x tpos G y = y G x$
34	33	feq1i	$⊢ (x tpos G y) : x Hom (O) y ⟶ F (x) Hom (P) F (y) \leftrightarrow (y G x) : x Hom (O) y ⟶ F (x) Hom (P) F (y)$
35	27 1	oppchom	$⊢ x Hom (O) y = y Hom (C) x$
36	28 2	oppchom	$⊢ F (x) Hom (P) F (y) = F (y) Hom (D) F (x)$
37	35 36	feq23i	$⊢ (y G x) : x Hom (O) y ⟶ F (x) Hom (P) F (y) \leftrightarrow (y G x) : y Hom (C) x ⟶ F (y) Hom (D) F (x)$
38	34 37	bitri	$⊢ (x tpos G y) : x Hom (O) y ⟶ F (x) Hom (P) F (y) \leftrightarrow (y G x) : y Hom (C) x ⟶ F (y) Hom (D) F (x)$
39	32 38	sylibr	$⊢ (φ \land (x \in {Base}_{C} \land y \in {Base}_{C})) \to (x tpos G y) : x Hom (O) y ⟶ F (x) Hom (P) F (y)$
40		eqid	$⊢ Id (C) = Id (C)$
41		eqid	$⊢ Id (D) = Id (D)$
42	3	adantr	$⊢ (φ \land x \in {Base}_{C}) \to F (C Func D) G$
43		simpr	$⊢ (φ \land x \in {Base}_{C}) \to x \in {Base}_{C}$
44	4 40 41 42 43	funcid	$⊢ (φ \land x \in {Base}_{C}) \to (x G x) (Id (C) (x)) = Id (D) (F (x))$
45		ovtpos	$⊢ x tpos G x = x G x$
46	45	a1i	$⊢ (φ \land x \in {Base}_{C}) \to x tpos G x = x G x$
47	1 40	oppcid	$⊢ C \in Cat \to Id (O) = Id (C)$
48	18 47	syl	$⊢ φ \to Id (O) = Id (C)$
49	48	adantr	$⊢ (φ \land x \in {Base}_{C}) \to Id (O) = Id (C)$
50	49	fveq1d	$⊢ (φ \land x \in {Base}_{C}) \to Id (O) (x) = Id (C) (x)$
51	46 50	fveq12d	$⊢ (φ \land x \in {Base}_{C}) \to (x tpos G x) (Id (O) (x)) = (x G x) (Id (C) (x))$
52	2 41	oppcid	$⊢ D \in Cat \to Id (P) = Id (D)$
53	17 52	simpl2im	$⊢ φ \to Id (P) = Id (D)$
54	53	adantr	$⊢ (φ \land x \in {Base}_{C}) \to Id (P) = Id (D)$
55	54	fveq1d	$⊢ (φ \land x \in {Base}_{C}) \to Id (P) (F (x)) = Id (D) (F (x))$
56	44 51 55	3eqtr4d	$⊢ (φ \land x \in {Base}_{C}) \to (x tpos G x) (Id (O) (x)) = Id (P) (F (x))$
57		eqid	$⊢ comp (C) = comp (C)$
58		eqid	$⊢ comp (D) = comp (D)$
59	3	3ad2ant1	$⊢ (φ \land (x \in {Base}_{C} \land y \in {Base}_{C} \land z \in {Base}_{C}) \land (f \in (x Hom (O) y) \land g \in (y Hom (O) z))) \to F (C Func D) G$
60		simp23	$⊢ (φ \land (x \in {Base}_{C} \land y \in {Base}_{C} \land z \in {Base}_{C}) \land (f \in (x Hom (O) y) \land g \in (y Hom (O) z))) \to z \in {Base}_{C}$
61		simp22	$⊢ (φ \land (x \in {Base}_{C} \land y \in {Base}_{C} \land z \in {Base}_{C}) \land (f \in (x Hom (O) y) \land g \in (y Hom (O) z))) \to y \in {Base}_{C}$
62		simp21	$⊢ (φ \land (x \in {Base}_{C} \land y \in {Base}_{C} \land z \in {Base}_{C}) \land (f \in (x Hom (O) y) \land g \in (y Hom (O) z))) \to x \in {Base}_{C}$
63		simp3r	$⊢ (φ \land (x \in {Base}_{C} \land y \in {Base}_{C} \land z \in {Base}_{C}) \land (f \in (x Hom (O) y) \land g \in (y Hom (O) z))) \to g \in (y Hom (O) z)$
64	27 1	oppchom	$⊢ y Hom (O) z = z Hom (C) y$
65	63 64	eleqtrdi	$⊢ (φ \land (x \in {Base}_{C} \land y \in {Base}_{C} \land z \in {Base}_{C}) \land (f \in (x Hom (O) y) \land g \in (y Hom (O) z))) \to g \in (z Hom (C) y)$
66		simp3l	$⊢ (φ \land (x \in {Base}_{C} \land y \in {Base}_{C} \land z \in {Base}_{C}) \land (f \in (x Hom (O) y) \land g \in (y Hom (O) z))) \to f \in (x Hom (O) y)$
67	66 35	eleqtrdi	$⊢ (φ \land (x \in {Base}_{C} \land y \in {Base}_{C} \land z \in {Base}_{C}) \land (f \in (x Hom (O) y) \land g \in (y Hom (O) z))) \to f \in (y Hom (C) x)$
68	4 27 57 58 59 60 61 62 65 67	funcco	$⊢ (φ \land (x \in {Base}_{C} \land y \in {Base}_{C} \land z \in {Base}_{C}) \land (f \in (x Hom (O) y) \land g \in (y Hom (O) z))) \to (z G x) (f (⟨z, y⟩ comp (C) x) g) = (y G x) (f) (⟨F (z), F (y)⟩ comp (D) F (x)) (z G y) (g)$
69	4 57 1 62 61 60	oppcco	$⊢ (φ \land (x \in {Base}_{C} \land y \in {Base}_{C} \land z \in {Base}_{C}) \land (f \in (x Hom (O) y) \land g \in (y Hom (O) z))) \to g (⟨x, y⟩ comp (O) z) f = f (⟨z, y⟩ comp (C) x) g$
70	69	fveq2d	$⊢ (φ \land (x \in {Base}_{C} \land y \in {Base}_{C} \land z \in {Base}_{C}) \land (f \in (x Hom (O) y) \land g \in (y Hom (O) z))) \to (z G x) (g (⟨x, y⟩ comp (O) z) f) = (z G x) (f (⟨z, y⟩ comp (C) x) g)$
71	23	3ad2ant1	$⊢ (φ \land (x \in {Base}_{C} \land y \in {Base}_{C} \land z \in {Base}_{C}) \land (f \in (x Hom (O) y) \land g \in (y Hom (O) z))) \to F : {Base}_{C} ⟶ {Base}_{D}$
72	71 62	ffvelcdmd	$⊢ (φ \land (x \in {Base}_{C} \land y \in {Base}_{C} \land z \in {Base}_{C}) \land (f \in (x Hom (O) y) \land g \in (y Hom (O) z))) \to F (x) \in {Base}_{D}$
73	71 61	ffvelcdmd	$⊢ (φ \land (x \in {Base}_{C} \land y \in {Base}_{C} \land z \in {Base}_{C}) \land (f \in (x Hom (O) y) \land g \in (y Hom (O) z))) \to F (y) \in {Base}_{D}$
74	71 60	ffvelcdmd	$⊢ (φ \land (x \in {Base}_{C} \land y \in {Base}_{C} \land z \in {Base}_{C}) \land (f \in (x Hom (O) y) \land g \in (y Hom (O) z))) \to F (z) \in {Base}_{D}$
75	6 58 2 72 73 74	oppcco	$⊢ (φ \land (x \in {Base}_{C} \land y \in {Base}_{C} \land z \in {Base}_{C}) \land (f \in (x Hom (O) y) \land g \in (y Hom (O) z))) \to (z G y) (g) (⟨F (x), F (y)⟩ comp (P) F (z)) (y G x) (f) = (y G x) (f) (⟨F (z), F (y)⟩ comp (D) F (x)) (z G y) (g)$
76	68 70 75	3eqtr4d	$⊢ (φ \land (x \in {Base}_{C} \land y \in {Base}_{C} \land z \in {Base}_{C}) \land (f \in (x Hom (O) y) \land g \in (y Hom (O) z))) \to (z G x) (g (⟨x, y⟩ comp (O) z) f) = (z G y) (g) (⟨F (x), F (y)⟩ comp (P) F (z)) (y G x) (f)$
77		ovtpos	$⊢ x tpos G z = z G x$
78	77	fveq1i	$⊢ (x tpos G z) (g (⟨x, y⟩ comp (O) z) f) = (z G x) (g (⟨x, y⟩ comp (O) z) f)$
79		ovtpos	$⊢ y tpos G z = z G y$
80	79	fveq1i	$⊢ (y tpos G z) (g) = (z G y) (g)$
81	33	fveq1i	$⊢ (x tpos G y) (f) = (y G x) (f)$
82	80 81	oveq12i	$⊢ (y tpos G z) (g) (⟨F (x), F (y)⟩ comp (P) F (z)) (x tpos G y) (f) = (z G y) (g) (⟨F (x), F (y)⟩ comp (P) F (z)) (y G x) (f)$
83	76 78 82	3eqtr4g	$⊢ (φ \land (x \in {Base}_{C} \land y \in {Base}_{C} \land z \in {Base}_{C}) \land (f \in (x Hom (O) y) \land g \in (y Hom (O) z))) \to (x tpos G z) (g (⟨x, y⟩ comp (O) z) f) = (y tpos G z) (g) (⟨F (x), F (y)⟩ comp (P) F (z)) (x tpos G y) (f)$
84	5 7 8 9 10 11 12 13 20 22 23 26 39 56 83	isfuncd	$⊢ φ \to F (O Func P) tpos G$

Metamath Proof Explorer

Theorem funcoppc

Proof