Step |
Hyp |
Ref |
Expression |
1 |
|
estrcbas.c |
⊢ 𝐶 = ( ExtStrCat ‘ 𝑈 ) |
2 |
|
estrcbas.u |
⊢ ( 𝜑 → 𝑈 ∈ 𝑉 ) |
3 |
|
estrcco.o |
⊢ · = ( comp ‘ 𝐶 ) |
4 |
|
eqid |
⊢ ( Hom ‘ 𝐶 ) = ( Hom ‘ 𝐶 ) |
5 |
1 2 4
|
estrchomfval |
⊢ ( 𝜑 → ( Hom ‘ 𝐶 ) = ( 𝑥 ∈ 𝑈 , 𝑦 ∈ 𝑈 ↦ ( ( Base ‘ 𝑦 ) ↑m ( Base ‘ 𝑥 ) ) ) ) |
6 |
|
eqidd |
⊢ ( 𝜑 → ( 𝑣 ∈ ( 𝑈 × 𝑈 ) , 𝑧 ∈ 𝑈 ↦ ( 𝑔 ∈ ( ( Base ‘ 𝑧 ) ↑m ( Base ‘ ( 2nd ‘ 𝑣 ) ) ) , 𝑓 ∈ ( ( Base ‘ ( 2nd ‘ 𝑣 ) ) ↑m ( Base ‘ ( 1st ‘ 𝑣 ) ) ) ↦ ( 𝑔 ∘ 𝑓 ) ) ) = ( 𝑣 ∈ ( 𝑈 × 𝑈 ) , 𝑧 ∈ 𝑈 ↦ ( 𝑔 ∈ ( ( Base ‘ 𝑧 ) ↑m ( Base ‘ ( 2nd ‘ 𝑣 ) ) ) , 𝑓 ∈ ( ( Base ‘ ( 2nd ‘ 𝑣 ) ) ↑m ( Base ‘ ( 1st ‘ 𝑣 ) ) ) ↦ ( 𝑔 ∘ 𝑓 ) ) ) ) |
7 |
1 2 5 6
|
estrcval |
⊢ ( 𝜑 → 𝐶 = { 〈 ( Base ‘ ndx ) , 𝑈 〉 , 〈 ( Hom ‘ ndx ) , ( Hom ‘ 𝐶 ) 〉 , 〈 ( comp ‘ ndx ) , ( 𝑣 ∈ ( 𝑈 × 𝑈 ) , 𝑧 ∈ 𝑈 ↦ ( 𝑔 ∈ ( ( Base ‘ 𝑧 ) ↑m ( Base ‘ ( 2nd ‘ 𝑣 ) ) ) , 𝑓 ∈ ( ( Base ‘ ( 2nd ‘ 𝑣 ) ) ↑m ( Base ‘ ( 1st ‘ 𝑣 ) ) ) ↦ ( 𝑔 ∘ 𝑓 ) ) ) 〉 } ) |
8 |
|
catstr |
⊢ { 〈 ( Base ‘ ndx ) , 𝑈 〉 , 〈 ( Hom ‘ ndx ) , ( Hom ‘ 𝐶 ) 〉 , 〈 ( comp ‘ ndx ) , ( 𝑣 ∈ ( 𝑈 × 𝑈 ) , 𝑧 ∈ 𝑈 ↦ ( 𝑔 ∈ ( ( Base ‘ 𝑧 ) ↑m ( Base ‘ ( 2nd ‘ 𝑣 ) ) ) , 𝑓 ∈ ( ( Base ‘ ( 2nd ‘ 𝑣 ) ) ↑m ( Base ‘ ( 1st ‘ 𝑣 ) ) ) ↦ ( 𝑔 ∘ 𝑓 ) ) ) 〉 } Struct 〈 1 , ; 1 5 〉 |
9 |
|
ccoid |
⊢ comp = Slot ( comp ‘ ndx ) |
10 |
|
snsstp3 |
⊢ { 〈 ( comp ‘ ndx ) , ( 𝑣 ∈ ( 𝑈 × 𝑈 ) , 𝑧 ∈ 𝑈 ↦ ( 𝑔 ∈ ( ( Base ‘ 𝑧 ) ↑m ( Base ‘ ( 2nd ‘ 𝑣 ) ) ) , 𝑓 ∈ ( ( Base ‘ ( 2nd ‘ 𝑣 ) ) ↑m ( Base ‘ ( 1st ‘ 𝑣 ) ) ) ↦ ( 𝑔 ∘ 𝑓 ) ) ) 〉 } ⊆ { 〈 ( Base ‘ ndx ) , 𝑈 〉 , 〈 ( Hom ‘ ndx ) , ( Hom ‘ 𝐶 ) 〉 , 〈 ( comp ‘ ndx ) , ( 𝑣 ∈ ( 𝑈 × 𝑈 ) , 𝑧 ∈ 𝑈 ↦ ( 𝑔 ∈ ( ( Base ‘ 𝑧 ) ↑m ( Base ‘ ( 2nd ‘ 𝑣 ) ) ) , 𝑓 ∈ ( ( Base ‘ ( 2nd ‘ 𝑣 ) ) ↑m ( Base ‘ ( 1st ‘ 𝑣 ) ) ) ↦ ( 𝑔 ∘ 𝑓 ) ) ) 〉 } |
11 |
2 2
|
xpexd |
⊢ ( 𝜑 → ( 𝑈 × 𝑈 ) ∈ V ) |
12 |
|
mpoexga |
⊢ ( ( ( 𝑈 × 𝑈 ) ∈ V ∧ 𝑈 ∈ 𝑉 ) → ( 𝑣 ∈ ( 𝑈 × 𝑈 ) , 𝑧 ∈ 𝑈 ↦ ( 𝑔 ∈ ( ( Base ‘ 𝑧 ) ↑m ( Base ‘ ( 2nd ‘ 𝑣 ) ) ) , 𝑓 ∈ ( ( Base ‘ ( 2nd ‘ 𝑣 ) ) ↑m ( Base ‘ ( 1st ‘ 𝑣 ) ) ) ↦ ( 𝑔 ∘ 𝑓 ) ) ) ∈ V ) |
13 |
11 2 12
|
syl2anc |
⊢ ( 𝜑 → ( 𝑣 ∈ ( 𝑈 × 𝑈 ) , 𝑧 ∈ 𝑈 ↦ ( 𝑔 ∈ ( ( Base ‘ 𝑧 ) ↑m ( Base ‘ ( 2nd ‘ 𝑣 ) ) ) , 𝑓 ∈ ( ( Base ‘ ( 2nd ‘ 𝑣 ) ) ↑m ( Base ‘ ( 1st ‘ 𝑣 ) ) ) ↦ ( 𝑔 ∘ 𝑓 ) ) ) ∈ V ) |
14 |
7 8 9 10 13 3
|
strfv3 |
⊢ ( 𝜑 → · = ( 𝑣 ∈ ( 𝑈 × 𝑈 ) , 𝑧 ∈ 𝑈 ↦ ( 𝑔 ∈ ( ( Base ‘ 𝑧 ) ↑m ( Base ‘ ( 2nd ‘ 𝑣 ) ) ) , 𝑓 ∈ ( ( Base ‘ ( 2nd ‘ 𝑣 ) ) ↑m ( Base ‘ ( 1st ‘ 𝑣 ) ) ) ↦ ( 𝑔 ∘ 𝑓 ) ) ) ) |