Theorem oppcup2

Description: The universal property for the universal pair <. X , M >. from a functor to an object, expressed explicitly. (Contributed by Zhi Wang, 4-Nov-2025)

	Ref	Expression
Hypotheses	oppcup2.b	$$⊢B={\mathrm{Base}}_D$$
	oppcup2.h	$$⊢H=\mathrm{Hom}\left(D\right)$$
	oppcup2.j	$$⊢J=\mathrm{Hom}\left(E\right)$$
	oppcup2.xb	$$⊢\underset{\dot{}}{\bullet }=\mathrm{comp}\left(E\right)$$
	oppcup2.o	$$⊢O=\mathrm{oppCat}\left(D\right)$$
	oppcup2.p	$$⊢P=\mathrm{oppCat}\left(E\right)$$
	oppcup2.f	$$⊢\phi \to F\left(D\mathrm{Func}E\right)G$$
	oppcup2.x	No typesetting found for |- ( ph -> X ( <. F , tpos G >. ( O UP P ) W ) M ) with typecode |-
Assertion	oppcup2	$$⊢\phi \to \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)$$

Proof

Step	Hyp	Ref	Expression
1		oppcup2.b	$$⊢B={\mathrm{Base}}_D$$
2		oppcup2.h	$$⊢H=\mathrm{Hom}\left(D\right)$$
3		oppcup2.j	$$⊢J=\mathrm{Hom}\left(E\right)$$
4		oppcup2.xb	$$⊢\underset{\dot{}}{\bullet }=\mathrm{comp}\left(E\right)$$
5		oppcup2.o	$$⊢O=\mathrm{oppCat}\left(D\right)$$
6		oppcup2.p	$$⊢P=\mathrm{oppCat}\left(E\right)$$
7		oppcup2.f	$$⊢\phi \to F\left(D\mathrm{Func}E\right)G$$
8		oppcup2.x	Could not format ( ph -> X ( <. F , tpos G >. ( O UP P ) W ) M ) : No typesetting found for |- ( ph -> X ( <. F , tpos G >. ( O UP P ) W ) M ) with typecode |-
9		eqid	$$⊢{\mathrm{Base}}_E={\mathrm{Base}}_E$$
10	8 6 9	oppcuprcl3	$$⊢\phi \to W\in {\mathrm{Base}}_E$$
11	8 5 1	oppcuprcl4	$$⊢\phi \to X\in B$$
12	8 6 3	oppcuprcl5	$$⊢\phi \to M\in \left(F\left(X\right)JW\right)$$
13	1 9 2 3 4 10 7 11 12 5 6	oppcup	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 |-
14	8 13	mpbid	$$⊢\phi \to \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)$$