Step | Hyp | Ref
| Expression |
1 | | coafval.o |
. 2
β’ Β· =
(compaβπΆ) |
2 | | fveq2 6892 |
. . . . . 6
β’ (π = πΆ β (Arrowβπ) = (ArrowβπΆ)) |
3 | | coafval.a |
. . . . . 6
β’ π΄ = (ArrowβπΆ) |
4 | 2, 3 | eqtr4di 2791 |
. . . . 5
β’ (π = πΆ β (Arrowβπ) = π΄) |
5 | 4 | rabeqdv 3448 |
. . . . 5
β’ (π = πΆ β {β β (Arrowβπ) β£ (codaββ) =
(domaβπ)} = {β β π΄ β£ (codaββ) =
(domaβπ)}) |
6 | | fveq2 6892 |
. . . . . . . . 9
β’ (π = πΆ β (compβπ) = (compβπΆ)) |
7 | | coafval.x |
. . . . . . . . 9
β’ β =
(compβπΆ) |
8 | 6, 7 | eqtr4di 2791 |
. . . . . . . 8
β’ (π = πΆ β (compβπ) = β ) |
9 | 8 | oveqd 7426 |
. . . . . . 7
β’ (π = πΆ β
(β¨(domaβπ), (domaβπ)β©(compβπ)(codaβπ)) =
(β¨(domaβπ), (domaβπ)β© β
(codaβπ))) |
10 | 9 | oveqd 7426 |
. . . . . 6
β’ (π = πΆ β ((2nd βπ)(β¨(domaβπ),
(domaβπ)β©(compβπ)(codaβπ))(2nd βπ)) = ((2nd
βπ)(β¨(domaβπ),
(domaβπ)β© β
(codaβπ))(2nd βπ))) |
11 | 10 | oteq3d 4888 |
. . . . 5
β’ (π = πΆ β
β¨(domaβπ), (codaβπ), ((2nd βπ)(β¨(domaβπ),
(domaβπ)β©(compβπ)(codaβπ))(2nd βπ))β© =
β¨(domaβπ), (codaβπ), ((2nd βπ)(β¨(domaβπ),
(domaβπ)β© β
(codaβπ))(2nd βπ))β©) |
12 | 4, 5, 11 | mpoeq123dv 7484 |
. . . 4
β’ (π = πΆ β (π β (Arrowβπ), π β {β β (Arrowβπ) β£ (codaββ) =
(domaβπ)} β¦
β¨(domaβπ), (codaβπ), ((2nd βπ)(β¨(domaβπ),
(domaβπ)β©(compβπ)(codaβπ))(2nd βπ))β©) = (π β π΄, π β {β β π΄ β£ (codaββ) =
(domaβπ)} β¦
β¨(domaβπ), (codaβπ), ((2nd βπ)(β¨(domaβπ),
(domaβπ)β© β
(codaβπ))(2nd βπ))β©)) |
13 | | df-coa 18006 |
. . . 4
β’
compa = (π β Cat β¦ (π β (Arrowβπ), π β {β β (Arrowβπ) β£ (codaββ) =
(domaβπ)} β¦
β¨(domaβπ), (codaβπ), ((2nd βπ)(β¨(domaβπ),
(domaβπ)β©(compβπ)(codaβπ))(2nd βπ))β©)) |
14 | 3 | fvexi 6906 |
. . . . 5
β’ π΄ β V |
15 | 14 | rabex 5333 |
. . . . 5
β’ {β β π΄ β£ (codaββ) =
(domaβπ)} β V |
16 | 14, 15 | mpoex 8066 |
. . . 4
β’ (π β π΄, π β {β β π΄ β£ (codaββ) =
(domaβπ)} β¦
β¨(domaβπ), (codaβπ), ((2nd βπ)(β¨(domaβπ),
(domaβπ)β© β
(codaβπ))(2nd βπ))β©) β V |
17 | 12, 13, 16 | fvmpt 6999 |
. . 3
β’ (πΆ β Cat β
(compaβπΆ) = (π β π΄, π β {β β π΄ β£ (codaββ) =
(domaβπ)} β¦
β¨(domaβπ), (codaβπ), ((2nd βπ)(β¨(domaβπ),
(domaβπ)β© β
(codaβπ))(2nd βπ))β©)) |
18 | 13 | fvmptndm 7029 |
. . . 4
β’ (Β¬
πΆ β Cat β
(compaβπΆ) = β
) |
19 | 3 | arwrcl 17994 |
. . . . . . . 8
β’ (π β π΄ β πΆ β Cat) |
20 | 19 | con3i 154 |
. . . . . . 7
β’ (Β¬
πΆ β Cat β Β¬
π β π΄) |
21 | 20 | eq0rdv 4405 |
. . . . . 6
β’ (Β¬
πΆ β Cat β π΄ = β
) |
22 | | eqidd 2734 |
. . . . . 6
β’ (Β¬
πΆ β Cat β {β β π΄ β£ (codaββ) =
(domaβπ)} = {β β π΄ β£ (codaββ) =
(domaβπ)}) |
23 | | eqidd 2734 |
. . . . . 6
β’ (Β¬
πΆ β Cat β
β¨(domaβπ), (codaβπ), ((2nd βπ)(β¨(domaβπ),
(domaβπ)β© β
(codaβπ))(2nd βπ))β© =
β¨(domaβπ), (codaβπ), ((2nd βπ)(β¨(domaβπ),
(domaβπ)β© β
(codaβπ))(2nd βπ))β©) |
24 | 21, 22, 23 | mpoeq123dv 7484 |
. . . . 5
β’ (Β¬
πΆ β Cat β (π β π΄, π β {β β π΄ β£ (codaββ) =
(domaβπ)} β¦
β¨(domaβπ), (codaβπ), ((2nd βπ)(β¨(domaβπ),
(domaβπ)β© β
(codaβπ))(2nd βπ))β©) = (π β β
, π β {β β π΄ β£ (codaββ) =
(domaβπ)} β¦
β¨(domaβπ), (codaβπ), ((2nd βπ)(β¨(domaβπ),
(domaβπ)β© β
(codaβπ))(2nd βπ))β©)) |
25 | | mpo0 7494 |
. . . . 5
β’ (π β β
, π β {β β π΄ β£ (codaββ) =
(domaβπ)} β¦
β¨(domaβπ), (codaβπ), ((2nd βπ)(β¨(domaβπ),
(domaβπ)β© β
(codaβπ))(2nd βπ))β©) = β
|
26 | 24, 25 | eqtrdi 2789 |
. . . 4
β’ (Β¬
πΆ β Cat β (π β π΄, π β {β β π΄ β£ (codaββ) =
(domaβπ)} β¦
β¨(domaβπ), (codaβπ), ((2nd βπ)(β¨(domaβπ),
(domaβπ)β© β
(codaβπ))(2nd βπ))β©) = β
) |
27 | 18, 26 | eqtr4d 2776 |
. . 3
β’ (Β¬
πΆ β Cat β
(compaβπΆ) = (π β π΄, π β {β β π΄ β£ (codaββ) =
(domaβπ)} β¦
β¨(domaβπ), (codaβπ), ((2nd βπ)(β¨(domaβπ),
(domaβπ)β© β
(codaβπ))(2nd βπ))β©)) |
28 | 17, 27 | pm2.61i 182 |
. 2
β’
(compaβπΆ) = (π β π΄, π β {β β π΄ β£ (codaββ) =
(domaβπ)} β¦
β¨(domaβπ), (codaβπ), ((2nd βπ)(β¨(domaβπ),
(domaβπ)β© β
(codaβπ))(2nd βπ))β©) |
29 | 1, 28 | eqtri 2761 |
1
β’ Β· =
(π β π΄, π β {β β π΄ β£ (codaββ) =
(domaβπ)} β¦
β¨(domaβπ), (codaβπ), ((2nd βπ)(β¨(domaβπ),
(domaβπ)β© β
(codaβπ))(2nd βπ))β©) |