Step | Hyp | Ref
| Expression |
1 | | catcval.c |
. 2
⊢ 𝐶 = (CatCat‘𝑈) |
2 | | df-catc 17483 |
. . 3
⊢ CatCat =
(𝑢 ∈ V ↦
⦋(𝑢 ∩
Cat) / 𝑏⦌{〈(Base‘ndx), 𝑏〉, 〈(Hom ‘ndx),
(𝑥 ∈ 𝑏, 𝑦 ∈ 𝑏 ↦ (𝑥 Func 𝑦))〉, 〈(comp‘ndx), (𝑣 ∈ (𝑏 × 𝑏), 𝑧 ∈ 𝑏 ↦ (𝑔 ∈ ((2nd ‘𝑣) Func 𝑧), 𝑓 ∈ ( Func ‘𝑣) ↦ (𝑔 ∘func 𝑓)))〉}) |
3 | | vex 3404 |
. . . . . 6
⊢ 𝑢 ∈ V |
4 | 3 | inex1 5195 |
. . . . 5
⊢ (𝑢 ∩ Cat) ∈
V |
5 | 4 | a1i 11 |
. . . 4
⊢ ((𝜑 ∧ 𝑢 = 𝑈) → (𝑢 ∩ Cat) ∈ V) |
6 | | simpr 488 |
. . . . . 6
⊢ ((𝜑 ∧ 𝑢 = 𝑈) → 𝑢 = 𝑈) |
7 | 6 | ineq1d 4112 |
. . . . 5
⊢ ((𝜑 ∧ 𝑢 = 𝑈) → (𝑢 ∩ Cat) = (𝑈 ∩ Cat)) |
8 | | catcval.b |
. . . . . 6
⊢ (𝜑 → 𝐵 = (𝑈 ∩ Cat)) |
9 | 8 | adantr 484 |
. . . . 5
⊢ ((𝜑 ∧ 𝑢 = 𝑈) → 𝐵 = (𝑈 ∩ Cat)) |
10 | 7, 9 | eqtr4d 2777 |
. . . 4
⊢ ((𝜑 ∧ 𝑢 = 𝑈) → (𝑢 ∩ Cat) = 𝐵) |
11 | | simpr 488 |
. . . . . 6
⊢ (((𝜑 ∧ 𝑢 = 𝑈) ∧ 𝑏 = 𝐵) → 𝑏 = 𝐵) |
12 | 11 | opeq2d 4778 |
. . . . 5
⊢ (((𝜑 ∧ 𝑢 = 𝑈) ∧ 𝑏 = 𝐵) → 〈(Base‘ndx), 𝑏〉 = 〈(Base‘ndx),
𝐵〉) |
13 | | eqidd 2740 |
. . . . . . . 8
⊢ (((𝜑 ∧ 𝑢 = 𝑈) ∧ 𝑏 = 𝐵) → (𝑥 Func 𝑦) = (𝑥 Func 𝑦)) |
14 | 11, 11, 13 | mpoeq123dv 7255 |
. . . . . . 7
⊢ (((𝜑 ∧ 𝑢 = 𝑈) ∧ 𝑏 = 𝐵) → (𝑥 ∈ 𝑏, 𝑦 ∈ 𝑏 ↦ (𝑥 Func 𝑦)) = (𝑥 ∈ 𝐵, 𝑦 ∈ 𝐵 ↦ (𝑥 Func 𝑦))) |
15 | | catcval.h |
. . . . . . . 8
⊢ (𝜑 → 𝐻 = (𝑥 ∈ 𝐵, 𝑦 ∈ 𝐵 ↦ (𝑥 Func 𝑦))) |
16 | 15 | ad2antrr 726 |
. . . . . . 7
⊢ (((𝜑 ∧ 𝑢 = 𝑈) ∧ 𝑏 = 𝐵) → 𝐻 = (𝑥 ∈ 𝐵, 𝑦 ∈ 𝐵 ↦ (𝑥 Func 𝑦))) |
17 | 14, 16 | eqtr4d 2777 |
. . . . . 6
⊢ (((𝜑 ∧ 𝑢 = 𝑈) ∧ 𝑏 = 𝐵) → (𝑥 ∈ 𝑏, 𝑦 ∈ 𝑏 ↦ (𝑥 Func 𝑦)) = 𝐻) |
18 | 17 | opeq2d 4778 |
. . . . 5
⊢ (((𝜑 ∧ 𝑢 = 𝑈) ∧ 𝑏 = 𝐵) → 〈(Hom ‘ndx), (𝑥 ∈ 𝑏, 𝑦 ∈ 𝑏 ↦ (𝑥 Func 𝑦))〉 = 〈(Hom ‘ndx), 𝐻〉) |
19 | 11 | sqxpeqd 5567 |
. . . . . . . 8
⊢ (((𝜑 ∧ 𝑢 = 𝑈) ∧ 𝑏 = 𝐵) → (𝑏 × 𝑏) = (𝐵 × 𝐵)) |
20 | | eqidd 2740 |
. . . . . . . 8
⊢ (((𝜑 ∧ 𝑢 = 𝑈) ∧ 𝑏 = 𝐵) → (𝑔 ∈ ((2nd ‘𝑣) Func 𝑧), 𝑓 ∈ ( Func ‘𝑣) ↦ (𝑔 ∘func 𝑓)) = (𝑔 ∈ ((2nd ‘𝑣) Func 𝑧), 𝑓 ∈ ( Func ‘𝑣) ↦ (𝑔 ∘func 𝑓))) |
21 | 19, 11, 20 | mpoeq123dv 7255 |
. . . . . . 7
⊢ (((𝜑 ∧ 𝑢 = 𝑈) ∧ 𝑏 = 𝐵) → (𝑣 ∈ (𝑏 × 𝑏), 𝑧 ∈ 𝑏 ↦ (𝑔 ∈ ((2nd ‘𝑣) Func 𝑧), 𝑓 ∈ ( Func ‘𝑣) ↦ (𝑔 ∘func 𝑓))) = (𝑣 ∈ (𝐵 × 𝐵), 𝑧 ∈ 𝐵 ↦ (𝑔 ∈ ((2nd ‘𝑣) Func 𝑧), 𝑓 ∈ ( Func ‘𝑣) ↦ (𝑔 ∘func 𝑓)))) |
22 | | catcval.o |
. . . . . . . 8
⊢ (𝜑 → · = (𝑣 ∈ (𝐵 × 𝐵), 𝑧 ∈ 𝐵 ↦ (𝑔 ∈ ((2nd ‘𝑣) Func 𝑧), 𝑓 ∈ ( Func ‘𝑣) ↦ (𝑔 ∘func 𝑓)))) |
23 | 22 | ad2antrr 726 |
. . . . . . 7
⊢ (((𝜑 ∧ 𝑢 = 𝑈) ∧ 𝑏 = 𝐵) → · = (𝑣 ∈ (𝐵 × 𝐵), 𝑧 ∈ 𝐵 ↦ (𝑔 ∈ ((2nd ‘𝑣) Func 𝑧), 𝑓 ∈ ( Func ‘𝑣) ↦ (𝑔 ∘func 𝑓)))) |
24 | 21, 23 | eqtr4d 2777 |
. . . . . 6
⊢ (((𝜑 ∧ 𝑢 = 𝑈) ∧ 𝑏 = 𝐵) → (𝑣 ∈ (𝑏 × 𝑏), 𝑧 ∈ 𝑏 ↦ (𝑔 ∈ ((2nd ‘𝑣) Func 𝑧), 𝑓 ∈ ( Func ‘𝑣) ↦ (𝑔 ∘func 𝑓))) = · ) |
25 | 24 | opeq2d 4778 |
. . . . 5
⊢ (((𝜑 ∧ 𝑢 = 𝑈) ∧ 𝑏 = 𝐵) → 〈(comp‘ndx), (𝑣 ∈ (𝑏 × 𝑏), 𝑧 ∈ 𝑏 ↦ (𝑔 ∈ ((2nd ‘𝑣) Func 𝑧), 𝑓 ∈ ( Func ‘𝑣) ↦ (𝑔 ∘func 𝑓)))〉 =
〈(comp‘ndx), ·
〉) |
26 | 12, 18, 25 | tpeq123d 4649 |
. . . 4
⊢ (((𝜑 ∧ 𝑢 = 𝑈) ∧ 𝑏 = 𝐵) → {〈(Base‘ndx), 𝑏〉, 〈(Hom ‘ndx),
(𝑥 ∈ 𝑏, 𝑦 ∈ 𝑏 ↦ (𝑥 Func 𝑦))〉, 〈(comp‘ndx), (𝑣 ∈ (𝑏 × 𝑏), 𝑧 ∈ 𝑏 ↦ (𝑔 ∈ ((2nd ‘𝑣) Func 𝑧), 𝑓 ∈ ( Func ‘𝑣) ↦ (𝑔 ∘func 𝑓)))〉} =
{〈(Base‘ndx), 𝐵〉, 〈(Hom ‘ndx), 𝐻〉, 〈(comp‘ndx),
·
〉}) |
27 | 5, 10, 26 | csbied2 3837 |
. . 3
⊢ ((𝜑 ∧ 𝑢 = 𝑈) → ⦋(𝑢 ∩ Cat) / 𝑏⦌{〈(Base‘ndx), 𝑏〉, 〈(Hom ‘ndx),
(𝑥 ∈ 𝑏, 𝑦 ∈ 𝑏 ↦ (𝑥 Func 𝑦))〉, 〈(comp‘ndx), (𝑣 ∈ (𝑏 × 𝑏), 𝑧 ∈ 𝑏 ↦ (𝑔 ∈ ((2nd ‘𝑣) Func 𝑧), 𝑓 ∈ ( Func ‘𝑣) ↦ (𝑔 ∘func 𝑓)))〉} =
{〈(Base‘ndx), 𝐵〉, 〈(Hom ‘ndx), 𝐻〉, 〈(comp‘ndx),
·
〉}) |
28 | | catcval.u |
. . . 4
⊢ (𝜑 → 𝑈 ∈ 𝑉) |
29 | 28 | elexd 3420 |
. . 3
⊢ (𝜑 → 𝑈 ∈ V) |
30 | | tpex 7500 |
. . . 4
⊢
{〈(Base‘ndx), 𝐵〉, 〈(Hom ‘ndx), 𝐻〉, 〈(comp‘ndx),
·
〉} ∈ V |
31 | 30 | a1i 11 |
. . 3
⊢ (𝜑 → {〈(Base‘ndx),
𝐵〉, 〈(Hom
‘ndx), 𝐻〉,
〈(comp‘ndx), · 〉} ∈
V) |
32 | 2, 27, 29, 31 | fvmptd2 6795 |
. 2
⊢ (𝜑 → (CatCat‘𝑈) = {〈(Base‘ndx),
𝐵〉, 〈(Hom
‘ndx), 𝐻〉,
〈(comp‘ndx), ·
〉}) |
33 | 1, 32 | syl5eq 2786 |
1
⊢ (𝜑 → 𝐶 = {〈(Base‘ndx), 𝐵〉, 〈(Hom ‘ndx),
𝐻〉,
〈(comp‘ndx), ·
〉}) |