| Step | Hyp | Ref
| Expression |
| 1 | | setccat.c |
. . 3
⊢ 𝐶 = (SetCat‘𝑈) |
| 2 | | id 22 |
. . 3
⊢ (𝑈 ∈ 𝑉 → 𝑈 ∈ 𝑉) |
| 3 | 1, 2 | setcbas 18123 |
. 2
⊢ (𝑈 ∈ 𝑉 → 𝑈 = (Base‘𝐶)) |
| 4 | | eqidd 2738 |
. 2
⊢ (𝑈 ∈ 𝑉 → (Hom ‘𝐶) = (Hom ‘𝐶)) |
| 5 | | eqidd 2738 |
. 2
⊢ (𝑈 ∈ 𝑉 → (comp‘𝐶) = (comp‘𝐶)) |
| 6 | 1 | fvexi 6920 |
. . 3
⊢ 𝐶 ∈ V |
| 7 | 6 | a1i 11 |
. 2
⊢ (𝑈 ∈ 𝑉 → 𝐶 ∈ V) |
| 8 | | biid 261 |
. 2
⊢ (((𝑤 ∈ 𝑈 ∧ 𝑥 ∈ 𝑈) ∧ (𝑦 ∈ 𝑈 ∧ 𝑧 ∈ 𝑈) ∧ (𝑓 ∈ (𝑤(Hom ‘𝐶)𝑥) ∧ 𝑔 ∈ (𝑥(Hom ‘𝐶)𝑦) ∧ ℎ ∈ (𝑦(Hom ‘𝐶)𝑧))) ↔ ((𝑤 ∈ 𝑈 ∧ 𝑥 ∈ 𝑈) ∧ (𝑦 ∈ 𝑈 ∧ 𝑧 ∈ 𝑈) ∧ (𝑓 ∈ (𝑤(Hom ‘𝐶)𝑥) ∧ 𝑔 ∈ (𝑥(Hom ‘𝐶)𝑦) ∧ ℎ ∈ (𝑦(Hom ‘𝐶)𝑧)))) |
| 9 | | f1oi 6886 |
. . . 4
⊢ ( I
↾ 𝑥):𝑥–1-1-onto→𝑥 |
| 10 | | f1of 6848 |
. . . 4
⊢ (( I
↾ 𝑥):𝑥–1-1-onto→𝑥 → ( I ↾ 𝑥):𝑥⟶𝑥) |
| 11 | 9, 10 | mp1i 13 |
. . 3
⊢ ((𝑈 ∈ 𝑉 ∧ 𝑥 ∈ 𝑈) → ( I ↾ 𝑥):𝑥⟶𝑥) |
| 12 | | simpl 482 |
. . . 4
⊢ ((𝑈 ∈ 𝑉 ∧ 𝑥 ∈ 𝑈) → 𝑈 ∈ 𝑉) |
| 13 | | eqid 2737 |
. . . 4
⊢ (Hom
‘𝐶) = (Hom
‘𝐶) |
| 14 | | simpr 484 |
. . . 4
⊢ ((𝑈 ∈ 𝑉 ∧ 𝑥 ∈ 𝑈) → 𝑥 ∈ 𝑈) |
| 15 | 1, 12, 13, 14, 14 | elsetchom 18126 |
. . 3
⊢ ((𝑈 ∈ 𝑉 ∧ 𝑥 ∈ 𝑈) → (( I ↾ 𝑥) ∈ (𝑥(Hom ‘𝐶)𝑥) ↔ ( I ↾ 𝑥):𝑥⟶𝑥)) |
| 16 | 11, 15 | mpbird 257 |
. 2
⊢ ((𝑈 ∈ 𝑉 ∧ 𝑥 ∈ 𝑈) → ( I ↾ 𝑥) ∈ (𝑥(Hom ‘𝐶)𝑥)) |
| 17 | | simpl 482 |
. . . 4
⊢ ((𝑈 ∈ 𝑉 ∧ ((𝑤 ∈ 𝑈 ∧ 𝑥 ∈ 𝑈) ∧ (𝑦 ∈ 𝑈 ∧ 𝑧 ∈ 𝑈) ∧ (𝑓 ∈ (𝑤(Hom ‘𝐶)𝑥) ∧ 𝑔 ∈ (𝑥(Hom ‘𝐶)𝑦) ∧ ℎ ∈ (𝑦(Hom ‘𝐶)𝑧)))) → 𝑈 ∈ 𝑉) |
| 18 | | eqid 2737 |
. . . 4
⊢
(comp‘𝐶) =
(comp‘𝐶) |
| 19 | | simpr1l 1231 |
. . . 4
⊢ ((𝑈 ∈ 𝑉 ∧ ((𝑤 ∈ 𝑈 ∧ 𝑥 ∈ 𝑈) ∧ (𝑦 ∈ 𝑈 ∧ 𝑧 ∈ 𝑈) ∧ (𝑓 ∈ (𝑤(Hom ‘𝐶)𝑥) ∧ 𝑔 ∈ (𝑥(Hom ‘𝐶)𝑦) ∧ ℎ ∈ (𝑦(Hom ‘𝐶)𝑧)))) → 𝑤 ∈ 𝑈) |
| 20 | | simpr1r 1232 |
. . . 4
⊢ ((𝑈 ∈ 𝑉 ∧ ((𝑤 ∈ 𝑈 ∧ 𝑥 ∈ 𝑈) ∧ (𝑦 ∈ 𝑈 ∧ 𝑧 ∈ 𝑈) ∧ (𝑓 ∈ (𝑤(Hom ‘𝐶)𝑥) ∧ 𝑔 ∈ (𝑥(Hom ‘𝐶)𝑦) ∧ ℎ ∈ (𝑦(Hom ‘𝐶)𝑧)))) → 𝑥 ∈ 𝑈) |
| 21 | | simpr31 1264 |
. . . . 5
⊢ ((𝑈 ∈ 𝑉 ∧ ((𝑤 ∈ 𝑈 ∧ 𝑥 ∈ 𝑈) ∧ (𝑦 ∈ 𝑈 ∧ 𝑧 ∈ 𝑈) ∧ (𝑓 ∈ (𝑤(Hom ‘𝐶)𝑥) ∧ 𝑔 ∈ (𝑥(Hom ‘𝐶)𝑦) ∧ ℎ ∈ (𝑦(Hom ‘𝐶)𝑧)))) → 𝑓 ∈ (𝑤(Hom ‘𝐶)𝑥)) |
| 22 | 1, 17, 13, 19, 20 | elsetchom 18126 |
. . . . 5
⊢ ((𝑈 ∈ 𝑉 ∧ ((𝑤 ∈ 𝑈 ∧ 𝑥 ∈ 𝑈) ∧ (𝑦 ∈ 𝑈 ∧ 𝑧 ∈ 𝑈) ∧ (𝑓 ∈ (𝑤(Hom ‘𝐶)𝑥) ∧ 𝑔 ∈ (𝑥(Hom ‘𝐶)𝑦) ∧ ℎ ∈ (𝑦(Hom ‘𝐶)𝑧)))) → (𝑓 ∈ (𝑤(Hom ‘𝐶)𝑥) ↔ 𝑓:𝑤⟶𝑥)) |
| 23 | 21, 22 | mpbid 232 |
. . . 4
⊢ ((𝑈 ∈ 𝑉 ∧ ((𝑤 ∈ 𝑈 ∧ 𝑥 ∈ 𝑈) ∧ (𝑦 ∈ 𝑈 ∧ 𝑧 ∈ 𝑈) ∧ (𝑓 ∈ (𝑤(Hom ‘𝐶)𝑥) ∧ 𝑔 ∈ (𝑥(Hom ‘𝐶)𝑦) ∧ ℎ ∈ (𝑦(Hom ‘𝐶)𝑧)))) → 𝑓:𝑤⟶𝑥) |
| 24 | 9, 10 | mp1i 13 |
. . . 4
⊢ ((𝑈 ∈ 𝑉 ∧ ((𝑤 ∈ 𝑈 ∧ 𝑥 ∈ 𝑈) ∧ (𝑦 ∈ 𝑈 ∧ 𝑧 ∈ 𝑈) ∧ (𝑓 ∈ (𝑤(Hom ‘𝐶)𝑥) ∧ 𝑔 ∈ (𝑥(Hom ‘𝐶)𝑦) ∧ ℎ ∈ (𝑦(Hom ‘𝐶)𝑧)))) → ( I ↾ 𝑥):𝑥⟶𝑥) |
| 25 | 1, 17, 18, 19, 20, 20, 23, 24 | setcco 18128 |
. . 3
⊢ ((𝑈 ∈ 𝑉 ∧ ((𝑤 ∈ 𝑈 ∧ 𝑥 ∈ 𝑈) ∧ (𝑦 ∈ 𝑈 ∧ 𝑧 ∈ 𝑈) ∧ (𝑓 ∈ (𝑤(Hom ‘𝐶)𝑥) ∧ 𝑔 ∈ (𝑥(Hom ‘𝐶)𝑦) ∧ ℎ ∈ (𝑦(Hom ‘𝐶)𝑧)))) → (( I ↾ 𝑥)(〈𝑤, 𝑥〉(comp‘𝐶)𝑥)𝑓) = (( I ↾ 𝑥) ∘ 𝑓)) |
| 26 | | fcoi2 6783 |
. . . 4
⊢ (𝑓:𝑤⟶𝑥 → (( I ↾ 𝑥) ∘ 𝑓) = 𝑓) |
| 27 | 23, 26 | syl 17 |
. . 3
⊢ ((𝑈 ∈ 𝑉 ∧ ((𝑤 ∈ 𝑈 ∧ 𝑥 ∈ 𝑈) ∧ (𝑦 ∈ 𝑈 ∧ 𝑧 ∈ 𝑈) ∧ (𝑓 ∈ (𝑤(Hom ‘𝐶)𝑥) ∧ 𝑔 ∈ (𝑥(Hom ‘𝐶)𝑦) ∧ ℎ ∈ (𝑦(Hom ‘𝐶)𝑧)))) → (( I ↾ 𝑥) ∘ 𝑓) = 𝑓) |
| 28 | 25, 27 | eqtrd 2777 |
. 2
⊢ ((𝑈 ∈ 𝑉 ∧ ((𝑤 ∈ 𝑈 ∧ 𝑥 ∈ 𝑈) ∧ (𝑦 ∈ 𝑈 ∧ 𝑧 ∈ 𝑈) ∧ (𝑓 ∈ (𝑤(Hom ‘𝐶)𝑥) ∧ 𝑔 ∈ (𝑥(Hom ‘𝐶)𝑦) ∧ ℎ ∈ (𝑦(Hom ‘𝐶)𝑧)))) → (( I ↾ 𝑥)(〈𝑤, 𝑥〉(comp‘𝐶)𝑥)𝑓) = 𝑓) |
| 29 | | simpr2l 1233 |
. . . 4
⊢ ((𝑈 ∈ 𝑉 ∧ ((𝑤 ∈ 𝑈 ∧ 𝑥 ∈ 𝑈) ∧ (𝑦 ∈ 𝑈 ∧ 𝑧 ∈ 𝑈) ∧ (𝑓 ∈ (𝑤(Hom ‘𝐶)𝑥) ∧ 𝑔 ∈ (𝑥(Hom ‘𝐶)𝑦) ∧ ℎ ∈ (𝑦(Hom ‘𝐶)𝑧)))) → 𝑦 ∈ 𝑈) |
| 30 | | simpr32 1265 |
. . . . 5
⊢ ((𝑈 ∈ 𝑉 ∧ ((𝑤 ∈ 𝑈 ∧ 𝑥 ∈ 𝑈) ∧ (𝑦 ∈ 𝑈 ∧ 𝑧 ∈ 𝑈) ∧ (𝑓 ∈ (𝑤(Hom ‘𝐶)𝑥) ∧ 𝑔 ∈ (𝑥(Hom ‘𝐶)𝑦) ∧ ℎ ∈ (𝑦(Hom ‘𝐶)𝑧)))) → 𝑔 ∈ (𝑥(Hom ‘𝐶)𝑦)) |
| 31 | 1, 17, 13, 20, 29 | elsetchom 18126 |
. . . . 5
⊢ ((𝑈 ∈ 𝑉 ∧ ((𝑤 ∈ 𝑈 ∧ 𝑥 ∈ 𝑈) ∧ (𝑦 ∈ 𝑈 ∧ 𝑧 ∈ 𝑈) ∧ (𝑓 ∈ (𝑤(Hom ‘𝐶)𝑥) ∧ 𝑔 ∈ (𝑥(Hom ‘𝐶)𝑦) ∧ ℎ ∈ (𝑦(Hom ‘𝐶)𝑧)))) → (𝑔 ∈ (𝑥(Hom ‘𝐶)𝑦) ↔ 𝑔:𝑥⟶𝑦)) |
| 32 | 30, 31 | mpbid 232 |
. . . 4
⊢ ((𝑈 ∈ 𝑉 ∧ ((𝑤 ∈ 𝑈 ∧ 𝑥 ∈ 𝑈) ∧ (𝑦 ∈ 𝑈 ∧ 𝑧 ∈ 𝑈) ∧ (𝑓 ∈ (𝑤(Hom ‘𝐶)𝑥) ∧ 𝑔 ∈ (𝑥(Hom ‘𝐶)𝑦) ∧ ℎ ∈ (𝑦(Hom ‘𝐶)𝑧)))) → 𝑔:𝑥⟶𝑦) |
| 33 | 1, 17, 18, 20, 20, 29, 24, 32 | setcco 18128 |
. . 3
⊢ ((𝑈 ∈ 𝑉 ∧ ((𝑤 ∈ 𝑈 ∧ 𝑥 ∈ 𝑈) ∧ (𝑦 ∈ 𝑈 ∧ 𝑧 ∈ 𝑈) ∧ (𝑓 ∈ (𝑤(Hom ‘𝐶)𝑥) ∧ 𝑔 ∈ (𝑥(Hom ‘𝐶)𝑦) ∧ ℎ ∈ (𝑦(Hom ‘𝐶)𝑧)))) → (𝑔(〈𝑥, 𝑥〉(comp‘𝐶)𝑦)( I ↾ 𝑥)) = (𝑔 ∘ ( I ↾ 𝑥))) |
| 34 | | fcoi1 6782 |
. . . 4
⊢ (𝑔:𝑥⟶𝑦 → (𝑔 ∘ ( I ↾ 𝑥)) = 𝑔) |
| 35 | 32, 34 | syl 17 |
. . 3
⊢ ((𝑈 ∈ 𝑉 ∧ ((𝑤 ∈ 𝑈 ∧ 𝑥 ∈ 𝑈) ∧ (𝑦 ∈ 𝑈 ∧ 𝑧 ∈ 𝑈) ∧ (𝑓 ∈ (𝑤(Hom ‘𝐶)𝑥) ∧ 𝑔 ∈ (𝑥(Hom ‘𝐶)𝑦) ∧ ℎ ∈ (𝑦(Hom ‘𝐶)𝑧)))) → (𝑔 ∘ ( I ↾ 𝑥)) = 𝑔) |
| 36 | 33, 35 | eqtrd 2777 |
. 2
⊢ ((𝑈 ∈ 𝑉 ∧ ((𝑤 ∈ 𝑈 ∧ 𝑥 ∈ 𝑈) ∧ (𝑦 ∈ 𝑈 ∧ 𝑧 ∈ 𝑈) ∧ (𝑓 ∈ (𝑤(Hom ‘𝐶)𝑥) ∧ 𝑔 ∈ (𝑥(Hom ‘𝐶)𝑦) ∧ ℎ ∈ (𝑦(Hom ‘𝐶)𝑧)))) → (𝑔(〈𝑥, 𝑥〉(comp‘𝐶)𝑦)( I ↾ 𝑥)) = 𝑔) |
| 37 | 1, 17, 18, 19, 20, 29, 23, 32 | setcco 18128 |
. . 3
⊢ ((𝑈 ∈ 𝑉 ∧ ((𝑤 ∈ 𝑈 ∧ 𝑥 ∈ 𝑈) ∧ (𝑦 ∈ 𝑈 ∧ 𝑧 ∈ 𝑈) ∧ (𝑓 ∈ (𝑤(Hom ‘𝐶)𝑥) ∧ 𝑔 ∈ (𝑥(Hom ‘𝐶)𝑦) ∧ ℎ ∈ (𝑦(Hom ‘𝐶)𝑧)))) → (𝑔(〈𝑤, 𝑥〉(comp‘𝐶)𝑦)𝑓) = (𝑔 ∘ 𝑓)) |
| 38 | | fco 6760 |
. . . . 5
⊢ ((𝑔:𝑥⟶𝑦 ∧ 𝑓:𝑤⟶𝑥) → (𝑔 ∘ 𝑓):𝑤⟶𝑦) |
| 39 | 32, 23, 38 | syl2anc 584 |
. . . 4
⊢ ((𝑈 ∈ 𝑉 ∧ ((𝑤 ∈ 𝑈 ∧ 𝑥 ∈ 𝑈) ∧ (𝑦 ∈ 𝑈 ∧ 𝑧 ∈ 𝑈) ∧ (𝑓 ∈ (𝑤(Hom ‘𝐶)𝑥) ∧ 𝑔 ∈ (𝑥(Hom ‘𝐶)𝑦) ∧ ℎ ∈ (𝑦(Hom ‘𝐶)𝑧)))) → (𝑔 ∘ 𝑓):𝑤⟶𝑦) |
| 40 | 1, 17, 13, 19, 29 | elsetchom 18126 |
. . . 4
⊢ ((𝑈 ∈ 𝑉 ∧ ((𝑤 ∈ 𝑈 ∧ 𝑥 ∈ 𝑈) ∧ (𝑦 ∈ 𝑈 ∧ 𝑧 ∈ 𝑈) ∧ (𝑓 ∈ (𝑤(Hom ‘𝐶)𝑥) ∧ 𝑔 ∈ (𝑥(Hom ‘𝐶)𝑦) ∧ ℎ ∈ (𝑦(Hom ‘𝐶)𝑧)))) → ((𝑔 ∘ 𝑓) ∈ (𝑤(Hom ‘𝐶)𝑦) ↔ (𝑔 ∘ 𝑓):𝑤⟶𝑦)) |
| 41 | 39, 40 | mpbird 257 |
. . 3
⊢ ((𝑈 ∈ 𝑉 ∧ ((𝑤 ∈ 𝑈 ∧ 𝑥 ∈ 𝑈) ∧ (𝑦 ∈ 𝑈 ∧ 𝑧 ∈ 𝑈) ∧ (𝑓 ∈ (𝑤(Hom ‘𝐶)𝑥) ∧ 𝑔 ∈ (𝑥(Hom ‘𝐶)𝑦) ∧ ℎ ∈ (𝑦(Hom ‘𝐶)𝑧)))) → (𝑔 ∘ 𝑓) ∈ (𝑤(Hom ‘𝐶)𝑦)) |
| 42 | 37, 41 | eqeltrd 2841 |
. 2
⊢ ((𝑈 ∈ 𝑉 ∧ ((𝑤 ∈ 𝑈 ∧ 𝑥 ∈ 𝑈) ∧ (𝑦 ∈ 𝑈 ∧ 𝑧 ∈ 𝑈) ∧ (𝑓 ∈ (𝑤(Hom ‘𝐶)𝑥) ∧ 𝑔 ∈ (𝑥(Hom ‘𝐶)𝑦) ∧ ℎ ∈ (𝑦(Hom ‘𝐶)𝑧)))) → (𝑔(〈𝑤, 𝑥〉(comp‘𝐶)𝑦)𝑓) ∈ (𝑤(Hom ‘𝐶)𝑦)) |
| 43 | | coass 6285 |
. . . 4
⊢ ((ℎ ∘ 𝑔) ∘ 𝑓) = (ℎ ∘ (𝑔 ∘ 𝑓)) |
| 44 | | simpr2r 1234 |
. . . . 5
⊢ ((𝑈 ∈ 𝑉 ∧ ((𝑤 ∈ 𝑈 ∧ 𝑥 ∈ 𝑈) ∧ (𝑦 ∈ 𝑈 ∧ 𝑧 ∈ 𝑈) ∧ (𝑓 ∈ (𝑤(Hom ‘𝐶)𝑥) ∧ 𝑔 ∈ (𝑥(Hom ‘𝐶)𝑦) ∧ ℎ ∈ (𝑦(Hom ‘𝐶)𝑧)))) → 𝑧 ∈ 𝑈) |
| 45 | | simpr33 1266 |
. . . . . . 7
⊢ ((𝑈 ∈ 𝑉 ∧ ((𝑤 ∈ 𝑈 ∧ 𝑥 ∈ 𝑈) ∧ (𝑦 ∈ 𝑈 ∧ 𝑧 ∈ 𝑈) ∧ (𝑓 ∈ (𝑤(Hom ‘𝐶)𝑥) ∧ 𝑔 ∈ (𝑥(Hom ‘𝐶)𝑦) ∧ ℎ ∈ (𝑦(Hom ‘𝐶)𝑧)))) → ℎ ∈ (𝑦(Hom ‘𝐶)𝑧)) |
| 46 | 1, 17, 13, 29, 44 | elsetchom 18126 |
. . . . . . 7
⊢ ((𝑈 ∈ 𝑉 ∧ ((𝑤 ∈ 𝑈 ∧ 𝑥 ∈ 𝑈) ∧ (𝑦 ∈ 𝑈 ∧ 𝑧 ∈ 𝑈) ∧ (𝑓 ∈ (𝑤(Hom ‘𝐶)𝑥) ∧ 𝑔 ∈ (𝑥(Hom ‘𝐶)𝑦) ∧ ℎ ∈ (𝑦(Hom ‘𝐶)𝑧)))) → (ℎ ∈ (𝑦(Hom ‘𝐶)𝑧) ↔ ℎ:𝑦⟶𝑧)) |
| 47 | 45, 46 | mpbid 232 |
. . . . . 6
⊢ ((𝑈 ∈ 𝑉 ∧ ((𝑤 ∈ 𝑈 ∧ 𝑥 ∈ 𝑈) ∧ (𝑦 ∈ 𝑈 ∧ 𝑧 ∈ 𝑈) ∧ (𝑓 ∈ (𝑤(Hom ‘𝐶)𝑥) ∧ 𝑔 ∈ (𝑥(Hom ‘𝐶)𝑦) ∧ ℎ ∈ (𝑦(Hom ‘𝐶)𝑧)))) → ℎ:𝑦⟶𝑧) |
| 48 | | fco 6760 |
. . . . . 6
⊢ ((ℎ:𝑦⟶𝑧 ∧ 𝑔:𝑥⟶𝑦) → (ℎ ∘ 𝑔):𝑥⟶𝑧) |
| 49 | 47, 32, 48 | syl2anc 584 |
. . . . 5
⊢ ((𝑈 ∈ 𝑉 ∧ ((𝑤 ∈ 𝑈 ∧ 𝑥 ∈ 𝑈) ∧ (𝑦 ∈ 𝑈 ∧ 𝑧 ∈ 𝑈) ∧ (𝑓 ∈ (𝑤(Hom ‘𝐶)𝑥) ∧ 𝑔 ∈ (𝑥(Hom ‘𝐶)𝑦) ∧ ℎ ∈ (𝑦(Hom ‘𝐶)𝑧)))) → (ℎ ∘ 𝑔):𝑥⟶𝑧) |
| 50 | 1, 17, 18, 19, 20, 44, 23, 49 | setcco 18128 |
. . . 4
⊢ ((𝑈 ∈ 𝑉 ∧ ((𝑤 ∈ 𝑈 ∧ 𝑥 ∈ 𝑈) ∧ (𝑦 ∈ 𝑈 ∧ 𝑧 ∈ 𝑈) ∧ (𝑓 ∈ (𝑤(Hom ‘𝐶)𝑥) ∧ 𝑔 ∈ (𝑥(Hom ‘𝐶)𝑦) ∧ ℎ ∈ (𝑦(Hom ‘𝐶)𝑧)))) → ((ℎ ∘ 𝑔)(〈𝑤, 𝑥〉(comp‘𝐶)𝑧)𝑓) = ((ℎ ∘ 𝑔) ∘ 𝑓)) |
| 51 | 1, 17, 18, 19, 29, 44, 39, 47 | setcco 18128 |
. . . 4
⊢ ((𝑈 ∈ 𝑉 ∧ ((𝑤 ∈ 𝑈 ∧ 𝑥 ∈ 𝑈) ∧ (𝑦 ∈ 𝑈 ∧ 𝑧 ∈ 𝑈) ∧ (𝑓 ∈ (𝑤(Hom ‘𝐶)𝑥) ∧ 𝑔 ∈ (𝑥(Hom ‘𝐶)𝑦) ∧ ℎ ∈ (𝑦(Hom ‘𝐶)𝑧)))) → (ℎ(〈𝑤, 𝑦〉(comp‘𝐶)𝑧)(𝑔 ∘ 𝑓)) = (ℎ ∘ (𝑔 ∘ 𝑓))) |
| 52 | 43, 50, 51 | 3eqtr4a 2803 |
. . 3
⊢ ((𝑈 ∈ 𝑉 ∧ ((𝑤 ∈ 𝑈 ∧ 𝑥 ∈ 𝑈) ∧ (𝑦 ∈ 𝑈 ∧ 𝑧 ∈ 𝑈) ∧ (𝑓 ∈ (𝑤(Hom ‘𝐶)𝑥) ∧ 𝑔 ∈ (𝑥(Hom ‘𝐶)𝑦) ∧ ℎ ∈ (𝑦(Hom ‘𝐶)𝑧)))) → ((ℎ ∘ 𝑔)(〈𝑤, 𝑥〉(comp‘𝐶)𝑧)𝑓) = (ℎ(〈𝑤, 𝑦〉(comp‘𝐶)𝑧)(𝑔 ∘ 𝑓))) |
| 53 | 1, 17, 18, 20, 29, 44, 32, 47 | setcco 18128 |
. . . 4
⊢ ((𝑈 ∈ 𝑉 ∧ ((𝑤 ∈ 𝑈 ∧ 𝑥 ∈ 𝑈) ∧ (𝑦 ∈ 𝑈 ∧ 𝑧 ∈ 𝑈) ∧ (𝑓 ∈ (𝑤(Hom ‘𝐶)𝑥) ∧ 𝑔 ∈ (𝑥(Hom ‘𝐶)𝑦) ∧ ℎ ∈ (𝑦(Hom ‘𝐶)𝑧)))) → (ℎ(〈𝑥, 𝑦〉(comp‘𝐶)𝑧)𝑔) = (ℎ ∘ 𝑔)) |
| 54 | 53 | oveq1d 7446 |
. . 3
⊢ ((𝑈 ∈ 𝑉 ∧ ((𝑤 ∈ 𝑈 ∧ 𝑥 ∈ 𝑈) ∧ (𝑦 ∈ 𝑈 ∧ 𝑧 ∈ 𝑈) ∧ (𝑓 ∈ (𝑤(Hom ‘𝐶)𝑥) ∧ 𝑔 ∈ (𝑥(Hom ‘𝐶)𝑦) ∧ ℎ ∈ (𝑦(Hom ‘𝐶)𝑧)))) → ((ℎ(〈𝑥, 𝑦〉(comp‘𝐶)𝑧)𝑔)(〈𝑤, 𝑥〉(comp‘𝐶)𝑧)𝑓) = ((ℎ ∘ 𝑔)(〈𝑤, 𝑥〉(comp‘𝐶)𝑧)𝑓)) |
| 55 | 37 | oveq2d 7447 |
. . 3
⊢ ((𝑈 ∈ 𝑉 ∧ ((𝑤 ∈ 𝑈 ∧ 𝑥 ∈ 𝑈) ∧ (𝑦 ∈ 𝑈 ∧ 𝑧 ∈ 𝑈) ∧ (𝑓 ∈ (𝑤(Hom ‘𝐶)𝑥) ∧ 𝑔 ∈ (𝑥(Hom ‘𝐶)𝑦) ∧ ℎ ∈ (𝑦(Hom ‘𝐶)𝑧)))) → (ℎ(〈𝑤, 𝑦〉(comp‘𝐶)𝑧)(𝑔(〈𝑤, 𝑥〉(comp‘𝐶)𝑦)𝑓)) = (ℎ(〈𝑤, 𝑦〉(comp‘𝐶)𝑧)(𝑔 ∘ 𝑓))) |
| 56 | 52, 54, 55 | 3eqtr4d 2787 |
. 2
⊢ ((𝑈 ∈ 𝑉 ∧ ((𝑤 ∈ 𝑈 ∧ 𝑥 ∈ 𝑈) ∧ (𝑦 ∈ 𝑈 ∧ 𝑧 ∈ 𝑈) ∧ (𝑓 ∈ (𝑤(Hom ‘𝐶)𝑥) ∧ 𝑔 ∈ (𝑥(Hom ‘𝐶)𝑦) ∧ ℎ ∈ (𝑦(Hom ‘𝐶)𝑧)))) → ((ℎ(〈𝑥, 𝑦〉(comp‘𝐶)𝑧)𝑔)(〈𝑤, 𝑥〉(comp‘𝐶)𝑧)𝑓) = (ℎ(〈𝑤, 𝑦〉(comp‘𝐶)𝑧)(𝑔(〈𝑤, 𝑥〉(comp‘𝐶)𝑦)𝑓))) |
| 57 | 3, 4, 5, 7, 8, 16,
28, 36, 42, 56 | iscatd2 17724 |
1
⊢ (𝑈 ∈ 𝑉 → (𝐶 ∈ Cat ∧ (Id‘𝐶) = (𝑥 ∈ 𝑈 ↦ ( I ↾ 𝑥)))) |