Step | Hyp | Ref
| Expression |
1 | | eqid 2738 |
. . . . 5
⊢
(Base‘𝐶) =
(Base‘𝐶) |
2 | | eqid 2738 |
. . . . 5
⊢ (Hom
‘𝐶) = (Hom
‘𝐶) |
3 | | eqid 2738 |
. . . . 5
⊢
(comp‘𝐶) =
(comp‘𝐶) |
4 | | eqid 2738 |
. . . . 5
⊢
(Epi‘𝐶) =
(Epi‘𝐶) |
5 | | grptcmon.c |
. . . . . 6
⊢ (𝜑 → 𝐶 = (MndToCat‘𝐺)) |
6 | | grptcmon.g |
. . . . . . 7
⊢ (𝜑 → 𝐺 ∈ Grp) |
7 | 6 | grpmndd 18589 |
. . . . . 6
⊢ (𝜑 → 𝐺 ∈ Mnd) |
8 | 5, 7 | mndtccat 46375 |
. . . . 5
⊢ (𝜑 → 𝐶 ∈ Cat) |
9 | | grptcmon.x |
. . . . . 6
⊢ (𝜑 → 𝑋 ∈ 𝐵) |
10 | | grptcmon.b |
. . . . . 6
⊢ (𝜑 → 𝐵 = (Base‘𝐶)) |
11 | 9, 10 | eleqtrd 2841 |
. . . . 5
⊢ (𝜑 → 𝑋 ∈ (Base‘𝐶)) |
12 | | grptcmon.y |
. . . . . 6
⊢ (𝜑 → 𝑌 ∈ 𝐵) |
13 | 12, 10 | eleqtrd 2841 |
. . . . 5
⊢ (𝜑 → 𝑌 ∈ (Base‘𝐶)) |
14 | 1, 2, 3, 4, 8, 11,
13 | isepi2 17453 |
. . . 4
⊢ (𝜑 → (𝑓 ∈ (𝑋(Epi‘𝐶)𝑌) ↔ (𝑓 ∈ (𝑋(Hom ‘𝐶)𝑌) ∧ ∀𝑧 ∈ (Base‘𝐶)∀𝑔 ∈ (𝑌(Hom ‘𝐶)𝑧)∀ℎ ∈ (𝑌(Hom ‘𝐶)𝑧)((𝑔(〈𝑋, 𝑌〉(comp‘𝐶)𝑧)𝑓) = (ℎ(〈𝑋, 𝑌〉(comp‘𝐶)𝑧)𝑓) → 𝑔 = ℎ)))) |
15 | 5 | ad2antrr 723 |
. . . . . . . . 9
⊢ (((𝜑 ∧ 𝑓 ∈ (𝑋(Hom ‘𝐶)𝑌)) ∧ (𝑧 ∈ (Base‘𝐶) ∧ 𝑔 ∈ (𝑌(Hom ‘𝐶)𝑧) ∧ ℎ ∈ (𝑌(Hom ‘𝐶)𝑧))) → 𝐶 = (MndToCat‘𝐺)) |
16 | 7 | ad2antrr 723 |
. . . . . . . . 9
⊢ (((𝜑 ∧ 𝑓 ∈ (𝑋(Hom ‘𝐶)𝑌)) ∧ (𝑧 ∈ (Base‘𝐶) ∧ 𝑔 ∈ (𝑌(Hom ‘𝐶)𝑧) ∧ ℎ ∈ (𝑌(Hom ‘𝐶)𝑧))) → 𝐺 ∈ Mnd) |
17 | 10 | ad2antrr 723 |
. . . . . . . . 9
⊢ (((𝜑 ∧ 𝑓 ∈ (𝑋(Hom ‘𝐶)𝑌)) ∧ (𝑧 ∈ (Base‘𝐶) ∧ 𝑔 ∈ (𝑌(Hom ‘𝐶)𝑧) ∧ ℎ ∈ (𝑌(Hom ‘𝐶)𝑧))) → 𝐵 = (Base‘𝐶)) |
18 | 9 | ad2antrr 723 |
. . . . . . . . 9
⊢ (((𝜑 ∧ 𝑓 ∈ (𝑋(Hom ‘𝐶)𝑌)) ∧ (𝑧 ∈ (Base‘𝐶) ∧ 𝑔 ∈ (𝑌(Hom ‘𝐶)𝑧) ∧ ℎ ∈ (𝑌(Hom ‘𝐶)𝑧))) → 𝑋 ∈ 𝐵) |
19 | 12 | ad2antrr 723 |
. . . . . . . . 9
⊢ (((𝜑 ∧ 𝑓 ∈ (𝑋(Hom ‘𝐶)𝑌)) ∧ (𝑧 ∈ (Base‘𝐶) ∧ 𝑔 ∈ (𝑌(Hom ‘𝐶)𝑧) ∧ ℎ ∈ (𝑌(Hom ‘𝐶)𝑧))) → 𝑌 ∈ 𝐵) |
20 | | simpr1 1193 |
. . . . . . . . . 10
⊢ (((𝜑 ∧ 𝑓 ∈ (𝑋(Hom ‘𝐶)𝑌)) ∧ (𝑧 ∈ (Base‘𝐶) ∧ 𝑔 ∈ (𝑌(Hom ‘𝐶)𝑧) ∧ ℎ ∈ (𝑌(Hom ‘𝐶)𝑧))) → 𝑧 ∈ (Base‘𝐶)) |
21 | 20, 17 | eleqtrrd 2842 |
. . . . . . . . 9
⊢ (((𝜑 ∧ 𝑓 ∈ (𝑋(Hom ‘𝐶)𝑌)) ∧ (𝑧 ∈ (Base‘𝐶) ∧ 𝑔 ∈ (𝑌(Hom ‘𝐶)𝑧) ∧ ℎ ∈ (𝑌(Hom ‘𝐶)𝑧))) → 𝑧 ∈ 𝐵) |
22 | | eqidd 2739 |
. . . . . . . . 9
⊢ (((𝜑 ∧ 𝑓 ∈ (𝑋(Hom ‘𝐶)𝑌)) ∧ (𝑧 ∈ (Base‘𝐶) ∧ 𝑔 ∈ (𝑌(Hom ‘𝐶)𝑧) ∧ ℎ ∈ (𝑌(Hom ‘𝐶)𝑧))) → (comp‘𝐶) = (comp‘𝐶)) |
23 | | eqidd 2739 |
. . . . . . . . 9
⊢ (((𝜑 ∧ 𝑓 ∈ (𝑋(Hom ‘𝐶)𝑌)) ∧ (𝑧 ∈ (Base‘𝐶) ∧ 𝑔 ∈ (𝑌(Hom ‘𝐶)𝑧) ∧ ℎ ∈ (𝑌(Hom ‘𝐶)𝑧))) → (〈𝑋, 𝑌〉(comp‘𝐶)𝑧) = (〈𝑋, 𝑌〉(comp‘𝐶)𝑧)) |
24 | 15, 16, 17, 18, 19, 21, 22, 23 | mndtcco2 46373 |
. . . . . . . 8
⊢ (((𝜑 ∧ 𝑓 ∈ (𝑋(Hom ‘𝐶)𝑌)) ∧ (𝑧 ∈ (Base‘𝐶) ∧ 𝑔 ∈ (𝑌(Hom ‘𝐶)𝑧) ∧ ℎ ∈ (𝑌(Hom ‘𝐶)𝑧))) → (𝑔(〈𝑋, 𝑌〉(comp‘𝐶)𝑧)𝑓) = (𝑔(+g‘𝐺)𝑓)) |
25 | 15, 16, 17, 18, 19, 21, 22, 23 | mndtcco2 46373 |
. . . . . . . 8
⊢ (((𝜑 ∧ 𝑓 ∈ (𝑋(Hom ‘𝐶)𝑌)) ∧ (𝑧 ∈ (Base‘𝐶) ∧ 𝑔 ∈ (𝑌(Hom ‘𝐶)𝑧) ∧ ℎ ∈ (𝑌(Hom ‘𝐶)𝑧))) → (ℎ(〈𝑋, 𝑌〉(comp‘𝐶)𝑧)𝑓) = (ℎ(+g‘𝐺)𝑓)) |
26 | 24, 25 | eqeq12d 2754 |
. . . . . . 7
⊢ (((𝜑 ∧ 𝑓 ∈ (𝑋(Hom ‘𝐶)𝑌)) ∧ (𝑧 ∈ (Base‘𝐶) ∧ 𝑔 ∈ (𝑌(Hom ‘𝐶)𝑧) ∧ ℎ ∈ (𝑌(Hom ‘𝐶)𝑧))) → ((𝑔(〈𝑋, 𝑌〉(comp‘𝐶)𝑧)𝑓) = (ℎ(〈𝑋, 𝑌〉(comp‘𝐶)𝑧)𝑓) ↔ (𝑔(+g‘𝐺)𝑓) = (ℎ(+g‘𝐺)𝑓))) |
27 | 6 | ad2antrr 723 |
. . . . . . . 8
⊢ (((𝜑 ∧ 𝑓 ∈ (𝑋(Hom ‘𝐶)𝑌)) ∧ (𝑧 ∈ (Base‘𝐶) ∧ 𝑔 ∈ (𝑌(Hom ‘𝐶)𝑧) ∧ ℎ ∈ (𝑌(Hom ‘𝐶)𝑧))) → 𝐺 ∈ Grp) |
28 | | simpr2 1194 |
. . . . . . . . 9
⊢ (((𝜑 ∧ 𝑓 ∈ (𝑋(Hom ‘𝐶)𝑌)) ∧ (𝑧 ∈ (Base‘𝐶) ∧ 𝑔 ∈ (𝑌(Hom ‘𝐶)𝑧) ∧ ℎ ∈ (𝑌(Hom ‘𝐶)𝑧))) → 𝑔 ∈ (𝑌(Hom ‘𝐶)𝑧)) |
29 | | eqidd 2739 |
. . . . . . . . . 10
⊢ (((𝜑 ∧ 𝑓 ∈ (𝑋(Hom ‘𝐶)𝑌)) ∧ (𝑧 ∈ (Base‘𝐶) ∧ 𝑔 ∈ (𝑌(Hom ‘𝐶)𝑧) ∧ ℎ ∈ (𝑌(Hom ‘𝐶)𝑧))) → (Hom ‘𝐶) = (Hom ‘𝐶)) |
30 | 15, 16, 17, 19, 21, 29 | mndtchom 46371 |
. . . . . . . . 9
⊢ (((𝜑 ∧ 𝑓 ∈ (𝑋(Hom ‘𝐶)𝑌)) ∧ (𝑧 ∈ (Base‘𝐶) ∧ 𝑔 ∈ (𝑌(Hom ‘𝐶)𝑧) ∧ ℎ ∈ (𝑌(Hom ‘𝐶)𝑧))) → (𝑌(Hom ‘𝐶)𝑧) = (Base‘𝐺)) |
31 | 28, 30 | eleqtrd 2841 |
. . . . . . . 8
⊢ (((𝜑 ∧ 𝑓 ∈ (𝑋(Hom ‘𝐶)𝑌)) ∧ (𝑧 ∈ (Base‘𝐶) ∧ 𝑔 ∈ (𝑌(Hom ‘𝐶)𝑧) ∧ ℎ ∈ (𝑌(Hom ‘𝐶)𝑧))) → 𝑔 ∈ (Base‘𝐺)) |
32 | | simpr3 1195 |
. . . . . . . . 9
⊢ (((𝜑 ∧ 𝑓 ∈ (𝑋(Hom ‘𝐶)𝑌)) ∧ (𝑧 ∈ (Base‘𝐶) ∧ 𝑔 ∈ (𝑌(Hom ‘𝐶)𝑧) ∧ ℎ ∈ (𝑌(Hom ‘𝐶)𝑧))) → ℎ ∈ (𝑌(Hom ‘𝐶)𝑧)) |
33 | 32, 30 | eleqtrd 2841 |
. . . . . . . 8
⊢ (((𝜑 ∧ 𝑓 ∈ (𝑋(Hom ‘𝐶)𝑌)) ∧ (𝑧 ∈ (Base‘𝐶) ∧ 𝑔 ∈ (𝑌(Hom ‘𝐶)𝑧) ∧ ℎ ∈ (𝑌(Hom ‘𝐶)𝑧))) → ℎ ∈ (Base‘𝐺)) |
34 | | simplr 766 |
. . . . . . . . 9
⊢ (((𝜑 ∧ 𝑓 ∈ (𝑋(Hom ‘𝐶)𝑌)) ∧ (𝑧 ∈ (Base‘𝐶) ∧ 𝑔 ∈ (𝑌(Hom ‘𝐶)𝑧) ∧ ℎ ∈ (𝑌(Hom ‘𝐶)𝑧))) → 𝑓 ∈ (𝑋(Hom ‘𝐶)𝑌)) |
35 | 15, 16, 17, 18, 19, 29 | mndtchom 46371 |
. . . . . . . . 9
⊢ (((𝜑 ∧ 𝑓 ∈ (𝑋(Hom ‘𝐶)𝑌)) ∧ (𝑧 ∈ (Base‘𝐶) ∧ 𝑔 ∈ (𝑌(Hom ‘𝐶)𝑧) ∧ ℎ ∈ (𝑌(Hom ‘𝐶)𝑧))) → (𝑋(Hom ‘𝐶)𝑌) = (Base‘𝐺)) |
36 | 34, 35 | eleqtrd 2841 |
. . . . . . . 8
⊢ (((𝜑 ∧ 𝑓 ∈ (𝑋(Hom ‘𝐶)𝑌)) ∧ (𝑧 ∈ (Base‘𝐶) ∧ 𝑔 ∈ (𝑌(Hom ‘𝐶)𝑧) ∧ ℎ ∈ (𝑌(Hom ‘𝐶)𝑧))) → 𝑓 ∈ (Base‘𝐺)) |
37 | | eqid 2738 |
. . . . . . . . 9
⊢
(Base‘𝐺) =
(Base‘𝐺) |
38 | | eqid 2738 |
. . . . . . . . 9
⊢
(+g‘𝐺) = (+g‘𝐺) |
39 | 37, 38 | grprcan 18613 |
. . . . . . . 8
⊢ ((𝐺 ∈ Grp ∧ (𝑔 ∈ (Base‘𝐺) ∧ ℎ ∈ (Base‘𝐺) ∧ 𝑓 ∈ (Base‘𝐺))) → ((𝑔(+g‘𝐺)𝑓) = (ℎ(+g‘𝐺)𝑓) ↔ 𝑔 = ℎ)) |
40 | 27, 31, 33, 36, 39 | syl13anc 1371 |
. . . . . . 7
⊢ (((𝜑 ∧ 𝑓 ∈ (𝑋(Hom ‘𝐶)𝑌)) ∧ (𝑧 ∈ (Base‘𝐶) ∧ 𝑔 ∈ (𝑌(Hom ‘𝐶)𝑧) ∧ ℎ ∈ (𝑌(Hom ‘𝐶)𝑧))) → ((𝑔(+g‘𝐺)𝑓) = (ℎ(+g‘𝐺)𝑓) ↔ 𝑔 = ℎ)) |
41 | 26, 40 | bitrd 278 |
. . . . . 6
⊢ (((𝜑 ∧ 𝑓 ∈ (𝑋(Hom ‘𝐶)𝑌)) ∧ (𝑧 ∈ (Base‘𝐶) ∧ 𝑔 ∈ (𝑌(Hom ‘𝐶)𝑧) ∧ ℎ ∈ (𝑌(Hom ‘𝐶)𝑧))) → ((𝑔(〈𝑋, 𝑌〉(comp‘𝐶)𝑧)𝑓) = (ℎ(〈𝑋, 𝑌〉(comp‘𝐶)𝑧)𝑓) ↔ 𝑔 = ℎ)) |
42 | 41 | biimpd 228 |
. . . . 5
⊢ (((𝜑 ∧ 𝑓 ∈ (𝑋(Hom ‘𝐶)𝑌)) ∧ (𝑧 ∈ (Base‘𝐶) ∧ 𝑔 ∈ (𝑌(Hom ‘𝐶)𝑧) ∧ ℎ ∈ (𝑌(Hom ‘𝐶)𝑧))) → ((𝑔(〈𝑋, 𝑌〉(comp‘𝐶)𝑧)𝑓) = (ℎ(〈𝑋, 𝑌〉(comp‘𝐶)𝑧)𝑓) → 𝑔 = ℎ)) |
43 | 42 | ralrimivvva 3127 |
. . . 4
⊢ ((𝜑 ∧ 𝑓 ∈ (𝑋(Hom ‘𝐶)𝑌)) → ∀𝑧 ∈ (Base‘𝐶)∀𝑔 ∈ (𝑌(Hom ‘𝐶)𝑧)∀ℎ ∈ (𝑌(Hom ‘𝐶)𝑧)((𝑔(〈𝑋, 𝑌〉(comp‘𝐶)𝑧)𝑓) = (ℎ(〈𝑋, 𝑌〉(comp‘𝐶)𝑧)𝑓) → 𝑔 = ℎ)) |
44 | 14, 43 | mpbiran3d 46142 |
. . 3
⊢ (𝜑 → (𝑓 ∈ (𝑋(Epi‘𝐶)𝑌) ↔ 𝑓 ∈ (𝑋(Hom ‘𝐶)𝑌))) |
45 | 44 | eqrdv 2736 |
. 2
⊢ (𝜑 → (𝑋(Epi‘𝐶)𝑌) = (𝑋(Hom ‘𝐶)𝑌)) |
46 | | grptcepi.e |
. . 3
⊢ (𝜑 → 𝐸 = (Epi‘𝐶)) |
47 | 46 | oveqd 7292 |
. 2
⊢ (𝜑 → (𝑋𝐸𝑌) = (𝑋(Epi‘𝐶)𝑌)) |
48 | | grptcmon.h |
. . 3
⊢ (𝜑 → 𝐻 = (Hom ‘𝐶)) |
49 | 48 | oveqd 7292 |
. 2
⊢ (𝜑 → (𝑋𝐻𝑌) = (𝑋(Hom ‘𝐶)𝑌)) |
50 | 45, 47, 49 | 3eqtr4d 2788 |
1
⊢ (𝜑 → (𝑋𝐸𝑌) = (𝑋𝐻𝑌)) |