| Step | Hyp | Ref
| Expression |
| 1 | | isthincd.b |
. . 3
⊢ (𝜑 → 𝐵 = (Base‘𝐶)) |
| 2 | | isthincd.h |
. . 3
⊢ (𝜑 → 𝐻 = (Hom ‘𝐶)) |
| 3 | | isthincd.t |
. . 3
⊢ ((𝜑 ∧ (𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐵)) → ∃*𝑓 𝑓 ∈ (𝑥𝐻𝑦)) |
| 4 | | isthincd2.o |
. . . . 5
⊢ (𝜑 → · = (comp‘𝐶)) |
| 5 | | isthincd2.c |
. . . . 5
⊢ (𝜑 → 𝐶 ∈ 𝑉) |
| 6 | | 3an4anass 1105 |
. . . . . . . 8
⊢ (((𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐵 ∧ 𝑧 ∈ 𝐵) ∧ 𝑤 ∈ 𝐵) ↔ ((𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐵) ∧ (𝑧 ∈ 𝐵 ∧ 𝑤 ∈ 𝐵))) |
| 7 | 6 | anbi1i 624 |
. . . . . . 7
⊢ ((((𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐵 ∧ 𝑧 ∈ 𝐵) ∧ 𝑤 ∈ 𝐵) ∧ ((𝑓 ∈ (𝑥𝐻𝑦) ∧ 𝑔 ∈ (𝑦𝐻𝑧)) ∧ 𝑘 ∈ (𝑧𝐻𝑤))) ↔ (((𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐵) ∧ (𝑧 ∈ 𝐵 ∧ 𝑤 ∈ 𝐵)) ∧ ((𝑓 ∈ (𝑥𝐻𝑦) ∧ 𝑔 ∈ (𝑦𝐻𝑧)) ∧ 𝑘 ∈ (𝑧𝐻𝑤)))) |
| 8 | | isthincd2.ps |
. . . . . . . . 9
⊢ (𝜓 ↔ ((𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐵 ∧ 𝑧 ∈ 𝐵) ∧ (𝑓 ∈ (𝑥𝐻𝑦) ∧ 𝑔 ∈ (𝑦𝐻𝑧)))) |
| 9 | 8 | 3anbi1i 1158 |
. . . . . . . 8
⊢ ((𝜓 ∧ 𝑤 ∈ 𝐵 ∧ 𝑘 ∈ (𝑧𝐻𝑤)) ↔ (((𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐵 ∧ 𝑧 ∈ 𝐵) ∧ (𝑓 ∈ (𝑥𝐻𝑦) ∧ 𝑔 ∈ (𝑦𝐻𝑧))) ∧ 𝑤 ∈ 𝐵 ∧ 𝑘 ∈ (𝑧𝐻𝑤))) |
| 10 | | 3anass 1095 |
. . . . . . . 8
⊢ ((((𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐵 ∧ 𝑧 ∈ 𝐵) ∧ (𝑓 ∈ (𝑥𝐻𝑦) ∧ 𝑔 ∈ (𝑦𝐻𝑧))) ∧ 𝑤 ∈ 𝐵 ∧ 𝑘 ∈ (𝑧𝐻𝑤)) ↔ (((𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐵 ∧ 𝑧 ∈ 𝐵) ∧ (𝑓 ∈ (𝑥𝐻𝑦) ∧ 𝑔 ∈ (𝑦𝐻𝑧))) ∧ (𝑤 ∈ 𝐵 ∧ 𝑘 ∈ (𝑧𝐻𝑤)))) |
| 11 | | an4 656 |
. . . . . . . 8
⊢ ((((𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐵 ∧ 𝑧 ∈ 𝐵) ∧ (𝑓 ∈ (𝑥𝐻𝑦) ∧ 𝑔 ∈ (𝑦𝐻𝑧))) ∧ (𝑤 ∈ 𝐵 ∧ 𝑘 ∈ (𝑧𝐻𝑤))) ↔ (((𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐵 ∧ 𝑧 ∈ 𝐵) ∧ 𝑤 ∈ 𝐵) ∧ ((𝑓 ∈ (𝑥𝐻𝑦) ∧ 𝑔 ∈ (𝑦𝐻𝑧)) ∧ 𝑘 ∈ (𝑧𝐻𝑤)))) |
| 12 | 9, 10, 11 | 3bitri 297 |
. . . . . . 7
⊢ ((𝜓 ∧ 𝑤 ∈ 𝐵 ∧ 𝑘 ∈ (𝑧𝐻𝑤)) ↔ (((𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐵 ∧ 𝑧 ∈ 𝐵) ∧ 𝑤 ∈ 𝐵) ∧ ((𝑓 ∈ (𝑥𝐻𝑦) ∧ 𝑔 ∈ (𝑦𝐻𝑧)) ∧ 𝑘 ∈ (𝑧𝐻𝑤)))) |
| 13 | | df-3an 1089 |
. . . . . . . 8
⊢ ((𝑓 ∈ (𝑥𝐻𝑦) ∧ 𝑔 ∈ (𝑦𝐻𝑧) ∧ 𝑘 ∈ (𝑧𝐻𝑤)) ↔ ((𝑓 ∈ (𝑥𝐻𝑦) ∧ 𝑔 ∈ (𝑦𝐻𝑧)) ∧ 𝑘 ∈ (𝑧𝐻𝑤))) |
| 14 | 13 | anbi2i 623 |
. . . . . . 7
⊢ ((((𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐵) ∧ (𝑧 ∈ 𝐵 ∧ 𝑤 ∈ 𝐵)) ∧ (𝑓 ∈ (𝑥𝐻𝑦) ∧ 𝑔 ∈ (𝑦𝐻𝑧) ∧ 𝑘 ∈ (𝑧𝐻𝑤))) ↔ (((𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐵) ∧ (𝑧 ∈ 𝐵 ∧ 𝑤 ∈ 𝐵)) ∧ ((𝑓 ∈ (𝑥𝐻𝑦) ∧ 𝑔 ∈ (𝑦𝐻𝑧)) ∧ 𝑘 ∈ (𝑧𝐻𝑤)))) |
| 15 | 7, 12, 14 | 3bitr4i 303 |
. . . . . 6
⊢ ((𝜓 ∧ 𝑤 ∈ 𝐵 ∧ 𝑘 ∈ (𝑧𝐻𝑤)) ↔ (((𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐵) ∧ (𝑧 ∈ 𝐵 ∧ 𝑤 ∈ 𝐵)) ∧ (𝑓 ∈ (𝑥𝐻𝑦) ∧ 𝑔 ∈ (𝑦𝐻𝑧) ∧ 𝑘 ∈ (𝑧𝐻𝑤)))) |
| 16 | | df-3an 1089 |
. . . . . 6
⊢ (((𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐵) ∧ (𝑧 ∈ 𝐵 ∧ 𝑤 ∈ 𝐵) ∧ (𝑓 ∈ (𝑥𝐻𝑦) ∧ 𝑔 ∈ (𝑦𝐻𝑧) ∧ 𝑘 ∈ (𝑧𝐻𝑤))) ↔ (((𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐵) ∧ (𝑧 ∈ 𝐵 ∧ 𝑤 ∈ 𝐵)) ∧ (𝑓 ∈ (𝑥𝐻𝑦) ∧ 𝑔 ∈ (𝑦𝐻𝑧) ∧ 𝑘 ∈ (𝑧𝐻𝑤)))) |
| 17 | 15, 16 | bitr4i 278 |
. . . . 5
⊢ ((𝜓 ∧ 𝑤 ∈ 𝐵 ∧ 𝑘 ∈ (𝑧𝐻𝑤)) ↔ ((𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐵) ∧ (𝑧 ∈ 𝐵 ∧ 𝑤 ∈ 𝐵) ∧ (𝑓 ∈ (𝑥𝐻𝑦) ∧ 𝑔 ∈ (𝑦𝐻𝑧) ∧ 𝑘 ∈ (𝑧𝐻𝑤)))) |
| 18 | | isthincd2.1 |
. . . . 5
⊢ ((𝜑 ∧ 𝑦 ∈ 𝐵) → 1 ∈ (𝑦𝐻𝑦)) |
| 19 | | simpr1l 1231 |
. . . . . . 7
⊢ ((𝜑 ∧ ((𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐵) ∧ (𝑧 ∈ 𝐵 ∧ 𝑤 ∈ 𝐵) ∧ (𝑓 ∈ (𝑥𝐻𝑦) ∧ 𝑔 ∈ (𝑦𝐻𝑧) ∧ 𝑘 ∈ (𝑧𝐻𝑤)))) → 𝑥 ∈ 𝐵) |
| 20 | | simpr1r 1232 |
. . . . . . 7
⊢ ((𝜑 ∧ ((𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐵) ∧ (𝑧 ∈ 𝐵 ∧ 𝑤 ∈ 𝐵) ∧ (𝑓 ∈ (𝑥𝐻𝑦) ∧ 𝑔 ∈ (𝑦𝐻𝑧) ∧ 𝑘 ∈ (𝑧𝐻𝑤)))) → 𝑦 ∈ 𝐵) |
| 21 | | simpr31 1264 |
. . . . . . . 8
⊢ ((𝜑 ∧ ((𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐵) ∧ (𝑧 ∈ 𝐵 ∧ 𝑤 ∈ 𝐵) ∧ (𝑓 ∈ (𝑥𝐻𝑦) ∧ 𝑔 ∈ (𝑦𝐻𝑧) ∧ 𝑘 ∈ (𝑧𝐻𝑤)))) → 𝑓 ∈ (𝑥𝐻𝑦)) |
| 22 | 20, 18 | syldan 591 |
. . . . . . . 8
⊢ ((𝜑 ∧ ((𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐵) ∧ (𝑧 ∈ 𝐵 ∧ 𝑤 ∈ 𝐵) ∧ (𝑓 ∈ (𝑥𝐻𝑦) ∧ 𝑔 ∈ (𝑦𝐻𝑧) ∧ 𝑘 ∈ (𝑧𝐻𝑤)))) → 1 ∈ (𝑦𝐻𝑦)) |
| 23 | 8 | bianass 642 |
. . . . . . . . . . . 12
⊢ ((𝜑 ∧ 𝜓) ↔ ((𝜑 ∧ (𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐵 ∧ 𝑧 ∈ 𝐵)) ∧ (𝑓 ∈ (𝑥𝐻𝑦) ∧ 𝑔 ∈ (𝑦𝐻𝑧)))) |
| 24 | | isthincd2.2 |
. . . . . . . . . . . 12
⊢ ((𝜑 ∧ 𝜓) → (𝑔(〈𝑥, 𝑦〉 · 𝑧)𝑓) ∈ (𝑥𝐻𝑧)) |
| 25 | 23, 24 | sylbir 235 |
. . . . . . . . . . 11
⊢ (((𝜑 ∧ (𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐵 ∧ 𝑧 ∈ 𝐵)) ∧ (𝑓 ∈ (𝑥𝐻𝑦) ∧ 𝑔 ∈ (𝑦𝐻𝑧))) → (𝑔(〈𝑥, 𝑦〉 · 𝑧)𝑓) ∈ (𝑥𝐻𝑧)) |
| 26 | 25 | ralrimivva 3202 |
. . . . . . . . . 10
⊢ ((𝜑 ∧ (𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐵 ∧ 𝑧 ∈ 𝐵)) → ∀𝑓 ∈ (𝑥𝐻𝑦)∀𝑔 ∈ (𝑦𝐻𝑧)(𝑔(〈𝑥, 𝑦〉 · 𝑧)𝑓) ∈ (𝑥𝐻𝑧)) |
| 27 | 26 | ralrimivvva 3205 |
. . . . . . . . 9
⊢ (𝜑 → ∀𝑥 ∈ 𝐵 ∀𝑦 ∈ 𝐵 ∀𝑧 ∈ 𝐵 ∀𝑓 ∈ (𝑥𝐻𝑦)∀𝑔 ∈ (𝑦𝐻𝑧)(𝑔(〈𝑥, 𝑦〉 · 𝑧)𝑓) ∈ (𝑥𝐻𝑧)) |
| 28 | 27 | adantr 480 |
. . . . . . . 8
⊢ ((𝜑 ∧ ((𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐵) ∧ (𝑧 ∈ 𝐵 ∧ 𝑤 ∈ 𝐵) ∧ (𝑓 ∈ (𝑥𝐻𝑦) ∧ 𝑔 ∈ (𝑦𝐻𝑧) ∧ 𝑘 ∈ (𝑧𝐻𝑤)))) → ∀𝑥 ∈ 𝐵 ∀𝑦 ∈ 𝐵 ∀𝑧 ∈ 𝐵 ∀𝑓 ∈ (𝑥𝐻𝑦)∀𝑔 ∈ (𝑦𝐻𝑧)(𝑔(〈𝑥, 𝑦〉 · 𝑧)𝑓) ∈ (𝑥𝐻𝑧)) |
| 29 | 19, 20, 20, 21, 22, 28 | isthincd2lem2 49084 |
. . . . . . 7
⊢ ((𝜑 ∧ ((𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐵) ∧ (𝑧 ∈ 𝐵 ∧ 𝑤 ∈ 𝐵) ∧ (𝑓 ∈ (𝑥𝐻𝑦) ∧ 𝑔 ∈ (𝑦𝐻𝑧) ∧ 𝑘 ∈ (𝑧𝐻𝑤)))) → ( 1 (〈𝑥, 𝑦〉 · 𝑦)𝑓) ∈ (𝑥𝐻𝑦)) |
| 30 | 3 | ralrimivva 3202 |
. . . . . . . 8
⊢ (𝜑 → ∀𝑥 ∈ 𝐵 ∀𝑦 ∈ 𝐵 ∃*𝑓 𝑓 ∈ (𝑥𝐻𝑦)) |
| 31 | 30 | adantr 480 |
. . . . . . 7
⊢ ((𝜑 ∧ ((𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐵) ∧ (𝑧 ∈ 𝐵 ∧ 𝑤 ∈ 𝐵) ∧ (𝑓 ∈ (𝑥𝐻𝑦) ∧ 𝑔 ∈ (𝑦𝐻𝑧) ∧ 𝑘 ∈ (𝑧𝐻𝑤)))) → ∀𝑥 ∈ 𝐵 ∀𝑦 ∈ 𝐵 ∃*𝑓 𝑓 ∈ (𝑥𝐻𝑦)) |
| 32 | 19, 20, 29, 21, 31 | isthincd2lem1 49075 |
. . . . . 6
⊢ ((𝜑 ∧ ((𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐵) ∧ (𝑧 ∈ 𝐵 ∧ 𝑤 ∈ 𝐵) ∧ (𝑓 ∈ (𝑥𝐻𝑦) ∧ 𝑔 ∈ (𝑦𝐻𝑧) ∧ 𝑘 ∈ (𝑧𝐻𝑤)))) → ( 1 (〈𝑥, 𝑦〉 · 𝑦)𝑓) = 𝑓) |
| 33 | 17, 32 | sylan2b 594 |
. . . . 5
⊢ ((𝜑 ∧ (𝜓 ∧ 𝑤 ∈ 𝐵 ∧ 𝑘 ∈ (𝑧𝐻𝑤))) → ( 1 (〈𝑥, 𝑦〉 · 𝑦)𝑓) = 𝑓) |
| 34 | | simpr2l 1233 |
. . . . . . 7
⊢ ((𝜑 ∧ ((𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐵) ∧ (𝑧 ∈ 𝐵 ∧ 𝑤 ∈ 𝐵) ∧ (𝑓 ∈ (𝑥𝐻𝑦) ∧ 𝑔 ∈ (𝑦𝐻𝑧) ∧ 𝑘 ∈ (𝑧𝐻𝑤)))) → 𝑧 ∈ 𝐵) |
| 35 | | simpr32 1265 |
. . . . . . . 8
⊢ ((𝜑 ∧ ((𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐵) ∧ (𝑧 ∈ 𝐵 ∧ 𝑤 ∈ 𝐵) ∧ (𝑓 ∈ (𝑥𝐻𝑦) ∧ 𝑔 ∈ (𝑦𝐻𝑧) ∧ 𝑘 ∈ (𝑧𝐻𝑤)))) → 𝑔 ∈ (𝑦𝐻𝑧)) |
| 36 | 20, 20, 34, 22, 35, 28 | isthincd2lem2 49084 |
. . . . . . 7
⊢ ((𝜑 ∧ ((𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐵) ∧ (𝑧 ∈ 𝐵 ∧ 𝑤 ∈ 𝐵) ∧ (𝑓 ∈ (𝑥𝐻𝑦) ∧ 𝑔 ∈ (𝑦𝐻𝑧) ∧ 𝑘 ∈ (𝑧𝐻𝑤)))) → (𝑔(〈𝑦, 𝑦〉 · 𝑧) 1 ) ∈ (𝑦𝐻𝑧)) |
| 37 | 20, 34, 36, 35, 31 | isthincd2lem1 49075 |
. . . . . 6
⊢ ((𝜑 ∧ ((𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐵) ∧ (𝑧 ∈ 𝐵 ∧ 𝑤 ∈ 𝐵) ∧ (𝑓 ∈ (𝑥𝐻𝑦) ∧ 𝑔 ∈ (𝑦𝐻𝑧) ∧ 𝑘 ∈ (𝑧𝐻𝑤)))) → (𝑔(〈𝑦, 𝑦〉 · 𝑧) 1 ) = 𝑔) |
| 38 | 17, 37 | sylan2b 594 |
. . . . 5
⊢ ((𝜑 ∧ (𝜓 ∧ 𝑤 ∈ 𝐵 ∧ 𝑘 ∈ (𝑧𝐻𝑤))) → (𝑔(〈𝑦, 𝑦〉 · 𝑧) 1 ) = 𝑔) |
| 39 | 24 | 3ad2antr1 1189 |
. . . . 5
⊢ ((𝜑 ∧ (𝜓 ∧ 𝑤 ∈ 𝐵 ∧ 𝑘 ∈ (𝑧𝐻𝑤))) → (𝑔(〈𝑥, 𝑦〉 · 𝑧)𝑓) ∈ (𝑥𝐻𝑧)) |
| 40 | | simpr2r 1234 |
. . . . . . 7
⊢ ((𝜑 ∧ ((𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐵) ∧ (𝑧 ∈ 𝐵 ∧ 𝑤 ∈ 𝐵) ∧ (𝑓 ∈ (𝑥𝐻𝑦) ∧ 𝑔 ∈ (𝑦𝐻𝑧) ∧ 𝑘 ∈ (𝑧𝐻𝑤)))) → 𝑤 ∈ 𝐵) |
| 41 | | simpr33 1266 |
. . . . . . . . 9
⊢ ((𝜑 ∧ ((𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐵) ∧ (𝑧 ∈ 𝐵 ∧ 𝑤 ∈ 𝐵) ∧ (𝑓 ∈ (𝑥𝐻𝑦) ∧ 𝑔 ∈ (𝑦𝐻𝑧) ∧ 𝑘 ∈ (𝑧𝐻𝑤)))) → 𝑘 ∈ (𝑧𝐻𝑤)) |
| 42 | 20, 34, 40, 35, 41, 28 | isthincd2lem2 49084 |
. . . . . . . 8
⊢ ((𝜑 ∧ ((𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐵) ∧ (𝑧 ∈ 𝐵 ∧ 𝑤 ∈ 𝐵) ∧ (𝑓 ∈ (𝑥𝐻𝑦) ∧ 𝑔 ∈ (𝑦𝐻𝑧) ∧ 𝑘 ∈ (𝑧𝐻𝑤)))) → (𝑘(〈𝑦, 𝑧〉 · 𝑤)𝑔) ∈ (𝑦𝐻𝑤)) |
| 43 | 19, 20, 40, 21, 42, 28 | isthincd2lem2 49084 |
. . . . . . 7
⊢ ((𝜑 ∧ ((𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐵) ∧ (𝑧 ∈ 𝐵 ∧ 𝑤 ∈ 𝐵) ∧ (𝑓 ∈ (𝑥𝐻𝑦) ∧ 𝑔 ∈ (𝑦𝐻𝑧) ∧ 𝑘 ∈ (𝑧𝐻𝑤)))) → ((𝑘(〈𝑦, 𝑧〉 · 𝑤)𝑔)(〈𝑥, 𝑦〉 · 𝑤)𝑓) ∈ (𝑥𝐻𝑤)) |
| 44 | 17, 39 | sylan2br 595 |
. . . . . . . 8
⊢ ((𝜑 ∧ ((𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐵) ∧ (𝑧 ∈ 𝐵 ∧ 𝑤 ∈ 𝐵) ∧ (𝑓 ∈ (𝑥𝐻𝑦) ∧ 𝑔 ∈ (𝑦𝐻𝑧) ∧ 𝑘 ∈ (𝑧𝐻𝑤)))) → (𝑔(〈𝑥, 𝑦〉 · 𝑧)𝑓) ∈ (𝑥𝐻𝑧)) |
| 45 | 19, 34, 40, 44, 41, 28 | isthincd2lem2 49084 |
. . . . . . 7
⊢ ((𝜑 ∧ ((𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐵) ∧ (𝑧 ∈ 𝐵 ∧ 𝑤 ∈ 𝐵) ∧ (𝑓 ∈ (𝑥𝐻𝑦) ∧ 𝑔 ∈ (𝑦𝐻𝑧) ∧ 𝑘 ∈ (𝑧𝐻𝑤)))) → (𝑘(〈𝑥, 𝑧〉 · 𝑤)(𝑔(〈𝑥, 𝑦〉 · 𝑧)𝑓)) ∈ (𝑥𝐻𝑤)) |
| 46 | 19, 40, 43, 45, 31 | isthincd2lem1 49075 |
. . . . . 6
⊢ ((𝜑 ∧ ((𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐵) ∧ (𝑧 ∈ 𝐵 ∧ 𝑤 ∈ 𝐵) ∧ (𝑓 ∈ (𝑥𝐻𝑦) ∧ 𝑔 ∈ (𝑦𝐻𝑧) ∧ 𝑘 ∈ (𝑧𝐻𝑤)))) → ((𝑘(〈𝑦, 𝑧〉 · 𝑤)𝑔)(〈𝑥, 𝑦〉 · 𝑤)𝑓) = (𝑘(〈𝑥, 𝑧〉 · 𝑤)(𝑔(〈𝑥, 𝑦〉 · 𝑧)𝑓))) |
| 47 | 17, 46 | sylan2b 594 |
. . . . 5
⊢ ((𝜑 ∧ (𝜓 ∧ 𝑤 ∈ 𝐵 ∧ 𝑘 ∈ (𝑧𝐻𝑤))) → ((𝑘(〈𝑦, 𝑧〉 · 𝑤)𝑔)(〈𝑥, 𝑦〉 · 𝑤)𝑓) = (𝑘(〈𝑥, 𝑧〉 · 𝑤)(𝑔(〈𝑥, 𝑦〉 · 𝑧)𝑓))) |
| 48 | 1, 2, 4, 5, 17, 18, 33, 38, 39, 47 | iscatd2 17724 |
. . . 4
⊢ (𝜑 → (𝐶 ∈ Cat ∧ (Id‘𝐶) = (𝑦 ∈ 𝐵 ↦ 1 ))) |
| 49 | 48 | simpld 494 |
. . 3
⊢ (𝜑 → 𝐶 ∈ Cat) |
| 50 | 1, 2, 3, 49 | isthincd 49085 |
. 2
⊢ (𝜑 → 𝐶 ∈ ThinCat) |
| 51 | 48 | simprd 495 |
. 2
⊢ (𝜑 → (Id‘𝐶) = (𝑦 ∈ 𝐵 ↦ 1 )) |
| 52 | 50, 51 | jca 511 |
1
⊢ (𝜑 → (𝐶 ∈ ThinCat ∧ (Id‘𝐶) = (𝑦 ∈ 𝐵 ↦ 1 ))) |