This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

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 |-