Metamath Proof Explorer

Theorem upeu2

Description: Generate new universal morphism through isomorphism from existing universal object. (Contributed by Zhi Wang, 20-Sep-2025)

Ref Expression
Hypotheses upcic.b ⊢ B = Base D
upcic.c ⊢ C = Base E
upcic.h ⊢ H = Hom ⁡ D
upcic.j ⊢ J = Hom ⁡ E
upcic.o ⊢ O = comp ⁡ E
upcic.f ⊢ φ → F D Func E G
upcic.x ⊢ φ → X ∈ B
upcic.y ⊢ φ → Y ∈ B
upcic.z ⊢ φ → Z ∈ C
upcic.m ⊢ φ → M ∈ Z J F ⁡ X
upcic.1 ⊢ φ → ∀ w ∈ B ∀ f ∈ Z J F ⁡ w ∃! k ∈ X H w f = X G w ⁡ k Z F ⁡ X O F ⁡ w M
upeu2.i ⊢ I = Iso ⁡ D
upeu2.k ⊢ φ → K ∈ X I Y
upeu2.n ⊢ φ → N = X G Y ⁡ K Z F ⁡ X O F ⁡ Y M
Assertion upeu2 ⊢ φ → N ∈ Z J F ⁡ Y ∧ ∀ v ∈ B ∀ g ∈ Z J F ⁡ v ∃! l ∈ Y H v g = Y G v ⁡ l Z F ⁡ Y O F ⁡ v N

Proof

