Metamath Proof Explorer


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 φ I = Iso D
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 φ K X I Y
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 φ I = Iso D
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 φ K X I Y
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 Base D = Base D
7 eqid Base E = Base E
8 eqid Hom D = Hom D
9 eqid Hom E = Hom E
10 eqid comp E = comp E
11 3 uprcl2 φ F D Func E G
12 3 6 uprcl4 φ X Base D
13 11 funcrcl2 φ D Cat
14 isofn D Cat Iso D Fn Base D × Base D
15 13 14 syl φ Iso D Fn Base D × Base D
16 1 fneq1d φ I Fn Base D × Base D Iso D Fn Base D × Base D
17 15 16 mpbird φ I Fn Base D × Base D
18 fnov I Fn Base D × Base D I = x Base D , y Base D x I y
19 17 18 sylib φ I = x Base D , y Base D x I y
20 19 oveqd φ X I Y = X x Base D , y Base D x I y Y
21 4 20 eleqtrd φ K X x Base D , y Base D x I y Y
22 eqid x Base D , y Base D x I y = x Base D , y Base D x I y
23 22 elmpocl2 K X x Base D , y Base D x I y Y Y Base D
24 21 23 syl φ Y Base D
25 3 7 uprcl3 φ W Base E
26 3 9 uprcl5 φ M W Hom E F X
27 6 8 9 10 3 isup2 φ x Base D f W Hom E F x ∃! k X Hom D x f = X G x k W F X comp E F x M
28 eqid Iso D = Iso D
29 1 oveqd φ X I Y = X Iso D Y
30 4 29 eleqtrd φ K X Iso D Y
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 φ N = X G Y K W F X comp E F Y M
33 6 7 8 9 10 11 12 24 25 26 27 28 30 32 upeu2 φ N W Hom E F Y y Base D g W Hom E F y ∃! k Y Hom D y g = Y G y k W F Y comp E F y N
34 33 simprd φ y Base D g W Hom E F y ∃! k Y Hom D y g = Y G y k W F Y comp E F y N
35 33 simpld φ N W Hom E F Y
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 |-