| Step | Hyp | Ref
| Expression |
| 1 | | eqid 2737 |
. . . . . . . . . . . 12
⊢
(Base‘𝐶) =
(Base‘𝐶) |
| 2 | | eqid 2737 |
. . . . . . . . . . . 12
⊢ (Hom
‘𝐶) = (Hom
‘𝐶) |
| 3 | | eqid 2737 |
. . . . . . . . . . . 12
⊢ (Hom
‘𝐷) = (Hom
‘𝐷) |
| 4 | | monpropd.3 |
. . . . . . . . . . . . . 14
⊢ (𝜑 → (Homf
‘𝐶) =
(Homf ‘𝐷)) |
| 5 | 4 | ad2antrr 726 |
. . . . . . . . . . . . 13
⊢ (((𝜑 ∧ 𝑎 ∈ (Base‘𝐶)) ∧ 𝑏 ∈ (Base‘𝐶)) → (Homf
‘𝐶) =
(Homf ‘𝐷)) |
| 6 | 5 | ad2antrr 726 |
. . . . . . . . . . . 12
⊢
(((((𝜑 ∧ 𝑎 ∈ (Base‘𝐶)) ∧ 𝑏 ∈ (Base‘𝐶)) ∧ 𝑓 ∈ (𝑎(Hom ‘𝐶)𝑏)) ∧ 𝑐 ∈ (Base‘𝐶)) → (Homf
‘𝐶) =
(Homf ‘𝐷)) |
| 7 | | simpr 484 |
. . . . . . . . . . . 12
⊢
(((((𝜑 ∧ 𝑎 ∈ (Base‘𝐶)) ∧ 𝑏 ∈ (Base‘𝐶)) ∧ 𝑓 ∈ (𝑎(Hom ‘𝐶)𝑏)) ∧ 𝑐 ∈ (Base‘𝐶)) → 𝑐 ∈ (Base‘𝐶)) |
| 8 | | simp-4r 784 |
. . . . . . . . . . . 12
⊢
(((((𝜑 ∧ 𝑎 ∈ (Base‘𝐶)) ∧ 𝑏 ∈ (Base‘𝐶)) ∧ 𝑓 ∈ (𝑎(Hom ‘𝐶)𝑏)) ∧ 𝑐 ∈ (Base‘𝐶)) → 𝑎 ∈ (Base‘𝐶)) |
| 9 | 1, 2, 3, 6, 7, 8 | homfeqval 17740 |
. . . . . . . . . . 11
⊢
(((((𝜑 ∧ 𝑎 ∈ (Base‘𝐶)) ∧ 𝑏 ∈ (Base‘𝐶)) ∧ 𝑓 ∈ (𝑎(Hom ‘𝐶)𝑏)) ∧ 𝑐 ∈ (Base‘𝐶)) → (𝑐(Hom ‘𝐶)𝑎) = (𝑐(Hom ‘𝐷)𝑎)) |
| 10 | | eqid 2737 |
. . . . . . . . . . . 12
⊢
(comp‘𝐶) =
(comp‘𝐶) |
| 11 | | eqid 2737 |
. . . . . . . . . . . 12
⊢
(comp‘𝐷) =
(comp‘𝐷) |
| 12 | 4 | ad5antr 734 |
. . . . . . . . . . . 12
⊢
((((((𝜑 ∧ 𝑎 ∈ (Base‘𝐶)) ∧ 𝑏 ∈ (Base‘𝐶)) ∧ 𝑓 ∈ (𝑎(Hom ‘𝐶)𝑏)) ∧ 𝑐 ∈ (Base‘𝐶)) ∧ 𝑔 ∈ (𝑐(Hom ‘𝐶)𝑎)) → (Homf
‘𝐶) =
(Homf ‘𝐷)) |
| 13 | | monpropd.4 |
. . . . . . . . . . . . 13
⊢ (𝜑 →
(compf‘𝐶) = (compf‘𝐷)) |
| 14 | 13 | ad5antr 734 |
. . . . . . . . . . . 12
⊢
((((((𝜑 ∧ 𝑎 ∈ (Base‘𝐶)) ∧ 𝑏 ∈ (Base‘𝐶)) ∧ 𝑓 ∈ (𝑎(Hom ‘𝐶)𝑏)) ∧ 𝑐 ∈ (Base‘𝐶)) ∧ 𝑔 ∈ (𝑐(Hom ‘𝐶)𝑎)) →
(compf‘𝐶) = (compf‘𝐷)) |
| 15 | | simplr 769 |
. . . . . . . . . . . 12
⊢
((((((𝜑 ∧ 𝑎 ∈ (Base‘𝐶)) ∧ 𝑏 ∈ (Base‘𝐶)) ∧ 𝑓 ∈ (𝑎(Hom ‘𝐶)𝑏)) ∧ 𝑐 ∈ (Base‘𝐶)) ∧ 𝑔 ∈ (𝑐(Hom ‘𝐶)𝑎)) → 𝑐 ∈ (Base‘𝐶)) |
| 16 | | simp-5r 786 |
. . . . . . . . . . . 12
⊢
((((((𝜑 ∧ 𝑎 ∈ (Base‘𝐶)) ∧ 𝑏 ∈ (Base‘𝐶)) ∧ 𝑓 ∈ (𝑎(Hom ‘𝐶)𝑏)) ∧ 𝑐 ∈ (Base‘𝐶)) ∧ 𝑔 ∈ (𝑐(Hom ‘𝐶)𝑎)) → 𝑎 ∈ (Base‘𝐶)) |
| 17 | | simp-4r 784 |
. . . . . . . . . . . 12
⊢
((((((𝜑 ∧ 𝑎 ∈ (Base‘𝐶)) ∧ 𝑏 ∈ (Base‘𝐶)) ∧ 𝑓 ∈ (𝑎(Hom ‘𝐶)𝑏)) ∧ 𝑐 ∈ (Base‘𝐶)) ∧ 𝑔 ∈ (𝑐(Hom ‘𝐶)𝑎)) → 𝑏 ∈ (Base‘𝐶)) |
| 18 | | simpr 484 |
. . . . . . . . . . . 12
⊢
((((((𝜑 ∧ 𝑎 ∈ (Base‘𝐶)) ∧ 𝑏 ∈ (Base‘𝐶)) ∧ 𝑓 ∈ (𝑎(Hom ‘𝐶)𝑏)) ∧ 𝑐 ∈ (Base‘𝐶)) ∧ 𝑔 ∈ (𝑐(Hom ‘𝐶)𝑎)) → 𝑔 ∈ (𝑐(Hom ‘𝐶)𝑎)) |
| 19 | | simpllr 776 |
. . . . . . . . . . . 12
⊢
((((((𝜑 ∧ 𝑎 ∈ (Base‘𝐶)) ∧ 𝑏 ∈ (Base‘𝐶)) ∧ 𝑓 ∈ (𝑎(Hom ‘𝐶)𝑏)) ∧ 𝑐 ∈ (Base‘𝐶)) ∧ 𝑔 ∈ (𝑐(Hom ‘𝐶)𝑎)) → 𝑓 ∈ (𝑎(Hom ‘𝐶)𝑏)) |
| 20 | 1, 2, 10, 11, 12, 14, 15, 16, 17, 18, 19 | comfeqval 17751 |
. . . . . . . . . . 11
⊢
((((((𝜑 ∧ 𝑎 ∈ (Base‘𝐶)) ∧ 𝑏 ∈ (Base‘𝐶)) ∧ 𝑓 ∈ (𝑎(Hom ‘𝐶)𝑏)) ∧ 𝑐 ∈ (Base‘𝐶)) ∧ 𝑔 ∈ (𝑐(Hom ‘𝐶)𝑎)) → (𝑓(〈𝑐, 𝑎〉(comp‘𝐶)𝑏)𝑔) = (𝑓(〈𝑐, 𝑎〉(comp‘𝐷)𝑏)𝑔)) |
| 21 | 9, 20 | mpteq12dva 5231 |
. . . . . . . . . 10
⊢
(((((𝜑 ∧ 𝑎 ∈ (Base‘𝐶)) ∧ 𝑏 ∈ (Base‘𝐶)) ∧ 𝑓 ∈ (𝑎(Hom ‘𝐶)𝑏)) ∧ 𝑐 ∈ (Base‘𝐶)) → (𝑔 ∈ (𝑐(Hom ‘𝐶)𝑎) ↦ (𝑓(〈𝑐, 𝑎〉(comp‘𝐶)𝑏)𝑔)) = (𝑔 ∈ (𝑐(Hom ‘𝐷)𝑎) ↦ (𝑓(〈𝑐, 𝑎〉(comp‘𝐷)𝑏)𝑔))) |
| 22 | 21 | cnveqd 5886 |
. . . . . . . . 9
⊢
(((((𝜑 ∧ 𝑎 ∈ (Base‘𝐶)) ∧ 𝑏 ∈ (Base‘𝐶)) ∧ 𝑓 ∈ (𝑎(Hom ‘𝐶)𝑏)) ∧ 𝑐 ∈ (Base‘𝐶)) → ◡(𝑔 ∈ (𝑐(Hom ‘𝐶)𝑎) ↦ (𝑓(〈𝑐, 𝑎〉(comp‘𝐶)𝑏)𝑔)) = ◡(𝑔 ∈ (𝑐(Hom ‘𝐷)𝑎) ↦ (𝑓(〈𝑐, 𝑎〉(comp‘𝐷)𝑏)𝑔))) |
| 23 | 22 | funeqd 6588 |
. . . . . . . 8
⊢
(((((𝜑 ∧ 𝑎 ∈ (Base‘𝐶)) ∧ 𝑏 ∈ (Base‘𝐶)) ∧ 𝑓 ∈ (𝑎(Hom ‘𝐶)𝑏)) ∧ 𝑐 ∈ (Base‘𝐶)) → (Fun ◡(𝑔 ∈ (𝑐(Hom ‘𝐶)𝑎) ↦ (𝑓(〈𝑐, 𝑎〉(comp‘𝐶)𝑏)𝑔)) ↔ Fun ◡(𝑔 ∈ (𝑐(Hom ‘𝐷)𝑎) ↦ (𝑓(〈𝑐, 𝑎〉(comp‘𝐷)𝑏)𝑔)))) |
| 24 | 23 | ralbidva 3176 |
. . . . . . 7
⊢ ((((𝜑 ∧ 𝑎 ∈ (Base‘𝐶)) ∧ 𝑏 ∈ (Base‘𝐶)) ∧ 𝑓 ∈ (𝑎(Hom ‘𝐶)𝑏)) → (∀𝑐 ∈ (Base‘𝐶)Fun ◡(𝑔 ∈ (𝑐(Hom ‘𝐶)𝑎) ↦ (𝑓(〈𝑐, 𝑎〉(comp‘𝐶)𝑏)𝑔)) ↔ ∀𝑐 ∈ (Base‘𝐶)Fun ◡(𝑔 ∈ (𝑐(Hom ‘𝐷)𝑎) ↦ (𝑓(〈𝑐, 𝑎〉(comp‘𝐷)𝑏)𝑔)))) |
| 25 | 24 | rabbidva 3443 |
. . . . . 6
⊢ (((𝜑 ∧ 𝑎 ∈ (Base‘𝐶)) ∧ 𝑏 ∈ (Base‘𝐶)) → {𝑓 ∈ (𝑎(Hom ‘𝐶)𝑏) ∣ ∀𝑐 ∈ (Base‘𝐶)Fun ◡(𝑔 ∈ (𝑐(Hom ‘𝐶)𝑎) ↦ (𝑓(〈𝑐, 𝑎〉(comp‘𝐶)𝑏)𝑔))} = {𝑓 ∈ (𝑎(Hom ‘𝐶)𝑏) ∣ ∀𝑐 ∈ (Base‘𝐶)Fun ◡(𝑔 ∈ (𝑐(Hom ‘𝐷)𝑎) ↦ (𝑓(〈𝑐, 𝑎〉(comp‘𝐷)𝑏)𝑔))}) |
| 26 | | simplr 769 |
. . . . . . . 8
⊢ (((𝜑 ∧ 𝑎 ∈ (Base‘𝐶)) ∧ 𝑏 ∈ (Base‘𝐶)) → 𝑎 ∈ (Base‘𝐶)) |
| 27 | | simpr 484 |
. . . . . . . 8
⊢ (((𝜑 ∧ 𝑎 ∈ (Base‘𝐶)) ∧ 𝑏 ∈ (Base‘𝐶)) → 𝑏 ∈ (Base‘𝐶)) |
| 28 | 1, 2, 3, 5, 26, 27 | homfeqval 17740 |
. . . . . . 7
⊢ (((𝜑 ∧ 𝑎 ∈ (Base‘𝐶)) ∧ 𝑏 ∈ (Base‘𝐶)) → (𝑎(Hom ‘𝐶)𝑏) = (𝑎(Hom ‘𝐷)𝑏)) |
| 29 | 4 | homfeqbas 17739 |
. . . . . . . . 9
⊢ (𝜑 → (Base‘𝐶) = (Base‘𝐷)) |
| 30 | 29 | ad2antrr 726 |
. . . . . . . 8
⊢ (((𝜑 ∧ 𝑎 ∈ (Base‘𝐶)) ∧ 𝑏 ∈ (Base‘𝐶)) → (Base‘𝐶) = (Base‘𝐷)) |
| 31 | 30 | raleqdv 3326 |
. . . . . . 7
⊢ (((𝜑 ∧ 𝑎 ∈ (Base‘𝐶)) ∧ 𝑏 ∈ (Base‘𝐶)) → (∀𝑐 ∈ (Base‘𝐶)Fun ◡(𝑔 ∈ (𝑐(Hom ‘𝐷)𝑎) ↦ (𝑓(〈𝑐, 𝑎〉(comp‘𝐷)𝑏)𝑔)) ↔ ∀𝑐 ∈ (Base‘𝐷)Fun ◡(𝑔 ∈ (𝑐(Hom ‘𝐷)𝑎) ↦ (𝑓(〈𝑐, 𝑎〉(comp‘𝐷)𝑏)𝑔)))) |
| 32 | 28, 31 | rabeqbidv 3455 |
. . . . . 6
⊢ (((𝜑 ∧ 𝑎 ∈ (Base‘𝐶)) ∧ 𝑏 ∈ (Base‘𝐶)) → {𝑓 ∈ (𝑎(Hom ‘𝐶)𝑏) ∣ ∀𝑐 ∈ (Base‘𝐶)Fun ◡(𝑔 ∈ (𝑐(Hom ‘𝐷)𝑎) ↦ (𝑓(〈𝑐, 𝑎〉(comp‘𝐷)𝑏)𝑔))} = {𝑓 ∈ (𝑎(Hom ‘𝐷)𝑏) ∣ ∀𝑐 ∈ (Base‘𝐷)Fun ◡(𝑔 ∈ (𝑐(Hom ‘𝐷)𝑎) ↦ (𝑓(〈𝑐, 𝑎〉(comp‘𝐷)𝑏)𝑔))}) |
| 33 | 25, 32 | eqtrd 2777 |
. . . . 5
⊢ (((𝜑 ∧ 𝑎 ∈ (Base‘𝐶)) ∧ 𝑏 ∈ (Base‘𝐶)) → {𝑓 ∈ (𝑎(Hom ‘𝐶)𝑏) ∣ ∀𝑐 ∈ (Base‘𝐶)Fun ◡(𝑔 ∈ (𝑐(Hom ‘𝐶)𝑎) ↦ (𝑓(〈𝑐, 𝑎〉(comp‘𝐶)𝑏)𝑔))} = {𝑓 ∈ (𝑎(Hom ‘𝐷)𝑏) ∣ ∀𝑐 ∈ (Base‘𝐷)Fun ◡(𝑔 ∈ (𝑐(Hom ‘𝐷)𝑎) ↦ (𝑓(〈𝑐, 𝑎〉(comp‘𝐷)𝑏)𝑔))}) |
| 34 | 33 | 3impa 1110 |
. . . 4
⊢ ((𝜑 ∧ 𝑎 ∈ (Base‘𝐶) ∧ 𝑏 ∈ (Base‘𝐶)) → {𝑓 ∈ (𝑎(Hom ‘𝐶)𝑏) ∣ ∀𝑐 ∈ (Base‘𝐶)Fun ◡(𝑔 ∈ (𝑐(Hom ‘𝐶)𝑎) ↦ (𝑓(〈𝑐, 𝑎〉(comp‘𝐶)𝑏)𝑔))} = {𝑓 ∈ (𝑎(Hom ‘𝐷)𝑏) ∣ ∀𝑐 ∈ (Base‘𝐷)Fun ◡(𝑔 ∈ (𝑐(Hom ‘𝐷)𝑎) ↦ (𝑓(〈𝑐, 𝑎〉(comp‘𝐷)𝑏)𝑔))}) |
| 35 | 34 | mpoeq3dva 7510 |
. . 3
⊢ (𝜑 → (𝑎 ∈ (Base‘𝐶), 𝑏 ∈ (Base‘𝐶) ↦ {𝑓 ∈ (𝑎(Hom ‘𝐶)𝑏) ∣ ∀𝑐 ∈ (Base‘𝐶)Fun ◡(𝑔 ∈ (𝑐(Hom ‘𝐶)𝑎) ↦ (𝑓(〈𝑐, 𝑎〉(comp‘𝐶)𝑏)𝑔))}) = (𝑎 ∈ (Base‘𝐶), 𝑏 ∈ (Base‘𝐶) ↦ {𝑓 ∈ (𝑎(Hom ‘𝐷)𝑏) ∣ ∀𝑐 ∈ (Base‘𝐷)Fun ◡(𝑔 ∈ (𝑐(Hom ‘𝐷)𝑎) ↦ (𝑓(〈𝑐, 𝑎〉(comp‘𝐷)𝑏)𝑔))})) |
| 36 | | mpoeq12 7506 |
. . . 4
⊢
(((Base‘𝐶) =
(Base‘𝐷) ∧
(Base‘𝐶) =
(Base‘𝐷)) →
(𝑎 ∈ (Base‘𝐶), 𝑏 ∈ (Base‘𝐶) ↦ {𝑓 ∈ (𝑎(Hom ‘𝐷)𝑏) ∣ ∀𝑐 ∈ (Base‘𝐷)Fun ◡(𝑔 ∈ (𝑐(Hom ‘𝐷)𝑎) ↦ (𝑓(〈𝑐, 𝑎〉(comp‘𝐷)𝑏)𝑔))}) = (𝑎 ∈ (Base‘𝐷), 𝑏 ∈ (Base‘𝐷) ↦ {𝑓 ∈ (𝑎(Hom ‘𝐷)𝑏) ∣ ∀𝑐 ∈ (Base‘𝐷)Fun ◡(𝑔 ∈ (𝑐(Hom ‘𝐷)𝑎) ↦ (𝑓(〈𝑐, 𝑎〉(comp‘𝐷)𝑏)𝑔))})) |
| 37 | 29, 29, 36 | syl2anc 584 |
. . 3
⊢ (𝜑 → (𝑎 ∈ (Base‘𝐶), 𝑏 ∈ (Base‘𝐶) ↦ {𝑓 ∈ (𝑎(Hom ‘𝐷)𝑏) ∣ ∀𝑐 ∈ (Base‘𝐷)Fun ◡(𝑔 ∈ (𝑐(Hom ‘𝐷)𝑎) ↦ (𝑓(〈𝑐, 𝑎〉(comp‘𝐷)𝑏)𝑔))}) = (𝑎 ∈ (Base‘𝐷), 𝑏 ∈ (Base‘𝐷) ↦ {𝑓 ∈ (𝑎(Hom ‘𝐷)𝑏) ∣ ∀𝑐 ∈ (Base‘𝐷)Fun ◡(𝑔 ∈ (𝑐(Hom ‘𝐷)𝑎) ↦ (𝑓(〈𝑐, 𝑎〉(comp‘𝐷)𝑏)𝑔))})) |
| 38 | 35, 37 | eqtrd 2777 |
. 2
⊢ (𝜑 → (𝑎 ∈ (Base‘𝐶), 𝑏 ∈ (Base‘𝐶) ↦ {𝑓 ∈ (𝑎(Hom ‘𝐶)𝑏) ∣ ∀𝑐 ∈ (Base‘𝐶)Fun ◡(𝑔 ∈ (𝑐(Hom ‘𝐶)𝑎) ↦ (𝑓(〈𝑐, 𝑎〉(comp‘𝐶)𝑏)𝑔))}) = (𝑎 ∈ (Base‘𝐷), 𝑏 ∈ (Base‘𝐷) ↦ {𝑓 ∈ (𝑎(Hom ‘𝐷)𝑏) ∣ ∀𝑐 ∈ (Base‘𝐷)Fun ◡(𝑔 ∈ (𝑐(Hom ‘𝐷)𝑎) ↦ (𝑓(〈𝑐, 𝑎〉(comp‘𝐷)𝑏)𝑔))})) |
| 39 | | eqid 2737 |
. . 3
⊢
(Mono‘𝐶) =
(Mono‘𝐶) |
| 40 | | monpropd.c |
. . 3
⊢ (𝜑 → 𝐶 ∈ Cat) |
| 41 | 1, 2, 10, 39, 40 | monfval 17776 |
. 2
⊢ (𝜑 → (Mono‘𝐶) = (𝑎 ∈ (Base‘𝐶), 𝑏 ∈ (Base‘𝐶) ↦ {𝑓 ∈ (𝑎(Hom ‘𝐶)𝑏) ∣ ∀𝑐 ∈ (Base‘𝐶)Fun ◡(𝑔 ∈ (𝑐(Hom ‘𝐶)𝑎) ↦ (𝑓(〈𝑐, 𝑎〉(comp‘𝐶)𝑏)𝑔))})) |
| 42 | | eqid 2737 |
. . 3
⊢
(Base‘𝐷) =
(Base‘𝐷) |
| 43 | | eqid 2737 |
. . 3
⊢
(Mono‘𝐷) =
(Mono‘𝐷) |
| 44 | | monpropd.d |
. . 3
⊢ (𝜑 → 𝐷 ∈ Cat) |
| 45 | 42, 3, 11, 43, 44 | monfval 17776 |
. 2
⊢ (𝜑 → (Mono‘𝐷) = (𝑎 ∈ (Base‘𝐷), 𝑏 ∈ (Base‘𝐷) ↦ {𝑓 ∈ (𝑎(Hom ‘𝐷)𝑏) ∣ ∀𝑐 ∈ (Base‘𝐷)Fun ◡(𝑔 ∈ (𝑐(Hom ‘𝐷)𝑎) ↦ (𝑓(〈𝑐, 𝑎〉(comp‘𝐷)𝑏)𝑔))})) |
| 46 | 38, 41, 45 | 3eqtr4d 2787 |
1
⊢ (𝜑 → (Mono‘𝐶) = (Mono‘𝐷)) |