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 = ( Base ` D )
	oppcup3.h	|- H = ( Hom ` D )
	oppcup3.j	|- J = ( Hom ` E )
	oppcup3.xb	|- .xb = ( comp ` E )
	oppcup3.o	|- O = ( oppCat ` D )
	oppcup3.p	|- P = ( oppCat ` E )
	oppcup3.x	|- ( ph -> X ( <. F , T >. ( O UP P ) W ) M )
	oppcup3.g	|- ( ph -> tpos T = G )
	oppcup3.y	|- ( ph -> Y e. B )
	oppcup3.n	|- ( ph -> N e. ( ( F ` Y ) J W ) )
Assertion	oppcup3	|- ( ph -> E! k e. ( Y H X ) N = ( M ( <. ( F ` Y ) , ( F ` X ) >. .xb W ) ( ( Y G X ) ` k ) ) )

Proof

Step	Hyp	Ref	Expression
1		oppcup3.b	|- B = ( Base ` D )
2		oppcup3.h	|- H = ( Hom ` D )
3		oppcup3.j	|- J = ( Hom ` E )
4		oppcup3.xb	|- .xb = ( comp ` E )
5		oppcup3.o	|- O = ( oppCat ` D )
6		oppcup3.p	|- P = ( oppCat ` E )
7		oppcup3.x	|- ( ph -> X ( <. F , T >. ( O UP P ) W ) M )
8		oppcup3.g	|- ( ph -> tpos T = G )
9		oppcup3.y	|- ( ph -> Y e. B )
10		oppcup3.n	|- ( ph -> N e. ( ( F ` Y ) J W ) )
11	9 1	eleqtrdi	|- ( ph -> Y e. ( Base ` D ) )
12	11	elfvexd	|- ( ph -> D e. _V )
13	10	ne0d	|- ( ph -> ( ( F ` Y ) J W ) =/= (/) )
14		fvprc	|- ( -. E e. _V -> ( Hom ` E ) = (/) )
15	3 14	eqtrid	|- ( -. E e. _V -> J = (/) )
16	15	oveqd	|- ( -. E e. _V -> ( ( F ` Y ) J W ) = ( ( F ` Y ) (/) W ) )
17		0ov	|- ( ( F ` Y ) (/) W ) = (/)
18	16 17	eqtrdi	|- ( -. E e. _V -> ( ( F ` Y ) J W ) = (/) )
19	18	necon1ai	|- ( ( ( F ` Y ) J W ) =/= (/) -> E e. _V )
20	13 19	syl	|- ( ph -> E e. _V )
21	7 6 5 12 20 8	oppcuprcl2	|- ( ph -> F ( D Func E ) G )
22	7 8	uptpos	|- ( ph -> X ( <. F , tpos G >. ( O UP P ) W ) M )
23	1 2 3 4 5 6 21 22	oppcup2	|- ( ph -> 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 ) ) )
24	23 9 10	oppcup3lem	|- ( ph -> E! k e. ( Y H X ) N = ( M ( <. ( F ` Y ) , ( F ` X ) >. .xb W ) ( ( Y G X ) ` k ) ) )