Step | Hyp | Ref
| Expression |
1 | | bj-endval.c |
. . . 4
⊢ (𝜑 → 𝐶 ∈ Cat) |
2 | | bj-endval.x |
. . . 4
⊢ (𝜑 → 𝑋 ∈ (Base‘𝐶)) |
3 | 1, 2 | bj-endbase 35170 |
. . 3
⊢ (𝜑 → (Base‘((End
‘𝐶)‘𝑋)) = (𝑋(Hom ‘𝐶)𝑋)) |
4 | 3 | eqcomd 2742 |
. 2
⊢ (𝜑 → (𝑋(Hom ‘𝐶)𝑋) = (Base‘((End ‘𝐶)‘𝑋))) |
5 | 1, 2 | bj-endcomp 35171 |
. . 3
⊢ (𝜑 → (+g‘((End
‘𝐶)‘𝑋)) = (〈𝑋, 𝑋〉(comp‘𝐶)𝑋)) |
6 | 5 | eqcomd 2742 |
. 2
⊢ (𝜑 → (〈𝑋, 𝑋〉(comp‘𝐶)𝑋) = (+g‘((End ‘𝐶)‘𝑋))) |
7 | | eqid 2736 |
. . 3
⊢
(Base‘𝐶) =
(Base‘𝐶) |
8 | | eqid 2736 |
. . 3
⊢ (Hom
‘𝐶) = (Hom
‘𝐶) |
9 | | eqid 2736 |
. . 3
⊢
(comp‘𝐶) =
(comp‘𝐶) |
10 | 1 | 3ad2ant1 1135 |
. . 3
⊢ ((𝜑 ∧ 𝑥 ∈ (𝑋(Hom ‘𝐶)𝑋) ∧ 𝑦 ∈ (𝑋(Hom ‘𝐶)𝑋)) → 𝐶 ∈ Cat) |
11 | 2 | 3ad2ant1 1135 |
. . 3
⊢ ((𝜑 ∧ 𝑥 ∈ (𝑋(Hom ‘𝐶)𝑋) ∧ 𝑦 ∈ (𝑋(Hom ‘𝐶)𝑋)) → 𝑋 ∈ (Base‘𝐶)) |
12 | | simp3 1140 |
. . 3
⊢ ((𝜑 ∧ 𝑥 ∈ (𝑋(Hom ‘𝐶)𝑋) ∧ 𝑦 ∈ (𝑋(Hom ‘𝐶)𝑋)) → 𝑦 ∈ (𝑋(Hom ‘𝐶)𝑋)) |
13 | | simp2 1139 |
. . 3
⊢ ((𝜑 ∧ 𝑥 ∈ (𝑋(Hom ‘𝐶)𝑋) ∧ 𝑦 ∈ (𝑋(Hom ‘𝐶)𝑋)) → 𝑥 ∈ (𝑋(Hom ‘𝐶)𝑋)) |
14 | 7, 8, 9, 10, 11, 11, 11, 12, 13 | catcocl 17142 |
. 2
⊢ ((𝜑 ∧ 𝑥 ∈ (𝑋(Hom ‘𝐶)𝑋) ∧ 𝑦 ∈ (𝑋(Hom ‘𝐶)𝑋)) → (𝑥(〈𝑋, 𝑋〉(comp‘𝐶)𝑋)𝑦) ∈ (𝑋(Hom ‘𝐶)𝑋)) |
15 | 1 | adantr 484 |
. . 3
⊢ ((𝜑 ∧ (𝑥 ∈ (𝑋(Hom ‘𝐶)𝑋) ∧ 𝑦 ∈ (𝑋(Hom ‘𝐶)𝑋) ∧ 𝑧 ∈ (𝑋(Hom ‘𝐶)𝑋))) → 𝐶 ∈ Cat) |
16 | 2 | adantr 484 |
. . 3
⊢ ((𝜑 ∧ (𝑥 ∈ (𝑋(Hom ‘𝐶)𝑋) ∧ 𝑦 ∈ (𝑋(Hom ‘𝐶)𝑋) ∧ 𝑧 ∈ (𝑋(Hom ‘𝐶)𝑋))) → 𝑋 ∈ (Base‘𝐶)) |
17 | | simpr 488 |
. . . 4
⊢ ((𝜑 ∧ (𝑥 ∈ (𝑋(Hom ‘𝐶)𝑋) ∧ 𝑦 ∈ (𝑋(Hom ‘𝐶)𝑋) ∧ 𝑧 ∈ (𝑋(Hom ‘𝐶)𝑋))) → (𝑥 ∈ (𝑋(Hom ‘𝐶)𝑋) ∧ 𝑦 ∈ (𝑋(Hom ‘𝐶)𝑋) ∧ 𝑧 ∈ (𝑋(Hom ‘𝐶)𝑋))) |
18 | | simp3 1140 |
. . . 4
⊢ ((𝑥 ∈ (𝑋(Hom ‘𝐶)𝑋) ∧ 𝑦 ∈ (𝑋(Hom ‘𝐶)𝑋) ∧ 𝑧 ∈ (𝑋(Hom ‘𝐶)𝑋)) → 𝑧 ∈ (𝑋(Hom ‘𝐶)𝑋)) |
19 | 17, 18 | syl 17 |
. . 3
⊢ ((𝜑 ∧ (𝑥 ∈ (𝑋(Hom ‘𝐶)𝑋) ∧ 𝑦 ∈ (𝑋(Hom ‘𝐶)𝑋) ∧ 𝑧 ∈ (𝑋(Hom ‘𝐶)𝑋))) → 𝑧 ∈ (𝑋(Hom ‘𝐶)𝑋)) |
20 | | simp2 1139 |
. . . 4
⊢ ((𝑥 ∈ (𝑋(Hom ‘𝐶)𝑋) ∧ 𝑦 ∈ (𝑋(Hom ‘𝐶)𝑋) ∧ 𝑧 ∈ (𝑋(Hom ‘𝐶)𝑋)) → 𝑦 ∈ (𝑋(Hom ‘𝐶)𝑋)) |
21 | 17, 20 | syl 17 |
. . 3
⊢ ((𝜑 ∧ (𝑥 ∈ (𝑋(Hom ‘𝐶)𝑋) ∧ 𝑦 ∈ (𝑋(Hom ‘𝐶)𝑋) ∧ 𝑧 ∈ (𝑋(Hom ‘𝐶)𝑋))) → 𝑦 ∈ (𝑋(Hom ‘𝐶)𝑋)) |
22 | | simp1 1138 |
. . . 4
⊢ ((𝑥 ∈ (𝑋(Hom ‘𝐶)𝑋) ∧ 𝑦 ∈ (𝑋(Hom ‘𝐶)𝑋) ∧ 𝑧 ∈ (𝑋(Hom ‘𝐶)𝑋)) → 𝑥 ∈ (𝑋(Hom ‘𝐶)𝑋)) |
23 | 17, 22 | syl 17 |
. . 3
⊢ ((𝜑 ∧ (𝑥 ∈ (𝑋(Hom ‘𝐶)𝑋) ∧ 𝑦 ∈ (𝑋(Hom ‘𝐶)𝑋) ∧ 𝑧 ∈ (𝑋(Hom ‘𝐶)𝑋))) → 𝑥 ∈ (𝑋(Hom ‘𝐶)𝑋)) |
24 | 7, 8, 9, 15, 16, 16, 16, 19, 21, 16, 23 | catass 17143 |
. 2
⊢ ((𝜑 ∧ (𝑥 ∈ (𝑋(Hom ‘𝐶)𝑋) ∧ 𝑦 ∈ (𝑋(Hom ‘𝐶)𝑋) ∧ 𝑧 ∈ (𝑋(Hom ‘𝐶)𝑋))) → ((𝑥(〈𝑋, 𝑋〉(comp‘𝐶)𝑋)𝑦)(〈𝑋, 𝑋〉(comp‘𝐶)𝑋)𝑧) = (𝑥(〈𝑋, 𝑋〉(comp‘𝐶)𝑋)(𝑦(〈𝑋, 𝑋〉(comp‘𝐶)𝑋)𝑧))) |
25 | | eqid 2736 |
. . 3
⊢
(Id‘𝐶) =
(Id‘𝐶) |
26 | 7, 8, 25, 1, 2 | catidcl 17139 |
. 2
⊢ (𝜑 → ((Id‘𝐶)‘𝑋) ∈ (𝑋(Hom ‘𝐶)𝑋)) |
27 | 1 | adantr 484 |
. . 3
⊢ ((𝜑 ∧ 𝑥 ∈ (𝑋(Hom ‘𝐶)𝑋)) → 𝐶 ∈ Cat) |
28 | 2 | adantr 484 |
. . 3
⊢ ((𝜑 ∧ 𝑥 ∈ (𝑋(Hom ‘𝐶)𝑋)) → 𝑋 ∈ (Base‘𝐶)) |
29 | | simpr 488 |
. . 3
⊢ ((𝜑 ∧ 𝑥 ∈ (𝑋(Hom ‘𝐶)𝑋)) → 𝑥 ∈ (𝑋(Hom ‘𝐶)𝑋)) |
30 | 7, 8, 25, 27, 28, 9, 28, 29 | catlid 17140 |
. 2
⊢ ((𝜑 ∧ 𝑥 ∈ (𝑋(Hom ‘𝐶)𝑋)) → (((Id‘𝐶)‘𝑋)(〈𝑋, 𝑋〉(comp‘𝐶)𝑋)𝑥) = 𝑥) |
31 | 7, 8, 25, 27, 28, 9, 28, 29 | catrid 17141 |
. 2
⊢ ((𝜑 ∧ 𝑥 ∈ (𝑋(Hom ‘𝐶)𝑋)) → (𝑥(〈𝑋, 𝑋〉(comp‘𝐶)𝑋)((Id‘𝐶)‘𝑋)) = 𝑥) |
32 | 4, 6, 14, 24, 26, 30, 31 | ismndd 18149 |
1
⊢ (𝜑 → ((End ‘𝐶)‘𝑋) ∈ Mnd) |