Step | Hyp | Ref
| Expression |
1 | | offval2.2 |
. . . . . 6
⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴) → 𝐵 ∈ 𝑊) |
2 | 1 | ralrimiva 3105 |
. . . . 5
⊢ (𝜑 → ∀𝑥 ∈ 𝐴 𝐵 ∈ 𝑊) |
3 | | eqid 2737 |
. . . . . 6
⊢ (𝑥 ∈ 𝐴 ↦ 𝐵) = (𝑥 ∈ 𝐴 ↦ 𝐵) |
4 | 3 | fnmpt 6518 |
. . . . 5
⊢
(∀𝑥 ∈
𝐴 𝐵 ∈ 𝑊 → (𝑥 ∈ 𝐴 ↦ 𝐵) Fn 𝐴) |
5 | 2, 4 | syl 17 |
. . . 4
⊢ (𝜑 → (𝑥 ∈ 𝐴 ↦ 𝐵) Fn 𝐴) |
6 | | offval2.4 |
. . . . 5
⊢ (𝜑 → 𝐹 = (𝑥 ∈ 𝐴 ↦ 𝐵)) |
7 | 6 | fneq1d 6472 |
. . . 4
⊢ (𝜑 → (𝐹 Fn 𝐴 ↔ (𝑥 ∈ 𝐴 ↦ 𝐵) Fn 𝐴)) |
8 | 5, 7 | mpbird 260 |
. . 3
⊢ (𝜑 → 𝐹 Fn 𝐴) |
9 | | offval2.3 |
. . . . . 6
⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴) → 𝐶 ∈ 𝑋) |
10 | 9 | ralrimiva 3105 |
. . . . 5
⊢ (𝜑 → ∀𝑥 ∈ 𝐴 𝐶 ∈ 𝑋) |
11 | | eqid 2737 |
. . . . . 6
⊢ (𝑥 ∈ 𝐴 ↦ 𝐶) = (𝑥 ∈ 𝐴 ↦ 𝐶) |
12 | 11 | fnmpt 6518 |
. . . . 5
⊢
(∀𝑥 ∈
𝐴 𝐶 ∈ 𝑋 → (𝑥 ∈ 𝐴 ↦ 𝐶) Fn 𝐴) |
13 | 10, 12 | syl 17 |
. . . 4
⊢ (𝜑 → (𝑥 ∈ 𝐴 ↦ 𝐶) Fn 𝐴) |
14 | | offval2.5 |
. . . . 5
⊢ (𝜑 → 𝐺 = (𝑥 ∈ 𝐴 ↦ 𝐶)) |
15 | 14 | fneq1d 6472 |
. . . 4
⊢ (𝜑 → (𝐺 Fn 𝐴 ↔ (𝑥 ∈ 𝐴 ↦ 𝐶) Fn 𝐴)) |
16 | 13, 15 | mpbird 260 |
. . 3
⊢ (𝜑 → 𝐺 Fn 𝐴) |
17 | | offval2.1 |
. . 3
⊢ (𝜑 → 𝐴 ∈ 𝑉) |
18 | | inidm 4133 |
. . 3
⊢ (𝐴 ∩ 𝐴) = 𝐴 |
19 | 6 | adantr 484 |
. . . 4
⊢ ((𝜑 ∧ 𝑦 ∈ 𝐴) → 𝐹 = (𝑥 ∈ 𝐴 ↦ 𝐵)) |
20 | 19 | fveq1d 6719 |
. . 3
⊢ ((𝜑 ∧ 𝑦 ∈ 𝐴) → (𝐹‘𝑦) = ((𝑥 ∈ 𝐴 ↦ 𝐵)‘𝑦)) |
21 | 14 | adantr 484 |
. . . 4
⊢ ((𝜑 ∧ 𝑦 ∈ 𝐴) → 𝐺 = (𝑥 ∈ 𝐴 ↦ 𝐶)) |
22 | 21 | fveq1d 6719 |
. . 3
⊢ ((𝜑 ∧ 𝑦 ∈ 𝐴) → (𝐺‘𝑦) = ((𝑥 ∈ 𝐴 ↦ 𝐶)‘𝑦)) |
23 | 8, 16, 17, 17, 18, 20, 22 | offval 7477 |
. 2
⊢ (𝜑 → (𝐹 ∘f 𝑅𝐺) = (𝑦 ∈ 𝐴 ↦ (((𝑥 ∈ 𝐴 ↦ 𝐵)‘𝑦)𝑅((𝑥 ∈ 𝐴 ↦ 𝐶)‘𝑦)))) |
24 | | nffvmpt1 6728 |
. . . . 5
⊢
Ⅎ𝑥((𝑥 ∈ 𝐴 ↦ 𝐵)‘𝑦) |
25 | | nfcv 2904 |
. . . . 5
⊢
Ⅎ𝑥𝑅 |
26 | | nffvmpt1 6728 |
. . . . 5
⊢
Ⅎ𝑥((𝑥 ∈ 𝐴 ↦ 𝐶)‘𝑦) |
27 | 24, 25, 26 | nfov 7243 |
. . . 4
⊢
Ⅎ𝑥(((𝑥 ∈ 𝐴 ↦ 𝐵)‘𝑦)𝑅((𝑥 ∈ 𝐴 ↦ 𝐶)‘𝑦)) |
28 | | nfcv 2904 |
. . . 4
⊢
Ⅎ𝑦(((𝑥 ∈ 𝐴 ↦ 𝐵)‘𝑥)𝑅((𝑥 ∈ 𝐴 ↦ 𝐶)‘𝑥)) |
29 | | fveq2 6717 |
. . . . 5
⊢ (𝑦 = 𝑥 → ((𝑥 ∈ 𝐴 ↦ 𝐵)‘𝑦) = ((𝑥 ∈ 𝐴 ↦ 𝐵)‘𝑥)) |
30 | | fveq2 6717 |
. . . . 5
⊢ (𝑦 = 𝑥 → ((𝑥 ∈ 𝐴 ↦ 𝐶)‘𝑦) = ((𝑥 ∈ 𝐴 ↦ 𝐶)‘𝑥)) |
31 | 29, 30 | oveq12d 7231 |
. . . 4
⊢ (𝑦 = 𝑥 → (((𝑥 ∈ 𝐴 ↦ 𝐵)‘𝑦)𝑅((𝑥 ∈ 𝐴 ↦ 𝐶)‘𝑦)) = (((𝑥 ∈ 𝐴 ↦ 𝐵)‘𝑥)𝑅((𝑥 ∈ 𝐴 ↦ 𝐶)‘𝑥))) |
32 | 27, 28, 31 | cbvmpt 5156 |
. . 3
⊢ (𝑦 ∈ 𝐴 ↦ (((𝑥 ∈ 𝐴 ↦ 𝐵)‘𝑦)𝑅((𝑥 ∈ 𝐴 ↦ 𝐶)‘𝑦))) = (𝑥 ∈ 𝐴 ↦ (((𝑥 ∈ 𝐴 ↦ 𝐵)‘𝑥)𝑅((𝑥 ∈ 𝐴 ↦ 𝐶)‘𝑥))) |
33 | | simpr 488 |
. . . . . 6
⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴) → 𝑥 ∈ 𝐴) |
34 | 3 | fvmpt2 6829 |
. . . . . 6
⊢ ((𝑥 ∈ 𝐴 ∧ 𝐵 ∈ 𝑊) → ((𝑥 ∈ 𝐴 ↦ 𝐵)‘𝑥) = 𝐵) |
35 | 33, 1, 34 | syl2anc 587 |
. . . . 5
⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴) → ((𝑥 ∈ 𝐴 ↦ 𝐵)‘𝑥) = 𝐵) |
36 | 11 | fvmpt2 6829 |
. . . . . 6
⊢ ((𝑥 ∈ 𝐴 ∧ 𝐶 ∈ 𝑋) → ((𝑥 ∈ 𝐴 ↦ 𝐶)‘𝑥) = 𝐶) |
37 | 33, 9, 36 | syl2anc 587 |
. . . . 5
⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴) → ((𝑥 ∈ 𝐴 ↦ 𝐶)‘𝑥) = 𝐶) |
38 | 35, 37 | oveq12d 7231 |
. . . 4
⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴) → (((𝑥 ∈ 𝐴 ↦ 𝐵)‘𝑥)𝑅((𝑥 ∈ 𝐴 ↦ 𝐶)‘𝑥)) = (𝐵𝑅𝐶)) |
39 | 38 | mpteq2dva 5150 |
. . 3
⊢ (𝜑 → (𝑥 ∈ 𝐴 ↦ (((𝑥 ∈ 𝐴 ↦ 𝐵)‘𝑥)𝑅((𝑥 ∈ 𝐴 ↦ 𝐶)‘𝑥))) = (𝑥 ∈ 𝐴 ↦ (𝐵𝑅𝐶))) |
40 | 32, 39 | eqtrid 2789 |
. 2
⊢ (𝜑 → (𝑦 ∈ 𝐴 ↦ (((𝑥 ∈ 𝐴 ↦ 𝐵)‘𝑦)𝑅((𝑥 ∈ 𝐴 ↦ 𝐶)‘𝑦))) = (𝑥 ∈ 𝐴 ↦ (𝐵𝑅𝐶))) |
41 | 23, 40 | eqtrd 2777 |
1
⊢ (𝜑 → (𝐹 ∘f 𝑅𝐺) = (𝑥 ∈ 𝐴 ↦ (𝐵𝑅𝐶))) |