Theorem oppcup

Description: The universal pair <. X , M >. from a functor to an object is universal from an object to a functor in the opposite category. (Contributed by Zhi Wang, 24-Sep-2025)

	Ref	Expression
Hypotheses	oppcup.b	$$⊢B={\mathrm{Base}}_D$$
	oppcup.c	$$⊢C={\mathrm{Base}}_E$$
	oppcup.h	$$⊢H=\mathrm{Hom}\left(D\right)$$
	oppcup.j	$$⊢J=\mathrm{Hom}\left(E\right)$$
	oppcup.xb	$$⊢\underset{\dot{}}{\bullet }=\mathrm{comp}\left(E\right)$$
	oppcup.w	$$⊢\phi \to W\in C$$
	oppcup.f	$$⊢\phi \to F\left(D\mathrm{Func}E\right)G$$
	oppcup.x	$$⊢\phi \to X\in B$$
	oppcup.m	$$⊢\phi \to M\in \left(F\left(X\right)JW\right)$$
	oppcup.o	$$⊢O=\mathrm{oppCat}\left(D\right)$$
	oppcup.p	$$⊢P=\mathrm{oppCat}\left(E\right)$$
Assertion	oppcup	Could not format assertion : No typesetting found for |- ( ph -> ( X ( <. F , tpos G >. ( O UP P ) W ) M <-> A. y e. B A. g e. ( ( F ` y ) J W ) E! k e. ( y H X ) g = ( M ( <. ( F ` y ) , ( F ` X ) >. .xb W ) ( ( y G X ) ` k ) ) ) ) with typecode |-

Proof

