Step | Hyp | Ref
| Expression |
1 | | issect.b |
. . . 4
โข ๐ต = (Baseโ๐ถ) |
2 | | issect.h |
. . . 4
โข ๐ป = (Hom โ๐ถ) |
3 | | issect.o |
. . . 4
โข ยท =
(compโ๐ถ) |
4 | | issect.i |
. . . 4
โข 1 =
(Idโ๐ถ) |
5 | | issect.s |
. . . 4
โข ๐ = (Sectโ๐ถ) |
6 | | issect.c |
. . . 4
โข (๐ โ ๐ถ โ Cat) |
7 | | issect.x |
. . . 4
โข (๐ โ ๐ โ ๐ต) |
8 | | issect.y |
. . . 4
โข (๐ โ ๐ โ ๐ต) |
9 | 1, 2, 3, 4, 5, 6, 7, 8 | sectfval 17704 |
. . 3
โข (๐ โ (๐๐๐) = {โจ๐, ๐โฉ โฃ ((๐ โ (๐๐ป๐) โง ๐ โ (๐๐ป๐)) โง (๐(โจ๐, ๐โฉ ยท ๐)๐) = ( 1 โ๐))}) |
10 | 9 | breqd 5160 |
. 2
โข (๐ โ (๐น(๐๐๐)๐บ โ ๐น{โจ๐, ๐โฉ โฃ ((๐ โ (๐๐ป๐) โง ๐ โ (๐๐ป๐)) โง (๐(โจ๐, ๐โฉ ยท ๐)๐) = ( 1 โ๐))}๐บ)) |
11 | | oveq12 7422 |
. . . . . 6
โข ((๐ = ๐บ โง ๐ = ๐น) โ (๐(โจ๐, ๐โฉ ยท ๐)๐) = (๐บ(โจ๐, ๐โฉ ยท ๐)๐น)) |
12 | 11 | ancoms 457 |
. . . . 5
โข ((๐ = ๐น โง ๐ = ๐บ) โ (๐(โจ๐, ๐โฉ ยท ๐)๐) = (๐บ(โจ๐, ๐โฉ ยท ๐)๐น)) |
13 | 12 | eqeq1d 2732 |
. . . 4
โข ((๐ = ๐น โง ๐ = ๐บ) โ ((๐(โจ๐, ๐โฉ ยท ๐)๐) = ( 1 โ๐) โ (๐บ(โจ๐, ๐โฉ ยท ๐)๐น) = ( 1 โ๐))) |
14 | | eqid 2730 |
. . . 4
โข
{โจ๐, ๐โฉ โฃ ((๐ โ (๐๐ป๐) โง ๐ โ (๐๐ป๐)) โง (๐(โจ๐, ๐โฉ ยท ๐)๐) = ( 1 โ๐))} = {โจ๐, ๐โฉ โฃ ((๐ โ (๐๐ป๐) โง ๐ โ (๐๐ป๐)) โง (๐(โจ๐, ๐โฉ ยท ๐)๐) = ( 1 โ๐))} |
15 | 13, 14 | brab2a 5770 |
. . 3
โข (๐น{โจ๐, ๐โฉ โฃ ((๐ โ (๐๐ป๐) โง ๐ โ (๐๐ป๐)) โง (๐(โจ๐, ๐โฉ ยท ๐)๐) = ( 1 โ๐))}๐บ โ ((๐น โ (๐๐ป๐) โง ๐บ โ (๐๐ป๐)) โง (๐บ(โจ๐, ๐โฉ ยท ๐)๐น) = ( 1 โ๐))) |
16 | | df-3an 1087 |
. . 3
โข ((๐น โ (๐๐ป๐) โง ๐บ โ (๐๐ป๐) โง (๐บ(โจ๐, ๐โฉ ยท ๐)๐น) = ( 1 โ๐)) โ ((๐น โ (๐๐ป๐) โง ๐บ โ (๐๐ป๐)) โง (๐บ(โจ๐, ๐โฉ ยท ๐)๐น) = ( 1 โ๐))) |
17 | 15, 16 | bitr4i 277 |
. 2
โข (๐น{โจ๐, ๐โฉ โฃ ((๐ โ (๐๐ป๐) โง ๐ โ (๐๐ป๐)) โง (๐(โจ๐, ๐โฉ ยท ๐)๐) = ( 1 โ๐))}๐บ โ (๐น โ (๐๐ป๐) โง ๐บ โ (๐๐ป๐) โง (๐บ(โจ๐, ๐โฉ ยท ๐)๐น) = ( 1 โ๐))) |
18 | 10, 17 | bitrdi 286 |
1
โข (๐ โ (๐น(๐๐๐)๐บ โ (๐น โ (๐๐ป๐) โง ๐บ โ (๐๐ป๐) โง (๐บ(โจ๐, ๐โฉ ยท ๐)๐น) = ( 1 โ๐)))) |