Step | Hyp | Ref
| Expression |
1 | | natfval.1 |
. 2
⊢ 𝑁 = (𝐶 Nat 𝐷) |
2 | | oveq12 6558 |
. . . . 5
⊢ ((𝑡 = 𝐶 ∧ 𝑢 = 𝐷) → (𝑡 Func 𝑢) = (𝐶 Func 𝐷)) |
3 | | simpl 472 |
. . . . . . . . . . . 12
⊢ ((𝑡 = 𝐶 ∧ 𝑢 = 𝐷) → 𝑡 = 𝐶) |
4 | 3 | fveq2d 6107 |
. . . . . . . . . . 11
⊢ ((𝑡 = 𝐶 ∧ 𝑢 = 𝐷) → (Base‘𝑡) = (Base‘𝐶)) |
5 | | natfval.b |
. . . . . . . . . . 11
⊢ 𝐵 = (Base‘𝐶) |
6 | 4, 5 | syl6eqr 2662 |
. . . . . . . . . 10
⊢ ((𝑡 = 𝐶 ∧ 𝑢 = 𝐷) → (Base‘𝑡) = 𝐵) |
7 | 6 | ixpeq1d 7806 |
. . . . . . . . 9
⊢ ((𝑡 = 𝐶 ∧ 𝑢 = 𝐷) → X𝑥 ∈ (Base‘𝑡)((𝑟‘𝑥)(Hom ‘𝑢)(𝑠‘𝑥)) = X𝑥 ∈ 𝐵 ((𝑟‘𝑥)(Hom ‘𝑢)(𝑠‘𝑥))) |
8 | | simpr 476 |
. . . . . . . . . . . . 13
⊢ ((𝑡 = 𝐶 ∧ 𝑢 = 𝐷) → 𝑢 = 𝐷) |
9 | 8 | fveq2d 6107 |
. . . . . . . . . . . 12
⊢ ((𝑡 = 𝐶 ∧ 𝑢 = 𝐷) → (Hom ‘𝑢) = (Hom ‘𝐷)) |
10 | | natfval.j |
. . . . . . . . . . . 12
⊢ 𝐽 = (Hom ‘𝐷) |
11 | 9, 10 | syl6eqr 2662 |
. . . . . . . . . . 11
⊢ ((𝑡 = 𝐶 ∧ 𝑢 = 𝐷) → (Hom ‘𝑢) = 𝐽) |
12 | 11 | oveqd 6566 |
. . . . . . . . . 10
⊢ ((𝑡 = 𝐶 ∧ 𝑢 = 𝐷) → ((𝑟‘𝑥)(Hom ‘𝑢)(𝑠‘𝑥)) = ((𝑟‘𝑥)𝐽(𝑠‘𝑥))) |
13 | 12 | ixpeq2dv 7810 |
. . . . . . . . 9
⊢ ((𝑡 = 𝐶 ∧ 𝑢 = 𝐷) → X𝑥 ∈ 𝐵 ((𝑟‘𝑥)(Hom ‘𝑢)(𝑠‘𝑥)) = X𝑥 ∈ 𝐵 ((𝑟‘𝑥)𝐽(𝑠‘𝑥))) |
14 | 7, 13 | eqtrd 2644 |
. . . . . . . 8
⊢ ((𝑡 = 𝐶 ∧ 𝑢 = 𝐷) → X𝑥 ∈ (Base‘𝑡)((𝑟‘𝑥)(Hom ‘𝑢)(𝑠‘𝑥)) = X𝑥 ∈ 𝐵 ((𝑟‘𝑥)𝐽(𝑠‘𝑥))) |
15 | 3 | fveq2d 6107 |
. . . . . . . . . . . . 13
⊢ ((𝑡 = 𝐶 ∧ 𝑢 = 𝐷) → (Hom ‘𝑡) = (Hom ‘𝐶)) |
16 | | natfval.h |
. . . . . . . . . . . . 13
⊢ 𝐻 = (Hom ‘𝐶) |
17 | 15, 16 | syl6eqr 2662 |
. . . . . . . . . . . 12
⊢ ((𝑡 = 𝐶 ∧ 𝑢 = 𝐷) → (Hom ‘𝑡) = 𝐻) |
18 | 17 | oveqd 6566 |
. . . . . . . . . . 11
⊢ ((𝑡 = 𝐶 ∧ 𝑢 = 𝐷) → (𝑥(Hom ‘𝑡)𝑦) = (𝑥𝐻𝑦)) |
19 | 8 | fveq2d 6107 |
. . . . . . . . . . . . . . 15
⊢ ((𝑡 = 𝐶 ∧ 𝑢 = 𝐷) → (comp‘𝑢) = (comp‘𝐷)) |
20 | | natfval.o |
. . . . . . . . . . . . . . 15
⊢ · =
(comp‘𝐷) |
21 | 19, 20 | syl6eqr 2662 |
. . . . . . . . . . . . . 14
⊢ ((𝑡 = 𝐶 ∧ 𝑢 = 𝐷) → (comp‘𝑢) = · ) |
22 | 21 | oveqd 6566 |
. . . . . . . . . . . . 13
⊢ ((𝑡 = 𝐶 ∧ 𝑢 = 𝐷) → (〈(𝑟‘𝑥), (𝑟‘𝑦)〉(comp‘𝑢)(𝑠‘𝑦)) = (〈(𝑟‘𝑥), (𝑟‘𝑦)〉 · (𝑠‘𝑦))) |
23 | 22 | oveqd 6566 |
. . . . . . . . . . . 12
⊢ ((𝑡 = 𝐶 ∧ 𝑢 = 𝐷) → ((𝑎‘𝑦)(〈(𝑟‘𝑥), (𝑟‘𝑦)〉(comp‘𝑢)(𝑠‘𝑦))((𝑥(2nd ‘𝑓)𝑦)‘ℎ)) = ((𝑎‘𝑦)(〈(𝑟‘𝑥), (𝑟‘𝑦)〉 · (𝑠‘𝑦))((𝑥(2nd ‘𝑓)𝑦)‘ℎ))) |
24 | 21 | oveqd 6566 |
. . . . . . . . . . . . 13
⊢ ((𝑡 = 𝐶 ∧ 𝑢 = 𝐷) → (〈(𝑟‘𝑥), (𝑠‘𝑥)〉(comp‘𝑢)(𝑠‘𝑦)) = (〈(𝑟‘𝑥), (𝑠‘𝑥)〉 · (𝑠‘𝑦))) |
25 | 24 | oveqd 6566 |
. . . . . . . . . . . 12
⊢ ((𝑡 = 𝐶 ∧ 𝑢 = 𝐷) → (((𝑥(2nd ‘𝑔)𝑦)‘ℎ)(〈(𝑟‘𝑥), (𝑠‘𝑥)〉(comp‘𝑢)(𝑠‘𝑦))(𝑎‘𝑥)) = (((𝑥(2nd ‘𝑔)𝑦)‘ℎ)(〈(𝑟‘𝑥), (𝑠‘𝑥)〉 · (𝑠‘𝑦))(𝑎‘𝑥))) |
26 | 23, 25 | eqeq12d 2625 |
. . . . . . . . . . 11
⊢ ((𝑡 = 𝐶 ∧ 𝑢 = 𝐷) → (((𝑎‘𝑦)(〈(𝑟‘𝑥), (𝑟‘𝑦)〉(comp‘𝑢)(𝑠‘𝑦))((𝑥(2nd ‘𝑓)𝑦)‘ℎ)) = (((𝑥(2nd ‘𝑔)𝑦)‘ℎ)(〈(𝑟‘𝑥), (𝑠‘𝑥)〉(comp‘𝑢)(𝑠‘𝑦))(𝑎‘𝑥)) ↔ ((𝑎‘𝑦)(〈(𝑟‘𝑥), (𝑟‘𝑦)〉 · (𝑠‘𝑦))((𝑥(2nd ‘𝑓)𝑦)‘ℎ)) = (((𝑥(2nd ‘𝑔)𝑦)‘ℎ)(〈(𝑟‘𝑥), (𝑠‘𝑥)〉 · (𝑠‘𝑦))(𝑎‘𝑥)))) |
27 | 18, 26 | raleqbidv 3129 |
. . . . . . . . . 10
⊢ ((𝑡 = 𝐶 ∧ 𝑢 = 𝐷) → (∀ℎ ∈ (𝑥(Hom ‘𝑡)𝑦)((𝑎‘𝑦)(〈(𝑟‘𝑥), (𝑟‘𝑦)〉(comp‘𝑢)(𝑠‘𝑦))((𝑥(2nd ‘𝑓)𝑦)‘ℎ)) = (((𝑥(2nd ‘𝑔)𝑦)‘ℎ)(〈(𝑟‘𝑥), (𝑠‘𝑥)〉(comp‘𝑢)(𝑠‘𝑦))(𝑎‘𝑥)) ↔ ∀ℎ ∈ (𝑥𝐻𝑦)((𝑎‘𝑦)(〈(𝑟‘𝑥), (𝑟‘𝑦)〉 · (𝑠‘𝑦))((𝑥(2nd ‘𝑓)𝑦)‘ℎ)) = (((𝑥(2nd ‘𝑔)𝑦)‘ℎ)(〈(𝑟‘𝑥), (𝑠‘𝑥)〉 · (𝑠‘𝑦))(𝑎‘𝑥)))) |
28 | 6, 27 | raleqbidv 3129 |
. . . . . . . . 9
⊢ ((𝑡 = 𝐶 ∧ 𝑢 = 𝐷) → (∀𝑦 ∈ (Base‘𝑡)∀ℎ ∈ (𝑥(Hom ‘𝑡)𝑦)((𝑎‘𝑦)(〈(𝑟‘𝑥), (𝑟‘𝑦)〉(comp‘𝑢)(𝑠‘𝑦))((𝑥(2nd ‘𝑓)𝑦)‘ℎ)) = (((𝑥(2nd ‘𝑔)𝑦)‘ℎ)(〈(𝑟‘𝑥), (𝑠‘𝑥)〉(comp‘𝑢)(𝑠‘𝑦))(𝑎‘𝑥)) ↔ ∀𝑦 ∈ 𝐵 ∀ℎ ∈ (𝑥𝐻𝑦)((𝑎‘𝑦)(〈(𝑟‘𝑥), (𝑟‘𝑦)〉 · (𝑠‘𝑦))((𝑥(2nd ‘𝑓)𝑦)‘ℎ)) = (((𝑥(2nd ‘𝑔)𝑦)‘ℎ)(〈(𝑟‘𝑥), (𝑠‘𝑥)〉 · (𝑠‘𝑦))(𝑎‘𝑥)))) |
29 | 6, 28 | raleqbidv 3129 |
. . . . . . . 8
⊢ ((𝑡 = 𝐶 ∧ 𝑢 = 𝐷) → (∀𝑥 ∈ (Base‘𝑡)∀𝑦 ∈ (Base‘𝑡)∀ℎ ∈ (𝑥(Hom ‘𝑡)𝑦)((𝑎‘𝑦)(〈(𝑟‘𝑥), (𝑟‘𝑦)〉(comp‘𝑢)(𝑠‘𝑦))((𝑥(2nd ‘𝑓)𝑦)‘ℎ)) = (((𝑥(2nd ‘𝑔)𝑦)‘ℎ)(〈(𝑟‘𝑥), (𝑠‘𝑥)〉(comp‘𝑢)(𝑠‘𝑦))(𝑎‘𝑥)) ↔ ∀𝑥 ∈ 𝐵 ∀𝑦 ∈ 𝐵 ∀ℎ ∈ (𝑥𝐻𝑦)((𝑎‘𝑦)(〈(𝑟‘𝑥), (𝑟‘𝑦)〉 · (𝑠‘𝑦))((𝑥(2nd ‘𝑓)𝑦)‘ℎ)) = (((𝑥(2nd ‘𝑔)𝑦)‘ℎ)(〈(𝑟‘𝑥), (𝑠‘𝑥)〉 · (𝑠‘𝑦))(𝑎‘𝑥)))) |
30 | 14, 29 | rabeqbidv 3168 |
. . . . . . 7
⊢ ((𝑡 = 𝐶 ∧ 𝑢 = 𝐷) → {𝑎 ∈ X𝑥 ∈ (Base‘𝑡)((𝑟‘𝑥)(Hom ‘𝑢)(𝑠‘𝑥)) ∣ ∀𝑥 ∈ (Base‘𝑡)∀𝑦 ∈ (Base‘𝑡)∀ℎ ∈ (𝑥(Hom ‘𝑡)𝑦)((𝑎‘𝑦)(〈(𝑟‘𝑥), (𝑟‘𝑦)〉(comp‘𝑢)(𝑠‘𝑦))((𝑥(2nd ‘𝑓)𝑦)‘ℎ)) = (((𝑥(2nd ‘𝑔)𝑦)‘ℎ)(〈(𝑟‘𝑥), (𝑠‘𝑥)〉(comp‘𝑢)(𝑠‘𝑦))(𝑎‘𝑥))} = {𝑎 ∈ X𝑥 ∈ 𝐵 ((𝑟‘𝑥)𝐽(𝑠‘𝑥)) ∣ ∀𝑥 ∈ 𝐵 ∀𝑦 ∈ 𝐵 ∀ℎ ∈ (𝑥𝐻𝑦)((𝑎‘𝑦)(〈(𝑟‘𝑥), (𝑟‘𝑦)〉 · (𝑠‘𝑦))((𝑥(2nd ‘𝑓)𝑦)‘ℎ)) = (((𝑥(2nd ‘𝑔)𝑦)‘ℎ)(〈(𝑟‘𝑥), (𝑠‘𝑥)〉 · (𝑠‘𝑦))(𝑎‘𝑥))}) |
31 | 30 | csbeq2dv 3944 |
. . . . . 6
⊢ ((𝑡 = 𝐶 ∧ 𝑢 = 𝐷) → ⦋(1st
‘𝑔) / 𝑠⦌{𝑎 ∈ X𝑥 ∈
(Base‘𝑡)((𝑟‘𝑥)(Hom ‘𝑢)(𝑠‘𝑥)) ∣ ∀𝑥 ∈ (Base‘𝑡)∀𝑦 ∈ (Base‘𝑡)∀ℎ ∈ (𝑥(Hom ‘𝑡)𝑦)((𝑎‘𝑦)(〈(𝑟‘𝑥), (𝑟‘𝑦)〉(comp‘𝑢)(𝑠‘𝑦))((𝑥(2nd ‘𝑓)𝑦)‘ℎ)) = (((𝑥(2nd ‘𝑔)𝑦)‘ℎ)(〈(𝑟‘𝑥), (𝑠‘𝑥)〉(comp‘𝑢)(𝑠‘𝑦))(𝑎‘𝑥))} = ⦋(1st
‘𝑔) / 𝑠⦌{𝑎 ∈ X𝑥 ∈
𝐵 ((𝑟‘𝑥)𝐽(𝑠‘𝑥)) ∣ ∀𝑥 ∈ 𝐵 ∀𝑦 ∈ 𝐵 ∀ℎ ∈ (𝑥𝐻𝑦)((𝑎‘𝑦)(〈(𝑟‘𝑥), (𝑟‘𝑦)〉 · (𝑠‘𝑦))((𝑥(2nd ‘𝑓)𝑦)‘ℎ)) = (((𝑥(2nd ‘𝑔)𝑦)‘ℎ)(〈(𝑟‘𝑥), (𝑠‘𝑥)〉 · (𝑠‘𝑦))(𝑎‘𝑥))}) |
32 | 31 | csbeq2dv 3944 |
. . . . 5
⊢ ((𝑡 = 𝐶 ∧ 𝑢 = 𝐷) → ⦋(1st
‘𝑓) / 𝑟⦌⦋(1st
‘𝑔) / 𝑠⦌{𝑎 ∈ X𝑥 ∈
(Base‘𝑡)((𝑟‘𝑥)(Hom ‘𝑢)(𝑠‘𝑥)) ∣ ∀𝑥 ∈ (Base‘𝑡)∀𝑦 ∈ (Base‘𝑡)∀ℎ ∈ (𝑥(Hom ‘𝑡)𝑦)((𝑎‘𝑦)(〈(𝑟‘𝑥), (𝑟‘𝑦)〉(comp‘𝑢)(𝑠‘𝑦))((𝑥(2nd ‘𝑓)𝑦)‘ℎ)) = (((𝑥(2nd ‘𝑔)𝑦)‘ℎ)(〈(𝑟‘𝑥), (𝑠‘𝑥)〉(comp‘𝑢)(𝑠‘𝑦))(𝑎‘𝑥))} = ⦋(1st
‘𝑓) / 𝑟⦌⦋(1st
‘𝑔) / 𝑠⦌{𝑎 ∈ X𝑥 ∈
𝐵 ((𝑟‘𝑥)𝐽(𝑠‘𝑥)) ∣ ∀𝑥 ∈ 𝐵 ∀𝑦 ∈ 𝐵 ∀ℎ ∈ (𝑥𝐻𝑦)((𝑎‘𝑦)(〈(𝑟‘𝑥), (𝑟‘𝑦)〉 · (𝑠‘𝑦))((𝑥(2nd ‘𝑓)𝑦)‘ℎ)) = (((𝑥(2nd ‘𝑔)𝑦)‘ℎ)(〈(𝑟‘𝑥), (𝑠‘𝑥)〉 · (𝑠‘𝑦))(𝑎‘𝑥))}) |
33 | 2, 2, 32 | mpt2eq123dv 6615 |
. . . 4
⊢ ((𝑡 = 𝐶 ∧ 𝑢 = 𝐷) → (𝑓 ∈ (𝑡 Func 𝑢), 𝑔 ∈ (𝑡 Func 𝑢) ↦ ⦋(1st
‘𝑓) / 𝑟⦌⦋(1st
‘𝑔) / 𝑠⦌{𝑎 ∈ X𝑥 ∈
(Base‘𝑡)((𝑟‘𝑥)(Hom ‘𝑢)(𝑠‘𝑥)) ∣ ∀𝑥 ∈ (Base‘𝑡)∀𝑦 ∈ (Base‘𝑡)∀ℎ ∈ (𝑥(Hom ‘𝑡)𝑦)((𝑎‘𝑦)(〈(𝑟‘𝑥), (𝑟‘𝑦)〉(comp‘𝑢)(𝑠‘𝑦))((𝑥(2nd ‘𝑓)𝑦)‘ℎ)) = (((𝑥(2nd ‘𝑔)𝑦)‘ℎ)(〈(𝑟‘𝑥), (𝑠‘𝑥)〉(comp‘𝑢)(𝑠‘𝑦))(𝑎‘𝑥))}) = (𝑓 ∈ (𝐶 Func 𝐷), 𝑔 ∈ (𝐶 Func 𝐷) ↦ ⦋(1st
‘𝑓) / 𝑟⦌⦋(1st
‘𝑔) / 𝑠⦌{𝑎 ∈ X𝑥 ∈
𝐵 ((𝑟‘𝑥)𝐽(𝑠‘𝑥)) ∣ ∀𝑥 ∈ 𝐵 ∀𝑦 ∈ 𝐵 ∀ℎ ∈ (𝑥𝐻𝑦)((𝑎‘𝑦)(〈(𝑟‘𝑥), (𝑟‘𝑦)〉 · (𝑠‘𝑦))((𝑥(2nd ‘𝑓)𝑦)‘ℎ)) = (((𝑥(2nd ‘𝑔)𝑦)‘ℎ)(〈(𝑟‘𝑥), (𝑠‘𝑥)〉 · (𝑠‘𝑦))(𝑎‘𝑥))})) |
34 | | df-nat 16426 |
. . . 4
⊢ Nat =
(𝑡 ∈ Cat, 𝑢 ∈ Cat ↦ (𝑓 ∈ (𝑡 Func 𝑢), 𝑔 ∈ (𝑡 Func 𝑢) ↦ ⦋(1st
‘𝑓) / 𝑟⦌⦋(1st
‘𝑔) / 𝑠⦌{𝑎 ∈ X𝑥 ∈
(Base‘𝑡)((𝑟‘𝑥)(Hom ‘𝑢)(𝑠‘𝑥)) ∣ ∀𝑥 ∈ (Base‘𝑡)∀𝑦 ∈ (Base‘𝑡)∀ℎ ∈ (𝑥(Hom ‘𝑡)𝑦)((𝑎‘𝑦)(〈(𝑟‘𝑥), (𝑟‘𝑦)〉(comp‘𝑢)(𝑠‘𝑦))((𝑥(2nd ‘𝑓)𝑦)‘ℎ)) = (((𝑥(2nd ‘𝑔)𝑦)‘ℎ)(〈(𝑟‘𝑥), (𝑠‘𝑥)〉(comp‘𝑢)(𝑠‘𝑦))(𝑎‘𝑥))})) |
35 | | ovex 6577 |
. . . . 5
⊢ (𝐶 Func 𝐷) ∈ V |
36 | 35, 35 | mpt2ex 7136 |
. . . 4
⊢ (𝑓 ∈ (𝐶 Func 𝐷), 𝑔 ∈ (𝐶 Func 𝐷) ↦ ⦋(1st
‘𝑓) / 𝑟⦌⦋(1st
‘𝑔) / 𝑠⦌{𝑎 ∈ X𝑥 ∈
𝐵 ((𝑟‘𝑥)𝐽(𝑠‘𝑥)) ∣ ∀𝑥 ∈ 𝐵 ∀𝑦 ∈ 𝐵 ∀ℎ ∈ (𝑥𝐻𝑦)((𝑎‘𝑦)(〈(𝑟‘𝑥), (𝑟‘𝑦)〉 · (𝑠‘𝑦))((𝑥(2nd ‘𝑓)𝑦)‘ℎ)) = (((𝑥(2nd ‘𝑔)𝑦)‘ℎ)(〈(𝑟‘𝑥), (𝑠‘𝑥)〉 · (𝑠‘𝑦))(𝑎‘𝑥))}) ∈ V |
37 | 33, 34, 36 | ovmpt2a 6689 |
. . 3
⊢ ((𝐶 ∈ Cat ∧ 𝐷 ∈ Cat) → (𝐶 Nat 𝐷) = (𝑓 ∈ (𝐶 Func 𝐷), 𝑔 ∈ (𝐶 Func 𝐷) ↦ ⦋(1st
‘𝑓) / 𝑟⦌⦋(1st
‘𝑔) / 𝑠⦌{𝑎 ∈ X𝑥 ∈
𝐵 ((𝑟‘𝑥)𝐽(𝑠‘𝑥)) ∣ ∀𝑥 ∈ 𝐵 ∀𝑦 ∈ 𝐵 ∀ℎ ∈ (𝑥𝐻𝑦)((𝑎‘𝑦)(〈(𝑟‘𝑥), (𝑟‘𝑦)〉 · (𝑠‘𝑦))((𝑥(2nd ‘𝑓)𝑦)‘ℎ)) = (((𝑥(2nd ‘𝑔)𝑦)‘ℎ)(〈(𝑟‘𝑥), (𝑠‘𝑥)〉 · (𝑠‘𝑦))(𝑎‘𝑥))})) |
38 | 34 | mpt2ndm0 6773 |
. . . 4
⊢ (¬
(𝐶 ∈ Cat ∧ 𝐷 ∈ Cat) → (𝐶 Nat 𝐷) = ∅) |
39 | | funcrcl 16346 |
. . . . . . . 8
⊢ (𝑓 ∈ (𝐶 Func 𝐷) → (𝐶 ∈ Cat ∧ 𝐷 ∈ Cat)) |
40 | 39 | con3i 149 |
. . . . . . 7
⊢ (¬
(𝐶 ∈ Cat ∧ 𝐷 ∈ Cat) → ¬ 𝑓 ∈ (𝐶 Func 𝐷)) |
41 | 40 | eq0rdv 3931 |
. . . . . 6
⊢ (¬
(𝐶 ∈ Cat ∧ 𝐷 ∈ Cat) → (𝐶 Func 𝐷) = ∅) |
42 | | mpt2eq12 6613 |
. . . . . 6
⊢ (((𝐶 Func 𝐷) = ∅ ∧ (𝐶 Func 𝐷) = ∅) → (𝑓 ∈ (𝐶 Func 𝐷), 𝑔 ∈ (𝐶 Func 𝐷) ↦ ⦋(1st
‘𝑓) / 𝑟⦌⦋(1st
‘𝑔) / 𝑠⦌{𝑎 ∈ X𝑥 ∈
𝐵 ((𝑟‘𝑥)𝐽(𝑠‘𝑥)) ∣ ∀𝑥 ∈ 𝐵 ∀𝑦 ∈ 𝐵 ∀ℎ ∈ (𝑥𝐻𝑦)((𝑎‘𝑦)(〈(𝑟‘𝑥), (𝑟‘𝑦)〉 · (𝑠‘𝑦))((𝑥(2nd ‘𝑓)𝑦)‘ℎ)) = (((𝑥(2nd ‘𝑔)𝑦)‘ℎ)(〈(𝑟‘𝑥), (𝑠‘𝑥)〉 · (𝑠‘𝑦))(𝑎‘𝑥))}) = (𝑓 ∈ ∅, 𝑔 ∈ ∅ ↦
⦋(1st ‘𝑓) / 𝑟⦌⦋(1st
‘𝑔) / 𝑠⦌{𝑎 ∈ X𝑥 ∈
𝐵 ((𝑟‘𝑥)𝐽(𝑠‘𝑥)) ∣ ∀𝑥 ∈ 𝐵 ∀𝑦 ∈ 𝐵 ∀ℎ ∈ (𝑥𝐻𝑦)((𝑎‘𝑦)(〈(𝑟‘𝑥), (𝑟‘𝑦)〉 · (𝑠‘𝑦))((𝑥(2nd ‘𝑓)𝑦)‘ℎ)) = (((𝑥(2nd ‘𝑔)𝑦)‘ℎ)(〈(𝑟‘𝑥), (𝑠‘𝑥)〉 · (𝑠‘𝑦))(𝑎‘𝑥))})) |
43 | 41, 41, 42 | syl2anc 691 |
. . . . 5
⊢ (¬
(𝐶 ∈ Cat ∧ 𝐷 ∈ Cat) → (𝑓 ∈ (𝐶 Func 𝐷), 𝑔 ∈ (𝐶 Func 𝐷) ↦ ⦋(1st
‘𝑓) / 𝑟⦌⦋(1st
‘𝑔) / 𝑠⦌{𝑎 ∈ X𝑥 ∈
𝐵 ((𝑟‘𝑥)𝐽(𝑠‘𝑥)) ∣ ∀𝑥 ∈ 𝐵 ∀𝑦 ∈ 𝐵 ∀ℎ ∈ (𝑥𝐻𝑦)((𝑎‘𝑦)(〈(𝑟‘𝑥), (𝑟‘𝑦)〉 · (𝑠‘𝑦))((𝑥(2nd ‘𝑓)𝑦)‘ℎ)) = (((𝑥(2nd ‘𝑔)𝑦)‘ℎ)(〈(𝑟‘𝑥), (𝑠‘𝑥)〉 · (𝑠‘𝑦))(𝑎‘𝑥))}) = (𝑓 ∈ ∅, 𝑔 ∈ ∅ ↦
⦋(1st ‘𝑓) / 𝑟⦌⦋(1st
‘𝑔) / 𝑠⦌{𝑎 ∈ X𝑥 ∈
𝐵 ((𝑟‘𝑥)𝐽(𝑠‘𝑥)) ∣ ∀𝑥 ∈ 𝐵 ∀𝑦 ∈ 𝐵 ∀ℎ ∈ (𝑥𝐻𝑦)((𝑎‘𝑦)(〈(𝑟‘𝑥), (𝑟‘𝑦)〉 · (𝑠‘𝑦))((𝑥(2nd ‘𝑓)𝑦)‘ℎ)) = (((𝑥(2nd ‘𝑔)𝑦)‘ℎ)(〈(𝑟‘𝑥), (𝑠‘𝑥)〉 · (𝑠‘𝑦))(𝑎‘𝑥))})) |
44 | | mpt20 6623 |
. . . . 5
⊢ (𝑓 ∈ ∅, 𝑔 ∈ ∅ ↦
⦋(1st ‘𝑓) / 𝑟⦌⦋(1st
‘𝑔) / 𝑠⦌{𝑎 ∈ X𝑥 ∈
𝐵 ((𝑟‘𝑥)𝐽(𝑠‘𝑥)) ∣ ∀𝑥 ∈ 𝐵 ∀𝑦 ∈ 𝐵 ∀ℎ ∈ (𝑥𝐻𝑦)((𝑎‘𝑦)(〈(𝑟‘𝑥), (𝑟‘𝑦)〉 · (𝑠‘𝑦))((𝑥(2nd ‘𝑓)𝑦)‘ℎ)) = (((𝑥(2nd ‘𝑔)𝑦)‘ℎ)(〈(𝑟‘𝑥), (𝑠‘𝑥)〉 · (𝑠‘𝑦))(𝑎‘𝑥))}) = ∅ |
45 | 43, 44 | syl6eq 2660 |
. . . 4
⊢ (¬
(𝐶 ∈ Cat ∧ 𝐷 ∈ Cat) → (𝑓 ∈ (𝐶 Func 𝐷), 𝑔 ∈ (𝐶 Func 𝐷) ↦ ⦋(1st
‘𝑓) / 𝑟⦌⦋(1st
‘𝑔) / 𝑠⦌{𝑎 ∈ X𝑥 ∈
𝐵 ((𝑟‘𝑥)𝐽(𝑠‘𝑥)) ∣ ∀𝑥 ∈ 𝐵 ∀𝑦 ∈ 𝐵 ∀ℎ ∈ (𝑥𝐻𝑦)((𝑎‘𝑦)(〈(𝑟‘𝑥), (𝑟‘𝑦)〉 · (𝑠‘𝑦))((𝑥(2nd ‘𝑓)𝑦)‘ℎ)) = (((𝑥(2nd ‘𝑔)𝑦)‘ℎ)(〈(𝑟‘𝑥), (𝑠‘𝑥)〉 · (𝑠‘𝑦))(𝑎‘𝑥))}) = ∅) |
46 | 38, 45 | eqtr4d 2647 |
. . 3
⊢ (¬
(𝐶 ∈ Cat ∧ 𝐷 ∈ Cat) → (𝐶 Nat 𝐷) = (𝑓 ∈ (𝐶 Func 𝐷), 𝑔 ∈ (𝐶 Func 𝐷) ↦ ⦋(1st
‘𝑓) / 𝑟⦌⦋(1st
‘𝑔) / 𝑠⦌{𝑎 ∈ X𝑥 ∈
𝐵 ((𝑟‘𝑥)𝐽(𝑠‘𝑥)) ∣ ∀𝑥 ∈ 𝐵 ∀𝑦 ∈ 𝐵 ∀ℎ ∈ (𝑥𝐻𝑦)((𝑎‘𝑦)(〈(𝑟‘𝑥), (𝑟‘𝑦)〉 · (𝑠‘𝑦))((𝑥(2nd ‘𝑓)𝑦)‘ℎ)) = (((𝑥(2nd ‘𝑔)𝑦)‘ℎ)(〈(𝑟‘𝑥), (𝑠‘𝑥)〉 · (𝑠‘𝑦))(𝑎‘𝑥))})) |
47 | 37, 46 | pm2.61i 175 |
. 2
⊢ (𝐶 Nat 𝐷) = (𝑓 ∈ (𝐶 Func 𝐷), 𝑔 ∈ (𝐶 Func 𝐷) ↦ ⦋(1st
‘𝑓) / 𝑟⦌⦋(1st
‘𝑔) / 𝑠⦌{𝑎 ∈ X𝑥 ∈
𝐵 ((𝑟‘𝑥)𝐽(𝑠‘𝑥)) ∣ ∀𝑥 ∈ 𝐵 ∀𝑦 ∈ 𝐵 ∀ℎ ∈ (𝑥𝐻𝑦)((𝑎‘𝑦)(〈(𝑟‘𝑥), (𝑟‘𝑦)〉 · (𝑠‘𝑦))((𝑥(2nd ‘𝑓)𝑦)‘ℎ)) = (((𝑥(2nd ‘𝑔)𝑦)‘ℎ)(〈(𝑟‘𝑥), (𝑠‘𝑥)〉 · (𝑠‘𝑦))(𝑎‘𝑥))}) |
48 | 1, 47 | eqtri 2632 |
1
⊢ 𝑁 = (𝑓 ∈ (𝐶 Func 𝐷), 𝑔 ∈ (𝐶 Func 𝐷) ↦ ⦋(1st
‘𝑓) / 𝑟⦌⦋(1st
‘𝑔) / 𝑠⦌{𝑎 ∈ X𝑥 ∈
𝐵 ((𝑟‘𝑥)𝐽(𝑠‘𝑥)) ∣ ∀𝑥 ∈ 𝐵 ∀𝑦 ∈ 𝐵 ∀ℎ ∈ (𝑥𝐻𝑦)((𝑎‘𝑦)(〈(𝑟‘𝑥), (𝑟‘𝑦)〉 · (𝑠‘𝑦))((𝑥(2nd ‘𝑓)𝑦)‘ℎ)) = (((𝑥(2nd ‘𝑔)𝑦)‘ℎ)(〈(𝑟‘𝑥), (𝑠‘𝑥)〉 · (𝑠‘𝑦))(𝑎‘𝑥))}) |