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 ‘ 𝐶 ) )