Metamath Proof Explorer


Theorem subccocl

Description: A subcategory is closed under composition. (Contributed by Mario Carneiro, 4-Jan-2017)

Ref Expression
Hypotheses subcidcl.j โŠข ( ๐œ‘ โ†’ ๐ฝ โˆˆ ( Subcat โ€˜ ๐ถ ) )
subcidcl.2 โŠข ( ๐œ‘ โ†’ ๐ฝ Fn ( ๐‘† ร— ๐‘† ) )
subcidcl.x โŠข ( ๐œ‘ โ†’ ๐‘‹ โˆˆ ๐‘† )
subccocl.o โŠข ยท = ( comp โ€˜ ๐ถ )
subccocl.y โŠข ( ๐œ‘ โ†’ ๐‘Œ โˆˆ ๐‘† )
subccocl.z โŠข ( ๐œ‘ โ†’ ๐‘ โˆˆ ๐‘† )
subccocl.f โŠข ( ๐œ‘ โ†’ ๐น โˆˆ ( ๐‘‹ ๐ฝ ๐‘Œ ) )
subccocl.g โŠข ( ๐œ‘ โ†’ ๐บ โˆˆ ( ๐‘Œ ๐ฝ ๐‘ ) )
Assertion subccocl ( ๐œ‘ โ†’ ( ๐บ ( โŸจ ๐‘‹ , ๐‘Œ โŸฉ ยท ๐‘ ) ๐น ) โˆˆ ( ๐‘‹ ๐ฝ ๐‘ ) )

Proof

