Theorem isup

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

	Ref	Expression
Hypotheses	upfval.b	$$⊢B={\mathrm{Base}}_D$$
	upfval.c	$$⊢C={\mathrm{Base}}_E$$
	upfval.h	$$⊢H=\mathrm{Hom}\left(D\right)$$
	upfval.j	$$⊢J=\mathrm{Hom}\left(E\right)$$
	upfval.o	$$⊢O=\mathrm{comp}\left(E\right)$$
	upfval2.w	$$⊢\phi \to W\in C$$
	upfval3.f	$$⊢\phi \to F\left(D\mathrm{Func}E\right)G$$
	isup.x	$$⊢\phi \to X\in B$$
	isup.m	$$⊢\phi \to M\in \left(WJF\left(X\right)\right)$$
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 |-

Proof

Step	Hyp	Ref	Expression
1		upfval.b	$$⊢B={\mathrm{Base}}_D$$
2		upfval.c	$$⊢C={\mathrm{Base}}_E$$
3		upfval.h	$$⊢H=\mathrm{Hom}\left(D\right)$$
4		upfval.j	$$⊢J=\mathrm{Hom}\left(E\right)$$
5		upfval.o	$$⊢O=\mathrm{comp}\left(E\right)$$
6		upfval2.w	$$⊢\phi \to W\in C$$
7		upfval3.f	$$⊢\phi \to F\left(D\mathrm{Func}E\right)G$$
8		isup.x	$$⊢\phi \to X\in B$$
9		isup.m	$$⊢\phi \to M\in \left(WJF\left(X\right)\right)$$
10	8 9	jca	$$⊢\phi \to \left(X\in B\wedge M\in \left(WJF\left(X\right)\right)\right)$$
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 |-