Metamath Proof Explorer

Theorem fuco22natlem2

Description: Lemma for fuco22nat . The commutative square of natural transformation B in category E , combined with the commutative square of fuco22natlem1 . (Contributed by Zhi Wang, 30-Sep-2025)

Ref Expression
Hypotheses fuco22natlem1.x ⊢ φ → X ∈ Base C
fuco22natlem1.y ⊢ φ → Y ∈ Base C
fuco22natlem1.a ⊢ φ → A ∈ F G C Nat D M N
fuco22natlem1.h ⊢ φ → H ∈ X Hom ⁡ C Y
fuco22natlem2.b ⊢ φ → B ∈ K L D Nat E R S
Assertion fuco22natlem2 ⊢ φ → B ⁡ M ⁡ Y K ⁡ F ⁡ Y K ⁡ M ⁡ Y comp ⁡ E R ⁡ M ⁡ Y F ⁡ Y L M ⁡ Y ⁡ A ⁡ Y K ⁡ F ⁡ X K ⁡ F ⁡ Y comp ⁡ E R ⁡ M ⁡ Y F ⁡ X L F ⁡ Y ⁡ X G Y ⁡ H = M ⁡ X S M ⁡ Y ⁡ X N Y ⁡ H K ⁡ F ⁡ X R ⁡ M ⁡ X comp ⁡ E R ⁡ M ⁡ Y B ⁡ M ⁡ X K ⁡ F ⁡ X K ⁡ M ⁡ X comp ⁡ E R ⁡ M ⁡ X F ⁡ X L M ⁡ X ⁡ A ⁡ X

Proof

