| Step | Hyp | Ref
| Expression |
| 1 | | ismon.b |
. . . . 5
⊢ 𝐵 = (Base‘𝐶) |
| 2 | | ismon.h |
. . . . 5
⊢ 𝐻 = (Hom ‘𝐶) |
| 3 | | ismon.o |
. . . . 5
⊢ · =
(comp‘𝐶) |
| 4 | | ismon.s |
. . . . 5
⊢ 𝑀 = (Mono‘𝐶) |
| 5 | | ismon.c |
. . . . 5
⊢ (𝜑 → 𝐶 ∈ Cat) |
| 6 | 1, 2, 3, 4, 5 | monfval 17776 |
. . . 4
⊢ (𝜑 → 𝑀 = (𝑥 ∈ 𝐵, 𝑦 ∈ 𝐵 ↦ {𝑓 ∈ (𝑥𝐻𝑦) ∣ ∀𝑧 ∈ 𝐵 Fun ◡(𝑔 ∈ (𝑧𝐻𝑥) ↦ (𝑓(〈𝑧, 𝑥〉 · 𝑦)𝑔))})) |
| 7 | | simprl 771 |
. . . . . 6
⊢ ((𝜑 ∧ (𝑥 = 𝑋 ∧ 𝑦 = 𝑌)) → 𝑥 = 𝑋) |
| 8 | | simprr 773 |
. . . . . 6
⊢ ((𝜑 ∧ (𝑥 = 𝑋 ∧ 𝑦 = 𝑌)) → 𝑦 = 𝑌) |
| 9 | 7, 8 | oveq12d 7449 |
. . . . 5
⊢ ((𝜑 ∧ (𝑥 = 𝑋 ∧ 𝑦 = 𝑌)) → (𝑥𝐻𝑦) = (𝑋𝐻𝑌)) |
| 10 | 7 | oveq2d 7447 |
. . . . . . . . 9
⊢ ((𝜑 ∧ (𝑥 = 𝑋 ∧ 𝑦 = 𝑌)) → (𝑧𝐻𝑥) = (𝑧𝐻𝑋)) |
| 11 | 7 | opeq2d 4880 |
. . . . . . . . . . 11
⊢ ((𝜑 ∧ (𝑥 = 𝑋 ∧ 𝑦 = 𝑌)) → 〈𝑧, 𝑥〉 = 〈𝑧, 𝑋〉) |
| 12 | 11, 8 | oveq12d 7449 |
. . . . . . . . . 10
⊢ ((𝜑 ∧ (𝑥 = 𝑋 ∧ 𝑦 = 𝑌)) → (〈𝑧, 𝑥〉 · 𝑦) = (〈𝑧, 𝑋〉 · 𝑌)) |
| 13 | 12 | oveqd 7448 |
. . . . . . . . 9
⊢ ((𝜑 ∧ (𝑥 = 𝑋 ∧ 𝑦 = 𝑌)) → (𝑓(〈𝑧, 𝑥〉 · 𝑦)𝑔) = (𝑓(〈𝑧, 𝑋〉 · 𝑌)𝑔)) |
| 14 | 10, 13 | mpteq12dv 5233 |
. . . . . . . 8
⊢ ((𝜑 ∧ (𝑥 = 𝑋 ∧ 𝑦 = 𝑌)) → (𝑔 ∈ (𝑧𝐻𝑥) ↦ (𝑓(〈𝑧, 𝑥〉 · 𝑦)𝑔)) = (𝑔 ∈ (𝑧𝐻𝑋) ↦ (𝑓(〈𝑧, 𝑋〉 · 𝑌)𝑔))) |
| 15 | 14 | cnveqd 5886 |
. . . . . . 7
⊢ ((𝜑 ∧ (𝑥 = 𝑋 ∧ 𝑦 = 𝑌)) → ◡(𝑔 ∈ (𝑧𝐻𝑥) ↦ (𝑓(〈𝑧, 𝑥〉 · 𝑦)𝑔)) = ◡(𝑔 ∈ (𝑧𝐻𝑋) ↦ (𝑓(〈𝑧, 𝑋〉 · 𝑌)𝑔))) |
| 16 | 15 | funeqd 6588 |
. . . . . 6
⊢ ((𝜑 ∧ (𝑥 = 𝑋 ∧ 𝑦 = 𝑌)) → (Fun ◡(𝑔 ∈ (𝑧𝐻𝑥) ↦ (𝑓(〈𝑧, 𝑥〉 · 𝑦)𝑔)) ↔ Fun ◡(𝑔 ∈ (𝑧𝐻𝑋) ↦ (𝑓(〈𝑧, 𝑋〉 · 𝑌)𝑔)))) |
| 17 | 16 | ralbidv 3178 |
. . . . 5
⊢ ((𝜑 ∧ (𝑥 = 𝑋 ∧ 𝑦 = 𝑌)) → (∀𝑧 ∈ 𝐵 Fun ◡(𝑔 ∈ (𝑧𝐻𝑥) ↦ (𝑓(〈𝑧, 𝑥〉 · 𝑦)𝑔)) ↔ ∀𝑧 ∈ 𝐵 Fun ◡(𝑔 ∈ (𝑧𝐻𝑋) ↦ (𝑓(〈𝑧, 𝑋〉 · 𝑌)𝑔)))) |
| 18 | 9, 17 | rabeqbidv 3455 |
. . . 4
⊢ ((𝜑 ∧ (𝑥 = 𝑋 ∧ 𝑦 = 𝑌)) → {𝑓 ∈ (𝑥𝐻𝑦) ∣ ∀𝑧 ∈ 𝐵 Fun ◡(𝑔 ∈ (𝑧𝐻𝑥) ↦ (𝑓(〈𝑧, 𝑥〉 · 𝑦)𝑔))} = {𝑓 ∈ (𝑋𝐻𝑌) ∣ ∀𝑧 ∈ 𝐵 Fun ◡(𝑔 ∈ (𝑧𝐻𝑋) ↦ (𝑓(〈𝑧, 𝑋〉 · 𝑌)𝑔))}) |
| 19 | | ismon.x |
. . . 4
⊢ (𝜑 → 𝑋 ∈ 𝐵) |
| 20 | | ismon.y |
. . . 4
⊢ (𝜑 → 𝑌 ∈ 𝐵) |
| 21 | | ovex 7464 |
. . . . . 6
⊢ (𝑋𝐻𝑌) ∈ V |
| 22 | 21 | rabex 5339 |
. . . . 5
⊢ {𝑓 ∈ (𝑋𝐻𝑌) ∣ ∀𝑧 ∈ 𝐵 Fun ◡(𝑔 ∈ (𝑧𝐻𝑋) ↦ (𝑓(〈𝑧, 𝑋〉 · 𝑌)𝑔))} ∈ V |
| 23 | 22 | a1i 11 |
. . . 4
⊢ (𝜑 → {𝑓 ∈ (𝑋𝐻𝑌) ∣ ∀𝑧 ∈ 𝐵 Fun ◡(𝑔 ∈ (𝑧𝐻𝑋) ↦ (𝑓(〈𝑧, 𝑋〉 · 𝑌)𝑔))} ∈ V) |
| 24 | 6, 18, 19, 20, 23 | ovmpod 7585 |
. . 3
⊢ (𝜑 → (𝑋𝑀𝑌) = {𝑓 ∈ (𝑋𝐻𝑌) ∣ ∀𝑧 ∈ 𝐵 Fun ◡(𝑔 ∈ (𝑧𝐻𝑋) ↦ (𝑓(〈𝑧, 𝑋〉 · 𝑌)𝑔))}) |
| 25 | 24 | eleq2d 2827 |
. 2
⊢ (𝜑 → (𝐹 ∈ (𝑋𝑀𝑌) ↔ 𝐹 ∈ {𝑓 ∈ (𝑋𝐻𝑌) ∣ ∀𝑧 ∈ 𝐵 Fun ◡(𝑔 ∈ (𝑧𝐻𝑋) ↦ (𝑓(〈𝑧, 𝑋〉 · 𝑌)𝑔))})) |
| 26 | | oveq1 7438 |
. . . . . . 7
⊢ (𝑓 = 𝐹 → (𝑓(〈𝑧, 𝑋〉 · 𝑌)𝑔) = (𝐹(〈𝑧, 𝑋〉 · 𝑌)𝑔)) |
| 27 | 26 | mpteq2dv 5244 |
. . . . . 6
⊢ (𝑓 = 𝐹 → (𝑔 ∈ (𝑧𝐻𝑋) ↦ (𝑓(〈𝑧, 𝑋〉 · 𝑌)𝑔)) = (𝑔 ∈ (𝑧𝐻𝑋) ↦ (𝐹(〈𝑧, 𝑋〉 · 𝑌)𝑔))) |
| 28 | 27 | cnveqd 5886 |
. . . . 5
⊢ (𝑓 = 𝐹 → ◡(𝑔 ∈ (𝑧𝐻𝑋) ↦ (𝑓(〈𝑧, 𝑋〉 · 𝑌)𝑔)) = ◡(𝑔 ∈ (𝑧𝐻𝑋) ↦ (𝐹(〈𝑧, 𝑋〉 · 𝑌)𝑔))) |
| 29 | 28 | funeqd 6588 |
. . . 4
⊢ (𝑓 = 𝐹 → (Fun ◡(𝑔 ∈ (𝑧𝐻𝑋) ↦ (𝑓(〈𝑧, 𝑋〉 · 𝑌)𝑔)) ↔ Fun ◡(𝑔 ∈ (𝑧𝐻𝑋) ↦ (𝐹(〈𝑧, 𝑋〉 · 𝑌)𝑔)))) |
| 30 | 29 | ralbidv 3178 |
. . 3
⊢ (𝑓 = 𝐹 → (∀𝑧 ∈ 𝐵 Fun ◡(𝑔 ∈ (𝑧𝐻𝑋) ↦ (𝑓(〈𝑧, 𝑋〉 · 𝑌)𝑔)) ↔ ∀𝑧 ∈ 𝐵 Fun ◡(𝑔 ∈ (𝑧𝐻𝑋) ↦ (𝐹(〈𝑧, 𝑋〉 · 𝑌)𝑔)))) |
| 31 | 30 | elrab 3692 |
. 2
⊢ (𝐹 ∈ {𝑓 ∈ (𝑋𝐻𝑌) ∣ ∀𝑧 ∈ 𝐵 Fun ◡(𝑔 ∈ (𝑧𝐻𝑋) ↦ (𝑓(〈𝑧, 𝑋〉 · 𝑌)𝑔))} ↔ (𝐹 ∈ (𝑋𝐻𝑌) ∧ ∀𝑧 ∈ 𝐵 Fun ◡(𝑔 ∈ (𝑧𝐻𝑋) ↦ (𝐹(〈𝑧, 𝑋〉 · 𝑌)𝑔)))) |
| 32 | 25, 31 | bitrdi 287 |
1
⊢ (𝜑 → (𝐹 ∈ (𝑋𝑀𝑌) ↔ (𝐹 ∈ (𝑋𝐻𝑌) ∧ ∀𝑧 ∈ 𝐵 Fun ◡(𝑔 ∈ (𝑧𝐻𝑋) ↦ (𝐹(〈𝑧, 𝑋〉 · 𝑌)𝑔))))) |