Theorem oppfdiag

Description: A diagonal functor for opposite categories is the opposite functor of the diagonal functor for original categories post-composed by an isomorphism ( fucoppc ). (Contributed by Zhi Wang, 19-Nov-2025)

	Ref	Expression
Hypotheses	oppfdiag.o	$$⊢O=\mathrm{oppCat}\left(C\right)$$
	oppfdiag.p	$$⊢P=\mathrm{oppCat}\left(D\right)$$
	oppfdiag.l	$$⊢L=C{\Delta }_{\mathrm{func}}D$$
	oppfdiag.c	$$⊢\phi \to C\in \mathrm{Cat}$$
	oppfdiag.d	$$⊢\phi \to D\in \mathrm{Cat}$$
	oppfdiag.f	No typesetting found for |- ( ph -> F = ( oppFunc |` ( D Func C ) ) ) with typecode |-
	oppfdiag.n	$$⊢N=D\mathrm{Nat}C$$
	oppfdiag.g	$$⊢\phi \to G=\left(m\in \left(D\mathrm{Func}C\right),n\in \left(D\mathrm{Func}C\right)⟼{\mathrm{I}\upharpoonright }_{\left(nNm\right)}\right)$$
Assertion	oppfdiag	Could not format assertion : No typesetting found for |- ( ph -> ( <. F , G >. o.func ( oppFunc ` L ) ) = ( O DiagFunc P ) ) with typecode |-

Proof

