Step | Hyp | Ref
| Expression |
1 | | simpr 488 |
. 2
⊢ ((𝐶 ∈ 𝑉 ∧ ∅ = (Base‘𝐶)) → ∅ =
(Base‘𝐶)) |
2 | | eqidd 2739 |
. 2
⊢ ((𝐶 ∈ 𝑉 ∧ ∅ = (Base‘𝐶)) → (Hom ‘𝐶) = (Hom ‘𝐶)) |
3 | | eqidd 2739 |
. 2
⊢ ((𝐶 ∈ 𝑉 ∧ ∅ = (Base‘𝐶)) → (comp‘𝐶) = (comp‘𝐶)) |
4 | | simpl 486 |
. 2
⊢ ((𝐶 ∈ 𝑉 ∧ ∅ = (Base‘𝐶)) → 𝐶 ∈ 𝑉) |
5 | | noel 4217 |
. . . 4
⊢ ¬
𝑥 ∈
∅ |
6 | 5 | pm2.21i 119 |
. . 3
⊢ (𝑥 ∈ ∅ → ∅
∈ (𝑥(Hom ‘𝐶)𝑥)) |
7 | 6 | adantl 485 |
. 2
⊢ (((𝐶 ∈ 𝑉 ∧ ∅ = (Base‘𝐶)) ∧ 𝑥 ∈ ∅) → ∅ ∈ (𝑥(Hom ‘𝐶)𝑥)) |
8 | | simpr1 1195 |
. . 3
⊢ (((𝐶 ∈ 𝑉 ∧ ∅ = (Base‘𝐶)) ∧ (𝑥 ∈ ∅ ∧ 𝑦 ∈ ∅ ∧ 𝑓 ∈ (𝑦(Hom ‘𝐶)𝑥))) → 𝑥 ∈ ∅) |
9 | 5 | pm2.21i 119 |
. . 3
⊢ (𝑥 ∈ ∅ →
(∅(〈𝑦, 𝑥〉(comp‘𝐶)𝑥)𝑓) = 𝑓) |
10 | 8, 9 | syl 17 |
. 2
⊢ (((𝐶 ∈ 𝑉 ∧ ∅ = (Base‘𝐶)) ∧ (𝑥 ∈ ∅ ∧ 𝑦 ∈ ∅ ∧ 𝑓 ∈ (𝑦(Hom ‘𝐶)𝑥))) → (∅(〈𝑦, 𝑥〉(comp‘𝐶)𝑥)𝑓) = 𝑓) |
11 | | simpr1 1195 |
. . 3
⊢ (((𝐶 ∈ 𝑉 ∧ ∅ = (Base‘𝐶)) ∧ (𝑥 ∈ ∅ ∧ 𝑦 ∈ ∅ ∧ 𝑓 ∈ (𝑥(Hom ‘𝐶)𝑦))) → 𝑥 ∈ ∅) |
12 | 5 | pm2.21i 119 |
. . 3
⊢ (𝑥 ∈ ∅ → (𝑓(〈𝑥, 𝑥〉(comp‘𝐶)𝑦)∅) = 𝑓) |
13 | 11, 12 | syl 17 |
. 2
⊢ (((𝐶 ∈ 𝑉 ∧ ∅ = (Base‘𝐶)) ∧ (𝑥 ∈ ∅ ∧ 𝑦 ∈ ∅ ∧ 𝑓 ∈ (𝑥(Hom ‘𝐶)𝑦))) → (𝑓(〈𝑥, 𝑥〉(comp‘𝐶)𝑦)∅) = 𝑓) |
14 | | simp21 1207 |
. . 3
⊢ (((𝐶 ∈ 𝑉 ∧ ∅ = (Base‘𝐶)) ∧ (𝑥 ∈ ∅ ∧ 𝑦 ∈ ∅ ∧ 𝑧 ∈ ∅) ∧ (𝑓 ∈ (𝑥(Hom ‘𝐶)𝑦) ∧ 𝑔 ∈ (𝑦(Hom ‘𝐶)𝑧))) → 𝑥 ∈ ∅) |
15 | 5 | pm2.21i 119 |
. . 3
⊢ (𝑥 ∈ ∅ → (𝑔(〈𝑥, 𝑦〉(comp‘𝐶)𝑧)𝑓) ∈ (𝑥(Hom ‘𝐶)𝑧)) |
16 | 14, 15 | syl 17 |
. 2
⊢ (((𝐶 ∈ 𝑉 ∧ ∅ = (Base‘𝐶)) ∧ (𝑥 ∈ ∅ ∧ 𝑦 ∈ ∅ ∧ 𝑧 ∈ ∅) ∧ (𝑓 ∈ (𝑥(Hom ‘𝐶)𝑦) ∧ 𝑔 ∈ (𝑦(Hom ‘𝐶)𝑧))) → (𝑔(〈𝑥, 𝑦〉(comp‘𝐶)𝑧)𝑓) ∈ (𝑥(Hom ‘𝐶)𝑧)) |
17 | | simp2ll 1241 |
. . 3
⊢ (((𝐶 ∈ 𝑉 ∧ ∅ = (Base‘𝐶)) ∧ ((𝑥 ∈ ∅ ∧ 𝑦 ∈ ∅) ∧ (𝑧 ∈ ∅ ∧ 𝑤 ∈ ∅)) ∧ (𝑓 ∈ (𝑥(Hom ‘𝐶)𝑦) ∧ 𝑔 ∈ (𝑦(Hom ‘𝐶)𝑧) ∧ ℎ ∈ (𝑧(Hom ‘𝐶)𝑤))) → 𝑥 ∈ ∅) |
18 | 5 | pm2.21i 119 |
. . 3
⊢ (𝑥 ∈ ∅ → ((ℎ(〈𝑦, 𝑧〉(comp‘𝐶)𝑤)𝑔)(〈𝑥, 𝑦〉(comp‘𝐶)𝑤)𝑓) = (ℎ(〈𝑥, 𝑧〉(comp‘𝐶)𝑤)(𝑔(〈𝑥, 𝑦〉(comp‘𝐶)𝑧)𝑓))) |
19 | 17, 18 | syl 17 |
. 2
⊢ (((𝐶 ∈ 𝑉 ∧ ∅ = (Base‘𝐶)) ∧ ((𝑥 ∈ ∅ ∧ 𝑦 ∈ ∅) ∧ (𝑧 ∈ ∅ ∧ 𝑤 ∈ ∅)) ∧ (𝑓 ∈ (𝑥(Hom ‘𝐶)𝑦) ∧ 𝑔 ∈ (𝑦(Hom ‘𝐶)𝑧) ∧ ℎ ∈ (𝑧(Hom ‘𝐶)𝑤))) → ((ℎ(〈𝑦, 𝑧〉(comp‘𝐶)𝑤)𝑔)(〈𝑥, 𝑦〉(comp‘𝐶)𝑤)𝑓) = (ℎ(〈𝑥, 𝑧〉(comp‘𝐶)𝑤)(𝑔(〈𝑥, 𝑦〉(comp‘𝐶)𝑧)𝑓))) |
20 | 1, 2, 3, 4, 7, 10,
13, 16, 19 | iscatd 17040 |
1
⊢ ((𝐶 ∈ 𝑉 ∧ ∅ = (Base‘𝐶)) → 𝐶 ∈ Cat) |