Step |
Hyp |
Ref |
Expression |
1 |
|
dfrngc2.c |
⊢ 𝐶 = ( RngCat ‘ 𝑈 ) |
2 |
|
dfrngc2.u |
⊢ ( 𝜑 → 𝑈 ∈ 𝑉 ) |
3 |
|
dfrngc2.b |
⊢ ( 𝜑 → 𝐵 = ( 𝑈 ∩ Rng ) ) |
4 |
|
dfrngc2.h |
⊢ ( 𝜑 → 𝐻 = ( RngHomo ↾ ( 𝐵 × 𝐵 ) ) ) |
5 |
|
dfrngc2.o |
⊢ ( 𝜑 → · = ( comp ‘ ( ExtStrCat ‘ 𝑈 ) ) ) |
6 |
1 2 3 4
|
rngcval |
⊢ ( 𝜑 → 𝐶 = ( ( ExtStrCat ‘ 𝑈 ) ↾cat 𝐻 ) ) |
7 |
|
eqid |
⊢ ( ( ExtStrCat ‘ 𝑈 ) ↾cat 𝐻 ) = ( ( ExtStrCat ‘ 𝑈 ) ↾cat 𝐻 ) |
8 |
|
fvexd |
⊢ ( 𝜑 → ( ExtStrCat ‘ 𝑈 ) ∈ V ) |
9 |
|
inex1g |
⊢ ( 𝑈 ∈ 𝑉 → ( 𝑈 ∩ Rng ) ∈ V ) |
10 |
2 9
|
syl |
⊢ ( 𝜑 → ( 𝑈 ∩ Rng ) ∈ V ) |
11 |
3 10
|
eqeltrd |
⊢ ( 𝜑 → 𝐵 ∈ V ) |
12 |
3 4
|
rnghmresfn |
⊢ ( 𝜑 → 𝐻 Fn ( 𝐵 × 𝐵 ) ) |
13 |
7 8 11 12
|
rescval2 |
⊢ ( 𝜑 → ( ( ExtStrCat ‘ 𝑈 ) ↾cat 𝐻 ) = ( ( ( ExtStrCat ‘ 𝑈 ) ↾s 𝐵 ) sSet 〈 ( Hom ‘ ndx ) , 𝐻 〉 ) ) |
14 |
|
eqid |
⊢ ( ExtStrCat ‘ 𝑈 ) = ( ExtStrCat ‘ 𝑈 ) |
15 |
|
eqidd |
⊢ ( 𝜑 → ( 𝑥 ∈ 𝑈 , 𝑦 ∈ 𝑈 ↦ ( ( Base ‘ 𝑦 ) ↑m ( Base ‘ 𝑥 ) ) ) = ( 𝑥 ∈ 𝑈 , 𝑦 ∈ 𝑈 ↦ ( ( Base ‘ 𝑦 ) ↑m ( Base ‘ 𝑥 ) ) ) ) |
16 |
|
eqid |
⊢ ( comp ‘ ( ExtStrCat ‘ 𝑈 ) ) = ( comp ‘ ( ExtStrCat ‘ 𝑈 ) ) |
17 |
14 2 16
|
estrccofval |
⊢ ( 𝜑 → ( comp ‘ ( ExtStrCat ‘ 𝑈 ) ) = ( 𝑣 ∈ ( 𝑈 × 𝑈 ) , 𝑧 ∈ 𝑈 ↦ ( 𝑔 ∈ ( ( Base ‘ 𝑧 ) ↑m ( Base ‘ ( 2nd ‘ 𝑣 ) ) ) , 𝑓 ∈ ( ( Base ‘ ( 2nd ‘ 𝑣 ) ) ↑m ( Base ‘ ( 1st ‘ 𝑣 ) ) ) ↦ ( 𝑔 ∘ 𝑓 ) ) ) ) |
18 |
5 17
|
eqtrd |
⊢ ( 𝜑 → · = ( 𝑣 ∈ ( 𝑈 × 𝑈 ) , 𝑧 ∈ 𝑈 ↦ ( 𝑔 ∈ ( ( Base ‘ 𝑧 ) ↑m ( Base ‘ ( 2nd ‘ 𝑣 ) ) ) , 𝑓 ∈ ( ( Base ‘ ( 2nd ‘ 𝑣 ) ) ↑m ( Base ‘ ( 1st ‘ 𝑣 ) ) ) ↦ ( 𝑔 ∘ 𝑓 ) ) ) ) |
19 |
14 2 15 18
|
estrcval |
⊢ ( 𝜑 → ( ExtStrCat ‘ 𝑈 ) = { 〈 ( Base ‘ ndx ) , 𝑈 〉 , 〈 ( Hom ‘ ndx ) , ( 𝑥 ∈ 𝑈 , 𝑦 ∈ 𝑈 ↦ ( ( Base ‘ 𝑦 ) ↑m ( Base ‘ 𝑥 ) ) ) 〉 , 〈 ( comp ‘ ndx ) , · 〉 } ) |
20 |
|
mpoexga |
⊢ ( ( 𝑈 ∈ 𝑉 ∧ 𝑈 ∈ 𝑉 ) → ( 𝑥 ∈ 𝑈 , 𝑦 ∈ 𝑈 ↦ ( ( Base ‘ 𝑦 ) ↑m ( Base ‘ 𝑥 ) ) ) ∈ V ) |
21 |
2 2 20
|
syl2anc |
⊢ ( 𝜑 → ( 𝑥 ∈ 𝑈 , 𝑦 ∈ 𝑈 ↦ ( ( Base ‘ 𝑦 ) ↑m ( Base ‘ 𝑥 ) ) ) ∈ V ) |
22 |
|
fvexd |
⊢ ( 𝜑 → ( comp ‘ ( ExtStrCat ‘ 𝑈 ) ) ∈ V ) |
23 |
5 22
|
eqeltrd |
⊢ ( 𝜑 → · ∈ V ) |
24 |
|
rnghmfn |
⊢ RngHomo Fn ( Rng × Rng ) |
25 |
|
fnfun |
⊢ ( RngHomo Fn ( Rng × Rng ) → Fun RngHomo ) |
26 |
24 25
|
mp1i |
⊢ ( 𝜑 → Fun RngHomo ) |
27 |
|
sqxpexg |
⊢ ( 𝐵 ∈ V → ( 𝐵 × 𝐵 ) ∈ V ) |
28 |
11 27
|
syl |
⊢ ( 𝜑 → ( 𝐵 × 𝐵 ) ∈ V ) |
29 |
|
resfunexg |
⊢ ( ( Fun RngHomo ∧ ( 𝐵 × 𝐵 ) ∈ V ) → ( RngHomo ↾ ( 𝐵 × 𝐵 ) ) ∈ V ) |
30 |
26 28 29
|
syl2anc |
⊢ ( 𝜑 → ( RngHomo ↾ ( 𝐵 × 𝐵 ) ) ∈ V ) |
31 |
4 30
|
eqeltrd |
⊢ ( 𝜑 → 𝐻 ∈ V ) |
32 |
|
inss1 |
⊢ ( 𝑈 ∩ Rng ) ⊆ 𝑈 |
33 |
3 32
|
eqsstrdi |
⊢ ( 𝜑 → 𝐵 ⊆ 𝑈 ) |
34 |
19 2 21 23 31 33
|
estrres |
⊢ ( 𝜑 → ( ( ( ExtStrCat ‘ 𝑈 ) ↾s 𝐵 ) sSet 〈 ( Hom ‘ ndx ) , 𝐻 〉 ) = { 〈 ( Base ‘ ndx ) , 𝐵 〉 , 〈 ( Hom ‘ ndx ) , 𝐻 〉 , 〈 ( comp ‘ ndx ) , · 〉 } ) |
35 |
6 13 34
|
3eqtrd |
⊢ ( 𝜑 → 𝐶 = { 〈 ( Base ‘ ndx ) , 𝐵 〉 , 〈 ( Hom ‘ ndx ) , 𝐻 〉 , 〈 ( comp ‘ ndx ) , · 〉 } ) |