This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

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 ) ) )