Step |
Hyp |
Ref |
Expression |
1 |
|
estrccat.c |
⊢ 𝐶 = ( ExtStrCat ‘ 𝑈 ) |
2 |
|
id |
⊢ ( 𝑈 ∈ 𝑉 → 𝑈 ∈ 𝑉 ) |
3 |
1 2
|
estrcbas |
⊢ ( 𝑈 ∈ 𝑉 → 𝑈 = ( Base ‘ 𝐶 ) ) |
4 |
|
eqidd |
⊢ ( 𝑈 ∈ 𝑉 → ( Hom ‘ 𝐶 ) = ( Hom ‘ 𝐶 ) ) |
5 |
|
eqidd |
⊢ ( 𝑈 ∈ 𝑉 → ( comp ‘ 𝐶 ) = ( comp ‘ 𝐶 ) ) |
6 |
1
|
fvexi |
⊢ 𝐶 ∈ V |
7 |
6
|
a1i |
⊢ ( 𝑈 ∈ 𝑉 → 𝐶 ∈ V ) |
8 |
|
biid |
⊢ ( ( ( 𝑤 ∈ 𝑈 ∧ 𝑥 ∈ 𝑈 ) ∧ ( 𝑦 ∈ 𝑈 ∧ 𝑧 ∈ 𝑈 ) ∧ ( 𝑓 ∈ ( 𝑤 ( Hom ‘ 𝐶 ) 𝑥 ) ∧ 𝑔 ∈ ( 𝑥 ( Hom ‘ 𝐶 ) 𝑦 ) ∧ ℎ ∈ ( 𝑦 ( Hom ‘ 𝐶 ) 𝑧 ) ) ) ↔ ( ( 𝑤 ∈ 𝑈 ∧ 𝑥 ∈ 𝑈 ) ∧ ( 𝑦 ∈ 𝑈 ∧ 𝑧 ∈ 𝑈 ) ∧ ( 𝑓 ∈ ( 𝑤 ( Hom ‘ 𝐶 ) 𝑥 ) ∧ 𝑔 ∈ ( 𝑥 ( Hom ‘ 𝐶 ) 𝑦 ) ∧ ℎ ∈ ( 𝑦 ( Hom ‘ 𝐶 ) 𝑧 ) ) ) ) |
9 |
|
f1oi |
⊢ ( I ↾ ( Base ‘ 𝑥 ) ) : ( Base ‘ 𝑥 ) –1-1-onto→ ( Base ‘ 𝑥 ) |
10 |
|
f1of |
⊢ ( ( I ↾ ( Base ‘ 𝑥 ) ) : ( Base ‘ 𝑥 ) –1-1-onto→ ( Base ‘ 𝑥 ) → ( I ↾ ( Base ‘ 𝑥 ) ) : ( Base ‘ 𝑥 ) ⟶ ( Base ‘ 𝑥 ) ) |
11 |
9 10
|
mp1i |
⊢ ( ( 𝑈 ∈ 𝑉 ∧ 𝑥 ∈ 𝑈 ) → ( I ↾ ( Base ‘ 𝑥 ) ) : ( Base ‘ 𝑥 ) ⟶ ( Base ‘ 𝑥 ) ) |
12 |
|
simpl |
⊢ ( ( 𝑈 ∈ 𝑉 ∧ 𝑥 ∈ 𝑈 ) → 𝑈 ∈ 𝑉 ) |
13 |
|
eqid |
⊢ ( Hom ‘ 𝐶 ) = ( Hom ‘ 𝐶 ) |
14 |
|
simpr |
⊢ ( ( 𝑈 ∈ 𝑉 ∧ 𝑥 ∈ 𝑈 ) → 𝑥 ∈ 𝑈 ) |
15 |
|
eqid |
⊢ ( Base ‘ 𝑥 ) = ( Base ‘ 𝑥 ) |
16 |
1 12 13 14 14 15 15
|
elestrchom |
⊢ ( ( 𝑈 ∈ 𝑉 ∧ 𝑥 ∈ 𝑈 ) → ( ( I ↾ ( Base ‘ 𝑥 ) ) ∈ ( 𝑥 ( Hom ‘ 𝐶 ) 𝑥 ) ↔ ( I ↾ ( Base ‘ 𝑥 ) ) : ( Base ‘ 𝑥 ) ⟶ ( Base ‘ 𝑥 ) ) ) |
17 |
11 16
|
mpbird |
⊢ ( ( 𝑈 ∈ 𝑉 ∧ 𝑥 ∈ 𝑈 ) → ( I ↾ ( Base ‘ 𝑥 ) ) ∈ ( 𝑥 ( Hom ‘ 𝐶 ) 𝑥 ) ) |
18 |
|
simpl |
⊢ ( ( 𝑈 ∈ 𝑉 ∧ ( ( 𝑤 ∈ 𝑈 ∧ 𝑥 ∈ 𝑈 ) ∧ ( 𝑦 ∈ 𝑈 ∧ 𝑧 ∈ 𝑈 ) ∧ ( 𝑓 ∈ ( 𝑤 ( Hom ‘ 𝐶 ) 𝑥 ) ∧ 𝑔 ∈ ( 𝑥 ( Hom ‘ 𝐶 ) 𝑦 ) ∧ ℎ ∈ ( 𝑦 ( Hom ‘ 𝐶 ) 𝑧 ) ) ) ) → 𝑈 ∈ 𝑉 ) |
19 |
|
eqid |
⊢ ( comp ‘ 𝐶 ) = ( comp ‘ 𝐶 ) |
20 |
|
simpr1l |
⊢ ( ( 𝑈 ∈ 𝑉 ∧ ( ( 𝑤 ∈ 𝑈 ∧ 𝑥 ∈ 𝑈 ) ∧ ( 𝑦 ∈ 𝑈 ∧ 𝑧 ∈ 𝑈 ) ∧ ( 𝑓 ∈ ( 𝑤 ( Hom ‘ 𝐶 ) 𝑥 ) ∧ 𝑔 ∈ ( 𝑥 ( Hom ‘ 𝐶 ) 𝑦 ) ∧ ℎ ∈ ( 𝑦 ( Hom ‘ 𝐶 ) 𝑧 ) ) ) ) → 𝑤 ∈ 𝑈 ) |
21 |
|
simpr1r |
⊢ ( ( 𝑈 ∈ 𝑉 ∧ ( ( 𝑤 ∈ 𝑈 ∧ 𝑥 ∈ 𝑈 ) ∧ ( 𝑦 ∈ 𝑈 ∧ 𝑧 ∈ 𝑈 ) ∧ ( 𝑓 ∈ ( 𝑤 ( Hom ‘ 𝐶 ) 𝑥 ) ∧ 𝑔 ∈ ( 𝑥 ( Hom ‘ 𝐶 ) 𝑦 ) ∧ ℎ ∈ ( 𝑦 ( Hom ‘ 𝐶 ) 𝑧 ) ) ) ) → 𝑥 ∈ 𝑈 ) |
22 |
|
eqid |
⊢ ( Base ‘ 𝑤 ) = ( Base ‘ 𝑤 ) |
23 |
|
simpr31 |
⊢ ( ( 𝑈 ∈ 𝑉 ∧ ( ( 𝑤 ∈ 𝑈 ∧ 𝑥 ∈ 𝑈 ) ∧ ( 𝑦 ∈ 𝑈 ∧ 𝑧 ∈ 𝑈 ) ∧ ( 𝑓 ∈ ( 𝑤 ( Hom ‘ 𝐶 ) 𝑥 ) ∧ 𝑔 ∈ ( 𝑥 ( Hom ‘ 𝐶 ) 𝑦 ) ∧ ℎ ∈ ( 𝑦 ( Hom ‘ 𝐶 ) 𝑧 ) ) ) ) → 𝑓 ∈ ( 𝑤 ( Hom ‘ 𝐶 ) 𝑥 ) ) |
24 |
1 18 13 20 21 22 15
|
elestrchom |
⊢ ( ( 𝑈 ∈ 𝑉 ∧ ( ( 𝑤 ∈ 𝑈 ∧ 𝑥 ∈ 𝑈 ) ∧ ( 𝑦 ∈ 𝑈 ∧ 𝑧 ∈ 𝑈 ) ∧ ( 𝑓 ∈ ( 𝑤 ( Hom ‘ 𝐶 ) 𝑥 ) ∧ 𝑔 ∈ ( 𝑥 ( Hom ‘ 𝐶 ) 𝑦 ) ∧ ℎ ∈ ( 𝑦 ( Hom ‘ 𝐶 ) 𝑧 ) ) ) ) → ( 𝑓 ∈ ( 𝑤 ( Hom ‘ 𝐶 ) 𝑥 ) ↔ 𝑓 : ( Base ‘ 𝑤 ) ⟶ ( Base ‘ 𝑥 ) ) ) |
25 |
23 24
|
mpbid |
⊢ ( ( 𝑈 ∈ 𝑉 ∧ ( ( 𝑤 ∈ 𝑈 ∧ 𝑥 ∈ 𝑈 ) ∧ ( 𝑦 ∈ 𝑈 ∧ 𝑧 ∈ 𝑈 ) ∧ ( 𝑓 ∈ ( 𝑤 ( Hom ‘ 𝐶 ) 𝑥 ) ∧ 𝑔 ∈ ( 𝑥 ( Hom ‘ 𝐶 ) 𝑦 ) ∧ ℎ ∈ ( 𝑦 ( Hom ‘ 𝐶 ) 𝑧 ) ) ) ) → 𝑓 : ( Base ‘ 𝑤 ) ⟶ ( Base ‘ 𝑥 ) ) |
26 |
9 10
|
mp1i |
⊢ ( ( 𝑈 ∈ 𝑉 ∧ ( ( 𝑤 ∈ 𝑈 ∧ 𝑥 ∈ 𝑈 ) ∧ ( 𝑦 ∈ 𝑈 ∧ 𝑧 ∈ 𝑈 ) ∧ ( 𝑓 ∈ ( 𝑤 ( Hom ‘ 𝐶 ) 𝑥 ) ∧ 𝑔 ∈ ( 𝑥 ( Hom ‘ 𝐶 ) 𝑦 ) ∧ ℎ ∈ ( 𝑦 ( Hom ‘ 𝐶 ) 𝑧 ) ) ) ) → ( I ↾ ( Base ‘ 𝑥 ) ) : ( Base ‘ 𝑥 ) ⟶ ( Base ‘ 𝑥 ) ) |
27 |
1 18 19 20 21 21 22 15 15 25 26
|
estrcco |
⊢ ( ( 𝑈 ∈ 𝑉 ∧ ( ( 𝑤 ∈ 𝑈 ∧ 𝑥 ∈ 𝑈 ) ∧ ( 𝑦 ∈ 𝑈 ∧ 𝑧 ∈ 𝑈 ) ∧ ( 𝑓 ∈ ( 𝑤 ( Hom ‘ 𝐶 ) 𝑥 ) ∧ 𝑔 ∈ ( 𝑥 ( Hom ‘ 𝐶 ) 𝑦 ) ∧ ℎ ∈ ( 𝑦 ( Hom ‘ 𝐶 ) 𝑧 ) ) ) ) → ( ( I ↾ ( Base ‘ 𝑥 ) ) ( 〈 𝑤 , 𝑥 〉 ( comp ‘ 𝐶 ) 𝑥 ) 𝑓 ) = ( ( I ↾ ( Base ‘ 𝑥 ) ) ∘ 𝑓 ) ) |
28 |
|
fcoi2 |
⊢ ( 𝑓 : ( Base ‘ 𝑤 ) ⟶ ( Base ‘ 𝑥 ) → ( ( I ↾ ( Base ‘ 𝑥 ) ) ∘ 𝑓 ) = 𝑓 ) |
29 |
25 28
|
syl |
⊢ ( ( 𝑈 ∈ 𝑉 ∧ ( ( 𝑤 ∈ 𝑈 ∧ 𝑥 ∈ 𝑈 ) ∧ ( 𝑦 ∈ 𝑈 ∧ 𝑧 ∈ 𝑈 ) ∧ ( 𝑓 ∈ ( 𝑤 ( Hom ‘ 𝐶 ) 𝑥 ) ∧ 𝑔 ∈ ( 𝑥 ( Hom ‘ 𝐶 ) 𝑦 ) ∧ ℎ ∈ ( 𝑦 ( Hom ‘ 𝐶 ) 𝑧 ) ) ) ) → ( ( I ↾ ( Base ‘ 𝑥 ) ) ∘ 𝑓 ) = 𝑓 ) |
30 |
27 29
|
eqtrd |
⊢ ( ( 𝑈 ∈ 𝑉 ∧ ( ( 𝑤 ∈ 𝑈 ∧ 𝑥 ∈ 𝑈 ) ∧ ( 𝑦 ∈ 𝑈 ∧ 𝑧 ∈ 𝑈 ) ∧ ( 𝑓 ∈ ( 𝑤 ( Hom ‘ 𝐶 ) 𝑥 ) ∧ 𝑔 ∈ ( 𝑥 ( Hom ‘ 𝐶 ) 𝑦 ) ∧ ℎ ∈ ( 𝑦 ( Hom ‘ 𝐶 ) 𝑧 ) ) ) ) → ( ( I ↾ ( Base ‘ 𝑥 ) ) ( 〈 𝑤 , 𝑥 〉 ( comp ‘ 𝐶 ) 𝑥 ) 𝑓 ) = 𝑓 ) |
31 |
|
simpr2l |
⊢ ( ( 𝑈 ∈ 𝑉 ∧ ( ( 𝑤 ∈ 𝑈 ∧ 𝑥 ∈ 𝑈 ) ∧ ( 𝑦 ∈ 𝑈 ∧ 𝑧 ∈ 𝑈 ) ∧ ( 𝑓 ∈ ( 𝑤 ( Hom ‘ 𝐶 ) 𝑥 ) ∧ 𝑔 ∈ ( 𝑥 ( Hom ‘ 𝐶 ) 𝑦 ) ∧ ℎ ∈ ( 𝑦 ( Hom ‘ 𝐶 ) 𝑧 ) ) ) ) → 𝑦 ∈ 𝑈 ) |
32 |
|
eqid |
⊢ ( Base ‘ 𝑦 ) = ( Base ‘ 𝑦 ) |
33 |
|
simpr32 |
⊢ ( ( 𝑈 ∈ 𝑉 ∧ ( ( 𝑤 ∈ 𝑈 ∧ 𝑥 ∈ 𝑈 ) ∧ ( 𝑦 ∈ 𝑈 ∧ 𝑧 ∈ 𝑈 ) ∧ ( 𝑓 ∈ ( 𝑤 ( Hom ‘ 𝐶 ) 𝑥 ) ∧ 𝑔 ∈ ( 𝑥 ( Hom ‘ 𝐶 ) 𝑦 ) ∧ ℎ ∈ ( 𝑦 ( Hom ‘ 𝐶 ) 𝑧 ) ) ) ) → 𝑔 ∈ ( 𝑥 ( Hom ‘ 𝐶 ) 𝑦 ) ) |
34 |
1 18 13 21 31 15 32
|
elestrchom |
⊢ ( ( 𝑈 ∈ 𝑉 ∧ ( ( 𝑤 ∈ 𝑈 ∧ 𝑥 ∈ 𝑈 ) ∧ ( 𝑦 ∈ 𝑈 ∧ 𝑧 ∈ 𝑈 ) ∧ ( 𝑓 ∈ ( 𝑤 ( Hom ‘ 𝐶 ) 𝑥 ) ∧ 𝑔 ∈ ( 𝑥 ( Hom ‘ 𝐶 ) 𝑦 ) ∧ ℎ ∈ ( 𝑦 ( Hom ‘ 𝐶 ) 𝑧 ) ) ) ) → ( 𝑔 ∈ ( 𝑥 ( Hom ‘ 𝐶 ) 𝑦 ) ↔ 𝑔 : ( Base ‘ 𝑥 ) ⟶ ( Base ‘ 𝑦 ) ) ) |
35 |
33 34
|
mpbid |
⊢ ( ( 𝑈 ∈ 𝑉 ∧ ( ( 𝑤 ∈ 𝑈 ∧ 𝑥 ∈ 𝑈 ) ∧ ( 𝑦 ∈ 𝑈 ∧ 𝑧 ∈ 𝑈 ) ∧ ( 𝑓 ∈ ( 𝑤 ( Hom ‘ 𝐶 ) 𝑥 ) ∧ 𝑔 ∈ ( 𝑥 ( Hom ‘ 𝐶 ) 𝑦 ) ∧ ℎ ∈ ( 𝑦 ( Hom ‘ 𝐶 ) 𝑧 ) ) ) ) → 𝑔 : ( Base ‘ 𝑥 ) ⟶ ( Base ‘ 𝑦 ) ) |
36 |
1 18 19 21 21 31 15 15 32 26 35
|
estrcco |
⊢ ( ( 𝑈 ∈ 𝑉 ∧ ( ( 𝑤 ∈ 𝑈 ∧ 𝑥 ∈ 𝑈 ) ∧ ( 𝑦 ∈ 𝑈 ∧ 𝑧 ∈ 𝑈 ) ∧ ( 𝑓 ∈ ( 𝑤 ( Hom ‘ 𝐶 ) 𝑥 ) ∧ 𝑔 ∈ ( 𝑥 ( Hom ‘ 𝐶 ) 𝑦 ) ∧ ℎ ∈ ( 𝑦 ( Hom ‘ 𝐶 ) 𝑧 ) ) ) ) → ( 𝑔 ( 〈 𝑥 , 𝑥 〉 ( comp ‘ 𝐶 ) 𝑦 ) ( I ↾ ( Base ‘ 𝑥 ) ) ) = ( 𝑔 ∘ ( I ↾ ( Base ‘ 𝑥 ) ) ) ) |
37 |
|
fcoi1 |
⊢ ( 𝑔 : ( Base ‘ 𝑥 ) ⟶ ( Base ‘ 𝑦 ) → ( 𝑔 ∘ ( I ↾ ( Base ‘ 𝑥 ) ) ) = 𝑔 ) |
38 |
35 37
|
syl |
⊢ ( ( 𝑈 ∈ 𝑉 ∧ ( ( 𝑤 ∈ 𝑈 ∧ 𝑥 ∈ 𝑈 ) ∧ ( 𝑦 ∈ 𝑈 ∧ 𝑧 ∈ 𝑈 ) ∧ ( 𝑓 ∈ ( 𝑤 ( Hom ‘ 𝐶 ) 𝑥 ) ∧ 𝑔 ∈ ( 𝑥 ( Hom ‘ 𝐶 ) 𝑦 ) ∧ ℎ ∈ ( 𝑦 ( Hom ‘ 𝐶 ) 𝑧 ) ) ) ) → ( 𝑔 ∘ ( I ↾ ( Base ‘ 𝑥 ) ) ) = 𝑔 ) |
39 |
36 38
|
eqtrd |
⊢ ( ( 𝑈 ∈ 𝑉 ∧ ( ( 𝑤 ∈ 𝑈 ∧ 𝑥 ∈ 𝑈 ) ∧ ( 𝑦 ∈ 𝑈 ∧ 𝑧 ∈ 𝑈 ) ∧ ( 𝑓 ∈ ( 𝑤 ( Hom ‘ 𝐶 ) 𝑥 ) ∧ 𝑔 ∈ ( 𝑥 ( Hom ‘ 𝐶 ) 𝑦 ) ∧ ℎ ∈ ( 𝑦 ( Hom ‘ 𝐶 ) 𝑧 ) ) ) ) → ( 𝑔 ( 〈 𝑥 , 𝑥 〉 ( comp ‘ 𝐶 ) 𝑦 ) ( I ↾ ( Base ‘ 𝑥 ) ) ) = 𝑔 ) |
40 |
1 18 19 20 21 31 22 15 32 25 35
|
estrcco |
⊢ ( ( 𝑈 ∈ 𝑉 ∧ ( ( 𝑤 ∈ 𝑈 ∧ 𝑥 ∈ 𝑈 ) ∧ ( 𝑦 ∈ 𝑈 ∧ 𝑧 ∈ 𝑈 ) ∧ ( 𝑓 ∈ ( 𝑤 ( Hom ‘ 𝐶 ) 𝑥 ) ∧ 𝑔 ∈ ( 𝑥 ( Hom ‘ 𝐶 ) 𝑦 ) ∧ ℎ ∈ ( 𝑦 ( Hom ‘ 𝐶 ) 𝑧 ) ) ) ) → ( 𝑔 ( 〈 𝑤 , 𝑥 〉 ( comp ‘ 𝐶 ) 𝑦 ) 𝑓 ) = ( 𝑔 ∘ 𝑓 ) ) |
41 |
|
fco |
⊢ ( ( 𝑔 : ( Base ‘ 𝑥 ) ⟶ ( Base ‘ 𝑦 ) ∧ 𝑓 : ( Base ‘ 𝑤 ) ⟶ ( Base ‘ 𝑥 ) ) → ( 𝑔 ∘ 𝑓 ) : ( Base ‘ 𝑤 ) ⟶ ( Base ‘ 𝑦 ) ) |
42 |
35 25 41
|
syl2anc |
⊢ ( ( 𝑈 ∈ 𝑉 ∧ ( ( 𝑤 ∈ 𝑈 ∧ 𝑥 ∈ 𝑈 ) ∧ ( 𝑦 ∈ 𝑈 ∧ 𝑧 ∈ 𝑈 ) ∧ ( 𝑓 ∈ ( 𝑤 ( Hom ‘ 𝐶 ) 𝑥 ) ∧ 𝑔 ∈ ( 𝑥 ( Hom ‘ 𝐶 ) 𝑦 ) ∧ ℎ ∈ ( 𝑦 ( Hom ‘ 𝐶 ) 𝑧 ) ) ) ) → ( 𝑔 ∘ 𝑓 ) : ( Base ‘ 𝑤 ) ⟶ ( Base ‘ 𝑦 ) ) |
43 |
1 18 13 20 31 22 32
|
elestrchom |
⊢ ( ( 𝑈 ∈ 𝑉 ∧ ( ( 𝑤 ∈ 𝑈 ∧ 𝑥 ∈ 𝑈 ) ∧ ( 𝑦 ∈ 𝑈 ∧ 𝑧 ∈ 𝑈 ) ∧ ( 𝑓 ∈ ( 𝑤 ( Hom ‘ 𝐶 ) 𝑥 ) ∧ 𝑔 ∈ ( 𝑥 ( Hom ‘ 𝐶 ) 𝑦 ) ∧ ℎ ∈ ( 𝑦 ( Hom ‘ 𝐶 ) 𝑧 ) ) ) ) → ( ( 𝑔 ∘ 𝑓 ) ∈ ( 𝑤 ( Hom ‘ 𝐶 ) 𝑦 ) ↔ ( 𝑔 ∘ 𝑓 ) : ( Base ‘ 𝑤 ) ⟶ ( Base ‘ 𝑦 ) ) ) |
44 |
42 43
|
mpbird |
⊢ ( ( 𝑈 ∈ 𝑉 ∧ ( ( 𝑤 ∈ 𝑈 ∧ 𝑥 ∈ 𝑈 ) ∧ ( 𝑦 ∈ 𝑈 ∧ 𝑧 ∈ 𝑈 ) ∧ ( 𝑓 ∈ ( 𝑤 ( Hom ‘ 𝐶 ) 𝑥 ) ∧ 𝑔 ∈ ( 𝑥 ( Hom ‘ 𝐶 ) 𝑦 ) ∧ ℎ ∈ ( 𝑦 ( Hom ‘ 𝐶 ) 𝑧 ) ) ) ) → ( 𝑔 ∘ 𝑓 ) ∈ ( 𝑤 ( Hom ‘ 𝐶 ) 𝑦 ) ) |
45 |
40 44
|
eqeltrd |
⊢ ( ( 𝑈 ∈ 𝑉 ∧ ( ( 𝑤 ∈ 𝑈 ∧ 𝑥 ∈ 𝑈 ) ∧ ( 𝑦 ∈ 𝑈 ∧ 𝑧 ∈ 𝑈 ) ∧ ( 𝑓 ∈ ( 𝑤 ( Hom ‘ 𝐶 ) 𝑥 ) ∧ 𝑔 ∈ ( 𝑥 ( Hom ‘ 𝐶 ) 𝑦 ) ∧ ℎ ∈ ( 𝑦 ( Hom ‘ 𝐶 ) 𝑧 ) ) ) ) → ( 𝑔 ( 〈 𝑤 , 𝑥 〉 ( comp ‘ 𝐶 ) 𝑦 ) 𝑓 ) ∈ ( 𝑤 ( Hom ‘ 𝐶 ) 𝑦 ) ) |
46 |
|
coass |
⊢ ( ( ℎ ∘ 𝑔 ) ∘ 𝑓 ) = ( ℎ ∘ ( 𝑔 ∘ 𝑓 ) ) |
47 |
|
simpr2r |
⊢ ( ( 𝑈 ∈ 𝑉 ∧ ( ( 𝑤 ∈ 𝑈 ∧ 𝑥 ∈ 𝑈 ) ∧ ( 𝑦 ∈ 𝑈 ∧ 𝑧 ∈ 𝑈 ) ∧ ( 𝑓 ∈ ( 𝑤 ( Hom ‘ 𝐶 ) 𝑥 ) ∧ 𝑔 ∈ ( 𝑥 ( Hom ‘ 𝐶 ) 𝑦 ) ∧ ℎ ∈ ( 𝑦 ( Hom ‘ 𝐶 ) 𝑧 ) ) ) ) → 𝑧 ∈ 𝑈 ) |
48 |
|
eqid |
⊢ ( Base ‘ 𝑧 ) = ( Base ‘ 𝑧 ) |
49 |
|
simpr33 |
⊢ ( ( 𝑈 ∈ 𝑉 ∧ ( ( 𝑤 ∈ 𝑈 ∧ 𝑥 ∈ 𝑈 ) ∧ ( 𝑦 ∈ 𝑈 ∧ 𝑧 ∈ 𝑈 ) ∧ ( 𝑓 ∈ ( 𝑤 ( Hom ‘ 𝐶 ) 𝑥 ) ∧ 𝑔 ∈ ( 𝑥 ( Hom ‘ 𝐶 ) 𝑦 ) ∧ ℎ ∈ ( 𝑦 ( Hom ‘ 𝐶 ) 𝑧 ) ) ) ) → ℎ ∈ ( 𝑦 ( Hom ‘ 𝐶 ) 𝑧 ) ) |
50 |
1 18 13 31 47 32 48
|
elestrchom |
⊢ ( ( 𝑈 ∈ 𝑉 ∧ ( ( 𝑤 ∈ 𝑈 ∧ 𝑥 ∈ 𝑈 ) ∧ ( 𝑦 ∈ 𝑈 ∧ 𝑧 ∈ 𝑈 ) ∧ ( 𝑓 ∈ ( 𝑤 ( Hom ‘ 𝐶 ) 𝑥 ) ∧ 𝑔 ∈ ( 𝑥 ( Hom ‘ 𝐶 ) 𝑦 ) ∧ ℎ ∈ ( 𝑦 ( Hom ‘ 𝐶 ) 𝑧 ) ) ) ) → ( ℎ ∈ ( 𝑦 ( Hom ‘ 𝐶 ) 𝑧 ) ↔ ℎ : ( Base ‘ 𝑦 ) ⟶ ( Base ‘ 𝑧 ) ) ) |
51 |
49 50
|
mpbid |
⊢ ( ( 𝑈 ∈ 𝑉 ∧ ( ( 𝑤 ∈ 𝑈 ∧ 𝑥 ∈ 𝑈 ) ∧ ( 𝑦 ∈ 𝑈 ∧ 𝑧 ∈ 𝑈 ) ∧ ( 𝑓 ∈ ( 𝑤 ( Hom ‘ 𝐶 ) 𝑥 ) ∧ 𝑔 ∈ ( 𝑥 ( Hom ‘ 𝐶 ) 𝑦 ) ∧ ℎ ∈ ( 𝑦 ( Hom ‘ 𝐶 ) 𝑧 ) ) ) ) → ℎ : ( Base ‘ 𝑦 ) ⟶ ( Base ‘ 𝑧 ) ) |
52 |
|
fco |
⊢ ( ( ℎ : ( Base ‘ 𝑦 ) ⟶ ( Base ‘ 𝑧 ) ∧ 𝑔 : ( Base ‘ 𝑥 ) ⟶ ( Base ‘ 𝑦 ) ) → ( ℎ ∘ 𝑔 ) : ( Base ‘ 𝑥 ) ⟶ ( Base ‘ 𝑧 ) ) |
53 |
51 35 52
|
syl2anc |
⊢ ( ( 𝑈 ∈ 𝑉 ∧ ( ( 𝑤 ∈ 𝑈 ∧ 𝑥 ∈ 𝑈 ) ∧ ( 𝑦 ∈ 𝑈 ∧ 𝑧 ∈ 𝑈 ) ∧ ( 𝑓 ∈ ( 𝑤 ( Hom ‘ 𝐶 ) 𝑥 ) ∧ 𝑔 ∈ ( 𝑥 ( Hom ‘ 𝐶 ) 𝑦 ) ∧ ℎ ∈ ( 𝑦 ( Hom ‘ 𝐶 ) 𝑧 ) ) ) ) → ( ℎ ∘ 𝑔 ) : ( Base ‘ 𝑥 ) ⟶ ( Base ‘ 𝑧 ) ) |
54 |
1 18 19 20 21 47 22 15 48 25 53
|
estrcco |
⊢ ( ( 𝑈 ∈ 𝑉 ∧ ( ( 𝑤 ∈ 𝑈 ∧ 𝑥 ∈ 𝑈 ) ∧ ( 𝑦 ∈ 𝑈 ∧ 𝑧 ∈ 𝑈 ) ∧ ( 𝑓 ∈ ( 𝑤 ( Hom ‘ 𝐶 ) 𝑥 ) ∧ 𝑔 ∈ ( 𝑥 ( Hom ‘ 𝐶 ) 𝑦 ) ∧ ℎ ∈ ( 𝑦 ( Hom ‘ 𝐶 ) 𝑧 ) ) ) ) → ( ( ℎ ∘ 𝑔 ) ( 〈 𝑤 , 𝑥 〉 ( comp ‘ 𝐶 ) 𝑧 ) 𝑓 ) = ( ( ℎ ∘ 𝑔 ) ∘ 𝑓 ) ) |
55 |
1 18 19 20 31 47 22 32 48 42 51
|
estrcco |
⊢ ( ( 𝑈 ∈ 𝑉 ∧ ( ( 𝑤 ∈ 𝑈 ∧ 𝑥 ∈ 𝑈 ) ∧ ( 𝑦 ∈ 𝑈 ∧ 𝑧 ∈ 𝑈 ) ∧ ( 𝑓 ∈ ( 𝑤 ( Hom ‘ 𝐶 ) 𝑥 ) ∧ 𝑔 ∈ ( 𝑥 ( Hom ‘ 𝐶 ) 𝑦 ) ∧ ℎ ∈ ( 𝑦 ( Hom ‘ 𝐶 ) 𝑧 ) ) ) ) → ( ℎ ( 〈 𝑤 , 𝑦 〉 ( comp ‘ 𝐶 ) 𝑧 ) ( 𝑔 ∘ 𝑓 ) ) = ( ℎ ∘ ( 𝑔 ∘ 𝑓 ) ) ) |
56 |
46 54 55
|
3eqtr4a |
⊢ ( ( 𝑈 ∈ 𝑉 ∧ ( ( 𝑤 ∈ 𝑈 ∧ 𝑥 ∈ 𝑈 ) ∧ ( 𝑦 ∈ 𝑈 ∧ 𝑧 ∈ 𝑈 ) ∧ ( 𝑓 ∈ ( 𝑤 ( Hom ‘ 𝐶 ) 𝑥 ) ∧ 𝑔 ∈ ( 𝑥 ( Hom ‘ 𝐶 ) 𝑦 ) ∧ ℎ ∈ ( 𝑦 ( Hom ‘ 𝐶 ) 𝑧 ) ) ) ) → ( ( ℎ ∘ 𝑔 ) ( 〈 𝑤 , 𝑥 〉 ( comp ‘ 𝐶 ) 𝑧 ) 𝑓 ) = ( ℎ ( 〈 𝑤 , 𝑦 〉 ( comp ‘ 𝐶 ) 𝑧 ) ( 𝑔 ∘ 𝑓 ) ) ) |
57 |
1 18 19 21 31 47 15 32 48 35 51
|
estrcco |
⊢ ( ( 𝑈 ∈ 𝑉 ∧ ( ( 𝑤 ∈ 𝑈 ∧ 𝑥 ∈ 𝑈 ) ∧ ( 𝑦 ∈ 𝑈 ∧ 𝑧 ∈ 𝑈 ) ∧ ( 𝑓 ∈ ( 𝑤 ( Hom ‘ 𝐶 ) 𝑥 ) ∧ 𝑔 ∈ ( 𝑥 ( Hom ‘ 𝐶 ) 𝑦 ) ∧ ℎ ∈ ( 𝑦 ( Hom ‘ 𝐶 ) 𝑧 ) ) ) ) → ( ℎ ( 〈 𝑥 , 𝑦 〉 ( comp ‘ 𝐶 ) 𝑧 ) 𝑔 ) = ( ℎ ∘ 𝑔 ) ) |
58 |
57
|
oveq1d |
⊢ ( ( 𝑈 ∈ 𝑉 ∧ ( ( 𝑤 ∈ 𝑈 ∧ 𝑥 ∈ 𝑈 ) ∧ ( 𝑦 ∈ 𝑈 ∧ 𝑧 ∈ 𝑈 ) ∧ ( 𝑓 ∈ ( 𝑤 ( Hom ‘ 𝐶 ) 𝑥 ) ∧ 𝑔 ∈ ( 𝑥 ( Hom ‘ 𝐶 ) 𝑦 ) ∧ ℎ ∈ ( 𝑦 ( Hom ‘ 𝐶 ) 𝑧 ) ) ) ) → ( ( ℎ ( 〈 𝑥 , 𝑦 〉 ( comp ‘ 𝐶 ) 𝑧 ) 𝑔 ) ( 〈 𝑤 , 𝑥 〉 ( comp ‘ 𝐶 ) 𝑧 ) 𝑓 ) = ( ( ℎ ∘ 𝑔 ) ( 〈 𝑤 , 𝑥 〉 ( comp ‘ 𝐶 ) 𝑧 ) 𝑓 ) ) |
59 |
40
|
oveq2d |
⊢ ( ( 𝑈 ∈ 𝑉 ∧ ( ( 𝑤 ∈ 𝑈 ∧ 𝑥 ∈ 𝑈 ) ∧ ( 𝑦 ∈ 𝑈 ∧ 𝑧 ∈ 𝑈 ) ∧ ( 𝑓 ∈ ( 𝑤 ( Hom ‘ 𝐶 ) 𝑥 ) ∧ 𝑔 ∈ ( 𝑥 ( Hom ‘ 𝐶 ) 𝑦 ) ∧ ℎ ∈ ( 𝑦 ( Hom ‘ 𝐶 ) 𝑧 ) ) ) ) → ( ℎ ( 〈 𝑤 , 𝑦 〉 ( comp ‘ 𝐶 ) 𝑧 ) ( 𝑔 ( 〈 𝑤 , 𝑥 〉 ( comp ‘ 𝐶 ) 𝑦 ) 𝑓 ) ) = ( ℎ ( 〈 𝑤 , 𝑦 〉 ( comp ‘ 𝐶 ) 𝑧 ) ( 𝑔 ∘ 𝑓 ) ) ) |
60 |
56 58 59
|
3eqtr4d |
⊢ ( ( 𝑈 ∈ 𝑉 ∧ ( ( 𝑤 ∈ 𝑈 ∧ 𝑥 ∈ 𝑈 ) ∧ ( 𝑦 ∈ 𝑈 ∧ 𝑧 ∈ 𝑈 ) ∧ ( 𝑓 ∈ ( 𝑤 ( Hom ‘ 𝐶 ) 𝑥 ) ∧ 𝑔 ∈ ( 𝑥 ( Hom ‘ 𝐶 ) 𝑦 ) ∧ ℎ ∈ ( 𝑦 ( Hom ‘ 𝐶 ) 𝑧 ) ) ) ) → ( ( ℎ ( 〈 𝑥 , 𝑦 〉 ( comp ‘ 𝐶 ) 𝑧 ) 𝑔 ) ( 〈 𝑤 , 𝑥 〉 ( comp ‘ 𝐶 ) 𝑧 ) 𝑓 ) = ( ℎ ( 〈 𝑤 , 𝑦 〉 ( comp ‘ 𝐶 ) 𝑧 ) ( 𝑔 ( 〈 𝑤 , 𝑥 〉 ( comp ‘ 𝐶 ) 𝑦 ) 𝑓 ) ) ) |
61 |
3 4 5 7 8 17 30 39 45 60
|
iscatd2 |
⊢ ( 𝑈 ∈ 𝑉 → ( 𝐶 ∈ Cat ∧ ( Id ‘ 𝐶 ) = ( 𝑥 ∈ 𝑈 ↦ ( I ↾ ( Base ‘ 𝑥 ) ) ) ) ) |