Step Hyp Ref Expression
1 fuco22natlem1.x ⊢ φ → X ∈ Base C
2 fuco22natlem1.y ⊢ φ → Y ∈ Base C
3 fuco22natlem1.a ⊢ φ → A ∈ F G C Nat D M N
4 fuco22natlem1.h ⊢ φ → H ∈ X Hom ⁡ C Y
5 fuco22natlem2.b ⊢ φ → B ∈ K L D Nat E R S
6 eqid ⊢ Base E = Base E
7 eqid ⊢ Hom ⁡ E = Hom ⁡ E
8 eqid ⊢ comp ⁡ E = comp ⁡ E
9 eqid ⊢ D Nat E = D Nat E
10 9 5 natrcl2 ⊢ φ → K D Func E L
11 10 funcrcl3 ⊢ φ → E ∈ Cat
12 eqid ⊢ Base D = Base D
13 12 6 10 funcf1 ⊢ φ → K : Base D ⟶ Base E
14 eqid ⊢ Base C = Base C
15 eqid ⊢ C Nat D = C Nat D
16 15 3 natrcl2 ⊢ φ → F C Func D G
17 14 12 16 funcf1 ⊢ φ → F : Base C ⟶ Base D
18 17 1 ffvelcdmd ⊢ φ → F ⁡ X ∈ Base D
19 13 18 ffvelcdmd ⊢ φ → K ⁡ F ⁡ X ∈ Base E
20 17 2 ffvelcdmd ⊢ φ → F ⁡ Y ∈ Base D
21 13 20 ffvelcdmd ⊢ φ → K ⁡ F ⁡ Y ∈ Base E
22 15 3 natrcl3 ⊢ φ → M C Func D N
23 14 12 22 funcf1 ⊢ φ → M : Base C ⟶ Base D
24 23 2 ffvelcdmd ⊢ φ → M ⁡ Y ∈ Base D
25 13 24 ffvelcdmd ⊢ φ → K ⁡ M ⁡ Y ∈ Base E
26 eqid ⊢ Hom ⁡ D = Hom ⁡ D
27 12 26 7 10 18 20 funcf2 ⊢ φ → F ⁡ X L F ⁡ Y : F ⁡ X Hom ⁡ D F ⁡ Y ⟶ K ⁡ F ⁡ X Hom ⁡ E K ⁡ F ⁡ Y
28 eqid ⊢ Hom ⁡ C = Hom ⁡ C
29 14 28 26 16 1 2 funcf2 ⊢ φ → X G Y : X Hom ⁡ C Y ⟶ F ⁡ X Hom ⁡ D F ⁡ Y
30 29 4 ffvelcdmd ⊢ φ → X G Y ⁡ H ∈ F ⁡ X Hom ⁡ D F ⁡ Y
31 27 30 ffvelcdmd ⊢ φ → F ⁡ X L F ⁡ Y ⁡ X G Y ⁡ H ∈ K ⁡ F ⁡ X Hom ⁡ E K ⁡ F ⁡ Y
32 12 26 7 10 20 24 funcf2 ⊢ φ → F ⁡ Y L M ⁡ Y : F ⁡ Y Hom ⁡ D M ⁡ Y ⟶ K ⁡ F ⁡ Y Hom ⁡ E K ⁡ M ⁡ Y
33 15 3 14 26 2 natcl ⊢ φ → A ⁡ Y ∈ F ⁡ Y Hom ⁡ D M ⁡ Y
34 32 33 ffvelcdmd ⊢ φ → F ⁡ Y L M ⁡ Y ⁡ A ⁡ Y ∈ K ⁡ F ⁡ Y Hom ⁡ E K ⁡ M ⁡ Y
35 9 5 natrcl3 ⊢ φ → R D Func E S
36 12 6 35 funcf1 ⊢ φ → R : Base D ⟶ Base E
37 36 24 ffvelcdmd ⊢ φ → R ⁡ M ⁡ Y ∈ Base E
38 9 5 12 7 24 natcl ⊢ φ → B ⁡ M ⁡ Y ∈ K ⁡ M ⁡ Y Hom ⁡ E R ⁡ M ⁡ Y
39 6 7 8 11 19 21 25 31 34 37 38 catass ⊢ φ → B ⁡ M ⁡ Y K ⁡ F ⁡ Y K ⁡ M ⁡ Y comp ⁡ E R ⁡ M ⁡ Y F ⁡ Y L M ⁡ Y ⁡ A ⁡ Y K ⁡ F ⁡ X K ⁡ F ⁡ Y comp ⁡ E R ⁡ M ⁡ Y F ⁡ X L F ⁡ Y ⁡ X G Y ⁡ H = B ⁡ M ⁡ Y K ⁡ F ⁡ X K ⁡ M ⁡ Y comp ⁡ E R ⁡ M ⁡ Y F ⁡ Y L M ⁡ Y ⁡ A ⁡ Y K ⁡ F ⁡ X K ⁡ F ⁡ Y comp ⁡ E K ⁡ M ⁡ Y F ⁡ X L F ⁡ Y ⁡ X G Y ⁡ H
40 1 2 3 4 10 fuco22natlem1 ⊢ φ → F ⁡ Y L M ⁡ Y ⁡ A ⁡ Y K ⁡ F ⁡ X K ⁡ F ⁡ Y comp ⁡ E K ⁡ M ⁡ Y F ⁡ X L F ⁡ Y ⁡ X G Y ⁡ H = M ⁡ X L M ⁡ Y ⁡ X N Y ⁡ H K ⁡ F ⁡ X K ⁡ M ⁡ X comp ⁡ E K ⁡ M ⁡ Y F ⁡ X L M ⁡ X ⁡ A ⁡ X
41 40 oveq2d ⊢ φ → B ⁡ M ⁡ Y K ⁡ F ⁡ X K ⁡ M ⁡ Y comp ⁡ E R ⁡ M ⁡ Y F ⁡ Y L M ⁡ Y ⁡ A ⁡ Y K ⁡ F ⁡ X K ⁡ F ⁡ Y comp ⁡ E K ⁡ M ⁡ Y F ⁡ X L F ⁡ Y ⁡ X G Y ⁡ H = B ⁡ M ⁡ Y K ⁡ F ⁡ X K ⁡ M ⁡ Y comp ⁡ E R ⁡ M ⁡ Y M ⁡ X L M ⁡ Y ⁡ X N Y ⁡ H K ⁡ F ⁡ X K ⁡ M ⁡ X comp ⁡ E K ⁡ M ⁡ Y F ⁡ X L M ⁡ X ⁡ A ⁡ X
42 23 1 ffvelcdmd ⊢ φ → M ⁡ X ∈ Base D
43 14 28 26 22 1 2 funcf2 ⊢ φ → X N Y : X Hom ⁡ C Y ⟶ M ⁡ X Hom ⁡ D M ⁡ Y
44 43 4 ffvelcdmd ⊢ φ → X N Y ⁡ H ∈ M ⁡ X Hom ⁡ D M ⁡ Y
45 9 5 12 26 8 42 24 44 nati ⊢ φ → B ⁡ M ⁡ Y K ⁡ M ⁡ X K ⁡ M ⁡ Y comp ⁡ E R ⁡ M ⁡ Y M ⁡ X L M ⁡ Y ⁡ X N Y ⁡ H = M ⁡ X S M ⁡ Y ⁡ X N Y ⁡ H K ⁡ M ⁡ X R ⁡ M ⁡ X comp ⁡ E R ⁡ M ⁡ Y B ⁡ M ⁡ X
46 45 oveq1d ⊢ φ → B ⁡ M ⁡ Y K ⁡ M ⁡ X K ⁡ M ⁡ Y comp ⁡ E R ⁡ M ⁡ Y M ⁡ X L M ⁡ Y ⁡ X N Y ⁡ H K ⁡ F ⁡ X K ⁡ M ⁡ X comp ⁡ E R ⁡ M ⁡ Y F ⁡ X L M ⁡ X ⁡ A ⁡ X = M ⁡ X S M ⁡ Y ⁡ X N Y ⁡ H K ⁡ M ⁡ X R ⁡ M ⁡ X comp ⁡ E R ⁡ M ⁡ Y B ⁡ M ⁡ X K ⁡ F ⁡ X K ⁡ M ⁡ X comp ⁡ E R ⁡ M ⁡ Y F ⁡ X L M ⁡ X ⁡ A ⁡ X
47 13 42 ffvelcdmd ⊢ φ → K ⁡ M ⁡ X ∈ Base E
48 12 26 7 10 18 42 funcf2 ⊢ φ → F ⁡ X L M ⁡ X : F ⁡ X Hom ⁡ D M ⁡ X ⟶ K ⁡ F ⁡ X Hom ⁡ E K ⁡ M ⁡ X
49 15 3 14 26 1 natcl ⊢ φ → A ⁡ X ∈ F ⁡ X Hom ⁡ D M ⁡ X
50 48 49 ffvelcdmd ⊢ φ → F ⁡ X L M ⁡ X ⁡ A ⁡ X ∈ K ⁡ F ⁡ X Hom ⁡ E K ⁡ M ⁡ X
51 12 26 7 10 42 24 funcf2 ⊢ φ → M ⁡ X L M ⁡ Y : M ⁡ X Hom ⁡ D M ⁡ Y ⟶ K ⁡ M ⁡ X Hom ⁡ E K ⁡ M ⁡ Y
52 51 44 ffvelcdmd ⊢ φ → M ⁡ X L M ⁡ Y ⁡ X N Y ⁡ H ∈ K ⁡ M ⁡ X Hom ⁡ E K ⁡ M ⁡ Y
53 6 7 8 11 19 47 25 50 52 37 38 catass ⊢ φ → B ⁡ M ⁡ Y K ⁡ M ⁡ X K ⁡ M ⁡ Y comp ⁡ E R ⁡ M ⁡ Y M ⁡ X L M ⁡ Y ⁡ X N Y ⁡ H K ⁡ F ⁡ X K ⁡ M ⁡ X comp ⁡ E R ⁡ M ⁡ Y F ⁡ X L M ⁡ X ⁡ A ⁡ X = B ⁡ M ⁡ Y K ⁡ F ⁡ X K ⁡ M ⁡ Y comp ⁡ E R ⁡ M ⁡ Y M ⁡ X L M ⁡ Y ⁡ X N Y ⁡ H K ⁡ F ⁡ X K ⁡ M ⁡ X comp ⁡ E K ⁡ M ⁡ Y F ⁡ X L M ⁡ X ⁡ A ⁡ X
54 36 42 ffvelcdmd ⊢ φ → R ⁡ M ⁡ X ∈ Base E
55 9 5 12 7 42 natcl ⊢ φ → B ⁡ M ⁡ X ∈ K ⁡ M ⁡ X Hom ⁡ E R ⁡ M ⁡ X
56 12 26 7 35 42 24 funcf2 ⊢ φ → M ⁡ X S M ⁡ Y : M ⁡ X Hom ⁡ D M ⁡ Y ⟶ R ⁡ M ⁡ X Hom ⁡ E R ⁡ M ⁡ Y
57 56 44 ffvelcdmd ⊢ φ → M ⁡ X S M ⁡ Y ⁡ X N Y ⁡ H ∈ R ⁡ M ⁡ X Hom ⁡ E R ⁡ M ⁡ Y
58 6 7 8 11 19 47 54 50 55 37 57 catass ⊢ φ → M ⁡ X S M ⁡ Y ⁡ X N Y ⁡ H K ⁡ M ⁡ X R ⁡ M ⁡ X comp ⁡ E R ⁡ M ⁡ Y B ⁡ M ⁡ X K ⁡ F ⁡ X K ⁡ M ⁡ X comp ⁡ E R ⁡ M ⁡ Y F ⁡ X L M ⁡ X ⁡ A ⁡ X = M ⁡ X S M ⁡ Y ⁡ X N Y ⁡ H K ⁡ F ⁡ X R ⁡ M ⁡ X comp ⁡ E R ⁡ M ⁡ Y B ⁡ M ⁡ X K ⁡ F ⁡ X K ⁡ M ⁡ X comp ⁡ E R ⁡ M ⁡ X F ⁡ X L M ⁡ X ⁡ A ⁡ X
59 46 53 58 3eqtr3d ⊢ φ → B ⁡ M ⁡ Y K ⁡ F ⁡ X K ⁡ M ⁡ Y comp ⁡ E R ⁡ M ⁡ Y M ⁡ X L M ⁡ Y ⁡ X N Y ⁡ H K ⁡ F ⁡ X K ⁡ M ⁡ X comp ⁡ E K ⁡ M ⁡ Y F ⁡ X L M ⁡ X ⁡ A ⁡ X = M ⁡ X S M ⁡ Y ⁡ X N Y ⁡ H K ⁡ F ⁡ X R ⁡ M ⁡ X comp ⁡ E R ⁡ M ⁡ Y B ⁡ M ⁡ X K ⁡ F ⁡ X K ⁡ M ⁡ X comp ⁡ E R ⁡ M ⁡ X F ⁡ X L M ⁡ X ⁡ A ⁡ X
60 39 41 59 3eqtrd ⊢ φ → B ⁡ M ⁡ Y K ⁡ F ⁡ Y K ⁡ M ⁡ Y comp ⁡ E R ⁡ M ⁡ Y F ⁡ Y L M ⁡ Y ⁡ A ⁡ Y K ⁡ F ⁡ X K ⁡ F ⁡ Y comp ⁡ E R ⁡ M ⁡ Y F ⁡ X L F ⁡ Y ⁡ X G Y ⁡ H = M ⁡ X S M ⁡ Y ⁡ X N Y ⁡ H K ⁡ F ⁡ X R ⁡ M ⁡ X comp ⁡ E R ⁡ M ⁡ Y B ⁡ M ⁡ X K ⁡ F ⁡ X K ⁡ M ⁡ X comp ⁡ E R ⁡ M ⁡ X F ⁡ X L M ⁡ X ⁡ A ⁡ X