Step | Hyp | Ref
| Expression |
1 | | issect.b |
. . 3
โข ๐ต = (Baseโ๐ถ) |
2 | | issect.h |
. . 3
โข ๐ป = (Hom โ๐ถ) |
3 | | issect.o |
. . 3
โข ยท =
(compโ๐ถ) |
4 | | issect.i |
. . 3
โข 1 =
(Idโ๐ถ) |
5 | | issect.s |
. . 3
โข ๐ = (Sectโ๐ถ) |
6 | | issect.c |
. . 3
โข (๐ โ ๐ถ โ Cat) |
7 | | issect.x |
. . 3
โข (๐ โ ๐ โ ๐ต) |
8 | 1, 2, 3, 4, 5, 6, 7, 7 | sectffval 17696 |
. 2
โข (๐ โ ๐ = (๐ฅ โ ๐ต, ๐ฆ โ ๐ต โฆ {โจ๐, ๐โฉ โฃ ((๐ โ (๐ฅ๐ป๐ฆ) โง ๐ โ (๐ฆ๐ป๐ฅ)) โง (๐(โจ๐ฅ, ๐ฆโฉ ยท ๐ฅ)๐) = ( 1 โ๐ฅ))})) |
9 | | simprl 769 |
. . . . . . 7
โข ((๐ โง (๐ฅ = ๐ โง ๐ฆ = ๐)) โ ๐ฅ = ๐) |
10 | | simprr 771 |
. . . . . . 7
โข ((๐ โง (๐ฅ = ๐ โง ๐ฆ = ๐)) โ ๐ฆ = ๐) |
11 | 9, 10 | oveq12d 7426 |
. . . . . 6
โข ((๐ โง (๐ฅ = ๐ โง ๐ฆ = ๐)) โ (๐ฅ๐ป๐ฆ) = (๐๐ป๐)) |
12 | 11 | eleq2d 2819 |
. . . . 5
โข ((๐ โง (๐ฅ = ๐ โง ๐ฆ = ๐)) โ (๐ โ (๐ฅ๐ป๐ฆ) โ ๐ โ (๐๐ป๐))) |
13 | 10, 9 | oveq12d 7426 |
. . . . . 6
โข ((๐ โง (๐ฅ = ๐ โง ๐ฆ = ๐)) โ (๐ฆ๐ป๐ฅ) = (๐๐ป๐)) |
14 | 13 | eleq2d 2819 |
. . . . 5
โข ((๐ โง (๐ฅ = ๐ โง ๐ฆ = ๐)) โ (๐ โ (๐ฆ๐ป๐ฅ) โ ๐ โ (๐๐ป๐))) |
15 | 12, 14 | anbi12d 631 |
. . . 4
โข ((๐ โง (๐ฅ = ๐ โง ๐ฆ = ๐)) โ ((๐ โ (๐ฅ๐ป๐ฆ) โง ๐ โ (๐ฆ๐ป๐ฅ)) โ (๐ โ (๐๐ป๐) โง ๐ โ (๐๐ป๐)))) |
16 | 9, 10 | opeq12d 4881 |
. . . . . . 7
โข ((๐ โง (๐ฅ = ๐ โง ๐ฆ = ๐)) โ โจ๐ฅ, ๐ฆโฉ = โจ๐, ๐โฉ) |
17 | 16, 9 | oveq12d 7426 |
. . . . . 6
โข ((๐ โง (๐ฅ = ๐ โง ๐ฆ = ๐)) โ (โจ๐ฅ, ๐ฆโฉ ยท ๐ฅ) = (โจ๐, ๐โฉ ยท ๐)) |
18 | 17 | oveqd 7425 |
. . . . 5
โข ((๐ โง (๐ฅ = ๐ โง ๐ฆ = ๐)) โ (๐(โจ๐ฅ, ๐ฆโฉ ยท ๐ฅ)๐) = (๐(โจ๐, ๐โฉ ยท ๐)๐)) |
19 | 9 | fveq2d 6895 |
. . . . 5
โข ((๐ โง (๐ฅ = ๐ โง ๐ฆ = ๐)) โ ( 1 โ๐ฅ) = ( 1 โ๐)) |
20 | 18, 19 | eqeq12d 2748 |
. . . 4
โข ((๐ โง (๐ฅ = ๐ โง ๐ฆ = ๐)) โ ((๐(โจ๐ฅ, ๐ฆโฉ ยท ๐ฅ)๐) = ( 1 โ๐ฅ) โ (๐(โจ๐, ๐โฉ ยท ๐)๐) = ( 1 โ๐))) |
21 | 15, 20 | anbi12d 631 |
. . 3
โข ((๐ โง (๐ฅ = ๐ โง ๐ฆ = ๐)) โ (((๐ โ (๐ฅ๐ป๐ฆ) โง ๐ โ (๐ฆ๐ป๐ฅ)) โง (๐(โจ๐ฅ, ๐ฆโฉ ยท ๐ฅ)๐) = ( 1 โ๐ฅ)) โ ((๐ โ (๐๐ป๐) โง ๐ โ (๐๐ป๐)) โง (๐(โจ๐, ๐โฉ ยท ๐)๐) = ( 1 โ๐)))) |
22 | 21 | opabbidv 5214 |
. 2
โข ((๐ โง (๐ฅ = ๐ โง ๐ฆ = ๐)) โ {โจ๐, ๐โฉ โฃ ((๐ โ (๐ฅ๐ป๐ฆ) โง ๐ โ (๐ฆ๐ป๐ฅ)) โง (๐(โจ๐ฅ, ๐ฆโฉ ยท ๐ฅ)๐) = ( 1 โ๐ฅ))} = {โจ๐, ๐โฉ โฃ ((๐ โ (๐๐ป๐) โง ๐ โ (๐๐ป๐)) โง (๐(โจ๐, ๐โฉ ยท ๐)๐) = ( 1 โ๐))}) |
23 | | issect.y |
. 2
โข (๐ โ ๐ โ ๐ต) |
24 | | ovex 7441 |
. . . . 5
โข (๐๐ป๐) โ V |
25 | | ovex 7441 |
. . . . 5
โข (๐๐ป๐) โ V |
26 | 24, 25 | xpex 7739 |
. . . 4
โข ((๐๐ป๐) ร (๐๐ป๐)) โ V |
27 | | opabssxp 5768 |
. . . 4
โข
{โจ๐, ๐โฉ โฃ ((๐ โ (๐๐ป๐) โง ๐ โ (๐๐ป๐)) โง (๐(โจ๐, ๐โฉ ยท ๐)๐) = ( 1 โ๐))} โ ((๐๐ป๐) ร (๐๐ป๐)) |
28 | 26, 27 | ssexi 5322 |
. . 3
โข
{โจ๐, ๐โฉ โฃ ((๐ โ (๐๐ป๐) โง ๐ โ (๐๐ป๐)) โง (๐(โจ๐, ๐โฉ ยท ๐)๐) = ( 1 โ๐))} โ V |
29 | 28 | a1i 11 |
. 2
โข (๐ โ {โจ๐, ๐โฉ โฃ ((๐ โ (๐๐ป๐) โง ๐ โ (๐๐ป๐)) โง (๐(โจ๐, ๐โฉ ยท ๐)๐) = ( 1 โ๐))} โ V) |
30 | 8, 22, 7, 23, 29 | ovmpod 7559 |
1
โข (๐ โ (๐๐๐) = {โจ๐, ๐โฉ โฃ ((๐ โ (๐๐ป๐) โง ๐ โ (๐๐ป๐)) โง (๐(โจ๐, ๐โฉ ยท ๐)๐) = ( 1 โ๐))}) |