Theorem upeu3

Description: The universal pair <. X , M >. from object W to functor <. F , G >. is essentially unique (strong form) if it exists. (Contributed by Zhi Wang, 24-Sep-2025)

	Ref	Expression
Hypotheses	upeu3.i	$$⊢\phi \to I=\mathrm{Iso}\left(D\right)$$
	upeu3.o	No typesetting found for |- ( ph -> .o. = ( <. W , ( F ` X ) >. ( comp ` E ) ( F ` Y ) ) ) with typecode |-
	upeu3.x	No typesetting found for |- ( ph -> X ( <. F , G >. ( D UP E ) W ) M ) with typecode |-
	upeu3.y	No typesetting found for |- ( ph -> Y ( <. F , G >. ( D UP E ) W ) N ) with typecode |-
Assertion	upeu3	Could not format assertion : No typesetting found for |- ( ph -> E! r e. ( X I Y ) N = ( ( ( X G Y ) ` r ) .o. M ) ) with typecode |-

Proof

Step	Hyp	Ref	Expression
1		upeu3.i	$$⊢\phi \to I=\mathrm{Iso}\left(D\right)$$
2		upeu3.o	Could not format ( ph -> .o. = ( <. W , ( F ` X ) >. ( comp ` E ) ( F ` Y ) ) ) : No typesetting found for |- ( ph -> .o. = ( <. W , ( F ` X ) >. ( comp ` E ) ( F ` Y ) ) ) with typecode |-
3		upeu3.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 |-
4		upeu3.y	Could not format ( ph -> Y ( <. F , G >. ( D UP E ) W ) N ) : No typesetting found for |- ( ph -> Y ( <. F , G >. ( D UP E ) W ) N ) with typecode |-
5		eqid	$$⊢{\mathrm{Base}}_D={\mathrm{Base}}_D$$
6		eqid	$$⊢{\mathrm{Base}}_E={\mathrm{Base}}_E$$
7		eqid	$$⊢\mathrm{Hom}\left(D\right)=\mathrm{Hom}\left(D\right)$$
8		eqid	$$⊢\mathrm{Hom}\left(E\right)=\mathrm{Hom}\left(E\right)$$
9		eqid	$$⊢\mathrm{comp}\left(E\right)=\mathrm{comp}\left(E\right)$$
10	3	uprcl2	$$⊢\phi \to F\left(D\mathrm{Func}E\right)G$$
11	3 5	uprcl4	$$⊢\phi \to X\in {\mathrm{Base}}_D$$
12	4 5	uprcl4	$$⊢\phi \to Y\in {\mathrm{Base}}_D$$
13	3 6	uprcl3	$$⊢\phi \to W\in {\mathrm{Base}}_E$$
14	3 8	uprcl5	$$⊢\phi \to M\in \left(W\mathrm{Hom}\left(E\right)F\left(X\right)\right)$$
15	5 7 8 9 3	isup2	$$⊢\phi \to \forall y\in {\mathrm{Base}}_D\forall g\in \left(W\mathrm{Hom}\left(E\right)F\left(y\right)\right)\exists !k\in \left(X\mathrm{Hom}\left(D\right)y\right)g=\left(XGy\right)\left(k\right)\left(⟨W,F\left(X\right)⟩\mathrm{comp}\left(E\right)F\left(y\right)\right)M$$
16	4 8	uprcl5	$$⊢\phi \to N\in \left(W\mathrm{Hom}\left(E\right)F\left(Y\right)\right)$$
17	5 7 8 9 4	isup2	$$⊢\phi \to \forall y\in {\mathrm{Base}}_D\forall g\in \left(W\mathrm{Hom}\left(E\right)F\left(y\right)\right)\exists !k\in \left(Y\mathrm{Hom}\left(D\right)y\right)g=\left(YGy\right)\left(k\right)\left(⟨W,F\left(Y\right)⟩\mathrm{comp}\left(E\right)F\left(y\right)\right)N$$
18	5 6 7 8 9 10 11 12 13 14 15 16 17	upeu	$$⊢\phi \to \exists !r\in \left(X\mathrm{Iso}\left(D\right)Y\right)N=\left(XGY\right)\left(r\right)\left(⟨W,F\left(X\right)⟩\mathrm{comp}\left(E\right)F\left(Y\right)\right)M$$
19	1	oveqd	$$⊢\phi \to XIY=X\mathrm{Iso}\left(D\right)Y$$
20	2	oveqd	Could not format ( ph -> ( ( ( X G Y ) ` r ) .o. M ) = ( ( ( X G Y ) ` r ) ( <. W , ( F ` X ) >. ( comp ` E ) ( F ` Y ) ) M ) ) : No typesetting found for |- ( ph -> ( ( ( X G Y ) ` r ) .o. M ) = ( ( ( X G Y ) ` r ) ( <. W , ( F ` X ) >. ( comp ` E ) ( F ` Y ) ) M ) ) with typecode |-
21	20	eqeq2d	Could not format ( ph -> ( N = ( ( ( X G Y ) ` r ) .o. M ) <-> N = ( ( ( X G Y ) ` r ) ( <. W , ( F ` X ) >. ( comp ` E ) ( F ` Y ) ) M ) ) ) : No typesetting found for |- ( ph -> ( N = ( ( ( X G Y ) ` r ) .o. M ) <-> N = ( ( ( X G Y ) ` r ) ( <. W , ( F ` X ) >. ( comp ` E ) ( F ` Y ) ) M ) ) ) with typecode |-
22	19 21	reueqbidv	Could not format ( ph -> ( E! r e. ( X I Y ) N = ( ( ( X G Y ) ` r ) .o. M ) <-> E! r e. ( X ( Iso ` D ) Y ) N = ( ( ( X G Y ) ` r ) ( <. W , ( F ` X ) >. ( comp ` E ) ( F ` Y ) ) M ) ) ) : No typesetting found for |- ( ph -> ( E! r e. ( X I Y ) N = ( ( ( X G Y ) ` r ) .o. M ) <-> E! r e. ( X ( Iso ` D ) Y ) N = ( ( ( X G Y ) ` r ) ( <. W , ( F ` X ) >. ( comp ` E ) ( F ` Y ) ) M ) ) ) with typecode |-
23	18 22	mpbird	Could not format ( ph -> E! r e. ( X I Y ) N = ( ( ( X G Y ) ` r ) .o. M ) ) : No typesetting found for |- ( ph -> E! r e. ( X I Y ) N = ( ( ( X G Y ) ` r ) .o. M ) ) with typecode |-