oppfdiag1

Description: A constant functor for opposite categories is the opposite functor of the constant functor for original categories. (Contributed by Zhi Wang, 19-Nov-2025)

	Ref	Expression
Hypotheses	oppfdiag.o	$⊢ O = oppCat (C)$
	oppfdiag.p	$⊢ P = oppCat (D)$
	oppfdiag.l	$⊢ L = C Δ_{func} D$
	oppfdiag.c	$⊢ φ \to C \in Cat$
	oppfdiag.d	$⊢ φ \to D \in Cat$
	oppfdiag1.f	No typesetting found for \|- ( ph -> F = ( oppFunc \|` ( D Func C ) ) ) with typecode \|-
	oppfdiag1.a	$⊢ A = {Base}_{C}$
	oppfdiag1.x	$⊢ φ \to X \in A$
Assertion	oppfdiag1	$⊢ φ \to F (1^{st} (L) (X)) = 1^{st} (O Δ_{func} P) (X)$

Proof

Step	Hyp	Ref	Expression
1		oppfdiag.o	$⊢ O = oppCat (C)$
2		oppfdiag.p	$⊢ P = oppCat (D)$
3		oppfdiag.l	$⊢ L = C Δ_{func} D$
4		oppfdiag.c	$⊢ φ \to C \in Cat$
5		oppfdiag.d	$⊢ φ \to D \in Cat$
6		oppfdiag1.f	Could not format ( ph -> F = ( oppFunc \|` ( D Func C ) ) ) : No typesetting found for \|- ( ph -> F = ( oppFunc \|` ( D Func C ) ) ) with typecode \|-
7		oppfdiag1.a	$⊢ A = {Base}_{C}$
8		oppfdiag1.x	$⊢ φ \to X \in A$
9		eqid	$⊢ D FuncCat C = D FuncCat C$
10	9	fucbas	$⊢ D Func C = {Base}_{(D FuncCat C)}$
11	3 4 5 9	diagcl	$⊢ φ \to L \in (C Func (D FuncCat C))$
12	11	func1st2nd	$⊢ φ \to 1^{st} (L) (C Func (D FuncCat C)) 2^{nd} (L)$
13	7 10 12	funcf1	$⊢ φ \to 1^{st} (L) : A ⟶ D Func C$
14	13 8	ffvelcdmd	$⊢ φ \to 1^{st} (L) (X) \in (D Func C)$
15	6 14	opf11	$⊢ φ \to 1^{st} (F (1^{st} (L) (X))) = 1^{st} (1^{st} (L) (X))$
16		eqid	$⊢ {Base}_{D} = {Base}_{D}$
17	2 16	oppcbas	$⊢ {Base}_{D} = {Base}_{P}$
18	1 7	oppcbas	$⊢ A = {Base}_{O}$
19		eqid	$⊢ oppCat (D FuncCat C) = oppCat (D FuncCat C)$
20	1 19 11	oppfoppc2	Could not format ( ph -> ( oppFunc ` L ) e. ( O Func ( oppCat ` ( D FuncCat C ) ) ) ) : No typesetting found for \|- ( ph -> ( oppFunc ` L ) e. ( O Func ( oppCat ` ( D FuncCat C ) ) ) ) with typecode \|-
21		eqid	$⊢ P FuncCat O = P FuncCat O$
22		eqid	$⊢ D Nat C = D Nat C$
23		eqidd	$⊢ φ \to (m \in (D Func C), n \in (D Func C) ⟼ {I ↾}_{(n (D Nat C) m)}) = (m \in (D Func C), n \in (D Func C) ⟼ {I ↾}_{(n (D Nat C) m)})$
24	2 1 9 19 21 22 6 23 5 4	fucoppcfunc	$⊢ φ \to F (oppCat (D FuncCat C) Func (P FuncCat O)) (m \in (D Func C), n \in (D Func C) ⟼ {I ↾}_{(n (D Nat C) m)})$
25		df-br	$⊢ F (oppCat (D FuncCat C) Func (P FuncCat O)) (m \in (D Func C), n \in (D Func C) ⟼ {I ↾}_{(n (D Nat C) m)}) \leftrightarrow ⟨F, (m \in (D Func C), n \in (D Func C) ⟼ {I ↾}_{(n (D Nat C) m)})⟩ \in (oppCat (D FuncCat C) Func (P FuncCat O))$
26	24 25	sylib	$⊢ φ \to ⟨F, (m \in (D Func C), n \in (D Func C) ⟼ {I ↾}_{(n (D Nat C) m)})⟩ \in (oppCat (D FuncCat C) Func (P FuncCat O))$
27	18 20 26 8	cofu1	Could not format ( ph -> ( ( 1st ` ( <. F , ( m e. ( D Func C ) , n e. ( D Func C ) \|-> ( _I \|` ( n ( D Nat C ) m ) ) ) >. o.func ( oppFunc ` L ) ) ) ` X ) = ( ( 1st ` <. F , ( m e. ( D Func C ) , n e. ( D Func C ) \|-> ( _I \|` ( n ( D Nat C ) m ) ) ) >. ) ` ( ( 1st ` ( oppFunc ` L ) ) ` X ) ) ) : No typesetting found for \|- ( ph -> ( ( 1st ` ( <. F , ( m e. ( D Func C ) , n e. ( D Func C ) \|-> ( _I \|` ( n ( D Nat C ) m ) ) ) >. o.func ( oppFunc ` L ) ) ) ` X ) = ( ( 1st ` <. F , ( m e. ( D Func C ) , n e. ( D Func C ) \|-> ( _I \|` ( n ( D Nat C ) m ) ) ) >. ) ` ( ( 1st ` ( oppFunc ` L ) ) ` X ) ) ) with typecode \|-
28	24	func1st	$⊢ φ \to 1^{st} (⟨F, (m \in (D Func C), n \in (D Func C) ⟼ {I ↾}_{(n (D Nat C) m)})⟩) = F$
29	11	oppf1	Could not format ( ph -> ( 1st ` ( oppFunc ` L ) ) = ( 1st ` L ) ) : No typesetting found for \|- ( ph -> ( 1st ` ( oppFunc ` L ) ) = ( 1st ` L ) ) with typecode \|-
30	29	fveq1d	Could not format ( ph -> ( ( 1st ` ( oppFunc ` L ) ) ` X ) = ( ( 1st ` L ) ` X ) ) : No typesetting found for \|- ( ph -> ( ( 1st ` ( oppFunc ` L ) ) ` X ) = ( ( 1st ` L ) ` X ) ) with typecode \|-
31	28 30	fveq12d	Could not format ( ph -> ( ( 1st ` <. F , ( m e. ( D Func C ) , n e. ( D Func C ) \|-> ( _I \|` ( n ( D Nat C ) m ) ) ) >. ) ` ( ( 1st ` ( oppFunc ` L ) ) ` X ) ) = ( F ` ( ( 1st ` L ) ` X ) ) ) : No typesetting found for \|- ( ph -> ( ( 1st ` <. F , ( m e. ( D Func C ) , n e. ( D Func C ) \|-> ( _I \|` ( n ( D Nat C ) m ) ) ) >. ) ` ( ( 1st ` ( oppFunc ` L ) ) ` X ) ) = ( F ` ( ( 1st ` L ) ` X ) ) ) with typecode \|-
32	27 31	eqtrd	Could not format ( ph -> ( ( 1st ` ( <. F , ( m e. ( D Func C ) , n e. ( D Func C ) \|-> ( _I \|` ( n ( D Nat C ) m ) ) ) >. o.func ( oppFunc ` L ) ) ) ` X ) = ( F ` ( ( 1st ` L ) ` X ) ) ) : No typesetting found for \|- ( ph -> ( ( 1st ` ( <. F , ( m e. ( D Func C ) , n e. ( D Func C ) \|-> ( _I \|` ( n ( D Nat C ) m ) ) ) >. o.func ( oppFunc ` L ) ) ) ` X ) = ( F ` ( ( 1st ` L ) ` X ) ) ) with typecode \|-
33	21	fucbas	$⊢ P Func O = {Base}_{(P FuncCat O)}$
34	20 26	cofucl	Could not format ( ph -> ( <. F , ( m e. ( D Func C ) , n e. ( D Func C ) \|-> ( _I \|` ( n ( D Nat C ) m ) ) ) >. o.func ( oppFunc ` L ) ) e. ( O Func ( P FuncCat O ) ) ) : No typesetting found for \|- ( ph -> ( <. F , ( m e. ( D Func C ) , n e. ( D Func C ) \|-> ( _I \|` ( n ( D Nat C ) m ) ) ) >. o.func ( oppFunc ` L ) ) e. ( O Func ( P FuncCat O ) ) ) with typecode \|-
35	34	func1st2nd	Could not format ( ph -> ( 1st ` ( <. F , ( m e. ( D Func C ) , n e. ( D Func C ) \|-> ( _I \|` ( n ( D Nat C ) m ) ) ) >. o.func ( oppFunc ` L ) ) ) ( O Func ( P FuncCat O ) ) ( 2nd ` ( <. F , ( m e. ( D Func C ) , n e. ( D Func C ) \|-> ( _I \|` ( n ( D Nat C ) m ) ) ) >. o.func ( oppFunc ` L ) ) ) ) : No typesetting found for \|- ( ph -> ( 1st ` ( <. F , ( m e. ( D Func C ) , n e. ( D Func C ) \|-> ( _I \|` ( n ( D Nat C ) m ) ) ) >. o.func ( oppFunc ` L ) ) ) ( O Func ( P FuncCat O ) ) ( 2nd ` ( <. F , ( m e. ( D Func C ) , n e. ( D Func C ) \|-> ( _I \|` ( n ( D Nat C ) m ) ) ) >. o.func ( oppFunc ` L ) ) ) ) with typecode \|-
36	18 33 35	funcf1	Could not format ( ph -> ( 1st ` ( <. F , ( m e. ( D Func C ) , n e. ( D Func C ) \|-> ( _I \|` ( n ( D Nat C ) m ) ) ) >. o.func ( oppFunc ` L ) ) ) : A --> ( P Func O ) ) : No typesetting found for \|- ( ph -> ( 1st ` ( <. F , ( m e. ( D Func C ) , n e. ( D Func C ) \|-> ( _I \|` ( n ( D Nat C ) m ) ) ) >. o.func ( oppFunc ` L ) ) ) : A --> ( P Func O ) ) with typecode \|-
37	36 8	ffvelcdmd	Could not format ( ph -> ( ( 1st ` ( <. F , ( m e. ( D Func C ) , n e. ( D Func C ) \|-> ( _I \|` ( n ( D Nat C ) m ) ) ) >. o.func ( oppFunc ` L ) ) ) ` X ) e. ( P Func O ) ) : No typesetting found for \|- ( ph -> ( ( 1st ` ( <. F , ( m e. ( D Func C ) , n e. ( D Func C ) \|-> ( _I \|` ( n ( D Nat C ) m ) ) ) >. o.func ( oppFunc ` L ) ) ) ` X ) e. ( P Func O ) ) with typecode \|-
38	32 37	eqeltrrd	$⊢ φ \to F (1^{st} (L) (X)) \in (P Func O)$
39	38	func1st2nd	$⊢ φ \to 1^{st} (F (1^{st} (L) (X))) (P Func O) 2^{nd} (F (1^{st} (L) (X)))$
40	17 18 39	funcf1	$⊢ φ \to 1^{st} (F (1^{st} (L) (X))) : {Base}_{D} ⟶ A$
41	15 40	feq1dd	$⊢ φ \to 1^{st} (1^{st} (L) (X)) : {Base}_{D} ⟶ A$
42	41	ffnd	$⊢ φ \to 1^{st} (1^{st} (L) (X)) Fn {Base}_{D}$
43		eqid	$⊢ O Δ_{func} P = O Δ_{func} P$
44	1	oppccat	$⊢ C \in Cat \to O \in Cat$
45	4 44	syl	$⊢ φ \to O \in Cat$
46	2	oppccat	$⊢ D \in Cat \to P \in Cat$
47	5 46	syl	$⊢ φ \to P \in Cat$
48	43 45 47 21	diagcl	$⊢ φ \to O Δ_{func} P \in (O Func (P FuncCat O))$
49	48	func1st2nd	$⊢ φ \to 1^{st} (O Δ_{func} P) (O Func (P FuncCat O)) 2^{nd} (O Δ_{func} P)$
50	18 33 49	funcf1	$⊢ φ \to 1^{st} (O Δ_{func} P) : A ⟶ P Func O$
51	50 8	ffvelcdmd	$⊢ φ \to 1^{st} (O Δ_{func} P) (X) \in (P Func O)$
52	51	func1st2nd	$⊢ φ \to 1^{st} (1^{st} (O Δ_{func} P) (X)) (P Func O) 2^{nd} (1^{st} (O Δ_{func} P) (X))$
53	17 18 52	funcf1	$⊢ φ \to 1^{st} (1^{st} (O Δ_{func} P) (X)) : {Base}_{D} ⟶ A$
54	53	ffnd	$⊢ φ \to 1^{st} (1^{st} (O Δ_{func} P) (X)) Fn {Base}_{D}$
55	4	adantr	$⊢ (φ \land y \in {Base}_{D}) \to C \in Cat$
56	5	adantr	$⊢ (φ \land y \in {Base}_{D}) \to D \in Cat$
57	8	adantr	$⊢ (φ \land y \in {Base}_{D}) \to X \in A$
58		eqid	$⊢ 1^{st} (L) (X) = 1^{st} (L) (X)$
59		simpr	$⊢ (φ \land y \in {Base}_{D}) \to y \in {Base}_{D}$
60	3 55 56 7 57 58 16 59	diag11	$⊢ (φ \land y \in {Base}_{D}) \to 1^{st} (1^{st} (L) (X)) (y) = X$
61	45	adantr	$⊢ (φ \land y \in {Base}_{D}) \to O \in Cat$
62	47	adantr	$⊢ (φ \land y \in {Base}_{D}) \to P \in Cat$
63		eqid	$⊢ 1^{st} (O Δ_{func} P) (X) = 1^{st} (O Δ_{func} P) (X)$
64	43 61 62 18 57 63 17 59	diag11	$⊢ (φ \land y \in {Base}_{D}) \to 1^{st} (1^{st} (O Δ_{func} P) (X)) (y) = X$
65	60 64	eqtr4d	$⊢ (φ \land y \in {Base}_{D}) \to 1^{st} (1^{st} (L) (X)) (y) = 1^{st} (1^{st} (O Δ_{func} P) (X)) (y)$
66	42 54 65	eqfnfvd	$⊢ φ \to 1^{st} (1^{st} (L) (X)) = 1^{st} (1^{st} (O Δ_{func} P) (X))$
67	15 66	eqtrd	$⊢ φ \to 1^{st} (F (1^{st} (L) (X))) = 1^{st} (1^{st} (O Δ_{func} P) (X))$
68	17 39	funcfn2	$⊢ φ \to 2^{nd} (F (1^{st} (L) (X))) Fn ({Base}_{D} \times {Base}_{D})$
69	17 52	funcfn2	$⊢ φ \to 2^{nd} (1^{st} (O Δ_{func} P) (X)) Fn ({Base}_{D} \times {Base}_{D})$
70	6 14	opf12	$⊢ φ \to y 2^{nd} (F (1^{st} (L) (X))) z = z 2^{nd} (1^{st} (L) (X)) y$
71	70	adantr	$⊢ (φ \land (y \in {Base}_{D} \land z \in {Base}_{D})) \to y 2^{nd} (F (1^{st} (L) (X))) z = z 2^{nd} (1^{st} (L) (X)) y$
72		eqid	$⊢ Hom (D) = Hom (D)$
73	72 2	oppchom	$⊢ y Hom (P) z = z Hom (D) y$
74	73	a1i	$⊢ (φ \land (y \in {Base}_{D} \land z \in {Base}_{D})) \to y Hom (P) z = z Hom (D) y$
75		eqid	$⊢ Hom (P) = Hom (P)$
76		eqid	$⊢ Hom (O) = Hom (O)$
77	39	adantr	$⊢ (φ \land (y \in {Base}_{D} \land z \in {Base}_{D})) \to 1^{st} (F (1^{st} (L) (X))) (P Func O) 2^{nd} (F (1^{st} (L) (X)))$
78		simprl	$⊢ (φ \land (y \in {Base}_{D} \land z \in {Base}_{D})) \to y \in {Base}_{D}$
79		simprr	$⊢ (φ \land (y \in {Base}_{D} \land z \in {Base}_{D})) \to z \in {Base}_{D}$
80	17 75 76 77 78 79	funcf2	$⊢ (φ \land (y \in {Base}_{D} \land z \in {Base}_{D})) \to (y 2^{nd} (F (1^{st} (L) (X))) z) : y Hom (P) z ⟶ 1^{st} (F (1^{st} (L) (X))) (y) Hom (O) 1^{st} (F (1^{st} (L) (X))) (z)$
81	74 80	feq2dd	$⊢ (φ \land (y \in {Base}_{D} \land z \in {Base}_{D})) \to (y 2^{nd} (F (1^{st} (L) (X))) z) : z Hom (D) y ⟶ 1^{st} (F (1^{st} (L) (X))) (y) Hom (O) 1^{st} (F (1^{st} (L) (X))) (z)$
82	71 81	feq1dd	$⊢ (φ \land (y \in {Base}_{D} \land z \in {Base}_{D})) \to (z 2^{nd} (1^{st} (L) (X)) y) : z Hom (D) y ⟶ 1^{st} (F (1^{st} (L) (X))) (y) Hom (O) 1^{st} (F (1^{st} (L) (X))) (z)$
83	82	ffnd	$⊢ (φ \land (y \in {Base}_{D} \land z \in {Base}_{D})) \to (z 2^{nd} (1^{st} (L) (X)) y) Fn (z Hom (D) y)$
84	52	adantr	$⊢ (φ \land (y \in {Base}_{D} \land z \in {Base}_{D})) \to 1^{st} (1^{st} (O Δ_{func} P) (X)) (P Func O) 2^{nd} (1^{st} (O Δ_{func} P) (X))$
85	17 75 76 84 78 79	funcf2	$⊢ (φ \land (y \in {Base}_{D} \land z \in {Base}_{D})) \to (y 2^{nd} (1^{st} (O Δ_{func} P) (X)) z) : y Hom (P) z ⟶ 1^{st} (1^{st} (O Δ_{func} P) (X)) (y) Hom (O) 1^{st} (1^{st} (O Δ_{func} P) (X)) (z)$
86	74 85	feq2dd	$⊢ (φ \land (y \in {Base}_{D} \land z \in {Base}_{D})) \to (y 2^{nd} (1^{st} (O Δ_{func} P) (X)) z) : z Hom (D) y ⟶ 1^{st} (1^{st} (O Δ_{func} P) (X)) (y) Hom (O) 1^{st} (1^{st} (O Δ_{func} P) (X)) (z)$
87	86	ffnd	$⊢ (φ \land (y \in {Base}_{D} \land z \in {Base}_{D})) \to (y 2^{nd} (1^{st} (O Δ_{func} P) (X)) z) Fn (z Hom (D) y)$
88		eqid	$⊢ Id (C) = Id (C)$
89	1 88	oppcid	$⊢ C \in Cat \to Id (O) = Id (C)$
90	4 89	syl	$⊢ φ \to Id (O) = Id (C)$
91	90	fveq1d	$⊢ φ \to Id (O) (X) = Id (C) (X)$
92	91	ad2antrr	$⊢ ((φ \land (y \in {Base}_{D} \land z \in {Base}_{D})) \land f \in (z Hom (D) y)) \to Id (O) (X) = Id (C) (X)$
93	4	ad2antrr	$⊢ ((φ \land (y \in {Base}_{D} \land z \in {Base}_{D})) \land f \in (z Hom (D) y)) \to C \in Cat$
94	93 44	syl	$⊢ ((φ \land (y \in {Base}_{D} \land z \in {Base}_{D})) \land f \in (z Hom (D) y)) \to O \in Cat$
95	5	ad2antrr	$⊢ ((φ \land (y \in {Base}_{D} \land z \in {Base}_{D})) \land f \in (z Hom (D) y)) \to D \in Cat$
96	95 46	syl	$⊢ ((φ \land (y \in {Base}_{D} \land z \in {Base}_{D})) \land f \in (z Hom (D) y)) \to P \in Cat$
97	8	ad2antrr	$⊢ ((φ \land (y \in {Base}_{D} \land z \in {Base}_{D})) \land f \in (z Hom (D) y)) \to X \in A$
98	78	adantr	$⊢ ((φ \land (y \in {Base}_{D} \land z \in {Base}_{D})) \land f \in (z Hom (D) y)) \to y \in {Base}_{D}$
99		eqid	$⊢ Id (O) = Id (O)$
100	79	adantr	$⊢ ((φ \land (y \in {Base}_{D} \land z \in {Base}_{D})) \land f \in (z Hom (D) y)) \to z \in {Base}_{D}$
101		simpr	$⊢ ((φ \land (y \in {Base}_{D} \land z \in {Base}_{D})) \land f \in (z Hom (D) y)) \to f \in (z Hom (D) y)$
102	101 73	eleqtrrdi	$⊢ ((φ \land (y \in {Base}_{D} \land z \in {Base}_{D})) \land f \in (z Hom (D) y)) \to f \in (y Hom (P) z)$
103	43 94 96 18 97 63 17 98 75 99 100 102	diag12	$⊢ ((φ \land (y \in {Base}_{D} \land z \in {Base}_{D})) \land f \in (z Hom (D) y)) \to (y 2^{nd} (1^{st} (O Δ_{func} P) (X)) z) (f) = Id (O) (X)$
104	3 93 95 7 97 58 16 100 72 88 98 101	diag12	$⊢ ((φ \land (y \in {Base}_{D} \land z \in {Base}_{D})) \land f \in (z Hom (D) y)) \to (z 2^{nd} (1^{st} (L) (X)) y) (f) = Id (C) (X)$
105	92 103 104	3eqtr4rd	$⊢ ((φ \land (y \in {Base}_{D} \land z \in {Base}_{D})) \land f \in (z Hom (D) y)) \to (z 2^{nd} (1^{st} (L) (X)) y) (f) = (y 2^{nd} (1^{st} (O Δ_{func} P) (X)) z) (f)$
106	83 87 105	eqfnfvd	$⊢ (φ \land (y \in {Base}_{D} \land z \in {Base}_{D})) \to z 2^{nd} (1^{st} (L) (X)) y = y 2^{nd} (1^{st} (O Δ_{func} P) (X)) z$
107	71 106	eqtrd	$⊢ (φ \land (y \in {Base}_{D} \land z \in {Base}_{D})) \to y 2^{nd} (F (1^{st} (L) (X))) z = y 2^{nd} (1^{st} (O Δ_{func} P) (X)) z$
108	68 69 107	eqfnovd	$⊢ φ \to 2^{nd} (F (1^{st} (L) (X))) = 2^{nd} (1^{st} (O Δ_{func} P) (X))$
109	67 108	opeq12d	$⊢ φ \to ⟨1^{st} (F (1^{st} (L) (X))), 2^{nd} (F (1^{st} (L) (X)))⟩ = ⟨1^{st} (1^{st} (O Δ_{func} P) (X)), 2^{nd} (1^{st} (O Δ_{func} P) (X))⟩$
110		relfunc	$⊢ Rel (P Func O)$
111		1st2nd	$⊢ (Rel (P Func O) \land F (1^{st} (L) (X)) \in (P Func O)) \to F (1^{st} (L) (X)) = ⟨1^{st} (F (1^{st} (L) (X))), 2^{nd} (F (1^{st} (L) (X)))⟩$
112	110 38 111	sylancr	$⊢ φ \to F (1^{st} (L) (X)) = ⟨1^{st} (F (1^{st} (L) (X))), 2^{nd} (F (1^{st} (L) (X)))⟩$
113		1st2nd	$⊢ (Rel (P Func O) \land 1^{st} (O Δ_{func} P) (X) \in (P Func O)) \to 1^{st} (O Δ_{func} P) (X) = ⟨1^{st} (1^{st} (O Δ_{func} P) (X)), 2^{nd} (1^{st} (O Δ_{func} P) (X))⟩$
114	110 51 113	sylancr	$⊢ φ \to 1^{st} (O Δ_{func} P) (X) = ⟨1^{st} (1^{st} (O Δ_{func} P) (X)), 2^{nd} (1^{st} (O Δ_{func} P) (X))⟩$
115	109 112 114	3eqtr4d	$⊢ φ \to F (1^{st} (L) (X)) = 1^{st} (O Δ_{func} P) (X)$

Metamath Proof Explorer

Theorem oppfdiag1

Proof