Step | Hyp | Ref
| Expression |
1 | | eqid 2733 |
. . . . . 6
โข
(Baseโ๐ถ) =
(Baseโ๐ถ) |
2 | | eqid 2733 |
. . . . . 6
โข (Hom
โ๐ถ) = (Hom
โ๐ถ) |
3 | | eqid 2733 |
. . . . . 6
โข
(compโ๐ถ) =
(compโ๐ถ) |
4 | | eqid 2733 |
. . . . . 6
โข
(compโ๐ท) =
(compโ๐ท) |
5 | | oppchomfpropd.1 |
. . . . . . 7
โข (๐ โ (Homf
โ๐ถ) =
(Homf โ๐ท)) |
6 | 5 | ad2antrr 725 |
. . . . . 6
โข (((๐ โง (๐ฅ โ (Baseโ๐ถ) โง ๐ฆ โ (Baseโ๐ถ) โง ๐ง โ (Baseโ๐ถ))) โง (๐ โ (๐ฅ(Hom โ(oppCatโ๐ถ))๐ฆ) โง ๐ โ (๐ฆ(Hom โ(oppCatโ๐ถ))๐ง))) โ (Homf
โ๐ถ) =
(Homf โ๐ท)) |
7 | | oppccomfpropd.1 |
. . . . . . 7
โข (๐ โ
(compfโ๐ถ) = (compfโ๐ท)) |
8 | 7 | ad2antrr 725 |
. . . . . 6
โข (((๐ โง (๐ฅ โ (Baseโ๐ถ) โง ๐ฆ โ (Baseโ๐ถ) โง ๐ง โ (Baseโ๐ถ))) โง (๐ โ (๐ฅ(Hom โ(oppCatโ๐ถ))๐ฆ) โง ๐ โ (๐ฆ(Hom โ(oppCatโ๐ถ))๐ง))) โ
(compfโ๐ถ) = (compfโ๐ท)) |
9 | | simplr3 1218 |
. . . . . 6
โข (((๐ โง (๐ฅ โ (Baseโ๐ถ) โง ๐ฆ โ (Baseโ๐ถ) โง ๐ง โ (Baseโ๐ถ))) โง (๐ โ (๐ฅ(Hom โ(oppCatโ๐ถ))๐ฆ) โง ๐ โ (๐ฆ(Hom โ(oppCatโ๐ถ))๐ง))) โ ๐ง โ (Baseโ๐ถ)) |
10 | | simplr2 1217 |
. . . . . 6
โข (((๐ โง (๐ฅ โ (Baseโ๐ถ) โง ๐ฆ โ (Baseโ๐ถ) โง ๐ง โ (Baseโ๐ถ))) โง (๐ โ (๐ฅ(Hom โ(oppCatโ๐ถ))๐ฆ) โง ๐ โ (๐ฆ(Hom โ(oppCatโ๐ถ))๐ง))) โ ๐ฆ โ (Baseโ๐ถ)) |
11 | | simplr1 1216 |
. . . . . 6
โข (((๐ โง (๐ฅ โ (Baseโ๐ถ) โง ๐ฆ โ (Baseโ๐ถ) โง ๐ง โ (Baseโ๐ถ))) โง (๐ โ (๐ฅ(Hom โ(oppCatโ๐ถ))๐ฆ) โง ๐ โ (๐ฆ(Hom โ(oppCatโ๐ถ))๐ง))) โ ๐ฅ โ (Baseโ๐ถ)) |
12 | | simprr 772 |
. . . . . . 7
โข (((๐ โง (๐ฅ โ (Baseโ๐ถ) โง ๐ฆ โ (Baseโ๐ถ) โง ๐ง โ (Baseโ๐ถ))) โง (๐ โ (๐ฅ(Hom โ(oppCatโ๐ถ))๐ฆ) โง ๐ โ (๐ฆ(Hom โ(oppCatโ๐ถ))๐ง))) โ ๐ โ (๐ฆ(Hom โ(oppCatโ๐ถ))๐ง)) |
13 | | eqid 2733 |
. . . . . . . 8
โข
(oppCatโ๐ถ) =
(oppCatโ๐ถ) |
14 | 2, 13 | oppchom 17660 |
. . . . . . 7
โข (๐ฆ(Hom โ(oppCatโ๐ถ))๐ง) = (๐ง(Hom โ๐ถ)๐ฆ) |
15 | 12, 14 | eleqtrdi 2844 |
. . . . . 6
โข (((๐ โง (๐ฅ โ (Baseโ๐ถ) โง ๐ฆ โ (Baseโ๐ถ) โง ๐ง โ (Baseโ๐ถ))) โง (๐ โ (๐ฅ(Hom โ(oppCatโ๐ถ))๐ฆ) โง ๐ โ (๐ฆ(Hom โ(oppCatโ๐ถ))๐ง))) โ ๐ โ (๐ง(Hom โ๐ถ)๐ฆ)) |
16 | | simprl 770 |
. . . . . . 7
โข (((๐ โง (๐ฅ โ (Baseโ๐ถ) โง ๐ฆ โ (Baseโ๐ถ) โง ๐ง โ (Baseโ๐ถ))) โง (๐ โ (๐ฅ(Hom โ(oppCatโ๐ถ))๐ฆ) โง ๐ โ (๐ฆ(Hom โ(oppCatโ๐ถ))๐ง))) โ ๐ โ (๐ฅ(Hom โ(oppCatโ๐ถ))๐ฆ)) |
17 | 2, 13 | oppchom 17660 |
. . . . . . 7
โข (๐ฅ(Hom โ(oppCatโ๐ถ))๐ฆ) = (๐ฆ(Hom โ๐ถ)๐ฅ) |
18 | 16, 17 | eleqtrdi 2844 |
. . . . . 6
โข (((๐ โง (๐ฅ โ (Baseโ๐ถ) โง ๐ฆ โ (Baseโ๐ถ) โง ๐ง โ (Baseโ๐ถ))) โง (๐ โ (๐ฅ(Hom โ(oppCatโ๐ถ))๐ฆ) โง ๐ โ (๐ฆ(Hom โ(oppCatโ๐ถ))๐ง))) โ ๐ โ (๐ฆ(Hom โ๐ถ)๐ฅ)) |
19 | 1, 2, 3, 4, 6, 8, 9, 10, 11, 15, 18 | comfeqval 17652 |
. . . . 5
โข (((๐ โง (๐ฅ โ (Baseโ๐ถ) โง ๐ฆ โ (Baseโ๐ถ) โง ๐ง โ (Baseโ๐ถ))) โง (๐ โ (๐ฅ(Hom โ(oppCatโ๐ถ))๐ฆ) โง ๐ โ (๐ฆ(Hom โ(oppCatโ๐ถ))๐ง))) โ (๐(โจ๐ง, ๐ฆโฉ(compโ๐ถ)๐ฅ)๐) = (๐(โจ๐ง, ๐ฆโฉ(compโ๐ท)๐ฅ)๐)) |
20 | 1, 3, 13, 11, 10, 9 | oppcco 17662 |
. . . . 5
โข (((๐ โง (๐ฅ โ (Baseโ๐ถ) โง ๐ฆ โ (Baseโ๐ถ) โง ๐ง โ (Baseโ๐ถ))) โง (๐ โ (๐ฅ(Hom โ(oppCatโ๐ถ))๐ฆ) โง ๐ โ (๐ฆ(Hom โ(oppCatโ๐ถ))๐ง))) โ (๐(โจ๐ฅ, ๐ฆโฉ(compโ(oppCatโ๐ถ))๐ง)๐) = (๐(โจ๐ง, ๐ฆโฉ(compโ๐ถ)๐ฅ)๐)) |
21 | | eqid 2733 |
. . . . . 6
โข
(Baseโ๐ท) =
(Baseโ๐ท) |
22 | | eqid 2733 |
. . . . . 6
โข
(oppCatโ๐ท) =
(oppCatโ๐ท) |
23 | 5 | homfeqbas 17640 |
. . . . . . . 8
โข (๐ โ (Baseโ๐ถ) = (Baseโ๐ท)) |
24 | 23 | ad2antrr 725 |
. . . . . . 7
โข (((๐ โง (๐ฅ โ (Baseโ๐ถ) โง ๐ฆ โ (Baseโ๐ถ) โง ๐ง โ (Baseโ๐ถ))) โง (๐ โ (๐ฅ(Hom โ(oppCatโ๐ถ))๐ฆ) โง ๐ โ (๐ฆ(Hom โ(oppCatโ๐ถ))๐ง))) โ (Baseโ๐ถ) = (Baseโ๐ท)) |
25 | 11, 24 | eleqtrd 2836 |
. . . . . 6
โข (((๐ โง (๐ฅ โ (Baseโ๐ถ) โง ๐ฆ โ (Baseโ๐ถ) โง ๐ง โ (Baseโ๐ถ))) โง (๐ โ (๐ฅ(Hom โ(oppCatโ๐ถ))๐ฆ) โง ๐ โ (๐ฆ(Hom โ(oppCatโ๐ถ))๐ง))) โ ๐ฅ โ (Baseโ๐ท)) |
26 | 10, 24 | eleqtrd 2836 |
. . . . . 6
โข (((๐ โง (๐ฅ โ (Baseโ๐ถ) โง ๐ฆ โ (Baseโ๐ถ) โง ๐ง โ (Baseโ๐ถ))) โง (๐ โ (๐ฅ(Hom โ(oppCatโ๐ถ))๐ฆ) โง ๐ โ (๐ฆ(Hom โ(oppCatโ๐ถ))๐ง))) โ ๐ฆ โ (Baseโ๐ท)) |
27 | 9, 24 | eleqtrd 2836 |
. . . . . 6
โข (((๐ โง (๐ฅ โ (Baseโ๐ถ) โง ๐ฆ โ (Baseโ๐ถ) โง ๐ง โ (Baseโ๐ถ))) โง (๐ โ (๐ฅ(Hom โ(oppCatโ๐ถ))๐ฆ) โง ๐ โ (๐ฆ(Hom โ(oppCatโ๐ถ))๐ง))) โ ๐ง โ (Baseโ๐ท)) |
28 | 21, 4, 22, 25, 26, 27 | oppcco 17662 |
. . . . 5
โข (((๐ โง (๐ฅ โ (Baseโ๐ถ) โง ๐ฆ โ (Baseโ๐ถ) โง ๐ง โ (Baseโ๐ถ))) โง (๐ โ (๐ฅ(Hom โ(oppCatโ๐ถ))๐ฆ) โง ๐ โ (๐ฆ(Hom โ(oppCatโ๐ถ))๐ง))) โ (๐(โจ๐ฅ, ๐ฆโฉ(compโ(oppCatโ๐ท))๐ง)๐) = (๐(โจ๐ง, ๐ฆโฉ(compโ๐ท)๐ฅ)๐)) |
29 | 19, 20, 28 | 3eqtr4d 2783 |
. . . 4
โข (((๐ โง (๐ฅ โ (Baseโ๐ถ) โง ๐ฆ โ (Baseโ๐ถ) โง ๐ง โ (Baseโ๐ถ))) โง (๐ โ (๐ฅ(Hom โ(oppCatโ๐ถ))๐ฆ) โง ๐ โ (๐ฆ(Hom โ(oppCatโ๐ถ))๐ง))) โ (๐(โจ๐ฅ, ๐ฆโฉ(compโ(oppCatโ๐ถ))๐ง)๐) = (๐(โจ๐ฅ, ๐ฆโฉ(compโ(oppCatโ๐ท))๐ง)๐)) |
30 | 29 | ralrimivva 3201 |
. . 3
โข ((๐ โง (๐ฅ โ (Baseโ๐ถ) โง ๐ฆ โ (Baseโ๐ถ) โง ๐ง โ (Baseโ๐ถ))) โ โ๐ โ (๐ฅ(Hom โ(oppCatโ๐ถ))๐ฆ)โ๐ โ (๐ฆ(Hom โ(oppCatโ๐ถ))๐ง)(๐(โจ๐ฅ, ๐ฆโฉ(compโ(oppCatโ๐ถ))๐ง)๐) = (๐(โจ๐ฅ, ๐ฆโฉ(compโ(oppCatโ๐ท))๐ง)๐)) |
31 | 30 | ralrimivvva 3204 |
. 2
โข (๐ โ โ๐ฅ โ (Baseโ๐ถ)โ๐ฆ โ (Baseโ๐ถ)โ๐ง โ (Baseโ๐ถ)โ๐ โ (๐ฅ(Hom โ(oppCatโ๐ถ))๐ฆ)โ๐ โ (๐ฆ(Hom โ(oppCatโ๐ถ))๐ง)(๐(โจ๐ฅ, ๐ฆโฉ(compโ(oppCatโ๐ถ))๐ง)๐) = (๐(โจ๐ฅ, ๐ฆโฉ(compโ(oppCatโ๐ท))๐ง)๐)) |
32 | | eqid 2733 |
. . 3
โข
(compโ(oppCatโ๐ถ)) = (compโ(oppCatโ๐ถ)) |
33 | | eqid 2733 |
. . 3
โข
(compโ(oppCatโ๐ท)) = (compโ(oppCatโ๐ท)) |
34 | | eqid 2733 |
. . 3
โข (Hom
โ(oppCatโ๐ถ)) =
(Hom โ(oppCatโ๐ถ)) |
35 | 13, 1 | oppcbas 17663 |
. . . 4
โข
(Baseโ๐ถ) =
(Baseโ(oppCatโ๐ถ)) |
36 | 35 | a1i 11 |
. . 3
โข (๐ โ (Baseโ๐ถ) =
(Baseโ(oppCatโ๐ถ))) |
37 | 22, 21 | oppcbas 17663 |
. . . 4
โข
(Baseโ๐ท) =
(Baseโ(oppCatโ๐ท)) |
38 | 23, 37 | eqtrdi 2789 |
. . 3
โข (๐ โ (Baseโ๐ถ) =
(Baseโ(oppCatโ๐ท))) |
39 | 5 | oppchomfpropd 17672 |
. . 3
โข (๐ โ (Homf
โ(oppCatโ๐ถ)) =
(Homf โ(oppCatโ๐ท))) |
40 | 32, 33, 34, 36, 38, 39 | comfeq 17650 |
. 2
โข (๐ โ
((compfโ(oppCatโ๐ถ)) =
(compfโ(oppCatโ๐ท)) โ โ๐ฅ โ (Baseโ๐ถ)โ๐ฆ โ (Baseโ๐ถ)โ๐ง โ (Baseโ๐ถ)โ๐ โ (๐ฅ(Hom โ(oppCatโ๐ถ))๐ฆ)โ๐ โ (๐ฆ(Hom โ(oppCatโ๐ถ))๐ง)(๐(โจ๐ฅ, ๐ฆโฉ(compโ(oppCatโ๐ถ))๐ง)๐) = (๐(โจ๐ฅ, ๐ฆโฉ(compโ(oppCatโ๐ท))๐ง)๐))) |
41 | 31, 40 | mpbird 257 |
1
โข (๐ โ
(compfโ(oppCatโ๐ถ)) =
(compfโ(oppCatโ๐ท))) |