Metamath Proof Explorer

Theorem estrccofval

Description: Composition in the category of extensible structures. (Contributed by AV, 7-Mar-2020)

Ref Expression
Hypotheses estrcbas.c โŠข ๐ถ = ( ExtStrCat โ€˜ ๐‘ˆ )
estrcbas.u โŠข ( ๐œ‘ โ†’ ๐‘ˆ โˆˆ ๐‘‰ )
estrcco.o โŠข ยท = ( comp โ€˜ ๐ถ )
Assertion estrccofval ( ๐œ‘ โ†’ ยท = ( ๐‘ฃ โˆˆ ( ๐‘ˆ ร— ๐‘ˆ ) , ๐‘ง โˆˆ ๐‘ˆ โ†ฆ ( ๐‘” โˆˆ ( ( Base โ€˜ ๐‘ง ) โ†‘m ( Base โ€˜ ( 2nd โ€˜ ๐‘ฃ ) ) ) , ๐‘“ โˆˆ ( ( Base โ€˜ ( 2nd โ€˜ ๐‘ฃ ) ) โ†‘m ( Base โ€˜ ( 1st โ€˜ ๐‘ฃ ) ) ) โ†ฆ ( ๐‘” โˆ˜ ๐‘“ ) ) ) )

Proof

Step Hyp Ref Expression
1 estrcbas.c โŠข ๐ถ = ( ExtStrCat โ€˜ ๐‘ˆ )
2 estrcbas.u โŠข ( ๐œ‘ โ†’ ๐‘ˆ โˆˆ ๐‘‰ )
3 estrcco.o โŠข ยท = ( comp โ€˜ ๐ถ )
4 eqid โŠข ( Hom โ€˜ ๐ถ ) = ( Hom โ€˜ ๐ถ )
5 1 2 4 estrchomfval โŠข ( ๐œ‘ โ†’ ( Hom โ€˜ ๐ถ ) = ( ๐‘ฅ โˆˆ ๐‘ˆ , ๐‘ฆ โˆˆ ๐‘ˆ โ†ฆ ( ( Base โ€˜ ๐‘ฆ ) โ†‘m ( Base โ€˜ ๐‘ฅ ) ) ) )
6 eqidd โŠข ( ๐œ‘ โ†’ ( ๐‘ฃ โˆˆ ( ๐‘ˆ ร— ๐‘ˆ ) , ๐‘ง โˆˆ ๐‘ˆ โ†ฆ ( ๐‘” โˆˆ ( ( Base โ€˜ ๐‘ง ) โ†‘m ( Base โ€˜ ( 2nd โ€˜ ๐‘ฃ ) ) ) , ๐‘“ โˆˆ ( ( Base โ€˜ ( 2nd โ€˜ ๐‘ฃ ) ) โ†‘m ( Base โ€˜ ( 1st โ€˜ ๐‘ฃ ) ) ) โ†ฆ ( ๐‘” โˆ˜ ๐‘“ ) ) ) = ( ๐‘ฃ โˆˆ ( ๐‘ˆ ร— ๐‘ˆ ) , ๐‘ง โˆˆ ๐‘ˆ โ†ฆ ( ๐‘” โˆˆ ( ( Base โ€˜ ๐‘ง ) โ†‘m ( Base โ€˜ ( 2nd โ€˜ ๐‘ฃ ) ) ) , ๐‘“ โˆˆ ( ( Base โ€˜ ( 2nd โ€˜ ๐‘ฃ ) ) โ†‘m ( Base โ€˜ ( 1st โ€˜ ๐‘ฃ ) ) ) โ†ฆ ( ๐‘” โˆ˜ ๐‘“ ) ) ) )
7 1 2 5 6 estrcval โŠข ( ๐œ‘ โ†’ ๐ถ = { โŸจ ( Base โ€˜ ndx ) , ๐‘ˆ โŸฉ , โŸจ ( Hom โ€˜ ndx ) , ( Hom โ€˜ ๐ถ ) โŸฉ , โŸจ ( comp โ€˜ ndx ) , ( ๐‘ฃ โˆˆ ( ๐‘ˆ ร— ๐‘ˆ ) , ๐‘ง โˆˆ ๐‘ˆ โ†ฆ ( ๐‘” โˆˆ ( ( Base โ€˜ ๐‘ง ) โ†‘m ( Base โ€˜ ( 2nd โ€˜ ๐‘ฃ ) ) ) , ๐‘“ โˆˆ ( ( Base โ€˜ ( 2nd โ€˜ ๐‘ฃ ) ) โ†‘m ( Base โ€˜ ( 1st โ€˜ ๐‘ฃ ) ) ) โ†ฆ ( ๐‘” โˆ˜ ๐‘“ ) ) ) โŸฉ } )
8 catstr โŠข { โŸจ ( Base โ€˜ ndx ) , ๐‘ˆ โŸฉ , โŸจ ( Hom โ€˜ ndx ) , ( Hom โ€˜ ๐ถ ) โŸฉ , โŸจ ( comp โ€˜ ndx ) , ( ๐‘ฃ โˆˆ ( ๐‘ˆ ร— ๐‘ˆ ) , ๐‘ง โˆˆ ๐‘ˆ โ†ฆ ( ๐‘” โˆˆ ( ( Base โ€˜ ๐‘ง ) โ†‘m ( Base โ€˜ ( 2nd โ€˜ ๐‘ฃ ) ) ) , ๐‘“ โˆˆ ( ( Base โ€˜ ( 2nd โ€˜ ๐‘ฃ ) ) โ†‘m ( Base โ€˜ ( 1st โ€˜ ๐‘ฃ ) ) ) โ†ฆ ( ๐‘” โˆ˜ ๐‘“ ) ) ) โŸฉ } Struct โŸจ 1 , 1 5 โŸฉ
9 ccoid โŠข comp = Slot ( comp โ€˜ ndx )
10 snsstp3 โŠข { โŸจ ( comp โ€˜ ndx ) , ( ๐‘ฃ โˆˆ ( ๐‘ˆ ร— ๐‘ˆ ) , ๐‘ง โˆˆ ๐‘ˆ โ†ฆ ( ๐‘” โˆˆ ( ( Base โ€˜ ๐‘ง ) โ†‘m ( Base โ€˜ ( 2nd โ€˜ ๐‘ฃ ) ) ) , ๐‘“ โˆˆ ( ( Base โ€˜ ( 2nd โ€˜ ๐‘ฃ ) ) โ†‘m ( Base โ€˜ ( 1st โ€˜ ๐‘ฃ ) ) ) โ†ฆ ( ๐‘” โˆ˜ ๐‘“ ) ) ) โŸฉ } โŠ† { โŸจ ( Base โ€˜ ndx ) , ๐‘ˆ โŸฉ , โŸจ ( Hom โ€˜ ndx ) , ( Hom โ€˜ ๐ถ ) โŸฉ , โŸจ ( comp โ€˜ ndx ) , ( ๐‘ฃ โˆˆ ( ๐‘ˆ ร— ๐‘ˆ ) , ๐‘ง โˆˆ ๐‘ˆ โ†ฆ ( ๐‘” โˆˆ ( ( Base โ€˜ ๐‘ง ) โ†‘m ( Base โ€˜ ( 2nd โ€˜ ๐‘ฃ ) ) ) , ๐‘“ โˆˆ ( ( Base โ€˜ ( 2nd โ€˜ ๐‘ฃ ) ) โ†‘m ( Base โ€˜ ( 1st โ€˜ ๐‘ฃ ) ) ) โ†ฆ ( ๐‘” โˆ˜ ๐‘“ ) ) ) โŸฉ }
11 2 2 xpexd โŠข ( ๐œ‘ โ†’ ( ๐‘ˆ ร— ๐‘ˆ ) โˆˆ V )
12 mpoexga โŠข ( ( ( ๐‘ˆ ร— ๐‘ˆ ) โˆˆ V โˆง ๐‘ˆ โˆˆ ๐‘‰ ) โ†’ ( ๐‘ฃ โˆˆ ( ๐‘ˆ ร— ๐‘ˆ ) , ๐‘ง โˆˆ ๐‘ˆ โ†ฆ ( ๐‘” โˆˆ ( ( Base โ€˜ ๐‘ง ) โ†‘m ( Base โ€˜ ( 2nd โ€˜ ๐‘ฃ ) ) ) , ๐‘“ โˆˆ ( ( Base โ€˜ ( 2nd โ€˜ ๐‘ฃ ) ) โ†‘m ( Base โ€˜ ( 1st โ€˜ ๐‘ฃ ) ) ) โ†ฆ ( ๐‘” โˆ˜ ๐‘“ ) ) ) โˆˆ V )
13 11 2 12 syl2anc โŠข ( ๐œ‘ โ†’ ( ๐‘ฃ โˆˆ ( ๐‘ˆ ร— ๐‘ˆ ) , ๐‘ง โˆˆ ๐‘ˆ โ†ฆ ( ๐‘” โˆˆ ( ( Base โ€˜ ๐‘ง ) โ†‘m ( Base โ€˜ ( 2nd โ€˜ ๐‘ฃ ) ) ) , ๐‘“ โˆˆ ( ( Base โ€˜ ( 2nd โ€˜ ๐‘ฃ ) ) โ†‘m ( Base โ€˜ ( 1st โ€˜ ๐‘ฃ ) ) ) โ†ฆ ( ๐‘” โˆ˜ ๐‘“ ) ) ) โˆˆ V )
14 7 8 9 10 13 3 strfv3 โŠข ( ๐œ‘ โ†’ ยท = ( ๐‘ฃ โˆˆ ( ๐‘ˆ ร— ๐‘ˆ ) , ๐‘ง โˆˆ ๐‘ˆ โ†ฆ ( ๐‘” โˆˆ ( ( Base โ€˜ ๐‘ง ) โ†‘m ( Base โ€˜ ( 2nd โ€˜ ๐‘ฃ ) ) ) , ๐‘“ โˆˆ ( ( Base โ€˜ ( 2nd โ€˜ ๐‘ฃ ) ) โ†‘m ( Base โ€˜ ( 1st โ€˜ ๐‘ฃ ) ) ) โ†ฆ ( ๐‘” โˆ˜ ๐‘“ ) ) ) )