Step | Hyp | Ref
| Expression |
1 | | simpl 472 |
. . . . . . . . . . 11
⊢ (((𝑔(〈𝑥, 𝑦〉(comp‘𝐶)𝑧)𝑓) ∈ (𝑥(Hom ‘𝐶)𝑧) ∧ ∀𝑤 ∈ (Base‘𝐶)∀ℎ ∈ (𝑧(Hom ‘𝐶)𝑤)((ℎ(〈𝑦, 𝑧〉(comp‘𝐶)𝑤)𝑔)(〈𝑥, 𝑦〉(comp‘𝐶)𝑤)𝑓) = (ℎ(〈𝑥, 𝑧〉(comp‘𝐶)𝑤)(𝑔(〈𝑥, 𝑦〉(comp‘𝐶)𝑧)𝑓))) → (𝑔(〈𝑥, 𝑦〉(comp‘𝐶)𝑧)𝑓) ∈ (𝑥(Hom ‘𝐶)𝑧)) |
2 | 1 | ralimi 2936 |
. . . . . . . . . 10
⊢
(∀𝑔 ∈
(𝑦(Hom ‘𝐶)𝑧)((𝑔(〈𝑥, 𝑦〉(comp‘𝐶)𝑧)𝑓) ∈ (𝑥(Hom ‘𝐶)𝑧) ∧ ∀𝑤 ∈ (Base‘𝐶)∀ℎ ∈ (𝑧(Hom ‘𝐶)𝑤)((ℎ(〈𝑦, 𝑧〉(comp‘𝐶)𝑤)𝑔)(〈𝑥, 𝑦〉(comp‘𝐶)𝑤)𝑓) = (ℎ(〈𝑥, 𝑧〉(comp‘𝐶)𝑤)(𝑔(〈𝑥, 𝑦〉(comp‘𝐶)𝑧)𝑓))) → ∀𝑔 ∈ (𝑦(Hom ‘𝐶)𝑧)(𝑔(〈𝑥, 𝑦〉(comp‘𝐶)𝑧)𝑓) ∈ (𝑥(Hom ‘𝐶)𝑧)) |
3 | 2 | ralimi 2936 |
. . . . . . . . 9
⊢
(∀𝑓 ∈
(𝑥(Hom ‘𝐶)𝑦)∀𝑔 ∈ (𝑦(Hom ‘𝐶)𝑧)((𝑔(〈𝑥, 𝑦〉(comp‘𝐶)𝑧)𝑓) ∈ (𝑥(Hom ‘𝐶)𝑧) ∧ ∀𝑤 ∈ (Base‘𝐶)∀ℎ ∈ (𝑧(Hom ‘𝐶)𝑤)((ℎ(〈𝑦, 𝑧〉(comp‘𝐶)𝑤)𝑔)(〈𝑥, 𝑦〉(comp‘𝐶)𝑤)𝑓) = (ℎ(〈𝑥, 𝑧〉(comp‘𝐶)𝑤)(𝑔(〈𝑥, 𝑦〉(comp‘𝐶)𝑧)𝑓))) → ∀𝑓 ∈ (𝑥(Hom ‘𝐶)𝑦)∀𝑔 ∈ (𝑦(Hom ‘𝐶)𝑧)(𝑔(〈𝑥, 𝑦〉(comp‘𝐶)𝑧)𝑓) ∈ (𝑥(Hom ‘𝐶)𝑧)) |
4 | 3 | ralimi 2936 |
. . . . . . . 8
⊢
(∀𝑧 ∈
(Base‘𝐶)∀𝑓 ∈ (𝑥(Hom ‘𝐶)𝑦)∀𝑔 ∈ (𝑦(Hom ‘𝐶)𝑧)((𝑔(〈𝑥, 𝑦〉(comp‘𝐶)𝑧)𝑓) ∈ (𝑥(Hom ‘𝐶)𝑧) ∧ ∀𝑤 ∈ (Base‘𝐶)∀ℎ ∈ (𝑧(Hom ‘𝐶)𝑤)((ℎ(〈𝑦, 𝑧〉(comp‘𝐶)𝑤)𝑔)(〈𝑥, 𝑦〉(comp‘𝐶)𝑤)𝑓) = (ℎ(〈𝑥, 𝑧〉(comp‘𝐶)𝑤)(𝑔(〈𝑥, 𝑦〉(comp‘𝐶)𝑧)𝑓))) → ∀𝑧 ∈ (Base‘𝐶)∀𝑓 ∈ (𝑥(Hom ‘𝐶)𝑦)∀𝑔 ∈ (𝑦(Hom ‘𝐶)𝑧)(𝑔(〈𝑥, 𝑦〉(comp‘𝐶)𝑧)𝑓) ∈ (𝑥(Hom ‘𝐶)𝑧)) |
5 | 4 | ralimi 2936 |
. . . . . . 7
⊢
(∀𝑦 ∈
(Base‘𝐶)∀𝑧 ∈ (Base‘𝐶)∀𝑓 ∈ (𝑥(Hom ‘𝐶)𝑦)∀𝑔 ∈ (𝑦(Hom ‘𝐶)𝑧)((𝑔(〈𝑥, 𝑦〉(comp‘𝐶)𝑧)𝑓) ∈ (𝑥(Hom ‘𝐶)𝑧) ∧ ∀𝑤 ∈ (Base‘𝐶)∀ℎ ∈ (𝑧(Hom ‘𝐶)𝑤)((ℎ(〈𝑦, 𝑧〉(comp‘𝐶)𝑤)𝑔)(〈𝑥, 𝑦〉(comp‘𝐶)𝑤)𝑓) = (ℎ(〈𝑥, 𝑧〉(comp‘𝐶)𝑤)(𝑔(〈𝑥, 𝑦〉(comp‘𝐶)𝑧)𝑓))) → ∀𝑦 ∈ (Base‘𝐶)∀𝑧 ∈ (Base‘𝐶)∀𝑓 ∈ (𝑥(Hom ‘𝐶)𝑦)∀𝑔 ∈ (𝑦(Hom ‘𝐶)𝑧)(𝑔(〈𝑥, 𝑦〉(comp‘𝐶)𝑧)𝑓) ∈ (𝑥(Hom ‘𝐶)𝑧)) |
6 | 5 | adantl 481 |
. . . . . 6
⊢
((∃𝑔 ∈
(𝑥(Hom ‘𝐶)𝑥)∀𝑦 ∈ (Base‘𝐶)(∀𝑓 ∈ (𝑦(Hom ‘𝐶)𝑥)(𝑔(〈𝑦, 𝑥〉(comp‘𝐶)𝑥)𝑓) = 𝑓 ∧ ∀𝑓 ∈ (𝑥(Hom ‘𝐶)𝑦)(𝑓(〈𝑥, 𝑥〉(comp‘𝐶)𝑦)𝑔) = 𝑓) ∧ ∀𝑦 ∈ (Base‘𝐶)∀𝑧 ∈ (Base‘𝐶)∀𝑓 ∈ (𝑥(Hom ‘𝐶)𝑦)∀𝑔 ∈ (𝑦(Hom ‘𝐶)𝑧)((𝑔(〈𝑥, 𝑦〉(comp‘𝐶)𝑧)𝑓) ∈ (𝑥(Hom ‘𝐶)𝑧) ∧ ∀𝑤 ∈ (Base‘𝐶)∀ℎ ∈ (𝑧(Hom ‘𝐶)𝑤)((ℎ(〈𝑦, 𝑧〉(comp‘𝐶)𝑤)𝑔)(〈𝑥, 𝑦〉(comp‘𝐶)𝑤)𝑓) = (ℎ(〈𝑥, 𝑧〉(comp‘𝐶)𝑤)(𝑔(〈𝑥, 𝑦〉(comp‘𝐶)𝑧)𝑓)))) → ∀𝑦 ∈ (Base‘𝐶)∀𝑧 ∈ (Base‘𝐶)∀𝑓 ∈ (𝑥(Hom ‘𝐶)𝑦)∀𝑔 ∈ (𝑦(Hom ‘𝐶)𝑧)(𝑔(〈𝑥, 𝑦〉(comp‘𝐶)𝑧)𝑓) ∈ (𝑥(Hom ‘𝐶)𝑧)) |
7 | 6 | ralimi 2936 |
. . . . 5
⊢
(∀𝑥 ∈
(Base‘𝐶)(∃𝑔 ∈ (𝑥(Hom ‘𝐶)𝑥)∀𝑦 ∈ (Base‘𝐶)(∀𝑓 ∈ (𝑦(Hom ‘𝐶)𝑥)(𝑔(〈𝑦, 𝑥〉(comp‘𝐶)𝑥)𝑓) = 𝑓 ∧ ∀𝑓 ∈ (𝑥(Hom ‘𝐶)𝑦)(𝑓(〈𝑥, 𝑥〉(comp‘𝐶)𝑦)𝑔) = 𝑓) ∧ ∀𝑦 ∈ (Base‘𝐶)∀𝑧 ∈ (Base‘𝐶)∀𝑓 ∈ (𝑥(Hom ‘𝐶)𝑦)∀𝑔 ∈ (𝑦(Hom ‘𝐶)𝑧)((𝑔(〈𝑥, 𝑦〉(comp‘𝐶)𝑧)𝑓) ∈ (𝑥(Hom ‘𝐶)𝑧) ∧ ∀𝑤 ∈ (Base‘𝐶)∀ℎ ∈ (𝑧(Hom ‘𝐶)𝑤)((ℎ(〈𝑦, 𝑧〉(comp‘𝐶)𝑤)𝑔)(〈𝑥, 𝑦〉(comp‘𝐶)𝑤)𝑓) = (ℎ(〈𝑥, 𝑧〉(comp‘𝐶)𝑤)(𝑔(〈𝑥, 𝑦〉(comp‘𝐶)𝑧)𝑓)))) → ∀𝑥 ∈ (Base‘𝐶)∀𝑦 ∈ (Base‘𝐶)∀𝑧 ∈ (Base‘𝐶)∀𝑓 ∈ (𝑥(Hom ‘𝐶)𝑦)∀𝑔 ∈ (𝑦(Hom ‘𝐶)𝑧)(𝑔(〈𝑥, 𝑦〉(comp‘𝐶)𝑧)𝑓) ∈ (𝑥(Hom ‘𝐶)𝑧)) |
8 | 7 | a1i 11 |
. . . 4
⊢ (𝜑 → (∀𝑥 ∈ (Base‘𝐶)(∃𝑔 ∈ (𝑥(Hom ‘𝐶)𝑥)∀𝑦 ∈ (Base‘𝐶)(∀𝑓 ∈ (𝑦(Hom ‘𝐶)𝑥)(𝑔(〈𝑦, 𝑥〉(comp‘𝐶)𝑥)𝑓) = 𝑓 ∧ ∀𝑓 ∈ (𝑥(Hom ‘𝐶)𝑦)(𝑓(〈𝑥, 𝑥〉(comp‘𝐶)𝑦)𝑔) = 𝑓) ∧ ∀𝑦 ∈ (Base‘𝐶)∀𝑧 ∈ (Base‘𝐶)∀𝑓 ∈ (𝑥(Hom ‘𝐶)𝑦)∀𝑔 ∈ (𝑦(Hom ‘𝐶)𝑧)((𝑔(〈𝑥, 𝑦〉(comp‘𝐶)𝑧)𝑓) ∈ (𝑥(Hom ‘𝐶)𝑧) ∧ ∀𝑤 ∈ (Base‘𝐶)∀ℎ ∈ (𝑧(Hom ‘𝐶)𝑤)((ℎ(〈𝑦, 𝑧〉(comp‘𝐶)𝑤)𝑔)(〈𝑥, 𝑦〉(comp‘𝐶)𝑤)𝑓) = (ℎ(〈𝑥, 𝑧〉(comp‘𝐶)𝑤)(𝑔(〈𝑥, 𝑦〉(comp‘𝐶)𝑧)𝑓)))) → ∀𝑥 ∈ (Base‘𝐶)∀𝑦 ∈ (Base‘𝐶)∀𝑧 ∈ (Base‘𝐶)∀𝑓 ∈ (𝑥(Hom ‘𝐶)𝑦)∀𝑔 ∈ (𝑦(Hom ‘𝐶)𝑧)(𝑔(〈𝑥, 𝑦〉(comp‘𝐶)𝑧)𝑓) ∈ (𝑥(Hom ‘𝐶)𝑧))) |
9 | | simpl 472 |
. . . . . . . . . . 11
⊢ (((𝑔(〈𝑥, 𝑦〉(comp‘𝐶)𝑧)𝑓) ∈ (𝑥(Hom ‘𝐶)𝑧) ∧ ∀𝑤 ∈ (Base‘𝐶)∀ℎ ∈ (𝑧(Hom ‘𝐶)𝑤)((ℎ(〈𝑦, 𝑧〉(comp‘𝐶)𝑤)𝑔)(〈𝑥, 𝑦〉(comp‘𝐷)𝑤)𝑓) = (ℎ(〈𝑥, 𝑧〉(comp‘𝐷)𝑤)(𝑔(〈𝑥, 𝑦〉(comp‘𝐶)𝑧)𝑓))) → (𝑔(〈𝑥, 𝑦〉(comp‘𝐶)𝑧)𝑓) ∈ (𝑥(Hom ‘𝐶)𝑧)) |
10 | 9 | ralimi 2936 |
. . . . . . . . . 10
⊢
(∀𝑔 ∈
(𝑦(Hom ‘𝐶)𝑧)((𝑔(〈𝑥, 𝑦〉(comp‘𝐶)𝑧)𝑓) ∈ (𝑥(Hom ‘𝐶)𝑧) ∧ ∀𝑤 ∈ (Base‘𝐶)∀ℎ ∈ (𝑧(Hom ‘𝐶)𝑤)((ℎ(〈𝑦, 𝑧〉(comp‘𝐶)𝑤)𝑔)(〈𝑥, 𝑦〉(comp‘𝐷)𝑤)𝑓) = (ℎ(〈𝑥, 𝑧〉(comp‘𝐷)𝑤)(𝑔(〈𝑥, 𝑦〉(comp‘𝐶)𝑧)𝑓))) → ∀𝑔 ∈ (𝑦(Hom ‘𝐶)𝑧)(𝑔(〈𝑥, 𝑦〉(comp‘𝐶)𝑧)𝑓) ∈ (𝑥(Hom ‘𝐶)𝑧)) |
11 | 10 | ralimi 2936 |
. . . . . . . . 9
⊢
(∀𝑓 ∈
(𝑥(Hom ‘𝐶)𝑦)∀𝑔 ∈ (𝑦(Hom ‘𝐶)𝑧)((𝑔(〈𝑥, 𝑦〉(comp‘𝐶)𝑧)𝑓) ∈ (𝑥(Hom ‘𝐶)𝑧) ∧ ∀𝑤 ∈ (Base‘𝐶)∀ℎ ∈ (𝑧(Hom ‘𝐶)𝑤)((ℎ(〈𝑦, 𝑧〉(comp‘𝐶)𝑤)𝑔)(〈𝑥, 𝑦〉(comp‘𝐷)𝑤)𝑓) = (ℎ(〈𝑥, 𝑧〉(comp‘𝐷)𝑤)(𝑔(〈𝑥, 𝑦〉(comp‘𝐶)𝑧)𝑓))) → ∀𝑓 ∈ (𝑥(Hom ‘𝐶)𝑦)∀𝑔 ∈ (𝑦(Hom ‘𝐶)𝑧)(𝑔(〈𝑥, 𝑦〉(comp‘𝐶)𝑧)𝑓) ∈ (𝑥(Hom ‘𝐶)𝑧)) |
12 | 11 | ralimi 2936 |
. . . . . . . 8
⊢
(∀𝑧 ∈
(Base‘𝐶)∀𝑓 ∈ (𝑥(Hom ‘𝐶)𝑦)∀𝑔 ∈ (𝑦(Hom ‘𝐶)𝑧)((𝑔(〈𝑥, 𝑦〉(comp‘𝐶)𝑧)𝑓) ∈ (𝑥(Hom ‘𝐶)𝑧) ∧ ∀𝑤 ∈ (Base‘𝐶)∀ℎ ∈ (𝑧(Hom ‘𝐶)𝑤)((ℎ(〈𝑦, 𝑧〉(comp‘𝐶)𝑤)𝑔)(〈𝑥, 𝑦〉(comp‘𝐷)𝑤)𝑓) = (ℎ(〈𝑥, 𝑧〉(comp‘𝐷)𝑤)(𝑔(〈𝑥, 𝑦〉(comp‘𝐶)𝑧)𝑓))) → ∀𝑧 ∈ (Base‘𝐶)∀𝑓 ∈ (𝑥(Hom ‘𝐶)𝑦)∀𝑔 ∈ (𝑦(Hom ‘𝐶)𝑧)(𝑔(〈𝑥, 𝑦〉(comp‘𝐶)𝑧)𝑓) ∈ (𝑥(Hom ‘𝐶)𝑧)) |
13 | 12 | ralimi 2936 |
. . . . . . 7
⊢
(∀𝑦 ∈
(Base‘𝐶)∀𝑧 ∈ (Base‘𝐶)∀𝑓 ∈ (𝑥(Hom ‘𝐶)𝑦)∀𝑔 ∈ (𝑦(Hom ‘𝐶)𝑧)((𝑔(〈𝑥, 𝑦〉(comp‘𝐶)𝑧)𝑓) ∈ (𝑥(Hom ‘𝐶)𝑧) ∧ ∀𝑤 ∈ (Base‘𝐶)∀ℎ ∈ (𝑧(Hom ‘𝐶)𝑤)((ℎ(〈𝑦, 𝑧〉(comp‘𝐶)𝑤)𝑔)(〈𝑥, 𝑦〉(comp‘𝐷)𝑤)𝑓) = (ℎ(〈𝑥, 𝑧〉(comp‘𝐷)𝑤)(𝑔(〈𝑥, 𝑦〉(comp‘𝐶)𝑧)𝑓))) → ∀𝑦 ∈ (Base‘𝐶)∀𝑧 ∈ (Base‘𝐶)∀𝑓 ∈ (𝑥(Hom ‘𝐶)𝑦)∀𝑔 ∈ (𝑦(Hom ‘𝐶)𝑧)(𝑔(〈𝑥, 𝑦〉(comp‘𝐶)𝑧)𝑓) ∈ (𝑥(Hom ‘𝐶)𝑧)) |
14 | 13 | adantl 481 |
. . . . . 6
⊢
((∃𝑔 ∈
(𝑥(Hom ‘𝐶)𝑥)∀𝑦 ∈ (Base‘𝐶)(∀𝑓 ∈ (𝑦(Hom ‘𝐶)𝑥)(𝑔(〈𝑦, 𝑥〉(comp‘𝐶)𝑥)𝑓) = 𝑓 ∧ ∀𝑓 ∈ (𝑥(Hom ‘𝐶)𝑦)(𝑓(〈𝑥, 𝑥〉(comp‘𝐶)𝑦)𝑔) = 𝑓) ∧ ∀𝑦 ∈ (Base‘𝐶)∀𝑧 ∈ (Base‘𝐶)∀𝑓 ∈ (𝑥(Hom ‘𝐶)𝑦)∀𝑔 ∈ (𝑦(Hom ‘𝐶)𝑧)((𝑔(〈𝑥, 𝑦〉(comp‘𝐶)𝑧)𝑓) ∈ (𝑥(Hom ‘𝐶)𝑧) ∧ ∀𝑤 ∈ (Base‘𝐶)∀ℎ ∈ (𝑧(Hom ‘𝐶)𝑤)((ℎ(〈𝑦, 𝑧〉(comp‘𝐶)𝑤)𝑔)(〈𝑥, 𝑦〉(comp‘𝐷)𝑤)𝑓) = (ℎ(〈𝑥, 𝑧〉(comp‘𝐷)𝑤)(𝑔(〈𝑥, 𝑦〉(comp‘𝐶)𝑧)𝑓)))) → ∀𝑦 ∈ (Base‘𝐶)∀𝑧 ∈ (Base‘𝐶)∀𝑓 ∈ (𝑥(Hom ‘𝐶)𝑦)∀𝑔 ∈ (𝑦(Hom ‘𝐶)𝑧)(𝑔(〈𝑥, 𝑦〉(comp‘𝐶)𝑧)𝑓) ∈ (𝑥(Hom ‘𝐶)𝑧)) |
15 | 14 | ralimi 2936 |
. . . . 5
⊢
(∀𝑥 ∈
(Base‘𝐶)(∃𝑔 ∈ (𝑥(Hom ‘𝐶)𝑥)∀𝑦 ∈ (Base‘𝐶)(∀𝑓 ∈ (𝑦(Hom ‘𝐶)𝑥)(𝑔(〈𝑦, 𝑥〉(comp‘𝐶)𝑥)𝑓) = 𝑓 ∧ ∀𝑓 ∈ (𝑥(Hom ‘𝐶)𝑦)(𝑓(〈𝑥, 𝑥〉(comp‘𝐶)𝑦)𝑔) = 𝑓) ∧ ∀𝑦 ∈ (Base‘𝐶)∀𝑧 ∈ (Base‘𝐶)∀𝑓 ∈ (𝑥(Hom ‘𝐶)𝑦)∀𝑔 ∈ (𝑦(Hom ‘𝐶)𝑧)((𝑔(〈𝑥, 𝑦〉(comp‘𝐶)𝑧)𝑓) ∈ (𝑥(Hom ‘𝐶)𝑧) ∧ ∀𝑤 ∈ (Base‘𝐶)∀ℎ ∈ (𝑧(Hom ‘𝐶)𝑤)((ℎ(〈𝑦, 𝑧〉(comp‘𝐶)𝑤)𝑔)(〈𝑥, 𝑦〉(comp‘𝐷)𝑤)𝑓) = (ℎ(〈𝑥, 𝑧〉(comp‘𝐷)𝑤)(𝑔(〈𝑥, 𝑦〉(comp‘𝐶)𝑧)𝑓)))) → ∀𝑥 ∈ (Base‘𝐶)∀𝑦 ∈ (Base‘𝐶)∀𝑧 ∈ (Base‘𝐶)∀𝑓 ∈ (𝑥(Hom ‘𝐶)𝑦)∀𝑔 ∈ (𝑦(Hom ‘𝐶)𝑧)(𝑔(〈𝑥, 𝑦〉(comp‘𝐶)𝑧)𝑓) ∈ (𝑥(Hom ‘𝐶)𝑧)) |
16 | 15 | a1i 11 |
. . . 4
⊢ (𝜑 → (∀𝑥 ∈ (Base‘𝐶)(∃𝑔 ∈ (𝑥(Hom ‘𝐶)𝑥)∀𝑦 ∈ (Base‘𝐶)(∀𝑓 ∈ (𝑦(Hom ‘𝐶)𝑥)(𝑔(〈𝑦, 𝑥〉(comp‘𝐶)𝑥)𝑓) = 𝑓 ∧ ∀𝑓 ∈ (𝑥(Hom ‘𝐶)𝑦)(𝑓(〈𝑥, 𝑥〉(comp‘𝐶)𝑦)𝑔) = 𝑓) ∧ ∀𝑦 ∈ (Base‘𝐶)∀𝑧 ∈ (Base‘𝐶)∀𝑓 ∈ (𝑥(Hom ‘𝐶)𝑦)∀𝑔 ∈ (𝑦(Hom ‘𝐶)𝑧)((𝑔(〈𝑥, 𝑦〉(comp‘𝐶)𝑧)𝑓) ∈ (𝑥(Hom ‘𝐶)𝑧) ∧ ∀𝑤 ∈ (Base‘𝐶)∀ℎ ∈ (𝑧(Hom ‘𝐶)𝑤)((ℎ(〈𝑦, 𝑧〉(comp‘𝐶)𝑤)𝑔)(〈𝑥, 𝑦〉(comp‘𝐷)𝑤)𝑓) = (ℎ(〈𝑥, 𝑧〉(comp‘𝐷)𝑤)(𝑔(〈𝑥, 𝑦〉(comp‘𝐶)𝑧)𝑓)))) → ∀𝑥 ∈ (Base‘𝐶)∀𝑦 ∈ (Base‘𝐶)∀𝑧 ∈ (Base‘𝐶)∀𝑓 ∈ (𝑥(Hom ‘𝐶)𝑦)∀𝑔 ∈ (𝑦(Hom ‘𝐶)𝑧)(𝑔(〈𝑥, 𝑦〉(comp‘𝐶)𝑧)𝑓) ∈ (𝑥(Hom ‘𝐶)𝑧))) |
17 | | nfra1 2925 |
. . . . . . . 8
⊢
Ⅎ𝑦∀𝑦 ∈ (Base‘𝐶)∀𝑧 ∈ (Base‘𝐶)∀𝑓 ∈ (𝑥(Hom ‘𝐶)𝑦)∀𝑔 ∈ (𝑦(Hom ‘𝐶)𝑧)(𝑔(〈𝑥, 𝑦〉(comp‘𝐶)𝑧)𝑓) ∈ (𝑥(Hom ‘𝐶)𝑧) |
18 | | nfv 1830 |
. . . . . . . 8
⊢
Ⅎ𝑥∀𝑧 ∈ (Base‘𝐶)∀𝑔 ∈ (𝑦(Hom ‘𝐶)𝑧)∀𝑤 ∈ (Base‘𝐶)∀ℎ ∈ (𝑧(Hom ‘𝐶)𝑤)(ℎ(〈𝑦, 𝑧〉(comp‘𝐶)𝑤)𝑔) ∈ (𝑦(Hom ‘𝐶)𝑤) |
19 | | nfra1 2925 |
. . . . . . . . . 10
⊢
Ⅎ𝑧∀𝑧 ∈ (Base‘𝐶)∀𝑓 ∈ (𝑥(Hom ‘𝐶)𝑦)∀𝑔 ∈ (𝑦(Hom ‘𝐶)𝑧)(𝑔(〈𝑥, 𝑦〉(comp‘𝐶)𝑧)𝑓) ∈ (𝑥(Hom ‘𝐶)𝑧) |
20 | | nfv 1830 |
. . . . . . . . . 10
⊢
Ⅎ𝑦∀𝑤 ∈ (Base‘𝐶)∀𝑔 ∈ (𝑥(Hom ‘𝐶)𝑧)∀ℎ ∈ (𝑧(Hom ‘𝐶)𝑤)(ℎ(〈𝑥, 𝑧〉(comp‘𝐶)𝑤)𝑔) ∈ (𝑥(Hom ‘𝐶)𝑤) |
21 | | nfra1 2925 |
. . . . . . . . . . . . . 14
⊢
Ⅎ𝑔∀𝑔 ∈ (𝑦(Hom ‘𝐶)𝑧)(𝑔(〈𝑥, 𝑦〉(comp‘𝐶)𝑧)𝑓) ∈ (𝑥(Hom ‘𝐶)𝑧) |
22 | | nfv 1830 |
. . . . . . . . . . . . . 14
⊢
Ⅎ𝑓∀ℎ ∈ (𝑦(Hom ‘𝐶)𝑧)(ℎ(〈𝑥, 𝑦〉(comp‘𝐶)𝑧)𝑔) ∈ (𝑥(Hom ‘𝐶)𝑧) |
23 | | oveq1 6556 |
. . . . . . . . . . . . . . . . 17
⊢ (𝑔 = ℎ → (𝑔(〈𝑥, 𝑦〉(comp‘𝐶)𝑧)𝑓) = (ℎ(〈𝑥, 𝑦〉(comp‘𝐶)𝑧)𝑓)) |
24 | 23 | eleq1d 2672 |
. . . . . . . . . . . . . . . 16
⊢ (𝑔 = ℎ → ((𝑔(〈𝑥, 𝑦〉(comp‘𝐶)𝑧)𝑓) ∈ (𝑥(Hom ‘𝐶)𝑧) ↔ (ℎ(〈𝑥, 𝑦〉(comp‘𝐶)𝑧)𝑓) ∈ (𝑥(Hom ‘𝐶)𝑧))) |
25 | 24 | cbvralv 3147 |
. . . . . . . . . . . . . . 15
⊢
(∀𝑔 ∈
(𝑦(Hom ‘𝐶)𝑧)(𝑔(〈𝑥, 𝑦〉(comp‘𝐶)𝑧)𝑓) ∈ (𝑥(Hom ‘𝐶)𝑧) ↔ ∀ℎ ∈ (𝑦(Hom ‘𝐶)𝑧)(ℎ(〈𝑥, 𝑦〉(comp‘𝐶)𝑧)𝑓) ∈ (𝑥(Hom ‘𝐶)𝑧)) |
26 | | oveq2 6557 |
. . . . . . . . . . . . . . . . 17
⊢ (𝑓 = 𝑔 → (ℎ(〈𝑥, 𝑦〉(comp‘𝐶)𝑧)𝑓) = (ℎ(〈𝑥, 𝑦〉(comp‘𝐶)𝑧)𝑔)) |
27 | 26 | eleq1d 2672 |
. . . . . . . . . . . . . . . 16
⊢ (𝑓 = 𝑔 → ((ℎ(〈𝑥, 𝑦〉(comp‘𝐶)𝑧)𝑓) ∈ (𝑥(Hom ‘𝐶)𝑧) ↔ (ℎ(〈𝑥, 𝑦〉(comp‘𝐶)𝑧)𝑔) ∈ (𝑥(Hom ‘𝐶)𝑧))) |
28 | 27 | ralbidv 2969 |
. . . . . . . . . . . . . . 15
⊢ (𝑓 = 𝑔 → (∀ℎ ∈ (𝑦(Hom ‘𝐶)𝑧)(ℎ(〈𝑥, 𝑦〉(comp‘𝐶)𝑧)𝑓) ∈ (𝑥(Hom ‘𝐶)𝑧) ↔ ∀ℎ ∈ (𝑦(Hom ‘𝐶)𝑧)(ℎ(〈𝑥, 𝑦〉(comp‘𝐶)𝑧)𝑔) ∈ (𝑥(Hom ‘𝐶)𝑧))) |
29 | 25, 28 | syl5bb 271 |
. . . . . . . . . . . . . 14
⊢ (𝑓 = 𝑔 → (∀𝑔 ∈ (𝑦(Hom ‘𝐶)𝑧)(𝑔(〈𝑥, 𝑦〉(comp‘𝐶)𝑧)𝑓) ∈ (𝑥(Hom ‘𝐶)𝑧) ↔ ∀ℎ ∈ (𝑦(Hom ‘𝐶)𝑧)(ℎ(〈𝑥, 𝑦〉(comp‘𝐶)𝑧)𝑔) ∈ (𝑥(Hom ‘𝐶)𝑧))) |
30 | 21, 22, 29 | cbvral 3143 |
. . . . . . . . . . . . 13
⊢
(∀𝑓 ∈
(𝑥(Hom ‘𝐶)𝑦)∀𝑔 ∈ (𝑦(Hom ‘𝐶)𝑧)(𝑔(〈𝑥, 𝑦〉(comp‘𝐶)𝑧)𝑓) ∈ (𝑥(Hom ‘𝐶)𝑧) ↔ ∀𝑔 ∈ (𝑥(Hom ‘𝐶)𝑦)∀ℎ ∈ (𝑦(Hom ‘𝐶)𝑧)(ℎ(〈𝑥, 𝑦〉(comp‘𝐶)𝑧)𝑔) ∈ (𝑥(Hom ‘𝐶)𝑧)) |
31 | | oveq2 6557 |
. . . . . . . . . . . . . . 15
⊢ (𝑧 = 𝑤 → (𝑦(Hom ‘𝐶)𝑧) = (𝑦(Hom ‘𝐶)𝑤)) |
32 | | oveq2 6557 |
. . . . . . . . . . . . . . . . 17
⊢ (𝑧 = 𝑤 → (〈𝑥, 𝑦〉(comp‘𝐶)𝑧) = (〈𝑥, 𝑦〉(comp‘𝐶)𝑤)) |
33 | 32 | oveqd 6566 |
. . . . . . . . . . . . . . . 16
⊢ (𝑧 = 𝑤 → (ℎ(〈𝑥, 𝑦〉(comp‘𝐶)𝑧)𝑔) = (ℎ(〈𝑥, 𝑦〉(comp‘𝐶)𝑤)𝑔)) |
34 | | oveq2 6557 |
. . . . . . . . . . . . . . . 16
⊢ (𝑧 = 𝑤 → (𝑥(Hom ‘𝐶)𝑧) = (𝑥(Hom ‘𝐶)𝑤)) |
35 | 33, 34 | eleq12d 2682 |
. . . . . . . . . . . . . . 15
⊢ (𝑧 = 𝑤 → ((ℎ(〈𝑥, 𝑦〉(comp‘𝐶)𝑧)𝑔) ∈ (𝑥(Hom ‘𝐶)𝑧) ↔ (ℎ(〈𝑥, 𝑦〉(comp‘𝐶)𝑤)𝑔) ∈ (𝑥(Hom ‘𝐶)𝑤))) |
36 | 31, 35 | raleqbidv 3129 |
. . . . . . . . . . . . . 14
⊢ (𝑧 = 𝑤 → (∀ℎ ∈ (𝑦(Hom ‘𝐶)𝑧)(ℎ(〈𝑥, 𝑦〉(comp‘𝐶)𝑧)𝑔) ∈ (𝑥(Hom ‘𝐶)𝑧) ↔ ∀ℎ ∈ (𝑦(Hom ‘𝐶)𝑤)(ℎ(〈𝑥, 𝑦〉(comp‘𝐶)𝑤)𝑔) ∈ (𝑥(Hom ‘𝐶)𝑤))) |
37 | 36 | ralbidv 2969 |
. . . . . . . . . . . . 13
⊢ (𝑧 = 𝑤 → (∀𝑔 ∈ (𝑥(Hom ‘𝐶)𝑦)∀ℎ ∈ (𝑦(Hom ‘𝐶)𝑧)(ℎ(〈𝑥, 𝑦〉(comp‘𝐶)𝑧)𝑔) ∈ (𝑥(Hom ‘𝐶)𝑧) ↔ ∀𝑔 ∈ (𝑥(Hom ‘𝐶)𝑦)∀ℎ ∈ (𝑦(Hom ‘𝐶)𝑤)(ℎ(〈𝑥, 𝑦〉(comp‘𝐶)𝑤)𝑔) ∈ (𝑥(Hom ‘𝐶)𝑤))) |
38 | 30, 37 | syl5bb 271 |
. . . . . . . . . . . 12
⊢ (𝑧 = 𝑤 → (∀𝑓 ∈ (𝑥(Hom ‘𝐶)𝑦)∀𝑔 ∈ (𝑦(Hom ‘𝐶)𝑧)(𝑔(〈𝑥, 𝑦〉(comp‘𝐶)𝑧)𝑓) ∈ (𝑥(Hom ‘𝐶)𝑧) ↔ ∀𝑔 ∈ (𝑥(Hom ‘𝐶)𝑦)∀ℎ ∈ (𝑦(Hom ‘𝐶)𝑤)(ℎ(〈𝑥, 𝑦〉(comp‘𝐶)𝑤)𝑔) ∈ (𝑥(Hom ‘𝐶)𝑤))) |
39 | 38 | cbvralv 3147 |
. . . . . . . . . . 11
⊢
(∀𝑧 ∈
(Base‘𝐶)∀𝑓 ∈ (𝑥(Hom ‘𝐶)𝑦)∀𝑔 ∈ (𝑦(Hom ‘𝐶)𝑧)(𝑔(〈𝑥, 𝑦〉(comp‘𝐶)𝑧)𝑓) ∈ (𝑥(Hom ‘𝐶)𝑧) ↔ ∀𝑤 ∈ (Base‘𝐶)∀𝑔 ∈ (𝑥(Hom ‘𝐶)𝑦)∀ℎ ∈ (𝑦(Hom ‘𝐶)𝑤)(ℎ(〈𝑥, 𝑦〉(comp‘𝐶)𝑤)𝑔) ∈ (𝑥(Hom ‘𝐶)𝑤)) |
40 | | oveq2 6557 |
. . . . . . . . . . . . 13
⊢ (𝑦 = 𝑧 → (𝑥(Hom ‘𝐶)𝑦) = (𝑥(Hom ‘𝐶)𝑧)) |
41 | | oveq1 6556 |
. . . . . . . . . . . . . 14
⊢ (𝑦 = 𝑧 → (𝑦(Hom ‘𝐶)𝑤) = (𝑧(Hom ‘𝐶)𝑤)) |
42 | | opeq2 4341 |
. . . . . . . . . . . . . . . . 17
⊢ (𝑦 = 𝑧 → 〈𝑥, 𝑦〉 = 〈𝑥, 𝑧〉) |
43 | 42 | oveq1d 6564 |
. . . . . . . . . . . . . . . 16
⊢ (𝑦 = 𝑧 → (〈𝑥, 𝑦〉(comp‘𝐶)𝑤) = (〈𝑥, 𝑧〉(comp‘𝐶)𝑤)) |
44 | 43 | oveqd 6566 |
. . . . . . . . . . . . . . 15
⊢ (𝑦 = 𝑧 → (ℎ(〈𝑥, 𝑦〉(comp‘𝐶)𝑤)𝑔) = (ℎ(〈𝑥, 𝑧〉(comp‘𝐶)𝑤)𝑔)) |
45 | 44 | eleq1d 2672 |
. . . . . . . . . . . . . 14
⊢ (𝑦 = 𝑧 → ((ℎ(〈𝑥, 𝑦〉(comp‘𝐶)𝑤)𝑔) ∈ (𝑥(Hom ‘𝐶)𝑤) ↔ (ℎ(〈𝑥, 𝑧〉(comp‘𝐶)𝑤)𝑔) ∈ (𝑥(Hom ‘𝐶)𝑤))) |
46 | 41, 45 | raleqbidv 3129 |
. . . . . . . . . . . . 13
⊢ (𝑦 = 𝑧 → (∀ℎ ∈ (𝑦(Hom ‘𝐶)𝑤)(ℎ(〈𝑥, 𝑦〉(comp‘𝐶)𝑤)𝑔) ∈ (𝑥(Hom ‘𝐶)𝑤) ↔ ∀ℎ ∈ (𝑧(Hom ‘𝐶)𝑤)(ℎ(〈𝑥, 𝑧〉(comp‘𝐶)𝑤)𝑔) ∈ (𝑥(Hom ‘𝐶)𝑤))) |
47 | 40, 46 | raleqbidv 3129 |
. . . . . . . . . . . 12
⊢ (𝑦 = 𝑧 → (∀𝑔 ∈ (𝑥(Hom ‘𝐶)𝑦)∀ℎ ∈ (𝑦(Hom ‘𝐶)𝑤)(ℎ(〈𝑥, 𝑦〉(comp‘𝐶)𝑤)𝑔) ∈ (𝑥(Hom ‘𝐶)𝑤) ↔ ∀𝑔 ∈ (𝑥(Hom ‘𝐶)𝑧)∀ℎ ∈ (𝑧(Hom ‘𝐶)𝑤)(ℎ(〈𝑥, 𝑧〉(comp‘𝐶)𝑤)𝑔) ∈ (𝑥(Hom ‘𝐶)𝑤))) |
48 | 47 | ralbidv 2969 |
. . . . . . . . . . 11
⊢ (𝑦 = 𝑧 → (∀𝑤 ∈ (Base‘𝐶)∀𝑔 ∈ (𝑥(Hom ‘𝐶)𝑦)∀ℎ ∈ (𝑦(Hom ‘𝐶)𝑤)(ℎ(〈𝑥, 𝑦〉(comp‘𝐶)𝑤)𝑔) ∈ (𝑥(Hom ‘𝐶)𝑤) ↔ ∀𝑤 ∈ (Base‘𝐶)∀𝑔 ∈ (𝑥(Hom ‘𝐶)𝑧)∀ℎ ∈ (𝑧(Hom ‘𝐶)𝑤)(ℎ(〈𝑥, 𝑧〉(comp‘𝐶)𝑤)𝑔) ∈ (𝑥(Hom ‘𝐶)𝑤))) |
49 | 39, 48 | syl5bb 271 |
. . . . . . . . . 10
⊢ (𝑦 = 𝑧 → (∀𝑧 ∈ (Base‘𝐶)∀𝑓 ∈ (𝑥(Hom ‘𝐶)𝑦)∀𝑔 ∈ (𝑦(Hom ‘𝐶)𝑧)(𝑔(〈𝑥, 𝑦〉(comp‘𝐶)𝑧)𝑓) ∈ (𝑥(Hom ‘𝐶)𝑧) ↔ ∀𝑤 ∈ (Base‘𝐶)∀𝑔 ∈ (𝑥(Hom ‘𝐶)𝑧)∀ℎ ∈ (𝑧(Hom ‘𝐶)𝑤)(ℎ(〈𝑥, 𝑧〉(comp‘𝐶)𝑤)𝑔) ∈ (𝑥(Hom ‘𝐶)𝑤))) |
50 | 19, 20, 49 | cbvral 3143 |
. . . . . . . . 9
⊢
(∀𝑦 ∈
(Base‘𝐶)∀𝑧 ∈ (Base‘𝐶)∀𝑓 ∈ (𝑥(Hom ‘𝐶)𝑦)∀𝑔 ∈ (𝑦(Hom ‘𝐶)𝑧)(𝑔(〈𝑥, 𝑦〉(comp‘𝐶)𝑧)𝑓) ∈ (𝑥(Hom ‘𝐶)𝑧) ↔ ∀𝑧 ∈ (Base‘𝐶)∀𝑤 ∈ (Base‘𝐶)∀𝑔 ∈ (𝑥(Hom ‘𝐶)𝑧)∀ℎ ∈ (𝑧(Hom ‘𝐶)𝑤)(ℎ(〈𝑥, 𝑧〉(comp‘𝐶)𝑤)𝑔) ∈ (𝑥(Hom ‘𝐶)𝑤)) |
51 | | oveq1 6556 |
. . . . . . . . . . . . 13
⊢ (𝑥 = 𝑦 → (𝑥(Hom ‘𝐶)𝑧) = (𝑦(Hom ‘𝐶)𝑧)) |
52 | | opeq1 4340 |
. . . . . . . . . . . . . . . . 17
⊢ (𝑥 = 𝑦 → 〈𝑥, 𝑧〉 = 〈𝑦, 𝑧〉) |
53 | 52 | oveq1d 6564 |
. . . . . . . . . . . . . . . 16
⊢ (𝑥 = 𝑦 → (〈𝑥, 𝑧〉(comp‘𝐶)𝑤) = (〈𝑦, 𝑧〉(comp‘𝐶)𝑤)) |
54 | 53 | oveqd 6566 |
. . . . . . . . . . . . . . 15
⊢ (𝑥 = 𝑦 → (ℎ(〈𝑥, 𝑧〉(comp‘𝐶)𝑤)𝑔) = (ℎ(〈𝑦, 𝑧〉(comp‘𝐶)𝑤)𝑔)) |
55 | | oveq1 6556 |
. . . . . . . . . . . . . . 15
⊢ (𝑥 = 𝑦 → (𝑥(Hom ‘𝐶)𝑤) = (𝑦(Hom ‘𝐶)𝑤)) |
56 | 54, 55 | eleq12d 2682 |
. . . . . . . . . . . . . 14
⊢ (𝑥 = 𝑦 → ((ℎ(〈𝑥, 𝑧〉(comp‘𝐶)𝑤)𝑔) ∈ (𝑥(Hom ‘𝐶)𝑤) ↔ (ℎ(〈𝑦, 𝑧〉(comp‘𝐶)𝑤)𝑔) ∈ (𝑦(Hom ‘𝐶)𝑤))) |
57 | 56 | ralbidv 2969 |
. . . . . . . . . . . . 13
⊢ (𝑥 = 𝑦 → (∀ℎ ∈ (𝑧(Hom ‘𝐶)𝑤)(ℎ(〈𝑥, 𝑧〉(comp‘𝐶)𝑤)𝑔) ∈ (𝑥(Hom ‘𝐶)𝑤) ↔ ∀ℎ ∈ (𝑧(Hom ‘𝐶)𝑤)(ℎ(〈𝑦, 𝑧〉(comp‘𝐶)𝑤)𝑔) ∈ (𝑦(Hom ‘𝐶)𝑤))) |
58 | 51, 57 | raleqbidv 3129 |
. . . . . . . . . . . 12
⊢ (𝑥 = 𝑦 → (∀𝑔 ∈ (𝑥(Hom ‘𝐶)𝑧)∀ℎ ∈ (𝑧(Hom ‘𝐶)𝑤)(ℎ(〈𝑥, 𝑧〉(comp‘𝐶)𝑤)𝑔) ∈ (𝑥(Hom ‘𝐶)𝑤) ↔ ∀𝑔 ∈ (𝑦(Hom ‘𝐶)𝑧)∀ℎ ∈ (𝑧(Hom ‘𝐶)𝑤)(ℎ(〈𝑦, 𝑧〉(comp‘𝐶)𝑤)𝑔) ∈ (𝑦(Hom ‘𝐶)𝑤))) |
59 | 58 | ralbidv 2969 |
. . . . . . . . . . 11
⊢ (𝑥 = 𝑦 → (∀𝑤 ∈ (Base‘𝐶)∀𝑔 ∈ (𝑥(Hom ‘𝐶)𝑧)∀ℎ ∈ (𝑧(Hom ‘𝐶)𝑤)(ℎ(〈𝑥, 𝑧〉(comp‘𝐶)𝑤)𝑔) ∈ (𝑥(Hom ‘𝐶)𝑤) ↔ ∀𝑤 ∈ (Base‘𝐶)∀𝑔 ∈ (𝑦(Hom ‘𝐶)𝑧)∀ℎ ∈ (𝑧(Hom ‘𝐶)𝑤)(ℎ(〈𝑦, 𝑧〉(comp‘𝐶)𝑤)𝑔) ∈ (𝑦(Hom ‘𝐶)𝑤))) |
60 | | ralcom 3079 |
. . . . . . . . . . 11
⊢
(∀𝑤 ∈
(Base‘𝐶)∀𝑔 ∈ (𝑦(Hom ‘𝐶)𝑧)∀ℎ ∈ (𝑧(Hom ‘𝐶)𝑤)(ℎ(〈𝑦, 𝑧〉(comp‘𝐶)𝑤)𝑔) ∈ (𝑦(Hom ‘𝐶)𝑤) ↔ ∀𝑔 ∈ (𝑦(Hom ‘𝐶)𝑧)∀𝑤 ∈ (Base‘𝐶)∀ℎ ∈ (𝑧(Hom ‘𝐶)𝑤)(ℎ(〈𝑦, 𝑧〉(comp‘𝐶)𝑤)𝑔) ∈ (𝑦(Hom ‘𝐶)𝑤)) |
61 | 59, 60 | syl6bb 275 |
. . . . . . . . . 10
⊢ (𝑥 = 𝑦 → (∀𝑤 ∈ (Base‘𝐶)∀𝑔 ∈ (𝑥(Hom ‘𝐶)𝑧)∀ℎ ∈ (𝑧(Hom ‘𝐶)𝑤)(ℎ(〈𝑥, 𝑧〉(comp‘𝐶)𝑤)𝑔) ∈ (𝑥(Hom ‘𝐶)𝑤) ↔ ∀𝑔 ∈ (𝑦(Hom ‘𝐶)𝑧)∀𝑤 ∈ (Base‘𝐶)∀ℎ ∈ (𝑧(Hom ‘𝐶)𝑤)(ℎ(〈𝑦, 𝑧〉(comp‘𝐶)𝑤)𝑔) ∈ (𝑦(Hom ‘𝐶)𝑤))) |
62 | 61 | ralbidv 2969 |
. . . . . . . . 9
⊢ (𝑥 = 𝑦 → (∀𝑧 ∈ (Base‘𝐶)∀𝑤 ∈ (Base‘𝐶)∀𝑔 ∈ (𝑥(Hom ‘𝐶)𝑧)∀ℎ ∈ (𝑧(Hom ‘𝐶)𝑤)(ℎ(〈𝑥, 𝑧〉(comp‘𝐶)𝑤)𝑔) ∈ (𝑥(Hom ‘𝐶)𝑤) ↔ ∀𝑧 ∈ (Base‘𝐶)∀𝑔 ∈ (𝑦(Hom ‘𝐶)𝑧)∀𝑤 ∈ (Base‘𝐶)∀ℎ ∈ (𝑧(Hom ‘𝐶)𝑤)(ℎ(〈𝑦, 𝑧〉(comp‘𝐶)𝑤)𝑔) ∈ (𝑦(Hom ‘𝐶)𝑤))) |
63 | 50, 62 | syl5bb 271 |
. . . . . . . 8
⊢ (𝑥 = 𝑦 → (∀𝑦 ∈ (Base‘𝐶)∀𝑧 ∈ (Base‘𝐶)∀𝑓 ∈ (𝑥(Hom ‘𝐶)𝑦)∀𝑔 ∈ (𝑦(Hom ‘𝐶)𝑧)(𝑔(〈𝑥, 𝑦〉(comp‘𝐶)𝑧)𝑓) ∈ (𝑥(Hom ‘𝐶)𝑧) ↔ ∀𝑧 ∈ (Base‘𝐶)∀𝑔 ∈ (𝑦(Hom ‘𝐶)𝑧)∀𝑤 ∈ (Base‘𝐶)∀ℎ ∈ (𝑧(Hom ‘𝐶)𝑤)(ℎ(〈𝑦, 𝑧〉(comp‘𝐶)𝑤)𝑔) ∈ (𝑦(Hom ‘𝐶)𝑤))) |
64 | 17, 18, 63 | cbvral 3143 |
. . . . . . 7
⊢
(∀𝑥 ∈
(Base‘𝐶)∀𝑦 ∈ (Base‘𝐶)∀𝑧 ∈ (Base‘𝐶)∀𝑓 ∈ (𝑥(Hom ‘𝐶)𝑦)∀𝑔 ∈ (𝑦(Hom ‘𝐶)𝑧)(𝑔(〈𝑥, 𝑦〉(comp‘𝐶)𝑧)𝑓) ∈ (𝑥(Hom ‘𝐶)𝑧) ↔ ∀𝑦 ∈ (Base‘𝐶)∀𝑧 ∈ (Base‘𝐶)∀𝑔 ∈ (𝑦(Hom ‘𝐶)𝑧)∀𝑤 ∈ (Base‘𝐶)∀ℎ ∈ (𝑧(Hom ‘𝐶)𝑤)(ℎ(〈𝑦, 𝑧〉(comp‘𝐶)𝑤)𝑔) ∈ (𝑦(Hom ‘𝐶)𝑤)) |
65 | 64 | biimpi 205 |
. . . . . 6
⊢
(∀𝑥 ∈
(Base‘𝐶)∀𝑦 ∈ (Base‘𝐶)∀𝑧 ∈ (Base‘𝐶)∀𝑓 ∈ (𝑥(Hom ‘𝐶)𝑦)∀𝑔 ∈ (𝑦(Hom ‘𝐶)𝑧)(𝑔(〈𝑥, 𝑦〉(comp‘𝐶)𝑧)𝑓) ∈ (𝑥(Hom ‘𝐶)𝑧) → ∀𝑦 ∈ (Base‘𝐶)∀𝑧 ∈ (Base‘𝐶)∀𝑔 ∈ (𝑦(Hom ‘𝐶)𝑧)∀𝑤 ∈ (Base‘𝐶)∀ℎ ∈ (𝑧(Hom ‘𝐶)𝑤)(ℎ(〈𝑦, 𝑧〉(comp‘𝐶)𝑤)𝑔) ∈ (𝑦(Hom ‘𝐶)𝑤)) |
66 | 65 | ancri 573 |
. . . . 5
⊢
(∀𝑥 ∈
(Base‘𝐶)∀𝑦 ∈ (Base‘𝐶)∀𝑧 ∈ (Base‘𝐶)∀𝑓 ∈ (𝑥(Hom ‘𝐶)𝑦)∀𝑔 ∈ (𝑦(Hom ‘𝐶)𝑧)(𝑔(〈𝑥, 𝑦〉(comp‘𝐶)𝑧)𝑓) ∈ (𝑥(Hom ‘𝐶)𝑧) → (∀𝑦 ∈ (Base‘𝐶)∀𝑧 ∈ (Base‘𝐶)∀𝑔 ∈ (𝑦(Hom ‘𝐶)𝑧)∀𝑤 ∈ (Base‘𝐶)∀ℎ ∈ (𝑧(Hom ‘𝐶)𝑤)(ℎ(〈𝑦, 𝑧〉(comp‘𝐶)𝑤)𝑔) ∈ (𝑦(Hom ‘𝐶)𝑤) ∧ ∀𝑥 ∈ (Base‘𝐶)∀𝑦 ∈ (Base‘𝐶)∀𝑧 ∈ (Base‘𝐶)∀𝑓 ∈ (𝑥(Hom ‘𝐶)𝑦)∀𝑔 ∈ (𝑦(Hom ‘𝐶)𝑧)(𝑔(〈𝑥, 𝑦〉(comp‘𝐶)𝑧)𝑓) ∈ (𝑥(Hom ‘𝐶)𝑧))) |
67 | | r19.26 3046 |
. . . . . . . . . . . 12
⊢
(∀𝑦 ∈
(Base‘𝐶)(∀𝑧 ∈ (Base‘𝐶)∀𝑔 ∈ (𝑦(Hom ‘𝐶)𝑧)∀𝑤 ∈ (Base‘𝐶)∀ℎ ∈ (𝑧(Hom ‘𝐶)𝑤)(ℎ(〈𝑦, 𝑧〉(comp‘𝐶)𝑤)𝑔) ∈ (𝑦(Hom ‘𝐶)𝑤) ∧ ∀𝑧 ∈ (Base‘𝐶)∀𝑓 ∈ (𝑥(Hom ‘𝐶)𝑦)∀𝑔 ∈ (𝑦(Hom ‘𝐶)𝑧)(𝑔(〈𝑥, 𝑦〉(comp‘𝐶)𝑧)𝑓) ∈ (𝑥(Hom ‘𝐶)𝑧)) ↔ (∀𝑦 ∈ (Base‘𝐶)∀𝑧 ∈ (Base‘𝐶)∀𝑔 ∈ (𝑦(Hom ‘𝐶)𝑧)∀𝑤 ∈ (Base‘𝐶)∀ℎ ∈ (𝑧(Hom ‘𝐶)𝑤)(ℎ(〈𝑦, 𝑧〉(comp‘𝐶)𝑤)𝑔) ∈ (𝑦(Hom ‘𝐶)𝑤) ∧ ∀𝑦 ∈ (Base‘𝐶)∀𝑧 ∈ (Base‘𝐶)∀𝑓 ∈ (𝑥(Hom ‘𝐶)𝑦)∀𝑔 ∈ (𝑦(Hom ‘𝐶)𝑧)(𝑔(〈𝑥, 𝑦〉(comp‘𝐶)𝑧)𝑓) ∈ (𝑥(Hom ‘𝐶)𝑧))) |
68 | | r19.26 3046 |
. . . . . . . . . . . . . . 15
⊢
(∀𝑧 ∈
(Base‘𝐶)(∀𝑔 ∈ (𝑦(Hom ‘𝐶)𝑧)∀𝑤 ∈ (Base‘𝐶)∀ℎ ∈ (𝑧(Hom ‘𝐶)𝑤)(ℎ(〈𝑦, 𝑧〉(comp‘𝐶)𝑤)𝑔) ∈ (𝑦(Hom ‘𝐶)𝑤) ∧ ∀𝑓 ∈ (𝑥(Hom ‘𝐶)𝑦)∀𝑔 ∈ (𝑦(Hom ‘𝐶)𝑧)(𝑔(〈𝑥, 𝑦〉(comp‘𝐶)𝑧)𝑓) ∈ (𝑥(Hom ‘𝐶)𝑧)) ↔ (∀𝑧 ∈ (Base‘𝐶)∀𝑔 ∈ (𝑦(Hom ‘𝐶)𝑧)∀𝑤 ∈ (Base‘𝐶)∀ℎ ∈ (𝑧(Hom ‘𝐶)𝑤)(ℎ(〈𝑦, 𝑧〉(comp‘𝐶)𝑤)𝑔) ∈ (𝑦(Hom ‘𝐶)𝑤) ∧ ∀𝑧 ∈ (Base‘𝐶)∀𝑓 ∈ (𝑥(Hom ‘𝐶)𝑦)∀𝑔 ∈ (𝑦(Hom ‘𝐶)𝑧)(𝑔(〈𝑥, 𝑦〉(comp‘𝐶)𝑧)𝑓) ∈ (𝑥(Hom ‘𝐶)𝑧))) |
69 | | r19.26 3046 |
. . . . . . . . . . . . . . . . . . . . . . . 24
⊢
(∀𝑔 ∈
(𝑦(Hom ‘𝐶)𝑧)(∀𝑤 ∈ (Base‘𝐶)∀ℎ ∈ (𝑧(Hom ‘𝐶)𝑤)(ℎ(〈𝑦, 𝑧〉(comp‘𝐶)𝑤)𝑔) ∈ (𝑦(Hom ‘𝐶)𝑤) ∧ (𝑔(〈𝑥, 𝑦〉(comp‘𝐶)𝑧)𝑓) ∈ (𝑥(Hom ‘𝐶)𝑧)) ↔ (∀𝑔 ∈ (𝑦(Hom ‘𝐶)𝑧)∀𝑤 ∈ (Base‘𝐶)∀ℎ ∈ (𝑧(Hom ‘𝐶)𝑤)(ℎ(〈𝑦, 𝑧〉(comp‘𝐶)𝑤)𝑔) ∈ (𝑦(Hom ‘𝐶)𝑤) ∧ ∀𝑔 ∈ (𝑦(Hom ‘𝐶)𝑧)(𝑔(〈𝑥, 𝑦〉(comp‘𝐶)𝑧)𝑓) ∈ (𝑥(Hom ‘𝐶)𝑧))) |
70 | | eqid 2610 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. . 36
⊢
(Base‘𝐶) =
(Base‘𝐶) |
71 | | eqid 2610 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. . 36
⊢ (Hom
‘𝐶) = (Hom
‘𝐶) |
72 | | eqid 2610 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. . 36
⊢
(comp‘𝐶) =
(comp‘𝐶) |
73 | | eqid 2610 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. . 36
⊢
(comp‘𝐷) =
(comp‘𝐷) |
74 | | catpropd.1 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. . . . . 39
⊢ (𝜑 → (Homf
‘𝐶) =
(Homf ‘𝐷)) |
75 | 74 | adantr 480 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. . . . 38
⊢ ((𝜑 ∧ 𝑥 ∈ (Base‘𝐶)) → (Homf
‘𝐶) =
(Homf ‘𝐷)) |
76 | 75 | ad4antr 764 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. . . 37
⊢
((((((𝜑 ∧ 𝑥 ∈ (Base‘𝐶)) ∧ 𝑦 ∈ (Base‘𝐶)) ∧ 𝑧 ∈ (Base‘𝐶)) ∧ 𝑓 ∈ (𝑥(Hom ‘𝐶)𝑦)) ∧ 𝑔 ∈ (𝑦(Hom ‘𝐶)𝑧)) → (Homf
‘𝐶) =
(Homf ‘𝐷)) |
77 | 76 | ad4antr 764 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. . 36
⊢
((((((((((𝜑 ∧
𝑥 ∈ (Base‘𝐶)) ∧ 𝑦 ∈ (Base‘𝐶)) ∧ 𝑧 ∈ (Base‘𝐶)) ∧ 𝑓 ∈ (𝑥(Hom ‘𝐶)𝑦)) ∧ 𝑔 ∈ (𝑦(Hom ‘𝐶)𝑧)) ∧ (𝑔(〈𝑥, 𝑦〉(comp‘𝐶)𝑧)𝑓) ∈ (𝑥(Hom ‘𝐶)𝑧)) ∧ 𝑤 ∈ (Base‘𝐶)) ∧ ℎ ∈ (𝑧(Hom ‘𝐶)𝑤)) ∧ (ℎ(〈𝑦, 𝑧〉(comp‘𝐶)𝑤)𝑔) ∈ (𝑦(Hom ‘𝐶)𝑤)) → (Homf
‘𝐶) =
(Homf ‘𝐷)) |
78 | | catpropd.2 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. . . . 38
⊢ (𝜑 →
(compf‘𝐶) = (compf‘𝐷)) |
79 | 78 | ad5antr 766 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. . . 37
⊢
((((((𝜑 ∧ 𝑥 ∈ (Base‘𝐶)) ∧ 𝑦 ∈ (Base‘𝐶)) ∧ 𝑧 ∈ (Base‘𝐶)) ∧ 𝑓 ∈ (𝑥(Hom ‘𝐶)𝑦)) ∧ 𝑔 ∈ (𝑦(Hom ‘𝐶)𝑧)) →
(compf‘𝐶) = (compf‘𝐷)) |
80 | 79 | ad4antr 764 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. . 36
⊢
((((((((((𝜑 ∧
𝑥 ∈ (Base‘𝐶)) ∧ 𝑦 ∈ (Base‘𝐶)) ∧ 𝑧 ∈ (Base‘𝐶)) ∧ 𝑓 ∈ (𝑥(Hom ‘𝐶)𝑦)) ∧ 𝑔 ∈ (𝑦(Hom ‘𝐶)𝑧)) ∧ (𝑔(〈𝑥, 𝑦〉(comp‘𝐶)𝑧)𝑓) ∈ (𝑥(Hom ‘𝐶)𝑧)) ∧ 𝑤 ∈ (Base‘𝐶)) ∧ ℎ ∈ (𝑧(Hom ‘𝐶)𝑤)) ∧ (ℎ(〈𝑦, 𝑧〉(comp‘𝐶)𝑤)𝑔) ∈ (𝑦(Hom ‘𝐶)𝑤)) →
(compf‘𝐶) = (compf‘𝐷)) |
81 | | simpllr 795 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. . . . 38
⊢ ((((𝜑 ∧ 𝑥 ∈ (Base‘𝐶)) ∧ 𝑦 ∈ (Base‘𝐶)) ∧ 𝑧 ∈ (Base‘𝐶)) → 𝑥 ∈ (Base‘𝐶)) |
82 | 81 | ad2antrr 758 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. . . 37
⊢
((((((𝜑 ∧ 𝑥 ∈ (Base‘𝐶)) ∧ 𝑦 ∈ (Base‘𝐶)) ∧ 𝑧 ∈ (Base‘𝐶)) ∧ 𝑓 ∈ (𝑥(Hom ‘𝐶)𝑦)) ∧ 𝑔 ∈ (𝑦(Hom ‘𝐶)𝑧)) → 𝑥 ∈ (Base‘𝐶)) |
83 | 82 | ad4antr 764 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. . 36
⊢
((((((((((𝜑 ∧
𝑥 ∈ (Base‘𝐶)) ∧ 𝑦 ∈ (Base‘𝐶)) ∧ 𝑧 ∈ (Base‘𝐶)) ∧ 𝑓 ∈ (𝑥(Hom ‘𝐶)𝑦)) ∧ 𝑔 ∈ (𝑦(Hom ‘𝐶)𝑧)) ∧ (𝑔(〈𝑥, 𝑦〉(comp‘𝐶)𝑧)𝑓) ∈ (𝑥(Hom ‘𝐶)𝑧)) ∧ 𝑤 ∈ (Base‘𝐶)) ∧ ℎ ∈ (𝑧(Hom ‘𝐶)𝑤)) ∧ (ℎ(〈𝑦, 𝑧〉(comp‘𝐶)𝑤)𝑔) ∈ (𝑦(Hom ‘𝐶)𝑤)) → 𝑥 ∈ (Base‘𝐶)) |
84 | | simp-4r 803 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. . . 37
⊢
((((((𝜑 ∧ 𝑥 ∈ (Base‘𝐶)) ∧ 𝑦 ∈ (Base‘𝐶)) ∧ 𝑧 ∈ (Base‘𝐶)) ∧ 𝑓 ∈ (𝑥(Hom ‘𝐶)𝑦)) ∧ 𝑔 ∈ (𝑦(Hom ‘𝐶)𝑧)) → 𝑦 ∈ (Base‘𝐶)) |
85 | 84 | ad4antr 764 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. . 36
⊢
((((((((((𝜑 ∧
𝑥 ∈ (Base‘𝐶)) ∧ 𝑦 ∈ (Base‘𝐶)) ∧ 𝑧 ∈ (Base‘𝐶)) ∧ 𝑓 ∈ (𝑥(Hom ‘𝐶)𝑦)) ∧ 𝑔 ∈ (𝑦(Hom ‘𝐶)𝑧)) ∧ (𝑔(〈𝑥, 𝑦〉(comp‘𝐶)𝑧)𝑓) ∈ (𝑥(Hom ‘𝐶)𝑧)) ∧ 𝑤 ∈ (Base‘𝐶)) ∧ ℎ ∈ (𝑧(Hom ‘𝐶)𝑤)) ∧ (ℎ(〈𝑦, 𝑧〉(comp‘𝐶)𝑤)𝑔) ∈ (𝑦(Hom ‘𝐶)𝑤)) → 𝑦 ∈ (Base‘𝐶)) |
86 | | simpllr 795 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. . 36
⊢
((((((((((𝜑 ∧
𝑥 ∈ (Base‘𝐶)) ∧ 𝑦 ∈ (Base‘𝐶)) ∧ 𝑧 ∈ (Base‘𝐶)) ∧ 𝑓 ∈ (𝑥(Hom ‘𝐶)𝑦)) ∧ 𝑔 ∈ (𝑦(Hom ‘𝐶)𝑧)) ∧ (𝑔(〈𝑥, 𝑦〉(comp‘𝐶)𝑧)𝑓) ∈ (𝑥(Hom ‘𝐶)𝑧)) ∧ 𝑤 ∈ (Base‘𝐶)) ∧ ℎ ∈ (𝑧(Hom ‘𝐶)𝑤)) ∧ (ℎ(〈𝑦, 𝑧〉(comp‘𝐶)𝑤)𝑔) ∈ (𝑦(Hom ‘𝐶)𝑤)) → 𝑤 ∈ (Base‘𝐶)) |
87 | | simplr 788 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. . . 37
⊢
((((((𝜑 ∧ 𝑥 ∈ (Base‘𝐶)) ∧ 𝑦 ∈ (Base‘𝐶)) ∧ 𝑧 ∈ (Base‘𝐶)) ∧ 𝑓 ∈ (𝑥(Hom ‘𝐶)𝑦)) ∧ 𝑔 ∈ (𝑦(Hom ‘𝐶)𝑧)) → 𝑓 ∈ (𝑥(Hom ‘𝐶)𝑦)) |
88 | 87 | ad4antr 764 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. . 36
⊢
((((((((((𝜑 ∧
𝑥 ∈ (Base‘𝐶)) ∧ 𝑦 ∈ (Base‘𝐶)) ∧ 𝑧 ∈ (Base‘𝐶)) ∧ 𝑓 ∈ (𝑥(Hom ‘𝐶)𝑦)) ∧ 𝑔 ∈ (𝑦(Hom ‘𝐶)𝑧)) ∧ (𝑔(〈𝑥, 𝑦〉(comp‘𝐶)𝑧)𝑓) ∈ (𝑥(Hom ‘𝐶)𝑧)) ∧ 𝑤 ∈ (Base‘𝐶)) ∧ ℎ ∈ (𝑧(Hom ‘𝐶)𝑤)) ∧ (ℎ(〈𝑦, 𝑧〉(comp‘𝐶)𝑤)𝑔) ∈ (𝑦(Hom ‘𝐶)𝑤)) → 𝑓 ∈ (𝑥(Hom ‘𝐶)𝑦)) |
89 | | simpr 476 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. . 36
⊢
((((((((((𝜑 ∧
𝑥 ∈ (Base‘𝐶)) ∧ 𝑦 ∈ (Base‘𝐶)) ∧ 𝑧 ∈ (Base‘𝐶)) ∧ 𝑓 ∈ (𝑥(Hom ‘𝐶)𝑦)) ∧ 𝑔 ∈ (𝑦(Hom ‘𝐶)𝑧)) ∧ (𝑔(〈𝑥, 𝑦〉(comp‘𝐶)𝑧)𝑓) ∈ (𝑥(Hom ‘𝐶)𝑧)) ∧ 𝑤 ∈ (Base‘𝐶)) ∧ ℎ ∈ (𝑧(Hom ‘𝐶)𝑤)) ∧ (ℎ(〈𝑦, 𝑧〉(comp‘𝐶)𝑤)𝑔) ∈ (𝑦(Hom ‘𝐶)𝑤)) → (ℎ(〈𝑦, 𝑧〉(comp‘𝐶)𝑤)𝑔) ∈ (𝑦(Hom ‘𝐶)𝑤)) |
90 | 70, 71, 72, 73, 77, 80, 83, 85, 86, 88, 89 | comfeqval 16191 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. 35
⊢
((((((((((𝜑 ∧
𝑥 ∈ (Base‘𝐶)) ∧ 𝑦 ∈ (Base‘𝐶)) ∧ 𝑧 ∈ (Base‘𝐶)) ∧ 𝑓 ∈ (𝑥(Hom ‘𝐶)𝑦)) ∧ 𝑔 ∈ (𝑦(Hom ‘𝐶)𝑧)) ∧ (𝑔(〈𝑥, 𝑦〉(comp‘𝐶)𝑧)𝑓) ∈ (𝑥(Hom ‘𝐶)𝑧)) ∧ 𝑤 ∈ (Base‘𝐶)) ∧ ℎ ∈ (𝑧(Hom ‘𝐶)𝑤)) ∧ (ℎ(〈𝑦, 𝑧〉(comp‘𝐶)𝑤)𝑔) ∈ (𝑦(Hom ‘𝐶)𝑤)) → ((ℎ(〈𝑦, 𝑧〉(comp‘𝐶)𝑤)𝑔)(〈𝑥, 𝑦〉(comp‘𝐶)𝑤)𝑓) = ((ℎ(〈𝑦, 𝑧〉(comp‘𝐶)𝑤)𝑔)(〈𝑥, 𝑦〉(comp‘𝐷)𝑤)𝑓)) |
91 | | simpllr 795 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. . . 37
⊢
((((((𝜑 ∧ 𝑥 ∈ (Base‘𝐶)) ∧ 𝑦 ∈ (Base‘𝐶)) ∧ 𝑧 ∈ (Base‘𝐶)) ∧ 𝑓 ∈ (𝑥(Hom ‘𝐶)𝑦)) ∧ 𝑔 ∈ (𝑦(Hom ‘𝐶)𝑧)) → 𝑧 ∈ (Base‘𝐶)) |
92 | 91 | ad4antr 764 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. . 36
⊢
((((((((((𝜑 ∧
𝑥 ∈ (Base‘𝐶)) ∧ 𝑦 ∈ (Base‘𝐶)) ∧ 𝑧 ∈ (Base‘𝐶)) ∧ 𝑓 ∈ (𝑥(Hom ‘𝐶)𝑦)) ∧ 𝑔 ∈ (𝑦(Hom ‘𝐶)𝑧)) ∧ (𝑔(〈𝑥, 𝑦〉(comp‘𝐶)𝑧)𝑓) ∈ (𝑥(Hom ‘𝐶)𝑧)) ∧ 𝑤 ∈ (Base‘𝐶)) ∧ ℎ ∈ (𝑧(Hom ‘𝐶)𝑤)) ∧ (ℎ(〈𝑦, 𝑧〉(comp‘𝐶)𝑤)𝑔) ∈ (𝑦(Hom ‘𝐶)𝑤)) → 𝑧 ∈ (Base‘𝐶)) |
93 | | simp-4r 803 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. . 36
⊢
((((((((((𝜑 ∧
𝑥 ∈ (Base‘𝐶)) ∧ 𝑦 ∈ (Base‘𝐶)) ∧ 𝑧 ∈ (Base‘𝐶)) ∧ 𝑓 ∈ (𝑥(Hom ‘𝐶)𝑦)) ∧ 𝑔 ∈ (𝑦(Hom ‘𝐶)𝑧)) ∧ (𝑔(〈𝑥, 𝑦〉(comp‘𝐶)𝑧)𝑓) ∈ (𝑥(Hom ‘𝐶)𝑧)) ∧ 𝑤 ∈ (Base‘𝐶)) ∧ ℎ ∈ (𝑧(Hom ‘𝐶)𝑤)) ∧ (ℎ(〈𝑦, 𝑧〉(comp‘𝐶)𝑤)𝑔) ∈ (𝑦(Hom ‘𝐶)𝑤)) → (𝑔(〈𝑥, 𝑦〉(comp‘𝐶)𝑧)𝑓) ∈ (𝑥(Hom ‘𝐶)𝑧)) |
94 | | simplr 788 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. . 36
⊢
((((((((((𝜑 ∧
𝑥 ∈ (Base‘𝐶)) ∧ 𝑦 ∈ (Base‘𝐶)) ∧ 𝑧 ∈ (Base‘𝐶)) ∧ 𝑓 ∈ (𝑥(Hom ‘𝐶)𝑦)) ∧ 𝑔 ∈ (𝑦(Hom ‘𝐶)𝑧)) ∧ (𝑔(〈𝑥, 𝑦〉(comp‘𝐶)𝑧)𝑓) ∈ (𝑥(Hom ‘𝐶)𝑧)) ∧ 𝑤 ∈ (Base‘𝐶)) ∧ ℎ ∈ (𝑧(Hom ‘𝐶)𝑤)) ∧ (ℎ(〈𝑦, 𝑧〉(comp‘𝐶)𝑤)𝑔) ∈ (𝑦(Hom ‘𝐶)𝑤)) → ℎ ∈ (𝑧(Hom ‘𝐶)𝑤)) |
95 | 70, 71, 72, 73, 77, 80, 83, 92, 86, 93, 94 | comfeqval 16191 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. 35
⊢
((((((((((𝜑 ∧
𝑥 ∈ (Base‘𝐶)) ∧ 𝑦 ∈ (Base‘𝐶)) ∧ 𝑧 ∈ (Base‘𝐶)) ∧ 𝑓 ∈ (𝑥(Hom ‘𝐶)𝑦)) ∧ 𝑔 ∈ (𝑦(Hom ‘𝐶)𝑧)) ∧ (𝑔(〈𝑥, 𝑦〉(comp‘𝐶)𝑧)𝑓) ∈ (𝑥(Hom ‘𝐶)𝑧)) ∧ 𝑤 ∈ (Base‘𝐶)) ∧ ℎ ∈ (𝑧(Hom ‘𝐶)𝑤)) ∧ (ℎ(〈𝑦, 𝑧〉(comp‘𝐶)𝑤)𝑔) ∈ (𝑦(Hom ‘𝐶)𝑤)) → (ℎ(〈𝑥, 𝑧〉(comp‘𝐶)𝑤)(𝑔(〈𝑥, 𝑦〉(comp‘𝐶)𝑧)𝑓)) = (ℎ(〈𝑥, 𝑧〉(comp‘𝐷)𝑤)(𝑔(〈𝑥, 𝑦〉(comp‘𝐶)𝑧)𝑓))) |
96 | 90, 95 | eqeq12d 2625 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
34
⊢
((((((((((𝜑 ∧
𝑥 ∈ (Base‘𝐶)) ∧ 𝑦 ∈ (Base‘𝐶)) ∧ 𝑧 ∈ (Base‘𝐶)) ∧ 𝑓 ∈ (𝑥(Hom ‘𝐶)𝑦)) ∧ 𝑔 ∈ (𝑦(Hom ‘𝐶)𝑧)) ∧ (𝑔(〈𝑥, 𝑦〉(comp‘𝐶)𝑧)𝑓) ∈ (𝑥(Hom ‘𝐶)𝑧)) ∧ 𝑤 ∈ (Base‘𝐶)) ∧ ℎ ∈ (𝑧(Hom ‘𝐶)𝑤)) ∧ (ℎ(〈𝑦, 𝑧〉(comp‘𝐶)𝑤)𝑔) ∈ (𝑦(Hom ‘𝐶)𝑤)) → (((ℎ(〈𝑦, 𝑧〉(comp‘𝐶)𝑤)𝑔)(〈𝑥, 𝑦〉(comp‘𝐶)𝑤)𝑓) = (ℎ(〈𝑥, 𝑧〉(comp‘𝐶)𝑤)(𝑔(〈𝑥, 𝑦〉(comp‘𝐶)𝑧)𝑓)) ↔ ((ℎ(〈𝑦, 𝑧〉(comp‘𝐶)𝑤)𝑔)(〈𝑥, 𝑦〉(comp‘𝐷)𝑤)𝑓) = (ℎ(〈𝑥, 𝑧〉(comp‘𝐷)𝑤)(𝑔(〈𝑥, 𝑦〉(comp‘𝐶)𝑧)𝑓)))) |
97 | 96 | ex 449 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
33
⊢
(((((((((𝜑 ∧ 𝑥 ∈ (Base‘𝐶)) ∧ 𝑦 ∈ (Base‘𝐶)) ∧ 𝑧 ∈ (Base‘𝐶)) ∧ 𝑓 ∈ (𝑥(Hom ‘𝐶)𝑦)) ∧ 𝑔 ∈ (𝑦(Hom ‘𝐶)𝑧)) ∧ (𝑔(〈𝑥, 𝑦〉(comp‘𝐶)𝑧)𝑓) ∈ (𝑥(Hom ‘𝐶)𝑧)) ∧ 𝑤 ∈ (Base‘𝐶)) ∧ ℎ ∈ (𝑧(Hom ‘𝐶)𝑤)) → ((ℎ(〈𝑦, 𝑧〉(comp‘𝐶)𝑤)𝑔) ∈ (𝑦(Hom ‘𝐶)𝑤) → (((ℎ(〈𝑦, 𝑧〉(comp‘𝐶)𝑤)𝑔)(〈𝑥, 𝑦〉(comp‘𝐶)𝑤)𝑓) = (ℎ(〈𝑥, 𝑧〉(comp‘𝐶)𝑤)(𝑔(〈𝑥, 𝑦〉(comp‘𝐶)𝑧)𝑓)) ↔ ((ℎ(〈𝑦, 𝑧〉(comp‘𝐶)𝑤)𝑔)(〈𝑥, 𝑦〉(comp‘𝐷)𝑤)𝑓) = (ℎ(〈𝑥, 𝑧〉(comp‘𝐷)𝑤)(𝑔(〈𝑥, 𝑦〉(comp‘𝐶)𝑧)𝑓))))) |
98 | 97 | ralimdva 2945 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
32
⊢
((((((((𝜑 ∧ 𝑥 ∈ (Base‘𝐶)) ∧ 𝑦 ∈ (Base‘𝐶)) ∧ 𝑧 ∈ (Base‘𝐶)) ∧ 𝑓 ∈ (𝑥(Hom ‘𝐶)𝑦)) ∧ 𝑔 ∈ (𝑦(Hom ‘𝐶)𝑧)) ∧ (𝑔(〈𝑥, 𝑦〉(comp‘𝐶)𝑧)𝑓) ∈ (𝑥(Hom ‘𝐶)𝑧)) ∧ 𝑤 ∈ (Base‘𝐶)) → (∀ℎ ∈ (𝑧(Hom ‘𝐶)𝑤)(ℎ(〈𝑦, 𝑧〉(comp‘𝐶)𝑤)𝑔) ∈ (𝑦(Hom ‘𝐶)𝑤) → ∀ℎ ∈ (𝑧(Hom ‘𝐶)𝑤)(((ℎ(〈𝑦, 𝑧〉(comp‘𝐶)𝑤)𝑔)(〈𝑥, 𝑦〉(comp‘𝐶)𝑤)𝑓) = (ℎ(〈𝑥, 𝑧〉(comp‘𝐶)𝑤)(𝑔(〈𝑥, 𝑦〉(comp‘𝐶)𝑧)𝑓)) ↔ ((ℎ(〈𝑦, 𝑧〉(comp‘𝐶)𝑤)𝑔)(〈𝑥, 𝑦〉(comp‘𝐷)𝑤)𝑓) = (ℎ(〈𝑥, 𝑧〉(comp‘𝐷)𝑤)(𝑔(〈𝑥, 𝑦〉(comp‘𝐶)𝑧)𝑓))))) |
99 | | ralbi 3050 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
32
⊢
(∀ℎ ∈
(𝑧(Hom ‘𝐶)𝑤)(((ℎ(〈𝑦, 𝑧〉(comp‘𝐶)𝑤)𝑔)(〈𝑥, 𝑦〉(comp‘𝐶)𝑤)𝑓) = (ℎ(〈𝑥, 𝑧〉(comp‘𝐶)𝑤)(𝑔(〈𝑥, 𝑦〉(comp‘𝐶)𝑧)𝑓)) ↔ ((ℎ(〈𝑦, 𝑧〉(comp‘𝐶)𝑤)𝑔)(〈𝑥, 𝑦〉(comp‘𝐷)𝑤)𝑓) = (ℎ(〈𝑥, 𝑧〉(comp‘𝐷)𝑤)(𝑔(〈𝑥, 𝑦〉(comp‘𝐶)𝑧)𝑓))) → (∀ℎ ∈ (𝑧(Hom ‘𝐶)𝑤)((ℎ(〈𝑦, 𝑧〉(comp‘𝐶)𝑤)𝑔)(〈𝑥, 𝑦〉(comp‘𝐶)𝑤)𝑓) = (ℎ(〈𝑥, 𝑧〉(comp‘𝐶)𝑤)(𝑔(〈𝑥, 𝑦〉(comp‘𝐶)𝑧)𝑓)) ↔ ∀ℎ ∈ (𝑧(Hom ‘𝐶)𝑤)((ℎ(〈𝑦, 𝑧〉(comp‘𝐶)𝑤)𝑔)(〈𝑥, 𝑦〉(comp‘𝐷)𝑤)𝑓) = (ℎ(〈𝑥, 𝑧〉(comp‘𝐷)𝑤)(𝑔(〈𝑥, 𝑦〉(comp‘𝐶)𝑧)𝑓)))) |
100 | 98, 99 | syl6 34 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
31
⊢
((((((((𝜑 ∧ 𝑥 ∈ (Base‘𝐶)) ∧ 𝑦 ∈ (Base‘𝐶)) ∧ 𝑧 ∈ (Base‘𝐶)) ∧ 𝑓 ∈ (𝑥(Hom ‘𝐶)𝑦)) ∧ 𝑔 ∈ (𝑦(Hom ‘𝐶)𝑧)) ∧ (𝑔(〈𝑥, 𝑦〉(comp‘𝐶)𝑧)𝑓) ∈ (𝑥(Hom ‘𝐶)𝑧)) ∧ 𝑤 ∈ (Base‘𝐶)) → (∀ℎ ∈ (𝑧(Hom ‘𝐶)𝑤)(ℎ(〈𝑦, 𝑧〉(comp‘𝐶)𝑤)𝑔) ∈ (𝑦(Hom ‘𝐶)𝑤) → (∀ℎ ∈ (𝑧(Hom ‘𝐶)𝑤)((ℎ(〈𝑦, 𝑧〉(comp‘𝐶)𝑤)𝑔)(〈𝑥, 𝑦〉(comp‘𝐶)𝑤)𝑓) = (ℎ(〈𝑥, 𝑧〉(comp‘𝐶)𝑤)(𝑔(〈𝑥, 𝑦〉(comp‘𝐶)𝑧)𝑓)) ↔ ∀ℎ ∈ (𝑧(Hom ‘𝐶)𝑤)((ℎ(〈𝑦, 𝑧〉(comp‘𝐶)𝑤)𝑔)(〈𝑥, 𝑦〉(comp‘𝐷)𝑤)𝑓) = (ℎ(〈𝑥, 𝑧〉(comp‘𝐷)𝑤)(𝑔(〈𝑥, 𝑦〉(comp‘𝐶)𝑧)𝑓))))) |
101 | 100 | ralimdva 2945 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . .
30
⊢
(((((((𝜑 ∧ 𝑥 ∈ (Base‘𝐶)) ∧ 𝑦 ∈ (Base‘𝐶)) ∧ 𝑧 ∈ (Base‘𝐶)) ∧ 𝑓 ∈ (𝑥(Hom ‘𝐶)𝑦)) ∧ 𝑔 ∈ (𝑦(Hom ‘𝐶)𝑧)) ∧ (𝑔(〈𝑥, 𝑦〉(comp‘𝐶)𝑧)𝑓) ∈ (𝑥(Hom ‘𝐶)𝑧)) → (∀𝑤 ∈ (Base‘𝐶)∀ℎ ∈ (𝑧(Hom ‘𝐶)𝑤)(ℎ(〈𝑦, 𝑧〉(comp‘𝐶)𝑤)𝑔) ∈ (𝑦(Hom ‘𝐶)𝑤) → ∀𝑤 ∈ (Base‘𝐶)(∀ℎ ∈ (𝑧(Hom ‘𝐶)𝑤)((ℎ(〈𝑦, 𝑧〉(comp‘𝐶)𝑤)𝑔)(〈𝑥, 𝑦〉(comp‘𝐶)𝑤)𝑓) = (ℎ(〈𝑥, 𝑧〉(comp‘𝐶)𝑤)(𝑔(〈𝑥, 𝑦〉(comp‘𝐶)𝑧)𝑓)) ↔ ∀ℎ ∈ (𝑧(Hom ‘𝐶)𝑤)((ℎ(〈𝑦, 𝑧〉(comp‘𝐶)𝑤)𝑔)(〈𝑥, 𝑦〉(comp‘𝐷)𝑤)𝑓) = (ℎ(〈𝑥, 𝑧〉(comp‘𝐷)𝑤)(𝑔(〈𝑥, 𝑦〉(comp‘𝐶)𝑧)𝑓))))) |
102 | 101 | impancom 455 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29
⊢
(((((((𝜑 ∧ 𝑥 ∈ (Base‘𝐶)) ∧ 𝑦 ∈ (Base‘𝐶)) ∧ 𝑧 ∈ (Base‘𝐶)) ∧ 𝑓 ∈ (𝑥(Hom ‘𝐶)𝑦)) ∧ 𝑔 ∈ (𝑦(Hom ‘𝐶)𝑧)) ∧ ∀𝑤 ∈ (Base‘𝐶)∀ℎ ∈ (𝑧(Hom ‘𝐶)𝑤)(ℎ(〈𝑦, 𝑧〉(comp‘𝐶)𝑤)𝑔) ∈ (𝑦(Hom ‘𝐶)𝑤)) → ((𝑔(〈𝑥, 𝑦〉(comp‘𝐶)𝑧)𝑓) ∈ (𝑥(Hom ‘𝐶)𝑧) → ∀𝑤 ∈ (Base‘𝐶)(∀ℎ ∈ (𝑧(Hom ‘𝐶)𝑤)((ℎ(〈𝑦, 𝑧〉(comp‘𝐶)𝑤)𝑔)(〈𝑥, 𝑦〉(comp‘𝐶)𝑤)𝑓) = (ℎ(〈𝑥, 𝑧〉(comp‘𝐶)𝑤)(𝑔(〈𝑥, 𝑦〉(comp‘𝐶)𝑧)𝑓)) ↔ ∀ℎ ∈ (𝑧(Hom ‘𝐶)𝑤)((ℎ(〈𝑦, 𝑧〉(comp‘𝐶)𝑤)𝑔)(〈𝑥, 𝑦〉(comp‘𝐷)𝑤)𝑓) = (ℎ(〈𝑥, 𝑧〉(comp‘𝐷)𝑤)(𝑔(〈𝑥, 𝑦〉(comp‘𝐶)𝑧)𝑓))))) |
103 | 102 | impr 647 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . 28
⊢
(((((((𝜑 ∧ 𝑥 ∈ (Base‘𝐶)) ∧ 𝑦 ∈ (Base‘𝐶)) ∧ 𝑧 ∈ (Base‘𝐶)) ∧ 𝑓 ∈ (𝑥(Hom ‘𝐶)𝑦)) ∧ 𝑔 ∈ (𝑦(Hom ‘𝐶)𝑧)) ∧ (∀𝑤 ∈ (Base‘𝐶)∀ℎ ∈ (𝑧(Hom ‘𝐶)𝑤)(ℎ(〈𝑦, 𝑧〉(comp‘𝐶)𝑤)𝑔) ∈ (𝑦(Hom ‘𝐶)𝑤) ∧ (𝑔(〈𝑥, 𝑦〉(comp‘𝐶)𝑧)𝑓) ∈ (𝑥(Hom ‘𝐶)𝑧))) → ∀𝑤 ∈ (Base‘𝐶)(∀ℎ ∈ (𝑧(Hom ‘𝐶)𝑤)((ℎ(〈𝑦, 𝑧〉(comp‘𝐶)𝑤)𝑔)(〈𝑥, 𝑦〉(comp‘𝐶)𝑤)𝑓) = (ℎ(〈𝑥, 𝑧〉(comp‘𝐶)𝑤)(𝑔(〈𝑥, 𝑦〉(comp‘𝐶)𝑧)𝑓)) ↔ ∀ℎ ∈ (𝑧(Hom ‘𝐶)𝑤)((ℎ(〈𝑦, 𝑧〉(comp‘𝐶)𝑤)𝑔)(〈𝑥, 𝑦〉(comp‘𝐷)𝑤)𝑓) = (ℎ(〈𝑥, 𝑧〉(comp‘𝐷)𝑤)(𝑔(〈𝑥, 𝑦〉(comp‘𝐶)𝑧)𝑓)))) |
104 | | ralbi 3050 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . 28
⊢
(∀𝑤 ∈
(Base‘𝐶)(∀ℎ ∈ (𝑧(Hom ‘𝐶)𝑤)((ℎ(〈𝑦, 𝑧〉(comp‘𝐶)𝑤)𝑔)(〈𝑥, 𝑦〉(comp‘𝐶)𝑤)𝑓) = (ℎ(〈𝑥, 𝑧〉(comp‘𝐶)𝑤)(𝑔(〈𝑥, 𝑦〉(comp‘𝐶)𝑧)𝑓)) ↔ ∀ℎ ∈ (𝑧(Hom ‘𝐶)𝑤)((ℎ(〈𝑦, 𝑧〉(comp‘𝐶)𝑤)𝑔)(〈𝑥, 𝑦〉(comp‘𝐷)𝑤)𝑓) = (ℎ(〈𝑥, 𝑧〉(comp‘𝐷)𝑤)(𝑔(〈𝑥, 𝑦〉(comp‘𝐶)𝑧)𝑓))) → (∀𝑤 ∈ (Base‘𝐶)∀ℎ ∈ (𝑧(Hom ‘𝐶)𝑤)((ℎ(〈𝑦, 𝑧〉(comp‘𝐶)𝑤)𝑔)(〈𝑥, 𝑦〉(comp‘𝐶)𝑤)𝑓) = (ℎ(〈𝑥, 𝑧〉(comp‘𝐶)𝑤)(𝑔(〈𝑥, 𝑦〉(comp‘𝐶)𝑧)𝑓)) ↔ ∀𝑤 ∈ (Base‘𝐶)∀ℎ ∈ (𝑧(Hom ‘𝐶)𝑤)((ℎ(〈𝑦, 𝑧〉(comp‘𝐶)𝑤)𝑔)(〈𝑥, 𝑦〉(comp‘𝐷)𝑤)𝑓) = (ℎ(〈𝑥, 𝑧〉(comp‘𝐷)𝑤)(𝑔(〈𝑥, 𝑦〉(comp‘𝐶)𝑧)𝑓)))) |
105 | 103, 104 | syl 17 |
. . . . . . . . . . . . . . . . . . . . . . . . . . 27
⊢
(((((((𝜑 ∧ 𝑥 ∈ (Base‘𝐶)) ∧ 𝑦 ∈ (Base‘𝐶)) ∧ 𝑧 ∈ (Base‘𝐶)) ∧ 𝑓 ∈ (𝑥(Hom ‘𝐶)𝑦)) ∧ 𝑔 ∈ (𝑦(Hom ‘𝐶)𝑧)) ∧ (∀𝑤 ∈ (Base‘𝐶)∀ℎ ∈ (𝑧(Hom ‘𝐶)𝑤)(ℎ(〈𝑦, 𝑧〉(comp‘𝐶)𝑤)𝑔) ∈ (𝑦(Hom ‘𝐶)𝑤) ∧ (𝑔(〈𝑥, 𝑦〉(comp‘𝐶)𝑧)𝑓) ∈ (𝑥(Hom ‘𝐶)𝑧))) → (∀𝑤 ∈ (Base‘𝐶)∀ℎ ∈ (𝑧(Hom ‘𝐶)𝑤)((ℎ(〈𝑦, 𝑧〉(comp‘𝐶)𝑤)𝑔)(〈𝑥, 𝑦〉(comp‘𝐶)𝑤)𝑓) = (ℎ(〈𝑥, 𝑧〉(comp‘𝐶)𝑤)(𝑔(〈𝑥, 𝑦〉(comp‘𝐶)𝑧)𝑓)) ↔ ∀𝑤 ∈ (Base‘𝐶)∀ℎ ∈ (𝑧(Hom ‘𝐶)𝑤)((ℎ(〈𝑦, 𝑧〉(comp‘𝐶)𝑤)𝑔)(〈𝑥, 𝑦〉(comp‘𝐷)𝑤)𝑓) = (ℎ(〈𝑥, 𝑧〉(comp‘𝐷)𝑤)(𝑔(〈𝑥, 𝑦〉(comp‘𝐶)𝑧)𝑓)))) |
106 | 105 | anbi2d 736 |
. . . . . . . . . . . . . . . . . . . . . . . . . 26
⊢
(((((((𝜑 ∧ 𝑥 ∈ (Base‘𝐶)) ∧ 𝑦 ∈ (Base‘𝐶)) ∧ 𝑧 ∈ (Base‘𝐶)) ∧ 𝑓 ∈ (𝑥(Hom ‘𝐶)𝑦)) ∧ 𝑔 ∈ (𝑦(Hom ‘𝐶)𝑧)) ∧ (∀𝑤 ∈ (Base‘𝐶)∀ℎ ∈ (𝑧(Hom ‘𝐶)𝑤)(ℎ(〈𝑦, 𝑧〉(comp‘𝐶)𝑤)𝑔) ∈ (𝑦(Hom ‘𝐶)𝑤) ∧ (𝑔(〈𝑥, 𝑦〉(comp‘𝐶)𝑧)𝑓) ∈ (𝑥(Hom ‘𝐶)𝑧))) → (((𝑔(〈𝑥, 𝑦〉(comp‘𝐶)𝑧)𝑓) ∈ (𝑥(Hom ‘𝐶)𝑧) ∧ ∀𝑤 ∈ (Base‘𝐶)∀ℎ ∈ (𝑧(Hom ‘𝐶)𝑤)((ℎ(〈𝑦, 𝑧〉(comp‘𝐶)𝑤)𝑔)(〈𝑥, 𝑦〉(comp‘𝐶)𝑤)𝑓) = (ℎ(〈𝑥, 𝑧〉(comp‘𝐶)𝑤)(𝑔(〈𝑥, 𝑦〉(comp‘𝐶)𝑧)𝑓))) ↔ ((𝑔(〈𝑥, 𝑦〉(comp‘𝐶)𝑧)𝑓) ∈ (𝑥(Hom ‘𝐶)𝑧) ∧ ∀𝑤 ∈ (Base‘𝐶)∀ℎ ∈ (𝑧(Hom ‘𝐶)𝑤)((ℎ(〈𝑦, 𝑧〉(comp‘𝐶)𝑤)𝑔)(〈𝑥, 𝑦〉(comp‘𝐷)𝑤)𝑓) = (ℎ(〈𝑥, 𝑧〉(comp‘𝐷)𝑤)(𝑔(〈𝑥, 𝑦〉(comp‘𝐶)𝑧)𝑓))))) |
107 | 106 | ex 449 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
⊢
((((((𝜑 ∧ 𝑥 ∈ (Base‘𝐶)) ∧ 𝑦 ∈ (Base‘𝐶)) ∧ 𝑧 ∈ (Base‘𝐶)) ∧ 𝑓 ∈ (𝑥(Hom ‘𝐶)𝑦)) ∧ 𝑔 ∈ (𝑦(Hom ‘𝐶)𝑧)) → ((∀𝑤 ∈ (Base‘𝐶)∀ℎ ∈ (𝑧(Hom ‘𝐶)𝑤)(ℎ(〈𝑦, 𝑧〉(comp‘𝐶)𝑤)𝑔) ∈ (𝑦(Hom ‘𝐶)𝑤) ∧ (𝑔(〈𝑥, 𝑦〉(comp‘𝐶)𝑧)𝑓) ∈ (𝑥(Hom ‘𝐶)𝑧)) → (((𝑔(〈𝑥, 𝑦〉(comp‘𝐶)𝑧)𝑓) ∈ (𝑥(Hom ‘𝐶)𝑧) ∧ ∀𝑤 ∈ (Base‘𝐶)∀ℎ ∈ (𝑧(Hom ‘𝐶)𝑤)((ℎ(〈𝑦, 𝑧〉(comp‘𝐶)𝑤)𝑔)(〈𝑥, 𝑦〉(comp‘𝐶)𝑤)𝑓) = (ℎ(〈𝑥, 𝑧〉(comp‘𝐶)𝑤)(𝑔(〈𝑥, 𝑦〉(comp‘𝐶)𝑧)𝑓))) ↔ ((𝑔(〈𝑥, 𝑦〉(comp‘𝐶)𝑧)𝑓) ∈ (𝑥(Hom ‘𝐶)𝑧) ∧ ∀𝑤 ∈ (Base‘𝐶)∀ℎ ∈ (𝑧(Hom ‘𝐶)𝑤)((ℎ(〈𝑦, 𝑧〉(comp‘𝐶)𝑤)𝑔)(〈𝑥, 𝑦〉(comp‘𝐷)𝑤)𝑓) = (ℎ(〈𝑥, 𝑧〉(comp‘𝐷)𝑤)(𝑔(〈𝑥, 𝑦〉(comp‘𝐶)𝑧)𝑓)))))) |
108 | 107 | ralimdva 2945 |
. . . . . . . . . . . . . . . . . . . . . . . 24
⊢
(((((𝜑 ∧ 𝑥 ∈ (Base‘𝐶)) ∧ 𝑦 ∈ (Base‘𝐶)) ∧ 𝑧 ∈ (Base‘𝐶)) ∧ 𝑓 ∈ (𝑥(Hom ‘𝐶)𝑦)) → (∀𝑔 ∈ (𝑦(Hom ‘𝐶)𝑧)(∀𝑤 ∈ (Base‘𝐶)∀ℎ ∈ (𝑧(Hom ‘𝐶)𝑤)(ℎ(〈𝑦, 𝑧〉(comp‘𝐶)𝑤)𝑔) ∈ (𝑦(Hom ‘𝐶)𝑤) ∧ (𝑔(〈𝑥, 𝑦〉(comp‘𝐶)𝑧)𝑓) ∈ (𝑥(Hom ‘𝐶)𝑧)) → ∀𝑔 ∈ (𝑦(Hom ‘𝐶)𝑧)(((𝑔(〈𝑥, 𝑦〉(comp‘𝐶)𝑧)𝑓) ∈ (𝑥(Hom ‘𝐶)𝑧) ∧ ∀𝑤 ∈ (Base‘𝐶)∀ℎ ∈ (𝑧(Hom ‘𝐶)𝑤)((ℎ(〈𝑦, 𝑧〉(comp‘𝐶)𝑤)𝑔)(〈𝑥, 𝑦〉(comp‘𝐶)𝑤)𝑓) = (ℎ(〈𝑥, 𝑧〉(comp‘𝐶)𝑤)(𝑔(〈𝑥, 𝑦〉(comp‘𝐶)𝑧)𝑓))) ↔ ((𝑔(〈𝑥, 𝑦〉(comp‘𝐶)𝑧)𝑓) ∈ (𝑥(Hom ‘𝐶)𝑧) ∧ ∀𝑤 ∈ (Base‘𝐶)∀ℎ ∈ (𝑧(Hom ‘𝐶)𝑤)((ℎ(〈𝑦, 𝑧〉(comp‘𝐶)𝑤)𝑔)(〈𝑥, 𝑦〉(comp‘𝐷)𝑤)𝑓) = (ℎ(〈𝑥, 𝑧〉(comp‘𝐷)𝑤)(𝑔(〈𝑥, 𝑦〉(comp‘𝐶)𝑧)𝑓)))))) |
109 | 69, 108 | syl5bir 232 |
. . . . . . . . . . . . . . . . . . . . . . 23
⊢
(((((𝜑 ∧ 𝑥 ∈ (Base‘𝐶)) ∧ 𝑦 ∈ (Base‘𝐶)) ∧ 𝑧 ∈ (Base‘𝐶)) ∧ 𝑓 ∈ (𝑥(Hom ‘𝐶)𝑦)) → ((∀𝑔 ∈ (𝑦(Hom ‘𝐶)𝑧)∀𝑤 ∈ (Base‘𝐶)∀ℎ ∈ (𝑧(Hom ‘𝐶)𝑤)(ℎ(〈𝑦, 𝑧〉(comp‘𝐶)𝑤)𝑔) ∈ (𝑦(Hom ‘𝐶)𝑤) ∧ ∀𝑔 ∈ (𝑦(Hom ‘𝐶)𝑧)(𝑔(〈𝑥, 𝑦〉(comp‘𝐶)𝑧)𝑓) ∈ (𝑥(Hom ‘𝐶)𝑧)) → ∀𝑔 ∈ (𝑦(Hom ‘𝐶)𝑧)(((𝑔(〈𝑥, 𝑦〉(comp‘𝐶)𝑧)𝑓) ∈ (𝑥(Hom ‘𝐶)𝑧) ∧ ∀𝑤 ∈ (Base‘𝐶)∀ℎ ∈ (𝑧(Hom ‘𝐶)𝑤)((ℎ(〈𝑦, 𝑧〉(comp‘𝐶)𝑤)𝑔)(〈𝑥, 𝑦〉(comp‘𝐶)𝑤)𝑓) = (ℎ(〈𝑥, 𝑧〉(comp‘𝐶)𝑤)(𝑔(〈𝑥, 𝑦〉(comp‘𝐶)𝑧)𝑓))) ↔ ((𝑔(〈𝑥, 𝑦〉(comp‘𝐶)𝑧)𝑓) ∈ (𝑥(Hom ‘𝐶)𝑧) ∧ ∀𝑤 ∈ (Base‘𝐶)∀ℎ ∈ (𝑧(Hom ‘𝐶)𝑤)((ℎ(〈𝑦, 𝑧〉(comp‘𝐶)𝑤)𝑔)(〈𝑥, 𝑦〉(comp‘𝐷)𝑤)𝑓) = (ℎ(〈𝑥, 𝑧〉(comp‘𝐷)𝑤)(𝑔(〈𝑥, 𝑦〉(comp‘𝐶)𝑧)𝑓)))))) |
110 | 109 | expdimp 452 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢
((((((𝜑 ∧ 𝑥 ∈ (Base‘𝐶)) ∧ 𝑦 ∈ (Base‘𝐶)) ∧ 𝑧 ∈ (Base‘𝐶)) ∧ 𝑓 ∈ (𝑥(Hom ‘𝐶)𝑦)) ∧ ∀𝑔 ∈ (𝑦(Hom ‘𝐶)𝑧)∀𝑤 ∈ (Base‘𝐶)∀ℎ ∈ (𝑧(Hom ‘𝐶)𝑤)(ℎ(〈𝑦, 𝑧〉(comp‘𝐶)𝑤)𝑔) ∈ (𝑦(Hom ‘𝐶)𝑤)) → (∀𝑔 ∈ (𝑦(Hom ‘𝐶)𝑧)(𝑔(〈𝑥, 𝑦〉(comp‘𝐶)𝑧)𝑓) ∈ (𝑥(Hom ‘𝐶)𝑧) → ∀𝑔 ∈ (𝑦(Hom ‘𝐶)𝑧)(((𝑔(〈𝑥, 𝑦〉(comp‘𝐶)𝑧)𝑓) ∈ (𝑥(Hom ‘𝐶)𝑧) ∧ ∀𝑤 ∈ (Base‘𝐶)∀ℎ ∈ (𝑧(Hom ‘𝐶)𝑤)((ℎ(〈𝑦, 𝑧〉(comp‘𝐶)𝑤)𝑔)(〈𝑥, 𝑦〉(comp‘𝐶)𝑤)𝑓) = (ℎ(〈𝑥, 𝑧〉(comp‘𝐶)𝑤)(𝑔(〈𝑥, 𝑦〉(comp‘𝐶)𝑧)𝑓))) ↔ ((𝑔(〈𝑥, 𝑦〉(comp‘𝐶)𝑧)𝑓) ∈ (𝑥(Hom ‘𝐶)𝑧) ∧ ∀𝑤 ∈ (Base‘𝐶)∀ℎ ∈ (𝑧(Hom ‘𝐶)𝑤)((ℎ(〈𝑦, 𝑧〉(comp‘𝐶)𝑤)𝑔)(〈𝑥, 𝑦〉(comp‘𝐷)𝑤)𝑓) = (ℎ(〈𝑥, 𝑧〉(comp‘𝐷)𝑤)(𝑔(〈𝑥, 𝑦〉(comp‘𝐶)𝑧)𝑓)))))) |
111 | | ralbi 3050 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢
(∀𝑔 ∈
(𝑦(Hom ‘𝐶)𝑧)(((𝑔(〈𝑥, 𝑦〉(comp‘𝐶)𝑧)𝑓) ∈ (𝑥(Hom ‘𝐶)𝑧) ∧ ∀𝑤 ∈ (Base‘𝐶)∀ℎ ∈ (𝑧(Hom ‘𝐶)𝑤)((ℎ(〈𝑦, 𝑧〉(comp‘𝐶)𝑤)𝑔)(〈𝑥, 𝑦〉(comp‘𝐶)𝑤)𝑓) = (ℎ(〈𝑥, 𝑧〉(comp‘𝐶)𝑤)(𝑔(〈𝑥, 𝑦〉(comp‘𝐶)𝑧)𝑓))) ↔ ((𝑔(〈𝑥, 𝑦〉(comp‘𝐶)𝑧)𝑓) ∈ (𝑥(Hom ‘𝐶)𝑧) ∧ ∀𝑤 ∈ (Base‘𝐶)∀ℎ ∈ (𝑧(Hom ‘𝐶)𝑤)((ℎ(〈𝑦, 𝑧〉(comp‘𝐶)𝑤)𝑔)(〈𝑥, 𝑦〉(comp‘𝐷)𝑤)𝑓) = (ℎ(〈𝑥, 𝑧〉(comp‘𝐷)𝑤)(𝑔(〈𝑥, 𝑦〉(comp‘𝐶)𝑧)𝑓)))) → (∀𝑔 ∈ (𝑦(Hom ‘𝐶)𝑧)((𝑔(〈𝑥, 𝑦〉(comp‘𝐶)𝑧)𝑓) ∈ (𝑥(Hom ‘𝐶)𝑧) ∧ ∀𝑤 ∈ (Base‘𝐶)∀ℎ ∈ (𝑧(Hom ‘𝐶)𝑤)((ℎ(〈𝑦, 𝑧〉(comp‘𝐶)𝑤)𝑔)(〈𝑥, 𝑦〉(comp‘𝐶)𝑤)𝑓) = (ℎ(〈𝑥, 𝑧〉(comp‘𝐶)𝑤)(𝑔(〈𝑥, 𝑦〉(comp‘𝐶)𝑧)𝑓))) ↔ ∀𝑔 ∈ (𝑦(Hom ‘𝐶)𝑧)((𝑔(〈𝑥, 𝑦〉(comp‘𝐶)𝑧)𝑓) ∈ (𝑥(Hom ‘𝐶)𝑧) ∧ ∀𝑤 ∈ (Base‘𝐶)∀ℎ ∈ (𝑧(Hom ‘𝐶)𝑤)((ℎ(〈𝑦, 𝑧〉(comp‘𝐶)𝑤)𝑔)(〈𝑥, 𝑦〉(comp‘𝐷)𝑤)𝑓) = (ℎ(〈𝑥, 𝑧〉(comp‘𝐷)𝑤)(𝑔(〈𝑥, 𝑦〉(comp‘𝐶)𝑧)𝑓))))) |
112 | 110, 111 | syl6 34 |
. . . . . . . . . . . . . . . . . . . . 21
⊢
((((((𝜑 ∧ 𝑥 ∈ (Base‘𝐶)) ∧ 𝑦 ∈ (Base‘𝐶)) ∧ 𝑧 ∈ (Base‘𝐶)) ∧ 𝑓 ∈ (𝑥(Hom ‘𝐶)𝑦)) ∧ ∀𝑔 ∈ (𝑦(Hom ‘𝐶)𝑧)∀𝑤 ∈ (Base‘𝐶)∀ℎ ∈ (𝑧(Hom ‘𝐶)𝑤)(ℎ(〈𝑦, 𝑧〉(comp‘𝐶)𝑤)𝑔) ∈ (𝑦(Hom ‘𝐶)𝑤)) → (∀𝑔 ∈ (𝑦(Hom ‘𝐶)𝑧)(𝑔(〈𝑥, 𝑦〉(comp‘𝐶)𝑧)𝑓) ∈ (𝑥(Hom ‘𝐶)𝑧) → (∀𝑔 ∈ (𝑦(Hom ‘𝐶)𝑧)((𝑔(〈𝑥, 𝑦〉(comp‘𝐶)𝑧)𝑓) ∈ (𝑥(Hom ‘𝐶)𝑧) ∧ ∀𝑤 ∈ (Base‘𝐶)∀ℎ ∈ (𝑧(Hom ‘𝐶)𝑤)((ℎ(〈𝑦, 𝑧〉(comp‘𝐶)𝑤)𝑔)(〈𝑥, 𝑦〉(comp‘𝐶)𝑤)𝑓) = (ℎ(〈𝑥, 𝑧〉(comp‘𝐶)𝑤)(𝑔(〈𝑥, 𝑦〉(comp‘𝐶)𝑧)𝑓))) ↔ ∀𝑔 ∈ (𝑦(Hom ‘𝐶)𝑧)((𝑔(〈𝑥, 𝑦〉(comp‘𝐶)𝑧)𝑓) ∈ (𝑥(Hom ‘𝐶)𝑧) ∧ ∀𝑤 ∈ (Base‘𝐶)∀ℎ ∈ (𝑧(Hom ‘𝐶)𝑤)((ℎ(〈𝑦, 𝑧〉(comp‘𝐶)𝑤)𝑔)(〈𝑥, 𝑦〉(comp‘𝐷)𝑤)𝑓) = (ℎ(〈𝑥, 𝑧〉(comp‘𝐷)𝑤)(𝑔(〈𝑥, 𝑦〉(comp‘𝐶)𝑧)𝑓)))))) |
113 | 112 | an32s 842 |
. . . . . . . . . . . . . . . . . . . 20
⊢
((((((𝜑 ∧ 𝑥 ∈ (Base‘𝐶)) ∧ 𝑦 ∈ (Base‘𝐶)) ∧ 𝑧 ∈ (Base‘𝐶)) ∧ ∀𝑔 ∈ (𝑦(Hom ‘𝐶)𝑧)∀𝑤 ∈ (Base‘𝐶)∀ℎ ∈ (𝑧(Hom ‘𝐶)𝑤)(ℎ(〈𝑦, 𝑧〉(comp‘𝐶)𝑤)𝑔) ∈ (𝑦(Hom ‘𝐶)𝑤)) ∧ 𝑓 ∈ (𝑥(Hom ‘𝐶)𝑦)) → (∀𝑔 ∈ (𝑦(Hom ‘𝐶)𝑧)(𝑔(〈𝑥, 𝑦〉(comp‘𝐶)𝑧)𝑓) ∈ (𝑥(Hom ‘𝐶)𝑧) → (∀𝑔 ∈ (𝑦(Hom ‘𝐶)𝑧)((𝑔(〈𝑥, 𝑦〉(comp‘𝐶)𝑧)𝑓) ∈ (𝑥(Hom ‘𝐶)𝑧) ∧ ∀𝑤 ∈ (Base‘𝐶)∀ℎ ∈ (𝑧(Hom ‘𝐶)𝑤)((ℎ(〈𝑦, 𝑧〉(comp‘𝐶)𝑤)𝑔)(〈𝑥, 𝑦〉(comp‘𝐶)𝑤)𝑓) = (ℎ(〈𝑥, 𝑧〉(comp‘𝐶)𝑤)(𝑔(〈𝑥, 𝑦〉(comp‘𝐶)𝑧)𝑓))) ↔ ∀𝑔 ∈ (𝑦(Hom ‘𝐶)𝑧)((𝑔(〈𝑥, 𝑦〉(comp‘𝐶)𝑧)𝑓) ∈ (𝑥(Hom ‘𝐶)𝑧) ∧ ∀𝑤 ∈ (Base‘𝐶)∀ℎ ∈ (𝑧(Hom ‘𝐶)𝑤)((ℎ(〈𝑦, 𝑧〉(comp‘𝐶)𝑤)𝑔)(〈𝑥, 𝑦〉(comp‘𝐷)𝑤)𝑓) = (ℎ(〈𝑥, 𝑧〉(comp‘𝐷)𝑤)(𝑔(〈𝑥, 𝑦〉(comp‘𝐶)𝑧)𝑓)))))) |
114 | 113 | ralimdva 2945 |
. . . . . . . . . . . . . . . . . . 19
⊢
(((((𝜑 ∧ 𝑥 ∈ (Base‘𝐶)) ∧ 𝑦 ∈ (Base‘𝐶)) ∧ 𝑧 ∈ (Base‘𝐶)) ∧ ∀𝑔 ∈ (𝑦(Hom ‘𝐶)𝑧)∀𝑤 ∈ (Base‘𝐶)∀ℎ ∈ (𝑧(Hom ‘𝐶)𝑤)(ℎ(〈𝑦, 𝑧〉(comp‘𝐶)𝑤)𝑔) ∈ (𝑦(Hom ‘𝐶)𝑤)) → (∀𝑓 ∈ (𝑥(Hom ‘𝐶)𝑦)∀𝑔 ∈ (𝑦(Hom ‘𝐶)𝑧)(𝑔(〈𝑥, 𝑦〉(comp‘𝐶)𝑧)𝑓) ∈ (𝑥(Hom ‘𝐶)𝑧) → ∀𝑓 ∈ (𝑥(Hom ‘𝐶)𝑦)(∀𝑔 ∈ (𝑦(Hom ‘𝐶)𝑧)((𝑔(〈𝑥, 𝑦〉(comp‘𝐶)𝑧)𝑓) ∈ (𝑥(Hom ‘𝐶)𝑧) ∧ ∀𝑤 ∈ (Base‘𝐶)∀ℎ ∈ (𝑧(Hom ‘𝐶)𝑤)((ℎ(〈𝑦, 𝑧〉(comp‘𝐶)𝑤)𝑔)(〈𝑥, 𝑦〉(comp‘𝐶)𝑤)𝑓) = (ℎ(〈𝑥, 𝑧〉(comp‘𝐶)𝑤)(𝑔(〈𝑥, 𝑦〉(comp‘𝐶)𝑧)𝑓))) ↔ ∀𝑔 ∈ (𝑦(Hom ‘𝐶)𝑧)((𝑔(〈𝑥, 𝑦〉(comp‘𝐶)𝑧)𝑓) ∈ (𝑥(Hom ‘𝐶)𝑧) ∧ ∀𝑤 ∈ (Base‘𝐶)∀ℎ ∈ (𝑧(Hom ‘𝐶)𝑤)((ℎ(〈𝑦, 𝑧〉(comp‘𝐶)𝑤)𝑔)(〈𝑥, 𝑦〉(comp‘𝐷)𝑤)𝑓) = (ℎ(〈𝑥, 𝑧〉(comp‘𝐷)𝑤)(𝑔(〈𝑥, 𝑦〉(comp‘𝐶)𝑧)𝑓)))))) |
115 | | ralbi 3050 |
. . . . . . . . . . . . . . . . . . 19
⊢
(∀𝑓 ∈
(𝑥(Hom ‘𝐶)𝑦)(∀𝑔 ∈ (𝑦(Hom ‘𝐶)𝑧)((𝑔(〈𝑥, 𝑦〉(comp‘𝐶)𝑧)𝑓) ∈ (𝑥(Hom ‘𝐶)𝑧) ∧ ∀𝑤 ∈ (Base‘𝐶)∀ℎ ∈ (𝑧(Hom ‘𝐶)𝑤)((ℎ(〈𝑦, 𝑧〉(comp‘𝐶)𝑤)𝑔)(〈𝑥, 𝑦〉(comp‘𝐶)𝑤)𝑓) = (ℎ(〈𝑥, 𝑧〉(comp‘𝐶)𝑤)(𝑔(〈𝑥, 𝑦〉(comp‘𝐶)𝑧)𝑓))) ↔ ∀𝑔 ∈ (𝑦(Hom ‘𝐶)𝑧)((𝑔(〈𝑥, 𝑦〉(comp‘𝐶)𝑧)𝑓) ∈ (𝑥(Hom ‘𝐶)𝑧) ∧ ∀𝑤 ∈ (Base‘𝐶)∀ℎ ∈ (𝑧(Hom ‘𝐶)𝑤)((ℎ(〈𝑦, 𝑧〉(comp‘𝐶)𝑤)𝑔)(〈𝑥, 𝑦〉(comp‘𝐷)𝑤)𝑓) = (ℎ(〈𝑥, 𝑧〉(comp‘𝐷)𝑤)(𝑔(〈𝑥, 𝑦〉(comp‘𝐶)𝑧)𝑓)))) → (∀𝑓 ∈ (𝑥(Hom ‘𝐶)𝑦)∀𝑔 ∈ (𝑦(Hom ‘𝐶)𝑧)((𝑔(〈𝑥, 𝑦〉(comp‘𝐶)𝑧)𝑓) ∈ (𝑥(Hom ‘𝐶)𝑧) ∧ ∀𝑤 ∈ (Base‘𝐶)∀ℎ ∈ (𝑧(Hom ‘𝐶)𝑤)((ℎ(〈𝑦, 𝑧〉(comp‘𝐶)𝑤)𝑔)(〈𝑥, 𝑦〉(comp‘𝐶)𝑤)𝑓) = (ℎ(〈𝑥, 𝑧〉(comp‘𝐶)𝑤)(𝑔(〈𝑥, 𝑦〉(comp‘𝐶)𝑧)𝑓))) ↔ ∀𝑓 ∈ (𝑥(Hom ‘𝐶)𝑦)∀𝑔 ∈ (𝑦(Hom ‘𝐶)𝑧)((𝑔(〈𝑥, 𝑦〉(comp‘𝐶)𝑧)𝑓) ∈ (𝑥(Hom ‘𝐶)𝑧) ∧ ∀𝑤 ∈ (Base‘𝐶)∀ℎ ∈ (𝑧(Hom ‘𝐶)𝑤)((ℎ(〈𝑦, 𝑧〉(comp‘𝐶)𝑤)𝑔)(〈𝑥, 𝑦〉(comp‘𝐷)𝑤)𝑓) = (ℎ(〈𝑥, 𝑧〉(comp‘𝐷)𝑤)(𝑔(〈𝑥, 𝑦〉(comp‘𝐶)𝑧)𝑓))))) |
116 | 114, 115 | syl6 34 |
. . . . . . . . . . . . . . . . . 18
⊢
(((((𝜑 ∧ 𝑥 ∈ (Base‘𝐶)) ∧ 𝑦 ∈ (Base‘𝐶)) ∧ 𝑧 ∈ (Base‘𝐶)) ∧ ∀𝑔 ∈ (𝑦(Hom ‘𝐶)𝑧)∀𝑤 ∈ (Base‘𝐶)∀ℎ ∈ (𝑧(Hom ‘𝐶)𝑤)(ℎ(〈𝑦, 𝑧〉(comp‘𝐶)𝑤)𝑔) ∈ (𝑦(Hom ‘𝐶)𝑤)) → (∀𝑓 ∈ (𝑥(Hom ‘𝐶)𝑦)∀𝑔 ∈ (𝑦(Hom ‘𝐶)𝑧)(𝑔(〈𝑥, 𝑦〉(comp‘𝐶)𝑧)𝑓) ∈ (𝑥(Hom ‘𝐶)𝑧) → (∀𝑓 ∈ (𝑥(Hom ‘𝐶)𝑦)∀𝑔 ∈ (𝑦(Hom ‘𝐶)𝑧)((𝑔(〈𝑥, 𝑦〉(comp‘𝐶)𝑧)𝑓) ∈ (𝑥(Hom ‘𝐶)𝑧) ∧ ∀𝑤 ∈ (Base‘𝐶)∀ℎ ∈ (𝑧(Hom ‘𝐶)𝑤)((ℎ(〈𝑦, 𝑧〉(comp‘𝐶)𝑤)𝑔)(〈𝑥, 𝑦〉(comp‘𝐶)𝑤)𝑓) = (ℎ(〈𝑥, 𝑧〉(comp‘𝐶)𝑤)(𝑔(〈𝑥, 𝑦〉(comp‘𝐶)𝑧)𝑓))) ↔ ∀𝑓 ∈ (𝑥(Hom ‘𝐶)𝑦)∀𝑔 ∈ (𝑦(Hom ‘𝐶)𝑧)((𝑔(〈𝑥, 𝑦〉(comp‘𝐶)𝑧)𝑓) ∈ (𝑥(Hom ‘𝐶)𝑧) ∧ ∀𝑤 ∈ (Base‘𝐶)∀ℎ ∈ (𝑧(Hom ‘𝐶)𝑤)((ℎ(〈𝑦, 𝑧〉(comp‘𝐶)𝑤)𝑔)(〈𝑥, 𝑦〉(comp‘𝐷)𝑤)𝑓) = (ℎ(〈𝑥, 𝑧〉(comp‘𝐷)𝑤)(𝑔(〈𝑥, 𝑦〉(comp‘𝐶)𝑧)𝑓)))))) |
117 | 116 | expimpd 627 |
. . . . . . . . . . . . . . . . 17
⊢ ((((𝜑 ∧ 𝑥 ∈ (Base‘𝐶)) ∧ 𝑦 ∈ (Base‘𝐶)) ∧ 𝑧 ∈ (Base‘𝐶)) → ((∀𝑔 ∈ (𝑦(Hom ‘𝐶)𝑧)∀𝑤 ∈ (Base‘𝐶)∀ℎ ∈ (𝑧(Hom ‘𝐶)𝑤)(ℎ(〈𝑦, 𝑧〉(comp‘𝐶)𝑤)𝑔) ∈ (𝑦(Hom ‘𝐶)𝑤) ∧ ∀𝑓 ∈ (𝑥(Hom ‘𝐶)𝑦)∀𝑔 ∈ (𝑦(Hom ‘𝐶)𝑧)(𝑔(〈𝑥, 𝑦〉(comp‘𝐶)𝑧)𝑓) ∈ (𝑥(Hom ‘𝐶)𝑧)) → (∀𝑓 ∈ (𝑥(Hom ‘𝐶)𝑦)∀𝑔 ∈ (𝑦(Hom ‘𝐶)𝑧)((𝑔(〈𝑥, 𝑦〉(comp‘𝐶)𝑧)𝑓) ∈ (𝑥(Hom ‘𝐶)𝑧) ∧ ∀𝑤 ∈ (Base‘𝐶)∀ℎ ∈ (𝑧(Hom ‘𝐶)𝑤)((ℎ(〈𝑦, 𝑧〉(comp‘𝐶)𝑤)𝑔)(〈𝑥, 𝑦〉(comp‘𝐶)𝑤)𝑓) = (ℎ(〈𝑥, 𝑧〉(comp‘𝐶)𝑤)(𝑔(〈𝑥, 𝑦〉(comp‘𝐶)𝑧)𝑓))) ↔ ∀𝑓 ∈ (𝑥(Hom ‘𝐶)𝑦)∀𝑔 ∈ (𝑦(Hom ‘𝐶)𝑧)((𝑔(〈𝑥, 𝑦〉(comp‘𝐶)𝑧)𝑓) ∈ (𝑥(Hom ‘𝐶)𝑧) ∧ ∀𝑤 ∈ (Base‘𝐶)∀ℎ ∈ (𝑧(Hom ‘𝐶)𝑤)((ℎ(〈𝑦, 𝑧〉(comp‘𝐶)𝑤)𝑔)(〈𝑥, 𝑦〉(comp‘𝐷)𝑤)𝑓) = (ℎ(〈𝑥, 𝑧〉(comp‘𝐷)𝑤)(𝑔(〈𝑥, 𝑦〉(comp‘𝐶)𝑧)𝑓)))))) |
118 | 117 | ralimdva 2945 |
. . . . . . . . . . . . . . . 16
⊢ (((𝜑 ∧ 𝑥 ∈ (Base‘𝐶)) ∧ 𝑦 ∈ (Base‘𝐶)) → (∀𝑧 ∈ (Base‘𝐶)(∀𝑔 ∈ (𝑦(Hom ‘𝐶)𝑧)∀𝑤 ∈ (Base‘𝐶)∀ℎ ∈ (𝑧(Hom ‘𝐶)𝑤)(ℎ(〈𝑦, 𝑧〉(comp‘𝐶)𝑤)𝑔) ∈ (𝑦(Hom ‘𝐶)𝑤) ∧ ∀𝑓 ∈ (𝑥(Hom ‘𝐶)𝑦)∀𝑔 ∈ (𝑦(Hom ‘𝐶)𝑧)(𝑔(〈𝑥, 𝑦〉(comp‘𝐶)𝑧)𝑓) ∈ (𝑥(Hom ‘𝐶)𝑧)) → ∀𝑧 ∈ (Base‘𝐶)(∀𝑓 ∈ (𝑥(Hom ‘𝐶)𝑦)∀𝑔 ∈ (𝑦(Hom ‘𝐶)𝑧)((𝑔(〈𝑥, 𝑦〉(comp‘𝐶)𝑧)𝑓) ∈ (𝑥(Hom ‘𝐶)𝑧) ∧ ∀𝑤 ∈ (Base‘𝐶)∀ℎ ∈ (𝑧(Hom ‘𝐶)𝑤)((ℎ(〈𝑦, 𝑧〉(comp‘𝐶)𝑤)𝑔)(〈𝑥, 𝑦〉(comp‘𝐶)𝑤)𝑓) = (ℎ(〈𝑥, 𝑧〉(comp‘𝐶)𝑤)(𝑔(〈𝑥, 𝑦〉(comp‘𝐶)𝑧)𝑓))) ↔ ∀𝑓 ∈ (𝑥(Hom ‘𝐶)𝑦)∀𝑔 ∈ (𝑦(Hom ‘𝐶)𝑧)((𝑔(〈𝑥, 𝑦〉(comp‘𝐶)𝑧)𝑓) ∈ (𝑥(Hom ‘𝐶)𝑧) ∧ ∀𝑤 ∈ (Base‘𝐶)∀ℎ ∈ (𝑧(Hom ‘𝐶)𝑤)((ℎ(〈𝑦, 𝑧〉(comp‘𝐶)𝑤)𝑔)(〈𝑥, 𝑦〉(comp‘𝐷)𝑤)𝑓) = (ℎ(〈𝑥, 𝑧〉(comp‘𝐷)𝑤)(𝑔(〈𝑥, 𝑦〉(comp‘𝐶)𝑧)𝑓)))))) |
119 | | ralbi 3050 |
. . . . . . . . . . . . . . . 16
⊢
(∀𝑧 ∈
(Base‘𝐶)(∀𝑓 ∈ (𝑥(Hom ‘𝐶)𝑦)∀𝑔 ∈ (𝑦(Hom ‘𝐶)𝑧)((𝑔(〈𝑥, 𝑦〉(comp‘𝐶)𝑧)𝑓) ∈ (𝑥(Hom ‘𝐶)𝑧) ∧ ∀𝑤 ∈ (Base‘𝐶)∀ℎ ∈ (𝑧(Hom ‘𝐶)𝑤)((ℎ(〈𝑦, 𝑧〉(comp‘𝐶)𝑤)𝑔)(〈𝑥, 𝑦〉(comp‘𝐶)𝑤)𝑓) = (ℎ(〈𝑥, 𝑧〉(comp‘𝐶)𝑤)(𝑔(〈𝑥, 𝑦〉(comp‘𝐶)𝑧)𝑓))) ↔ ∀𝑓 ∈ (𝑥(Hom ‘𝐶)𝑦)∀𝑔 ∈ (𝑦(Hom ‘𝐶)𝑧)((𝑔(〈𝑥, 𝑦〉(comp‘𝐶)𝑧)𝑓) ∈ (𝑥(Hom ‘𝐶)𝑧) ∧ ∀𝑤 ∈ (Base‘𝐶)∀ℎ ∈ (𝑧(Hom ‘𝐶)𝑤)((ℎ(〈𝑦, 𝑧〉(comp‘𝐶)𝑤)𝑔)(〈𝑥, 𝑦〉(comp‘𝐷)𝑤)𝑓) = (ℎ(〈𝑥, 𝑧〉(comp‘𝐷)𝑤)(𝑔(〈𝑥, 𝑦〉(comp‘𝐶)𝑧)𝑓)))) → (∀𝑧 ∈ (Base‘𝐶)∀𝑓 ∈ (𝑥(Hom ‘𝐶)𝑦)∀𝑔 ∈ (𝑦(Hom ‘𝐶)𝑧)((𝑔(〈𝑥, 𝑦〉(comp‘𝐶)𝑧)𝑓) ∈ (𝑥(Hom ‘𝐶)𝑧) ∧ ∀𝑤 ∈ (Base‘𝐶)∀ℎ ∈ (𝑧(Hom ‘𝐶)𝑤)((ℎ(〈𝑦, 𝑧〉(comp‘𝐶)𝑤)𝑔)(〈𝑥, 𝑦〉(comp‘𝐶)𝑤)𝑓) = (ℎ(〈𝑥, 𝑧〉(comp‘𝐶)𝑤)(𝑔(〈𝑥, 𝑦〉(comp‘𝐶)𝑧)𝑓))) ↔ ∀𝑧 ∈ (Base‘𝐶)∀𝑓 ∈ (𝑥(Hom ‘𝐶)𝑦)∀𝑔 ∈ (𝑦(Hom ‘𝐶)𝑧)((𝑔(〈𝑥, 𝑦〉(comp‘𝐶)𝑧)𝑓) ∈ (𝑥(Hom ‘𝐶)𝑧) ∧ ∀𝑤 ∈ (Base‘𝐶)∀ℎ ∈ (𝑧(Hom ‘𝐶)𝑤)((ℎ(〈𝑦, 𝑧〉(comp‘𝐶)𝑤)𝑔)(〈𝑥, 𝑦〉(comp‘𝐷)𝑤)𝑓) = (ℎ(〈𝑥, 𝑧〉(comp‘𝐷)𝑤)(𝑔(〈𝑥, 𝑦〉(comp‘𝐶)𝑧)𝑓))))) |
120 | 118, 119 | syl6 34 |
. . . . . . . . . . . . . . 15
⊢ (((𝜑 ∧ 𝑥 ∈ (Base‘𝐶)) ∧ 𝑦 ∈ (Base‘𝐶)) → (∀𝑧 ∈ (Base‘𝐶)(∀𝑔 ∈ (𝑦(Hom ‘𝐶)𝑧)∀𝑤 ∈ (Base‘𝐶)∀ℎ ∈ (𝑧(Hom ‘𝐶)𝑤)(ℎ(〈𝑦, 𝑧〉(comp‘𝐶)𝑤)𝑔) ∈ (𝑦(Hom ‘𝐶)𝑤) ∧ ∀𝑓 ∈ (𝑥(Hom ‘𝐶)𝑦)∀𝑔 ∈ (𝑦(Hom ‘𝐶)𝑧)(𝑔(〈𝑥, 𝑦〉(comp‘𝐶)𝑧)𝑓) ∈ (𝑥(Hom ‘𝐶)𝑧)) → (∀𝑧 ∈ (Base‘𝐶)∀𝑓 ∈ (𝑥(Hom ‘𝐶)𝑦)∀𝑔 ∈ (𝑦(Hom ‘𝐶)𝑧)((𝑔(〈𝑥, 𝑦〉(comp‘𝐶)𝑧)𝑓) ∈ (𝑥(Hom ‘𝐶)𝑧) ∧ ∀𝑤 ∈ (Base‘𝐶)∀ℎ ∈ (𝑧(Hom ‘𝐶)𝑤)((ℎ(〈𝑦, 𝑧〉(comp‘𝐶)𝑤)𝑔)(〈𝑥, 𝑦〉(comp‘𝐶)𝑤)𝑓) = (ℎ(〈𝑥, 𝑧〉(comp‘𝐶)𝑤)(𝑔(〈𝑥, 𝑦〉(comp‘𝐶)𝑧)𝑓))) ↔ ∀𝑧 ∈ (Base‘𝐶)∀𝑓 ∈ (𝑥(Hom ‘𝐶)𝑦)∀𝑔 ∈ (𝑦(Hom ‘𝐶)𝑧)((𝑔(〈𝑥, 𝑦〉(comp‘𝐶)𝑧)𝑓) ∈ (𝑥(Hom ‘𝐶)𝑧) ∧ ∀𝑤 ∈ (Base‘𝐶)∀ℎ ∈ (𝑧(Hom ‘𝐶)𝑤)((ℎ(〈𝑦, 𝑧〉(comp‘𝐶)𝑤)𝑔)(〈𝑥, 𝑦〉(comp‘𝐷)𝑤)𝑓) = (ℎ(〈𝑥, 𝑧〉(comp‘𝐷)𝑤)(𝑔(〈𝑥, 𝑦〉(comp‘𝐶)𝑧)𝑓)))))) |
121 | 68, 120 | syl5bir 232 |
. . . . . . . . . . . . . 14
⊢ (((𝜑 ∧ 𝑥 ∈ (Base‘𝐶)) ∧ 𝑦 ∈ (Base‘𝐶)) → ((∀𝑧 ∈ (Base‘𝐶)∀𝑔 ∈ (𝑦(Hom ‘𝐶)𝑧)∀𝑤 ∈ (Base‘𝐶)∀ℎ ∈ (𝑧(Hom ‘𝐶)𝑤)(ℎ(〈𝑦, 𝑧〉(comp‘𝐶)𝑤)𝑔) ∈ (𝑦(Hom ‘𝐶)𝑤) ∧ ∀𝑧 ∈ (Base‘𝐶)∀𝑓 ∈ (𝑥(Hom ‘𝐶)𝑦)∀𝑔 ∈ (𝑦(Hom ‘𝐶)𝑧)(𝑔(〈𝑥, 𝑦〉(comp‘𝐶)𝑧)𝑓) ∈ (𝑥(Hom ‘𝐶)𝑧)) → (∀𝑧 ∈ (Base‘𝐶)∀𝑓 ∈ (𝑥(Hom ‘𝐶)𝑦)∀𝑔 ∈ (𝑦(Hom ‘𝐶)𝑧)((𝑔(〈𝑥, 𝑦〉(comp‘𝐶)𝑧)𝑓) ∈ (𝑥(Hom ‘𝐶)𝑧) ∧ ∀𝑤 ∈ (Base‘𝐶)∀ℎ ∈ (𝑧(Hom ‘𝐶)𝑤)((ℎ(〈𝑦, 𝑧〉(comp‘𝐶)𝑤)𝑔)(〈𝑥, 𝑦〉(comp‘𝐶)𝑤)𝑓) = (ℎ(〈𝑥, 𝑧〉(comp‘𝐶)𝑤)(𝑔(〈𝑥, 𝑦〉(comp‘𝐶)𝑧)𝑓))) ↔ ∀𝑧 ∈ (Base‘𝐶)∀𝑓 ∈ (𝑥(Hom ‘𝐶)𝑦)∀𝑔 ∈ (𝑦(Hom ‘𝐶)𝑧)((𝑔(〈𝑥, 𝑦〉(comp‘𝐶)𝑧)𝑓) ∈ (𝑥(Hom ‘𝐶)𝑧) ∧ ∀𝑤 ∈ (Base‘𝐶)∀ℎ ∈ (𝑧(Hom ‘𝐶)𝑤)((ℎ(〈𝑦, 𝑧〉(comp‘𝐶)𝑤)𝑔)(〈𝑥, 𝑦〉(comp‘𝐷)𝑤)𝑓) = (ℎ(〈𝑥, 𝑧〉(comp‘𝐷)𝑤)(𝑔(〈𝑥, 𝑦〉(comp‘𝐶)𝑧)𝑓)))))) |
122 | 121 | ralimdva 2945 |
. . . . . . . . . . . . 13
⊢ ((𝜑 ∧ 𝑥 ∈ (Base‘𝐶)) → (∀𝑦 ∈ (Base‘𝐶)(∀𝑧 ∈ (Base‘𝐶)∀𝑔 ∈ (𝑦(Hom ‘𝐶)𝑧)∀𝑤 ∈ (Base‘𝐶)∀ℎ ∈ (𝑧(Hom ‘𝐶)𝑤)(ℎ(〈𝑦, 𝑧〉(comp‘𝐶)𝑤)𝑔) ∈ (𝑦(Hom ‘𝐶)𝑤) ∧ ∀𝑧 ∈ (Base‘𝐶)∀𝑓 ∈ (𝑥(Hom ‘𝐶)𝑦)∀𝑔 ∈ (𝑦(Hom ‘𝐶)𝑧)(𝑔(〈𝑥, 𝑦〉(comp‘𝐶)𝑧)𝑓) ∈ (𝑥(Hom ‘𝐶)𝑧)) → ∀𝑦 ∈ (Base‘𝐶)(∀𝑧 ∈ (Base‘𝐶)∀𝑓 ∈ (𝑥(Hom ‘𝐶)𝑦)∀𝑔 ∈ (𝑦(Hom ‘𝐶)𝑧)((𝑔(〈𝑥, 𝑦〉(comp‘𝐶)𝑧)𝑓) ∈ (𝑥(Hom ‘𝐶)𝑧) ∧ ∀𝑤 ∈ (Base‘𝐶)∀ℎ ∈ (𝑧(Hom ‘𝐶)𝑤)((ℎ(〈𝑦, 𝑧〉(comp‘𝐶)𝑤)𝑔)(〈𝑥, 𝑦〉(comp‘𝐶)𝑤)𝑓) = (ℎ(〈𝑥, 𝑧〉(comp‘𝐶)𝑤)(𝑔(〈𝑥, 𝑦〉(comp‘𝐶)𝑧)𝑓))) ↔ ∀𝑧 ∈ (Base‘𝐶)∀𝑓 ∈ (𝑥(Hom ‘𝐶)𝑦)∀𝑔 ∈ (𝑦(Hom ‘𝐶)𝑧)((𝑔(〈𝑥, 𝑦〉(comp‘𝐶)𝑧)𝑓) ∈ (𝑥(Hom ‘𝐶)𝑧) ∧ ∀𝑤 ∈ (Base‘𝐶)∀ℎ ∈ (𝑧(Hom ‘𝐶)𝑤)((ℎ(〈𝑦, 𝑧〉(comp‘𝐶)𝑤)𝑔)(〈𝑥, 𝑦〉(comp‘𝐷)𝑤)𝑓) = (ℎ(〈𝑥, 𝑧〉(comp‘𝐷)𝑤)(𝑔(〈𝑥, 𝑦〉(comp‘𝐶)𝑧)𝑓)))))) |
123 | | ralbi 3050 |
. . . . . . . . . . . . 13
⊢
(∀𝑦 ∈
(Base‘𝐶)(∀𝑧 ∈ (Base‘𝐶)∀𝑓 ∈ (𝑥(Hom ‘𝐶)𝑦)∀𝑔 ∈ (𝑦(Hom ‘𝐶)𝑧)((𝑔(〈𝑥, 𝑦〉(comp‘𝐶)𝑧)𝑓) ∈ (𝑥(Hom ‘𝐶)𝑧) ∧ ∀𝑤 ∈ (Base‘𝐶)∀ℎ ∈ (𝑧(Hom ‘𝐶)𝑤)((ℎ(〈𝑦, 𝑧〉(comp‘𝐶)𝑤)𝑔)(〈𝑥, 𝑦〉(comp‘𝐶)𝑤)𝑓) = (ℎ(〈𝑥, 𝑧〉(comp‘𝐶)𝑤)(𝑔(〈𝑥, 𝑦〉(comp‘𝐶)𝑧)𝑓))) ↔ ∀𝑧 ∈ (Base‘𝐶)∀𝑓 ∈ (𝑥(Hom ‘𝐶)𝑦)∀𝑔 ∈ (𝑦(Hom ‘𝐶)𝑧)((𝑔(〈𝑥, 𝑦〉(comp‘𝐶)𝑧)𝑓) ∈ (𝑥(Hom ‘𝐶)𝑧) ∧ ∀𝑤 ∈ (Base‘𝐶)∀ℎ ∈ (𝑧(Hom ‘𝐶)𝑤)((ℎ(〈𝑦, 𝑧〉(comp‘𝐶)𝑤)𝑔)(〈𝑥, 𝑦〉(comp‘𝐷)𝑤)𝑓) = (ℎ(〈𝑥, 𝑧〉(comp‘𝐷)𝑤)(𝑔(〈𝑥, 𝑦〉(comp‘𝐶)𝑧)𝑓)))) → (∀𝑦 ∈ (Base‘𝐶)∀𝑧 ∈ (Base‘𝐶)∀𝑓 ∈ (𝑥(Hom ‘𝐶)𝑦)∀𝑔 ∈ (𝑦(Hom ‘𝐶)𝑧)((𝑔(〈𝑥, 𝑦〉(comp‘𝐶)𝑧)𝑓) ∈ (𝑥(Hom ‘𝐶)𝑧) ∧ ∀𝑤 ∈ (Base‘𝐶)∀ℎ ∈ (𝑧(Hom ‘𝐶)𝑤)((ℎ(〈𝑦, 𝑧〉(comp‘𝐶)𝑤)𝑔)(〈𝑥, 𝑦〉(comp‘𝐶)𝑤)𝑓) = (ℎ(〈𝑥, 𝑧〉(comp‘𝐶)𝑤)(𝑔(〈𝑥, 𝑦〉(comp‘𝐶)𝑧)𝑓))) ↔ ∀𝑦 ∈ (Base‘𝐶)∀𝑧 ∈ (Base‘𝐶)∀𝑓 ∈ (𝑥(Hom ‘𝐶)𝑦)∀𝑔 ∈ (𝑦(Hom ‘𝐶)𝑧)((𝑔(〈𝑥, 𝑦〉(comp‘𝐶)𝑧)𝑓) ∈ (𝑥(Hom ‘𝐶)𝑧) ∧ ∀𝑤 ∈ (Base‘𝐶)∀ℎ ∈ (𝑧(Hom ‘𝐶)𝑤)((ℎ(〈𝑦, 𝑧〉(comp‘𝐶)𝑤)𝑔)(〈𝑥, 𝑦〉(comp‘𝐷)𝑤)𝑓) = (ℎ(〈𝑥, 𝑧〉(comp‘𝐷)𝑤)(𝑔(〈𝑥, 𝑦〉(comp‘𝐶)𝑧)𝑓))))) |
124 | 122, 123 | syl6 34 |
. . . . . . . . . . . 12
⊢ ((𝜑 ∧ 𝑥 ∈ (Base‘𝐶)) → (∀𝑦 ∈ (Base‘𝐶)(∀𝑧 ∈ (Base‘𝐶)∀𝑔 ∈ (𝑦(Hom ‘𝐶)𝑧)∀𝑤 ∈ (Base‘𝐶)∀ℎ ∈ (𝑧(Hom ‘𝐶)𝑤)(ℎ(〈𝑦, 𝑧〉(comp‘𝐶)𝑤)𝑔) ∈ (𝑦(Hom ‘𝐶)𝑤) ∧ ∀𝑧 ∈ (Base‘𝐶)∀𝑓 ∈ (𝑥(Hom ‘𝐶)𝑦)∀𝑔 ∈ (𝑦(Hom ‘𝐶)𝑧)(𝑔(〈𝑥, 𝑦〉(comp‘𝐶)𝑧)𝑓) ∈ (𝑥(Hom ‘𝐶)𝑧)) → (∀𝑦 ∈ (Base‘𝐶)∀𝑧 ∈ (Base‘𝐶)∀𝑓 ∈ (𝑥(Hom ‘𝐶)𝑦)∀𝑔 ∈ (𝑦(Hom ‘𝐶)𝑧)((𝑔(〈𝑥, 𝑦〉(comp‘𝐶)𝑧)𝑓) ∈ (𝑥(Hom ‘𝐶)𝑧) ∧ ∀𝑤 ∈ (Base‘𝐶)∀ℎ ∈ (𝑧(Hom ‘𝐶)𝑤)((ℎ(〈𝑦, 𝑧〉(comp‘𝐶)𝑤)𝑔)(〈𝑥, 𝑦〉(comp‘𝐶)𝑤)𝑓) = (ℎ(〈𝑥, 𝑧〉(comp‘𝐶)𝑤)(𝑔(〈𝑥, 𝑦〉(comp‘𝐶)𝑧)𝑓))) ↔ ∀𝑦 ∈ (Base‘𝐶)∀𝑧 ∈ (Base‘𝐶)∀𝑓 ∈ (𝑥(Hom ‘𝐶)𝑦)∀𝑔 ∈ (𝑦(Hom ‘𝐶)𝑧)((𝑔(〈𝑥, 𝑦〉(comp‘𝐶)𝑧)𝑓) ∈ (𝑥(Hom ‘𝐶)𝑧) ∧ ∀𝑤 ∈ (Base‘𝐶)∀ℎ ∈ (𝑧(Hom ‘𝐶)𝑤)((ℎ(〈𝑦, 𝑧〉(comp‘𝐶)𝑤)𝑔)(〈𝑥, 𝑦〉(comp‘𝐷)𝑤)𝑓) = (ℎ(〈𝑥, 𝑧〉(comp‘𝐷)𝑤)(𝑔(〈𝑥, 𝑦〉(comp‘𝐶)𝑧)𝑓)))))) |
125 | 67, 124 | syl5bir 232 |
. . . . . . . . . . 11
⊢ ((𝜑 ∧ 𝑥 ∈ (Base‘𝐶)) → ((∀𝑦 ∈ (Base‘𝐶)∀𝑧 ∈ (Base‘𝐶)∀𝑔 ∈ (𝑦(Hom ‘𝐶)𝑧)∀𝑤 ∈ (Base‘𝐶)∀ℎ ∈ (𝑧(Hom ‘𝐶)𝑤)(ℎ(〈𝑦, 𝑧〉(comp‘𝐶)𝑤)𝑔) ∈ (𝑦(Hom ‘𝐶)𝑤) ∧ ∀𝑦 ∈ (Base‘𝐶)∀𝑧 ∈ (Base‘𝐶)∀𝑓 ∈ (𝑥(Hom ‘𝐶)𝑦)∀𝑔 ∈ (𝑦(Hom ‘𝐶)𝑧)(𝑔(〈𝑥, 𝑦〉(comp‘𝐶)𝑧)𝑓) ∈ (𝑥(Hom ‘𝐶)𝑧)) → (∀𝑦 ∈ (Base‘𝐶)∀𝑧 ∈ (Base‘𝐶)∀𝑓 ∈ (𝑥(Hom ‘𝐶)𝑦)∀𝑔 ∈ (𝑦(Hom ‘𝐶)𝑧)((𝑔(〈𝑥, 𝑦〉(comp‘𝐶)𝑧)𝑓) ∈ (𝑥(Hom ‘𝐶)𝑧) ∧ ∀𝑤 ∈ (Base‘𝐶)∀ℎ ∈ (𝑧(Hom ‘𝐶)𝑤)((ℎ(〈𝑦, 𝑧〉(comp‘𝐶)𝑤)𝑔)(〈𝑥, 𝑦〉(comp‘𝐶)𝑤)𝑓) = (ℎ(〈𝑥, 𝑧〉(comp‘𝐶)𝑤)(𝑔(〈𝑥, 𝑦〉(comp‘𝐶)𝑧)𝑓))) ↔ ∀𝑦 ∈ (Base‘𝐶)∀𝑧 ∈ (Base‘𝐶)∀𝑓 ∈ (𝑥(Hom ‘𝐶)𝑦)∀𝑔 ∈ (𝑦(Hom ‘𝐶)𝑧)((𝑔(〈𝑥, 𝑦〉(comp‘𝐶)𝑧)𝑓) ∈ (𝑥(Hom ‘𝐶)𝑧) ∧ ∀𝑤 ∈ (Base‘𝐶)∀ℎ ∈ (𝑧(Hom ‘𝐶)𝑤)((ℎ(〈𝑦, 𝑧〉(comp‘𝐶)𝑤)𝑔)(〈𝑥, 𝑦〉(comp‘𝐷)𝑤)𝑓) = (ℎ(〈𝑥, 𝑧〉(comp‘𝐷)𝑤)(𝑔(〈𝑥, 𝑦〉(comp‘𝐶)𝑧)𝑓)))))) |
126 | 125 | imp 444 |
. . . . . . . . . 10
⊢ (((𝜑 ∧ 𝑥 ∈ (Base‘𝐶)) ∧ (∀𝑦 ∈ (Base‘𝐶)∀𝑧 ∈ (Base‘𝐶)∀𝑔 ∈ (𝑦(Hom ‘𝐶)𝑧)∀𝑤 ∈ (Base‘𝐶)∀ℎ ∈ (𝑧(Hom ‘𝐶)𝑤)(ℎ(〈𝑦, 𝑧〉(comp‘𝐶)𝑤)𝑔) ∈ (𝑦(Hom ‘𝐶)𝑤) ∧ ∀𝑦 ∈ (Base‘𝐶)∀𝑧 ∈ (Base‘𝐶)∀𝑓 ∈ (𝑥(Hom ‘𝐶)𝑦)∀𝑔 ∈ (𝑦(Hom ‘𝐶)𝑧)(𝑔(〈𝑥, 𝑦〉(comp‘𝐶)𝑧)𝑓) ∈ (𝑥(Hom ‘𝐶)𝑧))) → (∀𝑦 ∈ (Base‘𝐶)∀𝑧 ∈ (Base‘𝐶)∀𝑓 ∈ (𝑥(Hom ‘𝐶)𝑦)∀𝑔 ∈ (𝑦(Hom ‘𝐶)𝑧)((𝑔(〈𝑥, 𝑦〉(comp‘𝐶)𝑧)𝑓) ∈ (𝑥(Hom ‘𝐶)𝑧) ∧ ∀𝑤 ∈ (Base‘𝐶)∀ℎ ∈ (𝑧(Hom ‘𝐶)𝑤)((ℎ(〈𝑦, 𝑧〉(comp‘𝐶)𝑤)𝑔)(〈𝑥, 𝑦〉(comp‘𝐶)𝑤)𝑓) = (ℎ(〈𝑥, 𝑧〉(comp‘𝐶)𝑤)(𝑔(〈𝑥, 𝑦〉(comp‘𝐶)𝑧)𝑓))) ↔ ∀𝑦 ∈ (Base‘𝐶)∀𝑧 ∈ (Base‘𝐶)∀𝑓 ∈ (𝑥(Hom ‘𝐶)𝑦)∀𝑔 ∈ (𝑦(Hom ‘𝐶)𝑧)((𝑔(〈𝑥, 𝑦〉(comp‘𝐶)𝑧)𝑓) ∈ (𝑥(Hom ‘𝐶)𝑧) ∧ ∀𝑤 ∈ (Base‘𝐶)∀ℎ ∈ (𝑧(Hom ‘𝐶)𝑤)((ℎ(〈𝑦, 𝑧〉(comp‘𝐶)𝑤)𝑔)(〈𝑥, 𝑦〉(comp‘𝐷)𝑤)𝑓) = (ℎ(〈𝑥, 𝑧〉(comp‘𝐷)𝑤)(𝑔(〈𝑥, 𝑦〉(comp‘𝐶)𝑧)𝑓))))) |
127 | 126 | an4s 865 |
. . . . . . . . 9
⊢ (((𝜑 ∧ ∀𝑦 ∈ (Base‘𝐶)∀𝑧 ∈ (Base‘𝐶)∀𝑔 ∈ (𝑦(Hom ‘𝐶)𝑧)∀𝑤 ∈ (Base‘𝐶)∀ℎ ∈ (𝑧(Hom ‘𝐶)𝑤)(ℎ(〈𝑦, 𝑧〉(comp‘𝐶)𝑤)𝑔) ∈ (𝑦(Hom ‘𝐶)𝑤)) ∧ (𝑥 ∈ (Base‘𝐶) ∧ ∀𝑦 ∈ (Base‘𝐶)∀𝑧 ∈ (Base‘𝐶)∀𝑓 ∈ (𝑥(Hom ‘𝐶)𝑦)∀𝑔 ∈ (𝑦(Hom ‘𝐶)𝑧)(𝑔(〈𝑥, 𝑦〉(comp‘𝐶)𝑧)𝑓) ∈ (𝑥(Hom ‘𝐶)𝑧))) → (∀𝑦 ∈ (Base‘𝐶)∀𝑧 ∈ (Base‘𝐶)∀𝑓 ∈ (𝑥(Hom ‘𝐶)𝑦)∀𝑔 ∈ (𝑦(Hom ‘𝐶)𝑧)((𝑔(〈𝑥, 𝑦〉(comp‘𝐶)𝑧)𝑓) ∈ (𝑥(Hom ‘𝐶)𝑧) ∧ ∀𝑤 ∈ (Base‘𝐶)∀ℎ ∈ (𝑧(Hom ‘𝐶)𝑤)((ℎ(〈𝑦, 𝑧〉(comp‘𝐶)𝑤)𝑔)(〈𝑥, 𝑦〉(comp‘𝐶)𝑤)𝑓) = (ℎ(〈𝑥, 𝑧〉(comp‘𝐶)𝑤)(𝑔(〈𝑥, 𝑦〉(comp‘𝐶)𝑧)𝑓))) ↔ ∀𝑦 ∈ (Base‘𝐶)∀𝑧 ∈ (Base‘𝐶)∀𝑓 ∈ (𝑥(Hom ‘𝐶)𝑦)∀𝑔 ∈ (𝑦(Hom ‘𝐶)𝑧)((𝑔(〈𝑥, 𝑦〉(comp‘𝐶)𝑧)𝑓) ∈ (𝑥(Hom ‘𝐶)𝑧) ∧ ∀𝑤 ∈ (Base‘𝐶)∀ℎ ∈ (𝑧(Hom ‘𝐶)𝑤)((ℎ(〈𝑦, 𝑧〉(comp‘𝐶)𝑤)𝑔)(〈𝑥, 𝑦〉(comp‘𝐷)𝑤)𝑓) = (ℎ(〈𝑥, 𝑧〉(comp‘𝐷)𝑤)(𝑔(〈𝑥, 𝑦〉(comp‘𝐶)𝑧)𝑓))))) |
128 | 127 | anbi2d 736 |
. . . . . . . 8
⊢ (((𝜑 ∧ ∀𝑦 ∈ (Base‘𝐶)∀𝑧 ∈ (Base‘𝐶)∀𝑔 ∈ (𝑦(Hom ‘𝐶)𝑧)∀𝑤 ∈ (Base‘𝐶)∀ℎ ∈ (𝑧(Hom ‘𝐶)𝑤)(ℎ(〈𝑦, 𝑧〉(comp‘𝐶)𝑤)𝑔) ∈ (𝑦(Hom ‘𝐶)𝑤)) ∧ (𝑥 ∈ (Base‘𝐶) ∧ ∀𝑦 ∈ (Base‘𝐶)∀𝑧 ∈ (Base‘𝐶)∀𝑓 ∈ (𝑥(Hom ‘𝐶)𝑦)∀𝑔 ∈ (𝑦(Hom ‘𝐶)𝑧)(𝑔(〈𝑥, 𝑦〉(comp‘𝐶)𝑧)𝑓) ∈ (𝑥(Hom ‘𝐶)𝑧))) → ((∃𝑔 ∈ (𝑥(Hom ‘𝐶)𝑥)∀𝑦 ∈ (Base‘𝐶)(∀𝑓 ∈ (𝑦(Hom ‘𝐶)𝑥)(𝑔(〈𝑦, 𝑥〉(comp‘𝐶)𝑥)𝑓) = 𝑓 ∧ ∀𝑓 ∈ (𝑥(Hom ‘𝐶)𝑦)(𝑓(〈𝑥, 𝑥〉(comp‘𝐶)𝑦)𝑔) = 𝑓) ∧ ∀𝑦 ∈ (Base‘𝐶)∀𝑧 ∈ (Base‘𝐶)∀𝑓 ∈ (𝑥(Hom ‘𝐶)𝑦)∀𝑔 ∈ (𝑦(Hom ‘𝐶)𝑧)((𝑔(〈𝑥, 𝑦〉(comp‘𝐶)𝑧)𝑓) ∈ (𝑥(Hom ‘𝐶)𝑧) ∧ ∀𝑤 ∈ (Base‘𝐶)∀ℎ ∈ (𝑧(Hom ‘𝐶)𝑤)((ℎ(〈𝑦, 𝑧〉(comp‘𝐶)𝑤)𝑔)(〈𝑥, 𝑦〉(comp‘𝐶)𝑤)𝑓) = (ℎ(〈𝑥, 𝑧〉(comp‘𝐶)𝑤)(𝑔(〈𝑥, 𝑦〉(comp‘𝐶)𝑧)𝑓)))) ↔ (∃𝑔 ∈ (𝑥(Hom ‘𝐶)𝑥)∀𝑦 ∈ (Base‘𝐶)(∀𝑓 ∈ (𝑦(Hom ‘𝐶)𝑥)(𝑔(〈𝑦, 𝑥〉(comp‘𝐶)𝑥)𝑓) = 𝑓 ∧ ∀𝑓 ∈ (𝑥(Hom ‘𝐶)𝑦)(𝑓(〈𝑥, 𝑥〉(comp‘𝐶)𝑦)𝑔) = 𝑓) ∧ ∀𝑦 ∈ (Base‘𝐶)∀𝑧 ∈ (Base‘𝐶)∀𝑓 ∈ (𝑥(Hom ‘𝐶)𝑦)∀𝑔 ∈ (𝑦(Hom ‘𝐶)𝑧)((𝑔(〈𝑥, 𝑦〉(comp‘𝐶)𝑧)𝑓) ∈ (𝑥(Hom ‘𝐶)𝑧) ∧ ∀𝑤 ∈ (Base‘𝐶)∀ℎ ∈ (𝑧(Hom ‘𝐶)𝑤)((ℎ(〈𝑦, 𝑧〉(comp‘𝐶)𝑤)𝑔)(〈𝑥, 𝑦〉(comp‘𝐷)𝑤)𝑓) = (ℎ(〈𝑥, 𝑧〉(comp‘𝐷)𝑤)(𝑔(〈𝑥, 𝑦〉(comp‘𝐶)𝑧)𝑓)))))) |
129 | 128 | expr 641 |
. . . . . . 7
⊢ (((𝜑 ∧ ∀𝑦 ∈ (Base‘𝐶)∀𝑧 ∈ (Base‘𝐶)∀𝑔 ∈ (𝑦(Hom ‘𝐶)𝑧)∀𝑤 ∈ (Base‘𝐶)∀ℎ ∈ (𝑧(Hom ‘𝐶)𝑤)(ℎ(〈𝑦, 𝑧〉(comp‘𝐶)𝑤)𝑔) ∈ (𝑦(Hom ‘𝐶)𝑤)) ∧ 𝑥 ∈ (Base‘𝐶)) → (∀𝑦 ∈ (Base‘𝐶)∀𝑧 ∈ (Base‘𝐶)∀𝑓 ∈ (𝑥(Hom ‘𝐶)𝑦)∀𝑔 ∈ (𝑦(Hom ‘𝐶)𝑧)(𝑔(〈𝑥, 𝑦〉(comp‘𝐶)𝑧)𝑓) ∈ (𝑥(Hom ‘𝐶)𝑧) → ((∃𝑔 ∈ (𝑥(Hom ‘𝐶)𝑥)∀𝑦 ∈ (Base‘𝐶)(∀𝑓 ∈ (𝑦(Hom ‘𝐶)𝑥)(𝑔(〈𝑦, 𝑥〉(comp‘𝐶)𝑥)𝑓) = 𝑓 ∧ ∀𝑓 ∈ (𝑥(Hom ‘𝐶)𝑦)(𝑓(〈𝑥, 𝑥〉(comp‘𝐶)𝑦)𝑔) = 𝑓) ∧ ∀𝑦 ∈ (Base‘𝐶)∀𝑧 ∈ (Base‘𝐶)∀𝑓 ∈ (𝑥(Hom ‘𝐶)𝑦)∀𝑔 ∈ (𝑦(Hom ‘𝐶)𝑧)((𝑔(〈𝑥, 𝑦〉(comp‘𝐶)𝑧)𝑓) ∈ (𝑥(Hom ‘𝐶)𝑧) ∧ ∀𝑤 ∈ (Base‘𝐶)∀ℎ ∈ (𝑧(Hom ‘𝐶)𝑤)((ℎ(〈𝑦, 𝑧〉(comp‘𝐶)𝑤)𝑔)(〈𝑥, 𝑦〉(comp‘𝐶)𝑤)𝑓) = (ℎ(〈𝑥, 𝑧〉(comp‘𝐶)𝑤)(𝑔(〈𝑥, 𝑦〉(comp‘𝐶)𝑧)𝑓)))) ↔ (∃𝑔 ∈ (𝑥(Hom ‘𝐶)𝑥)∀𝑦 ∈ (Base‘𝐶)(∀𝑓 ∈ (𝑦(Hom ‘𝐶)𝑥)(𝑔(〈𝑦, 𝑥〉(comp‘𝐶)𝑥)𝑓) = 𝑓 ∧ ∀𝑓 ∈ (𝑥(Hom ‘𝐶)𝑦)(𝑓(〈𝑥, 𝑥〉(comp‘𝐶)𝑦)𝑔) = 𝑓) ∧ ∀𝑦 ∈ (Base‘𝐶)∀𝑧 ∈ (Base‘𝐶)∀𝑓 ∈ (𝑥(Hom ‘𝐶)𝑦)∀𝑔 ∈ (𝑦(Hom ‘𝐶)𝑧)((𝑔(〈𝑥, 𝑦〉(comp‘𝐶)𝑧)𝑓) ∈ (𝑥(Hom ‘𝐶)𝑧) ∧ ∀𝑤 ∈ (Base‘𝐶)∀ℎ ∈ (𝑧(Hom ‘𝐶)𝑤)((ℎ(〈𝑦, 𝑧〉(comp‘𝐶)𝑤)𝑔)(〈𝑥, 𝑦〉(comp‘𝐷)𝑤)𝑓) = (ℎ(〈𝑥, 𝑧〉(comp‘𝐷)𝑤)(𝑔(〈𝑥, 𝑦〉(comp‘𝐶)𝑧)𝑓))))))) |
130 | 129 | ralimdva 2945 |
. . . . . 6
⊢ ((𝜑 ∧ ∀𝑦 ∈ (Base‘𝐶)∀𝑧 ∈ (Base‘𝐶)∀𝑔 ∈ (𝑦(Hom ‘𝐶)𝑧)∀𝑤 ∈ (Base‘𝐶)∀ℎ ∈ (𝑧(Hom ‘𝐶)𝑤)(ℎ(〈𝑦, 𝑧〉(comp‘𝐶)𝑤)𝑔) ∈ (𝑦(Hom ‘𝐶)𝑤)) → (∀𝑥 ∈ (Base‘𝐶)∀𝑦 ∈ (Base‘𝐶)∀𝑧 ∈ (Base‘𝐶)∀𝑓 ∈ (𝑥(Hom ‘𝐶)𝑦)∀𝑔 ∈ (𝑦(Hom ‘𝐶)𝑧)(𝑔(〈𝑥, 𝑦〉(comp‘𝐶)𝑧)𝑓) ∈ (𝑥(Hom ‘𝐶)𝑧) → ∀𝑥 ∈ (Base‘𝐶)((∃𝑔 ∈ (𝑥(Hom ‘𝐶)𝑥)∀𝑦 ∈ (Base‘𝐶)(∀𝑓 ∈ (𝑦(Hom ‘𝐶)𝑥)(𝑔(〈𝑦, 𝑥〉(comp‘𝐶)𝑥)𝑓) = 𝑓 ∧ ∀𝑓 ∈ (𝑥(Hom ‘𝐶)𝑦)(𝑓(〈𝑥, 𝑥〉(comp‘𝐶)𝑦)𝑔) = 𝑓) ∧ ∀𝑦 ∈ (Base‘𝐶)∀𝑧 ∈ (Base‘𝐶)∀𝑓 ∈ (𝑥(Hom ‘𝐶)𝑦)∀𝑔 ∈ (𝑦(Hom ‘𝐶)𝑧)((𝑔(〈𝑥, 𝑦〉(comp‘𝐶)𝑧)𝑓) ∈ (𝑥(Hom ‘𝐶)𝑧) ∧ ∀𝑤 ∈ (Base‘𝐶)∀ℎ ∈ (𝑧(Hom ‘𝐶)𝑤)((ℎ(〈𝑦, 𝑧〉(comp‘𝐶)𝑤)𝑔)(〈𝑥, 𝑦〉(comp‘𝐶)𝑤)𝑓) = (ℎ(〈𝑥, 𝑧〉(comp‘𝐶)𝑤)(𝑔(〈𝑥, 𝑦〉(comp‘𝐶)𝑧)𝑓)))) ↔ (∃𝑔 ∈ (𝑥(Hom ‘𝐶)𝑥)∀𝑦 ∈ (Base‘𝐶)(∀𝑓 ∈ (𝑦(Hom ‘𝐶)𝑥)(𝑔(〈𝑦, 𝑥〉(comp‘𝐶)𝑥)𝑓) = 𝑓 ∧ ∀𝑓 ∈ (𝑥(Hom ‘𝐶)𝑦)(𝑓(〈𝑥, 𝑥〉(comp‘𝐶)𝑦)𝑔) = 𝑓) ∧ ∀𝑦 ∈ (Base‘𝐶)∀𝑧 ∈ (Base‘𝐶)∀𝑓 ∈ (𝑥(Hom ‘𝐶)𝑦)∀𝑔 ∈ (𝑦(Hom ‘𝐶)𝑧)((𝑔(〈𝑥, 𝑦〉(comp‘𝐶)𝑧)𝑓) ∈ (𝑥(Hom ‘𝐶)𝑧) ∧ ∀𝑤 ∈ (Base‘𝐶)∀ℎ ∈ (𝑧(Hom ‘𝐶)𝑤)((ℎ(〈𝑦, 𝑧〉(comp‘𝐶)𝑤)𝑔)(〈𝑥, 𝑦〉(comp‘𝐷)𝑤)𝑓) = (ℎ(〈𝑥, 𝑧〉(comp‘𝐷)𝑤)(𝑔(〈𝑥, 𝑦〉(comp‘𝐶)𝑧)𝑓))))))) |
131 | 130 | expimpd 627 |
. . . . 5
⊢ (𝜑 → ((∀𝑦 ∈ (Base‘𝐶)∀𝑧 ∈ (Base‘𝐶)∀𝑔 ∈ (𝑦(Hom ‘𝐶)𝑧)∀𝑤 ∈ (Base‘𝐶)∀ℎ ∈ (𝑧(Hom ‘𝐶)𝑤)(ℎ(〈𝑦, 𝑧〉(comp‘𝐶)𝑤)𝑔) ∈ (𝑦(Hom ‘𝐶)𝑤) ∧ ∀𝑥 ∈ (Base‘𝐶)∀𝑦 ∈ (Base‘𝐶)∀𝑧 ∈ (Base‘𝐶)∀𝑓 ∈ (𝑥(Hom ‘𝐶)𝑦)∀𝑔 ∈ (𝑦(Hom ‘𝐶)𝑧)(𝑔(〈𝑥, 𝑦〉(comp‘𝐶)𝑧)𝑓) ∈ (𝑥(Hom ‘𝐶)𝑧)) → ∀𝑥 ∈ (Base‘𝐶)((∃𝑔 ∈ (𝑥(Hom ‘𝐶)𝑥)∀𝑦 ∈ (Base‘𝐶)(∀𝑓 ∈ (𝑦(Hom ‘𝐶)𝑥)(𝑔(〈𝑦, 𝑥〉(comp‘𝐶)𝑥)𝑓) = 𝑓 ∧ ∀𝑓 ∈ (𝑥(Hom ‘𝐶)𝑦)(𝑓(〈𝑥, 𝑥〉(comp‘𝐶)𝑦)𝑔) = 𝑓) ∧ ∀𝑦 ∈ (Base‘𝐶)∀𝑧 ∈ (Base‘𝐶)∀𝑓 ∈ (𝑥(Hom ‘𝐶)𝑦)∀𝑔 ∈ (𝑦(Hom ‘𝐶)𝑧)((𝑔(〈𝑥, 𝑦〉(comp‘𝐶)𝑧)𝑓) ∈ (𝑥(Hom ‘𝐶)𝑧) ∧ ∀𝑤 ∈ (Base‘𝐶)∀ℎ ∈ (𝑧(Hom ‘𝐶)𝑤)((ℎ(〈𝑦, 𝑧〉(comp‘𝐶)𝑤)𝑔)(〈𝑥, 𝑦〉(comp‘𝐶)𝑤)𝑓) = (ℎ(〈𝑥, 𝑧〉(comp‘𝐶)𝑤)(𝑔(〈𝑥, 𝑦〉(comp‘𝐶)𝑧)𝑓)))) ↔ (∃𝑔 ∈ (𝑥(Hom ‘𝐶)𝑥)∀𝑦 ∈ (Base‘𝐶)(∀𝑓 ∈ (𝑦(Hom ‘𝐶)𝑥)(𝑔(〈𝑦, 𝑥〉(comp‘𝐶)𝑥)𝑓) = 𝑓 ∧ ∀𝑓 ∈ (𝑥(Hom ‘𝐶)𝑦)(𝑓(〈𝑥, 𝑥〉(comp‘𝐶)𝑦)𝑔) = 𝑓) ∧ ∀𝑦 ∈ (Base‘𝐶)∀𝑧 ∈ (Base‘𝐶)∀𝑓 ∈ (𝑥(Hom ‘𝐶)𝑦)∀𝑔 ∈ (𝑦(Hom ‘𝐶)𝑧)((𝑔(〈𝑥, 𝑦〉(comp‘𝐶)𝑧)𝑓) ∈ (𝑥(Hom ‘𝐶)𝑧) ∧ ∀𝑤 ∈ (Base‘𝐶)∀ℎ ∈ (𝑧(Hom ‘𝐶)𝑤)((ℎ(〈𝑦, 𝑧〉(comp‘𝐶)𝑤)𝑔)(〈𝑥, 𝑦〉(comp‘𝐷)𝑤)𝑓) = (ℎ(〈𝑥, 𝑧〉(comp‘𝐷)𝑤)(𝑔(〈𝑥, 𝑦〉(comp‘𝐶)𝑧)𝑓))))))) |
132 | | ralbi 3050 |
. . . . 5
⊢
(∀𝑥 ∈
(Base‘𝐶)((∃𝑔 ∈ (𝑥(Hom ‘𝐶)𝑥)∀𝑦 ∈ (Base‘𝐶)(∀𝑓 ∈ (𝑦(Hom ‘𝐶)𝑥)(𝑔(〈𝑦, 𝑥〉(comp‘𝐶)𝑥)𝑓) = 𝑓 ∧ ∀𝑓 ∈ (𝑥(Hom ‘𝐶)𝑦)(𝑓(〈𝑥, 𝑥〉(comp‘𝐶)𝑦)𝑔) = 𝑓) ∧ ∀𝑦 ∈ (Base‘𝐶)∀𝑧 ∈ (Base‘𝐶)∀𝑓 ∈ (𝑥(Hom ‘𝐶)𝑦)∀𝑔 ∈ (𝑦(Hom ‘𝐶)𝑧)((𝑔(〈𝑥, 𝑦〉(comp‘𝐶)𝑧)𝑓) ∈ (𝑥(Hom ‘𝐶)𝑧) ∧ ∀𝑤 ∈ (Base‘𝐶)∀ℎ ∈ (𝑧(Hom ‘𝐶)𝑤)((ℎ(〈𝑦, 𝑧〉(comp‘𝐶)𝑤)𝑔)(〈𝑥, 𝑦〉(comp‘𝐶)𝑤)𝑓) = (ℎ(〈𝑥, 𝑧〉(comp‘𝐶)𝑤)(𝑔(〈𝑥, 𝑦〉(comp‘𝐶)𝑧)𝑓)))) ↔ (∃𝑔 ∈ (𝑥(Hom ‘𝐶)𝑥)∀𝑦 ∈ (Base‘𝐶)(∀𝑓 ∈ (𝑦(Hom ‘𝐶)𝑥)(𝑔(〈𝑦, 𝑥〉(comp‘𝐶)𝑥)𝑓) = 𝑓 ∧ ∀𝑓 ∈ (𝑥(Hom ‘𝐶)𝑦)(𝑓(〈𝑥, 𝑥〉(comp‘𝐶)𝑦)𝑔) = 𝑓) ∧ ∀𝑦 ∈ (Base‘𝐶)∀𝑧 ∈ (Base‘𝐶)∀𝑓 ∈ (𝑥(Hom ‘𝐶)𝑦)∀𝑔 ∈ (𝑦(Hom ‘𝐶)𝑧)((𝑔(〈𝑥, 𝑦〉(comp‘𝐶)𝑧)𝑓) ∈ (𝑥(Hom ‘𝐶)𝑧) ∧ ∀𝑤 ∈ (Base‘𝐶)∀ℎ ∈ (𝑧(Hom ‘𝐶)𝑤)((ℎ(〈𝑦, 𝑧〉(comp‘𝐶)𝑤)𝑔)(〈𝑥, 𝑦〉(comp‘𝐷)𝑤)𝑓) = (ℎ(〈𝑥, 𝑧〉(comp‘𝐷)𝑤)(𝑔(〈𝑥, 𝑦〉(comp‘𝐶)𝑧)𝑓))))) → (∀𝑥 ∈ (Base‘𝐶)(∃𝑔 ∈ (𝑥(Hom ‘𝐶)𝑥)∀𝑦 ∈ (Base‘𝐶)(∀𝑓 ∈ (𝑦(Hom ‘𝐶)𝑥)(𝑔(〈𝑦, 𝑥〉(comp‘𝐶)𝑥)𝑓) = 𝑓 ∧ ∀𝑓 ∈ (𝑥(Hom ‘𝐶)𝑦)(𝑓(〈𝑥, 𝑥〉(comp‘𝐶)𝑦)𝑔) = 𝑓) ∧ ∀𝑦 ∈ (Base‘𝐶)∀𝑧 ∈ (Base‘𝐶)∀𝑓 ∈ (𝑥(Hom ‘𝐶)𝑦)∀𝑔 ∈ (𝑦(Hom ‘𝐶)𝑧)((𝑔(〈𝑥, 𝑦〉(comp‘𝐶)𝑧)𝑓) ∈ (𝑥(Hom ‘𝐶)𝑧) ∧ ∀𝑤 ∈ (Base‘𝐶)∀ℎ ∈ (𝑧(Hom ‘𝐶)𝑤)((ℎ(〈𝑦, 𝑧〉(comp‘𝐶)𝑤)𝑔)(〈𝑥, 𝑦〉(comp‘𝐶)𝑤)𝑓) = (ℎ(〈𝑥, 𝑧〉(comp‘𝐶)𝑤)(𝑔(〈𝑥, 𝑦〉(comp‘𝐶)𝑧)𝑓)))) ↔ ∀𝑥 ∈ (Base‘𝐶)(∃𝑔 ∈ (𝑥(Hom ‘𝐶)𝑥)∀𝑦 ∈ (Base‘𝐶)(∀𝑓 ∈ (𝑦(Hom ‘𝐶)𝑥)(𝑔(〈𝑦, 𝑥〉(comp‘𝐶)𝑥)𝑓) = 𝑓 ∧ ∀𝑓 ∈ (𝑥(Hom ‘𝐶)𝑦)(𝑓(〈𝑥, 𝑥〉(comp‘𝐶)𝑦)𝑔) = 𝑓) ∧ ∀𝑦 ∈ (Base‘𝐶)∀𝑧 ∈ (Base‘𝐶)∀𝑓 ∈ (𝑥(Hom ‘𝐶)𝑦)∀𝑔 ∈ (𝑦(Hom ‘𝐶)𝑧)((𝑔(〈𝑥, 𝑦〉(comp‘𝐶)𝑧)𝑓) ∈ (𝑥(Hom ‘𝐶)𝑧) ∧ ∀𝑤 ∈ (Base‘𝐶)∀ℎ ∈ (𝑧(Hom ‘𝐶)𝑤)((ℎ(〈𝑦, 𝑧〉(comp‘𝐶)𝑤)𝑔)(〈𝑥, 𝑦〉(comp‘𝐷)𝑤)𝑓) = (ℎ(〈𝑥, 𝑧〉(comp‘𝐷)𝑤)(𝑔(〈𝑥, 𝑦〉(comp‘𝐶)𝑧)𝑓)))))) |
133 | 66, 131, 132 | syl56 35 |
. . . 4
⊢ (𝜑 → (∀𝑥 ∈ (Base‘𝐶)∀𝑦 ∈ (Base‘𝐶)∀𝑧 ∈ (Base‘𝐶)∀𝑓 ∈ (𝑥(Hom ‘𝐶)𝑦)∀𝑔 ∈ (𝑦(Hom ‘𝐶)𝑧)(𝑔(〈𝑥, 𝑦〉(comp‘𝐶)𝑧)𝑓) ∈ (𝑥(Hom ‘𝐶)𝑧) → (∀𝑥 ∈ (Base‘𝐶)(∃𝑔 ∈ (𝑥(Hom ‘𝐶)𝑥)∀𝑦 ∈ (Base‘𝐶)(∀𝑓 ∈ (𝑦(Hom ‘𝐶)𝑥)(𝑔(〈𝑦, 𝑥〉(comp‘𝐶)𝑥)𝑓) = 𝑓 ∧ ∀𝑓 ∈ (𝑥(Hom ‘𝐶)𝑦)(𝑓(〈𝑥, 𝑥〉(comp‘𝐶)𝑦)𝑔) = 𝑓) ∧ ∀𝑦 ∈ (Base‘𝐶)∀𝑧 ∈ (Base‘𝐶)∀𝑓 ∈ (𝑥(Hom ‘𝐶)𝑦)∀𝑔 ∈ (𝑦(Hom ‘𝐶)𝑧)((𝑔(〈𝑥, 𝑦〉(comp‘𝐶)𝑧)𝑓) ∈ (𝑥(Hom ‘𝐶)𝑧) ∧ ∀𝑤 ∈ (Base‘𝐶)∀ℎ ∈ (𝑧(Hom ‘𝐶)𝑤)((ℎ(〈𝑦, 𝑧〉(comp‘𝐶)𝑤)𝑔)(〈𝑥, 𝑦〉(comp‘𝐶)𝑤)𝑓) = (ℎ(〈𝑥, 𝑧〉(comp‘𝐶)𝑤)(𝑔(〈𝑥, 𝑦〉(comp‘𝐶)𝑧)𝑓)))) ↔ ∀𝑥 ∈ (Base‘𝐶)(∃𝑔 ∈ (𝑥(Hom ‘𝐶)𝑥)∀𝑦 ∈ (Base‘𝐶)(∀𝑓 ∈ (𝑦(Hom ‘𝐶)𝑥)(𝑔(〈𝑦, 𝑥〉(comp‘𝐶)𝑥)𝑓) = 𝑓 ∧ ∀𝑓 ∈ (𝑥(Hom ‘𝐶)𝑦)(𝑓(〈𝑥, 𝑥〉(comp‘𝐶)𝑦)𝑔) = 𝑓) ∧ ∀𝑦 ∈ (Base‘𝐶)∀𝑧 ∈ (Base‘𝐶)∀𝑓 ∈ (𝑥(Hom ‘𝐶)𝑦)∀𝑔 ∈ (𝑦(Hom ‘𝐶)𝑧)((𝑔(〈𝑥, 𝑦〉(comp‘𝐶)𝑧)𝑓) ∈ (𝑥(Hom ‘𝐶)𝑧) ∧ ∀𝑤 ∈ (Base‘𝐶)∀ℎ ∈ (𝑧(Hom ‘𝐶)𝑤)((ℎ(〈𝑦, 𝑧〉(comp‘𝐶)𝑤)𝑔)(〈𝑥, 𝑦〉(comp‘𝐷)𝑤)𝑓) = (ℎ(〈𝑥, 𝑧〉(comp‘𝐷)𝑤)(𝑔(〈𝑥, 𝑦〉(comp‘𝐶)𝑧)𝑓))))))) |
134 | 8, 16, 133 | pm5.21ndd 368 |
. . 3
⊢ (𝜑 → (∀𝑥 ∈ (Base‘𝐶)(∃𝑔 ∈ (𝑥(Hom ‘𝐶)𝑥)∀𝑦 ∈ (Base‘𝐶)(∀𝑓 ∈ (𝑦(Hom ‘𝐶)𝑥)(𝑔(〈𝑦, 𝑥〉(comp‘𝐶)𝑥)𝑓) = 𝑓 ∧ ∀𝑓 ∈ (𝑥(Hom ‘𝐶)𝑦)(𝑓(〈𝑥, 𝑥〉(comp‘𝐶)𝑦)𝑔) = 𝑓) ∧ ∀𝑦 ∈ (Base‘𝐶)∀𝑧 ∈ (Base‘𝐶)∀𝑓 ∈ (𝑥(Hom ‘𝐶)𝑦)∀𝑔 ∈ (𝑦(Hom ‘𝐶)𝑧)((𝑔(〈𝑥, 𝑦〉(comp‘𝐶)𝑧)𝑓) ∈ (𝑥(Hom ‘𝐶)𝑧) ∧ ∀𝑤 ∈ (Base‘𝐶)∀ℎ ∈ (𝑧(Hom ‘𝐶)𝑤)((ℎ(〈𝑦, 𝑧〉(comp‘𝐶)𝑤)𝑔)(〈𝑥, 𝑦〉(comp‘𝐶)𝑤)𝑓) = (ℎ(〈𝑥, 𝑧〉(comp‘𝐶)𝑤)(𝑔(〈𝑥, 𝑦〉(comp‘𝐶)𝑧)𝑓)))) ↔ ∀𝑥 ∈ (Base‘𝐶)(∃𝑔 ∈ (𝑥(Hom ‘𝐶)𝑥)∀𝑦 ∈ (Base‘𝐶)(∀𝑓 ∈ (𝑦(Hom ‘𝐶)𝑥)(𝑔(〈𝑦, 𝑥〉(comp‘𝐶)𝑥)𝑓) = 𝑓 ∧ ∀𝑓 ∈ (𝑥(Hom ‘𝐶)𝑦)(𝑓(〈𝑥, 𝑥〉(comp‘𝐶)𝑦)𝑔) = 𝑓) ∧ ∀𝑦 ∈ (Base‘𝐶)∀𝑧 ∈ (Base‘𝐶)∀𝑓 ∈ (𝑥(Hom ‘𝐶)𝑦)∀𝑔 ∈ (𝑦(Hom ‘𝐶)𝑧)((𝑔(〈𝑥, 𝑦〉(comp‘𝐶)𝑧)𝑓) ∈ (𝑥(Hom ‘𝐶)𝑧) ∧ ∀𝑤 ∈ (Base‘𝐶)∀ℎ ∈ (𝑧(Hom ‘𝐶)𝑤)((ℎ(〈𝑦, 𝑧〉(comp‘𝐶)𝑤)𝑔)(〈𝑥, 𝑦〉(comp‘𝐷)𝑤)𝑓) = (ℎ(〈𝑥, 𝑧〉(comp‘𝐷)𝑤)(𝑔(〈𝑥, 𝑦〉(comp‘𝐶)𝑧)𝑓)))))) |
135 | 74 | homfeqbas 16179 |
. . . 4
⊢ (𝜑 → (Base‘𝐶) = (Base‘𝐷)) |
136 | | eqid 2610 |
. . . . . . 7
⊢ (Hom
‘𝐷) = (Hom
‘𝐷) |
137 | | simpr 476 |
. . . . . . 7
⊢ ((𝜑 ∧ 𝑥 ∈ (Base‘𝐶)) → 𝑥 ∈ (Base‘𝐶)) |
138 | 70, 71, 136, 75, 137, 137 | homfeqval 16180 |
. . . . . 6
⊢ ((𝜑 ∧ 𝑥 ∈ (Base‘𝐶)) → (𝑥(Hom ‘𝐶)𝑥) = (𝑥(Hom ‘𝐷)𝑥)) |
139 | 135 | ad2antrr 758 |
. . . . . . 7
⊢ (((𝜑 ∧ 𝑥 ∈ (Base‘𝐶)) ∧ 𝑔 ∈ (𝑥(Hom ‘𝐶)𝑥)) → (Base‘𝐶) = (Base‘𝐷)) |
140 | 75 | ad2antrr 758 |
. . . . . . . . . 10
⊢ ((((𝜑 ∧ 𝑥 ∈ (Base‘𝐶)) ∧ 𝑔 ∈ (𝑥(Hom ‘𝐶)𝑥)) ∧ 𝑦 ∈ (Base‘𝐶)) → (Homf
‘𝐶) =
(Homf ‘𝐷)) |
141 | | simpr 476 |
. . . . . . . . . 10
⊢ ((((𝜑 ∧ 𝑥 ∈ (Base‘𝐶)) ∧ 𝑔 ∈ (𝑥(Hom ‘𝐶)𝑥)) ∧ 𝑦 ∈ (Base‘𝐶)) → 𝑦 ∈ (Base‘𝐶)) |
142 | | simpllr 795 |
. . . . . . . . . 10
⊢ ((((𝜑 ∧ 𝑥 ∈ (Base‘𝐶)) ∧ 𝑔 ∈ (𝑥(Hom ‘𝐶)𝑥)) ∧ 𝑦 ∈ (Base‘𝐶)) → 𝑥 ∈ (Base‘𝐶)) |
143 | 70, 71, 136, 140, 141, 142 | homfeqval 16180 |
. . . . . . . . 9
⊢ ((((𝜑 ∧ 𝑥 ∈ (Base‘𝐶)) ∧ 𝑔 ∈ (𝑥(Hom ‘𝐶)𝑥)) ∧ 𝑦 ∈ (Base‘𝐶)) → (𝑦(Hom ‘𝐶)𝑥) = (𝑦(Hom ‘𝐷)𝑥)) |
144 | 74 | ad4antr 764 |
. . . . . . . . . . 11
⊢
(((((𝜑 ∧ 𝑥 ∈ (Base‘𝐶)) ∧ 𝑔 ∈ (𝑥(Hom ‘𝐶)𝑥)) ∧ 𝑦 ∈ (Base‘𝐶)) ∧ 𝑓 ∈ (𝑦(Hom ‘𝐶)𝑥)) → (Homf
‘𝐶) =
(Homf ‘𝐷)) |
145 | 78 | ad4antr 764 |
. . . . . . . . . . 11
⊢
(((((𝜑 ∧ 𝑥 ∈ (Base‘𝐶)) ∧ 𝑔 ∈ (𝑥(Hom ‘𝐶)𝑥)) ∧ 𝑦 ∈ (Base‘𝐶)) ∧ 𝑓 ∈ (𝑦(Hom ‘𝐶)𝑥)) →
(compf‘𝐶) = (compf‘𝐷)) |
146 | | simplr 788 |
. . . . . . . . . . 11
⊢
(((((𝜑 ∧ 𝑥 ∈ (Base‘𝐶)) ∧ 𝑔 ∈ (𝑥(Hom ‘𝐶)𝑥)) ∧ 𝑦 ∈ (Base‘𝐶)) ∧ 𝑓 ∈ (𝑦(Hom ‘𝐶)𝑥)) → 𝑦 ∈ (Base‘𝐶)) |
147 | | simp-4r 803 |
. . . . . . . . . . 11
⊢
(((((𝜑 ∧ 𝑥 ∈ (Base‘𝐶)) ∧ 𝑔 ∈ (𝑥(Hom ‘𝐶)𝑥)) ∧ 𝑦 ∈ (Base‘𝐶)) ∧ 𝑓 ∈ (𝑦(Hom ‘𝐶)𝑥)) → 𝑥 ∈ (Base‘𝐶)) |
148 | | simpr 476 |
. . . . . . . . . . 11
⊢
(((((𝜑 ∧ 𝑥 ∈ (Base‘𝐶)) ∧ 𝑔 ∈ (𝑥(Hom ‘𝐶)𝑥)) ∧ 𝑦 ∈ (Base‘𝐶)) ∧ 𝑓 ∈ (𝑦(Hom ‘𝐶)𝑥)) → 𝑓 ∈ (𝑦(Hom ‘𝐶)𝑥)) |
149 | | simpllr 795 |
. . . . . . . . . . 11
⊢
(((((𝜑 ∧ 𝑥 ∈ (Base‘𝐶)) ∧ 𝑔 ∈ (𝑥(Hom ‘𝐶)𝑥)) ∧ 𝑦 ∈ (Base‘𝐶)) ∧ 𝑓 ∈ (𝑦(Hom ‘𝐶)𝑥)) → 𝑔 ∈ (𝑥(Hom ‘𝐶)𝑥)) |
150 | 70, 71, 72, 73, 144, 145, 146, 147, 147, 148, 149 | comfeqval 16191 |
. . . . . . . . . 10
⊢
(((((𝜑 ∧ 𝑥 ∈ (Base‘𝐶)) ∧ 𝑔 ∈ (𝑥(Hom ‘𝐶)𝑥)) ∧ 𝑦 ∈ (Base‘𝐶)) ∧ 𝑓 ∈ (𝑦(Hom ‘𝐶)𝑥)) → (𝑔(〈𝑦, 𝑥〉(comp‘𝐶)𝑥)𝑓) = (𝑔(〈𝑦, 𝑥〉(comp‘𝐷)𝑥)𝑓)) |
151 | 150 | eqeq1d 2612 |
. . . . . . . . 9
⊢
(((((𝜑 ∧ 𝑥 ∈ (Base‘𝐶)) ∧ 𝑔 ∈ (𝑥(Hom ‘𝐶)𝑥)) ∧ 𝑦 ∈ (Base‘𝐶)) ∧ 𝑓 ∈ (𝑦(Hom ‘𝐶)𝑥)) → ((𝑔(〈𝑦, 𝑥〉(comp‘𝐶)𝑥)𝑓) = 𝑓 ↔ (𝑔(〈𝑦, 𝑥〉(comp‘𝐷)𝑥)𝑓) = 𝑓)) |
152 | 143, 151 | raleqbidva 3131 |
. . . . . . . 8
⊢ ((((𝜑 ∧ 𝑥 ∈ (Base‘𝐶)) ∧ 𝑔 ∈ (𝑥(Hom ‘𝐶)𝑥)) ∧ 𝑦 ∈ (Base‘𝐶)) → (∀𝑓 ∈ (𝑦(Hom ‘𝐶)𝑥)(𝑔(〈𝑦, 𝑥〉(comp‘𝐶)𝑥)𝑓) = 𝑓 ↔ ∀𝑓 ∈ (𝑦(Hom ‘𝐷)𝑥)(𝑔(〈𝑦, 𝑥〉(comp‘𝐷)𝑥)𝑓) = 𝑓)) |
153 | 70, 71, 136, 140, 142, 141 | homfeqval 16180 |
. . . . . . . . 9
⊢ ((((𝜑 ∧ 𝑥 ∈ (Base‘𝐶)) ∧ 𝑔 ∈ (𝑥(Hom ‘𝐶)𝑥)) ∧ 𝑦 ∈ (Base‘𝐶)) → (𝑥(Hom ‘𝐶)𝑦) = (𝑥(Hom ‘𝐷)𝑦)) |
154 | 74 | ad4antr 764 |
. . . . . . . . . . 11
⊢
(((((𝜑 ∧ 𝑥 ∈ (Base‘𝐶)) ∧ 𝑔 ∈ (𝑥(Hom ‘𝐶)𝑥)) ∧ 𝑦 ∈ (Base‘𝐶)) ∧ 𝑓 ∈ (𝑥(Hom ‘𝐶)𝑦)) → (Homf
‘𝐶) =
(Homf ‘𝐷)) |
155 | 78 | ad4antr 764 |
. . . . . . . . . . 11
⊢
(((((𝜑 ∧ 𝑥 ∈ (Base‘𝐶)) ∧ 𝑔 ∈ (𝑥(Hom ‘𝐶)𝑥)) ∧ 𝑦 ∈ (Base‘𝐶)) ∧ 𝑓 ∈ (𝑥(Hom ‘𝐶)𝑦)) →
(compf‘𝐶) = (compf‘𝐷)) |
156 | | simp-4r 803 |
. . . . . . . . . . 11
⊢
(((((𝜑 ∧ 𝑥 ∈ (Base‘𝐶)) ∧ 𝑔 ∈ (𝑥(Hom ‘𝐶)𝑥)) ∧ 𝑦 ∈ (Base‘𝐶)) ∧ 𝑓 ∈ (𝑥(Hom ‘𝐶)𝑦)) → 𝑥 ∈ (Base‘𝐶)) |
157 | | simplr 788 |
. . . . . . . . . . 11
⊢
(((((𝜑 ∧ 𝑥 ∈ (Base‘𝐶)) ∧ 𝑔 ∈ (𝑥(Hom ‘𝐶)𝑥)) ∧ 𝑦 ∈ (Base‘𝐶)) ∧ 𝑓 ∈ (𝑥(Hom ‘𝐶)𝑦)) → 𝑦 ∈ (Base‘𝐶)) |
158 | | simpllr 795 |
. . . . . . . . . . 11
⊢
(((((𝜑 ∧ 𝑥 ∈ (Base‘𝐶)) ∧ 𝑔 ∈ (𝑥(Hom ‘𝐶)𝑥)) ∧ 𝑦 ∈ (Base‘𝐶)) ∧ 𝑓 ∈ (𝑥(Hom ‘𝐶)𝑦)) → 𝑔 ∈ (𝑥(Hom ‘𝐶)𝑥)) |
159 | | simpr 476 |
. . . . . . . . . . 11
⊢
(((((𝜑 ∧ 𝑥 ∈ (Base‘𝐶)) ∧ 𝑔 ∈ (𝑥(Hom ‘𝐶)𝑥)) ∧ 𝑦 ∈ (Base‘𝐶)) ∧ 𝑓 ∈ (𝑥(Hom ‘𝐶)𝑦)) → 𝑓 ∈ (𝑥(Hom ‘𝐶)𝑦)) |
160 | 70, 71, 72, 73, 154, 155, 156, 156, 157, 158, 159 | comfeqval 16191 |
. . . . . . . . . 10
⊢
(((((𝜑 ∧ 𝑥 ∈ (Base‘𝐶)) ∧ 𝑔 ∈ (𝑥(Hom ‘𝐶)𝑥)) ∧ 𝑦 ∈ (Base‘𝐶)) ∧ 𝑓 ∈ (𝑥(Hom ‘𝐶)𝑦)) → (𝑓(〈𝑥, 𝑥〉(comp‘𝐶)𝑦)𝑔) = (𝑓(〈𝑥, 𝑥〉(comp‘𝐷)𝑦)𝑔)) |
161 | 160 | eqeq1d 2612 |
. . . . . . . . 9
⊢
(((((𝜑 ∧ 𝑥 ∈ (Base‘𝐶)) ∧ 𝑔 ∈ (𝑥(Hom ‘𝐶)𝑥)) ∧ 𝑦 ∈ (Base‘𝐶)) ∧ 𝑓 ∈ (𝑥(Hom ‘𝐶)𝑦)) → ((𝑓(〈𝑥, 𝑥〉(comp‘𝐶)𝑦)𝑔) = 𝑓 ↔ (𝑓(〈𝑥, 𝑥〉(comp‘𝐷)𝑦)𝑔) = 𝑓)) |
162 | 153, 161 | raleqbidva 3131 |
. . . . . . . 8
⊢ ((((𝜑 ∧ 𝑥 ∈ (Base‘𝐶)) ∧ 𝑔 ∈ (𝑥(Hom ‘𝐶)𝑥)) ∧ 𝑦 ∈ (Base‘𝐶)) → (∀𝑓 ∈ (𝑥(Hom ‘𝐶)𝑦)(𝑓(〈𝑥, 𝑥〉(comp‘𝐶)𝑦)𝑔) = 𝑓 ↔ ∀𝑓 ∈ (𝑥(Hom ‘𝐷)𝑦)(𝑓(〈𝑥, 𝑥〉(comp‘𝐷)𝑦)𝑔) = 𝑓)) |
163 | 152, 162 | anbi12d 743 |
. . . . . . 7
⊢ ((((𝜑 ∧ 𝑥 ∈ (Base‘𝐶)) ∧ 𝑔 ∈ (𝑥(Hom ‘𝐶)𝑥)) ∧ 𝑦 ∈ (Base‘𝐶)) → ((∀𝑓 ∈ (𝑦(Hom ‘𝐶)𝑥)(𝑔(〈𝑦, 𝑥〉(comp‘𝐶)𝑥)𝑓) = 𝑓 ∧ ∀𝑓 ∈ (𝑥(Hom ‘𝐶)𝑦)(𝑓(〈𝑥, 𝑥〉(comp‘𝐶)𝑦)𝑔) = 𝑓) ↔ (∀𝑓 ∈ (𝑦(Hom ‘𝐷)𝑥)(𝑔(〈𝑦, 𝑥〉(comp‘𝐷)𝑥)𝑓) = 𝑓 ∧ ∀𝑓 ∈ (𝑥(Hom ‘𝐷)𝑦)(𝑓(〈𝑥, 𝑥〉(comp‘𝐷)𝑦)𝑔) = 𝑓))) |
164 | 139, 163 | raleqbidva 3131 |
. . . . . 6
⊢ (((𝜑 ∧ 𝑥 ∈ (Base‘𝐶)) ∧ 𝑔 ∈ (𝑥(Hom ‘𝐶)𝑥)) → (∀𝑦 ∈ (Base‘𝐶)(∀𝑓 ∈ (𝑦(Hom ‘𝐶)𝑥)(𝑔(〈𝑦, 𝑥〉(comp‘𝐶)𝑥)𝑓) = 𝑓 ∧ ∀𝑓 ∈ (𝑥(Hom ‘𝐶)𝑦)(𝑓(〈𝑥, 𝑥〉(comp‘𝐶)𝑦)𝑔) = 𝑓) ↔ ∀𝑦 ∈ (Base‘𝐷)(∀𝑓 ∈ (𝑦(Hom ‘𝐷)𝑥)(𝑔(〈𝑦, 𝑥〉(comp‘𝐷)𝑥)𝑓) = 𝑓 ∧ ∀𝑓 ∈ (𝑥(Hom ‘𝐷)𝑦)(𝑓(〈𝑥, 𝑥〉(comp‘𝐷)𝑦)𝑔) = 𝑓))) |
165 | 138, 164 | rexeqbidva 3132 |
. . . . 5
⊢ ((𝜑 ∧ 𝑥 ∈ (Base‘𝐶)) → (∃𝑔 ∈ (𝑥(Hom ‘𝐶)𝑥)∀𝑦 ∈ (Base‘𝐶)(∀𝑓 ∈ (𝑦(Hom ‘𝐶)𝑥)(𝑔(〈𝑦, 𝑥〉(comp‘𝐶)𝑥)𝑓) = 𝑓 ∧ ∀𝑓 ∈ (𝑥(Hom ‘𝐶)𝑦)(𝑓(〈𝑥, 𝑥〉(comp‘𝐶)𝑦)𝑔) = 𝑓) ↔ ∃𝑔 ∈ (𝑥(Hom ‘𝐷)𝑥)∀𝑦 ∈ (Base‘𝐷)(∀𝑓 ∈ (𝑦(Hom ‘𝐷)𝑥)(𝑔(〈𝑦, 𝑥〉(comp‘𝐷)𝑥)𝑓) = 𝑓 ∧ ∀𝑓 ∈ (𝑥(Hom ‘𝐷)𝑦)(𝑓(〈𝑥, 𝑥〉(comp‘𝐷)𝑦)𝑔) = 𝑓))) |
166 | 135 | adantr 480 |
. . . . . 6
⊢ ((𝜑 ∧ 𝑥 ∈ (Base‘𝐶)) → (Base‘𝐶) = (Base‘𝐷)) |
167 | 166 | adantr 480 |
. . . . . . 7
⊢ (((𝜑 ∧ 𝑥 ∈ (Base‘𝐶)) ∧ 𝑦 ∈ (Base‘𝐶)) → (Base‘𝐶) = (Base‘𝐷)) |
168 | 75 | ad2antrr 758 |
. . . . . . . . 9
⊢ ((((𝜑 ∧ 𝑥 ∈ (Base‘𝐶)) ∧ 𝑦 ∈ (Base‘𝐶)) ∧ 𝑧 ∈ (Base‘𝐶)) → (Homf
‘𝐶) =
(Homf ‘𝐷)) |
169 | | simplr 788 |
. . . . . . . . 9
⊢ ((((𝜑 ∧ 𝑥 ∈ (Base‘𝐶)) ∧ 𝑦 ∈ (Base‘𝐶)) ∧ 𝑧 ∈ (Base‘𝐶)) → 𝑦 ∈ (Base‘𝐶)) |
170 | 70, 71, 136, 168, 81, 169 | homfeqval 16180 |
. . . . . . . 8
⊢ ((((𝜑 ∧ 𝑥 ∈ (Base‘𝐶)) ∧ 𝑦 ∈ (Base‘𝐶)) ∧ 𝑧 ∈ (Base‘𝐶)) → (𝑥(Hom ‘𝐶)𝑦) = (𝑥(Hom ‘𝐷)𝑦)) |
171 | | simpr 476 |
. . . . . . . . . . 11
⊢ ((((𝜑 ∧ 𝑥 ∈ (Base‘𝐶)) ∧ 𝑦 ∈ (Base‘𝐶)) ∧ 𝑧 ∈ (Base‘𝐶)) → 𝑧 ∈ (Base‘𝐶)) |
172 | 70, 71, 136, 168, 169, 171 | homfeqval 16180 |
. . . . . . . . . 10
⊢ ((((𝜑 ∧ 𝑥 ∈ (Base‘𝐶)) ∧ 𝑦 ∈ (Base‘𝐶)) ∧ 𝑧 ∈ (Base‘𝐶)) → (𝑦(Hom ‘𝐶)𝑧) = (𝑦(Hom ‘𝐷)𝑧)) |
173 | 172 | adantr 480 |
. . . . . . . . 9
⊢
(((((𝜑 ∧ 𝑥 ∈ (Base‘𝐶)) ∧ 𝑦 ∈ (Base‘𝐶)) ∧ 𝑧 ∈ (Base‘𝐶)) ∧ 𝑓 ∈ (𝑥(Hom ‘𝐶)𝑦)) → (𝑦(Hom ‘𝐶)𝑧) = (𝑦(Hom ‘𝐷)𝑧)) |
174 | | simpr 476 |
. . . . . . . . . . . 12
⊢
((((((𝜑 ∧ 𝑥 ∈ (Base‘𝐶)) ∧ 𝑦 ∈ (Base‘𝐶)) ∧ 𝑧 ∈ (Base‘𝐶)) ∧ 𝑓 ∈ (𝑥(Hom ‘𝐶)𝑦)) ∧ 𝑔 ∈ (𝑦(Hom ‘𝐶)𝑧)) → 𝑔 ∈ (𝑦(Hom ‘𝐶)𝑧)) |
175 | 70, 71, 72, 73, 76, 79, 82, 84, 91, 87, 174 | comfeqval 16191 |
. . . . . . . . . . 11
⊢
((((((𝜑 ∧ 𝑥 ∈ (Base‘𝐶)) ∧ 𝑦 ∈ (Base‘𝐶)) ∧ 𝑧 ∈ (Base‘𝐶)) ∧ 𝑓 ∈ (𝑥(Hom ‘𝐶)𝑦)) ∧ 𝑔 ∈ (𝑦(Hom ‘𝐶)𝑧)) → (𝑔(〈𝑥, 𝑦〉(comp‘𝐶)𝑧)𝑓) = (𝑔(〈𝑥, 𝑦〉(comp‘𝐷)𝑧)𝑓)) |
176 | 70, 71, 136, 168, 81, 171 | homfeqval 16180 |
. . . . . . . . . . . 12
⊢ ((((𝜑 ∧ 𝑥 ∈ (Base‘𝐶)) ∧ 𝑦 ∈ (Base‘𝐶)) ∧ 𝑧 ∈ (Base‘𝐶)) → (𝑥(Hom ‘𝐶)𝑧) = (𝑥(Hom ‘𝐷)𝑧)) |
177 | 176 | ad2antrr 758 |
. . . . . . . . . . 11
⊢
((((((𝜑 ∧ 𝑥 ∈ (Base‘𝐶)) ∧ 𝑦 ∈ (Base‘𝐶)) ∧ 𝑧 ∈ (Base‘𝐶)) ∧ 𝑓 ∈ (𝑥(Hom ‘𝐶)𝑦)) ∧ 𝑔 ∈ (𝑦(Hom ‘𝐶)𝑧)) → (𝑥(Hom ‘𝐶)𝑧) = (𝑥(Hom ‘𝐷)𝑧)) |
178 | 175, 177 | eleq12d 2682 |
. . . . . . . . . 10
⊢
((((((𝜑 ∧ 𝑥 ∈ (Base‘𝐶)) ∧ 𝑦 ∈ (Base‘𝐶)) ∧ 𝑧 ∈ (Base‘𝐶)) ∧ 𝑓 ∈ (𝑥(Hom ‘𝐶)𝑦)) ∧ 𝑔 ∈ (𝑦(Hom ‘𝐶)𝑧)) → ((𝑔(〈𝑥, 𝑦〉(comp‘𝐶)𝑧)𝑓) ∈ (𝑥(Hom ‘𝐶)𝑧) ↔ (𝑔(〈𝑥, 𝑦〉(comp‘𝐷)𝑧)𝑓) ∈ (𝑥(Hom ‘𝐷)𝑧))) |
179 | 166 | ad4antr 764 |
. . . . . . . . . . 11
⊢
((((((𝜑 ∧ 𝑥 ∈ (Base‘𝐶)) ∧ 𝑦 ∈ (Base‘𝐶)) ∧ 𝑧 ∈ (Base‘𝐶)) ∧ 𝑓 ∈ (𝑥(Hom ‘𝐶)𝑦)) ∧ 𝑔 ∈ (𝑦(Hom ‘𝐶)𝑧)) → (Base‘𝐶) = (Base‘𝐷)) |
180 | 76 | adantr 480 |
. . . . . . . . . . . . 13
⊢
(((((((𝜑 ∧ 𝑥 ∈ (Base‘𝐶)) ∧ 𝑦 ∈ (Base‘𝐶)) ∧ 𝑧 ∈ (Base‘𝐶)) ∧ 𝑓 ∈ (𝑥(Hom ‘𝐶)𝑦)) ∧ 𝑔 ∈ (𝑦(Hom ‘𝐶)𝑧)) ∧ 𝑤 ∈ (Base‘𝐶)) → (Homf
‘𝐶) =
(Homf ‘𝐷)) |
181 | | simp-4r 803 |
. . . . . . . . . . . . 13
⊢
(((((((𝜑 ∧ 𝑥 ∈ (Base‘𝐶)) ∧ 𝑦 ∈ (Base‘𝐶)) ∧ 𝑧 ∈ (Base‘𝐶)) ∧ 𝑓 ∈ (𝑥(Hom ‘𝐶)𝑦)) ∧ 𝑔 ∈ (𝑦(Hom ‘𝐶)𝑧)) ∧ 𝑤 ∈ (Base‘𝐶)) → 𝑧 ∈ (Base‘𝐶)) |
182 | | simpr 476 |
. . . . . . . . . . . . 13
⊢
(((((((𝜑 ∧ 𝑥 ∈ (Base‘𝐶)) ∧ 𝑦 ∈ (Base‘𝐶)) ∧ 𝑧 ∈ (Base‘𝐶)) ∧ 𝑓 ∈ (𝑥(Hom ‘𝐶)𝑦)) ∧ 𝑔 ∈ (𝑦(Hom ‘𝐶)𝑧)) ∧ 𝑤 ∈ (Base‘𝐶)) → 𝑤 ∈ (Base‘𝐶)) |
183 | 70, 71, 136, 180, 181, 182 | homfeqval 16180 |
. . . . . . . . . . . 12
⊢
(((((((𝜑 ∧ 𝑥 ∈ (Base‘𝐶)) ∧ 𝑦 ∈ (Base‘𝐶)) ∧ 𝑧 ∈ (Base‘𝐶)) ∧ 𝑓 ∈ (𝑥(Hom ‘𝐶)𝑦)) ∧ 𝑔 ∈ (𝑦(Hom ‘𝐶)𝑧)) ∧ 𝑤 ∈ (Base‘𝐶)) → (𝑧(Hom ‘𝐶)𝑤) = (𝑧(Hom ‘𝐷)𝑤)) |
184 | 168 | ad4antr 764 |
. . . . . . . . . . . . . . 15
⊢
((((((((𝜑 ∧ 𝑥 ∈ (Base‘𝐶)) ∧ 𝑦 ∈ (Base‘𝐶)) ∧ 𝑧 ∈ (Base‘𝐶)) ∧ 𝑓 ∈ (𝑥(Hom ‘𝐶)𝑦)) ∧ 𝑔 ∈ (𝑦(Hom ‘𝐶)𝑧)) ∧ 𝑤 ∈ (Base‘𝐶)) ∧ ℎ ∈ (𝑧(Hom ‘𝐶)𝑤)) → (Homf
‘𝐶) =
(Homf ‘𝐷)) |
185 | 78 | ad7antr 770 |
. . . . . . . . . . . . . . 15
⊢
((((((((𝜑 ∧ 𝑥 ∈ (Base‘𝐶)) ∧ 𝑦 ∈ (Base‘𝐶)) ∧ 𝑧 ∈ (Base‘𝐶)) ∧ 𝑓 ∈ (𝑥(Hom ‘𝐶)𝑦)) ∧ 𝑔 ∈ (𝑦(Hom ‘𝐶)𝑧)) ∧ 𝑤 ∈ (Base‘𝐶)) ∧ ℎ ∈ (𝑧(Hom ‘𝐶)𝑤)) →
(compf‘𝐶) = (compf‘𝐷)) |
186 | 169 | ad4antr 764 |
. . . . . . . . . . . . . . 15
⊢
((((((((𝜑 ∧ 𝑥 ∈ (Base‘𝐶)) ∧ 𝑦 ∈ (Base‘𝐶)) ∧ 𝑧 ∈ (Base‘𝐶)) ∧ 𝑓 ∈ (𝑥(Hom ‘𝐶)𝑦)) ∧ 𝑔 ∈ (𝑦(Hom ‘𝐶)𝑧)) ∧ 𝑤 ∈ (Base‘𝐶)) ∧ ℎ ∈ (𝑧(Hom ‘𝐶)𝑤)) → 𝑦 ∈ (Base‘𝐶)) |
187 | 171 | ad4antr 764 |
. . . . . . . . . . . . . . 15
⊢
((((((((𝜑 ∧ 𝑥 ∈ (Base‘𝐶)) ∧ 𝑦 ∈ (Base‘𝐶)) ∧ 𝑧 ∈ (Base‘𝐶)) ∧ 𝑓 ∈ (𝑥(Hom ‘𝐶)𝑦)) ∧ 𝑔 ∈ (𝑦(Hom ‘𝐶)𝑧)) ∧ 𝑤 ∈ (Base‘𝐶)) ∧ ℎ ∈ (𝑧(Hom ‘𝐶)𝑤)) → 𝑧 ∈ (Base‘𝐶)) |
188 | | simplr 788 |
. . . . . . . . . . . . . . 15
⊢
((((((((𝜑 ∧ 𝑥 ∈ (Base‘𝐶)) ∧ 𝑦 ∈ (Base‘𝐶)) ∧ 𝑧 ∈ (Base‘𝐶)) ∧ 𝑓 ∈ (𝑥(Hom ‘𝐶)𝑦)) ∧ 𝑔 ∈ (𝑦(Hom ‘𝐶)𝑧)) ∧ 𝑤 ∈ (Base‘𝐶)) ∧ ℎ ∈ (𝑧(Hom ‘𝐶)𝑤)) → 𝑤 ∈ (Base‘𝐶)) |
189 | | simpllr 795 |
. . . . . . . . . . . . . . 15
⊢
((((((((𝜑 ∧ 𝑥 ∈ (Base‘𝐶)) ∧ 𝑦 ∈ (Base‘𝐶)) ∧ 𝑧 ∈ (Base‘𝐶)) ∧ 𝑓 ∈ (𝑥(Hom ‘𝐶)𝑦)) ∧ 𝑔 ∈ (𝑦(Hom ‘𝐶)𝑧)) ∧ 𝑤 ∈ (Base‘𝐶)) ∧ ℎ ∈ (𝑧(Hom ‘𝐶)𝑤)) → 𝑔 ∈ (𝑦(Hom ‘𝐶)𝑧)) |
190 | | simpr 476 |
. . . . . . . . . . . . . . 15
⊢
((((((((𝜑 ∧ 𝑥 ∈ (Base‘𝐶)) ∧ 𝑦 ∈ (Base‘𝐶)) ∧ 𝑧 ∈ (Base‘𝐶)) ∧ 𝑓 ∈ (𝑥(Hom ‘𝐶)𝑦)) ∧ 𝑔 ∈ (𝑦(Hom ‘𝐶)𝑧)) ∧ 𝑤 ∈ (Base‘𝐶)) ∧ ℎ ∈ (𝑧(Hom ‘𝐶)𝑤)) → ℎ ∈ (𝑧(Hom ‘𝐶)𝑤)) |
191 | 70, 71, 72, 73, 184, 185, 186, 187, 188, 189, 190 | comfeqval 16191 |
. . . . . . . . . . . . . 14
⊢
((((((((𝜑 ∧ 𝑥 ∈ (Base‘𝐶)) ∧ 𝑦 ∈ (Base‘𝐶)) ∧ 𝑧 ∈ (Base‘𝐶)) ∧ 𝑓 ∈ (𝑥(Hom ‘𝐶)𝑦)) ∧ 𝑔 ∈ (𝑦(Hom ‘𝐶)𝑧)) ∧ 𝑤 ∈ (Base‘𝐶)) ∧ ℎ ∈ (𝑧(Hom ‘𝐶)𝑤)) → (ℎ(〈𝑦, 𝑧〉(comp‘𝐶)𝑤)𝑔) = (ℎ(〈𝑦, 𝑧〉(comp‘𝐷)𝑤)𝑔)) |
192 | 191 | oveq1d 6564 |
. . . . . . . . . . . . 13
⊢
((((((((𝜑 ∧ 𝑥 ∈ (Base‘𝐶)) ∧ 𝑦 ∈ (Base‘𝐶)) ∧ 𝑧 ∈ (Base‘𝐶)) ∧ 𝑓 ∈ (𝑥(Hom ‘𝐶)𝑦)) ∧ 𝑔 ∈ (𝑦(Hom ‘𝐶)𝑧)) ∧ 𝑤 ∈ (Base‘𝐶)) ∧ ℎ ∈ (𝑧(Hom ‘𝐶)𝑤)) → ((ℎ(〈𝑦, 𝑧〉(comp‘𝐶)𝑤)𝑔)(〈𝑥, 𝑦〉(comp‘𝐷)𝑤)𝑓) = ((ℎ(〈𝑦, 𝑧〉(comp‘𝐷)𝑤)𝑔)(〈𝑥, 𝑦〉(comp‘𝐷)𝑤)𝑓)) |
193 | 81 | ad4antr 764 |
. . . . . . . . . . . . . . 15
⊢
((((((((𝜑 ∧ 𝑥 ∈ (Base‘𝐶)) ∧ 𝑦 ∈ (Base‘𝐶)) ∧ 𝑧 ∈ (Base‘𝐶)) ∧ 𝑓 ∈ (𝑥(Hom ‘𝐶)𝑦)) ∧ 𝑔 ∈ (𝑦(Hom ‘𝐶)𝑧)) ∧ 𝑤 ∈ (Base‘𝐶)) ∧ ℎ ∈ (𝑧(Hom ‘𝐶)𝑤)) → 𝑥 ∈ (Base‘𝐶)) |
194 | | simp-4r 803 |
. . . . . . . . . . . . . . 15
⊢
((((((((𝜑 ∧ 𝑥 ∈ (Base‘𝐶)) ∧ 𝑦 ∈ (Base‘𝐶)) ∧ 𝑧 ∈ (Base‘𝐶)) ∧ 𝑓 ∈ (𝑥(Hom ‘𝐶)𝑦)) ∧ 𝑔 ∈ (𝑦(Hom ‘𝐶)𝑧)) ∧ 𝑤 ∈ (Base‘𝐶)) ∧ ℎ ∈ (𝑧(Hom ‘𝐶)𝑤)) → 𝑓 ∈ (𝑥(Hom ‘𝐶)𝑦)) |
195 | 70, 71, 72, 73, 184, 185, 193, 186, 187, 194, 189 | comfeqval 16191 |
. . . . . . . . . . . . . 14
⊢
((((((((𝜑 ∧ 𝑥 ∈ (Base‘𝐶)) ∧ 𝑦 ∈ (Base‘𝐶)) ∧ 𝑧 ∈ (Base‘𝐶)) ∧ 𝑓 ∈ (𝑥(Hom ‘𝐶)𝑦)) ∧ 𝑔 ∈ (𝑦(Hom ‘𝐶)𝑧)) ∧ 𝑤 ∈ (Base‘𝐶)) ∧ ℎ ∈ (𝑧(Hom ‘𝐶)𝑤)) → (𝑔(〈𝑥, 𝑦〉(comp‘𝐶)𝑧)𝑓) = (𝑔(〈𝑥, 𝑦〉(comp‘𝐷)𝑧)𝑓)) |
196 | 195 | oveq2d 6565 |
. . . . . . . . . . . . 13
⊢
((((((((𝜑 ∧ 𝑥 ∈ (Base‘𝐶)) ∧ 𝑦 ∈ (Base‘𝐶)) ∧ 𝑧 ∈ (Base‘𝐶)) ∧ 𝑓 ∈ (𝑥(Hom ‘𝐶)𝑦)) ∧ 𝑔 ∈ (𝑦(Hom ‘𝐶)𝑧)) ∧ 𝑤 ∈ (Base‘𝐶)) ∧ ℎ ∈ (𝑧(Hom ‘𝐶)𝑤)) → (ℎ(〈𝑥, 𝑧〉(comp‘𝐷)𝑤)(𝑔(〈𝑥, 𝑦〉(comp‘𝐶)𝑧)𝑓)) = (ℎ(〈𝑥, 𝑧〉(comp‘𝐷)𝑤)(𝑔(〈𝑥, 𝑦〉(comp‘𝐷)𝑧)𝑓))) |
197 | 192, 196 | eqeq12d 2625 |
. . . . . . . . . . . 12
⊢
((((((((𝜑 ∧ 𝑥 ∈ (Base‘𝐶)) ∧ 𝑦 ∈ (Base‘𝐶)) ∧ 𝑧 ∈ (Base‘𝐶)) ∧ 𝑓 ∈ (𝑥(Hom ‘𝐶)𝑦)) ∧ 𝑔 ∈ (𝑦(Hom ‘𝐶)𝑧)) ∧ 𝑤 ∈ (Base‘𝐶)) ∧ ℎ ∈ (𝑧(Hom ‘𝐶)𝑤)) → (((ℎ(〈𝑦, 𝑧〉(comp‘𝐶)𝑤)𝑔)(〈𝑥, 𝑦〉(comp‘𝐷)𝑤)𝑓) = (ℎ(〈𝑥, 𝑧〉(comp‘𝐷)𝑤)(𝑔(〈𝑥, 𝑦〉(comp‘𝐶)𝑧)𝑓)) ↔ ((ℎ(〈𝑦, 𝑧〉(comp‘𝐷)𝑤)𝑔)(〈𝑥, 𝑦〉(comp‘𝐷)𝑤)𝑓) = (ℎ(〈𝑥, 𝑧〉(comp‘𝐷)𝑤)(𝑔(〈𝑥, 𝑦〉(comp‘𝐷)𝑧)𝑓)))) |
198 | 183, 197 | raleqbidva 3131 |
. . . . . . . . . . 11
⊢
(((((((𝜑 ∧ 𝑥 ∈ (Base‘𝐶)) ∧ 𝑦 ∈ (Base‘𝐶)) ∧ 𝑧 ∈ (Base‘𝐶)) ∧ 𝑓 ∈ (𝑥(Hom ‘𝐶)𝑦)) ∧ 𝑔 ∈ (𝑦(Hom ‘𝐶)𝑧)) ∧ 𝑤 ∈ (Base‘𝐶)) → (∀ℎ ∈ (𝑧(Hom ‘𝐶)𝑤)((ℎ(〈𝑦, 𝑧〉(comp‘𝐶)𝑤)𝑔)(〈𝑥, 𝑦〉(comp‘𝐷)𝑤)𝑓) = (ℎ(〈𝑥, 𝑧〉(comp‘𝐷)𝑤)(𝑔(〈𝑥, 𝑦〉(comp‘𝐶)𝑧)𝑓)) ↔ ∀ℎ ∈ (𝑧(Hom ‘𝐷)𝑤)((ℎ(〈𝑦, 𝑧〉(comp‘𝐷)𝑤)𝑔)(〈𝑥, 𝑦〉(comp‘𝐷)𝑤)𝑓) = (ℎ(〈𝑥, 𝑧〉(comp‘𝐷)𝑤)(𝑔(〈𝑥, 𝑦〉(comp‘𝐷)𝑧)𝑓)))) |
199 | 179, 198 | raleqbidva 3131 |
. . . . . . . . . 10
⊢
((((((𝜑 ∧ 𝑥 ∈ (Base‘𝐶)) ∧ 𝑦 ∈ (Base‘𝐶)) ∧ 𝑧 ∈ (Base‘𝐶)) ∧ 𝑓 ∈ (𝑥(Hom ‘𝐶)𝑦)) ∧ 𝑔 ∈ (𝑦(Hom ‘𝐶)𝑧)) → (∀𝑤 ∈ (Base‘𝐶)∀ℎ ∈ (𝑧(Hom ‘𝐶)𝑤)((ℎ(〈𝑦, 𝑧〉(comp‘𝐶)𝑤)𝑔)(〈𝑥, 𝑦〉(comp‘𝐷)𝑤)𝑓) = (ℎ(〈𝑥, 𝑧〉(comp‘𝐷)𝑤)(𝑔(〈𝑥, 𝑦〉(comp‘𝐶)𝑧)𝑓)) ↔ ∀𝑤 ∈ (Base‘𝐷)∀ℎ ∈ (𝑧(Hom ‘𝐷)𝑤)((ℎ(〈𝑦, 𝑧〉(comp‘𝐷)𝑤)𝑔)(〈𝑥, 𝑦〉(comp‘𝐷)𝑤)𝑓) = (ℎ(〈𝑥, 𝑧〉(comp‘𝐷)𝑤)(𝑔(〈𝑥, 𝑦〉(comp‘𝐷)𝑧)𝑓)))) |
200 | 178, 199 | anbi12d 743 |
. . . . . . . . 9
⊢
((((((𝜑 ∧ 𝑥 ∈ (Base‘𝐶)) ∧ 𝑦 ∈ (Base‘𝐶)) ∧ 𝑧 ∈ (Base‘𝐶)) ∧ 𝑓 ∈ (𝑥(Hom ‘𝐶)𝑦)) ∧ 𝑔 ∈ (𝑦(Hom ‘𝐶)𝑧)) → (((𝑔(〈𝑥, 𝑦〉(comp‘𝐶)𝑧)𝑓) ∈ (𝑥(Hom ‘𝐶)𝑧) ∧ ∀𝑤 ∈ (Base‘𝐶)∀ℎ ∈ (𝑧(Hom ‘𝐶)𝑤)((ℎ(〈𝑦, 𝑧〉(comp‘𝐶)𝑤)𝑔)(〈𝑥, 𝑦〉(comp‘𝐷)𝑤)𝑓) = (ℎ(〈𝑥, 𝑧〉(comp‘𝐷)𝑤)(𝑔(〈𝑥, 𝑦〉(comp‘𝐶)𝑧)𝑓))) ↔ ((𝑔(〈𝑥, 𝑦〉(comp‘𝐷)𝑧)𝑓) ∈ (𝑥(Hom ‘𝐷)𝑧) ∧ ∀𝑤 ∈ (Base‘𝐷)∀ℎ ∈ (𝑧(Hom ‘𝐷)𝑤)((ℎ(〈𝑦, 𝑧〉(comp‘𝐷)𝑤)𝑔)(〈𝑥, 𝑦〉(comp‘𝐷)𝑤)𝑓) = (ℎ(〈𝑥, 𝑧〉(comp‘𝐷)𝑤)(𝑔(〈𝑥, 𝑦〉(comp‘𝐷)𝑧)𝑓))))) |
201 | 173, 200 | raleqbidva 3131 |
. . . . . . . 8
⊢
(((((𝜑 ∧ 𝑥 ∈ (Base‘𝐶)) ∧ 𝑦 ∈ (Base‘𝐶)) ∧ 𝑧 ∈ (Base‘𝐶)) ∧ 𝑓 ∈ (𝑥(Hom ‘𝐶)𝑦)) → (∀𝑔 ∈ (𝑦(Hom ‘𝐶)𝑧)((𝑔(〈𝑥, 𝑦〉(comp‘𝐶)𝑧)𝑓) ∈ (𝑥(Hom ‘𝐶)𝑧) ∧ ∀𝑤 ∈ (Base‘𝐶)∀ℎ ∈ (𝑧(Hom ‘𝐶)𝑤)((ℎ(〈𝑦, 𝑧〉(comp‘𝐶)𝑤)𝑔)(〈𝑥, 𝑦〉(comp‘𝐷)𝑤)𝑓) = (ℎ(〈𝑥, 𝑧〉(comp‘𝐷)𝑤)(𝑔(〈𝑥, 𝑦〉(comp‘𝐶)𝑧)𝑓))) ↔ ∀𝑔 ∈ (𝑦(Hom ‘𝐷)𝑧)((𝑔(〈𝑥, 𝑦〉(comp‘𝐷)𝑧)𝑓) ∈ (𝑥(Hom ‘𝐷)𝑧) ∧ ∀𝑤 ∈ (Base‘𝐷)∀ℎ ∈ (𝑧(Hom ‘𝐷)𝑤)((ℎ(〈𝑦, 𝑧〉(comp‘𝐷)𝑤)𝑔)(〈𝑥, 𝑦〉(comp‘𝐷)𝑤)𝑓) = (ℎ(〈𝑥, 𝑧〉(comp‘𝐷)𝑤)(𝑔(〈𝑥, 𝑦〉(comp‘𝐷)𝑧)𝑓))))) |
202 | 170, 201 | raleqbidva 3131 |
. . . . . . 7
⊢ ((((𝜑 ∧ 𝑥 ∈ (Base‘𝐶)) ∧ 𝑦 ∈ (Base‘𝐶)) ∧ 𝑧 ∈ (Base‘𝐶)) → (∀𝑓 ∈ (𝑥(Hom ‘𝐶)𝑦)∀𝑔 ∈ (𝑦(Hom ‘𝐶)𝑧)((𝑔(〈𝑥, 𝑦〉(comp‘𝐶)𝑧)𝑓) ∈ (𝑥(Hom ‘𝐶)𝑧) ∧ ∀𝑤 ∈ (Base‘𝐶)∀ℎ ∈ (𝑧(Hom ‘𝐶)𝑤)((ℎ(〈𝑦, 𝑧〉(comp‘𝐶)𝑤)𝑔)(〈𝑥, 𝑦〉(comp‘𝐷)𝑤)𝑓) = (ℎ(〈𝑥, 𝑧〉(comp‘𝐷)𝑤)(𝑔(〈𝑥, 𝑦〉(comp‘𝐶)𝑧)𝑓))) ↔ ∀𝑓 ∈ (𝑥(Hom ‘𝐷)𝑦)∀𝑔 ∈ (𝑦(Hom ‘𝐷)𝑧)((𝑔(〈𝑥, 𝑦〉(comp‘𝐷)𝑧)𝑓) ∈ (𝑥(Hom ‘𝐷)𝑧) ∧ ∀𝑤 ∈ (Base‘𝐷)∀ℎ ∈ (𝑧(Hom ‘𝐷)𝑤)((ℎ(〈𝑦, 𝑧〉(comp‘𝐷)𝑤)𝑔)(〈𝑥, 𝑦〉(comp‘𝐷)𝑤)𝑓) = (ℎ(〈𝑥, 𝑧〉(comp‘𝐷)𝑤)(𝑔(〈𝑥, 𝑦〉(comp‘𝐷)𝑧)𝑓))))) |
203 | 167, 202 | raleqbidva 3131 |
. . . . . 6
⊢ (((𝜑 ∧ 𝑥 ∈ (Base‘𝐶)) ∧ 𝑦 ∈ (Base‘𝐶)) → (∀𝑧 ∈ (Base‘𝐶)∀𝑓 ∈ (𝑥(Hom ‘𝐶)𝑦)∀𝑔 ∈ (𝑦(Hom ‘𝐶)𝑧)((𝑔(〈𝑥, 𝑦〉(comp‘𝐶)𝑧)𝑓) ∈ (𝑥(Hom ‘𝐶)𝑧) ∧ ∀𝑤 ∈ (Base‘𝐶)∀ℎ ∈ (𝑧(Hom ‘𝐶)𝑤)((ℎ(〈𝑦, 𝑧〉(comp‘𝐶)𝑤)𝑔)(〈𝑥, 𝑦〉(comp‘𝐷)𝑤)𝑓) = (ℎ(〈𝑥, 𝑧〉(comp‘𝐷)𝑤)(𝑔(〈𝑥, 𝑦〉(comp‘𝐶)𝑧)𝑓))) ↔ ∀𝑧 ∈ (Base‘𝐷)∀𝑓 ∈ (𝑥(Hom ‘𝐷)𝑦)∀𝑔 ∈ (𝑦(Hom ‘𝐷)𝑧)((𝑔(〈𝑥, 𝑦〉(comp‘𝐷)𝑧)𝑓) ∈ (𝑥(Hom ‘𝐷)𝑧) ∧ ∀𝑤 ∈ (Base‘𝐷)∀ℎ ∈ (𝑧(Hom ‘𝐷)𝑤)((ℎ(〈𝑦, 𝑧〉(comp‘𝐷)𝑤)𝑔)(〈𝑥, 𝑦〉(comp‘𝐷)𝑤)𝑓) = (ℎ(〈𝑥, 𝑧〉(comp‘𝐷)𝑤)(𝑔(〈𝑥, 𝑦〉(comp‘𝐷)𝑧)𝑓))))) |
204 | 166, 203 | raleqbidva 3131 |
. . . . 5
⊢ ((𝜑 ∧ 𝑥 ∈ (Base‘𝐶)) → (∀𝑦 ∈ (Base‘𝐶)∀𝑧 ∈ (Base‘𝐶)∀𝑓 ∈ (𝑥(Hom ‘𝐶)𝑦)∀𝑔 ∈ (𝑦(Hom ‘𝐶)𝑧)((𝑔(〈𝑥, 𝑦〉(comp‘𝐶)𝑧)𝑓) ∈ (𝑥(Hom ‘𝐶)𝑧) ∧ ∀𝑤 ∈ (Base‘𝐶)∀ℎ ∈ (𝑧(Hom ‘𝐶)𝑤)((ℎ(〈𝑦, 𝑧〉(comp‘𝐶)𝑤)𝑔)(〈𝑥, 𝑦〉(comp‘𝐷)𝑤)𝑓) = (ℎ(〈𝑥, 𝑧〉(comp‘𝐷)𝑤)(𝑔(〈𝑥, 𝑦〉(comp‘𝐶)𝑧)𝑓))) ↔ ∀𝑦 ∈ (Base‘𝐷)∀𝑧 ∈ (Base‘𝐷)∀𝑓 ∈ (𝑥(Hom ‘𝐷)𝑦)∀𝑔 ∈ (𝑦(Hom ‘𝐷)𝑧)((𝑔(〈𝑥, 𝑦〉(comp‘𝐷)𝑧)𝑓) ∈ (𝑥(Hom ‘𝐷)𝑧) ∧ ∀𝑤 ∈ (Base‘𝐷)∀ℎ ∈ (𝑧(Hom ‘𝐷)𝑤)((ℎ(〈𝑦, 𝑧〉(comp‘𝐷)𝑤)𝑔)(〈𝑥, 𝑦〉(comp‘𝐷)𝑤)𝑓) = (ℎ(〈𝑥, 𝑧〉(comp‘𝐷)𝑤)(𝑔(〈𝑥, 𝑦〉(comp‘𝐷)𝑧)𝑓))))) |
205 | 165, 204 | anbi12d 743 |
. . . 4
⊢ ((𝜑 ∧ 𝑥 ∈ (Base‘𝐶)) → ((∃𝑔 ∈ (𝑥(Hom ‘𝐶)𝑥)∀𝑦 ∈ (Base‘𝐶)(∀𝑓 ∈ (𝑦(Hom ‘𝐶)𝑥)(𝑔(〈𝑦, 𝑥〉(comp‘𝐶)𝑥)𝑓) = 𝑓 ∧ ∀𝑓 ∈ (𝑥(Hom ‘𝐶)𝑦)(𝑓(〈𝑥, 𝑥〉(comp‘𝐶)𝑦)𝑔) = 𝑓) ∧ ∀𝑦 ∈ (Base‘𝐶)∀𝑧 ∈ (Base‘𝐶)∀𝑓 ∈ (𝑥(Hom ‘𝐶)𝑦)∀𝑔 ∈ (𝑦(Hom ‘𝐶)𝑧)((𝑔(〈𝑥, 𝑦〉(comp‘𝐶)𝑧)𝑓) ∈ (𝑥(Hom ‘𝐶)𝑧) ∧ ∀𝑤 ∈ (Base‘𝐶)∀ℎ ∈ (𝑧(Hom ‘𝐶)𝑤)((ℎ(〈𝑦, 𝑧〉(comp‘𝐶)𝑤)𝑔)(〈𝑥, 𝑦〉(comp‘𝐷)𝑤)𝑓) = (ℎ(〈𝑥, 𝑧〉(comp‘𝐷)𝑤)(𝑔(〈𝑥, 𝑦〉(comp‘𝐶)𝑧)𝑓)))) ↔ (∃𝑔 ∈ (𝑥(Hom ‘𝐷)𝑥)∀𝑦 ∈ (Base‘𝐷)(∀𝑓 ∈ (𝑦(Hom ‘𝐷)𝑥)(𝑔(〈𝑦, 𝑥〉(comp‘𝐷)𝑥)𝑓) = 𝑓 ∧ ∀𝑓 ∈ (𝑥(Hom ‘𝐷)𝑦)(𝑓(〈𝑥, 𝑥〉(comp‘𝐷)𝑦)𝑔) = 𝑓) ∧ ∀𝑦 ∈ (Base‘𝐷)∀𝑧 ∈ (Base‘𝐷)∀𝑓 ∈ (𝑥(Hom ‘𝐷)𝑦)∀𝑔 ∈ (𝑦(Hom ‘𝐷)𝑧)((𝑔(〈𝑥, 𝑦〉(comp‘𝐷)𝑧)𝑓) ∈ (𝑥(Hom ‘𝐷)𝑧) ∧ ∀𝑤 ∈ (Base‘𝐷)∀ℎ ∈ (𝑧(Hom ‘𝐷)𝑤)((ℎ(〈𝑦, 𝑧〉(comp‘𝐷)𝑤)𝑔)(〈𝑥, 𝑦〉(comp‘𝐷)𝑤)𝑓) = (ℎ(〈𝑥, 𝑧〉(comp‘𝐷)𝑤)(𝑔(〈𝑥, 𝑦〉(comp‘𝐷)𝑧)𝑓)))))) |
206 | 135, 205 | raleqbidva 3131 |
. . 3
⊢ (𝜑 → (∀𝑥 ∈ (Base‘𝐶)(∃𝑔 ∈ (𝑥(Hom ‘𝐶)𝑥)∀𝑦 ∈ (Base‘𝐶)(∀𝑓 ∈ (𝑦(Hom ‘𝐶)𝑥)(𝑔(〈𝑦, 𝑥〉(comp‘𝐶)𝑥)𝑓) = 𝑓 ∧ ∀𝑓 ∈ (𝑥(Hom ‘𝐶)𝑦)(𝑓(〈𝑥, 𝑥〉(comp‘𝐶)𝑦)𝑔) = 𝑓) ∧ ∀𝑦 ∈ (Base‘𝐶)∀𝑧 ∈ (Base‘𝐶)∀𝑓 ∈ (𝑥(Hom ‘𝐶)𝑦)∀𝑔 ∈ (𝑦(Hom ‘𝐶)𝑧)((𝑔(〈𝑥, 𝑦〉(comp‘𝐶)𝑧)𝑓) ∈ (𝑥(Hom ‘𝐶)𝑧) ∧ ∀𝑤 ∈ (Base‘𝐶)∀ℎ ∈ (𝑧(Hom ‘𝐶)𝑤)((ℎ(〈𝑦, 𝑧〉(comp‘𝐶)𝑤)𝑔)(〈𝑥, 𝑦〉(comp‘𝐷)𝑤)𝑓) = (ℎ(〈𝑥, 𝑧〉(comp‘𝐷)𝑤)(𝑔(〈𝑥, 𝑦〉(comp‘𝐶)𝑧)𝑓)))) ↔ ∀𝑥 ∈ (Base‘𝐷)(∃𝑔 ∈ (𝑥(Hom ‘𝐷)𝑥)∀𝑦 ∈ (Base‘𝐷)(∀𝑓 ∈ (𝑦(Hom ‘𝐷)𝑥)(𝑔(〈𝑦, 𝑥〉(comp‘𝐷)𝑥)𝑓) = 𝑓 ∧ ∀𝑓 ∈ (𝑥(Hom ‘𝐷)𝑦)(𝑓(〈𝑥, 𝑥〉(comp‘𝐷)𝑦)𝑔) = 𝑓) ∧ ∀𝑦 ∈ (Base‘𝐷)∀𝑧 ∈ (Base‘𝐷)∀𝑓 ∈ (𝑥(Hom ‘𝐷)𝑦)∀𝑔 ∈ (𝑦(Hom ‘𝐷)𝑧)((𝑔(〈𝑥, 𝑦〉(comp‘𝐷)𝑧)𝑓) ∈ (𝑥(Hom ‘𝐷)𝑧) ∧ ∀𝑤 ∈ (Base‘𝐷)∀ℎ ∈ (𝑧(Hom ‘𝐷)𝑤)((ℎ(〈𝑦, 𝑧〉(comp‘𝐷)𝑤)𝑔)(〈𝑥, 𝑦〉(comp‘𝐷)𝑤)𝑓) = (ℎ(〈𝑥, 𝑧〉(comp‘𝐷)𝑤)(𝑔(〈𝑥, 𝑦〉(comp‘𝐷)𝑧)𝑓)))))) |
207 | 134, 206 | bitrd 267 |
. 2
⊢ (𝜑 → (∀𝑥 ∈ (Base‘𝐶)(∃𝑔 ∈ (𝑥(Hom ‘𝐶)𝑥)∀𝑦 ∈ (Base‘𝐶)(∀𝑓 ∈ (𝑦(Hom ‘𝐶)𝑥)(𝑔(〈𝑦, 𝑥〉(comp‘𝐶)𝑥)𝑓) = 𝑓 ∧ ∀𝑓 ∈ (𝑥(Hom ‘𝐶)𝑦)(𝑓(〈𝑥, 𝑥〉(comp‘𝐶)𝑦)𝑔) = 𝑓) ∧ ∀𝑦 ∈ (Base‘𝐶)∀𝑧 ∈ (Base‘𝐶)∀𝑓 ∈ (𝑥(Hom ‘𝐶)𝑦)∀𝑔 ∈ (𝑦(Hom ‘𝐶)𝑧)((𝑔(〈𝑥, 𝑦〉(comp‘𝐶)𝑧)𝑓) ∈ (𝑥(Hom ‘𝐶)𝑧) ∧ ∀𝑤 ∈ (Base‘𝐶)∀ℎ ∈ (𝑧(Hom ‘𝐶)𝑤)((ℎ(〈𝑦, 𝑧〉(comp‘𝐶)𝑤)𝑔)(〈𝑥, 𝑦〉(comp‘𝐶)𝑤)𝑓) = (ℎ(〈𝑥, 𝑧〉(comp‘𝐶)𝑤)(𝑔(〈𝑥, 𝑦〉(comp‘𝐶)𝑧)𝑓)))) ↔ ∀𝑥 ∈ (Base‘𝐷)(∃𝑔 ∈ (𝑥(Hom ‘𝐷)𝑥)∀𝑦 ∈ (Base‘𝐷)(∀𝑓 ∈ (𝑦(Hom ‘𝐷)𝑥)(𝑔(〈𝑦, 𝑥〉(comp‘𝐷)𝑥)𝑓) = 𝑓 ∧ ∀𝑓 ∈ (𝑥(Hom ‘𝐷)𝑦)(𝑓(〈𝑥, 𝑥〉(comp‘𝐷)𝑦)𝑔) = 𝑓) ∧ ∀𝑦 ∈ (Base‘𝐷)∀𝑧 ∈ (Base‘𝐷)∀𝑓 ∈ (𝑥(Hom ‘𝐷)𝑦)∀𝑔 ∈ (𝑦(Hom ‘𝐷)𝑧)((𝑔(〈𝑥, 𝑦〉(comp‘𝐷)𝑧)𝑓) ∈ (𝑥(Hom ‘𝐷)𝑧) ∧ ∀𝑤 ∈ (Base‘𝐷)∀ℎ ∈ (𝑧(Hom ‘𝐷)𝑤)((ℎ(〈𝑦, 𝑧〉(comp‘𝐷)𝑤)𝑔)(〈𝑥, 𝑦〉(comp‘𝐷)𝑤)𝑓) = (ℎ(〈𝑥, 𝑧〉(comp‘𝐷)𝑤)(𝑔(〈𝑥, 𝑦〉(comp‘𝐷)𝑧)𝑓)))))) |
208 | | catpropd.3 |
. . 3
⊢ (𝜑 → 𝐶 ∈ 𝑉) |
209 | 70, 71, 72 | iscat 16156 |
. . 3
⊢ (𝐶 ∈ 𝑉 → (𝐶 ∈ Cat ↔ ∀𝑥 ∈ (Base‘𝐶)(∃𝑔 ∈ (𝑥(Hom ‘𝐶)𝑥)∀𝑦 ∈ (Base‘𝐶)(∀𝑓 ∈ (𝑦(Hom ‘𝐶)𝑥)(𝑔(〈𝑦, 𝑥〉(comp‘𝐶)𝑥)𝑓) = 𝑓 ∧ ∀𝑓 ∈ (𝑥(Hom ‘𝐶)𝑦)(𝑓(〈𝑥, 𝑥〉(comp‘𝐶)𝑦)𝑔) = 𝑓) ∧ ∀𝑦 ∈ (Base‘𝐶)∀𝑧 ∈ (Base‘𝐶)∀𝑓 ∈ (𝑥(Hom ‘𝐶)𝑦)∀𝑔 ∈ (𝑦(Hom ‘𝐶)𝑧)((𝑔(〈𝑥, 𝑦〉(comp‘𝐶)𝑧)𝑓) ∈ (𝑥(Hom ‘𝐶)𝑧) ∧ ∀𝑤 ∈ (Base‘𝐶)∀ℎ ∈ (𝑧(Hom ‘𝐶)𝑤)((ℎ(〈𝑦, 𝑧〉(comp‘𝐶)𝑤)𝑔)(〈𝑥, 𝑦〉(comp‘𝐶)𝑤)𝑓) = (ℎ(〈𝑥, 𝑧〉(comp‘𝐶)𝑤)(𝑔(〈𝑥, 𝑦〉(comp‘𝐶)𝑧)𝑓)))))) |
210 | 208, 209 | syl 17 |
. 2
⊢ (𝜑 → (𝐶 ∈ Cat ↔ ∀𝑥 ∈ (Base‘𝐶)(∃𝑔 ∈ (𝑥(Hom ‘𝐶)𝑥)∀𝑦 ∈ (Base‘𝐶)(∀𝑓 ∈ (𝑦(Hom ‘𝐶)𝑥)(𝑔(〈𝑦, 𝑥〉(comp‘𝐶)𝑥)𝑓) = 𝑓 ∧ ∀𝑓 ∈ (𝑥(Hom ‘𝐶)𝑦)(𝑓(〈𝑥, 𝑥〉(comp‘𝐶)𝑦)𝑔) = 𝑓) ∧ ∀𝑦 ∈ (Base‘𝐶)∀𝑧 ∈ (Base‘𝐶)∀𝑓 ∈ (𝑥(Hom ‘𝐶)𝑦)∀𝑔 ∈ (𝑦(Hom ‘𝐶)𝑧)((𝑔(〈𝑥, 𝑦〉(comp‘𝐶)𝑧)𝑓) ∈ (𝑥(Hom ‘𝐶)𝑧) ∧ ∀𝑤 ∈ (Base‘𝐶)∀ℎ ∈ (𝑧(Hom ‘𝐶)𝑤)((ℎ(〈𝑦, 𝑧〉(comp‘𝐶)𝑤)𝑔)(〈𝑥, 𝑦〉(comp‘𝐶)𝑤)𝑓) = (ℎ(〈𝑥, 𝑧〉(comp‘𝐶)𝑤)(𝑔(〈𝑥, 𝑦〉(comp‘𝐶)𝑧)𝑓)))))) |
211 | | catpropd.4 |
. . 3
⊢ (𝜑 → 𝐷 ∈ 𝑊) |
212 | | eqid 2610 |
. . . 4
⊢
(Base‘𝐷) =
(Base‘𝐷) |
213 | 212, 136,
73 | iscat 16156 |
. . 3
⊢ (𝐷 ∈ 𝑊 → (𝐷 ∈ Cat ↔ ∀𝑥 ∈ (Base‘𝐷)(∃𝑔 ∈ (𝑥(Hom ‘𝐷)𝑥)∀𝑦 ∈ (Base‘𝐷)(∀𝑓 ∈ (𝑦(Hom ‘𝐷)𝑥)(𝑔(〈𝑦, 𝑥〉(comp‘𝐷)𝑥)𝑓) = 𝑓 ∧ ∀𝑓 ∈ (𝑥(Hom ‘𝐷)𝑦)(𝑓(〈𝑥, 𝑥〉(comp‘𝐷)𝑦)𝑔) = 𝑓) ∧ ∀𝑦 ∈ (Base‘𝐷)∀𝑧 ∈ (Base‘𝐷)∀𝑓 ∈ (𝑥(Hom ‘𝐷)𝑦)∀𝑔 ∈ (𝑦(Hom ‘𝐷)𝑧)((𝑔(〈𝑥, 𝑦〉(comp‘𝐷)𝑧)𝑓) ∈ (𝑥(Hom ‘𝐷)𝑧) ∧ ∀𝑤 ∈ (Base‘𝐷)∀ℎ ∈ (𝑧(Hom ‘𝐷)𝑤)((ℎ(〈𝑦, 𝑧〉(comp‘𝐷)𝑤)𝑔)(〈𝑥, 𝑦〉(comp‘𝐷)𝑤)𝑓) = (ℎ(〈𝑥, 𝑧〉(comp‘𝐷)𝑤)(𝑔(〈𝑥, 𝑦〉(comp‘𝐷)𝑧)𝑓)))))) |
214 | 211, 213 | syl 17 |
. 2
⊢ (𝜑 → (𝐷 ∈ Cat ↔ ∀𝑥 ∈ (Base‘𝐷)(∃𝑔 ∈ (𝑥(Hom ‘𝐷)𝑥)∀𝑦 ∈ (Base‘𝐷)(∀𝑓 ∈ (𝑦(Hom ‘𝐷)𝑥)(𝑔(〈𝑦, 𝑥〉(comp‘𝐷)𝑥)𝑓) = 𝑓 ∧ ∀𝑓 ∈ (𝑥(Hom ‘𝐷)𝑦)(𝑓(〈𝑥, 𝑥〉(comp‘𝐷)𝑦)𝑔) = 𝑓) ∧ ∀𝑦 ∈ (Base‘𝐷)∀𝑧 ∈ (Base‘𝐷)∀𝑓 ∈ (𝑥(Hom ‘𝐷)𝑦)∀𝑔 ∈ (𝑦(Hom ‘𝐷)𝑧)((𝑔(〈𝑥, 𝑦〉(comp‘𝐷)𝑧)𝑓) ∈ (𝑥(Hom ‘𝐷)𝑧) ∧ ∀𝑤 ∈ (Base‘𝐷)∀ℎ ∈ (𝑧(Hom ‘𝐷)𝑤)((ℎ(〈𝑦, 𝑧〉(comp‘𝐷)𝑤)𝑔)(〈𝑥, 𝑦〉(comp‘𝐷)𝑤)𝑓) = (ℎ(〈𝑥, 𝑧〉(comp‘𝐷)𝑤)(𝑔(〈𝑥, 𝑦〉(comp‘𝐷)𝑧)𝑓)))))) |
215 | 207, 210,
214 | 3bitr4d 299 |
1
⊢ (𝜑 → (𝐶 ∈ Cat ↔ 𝐷 ∈ Cat)) |