| Step | Hyp | Ref
| Expression |
| 1 | | offval2.2 |
. . . . . 6
⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴) → 𝐵 ∈ 𝑊) |
| 2 | 1 | ralrimiva 3146 |
. . . . 5
⊢ (𝜑 → ∀𝑥 ∈ 𝐴 𝐵 ∈ 𝑊) |
| 3 | | eqid 2737 |
. . . . . 6
⊢ (𝑥 ∈ 𝐴 ↦ 𝐵) = (𝑥 ∈ 𝐴 ↦ 𝐵) |
| 4 | 3 | fnmpt 6708 |
. . . . 5
⊢
(∀𝑥 ∈
𝐴 𝐵 ∈ 𝑊 → (𝑥 ∈ 𝐴 ↦ 𝐵) Fn 𝐴) |
| 5 | 2, 4 | syl 17 |
. . . 4
⊢ (𝜑 → (𝑥 ∈ 𝐴 ↦ 𝐵) Fn 𝐴) |
| 6 | | offval2.4 |
. . . . 5
⊢ (𝜑 → 𝐹 = (𝑥 ∈ 𝐴 ↦ 𝐵)) |
| 7 | 6 | fneq1d 6661 |
. . . 4
⊢ (𝜑 → (𝐹 Fn 𝐴 ↔ (𝑥 ∈ 𝐴 ↦ 𝐵) Fn 𝐴)) |
| 8 | 5, 7 | mpbird 257 |
. . 3
⊢ (𝜑 → 𝐹 Fn 𝐴) |
| 9 | | offval2.3 |
. . . . . 6
⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴) → 𝐶 ∈ 𝑋) |
| 10 | 9 | ralrimiva 3146 |
. . . . 5
⊢ (𝜑 → ∀𝑥 ∈ 𝐴 𝐶 ∈ 𝑋) |
| 11 | | eqid 2737 |
. . . . . 6
⊢ (𝑥 ∈ 𝐴 ↦ 𝐶) = (𝑥 ∈ 𝐴 ↦ 𝐶) |
| 12 | 11 | fnmpt 6708 |
. . . . 5
⊢
(∀𝑥 ∈
𝐴 𝐶 ∈ 𝑋 → (𝑥 ∈ 𝐴 ↦ 𝐶) Fn 𝐴) |
| 13 | 10, 12 | syl 17 |
. . . 4
⊢ (𝜑 → (𝑥 ∈ 𝐴 ↦ 𝐶) Fn 𝐴) |
| 14 | | offval2.5 |
. . . . 5
⊢ (𝜑 → 𝐺 = (𝑥 ∈ 𝐴 ↦ 𝐶)) |
| 15 | 14 | fneq1d 6661 |
. . . 4
⊢ (𝜑 → (𝐺 Fn 𝐴 ↔ (𝑥 ∈ 𝐴 ↦ 𝐶) Fn 𝐴)) |
| 16 | 13, 15 | mpbird 257 |
. . 3
⊢ (𝜑 → 𝐺 Fn 𝐴) |
| 17 | | offval2.1 |
. . 3
⊢ (𝜑 → 𝐴 ∈ 𝑉) |
| 18 | | inidm 4227 |
. . 3
⊢ (𝐴 ∩ 𝐴) = 𝐴 |
| 19 | 6 | adantr 480 |
. . . 4
⊢ ((𝜑 ∧ 𝑦 ∈ 𝐴) → 𝐹 = (𝑥 ∈ 𝐴 ↦ 𝐵)) |
| 20 | 19 | fveq1d 6908 |
. . 3
⊢ ((𝜑 ∧ 𝑦 ∈ 𝐴) → (𝐹‘𝑦) = ((𝑥 ∈ 𝐴 ↦ 𝐵)‘𝑦)) |
| 21 | 14 | adantr 480 |
. . . 4
⊢ ((𝜑 ∧ 𝑦 ∈ 𝐴) → 𝐺 = (𝑥 ∈ 𝐴 ↦ 𝐶)) |
| 22 | 21 | fveq1d 6908 |
. . 3
⊢ ((𝜑 ∧ 𝑦 ∈ 𝐴) → (𝐺‘𝑦) = ((𝑥 ∈ 𝐴 ↦ 𝐶)‘𝑦)) |
| 23 | 8, 16, 17, 17, 18, 20, 22 | offval 7706 |
. 2
⊢ (𝜑 → (𝐹 ∘f 𝑅𝐺) = (𝑦 ∈ 𝐴 ↦ (((𝑥 ∈ 𝐴 ↦ 𝐵)‘𝑦)𝑅((𝑥 ∈ 𝐴 ↦ 𝐶)‘𝑦)))) |
| 24 | | nffvmpt1 6917 |
. . . . 5
⊢
Ⅎ𝑥((𝑥 ∈ 𝐴 ↦ 𝐵)‘𝑦) |
| 25 | | nfcv 2905 |
. . . . 5
⊢
Ⅎ𝑥𝑅 |
| 26 | | nffvmpt1 6917 |
. . . . 5
⊢
Ⅎ𝑥((𝑥 ∈ 𝐴 ↦ 𝐶)‘𝑦) |
| 27 | 24, 25, 26 | nfov 7461 |
. . . 4
⊢
Ⅎ𝑥(((𝑥 ∈ 𝐴 ↦ 𝐵)‘𝑦)𝑅((𝑥 ∈ 𝐴 ↦ 𝐶)‘𝑦)) |
| 28 | | nfcv 2905 |
. . . 4
⊢
Ⅎ𝑦(((𝑥 ∈ 𝐴 ↦ 𝐵)‘𝑥)𝑅((𝑥 ∈ 𝐴 ↦ 𝐶)‘𝑥)) |
| 29 | | fveq2 6906 |
. . . . 5
⊢ (𝑦 = 𝑥 → ((𝑥 ∈ 𝐴 ↦ 𝐵)‘𝑦) = ((𝑥 ∈ 𝐴 ↦ 𝐵)‘𝑥)) |
| 30 | | fveq2 6906 |
. . . . 5
⊢ (𝑦 = 𝑥 → ((𝑥 ∈ 𝐴 ↦ 𝐶)‘𝑦) = ((𝑥 ∈ 𝐴 ↦ 𝐶)‘𝑥)) |
| 31 | 29, 30 | oveq12d 7449 |
. . . 4
⊢ (𝑦 = 𝑥 → (((𝑥 ∈ 𝐴 ↦ 𝐵)‘𝑦)𝑅((𝑥 ∈ 𝐴 ↦ 𝐶)‘𝑦)) = (((𝑥 ∈ 𝐴 ↦ 𝐵)‘𝑥)𝑅((𝑥 ∈ 𝐴 ↦ 𝐶)‘𝑥))) |
| 32 | 27, 28, 31 | cbvmpt 5253 |
. . 3
⊢ (𝑦 ∈ 𝐴 ↦ (((𝑥 ∈ 𝐴 ↦ 𝐵)‘𝑦)𝑅((𝑥 ∈ 𝐴 ↦ 𝐶)‘𝑦))) = (𝑥 ∈ 𝐴 ↦ (((𝑥 ∈ 𝐴 ↦ 𝐵)‘𝑥)𝑅((𝑥 ∈ 𝐴 ↦ 𝐶)‘𝑥))) |
| 33 | | simpr 484 |
. . . . . 6
⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴) → 𝑥 ∈ 𝐴) |
| 34 | 3 | fvmpt2 7027 |
. . . . . 6
⊢ ((𝑥 ∈ 𝐴 ∧ 𝐵 ∈ 𝑊) → ((𝑥 ∈ 𝐴 ↦ 𝐵)‘𝑥) = 𝐵) |
| 35 | 33, 1, 34 | syl2anc 584 |
. . . . 5
⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴) → ((𝑥 ∈ 𝐴 ↦ 𝐵)‘𝑥) = 𝐵) |
| 36 | 11 | fvmpt2 7027 |
. . . . . 6
⊢ ((𝑥 ∈ 𝐴 ∧ 𝐶 ∈ 𝑋) → ((𝑥 ∈ 𝐴 ↦ 𝐶)‘𝑥) = 𝐶) |
| 37 | 33, 9, 36 | syl2anc 584 |
. . . . 5
⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴) → ((𝑥 ∈ 𝐴 ↦ 𝐶)‘𝑥) = 𝐶) |
| 38 | 35, 37 | oveq12d 7449 |
. . . 4
⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴) → (((𝑥 ∈ 𝐴 ↦ 𝐵)‘𝑥)𝑅((𝑥 ∈ 𝐴 ↦ 𝐶)‘𝑥)) = (𝐵𝑅𝐶)) |
| 39 | 38 | mpteq2dva 5242 |
. . 3
⊢ (𝜑 → (𝑥 ∈ 𝐴 ↦ (((𝑥 ∈ 𝐴 ↦ 𝐵)‘𝑥)𝑅((𝑥 ∈ 𝐴 ↦ 𝐶)‘𝑥))) = (𝑥 ∈ 𝐴 ↦ (𝐵𝑅𝐶))) |
| 40 | 32, 39 | eqtrid 2789 |
. 2
⊢ (𝜑 → (𝑦 ∈ 𝐴 ↦ (((𝑥 ∈ 𝐴 ↦ 𝐵)‘𝑦)𝑅((𝑥 ∈ 𝐴 ↦ 𝐶)‘𝑦))) = (𝑥 ∈ 𝐴 ↦ (𝐵𝑅𝐶))) |
| 41 | 23, 40 | eqtrd 2777 |
1
⊢ (𝜑 → (𝐹 ∘f 𝑅𝐺) = (𝑥 ∈ 𝐴 ↦ (𝐵𝑅𝐶))) |