Step Hyp Ref Expression
1 subcidcl.j โŠข ( ๐œ‘ โ†’ ๐ฝ โˆˆ ( Subcat โ€˜ ๐ถ ) )
2 subcidcl.2 โŠข ( ๐œ‘ โ†’ ๐ฝ Fn ( ๐‘† ร— ๐‘† ) )
3 subcidcl.x โŠข ( ๐œ‘ โ†’ ๐‘‹ โˆˆ ๐‘† )
4 subccocl.o โŠข ยท = ( comp โ€˜ ๐ถ )
5 subccocl.y โŠข ( ๐œ‘ โ†’ ๐‘Œ โˆˆ ๐‘† )
6 subccocl.z โŠข ( ๐œ‘ โ†’ ๐‘ โˆˆ ๐‘† )
7 subccocl.f โŠข ( ๐œ‘ โ†’ ๐น โˆˆ ( ๐‘‹ ๐ฝ ๐‘Œ ) )
8 subccocl.g โŠข ( ๐œ‘ โ†’ ๐บ โˆˆ ( ๐‘Œ ๐ฝ ๐‘ ) )
9 eqid โŠข ( Homf โ€˜ ๐ถ ) = ( Homf โ€˜ ๐ถ )
10 eqid โŠข ( Id โ€˜ ๐ถ ) = ( Id โ€˜ ๐ถ )
11 subcrcl โŠข ( ๐ฝ โˆˆ ( Subcat โ€˜ ๐ถ ) โ†’ ๐ถ โˆˆ Cat )
12 1 11 syl โŠข ( ๐œ‘ โ†’ ๐ถ โˆˆ Cat )
13 9 10 4 12 2 issubc2 โŠข ( ๐œ‘ โ†’ ( ๐ฝ โˆˆ ( Subcat โ€˜ ๐ถ ) โ†” ( ๐ฝ โŠ†cat ( Homf โ€˜ ๐ถ ) โˆง โˆ€ ๐‘ฅ โˆˆ ๐‘† ( ( ( Id โ€˜ ๐ถ ) โ€˜ ๐‘ฅ ) โˆˆ ( ๐‘ฅ ๐ฝ ๐‘ฅ ) โˆง โˆ€ ๐‘ฆ โˆˆ ๐‘† โˆ€ ๐‘ง โˆˆ ๐‘† โˆ€ ๐‘“ โˆˆ ( ๐‘ฅ ๐ฝ ๐‘ฆ ) โˆ€ ๐‘” โˆˆ ( ๐‘ฆ ๐ฝ ๐‘ง ) ( ๐‘” ( โŸจ ๐‘ฅ , ๐‘ฆ โŸฉ ยท ๐‘ง ) ๐‘“ ) โˆˆ ( ๐‘ฅ ๐ฝ ๐‘ง ) ) ) ) )
14 1 13 mpbid โŠข ( ๐œ‘ โ†’ ( ๐ฝ โŠ†cat ( Homf โ€˜ ๐ถ ) โˆง โˆ€ ๐‘ฅ โˆˆ ๐‘† ( ( ( Id โ€˜ ๐ถ ) โ€˜ ๐‘ฅ ) โˆˆ ( ๐‘ฅ ๐ฝ ๐‘ฅ ) โˆง โˆ€ ๐‘ฆ โˆˆ ๐‘† โˆ€ ๐‘ง โˆˆ ๐‘† โˆ€ ๐‘“ โˆˆ ( ๐‘ฅ ๐ฝ ๐‘ฆ ) โˆ€ ๐‘” โˆˆ ( ๐‘ฆ ๐ฝ ๐‘ง ) ( ๐‘” ( โŸจ ๐‘ฅ , ๐‘ฆ โŸฉ ยท ๐‘ง ) ๐‘“ ) โˆˆ ( ๐‘ฅ ๐ฝ ๐‘ง ) ) ) )
15 14 simprd โŠข ( ๐œ‘ โ†’ โˆ€ ๐‘ฅ โˆˆ ๐‘† ( ( ( Id โ€˜ ๐ถ ) โ€˜ ๐‘ฅ ) โˆˆ ( ๐‘ฅ ๐ฝ ๐‘ฅ ) โˆง โˆ€ ๐‘ฆ โˆˆ ๐‘† โˆ€ ๐‘ง โˆˆ ๐‘† โˆ€ ๐‘“ โˆˆ ( ๐‘ฅ ๐ฝ ๐‘ฆ ) โˆ€ ๐‘” โˆˆ ( ๐‘ฆ ๐ฝ ๐‘ง ) ( ๐‘” ( โŸจ ๐‘ฅ , ๐‘ฆ โŸฉ ยท ๐‘ง ) ๐‘“ ) โˆˆ ( ๐‘ฅ ๐ฝ ๐‘ง ) ) )
16 5 adantr โŠข ( ( ๐œ‘ โˆง ๐‘ฅ = ๐‘‹ ) โ†’ ๐‘Œ โˆˆ ๐‘† )
17 6 ad2antrr โŠข ( ( ( ๐œ‘ โˆง ๐‘ฅ = ๐‘‹ ) โˆง ๐‘ฆ = ๐‘Œ ) โ†’ ๐‘ โˆˆ ๐‘† )
18 7 ad3antrrr โŠข ( ( ( ( ๐œ‘ โˆง ๐‘ฅ = ๐‘‹ ) โˆง ๐‘ฆ = ๐‘Œ ) โˆง ๐‘ง = ๐‘ ) โ†’ ๐น โˆˆ ( ๐‘‹ ๐ฝ ๐‘Œ ) )
19 simpllr โŠข ( ( ( ( ๐œ‘ โˆง ๐‘ฅ = ๐‘‹ ) โˆง ๐‘ฆ = ๐‘Œ ) โˆง ๐‘ง = ๐‘ ) โ†’ ๐‘ฅ = ๐‘‹ )
20 simplr โŠข ( ( ( ( ๐œ‘ โˆง ๐‘ฅ = ๐‘‹ ) โˆง ๐‘ฆ = ๐‘Œ ) โˆง ๐‘ง = ๐‘ ) โ†’ ๐‘ฆ = ๐‘Œ )
21 19 20 oveq12d โŠข ( ( ( ( ๐œ‘ โˆง ๐‘ฅ = ๐‘‹ ) โˆง ๐‘ฆ = ๐‘Œ ) โˆง ๐‘ง = ๐‘ ) โ†’ ( ๐‘ฅ ๐ฝ ๐‘ฆ ) = ( ๐‘‹ ๐ฝ ๐‘Œ ) )
22 18 21 eleqtrrd โŠข ( ( ( ( ๐œ‘ โˆง ๐‘ฅ = ๐‘‹ ) โˆง ๐‘ฆ = ๐‘Œ ) โˆง ๐‘ง = ๐‘ ) โ†’ ๐น โˆˆ ( ๐‘ฅ ๐ฝ ๐‘ฆ ) )
23 8 ad4antr โŠข ( ( ( ( ( ๐œ‘ โˆง ๐‘ฅ = ๐‘‹ ) โˆง ๐‘ฆ = ๐‘Œ ) โˆง ๐‘ง = ๐‘ ) โˆง ๐‘“ = ๐น ) โ†’ ๐บ โˆˆ ( ๐‘Œ ๐ฝ ๐‘ ) )
24 simpllr โŠข ( ( ( ( ( ๐œ‘ โˆง ๐‘ฅ = ๐‘‹ ) โˆง ๐‘ฆ = ๐‘Œ ) โˆง ๐‘ง = ๐‘ ) โˆง ๐‘“ = ๐น ) โ†’ ๐‘ฆ = ๐‘Œ )
25 simplr โŠข ( ( ( ( ( ๐œ‘ โˆง ๐‘ฅ = ๐‘‹ ) โˆง ๐‘ฆ = ๐‘Œ ) โˆง ๐‘ง = ๐‘ ) โˆง ๐‘“ = ๐น ) โ†’ ๐‘ง = ๐‘ )
26 24 25 oveq12d โŠข ( ( ( ( ( ๐œ‘ โˆง ๐‘ฅ = ๐‘‹ ) โˆง ๐‘ฆ = ๐‘Œ ) โˆง ๐‘ง = ๐‘ ) โˆง ๐‘“ = ๐น ) โ†’ ( ๐‘ฆ ๐ฝ ๐‘ง ) = ( ๐‘Œ ๐ฝ ๐‘ ) )
27 23 26 eleqtrrd โŠข ( ( ( ( ( ๐œ‘ โˆง ๐‘ฅ = ๐‘‹ ) โˆง ๐‘ฆ = ๐‘Œ ) โˆง ๐‘ง = ๐‘ ) โˆง ๐‘“ = ๐น ) โ†’ ๐บ โˆˆ ( ๐‘ฆ ๐ฝ ๐‘ง ) )
28 simp-5r โŠข ( ( ( ( ( ( ๐œ‘ โˆง ๐‘ฅ = ๐‘‹ ) โˆง ๐‘ฆ = ๐‘Œ ) โˆง ๐‘ง = ๐‘ ) โˆง ๐‘“ = ๐น ) โˆง ๐‘” = ๐บ ) โ†’ ๐‘ฅ = ๐‘‹ )
29 simp-4r โŠข ( ( ( ( ( ( ๐œ‘ โˆง ๐‘ฅ = ๐‘‹ ) โˆง ๐‘ฆ = ๐‘Œ ) โˆง ๐‘ง = ๐‘ ) โˆง ๐‘“ = ๐น ) โˆง ๐‘” = ๐บ ) โ†’ ๐‘ฆ = ๐‘Œ )
30 28 29 opeq12d โŠข ( ( ( ( ( ( ๐œ‘ โˆง ๐‘ฅ = ๐‘‹ ) โˆง ๐‘ฆ = ๐‘Œ ) โˆง ๐‘ง = ๐‘ ) โˆง ๐‘“ = ๐น ) โˆง ๐‘” = ๐บ ) โ†’ โŸจ ๐‘ฅ , ๐‘ฆ โŸฉ = โŸจ ๐‘‹ , ๐‘Œ โŸฉ )
31 simpllr โŠข ( ( ( ( ( ( ๐œ‘ โˆง ๐‘ฅ = ๐‘‹ ) โˆง ๐‘ฆ = ๐‘Œ ) โˆง ๐‘ง = ๐‘ ) โˆง ๐‘“ = ๐น ) โˆง ๐‘” = ๐บ ) โ†’ ๐‘ง = ๐‘ )
32 30 31 oveq12d โŠข ( ( ( ( ( ( ๐œ‘ โˆง ๐‘ฅ = ๐‘‹ ) โˆง ๐‘ฆ = ๐‘Œ ) โˆง ๐‘ง = ๐‘ ) โˆง ๐‘“ = ๐น ) โˆง ๐‘” = ๐บ ) โ†’ ( โŸจ ๐‘ฅ , ๐‘ฆ โŸฉ ยท ๐‘ง ) = ( โŸจ ๐‘‹ , ๐‘Œ โŸฉ ยท ๐‘ ) )
33 simpr โŠข ( ( ( ( ( ( ๐œ‘ โˆง ๐‘ฅ = ๐‘‹ ) โˆง ๐‘ฆ = ๐‘Œ ) โˆง ๐‘ง = ๐‘ ) โˆง ๐‘“ = ๐น ) โˆง ๐‘” = ๐บ ) โ†’ ๐‘” = ๐บ )
34 simplr โŠข ( ( ( ( ( ( ๐œ‘ โˆง ๐‘ฅ = ๐‘‹ ) โˆง ๐‘ฆ = ๐‘Œ ) โˆง ๐‘ง = ๐‘ ) โˆง ๐‘“ = ๐น ) โˆง ๐‘” = ๐บ ) โ†’ ๐‘“ = ๐น )
35 32 33 34 oveq123d โŠข ( ( ( ( ( ( ๐œ‘ โˆง ๐‘ฅ = ๐‘‹ ) โˆง ๐‘ฆ = ๐‘Œ ) โˆง ๐‘ง = ๐‘ ) โˆง ๐‘“ = ๐น ) โˆง ๐‘” = ๐บ ) โ†’ ( ๐‘” ( โŸจ ๐‘ฅ , ๐‘ฆ โŸฉ ยท ๐‘ง ) ๐‘“ ) = ( ๐บ ( โŸจ ๐‘‹ , ๐‘Œ โŸฉ ยท ๐‘ ) ๐น ) )
36 28 31 oveq12d โŠข ( ( ( ( ( ( ๐œ‘ โˆง ๐‘ฅ = ๐‘‹ ) โˆง ๐‘ฆ = ๐‘Œ ) โˆง ๐‘ง = ๐‘ ) โˆง ๐‘“ = ๐น ) โˆง ๐‘” = ๐บ ) โ†’ ( ๐‘ฅ ๐ฝ ๐‘ง ) = ( ๐‘‹ ๐ฝ ๐‘ ) )
37 35 36 eleq12d โŠข ( ( ( ( ( ( ๐œ‘ โˆง ๐‘ฅ = ๐‘‹ ) โˆง ๐‘ฆ = ๐‘Œ ) โˆง ๐‘ง = ๐‘ ) โˆง ๐‘“ = ๐น ) โˆง ๐‘” = ๐บ ) โ†’ ( ( ๐‘” ( โŸจ ๐‘ฅ , ๐‘ฆ โŸฉ ยท ๐‘ง ) ๐‘“ ) โˆˆ ( ๐‘ฅ ๐ฝ ๐‘ง ) โ†” ( ๐บ ( โŸจ ๐‘‹ , ๐‘Œ โŸฉ ยท ๐‘ ) ๐น ) โˆˆ ( ๐‘‹ ๐ฝ ๐‘ ) ) )
38 27 37 rspcdv โŠข ( ( ( ( ( ๐œ‘ โˆง ๐‘ฅ = ๐‘‹ ) โˆง ๐‘ฆ = ๐‘Œ ) โˆง ๐‘ง = ๐‘ ) โˆง ๐‘“ = ๐น ) โ†’ ( โˆ€ ๐‘” โˆˆ ( ๐‘ฆ ๐ฝ ๐‘ง ) ( ๐‘” ( โŸจ ๐‘ฅ , ๐‘ฆ โŸฉ ยท ๐‘ง ) ๐‘“ ) โˆˆ ( ๐‘ฅ ๐ฝ ๐‘ง ) โ†’ ( ๐บ ( โŸจ ๐‘‹ , ๐‘Œ โŸฉ ยท ๐‘ ) ๐น ) โˆˆ ( ๐‘‹ ๐ฝ ๐‘ ) ) )
39 22 38 rspcimdv โŠข ( ( ( ( ๐œ‘ โˆง ๐‘ฅ = ๐‘‹ ) โˆง ๐‘ฆ = ๐‘Œ ) โˆง ๐‘ง = ๐‘ ) โ†’ ( โˆ€ ๐‘“ โˆˆ ( ๐‘ฅ ๐ฝ ๐‘ฆ ) โˆ€ ๐‘” โˆˆ ( ๐‘ฆ ๐ฝ ๐‘ง ) ( ๐‘” ( โŸจ ๐‘ฅ , ๐‘ฆ โŸฉ ยท ๐‘ง ) ๐‘“ ) โˆˆ ( ๐‘ฅ ๐ฝ ๐‘ง ) โ†’ ( ๐บ ( โŸจ ๐‘‹ , ๐‘Œ โŸฉ ยท ๐‘ ) ๐น ) โˆˆ ( ๐‘‹ ๐ฝ ๐‘ ) ) )
40 17 39 rspcimdv โŠข ( ( ( ๐œ‘ โˆง ๐‘ฅ = ๐‘‹ ) โˆง ๐‘ฆ = ๐‘Œ ) โ†’ ( โˆ€ ๐‘ง โˆˆ ๐‘† โˆ€ ๐‘“ โˆˆ ( ๐‘ฅ ๐ฝ ๐‘ฆ ) โˆ€ ๐‘” โˆˆ ( ๐‘ฆ ๐ฝ ๐‘ง ) ( ๐‘” ( โŸจ ๐‘ฅ , ๐‘ฆ โŸฉ ยท ๐‘ง ) ๐‘“ ) โˆˆ ( ๐‘ฅ ๐ฝ ๐‘ง ) โ†’ ( ๐บ ( โŸจ ๐‘‹ , ๐‘Œ โŸฉ ยท ๐‘ ) ๐น ) โˆˆ ( ๐‘‹ ๐ฝ ๐‘ ) ) )
41 16 40 rspcimdv โŠข ( ( ๐œ‘ โˆง ๐‘ฅ = ๐‘‹ ) โ†’ ( โˆ€ ๐‘ฆ โˆˆ ๐‘† โˆ€ ๐‘ง โˆˆ ๐‘† โˆ€ ๐‘“ โˆˆ ( ๐‘ฅ ๐ฝ ๐‘ฆ ) โˆ€ ๐‘” โˆˆ ( ๐‘ฆ ๐ฝ ๐‘ง ) ( ๐‘” ( โŸจ ๐‘ฅ , ๐‘ฆ โŸฉ ยท ๐‘ง ) ๐‘“ ) โˆˆ ( ๐‘ฅ ๐ฝ ๐‘ง ) โ†’ ( ๐บ ( โŸจ ๐‘‹ , ๐‘Œ โŸฉ ยท ๐‘ ) ๐น ) โˆˆ ( ๐‘‹ ๐ฝ ๐‘ ) ) )
42 41 adantld โŠข ( ( ๐œ‘ โˆง ๐‘ฅ = ๐‘‹ ) โ†’ ( ( ( ( Id โ€˜ ๐ถ ) โ€˜ ๐‘ฅ ) โˆˆ ( ๐‘ฅ ๐ฝ ๐‘ฅ ) โˆง โˆ€ ๐‘ฆ โˆˆ ๐‘† โˆ€ ๐‘ง โˆˆ ๐‘† โˆ€ ๐‘“ โˆˆ ( ๐‘ฅ ๐ฝ ๐‘ฆ ) โˆ€ ๐‘” โˆˆ ( ๐‘ฆ ๐ฝ ๐‘ง ) ( ๐‘” ( โŸจ ๐‘ฅ , ๐‘ฆ โŸฉ ยท ๐‘ง ) ๐‘“ ) โˆˆ ( ๐‘ฅ ๐ฝ ๐‘ง ) ) โ†’ ( ๐บ ( โŸจ ๐‘‹ , ๐‘Œ โŸฉ ยท ๐‘ ) ๐น ) โˆˆ ( ๐‘‹ ๐ฝ ๐‘ ) ) )
43 3 42 rspcimdv โŠข ( ๐œ‘ โ†’ ( โˆ€ ๐‘ฅ โˆˆ ๐‘† ( ( ( Id โ€˜ ๐ถ ) โ€˜ ๐‘ฅ ) โˆˆ ( ๐‘ฅ ๐ฝ ๐‘ฅ ) โˆง โˆ€ ๐‘ฆ โˆˆ ๐‘† โˆ€ ๐‘ง โˆˆ ๐‘† โˆ€ ๐‘“ โˆˆ ( ๐‘ฅ ๐ฝ ๐‘ฆ ) โˆ€ ๐‘” โˆˆ ( ๐‘ฆ ๐ฝ ๐‘ง ) ( ๐‘” ( โŸจ ๐‘ฅ , ๐‘ฆ โŸฉ ยท ๐‘ง ) ๐‘“ ) โˆˆ ( ๐‘ฅ ๐ฝ ๐‘ง ) ) โ†’ ( ๐บ ( โŸจ ๐‘‹ , ๐‘Œ โŸฉ ยท ๐‘ ) ๐น ) โˆˆ ( ๐‘‹ ๐ฝ ๐‘ ) ) )
44 15 43 mpd โŠข ( ๐œ‘ โ†’ ( ๐บ ( โŸจ ๐‘‹ , ๐‘Œ โŸฉ ยท ๐‘ ) ๐น ) โˆˆ ( ๐‘‹ ๐ฝ ๐‘ ) )