Step | Hyp | Ref
| Expression |
1 | | isfuncd.1 |
. 2
โข (๐ โ ๐น:๐ตโถ๐ถ) |
2 | | isfuncd.2 |
. . . 4
โข (๐ โ ๐บ Fn (๐ต ร ๐ต)) |
3 | | isfunc.b |
. . . . . 6
โข ๐ต = (Baseโ๐ท) |
4 | 3 | fvexi 6860 |
. . . . 5
โข ๐ต โ V |
5 | 4, 4 | xpex 7691 |
. . . 4
โข (๐ต ร ๐ต) โ V |
6 | | fnex 7171 |
. . . 4
โข ((๐บ Fn (๐ต ร ๐ต) โง (๐ต ร ๐ต) โ V) โ ๐บ โ V) |
7 | 2, 5, 6 | sylancl 587 |
. . 3
โข (๐ โ ๐บ โ V) |
8 | | isfuncd.3 |
. . . . . 6
โข ((๐ โง (๐ฅ โ ๐ต โง ๐ฆ โ ๐ต)) โ (๐ฅ๐บ๐ฆ):(๐ฅ๐ป๐ฆ)โถ((๐นโ๐ฅ)๐ฝ(๐นโ๐ฆ))) |
9 | | ovex 7394 |
. . . . . . 7
โข ((๐นโ๐ฅ)๐ฝ(๐นโ๐ฆ)) โ V |
10 | | ovex 7394 |
. . . . . . 7
โข (๐ฅ๐ป๐ฆ) โ V |
11 | 9, 10 | elmap 8815 |
. . . . . 6
โข ((๐ฅ๐บ๐ฆ) โ (((๐นโ๐ฅ)๐ฝ(๐นโ๐ฆ)) โm (๐ฅ๐ป๐ฆ)) โ (๐ฅ๐บ๐ฆ):(๐ฅ๐ป๐ฆ)โถ((๐นโ๐ฅ)๐ฝ(๐นโ๐ฆ))) |
12 | 8, 11 | sylibr 233 |
. . . . 5
โข ((๐ โง (๐ฅ โ ๐ต โง ๐ฆ โ ๐ต)) โ (๐ฅ๐บ๐ฆ) โ (((๐นโ๐ฅ)๐ฝ(๐นโ๐ฆ)) โm (๐ฅ๐ป๐ฆ))) |
13 | 12 | ralrimivva 3194 |
. . . 4
โข (๐ โ โ๐ฅ โ ๐ต โ๐ฆ โ ๐ต (๐ฅ๐บ๐ฆ) โ (((๐นโ๐ฅ)๐ฝ(๐นโ๐ฆ)) โm (๐ฅ๐ป๐ฆ))) |
14 | | fveq2 6846 |
. . . . . . 7
โข (๐ง = โจ๐ฅ, ๐ฆโฉ โ (๐บโ๐ง) = (๐บโโจ๐ฅ, ๐ฆโฉ)) |
15 | | df-ov 7364 |
. . . . . . 7
โข (๐ฅ๐บ๐ฆ) = (๐บโโจ๐ฅ, ๐ฆโฉ) |
16 | 14, 15 | eqtr4di 2791 |
. . . . . 6
โข (๐ง = โจ๐ฅ, ๐ฆโฉ โ (๐บโ๐ง) = (๐ฅ๐บ๐ฆ)) |
17 | | vex 3451 |
. . . . . . . . . 10
โข ๐ฅ โ V |
18 | | vex 3451 |
. . . . . . . . . 10
โข ๐ฆ โ V |
19 | 17, 18 | op1std 7935 |
. . . . . . . . 9
โข (๐ง = โจ๐ฅ, ๐ฆโฉ โ (1st โ๐ง) = ๐ฅ) |
20 | 19 | fveq2d 6850 |
. . . . . . . 8
โข (๐ง = โจ๐ฅ, ๐ฆโฉ โ (๐นโ(1st โ๐ง)) = (๐นโ๐ฅ)) |
21 | 17, 18 | op2ndd 7936 |
. . . . . . . . 9
โข (๐ง = โจ๐ฅ, ๐ฆโฉ โ (2nd โ๐ง) = ๐ฆ) |
22 | 21 | fveq2d 6850 |
. . . . . . . 8
โข (๐ง = โจ๐ฅ, ๐ฆโฉ โ (๐นโ(2nd โ๐ง)) = (๐นโ๐ฆ)) |
23 | 20, 22 | oveq12d 7379 |
. . . . . . 7
โข (๐ง = โจ๐ฅ, ๐ฆโฉ โ ((๐นโ(1st โ๐ง))๐ฝ(๐นโ(2nd โ๐ง))) = ((๐นโ๐ฅ)๐ฝ(๐นโ๐ฆ))) |
24 | | fveq2 6846 |
. . . . . . . 8
โข (๐ง = โจ๐ฅ, ๐ฆโฉ โ (๐ปโ๐ง) = (๐ปโโจ๐ฅ, ๐ฆโฉ)) |
25 | | df-ov 7364 |
. . . . . . . 8
โข (๐ฅ๐ป๐ฆ) = (๐ปโโจ๐ฅ, ๐ฆโฉ) |
26 | 24, 25 | eqtr4di 2791 |
. . . . . . 7
โข (๐ง = โจ๐ฅ, ๐ฆโฉ โ (๐ปโ๐ง) = (๐ฅ๐ป๐ฆ)) |
27 | 23, 26 | oveq12d 7379 |
. . . . . 6
โข (๐ง = โจ๐ฅ, ๐ฆโฉ โ (((๐นโ(1st โ๐ง))๐ฝ(๐นโ(2nd โ๐ง))) โm (๐ปโ๐ง)) = (((๐นโ๐ฅ)๐ฝ(๐นโ๐ฆ)) โm (๐ฅ๐ป๐ฆ))) |
28 | 16, 27 | eleq12d 2828 |
. . . . 5
โข (๐ง = โจ๐ฅ, ๐ฆโฉ โ ((๐บโ๐ง) โ (((๐นโ(1st โ๐ง))๐ฝ(๐นโ(2nd โ๐ง))) โm (๐ปโ๐ง)) โ (๐ฅ๐บ๐ฆ) โ (((๐นโ๐ฅ)๐ฝ(๐นโ๐ฆ)) โm (๐ฅ๐ป๐ฆ)))) |
29 | 28 | ralxp 5801 |
. . . 4
โข
(โ๐ง โ
(๐ต ร ๐ต)(๐บโ๐ง) โ (((๐นโ(1st โ๐ง))๐ฝ(๐นโ(2nd โ๐ง))) โm (๐ปโ๐ง)) โ โ๐ฅ โ ๐ต โ๐ฆ โ ๐ต (๐ฅ๐บ๐ฆ) โ (((๐นโ๐ฅ)๐ฝ(๐นโ๐ฆ)) โm (๐ฅ๐ป๐ฆ))) |
30 | 13, 29 | sylibr 233 |
. . 3
โข (๐ โ โ๐ง โ (๐ต ร ๐ต)(๐บโ๐ง) โ (((๐นโ(1st โ๐ง))๐ฝ(๐นโ(2nd โ๐ง))) โm (๐ปโ๐ง))) |
31 | | elixp2 8845 |
. . 3
โข (๐บ โ X๐ง โ
(๐ต ร ๐ต)(((๐นโ(1st โ๐ง))๐ฝ(๐นโ(2nd โ๐ง))) โm (๐ปโ๐ง)) โ (๐บ โ V โง ๐บ Fn (๐ต ร ๐ต) โง โ๐ง โ (๐ต ร ๐ต)(๐บโ๐ง) โ (((๐นโ(1st โ๐ง))๐ฝ(๐นโ(2nd โ๐ง))) โm (๐ปโ๐ง)))) |
32 | 7, 2, 30, 31 | syl3anbrc 1344 |
. 2
โข (๐ โ ๐บ โ X๐ง โ (๐ต ร ๐ต)(((๐นโ(1st โ๐ง))๐ฝ(๐นโ(2nd โ๐ง))) โm (๐ปโ๐ง))) |
33 | | isfuncd.4 |
. . . 4
โข ((๐ โง ๐ฅ โ ๐ต) โ ((๐ฅ๐บ๐ฅ)โ( 1 โ๐ฅ)) = (๐ผโ(๐นโ๐ฅ))) |
34 | | isfuncd.5 |
. . . . . . . . 9
โข ((๐ โง (๐ฅ โ ๐ต โง ๐ฆ โ ๐ต โง ๐ง โ ๐ต) โง (๐ โ (๐ฅ๐ป๐ฆ) โง ๐ โ (๐ฆ๐ป๐ง))) โ ((๐ฅ๐บ๐ง)โ(๐(โจ๐ฅ, ๐ฆโฉ ยท ๐ง)๐)) = (((๐ฆ๐บ๐ง)โ๐)(โจ(๐นโ๐ฅ), (๐นโ๐ฆ)โฉ๐(๐นโ๐ง))((๐ฅ๐บ๐ฆ)โ๐))) |
35 | 34 | 3expia 1122 |
. . . . . . . 8
โข ((๐ โง (๐ฅ โ ๐ต โง ๐ฆ โ ๐ต โง ๐ง โ ๐ต)) โ ((๐ โ (๐ฅ๐ป๐ฆ) โง ๐ โ (๐ฆ๐ป๐ง)) โ ((๐ฅ๐บ๐ง)โ(๐(โจ๐ฅ, ๐ฆโฉ ยท ๐ง)๐)) = (((๐ฆ๐บ๐ง)โ๐)(โจ(๐นโ๐ฅ), (๐นโ๐ฆ)โฉ๐(๐นโ๐ง))((๐ฅ๐บ๐ฆ)โ๐)))) |
36 | 35 | 3exp2 1355 |
. . . . . . 7
โข (๐ โ (๐ฅ โ ๐ต โ (๐ฆ โ ๐ต โ (๐ง โ ๐ต โ ((๐ โ (๐ฅ๐ป๐ฆ) โง ๐ โ (๐ฆ๐ป๐ง)) โ ((๐ฅ๐บ๐ง)โ(๐(โจ๐ฅ, ๐ฆโฉ ยท ๐ง)๐)) = (((๐ฆ๐บ๐ง)โ๐)(โจ(๐นโ๐ฅ), (๐นโ๐ฆ)โฉ๐(๐นโ๐ง))((๐ฅ๐บ๐ฆ)โ๐))))))) |
37 | 36 | imp43 429 |
. . . . . 6
โข (((๐ โง ๐ฅ โ ๐ต) โง (๐ฆ โ ๐ต โง ๐ง โ ๐ต)) โ ((๐ โ (๐ฅ๐ป๐ฆ) โง ๐ โ (๐ฆ๐ป๐ง)) โ ((๐ฅ๐บ๐ง)โ(๐(โจ๐ฅ, ๐ฆโฉ ยท ๐ง)๐)) = (((๐ฆ๐บ๐ง)โ๐)(โจ(๐นโ๐ฅ), (๐นโ๐ฆ)โฉ๐(๐นโ๐ง))((๐ฅ๐บ๐ฆ)โ๐)))) |
38 | 37 | ralrimivv 3192 |
. . . . 5
โข (((๐ โง ๐ฅ โ ๐ต) โง (๐ฆ โ ๐ต โง ๐ง โ ๐ต)) โ โ๐ โ (๐ฅ๐ป๐ฆ)โ๐ โ (๐ฆ๐ป๐ง)((๐ฅ๐บ๐ง)โ(๐(โจ๐ฅ, ๐ฆโฉ ยท ๐ง)๐)) = (((๐ฆ๐บ๐ง)โ๐)(โจ(๐นโ๐ฅ), (๐นโ๐ฆ)โฉ๐(๐นโ๐ง))((๐ฅ๐บ๐ฆ)โ๐))) |
39 | 38 | ralrimivva 3194 |
. . . 4
โข ((๐ โง ๐ฅ โ ๐ต) โ โ๐ฆ โ ๐ต โ๐ง โ ๐ต โ๐ โ (๐ฅ๐ป๐ฆ)โ๐ โ (๐ฆ๐ป๐ง)((๐ฅ๐บ๐ง)โ(๐(โจ๐ฅ, ๐ฆโฉ ยท ๐ง)๐)) = (((๐ฆ๐บ๐ง)โ๐)(โจ(๐นโ๐ฅ), (๐นโ๐ฆ)โฉ๐(๐นโ๐ง))((๐ฅ๐บ๐ฆ)โ๐))) |
40 | 33, 39 | jca 513 |
. . 3
โข ((๐ โง ๐ฅ โ ๐ต) โ (((๐ฅ๐บ๐ฅ)โ( 1 โ๐ฅ)) = (๐ผโ(๐นโ๐ฅ)) โง โ๐ฆ โ ๐ต โ๐ง โ ๐ต โ๐ โ (๐ฅ๐ป๐ฆ)โ๐ โ (๐ฆ๐ป๐ง)((๐ฅ๐บ๐ง)โ(๐(โจ๐ฅ, ๐ฆโฉ ยท ๐ง)๐)) = (((๐ฆ๐บ๐ง)โ๐)(โจ(๐นโ๐ฅ), (๐นโ๐ฆ)โฉ๐(๐นโ๐ง))((๐ฅ๐บ๐ฆ)โ๐)))) |
41 | 40 | ralrimiva 3140 |
. 2
โข (๐ โ โ๐ฅ โ ๐ต (((๐ฅ๐บ๐ฅ)โ( 1 โ๐ฅ)) = (๐ผโ(๐นโ๐ฅ)) โง โ๐ฆ โ ๐ต โ๐ง โ ๐ต โ๐ โ (๐ฅ๐ป๐ฆ)โ๐ โ (๐ฆ๐ป๐ง)((๐ฅ๐บ๐ง)โ(๐(โจ๐ฅ, ๐ฆโฉ ยท ๐ง)๐)) = (((๐ฆ๐บ๐ง)โ๐)(โจ(๐นโ๐ฅ), (๐นโ๐ฆ)โฉ๐(๐นโ๐ง))((๐ฅ๐บ๐ฆ)โ๐)))) |
42 | | isfunc.c |
. . 3
โข ๐ถ = (Baseโ๐ธ) |
43 | | isfunc.h |
. . 3
โข ๐ป = (Hom โ๐ท) |
44 | | isfunc.j |
. . 3
โข ๐ฝ = (Hom โ๐ธ) |
45 | | isfunc.1 |
. . 3
โข 1 =
(Idโ๐ท) |
46 | | isfunc.i |
. . 3
โข ๐ผ = (Idโ๐ธ) |
47 | | isfunc.x |
. . 3
โข ยท =
(compโ๐ท) |
48 | | isfunc.o |
. . 3
โข ๐ = (compโ๐ธ) |
49 | | isfunc.d |
. . 3
โข (๐ โ ๐ท โ Cat) |
50 | | isfunc.e |
. . 3
โข (๐ โ ๐ธ โ Cat) |
51 | 3, 42, 43, 44, 45, 46, 47, 48, 49, 50 | isfunc 17758 |
. 2
โข (๐ โ (๐น(๐ท Func ๐ธ)๐บ โ (๐น:๐ตโถ๐ถ โง ๐บ โ X๐ง โ (๐ต ร ๐ต)(((๐นโ(1st โ๐ง))๐ฝ(๐นโ(2nd โ๐ง))) โm (๐ปโ๐ง)) โง โ๐ฅ โ ๐ต (((๐ฅ๐บ๐ฅ)โ( 1 โ๐ฅ)) = (๐ผโ(๐นโ๐ฅ)) โง โ๐ฆ โ ๐ต โ๐ง โ ๐ต โ๐ โ (๐ฅ๐ป๐ฆ)โ๐ โ (๐ฆ๐ป๐ง)((๐ฅ๐บ๐ง)โ(๐(โจ๐ฅ, ๐ฆโฉ ยท ๐ง)๐)) = (((๐ฆ๐บ๐ง)โ๐)(โจ(๐นโ๐ฅ), (๐นโ๐ฆ)โฉ๐(๐นโ๐ง))((๐ฅ๐บ๐ฆ)โ๐)))))) |
52 | 1, 32, 41, 51 | mpbir3and 1343 |
1
โข (๐ โ ๐น(๐ท Func ๐ธ)๐บ) |