Metamath Proof Explorer


Theorem fullsubc

Description: The full subcategory generated by a subset of objects is the category with these objects and the same morphisms as the original. The result is always a subcategory (and it is full, meaning that all morphisms of the original category between objects in the subcategory is also in the subcategory), see definition 4.1(2) of Adamek p. 48. (Contributed by Mario Carneiro, 4-Jan-2017)

Ref Expression
Hypotheses fullsubc.b 𝐵 = ( Base ‘ 𝐶 )
fullsubc.h 𝐻 = ( Homf𝐶 )
fullsubc.c ( 𝜑𝐶 ∈ Cat )
fullsubc.s ( 𝜑𝑆𝐵 )
Assertion fullsubc ( 𝜑 → ( 𝐻 ↾ ( 𝑆 × 𝑆 ) ) ∈ ( Subcat ‘ 𝐶 ) )

Proof

Step Hyp Ref Expression
1 fullsubc.b 𝐵 = ( Base ‘ 𝐶 )
2 fullsubc.h 𝐻 = ( Homf𝐶 )
3 fullsubc.c ( 𝜑𝐶 ∈ Cat )
4 fullsubc.s ( 𝜑𝑆𝐵 )
5 2 1 homffn 𝐻 Fn ( 𝐵 × 𝐵 )
6 1 fvexi 𝐵 ∈ V
7 sscres ( ( 𝐻 Fn ( 𝐵 × 𝐵 ) ∧ 𝐵 ∈ V ) → ( 𝐻 ↾ ( 𝑆 × 𝑆 ) ) ⊆cat 𝐻 )
8 5 6 7 mp2an ( 𝐻 ↾ ( 𝑆 × 𝑆 ) ) ⊆cat 𝐻
9 8 a1i ( 𝜑 → ( 𝐻 ↾ ( 𝑆 × 𝑆 ) ) ⊆cat 𝐻 )
10 eqid ( Hom ‘ 𝐶 ) = ( Hom ‘ 𝐶 )
11 eqid ( Id ‘ 𝐶 ) = ( Id ‘ 𝐶 )
12 3 adantr ( ( 𝜑𝑥𝑆 ) → 𝐶 ∈ Cat )
13 4 sselda ( ( 𝜑𝑥𝑆 ) → 𝑥𝐵 )
14 1 10 11 12 13 catidcl ( ( 𝜑𝑥𝑆 ) → ( ( Id ‘ 𝐶 ) ‘ 𝑥 ) ∈ ( 𝑥 ( Hom ‘ 𝐶 ) 𝑥 ) )
15 simpr ( ( 𝜑𝑥𝑆 ) → 𝑥𝑆 )
16 15 15 ovresd ( ( 𝜑𝑥𝑆 ) → ( 𝑥 ( 𝐻 ↾ ( 𝑆 × 𝑆 ) ) 𝑥 ) = ( 𝑥 𝐻 𝑥 ) )
17 2 1 10 13 13 homfval ( ( 𝜑𝑥𝑆 ) → ( 𝑥 𝐻 𝑥 ) = ( 𝑥 ( Hom ‘ 𝐶 ) 𝑥 ) )
18 16 17 eqtrd ( ( 𝜑𝑥𝑆 ) → ( 𝑥 ( 𝐻 ↾ ( 𝑆 × 𝑆 ) ) 𝑥 ) = ( 𝑥 ( Hom ‘ 𝐶 ) 𝑥 ) )
19 14 18 eleqtrrd ( ( 𝜑𝑥𝑆 ) → ( ( Id ‘ 𝐶 ) ‘ 𝑥 ) ∈ ( 𝑥 ( 𝐻 ↾ ( 𝑆 × 𝑆 ) ) 𝑥 ) )
20 eqid ( comp ‘ 𝐶 ) = ( comp ‘ 𝐶 )
21 12 ad3antrrr ( ( ( ( ( 𝜑𝑥𝑆 ) ∧ 𝑦𝑆 ) ∧ 𝑧𝑆 ) ∧ ( 𝑓 ∈ ( 𝑥 ( Hom ‘ 𝐶 ) 𝑦 ) ∧ 𝑔 ∈ ( 𝑦 ( Hom ‘ 𝐶 ) 𝑧 ) ) ) → 𝐶 ∈ Cat )
22 13 ad3antrrr ( ( ( ( ( 𝜑𝑥𝑆 ) ∧ 𝑦𝑆 ) ∧ 𝑧𝑆 ) ∧ ( 𝑓 ∈ ( 𝑥 ( Hom ‘ 𝐶 ) 𝑦 ) ∧ 𝑔 ∈ ( 𝑦 ( Hom ‘ 𝐶 ) 𝑧 ) ) ) → 𝑥𝐵 )
23 4 adantr ( ( 𝜑𝑥𝑆 ) → 𝑆𝐵 )
24 23 sselda ( ( ( 𝜑𝑥𝑆 ) ∧ 𝑦𝑆 ) → 𝑦𝐵 )
25 24 adantr ( ( ( ( 𝜑𝑥𝑆 ) ∧ 𝑦𝑆 ) ∧ 𝑧𝑆 ) → 𝑦𝐵 )
26 25 adantr ( ( ( ( ( 𝜑𝑥𝑆 ) ∧ 𝑦𝑆 ) ∧ 𝑧𝑆 ) ∧ ( 𝑓 ∈ ( 𝑥 ( Hom ‘ 𝐶 ) 𝑦 ) ∧ 𝑔 ∈ ( 𝑦 ( Hom ‘ 𝐶 ) 𝑧 ) ) ) → 𝑦𝐵 )
27 23 adantr ( ( ( 𝜑𝑥𝑆 ) ∧ 𝑦𝑆 ) → 𝑆𝐵 )
28 27 sselda ( ( ( ( 𝜑𝑥𝑆 ) ∧ 𝑦𝑆 ) ∧ 𝑧𝑆 ) → 𝑧𝐵 )
29 28 adantr ( ( ( ( ( 𝜑𝑥𝑆 ) ∧ 𝑦𝑆 ) ∧ 𝑧𝑆 ) ∧ ( 𝑓 ∈ ( 𝑥 ( Hom ‘ 𝐶 ) 𝑦 ) ∧ 𝑔 ∈ ( 𝑦 ( Hom ‘ 𝐶 ) 𝑧 ) ) ) → 𝑧𝐵 )
30 simprl ( ( ( ( ( 𝜑𝑥𝑆 ) ∧ 𝑦𝑆 ) ∧ 𝑧𝑆 ) ∧ ( 𝑓 ∈ ( 𝑥 ( Hom ‘ 𝐶 ) 𝑦 ) ∧ 𝑔 ∈ ( 𝑦 ( Hom ‘ 𝐶 ) 𝑧 ) ) ) → 𝑓 ∈ ( 𝑥 ( Hom ‘ 𝐶 ) 𝑦 ) )
31 simprr ( ( ( ( ( 𝜑𝑥𝑆 ) ∧ 𝑦𝑆 ) ∧ 𝑧𝑆 ) ∧ ( 𝑓 ∈ ( 𝑥 ( Hom ‘ 𝐶 ) 𝑦 ) ∧ 𝑔 ∈ ( 𝑦 ( Hom ‘ 𝐶 ) 𝑧 ) ) ) → 𝑔 ∈ ( 𝑦 ( Hom ‘ 𝐶 ) 𝑧 ) )
32 1 10 20 21 22 26 29 30 31 catcocl ( ( ( ( ( 𝜑𝑥𝑆 ) ∧ 𝑦𝑆 ) ∧ 𝑧𝑆 ) ∧ ( 𝑓 ∈ ( 𝑥 ( Hom ‘ 𝐶 ) 𝑦 ) ∧ 𝑔 ∈ ( 𝑦 ( Hom ‘ 𝐶 ) 𝑧 ) ) ) → ( 𝑔 ( ⟨ 𝑥 , 𝑦 ⟩ ( comp ‘ 𝐶 ) 𝑧 ) 𝑓 ) ∈ ( 𝑥 ( Hom ‘ 𝐶 ) 𝑧 ) )
33 15 ad3antrrr ( ( ( ( ( 𝜑𝑥𝑆 ) ∧ 𝑦𝑆 ) ∧ 𝑧𝑆 ) ∧ ( 𝑓 ∈ ( 𝑥 ( Hom ‘ 𝐶 ) 𝑦 ) ∧ 𝑔 ∈ ( 𝑦 ( Hom ‘ 𝐶 ) 𝑧 ) ) ) → 𝑥𝑆 )
34 simplr ( ( ( ( ( 𝜑𝑥𝑆 ) ∧ 𝑦𝑆 ) ∧ 𝑧𝑆 ) ∧ ( 𝑓 ∈ ( 𝑥 ( Hom ‘ 𝐶 ) 𝑦 ) ∧ 𝑔 ∈ ( 𝑦 ( Hom ‘ 𝐶 ) 𝑧 ) ) ) → 𝑧𝑆 )
35 33 34 ovresd ( ( ( ( ( 𝜑𝑥𝑆 ) ∧ 𝑦𝑆 ) ∧ 𝑧𝑆 ) ∧ ( 𝑓 ∈ ( 𝑥 ( Hom ‘ 𝐶 ) 𝑦 ) ∧ 𝑔 ∈ ( 𝑦 ( Hom ‘ 𝐶 ) 𝑧 ) ) ) → ( 𝑥 ( 𝐻 ↾ ( 𝑆 × 𝑆 ) ) 𝑧 ) = ( 𝑥 𝐻 𝑧 ) )
36 2 1 10 22 29 homfval ( ( ( ( ( 𝜑𝑥𝑆 ) ∧ 𝑦𝑆 ) ∧ 𝑧𝑆 ) ∧ ( 𝑓 ∈ ( 𝑥 ( Hom ‘ 𝐶 ) 𝑦 ) ∧ 𝑔 ∈ ( 𝑦 ( Hom ‘ 𝐶 ) 𝑧 ) ) ) → ( 𝑥 𝐻 𝑧 ) = ( 𝑥 ( Hom ‘ 𝐶 ) 𝑧 ) )
37 35 36 eqtrd ( ( ( ( ( 𝜑𝑥𝑆 ) ∧ 𝑦𝑆 ) ∧ 𝑧𝑆 ) ∧ ( 𝑓 ∈ ( 𝑥 ( Hom ‘ 𝐶 ) 𝑦 ) ∧ 𝑔 ∈ ( 𝑦 ( Hom ‘ 𝐶 ) 𝑧 ) ) ) → ( 𝑥 ( 𝐻 ↾ ( 𝑆 × 𝑆 ) ) 𝑧 ) = ( 𝑥 ( Hom ‘ 𝐶 ) 𝑧 ) )
38 32 37 eleqtrrd ( ( ( ( ( 𝜑𝑥𝑆 ) ∧ 𝑦𝑆 ) ∧ 𝑧𝑆 ) ∧ ( 𝑓 ∈ ( 𝑥 ( Hom ‘ 𝐶 ) 𝑦 ) ∧ 𝑔 ∈ ( 𝑦 ( Hom ‘ 𝐶 ) 𝑧 ) ) ) → ( 𝑔 ( ⟨ 𝑥 , 𝑦 ⟩ ( comp ‘ 𝐶 ) 𝑧 ) 𝑓 ) ∈ ( 𝑥 ( 𝐻 ↾ ( 𝑆 × 𝑆 ) ) 𝑧 ) )
39 38 ralrimivva ( ( ( ( 𝜑𝑥𝑆 ) ∧ 𝑦𝑆 ) ∧ 𝑧𝑆 ) → ∀ 𝑓 ∈ ( 𝑥 ( Hom ‘ 𝐶 ) 𝑦 ) ∀ 𝑔 ∈ ( 𝑦 ( Hom ‘ 𝐶 ) 𝑧 ) ( 𝑔 ( ⟨ 𝑥 , 𝑦 ⟩ ( comp ‘ 𝐶 ) 𝑧 ) 𝑓 ) ∈ ( 𝑥 ( 𝐻 ↾ ( 𝑆 × 𝑆 ) ) 𝑧 ) )
40 simplr ( ( ( 𝜑𝑥𝑆 ) ∧ 𝑦𝑆 ) → 𝑥𝑆 )
41 simpr ( ( ( 𝜑𝑥𝑆 ) ∧ 𝑦𝑆 ) → 𝑦𝑆 )
42 40 41 ovresd ( ( ( 𝜑𝑥𝑆 ) ∧ 𝑦𝑆 ) → ( 𝑥 ( 𝐻 ↾ ( 𝑆 × 𝑆 ) ) 𝑦 ) = ( 𝑥 𝐻 𝑦 ) )
43 13 adantr ( ( ( 𝜑𝑥𝑆 ) ∧ 𝑦𝑆 ) → 𝑥𝐵 )
44 2 1 10 43 24 homfval ( ( ( 𝜑𝑥𝑆 ) ∧ 𝑦𝑆 ) → ( 𝑥 𝐻 𝑦 ) = ( 𝑥 ( Hom ‘ 𝐶 ) 𝑦 ) )
45 42 44 eqtrd ( ( ( 𝜑𝑥𝑆 ) ∧ 𝑦𝑆 ) → ( 𝑥 ( 𝐻 ↾ ( 𝑆 × 𝑆 ) ) 𝑦 ) = ( 𝑥 ( Hom ‘ 𝐶 ) 𝑦 ) )
46 45 adantr ( ( ( ( 𝜑𝑥𝑆 ) ∧ 𝑦𝑆 ) ∧ 𝑧𝑆 ) → ( 𝑥 ( 𝐻 ↾ ( 𝑆 × 𝑆 ) ) 𝑦 ) = ( 𝑥 ( Hom ‘ 𝐶 ) 𝑦 ) )
47 simplr ( ( ( ( 𝜑𝑥𝑆 ) ∧ 𝑦𝑆 ) ∧ 𝑧𝑆 ) → 𝑦𝑆 )
48 simpr ( ( ( ( 𝜑𝑥𝑆 ) ∧ 𝑦𝑆 ) ∧ 𝑧𝑆 ) → 𝑧𝑆 )
49 47 48 ovresd ( ( ( ( 𝜑𝑥𝑆 ) ∧ 𝑦𝑆 ) ∧ 𝑧𝑆 ) → ( 𝑦 ( 𝐻 ↾ ( 𝑆 × 𝑆 ) ) 𝑧 ) = ( 𝑦 𝐻 𝑧 ) )
50 2 1 10 25 28 homfval ( ( ( ( 𝜑𝑥𝑆 ) ∧ 𝑦𝑆 ) ∧ 𝑧𝑆 ) → ( 𝑦 𝐻 𝑧 ) = ( 𝑦 ( Hom ‘ 𝐶 ) 𝑧 ) )
51 49 50 eqtrd ( ( ( ( 𝜑𝑥𝑆 ) ∧ 𝑦𝑆 ) ∧ 𝑧𝑆 ) → ( 𝑦 ( 𝐻 ↾ ( 𝑆 × 𝑆 ) ) 𝑧 ) = ( 𝑦 ( Hom ‘ 𝐶 ) 𝑧 ) )
52 51 raleqdv ( ( ( ( 𝜑𝑥𝑆 ) ∧ 𝑦𝑆 ) ∧ 𝑧𝑆 ) → ( ∀ 𝑔 ∈ ( 𝑦 ( 𝐻 ↾ ( 𝑆 × 𝑆 ) ) 𝑧 ) ( 𝑔 ( ⟨ 𝑥 , 𝑦 ⟩ ( comp ‘ 𝐶 ) 𝑧 ) 𝑓 ) ∈ ( 𝑥 ( 𝐻 ↾ ( 𝑆 × 𝑆 ) ) 𝑧 ) ↔ ∀ 𝑔 ∈ ( 𝑦 ( Hom ‘ 𝐶 ) 𝑧 ) ( 𝑔 ( ⟨ 𝑥 , 𝑦 ⟩ ( comp ‘ 𝐶 ) 𝑧 ) 𝑓 ) ∈ ( 𝑥 ( 𝐻 ↾ ( 𝑆 × 𝑆 ) ) 𝑧 ) ) )
53 46 52 raleqbidv ( ( ( ( 𝜑𝑥𝑆 ) ∧ 𝑦𝑆 ) ∧ 𝑧𝑆 ) → ( ∀ 𝑓 ∈ ( 𝑥 ( 𝐻 ↾ ( 𝑆 × 𝑆 ) ) 𝑦 ) ∀ 𝑔 ∈ ( 𝑦 ( 𝐻 ↾ ( 𝑆 × 𝑆 ) ) 𝑧 ) ( 𝑔 ( ⟨ 𝑥 , 𝑦 ⟩ ( comp ‘ 𝐶 ) 𝑧 ) 𝑓 ) ∈ ( 𝑥 ( 𝐻 ↾ ( 𝑆 × 𝑆 ) ) 𝑧 ) ↔ ∀ 𝑓 ∈ ( 𝑥 ( Hom ‘ 𝐶 ) 𝑦 ) ∀ 𝑔 ∈ ( 𝑦 ( Hom ‘ 𝐶 ) 𝑧 ) ( 𝑔 ( ⟨ 𝑥 , 𝑦 ⟩ ( comp ‘ 𝐶 ) 𝑧 ) 𝑓 ) ∈ ( 𝑥 ( 𝐻 ↾ ( 𝑆 × 𝑆 ) ) 𝑧 ) ) )
54 39 53 mpbird ( ( ( ( 𝜑𝑥𝑆 ) ∧ 𝑦𝑆 ) ∧ 𝑧𝑆 ) → ∀ 𝑓 ∈ ( 𝑥 ( 𝐻 ↾ ( 𝑆 × 𝑆 ) ) 𝑦 ) ∀ 𝑔 ∈ ( 𝑦 ( 𝐻 ↾ ( 𝑆 × 𝑆 ) ) 𝑧 ) ( 𝑔 ( ⟨ 𝑥 , 𝑦 ⟩ ( comp ‘ 𝐶 ) 𝑧 ) 𝑓 ) ∈ ( 𝑥 ( 𝐻 ↾ ( 𝑆 × 𝑆 ) ) 𝑧 ) )
55 54 ralrimiva ( ( ( 𝜑𝑥𝑆 ) ∧ 𝑦𝑆 ) → ∀ 𝑧𝑆𝑓 ∈ ( 𝑥 ( 𝐻 ↾ ( 𝑆 × 𝑆 ) ) 𝑦 ) ∀ 𝑔 ∈ ( 𝑦 ( 𝐻 ↾ ( 𝑆 × 𝑆 ) ) 𝑧 ) ( 𝑔 ( ⟨ 𝑥 , 𝑦 ⟩ ( comp ‘ 𝐶 ) 𝑧 ) 𝑓 ) ∈ ( 𝑥 ( 𝐻 ↾ ( 𝑆 × 𝑆 ) ) 𝑧 ) )
56 55 ralrimiva ( ( 𝜑𝑥𝑆 ) → ∀ 𝑦𝑆𝑧𝑆𝑓 ∈ ( 𝑥 ( 𝐻 ↾ ( 𝑆 × 𝑆 ) ) 𝑦 ) ∀ 𝑔 ∈ ( 𝑦 ( 𝐻 ↾ ( 𝑆 × 𝑆 ) ) 𝑧 ) ( 𝑔 ( ⟨ 𝑥 , 𝑦 ⟩ ( comp ‘ 𝐶 ) 𝑧 ) 𝑓 ) ∈ ( 𝑥 ( 𝐻 ↾ ( 𝑆 × 𝑆 ) ) 𝑧 ) )
57 19 56 jca ( ( 𝜑𝑥𝑆 ) → ( ( ( Id ‘ 𝐶 ) ‘ 𝑥 ) ∈ ( 𝑥 ( 𝐻 ↾ ( 𝑆 × 𝑆 ) ) 𝑥 ) ∧ ∀ 𝑦𝑆𝑧𝑆𝑓 ∈ ( 𝑥 ( 𝐻 ↾ ( 𝑆 × 𝑆 ) ) 𝑦 ) ∀ 𝑔 ∈ ( 𝑦 ( 𝐻 ↾ ( 𝑆 × 𝑆 ) ) 𝑧 ) ( 𝑔 ( ⟨ 𝑥 , 𝑦 ⟩ ( comp ‘ 𝐶 ) 𝑧 ) 𝑓 ) ∈ ( 𝑥 ( 𝐻 ↾ ( 𝑆 × 𝑆 ) ) 𝑧 ) ) )
58 57 ralrimiva ( 𝜑 → ∀ 𝑥𝑆 ( ( ( Id ‘ 𝐶 ) ‘ 𝑥 ) ∈ ( 𝑥 ( 𝐻 ↾ ( 𝑆 × 𝑆 ) ) 𝑥 ) ∧ ∀ 𝑦𝑆𝑧𝑆𝑓 ∈ ( 𝑥 ( 𝐻 ↾ ( 𝑆 × 𝑆 ) ) 𝑦 ) ∀ 𝑔 ∈ ( 𝑦 ( 𝐻 ↾ ( 𝑆 × 𝑆 ) ) 𝑧 ) ( 𝑔 ( ⟨ 𝑥 , 𝑦 ⟩ ( comp ‘ 𝐶 ) 𝑧 ) 𝑓 ) ∈ ( 𝑥 ( 𝐻 ↾ ( 𝑆 × 𝑆 ) ) 𝑧 ) ) )
59 xpss12 ( ( 𝑆𝐵𝑆𝐵 ) → ( 𝑆 × 𝑆 ) ⊆ ( 𝐵 × 𝐵 ) )
60 4 4 59 syl2anc ( 𝜑 → ( 𝑆 × 𝑆 ) ⊆ ( 𝐵 × 𝐵 ) )
61 fnssres ( ( 𝐻 Fn ( 𝐵 × 𝐵 ) ∧ ( 𝑆 × 𝑆 ) ⊆ ( 𝐵 × 𝐵 ) ) → ( 𝐻 ↾ ( 𝑆 × 𝑆 ) ) Fn ( 𝑆 × 𝑆 ) )
62 5 60 61 sylancr ( 𝜑 → ( 𝐻 ↾ ( 𝑆 × 𝑆 ) ) Fn ( 𝑆 × 𝑆 ) )
63 2 11 20 3 62 issubc2 ( 𝜑 → ( ( 𝐻 ↾ ( 𝑆 × 𝑆 ) ) ∈ ( Subcat ‘ 𝐶 ) ↔ ( ( 𝐻 ↾ ( 𝑆 × 𝑆 ) ) ⊆cat 𝐻 ∧ ∀ 𝑥𝑆 ( ( ( Id ‘ 𝐶 ) ‘ 𝑥 ) ∈ ( 𝑥 ( 𝐻 ↾ ( 𝑆 × 𝑆 ) ) 𝑥 ) ∧ ∀ 𝑦𝑆𝑧𝑆𝑓 ∈ ( 𝑥 ( 𝐻 ↾ ( 𝑆 × 𝑆 ) ) 𝑦 ) ∀ 𝑔 ∈ ( 𝑦 ( 𝐻 ↾ ( 𝑆 × 𝑆 ) ) 𝑧 ) ( 𝑔 ( ⟨ 𝑥 , 𝑦 ⟩ ( comp ‘ 𝐶 ) 𝑧 ) 𝑓 ) ∈ ( 𝑥 ( 𝐻 ↾ ( 𝑆 × 𝑆 ) ) 𝑧 ) ) ) ) )
64 9 58 63 mpbir2and ( 𝜑 → ( 𝐻 ↾ ( 𝑆 × 𝑆 ) ) ∈ ( Subcat ‘ 𝐶 ) )