Metamath Proof Explorer


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 φ 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 |-
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 φ 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 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 Base D = Base D
6 eqid Base E = Base E
7 eqid Hom D = Hom D
8 eqid Hom E = Hom E
9 eqid comp E = comp E
10 3 uprcl2 φ F D Func E G
11 3 5 uprcl4 φ X Base D
12 4 5 uprcl4 φ Y Base D
13 3 6 uprcl3 φ W Base E
14 3 8 uprcl5 φ M W Hom E F X
15 5 7 8 9 3 isup2 φ y Base D g W Hom E F y ∃! k X Hom D y g = X G y k W F X comp E F y M
16 4 8 uprcl5 φ N W Hom E F Y
17 5 7 8 9 4 isup2 φ 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
18 5 6 7 8 9 10 11 12 13 14 15 16 17 upeu φ ∃! r X Iso D Y N = X G Y r W F X comp E F Y M
19 1 oveqd φ X I Y = X Iso D 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 |-