Step Hyp Ref Expression
1 upcic.b ⊢ B = Base D
2 upcic.c ⊢ C = Base E
3 upcic.h ⊢ H = Hom ⁡ D
4 upcic.j ⊢ J = Hom ⁡ E
5 upcic.o ⊢ O = comp ⁡ E
6 upcic.f ⊢ φ → F D Func E G
7 upcic.x ⊢ φ → X ∈ B
8 upcic.y ⊢ φ → Y ∈ B
9 upcic.z ⊢ φ → Z ∈ C
10 upcic.m ⊢ φ → M ∈ Z J F ⁡ X
11 upcic.1 ⊢ φ → ∀ w ∈ B ∀ f ∈ Z J F ⁡ w ∃! k ∈ X H w f = X G w ⁡ k Z F ⁡ X O F ⁡ w M
12 upeu2.i ⊢ I = Iso ⁡ D
13 upeu2.k ⊢ φ → K ∈ X I Y
14 upeu2.n ⊢ φ → N = X G Y ⁡ K Z F ⁡ X O F ⁡ Y M
15 6 funcrcl3 ⊢ φ → E ∈ Cat
16 1 2 6 funcf1 ⊢ φ → F : B ⟶ C
17 16 7 ffvelcdmd ⊢ φ → F ⁡ X ∈ C
18 16 8 ffvelcdmd ⊢ φ → F ⁡ Y ∈ C
19 1 3 4 6 7 8 funcf2 ⊢ φ → X G Y : X H Y ⟶ F ⁡ X J F ⁡ Y
20 6 funcrcl2 ⊢ φ → D ∈ Cat
21 1 3 12 20 7 8 isohom ⊢ φ → X I Y ⊆ X H Y
22 21 13 sseldd ⊢ φ → K ∈ X H Y
23 19 22 ffvelcdmd ⊢ φ → X G Y ⁡ K ∈ F ⁡ X J F ⁡ Y
24 2 4 5 15 9 17 18 10 23 catcocl ⊢ φ → X G Y ⁡ K Z F ⁡ X O F ⁡ Y M ∈ Z J F ⁡ Y
25 14 24 eqeltrd ⊢ φ → N ∈ Z J F ⁡ Y
26 11 adantr ⊢ φ ∧ v ∈ B ∧ g ∈ Z J F ⁡ v → ∀ w ∈ B ∀ f ∈ Z J F ⁡ w ∃! k ∈ X H w f = X G w ⁡ k Z F ⁡ X O F ⁡ w M
27 simprl ⊢ φ ∧ v ∈ B ∧ g ∈ Z J F ⁡ v → v ∈ B
28 simprr ⊢ φ ∧ v ∈ B ∧ g ∈ Z J F ⁡ v → g ∈ Z J F ⁡ v
29 26 27 28 upciclem1 ⊢ φ ∧ v ∈ B ∧ g ∈ Z J F ⁡ v → ∃! p ∈ X H v g = X G v ⁡ p Z F ⁡ X O F ⁡ v M
30 eqid ⊢ comp ⁡ D = comp ⁡ D
31 20 ad2antrr ⊢ φ ∧ v ∈ B ∧ g ∈ Z J F ⁡ v ∧ l ∈ Y H v → D ∈ Cat
32 7 ad2antrr ⊢ φ ∧ v ∈ B ∧ g ∈ Z J F ⁡ v ∧ l ∈ Y H v → X ∈ B
33 8 ad2antrr ⊢ φ ∧ v ∈ B ∧ g ∈ Z J F ⁡ v ∧ l ∈ Y H v → Y ∈ B
34 27 adantr ⊢ φ ∧ v ∈ B ∧ g ∈ Z J F ⁡ v ∧ l ∈ Y H v → v ∈ B
35 22 ad2antrr ⊢ φ ∧ v ∈ B ∧ g ∈ Z J F ⁡ v ∧ l ∈ Y H v → K ∈ X H Y
36 simpr ⊢ φ ∧ v ∈ B ∧ g ∈ Z J F ⁡ v ∧ l ∈ Y H v → l ∈ Y H v
37 1 3 30 31 32 33 34 35 36 catcocl ⊢ φ ∧ v ∈ B ∧ g ∈ Z J F ⁡ v ∧ l ∈ Y H v → l X Y comp ⁡ D v K ∈ X H v
38 20 ad2antrr ⊢ φ ∧ v ∈ B ∧ g ∈ Z J F ⁡ v ∧ p ∈ X H v → D ∈ Cat
39 7 ad2antrr ⊢ φ ∧ v ∈ B ∧ g ∈ Z J F ⁡ v ∧ p ∈ X H v → X ∈ B
40 8 ad2antrr ⊢ φ ∧ v ∈ B ∧ g ∈ Z J F ⁡ v ∧ p ∈ X H v → Y ∈ B
41 27 adantr ⊢ φ ∧ v ∈ B ∧ g ∈ Z J F ⁡ v ∧ p ∈ X H v → v ∈ B
42 13 ad2antrr ⊢ φ ∧ v ∈ B ∧ g ∈ Z J F ⁡ v ∧ p ∈ X H v → K ∈ X I Y
43 simpr ⊢ φ ∧ v ∈ B ∧ g ∈ Z J F ⁡ v ∧ p ∈ X H v → p ∈ X H v
44 1 3 30 12 38 39 40 41 42 43 upeu2lem ⊢ φ ∧ v ∈ B ∧ g ∈ Z J F ⁡ v ∧ p ∈ X H v → ∃! l ∈ Y H v p = l X Y comp ⁡ D v K
45 simprr ⊢ φ ∧ v ∈ B ∧ g ∈ Z J F ⁡ v ∧ l ∈ Y H v ∧ p = l X Y comp ⁡ D v K → p = l X Y comp ⁡ D v K
46 45 fveq2d ⊢ φ ∧ v ∈ B ∧ g ∈ Z J F ⁡ v ∧ l ∈ Y H v ∧ p = l X Y comp ⁡ D v K → X G v ⁡ p = X G v ⁡ l X Y comp ⁡ D v K
47 46 oveq1d ⊢ φ ∧ v ∈ B ∧ g ∈ Z J F ⁡ v ∧ l ∈ Y H v ∧ p = l X Y comp ⁡ D v K → X G v ⁡ p Z F ⁡ X O F ⁡ v M = X G v ⁡ l X Y comp ⁡ D v K Z F ⁡ X O F ⁡ v M
48 6 ad2antrr ⊢ φ ∧ v ∈ B ∧ g ∈ Z J F ⁡ v ∧ l ∈ Y H v ∧ p = l X Y comp ⁡ D v K → F D Func E G
49 7 ad2antrr ⊢ φ ∧ v ∈ B ∧ g ∈ Z J F ⁡ v ∧ l ∈ Y H v ∧ p = l X Y comp ⁡ D v K → X ∈ B
50 8 ad2antrr ⊢ φ ∧ v ∈ B ∧ g ∈ Z J F ⁡ v ∧ l ∈ Y H v ∧ p = l X Y comp ⁡ D v K → Y ∈ B
51 27 adantr ⊢ φ ∧ v ∈ B ∧ g ∈ Z J F ⁡ v ∧ l ∈ Y H v ∧ p = l X Y comp ⁡ D v K → v ∈ B
52 9 ad2antrr ⊢ φ ∧ v ∈ B ∧ g ∈ Z J F ⁡ v ∧ l ∈ Y H v ∧ p = l X Y comp ⁡ D v K → Z ∈ C
53 10 ad2antrr ⊢ φ ∧ v ∈ B ∧ g ∈ Z J F ⁡ v ∧ l ∈ Y H v ∧ p = l X Y comp ⁡ D v K → M ∈ Z J F ⁡ X
54 22 ad2antrr ⊢ φ ∧ v ∈ B ∧ g ∈ Z J F ⁡ v ∧ l ∈ Y H v ∧ p = l X Y comp ⁡ D v K → K ∈ X H Y
55 simprl ⊢ φ ∧ v ∈ B ∧ g ∈ Z J F ⁡ v ∧ l ∈ Y H v ∧ p = l X Y comp ⁡ D v K → l ∈ Y H v
56 14 ad2antrr ⊢ φ ∧ v ∈ B ∧ g ∈ Z J F ⁡ v ∧ l ∈ Y H v ∧ p = l X Y comp ⁡ D v K → N = X G Y ⁡ K Z F ⁡ X O F ⁡ Y M
57 1 2 3 4 5 48 49 50 51 52 53 30 54 55 56 upciclem2 ⊢ φ ∧ v ∈ B ∧ g ∈ Z J F ⁡ v ∧ l ∈ Y H v ∧ p = l X Y comp ⁡ D v K → X G v ⁡ l X Y comp ⁡ D v K Z F ⁡ X O F ⁡ v M = Y G v ⁡ l Z F ⁡ Y O F ⁡ v N
58 47 57 eqtrd ⊢ φ ∧ v ∈ B ∧ g ∈ Z J F ⁡ v ∧ l ∈ Y H v ∧ p = l X Y comp ⁡ D v K → X G v ⁡ p Z F ⁡ X O F ⁡ v M = Y G v ⁡ l Z F ⁡ Y O F ⁡ v N
59 58 eqeq2d ⊢ φ ∧ v ∈ B ∧ g ∈ Z J F ⁡ v ∧ l ∈ Y H v ∧ p = l X Y comp ⁡ D v K → g = X G v ⁡ p Z F ⁡ X O F ⁡ v M ↔ g = Y G v ⁡ l Z F ⁡ Y O F ⁡ v N
60 37 44 59 reuxfr1dd ⊢ φ ∧ v ∈ B ∧ g ∈ Z J F ⁡ v → ∃! p ∈ X H v g = X G v ⁡ p Z F ⁡ X O F ⁡ v M ↔ ∃! l ∈ Y H v g = Y G v ⁡ l Z F ⁡ Y O F ⁡ v N
61 29 60 mpbid ⊢ φ ∧ v ∈ B ∧ g ∈ Z J F ⁡ v → ∃! l ∈ Y H v g = Y G v ⁡ l Z F ⁡ Y O F ⁡ v N
62 61 ralrimivva ⊢ φ → ∀ v ∈ B ∀ g ∈ Z J F ⁡ v ∃! l ∈ Y H v g = Y G v ⁡ l Z F ⁡ Y O F ⁡ v N
63 25 62 jca ⊢ φ → N ∈ Z J F ⁡ Y ∧ ∀ v ∈ B ∀ g ∈ Z J F ⁡ v ∃! l ∈ Y H v g = Y G v ⁡ l Z F ⁡ Y O F ⁡ v N