Theorem isup2

Description: The universal property of a universal pair. (Contributed by Zhi Wang, 24-Sep-2025)

	Ref	Expression
Hypotheses	isup2.b	$$⊢B={\mathrm{Base}}_D$$
	isup2.h	$$⊢H=\mathrm{Hom}\left(D\right)$$
	isup2.j	$$⊢J=\mathrm{Hom}\left(E\right)$$
	isup2.o	$$⊢O=\mathrm{comp}\left(E\right)$$
	isup2.x	No typesetting found for |- ( ph -> X ( <. F , G >. ( D UP E ) W ) M ) with typecode |-
Assertion	isup2	$$⊢\phi \to \forall y\in B\forall g\in \left(WJF\left(y\right)\right)\exists !k\in \left(XHy\right)g=\left(XGy\right)\left(k\right)\left(⟨W,F\left(X\right)⟩OF\left(y\right)\right)M$$

Proof

Step	Hyp	Ref	Expression
1		isup2.b	$$⊢B={\mathrm{Base}}_D$$
2		isup2.h	$$⊢H=\mathrm{Hom}\left(D\right)$$
3		isup2.j	$$⊢J=\mathrm{Hom}\left(E\right)$$
4		isup2.o	$$⊢O=\mathrm{comp}\left(E\right)$$
5		isup2.x	Could not format ( ph -> X ( <. F , G >. ( D UP E ) W ) M ) : No typesetting found for |- ( ph -> X ( <. F , G >. ( D UP E ) W ) M ) with typecode |-
6		eqid	$$⊢{\mathrm{Base}}_E={\mathrm{Base}}_E$$
7	5 6	uprcl3	$$⊢\phi \to W\in {\mathrm{Base}}_E$$
8	5	uprcl2	$$⊢\phi \to F\left(D\mathrm{Func}E\right)G$$
9	5 1	uprcl4	$$⊢\phi \to X\in B$$
10	5 3	uprcl5	$$⊢\phi \to M\in \left(WJF\left(X\right)\right)$$
11	1 6 2 3 4 7 8 9 10	isup	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 |-
12	5 11	mpbid	$$⊢\phi \to \forall y\in B\forall g\in \left(WJF\left(y\right)\right)\exists !k\in \left(XHy\right)g=\left(XGy\right)\left(k\right)\left(⟨W,F\left(X\right)⟩OF\left(y\right)\right)M$$