Metamath Proof Explorer


Theorem fuco21

Description: The morphism part of the functor composition bifunctor. (Contributed by Zhi Wang, 29-Sep-2025)

Ref Expression
Hypotheses fuco11.o No typesetting found for |- ( ph -> ( <. C , D >. o.F E ) = <. O , P >. ) with typecode |-
fuco11.f φ F C Func D G
fuco11.k φ K D Func E L
fuco11.u φ U = K L F G
fuco21.m φ M C Func D N
fuco21.r φ R D Func E S
fuco21.v φ V = R S M N
Assertion fuco21 φ U P V = b K L D Nat E R S , a F G C Nat D M N x Base C 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 fuco11.o Could not format ( ph -> ( <. C , D >. o.F E ) = <. O , P >. ) : No typesetting found for |- ( ph -> ( <. C , D >. o.F E ) = <. O , P >. ) with typecode |-
2 fuco11.f φ F C Func D G
3 fuco11.k φ K D Func E L
4 fuco11.u φ U = K L F G
5 fuco21.m φ M C Func D N
6 fuco21.r φ R D Func E S
7 fuco21.v φ V = R S M N
8 2 funcrcl2 φ C Cat
9 3 funcrcl2 φ D Cat
10 3 funcrcl3 φ E Cat
11 eqidd φ D Func E × C Func D = D Func E × C Func D
12 8 9 10 1 11 fuco2 φ P = u D Func E × C Func D , v D Func E × C Func D 1 st 2 nd u / f 1 st 1 st u / k 2 nd 1 st u / l 1 st 2 nd v / m 1 st 1 st v / r b 1 st u D Nat E 1 st v , a 2 nd u C Nat D 2 nd v x Base C b m x k f x k m x comp E r m x f x l m x a x
13 fvexd φ u = U v = V 1 st 2 nd u V
14 simprl φ u = U v = V u = U
15 4 adantr φ u = U v = V U = K L F G
16 14 15 eqtrd φ u = U v = V u = K L F G
17 16 fveq2d φ u = U v = V 2 nd u = 2 nd K L F G
18 17 fveq2d φ u = U v = V 1 st 2 nd u = 1 st 2 nd K L F G
19 opex K L V
20 opex F G V
21 19 20 op2nd 2 nd K L F G = F G
22 21 fveq2i 1 st 2 nd K L F G = 1 st F G
23 relfunc Rel C Func D
24 23 brrelex1i F C Func D G F V
25 2 24 syl φ F V
26 23 brrelex2i F C Func D G G V
27 2 26 syl φ G V
28 op1stg F V G V 1 st F G = F
29 25 27 28 syl2anc φ 1 st F G = F
30 22 29 eqtrid φ 1 st 2 nd K L F G = F
31 30 adantr φ u = U v = V 1 st 2 nd K L F G = F
32 18 31 eqtrd φ u = U v = V 1 st 2 nd u = F
33 fvexd φ u = U v = V f = F 1 st 1 st u V
34 14 adantr φ u = U v = V f = F u = U
35 15 adantr φ u = U v = V f = F U = K L F G
36 34 35 eqtrd φ u = U v = V f = F u = K L F G
37 36 fveq2d φ u = U v = V f = F 1 st u = 1 st K L F G
38 37 fveq2d φ u = U v = V f = F 1 st 1 st u = 1 st 1 st K L F G
39 19 20 op1st 1 st K L F G = K L
40 39 fveq2i 1 st 1 st K L F G = 1 st K L
41 relfunc Rel D Func E
42 41 brrelex1i K D Func E L K V
43 3 42 syl φ K V
44 41 brrelex2i K D Func E L L V
45 3 44 syl φ L V
46 op1stg K V L V 1 st K L = K
47 43 45 46 syl2anc φ 1 st K L = K
48 40 47 eqtrid φ 1 st 1 st K L F G = K
49 48 ad2antrr φ u = U v = V f = F 1 st 1 st K L F G = K
50 38 49 eqtrd φ u = U v = V f = F 1 st 1 st u = K
51 fvexd φ u = U v = V f = F k = K 2 nd 1 st u V
52 34 adantr φ u = U v = V f = F k = K u = U
53 35 adantr φ u = U v = V f = F k = K U = K L F G
54 52 53 eqtrd φ u = U v = V f = F k = K u = K L F G
55 54 fveq2d φ u = U v = V f = F k = K 1 st u = 1 st K L F G
56 55 fveq2d φ u = U v = V f = F k = K 2 nd 1 st u = 2 nd 1 st K L F G
57 39 fveq2i 2 nd 1 st K L F G = 2 nd K L
58 op2ndg K V L V 2 nd K L = L
59 43 45 58 syl2anc φ 2 nd K L = L
60 57 59 eqtrid φ 2 nd 1 st K L F G = L
61 60 ad3antrrr φ u = U v = V f = F k = K 2 nd 1 st K L F G = L
62 56 61 eqtrd φ u = U v = V f = F k = K 2 nd 1 st u = L
63 fvexd φ u = U v = V f = F k = K l = L 1 st 2 nd v V
64 simp-4r φ u = U v = V f = F k = K l = L u = U v = V
65 64 simprd φ u = U v = V f = F k = K l = L v = V
66 7 ad4antr φ u = U v = V f = F k = K l = L V = R S M N
67 65 66 eqtrd φ u = U v = V f = F k = K l = L v = R S M N
68 67 fveq2d φ u = U v = V f = F k = K l = L 2 nd v = 2 nd R S M N
69 68 fveq2d φ u = U v = V f = F k = K l = L 1 st 2 nd v = 1 st 2 nd R S M N
70 opex R S V
71 opex M N V
72 70 71 op2nd 2 nd R S M N = M N
73 72 fveq2i 1 st 2 nd R S M N = 1 st M N
74 23 brrelex1i M C Func D N M V
75 5 74 syl φ M V
76 23 brrelex2i M C Func D N N V
77 5 76 syl φ N V
78 op1stg M V N V 1 st M N = M
79 75 77 78 syl2anc φ 1 st M N = M
80 73 79 eqtrid φ 1 st 2 nd R S M N = M
81 80 ad4antr φ u = U v = V f = F k = K l = L 1 st 2 nd R S M N = M
82 69 81 eqtrd φ u = U v = V f = F k = K l = L 1 st 2 nd v = M
83 fvexd φ u = U v = V f = F k = K l = L m = M 1 st 1 st v V
84 65 adantr φ u = U v = V f = F k = K l = L m = M v = V
85 66 adantr φ u = U v = V f = F k = K l = L m = M V = R S M N
86 84 85 eqtrd φ u = U v = V f = F k = K l = L m = M v = R S M N
87 86 fveq2d φ u = U v = V f = F k = K l = L m = M 1 st v = 1 st R S M N
88 87 fveq2d φ u = U v = V f = F k = K l = L m = M 1 st 1 st v = 1 st 1 st R S M N
89 70 71 op1st 1 st R S M N = R S
90 89 fveq2i 1 st 1 st R S M N = 1 st R S
91 41 brrelex1i R D Func E S R V
92 6 91 syl φ R V
93 41 brrelex2i R D Func E S S V
94 6 93 syl φ S V
95 op1stg R V S V 1 st R S = R
96 92 94 95 syl2anc φ 1 st R S = R
97 90 96 eqtrid φ 1 st 1 st R S M N = R
98 97 ad5antr φ u = U v = V f = F k = K l = L m = M 1 st 1 st R S M N = R
99 88 98 eqtrd φ u = U v = V f = F k = K l = L m = M 1 st 1 st v = R
100 55 ad3antrrr φ u = U v = V f = F k = K l = L m = M r = R 1 st u = 1 st K L F G
101 100 39 eqtrdi φ u = U v = V f = F k = K l = L m = M r = R 1 st u = K L
102 87 adantr φ u = U v = V f = F k = K l = L m = M r = R 1 st v = 1 st R S M N
103 102 89 eqtrdi φ u = U v = V f = F k = K l = L m = M r = R 1 st v = R S
104 101 103 oveq12d φ u = U v = V f = F k = K l = L m = M r = R 1 st u D Nat E 1 st v = K L D Nat E R S
105 17 ad5antr φ u = U v = V f = F k = K l = L m = M r = R 2 nd u = 2 nd K L F G
106 105 21 eqtrdi φ u = U v = V f = F k = K l = L m = M r = R 2 nd u = F G
107 68 ad2antrr φ u = U v = V f = F k = K l = L m = M r = R 2 nd v = 2 nd R S M N
108 107 72 eqtrdi φ u = U v = V f = F k = K l = L m = M r = R 2 nd v = M N
109 106 108 oveq12d φ u = U v = V f = F k = K l = L m = M r = R 2 nd u C Nat D 2 nd v = F G C Nat D M N
110 simp-4r φ u = U v = V f = F k = K l = L m = M r = R k = K
111 simp-5r φ u = U v = V f = F k = K l = L m = M r = R f = F
112 111 fveq1d φ u = U v = V f = F k = K l = L m = M r = R f x = F x
113 110 112 fveq12d φ u = U v = V f = F k = K l = L m = M r = R k f x = K F x
114 simplr φ u = U v = V f = F k = K l = L m = M r = R m = M
115 114 fveq1d φ u = U v = V f = F k = K l = L m = M r = R m x = M x
116 110 115 fveq12d φ u = U v = V f = F k = K l = L m = M r = R k m x = K M x
117 113 116 opeq12d φ u = U v = V f = F k = K l = L m = M r = R k f x k m x = K F x K M x
118 simpr φ u = U v = V f = F k = K l = L m = M r = R r = R
119 118 115 fveq12d φ u = U v = V f = F k = K l = L m = M r = R r m x = R M x
120 117 119 oveq12d φ u = U v = V f = F k = K l = L m = M r = R k f x k m x comp E r m x = K F x K M x comp E R M x
121 115 fveq2d φ u = U v = V f = F k = K l = L m = M r = R b m x = b M x
122 simpllr φ u = U v = V f = F k = K l = L m = M r = R l = L
123 122 112 115 oveq123d φ u = U v = V f = F k = K l = L m = M r = R f x l m x = F x L M x
124 123 fveq1d φ u = U v = V f = F k = K l = L m = M r = R f x l m x a x = F x L M x a x
125 120 121 124 oveq123d φ u = U v = V f = F k = K l = L m = M r = R b m x k f x k m x comp E r m x f x l m x a x = b M x K F x K M x comp E R M x F x L M x a x
126 125 mpteq2dv φ u = U v = V f = F k = K l = L m = M r = R x Base C b m x k f x k m x comp E r m x f x l m x a x = x Base C b M x K F x K M x comp E R M x F x L M x a x
127 104 109 126 mpoeq123dv φ u = U v = V f = F k = K l = L m = M r = R b 1 st u D Nat E 1 st v , a 2 nd u C Nat D 2 nd v x Base C b m x k f x k m x comp E r m x f x l m x a x = b K L D Nat E R S , a F G C Nat D M N x Base C b M x K F x K M x comp E R M x F x L M x a x
128 83 99 127 csbied2 φ u = U v = V f = F k = K l = L m = M 1 st 1 st v / r b 1 st u D Nat E 1 st v , a 2 nd u C Nat D 2 nd v x Base C b m x k f x k m x comp E r m x f x l m x a x = b K L D Nat E R S , a F G C Nat D M N x Base C b M x K F x K M x comp E R M x F x L M x a x
129 63 82 128 csbied2 φ u = U v = V f = F k = K l = L 1 st 2 nd v / m 1 st 1 st v / r b 1 st u D Nat E 1 st v , a 2 nd u C Nat D 2 nd v x Base C b m x k f x k m x comp E r m x f x l m x a x = b K L D Nat E R S , a F G C Nat D M N x Base C b M x K F x K M x comp E R M x F x L M x a x
130 51 62 129 csbied2 φ u = U v = V f = F k = K 2 nd 1 st u / l 1 st 2 nd v / m 1 st 1 st v / r b 1 st u D Nat E 1 st v , a 2 nd u C Nat D 2 nd v x Base C b m x k f x k m x comp E r m x f x l m x a x = b K L D Nat E R S , a F G C Nat D M N x Base C b M x K F x K M x comp E R M x F x L M x a x
131 33 50 130 csbied2 φ u = U v = V f = F 1 st 1 st u / k 2 nd 1 st u / l 1 st 2 nd v / m 1 st 1 st v / r b 1 st u D Nat E 1 st v , a 2 nd u C Nat D 2 nd v x Base C b m x k f x k m x comp E r m x f x l m x a x = b K L D Nat E R S , a F G C Nat D M N x Base C b M x K F x K M x comp E R M x F x L M x a x
132 13 32 131 csbied2 φ u = U v = V 1 st 2 nd u / f 1 st 1 st u / k 2 nd 1 st u / l 1 st 2 nd v / m 1 st 1 st v / r b 1 st u D Nat E 1 st v , a 2 nd u C Nat D 2 nd v x Base C b m x k f x k m x comp E r m x f x l m x a x = b K L D Nat E R S , a F G C Nat D M N x Base C b M x K F x K M x comp E R M x F x L M x a x
133 11 4 3 2 fuco2eld φ U D Func E × C Func D
134 11 7 6 5 fuco2eld φ V D Func E × C Func D
135 ovex K L D Nat E R S V
136 ovex F G C Nat D M N V
137 135 136 mpoex b K L D Nat E R S , a F G C Nat D M N x Base C b M x K F x K M x comp E R M x F x L M x a x V
138 137 a1i φ b K L D Nat E R S , a F G C Nat D M N x Base C b M x K F x K M x comp E R M x F x L M x a x V
139 12 132 133 134 138 ovmpod φ U P V = b K L D Nat E R S , a F G C Nat D M N x Base C b M x K F x K M x comp E R M x F x L M x a x