Step	Hyp	Ref	Expression
1		oppcup.b	$$⊢B={\mathrm{Base}}_D$$
2		oppcup.c	$$⊢C={\mathrm{Base}}_E$$
3		oppcup.h	$$⊢H=\mathrm{Hom}\left(D\right)$$
4		oppcup.j	$$⊢J=\mathrm{Hom}\left(E\right)$$
5		oppcup.xb	$$⊢\underset{\dot{}}{\bullet }=\mathrm{comp}\left(E\right)$$
6		oppcup.w	$$⊢\phi \to W\in C$$
7		oppcup.f	$$⊢\phi \to F\left(D\mathrm{Func}E\right)G$$
8		oppcup.x	$$⊢\phi \to X\in B$$
9		oppcup.m	$$⊢\phi \to M\in \left(F\left(X\right)JW\right)$$
10		oppcup.o	$$⊢O=\mathrm{oppCat}\left(D\right)$$
11		oppcup.p	$$⊢P=\mathrm{oppCat}\left(E\right)$$
12	10 1	oppcbas	$$⊢B={\mathrm{Base}}_O$$
13	11 2	oppcbas	$$⊢C={\mathrm{Base}}_P$$
14		eqid	$$⊢\mathrm{Hom}\left(O\right)=\mathrm{Hom}\left(O\right)$$
15		eqid	$$⊢\mathrm{Hom}\left(P\right)=\mathrm{Hom}\left(P\right)$$
16		eqid	$$⊢\mathrm{comp}\left(P\right)=\mathrm{comp}\left(P\right)$$
17	10 11 7	funcoppc	$$⊢\phi \to F\left(O\mathrm{Func}P\right)tposG$$
18	4 11	oppchom	$$⊢W\mathrm{Hom}\left(P\right)F\left(X\right)=F\left(X\right)JW$$
19	9 18	eleqtrrdi	$$⊢\phi \to M\in \left(W\mathrm{Hom}\left(P\right)F\left(X\right)\right)$$
20	12 13 14 15 16 6 17 8 19	isup	Could not format ( ph -> ( X ( <. F , tpos G >. ( O UP P ) W ) M <-> A. y e. B A. g e. ( W ( Hom ` P ) ( F ` y ) ) E! k e. ( X ( Hom ` O ) y ) g = ( ( ( X tpos G y ) ` k ) ( <. W , ( F ` X ) >. ( comp ` P ) ( F ` y ) ) M ) ) ) : No typesetting found for |- ( ph -> ( X ( <. F , tpos G >. ( O UP P ) W ) M <-> A. y e. B A. g e. ( W ( Hom ` P ) ( F ` y ) ) E! k e. ( X ( Hom ` O ) y ) g = ( ( ( X tpos G y ) ` k ) ( <. W , ( F ` X ) >. ( comp ` P ) ( F ` y ) ) M ) ) ) with typecode |-
21	4 11	oppchom	$$⊢W\mathrm{Hom}\left(P\right)F\left(y\right)=F\left(y\right)JW$$
22	21	a1i	$$⊢\left(\phi \wedge y\in B\right)\to W\mathrm{Hom}\left(P\right)F\left(y\right)=F\left(y\right)JW$$
23	3 10	oppchom	$$⊢X\mathrm{Hom}\left(O\right)y=yHX$$
24	23	a1i	$$⊢\left(\phi \wedge y\in B\right)\to X\mathrm{Hom}\left(O\right)y=yHX$$
25		ovtpos	$$⊢XtposGy=yGX$$
26	25	fveq1i	$$⊢\left(XtposGy\right)\left(k\right)=\left(yGX\right)\left(k\right)$$
27	26	oveq1i	$$⊢\left(XtposGy\right)\left(k\right)\left(⟨W,F\left(X\right)⟩\mathrm{comp}\left(P\right)F\left(y\right)\right)M=\left(yGX\right)\left(k\right)\left(⟨W,F\left(X\right)⟩\mathrm{comp}\left(P\right)F\left(y\right)\right)M$$
28	6	adantr	$$⊢\left(\phi \wedge y\in B\right)\to W\in C$$
29	7	adantr	$$⊢\left(\phi \wedge y\in B\right)\to F\left(D\mathrm{Func}E\right)G$$
30	1 2 29	funcf1	$$⊢\left(\phi \wedge y\in B\right)\to F:B⟶C$$
31	8	adantr	$$⊢\left(\phi \wedge y\in B\right)\to X\in B$$
32	30 31	ffvelcdmd	$$⊢\left(\phi \wedge y\in B\right)\to F\left(X\right)\in C$$
33		simpr	$$⊢\left(\phi \wedge y\in B\right)\to y\in B$$
34	30 33	ffvelcdmd	$$⊢\left(\phi \wedge y\in B\right)\to F\left(y\right)\in C$$
35	2 5 11 28 32 34	oppcco	$$⊢\left(\phi \wedge y\in B\right)\to \left(yGX\right)\left(k\right)\left(⟨W,F\left(X\right)⟩\mathrm{comp}\left(P\right)F\left(y\right)\right)M=M\left(⟨F\left(y\right),F\left(X\right)⟩\underset{\dot{}}{\bullet }W\right)\left(yGX\right)\left(k\right)$$
36	27 35	eqtrid	$$⊢\left(\phi \wedge y\in B\right)\to \left(XtposGy\right)\left(k\right)\left(⟨W,F\left(X\right)⟩\mathrm{comp}\left(P\right)F\left(y\right)\right)M=M\left(⟨F\left(y\right),F\left(X\right)⟩\underset{\dot{}}{\bullet }W\right)\left(yGX\right)\left(k\right)$$
37	36	eqeq2d	$$⊢\left(\phi \wedge y\in B\right)\to \left(g=\left(XtposGy\right)\left(k\right)\left(⟨W,F\left(X\right)⟩\mathrm{comp}\left(P\right)F\left(y\right)\right)M\leftrightarrow g=M\left(⟨F\left(y\right),F\left(X\right)⟩\underset{\dot{}}{\bullet }W\right)\left(yGX\right)\left(k\right)\right)$$
38	24 37	reueqbidv	$$⊢\left(\phi \wedge y\in B\right)\to \left(\exists !k\in \left(X\mathrm{Hom}\left(O\right)y\right)g=\left(XtposGy\right)\left(k\right)\left(⟨W,F\left(X\right)⟩\mathrm{comp}\left(P\right)F\left(y\right)\right)M\leftrightarrow \exists !k\in \left(yHX\right)g=M\left(⟨F\left(y\right),F\left(X\right)⟩\underset{\dot{}}{\bullet }W\right)\left(yGX\right)\left(k\right)\right)$$
39	22 38	raleqbidv	$$⊢\left(\phi \wedge y\in B\right)\to \left(\forall g\in \left(W\mathrm{Hom}\left(P\right)F\left(y\right)\right)\exists !k\in \left(X\mathrm{Hom}\left(O\right)y\right)g=\left(XtposGy\right)\left(k\right)\left(⟨W,F\left(X\right)⟩\mathrm{comp}\left(P\right)F\left(y\right)\right)M\leftrightarrow \forall g\in \left(F\left(y\right)JW\right)\exists !k\in \left(yHX\right)g=M\left(⟨F\left(y\right),F\left(X\right)⟩\underset{\dot{}}{\bullet }W\right)\left(yGX\right)\left(k\right)\right)$$
40	39	ralbidva	$$⊢\phi \to \left(\forall y\in B\forall g\in \left(W\mathrm{Hom}\left(P\right)F\left(y\right)\right)\exists !k\in \left(X\mathrm{Hom}\left(O\right)y\right)g=\left(XtposGy\right)\left(k\right)\left(⟨W,F\left(X\right)⟩\mathrm{comp}\left(P\right)F\left(y\right)\right)M\leftrightarrow \forall y\in B\forall g\in \left(F\left(y\right)JW\right)\exists !k\in \left(yHX\right)g=M\left(⟨F\left(y\right),F\left(X\right)⟩\underset{\dot{}}{\bullet }W\right)\left(yGX\right)\left(k\right)\right)$$
41	20 40	bitrd	Could not format ( ph -> ( X ( <. F , tpos G >. ( O UP P ) W ) M <-> A. y e. B A. g e. ( ( F ` y ) J W ) E! k e. ( y H X ) g = ( M ( <. ( F ` y ) , ( F ` X ) >. .xb W ) ( ( y G X ) ` k ) ) ) ) : No typesetting found for |- ( ph -> ( X ( <. F , tpos G >. ( O UP P ) W ) M <-> A. y e. B A. g e. ( ( F ` y ) J W ) E! k e. ( y H X ) g = ( M ( <. ( F ` y ) , ( F ` X ) >. .xb W ) ( ( y G X ) ` k ) ) ) ) with typecode |-