| Step | Hyp | Ref
| Expression |
| 1 | | catcval.c |
. 2
⊢ 𝐶 = (CatCat‘𝑈) |
| 2 | | df-catc 18144 |
. . 3
⊢ CatCat =
(𝑢 ∈ V ↦
⦋(𝑢 ∩
Cat) / 𝑏⦌{〈(Base‘ndx), 𝑏〉, 〈(Hom ‘ndx),
(𝑥 ∈ 𝑏, 𝑦 ∈ 𝑏 ↦ (𝑥 Func 𝑦))〉, 〈(comp‘ndx), (𝑣 ∈ (𝑏 × 𝑏), 𝑧 ∈ 𝑏 ↦ (𝑔 ∈ ((2nd ‘𝑣) Func 𝑧), 𝑓 ∈ ( Func ‘𝑣) ↦ (𝑔 ∘func 𝑓)))〉}) |
| 3 | | vex 3484 |
. . . . . 6
⊢ 𝑢 ∈ V |
| 4 | 3 | inex1 5317 |
. . . . 5
⊢ (𝑢 ∩ Cat) ∈
V |
| 5 | 4 | a1i 11 |
. . . 4
⊢ ((𝜑 ∧ 𝑢 = 𝑈) → (𝑢 ∩ Cat) ∈ V) |
| 6 | | simpr 484 |
. . . . . 6
⊢ ((𝜑 ∧ 𝑢 = 𝑈) → 𝑢 = 𝑈) |
| 7 | 6 | ineq1d 4219 |
. . . . 5
⊢ ((𝜑 ∧ 𝑢 = 𝑈) → (𝑢 ∩ Cat) = (𝑈 ∩ Cat)) |
| 8 | | catcval.b |
. . . . . 6
⊢ (𝜑 → 𝐵 = (𝑈 ∩ Cat)) |
| 9 | 8 | adantr 480 |
. . . . 5
⊢ ((𝜑 ∧ 𝑢 = 𝑈) → 𝐵 = (𝑈 ∩ Cat)) |
| 10 | 7, 9 | eqtr4d 2780 |
. . . 4
⊢ ((𝜑 ∧ 𝑢 = 𝑈) → (𝑢 ∩ Cat) = 𝐵) |
| 11 | | simpr 484 |
. . . . . 6
⊢ (((𝜑 ∧ 𝑢 = 𝑈) ∧ 𝑏 = 𝐵) → 𝑏 = 𝐵) |
| 12 | 11 | opeq2d 4880 |
. . . . 5
⊢ (((𝜑 ∧ 𝑢 = 𝑈) ∧ 𝑏 = 𝐵) → 〈(Base‘ndx), 𝑏〉 = 〈(Base‘ndx),
𝐵〉) |
| 13 | | eqidd 2738 |
. . . . . . . 8
⊢ (((𝜑 ∧ 𝑢 = 𝑈) ∧ 𝑏 = 𝐵) → (𝑥 Func 𝑦) = (𝑥 Func 𝑦)) |
| 14 | 11, 11, 13 | mpoeq123dv 7508 |
. . . . . . 7
⊢ (((𝜑 ∧ 𝑢 = 𝑈) ∧ 𝑏 = 𝐵) → (𝑥 ∈ 𝑏, 𝑦 ∈ 𝑏 ↦ (𝑥 Func 𝑦)) = (𝑥 ∈ 𝐵, 𝑦 ∈ 𝐵 ↦ (𝑥 Func 𝑦))) |
| 15 | | catcval.h |
. . . . . . . 8
⊢ (𝜑 → 𝐻 = (𝑥 ∈ 𝐵, 𝑦 ∈ 𝐵 ↦ (𝑥 Func 𝑦))) |
| 16 | 15 | ad2antrr 726 |
. . . . . . 7
⊢ (((𝜑 ∧ 𝑢 = 𝑈) ∧ 𝑏 = 𝐵) → 𝐻 = (𝑥 ∈ 𝐵, 𝑦 ∈ 𝐵 ↦ (𝑥 Func 𝑦))) |
| 17 | 14, 16 | eqtr4d 2780 |
. . . . . 6
⊢ (((𝜑 ∧ 𝑢 = 𝑈) ∧ 𝑏 = 𝐵) → (𝑥 ∈ 𝑏, 𝑦 ∈ 𝑏 ↦ (𝑥 Func 𝑦)) = 𝐻) |
| 18 | 17 | opeq2d 4880 |
. . . . 5
⊢ (((𝜑 ∧ 𝑢 = 𝑈) ∧ 𝑏 = 𝐵) → 〈(Hom ‘ndx), (𝑥 ∈ 𝑏, 𝑦 ∈ 𝑏 ↦ (𝑥 Func 𝑦))〉 = 〈(Hom ‘ndx), 𝐻〉) |
| 19 | 11 | sqxpeqd 5717 |
. . . . . . . 8
⊢ (((𝜑 ∧ 𝑢 = 𝑈) ∧ 𝑏 = 𝐵) → (𝑏 × 𝑏) = (𝐵 × 𝐵)) |
| 20 | | eqidd 2738 |
. . . . . . . 8
⊢ (((𝜑 ∧ 𝑢 = 𝑈) ∧ 𝑏 = 𝐵) → (𝑔 ∈ ((2nd ‘𝑣) Func 𝑧), 𝑓 ∈ ( Func ‘𝑣) ↦ (𝑔 ∘func 𝑓)) = (𝑔 ∈ ((2nd ‘𝑣) Func 𝑧), 𝑓 ∈ ( Func ‘𝑣) ↦ (𝑔 ∘func 𝑓))) |
| 21 | 19, 11, 20 | mpoeq123dv 7508 |
. . . . . . 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 2780 |
. . . . . 6
⊢ (((𝜑 ∧ 𝑢 = 𝑈) ∧ 𝑏 = 𝐵) → (𝑣 ∈ (𝑏 × 𝑏), 𝑧 ∈ 𝑏 ↦ (𝑔 ∈ ((2nd ‘𝑣) Func 𝑧), 𝑓 ∈ ( Func ‘𝑣) ↦ (𝑔 ∘func 𝑓))) = · ) |
| 25 | 24 | opeq2d 4880 |
. . . . 5
⊢ (((𝜑 ∧ 𝑢 = 𝑈) ∧ 𝑏 = 𝐵) → 〈(comp‘ndx), (𝑣 ∈ (𝑏 × 𝑏), 𝑧 ∈ 𝑏 ↦ (𝑔 ∈ ((2nd ‘𝑣) Func 𝑧), 𝑓 ∈ ( Func ‘𝑣) ↦ (𝑔 ∘func 𝑓)))〉 =
〈(comp‘ndx), ·
〉) |
| 26 | 12, 18, 25 | tpeq123d 4748 |
. . . 4
⊢ (((𝜑 ∧ 𝑢 = 𝑈) ∧ 𝑏 = 𝐵) → {〈(Base‘ndx), 𝑏〉, 〈(Hom ‘ndx),
(𝑥 ∈ 𝑏, 𝑦 ∈ 𝑏 ↦ (𝑥 Func 𝑦))〉, 〈(comp‘ndx), (𝑣 ∈ (𝑏 × 𝑏), 𝑧 ∈ 𝑏 ↦ (𝑔 ∈ ((2nd ‘𝑣) Func 𝑧), 𝑓 ∈ ( Func ‘𝑣) ↦ (𝑔 ∘func 𝑓)))〉} =
{〈(Base‘ndx), 𝐵〉, 〈(Hom ‘ndx), 𝐻〉, 〈(comp‘ndx),
·
〉}) |
| 27 | 5, 10, 26 | csbied2 3936 |
. . 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 3504 |
. . 3
⊢ (𝜑 → 𝑈 ∈ V) |
| 30 | | tpex 7766 |
. . . 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 7024 |
. 2
⊢ (𝜑 → (CatCat‘𝑈) = {〈(Base‘ndx),
𝐵〉, 〈(Hom
‘ndx), 𝐻〉,
〈(comp‘ndx), ·
〉}) |
| 33 | 1, 32 | eqtrid 2789 |
1
⊢ (𝜑 → 𝐶 = {〈(Base‘ndx), 𝐵〉, 〈(Hom ‘ndx),
𝐻〉,
〈(comp‘ndx), ·
〉}) |