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 ⊢ 𝐵 = ( Base ‘ 𝐶 )
fullsubc.h ⊢ 𝐻 = ( Homf ‘ 𝐶 )
fullsubc.c ⊢ ( 𝜑 → 𝐶 ∈ Cat )
fullsubc.s ⊢ ( 𝜑 → 𝑆 ⊆ 𝐵 )
fullsubc.d ⊢ 𝐷 = ( 𝐶 ↾s 𝑆 )
fullsubc.e ⊢ 𝐸 = ( 𝐶 ↾cat ( 𝐻 ↾ ( 𝑆 × 𝑆 ) ) )
Assertion fullresc ( 𝜑 → ( ( Homf ‘ 𝐷 ) = ( Homf ‘ 𝐸 ) ∧ ( compf ‘ 𝐷 ) = ( compf ‘ 𝐸 ) ) )

Proof

Step Hyp Ref Expression
1 fullsubc.b ⊢ 𝐵 = ( Base ‘ 𝐶 )
2 fullsubc.h ⊢ 𝐻 = ( Homf ‘ 𝐶 )
3 fullsubc.c ⊢ ( 𝜑 → 𝐶 ∈ Cat )
4 fullsubc.s ⊢ ( 𝜑 → 𝑆 ⊆ 𝐵 )
5 fullsubc.d ⊢ 𝐷 = ( 𝐶 ↾s 𝑆 )
6 fullsubc.e ⊢ 𝐸 = ( 𝐶 ↾cat ( 𝐻 ↾ ( 𝑆 × 𝑆 ) ) )
7 eqid ⊢ ( Hom ‘ 𝐶 ) = ( Hom ‘ 𝐶 )
8 4 adantr ⊢ ( ( 𝜑 ∧ ( 𝑥 ∈ 𝑆 ∧ 𝑦 ∈ 𝑆 ) ) → 𝑆 ⊆ 𝐵 )
9 simprl ⊢ ( ( 𝜑 ∧ ( 𝑥 ∈ 𝑆 ∧ 𝑦 ∈ 𝑆 ) ) → 𝑥 ∈ 𝑆 )
10 8 9 sseldd ⊢ ( ( 𝜑 ∧ ( 𝑥 ∈ 𝑆 ∧ 𝑦 ∈ 𝑆 ) ) → 𝑥 ∈ 𝐵 )
11 simprr ⊢ ( ( 𝜑 ∧ ( 𝑥 ∈ 𝑆 ∧ 𝑦 ∈ 𝑆 ) ) → 𝑦 ∈ 𝑆 )
12 8 11 sseldd ⊢ ( ( 𝜑 ∧ ( 𝑥 ∈ 𝑆 ∧ 𝑦 ∈ 𝑆 ) ) → 𝑦 ∈ 𝐵 )
13 2 1 7 10 12 homfval ⊢ ( ( 𝜑 ∧ ( 𝑥 ∈ 𝑆 ∧ 𝑦 ∈ 𝑆 ) ) → ( 𝑥 𝐻 𝑦 ) = ( 𝑥 ( Hom ‘ 𝐶 ) 𝑦 ) )
14 9 11 ovresd ⊢ ( ( 𝜑 ∧ ( 𝑥 ∈ 𝑆 ∧ 𝑦 ∈ 𝑆 ) ) → ( 𝑥 ( 𝐻 ↾ ( 𝑆 × 𝑆 ) ) 𝑦 ) = ( 𝑥 𝐻 𝑦 ) )
15 2 1 homffn ⊢ 𝐻 Fn ( 𝐵 × 𝐵 )
16 xpss12 ⊢ ( ( 𝑆 ⊆ 𝐵 ∧ 𝑆 ⊆ 𝐵 ) → ( 𝑆 × 𝑆 ) ⊆ ( 𝐵 × 𝐵 ) )
17 4 4 16 syl2anc ⊢ ( 𝜑 → ( 𝑆 × 𝑆 ) ⊆ ( 𝐵 × 𝐵 ) )
18 fnssres ⊢ ( ( 𝐻 Fn ( 𝐵 × 𝐵 ) ∧ ( 𝑆 × 𝑆 ) ⊆ ( 𝐵 × 𝐵 ) ) → ( 𝐻 ↾ ( 𝑆 × 𝑆 ) ) Fn ( 𝑆 × 𝑆 ) )
19 15 17 18 sylancr ⊢ ( 𝜑 → ( 𝐻 ↾ ( 𝑆 × 𝑆 ) ) Fn ( 𝑆 × 𝑆 ) )
20 6 1 3 19 4 reschom ⊢ ( 𝜑 → ( 𝐻 ↾ ( 𝑆 × 𝑆 ) ) = ( Hom ‘ 𝐸 ) )
21 20 oveqdr ⊢ ( ( 𝜑 ∧ ( 𝑥 ∈ 𝑆 ∧ 𝑦 ∈ 𝑆 ) ) → ( 𝑥 ( 𝐻 ↾ ( 𝑆 × 𝑆 ) ) 𝑦 ) = ( 𝑥 ( Hom ‘ 𝐸 ) 𝑦 ) )
22 14 21 eqtr3d ⊢ ( ( 𝜑 ∧ ( 𝑥 ∈ 𝑆 ∧ 𝑦 ∈ 𝑆 ) ) → ( 𝑥 𝐻 𝑦 ) = ( 𝑥 ( Hom ‘ 𝐸 ) 𝑦 ) )
23 5 1 ressbas2 ⊢ ( 𝑆 ⊆ 𝐵 → 𝑆 = ( Base ‘ 𝐷 ) )
24 4 23 syl ⊢ ( 𝜑 → 𝑆 = ( Base ‘ 𝐷 ) )
25 fvex ⊢ ( Base ‘ 𝐷 ) ∈ V
26 24 25 eqeltrdi ⊢ ( 𝜑 → 𝑆 ∈ V )
27 5 7 resshom ⊢ ( 𝑆 ∈ V → ( Hom ‘ 𝐶 ) = ( Hom ‘ 𝐷 ) )
28 26 27 syl ⊢ ( 𝜑 → ( Hom ‘ 𝐶 ) = ( Hom ‘ 𝐷 ) )
29 28 oveqdr ⊢ ( ( 𝜑 ∧ ( 𝑥 ∈ 𝑆 ∧ 𝑦 ∈ 𝑆 ) ) → ( 𝑥 ( Hom ‘ 𝐶 ) 𝑦 ) = ( 𝑥 ( Hom ‘ 𝐷 ) 𝑦 ) )
30 13 22 29 3eqtr3rd ⊢ ( ( 𝜑 ∧ ( 𝑥 ∈ 𝑆 ∧ 𝑦 ∈ 𝑆 ) ) → ( 𝑥 ( Hom ‘ 𝐷 ) 𝑦 ) = ( 𝑥 ( Hom ‘ 𝐸 ) 𝑦 ) )
31 30 ralrimivva ⊢ ( 𝜑 → ∀ 𝑥 ∈ 𝑆 ∀ 𝑦 ∈ 𝑆 ( 𝑥 ( Hom ‘ 𝐷 ) 𝑦 ) = ( 𝑥 ( Hom ‘ 𝐸 ) 𝑦 ) )
32 eqid ⊢ ( Hom ‘ 𝐷 ) = ( Hom ‘ 𝐷 )
33 eqid ⊢ ( Hom ‘ 𝐸 ) = ( Hom ‘ 𝐸 )
34 6 1 3 19 4 rescbas ⊢ ( 𝜑 → 𝑆 = ( Base ‘ 𝐸 ) )
35 32 33 24 34 homfeq ⊢ ( 𝜑 → ( ( Homf ‘ 𝐷 ) = ( Homf ‘ 𝐸 ) ↔ ∀ 𝑥 ∈ 𝑆 ∀ 𝑦 ∈ 𝑆 ( 𝑥 ( Hom ‘ 𝐷 ) 𝑦 ) = ( 𝑥 ( Hom ‘ 𝐸 ) 𝑦 ) ) )
36 31 35 mpbird ⊢ ( 𝜑 → ( Homf ‘ 𝐷 ) = ( Homf ‘ 𝐸 ) )
37 eqid ⊢ ( comp ‘ 𝐶 ) = ( comp ‘ 𝐶 )
38 5 37 ressco ⊢ ( 𝑆 ∈ V → ( comp ‘ 𝐶 ) = ( comp ‘ 𝐷 ) )
39 26 38 syl ⊢ ( 𝜑 → ( comp ‘ 𝐶 ) = ( comp ‘ 𝐷 ) )
40 6 1 3 19 4 37 rescco ⊢ ( 𝜑 → ( comp ‘ 𝐶 ) = ( comp ‘ 𝐸 ) )
41 39 40 eqtr3d ⊢ ( 𝜑 → ( comp ‘ 𝐷 ) = ( comp ‘ 𝐸 ) )
42 41 36 comfeqd ⊢ ( 𝜑 → ( compf ‘ 𝐷 ) = ( compf ‘ 𝐸 ) )
43 36 42 jca ⊢ ( 𝜑 → ( ( Homf ‘ 𝐷 ) = ( Homf ‘ 𝐸 ) ∧ ( compf ‘ 𝐷 ) = ( compf ‘ 𝐸 ) ) )