Step | Hyp | Ref
| Expression |
1 | | rngcvalALTV.c |
. 2
⊢ 𝐶 = (RngCatALTV‘𝑈) |
2 | | df-rngcALTV 45470 |
. . . 4
⊢
RngCatALTV = (𝑢
∈ V ↦ ⦋(𝑢 ∩ Rng) / 𝑏⦌{〈(Base‘ndx), 𝑏〉, 〈(Hom ‘ndx),
(𝑥 ∈ 𝑏, 𝑦 ∈ 𝑏 ↦ (𝑥 RngHomo 𝑦))〉, 〈(comp‘ndx), (𝑣 ∈ (𝑏 × 𝑏), 𝑧 ∈ 𝑏 ↦ (𝑔 ∈ ((2nd ‘𝑣) RngHomo 𝑧), 𝑓 ∈ ((1st ‘𝑣) RngHomo (2nd
‘𝑣)) ↦ (𝑔 ∘ 𝑓)))〉}) |
3 | 2 | a1i 11 |
. . 3
⊢ (𝜑 → RngCatALTV = (𝑢 ∈ V ↦
⦋(𝑢 ∩
Rng) / 𝑏⦌{〈(Base‘ndx), 𝑏〉, 〈(Hom ‘ndx),
(𝑥 ∈ 𝑏, 𝑦 ∈ 𝑏 ↦ (𝑥 RngHomo 𝑦))〉, 〈(comp‘ndx), (𝑣 ∈ (𝑏 × 𝑏), 𝑧 ∈ 𝑏 ↦ (𝑔 ∈ ((2nd ‘𝑣) RngHomo 𝑧), 𝑓 ∈ ((1st ‘𝑣) RngHomo (2nd
‘𝑣)) ↦ (𝑔 ∘ 𝑓)))〉})) |
4 | | vex 3434 |
. . . . . 6
⊢ 𝑢 ∈ V |
5 | 4 | inex1 5244 |
. . . . 5
⊢ (𝑢 ∩ Rng) ∈
V |
6 | 5 | a1i 11 |
. . . 4
⊢ ((𝜑 ∧ 𝑢 = 𝑈) → (𝑢 ∩ Rng) ∈ V) |
7 | | ineq1 4144 |
. . . . . 6
⊢ (𝑢 = 𝑈 → (𝑢 ∩ Rng) = (𝑈 ∩ Rng)) |
8 | 7 | adantl 481 |
. . . . 5
⊢ ((𝜑 ∧ 𝑢 = 𝑈) → (𝑢 ∩ Rng) = (𝑈 ∩ Rng)) |
9 | | rngcvalALTV.b |
. . . . . 6
⊢ (𝜑 → 𝐵 = (𝑈 ∩ Rng)) |
10 | 9 | adantr 480 |
. . . . 5
⊢ ((𝜑 ∧ 𝑢 = 𝑈) → 𝐵 = (𝑈 ∩ Rng)) |
11 | 8, 10 | eqtr4d 2782 |
. . . 4
⊢ ((𝜑 ∧ 𝑢 = 𝑈) → (𝑢 ∩ Rng) = 𝐵) |
12 | | simpr 484 |
. . . . . 6
⊢ (((𝜑 ∧ 𝑢 = 𝑈) ∧ 𝑏 = 𝐵) → 𝑏 = 𝐵) |
13 | 12 | opeq2d 4816 |
. . . . 5
⊢ (((𝜑 ∧ 𝑢 = 𝑈) ∧ 𝑏 = 𝐵) → 〈(Base‘ndx), 𝑏〉 = 〈(Base‘ndx),
𝐵〉) |
14 | | eqidd 2740 |
. . . . . . . 8
⊢ (((𝜑 ∧ 𝑢 = 𝑈) ∧ 𝑏 = 𝐵) → (𝑥 RngHomo 𝑦) = (𝑥 RngHomo 𝑦)) |
15 | 12, 12, 14 | mpoeq123dv 7341 |
. . . . . . 7
⊢ (((𝜑 ∧ 𝑢 = 𝑈) ∧ 𝑏 = 𝐵) → (𝑥 ∈ 𝑏, 𝑦 ∈ 𝑏 ↦ (𝑥 RngHomo 𝑦)) = (𝑥 ∈ 𝐵, 𝑦 ∈ 𝐵 ↦ (𝑥 RngHomo 𝑦))) |
16 | | rngcvalALTV.h |
. . . . . . . 8
⊢ (𝜑 → 𝐻 = (𝑥 ∈ 𝐵, 𝑦 ∈ 𝐵 ↦ (𝑥 RngHomo 𝑦))) |
17 | 16 | ad2antrr 722 |
. . . . . . 7
⊢ (((𝜑 ∧ 𝑢 = 𝑈) ∧ 𝑏 = 𝐵) → 𝐻 = (𝑥 ∈ 𝐵, 𝑦 ∈ 𝐵 ↦ (𝑥 RngHomo 𝑦))) |
18 | 15, 17 | eqtr4d 2782 |
. . . . . 6
⊢ (((𝜑 ∧ 𝑢 = 𝑈) ∧ 𝑏 = 𝐵) → (𝑥 ∈ 𝑏, 𝑦 ∈ 𝑏 ↦ (𝑥 RngHomo 𝑦)) = 𝐻) |
19 | 18 | opeq2d 4816 |
. . . . 5
⊢ (((𝜑 ∧ 𝑢 = 𝑈) ∧ 𝑏 = 𝐵) → 〈(Hom ‘ndx), (𝑥 ∈ 𝑏, 𝑦 ∈ 𝑏 ↦ (𝑥 RngHomo 𝑦))〉 = 〈(Hom ‘ndx), 𝐻〉) |
20 | 12 | sqxpeqd 5620 |
. . . . . . . 8
⊢ (((𝜑 ∧ 𝑢 = 𝑈) ∧ 𝑏 = 𝐵) → (𝑏 × 𝑏) = (𝐵 × 𝐵)) |
21 | | eqidd 2740 |
. . . . . . . 8
⊢ (((𝜑 ∧ 𝑢 = 𝑈) ∧ 𝑏 = 𝐵) → (𝑔 ∈ ((2nd ‘𝑣) RngHomo 𝑧), 𝑓 ∈ ((1st ‘𝑣) RngHomo (2nd
‘𝑣)) ↦ (𝑔 ∘ 𝑓)) = (𝑔 ∈ ((2nd ‘𝑣) RngHomo 𝑧), 𝑓 ∈ ((1st ‘𝑣) RngHomo (2nd
‘𝑣)) ↦ (𝑔 ∘ 𝑓))) |
22 | 20, 12, 21 | mpoeq123dv 7341 |
. . . . . . 7
⊢ (((𝜑 ∧ 𝑢 = 𝑈) ∧ 𝑏 = 𝐵) → (𝑣 ∈ (𝑏 × 𝑏), 𝑧 ∈ 𝑏 ↦ (𝑔 ∈ ((2nd ‘𝑣) RngHomo 𝑧), 𝑓 ∈ ((1st ‘𝑣) RngHomo (2nd
‘𝑣)) ↦ (𝑔 ∘ 𝑓))) = (𝑣 ∈ (𝐵 × 𝐵), 𝑧 ∈ 𝐵 ↦ (𝑔 ∈ ((2nd ‘𝑣) RngHomo 𝑧), 𝑓 ∈ ((1st ‘𝑣) RngHomo (2nd
‘𝑣)) ↦ (𝑔 ∘ 𝑓)))) |
23 | | rngcvalALTV.o |
. . . . . . . 8
⊢ (𝜑 → · = (𝑣 ∈ (𝐵 × 𝐵), 𝑧 ∈ 𝐵 ↦ (𝑔 ∈ ((2nd ‘𝑣) RngHomo 𝑧), 𝑓 ∈ ((1st ‘𝑣) RngHomo (2nd
‘𝑣)) ↦ (𝑔 ∘ 𝑓)))) |
24 | 23 | ad2antrr 722 |
. . . . . . 7
⊢ (((𝜑 ∧ 𝑢 = 𝑈) ∧ 𝑏 = 𝐵) → · = (𝑣 ∈ (𝐵 × 𝐵), 𝑧 ∈ 𝐵 ↦ (𝑔 ∈ ((2nd ‘𝑣) RngHomo 𝑧), 𝑓 ∈ ((1st ‘𝑣) RngHomo (2nd
‘𝑣)) ↦ (𝑔 ∘ 𝑓)))) |
25 | 22, 24 | eqtr4d 2782 |
. . . . . 6
⊢ (((𝜑 ∧ 𝑢 = 𝑈) ∧ 𝑏 = 𝐵) → (𝑣 ∈ (𝑏 × 𝑏), 𝑧 ∈ 𝑏 ↦ (𝑔 ∈ ((2nd ‘𝑣) RngHomo 𝑧), 𝑓 ∈ ((1st ‘𝑣) RngHomo (2nd
‘𝑣)) ↦ (𝑔 ∘ 𝑓))) = · ) |
26 | 25 | opeq2d 4816 |
. . . . 5
⊢ (((𝜑 ∧ 𝑢 = 𝑈) ∧ 𝑏 = 𝐵) → 〈(comp‘ndx), (𝑣 ∈ (𝑏 × 𝑏), 𝑧 ∈ 𝑏 ↦ (𝑔 ∈ ((2nd ‘𝑣) RngHomo 𝑧), 𝑓 ∈ ((1st ‘𝑣) RngHomo (2nd
‘𝑣)) ↦ (𝑔 ∘ 𝑓)))〉 = 〈(comp‘ndx), ·
〉) |
27 | 13, 19, 26 | tpeq123d 4689 |
. . . 4
⊢ (((𝜑 ∧ 𝑢 = 𝑈) ∧ 𝑏 = 𝐵) → {〈(Base‘ndx), 𝑏〉, 〈(Hom ‘ndx),
(𝑥 ∈ 𝑏, 𝑦 ∈ 𝑏 ↦ (𝑥 RngHomo 𝑦))〉, 〈(comp‘ndx), (𝑣 ∈ (𝑏 × 𝑏), 𝑧 ∈ 𝑏 ↦ (𝑔 ∈ ((2nd ‘𝑣) RngHomo 𝑧), 𝑓 ∈ ((1st ‘𝑣) RngHomo (2nd
‘𝑣)) ↦ (𝑔 ∘ 𝑓)))〉} = {〈(Base‘ndx), 𝐵〉, 〈(Hom ‘ndx),
𝐻〉,
〈(comp‘ndx), ·
〉}) |
28 | 6, 11, 27 | csbied2 3876 |
. . 3
⊢ ((𝜑 ∧ 𝑢 = 𝑈) → ⦋(𝑢 ∩ Rng) / 𝑏⦌{〈(Base‘ndx), 𝑏〉, 〈(Hom ‘ndx),
(𝑥 ∈ 𝑏, 𝑦 ∈ 𝑏 ↦ (𝑥 RngHomo 𝑦))〉, 〈(comp‘ndx), (𝑣 ∈ (𝑏 × 𝑏), 𝑧 ∈ 𝑏 ↦ (𝑔 ∈ ((2nd ‘𝑣) RngHomo 𝑧), 𝑓 ∈ ((1st ‘𝑣) RngHomo (2nd
‘𝑣)) ↦ (𝑔 ∘ 𝑓)))〉} = {〈(Base‘ndx), 𝐵〉, 〈(Hom ‘ndx),
𝐻〉,
〈(comp‘ndx), ·
〉}) |
29 | | rngcvalALTV.u |
. . . 4
⊢ (𝜑 → 𝑈 ∈ 𝑉) |
30 | | elex 3448 |
. . . 4
⊢ (𝑈 ∈ 𝑉 → 𝑈 ∈ V) |
31 | 29, 30 | syl 17 |
. . 3
⊢ (𝜑 → 𝑈 ∈ V) |
32 | | tpex 7588 |
. . . 4
⊢
{〈(Base‘ndx), 𝐵〉, 〈(Hom ‘ndx), 𝐻〉, 〈(comp‘ndx),
·
〉} ∈ V |
33 | 32 | a1i 11 |
. . 3
⊢ (𝜑 → {〈(Base‘ndx),
𝐵〉, 〈(Hom
‘ndx), 𝐻〉,
〈(comp‘ndx), · 〉} ∈
V) |
34 | 3, 28, 31, 33 | fvmptd 6876 |
. 2
⊢ (𝜑 → (RngCatALTV‘𝑈) = {〈(Base‘ndx),
𝐵〉, 〈(Hom
‘ndx), 𝐻〉,
〈(comp‘ndx), ·
〉}) |
35 | 1, 34 | eqtrid 2791 |
1
⊢ (𝜑 → 𝐶 = {〈(Base‘ndx), 𝐵〉, 〈(Hom ‘ndx),
𝐻〉,
〈(comp‘ndx), ·
〉}) |