Metamath Proof Explorer


Theorem rescco

Description: Composition in the category restriction. (Contributed by Mario Carneiro, 4-Jan-2017) (Proof shortened by AV, 13-Oct-2024)

Ref Expression
Hypotheses rescbas.d โŠข ๐ท = ( ๐ถ โ†พcat ๐ป )
rescbas.b โŠข ๐ต = ( Base โ€˜ ๐ถ )
rescbas.c โŠข ( ๐œ‘ โ†’ ๐ถ โˆˆ ๐‘‰ )
rescbas.h โŠข ( ๐œ‘ โ†’ ๐ป Fn ( ๐‘† ร— ๐‘† ) )
rescbas.s โŠข ( ๐œ‘ โ†’ ๐‘† โŠ† ๐ต )
rescco.o โŠข ยท = ( comp โ€˜ ๐ถ )
Assertion rescco ( ๐œ‘ โ†’ ยท = ( comp โ€˜ ๐ท ) )

Proof

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 โ€˜ ๐ท ) )