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 = ( Base ` D )
	oppcup2.h	|- H = ( Hom ` D )
	oppcup2.j	|- J = ( Hom ` E )
	oppcup2.xb	|- .xb = ( comp ` E )
	oppcup2.o	|- O = ( oppCat ` D )
	oppcup2.p	|- P = ( oppCat ` E )
	oppcup2.f	|- ( ph -> F ( D Func E ) G )
	oppcup2.x	|- ( ph -> X ( <. F , tpos G >. ( O UP P ) W ) M )
Assertion	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 ) ) )

Proof

Step	Hyp	Ref	Expression
1		oppcup2.b	|- B = ( Base ` D )
2		oppcup2.h	|- H = ( Hom ` D )
3		oppcup2.j	|- J = ( Hom ` E )
4		oppcup2.xb	|- .xb = ( comp ` E )
5		oppcup2.o	|- O = ( oppCat ` D )
6		oppcup2.p	|- P = ( oppCat ` E )
7		oppcup2.f	|- ( ph -> F ( D Func E ) G )
8		oppcup2.x	|- ( ph -> X ( <. F , tpos G >. ( O UP P ) W ) M )
9		eqid	|- ( Base ` E ) = ( Base ` E )
10	8 6 9	oppcuprcl3	|- ( ph -> W e. ( Base ` E ) )
11	8 5 1	oppcuprcl4	|- ( ph -> X e. B )
12	8 6 3	oppcuprcl5	|- ( ph -> M e. ( ( F ` X ) J W ) )
13	1 9 2 3 4 10 7 11 12 5 6	oppcup	|- ( 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 ) ) ) )
14	8 13	mpbid	|- ( 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 ) ) )