Step | Hyp | Ref
| Expression |
1 | | id 22 |
. . . 4
โข (๐ฅ = ๐ โ ๐ฅ = ๐) |
2 | 1, 1 | oveq12d 7423 |
. . 3
โข (๐ฅ = ๐ โ (๐ฅ๐ป๐ฅ) = (๐๐ป๐)) |
3 | | oveq2 7413 |
. . . . . 6
โข (๐ฅ = ๐ โ (๐ฆ๐ป๐ฅ) = (๐ฆ๐ป๐)) |
4 | | opeq2 4873 |
. . . . . . . . 9
โข (๐ฅ = ๐ โ โจ๐ฆ, ๐ฅโฉ = โจ๐ฆ, ๐โฉ) |
5 | 4, 1 | oveq12d 7423 |
. . . . . . . 8
โข (๐ฅ = ๐ โ (โจ๐ฆ, ๐ฅโฉ ยท ๐ฅ) = (โจ๐ฆ, ๐โฉ ยท ๐)) |
6 | 5 | oveqd 7422 |
. . . . . . 7
โข (๐ฅ = ๐ โ (๐(โจ๐ฆ, ๐ฅโฉ ยท ๐ฅ)๐) = (๐(โจ๐ฆ, ๐โฉ ยท ๐)๐)) |
7 | 6 | eqeq1d 2734 |
. . . . . 6
โข (๐ฅ = ๐ โ ((๐(โจ๐ฆ, ๐ฅโฉ ยท ๐ฅ)๐) = ๐ โ (๐(โจ๐ฆ, ๐โฉ ยท ๐)๐) = ๐)) |
8 | 3, 7 | raleqbidv 3342 |
. . . . 5
โข (๐ฅ = ๐ โ (โ๐ โ (๐ฆ๐ป๐ฅ)(๐(โจ๐ฆ, ๐ฅโฉ ยท ๐ฅ)๐) = ๐ โ โ๐ โ (๐ฆ๐ป๐)(๐(โจ๐ฆ, ๐โฉ ยท ๐)๐) = ๐)) |
9 | | oveq1 7412 |
. . . . . 6
โข (๐ฅ = ๐ โ (๐ฅ๐ป๐ฆ) = (๐๐ป๐ฆ)) |
10 | 1, 1 | opeq12d 4880 |
. . . . . . . . 9
โข (๐ฅ = ๐ โ โจ๐ฅ, ๐ฅโฉ = โจ๐, ๐โฉ) |
11 | 10 | oveq1d 7420 |
. . . . . . . 8
โข (๐ฅ = ๐ โ (โจ๐ฅ, ๐ฅโฉ ยท ๐ฆ) = (โจ๐, ๐โฉ ยท ๐ฆ)) |
12 | 11 | oveqd 7422 |
. . . . . . 7
โข (๐ฅ = ๐ โ (๐(โจ๐ฅ, ๐ฅโฉ ยท ๐ฆ)๐) = (๐(โจ๐, ๐โฉ ยท ๐ฆ)๐)) |
13 | 12 | eqeq1d 2734 |
. . . . . 6
โข (๐ฅ = ๐ โ ((๐(โจ๐ฅ, ๐ฅโฉ ยท ๐ฆ)๐) = ๐ โ (๐(โจ๐, ๐โฉ ยท ๐ฆ)๐) = ๐)) |
14 | 9, 13 | raleqbidv 3342 |
. . . . 5
โข (๐ฅ = ๐ โ (โ๐ โ (๐ฅ๐ป๐ฆ)(๐(โจ๐ฅ, ๐ฅโฉ ยท ๐ฆ)๐) = ๐ โ โ๐ โ (๐๐ป๐ฆ)(๐(โจ๐, ๐โฉ ยท ๐ฆ)๐) = ๐)) |
15 | 8, 14 | anbi12d 631 |
. . . 4
โข (๐ฅ = ๐ โ ((โ๐ โ (๐ฆ๐ป๐ฅ)(๐(โจ๐ฆ, ๐ฅโฉ ยท ๐ฅ)๐) = ๐ โง โ๐ โ (๐ฅ๐ป๐ฆ)(๐(โจ๐ฅ, ๐ฅโฉ ยท ๐ฆ)๐) = ๐) โ (โ๐ โ (๐ฆ๐ป๐)(๐(โจ๐ฆ, ๐โฉ ยท ๐)๐) = ๐ โง โ๐ โ (๐๐ป๐ฆ)(๐(โจ๐, ๐โฉ ยท ๐ฆ)๐) = ๐))) |
16 | 15 | ralbidv 3177 |
. . 3
โข (๐ฅ = ๐ โ (โ๐ฆ โ ๐ต (โ๐ โ (๐ฆ๐ป๐ฅ)(๐(โจ๐ฆ, ๐ฅโฉ ยท ๐ฅ)๐) = ๐ โง โ๐ โ (๐ฅ๐ป๐ฆ)(๐(โจ๐ฅ, ๐ฅโฉ ยท ๐ฆ)๐) = ๐) โ โ๐ฆ โ ๐ต (โ๐ โ (๐ฆ๐ป๐)(๐(โจ๐ฆ, ๐โฉ ยท ๐)๐) = ๐ โง โ๐ โ (๐๐ป๐ฆ)(๐(โจ๐, ๐โฉ ยท ๐ฆ)๐) = ๐))) |
17 | 2, 16 | rexeqbidv 3343 |
. 2
โข (๐ฅ = ๐ โ (โ๐ โ (๐ฅ๐ป๐ฅ)โ๐ฆ โ ๐ต (โ๐ โ (๐ฆ๐ป๐ฅ)(๐(โจ๐ฆ, ๐ฅโฉ ยท ๐ฅ)๐) = ๐ โง โ๐ โ (๐ฅ๐ป๐ฆ)(๐(โจ๐ฅ, ๐ฅโฉ ยท ๐ฆ)๐) = ๐) โ โ๐ โ (๐๐ป๐)โ๐ฆ โ ๐ต (โ๐ โ (๐ฆ๐ป๐)(๐(โจ๐ฆ, ๐โฉ ยท ๐)๐) = ๐ โง โ๐ โ (๐๐ป๐ฆ)(๐(โจ๐, ๐โฉ ยท ๐ฆ)๐) = ๐))) |
18 | | catidex.c |
. . 3
โข (๐ โ ๐ถ โ Cat) |
19 | | catidex.b |
. . . . 5
โข ๐ต = (Baseโ๐ถ) |
20 | | catidex.h |
. . . . 5
โข ๐ป = (Hom โ๐ถ) |
21 | | catidex.o |
. . . . 5
โข ยท =
(compโ๐ถ) |
22 | 19, 20, 21 | iscat 17612 |
. . . 4
โข (๐ถ โ Cat โ (๐ถ โ Cat โ โ๐ฅ โ ๐ต (โ๐ โ (๐ฅ๐ป๐ฅ)โ๐ฆ โ ๐ต (โ๐ โ (๐ฆ๐ป๐ฅ)(๐(โจ๐ฆ, ๐ฅโฉ ยท ๐ฅ)๐) = ๐ โง โ๐ โ (๐ฅ๐ป๐ฆ)(๐(โจ๐ฅ, ๐ฅโฉ ยท ๐ฆ)๐) = ๐) โง โ๐ฆ โ ๐ต โ๐ง โ ๐ต โ๐ โ (๐ฅ๐ป๐ฆ)โ๐ โ (๐ฆ๐ป๐ง)((๐(โจ๐ฅ, ๐ฆโฉ ยท ๐ง)๐) โ (๐ฅ๐ป๐ง) โง โ๐ค โ ๐ต โ๐ โ (๐ง๐ป๐ค)((๐(โจ๐ฆ, ๐งโฉ ยท ๐ค)๐)(โจ๐ฅ, ๐ฆโฉ ยท ๐ค)๐) = (๐(โจ๐ฅ, ๐งโฉ ยท ๐ค)(๐(โจ๐ฅ, ๐ฆโฉ ยท ๐ง)๐)))))) |
23 | 22 | ibi 266 |
. . 3
โข (๐ถ โ Cat โ โ๐ฅ โ ๐ต (โ๐ โ (๐ฅ๐ป๐ฅ)โ๐ฆ โ ๐ต (โ๐ โ (๐ฆ๐ป๐ฅ)(๐(โจ๐ฆ, ๐ฅโฉ ยท ๐ฅ)๐) = ๐ โง โ๐ โ (๐ฅ๐ป๐ฆ)(๐(โจ๐ฅ, ๐ฅโฉ ยท ๐ฆ)๐) = ๐) โง โ๐ฆ โ ๐ต โ๐ง โ ๐ต โ๐ โ (๐ฅ๐ป๐ฆ)โ๐ โ (๐ฆ๐ป๐ง)((๐(โจ๐ฅ, ๐ฆโฉ ยท ๐ง)๐) โ (๐ฅ๐ป๐ง) โง โ๐ค โ ๐ต โ๐ โ (๐ง๐ป๐ค)((๐(โจ๐ฆ, ๐งโฉ ยท ๐ค)๐)(โจ๐ฅ, ๐ฆโฉ ยท ๐ค)๐) = (๐(โจ๐ฅ, ๐งโฉ ยท ๐ค)(๐(โจ๐ฅ, ๐ฆโฉ ยท ๐ง)๐))))) |
24 | | simpl 483 |
. . . 4
โข
((โ๐ โ
(๐ฅ๐ป๐ฅ)โ๐ฆ โ ๐ต (โ๐ โ (๐ฆ๐ป๐ฅ)(๐(โจ๐ฆ, ๐ฅโฉ ยท ๐ฅ)๐) = ๐ โง โ๐ โ (๐ฅ๐ป๐ฆ)(๐(โจ๐ฅ, ๐ฅโฉ ยท ๐ฆ)๐) = ๐) โง โ๐ฆ โ ๐ต โ๐ง โ ๐ต โ๐ โ (๐ฅ๐ป๐ฆ)โ๐ โ (๐ฆ๐ป๐ง)((๐(โจ๐ฅ, ๐ฆโฉ ยท ๐ง)๐) โ (๐ฅ๐ป๐ง) โง โ๐ค โ ๐ต โ๐ โ (๐ง๐ป๐ค)((๐(โจ๐ฆ, ๐งโฉ ยท ๐ค)๐)(โจ๐ฅ, ๐ฆโฉ ยท ๐ค)๐) = (๐(โจ๐ฅ, ๐งโฉ ยท ๐ค)(๐(โจ๐ฅ, ๐ฆโฉ ยท ๐ง)๐)))) โ โ๐ โ (๐ฅ๐ป๐ฅ)โ๐ฆ โ ๐ต (โ๐ โ (๐ฆ๐ป๐ฅ)(๐(โจ๐ฆ, ๐ฅโฉ ยท ๐ฅ)๐) = ๐ โง โ๐ โ (๐ฅ๐ป๐ฆ)(๐(โจ๐ฅ, ๐ฅโฉ ยท ๐ฆ)๐) = ๐)) |
25 | 24 | ralimi 3083 |
. . 3
โข
(โ๐ฅ โ
๐ต (โ๐ โ (๐ฅ๐ป๐ฅ)โ๐ฆ โ ๐ต (โ๐ โ (๐ฆ๐ป๐ฅ)(๐(โจ๐ฆ, ๐ฅโฉ ยท ๐ฅ)๐) = ๐ โง โ๐ โ (๐ฅ๐ป๐ฆ)(๐(โจ๐ฅ, ๐ฅโฉ ยท ๐ฆ)๐) = ๐) โง โ๐ฆ โ ๐ต โ๐ง โ ๐ต โ๐ โ (๐ฅ๐ป๐ฆ)โ๐ โ (๐ฆ๐ป๐ง)((๐(โจ๐ฅ, ๐ฆโฉ ยท ๐ง)๐) โ (๐ฅ๐ป๐ง) โง โ๐ค โ ๐ต โ๐ โ (๐ง๐ป๐ค)((๐(โจ๐ฆ, ๐งโฉ ยท ๐ค)๐)(โจ๐ฅ, ๐ฆโฉ ยท ๐ค)๐) = (๐(โจ๐ฅ, ๐งโฉ ยท ๐ค)(๐(โจ๐ฅ, ๐ฆโฉ ยท ๐ง)๐)))) โ โ๐ฅ โ ๐ต โ๐ โ (๐ฅ๐ป๐ฅ)โ๐ฆ โ ๐ต (โ๐ โ (๐ฆ๐ป๐ฅ)(๐(โจ๐ฆ, ๐ฅโฉ ยท ๐ฅ)๐) = ๐ โง โ๐ โ (๐ฅ๐ป๐ฆ)(๐(โจ๐ฅ, ๐ฅโฉ ยท ๐ฆ)๐) = ๐)) |
26 | 18, 23, 25 | 3syl 18 |
. 2
โข (๐ โ โ๐ฅ โ ๐ต โ๐ โ (๐ฅ๐ป๐ฅ)โ๐ฆ โ ๐ต (โ๐ โ (๐ฆ๐ป๐ฅ)(๐(โจ๐ฆ, ๐ฅโฉ ยท ๐ฅ)๐) = ๐ โง โ๐ โ (๐ฅ๐ป๐ฆ)(๐(โจ๐ฅ, ๐ฅโฉ ยท ๐ฆ)๐) = ๐)) |
27 | | catidex.x |
. 2
โข (๐ โ ๐ โ ๐ต) |
28 | 17, 26, 27 | rspcdva 3613 |
1
โข (๐ โ โ๐ โ (๐๐ป๐)โ๐ฆ โ ๐ต (โ๐ โ (๐ฆ๐ป๐)(๐(โจ๐ฆ, ๐โฉ ยท ๐)๐) = ๐ โง โ๐ โ (๐๐ป๐ฆ)(๐(โจ๐, ๐โฉ ยท ๐ฆ)๐) = ๐)) |