Step | Hyp | Ref
| Expression |
1 | | id 22 |
. . . 4
โข (๐ฅ = ๐ โ ๐ฅ = ๐) |
2 | 1, 1 | oveq12d 7422 |
. . 3
โข (๐ฅ = ๐ โ (๐ฅ๐ป๐ฅ) = (๐๐ป๐)) |
3 | | oveq2 7412 |
. . . . . 6
โข (๐ฅ = ๐ โ (๐ฆ๐ป๐ฅ) = (๐ฆ๐ป๐)) |
4 | | opeq2 4869 |
. . . . . . . . 9
โข (๐ฅ = ๐ โ โจ๐ฆ, ๐ฅโฉ = โจ๐ฆ, ๐โฉ) |
5 | 4, 1 | oveq12d 7422 |
. . . . . . . 8
โข (๐ฅ = ๐ โ (โจ๐ฆ, ๐ฅโฉ ยท ๐ฅ) = (โจ๐ฆ, ๐โฉ ยท ๐)) |
6 | 5 | oveqd 7421 |
. . . . . . 7
โข (๐ฅ = ๐ โ (๐(โจ๐ฆ, ๐ฅโฉ ยท ๐ฅ)๐) = (๐(โจ๐ฆ, ๐โฉ ยท ๐)๐)) |
7 | 6 | eqeq1d 2728 |
. . . . . 6
โข (๐ฅ = ๐ โ ((๐(โจ๐ฆ, ๐ฅโฉ ยท ๐ฅ)๐) = ๐ โ (๐(โจ๐ฆ, ๐โฉ ยท ๐)๐) = ๐)) |
8 | 3, 7 | raleqbidv 3336 |
. . . . 5
โข (๐ฅ = ๐ โ (โ๐ โ (๐ฆ๐ป๐ฅ)(๐(โจ๐ฆ, ๐ฅโฉ ยท ๐ฅ)๐) = ๐ โ โ๐ โ (๐ฆ๐ป๐)(๐(โจ๐ฆ, ๐โฉ ยท ๐)๐) = ๐)) |
9 | | oveq1 7411 |
. . . . . 6
โข (๐ฅ = ๐ โ (๐ฅ๐ป๐ฆ) = (๐๐ป๐ฆ)) |
10 | 1, 1 | opeq12d 4876 |
. . . . . . . . 9
โข (๐ฅ = ๐ โ โจ๐ฅ, ๐ฅโฉ = โจ๐, ๐โฉ) |
11 | 10 | oveq1d 7419 |
. . . . . . . 8
โข (๐ฅ = ๐ โ (โจ๐ฅ, ๐ฅโฉ ยท ๐ฆ) = (โจ๐, ๐โฉ ยท ๐ฆ)) |
12 | 11 | oveqd 7421 |
. . . . . . 7
โข (๐ฅ = ๐ โ (๐(โจ๐ฅ, ๐ฅโฉ ยท ๐ฆ)๐) = (๐(โจ๐, ๐โฉ ยท ๐ฆ)๐)) |
13 | 12 | eqeq1d 2728 |
. . . . . 6
โข (๐ฅ = ๐ โ ((๐(โจ๐ฅ, ๐ฅโฉ ยท ๐ฆ)๐) = ๐ โ (๐(โจ๐, ๐โฉ ยท ๐ฆ)๐) = ๐)) |
14 | 9, 13 | raleqbidv 3336 |
. . . . 5
โข (๐ฅ = ๐ โ (โ๐ โ (๐ฅ๐ป๐ฆ)(๐(โจ๐ฅ, ๐ฅโฉ ยท ๐ฆ)๐) = ๐ โ โ๐ โ (๐๐ป๐ฆ)(๐(โจ๐, ๐โฉ ยท ๐ฆ)๐) = ๐)) |
15 | 8, 14 | anbi12d 630 |
. . . 4
โข (๐ฅ = ๐ โ ((โ๐ โ (๐ฆ๐ป๐ฅ)(๐(โจ๐ฆ, ๐ฅโฉ ยท ๐ฅ)๐) = ๐ โง โ๐ โ (๐ฅ๐ป๐ฆ)(๐(โจ๐ฅ, ๐ฅโฉ ยท ๐ฆ)๐) = ๐) โ (โ๐ โ (๐ฆ๐ป๐)(๐(โจ๐ฆ, ๐โฉ ยท ๐)๐) = ๐ โง โ๐ โ (๐๐ป๐ฆ)(๐(โจ๐, ๐โฉ ยท ๐ฆ)๐) = ๐))) |
16 | 15 | ralbidv 3171 |
. . 3
โข (๐ฅ = ๐ โ (โ๐ฆ โ ๐ต (โ๐ โ (๐ฆ๐ป๐ฅ)(๐(โจ๐ฆ, ๐ฅโฉ ยท ๐ฅ)๐) = ๐ โง โ๐ โ (๐ฅ๐ป๐ฆ)(๐(โจ๐ฅ, ๐ฅโฉ ยท ๐ฆ)๐) = ๐) โ โ๐ฆ โ ๐ต (โ๐ โ (๐ฆ๐ป๐)(๐(โจ๐ฆ, ๐โฉ ยท ๐)๐) = ๐ โง โ๐ โ (๐๐ป๐ฆ)(๐(โจ๐, ๐โฉ ยท ๐ฆ)๐) = ๐))) |
17 | 2, 16 | rexeqbidv 3337 |
. 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 17622 |
. . . 4
โข (๐ถ โ Cat โ (๐ถ โ Cat โ โ๐ฅ โ ๐ต (โ๐ โ (๐ฅ๐ป๐ฅ)โ๐ฆ โ ๐ต (โ๐ โ (๐ฆ๐ป๐ฅ)(๐(โจ๐ฆ, ๐ฅโฉ ยท ๐ฅ)๐) = ๐ โง โ๐ โ (๐ฅ๐ป๐ฆ)(๐(โจ๐ฅ, ๐ฅโฉ ยท ๐ฆ)๐) = ๐) โง โ๐ฆ โ ๐ต โ๐ง โ ๐ต โ๐ โ (๐ฅ๐ป๐ฆ)โ๐ โ (๐ฆ๐ป๐ง)((๐(โจ๐ฅ, ๐ฆโฉ ยท ๐ง)๐) โ (๐ฅ๐ป๐ง) โง โ๐ค โ ๐ต โ๐ โ (๐ง๐ป๐ค)((๐(โจ๐ฆ, ๐งโฉ ยท ๐ค)๐)(โจ๐ฅ, ๐ฆโฉ ยท ๐ค)๐) = (๐(โจ๐ฅ, ๐งโฉ ยท ๐ค)(๐(โจ๐ฅ, ๐ฆโฉ ยท ๐ง)๐)))))) |
23 | 22 | ibi 267 |
. . 3
โข (๐ถ โ Cat โ โ๐ฅ โ ๐ต (โ๐ โ (๐ฅ๐ป๐ฅ)โ๐ฆ โ ๐ต (โ๐ โ (๐ฆ๐ป๐ฅ)(๐(โจ๐ฆ, ๐ฅโฉ ยท ๐ฅ)๐) = ๐ โง โ๐ โ (๐ฅ๐ป๐ฆ)(๐(โจ๐ฅ, ๐ฅโฉ ยท ๐ฆ)๐) = ๐) โง โ๐ฆ โ ๐ต โ๐ง โ ๐ต โ๐ โ (๐ฅ๐ป๐ฆ)โ๐ โ (๐ฆ๐ป๐ง)((๐(โจ๐ฅ, ๐ฆโฉ ยท ๐ง)๐) โ (๐ฅ๐ป๐ง) โง โ๐ค โ ๐ต โ๐ โ (๐ง๐ป๐ค)((๐(โจ๐ฆ, ๐งโฉ ยท ๐ค)๐)(โจ๐ฅ, ๐ฆโฉ ยท ๐ค)๐) = (๐(โจ๐ฅ, ๐งโฉ ยท ๐ค)(๐(โจ๐ฅ, ๐ฆโฉ ยท ๐ง)๐))))) |
24 | | simpl 482 |
. . . 4
โข
((โ๐ โ
(๐ฅ๐ป๐ฅ)โ๐ฆ โ ๐ต (โ๐ โ (๐ฆ๐ป๐ฅ)(๐(โจ๐ฆ, ๐ฅโฉ ยท ๐ฅ)๐) = ๐ โง โ๐ โ (๐ฅ๐ป๐ฆ)(๐(โจ๐ฅ, ๐ฅโฉ ยท ๐ฆ)๐) = ๐) โง โ๐ฆ โ ๐ต โ๐ง โ ๐ต โ๐ โ (๐ฅ๐ป๐ฆ)โ๐ โ (๐ฆ๐ป๐ง)((๐(โจ๐ฅ, ๐ฆโฉ ยท ๐ง)๐) โ (๐ฅ๐ป๐ง) โง โ๐ค โ ๐ต โ๐ โ (๐ง๐ป๐ค)((๐(โจ๐ฆ, ๐งโฉ ยท ๐ค)๐)(โจ๐ฅ, ๐ฆโฉ ยท ๐ค)๐) = (๐(โจ๐ฅ, ๐งโฉ ยท ๐ค)(๐(โจ๐ฅ, ๐ฆโฉ ยท ๐ง)๐)))) โ โ๐ โ (๐ฅ๐ป๐ฅ)โ๐ฆ โ ๐ต (โ๐ โ (๐ฆ๐ป๐ฅ)(๐(โจ๐ฆ, ๐ฅโฉ ยท ๐ฅ)๐) = ๐ โง โ๐ โ (๐ฅ๐ป๐ฆ)(๐(โจ๐ฅ, ๐ฅโฉ ยท ๐ฆ)๐) = ๐)) |
25 | 24 | ralimi 3077 |
. . 3
โข
(โ๐ฅ โ
๐ต (โ๐ โ (๐ฅ๐ป๐ฅ)โ๐ฆ โ ๐ต (โ๐ โ (๐ฆ๐ป๐ฅ)(๐(โจ๐ฆ, ๐ฅโฉ ยท ๐ฅ)๐) = ๐ โง โ๐ โ (๐ฅ๐ป๐ฆ)(๐(โจ๐ฅ, ๐ฅโฉ ยท ๐ฆ)๐) = ๐) โง โ๐ฆ โ ๐ต โ๐ง โ ๐ต โ๐ โ (๐ฅ๐ป๐ฆ)โ๐ โ (๐ฆ๐ป๐ง)((๐(โจ๐ฅ, ๐ฆโฉ ยท ๐ง)๐) โ (๐ฅ๐ป๐ง) โง โ๐ค โ ๐ต โ๐ โ (๐ง๐ป๐ค)((๐(โจ๐ฆ, ๐งโฉ ยท ๐ค)๐)(โจ๐ฅ, ๐ฆโฉ ยท ๐ค)๐) = (๐(โจ๐ฅ, ๐งโฉ ยท ๐ค)(๐(โจ๐ฅ, ๐ฆโฉ ยท ๐ง)๐)))) โ โ๐ฅ โ ๐ต โ๐ โ (๐ฅ๐ป๐ฅ)โ๐ฆ โ ๐ต (โ๐ โ (๐ฆ๐ป๐ฅ)(๐(โจ๐ฆ, ๐ฅโฉ ยท ๐ฅ)๐) = ๐ โง โ๐ โ (๐ฅ๐ป๐ฆ)(๐(โจ๐ฅ, ๐ฅโฉ ยท ๐ฆ)๐) = ๐)) |
26 | 18, 23, 25 | 3syl 18 |
. 2
โข (๐ โ โ๐ฅ โ ๐ต โ๐ โ (๐ฅ๐ป๐ฅ)โ๐ฆ โ ๐ต (โ๐ โ (๐ฆ๐ป๐ฅ)(๐(โจ๐ฆ, ๐ฅโฉ ยท ๐ฅ)๐) = ๐ โง โ๐ โ (๐ฅ๐ป๐ฆ)(๐(โจ๐ฅ, ๐ฅโฉ ยท ๐ฆ)๐) = ๐)) |
27 | | catidex.x |
. 2
โข (๐ โ ๐ โ ๐ต) |
28 | 17, 26, 27 | rspcdva 3607 |
1
โข (๐ โ โ๐ โ (๐๐ป๐)โ๐ฆ โ ๐ต (โ๐ โ (๐ฆ๐ป๐)(๐(โจ๐ฆ, ๐โฉ ยท ๐)๐) = ๐ โง โ๐ โ (๐๐ป๐ฆ)(๐(โจ๐, ๐โฉ ยท ๐ฆ)๐) = ๐)) |