Step | Hyp | Ref
| Expression |
1 | | natfval.1 |
. 2
โข ๐ = (๐ถ Nat ๐ท) |
2 | | oveq12 7360 |
. . . . 5
โข ((๐ก = ๐ถ โง ๐ข = ๐ท) โ (๐ก Func ๐ข) = (๐ถ Func ๐ท)) |
3 | | simpl 483 |
. . . . . . . . . . . 12
โข ((๐ก = ๐ถ โง ๐ข = ๐ท) โ ๐ก = ๐ถ) |
4 | 3 | fveq2d 6843 |
. . . . . . . . . . 11
โข ((๐ก = ๐ถ โง ๐ข = ๐ท) โ (Baseโ๐ก) = (Baseโ๐ถ)) |
5 | | natfval.b |
. . . . . . . . . . 11
โข ๐ต = (Baseโ๐ถ) |
6 | 4, 5 | eqtr4di 2795 |
. . . . . . . . . 10
โข ((๐ก = ๐ถ โง ๐ข = ๐ท) โ (Baseโ๐ก) = ๐ต) |
7 | 6 | ixpeq1d 8805 |
. . . . . . . . 9
โข ((๐ก = ๐ถ โง ๐ข = ๐ท) โ X๐ฅ โ (Baseโ๐ก)((๐โ๐ฅ)(Hom โ๐ข)(๐ โ๐ฅ)) = X๐ฅ โ ๐ต ((๐โ๐ฅ)(Hom โ๐ข)(๐ โ๐ฅ))) |
8 | | simpr 485 |
. . . . . . . . . . . . 13
โข ((๐ก = ๐ถ โง ๐ข = ๐ท) โ ๐ข = ๐ท) |
9 | 8 | fveq2d 6843 |
. . . . . . . . . . . 12
โข ((๐ก = ๐ถ โง ๐ข = ๐ท) โ (Hom โ๐ข) = (Hom โ๐ท)) |
10 | | natfval.j |
. . . . . . . . . . . 12
โข ๐ฝ = (Hom โ๐ท) |
11 | 9, 10 | eqtr4di 2795 |
. . . . . . . . . . 11
โข ((๐ก = ๐ถ โง ๐ข = ๐ท) โ (Hom โ๐ข) = ๐ฝ) |
12 | 11 | oveqd 7368 |
. . . . . . . . . 10
โข ((๐ก = ๐ถ โง ๐ข = ๐ท) โ ((๐โ๐ฅ)(Hom โ๐ข)(๐ โ๐ฅ)) = ((๐โ๐ฅ)๐ฝ(๐ โ๐ฅ))) |
13 | 12 | ixpeq2dv 8809 |
. . . . . . . . 9
โข ((๐ก = ๐ถ โง ๐ข = ๐ท) โ X๐ฅ โ ๐ต ((๐โ๐ฅ)(Hom โ๐ข)(๐ โ๐ฅ)) = X๐ฅ โ ๐ต ((๐โ๐ฅ)๐ฝ(๐ โ๐ฅ))) |
14 | 7, 13 | eqtrd 2777 |
. . . . . . . 8
โข ((๐ก = ๐ถ โง ๐ข = ๐ท) โ X๐ฅ โ (Baseโ๐ก)((๐โ๐ฅ)(Hom โ๐ข)(๐ โ๐ฅ)) = X๐ฅ โ ๐ต ((๐โ๐ฅ)๐ฝ(๐ โ๐ฅ))) |
15 | 3 | fveq2d 6843 |
. . . . . . . . . . . . 13
โข ((๐ก = ๐ถ โง ๐ข = ๐ท) โ (Hom โ๐ก) = (Hom โ๐ถ)) |
16 | | natfval.h |
. . . . . . . . . . . . 13
โข ๐ป = (Hom โ๐ถ) |
17 | 15, 16 | eqtr4di 2795 |
. . . . . . . . . . . 12
โข ((๐ก = ๐ถ โง ๐ข = ๐ท) โ (Hom โ๐ก) = ๐ป) |
18 | 17 | oveqd 7368 |
. . . . . . . . . . 11
โข ((๐ก = ๐ถ โง ๐ข = ๐ท) โ (๐ฅ(Hom โ๐ก)๐ฆ) = (๐ฅ๐ป๐ฆ)) |
19 | 8 | fveq2d 6843 |
. . . . . . . . . . . . . . 15
โข ((๐ก = ๐ถ โง ๐ข = ๐ท) โ (compโ๐ข) = (compโ๐ท)) |
20 | | natfval.o |
. . . . . . . . . . . . . . 15
โข ยท =
(compโ๐ท) |
21 | 19, 20 | eqtr4di 2795 |
. . . . . . . . . . . . . 14
โข ((๐ก = ๐ถ โง ๐ข = ๐ท) โ (compโ๐ข) = ยท ) |
22 | 21 | oveqd 7368 |
. . . . . . . . . . . . 13
โข ((๐ก = ๐ถ โง ๐ข = ๐ท) โ (โจ(๐โ๐ฅ), (๐โ๐ฆ)โฉ(compโ๐ข)(๐ โ๐ฆ)) = (โจ(๐โ๐ฅ), (๐โ๐ฆ)โฉ ยท (๐ โ๐ฆ))) |
23 | 22 | oveqd 7368 |
. . . . . . . . . . . 12
โข ((๐ก = ๐ถ โง ๐ข = ๐ท) โ ((๐โ๐ฆ)(โจ(๐โ๐ฅ), (๐โ๐ฆ)โฉ(compโ๐ข)(๐ โ๐ฆ))((๐ฅ(2nd โ๐)๐ฆ)โโ)) = ((๐โ๐ฆ)(โจ(๐โ๐ฅ), (๐โ๐ฆ)โฉ ยท (๐ โ๐ฆ))((๐ฅ(2nd โ๐)๐ฆ)โโ))) |
24 | 21 | oveqd 7368 |
. . . . . . . . . . . . 13
โข ((๐ก = ๐ถ โง ๐ข = ๐ท) โ (โจ(๐โ๐ฅ), (๐ โ๐ฅ)โฉ(compโ๐ข)(๐ โ๐ฆ)) = (โจ(๐โ๐ฅ), (๐ โ๐ฅ)โฉ ยท (๐ โ๐ฆ))) |
25 | 24 | oveqd 7368 |
. . . . . . . . . . . 12
โข ((๐ก = ๐ถ โง ๐ข = ๐ท) โ (((๐ฅ(2nd โ๐)๐ฆ)โโ)(โจ(๐โ๐ฅ), (๐ โ๐ฅ)โฉ(compโ๐ข)(๐ โ๐ฆ))(๐โ๐ฅ)) = (((๐ฅ(2nd โ๐)๐ฆ)โโ)(โจ(๐โ๐ฅ), (๐ โ๐ฅ)โฉ ยท (๐ โ๐ฆ))(๐โ๐ฅ))) |
26 | 23, 25 | eqeq12d 2753 |
. . . . . . . . . . 11
โข ((๐ก = ๐ถ โง ๐ข = ๐ท) โ (((๐โ๐ฆ)(โจ(๐โ๐ฅ), (๐โ๐ฆ)โฉ(compโ๐ข)(๐ โ๐ฆ))((๐ฅ(2nd โ๐)๐ฆ)โโ)) = (((๐ฅ(2nd โ๐)๐ฆ)โโ)(โจ(๐โ๐ฅ), (๐ โ๐ฅ)โฉ(compโ๐ข)(๐ โ๐ฆ))(๐โ๐ฅ)) โ ((๐โ๐ฆ)(โจ(๐โ๐ฅ), (๐โ๐ฆ)โฉ ยท (๐ โ๐ฆ))((๐ฅ(2nd โ๐)๐ฆ)โโ)) = (((๐ฅ(2nd โ๐)๐ฆ)โโ)(โจ(๐โ๐ฅ), (๐ โ๐ฅ)โฉ ยท (๐ โ๐ฆ))(๐โ๐ฅ)))) |
27 | 18, 26 | raleqbidv 3317 |
. . . . . . . . . 10
โข ((๐ก = ๐ถ โง ๐ข = ๐ท) โ (โโ โ (๐ฅ(Hom โ๐ก)๐ฆ)((๐โ๐ฆ)(โจ(๐โ๐ฅ), (๐โ๐ฆ)โฉ(compโ๐ข)(๐ โ๐ฆ))((๐ฅ(2nd โ๐)๐ฆ)โโ)) = (((๐ฅ(2nd โ๐)๐ฆ)โโ)(โจ(๐โ๐ฅ), (๐ โ๐ฅ)โฉ(compโ๐ข)(๐ โ๐ฆ))(๐โ๐ฅ)) โ โโ โ (๐ฅ๐ป๐ฆ)((๐โ๐ฆ)(โจ(๐โ๐ฅ), (๐โ๐ฆ)โฉ ยท (๐ โ๐ฆ))((๐ฅ(2nd โ๐)๐ฆ)โโ)) = (((๐ฅ(2nd โ๐)๐ฆ)โโ)(โจ(๐โ๐ฅ), (๐ โ๐ฅ)โฉ ยท (๐ โ๐ฆ))(๐โ๐ฅ)))) |
28 | 6, 27 | raleqbidv 3317 |
. . . . . . . . 9
โข ((๐ก = ๐ถ โง ๐ข = ๐ท) โ (โ๐ฆ โ (Baseโ๐ก)โโ โ (๐ฅ(Hom โ๐ก)๐ฆ)((๐โ๐ฆ)(โจ(๐โ๐ฅ), (๐โ๐ฆ)โฉ(compโ๐ข)(๐ โ๐ฆ))((๐ฅ(2nd โ๐)๐ฆ)โโ)) = (((๐ฅ(2nd โ๐)๐ฆ)โโ)(โจ(๐โ๐ฅ), (๐ โ๐ฅ)โฉ(compโ๐ข)(๐ โ๐ฆ))(๐โ๐ฅ)) โ โ๐ฆ โ ๐ต โโ โ (๐ฅ๐ป๐ฆ)((๐โ๐ฆ)(โจ(๐โ๐ฅ), (๐โ๐ฆ)โฉ ยท (๐ โ๐ฆ))((๐ฅ(2nd โ๐)๐ฆ)โโ)) = (((๐ฅ(2nd โ๐)๐ฆ)โโ)(โจ(๐โ๐ฅ), (๐ โ๐ฅ)โฉ ยท (๐ โ๐ฆ))(๐โ๐ฅ)))) |
29 | 6, 28 | raleqbidv 3317 |
. . . . . . . 8
โข ((๐ก = ๐ถ โง ๐ข = ๐ท) โ (โ๐ฅ โ (Baseโ๐ก)โ๐ฆ โ (Baseโ๐ก)โโ โ (๐ฅ(Hom โ๐ก)๐ฆ)((๐โ๐ฆ)(โจ(๐โ๐ฅ), (๐โ๐ฆ)โฉ(compโ๐ข)(๐ โ๐ฆ))((๐ฅ(2nd โ๐)๐ฆ)โโ)) = (((๐ฅ(2nd โ๐)๐ฆ)โโ)(โจ(๐โ๐ฅ), (๐ โ๐ฅ)โฉ(compโ๐ข)(๐ โ๐ฆ))(๐โ๐ฅ)) โ โ๐ฅ โ ๐ต โ๐ฆ โ ๐ต โโ โ (๐ฅ๐ป๐ฆ)((๐โ๐ฆ)(โจ(๐โ๐ฅ), (๐โ๐ฆ)โฉ ยท (๐ โ๐ฆ))((๐ฅ(2nd โ๐)๐ฆ)โโ)) = (((๐ฅ(2nd โ๐)๐ฆ)โโ)(โจ(๐โ๐ฅ), (๐ โ๐ฅ)โฉ ยท (๐ โ๐ฆ))(๐โ๐ฅ)))) |
30 | 14, 29 | rabeqbidv 3422 |
. . . . . . 7
โข ((๐ก = ๐ถ โง ๐ข = ๐ท) โ {๐ โ X๐ฅ โ (Baseโ๐ก)((๐โ๐ฅ)(Hom โ๐ข)(๐ โ๐ฅ)) โฃ โ๐ฅ โ (Baseโ๐ก)โ๐ฆ โ (Baseโ๐ก)โโ โ (๐ฅ(Hom โ๐ก)๐ฆ)((๐โ๐ฆ)(โจ(๐โ๐ฅ), (๐โ๐ฆ)โฉ(compโ๐ข)(๐ โ๐ฆ))((๐ฅ(2nd โ๐)๐ฆ)โโ)) = (((๐ฅ(2nd โ๐)๐ฆ)โโ)(โจ(๐โ๐ฅ), (๐ โ๐ฅ)โฉ(compโ๐ข)(๐ โ๐ฆ))(๐โ๐ฅ))} = {๐ โ X๐ฅ โ ๐ต ((๐โ๐ฅ)๐ฝ(๐ โ๐ฅ)) โฃ โ๐ฅ โ ๐ต โ๐ฆ โ ๐ต โโ โ (๐ฅ๐ป๐ฆ)((๐โ๐ฆ)(โจ(๐โ๐ฅ), (๐โ๐ฆ)โฉ ยท (๐ โ๐ฆ))((๐ฅ(2nd โ๐)๐ฆ)โโ)) = (((๐ฅ(2nd โ๐)๐ฆ)โโ)(โจ(๐โ๐ฅ), (๐ โ๐ฅ)โฉ ยท (๐ โ๐ฆ))(๐โ๐ฅ))}) |
31 | 30 | csbeq2dv 3860 |
. . . . . 6
โข ((๐ก = ๐ถ โง ๐ข = ๐ท) โ โฆ(1st
โ๐) / ๐ โฆ{๐ โ X๐ฅ โ
(Baseโ๐ก)((๐โ๐ฅ)(Hom โ๐ข)(๐ โ๐ฅ)) โฃ โ๐ฅ โ (Baseโ๐ก)โ๐ฆ โ (Baseโ๐ก)โโ โ (๐ฅ(Hom โ๐ก)๐ฆ)((๐โ๐ฆ)(โจ(๐โ๐ฅ), (๐โ๐ฆ)โฉ(compโ๐ข)(๐ โ๐ฆ))((๐ฅ(2nd โ๐)๐ฆ)โโ)) = (((๐ฅ(2nd โ๐)๐ฆ)โโ)(โจ(๐โ๐ฅ), (๐ โ๐ฅ)โฉ(compโ๐ข)(๐ โ๐ฆ))(๐โ๐ฅ))} = โฆ(1st
โ๐) / ๐ โฆ{๐ โ X๐ฅ โ
๐ต ((๐โ๐ฅ)๐ฝ(๐ โ๐ฅ)) โฃ โ๐ฅ โ ๐ต โ๐ฆ โ ๐ต โโ โ (๐ฅ๐ป๐ฆ)((๐โ๐ฆ)(โจ(๐โ๐ฅ), (๐โ๐ฆ)โฉ ยท (๐ โ๐ฆ))((๐ฅ(2nd โ๐)๐ฆ)โโ)) = (((๐ฅ(2nd โ๐)๐ฆ)โโ)(โจ(๐โ๐ฅ), (๐ โ๐ฅ)โฉ ยท (๐ โ๐ฆ))(๐โ๐ฅ))}) |
32 | 31 | csbeq2dv 3860 |
. . . . 5
โข ((๐ก = ๐ถ โง ๐ข = ๐ท) โ โฆ(1st
โ๐) / ๐โฆโฆ(1st
โ๐) / ๐ โฆ{๐ โ X๐ฅ โ
(Baseโ๐ก)((๐โ๐ฅ)(Hom โ๐ข)(๐ โ๐ฅ)) โฃ โ๐ฅ โ (Baseโ๐ก)โ๐ฆ โ (Baseโ๐ก)โโ โ (๐ฅ(Hom โ๐ก)๐ฆ)((๐โ๐ฆ)(โจ(๐โ๐ฅ), (๐โ๐ฆ)โฉ(compโ๐ข)(๐ โ๐ฆ))((๐ฅ(2nd โ๐)๐ฆ)โโ)) = (((๐ฅ(2nd โ๐)๐ฆ)โโ)(โจ(๐โ๐ฅ), (๐ โ๐ฅ)โฉ(compโ๐ข)(๐ โ๐ฆ))(๐โ๐ฅ))} = โฆ(1st
โ๐) / ๐โฆโฆ(1st
โ๐) / ๐ โฆ{๐ โ X๐ฅ โ
๐ต ((๐โ๐ฅ)๐ฝ(๐ โ๐ฅ)) โฃ โ๐ฅ โ ๐ต โ๐ฆ โ ๐ต โโ โ (๐ฅ๐ป๐ฆ)((๐โ๐ฆ)(โจ(๐โ๐ฅ), (๐โ๐ฆ)โฉ ยท (๐ โ๐ฆ))((๐ฅ(2nd โ๐)๐ฆ)โโ)) = (((๐ฅ(2nd โ๐)๐ฆ)โโ)(โจ(๐โ๐ฅ), (๐ โ๐ฅ)โฉ ยท (๐ โ๐ฆ))(๐โ๐ฅ))}) |
33 | 2, 2, 32 | mpoeq123dv 7426 |
. . . 4
โข ((๐ก = ๐ถ โง ๐ข = ๐ท) โ (๐ โ (๐ก Func ๐ข), ๐ โ (๐ก Func ๐ข) โฆ โฆ(1st
โ๐) / ๐โฆโฆ(1st
โ๐) / ๐ โฆ{๐ โ X๐ฅ โ
(Baseโ๐ก)((๐โ๐ฅ)(Hom โ๐ข)(๐ โ๐ฅ)) โฃ โ๐ฅ โ (Baseโ๐ก)โ๐ฆ โ (Baseโ๐ก)โโ โ (๐ฅ(Hom โ๐ก)๐ฆ)((๐โ๐ฆ)(โจ(๐โ๐ฅ), (๐โ๐ฆ)โฉ(compโ๐ข)(๐ โ๐ฆ))((๐ฅ(2nd โ๐)๐ฆ)โโ)) = (((๐ฅ(2nd โ๐)๐ฆ)โโ)(โจ(๐โ๐ฅ), (๐ โ๐ฅ)โฉ(compโ๐ข)(๐ โ๐ฆ))(๐โ๐ฅ))}) = (๐ โ (๐ถ Func ๐ท), ๐ โ (๐ถ Func ๐ท) โฆ โฆ(1st
โ๐) / ๐โฆโฆ(1st
โ๐) / ๐ โฆ{๐ โ X๐ฅ โ
๐ต ((๐โ๐ฅ)๐ฝ(๐ โ๐ฅ)) โฃ โ๐ฅ โ ๐ต โ๐ฆ โ ๐ต โโ โ (๐ฅ๐ป๐ฆ)((๐โ๐ฆ)(โจ(๐โ๐ฅ), (๐โ๐ฆ)โฉ ยท (๐ โ๐ฆ))((๐ฅ(2nd โ๐)๐ฆ)โโ)) = (((๐ฅ(2nd โ๐)๐ฆ)โโ)(โจ(๐โ๐ฅ), (๐ โ๐ฅ)โฉ ยท (๐ โ๐ฆ))(๐โ๐ฅ))})) |
34 | | df-nat 17790 |
. . . 4
โข Nat =
(๐ก โ Cat, ๐ข โ Cat โฆ (๐ โ (๐ก Func ๐ข), ๐ โ (๐ก Func ๐ข) โฆ โฆ(1st
โ๐) / ๐โฆโฆ(1st
โ๐) / ๐ โฆ{๐ โ X๐ฅ โ
(Baseโ๐ก)((๐โ๐ฅ)(Hom โ๐ข)(๐ โ๐ฅ)) โฃ โ๐ฅ โ (Baseโ๐ก)โ๐ฆ โ (Baseโ๐ก)โโ โ (๐ฅ(Hom โ๐ก)๐ฆ)((๐โ๐ฆ)(โจ(๐โ๐ฅ), (๐โ๐ฆ)โฉ(compโ๐ข)(๐ โ๐ฆ))((๐ฅ(2nd โ๐)๐ฆ)โโ)) = (((๐ฅ(2nd โ๐)๐ฆ)โโ)(โจ(๐โ๐ฅ), (๐ โ๐ฅ)โฉ(compโ๐ข)(๐ โ๐ฆ))(๐โ๐ฅ))})) |
35 | | ovex 7384 |
. . . . 5
โข (๐ถ Func ๐ท) โ V |
36 | 35, 35 | mpoex 8004 |
. . . 4
โข (๐ โ (๐ถ Func ๐ท), ๐ โ (๐ถ Func ๐ท) โฆ โฆ(1st
โ๐) / ๐โฆโฆ(1st
โ๐) / ๐ โฆ{๐ โ X๐ฅ โ
๐ต ((๐โ๐ฅ)๐ฝ(๐ โ๐ฅ)) โฃ โ๐ฅ โ ๐ต โ๐ฆ โ ๐ต โโ โ (๐ฅ๐ป๐ฆ)((๐โ๐ฆ)(โจ(๐โ๐ฅ), (๐โ๐ฆ)โฉ ยท (๐ โ๐ฆ))((๐ฅ(2nd โ๐)๐ฆ)โโ)) = (((๐ฅ(2nd โ๐)๐ฆ)โโ)(โจ(๐โ๐ฅ), (๐ โ๐ฅ)โฉ ยท (๐ โ๐ฆ))(๐โ๐ฅ))}) โ V |
37 | 33, 34, 36 | ovmpoa 7504 |
. . 3
โข ((๐ถ โ Cat โง ๐ท โ Cat) โ (๐ถ Nat ๐ท) = (๐ โ (๐ถ Func ๐ท), ๐ โ (๐ถ Func ๐ท) โฆ โฆ(1st
โ๐) / ๐โฆโฆ(1st
โ๐) / ๐ โฆ{๐ โ X๐ฅ โ
๐ต ((๐โ๐ฅ)๐ฝ(๐ โ๐ฅ)) โฃ โ๐ฅ โ ๐ต โ๐ฆ โ ๐ต โโ โ (๐ฅ๐ป๐ฆ)((๐โ๐ฆ)(โจ(๐โ๐ฅ), (๐โ๐ฆ)โฉ ยท (๐ โ๐ฆ))((๐ฅ(2nd โ๐)๐ฆ)โโ)) = (((๐ฅ(2nd โ๐)๐ฆ)โโ)(โจ(๐โ๐ฅ), (๐ โ๐ฅ)โฉ ยท (๐ โ๐ฆ))(๐โ๐ฅ))})) |
38 | 34 | mpondm0 7586 |
. . . 4
โข (ยฌ
(๐ถ โ Cat โง ๐ท โ Cat) โ (๐ถ Nat ๐ท) = โ
) |
39 | | funcrcl 17709 |
. . . . . . . 8
โข (๐ โ (๐ถ Func ๐ท) โ (๐ถ โ Cat โง ๐ท โ Cat)) |
40 | 39 | con3i 154 |
. . . . . . 7
โข (ยฌ
(๐ถ โ Cat โง ๐ท โ Cat) โ ยฌ ๐ โ (๐ถ Func ๐ท)) |
41 | 40 | eq0rdv 4362 |
. . . . . 6
โข (ยฌ
(๐ถ โ Cat โง ๐ท โ Cat) โ (๐ถ Func ๐ท) = โ
) |
42 | 41 | olcd 872 |
. . . . 5
โข (ยฌ
(๐ถ โ Cat โง ๐ท โ Cat) โ ((๐ถ Func ๐ท) = โ
โจ (๐ถ Func ๐ท) = โ
)) |
43 | | 0mpo0 7434 |
. . . . 5
โข (((๐ถ Func ๐ท) = โ
โจ (๐ถ Func ๐ท) = โ
) โ (๐ โ (๐ถ Func ๐ท), ๐ โ (๐ถ Func ๐ท) โฆ โฆ(1st
โ๐) / ๐โฆโฆ(1st
โ๐) / ๐ โฆ{๐ โ X๐ฅ โ
๐ต ((๐โ๐ฅ)๐ฝ(๐ โ๐ฅ)) โฃ โ๐ฅ โ ๐ต โ๐ฆ โ ๐ต โโ โ (๐ฅ๐ป๐ฆ)((๐โ๐ฆ)(โจ(๐โ๐ฅ), (๐โ๐ฆ)โฉ ยท (๐ โ๐ฆ))((๐ฅ(2nd โ๐)๐ฆ)โโ)) = (((๐ฅ(2nd โ๐)๐ฆ)โโ)(โจ(๐โ๐ฅ), (๐ โ๐ฅ)โฉ ยท (๐ โ๐ฆ))(๐โ๐ฅ))}) = โ
) |
44 | 42, 43 | syl 17 |
. . . 4
โข (ยฌ
(๐ถ โ Cat โง ๐ท โ Cat) โ (๐ โ (๐ถ Func ๐ท), ๐ โ (๐ถ Func ๐ท) โฆ โฆ(1st
โ๐) / ๐โฆโฆ(1st
โ๐) / ๐ โฆ{๐ โ X๐ฅ โ
๐ต ((๐โ๐ฅ)๐ฝ(๐ โ๐ฅ)) โฃ โ๐ฅ โ ๐ต โ๐ฆ โ ๐ต โโ โ (๐ฅ๐ป๐ฆ)((๐โ๐ฆ)(โจ(๐โ๐ฅ), (๐โ๐ฆ)โฉ ยท (๐ โ๐ฆ))((๐ฅ(2nd โ๐)๐ฆ)โโ)) = (((๐ฅ(2nd โ๐)๐ฆ)โโ)(โจ(๐โ๐ฅ), (๐ โ๐ฅ)โฉ ยท (๐ โ๐ฆ))(๐โ๐ฅ))}) = โ
) |
45 | 38, 44 | eqtr4d 2780 |
. . 3
โข (ยฌ
(๐ถ โ Cat โง ๐ท โ Cat) โ (๐ถ Nat ๐ท) = (๐ โ (๐ถ Func ๐ท), ๐ โ (๐ถ Func ๐ท) โฆ โฆ(1st
โ๐) / ๐โฆโฆ(1st
โ๐) / ๐ โฆ{๐ โ X๐ฅ โ
๐ต ((๐โ๐ฅ)๐ฝ(๐ โ๐ฅ)) โฃ โ๐ฅ โ ๐ต โ๐ฆ โ ๐ต โโ โ (๐ฅ๐ป๐ฆ)((๐โ๐ฆ)(โจ(๐โ๐ฅ), (๐โ๐ฆ)โฉ ยท (๐ โ๐ฆ))((๐ฅ(2nd โ๐)๐ฆ)โโ)) = (((๐ฅ(2nd โ๐)๐ฆ)โโ)(โจ(๐โ๐ฅ), (๐ โ๐ฅ)โฉ ยท (๐ โ๐ฆ))(๐โ๐ฅ))})) |
46 | 37, 45 | pm2.61i 182 |
. 2
โข (๐ถ Nat ๐ท) = (๐ โ (๐ถ Func ๐ท), ๐ โ (๐ถ Func ๐ท) โฆ โฆ(1st
โ๐) / ๐โฆโฆ(1st
โ๐) / ๐ โฆ{๐ โ X๐ฅ โ
๐ต ((๐โ๐ฅ)๐ฝ(๐ โ๐ฅ)) โฃ โ๐ฅ โ ๐ต โ๐ฆ โ ๐ต โโ โ (๐ฅ๐ป๐ฆ)((๐โ๐ฆ)(โจ(๐โ๐ฅ), (๐โ๐ฆ)โฉ ยท (๐ โ๐ฆ))((๐ฅ(2nd โ๐)๐ฆ)โโ)) = (((๐ฅ(2nd โ๐)๐ฆ)โโ)(โจ(๐โ๐ฅ), (๐ โ๐ฅ)โฉ ยท (๐ โ๐ฆ))(๐โ๐ฅ))}) |
47 | 1, 46 | eqtri 2765 |
1
โข ๐ = (๐ โ (๐ถ Func ๐ท), ๐ โ (๐ถ Func ๐ท) โฆ โฆ(1st
โ๐) / ๐โฆโฆ(1st
โ๐) / ๐ โฆ{๐ โ X๐ฅ โ
๐ต ((๐โ๐ฅ)๐ฝ(๐ โ๐ฅ)) โฃ โ๐ฅ โ ๐ต โ๐ฆ โ ๐ต โโ โ (๐ฅ๐ป๐ฆ)((๐โ๐ฆ)(โจ(๐โ๐ฅ), (๐โ๐ฆ)โฉ ยท (๐ โ๐ฆ))((๐ฅ(2nd โ๐)๐ฆ)โโ)) = (((๐ฅ(2nd โ๐)๐ฆ)โโ)(โจ(๐โ๐ฅ), (๐ โ๐ฅ)โฉ ยท (๐ โ๐ฆ))(๐โ๐ฅ))}) |