| Step | Hyp | Ref
| Expression |
| 1 | | moni.f |
. . . . 5
⊢ (𝜑 → 𝐹 ∈ (𝑋𝑀𝑌)) |
| 2 | | ismon.b |
. . . . . 6
⊢ 𝐵 = (Base‘𝐶) |
| 3 | | ismon.h |
. . . . . 6
⊢ 𝐻 = (Hom ‘𝐶) |
| 4 | | ismon.o |
. . . . . 6
⊢ · =
(comp‘𝐶) |
| 5 | | ismon.s |
. . . . . 6
⊢ 𝑀 = (Mono‘𝐶) |
| 6 | | ismon.c |
. . . . . 6
⊢ (𝜑 → 𝐶 ∈ Cat) |
| 7 | | ismon.x |
. . . . . 6
⊢ (𝜑 → 𝑋 ∈ 𝐵) |
| 8 | | ismon.y |
. . . . . 6
⊢ (𝜑 → 𝑌 ∈ 𝐵) |
| 9 | 2, 3, 4, 5, 6, 7, 8 | ismon2 17778 |
. . . . 5
⊢ (𝜑 → (𝐹 ∈ (𝑋𝑀𝑌) ↔ (𝐹 ∈ (𝑋𝐻𝑌) ∧ ∀𝑧 ∈ 𝐵 ∀𝑔 ∈ (𝑧𝐻𝑋)∀ℎ ∈ (𝑧𝐻𝑋)((𝐹(〈𝑧, 𝑋〉 · 𝑌)𝑔) = (𝐹(〈𝑧, 𝑋〉 · 𝑌)ℎ) → 𝑔 = ℎ)))) |
| 10 | 1, 9 | mpbid 232 |
. . . 4
⊢ (𝜑 → (𝐹 ∈ (𝑋𝐻𝑌) ∧ ∀𝑧 ∈ 𝐵 ∀𝑔 ∈ (𝑧𝐻𝑋)∀ℎ ∈ (𝑧𝐻𝑋)((𝐹(〈𝑧, 𝑋〉 · 𝑌)𝑔) = (𝐹(〈𝑧, 𝑋〉 · 𝑌)ℎ) → 𝑔 = ℎ))) |
| 11 | 10 | simprd 495 |
. . 3
⊢ (𝜑 → ∀𝑧 ∈ 𝐵 ∀𝑔 ∈ (𝑧𝐻𝑋)∀ℎ ∈ (𝑧𝐻𝑋)((𝐹(〈𝑧, 𝑋〉 · 𝑌)𝑔) = (𝐹(〈𝑧, 𝑋〉 · 𝑌)ℎ) → 𝑔 = ℎ)) |
| 12 | | moni.z |
. . . 4
⊢ (𝜑 → 𝑍 ∈ 𝐵) |
| 13 | | moni.g |
. . . . . . 7
⊢ (𝜑 → 𝐺 ∈ (𝑍𝐻𝑋)) |
| 14 | 13 | adantr 480 |
. . . . . 6
⊢ ((𝜑 ∧ 𝑧 = 𝑍) → 𝐺 ∈ (𝑍𝐻𝑋)) |
| 15 | | simpr 484 |
. . . . . . 7
⊢ ((𝜑 ∧ 𝑧 = 𝑍) → 𝑧 = 𝑍) |
| 16 | 15 | oveq1d 7446 |
. . . . . 6
⊢ ((𝜑 ∧ 𝑧 = 𝑍) → (𝑧𝐻𝑋) = (𝑍𝐻𝑋)) |
| 17 | 14, 16 | eleqtrrd 2844 |
. . . . 5
⊢ ((𝜑 ∧ 𝑧 = 𝑍) → 𝐺 ∈ (𝑧𝐻𝑋)) |
| 18 | | moni.k |
. . . . . . . . 9
⊢ (𝜑 → 𝐾 ∈ (𝑍𝐻𝑋)) |
| 19 | 18 | adantr 480 |
. . . . . . . 8
⊢ ((𝜑 ∧ 𝑧 = 𝑍) → 𝐾 ∈ (𝑍𝐻𝑋)) |
| 20 | 19, 16 | eleqtrrd 2844 |
. . . . . . 7
⊢ ((𝜑 ∧ 𝑧 = 𝑍) → 𝐾 ∈ (𝑧𝐻𝑋)) |
| 21 | 20 | adantr 480 |
. . . . . 6
⊢ (((𝜑 ∧ 𝑧 = 𝑍) ∧ 𝑔 = 𝐺) → 𝐾 ∈ (𝑧𝐻𝑋)) |
| 22 | | simpllr 776 |
. . . . . . . . . . 11
⊢ ((((𝜑 ∧ 𝑧 = 𝑍) ∧ 𝑔 = 𝐺) ∧ ℎ = 𝐾) → 𝑧 = 𝑍) |
| 23 | 22 | opeq1d 4879 |
. . . . . . . . . 10
⊢ ((((𝜑 ∧ 𝑧 = 𝑍) ∧ 𝑔 = 𝐺) ∧ ℎ = 𝐾) → 〈𝑧, 𝑋〉 = 〈𝑍, 𝑋〉) |
| 24 | 23 | oveq1d 7446 |
. . . . . . . . 9
⊢ ((((𝜑 ∧ 𝑧 = 𝑍) ∧ 𝑔 = 𝐺) ∧ ℎ = 𝐾) → (〈𝑧, 𝑋〉 · 𝑌) = (〈𝑍, 𝑋〉 · 𝑌)) |
| 25 | | eqidd 2738 |
. . . . . . . . 9
⊢ ((((𝜑 ∧ 𝑧 = 𝑍) ∧ 𝑔 = 𝐺) ∧ ℎ = 𝐾) → 𝐹 = 𝐹) |
| 26 | | simplr 769 |
. . . . . . . . 9
⊢ ((((𝜑 ∧ 𝑧 = 𝑍) ∧ 𝑔 = 𝐺) ∧ ℎ = 𝐾) → 𝑔 = 𝐺) |
| 27 | 24, 25, 26 | oveq123d 7452 |
. . . . . . . 8
⊢ ((((𝜑 ∧ 𝑧 = 𝑍) ∧ 𝑔 = 𝐺) ∧ ℎ = 𝐾) → (𝐹(〈𝑧, 𝑋〉 · 𝑌)𝑔) = (𝐹(〈𝑍, 𝑋〉 · 𝑌)𝐺)) |
| 28 | | simpr 484 |
. . . . . . . . 9
⊢ ((((𝜑 ∧ 𝑧 = 𝑍) ∧ 𝑔 = 𝐺) ∧ ℎ = 𝐾) → ℎ = 𝐾) |
| 29 | 24, 25, 28 | oveq123d 7452 |
. . . . . . . 8
⊢ ((((𝜑 ∧ 𝑧 = 𝑍) ∧ 𝑔 = 𝐺) ∧ ℎ = 𝐾) → (𝐹(〈𝑧, 𝑋〉 · 𝑌)ℎ) = (𝐹(〈𝑍, 𝑋〉 · 𝑌)𝐾)) |
| 30 | 27, 29 | eqeq12d 2753 |
. . . . . . 7
⊢ ((((𝜑 ∧ 𝑧 = 𝑍) ∧ 𝑔 = 𝐺) ∧ ℎ = 𝐾) → ((𝐹(〈𝑧, 𝑋〉 · 𝑌)𝑔) = (𝐹(〈𝑧, 𝑋〉 · 𝑌)ℎ) ↔ (𝐹(〈𝑍, 𝑋〉 · 𝑌)𝐺) = (𝐹(〈𝑍, 𝑋〉 · 𝑌)𝐾))) |
| 31 | 26, 28 | eqeq12d 2753 |
. . . . . . 7
⊢ ((((𝜑 ∧ 𝑧 = 𝑍) ∧ 𝑔 = 𝐺) ∧ ℎ = 𝐾) → (𝑔 = ℎ ↔ 𝐺 = 𝐾)) |
| 32 | 30, 31 | imbi12d 344 |
. . . . . 6
⊢ ((((𝜑 ∧ 𝑧 = 𝑍) ∧ 𝑔 = 𝐺) ∧ ℎ = 𝐾) → (((𝐹(〈𝑧, 𝑋〉 · 𝑌)𝑔) = (𝐹(〈𝑧, 𝑋〉 · 𝑌)ℎ) → 𝑔 = ℎ) ↔ ((𝐹(〈𝑍, 𝑋〉 · 𝑌)𝐺) = (𝐹(〈𝑍, 𝑋〉 · 𝑌)𝐾) → 𝐺 = 𝐾))) |
| 33 | 21, 32 | rspcdv 3614 |
. . . . 5
⊢ (((𝜑 ∧ 𝑧 = 𝑍) ∧ 𝑔 = 𝐺) → (∀ℎ ∈ (𝑧𝐻𝑋)((𝐹(〈𝑧, 𝑋〉 · 𝑌)𝑔) = (𝐹(〈𝑧, 𝑋〉 · 𝑌)ℎ) → 𝑔 = ℎ) → ((𝐹(〈𝑍, 𝑋〉 · 𝑌)𝐺) = (𝐹(〈𝑍, 𝑋〉 · 𝑌)𝐾) → 𝐺 = 𝐾))) |
| 34 | 17, 33 | rspcimdv 3612 |
. . . 4
⊢ ((𝜑 ∧ 𝑧 = 𝑍) → (∀𝑔 ∈ (𝑧𝐻𝑋)∀ℎ ∈ (𝑧𝐻𝑋)((𝐹(〈𝑧, 𝑋〉 · 𝑌)𝑔) = (𝐹(〈𝑧, 𝑋〉 · 𝑌)ℎ) → 𝑔 = ℎ) → ((𝐹(〈𝑍, 𝑋〉 · 𝑌)𝐺) = (𝐹(〈𝑍, 𝑋〉 · 𝑌)𝐾) → 𝐺 = 𝐾))) |
| 35 | 12, 34 | rspcimdv 3612 |
. . 3
⊢ (𝜑 → (∀𝑧 ∈ 𝐵 ∀𝑔 ∈ (𝑧𝐻𝑋)∀ℎ ∈ (𝑧𝐻𝑋)((𝐹(〈𝑧, 𝑋〉 · 𝑌)𝑔) = (𝐹(〈𝑧, 𝑋〉 · 𝑌)ℎ) → 𝑔 = ℎ) → ((𝐹(〈𝑍, 𝑋〉 · 𝑌)𝐺) = (𝐹(〈𝑍, 𝑋〉 · 𝑌)𝐾) → 𝐺 = 𝐾))) |
| 36 | 11, 35 | mpd 15 |
. 2
⊢ (𝜑 → ((𝐹(〈𝑍, 𝑋〉 · 𝑌)𝐺) = (𝐹(〈𝑍, 𝑋〉 · 𝑌)𝐾) → 𝐺 = 𝐾)) |
| 37 | | oveq2 7439 |
. 2
⊢ (𝐺 = 𝐾 → (𝐹(〈𝑍, 𝑋〉 · 𝑌)𝐺) = (𝐹(〈𝑍, 𝑋〉 · 𝑌)𝐾)) |
| 38 | 36, 37 | impbid1 225 |
1
⊢ (𝜑 → ((𝐹(〈𝑍, 𝑋〉 · 𝑌)𝐺) = (𝐹(〈𝑍, 𝑋〉 · 𝑌)𝐾) ↔ 𝐺 = 𝐾)) |