Step | Hyp | Ref
| Expression |
1 | | ismon.s |
. 2
⊢ 𝑀 = (Mono‘𝐶) |
2 | | ismon.c |
. . 3
⊢ (𝜑 → 𝐶 ∈ Cat) |
3 | | fvex 6113 |
. . . . . 6
⊢
(Base‘𝑐)
∈ V |
4 | 3 | a1i 11 |
. . . . 5
⊢ (𝑐 = 𝐶 → (Base‘𝑐) ∈ V) |
5 | | fveq2 6103 |
. . . . . 6
⊢ (𝑐 = 𝐶 → (Base‘𝑐) = (Base‘𝐶)) |
6 | | ismon.b |
. . . . . 6
⊢ 𝐵 = (Base‘𝐶) |
7 | 5, 6 | syl6eqr 2662 |
. . . . 5
⊢ (𝑐 = 𝐶 → (Base‘𝑐) = 𝐵) |
8 | | fvex 6113 |
. . . . . . 7
⊢ (Hom
‘𝑐) ∈
V |
9 | 8 | a1i 11 |
. . . . . 6
⊢ ((𝑐 = 𝐶 ∧ 𝑏 = 𝐵) → (Hom ‘𝑐) ∈ V) |
10 | | simpl 472 |
. . . . . . . 8
⊢ ((𝑐 = 𝐶 ∧ 𝑏 = 𝐵) → 𝑐 = 𝐶) |
11 | 10 | fveq2d 6107 |
. . . . . . 7
⊢ ((𝑐 = 𝐶 ∧ 𝑏 = 𝐵) → (Hom ‘𝑐) = (Hom ‘𝐶)) |
12 | | ismon.h |
. . . . . . 7
⊢ 𝐻 = (Hom ‘𝐶) |
13 | 11, 12 | syl6eqr 2662 |
. . . . . 6
⊢ ((𝑐 = 𝐶 ∧ 𝑏 = 𝐵) → (Hom ‘𝑐) = 𝐻) |
14 | | simplr 788 |
. . . . . . 7
⊢ (((𝑐 = 𝐶 ∧ 𝑏 = 𝐵) ∧ ℎ = 𝐻) → 𝑏 = 𝐵) |
15 | | simpr 476 |
. . . . . . . . 9
⊢ (((𝑐 = 𝐶 ∧ 𝑏 = 𝐵) ∧ ℎ = 𝐻) → ℎ = 𝐻) |
16 | 15 | oveqd 6566 |
. . . . . . . 8
⊢ (((𝑐 = 𝐶 ∧ 𝑏 = 𝐵) ∧ ℎ = 𝐻) → (𝑥ℎ𝑦) = (𝑥𝐻𝑦)) |
17 | 15 | oveqd 6566 |
. . . . . . . . . . . 12
⊢ (((𝑐 = 𝐶 ∧ 𝑏 = 𝐵) ∧ ℎ = 𝐻) → (𝑧ℎ𝑥) = (𝑧𝐻𝑥)) |
18 | | simpll 786 |
. . . . . . . . . . . . . . . 16
⊢ (((𝑐 = 𝐶 ∧ 𝑏 = 𝐵) ∧ ℎ = 𝐻) → 𝑐 = 𝐶) |
19 | 18 | fveq2d 6107 |
. . . . . . . . . . . . . . 15
⊢ (((𝑐 = 𝐶 ∧ 𝑏 = 𝐵) ∧ ℎ = 𝐻) → (comp‘𝑐) = (comp‘𝐶)) |
20 | | ismon.o |
. . . . . . . . . . . . . . 15
⊢ · =
(comp‘𝐶) |
21 | 19, 20 | syl6eqr 2662 |
. . . . . . . . . . . . . 14
⊢ (((𝑐 = 𝐶 ∧ 𝑏 = 𝐵) ∧ ℎ = 𝐻) → (comp‘𝑐) = · ) |
22 | 21 | oveqd 6566 |
. . . . . . . . . . . . 13
⊢ (((𝑐 = 𝐶 ∧ 𝑏 = 𝐵) ∧ ℎ = 𝐻) → (〈𝑧, 𝑥〉(comp‘𝑐)𝑦) = (〈𝑧, 𝑥〉 · 𝑦)) |
23 | 22 | oveqd 6566 |
. . . . . . . . . . . 12
⊢ (((𝑐 = 𝐶 ∧ 𝑏 = 𝐵) ∧ ℎ = 𝐻) → (𝑓(〈𝑧, 𝑥〉(comp‘𝑐)𝑦)𝑔) = (𝑓(〈𝑧, 𝑥〉 · 𝑦)𝑔)) |
24 | 17, 23 | mpteq12dv 4663 |
. . . . . . . . . . 11
⊢ (((𝑐 = 𝐶 ∧ 𝑏 = 𝐵) ∧ ℎ = 𝐻) → (𝑔 ∈ (𝑧ℎ𝑥) ↦ (𝑓(〈𝑧, 𝑥〉(comp‘𝑐)𝑦)𝑔)) = (𝑔 ∈ (𝑧𝐻𝑥) ↦ (𝑓(〈𝑧, 𝑥〉 · 𝑦)𝑔))) |
25 | 24 | cnveqd 5220 |
. . . . . . . . . 10
⊢ (((𝑐 = 𝐶 ∧ 𝑏 = 𝐵) ∧ ℎ = 𝐻) → ◡(𝑔 ∈ (𝑧ℎ𝑥) ↦ (𝑓(〈𝑧, 𝑥〉(comp‘𝑐)𝑦)𝑔)) = ◡(𝑔 ∈ (𝑧𝐻𝑥) ↦ (𝑓(〈𝑧, 𝑥〉 · 𝑦)𝑔))) |
26 | 25 | funeqd 5825 |
. . . . . . . . 9
⊢ (((𝑐 = 𝐶 ∧ 𝑏 = 𝐵) ∧ ℎ = 𝐻) → (Fun ◡(𝑔 ∈ (𝑧ℎ𝑥) ↦ (𝑓(〈𝑧, 𝑥〉(comp‘𝑐)𝑦)𝑔)) ↔ Fun ◡(𝑔 ∈ (𝑧𝐻𝑥) ↦ (𝑓(〈𝑧, 𝑥〉 · 𝑦)𝑔)))) |
27 | 14, 26 | raleqbidv 3129 |
. . . . . . . 8
⊢ (((𝑐 = 𝐶 ∧ 𝑏 = 𝐵) ∧ ℎ = 𝐻) → (∀𝑧 ∈ 𝑏 Fun ◡(𝑔 ∈ (𝑧ℎ𝑥) ↦ (𝑓(〈𝑧, 𝑥〉(comp‘𝑐)𝑦)𝑔)) ↔ ∀𝑧 ∈ 𝐵 Fun ◡(𝑔 ∈ (𝑧𝐻𝑥) ↦ (𝑓(〈𝑧, 𝑥〉 · 𝑦)𝑔)))) |
28 | 16, 27 | rabeqbidv 3168 |
. . . . . . 7
⊢ (((𝑐 = 𝐶 ∧ 𝑏 = 𝐵) ∧ ℎ = 𝐻) → {𝑓 ∈ (𝑥ℎ𝑦) ∣ ∀𝑧 ∈ 𝑏 Fun ◡(𝑔 ∈ (𝑧ℎ𝑥) ↦ (𝑓(〈𝑧, 𝑥〉(comp‘𝑐)𝑦)𝑔))} = {𝑓 ∈ (𝑥𝐻𝑦) ∣ ∀𝑧 ∈ 𝐵 Fun ◡(𝑔 ∈ (𝑧𝐻𝑥) ↦ (𝑓(〈𝑧, 𝑥〉 · 𝑦)𝑔))}) |
29 | 14, 14, 28 | mpt2eq123dv 6615 |
. . . . . 6
⊢ (((𝑐 = 𝐶 ∧ 𝑏 = 𝐵) ∧ ℎ = 𝐻) → (𝑥 ∈ 𝑏, 𝑦 ∈ 𝑏 ↦ {𝑓 ∈ (𝑥ℎ𝑦) ∣ ∀𝑧 ∈ 𝑏 Fun ◡(𝑔 ∈ (𝑧ℎ𝑥) ↦ (𝑓(〈𝑧, 𝑥〉(comp‘𝑐)𝑦)𝑔))}) = (𝑥 ∈ 𝐵, 𝑦 ∈ 𝐵 ↦ {𝑓 ∈ (𝑥𝐻𝑦) ∣ ∀𝑧 ∈ 𝐵 Fun ◡(𝑔 ∈ (𝑧𝐻𝑥) ↦ (𝑓(〈𝑧, 𝑥〉 · 𝑦)𝑔))})) |
30 | 9, 13, 29 | csbied2 3527 |
. . . . 5
⊢ ((𝑐 = 𝐶 ∧ 𝑏 = 𝐵) → ⦋(Hom ‘𝑐) / ℎ⦌(𝑥 ∈ 𝑏, 𝑦 ∈ 𝑏 ↦ {𝑓 ∈ (𝑥ℎ𝑦) ∣ ∀𝑧 ∈ 𝑏 Fun ◡(𝑔 ∈ (𝑧ℎ𝑥) ↦ (𝑓(〈𝑧, 𝑥〉(comp‘𝑐)𝑦)𝑔))}) = (𝑥 ∈ 𝐵, 𝑦 ∈ 𝐵 ↦ {𝑓 ∈ (𝑥𝐻𝑦) ∣ ∀𝑧 ∈ 𝐵 Fun ◡(𝑔 ∈ (𝑧𝐻𝑥) ↦ (𝑓(〈𝑧, 𝑥〉 · 𝑦)𝑔))})) |
31 | 4, 7, 30 | csbied2 3527 |
. . . 4
⊢ (𝑐 = 𝐶 → ⦋(Base‘𝑐) / 𝑏⦌⦋(Hom
‘𝑐) / ℎ⦌(𝑥 ∈ 𝑏, 𝑦 ∈ 𝑏 ↦ {𝑓 ∈ (𝑥ℎ𝑦) ∣ ∀𝑧 ∈ 𝑏 Fun ◡(𝑔 ∈ (𝑧ℎ𝑥) ↦ (𝑓(〈𝑧, 𝑥〉(comp‘𝑐)𝑦)𝑔))}) = (𝑥 ∈ 𝐵, 𝑦 ∈ 𝐵 ↦ {𝑓 ∈ (𝑥𝐻𝑦) ∣ ∀𝑧 ∈ 𝐵 Fun ◡(𝑔 ∈ (𝑧𝐻𝑥) ↦ (𝑓(〈𝑧, 𝑥〉 · 𝑦)𝑔))})) |
32 | | df-mon 16213 |
. . . 4
⊢ Mono =
(𝑐 ∈ Cat ↦
⦋(Base‘𝑐) / 𝑏⦌⦋(Hom
‘𝑐) / ℎ⦌(𝑥 ∈ 𝑏, 𝑦 ∈ 𝑏 ↦ {𝑓 ∈ (𝑥ℎ𝑦) ∣ ∀𝑧 ∈ 𝑏 Fun ◡(𝑔 ∈ (𝑧ℎ𝑥) ↦ (𝑓(〈𝑧, 𝑥〉(comp‘𝑐)𝑦)𝑔))})) |
33 | | fvex 6113 |
. . . . . 6
⊢
(Base‘𝐶)
∈ V |
34 | 6, 33 | eqeltri 2684 |
. . . . 5
⊢ 𝐵 ∈ V |
35 | 34, 34 | mpt2ex 7136 |
. . . 4
⊢ (𝑥 ∈ 𝐵, 𝑦 ∈ 𝐵 ↦ {𝑓 ∈ (𝑥𝐻𝑦) ∣ ∀𝑧 ∈ 𝐵 Fun ◡(𝑔 ∈ (𝑧𝐻𝑥) ↦ (𝑓(〈𝑧, 𝑥〉 · 𝑦)𝑔))}) ∈ V |
36 | 31, 32, 35 | fvmpt 6191 |
. . 3
⊢ (𝐶 ∈ Cat →
(Mono‘𝐶) = (𝑥 ∈ 𝐵, 𝑦 ∈ 𝐵 ↦ {𝑓 ∈ (𝑥𝐻𝑦) ∣ ∀𝑧 ∈ 𝐵 Fun ◡(𝑔 ∈ (𝑧𝐻𝑥) ↦ (𝑓(〈𝑧, 𝑥〉 · 𝑦)𝑔))})) |
37 | 2, 36 | syl 17 |
. 2
⊢ (𝜑 → (Mono‘𝐶) = (𝑥 ∈ 𝐵, 𝑦 ∈ 𝐵 ↦ {𝑓 ∈ (𝑥𝐻𝑦) ∣ ∀𝑧 ∈ 𝐵 Fun ◡(𝑔 ∈ (𝑧𝐻𝑥) ↦ (𝑓(〈𝑧, 𝑥〉 · 𝑦)𝑔))})) |
38 | 1, 37 | syl5eq 2656 |
1
⊢ (𝜑 → 𝑀 = (𝑥 ∈ 𝐵, 𝑦 ∈ 𝐵 ↦ {𝑓 ∈ (𝑥𝐻𝑦) ∣ ∀𝑧 ∈ 𝐵 Fun ◡(𝑔 ∈ (𝑧𝐻𝑥) ↦ (𝑓(〈𝑧, 𝑥〉 · 𝑦)𝑔))})) |