Proof of Theorem catprs
| Step | Hyp | Ref
| Expression |
| 1 | | eqid 2737 |
. . . . . 6
⊢
(Base‘𝐶) =
(Base‘𝐶) |
| 2 | | eqid 2737 |
. . . . . 6
⊢ (Hom
‘𝐶) = (Hom
‘𝐶) |
| 3 | | eqid 2737 |
. . . . . 6
⊢
(Id‘𝐶) =
(Id‘𝐶) |
| 4 | | catprs.c |
. . . . . . 7
⊢ (𝜑 → 𝐶 ∈ Cat) |
| 5 | 4 | adantr 480 |
. . . . . 6
⊢ ((𝜑 ∧ (𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵 ∧ 𝑍 ∈ 𝐵)) → 𝐶 ∈ Cat) |
| 6 | | simpr1 1195 |
. . . . . . 7
⊢ ((𝜑 ∧ (𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵 ∧ 𝑍 ∈ 𝐵)) → 𝑋 ∈ 𝐵) |
| 7 | | catprs.b |
. . . . . . . 8
⊢ (𝜑 → 𝐵 = (Base‘𝐶)) |
| 8 | 7 | adantr 480 |
. . . . . . 7
⊢ ((𝜑 ∧ (𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵 ∧ 𝑍 ∈ 𝐵)) → 𝐵 = (Base‘𝐶)) |
| 9 | 6, 8 | eleqtrd 2843 |
. . . . . 6
⊢ ((𝜑 ∧ (𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵 ∧ 𝑍 ∈ 𝐵)) → 𝑋 ∈ (Base‘𝐶)) |
| 10 | 1, 2, 3, 5, 9 | catidcl 17725 |
. . . . 5
⊢ ((𝜑 ∧ (𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵 ∧ 𝑍 ∈ 𝐵)) → ((Id‘𝐶)‘𝑋) ∈ (𝑋(Hom ‘𝐶)𝑋)) |
| 11 | | catprs.h |
. . . . . . 7
⊢ (𝜑 → 𝐻 = (Hom ‘𝐶)) |
| 12 | 11 | adantr 480 |
. . . . . 6
⊢ ((𝜑 ∧ (𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵 ∧ 𝑍 ∈ 𝐵)) → 𝐻 = (Hom ‘𝐶)) |
| 13 | 12 | oveqd 7448 |
. . . . 5
⊢ ((𝜑 ∧ (𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵 ∧ 𝑍 ∈ 𝐵)) → (𝑋𝐻𝑋) = (𝑋(Hom ‘𝐶)𝑋)) |
| 14 | 10, 13 | eleqtrrd 2844 |
. . . 4
⊢ ((𝜑 ∧ (𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵 ∧ 𝑍 ∈ 𝐵)) → ((Id‘𝐶)‘𝑋) ∈ (𝑋𝐻𝑋)) |
| 15 | 14 | ne0d 4342 |
. . 3
⊢ ((𝜑 ∧ (𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵 ∧ 𝑍 ∈ 𝐵)) → (𝑋𝐻𝑋) ≠ ∅) |
| 16 | | catprs.1 |
. . . . 5
⊢ (𝜑 → ∀𝑥 ∈ 𝐵 ∀𝑦 ∈ 𝐵 (𝑥 ≤ 𝑦 ↔ (𝑥𝐻𝑦) ≠ ∅)) |
| 17 | 16 | adantr 480 |
. . . 4
⊢ ((𝜑 ∧ (𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵 ∧ 𝑍 ∈ 𝐵)) → ∀𝑥 ∈ 𝐵 ∀𝑦 ∈ 𝐵 (𝑥 ≤ 𝑦 ↔ (𝑥𝐻𝑦) ≠ ∅)) |
| 18 | 17, 6, 6 | catprslem 48899 |
. . 3
⊢ ((𝜑 ∧ (𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵 ∧ 𝑍 ∈ 𝐵)) → (𝑋 ≤ 𝑋 ↔ (𝑋𝐻𝑋) ≠ ∅)) |
| 19 | 15, 18 | mpbird 257 |
. 2
⊢ ((𝜑 ∧ (𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵 ∧ 𝑍 ∈ 𝐵)) → 𝑋 ≤ 𝑋) |
| 20 | 11 | ad2antrr 726 |
. . . . . 6
⊢ (((𝜑 ∧ (𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵 ∧ 𝑍 ∈ 𝐵)) ∧ (𝑋 ≤ 𝑌 ∧ 𝑌 ≤ 𝑍)) → 𝐻 = (Hom ‘𝐶)) |
| 21 | 20 | oveqd 7448 |
. . . . 5
⊢ (((𝜑 ∧ (𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵 ∧ 𝑍 ∈ 𝐵)) ∧ (𝑋 ≤ 𝑌 ∧ 𝑌 ≤ 𝑍)) → (𝑋𝐻𝑍) = (𝑋(Hom ‘𝐶)𝑍)) |
| 22 | 7 | eleq2d 2827 |
. . . . . . . 8
⊢ (𝜑 → (𝑋 ∈ 𝐵 ↔ 𝑋 ∈ (Base‘𝐶))) |
| 23 | 7 | eleq2d 2827 |
. . . . . . . 8
⊢ (𝜑 → (𝑌 ∈ 𝐵 ↔ 𝑌 ∈ (Base‘𝐶))) |
| 24 | 7 | eleq2d 2827 |
. . . . . . . 8
⊢ (𝜑 → (𝑍 ∈ 𝐵 ↔ 𝑍 ∈ (Base‘𝐶))) |
| 25 | 22, 23, 24 | 3anbi123d 1438 |
. . . . . . 7
⊢ (𝜑 → ((𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵 ∧ 𝑍 ∈ 𝐵) ↔ (𝑋 ∈ (Base‘𝐶) ∧ 𝑌 ∈ (Base‘𝐶) ∧ 𝑍 ∈ (Base‘𝐶)))) |
| 26 | 25 | pm5.32i 574 |
. . . . . 6
⊢ ((𝜑 ∧ (𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵 ∧ 𝑍 ∈ 𝐵)) ↔ (𝜑 ∧ (𝑋 ∈ (Base‘𝐶) ∧ 𝑌 ∈ (Base‘𝐶) ∧ 𝑍 ∈ (Base‘𝐶)))) |
| 27 | | eqid 2737 |
. . . . . . 7
⊢
(comp‘𝐶) =
(comp‘𝐶) |
| 28 | 4 | ad2antrr 726 |
. . . . . . 7
⊢ (((𝜑 ∧ (𝑋 ∈ (Base‘𝐶) ∧ 𝑌 ∈ (Base‘𝐶) ∧ 𝑍 ∈ (Base‘𝐶))) ∧ (𝑋 ≤ 𝑌 ∧ 𝑌 ≤ 𝑍)) → 𝐶 ∈ Cat) |
| 29 | | simplr1 1216 |
. . . . . . 7
⊢ (((𝜑 ∧ (𝑋 ∈ (Base‘𝐶) ∧ 𝑌 ∈ (Base‘𝐶) ∧ 𝑍 ∈ (Base‘𝐶))) ∧ (𝑋 ≤ 𝑌 ∧ 𝑌 ≤ 𝑍)) → 𝑋 ∈ (Base‘𝐶)) |
| 30 | | simplr2 1217 |
. . . . . . 7
⊢ (((𝜑 ∧ (𝑋 ∈ (Base‘𝐶) ∧ 𝑌 ∈ (Base‘𝐶) ∧ 𝑍 ∈ (Base‘𝐶))) ∧ (𝑋 ≤ 𝑌 ∧ 𝑌 ≤ 𝑍)) → 𝑌 ∈ (Base‘𝐶)) |
| 31 | | simplr3 1218 |
. . . . . . 7
⊢ (((𝜑 ∧ (𝑋 ∈ (Base‘𝐶) ∧ 𝑌 ∈ (Base‘𝐶) ∧ 𝑍 ∈ (Base‘𝐶))) ∧ (𝑋 ≤ 𝑌 ∧ 𝑌 ≤ 𝑍)) → 𝑍 ∈ (Base‘𝐶)) |
| 32 | 20 | oveqd 7448 |
. . . . . . . . 9
⊢ (((𝜑 ∧ (𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵 ∧ 𝑍 ∈ 𝐵)) ∧ (𝑋 ≤ 𝑌 ∧ 𝑌 ≤ 𝑍)) → (𝑋𝐻𝑌) = (𝑋(Hom ‘𝐶)𝑌)) |
| 33 | | simpr2 1196 |
. . . . . . . . . . . 12
⊢ ((𝜑 ∧ (𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵 ∧ 𝑍 ∈ 𝐵)) → 𝑌 ∈ 𝐵) |
| 34 | 17, 6, 33 | catprslem 48899 |
. . . . . . . . . . 11
⊢ ((𝜑 ∧ (𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵 ∧ 𝑍 ∈ 𝐵)) → (𝑋 ≤ 𝑌 ↔ (𝑋𝐻𝑌) ≠ ∅)) |
| 35 | 34 | biimpa 476 |
. . . . . . . . . 10
⊢ (((𝜑 ∧ (𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵 ∧ 𝑍 ∈ 𝐵)) ∧ 𝑋 ≤ 𝑌) → (𝑋𝐻𝑌) ≠ ∅) |
| 36 | 35 | adantrr 717 |
. . . . . . . . 9
⊢ (((𝜑 ∧ (𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵 ∧ 𝑍 ∈ 𝐵)) ∧ (𝑋 ≤ 𝑌 ∧ 𝑌 ≤ 𝑍)) → (𝑋𝐻𝑌) ≠ ∅) |
| 37 | 32, 36 | eqnetrrd 3009 |
. . . . . . . 8
⊢ (((𝜑 ∧ (𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵 ∧ 𝑍 ∈ 𝐵)) ∧ (𝑋 ≤ 𝑌 ∧ 𝑌 ≤ 𝑍)) → (𝑋(Hom ‘𝐶)𝑌) ≠ ∅) |
| 38 | 26, 37 | sylanbr 582 |
. . . . . . 7
⊢ (((𝜑 ∧ (𝑋 ∈ (Base‘𝐶) ∧ 𝑌 ∈ (Base‘𝐶) ∧ 𝑍 ∈ (Base‘𝐶))) ∧ (𝑋 ≤ 𝑌 ∧ 𝑌 ≤ 𝑍)) → (𝑋(Hom ‘𝐶)𝑌) ≠ ∅) |
| 39 | 20 | oveqd 7448 |
. . . . . . . . 9
⊢ (((𝜑 ∧ (𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵 ∧ 𝑍 ∈ 𝐵)) ∧ (𝑋 ≤ 𝑌 ∧ 𝑌 ≤ 𝑍)) → (𝑌𝐻𝑍) = (𝑌(Hom ‘𝐶)𝑍)) |
| 40 | | simpr3 1197 |
. . . . . . . . . . . 12
⊢ ((𝜑 ∧ (𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵 ∧ 𝑍 ∈ 𝐵)) → 𝑍 ∈ 𝐵) |
| 41 | 17, 33, 40 | catprslem 48899 |
. . . . . . . . . . 11
⊢ ((𝜑 ∧ (𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵 ∧ 𝑍 ∈ 𝐵)) → (𝑌 ≤ 𝑍 ↔ (𝑌𝐻𝑍) ≠ ∅)) |
| 42 | 41 | biimpa 476 |
. . . . . . . . . 10
⊢ (((𝜑 ∧ (𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵 ∧ 𝑍 ∈ 𝐵)) ∧ 𝑌 ≤ 𝑍) → (𝑌𝐻𝑍) ≠ ∅) |
| 43 | 42 | adantrl 716 |
. . . . . . . . 9
⊢ (((𝜑 ∧ (𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵 ∧ 𝑍 ∈ 𝐵)) ∧ (𝑋 ≤ 𝑌 ∧ 𝑌 ≤ 𝑍)) → (𝑌𝐻𝑍) ≠ ∅) |
| 44 | 39, 43 | eqnetrrd 3009 |
. . . . . . . 8
⊢ (((𝜑 ∧ (𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵 ∧ 𝑍 ∈ 𝐵)) ∧ (𝑋 ≤ 𝑌 ∧ 𝑌 ≤ 𝑍)) → (𝑌(Hom ‘𝐶)𝑍) ≠ ∅) |
| 45 | 26, 44 | sylanbr 582 |
. . . . . . 7
⊢ (((𝜑 ∧ (𝑋 ∈ (Base‘𝐶) ∧ 𝑌 ∈ (Base‘𝐶) ∧ 𝑍 ∈ (Base‘𝐶))) ∧ (𝑋 ≤ 𝑌 ∧ 𝑌 ≤ 𝑍)) → (𝑌(Hom ‘𝐶)𝑍) ≠ ∅) |
| 46 | 1, 2, 27, 28, 29, 30, 31, 38, 45 | catcone0 17730 |
. . . . . 6
⊢ (((𝜑 ∧ (𝑋 ∈ (Base‘𝐶) ∧ 𝑌 ∈ (Base‘𝐶) ∧ 𝑍 ∈ (Base‘𝐶))) ∧ (𝑋 ≤ 𝑌 ∧ 𝑌 ≤ 𝑍)) → (𝑋(Hom ‘𝐶)𝑍) ≠ ∅) |
| 47 | 26, 46 | sylanb 581 |
. . . . 5
⊢ (((𝜑 ∧ (𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵 ∧ 𝑍 ∈ 𝐵)) ∧ (𝑋 ≤ 𝑌 ∧ 𝑌 ≤ 𝑍)) → (𝑋(Hom ‘𝐶)𝑍) ≠ ∅) |
| 48 | 21, 47 | eqnetrd 3008 |
. . . 4
⊢ (((𝜑 ∧ (𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵 ∧ 𝑍 ∈ 𝐵)) ∧ (𝑋 ≤ 𝑌 ∧ 𝑌 ≤ 𝑍)) → (𝑋𝐻𝑍) ≠ ∅) |
| 49 | 17, 6, 40 | catprslem 48899 |
. . . . 5
⊢ ((𝜑 ∧ (𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵 ∧ 𝑍 ∈ 𝐵)) → (𝑋 ≤ 𝑍 ↔ (𝑋𝐻𝑍) ≠ ∅)) |
| 50 | 49 | adantr 480 |
. . . 4
⊢ (((𝜑 ∧ (𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵 ∧ 𝑍 ∈ 𝐵)) ∧ (𝑋 ≤ 𝑌 ∧ 𝑌 ≤ 𝑍)) → (𝑋 ≤ 𝑍 ↔ (𝑋𝐻𝑍) ≠ ∅)) |
| 51 | 48, 50 | mpbird 257 |
. . 3
⊢ (((𝜑 ∧ (𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵 ∧ 𝑍 ∈ 𝐵)) ∧ (𝑋 ≤ 𝑌 ∧ 𝑌 ≤ 𝑍)) → 𝑋 ≤ 𝑍) |
| 52 | 51 | ex 412 |
. 2
⊢ ((𝜑 ∧ (𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵 ∧ 𝑍 ∈ 𝐵)) → ((𝑋 ≤ 𝑌 ∧ 𝑌 ≤ 𝑍) → 𝑋 ≤ 𝑍)) |
| 53 | 19, 52 | jca 511 |
1
⊢ ((𝜑 ∧ (𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵 ∧ 𝑍 ∈ 𝐵)) → (𝑋 ≤ 𝑋 ∧ ((𝑋 ≤ 𝑌 ∧ 𝑌 ≤ 𝑍) → 𝑋 ≤ 𝑍))) |