| Step | Hyp | Ref
| Expression |
| 1 | | sectmon.1 |
. . . 4
⊢ (𝜑 → 𝐹(𝑋𝑆𝑌)𝐺) |
| 2 | | sectmon.b |
. . . . 5
⊢ 𝐵 = (Base‘𝐶) |
| 3 | | eqid 2737 |
. . . . 5
⊢ (Hom
‘𝐶) = (Hom
‘𝐶) |
| 4 | | eqid 2737 |
. . . . 5
⊢
(comp‘𝐶) =
(comp‘𝐶) |
| 5 | | eqid 2737 |
. . . . 5
⊢
(Id‘𝐶) =
(Id‘𝐶) |
| 6 | | sectmon.s |
. . . . 5
⊢ 𝑆 = (Sect‘𝐶) |
| 7 | | sectmon.c |
. . . . 5
⊢ (𝜑 → 𝐶 ∈ Cat) |
| 8 | | sectmon.x |
. . . . 5
⊢ (𝜑 → 𝑋 ∈ 𝐵) |
| 9 | | sectmon.y |
. . . . 5
⊢ (𝜑 → 𝑌 ∈ 𝐵) |
| 10 | 2, 3, 4, 5, 6, 7, 8, 9 | issect 17797 |
. . . 4
⊢ (𝜑 → (𝐹(𝑋𝑆𝑌)𝐺 ↔ (𝐹 ∈ (𝑋(Hom ‘𝐶)𝑌) ∧ 𝐺 ∈ (𝑌(Hom ‘𝐶)𝑋) ∧ (𝐺(〈𝑋, 𝑌〉(comp‘𝐶)𝑋)𝐹) = ((Id‘𝐶)‘𝑋)))) |
| 11 | 1, 10 | mpbid 232 |
. . 3
⊢ (𝜑 → (𝐹 ∈ (𝑋(Hom ‘𝐶)𝑌) ∧ 𝐺 ∈ (𝑌(Hom ‘𝐶)𝑋) ∧ (𝐺(〈𝑋, 𝑌〉(comp‘𝐶)𝑋)𝐹) = ((Id‘𝐶)‘𝑋))) |
| 12 | 11 | simp1d 1143 |
. 2
⊢ (𝜑 → 𝐹 ∈ (𝑋(Hom ‘𝐶)𝑌)) |
| 13 | | oveq2 7439 |
. . . . 5
⊢ ((𝐹(〈𝑥, 𝑋〉(comp‘𝐶)𝑌)𝑔) = (𝐹(〈𝑥, 𝑋〉(comp‘𝐶)𝑌)ℎ) → (𝐺(〈𝑥, 𝑌〉(comp‘𝐶)𝑋)(𝐹(〈𝑥, 𝑋〉(comp‘𝐶)𝑌)𝑔)) = (𝐺(〈𝑥, 𝑌〉(comp‘𝐶)𝑋)(𝐹(〈𝑥, 𝑋〉(comp‘𝐶)𝑌)ℎ))) |
| 14 | 11 | simp3d 1145 |
. . . . . . . . 9
⊢ (𝜑 → (𝐺(〈𝑋, 𝑌〉(comp‘𝐶)𝑋)𝐹) = ((Id‘𝐶)‘𝑋)) |
| 15 | 14 | ad2antrr 726 |
. . . . . . . 8
⊢ (((𝜑 ∧ 𝑥 ∈ 𝐵) ∧ (𝑔 ∈ (𝑥(Hom ‘𝐶)𝑋) ∧ ℎ ∈ (𝑥(Hom ‘𝐶)𝑋))) → (𝐺(〈𝑋, 𝑌〉(comp‘𝐶)𝑋)𝐹) = ((Id‘𝐶)‘𝑋)) |
| 16 | 15 | oveq1d 7446 |
. . . . . . 7
⊢ (((𝜑 ∧ 𝑥 ∈ 𝐵) ∧ (𝑔 ∈ (𝑥(Hom ‘𝐶)𝑋) ∧ ℎ ∈ (𝑥(Hom ‘𝐶)𝑋))) → ((𝐺(〈𝑋, 𝑌〉(comp‘𝐶)𝑋)𝐹)(〈𝑥, 𝑋〉(comp‘𝐶)𝑋)𝑔) = (((Id‘𝐶)‘𝑋)(〈𝑥, 𝑋〉(comp‘𝐶)𝑋)𝑔)) |
| 17 | 7 | ad2antrr 726 |
. . . . . . . 8
⊢ (((𝜑 ∧ 𝑥 ∈ 𝐵) ∧ (𝑔 ∈ (𝑥(Hom ‘𝐶)𝑋) ∧ ℎ ∈ (𝑥(Hom ‘𝐶)𝑋))) → 𝐶 ∈ Cat) |
| 18 | | simplr 769 |
. . . . . . . 8
⊢ (((𝜑 ∧ 𝑥 ∈ 𝐵) ∧ (𝑔 ∈ (𝑥(Hom ‘𝐶)𝑋) ∧ ℎ ∈ (𝑥(Hom ‘𝐶)𝑋))) → 𝑥 ∈ 𝐵) |
| 19 | 8 | ad2antrr 726 |
. . . . . . . 8
⊢ (((𝜑 ∧ 𝑥 ∈ 𝐵) ∧ (𝑔 ∈ (𝑥(Hom ‘𝐶)𝑋) ∧ ℎ ∈ (𝑥(Hom ‘𝐶)𝑋))) → 𝑋 ∈ 𝐵) |
| 20 | 9 | ad2antrr 726 |
. . . . . . . 8
⊢ (((𝜑 ∧ 𝑥 ∈ 𝐵) ∧ (𝑔 ∈ (𝑥(Hom ‘𝐶)𝑋) ∧ ℎ ∈ (𝑥(Hom ‘𝐶)𝑋))) → 𝑌 ∈ 𝐵) |
| 21 | | simprl 771 |
. . . . . . . 8
⊢ (((𝜑 ∧ 𝑥 ∈ 𝐵) ∧ (𝑔 ∈ (𝑥(Hom ‘𝐶)𝑋) ∧ ℎ ∈ (𝑥(Hom ‘𝐶)𝑋))) → 𝑔 ∈ (𝑥(Hom ‘𝐶)𝑋)) |
| 22 | 12 | ad2antrr 726 |
. . . . . . . 8
⊢ (((𝜑 ∧ 𝑥 ∈ 𝐵) ∧ (𝑔 ∈ (𝑥(Hom ‘𝐶)𝑋) ∧ ℎ ∈ (𝑥(Hom ‘𝐶)𝑋))) → 𝐹 ∈ (𝑋(Hom ‘𝐶)𝑌)) |
| 23 | 11 | simp2d 1144 |
. . . . . . . . 9
⊢ (𝜑 → 𝐺 ∈ (𝑌(Hom ‘𝐶)𝑋)) |
| 24 | 23 | ad2antrr 726 |
. . . . . . . 8
⊢ (((𝜑 ∧ 𝑥 ∈ 𝐵) ∧ (𝑔 ∈ (𝑥(Hom ‘𝐶)𝑋) ∧ ℎ ∈ (𝑥(Hom ‘𝐶)𝑋))) → 𝐺 ∈ (𝑌(Hom ‘𝐶)𝑋)) |
| 25 | 2, 3, 4, 17, 18, 19, 20, 21, 22, 19, 24 | catass 17729 |
. . . . . . 7
⊢ (((𝜑 ∧ 𝑥 ∈ 𝐵) ∧ (𝑔 ∈ (𝑥(Hom ‘𝐶)𝑋) ∧ ℎ ∈ (𝑥(Hom ‘𝐶)𝑋))) → ((𝐺(〈𝑋, 𝑌〉(comp‘𝐶)𝑋)𝐹)(〈𝑥, 𝑋〉(comp‘𝐶)𝑋)𝑔) = (𝐺(〈𝑥, 𝑌〉(comp‘𝐶)𝑋)(𝐹(〈𝑥, 𝑋〉(comp‘𝐶)𝑌)𝑔))) |
| 26 | 2, 3, 5, 17, 18, 4, 19, 21 | catlid 17726 |
. . . . . . 7
⊢ (((𝜑 ∧ 𝑥 ∈ 𝐵) ∧ (𝑔 ∈ (𝑥(Hom ‘𝐶)𝑋) ∧ ℎ ∈ (𝑥(Hom ‘𝐶)𝑋))) → (((Id‘𝐶)‘𝑋)(〈𝑥, 𝑋〉(comp‘𝐶)𝑋)𝑔) = 𝑔) |
| 27 | 16, 25, 26 | 3eqtr3d 2785 |
. . . . . 6
⊢ (((𝜑 ∧ 𝑥 ∈ 𝐵) ∧ (𝑔 ∈ (𝑥(Hom ‘𝐶)𝑋) ∧ ℎ ∈ (𝑥(Hom ‘𝐶)𝑋))) → (𝐺(〈𝑥, 𝑌〉(comp‘𝐶)𝑋)(𝐹(〈𝑥, 𝑋〉(comp‘𝐶)𝑌)𝑔)) = 𝑔) |
| 28 | 15 | oveq1d 7446 |
. . . . . . 7
⊢ (((𝜑 ∧ 𝑥 ∈ 𝐵) ∧ (𝑔 ∈ (𝑥(Hom ‘𝐶)𝑋) ∧ ℎ ∈ (𝑥(Hom ‘𝐶)𝑋))) → ((𝐺(〈𝑋, 𝑌〉(comp‘𝐶)𝑋)𝐹)(〈𝑥, 𝑋〉(comp‘𝐶)𝑋)ℎ) = (((Id‘𝐶)‘𝑋)(〈𝑥, 𝑋〉(comp‘𝐶)𝑋)ℎ)) |
| 29 | | simprr 773 |
. . . . . . . 8
⊢ (((𝜑 ∧ 𝑥 ∈ 𝐵) ∧ (𝑔 ∈ (𝑥(Hom ‘𝐶)𝑋) ∧ ℎ ∈ (𝑥(Hom ‘𝐶)𝑋))) → ℎ ∈ (𝑥(Hom ‘𝐶)𝑋)) |
| 30 | 2, 3, 4, 17, 18, 19, 20, 29, 22, 19, 24 | catass 17729 |
. . . . . . 7
⊢ (((𝜑 ∧ 𝑥 ∈ 𝐵) ∧ (𝑔 ∈ (𝑥(Hom ‘𝐶)𝑋) ∧ ℎ ∈ (𝑥(Hom ‘𝐶)𝑋))) → ((𝐺(〈𝑋, 𝑌〉(comp‘𝐶)𝑋)𝐹)(〈𝑥, 𝑋〉(comp‘𝐶)𝑋)ℎ) = (𝐺(〈𝑥, 𝑌〉(comp‘𝐶)𝑋)(𝐹(〈𝑥, 𝑋〉(comp‘𝐶)𝑌)ℎ))) |
| 31 | 2, 3, 5, 17, 18, 4, 19, 29 | catlid 17726 |
. . . . . . 7
⊢ (((𝜑 ∧ 𝑥 ∈ 𝐵) ∧ (𝑔 ∈ (𝑥(Hom ‘𝐶)𝑋) ∧ ℎ ∈ (𝑥(Hom ‘𝐶)𝑋))) → (((Id‘𝐶)‘𝑋)(〈𝑥, 𝑋〉(comp‘𝐶)𝑋)ℎ) = ℎ) |
| 32 | 28, 30, 31 | 3eqtr3d 2785 |
. . . . . 6
⊢ (((𝜑 ∧ 𝑥 ∈ 𝐵) ∧ (𝑔 ∈ (𝑥(Hom ‘𝐶)𝑋) ∧ ℎ ∈ (𝑥(Hom ‘𝐶)𝑋))) → (𝐺(〈𝑥, 𝑌〉(comp‘𝐶)𝑋)(𝐹(〈𝑥, 𝑋〉(comp‘𝐶)𝑌)ℎ)) = ℎ) |
| 33 | 27, 32 | eqeq12d 2753 |
. . . . 5
⊢ (((𝜑 ∧ 𝑥 ∈ 𝐵) ∧ (𝑔 ∈ (𝑥(Hom ‘𝐶)𝑋) ∧ ℎ ∈ (𝑥(Hom ‘𝐶)𝑋))) → ((𝐺(〈𝑥, 𝑌〉(comp‘𝐶)𝑋)(𝐹(〈𝑥, 𝑋〉(comp‘𝐶)𝑌)𝑔)) = (𝐺(〈𝑥, 𝑌〉(comp‘𝐶)𝑋)(𝐹(〈𝑥, 𝑋〉(comp‘𝐶)𝑌)ℎ)) ↔ 𝑔 = ℎ)) |
| 34 | 13, 33 | imbitrid 244 |
. . . 4
⊢ (((𝜑 ∧ 𝑥 ∈ 𝐵) ∧ (𝑔 ∈ (𝑥(Hom ‘𝐶)𝑋) ∧ ℎ ∈ (𝑥(Hom ‘𝐶)𝑋))) → ((𝐹(〈𝑥, 𝑋〉(comp‘𝐶)𝑌)𝑔) = (𝐹(〈𝑥, 𝑋〉(comp‘𝐶)𝑌)ℎ) → 𝑔 = ℎ)) |
| 35 | 34 | ralrimivva 3202 |
. . 3
⊢ ((𝜑 ∧ 𝑥 ∈ 𝐵) → ∀𝑔 ∈ (𝑥(Hom ‘𝐶)𝑋)∀ℎ ∈ (𝑥(Hom ‘𝐶)𝑋)((𝐹(〈𝑥, 𝑋〉(comp‘𝐶)𝑌)𝑔) = (𝐹(〈𝑥, 𝑋〉(comp‘𝐶)𝑌)ℎ) → 𝑔 = ℎ)) |
| 36 | 35 | ralrimiva 3146 |
. 2
⊢ (𝜑 → ∀𝑥 ∈ 𝐵 ∀𝑔 ∈ (𝑥(Hom ‘𝐶)𝑋)∀ℎ ∈ (𝑥(Hom ‘𝐶)𝑋)((𝐹(〈𝑥, 𝑋〉(comp‘𝐶)𝑌)𝑔) = (𝐹(〈𝑥, 𝑋〉(comp‘𝐶)𝑌)ℎ) → 𝑔 = ℎ)) |
| 37 | | sectmon.m |
. . 3
⊢ 𝑀 = (Mono‘𝐶) |
| 38 | 2, 3, 4, 37, 7, 8,
9 | ismon2 17778 |
. 2
⊢ (𝜑 → (𝐹 ∈ (𝑋𝑀𝑌) ↔ (𝐹 ∈ (𝑋(Hom ‘𝐶)𝑌) ∧ ∀𝑥 ∈ 𝐵 ∀𝑔 ∈ (𝑥(Hom ‘𝐶)𝑋)∀ℎ ∈ (𝑥(Hom ‘𝐶)𝑋)((𝐹(〈𝑥, 𝑋〉(comp‘𝐶)𝑌)𝑔) = (𝐹(〈𝑥, 𝑋〉(comp‘𝐶)𝑌)ℎ) → 𝑔 = ℎ)))) |
| 39 | 12, 36, 38 | mpbir2and 713 |
1
⊢ (𝜑 → 𝐹 ∈ (𝑋𝑀𝑌)) |