Step | Hyp | Ref
| Expression |
1 | | natfval.1 |
. . . . . 6
⊢ 𝑁 = (𝐶 Nat 𝐷) |
2 | | natfval.b |
. . . . . 6
⊢ 𝐵 = (Base‘𝐶) |
3 | | natfval.h |
. . . . . 6
⊢ 𝐻 = (Hom ‘𝐶) |
4 | | natfval.j |
. . . . . 6
⊢ 𝐽 = (Hom ‘𝐷) |
5 | | natfval.o |
. . . . . 6
⊢ · =
(comp‘𝐷) |
6 | 1, 2, 3, 4, 5 | natfval 16429 |
. . . . 5
⊢ 𝑁 = (𝑓 ∈ (𝐶 Func 𝐷), 𝑔 ∈ (𝐶 Func 𝐷) ↦ ⦋(1st
‘𝑓) / 𝑟⦌⦋(1st
‘𝑔) / 𝑠⦌{𝑎 ∈ X𝑥 ∈
𝐵 ((𝑟‘𝑥)𝐽(𝑠‘𝑥)) ∣ ∀𝑥 ∈ 𝐵 ∀𝑦 ∈ 𝐵 ∀ℎ ∈ (𝑥𝐻𝑦)((𝑎‘𝑦)(〈(𝑟‘𝑥), (𝑟‘𝑦)〉 · (𝑠‘𝑦))((𝑥(2nd ‘𝑓)𝑦)‘ℎ)) = (((𝑥(2nd ‘𝑔)𝑦)‘ℎ)(〈(𝑟‘𝑥), (𝑠‘𝑥)〉 · (𝑠‘𝑦))(𝑎‘𝑥))}) |
7 | 6 | a1i 11 |
. . . 4
⊢ (𝜑 → 𝑁 = (𝑓 ∈ (𝐶 Func 𝐷), 𝑔 ∈ (𝐶 Func 𝐷) ↦ ⦋(1st
‘𝑓) / 𝑟⦌⦋(1st
‘𝑔) / 𝑠⦌{𝑎 ∈ X𝑥 ∈
𝐵 ((𝑟‘𝑥)𝐽(𝑠‘𝑥)) ∣ ∀𝑥 ∈ 𝐵 ∀𝑦 ∈ 𝐵 ∀ℎ ∈ (𝑥𝐻𝑦)((𝑎‘𝑦)(〈(𝑟‘𝑥), (𝑟‘𝑦)〉 · (𝑠‘𝑦))((𝑥(2nd ‘𝑓)𝑦)‘ℎ)) = (((𝑥(2nd ‘𝑔)𝑦)‘ℎ)(〈(𝑟‘𝑥), (𝑠‘𝑥)〉 · (𝑠‘𝑦))(𝑎‘𝑥))})) |
8 | | fvex 6113 |
. . . . . 6
⊢
(1st ‘𝑓) ∈ V |
9 | 8 | a1i 11 |
. . . . 5
⊢ ((𝜑 ∧ (𝑓 = 〈𝐹, 𝐺〉 ∧ 𝑔 = 〈𝐾, 𝐿〉)) → (1st ‘𝑓) ∈ V) |
10 | | simprl 790 |
. . . . . . 7
⊢ ((𝜑 ∧ (𝑓 = 〈𝐹, 𝐺〉 ∧ 𝑔 = 〈𝐾, 𝐿〉)) → 𝑓 = 〈𝐹, 𝐺〉) |
11 | 10 | fveq2d 6107 |
. . . . . 6
⊢ ((𝜑 ∧ (𝑓 = 〈𝐹, 𝐺〉 ∧ 𝑔 = 〈𝐾, 𝐿〉)) → (1st ‘𝑓) = (1st
‘〈𝐹, 𝐺〉)) |
12 | | relfunc 16345 |
. . . . . . . . 9
⊢ Rel
(𝐶 Func 𝐷) |
13 | | isnat.f |
. . . . . . . . 9
⊢ (𝜑 → 𝐹(𝐶 Func 𝐷)𝐺) |
14 | | brrelex12 5079 |
. . . . . . . . 9
⊢ ((Rel
(𝐶 Func 𝐷) ∧ 𝐹(𝐶 Func 𝐷)𝐺) → (𝐹 ∈ V ∧ 𝐺 ∈ V)) |
15 | 12, 13, 14 | sylancr 694 |
. . . . . . . 8
⊢ (𝜑 → (𝐹 ∈ V ∧ 𝐺 ∈ V)) |
16 | | op1stg 7071 |
. . . . . . . 8
⊢ ((𝐹 ∈ V ∧ 𝐺 ∈ V) →
(1st ‘〈𝐹, 𝐺〉) = 𝐹) |
17 | 15, 16 | syl 17 |
. . . . . . 7
⊢ (𝜑 → (1st
‘〈𝐹, 𝐺〉) = 𝐹) |
18 | 17 | adantr 480 |
. . . . . 6
⊢ ((𝜑 ∧ (𝑓 = 〈𝐹, 𝐺〉 ∧ 𝑔 = 〈𝐾, 𝐿〉)) → (1st
‘〈𝐹, 𝐺〉) = 𝐹) |
19 | 11, 18 | eqtrd 2644 |
. . . . 5
⊢ ((𝜑 ∧ (𝑓 = 〈𝐹, 𝐺〉 ∧ 𝑔 = 〈𝐾, 𝐿〉)) → (1st ‘𝑓) = 𝐹) |
20 | | fvex 6113 |
. . . . . . 7
⊢
(1st ‘𝑔) ∈ V |
21 | 20 | a1i 11 |
. . . . . 6
⊢ (((𝜑 ∧ (𝑓 = 〈𝐹, 𝐺〉 ∧ 𝑔 = 〈𝐾, 𝐿〉)) ∧ 𝑟 = 𝐹) → (1st ‘𝑔) ∈ V) |
22 | | simplrr 797 |
. . . . . . . 8
⊢ (((𝜑 ∧ (𝑓 = 〈𝐹, 𝐺〉 ∧ 𝑔 = 〈𝐾, 𝐿〉)) ∧ 𝑟 = 𝐹) → 𝑔 = 〈𝐾, 𝐿〉) |
23 | 22 | fveq2d 6107 |
. . . . . . 7
⊢ (((𝜑 ∧ (𝑓 = 〈𝐹, 𝐺〉 ∧ 𝑔 = 〈𝐾, 𝐿〉)) ∧ 𝑟 = 𝐹) → (1st ‘𝑔) = (1st
‘〈𝐾, 𝐿〉)) |
24 | | isnat.g |
. . . . . . . . . 10
⊢ (𝜑 → 𝐾(𝐶 Func 𝐷)𝐿) |
25 | | brrelex12 5079 |
. . . . . . . . . 10
⊢ ((Rel
(𝐶 Func 𝐷) ∧ 𝐾(𝐶 Func 𝐷)𝐿) → (𝐾 ∈ V ∧ 𝐿 ∈ V)) |
26 | 12, 24, 25 | sylancr 694 |
. . . . . . . . 9
⊢ (𝜑 → (𝐾 ∈ V ∧ 𝐿 ∈ V)) |
27 | | op1stg 7071 |
. . . . . . . . 9
⊢ ((𝐾 ∈ V ∧ 𝐿 ∈ V) →
(1st ‘〈𝐾, 𝐿〉) = 𝐾) |
28 | 26, 27 | syl 17 |
. . . . . . . 8
⊢ (𝜑 → (1st
‘〈𝐾, 𝐿〉) = 𝐾) |
29 | 28 | ad2antrr 758 |
. . . . . . 7
⊢ (((𝜑 ∧ (𝑓 = 〈𝐹, 𝐺〉 ∧ 𝑔 = 〈𝐾, 𝐿〉)) ∧ 𝑟 = 𝐹) → (1st ‘〈𝐾, 𝐿〉) = 𝐾) |
30 | 23, 29 | eqtrd 2644 |
. . . . . 6
⊢ (((𝜑 ∧ (𝑓 = 〈𝐹, 𝐺〉 ∧ 𝑔 = 〈𝐾, 𝐿〉)) ∧ 𝑟 = 𝐹) → (1st ‘𝑔) = 𝐾) |
31 | | simplr 788 |
. . . . . . . . . 10
⊢ ((((𝜑 ∧ (𝑓 = 〈𝐹, 𝐺〉 ∧ 𝑔 = 〈𝐾, 𝐿〉)) ∧ 𝑟 = 𝐹) ∧ 𝑠 = 𝐾) → 𝑟 = 𝐹) |
32 | 31 | fveq1d 6105 |
. . . . . . . . 9
⊢ ((((𝜑 ∧ (𝑓 = 〈𝐹, 𝐺〉 ∧ 𝑔 = 〈𝐾, 𝐿〉)) ∧ 𝑟 = 𝐹) ∧ 𝑠 = 𝐾) → (𝑟‘𝑥) = (𝐹‘𝑥)) |
33 | | simpr 476 |
. . . . . . . . . 10
⊢ ((((𝜑 ∧ (𝑓 = 〈𝐹, 𝐺〉 ∧ 𝑔 = 〈𝐾, 𝐿〉)) ∧ 𝑟 = 𝐹) ∧ 𝑠 = 𝐾) → 𝑠 = 𝐾) |
34 | 33 | fveq1d 6105 |
. . . . . . . . 9
⊢ ((((𝜑 ∧ (𝑓 = 〈𝐹, 𝐺〉 ∧ 𝑔 = 〈𝐾, 𝐿〉)) ∧ 𝑟 = 𝐹) ∧ 𝑠 = 𝐾) → (𝑠‘𝑥) = (𝐾‘𝑥)) |
35 | 32, 34 | oveq12d 6567 |
. . . . . . . 8
⊢ ((((𝜑 ∧ (𝑓 = 〈𝐹, 𝐺〉 ∧ 𝑔 = 〈𝐾, 𝐿〉)) ∧ 𝑟 = 𝐹) ∧ 𝑠 = 𝐾) → ((𝑟‘𝑥)𝐽(𝑠‘𝑥)) = ((𝐹‘𝑥)𝐽(𝐾‘𝑥))) |
36 | 35 | ixpeq2dv 7810 |
. . . . . . 7
⊢ ((((𝜑 ∧ (𝑓 = 〈𝐹, 𝐺〉 ∧ 𝑔 = 〈𝐾, 𝐿〉)) ∧ 𝑟 = 𝐹) ∧ 𝑠 = 𝐾) → X𝑥 ∈ 𝐵 ((𝑟‘𝑥)𝐽(𝑠‘𝑥)) = X𝑥 ∈ 𝐵 ((𝐹‘𝑥)𝐽(𝐾‘𝑥))) |
37 | 31 | fveq1d 6105 |
. . . . . . . . . . . . 13
⊢ ((((𝜑 ∧ (𝑓 = 〈𝐹, 𝐺〉 ∧ 𝑔 = 〈𝐾, 𝐿〉)) ∧ 𝑟 = 𝐹) ∧ 𝑠 = 𝐾) → (𝑟‘𝑦) = (𝐹‘𝑦)) |
38 | 32, 37 | opeq12d 4348 |
. . . . . . . . . . . 12
⊢ ((((𝜑 ∧ (𝑓 = 〈𝐹, 𝐺〉 ∧ 𝑔 = 〈𝐾, 𝐿〉)) ∧ 𝑟 = 𝐹) ∧ 𝑠 = 𝐾) → 〈(𝑟‘𝑥), (𝑟‘𝑦)〉 = 〈(𝐹‘𝑥), (𝐹‘𝑦)〉) |
39 | 33 | fveq1d 6105 |
. . . . . . . . . . . 12
⊢ ((((𝜑 ∧ (𝑓 = 〈𝐹, 𝐺〉 ∧ 𝑔 = 〈𝐾, 𝐿〉)) ∧ 𝑟 = 𝐹) ∧ 𝑠 = 𝐾) → (𝑠‘𝑦) = (𝐾‘𝑦)) |
40 | 38, 39 | oveq12d 6567 |
. . . . . . . . . . 11
⊢ ((((𝜑 ∧ (𝑓 = 〈𝐹, 𝐺〉 ∧ 𝑔 = 〈𝐾, 𝐿〉)) ∧ 𝑟 = 𝐹) ∧ 𝑠 = 𝐾) → (〈(𝑟‘𝑥), (𝑟‘𝑦)〉 · (𝑠‘𝑦)) = (〈(𝐹‘𝑥), (𝐹‘𝑦)〉 · (𝐾‘𝑦))) |
41 | | eqidd 2611 |
. . . . . . . . . . 11
⊢ ((((𝜑 ∧ (𝑓 = 〈𝐹, 𝐺〉 ∧ 𝑔 = 〈𝐾, 𝐿〉)) ∧ 𝑟 = 𝐹) ∧ 𝑠 = 𝐾) → (𝑎‘𝑦) = (𝑎‘𝑦)) |
42 | 10 | ad2antrr 758 |
. . . . . . . . . . . . . . 15
⊢ ((((𝜑 ∧ (𝑓 = 〈𝐹, 𝐺〉 ∧ 𝑔 = 〈𝐾, 𝐿〉)) ∧ 𝑟 = 𝐹) ∧ 𝑠 = 𝐾) → 𝑓 = 〈𝐹, 𝐺〉) |
43 | 42 | fveq2d 6107 |
. . . . . . . . . . . . . 14
⊢ ((((𝜑 ∧ (𝑓 = 〈𝐹, 𝐺〉 ∧ 𝑔 = 〈𝐾, 𝐿〉)) ∧ 𝑟 = 𝐹) ∧ 𝑠 = 𝐾) → (2nd ‘𝑓) = (2nd
‘〈𝐹, 𝐺〉)) |
44 | | op2ndg 7072 |
. . . . . . . . . . . . . . . 16
⊢ ((𝐹 ∈ V ∧ 𝐺 ∈ V) →
(2nd ‘〈𝐹, 𝐺〉) = 𝐺) |
45 | 15, 44 | syl 17 |
. . . . . . . . . . . . . . 15
⊢ (𝜑 → (2nd
‘〈𝐹, 𝐺〉) = 𝐺) |
46 | 45 | ad3antrrr 762 |
. . . . . . . . . . . . . 14
⊢ ((((𝜑 ∧ (𝑓 = 〈𝐹, 𝐺〉 ∧ 𝑔 = 〈𝐾, 𝐿〉)) ∧ 𝑟 = 𝐹) ∧ 𝑠 = 𝐾) → (2nd ‘〈𝐹, 𝐺〉) = 𝐺) |
47 | 43, 46 | eqtrd 2644 |
. . . . . . . . . . . . 13
⊢ ((((𝜑 ∧ (𝑓 = 〈𝐹, 𝐺〉 ∧ 𝑔 = 〈𝐾, 𝐿〉)) ∧ 𝑟 = 𝐹) ∧ 𝑠 = 𝐾) → (2nd ‘𝑓) = 𝐺) |
48 | 47 | oveqd 6566 |
. . . . . . . . . . . 12
⊢ ((((𝜑 ∧ (𝑓 = 〈𝐹, 𝐺〉 ∧ 𝑔 = 〈𝐾, 𝐿〉)) ∧ 𝑟 = 𝐹) ∧ 𝑠 = 𝐾) → (𝑥(2nd ‘𝑓)𝑦) = (𝑥𝐺𝑦)) |
49 | 48 | fveq1d 6105 |
. . . . . . . . . . 11
⊢ ((((𝜑 ∧ (𝑓 = 〈𝐹, 𝐺〉 ∧ 𝑔 = 〈𝐾, 𝐿〉)) ∧ 𝑟 = 𝐹) ∧ 𝑠 = 𝐾) → ((𝑥(2nd ‘𝑓)𝑦)‘ℎ) = ((𝑥𝐺𝑦)‘ℎ)) |
50 | 40, 41, 49 | oveq123d 6570 |
. . . . . . . . . 10
⊢ ((((𝜑 ∧ (𝑓 = 〈𝐹, 𝐺〉 ∧ 𝑔 = 〈𝐾, 𝐿〉)) ∧ 𝑟 = 𝐹) ∧ 𝑠 = 𝐾) → ((𝑎‘𝑦)(〈(𝑟‘𝑥), (𝑟‘𝑦)〉 · (𝑠‘𝑦))((𝑥(2nd ‘𝑓)𝑦)‘ℎ)) = ((𝑎‘𝑦)(〈(𝐹‘𝑥), (𝐹‘𝑦)〉 · (𝐾‘𝑦))((𝑥𝐺𝑦)‘ℎ))) |
51 | 32, 34 | opeq12d 4348 |
. . . . . . . . . . . 12
⊢ ((((𝜑 ∧ (𝑓 = 〈𝐹, 𝐺〉 ∧ 𝑔 = 〈𝐾, 𝐿〉)) ∧ 𝑟 = 𝐹) ∧ 𝑠 = 𝐾) → 〈(𝑟‘𝑥), (𝑠‘𝑥)〉 = 〈(𝐹‘𝑥), (𝐾‘𝑥)〉) |
52 | 51, 39 | oveq12d 6567 |
. . . . . . . . . . 11
⊢ ((((𝜑 ∧ (𝑓 = 〈𝐹, 𝐺〉 ∧ 𝑔 = 〈𝐾, 𝐿〉)) ∧ 𝑟 = 𝐹) ∧ 𝑠 = 𝐾) → (〈(𝑟‘𝑥), (𝑠‘𝑥)〉 · (𝑠‘𝑦)) = (〈(𝐹‘𝑥), (𝐾‘𝑥)〉 · (𝐾‘𝑦))) |
53 | 22 | adantr 480 |
. . . . . . . . . . . . . . 15
⊢ ((((𝜑 ∧ (𝑓 = 〈𝐹, 𝐺〉 ∧ 𝑔 = 〈𝐾, 𝐿〉)) ∧ 𝑟 = 𝐹) ∧ 𝑠 = 𝐾) → 𝑔 = 〈𝐾, 𝐿〉) |
54 | 53 | fveq2d 6107 |
. . . . . . . . . . . . . 14
⊢ ((((𝜑 ∧ (𝑓 = 〈𝐹, 𝐺〉 ∧ 𝑔 = 〈𝐾, 𝐿〉)) ∧ 𝑟 = 𝐹) ∧ 𝑠 = 𝐾) → (2nd ‘𝑔) = (2nd
‘〈𝐾, 𝐿〉)) |
55 | | op2ndg 7072 |
. . . . . . . . . . . . . . . 16
⊢ ((𝐾 ∈ V ∧ 𝐿 ∈ V) →
(2nd ‘〈𝐾, 𝐿〉) = 𝐿) |
56 | 26, 55 | syl 17 |
. . . . . . . . . . . . . . 15
⊢ (𝜑 → (2nd
‘〈𝐾, 𝐿〉) = 𝐿) |
57 | 56 | ad3antrrr 762 |
. . . . . . . . . . . . . 14
⊢ ((((𝜑 ∧ (𝑓 = 〈𝐹, 𝐺〉 ∧ 𝑔 = 〈𝐾, 𝐿〉)) ∧ 𝑟 = 𝐹) ∧ 𝑠 = 𝐾) → (2nd ‘〈𝐾, 𝐿〉) = 𝐿) |
58 | 54, 57 | eqtrd 2644 |
. . . . . . . . . . . . 13
⊢ ((((𝜑 ∧ (𝑓 = 〈𝐹, 𝐺〉 ∧ 𝑔 = 〈𝐾, 𝐿〉)) ∧ 𝑟 = 𝐹) ∧ 𝑠 = 𝐾) → (2nd ‘𝑔) = 𝐿) |
59 | 58 | oveqd 6566 |
. . . . . . . . . . . 12
⊢ ((((𝜑 ∧ (𝑓 = 〈𝐹, 𝐺〉 ∧ 𝑔 = 〈𝐾, 𝐿〉)) ∧ 𝑟 = 𝐹) ∧ 𝑠 = 𝐾) → (𝑥(2nd ‘𝑔)𝑦) = (𝑥𝐿𝑦)) |
60 | 59 | fveq1d 6105 |
. . . . . . . . . . 11
⊢ ((((𝜑 ∧ (𝑓 = 〈𝐹, 𝐺〉 ∧ 𝑔 = 〈𝐾, 𝐿〉)) ∧ 𝑟 = 𝐹) ∧ 𝑠 = 𝐾) → ((𝑥(2nd ‘𝑔)𝑦)‘ℎ) = ((𝑥𝐿𝑦)‘ℎ)) |
61 | | eqidd 2611 |
. . . . . . . . . . 11
⊢ ((((𝜑 ∧ (𝑓 = 〈𝐹, 𝐺〉 ∧ 𝑔 = 〈𝐾, 𝐿〉)) ∧ 𝑟 = 𝐹) ∧ 𝑠 = 𝐾) → (𝑎‘𝑥) = (𝑎‘𝑥)) |
62 | 52, 60, 61 | oveq123d 6570 |
. . . . . . . . . 10
⊢ ((((𝜑 ∧ (𝑓 = 〈𝐹, 𝐺〉 ∧ 𝑔 = 〈𝐾, 𝐿〉)) ∧ 𝑟 = 𝐹) ∧ 𝑠 = 𝐾) → (((𝑥(2nd ‘𝑔)𝑦)‘ℎ)(〈(𝑟‘𝑥), (𝑠‘𝑥)〉 · (𝑠‘𝑦))(𝑎‘𝑥)) = (((𝑥𝐿𝑦)‘ℎ)(〈(𝐹‘𝑥), (𝐾‘𝑥)〉 · (𝐾‘𝑦))(𝑎‘𝑥))) |
63 | 50, 62 | eqeq12d 2625 |
. . . . . . . . 9
⊢ ((((𝜑 ∧ (𝑓 = 〈𝐹, 𝐺〉 ∧ 𝑔 = 〈𝐾, 𝐿〉)) ∧ 𝑟 = 𝐹) ∧ 𝑠 = 𝐾) → (((𝑎‘𝑦)(〈(𝑟‘𝑥), (𝑟‘𝑦)〉 · (𝑠‘𝑦))((𝑥(2nd ‘𝑓)𝑦)‘ℎ)) = (((𝑥(2nd ‘𝑔)𝑦)‘ℎ)(〈(𝑟‘𝑥), (𝑠‘𝑥)〉 · (𝑠‘𝑦))(𝑎‘𝑥)) ↔ ((𝑎‘𝑦)(〈(𝐹‘𝑥), (𝐹‘𝑦)〉 · (𝐾‘𝑦))((𝑥𝐺𝑦)‘ℎ)) = (((𝑥𝐿𝑦)‘ℎ)(〈(𝐹‘𝑥), (𝐾‘𝑥)〉 · (𝐾‘𝑦))(𝑎‘𝑥)))) |
64 | 63 | ralbidv 2969 |
. . . . . . . 8
⊢ ((((𝜑 ∧ (𝑓 = 〈𝐹, 𝐺〉 ∧ 𝑔 = 〈𝐾, 𝐿〉)) ∧ 𝑟 = 𝐹) ∧ 𝑠 = 𝐾) → (∀ℎ ∈ (𝑥𝐻𝑦)((𝑎‘𝑦)(〈(𝑟‘𝑥), (𝑟‘𝑦)〉 · (𝑠‘𝑦))((𝑥(2nd ‘𝑓)𝑦)‘ℎ)) = (((𝑥(2nd ‘𝑔)𝑦)‘ℎ)(〈(𝑟‘𝑥), (𝑠‘𝑥)〉 · (𝑠‘𝑦))(𝑎‘𝑥)) ↔ ∀ℎ ∈ (𝑥𝐻𝑦)((𝑎‘𝑦)(〈(𝐹‘𝑥), (𝐹‘𝑦)〉 · (𝐾‘𝑦))((𝑥𝐺𝑦)‘ℎ)) = (((𝑥𝐿𝑦)‘ℎ)(〈(𝐹‘𝑥), (𝐾‘𝑥)〉 · (𝐾‘𝑦))(𝑎‘𝑥)))) |
65 | 64 | 2ralbidv 2972 |
. . . . . . 7
⊢ ((((𝜑 ∧ (𝑓 = 〈𝐹, 𝐺〉 ∧ 𝑔 = 〈𝐾, 𝐿〉)) ∧ 𝑟 = 𝐹) ∧ 𝑠 = 𝐾) → (∀𝑥 ∈ 𝐵 ∀𝑦 ∈ 𝐵 ∀ℎ ∈ (𝑥𝐻𝑦)((𝑎‘𝑦)(〈(𝑟‘𝑥), (𝑟‘𝑦)〉 · (𝑠‘𝑦))((𝑥(2nd ‘𝑓)𝑦)‘ℎ)) = (((𝑥(2nd ‘𝑔)𝑦)‘ℎ)(〈(𝑟‘𝑥), (𝑠‘𝑥)〉 · (𝑠‘𝑦))(𝑎‘𝑥)) ↔ ∀𝑥 ∈ 𝐵 ∀𝑦 ∈ 𝐵 ∀ℎ ∈ (𝑥𝐻𝑦)((𝑎‘𝑦)(〈(𝐹‘𝑥), (𝐹‘𝑦)〉 · (𝐾‘𝑦))((𝑥𝐺𝑦)‘ℎ)) = (((𝑥𝐿𝑦)‘ℎ)(〈(𝐹‘𝑥), (𝐾‘𝑥)〉 · (𝐾‘𝑦))(𝑎‘𝑥)))) |
66 | 36, 65 | rabeqbidv 3168 |
. . . . . 6
⊢ ((((𝜑 ∧ (𝑓 = 〈𝐹, 𝐺〉 ∧ 𝑔 = 〈𝐾, 𝐿〉)) ∧ 𝑟 = 𝐹) ∧ 𝑠 = 𝐾) → {𝑎 ∈ X𝑥 ∈ 𝐵 ((𝑟‘𝑥)𝐽(𝑠‘𝑥)) ∣ ∀𝑥 ∈ 𝐵 ∀𝑦 ∈ 𝐵 ∀ℎ ∈ (𝑥𝐻𝑦)((𝑎‘𝑦)(〈(𝑟‘𝑥), (𝑟‘𝑦)〉 · (𝑠‘𝑦))((𝑥(2nd ‘𝑓)𝑦)‘ℎ)) = (((𝑥(2nd ‘𝑔)𝑦)‘ℎ)(〈(𝑟‘𝑥), (𝑠‘𝑥)〉 · (𝑠‘𝑦))(𝑎‘𝑥))} = {𝑎 ∈ X𝑥 ∈ 𝐵 ((𝐹‘𝑥)𝐽(𝐾‘𝑥)) ∣ ∀𝑥 ∈ 𝐵 ∀𝑦 ∈ 𝐵 ∀ℎ ∈ (𝑥𝐻𝑦)((𝑎‘𝑦)(〈(𝐹‘𝑥), (𝐹‘𝑦)〉 · (𝐾‘𝑦))((𝑥𝐺𝑦)‘ℎ)) = (((𝑥𝐿𝑦)‘ℎ)(〈(𝐹‘𝑥), (𝐾‘𝑥)〉 · (𝐾‘𝑦))(𝑎‘𝑥))}) |
67 | 21, 30, 66 | csbied2 3527 |
. . . . 5
⊢ (((𝜑 ∧ (𝑓 = 〈𝐹, 𝐺〉 ∧ 𝑔 = 〈𝐾, 𝐿〉)) ∧ 𝑟 = 𝐹) → ⦋(1st
‘𝑔) / 𝑠⦌{𝑎 ∈ X𝑥 ∈
𝐵 ((𝑟‘𝑥)𝐽(𝑠‘𝑥)) ∣ ∀𝑥 ∈ 𝐵 ∀𝑦 ∈ 𝐵 ∀ℎ ∈ (𝑥𝐻𝑦)((𝑎‘𝑦)(〈(𝑟‘𝑥), (𝑟‘𝑦)〉 · (𝑠‘𝑦))((𝑥(2nd ‘𝑓)𝑦)‘ℎ)) = (((𝑥(2nd ‘𝑔)𝑦)‘ℎ)(〈(𝑟‘𝑥), (𝑠‘𝑥)〉 · (𝑠‘𝑦))(𝑎‘𝑥))} = {𝑎 ∈ X𝑥 ∈ 𝐵 ((𝐹‘𝑥)𝐽(𝐾‘𝑥)) ∣ ∀𝑥 ∈ 𝐵 ∀𝑦 ∈ 𝐵 ∀ℎ ∈ (𝑥𝐻𝑦)((𝑎‘𝑦)(〈(𝐹‘𝑥), (𝐹‘𝑦)〉 · (𝐾‘𝑦))((𝑥𝐺𝑦)‘ℎ)) = (((𝑥𝐿𝑦)‘ℎ)(〈(𝐹‘𝑥), (𝐾‘𝑥)〉 · (𝐾‘𝑦))(𝑎‘𝑥))}) |
68 | 9, 19, 67 | csbied2 3527 |
. . . 4
⊢ ((𝜑 ∧ (𝑓 = 〈𝐹, 𝐺〉 ∧ 𝑔 = 〈𝐾, 𝐿〉)) →
⦋(1st ‘𝑓) / 𝑟⦌⦋(1st
‘𝑔) / 𝑠⦌{𝑎 ∈ X𝑥 ∈
𝐵 ((𝑟‘𝑥)𝐽(𝑠‘𝑥)) ∣ ∀𝑥 ∈ 𝐵 ∀𝑦 ∈ 𝐵 ∀ℎ ∈ (𝑥𝐻𝑦)((𝑎‘𝑦)(〈(𝑟‘𝑥), (𝑟‘𝑦)〉 · (𝑠‘𝑦))((𝑥(2nd ‘𝑓)𝑦)‘ℎ)) = (((𝑥(2nd ‘𝑔)𝑦)‘ℎ)(〈(𝑟‘𝑥), (𝑠‘𝑥)〉 · (𝑠‘𝑦))(𝑎‘𝑥))} = {𝑎 ∈ X𝑥 ∈ 𝐵 ((𝐹‘𝑥)𝐽(𝐾‘𝑥)) ∣ ∀𝑥 ∈ 𝐵 ∀𝑦 ∈ 𝐵 ∀ℎ ∈ (𝑥𝐻𝑦)((𝑎‘𝑦)(〈(𝐹‘𝑥), (𝐹‘𝑦)〉 · (𝐾‘𝑦))((𝑥𝐺𝑦)‘ℎ)) = (((𝑥𝐿𝑦)‘ℎ)(〈(𝐹‘𝑥), (𝐾‘𝑥)〉 · (𝐾‘𝑦))(𝑎‘𝑥))}) |
69 | | df-br 4584 |
. . . . 5
⊢ (𝐹(𝐶 Func 𝐷)𝐺 ↔ 〈𝐹, 𝐺〉 ∈ (𝐶 Func 𝐷)) |
70 | 13, 69 | sylib 207 |
. . . 4
⊢ (𝜑 → 〈𝐹, 𝐺〉 ∈ (𝐶 Func 𝐷)) |
71 | | df-br 4584 |
. . . . 5
⊢ (𝐾(𝐶 Func 𝐷)𝐿 ↔ 〈𝐾, 𝐿〉 ∈ (𝐶 Func 𝐷)) |
72 | 24, 71 | sylib 207 |
. . . 4
⊢ (𝜑 → 〈𝐾, 𝐿〉 ∈ (𝐶 Func 𝐷)) |
73 | | ovex 6577 |
. . . . . . . 8
⊢ ((𝐹‘𝑥)𝐽(𝐾‘𝑥)) ∈ V |
74 | 73 | rgenw 2908 |
. . . . . . 7
⊢
∀𝑥 ∈
𝐵 ((𝐹‘𝑥)𝐽(𝐾‘𝑥)) ∈ V |
75 | | ixpexg 7818 |
. . . . . . 7
⊢
(∀𝑥 ∈
𝐵 ((𝐹‘𝑥)𝐽(𝐾‘𝑥)) ∈ V → X𝑥 ∈
𝐵 ((𝐹‘𝑥)𝐽(𝐾‘𝑥)) ∈ V) |
76 | 74, 75 | ax-mp 5 |
. . . . . 6
⊢ X𝑥 ∈
𝐵 ((𝐹‘𝑥)𝐽(𝐾‘𝑥)) ∈ V |
77 | 76 | rabex 4740 |
. . . . 5
⊢ {𝑎 ∈ X𝑥 ∈
𝐵 ((𝐹‘𝑥)𝐽(𝐾‘𝑥)) ∣ ∀𝑥 ∈ 𝐵 ∀𝑦 ∈ 𝐵 ∀ℎ ∈ (𝑥𝐻𝑦)((𝑎‘𝑦)(〈(𝐹‘𝑥), (𝐹‘𝑦)〉 · (𝐾‘𝑦))((𝑥𝐺𝑦)‘ℎ)) = (((𝑥𝐿𝑦)‘ℎ)(〈(𝐹‘𝑥), (𝐾‘𝑥)〉 · (𝐾‘𝑦))(𝑎‘𝑥))} ∈ V |
78 | 77 | a1i 11 |
. . . 4
⊢ (𝜑 → {𝑎 ∈ X𝑥 ∈ 𝐵 ((𝐹‘𝑥)𝐽(𝐾‘𝑥)) ∣ ∀𝑥 ∈ 𝐵 ∀𝑦 ∈ 𝐵 ∀ℎ ∈ (𝑥𝐻𝑦)((𝑎‘𝑦)(〈(𝐹‘𝑥), (𝐹‘𝑦)〉 · (𝐾‘𝑦))((𝑥𝐺𝑦)‘ℎ)) = (((𝑥𝐿𝑦)‘ℎ)(〈(𝐹‘𝑥), (𝐾‘𝑥)〉 · (𝐾‘𝑦))(𝑎‘𝑥))} ∈ V) |
79 | 7, 68, 70, 72, 78 | ovmpt2d 6686 |
. . 3
⊢ (𝜑 → (〈𝐹, 𝐺〉𝑁〈𝐾, 𝐿〉) = {𝑎 ∈ X𝑥 ∈ 𝐵 ((𝐹‘𝑥)𝐽(𝐾‘𝑥)) ∣ ∀𝑥 ∈ 𝐵 ∀𝑦 ∈ 𝐵 ∀ℎ ∈ (𝑥𝐻𝑦)((𝑎‘𝑦)(〈(𝐹‘𝑥), (𝐹‘𝑦)〉 · (𝐾‘𝑦))((𝑥𝐺𝑦)‘ℎ)) = (((𝑥𝐿𝑦)‘ℎ)(〈(𝐹‘𝑥), (𝐾‘𝑥)〉 · (𝐾‘𝑦))(𝑎‘𝑥))}) |
80 | 79 | eleq2d 2673 |
. 2
⊢ (𝜑 → (𝐴 ∈ (〈𝐹, 𝐺〉𝑁〈𝐾, 𝐿〉) ↔ 𝐴 ∈ {𝑎 ∈ X𝑥 ∈ 𝐵 ((𝐹‘𝑥)𝐽(𝐾‘𝑥)) ∣ ∀𝑥 ∈ 𝐵 ∀𝑦 ∈ 𝐵 ∀ℎ ∈ (𝑥𝐻𝑦)((𝑎‘𝑦)(〈(𝐹‘𝑥), (𝐹‘𝑦)〉 · (𝐾‘𝑦))((𝑥𝐺𝑦)‘ℎ)) = (((𝑥𝐿𝑦)‘ℎ)(〈(𝐹‘𝑥), (𝐾‘𝑥)〉 · (𝐾‘𝑦))(𝑎‘𝑥))})) |
81 | | fveq1 6102 |
. . . . . . 7
⊢ (𝑎 = 𝐴 → (𝑎‘𝑦) = (𝐴‘𝑦)) |
82 | 81 | oveq1d 6564 |
. . . . . 6
⊢ (𝑎 = 𝐴 → ((𝑎‘𝑦)(〈(𝐹‘𝑥), (𝐹‘𝑦)〉 · (𝐾‘𝑦))((𝑥𝐺𝑦)‘ℎ)) = ((𝐴‘𝑦)(〈(𝐹‘𝑥), (𝐹‘𝑦)〉 · (𝐾‘𝑦))((𝑥𝐺𝑦)‘ℎ))) |
83 | | fveq1 6102 |
. . . . . . 7
⊢ (𝑎 = 𝐴 → (𝑎‘𝑥) = (𝐴‘𝑥)) |
84 | 83 | oveq2d 6565 |
. . . . . 6
⊢ (𝑎 = 𝐴 → (((𝑥𝐿𝑦)‘ℎ)(〈(𝐹‘𝑥), (𝐾‘𝑥)〉 · (𝐾‘𝑦))(𝑎‘𝑥)) = (((𝑥𝐿𝑦)‘ℎ)(〈(𝐹‘𝑥), (𝐾‘𝑥)〉 · (𝐾‘𝑦))(𝐴‘𝑥))) |
85 | 82, 84 | eqeq12d 2625 |
. . . . 5
⊢ (𝑎 = 𝐴 → (((𝑎‘𝑦)(〈(𝐹‘𝑥), (𝐹‘𝑦)〉 · (𝐾‘𝑦))((𝑥𝐺𝑦)‘ℎ)) = (((𝑥𝐿𝑦)‘ℎ)(〈(𝐹‘𝑥), (𝐾‘𝑥)〉 · (𝐾‘𝑦))(𝑎‘𝑥)) ↔ ((𝐴‘𝑦)(〈(𝐹‘𝑥), (𝐹‘𝑦)〉 · (𝐾‘𝑦))((𝑥𝐺𝑦)‘ℎ)) = (((𝑥𝐿𝑦)‘ℎ)(〈(𝐹‘𝑥), (𝐾‘𝑥)〉 · (𝐾‘𝑦))(𝐴‘𝑥)))) |
86 | 85 | ralbidv 2969 |
. . . 4
⊢ (𝑎 = 𝐴 → (∀ℎ ∈ (𝑥𝐻𝑦)((𝑎‘𝑦)(〈(𝐹‘𝑥), (𝐹‘𝑦)〉 · (𝐾‘𝑦))((𝑥𝐺𝑦)‘ℎ)) = (((𝑥𝐿𝑦)‘ℎ)(〈(𝐹‘𝑥), (𝐾‘𝑥)〉 · (𝐾‘𝑦))(𝑎‘𝑥)) ↔ ∀ℎ ∈ (𝑥𝐻𝑦)((𝐴‘𝑦)(〈(𝐹‘𝑥), (𝐹‘𝑦)〉 · (𝐾‘𝑦))((𝑥𝐺𝑦)‘ℎ)) = (((𝑥𝐿𝑦)‘ℎ)(〈(𝐹‘𝑥), (𝐾‘𝑥)〉 · (𝐾‘𝑦))(𝐴‘𝑥)))) |
87 | 86 | 2ralbidv 2972 |
. . 3
⊢ (𝑎 = 𝐴 → (∀𝑥 ∈ 𝐵 ∀𝑦 ∈ 𝐵 ∀ℎ ∈ (𝑥𝐻𝑦)((𝑎‘𝑦)(〈(𝐹‘𝑥), (𝐹‘𝑦)〉 · (𝐾‘𝑦))((𝑥𝐺𝑦)‘ℎ)) = (((𝑥𝐿𝑦)‘ℎ)(〈(𝐹‘𝑥), (𝐾‘𝑥)〉 · (𝐾‘𝑦))(𝑎‘𝑥)) ↔ ∀𝑥 ∈ 𝐵 ∀𝑦 ∈ 𝐵 ∀ℎ ∈ (𝑥𝐻𝑦)((𝐴‘𝑦)(〈(𝐹‘𝑥), (𝐹‘𝑦)〉 · (𝐾‘𝑦))((𝑥𝐺𝑦)‘ℎ)) = (((𝑥𝐿𝑦)‘ℎ)(〈(𝐹‘𝑥), (𝐾‘𝑥)〉 · (𝐾‘𝑦))(𝐴‘𝑥)))) |
88 | 87 | elrab 3331 |
. 2
⊢ (𝐴 ∈ {𝑎 ∈ X𝑥 ∈ 𝐵 ((𝐹‘𝑥)𝐽(𝐾‘𝑥)) ∣ ∀𝑥 ∈ 𝐵 ∀𝑦 ∈ 𝐵 ∀ℎ ∈ (𝑥𝐻𝑦)((𝑎‘𝑦)(〈(𝐹‘𝑥), (𝐹‘𝑦)〉 · (𝐾‘𝑦))((𝑥𝐺𝑦)‘ℎ)) = (((𝑥𝐿𝑦)‘ℎ)(〈(𝐹‘𝑥), (𝐾‘𝑥)〉 · (𝐾‘𝑦))(𝑎‘𝑥))} ↔ (𝐴 ∈ X𝑥 ∈ 𝐵 ((𝐹‘𝑥)𝐽(𝐾‘𝑥)) ∧ ∀𝑥 ∈ 𝐵 ∀𝑦 ∈ 𝐵 ∀ℎ ∈ (𝑥𝐻𝑦)((𝐴‘𝑦)(〈(𝐹‘𝑥), (𝐹‘𝑦)〉 · (𝐾‘𝑦))((𝑥𝐺𝑦)‘ℎ)) = (((𝑥𝐿𝑦)‘ℎ)(〈(𝐹‘𝑥), (𝐾‘𝑥)〉 · (𝐾‘𝑦))(𝐴‘𝑥)))) |
89 | 80, 88 | syl6bb 275 |
1
⊢ (𝜑 → (𝐴 ∈ (〈𝐹, 𝐺〉𝑁〈𝐾, 𝐿〉) ↔ (𝐴 ∈ X𝑥 ∈ 𝐵 ((𝐹‘𝑥)𝐽(𝐾‘𝑥)) ∧ ∀𝑥 ∈ 𝐵 ∀𝑦 ∈ 𝐵 ∀ℎ ∈ (𝑥𝐻𝑦)((𝐴‘𝑦)(〈(𝐹‘𝑥), (𝐹‘𝑦)〉 · (𝐾‘𝑦))((𝑥𝐺𝑦)‘ℎ)) = (((𝑥𝐿𝑦)‘ℎ)(〈(𝐹‘𝑥), (𝐾‘𝑥)〉 · (𝐾‘𝑦))(𝐴‘𝑥))))) |