Theorem upeu4

Description: Generate a new universal morphism through an isomorphism from an existing universal object, and pair with the codomain of the isomorphism to form a universal pair. (Contributed by Zhi Wang, 25-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 |-
	upeu4.k	$$⊢\phi \to K\in \left(XIY\right)$$
	upeu4.n	No typesetting found for |- ( ph -> N = ( ( ( X G Y ) ` K ) .o. M ) ) with typecode |-
Assertion	upeu4	Could not format assertion : No typesetting found for |- ( ph -> Y ( <. F , G >. ( D UP E ) W ) N ) 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		upeu4.k	$$⊢\phi \to K\in \left(XIY\right)$$
5		upeu4.n	Could not format ( ph -> N = ( ( ( X G Y ) ` K ) .o. M ) ) : No typesetting found for |- ( ph -> N = ( ( ( X G Y ) ` K ) .o. M ) ) with typecode |-
6		eqid	$$⊢{\mathrm{Base}}_D={\mathrm{Base}}_D$$
7		eqid	$$⊢{\mathrm{Base}}_E={\mathrm{Base}}_E$$
8		eqid	$$⊢\mathrm{Hom}\left(D\right)=\mathrm{Hom}\left(D\right)$$
9		eqid	$$⊢\mathrm{Hom}\left(E\right)=\mathrm{Hom}\left(E\right)$$
10		eqid	$$⊢\mathrm{comp}\left(E\right)=\mathrm{comp}\left(E\right)$$
11	3	uprcl2	$$⊢\phi \to F\left(D\mathrm{Func}E\right)G$$
12	3 6	uprcl4	$$⊢\phi \to X\in {\mathrm{Base}}_D$$
13	11	funcrcl2	$$⊢\phi \to D\in \mathrm{Cat}$$
14		isofn	$$⊢D\in \mathrm{Cat}\to \mathrm{Iso}\left(D\right)Fn\left({\mathrm{Base}}_D\times {\mathrm{Base}}_D\right)$$
15	13 14	syl	$$⊢\phi \to \mathrm{Iso}\left(D\right)Fn\left({\mathrm{Base}}_D\times {\mathrm{Base}}_D\right)$$
16	1	fneq1d	$$⊢\phi \to \left(IFn\left({\mathrm{Base}}_D\times {\mathrm{Base}}_D\right)\leftrightarrow \mathrm{Iso}\left(D\right)Fn\left({\mathrm{Base}}_D\times {\mathrm{Base}}_D\right)\right)$$
17	15 16	mpbird	$$⊢\phi \to IFn\left({\mathrm{Base}}_D\times {\mathrm{Base}}_D\right)$$
18		fnov	$$⊢IFn\left({\mathrm{Base}}_D\times {\mathrm{Base}}_D\right)\leftrightarrow I=\left(x\in {\mathrm{Base}}_D,y\in {\mathrm{Base}}_D⟼xIy\right)$$
19	17 18	sylib	$$⊢\phi \to I=\left(x\in {\mathrm{Base}}_D,y\in {\mathrm{Base}}_D⟼xIy\right)$$
20	19	oveqd	$$⊢\phi \to XIY=X\left(x\in {\mathrm{Base}}_D,y\in {\mathrm{Base}}_D⟼xIy\right)Y$$
21	4 20	eleqtrd	$$⊢\phi \to K\in \left(X\left(x\in {\mathrm{Base}}_D,y\in {\mathrm{Base}}_D⟼xIy\right)Y\right)$$
22		eqid	$$⊢\left(x\in {\mathrm{Base}}_D,y\in {\mathrm{Base}}_D⟼xIy\right)=\left(x\in {\mathrm{Base}}_D,y\in {\mathrm{Base}}_D⟼xIy\right)$$
23	22	elmpocl2	$$⊢K\in \left(X\left(x\in {\mathrm{Base}}_D,y\in {\mathrm{Base}}_D⟼xIy\right)Y\right)\to Y\in {\mathrm{Base}}_D$$
24	21 23	syl	$$⊢\phi \to Y\in {\mathrm{Base}}_D$$
25	3 7	uprcl3	$$⊢\phi \to W\in {\mathrm{Base}}_E$$
26	3 9	uprcl5	$$⊢\phi \to M\in \left(W\mathrm{Hom}\left(E\right)F\left(X\right)\right)$$
27	6 8 9 10 3	isup2	$$⊢\phi \to \forall x\in {\mathrm{Base}}_D\forall f\in \left(W\mathrm{Hom}\left(E\right)F\left(x\right)\right)\exists !k\in \left(X\mathrm{Hom}\left(D\right)x\right)f=\left(XGx\right)\left(k\right)\left(⟨W,F\left(X\right)⟩\mathrm{comp}\left(E\right)F\left(x\right)\right)M$$
28		eqid	$$⊢\mathrm{Iso}\left(D\right)=\mathrm{Iso}\left(D\right)$$
29	1	oveqd	$$⊢\phi \to XIY=X\mathrm{Iso}\left(D\right)Y$$
30	4 29	eleqtrd	$$⊢\phi \to K\in \left(X\mathrm{Iso}\left(D\right)Y\right)$$
31	2	oveqd	Could not format ( ph -> ( ( ( X G Y ) ` K ) .o. M ) = ( ( ( X G Y ) ` K ) ( <. W , ( F ` X ) >. ( comp ` E ) ( F ` Y ) ) M ) ) : No typesetting found for |- ( ph -> ( ( ( X G Y ) ` K ) .o. M ) = ( ( ( X G Y ) ` K ) ( <. W , ( F ` X ) >. ( comp ` E ) ( F ` Y ) ) M ) ) with typecode |-
32	5 31	eqtrd	$$⊢\phi \to N=\left(XGY\right)\left(K\right)\left(⟨W,F\left(X\right)⟩\mathrm{comp}\left(E\right)F\left(Y\right)\right)M$$
33	6 7 8 9 10 11 12 24 25 26 27 28 30 32	upeu2	$$⊢\phi \to \left(N\in \left(W\mathrm{Hom}\left(E\right)F\left(Y\right)\right)\wedge \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\right)$$
34	33	simprd	$$⊢\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$$
35	33	simpld	$$⊢\phi \to N\in \left(W\mathrm{Hom}\left(E\right)F\left(Y\right)\right)$$
36	6 7 8 9 10 25 11 24 35	isup	Could not format ( ph -> ( Y ( <. F , G >. ( D UP E ) W ) N <-> A. y e. ( Base ` D ) A. g e. ( W ( Hom ` E ) ( F ` y ) ) E! k e. ( Y ( Hom ` D ) y ) g = ( ( ( Y G y ) ` k ) ( <. W , ( F ` Y ) >. ( comp ` E ) ( F ` y ) ) N ) ) ) : No typesetting found for |- ( ph -> ( Y ( <. F , G >. ( D UP E ) W ) N <-> A. y e. ( Base ` D ) A. g e. ( W ( Hom ` E ) ( F ` y ) ) E! k e. ( Y ( Hom ` D ) y ) g = ( ( ( Y G y ) ` k ) ( <. W , ( F ` Y ) >. ( comp ` E ) ( F ` y ) ) N ) ) ) with typecode |-
37	34 36	mpbird	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 |-