Step | Hyp | Ref
| Expression |
1 | | estrcval.c |
. 2
⊢ 𝐶 = (ExtStrCat‘𝑈) |
2 | | df-estrc 16586 |
. . . 4
⊢ ExtStrCat
= (𝑢 ∈ V ↦
{〈(Base‘ndx), 𝑢〉, 〈(Hom ‘ndx), (𝑥 ∈ 𝑢, 𝑦 ∈ 𝑢 ↦ ((Base‘𝑦) ↑𝑚
(Base‘𝑥)))〉,
〈(comp‘ndx), (𝑣
∈ (𝑢 × 𝑢), 𝑧 ∈ 𝑢 ↦ (𝑔 ∈ ((Base‘𝑧) ↑𝑚
(Base‘(2nd ‘𝑣))), 𝑓 ∈ ((Base‘(2nd
‘𝑣))
↑𝑚 (Base‘(1st ‘𝑣))) ↦ (𝑔 ∘ 𝑓)))〉}) |
3 | 2 | a1i 11 |
. . 3
⊢ (𝜑 → ExtStrCat = (𝑢 ∈ V ↦
{〈(Base‘ndx), 𝑢〉, 〈(Hom ‘ndx), (𝑥 ∈ 𝑢, 𝑦 ∈ 𝑢 ↦ ((Base‘𝑦) ↑𝑚
(Base‘𝑥)))〉,
〈(comp‘ndx), (𝑣
∈ (𝑢 × 𝑢), 𝑧 ∈ 𝑢 ↦ (𝑔 ∈ ((Base‘𝑧) ↑𝑚
(Base‘(2nd ‘𝑣))), 𝑓 ∈ ((Base‘(2nd
‘𝑣))
↑𝑚 (Base‘(1st ‘𝑣))) ↦ (𝑔 ∘ 𝑓)))〉})) |
4 | | simpr 476 |
. . . . 5
⊢ ((𝜑 ∧ 𝑢 = 𝑈) → 𝑢 = 𝑈) |
5 | 4 | opeq2d 4347 |
. . . 4
⊢ ((𝜑 ∧ 𝑢 = 𝑈) → 〈(Base‘ndx), 𝑢〉 = 〈(Base‘ndx),
𝑈〉) |
6 | | eqidd 2611 |
. . . . . . 7
⊢ ((𝜑 ∧ 𝑢 = 𝑈) → ((Base‘𝑦) ↑𝑚
(Base‘𝑥)) =
((Base‘𝑦)
↑𝑚 (Base‘𝑥))) |
7 | 4, 4, 6 | mpt2eq123dv 6615 |
. . . . . 6
⊢ ((𝜑 ∧ 𝑢 = 𝑈) → (𝑥 ∈ 𝑢, 𝑦 ∈ 𝑢 ↦ ((Base‘𝑦) ↑𝑚
(Base‘𝑥))) = (𝑥 ∈ 𝑈, 𝑦 ∈ 𝑈 ↦ ((Base‘𝑦) ↑𝑚
(Base‘𝑥)))) |
8 | | estrcval.h |
. . . . . . 7
⊢ (𝜑 → 𝐻 = (𝑥 ∈ 𝑈, 𝑦 ∈ 𝑈 ↦ ((Base‘𝑦) ↑𝑚
(Base‘𝑥)))) |
9 | 8 | adantr 480 |
. . . . . 6
⊢ ((𝜑 ∧ 𝑢 = 𝑈) → 𝐻 = (𝑥 ∈ 𝑈, 𝑦 ∈ 𝑈 ↦ ((Base‘𝑦) ↑𝑚
(Base‘𝑥)))) |
10 | 7, 9 | eqtr4d 2647 |
. . . . 5
⊢ ((𝜑 ∧ 𝑢 = 𝑈) → (𝑥 ∈ 𝑢, 𝑦 ∈ 𝑢 ↦ ((Base‘𝑦) ↑𝑚
(Base‘𝑥))) = 𝐻) |
11 | 10 | opeq2d 4347 |
. . . 4
⊢ ((𝜑 ∧ 𝑢 = 𝑈) → 〈(Hom ‘ndx), (𝑥 ∈ 𝑢, 𝑦 ∈ 𝑢 ↦ ((Base‘𝑦) ↑𝑚
(Base‘𝑥)))〉 =
〈(Hom ‘ndx), 𝐻〉) |
12 | 4 | sqxpeqd 5065 |
. . . . . . 7
⊢ ((𝜑 ∧ 𝑢 = 𝑈) → (𝑢 × 𝑢) = (𝑈 × 𝑈)) |
13 | | eqidd 2611 |
. . . . . . 7
⊢ ((𝜑 ∧ 𝑢 = 𝑈) → (𝑔 ∈ ((Base‘𝑧) ↑𝑚
(Base‘(2nd ‘𝑣))), 𝑓 ∈ ((Base‘(2nd
‘𝑣))
↑𝑚 (Base‘(1st ‘𝑣))) ↦ (𝑔 ∘ 𝑓)) = (𝑔 ∈ ((Base‘𝑧) ↑𝑚
(Base‘(2nd ‘𝑣))), 𝑓 ∈ ((Base‘(2nd
‘𝑣))
↑𝑚 (Base‘(1st ‘𝑣))) ↦ (𝑔 ∘ 𝑓))) |
14 | 12, 4, 13 | mpt2eq123dv 6615 |
. . . . . 6
⊢ ((𝜑 ∧ 𝑢 = 𝑈) → (𝑣 ∈ (𝑢 × 𝑢), 𝑧 ∈ 𝑢 ↦ (𝑔 ∈ ((Base‘𝑧) ↑𝑚
(Base‘(2nd ‘𝑣))), 𝑓 ∈ ((Base‘(2nd
‘𝑣))
↑𝑚 (Base‘(1st ‘𝑣))) ↦ (𝑔 ∘ 𝑓))) = (𝑣 ∈ (𝑈 × 𝑈), 𝑧 ∈ 𝑈 ↦ (𝑔 ∈ ((Base‘𝑧) ↑𝑚
(Base‘(2nd ‘𝑣))), 𝑓 ∈ ((Base‘(2nd
‘𝑣))
↑𝑚 (Base‘(1st ‘𝑣))) ↦ (𝑔 ∘ 𝑓)))) |
15 | | estrcval.o |
. . . . . . 7
⊢ (𝜑 → · = (𝑣 ∈ (𝑈 × 𝑈), 𝑧 ∈ 𝑈 ↦ (𝑔 ∈ ((Base‘𝑧) ↑𝑚
(Base‘(2nd ‘𝑣))), 𝑓 ∈ ((Base‘(2nd
‘𝑣))
↑𝑚 (Base‘(1st ‘𝑣))) ↦ (𝑔 ∘ 𝑓)))) |
16 | 15 | adantr 480 |
. . . . . 6
⊢ ((𝜑 ∧ 𝑢 = 𝑈) → · = (𝑣 ∈ (𝑈 × 𝑈), 𝑧 ∈ 𝑈 ↦ (𝑔 ∈ ((Base‘𝑧) ↑𝑚
(Base‘(2nd ‘𝑣))), 𝑓 ∈ ((Base‘(2nd
‘𝑣))
↑𝑚 (Base‘(1st ‘𝑣))) ↦ (𝑔 ∘ 𝑓)))) |
17 | 14, 16 | eqtr4d 2647 |
. . . . 5
⊢ ((𝜑 ∧ 𝑢 = 𝑈) → (𝑣 ∈ (𝑢 × 𝑢), 𝑧 ∈ 𝑢 ↦ (𝑔 ∈ ((Base‘𝑧) ↑𝑚
(Base‘(2nd ‘𝑣))), 𝑓 ∈ ((Base‘(2nd
‘𝑣))
↑𝑚 (Base‘(1st ‘𝑣))) ↦ (𝑔 ∘ 𝑓))) = · ) |
18 | 17 | opeq2d 4347 |
. . . 4
⊢ ((𝜑 ∧ 𝑢 = 𝑈) → 〈(comp‘ndx), (𝑣 ∈ (𝑢 × 𝑢), 𝑧 ∈ 𝑢 ↦ (𝑔 ∈ ((Base‘𝑧) ↑𝑚
(Base‘(2nd ‘𝑣))), 𝑓 ∈ ((Base‘(2nd
‘𝑣))
↑𝑚 (Base‘(1st ‘𝑣))) ↦ (𝑔 ∘ 𝑓)))〉 = 〈(comp‘ndx), ·
〉) |
19 | 5, 11, 18 | tpeq123d 4227 |
. . 3
⊢ ((𝜑 ∧ 𝑢 = 𝑈) → {〈(Base‘ndx), 𝑢〉, 〈(Hom ‘ndx),
(𝑥 ∈ 𝑢, 𝑦 ∈ 𝑢 ↦ ((Base‘𝑦) ↑𝑚
(Base‘𝑥)))〉,
〈(comp‘ndx), (𝑣
∈ (𝑢 × 𝑢), 𝑧 ∈ 𝑢 ↦ (𝑔 ∈ ((Base‘𝑧) ↑𝑚
(Base‘(2nd ‘𝑣))), 𝑓 ∈ ((Base‘(2nd
‘𝑣))
↑𝑚 (Base‘(1st ‘𝑣))) ↦ (𝑔 ∘ 𝑓)))〉} = {〈(Base‘ndx), 𝑈〉, 〈(Hom ‘ndx),
𝐻〉,
〈(comp‘ndx), ·
〉}) |
20 | | estrcval.u |
. . . 4
⊢ (𝜑 → 𝑈 ∈ 𝑉) |
21 | | elex 3185 |
. . . 4
⊢ (𝑈 ∈ 𝑉 → 𝑈 ∈ V) |
22 | 20, 21 | syl 17 |
. . 3
⊢ (𝜑 → 𝑈 ∈ V) |
23 | | tpex 6855 |
. . . 4
⊢
{〈(Base‘ndx), 𝑈〉, 〈(Hom ‘ndx), 𝐻〉, 〈(comp‘ndx),
·
〉} ∈ V |
24 | 23 | a1i 11 |
. . 3
⊢ (𝜑 → {〈(Base‘ndx),
𝑈〉, 〈(Hom
‘ndx), 𝐻〉,
〈(comp‘ndx), · 〉} ∈
V) |
25 | 3, 19, 22, 24 | fvmptd 6197 |
. 2
⊢ (𝜑 → (ExtStrCat‘𝑈) = {〈(Base‘ndx),
𝑈〉, 〈(Hom
‘ndx), 𝐻〉,
〈(comp‘ndx), ·
〉}) |
26 | 1, 25 | syl5eq 2656 |
1
⊢ (𝜑 → 𝐶 = {〈(Base‘ndx), 𝑈〉, 〈(Hom ‘ndx),
𝐻〉,
〈(comp‘ndx), ·
〉}) |