Step | Hyp | Ref
| Expression |
1 | | estrcval.c |
. 2
⊢ 𝐶 = (ExtStrCat‘𝑈) |
2 | | df-estrc 17837 |
. . 3
⊢ ExtStrCat
= (𝑢 ∈ V ↦
{〈(Base‘ndx), 𝑢〉, 〈(Hom ‘ndx), (𝑥 ∈ 𝑢, 𝑦 ∈ 𝑢 ↦ ((Base‘𝑦) ↑m (Base‘𝑥)))〉,
〈(comp‘ndx), (𝑣
∈ (𝑢 × 𝑢), 𝑧 ∈ 𝑢 ↦ (𝑔 ∈ ((Base‘𝑧) ↑m
(Base‘(2nd ‘𝑣))), 𝑓 ∈ ((Base‘(2nd
‘𝑣))
↑m (Base‘(1st ‘𝑣))) ↦ (𝑔 ∘ 𝑓)))〉}) |
3 | | simpr 485 |
. . . . 5
⊢ ((𝜑 ∧ 𝑢 = 𝑈) → 𝑢 = 𝑈) |
4 | 3 | opeq2d 4817 |
. . . 4
⊢ ((𝜑 ∧ 𝑢 = 𝑈) → 〈(Base‘ndx), 𝑢〉 = 〈(Base‘ndx),
𝑈〉) |
5 | | eqidd 2741 |
. . . . . . 7
⊢ ((𝜑 ∧ 𝑢 = 𝑈) → ((Base‘𝑦) ↑m (Base‘𝑥)) = ((Base‘𝑦) ↑m
(Base‘𝑥))) |
6 | 3, 3, 5 | mpoeq123dv 7344 |
. . . . . 6
⊢ ((𝜑 ∧ 𝑢 = 𝑈) → (𝑥 ∈ 𝑢, 𝑦 ∈ 𝑢 ↦ ((Base‘𝑦) ↑m (Base‘𝑥))) = (𝑥 ∈ 𝑈, 𝑦 ∈ 𝑈 ↦ ((Base‘𝑦) ↑m (Base‘𝑥)))) |
7 | | estrcval.h |
. . . . . . 7
⊢ (𝜑 → 𝐻 = (𝑥 ∈ 𝑈, 𝑦 ∈ 𝑈 ↦ ((Base‘𝑦) ↑m (Base‘𝑥)))) |
8 | 7 | adantr 481 |
. . . . . 6
⊢ ((𝜑 ∧ 𝑢 = 𝑈) → 𝐻 = (𝑥 ∈ 𝑈, 𝑦 ∈ 𝑈 ↦ ((Base‘𝑦) ↑m (Base‘𝑥)))) |
9 | 6, 8 | eqtr4d 2783 |
. . . . 5
⊢ ((𝜑 ∧ 𝑢 = 𝑈) → (𝑥 ∈ 𝑢, 𝑦 ∈ 𝑢 ↦ ((Base‘𝑦) ↑m (Base‘𝑥))) = 𝐻) |
10 | 9 | opeq2d 4817 |
. . . 4
⊢ ((𝜑 ∧ 𝑢 = 𝑈) → 〈(Hom ‘ndx), (𝑥 ∈ 𝑢, 𝑦 ∈ 𝑢 ↦ ((Base‘𝑦) ↑m (Base‘𝑥)))〉 = 〈(Hom
‘ndx), 𝐻〉) |
11 | 3 | sqxpeqd 5622 |
. . . . . . 7
⊢ ((𝜑 ∧ 𝑢 = 𝑈) → (𝑢 × 𝑢) = (𝑈 × 𝑈)) |
12 | | eqidd 2741 |
. . . . . . 7
⊢ ((𝜑 ∧ 𝑢 = 𝑈) → (𝑔 ∈ ((Base‘𝑧) ↑m
(Base‘(2nd ‘𝑣))), 𝑓 ∈ ((Base‘(2nd
‘𝑣))
↑m (Base‘(1st ‘𝑣))) ↦ (𝑔 ∘ 𝑓)) = (𝑔 ∈ ((Base‘𝑧) ↑m
(Base‘(2nd ‘𝑣))), 𝑓 ∈ ((Base‘(2nd
‘𝑣))
↑m (Base‘(1st ‘𝑣))) ↦ (𝑔 ∘ 𝑓))) |
13 | 11, 3, 12 | mpoeq123dv 7344 |
. . . . . 6
⊢ ((𝜑 ∧ 𝑢 = 𝑈) → (𝑣 ∈ (𝑢 × 𝑢), 𝑧 ∈ 𝑢 ↦ (𝑔 ∈ ((Base‘𝑧) ↑m
(Base‘(2nd ‘𝑣))), 𝑓 ∈ ((Base‘(2nd
‘𝑣))
↑m (Base‘(1st ‘𝑣))) ↦ (𝑔 ∘ 𝑓))) = (𝑣 ∈ (𝑈 × 𝑈), 𝑧 ∈ 𝑈 ↦ (𝑔 ∈ ((Base‘𝑧) ↑m
(Base‘(2nd ‘𝑣))), 𝑓 ∈ ((Base‘(2nd
‘𝑣))
↑m (Base‘(1st ‘𝑣))) ↦ (𝑔 ∘ 𝑓)))) |
14 | | estrcval.o |
. . . . . . 7
⊢ (𝜑 → · = (𝑣 ∈ (𝑈 × 𝑈), 𝑧 ∈ 𝑈 ↦ (𝑔 ∈ ((Base‘𝑧) ↑m
(Base‘(2nd ‘𝑣))), 𝑓 ∈ ((Base‘(2nd
‘𝑣))
↑m (Base‘(1st ‘𝑣))) ↦ (𝑔 ∘ 𝑓)))) |
15 | 14 | adantr 481 |
. . . . . 6
⊢ ((𝜑 ∧ 𝑢 = 𝑈) → · = (𝑣 ∈ (𝑈 × 𝑈), 𝑧 ∈ 𝑈 ↦ (𝑔 ∈ ((Base‘𝑧) ↑m
(Base‘(2nd ‘𝑣))), 𝑓 ∈ ((Base‘(2nd
‘𝑣))
↑m (Base‘(1st ‘𝑣))) ↦ (𝑔 ∘ 𝑓)))) |
16 | 13, 15 | eqtr4d 2783 |
. . . . 5
⊢ ((𝜑 ∧ 𝑢 = 𝑈) → (𝑣 ∈ (𝑢 × 𝑢), 𝑧 ∈ 𝑢 ↦ (𝑔 ∈ ((Base‘𝑧) ↑m
(Base‘(2nd ‘𝑣))), 𝑓 ∈ ((Base‘(2nd
‘𝑣))
↑m (Base‘(1st ‘𝑣))) ↦ (𝑔 ∘ 𝑓))) = · ) |
17 | 16 | opeq2d 4817 |
. . . 4
⊢ ((𝜑 ∧ 𝑢 = 𝑈) → 〈(comp‘ndx), (𝑣 ∈ (𝑢 × 𝑢), 𝑧 ∈ 𝑢 ↦ (𝑔 ∈ ((Base‘𝑧) ↑m
(Base‘(2nd ‘𝑣))), 𝑓 ∈ ((Base‘(2nd
‘𝑣))
↑m (Base‘(1st ‘𝑣))) ↦ (𝑔 ∘ 𝑓)))〉 = 〈(comp‘ndx), ·
〉) |
18 | 4, 10, 17 | tpeq123d 4690 |
. . 3
⊢ ((𝜑 ∧ 𝑢 = 𝑈) → {〈(Base‘ndx), 𝑢〉, 〈(Hom ‘ndx),
(𝑥 ∈ 𝑢, 𝑦 ∈ 𝑢 ↦ ((Base‘𝑦) ↑m (Base‘𝑥)))〉,
〈(comp‘ndx), (𝑣
∈ (𝑢 × 𝑢), 𝑧 ∈ 𝑢 ↦ (𝑔 ∈ ((Base‘𝑧) ↑m
(Base‘(2nd ‘𝑣))), 𝑓 ∈ ((Base‘(2nd
‘𝑣))
↑m (Base‘(1st ‘𝑣))) ↦ (𝑔 ∘ 𝑓)))〉} = {〈(Base‘ndx), 𝑈〉, 〈(Hom ‘ndx),
𝐻〉,
〈(comp‘ndx), ·
〉}) |
19 | | estrcval.u |
. . . 4
⊢ (𝜑 → 𝑈 ∈ 𝑉) |
20 | 19 | elexd 3451 |
. . 3
⊢ (𝜑 → 𝑈 ∈ V) |
21 | | tpex 7591 |
. . . 4
⊢
{〈(Base‘ndx), 𝑈〉, 〈(Hom ‘ndx), 𝐻〉, 〈(comp‘ndx),
·
〉} ∈ V |
22 | 21 | a1i 11 |
. . 3
⊢ (𝜑 → {〈(Base‘ndx),
𝑈〉, 〈(Hom
‘ndx), 𝐻〉,
〈(comp‘ndx), · 〉} ∈
V) |
23 | 2, 18, 20, 22 | fvmptd2 6880 |
. 2
⊢ (𝜑 → (ExtStrCat‘𝑈) = {〈(Base‘ndx),
𝑈〉, 〈(Hom
‘ndx), 𝐻〉,
〈(comp‘ndx), ·
〉}) |
24 | 1, 23 | eqtrid 2792 |
1
⊢ (𝜑 → 𝐶 = {〈(Base‘ndx), 𝑈〉, 〈(Hom ‘ndx),
𝐻〉,
〈(comp‘ndx), ·
〉}) |