Step	Hyp	Ref	Expression
1		oppfdiag.o	$$⊢O=\mathrm{oppCat}\left(C\right)$$
2		oppfdiag.p	$$⊢P=\mathrm{oppCat}\left(D\right)$$
3		oppfdiag.l	$$⊢L=C{\Delta }_{\mathrm{func}}D$$
4		oppfdiag.c	$$⊢\phi \to C\in \mathrm{Cat}$$
5		oppfdiag.d	$$⊢\phi \to D\in \mathrm{Cat}$$
6		oppfdiag.f	Could not format ( ph -> F = ( oppFunc |` ( D Func C ) ) ) : No typesetting found for |- ( ph -> F = ( oppFunc |` ( D Func C ) ) ) with typecode |-
7		oppfdiag.n	$$⊢N=D\mathrm{Nat}C$$
8		oppfdiag.g	$$⊢\phi \to G=\left(m\in \left(D\mathrm{Func}C\right),n\in \left(D\mathrm{Func}C\right)⟼{\mathrm{I}\upharpoonright }_{\left(nNm\right)}\right)$$
9		eqid	$$⊢{\mathrm{Base}}_C={\mathrm{Base}}_C$$
10	1 9	oppcbas	$$⊢{\mathrm{Base}}_C={\mathrm{Base}}_O$$
11		eqid	$$⊢P\mathrm{FuncCat}O=P\mathrm{FuncCat}O$$
12	11	fucbas	$$⊢P\mathrm{Func}O={\mathrm{Base}}_{\left(P\mathrm{FuncCat}O\right)}$$
13		eqid	$$⊢\mathrm{oppCat}\left(D\mathrm{FuncCat}C\right)=\mathrm{oppCat}\left(D\mathrm{FuncCat}C\right)$$
14		eqid	$$⊢D\mathrm{FuncCat}C=D\mathrm{FuncCat}C$$
15	3 4 5 14	diagcl	$$⊢\phi \to L\in \left(C\mathrm{Func}\left(D\mathrm{FuncCat}C\right)\right)$$
16	1 13 15	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 |-
17	2 1 14 13 11 7 6 8 5 4	fucoppcfunc	$$⊢\phi \to F\left(\mathrm{oppCat}\left(D\mathrm{FuncCat}C\right)\mathrm{Func}\left(P\mathrm{FuncCat}O\right)\right)G$$
18		df-br	$$⊢F\left(\mathrm{oppCat}\left(D\mathrm{FuncCat}C\right)\mathrm{Func}\left(P\mathrm{FuncCat}O\right)\right)G\leftrightarrow ⟨F,G⟩\in \left(\mathrm{oppCat}\left(D\mathrm{FuncCat}C\right)\mathrm{Func}\left(P\mathrm{FuncCat}O\right)\right)$$
19	17 18	sylib	$$⊢\phi \to ⟨F,G⟩\in \left(\mathrm{oppCat}\left(D\mathrm{FuncCat}C\right)\mathrm{Func}\left(P\mathrm{FuncCat}O\right)\right)$$
20	16 19	cofucl	Could not format ( ph -> ( <. F , G >. o.func ( oppFunc ` L ) ) e. ( O Func ( P FuncCat O ) ) ) : No typesetting found for |- ( ph -> ( <. F , G >. o.func ( oppFunc ` L ) ) e. ( O Func ( P FuncCat O ) ) ) with typecode |-
21	20	func1st2nd	Could not format ( ph -> ( 1st ` ( <. F , G >. o.func ( oppFunc ` L ) ) ) ( O Func ( P FuncCat O ) ) ( 2nd ` ( <. F , G >. o.func ( oppFunc ` L ) ) ) ) : No typesetting found for |- ( ph -> ( 1st ` ( <. F , G >. o.func ( oppFunc ` L ) ) ) ( O Func ( P FuncCat O ) ) ( 2nd ` ( <. F , G >. o.func ( oppFunc ` L ) ) ) ) with typecode |-
22	10 12 21	funcf1	Could not format ( ph -> ( 1st ` ( <. F , G >. o.func ( oppFunc ` L ) ) ) : ( Base ` C ) --> ( P Func O ) ) : No typesetting found for |- ( ph -> ( 1st ` ( <. F , G >. o.func ( oppFunc ` L ) ) ) : ( Base ` C ) --> ( P Func O ) ) with typecode |-
23	22	ffnd	Could not format ( ph -> ( 1st ` ( <. F , G >. o.func ( oppFunc ` L ) ) ) Fn ( Base ` C ) ) : No typesetting found for |- ( ph -> ( 1st ` ( <. F , G >. o.func ( oppFunc ` L ) ) ) Fn ( Base ` C ) ) with typecode |-
24		eqid	$$⊢O{\Delta }_{\mathrm{func}}P=O{\Delta }_{\mathrm{func}}P$$
25	1	oppccat	$$⊢C\in \mathrm{Cat}\to O\in \mathrm{Cat}$$
26	4 25	syl	$$⊢\phi \to O\in \mathrm{Cat}$$
27	2	oppccat	$$⊢D\in \mathrm{Cat}\to P\in \mathrm{Cat}$$
28	5 27	syl	$$⊢\phi \to P\in \mathrm{Cat}$$
29	24 26 28 11	diagcl	$$⊢\phi \to O{\Delta }_{\mathrm{func}}P\in \left(O\mathrm{Func}\left(P\mathrm{FuncCat}O\right)\right)$$
30	29	func1st2nd	$$⊢\phi \to 1^{st}\left(O{\Delta }_{\mathrm{func}}P\right)\left(O\mathrm{Func}\left(P\mathrm{FuncCat}O\right)\right)2^{nd}\left(O{\Delta }_{\mathrm{func}}P\right)$$
31	10 12 30	funcf1	$$⊢\phi \to 1^{st}\left(O{\Delta }_{\mathrm{func}}P\right):{\mathrm{Base}}_C⟶P\mathrm{Func}O$$
32	31	ffnd	$$⊢\phi \to 1^{st}\left(O{\Delta }_{\mathrm{func}}P\right)Fn{\mathrm{Base}}_C$$
33	16	adantr	Could not format ( ( ph /\ x e. ( Base ` C ) ) -> ( oppFunc ` L ) e. ( O Func ( oppCat ` ( D FuncCat C ) ) ) ) : No typesetting found for |- ( ( ph /\ x e. ( Base ` C ) ) -> ( oppFunc ` L ) e. ( O Func ( oppCat ` ( D FuncCat C ) ) ) ) with typecode |-
34	19	adantr	$$⊢\left(\phi \wedge x\in {\mathrm{Base}}_C\right)\to ⟨F,G⟩\in \left(\mathrm{oppCat}\left(D\mathrm{FuncCat}C\right)\mathrm{Func}\left(P\mathrm{FuncCat}O\right)\right)$$
35		simpr	$$⊢\left(\phi \wedge x\in {\mathrm{Base}}_C\right)\to x\in {\mathrm{Base}}_C$$
36	10 33 34 35	cofu1	Could not format ( ( ph /\ x e. ( Base ` C ) ) -> ( ( 1st ` ( <. F , G >. o.func ( oppFunc ` L ) ) ) ` x ) = ( ( 1st ` <. F , G >. ) ` ( ( 1st ` ( oppFunc ` L ) ) ` x ) ) ) : No typesetting found for |- ( ( ph /\ x e. ( Base ` C ) ) -> ( ( 1st ` ( <. F , G >. o.func ( oppFunc ` L ) ) ) ` x ) = ( ( 1st ` <. F , G >. ) ` ( ( 1st ` ( oppFunc ` L ) ) ` x ) ) ) with typecode |-
37	17	func1st	$$⊢\phi \to 1^{st}\left(⟨F,G⟩\right)=F$$
38	15	oppf1	Could not format ( ph -> ( 1st ` ( oppFunc ` L ) ) = ( 1st ` L ) ) : No typesetting found for |- ( ph -> ( 1st ` ( oppFunc ` L ) ) = ( 1st ` L ) ) with typecode |-
39	38	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 |-
40	37 39	fveq12d	Could not format ( ph -> ( ( 1st ` <. F , G >. ) ` ( ( 1st ` ( oppFunc ` L ) ) ` x ) ) = ( F ` ( ( 1st ` L ) ` x ) ) ) : No typesetting found for |- ( ph -> ( ( 1st ` <. F , G >. ) ` ( ( 1st ` ( oppFunc ` L ) ) ` x ) ) = ( F ` ( ( 1st ` L ) ` x ) ) ) with typecode |-
41	40	adantr	Could not format ( ( ph /\ x e. ( Base ` C ) ) -> ( ( 1st ` <. F , G >. ) ` ( ( 1st ` ( oppFunc ` L ) ) ` x ) ) = ( F ` ( ( 1st ` L ) ` x ) ) ) : No typesetting found for |- ( ( ph /\ x e. ( Base ` C ) ) -> ( ( 1st ` <. F , G >. ) ` ( ( 1st ` ( oppFunc ` L ) ) ` x ) ) = ( F ` ( ( 1st ` L ) ` x ) ) ) with typecode |-
42	4	adantr	$$⊢\left(\phi \wedge x\in {\mathrm{Base}}_C\right)\to C\in \mathrm{Cat}$$
43	5	adantr	$$⊢\left(\phi \wedge x\in {\mathrm{Base}}_C\right)\to D\in \mathrm{Cat}$$
44	6	adantr	Could not format ( ( ph /\ x e. ( Base ` C ) ) -> F = ( oppFunc |` ( D Func C ) ) ) : No typesetting found for |- ( ( ph /\ x e. ( Base ` C ) ) -> F = ( oppFunc |` ( D Func C ) ) ) with typecode |-
45	1 2 3 42 43 44 9 35	oppfdiag1	$$⊢\left(\phi \wedge x\in {\mathrm{Base}}_C\right)\to F\left(1^{st}\left(L\right)\left(x\right)\right)=1^{st}\left(O{\Delta }_{\mathrm{func}}P\right)\left(x\right)$$
46	36 41 45	3eqtrd	Could not format ( ( ph /\ x e. ( Base ` C ) ) -> ( ( 1st ` ( <. F , G >. o.func ( oppFunc ` L ) ) ) ` x ) = ( ( 1st ` ( O DiagFunc P ) ) ` x ) ) : No typesetting found for |- ( ( ph /\ x e. ( Base ` C ) ) -> ( ( 1st ` ( <. F , G >. o.func ( oppFunc ` L ) ) ) ` x ) = ( ( 1st ` ( O DiagFunc P ) ) ` x ) ) with typecode |-
47	23 32 46	eqfnfvd	Could not format ( ph -> ( 1st ` ( <. F , G >. o.func ( oppFunc ` L ) ) ) = ( 1st ` ( O DiagFunc P ) ) ) : No typesetting found for |- ( ph -> ( 1st ` ( <. F , G >. o.func ( oppFunc ` L ) ) ) = ( 1st ` ( O DiagFunc P ) ) ) with typecode |-
48	10 21	funcfn2	Could not format ( ph -> ( 2nd ` ( <. F , G >. o.func ( oppFunc ` L ) ) ) Fn ( ( Base ` C ) X. ( Base ` C ) ) ) : No typesetting found for |- ( ph -> ( 2nd ` ( <. F , G >. o.func ( oppFunc ` L ) ) ) Fn ( ( Base ` C ) X. ( Base ` C ) ) ) with typecode |-
49	10 30	funcfn2	$$⊢\phi \to 2^{nd}\left(O{\Delta }_{\mathrm{func}}P\right)Fn\left({\mathrm{Base}}_C\times {\mathrm{Base}}_C\right)$$
50		eqid	$$⊢\mathrm{Hom}\left(C\right)=\mathrm{Hom}\left(C\right)$$
51	50 1	oppchom	$$⊢x\mathrm{Hom}\left(O\right)y=y\mathrm{Hom}\left(C\right)x$$
52	51	a1i	$$⊢\left(\phi \wedge \left(x\in {\mathrm{Base}}_C\wedge y\in {\mathrm{Base}}_C\right)\right)\to x\mathrm{Hom}\left(O\right)y=y\mathrm{Hom}\left(C\right)x$$
53		eqid	$$⊢\mathrm{Hom}\left(O\right)=\mathrm{Hom}\left(O\right)$$
54		eqid	$$⊢P\mathrm{Nat}O=P\mathrm{Nat}O$$
55	11 54	fuchom	$$⊢P\mathrm{Nat}O=\mathrm{Hom}\left(P\mathrm{FuncCat}O\right)$$
56	21	adantr	Could not format ( ( ph /\ ( x e. ( Base ` C ) /\ y e. ( Base ` C ) ) ) -> ( 1st ` ( <. F , G >. o.func ( oppFunc ` L ) ) ) ( O Func ( P FuncCat O ) ) ( 2nd ` ( <. F , G >. o.func ( oppFunc ` L ) ) ) ) : No typesetting found for |- ( ( ph /\ ( x e. ( Base ` C ) /\ y e. ( Base ` C ) ) ) -> ( 1st ` ( <. F , G >. o.func ( oppFunc ` L ) ) ) ( O Func ( P FuncCat O ) ) ( 2nd ` ( <. F , G >. o.func ( oppFunc ` L ) ) ) ) with typecode |-
57		simprl	$$⊢\left(\phi \wedge \left(x\in {\mathrm{Base}}_C\wedge y\in {\mathrm{Base}}_C\right)\right)\to x\in {\mathrm{Base}}_C$$
58		simprr	$$⊢\left(\phi \wedge \left(x\in {\mathrm{Base}}_C\wedge y\in {\mathrm{Base}}_C\right)\right)\to y\in {\mathrm{Base}}_C$$
59	10 53 55 56 57 58	funcf2	Could not format ( ( ph /\ ( x e. ( Base ` C ) /\ y e. ( Base ` C ) ) ) -> ( x ( 2nd ` ( <. F , G >. o.func ( oppFunc ` L ) ) ) y ) : ( x ( Hom ` O ) y ) --> ( ( ( 1st ` ( <. F , G >. o.func ( oppFunc ` L ) ) ) ` x ) ( P Nat O ) ( ( 1st ` ( <. F , G >. o.func ( oppFunc ` L ) ) ) ` y ) ) ) : No typesetting found for |- ( ( ph /\ ( x e. ( Base ` C ) /\ y e. ( Base ` C ) ) ) -> ( x ( 2nd ` ( <. F , G >. o.func ( oppFunc ` L ) ) ) y ) : ( x ( Hom ` O ) y ) --> ( ( ( 1st ` ( <. F , G >. o.func ( oppFunc ` L ) ) ) ` x ) ( P Nat O ) ( ( 1st ` ( <. F , G >. o.func ( oppFunc ` L ) ) ) ` y ) ) ) with typecode |-
60	52 59	feq2dd	Could not format ( ( ph /\ ( x e. ( Base ` C ) /\ y e. ( Base ` C ) ) ) -> ( x ( 2nd ` ( <. F , G >. o.func ( oppFunc ` L ) ) ) y ) : ( y ( Hom ` C ) x ) --> ( ( ( 1st ` ( <. F , G >. o.func ( oppFunc ` L ) ) ) ` x ) ( P Nat O ) ( ( 1st ` ( <. F , G >. o.func ( oppFunc ` L ) ) ) ` y ) ) ) : No typesetting found for |- ( ( ph /\ ( x e. ( Base ` C ) /\ y e. ( Base ` C ) ) ) -> ( x ( 2nd ` ( <. F , G >. o.func ( oppFunc ` L ) ) ) y ) : ( y ( Hom ` C ) x ) --> ( ( ( 1st ` ( <. F , G >. o.func ( oppFunc ` L ) ) ) ` x ) ( P Nat O ) ( ( 1st ` ( <. F , G >. o.func ( oppFunc ` L ) ) ) ` y ) ) ) with typecode |-
61	60	ffnd	Could not format ( ( ph /\ ( x e. ( Base ` C ) /\ y e. ( Base ` C ) ) ) -> ( x ( 2nd ` ( <. F , G >. o.func ( oppFunc ` L ) ) ) y ) Fn ( y ( Hom ` C ) x ) ) : No typesetting found for |- ( ( ph /\ ( x e. ( Base ` C ) /\ y e. ( Base ` C ) ) ) -> ( x ( 2nd ` ( <. F , G >. o.func ( oppFunc ` L ) ) ) y ) Fn ( y ( Hom ` C ) x ) ) with typecode |-
62	30	adantr	$$⊢\left(\phi \wedge \left(x\in {\mathrm{Base}}_C\wedge y\in {\mathrm{Base}}_C\right)\right)\to 1^{st}\left(O{\Delta }_{\mathrm{func}}P\right)\left(O\mathrm{Func}\left(P\mathrm{FuncCat}O\right)\right)2^{nd}\left(O{\Delta }_{\mathrm{func}}P\right)$$
63	10 53 55 62 57 58	funcf2	$$⊢\left(\phi \wedge \left(x\in {\mathrm{Base}}_C\wedge y\in {\mathrm{Base}}_C\right)\right)\to \left(x{2}^{nd}\left(O{\Delta }_{\mathrm{func}}P\right)y\right):x\mathrm{Hom}\left(O\right)y⟶1^{st}\left(O{\Delta }_{\mathrm{func}}P\right)\left(x\right)\left(P\mathrm{Nat}O\right)1^{st}\left(O{\Delta }_{\mathrm{func}}P\right)\left(y\right)$$
64	52 63	feq2dd	$$⊢\left(\phi \wedge \left(x\in {\mathrm{Base}}_C\wedge y\in {\mathrm{Base}}_C\right)\right)\to \left(x{2}^{nd}\left(O{\Delta }_{\mathrm{func}}P\right)y\right):y\mathrm{Hom}\left(C\right)x⟶1^{st}\left(O{\Delta }_{\mathrm{func}}P\right)\left(x\right)\left(P\mathrm{Nat}O\right)1^{st}\left(O{\Delta }_{\mathrm{func}}P\right)\left(y\right)$$
65	64	ffnd	$$⊢\left(\phi \wedge \left(x\in {\mathrm{Base}}_C\wedge y\in {\mathrm{Base}}_C\right)\right)\to \left(x{2}^{nd}\left(O{\Delta }_{\mathrm{func}}P\right)y\right)Fn\left(y\mathrm{Hom}\left(C\right)x\right)$$
66	16	ad2antrr	Could not format ( ( ( ph /\ ( x e. ( Base ` C ) /\ y e. ( Base ` C ) ) ) /\ f e. ( y ( Hom ` C ) x ) ) -> ( oppFunc ` L ) e. ( O Func ( oppCat ` ( D FuncCat C ) ) ) ) : No typesetting found for |- ( ( ( ph /\ ( x e. ( Base ` C ) /\ y e. ( Base ` C ) ) ) /\ f e. ( y ( Hom ` C ) x ) ) -> ( oppFunc ` L ) e. ( O Func ( oppCat ` ( D FuncCat C ) ) ) ) with typecode |-
67	19	ad2antrr	$$⊢\left(\left(\phi \wedge \left(x\in {\mathrm{Base}}_C\wedge y\in {\mathrm{Base}}_C\right)\right)\wedge f\in \left(y\mathrm{Hom}\left(C\right)x\right)\right)\to ⟨F,G⟩\in \left(\mathrm{oppCat}\left(D\mathrm{FuncCat}C\right)\mathrm{Func}\left(P\mathrm{FuncCat}O\right)\right)$$
68	57	adantr	$$⊢\left(\left(\phi \wedge \left(x\in {\mathrm{Base}}_C\wedge y\in {\mathrm{Base}}_C\right)\right)\wedge f\in \left(y\mathrm{Hom}\left(C\right)x\right)\right)\to x\in {\mathrm{Base}}_C$$
69	58	adantr	$$⊢\left(\left(\phi \wedge \left(x\in {\mathrm{Base}}_C\wedge y\in {\mathrm{Base}}_C\right)\right)\wedge f\in \left(y\mathrm{Hom}\left(C\right)x\right)\right)\to y\in {\mathrm{Base}}_C$$
70		simpr	$$⊢\left(\left(\phi \wedge \left(x\in {\mathrm{Base}}_C\wedge y\in {\mathrm{Base}}_C\right)\right)\wedge f\in \left(y\mathrm{Hom}\left(C\right)x\right)\right)\to f\in \left(y\mathrm{Hom}\left(C\right)x\right)$$
71	70 51	eleqtrrdi	$$⊢\left(\left(\phi \wedge \left(x\in {\mathrm{Base}}_C\wedge y\in {\mathrm{Base}}_C\right)\right)\wedge f\in \left(y\mathrm{Hom}\left(C\right)x\right)\right)\to f\in \left(x\mathrm{Hom}\left(O\right)y\right)$$
72	10 66 67 68 69 53 71	cofu2	Could not format ( ( ( ph /\ ( x e. ( Base ` C ) /\ y e. ( Base ` C ) ) ) /\ f e. ( y ( Hom ` C ) x ) ) -> ( ( x ( 2nd ` ( <. F , G >. o.func ( oppFunc ` L ) ) ) y ) ` f ) = ( ( ( ( 1st ` ( oppFunc ` L ) ) ` x ) ( 2nd ` <. F , G >. ) ( ( 1st ` ( oppFunc ` L ) ) ` y ) ) ` ( ( x ( 2nd ` ( oppFunc ` L ) ) y ) ` f ) ) ) : No typesetting found for |- ( ( ( ph /\ ( x e. ( Base ` C ) /\ y e. ( Base ` C ) ) ) /\ f e. ( y ( Hom ` C ) x ) ) -> ( ( x ( 2nd ` ( <. F , G >. o.func ( oppFunc ` L ) ) ) y ) ` f ) = ( ( ( ( 1st ` ( oppFunc ` L ) ) ` x ) ( 2nd ` <. F , G >. ) ( ( 1st ` ( oppFunc ` L ) ) ` y ) ) ` ( ( x ( 2nd ` ( oppFunc ` L ) ) y ) ` f ) ) ) with typecode |-
73	17	func2nd	$$⊢\phi \to 2^{nd}\left(⟨F,G⟩\right)=G$$
74	38	fveq1d	Could not format ( ph -> ( ( 1st ` ( oppFunc ` L ) ) ` y ) = ( ( 1st ` L ) ` y ) ) : No typesetting found for |- ( ph -> ( ( 1st ` ( oppFunc ` L ) ) ` y ) = ( ( 1st ` L ) ` y ) ) with typecode |-
75	73 39 74	oveq123d	Could not format ( ph -> ( ( ( 1st ` ( oppFunc ` L ) ) ` x ) ( 2nd ` <. F , G >. ) ( ( 1st ` ( oppFunc ` L ) ) ` y ) ) = ( ( ( 1st ` L ) ` x ) G ( ( 1st ` L ) ` y ) ) ) : No typesetting found for |- ( ph -> ( ( ( 1st ` ( oppFunc ` L ) ) ` x ) ( 2nd ` <. F , G >. ) ( ( 1st ` ( oppFunc ` L ) ) ` y ) ) = ( ( ( 1st ` L ) ` x ) G ( ( 1st ` L ) ` y ) ) ) with typecode |-
76	15	oppf2	Could not format ( ph -> ( x ( 2nd ` ( oppFunc ` L ) ) y ) = ( y ( 2nd ` L ) x ) ) : No typesetting found for |- ( ph -> ( x ( 2nd ` ( oppFunc ` L ) ) y ) = ( y ( 2nd ` L ) x ) ) with typecode |-
77	76	fveq1d	Could not format ( ph -> ( ( x ( 2nd ` ( oppFunc ` L ) ) y ) ` f ) = ( ( y ( 2nd ` L ) x ) ` f ) ) : No typesetting found for |- ( ph -> ( ( x ( 2nd ` ( oppFunc ` L ) ) y ) ` f ) = ( ( y ( 2nd ` L ) x ) ` f ) ) with typecode |-
78	75 77	fveq12d	Could not format ( ph -> ( ( ( ( 1st ` ( oppFunc ` L ) ) ` x ) ( 2nd ` <. F , G >. ) ( ( 1st ` ( oppFunc ` L ) ) ` y ) ) ` ( ( x ( 2nd ` ( oppFunc ` L ) ) y ) ` f ) ) = ( ( ( ( 1st ` L ) ` x ) G ( ( 1st ` L ) ` y ) ) ` ( ( y ( 2nd ` L ) x ) ` f ) ) ) : No typesetting found for |- ( ph -> ( ( ( ( 1st ` ( oppFunc ` L ) ) ` x ) ( 2nd ` <. F , G >. ) ( ( 1st ` ( oppFunc ` L ) ) ` y ) ) ` ( ( x ( 2nd ` ( oppFunc ` L ) ) y ) ` f ) ) = ( ( ( ( 1st ` L ) ` x ) G ( ( 1st ` L ) ` y ) ) ` ( ( y ( 2nd ` L ) x ) ` f ) ) ) with typecode |-
79	78	ad2antrr	Could not format ( ( ( ph /\ ( x e. ( Base ` C ) /\ y e. ( Base ` C ) ) ) /\ f e. ( y ( Hom ` C ) x ) ) -> ( ( ( ( 1st ` ( oppFunc ` L ) ) ` x ) ( 2nd ` <. F , G >. ) ( ( 1st ` ( oppFunc ` L ) ) ` y ) ) ` ( ( x ( 2nd ` ( oppFunc ` L ) ) y ) ` f ) ) = ( ( ( ( 1st ` L ) ` x ) G ( ( 1st ` L ) ` y ) ) ` ( ( y ( 2nd ` L ) x ) ` f ) ) ) : No typesetting found for |- ( ( ( ph /\ ( x e. ( Base ` C ) /\ y e. ( Base ` C ) ) ) /\ f e. ( y ( Hom ` C ) x ) ) -> ( ( ( ( 1st ` ( oppFunc ` L ) ) ` x ) ( 2nd ` <. F , G >. ) ( ( 1st ` ( oppFunc ` L ) ) ` y ) ) ` ( ( x ( 2nd ` ( oppFunc ` L ) ) y ) ` f ) ) = ( ( ( ( 1st ` L ) ` x ) G ( ( 1st ` L ) ` y ) ) ` ( ( y ( 2nd ` L ) x ) ` f ) ) ) with typecode |-
80	8	ad2antrr	$$⊢\left(\left(\phi \wedge \left(x\in {\mathrm{Base}}_C\wedge y\in {\mathrm{Base}}_C\right)\right)\wedge f\in \left(y\mathrm{Hom}\left(C\right)x\right)\right)\to G=\left(m\in \left(D\mathrm{Func}C\right),n\in \left(D\mathrm{Func}C\right)⟼{\mathrm{I}\upharpoonright }_{\left(nNm\right)}\right)$$
81	4	ad2antrr	$$⊢\left(\left(\phi \wedge \left(x\in {\mathrm{Base}}_C\wedge y\in {\mathrm{Base}}_C\right)\right)\wedge f\in \left(y\mathrm{Hom}\left(C\right)x\right)\right)\to C\in \mathrm{Cat}$$
82	5	ad2antrr	$$⊢\left(\left(\phi \wedge \left(x\in {\mathrm{Base}}_C\wedge y\in {\mathrm{Base}}_C\right)\right)\wedge f\in \left(y\mathrm{Hom}\left(C\right)x\right)\right)\to D\in \mathrm{Cat}$$
83		eqid	$$⊢1^{st}\left(L\right)\left(x\right)=1^{st}\left(L\right)\left(x\right)$$
84	3 81 82 9 68 83	diag1cl	$$⊢\left(\left(\phi \wedge \left(x\in {\mathrm{Base}}_C\wedge y\in {\mathrm{Base}}_C\right)\right)\wedge f\in \left(y\mathrm{Hom}\left(C\right)x\right)\right)\to 1^{st}\left(L\right)\left(x\right)\in \left(D\mathrm{Func}C\right)$$
85		eqid	$$⊢1^{st}\left(L\right)\left(y\right)=1^{st}\left(L\right)\left(y\right)$$
86	3 81 82 9 69 85	diag1cl	$$⊢\left(\left(\phi \wedge \left(x\in {\mathrm{Base}}_C\wedge y\in {\mathrm{Base}}_C\right)\right)\wedge f\in \left(y\mathrm{Hom}\left(C\right)x\right)\right)\to 1^{st}\left(L\right)\left(y\right)\in \left(D\mathrm{Func}C\right)$$
87		eqid	$$⊢{\mathrm{Base}}_D={\mathrm{Base}}_D$$
88	3 9 87 50 81 82 69 68 70	diag2	$$⊢\left(\left(\phi \wedge \left(x\in {\mathrm{Base}}_C\wedge y\in {\mathrm{Base}}_C\right)\right)\wedge f\in \left(y\mathrm{Hom}\left(C\right)x\right)\right)\to \left(y{2}^{nd}\left(L\right)x\right)\left(f\right)={\mathrm{Base}}_D\times \left\{f\right\}$$
89	3 9 87 50 81 82 69 68 70 7	diag2cl	$$⊢\left(\left(\phi \wedge \left(x\in {\mathrm{Base}}_C\wedge y\in {\mathrm{Base}}_C\right)\right)\wedge f\in \left(y\mathrm{Hom}\left(C\right)x\right)\right)\to {\mathrm{Base}}_D\times \left\{f\right\}\in \left(1^{st}\left(L\right)\left(y\right)N{1}^{st}\left(L\right)\left(x\right)\right)$$
90	80 84 86 88 89	opf2	$$⊢\left(\left(\phi \wedge \left(x\in {\mathrm{Base}}_C\wedge y\in {\mathrm{Base}}_C\right)\right)\wedge f\in \left(y\mathrm{Hom}\left(C\right)x\right)\right)\to \left(1^{st}\left(L\right)\left(x\right)G{1}^{st}\left(L\right)\left(y\right)\right)\left(\left(y{2}^{nd}\left(L\right)x\right)\left(f\right)\right)={\mathrm{Base}}_D\times \left\{f\right\}$$
91	72 79 90	3eqtrd	Could not format ( ( ( ph /\ ( x e. ( Base ` C ) /\ y e. ( Base ` C ) ) ) /\ f e. ( y ( Hom ` C ) x ) ) -> ( ( x ( 2nd ` ( <. F , G >. o.func ( oppFunc ` L ) ) ) y ) ` f ) = ( ( Base ` D ) X. { f } ) ) : No typesetting found for |- ( ( ( ph /\ ( x e. ( Base ` C ) /\ y e. ( Base ` C ) ) ) /\ f e. ( y ( Hom ` C ) x ) ) -> ( ( x ( 2nd ` ( <. F , G >. o.func ( oppFunc ` L ) ) ) y ) ` f ) = ( ( Base ` D ) X. { f } ) ) with typecode |-
92	2 87	oppcbas	$$⊢{\mathrm{Base}}_D={\mathrm{Base}}_P$$
93	81 25	syl	$$⊢\left(\left(\phi \wedge \left(x\in {\mathrm{Base}}_C\wedge y\in {\mathrm{Base}}_C\right)\right)\wedge f\in \left(y\mathrm{Hom}\left(C\right)x\right)\right)\to O\in \mathrm{Cat}$$
94	82 27	syl	$$⊢\left(\left(\phi \wedge \left(x\in {\mathrm{Base}}_C\wedge y\in {\mathrm{Base}}_C\right)\right)\wedge f\in \left(y\mathrm{Hom}\left(C\right)x\right)\right)\to P\in \mathrm{Cat}$$
95	24 10 92 53 93 94 68 69 71	diag2	$$⊢\left(\left(\phi \wedge \left(x\in {\mathrm{Base}}_C\wedge y\in {\mathrm{Base}}_C\right)\right)\wedge f\in \left(y\mathrm{Hom}\left(C\right)x\right)\right)\to \left(x{2}^{nd}\left(O{\Delta }_{\mathrm{func}}P\right)y\right)\left(f\right)={\mathrm{Base}}_D\times \left\{f\right\}$$
96	91 95	eqtr4d	Could not format ( ( ( ph /\ ( x e. ( Base ` C ) /\ y e. ( Base ` C ) ) ) /\ f e. ( y ( Hom ` C ) x ) ) -> ( ( x ( 2nd ` ( <. F , G >. o.func ( oppFunc ` L ) ) ) y ) ` f ) = ( ( x ( 2nd ` ( O DiagFunc P ) ) y ) ` f ) ) : No typesetting found for |- ( ( ( ph /\ ( x e. ( Base ` C ) /\ y e. ( Base ` C ) ) ) /\ f e. ( y ( Hom ` C ) x ) ) -> ( ( x ( 2nd ` ( <. F , G >. o.func ( oppFunc ` L ) ) ) y ) ` f ) = ( ( x ( 2nd ` ( O DiagFunc P ) ) y ) ` f ) ) with typecode |-
97	61 65 96	eqfnfvd	Could not format ( ( ph /\ ( x e. ( Base ` C ) /\ y e. ( Base ` C ) ) ) -> ( x ( 2nd ` ( <. F , G >. o.func ( oppFunc ` L ) ) ) y ) = ( x ( 2nd ` ( O DiagFunc P ) ) y ) ) : No typesetting found for |- ( ( ph /\ ( x e. ( Base ` C ) /\ y e. ( Base ` C ) ) ) -> ( x ( 2nd ` ( <. F , G >. o.func ( oppFunc ` L ) ) ) y ) = ( x ( 2nd ` ( O DiagFunc P ) ) y ) ) with typecode |-
98	48 49 97	eqfnovd	Could not format ( ph -> ( 2nd ` ( <. F , G >. o.func ( oppFunc ` L ) ) ) = ( 2nd ` ( O DiagFunc P ) ) ) : No typesetting found for |- ( ph -> ( 2nd ` ( <. F , G >. o.func ( oppFunc ` L ) ) ) = ( 2nd ` ( O DiagFunc P ) ) ) with typecode |-
99	47 98	opeq12d	Could not format ( ph -> <. ( 1st ` ( <. F , G >. o.func ( oppFunc ` L ) ) ) , ( 2nd ` ( <. F , G >. o.func ( oppFunc ` L ) ) ) >. = <. ( 1st ` ( O DiagFunc P ) ) , ( 2nd ` ( O DiagFunc P ) ) >. ) : No typesetting found for |- ( ph -> <. ( 1st ` ( <. F , G >. o.func ( oppFunc ` L ) ) ) , ( 2nd ` ( <. F , G >. o.func ( oppFunc ` L ) ) ) >. = <. ( 1st ` ( O DiagFunc P ) ) , ( 2nd ` ( O DiagFunc P ) ) >. ) with typecode |-
100		relfunc	$$⊢\mathrm{Rel}\left(O\mathrm{Func}\left(P\mathrm{FuncCat}O\right)\right)$$
101		1st2nd	Could not format ( ( Rel ( O Func ( P FuncCat O ) ) /\ ( <. F , G >. o.func ( oppFunc ` L ) ) e. ( O Func ( P FuncCat O ) ) ) -> ( <. F , G >. o.func ( oppFunc ` L ) ) = <. ( 1st ` ( <. F , G >. o.func ( oppFunc ` L ) ) ) , ( 2nd ` ( <. F , G >. o.func ( oppFunc ` L ) ) ) >. ) : No typesetting found for |- ( ( Rel ( O Func ( P FuncCat O ) ) /\ ( <. F , G >. o.func ( oppFunc ` L ) ) e. ( O Func ( P FuncCat O ) ) ) -> ( <. F , G >. o.func ( oppFunc ` L ) ) = <. ( 1st ` ( <. F , G >. o.func ( oppFunc ` L ) ) ) , ( 2nd ` ( <. F , G >. o.func ( oppFunc ` L ) ) ) >. ) with typecode |-
102	100 20 101	sylancr	Could not format ( ph -> ( <. F , G >. o.func ( oppFunc ` L ) ) = <. ( 1st ` ( <. F , G >. o.func ( oppFunc ` L ) ) ) , ( 2nd ` ( <. F , G >. o.func ( oppFunc ` L ) ) ) >. ) : No typesetting found for |- ( ph -> ( <. F , G >. o.func ( oppFunc ` L ) ) = <. ( 1st ` ( <. F , G >. o.func ( oppFunc ` L ) ) ) , ( 2nd ` ( <. F , G >. o.func ( oppFunc ` L ) ) ) >. ) with typecode |-
103		1st2nd	$$⊢\left(\mathrm{Rel}\left(O\mathrm{Func}\left(P\mathrm{FuncCat}O\right)\right)\wedge O{\Delta }_{\mathrm{func}}P\in \left(O\mathrm{Func}\left(P\mathrm{FuncCat}O\right)\right)\right)\to O{\Delta }_{\mathrm{func}}P=⟨1^{st}\left(O{\Delta }_{\mathrm{func}}P\right),2^{nd}\left(O{\Delta }_{\mathrm{func}}P\right)⟩$$
104	100 29 103	sylancr	$$⊢\phi \to O{\Delta }_{\mathrm{func}}P=⟨1^{st}\left(O{\Delta }_{\mathrm{func}}P\right),2^{nd}\left(O{\Delta }_{\mathrm{func}}P\right)⟩$$
105	99 102 104	3eqtr4d	Could not format ( ph -> ( <. F , G >. o.func ( oppFunc ` L ) ) = ( O DiagFunc P ) ) : No typesetting found for |- ( ph -> ( <. F , G >. o.func ( oppFunc ` L ) ) = ( O DiagFunc P ) ) with typecode |-