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

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