isup

Description: The predicate "is a universal pair". (Contributed by Zhi Wang, 24-Sep-2025)

	Ref	Expression
Hypotheses	upfval.b	$⊢ B = {Base}_{D}$
	upfval.c	$⊢ C = {Base}_{E}$
	upfval.h	$⊢ H = Hom (D)$
	upfval.j	$⊢ J = Hom (E)$
	upfval.o	$⊢ O = comp (E)$
	upfval2.w	$⊢ φ \to W \in C$
	upfval3.f	$⊢ φ \to F (D Func E) G$
	isup.x	$⊢ φ \to X \in B$
	isup.m	$⊢ φ \to M \in (W J F (X))$
Assertion	isup	Could not format assertion : No typesetting found for \|- ( ph -> ( X ( <. F , G >. ( D UP E ) W ) M <-> A. y e. B A. g e. ( W J ( F ` y ) ) E! k e. ( X H y ) g = ( ( ( X G y ) ` k ) ( <. W , ( F ` X ) >. O ( F ` y ) ) M ) ) ) with typecode \|-

Step	Hyp	Ref	Expression
1		upfval.b	$⊢ B = {Base}_{D}$
2		upfval.c	$⊢ C = {Base}_{E}$
3		upfval.h	$⊢ H = Hom (D)$
4		upfval.j	$⊢ J = Hom (E)$
5		upfval.o	$⊢ O = comp (E)$
6		upfval2.w	$⊢ φ \to W \in C$
7		upfval3.f	$⊢ φ \to F (D Func E) G$
8		isup.x	$⊢ φ \to X \in B$
9		isup.m	$⊢ φ \to M \in (W J F (X))$
10	8 9	jca	$⊢ φ \to (X \in B \land M \in (W J F (X)))$
11	1 2 3 4 5 6 7	isuplem	Could not format ( ph -> ( X ( <. F , G >. ( D UP E ) W ) M <-> ( ( X e. B /\ M e. ( W J ( F ` X ) ) ) /\ A. y e. B A. g e. ( W J ( F ` y ) ) E! k e. ( X H y ) g = ( ( ( X G y ) ` k ) ( <. W , ( F ` X ) >. O ( F ` y ) ) M ) ) ) ) : No typesetting found for \|- ( ph -> ( X ( <. F , G >. ( D UP E ) W ) M <-> ( ( X e. B /\ M e. ( W J ( F ` X ) ) ) /\ A. y e. B A. g e. ( W J ( F ` y ) ) E! k e. ( X H y ) g = ( ( ( X G y ) ` k ) ( <. W , ( F ` X ) >. O ( F ` y ) ) M ) ) ) ) with typecode \|-
12	10 11	mpbirand	Could not format ( ph -> ( X ( <. F , G >. ( D UP E ) W ) M <-> A. y e. B A. g e. ( W J ( F ` y ) ) E! k e. ( X H y ) g = ( ( ( X G y ) ` k ) ( <. W , ( F ` X ) >. O ( F ` y ) ) M ) ) ) : No typesetting found for \|- ( ph -> ( X ( <. F , G >. ( D UP E ) W ) M <-> A. y e. B A. g e. ( W J ( F ` y ) ) E! k e. ( X H y ) g = ( ( ( X G y ) ` k ) ( <. W , ( F ` X ) >. O ( F ` y ) ) M ) ) ) with typecode \|-

Metamath Proof Explorer