Metamath Proof Explorer


Theorem fullresc

Description: The category formed by structure restriction is the same as the category restriction. (Contributed by Mario Carneiro, 5-Jan-2017)

Ref Expression
Hypotheses fullsubc.b B = Base C
fullsubc.h H = Hom 𝑓 C
fullsubc.c φ C Cat
fullsubc.s φ S B
fullsubc.d D = C 𝑠 S
fullsubc.e E = C cat H S × S
Assertion fullresc φ Hom 𝑓 D = Hom 𝑓 E comp 𝑓 D = comp 𝑓 E

Proof

Step Hyp Ref Expression
1 fullsubc.b B = Base C
2 fullsubc.h H = Hom 𝑓 C
3 fullsubc.c φ C Cat
4 fullsubc.s φ S B
5 fullsubc.d D = C 𝑠 S
6 fullsubc.e E = C cat H S × S
7 eqid Hom C = Hom C
8 4 adantr φ x S y S S B
9 simprl φ x S y S x S
10 8 9 sseldd φ x S y S x B
11 simprr φ x S y S y S
12 8 11 sseldd φ x S y S y B
13 2 1 7 10 12 homfval φ x S y S x H y = x Hom C y
14 9 11 ovresd φ x S y S x H S × S y = x H y
15 2 1 homffn H Fn B × B
16 xpss12 S B S B S × S B × B
17 4 4 16 syl2anc φ S × S B × B
18 fnssres H Fn B × B S × S B × B H S × S Fn S × S
19 15 17 18 sylancr φ H S × S Fn S × S
20 6 1 3 19 4 reschom φ H S × S = Hom E
21 20 oveqdr φ x S y S x H S × S y = x Hom E y
22 14 21 eqtr3d φ x S y S x H y = x Hom E y
23 5 1 ressbas2 S B S = Base D
24 4 23 syl φ S = Base D
25 fvex Base D V
26 24 25 eqeltrdi φ S V
27 5 7 resshom S V Hom C = Hom D
28 26 27 syl φ Hom C = Hom D
29 28 oveqdr φ x S y S x Hom C y = x Hom D y
30 13 22 29 3eqtr3rd φ x S y S x Hom D y = x Hom E y
31 30 ralrimivva φ x S y S x Hom D y = x Hom E y
32 eqid Hom D = Hom D
33 eqid Hom E = Hom E
34 6 1 3 19 4 rescbas φ S = Base E
35 32 33 24 34 homfeq φ Hom 𝑓 D = Hom 𝑓 E x S y S x Hom D y = x Hom E y
36 31 35 mpbird φ Hom 𝑓 D = Hom 𝑓 E
37 eqid comp C = comp C
38 5 37 ressco S V comp C = comp D
39 26 38 syl φ comp C = comp D
40 6 1 3 19 4 37 rescco φ comp C = comp E
41 39 40 eqtr3d φ comp D = comp E
42 41 36 comfeqd φ comp 𝑓 D = comp 𝑓 E
43 36 42 jca φ Hom 𝑓 D = Hom 𝑓 E comp 𝑓 D = comp 𝑓 E