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