Metamath Proof Explorer


Theorem subccatid

Description: A subcategory is a category. (Contributed by Mario Carneiro, 4-Jan-2017)

Ref Expression
Hypotheses subccat.1 D=CcatJ
subccat.j φJSubcatC
subccatid.1 φJFnS×S
subccatid.2 1˙=IdC
Assertion subccatid φDCatIdD=xS1˙x

Proof

Step Hyp Ref Expression
1 subccat.1 D=CcatJ
2 subccat.j φJSubcatC
3 subccatid.1 φJFnS×S
4 subccatid.2 1˙=IdC
5 eqid BaseC=BaseC
6 subcrcl JSubcatCCCat
7 2 6 syl φCCat
8 2 3 5 subcss1 φSBaseC
9 1 5 7 3 8 rescbas φS=BaseD
10 1 5 7 3 8 reschom φJ=HomD
11 eqid compC=compC
12 1 5 7 3 8 11 rescco φcompC=compD
13 1 ovexi DV
14 13 a1i φDV
15 biid wSxSySzSfwJxgxJyhyJzwSxSySzSfwJxgxJyhyJz
16 2 adantr φxSJSubcatC
17 3 adantr φxSJFnS×S
18 simpr φxSxS
19 16 17 18 4 subcidcl φxS1˙xxJx
20 eqid HomC=HomC
21 7 adantr φwSxSySzSfwJxgxJyhyJzCCat
22 8 adantr φwSxSySzSfwJxgxJyhyJzSBaseC
23 simpr1l φwSxSySzSfwJxgxJyhyJzwS
24 22 23 sseldd φwSxSySzSfwJxgxJyhyJzwBaseC
25 simpr1r φwSxSySzSfwJxgxJyhyJzxS
26 22 25 sseldd φwSxSySzSfwJxgxJyhyJzxBaseC
27 2 adantr φwSxSySzSfwJxgxJyhyJzJSubcatC
28 3 adantr φwSxSySzSfwJxgxJyhyJzJFnS×S
29 27 28 20 23 25 subcss2 φwSxSySzSfwJxgxJyhyJzwJxwHomCx
30 simpr31 φwSxSySzSfwJxgxJyhyJzfwJx
31 29 30 sseldd φwSxSySzSfwJxgxJyhyJzfwHomCx
32 5 20 4 21 24 11 26 31 catlid φwSxSySzSfwJxgxJyhyJz1˙xwxcompCxf=f
33 simpr2l φwSxSySzSfwJxgxJyhyJzyS
34 22 33 sseldd φwSxSySzSfwJxgxJyhyJzyBaseC
35 27 28 20 25 33 subcss2 φwSxSySzSfwJxgxJyhyJzxJyxHomCy
36 simpr32 φwSxSySzSfwJxgxJyhyJzgxJy
37 35 36 sseldd φwSxSySzSfwJxgxJyhyJzgxHomCy
38 5 20 4 21 26 11 34 37 catrid φwSxSySzSfwJxgxJyhyJzgxxcompCy1˙x=g
39 27 28 23 11 25 33 30 36 subccocl φwSxSySzSfwJxgxJyhyJzgwxcompCyfwJy
40 simpr2r φwSxSySzSfwJxgxJyhyJzzS
41 22 40 sseldd φwSxSySzSfwJxgxJyhyJzzBaseC
42 27 28 20 33 40 subcss2 φwSxSySzSfwJxgxJyhyJzyJzyHomCz
43 simpr33 φwSxSySzSfwJxgxJyhyJzhyJz
44 42 43 sseldd φwSxSySzSfwJxgxJyhyJzhyHomCz
45 5 20 11 21 24 26 34 31 37 41 44 catass φwSxSySzSfwJxgxJyhyJzhxycompCzgwxcompCzf=hwycompCzgwxcompCyf
46 9 10 12 14 15 19 32 38 39 45 iscatd2 φDCatIdD=xS1˙x