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

Metamath Proof Explorer

Theorem uptrlem2

Description: Lemma for uptr . (Contributed by Zhi Wang, 16-Nov-2025)

Ref Expression
Hypotheses uptrlem1.h ⊢ H = Hom ⁡ C
uptrlem1.i ⊢ I = Hom ⁡ D
uptrlem1.j ⊢ J = Hom ⁡ E
uptrlem1.d ⊢ ∙ ˙ = comp ⁡ D
uptrlem1.e No typesetting found for |- .o. = ( comp ` E ) with typecode |-
uptrlem2.a ⊢ A = Base C
uptrlem2.b ⊢ B = Base D
uptrlem2.x ⊢ φ → X ∈ B
uptrlem2.y ⊢ φ → 1 st ⁡ K ⁡ X = Y
uptrlem2.z ⊢ φ → Z ∈ A
uptrlem2.w ⊢ φ → W ∈ A
uptrlem2.m ⊢ φ → M ∈ X I 1 st ⁡ F ⁡ Z
uptrlem2.n ⊢ φ → X 2 nd ⁡ K 1 st ⁡ F ⁡ Z ⁡ M = N
uptrlem2.f ⊢ φ → F ∈ C Func D
uptrlem2.k ⊢ φ → K ∈ D Full E ∩ D Faith E
uptrlem2.g ⊢ φ → K ∘ func F = G
Assertion uptrlem2 Could not format assertion : No typesetting found for |- ( ph -> ( A. h e. ( Y J ( ( 1st ` G ) ` W ) ) E! k e. ( Z H W ) h = ( ( ( Z ( 2nd ` G ) W ) ` k ) ( <. Y , ( ( 1st ` G ) ` Z ) >. .o. ( ( 1st ` G ) ` W ) ) N ) <-> A. g e. ( X I ( ( 1st ` F ) ` W ) ) E! k e. ( Z H W ) g = ( ( ( Z ( 2nd ` F ) W ) ` k ) ( <. X , ( ( 1st ` F ) ` Z ) >. .xb ( ( 1st ` F ) ` W ) ) M ) ) ) with typecode |-

Proof

Step Hyp Ref Expression
1 uptrlem1.h ⊢ H = Hom ⁡ C
2 uptrlem1.i ⊢ I = Hom ⁡ D
3 uptrlem1.j ⊢ J = Hom ⁡ E
4 uptrlem1.d ⊢ ∙ ˙ = comp ⁡ D
5 uptrlem1.e Could not format .o. = ( comp ` E ) : No typesetting found for |- .o. = ( comp ` E ) with typecode |-
6 uptrlem2.a ⊢ A = Base C
7 uptrlem2.b ⊢ B = Base D
8 uptrlem2.x ⊢ φ → X ∈ B
9 uptrlem2.y ⊢ φ → 1 st ⁡ K ⁡ X = Y
10 uptrlem2.z ⊢ φ → Z ∈ A
11 uptrlem2.w ⊢ φ → W ∈ A
12 uptrlem2.m ⊢ φ → M ∈ X I 1 st ⁡ F ⁡ Z
13 uptrlem2.n ⊢ φ → X 2 nd ⁡ K 1 st ⁡ F ⁡ Z ⁡ M = N
14 uptrlem2.f ⊢ φ → F ∈ C Func D
15 uptrlem2.k ⊢ φ → K ∈ D Full E ∩ D Faith E
16 uptrlem2.g ⊢ φ → K ∘ func F = G
17 8 7 eleqtrdi ⊢ φ → X ∈ Base D
18 10 6 eleqtrdi ⊢ φ → Z ∈ Base C
19 11 6 eleqtrdi ⊢ φ → W ∈ Base C
20 14 func1st2nd ⊢ φ → 1 st ⁡ F C Func D 2 nd ⁡ F
21 relfull ⊢ Rel ⁡ D Full E
22 relin1 ⊢ Rel ⁡ D Full E → Rel ⁡ D Full E ∩ D Faith E
23 21 22 ax-mp ⊢ Rel ⁡ D Full E ∩ D Faith E
24 1st2nd ⊢ Rel ⁡ D Full E ∩ D Faith E ∧ K ∈ D Full E ∩ D Faith E → K = 1 st ⁡ K 2 nd ⁡ K
25 23 15 24 sylancr ⊢ φ → K = 1 st ⁡ K 2 nd ⁡ K
26 25 15 eqeltrrd ⊢ φ → 1 st ⁡ K 2 nd ⁡ K ∈ D Full E ∩ D Faith E
27 df-br ⊢ 1 st ⁡ K D Full E ∩ D Faith E 2 nd ⁡ K ↔ 1 st ⁡ K 2 nd ⁡ K ∈ D Full E ∩ D Faith E
28 26 27 sylibr ⊢ φ → 1 st ⁡ K D Full E ∩ D Faith E 2 nd ⁡ K
29 inss1 ⊢ D Full E ∩ D Faith E ⊆ D Full E
30 fullfunc ⊢ D Full E ⊆ D Func E
31 29 30 sstri ⊢ D Full E ∩ D Faith E ⊆ D Func E
32 31 15 sselid ⊢ φ → K ∈ D Func E
33 14 32 cofu1st2nd ⊢ φ → K ∘ func F = 1 st ⁡ K 2 nd ⁡ K ∘ func 1 st ⁡ F 2 nd ⁡ F
34 relfunc ⊢ Rel ⁡ C Func E
35 14 32 cofucl ⊢ φ → K ∘ func F ∈ C Func E
36 16 35 eqeltrrd ⊢ φ → G ∈ C Func E
37 1st2nd ⊢ Rel ⁡ C Func E ∧ G ∈ C Func E → G = 1 st ⁡ G 2 nd ⁡ G
38 34 36 37 sylancr ⊢ φ → G = 1 st ⁡ G 2 nd ⁡ G
39 16 33 38 3eqtr3d ⊢ φ → 1 st ⁡ K 2 nd ⁡ K ∘ func 1 st ⁡ F 2 nd ⁡ F = 1 st ⁡ G 2 nd ⁡ G
40 1 2 3 4 5 17 9 18 19 12 13 20 28 39 uptrlem1 Could not format ( ph -> ( A. h e. ( Y J ( ( 1st ` G ) ` W ) ) E! k e. ( Z H W ) h = ( ( ( Z ( 2nd ` G ) W ) ` k ) ( <. Y , ( ( 1st ` G ) ` Z ) >. .o. ( ( 1st ` G ) ` W ) ) N ) <-> A. g e. ( X I ( ( 1st ` F ) ` W ) ) E! k e. ( Z H W ) g = ( ( ( Z ( 2nd ` F ) W ) ` k ) ( <. X , ( ( 1st ` F ) ` Z ) >. .xb ( ( 1st ` F ) ` W ) ) M ) ) ) : No typesetting found for |- ( ph -> ( A. h e. ( Y J ( ( 1st ` G ) ` W ) ) E! k e. ( Z H W ) h = ( ( ( Z ( 2nd ` G ) W ) ` k ) ( <. Y , ( ( 1st ` G ) ` Z ) >. .o. ( ( 1st ` G ) ` W ) ) N ) <-> A. g e. ( X I ( ( 1st ` F ) ` W ) ) E! k e. ( Z H W ) g = ( ( ( Z ( 2nd ` F ) W ) ` k ) ( <. X , ( ( 1st ` F ) ` Z ) >. .xb ( ( 1st ` F ) ` W ) ) M ) ) ) with typecode |-