| Step | Hyp | Ref
| Expression |
| 1 | | fthmon.r |
. 2
⊢ (𝜑 → 𝑅 ∈ (𝑋𝐻𝑌)) |
| 2 | | eqid 2737 |
. . . . . 6
⊢
(Base‘𝐷) =
(Base‘𝐷) |
| 3 | | eqid 2737 |
. . . . . 6
⊢ (Hom
‘𝐷) = (Hom
‘𝐷) |
| 4 | | eqid 2737 |
. . . . . 6
⊢
(comp‘𝐷) =
(comp‘𝐷) |
| 5 | | fthmon.n |
. . . . . 6
⊢ 𝑁 = (Mono‘𝐷) |
| 6 | | fthmon.f |
. . . . . . . . . . 11
⊢ (𝜑 → 𝐹(𝐶 Faith 𝐷)𝐺) |
| 7 | | fthfunc 17954 |
. . . . . . . . . . . 12
⊢ (𝐶 Faith 𝐷) ⊆ (𝐶 Func 𝐷) |
| 8 | 7 | ssbri 5188 |
. . . . . . . . . . 11
⊢ (𝐹(𝐶 Faith 𝐷)𝐺 → 𝐹(𝐶 Func 𝐷)𝐺) |
| 9 | 6, 8 | syl 17 |
. . . . . . . . . 10
⊢ (𝜑 → 𝐹(𝐶 Func 𝐷)𝐺) |
| 10 | | df-br 5144 |
. . . . . . . . . 10
⊢ (𝐹(𝐶 Func 𝐷)𝐺 ↔ 〈𝐹, 𝐺〉 ∈ (𝐶 Func 𝐷)) |
| 11 | 9, 10 | sylib 218 |
. . . . . . . . 9
⊢ (𝜑 → 〈𝐹, 𝐺〉 ∈ (𝐶 Func 𝐷)) |
| 12 | | funcrcl 17908 |
. . . . . . . . 9
⊢
(〈𝐹, 𝐺〉 ∈ (𝐶 Func 𝐷) → (𝐶 ∈ Cat ∧ 𝐷 ∈ Cat)) |
| 13 | 11, 12 | syl 17 |
. . . . . . . 8
⊢ (𝜑 → (𝐶 ∈ Cat ∧ 𝐷 ∈ Cat)) |
| 14 | 13 | simprd 495 |
. . . . . . 7
⊢ (𝜑 → 𝐷 ∈ Cat) |
| 15 | 14 | adantr 480 |
. . . . . 6
⊢ ((𝜑 ∧ (𝑧 ∈ 𝐵 ∧ 𝑓 ∈ (𝑧𝐻𝑋) ∧ 𝑔 ∈ (𝑧𝐻𝑋))) → 𝐷 ∈ Cat) |
| 16 | | fthmon.b |
. . . . . . . 8
⊢ 𝐵 = (Base‘𝐶) |
| 17 | 9 | adantr 480 |
. . . . . . . 8
⊢ ((𝜑 ∧ (𝑧 ∈ 𝐵 ∧ 𝑓 ∈ (𝑧𝐻𝑋) ∧ 𝑔 ∈ (𝑧𝐻𝑋))) → 𝐹(𝐶 Func 𝐷)𝐺) |
| 18 | 16, 2, 17 | funcf1 17911 |
. . . . . . 7
⊢ ((𝜑 ∧ (𝑧 ∈ 𝐵 ∧ 𝑓 ∈ (𝑧𝐻𝑋) ∧ 𝑔 ∈ (𝑧𝐻𝑋))) → 𝐹:𝐵⟶(Base‘𝐷)) |
| 19 | | fthmon.x |
. . . . . . . 8
⊢ (𝜑 → 𝑋 ∈ 𝐵) |
| 20 | 19 | adantr 480 |
. . . . . . 7
⊢ ((𝜑 ∧ (𝑧 ∈ 𝐵 ∧ 𝑓 ∈ (𝑧𝐻𝑋) ∧ 𝑔 ∈ (𝑧𝐻𝑋))) → 𝑋 ∈ 𝐵) |
| 21 | 18, 20 | ffvelcdmd 7105 |
. . . . . 6
⊢ ((𝜑 ∧ (𝑧 ∈ 𝐵 ∧ 𝑓 ∈ (𝑧𝐻𝑋) ∧ 𝑔 ∈ (𝑧𝐻𝑋))) → (𝐹‘𝑋) ∈ (Base‘𝐷)) |
| 22 | | fthmon.y |
. . . . . . . 8
⊢ (𝜑 → 𝑌 ∈ 𝐵) |
| 23 | 22 | adantr 480 |
. . . . . . 7
⊢ ((𝜑 ∧ (𝑧 ∈ 𝐵 ∧ 𝑓 ∈ (𝑧𝐻𝑋) ∧ 𝑔 ∈ (𝑧𝐻𝑋))) → 𝑌 ∈ 𝐵) |
| 24 | 18, 23 | ffvelcdmd 7105 |
. . . . . 6
⊢ ((𝜑 ∧ (𝑧 ∈ 𝐵 ∧ 𝑓 ∈ (𝑧𝐻𝑋) ∧ 𝑔 ∈ (𝑧𝐻𝑋))) → (𝐹‘𝑌) ∈ (Base‘𝐷)) |
| 25 | | simpr1 1195 |
. . . . . . 7
⊢ ((𝜑 ∧ (𝑧 ∈ 𝐵 ∧ 𝑓 ∈ (𝑧𝐻𝑋) ∧ 𝑔 ∈ (𝑧𝐻𝑋))) → 𝑧 ∈ 𝐵) |
| 26 | 18, 25 | ffvelcdmd 7105 |
. . . . . 6
⊢ ((𝜑 ∧ (𝑧 ∈ 𝐵 ∧ 𝑓 ∈ (𝑧𝐻𝑋) ∧ 𝑔 ∈ (𝑧𝐻𝑋))) → (𝐹‘𝑧) ∈ (Base‘𝐷)) |
| 27 | | fthmon.1 |
. . . . . . 7
⊢ (𝜑 → ((𝑋𝐺𝑌)‘𝑅) ∈ ((𝐹‘𝑋)𝑁(𝐹‘𝑌))) |
| 28 | 27 | adantr 480 |
. . . . . 6
⊢ ((𝜑 ∧ (𝑧 ∈ 𝐵 ∧ 𝑓 ∈ (𝑧𝐻𝑋) ∧ 𝑔 ∈ (𝑧𝐻𝑋))) → ((𝑋𝐺𝑌)‘𝑅) ∈ ((𝐹‘𝑋)𝑁(𝐹‘𝑌))) |
| 29 | | fthmon.h |
. . . . . . . 8
⊢ 𝐻 = (Hom ‘𝐶) |
| 30 | 16, 29, 3, 17, 25, 20 | funcf2 17913 |
. . . . . . 7
⊢ ((𝜑 ∧ (𝑧 ∈ 𝐵 ∧ 𝑓 ∈ (𝑧𝐻𝑋) ∧ 𝑔 ∈ (𝑧𝐻𝑋))) → (𝑧𝐺𝑋):(𝑧𝐻𝑋)⟶((𝐹‘𝑧)(Hom ‘𝐷)(𝐹‘𝑋))) |
| 31 | | simpr2 1196 |
. . . . . . 7
⊢ ((𝜑 ∧ (𝑧 ∈ 𝐵 ∧ 𝑓 ∈ (𝑧𝐻𝑋) ∧ 𝑔 ∈ (𝑧𝐻𝑋))) → 𝑓 ∈ (𝑧𝐻𝑋)) |
| 32 | 30, 31 | ffvelcdmd 7105 |
. . . . . 6
⊢ ((𝜑 ∧ (𝑧 ∈ 𝐵 ∧ 𝑓 ∈ (𝑧𝐻𝑋) ∧ 𝑔 ∈ (𝑧𝐻𝑋))) → ((𝑧𝐺𝑋)‘𝑓) ∈ ((𝐹‘𝑧)(Hom ‘𝐷)(𝐹‘𝑋))) |
| 33 | | simpr3 1197 |
. . . . . . 7
⊢ ((𝜑 ∧ (𝑧 ∈ 𝐵 ∧ 𝑓 ∈ (𝑧𝐻𝑋) ∧ 𝑔 ∈ (𝑧𝐻𝑋))) → 𝑔 ∈ (𝑧𝐻𝑋)) |
| 34 | 30, 33 | ffvelcdmd 7105 |
. . . . . 6
⊢ ((𝜑 ∧ (𝑧 ∈ 𝐵 ∧ 𝑓 ∈ (𝑧𝐻𝑋) ∧ 𝑔 ∈ (𝑧𝐻𝑋))) → ((𝑧𝐺𝑋)‘𝑔) ∈ ((𝐹‘𝑧)(Hom ‘𝐷)(𝐹‘𝑋))) |
| 35 | 2, 3, 4, 5, 15, 21, 24, 26, 28, 32, 34 | moni 17780 |
. . . . 5
⊢ ((𝜑 ∧ (𝑧 ∈ 𝐵 ∧ 𝑓 ∈ (𝑧𝐻𝑋) ∧ 𝑔 ∈ (𝑧𝐻𝑋))) → ((((𝑋𝐺𝑌)‘𝑅)(〈(𝐹‘𝑧), (𝐹‘𝑋)〉(comp‘𝐷)(𝐹‘𝑌))((𝑧𝐺𝑋)‘𝑓)) = (((𝑋𝐺𝑌)‘𝑅)(〈(𝐹‘𝑧), (𝐹‘𝑋)〉(comp‘𝐷)(𝐹‘𝑌))((𝑧𝐺𝑋)‘𝑔)) ↔ ((𝑧𝐺𝑋)‘𝑓) = ((𝑧𝐺𝑋)‘𝑔))) |
| 36 | | eqid 2737 |
. . . . . . . 8
⊢
(comp‘𝐶) =
(comp‘𝐶) |
| 37 | 1 | adantr 480 |
. . . . . . . 8
⊢ ((𝜑 ∧ (𝑧 ∈ 𝐵 ∧ 𝑓 ∈ (𝑧𝐻𝑋) ∧ 𝑔 ∈ (𝑧𝐻𝑋))) → 𝑅 ∈ (𝑋𝐻𝑌)) |
| 38 | 16, 29, 36, 4, 17, 25, 20, 23, 31, 37 | funcco 17916 |
. . . . . . 7
⊢ ((𝜑 ∧ (𝑧 ∈ 𝐵 ∧ 𝑓 ∈ (𝑧𝐻𝑋) ∧ 𝑔 ∈ (𝑧𝐻𝑋))) → ((𝑧𝐺𝑌)‘(𝑅(〈𝑧, 𝑋〉(comp‘𝐶)𝑌)𝑓)) = (((𝑋𝐺𝑌)‘𝑅)(〈(𝐹‘𝑧), (𝐹‘𝑋)〉(comp‘𝐷)(𝐹‘𝑌))((𝑧𝐺𝑋)‘𝑓))) |
| 39 | 16, 29, 36, 4, 17, 25, 20, 23, 33, 37 | funcco 17916 |
. . . . . . 7
⊢ ((𝜑 ∧ (𝑧 ∈ 𝐵 ∧ 𝑓 ∈ (𝑧𝐻𝑋) ∧ 𝑔 ∈ (𝑧𝐻𝑋))) → ((𝑧𝐺𝑌)‘(𝑅(〈𝑧, 𝑋〉(comp‘𝐶)𝑌)𝑔)) = (((𝑋𝐺𝑌)‘𝑅)(〈(𝐹‘𝑧), (𝐹‘𝑋)〉(comp‘𝐷)(𝐹‘𝑌))((𝑧𝐺𝑋)‘𝑔))) |
| 40 | 38, 39 | eqeq12d 2753 |
. . . . . 6
⊢ ((𝜑 ∧ (𝑧 ∈ 𝐵 ∧ 𝑓 ∈ (𝑧𝐻𝑋) ∧ 𝑔 ∈ (𝑧𝐻𝑋))) → (((𝑧𝐺𝑌)‘(𝑅(〈𝑧, 𝑋〉(comp‘𝐶)𝑌)𝑓)) = ((𝑧𝐺𝑌)‘(𝑅(〈𝑧, 𝑋〉(comp‘𝐶)𝑌)𝑔)) ↔ (((𝑋𝐺𝑌)‘𝑅)(〈(𝐹‘𝑧), (𝐹‘𝑋)〉(comp‘𝐷)(𝐹‘𝑌))((𝑧𝐺𝑋)‘𝑓)) = (((𝑋𝐺𝑌)‘𝑅)(〈(𝐹‘𝑧), (𝐹‘𝑋)〉(comp‘𝐷)(𝐹‘𝑌))((𝑧𝐺𝑋)‘𝑔)))) |
| 41 | 6 | adantr 480 |
. . . . . . 7
⊢ ((𝜑 ∧ (𝑧 ∈ 𝐵 ∧ 𝑓 ∈ (𝑧𝐻𝑋) ∧ 𝑔 ∈ (𝑧𝐻𝑋))) → 𝐹(𝐶 Faith 𝐷)𝐺) |
| 42 | 13 | simpld 494 |
. . . . . . . . 9
⊢ (𝜑 → 𝐶 ∈ Cat) |
| 43 | 42 | adantr 480 |
. . . . . . . 8
⊢ ((𝜑 ∧ (𝑧 ∈ 𝐵 ∧ 𝑓 ∈ (𝑧𝐻𝑋) ∧ 𝑔 ∈ (𝑧𝐻𝑋))) → 𝐶 ∈ Cat) |
| 44 | 16, 29, 36, 43, 25, 20, 23, 31, 37 | catcocl 17728 |
. . . . . . 7
⊢ ((𝜑 ∧ (𝑧 ∈ 𝐵 ∧ 𝑓 ∈ (𝑧𝐻𝑋) ∧ 𝑔 ∈ (𝑧𝐻𝑋))) → (𝑅(〈𝑧, 𝑋〉(comp‘𝐶)𝑌)𝑓) ∈ (𝑧𝐻𝑌)) |
| 45 | 16, 29, 36, 43, 25, 20, 23, 33, 37 | catcocl 17728 |
. . . . . . 7
⊢ ((𝜑 ∧ (𝑧 ∈ 𝐵 ∧ 𝑓 ∈ (𝑧𝐻𝑋) ∧ 𝑔 ∈ (𝑧𝐻𝑋))) → (𝑅(〈𝑧, 𝑋〉(comp‘𝐶)𝑌)𝑔) ∈ (𝑧𝐻𝑌)) |
| 46 | 16, 29, 3, 41, 25, 23, 44, 45 | fthi 17965 |
. . . . . 6
⊢ ((𝜑 ∧ (𝑧 ∈ 𝐵 ∧ 𝑓 ∈ (𝑧𝐻𝑋) ∧ 𝑔 ∈ (𝑧𝐻𝑋))) → (((𝑧𝐺𝑌)‘(𝑅(〈𝑧, 𝑋〉(comp‘𝐶)𝑌)𝑓)) = ((𝑧𝐺𝑌)‘(𝑅(〈𝑧, 𝑋〉(comp‘𝐶)𝑌)𝑔)) ↔ (𝑅(〈𝑧, 𝑋〉(comp‘𝐶)𝑌)𝑓) = (𝑅(〈𝑧, 𝑋〉(comp‘𝐶)𝑌)𝑔))) |
| 47 | 40, 46 | bitr3d 281 |
. . . . 5
⊢ ((𝜑 ∧ (𝑧 ∈ 𝐵 ∧ 𝑓 ∈ (𝑧𝐻𝑋) ∧ 𝑔 ∈ (𝑧𝐻𝑋))) → ((((𝑋𝐺𝑌)‘𝑅)(〈(𝐹‘𝑧), (𝐹‘𝑋)〉(comp‘𝐷)(𝐹‘𝑌))((𝑧𝐺𝑋)‘𝑓)) = (((𝑋𝐺𝑌)‘𝑅)(〈(𝐹‘𝑧), (𝐹‘𝑋)〉(comp‘𝐷)(𝐹‘𝑌))((𝑧𝐺𝑋)‘𝑔)) ↔ (𝑅(〈𝑧, 𝑋〉(comp‘𝐶)𝑌)𝑓) = (𝑅(〈𝑧, 𝑋〉(comp‘𝐶)𝑌)𝑔))) |
| 48 | 16, 29, 3, 41, 25, 20, 31, 33 | fthi 17965 |
. . . . 5
⊢ ((𝜑 ∧ (𝑧 ∈ 𝐵 ∧ 𝑓 ∈ (𝑧𝐻𝑋) ∧ 𝑔 ∈ (𝑧𝐻𝑋))) → (((𝑧𝐺𝑋)‘𝑓) = ((𝑧𝐺𝑋)‘𝑔) ↔ 𝑓 = 𝑔)) |
| 49 | 35, 47, 48 | 3bitr3d 309 |
. . . 4
⊢ ((𝜑 ∧ (𝑧 ∈ 𝐵 ∧ 𝑓 ∈ (𝑧𝐻𝑋) ∧ 𝑔 ∈ (𝑧𝐻𝑋))) → ((𝑅(〈𝑧, 𝑋〉(comp‘𝐶)𝑌)𝑓) = (𝑅(〈𝑧, 𝑋〉(comp‘𝐶)𝑌)𝑔) ↔ 𝑓 = 𝑔)) |
| 50 | 49 | biimpd 229 |
. . 3
⊢ ((𝜑 ∧ (𝑧 ∈ 𝐵 ∧ 𝑓 ∈ (𝑧𝐻𝑋) ∧ 𝑔 ∈ (𝑧𝐻𝑋))) → ((𝑅(〈𝑧, 𝑋〉(comp‘𝐶)𝑌)𝑓) = (𝑅(〈𝑧, 𝑋〉(comp‘𝐶)𝑌)𝑔) → 𝑓 = 𝑔)) |
| 51 | 50 | ralrimivvva 3205 |
. 2
⊢ (𝜑 → ∀𝑧 ∈ 𝐵 ∀𝑓 ∈ (𝑧𝐻𝑋)∀𝑔 ∈ (𝑧𝐻𝑋)((𝑅(〈𝑧, 𝑋〉(comp‘𝐶)𝑌)𝑓) = (𝑅(〈𝑧, 𝑋〉(comp‘𝐶)𝑌)𝑔) → 𝑓 = 𝑔)) |
| 52 | | fthmon.m |
. . 3
⊢ 𝑀 = (Mono‘𝐶) |
| 53 | 16, 29, 36, 52, 42, 19, 22 | ismon2 17778 |
. 2
⊢ (𝜑 → (𝑅 ∈ (𝑋𝑀𝑌) ↔ (𝑅 ∈ (𝑋𝐻𝑌) ∧ ∀𝑧 ∈ 𝐵 ∀𝑓 ∈ (𝑧𝐻𝑋)∀𝑔 ∈ (𝑧𝐻𝑋)((𝑅(〈𝑧, 𝑋〉(comp‘𝐶)𝑌)𝑓) = (𝑅(〈𝑧, 𝑋〉(comp‘𝐶)𝑌)𝑔) → 𝑓 = 𝑔)))) |
| 54 | 1, 51, 53 | mpbir2and 713 |
1
⊢ (𝜑 → 𝑅 ∈ (𝑋𝑀𝑌)) |