Step | Hyp | Ref
| Expression |
1 | | idfuval.i |
. 2
⊢ 𝐼 =
(idfunc‘𝐶) |
2 | | idfuval.c |
. . 3
⊢ (𝜑 → 𝐶 ∈ Cat) |
3 | | fvex 6113 |
. . . . . 6
⊢
(Base‘𝑐)
∈ V |
4 | 3 | a1i 11 |
. . . . 5
⊢ (𝑐 = 𝐶 → (Base‘𝑐) ∈ V) |
5 | | fveq2 6103 |
. . . . . 6
⊢ (𝑐 = 𝐶 → (Base‘𝑐) = (Base‘𝐶)) |
6 | | idfuval.b |
. . . . . 6
⊢ 𝐵 = (Base‘𝐶) |
7 | 5, 6 | syl6eqr 2662 |
. . . . 5
⊢ (𝑐 = 𝐶 → (Base‘𝑐) = 𝐵) |
8 | | simpr 476 |
. . . . . . 7
⊢ ((𝑐 = 𝐶 ∧ 𝑏 = 𝐵) → 𝑏 = 𝐵) |
9 | 8 | reseq2d 5317 |
. . . . . 6
⊢ ((𝑐 = 𝐶 ∧ 𝑏 = 𝐵) → ( I ↾ 𝑏) = ( I ↾ 𝐵)) |
10 | 8 | sqxpeqd 5065 |
. . . . . . 7
⊢ ((𝑐 = 𝐶 ∧ 𝑏 = 𝐵) → (𝑏 × 𝑏) = (𝐵 × 𝐵)) |
11 | | simpl 472 |
. . . . . . . . . . 11
⊢ ((𝑐 = 𝐶 ∧ 𝑏 = 𝐵) → 𝑐 = 𝐶) |
12 | 11 | fveq2d 6107 |
. . . . . . . . . 10
⊢ ((𝑐 = 𝐶 ∧ 𝑏 = 𝐵) → (Hom ‘𝑐) = (Hom ‘𝐶)) |
13 | | idfuval.h |
. . . . . . . . . 10
⊢ 𝐻 = (Hom ‘𝐶) |
14 | 12, 13 | syl6eqr 2662 |
. . . . . . . . 9
⊢ ((𝑐 = 𝐶 ∧ 𝑏 = 𝐵) → (Hom ‘𝑐) = 𝐻) |
15 | 14 | fveq1d 6105 |
. . . . . . . 8
⊢ ((𝑐 = 𝐶 ∧ 𝑏 = 𝐵) → ((Hom ‘𝑐)‘𝑧) = (𝐻‘𝑧)) |
16 | 15 | reseq2d 5317 |
. . . . . . 7
⊢ ((𝑐 = 𝐶 ∧ 𝑏 = 𝐵) → ( I ↾ ((Hom ‘𝑐)‘𝑧)) = ( I ↾ (𝐻‘𝑧))) |
17 | 10, 16 | mpteq12dv 4663 |
. . . . . 6
⊢ ((𝑐 = 𝐶 ∧ 𝑏 = 𝐵) → (𝑧 ∈ (𝑏 × 𝑏) ↦ ( I ↾ ((Hom ‘𝑐)‘𝑧))) = (𝑧 ∈ (𝐵 × 𝐵) ↦ ( I ↾ (𝐻‘𝑧)))) |
18 | 9, 17 | opeq12d 4348 |
. . . . 5
⊢ ((𝑐 = 𝐶 ∧ 𝑏 = 𝐵) → 〈( I ↾ 𝑏), (𝑧 ∈ (𝑏 × 𝑏) ↦ ( I ↾ ((Hom ‘𝑐)‘𝑧)))〉 = 〈( I ↾ 𝐵), (𝑧 ∈ (𝐵 × 𝐵) ↦ ( I ↾ (𝐻‘𝑧)))〉) |
19 | 4, 7, 18 | csbied2 3527 |
. . . 4
⊢ (𝑐 = 𝐶 → ⦋(Base‘𝑐) / 𝑏⦌〈( I ↾ 𝑏), (𝑧 ∈ (𝑏 × 𝑏) ↦ ( I ↾ ((Hom ‘𝑐)‘𝑧)))〉 = 〈( I ↾ 𝐵), (𝑧 ∈ (𝐵 × 𝐵) ↦ ( I ↾ (𝐻‘𝑧)))〉) |
20 | | df-idfu 16342 |
. . . 4
⊢
idfunc = (𝑐 ∈ Cat ↦
⦋(Base‘𝑐) / 𝑏⦌〈( I ↾ 𝑏), (𝑧 ∈ (𝑏 × 𝑏) ↦ ( I ↾ ((Hom ‘𝑐)‘𝑧)))〉) |
21 | | opex 4859 |
. . . 4
⊢ 〈( I
↾ 𝐵), (𝑧 ∈ (𝐵 × 𝐵) ↦ ( I ↾ (𝐻‘𝑧)))〉 ∈ V |
22 | 19, 20, 21 | fvmpt 6191 |
. . 3
⊢ (𝐶 ∈ Cat →
(idfunc‘𝐶) = 〈( I ↾ 𝐵), (𝑧 ∈ (𝐵 × 𝐵) ↦ ( I ↾ (𝐻‘𝑧)))〉) |
23 | 2, 22 | syl 17 |
. 2
⊢ (𝜑 →
(idfunc‘𝐶) = 〈( I ↾ 𝐵), (𝑧 ∈ (𝐵 × 𝐵) ↦ ( I ↾ (𝐻‘𝑧)))〉) |
24 | 1, 23 | syl5eq 2656 |
1
⊢ (𝜑 → 𝐼 = 〈( I ↾ 𝐵), (𝑧 ∈ (𝐵 × 𝐵) ↦ ( I ↾ (𝐻‘𝑧)))〉) |