Step |
Hyp |
Ref |
Expression |
1 |
|
rescbas.d |
โข ๐ท = ( ๐ถ โพcat ๐ป ) |
2 |
|
rescbas.b |
โข ๐ต = ( Base โ ๐ถ ) |
3 |
|
rescbas.c |
โข ( ๐ โ ๐ถ โ ๐ ) |
4 |
|
rescbas.h |
โข ( ๐ โ ๐ป Fn ( ๐ ร ๐ ) ) |
5 |
|
rescbas.s |
โข ( ๐ โ ๐ โ ๐ต ) |
6 |
|
rescco.o |
โข ยท = ( comp โ ๐ถ ) |
7 |
|
ccoid |
โข comp = Slot ( comp โ ndx ) |
8 |
|
slotsbhcdif |
โข ( ( Base โ ndx ) โ ( Hom โ ndx ) โง ( Base โ ndx ) โ ( comp โ ndx ) โง ( Hom โ ndx ) โ ( comp โ ndx ) ) |
9 |
|
simp3 |
โข ( ( ( Base โ ndx ) โ ( Hom โ ndx ) โง ( Base โ ndx ) โ ( comp โ ndx ) โง ( Hom โ ndx ) โ ( comp โ ndx ) ) โ ( Hom โ ndx ) โ ( comp โ ndx ) ) |
10 |
9
|
necomd |
โข ( ( ( Base โ ndx ) โ ( Hom โ ndx ) โง ( Base โ ndx ) โ ( comp โ ndx ) โง ( Hom โ ndx ) โ ( comp โ ndx ) ) โ ( comp โ ndx ) โ ( Hom โ ndx ) ) |
11 |
8 10
|
ax-mp |
โข ( comp โ ndx ) โ ( Hom โ ndx ) |
12 |
7 11
|
setsnid |
โข ( comp โ ( ๐ถ โพs ๐ ) ) = ( comp โ ( ( ๐ถ โพs ๐ ) sSet โจ ( Hom โ ndx ) , ๐ป โฉ ) ) |
13 |
2
|
fvexi |
โข ๐ต โ V |
14 |
13
|
ssex |
โข ( ๐ โ ๐ต โ ๐ โ V ) |
15 |
5 14
|
syl |
โข ( ๐ โ ๐ โ V ) |
16 |
|
eqid |
โข ( ๐ถ โพs ๐ ) = ( ๐ถ โพs ๐ ) |
17 |
16 6
|
ressco |
โข ( ๐ โ V โ ยท = ( comp โ ( ๐ถ โพs ๐ ) ) ) |
18 |
15 17
|
syl |
โข ( ๐ โ ยท = ( comp โ ( ๐ถ โพs ๐ ) ) ) |
19 |
1 3 15 4
|
rescval2 |
โข ( ๐ โ ๐ท = ( ( ๐ถ โพs ๐ ) sSet โจ ( Hom โ ndx ) , ๐ป โฉ ) ) |
20 |
19
|
fveq2d |
โข ( ๐ โ ( comp โ ๐ท ) = ( comp โ ( ( ๐ถ โพs ๐ ) sSet โจ ( Hom โ ndx ) , ๐ป โฉ ) ) ) |
21 |
12 18 20
|
3eqtr4a |
โข ( ๐ โ ยท = ( comp โ ๐ท ) ) |