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 |
โข ( ๐ โ ( ๐บ ( โจ ๐ , ๐ โฉ ยท ๐ ) ๐น ) โ ( ๐ ๐ฝ ๐ ) ) |