Theorem oppcup3

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	oppcup3.b	$$⊢B={\mathrm{Base}}_D$$
	oppcup3.h	$$⊢H=\mathrm{Hom}\left(D\right)$$
	oppcup3.j	$$⊢J=\mathrm{Hom}\left(E\right)$$
	oppcup3.xb	$$⊢\underset{\dot{}}{\bullet }=\mathrm{comp}\left(E\right)$$
	oppcup3.o	$$⊢O=\mathrm{oppCat}\left(D\right)$$
	oppcup3.p	$$⊢P=\mathrm{oppCat}\left(E\right)$$
	oppcup3.x	No typesetting found for |- ( ph -> X ( <. F , T >. ( O UP P ) W ) M ) with typecode |-
	oppcup3.g	$$⊢\phi \to tposT=G$$
	oppcup3.y	$$⊢\phi \to Y\in B$$
	oppcup3.n	$$⊢\phi \to N\in \left(F\left(Y\right)JW\right)$$
Assertion	oppcup3	$$⊢\phi \to \exists !k\in \left(YHX\right)N=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		oppcup3.b	$$⊢B={\mathrm{Base}}_D$$
2		oppcup3.h	$$⊢H=\mathrm{Hom}\left(D\right)$$
3		oppcup3.j	$$⊢J=\mathrm{Hom}\left(E\right)$$
4		oppcup3.xb	$$⊢\underset{\dot{}}{\bullet }=\mathrm{comp}\left(E\right)$$
5		oppcup3.o	$$⊢O=\mathrm{oppCat}\left(D\right)$$
6		oppcup3.p	$$⊢P=\mathrm{oppCat}\left(E\right)$$
7		oppcup3.x	Could not format ( ph -> X ( <. F , T >. ( O UP P ) W ) M ) : No typesetting found for |- ( ph -> X ( <. F , T >. ( O UP P ) W ) M ) with typecode |-
8		oppcup3.g	$$⊢\phi \to tposT=G$$
9		oppcup3.y	$$⊢\phi \to Y\in B$$
10		oppcup3.n	$$⊢\phi \to N\in \left(F\left(Y\right)JW\right)$$
11	9 1	eleqtrdi	$$⊢\phi \to Y\in {\mathrm{Base}}_D$$
12	11	elfvexd	$$⊢\phi \to D\in \mathrm{V}$$
13	10	ne0d	$$⊢\phi \to F\left(Y\right)JW\ne \varnothing$$
14		fvprc	$$⊢\neg E\in \mathrm{V}\to \mathrm{Hom}\left(E\right)=\varnothing$$
15	3 14	eqtrid	$$⊢\neg E\in \mathrm{V}\to J=\varnothing$$
16	15	oveqd	$$⊢\neg E\in \mathrm{V}\to F\left(Y\right)JW=F\left(Y\right)\varnothing W$$
17		0ov	$$⊢F\left(Y\right)\varnothing W=\varnothing$$
18	16 17	eqtrdi	$$⊢\neg E\in \mathrm{V}\to F\left(Y\right)JW=\varnothing$$
19	18	necon1ai	$$⊢F\left(Y\right)JW\ne \varnothing \to E\in \mathrm{V}$$
20	13 19	syl	$$⊢\phi \to E\in \mathrm{V}$$
21	7 6 5 12 20 8	oppcuprcl2	$$⊢\phi \to F\left(D\mathrm{Func}E\right)G$$
22	7 8	uptpos	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 |-
23	1 2 3 4 5 6 21 22	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)$$
24	23 9 10	oppcup3lem	$$⊢\phi \to \exists !k\in \left(YHX\right)N=M\left(⟨F\left(Y\right),F\left(X\right)⟩\underset{\dot{}}{\bullet }W\right)\left(YGX\right)\left(k\right)$$