Step | Hyp | Ref
| Expression |
1 | | df-ov 7146 |
. . 3
⊢ (𝑎(𝑎 ∈ 𝐴, 𝑏 ∈ 𝐵 ↦ 𝐶)𝑏) = ((𝑎 ∈ 𝐴, 𝑏 ∈ 𝐵 ↦ 𝐶)‘〈𝑎, 𝑏〉) |
2 | | fvmpopr2d.1 |
. . . . 5
⊢ (𝜑 → 𝐹 = (𝑎 ∈ 𝐴, 𝑏 ∈ 𝐵 ↦ 𝐶)) |
3 | 2 | 3ad2ant1 1131 |
. . . 4
⊢ ((𝜑 ∧ 𝑎 ∈ 𝐴 ∧ 𝑏 ∈ 𝐵) → 𝐹 = (𝑎 ∈ 𝐴, 𝑏 ∈ 𝐵 ↦ 𝐶)) |
4 | | fvmpopr2d.2 |
. . . . 5
⊢ (𝜑 → 𝑃 = 〈𝑎, 𝑏〉) |
5 | 4 | 3ad2ant1 1131 |
. . . 4
⊢ ((𝜑 ∧ 𝑎 ∈ 𝐴 ∧ 𝑏 ∈ 𝐵) → 𝑃 = 〈𝑎, 𝑏〉) |
6 | 3, 5 | fveq12d 6658 |
. . 3
⊢ ((𝜑 ∧ 𝑎 ∈ 𝐴 ∧ 𝑏 ∈ 𝐵) → (𝐹‘𝑃) = ((𝑎 ∈ 𝐴, 𝑏 ∈ 𝐵 ↦ 𝐶)‘〈𝑎, 𝑏〉)) |
7 | 1, 6 | eqtr4id 2813 |
. 2
⊢ ((𝜑 ∧ 𝑎 ∈ 𝐴 ∧ 𝑏 ∈ 𝐵) → (𝑎(𝑎 ∈ 𝐴, 𝑏 ∈ 𝐵 ↦ 𝐶)𝑏) = (𝐹‘𝑃)) |
8 | | nfcv 2917 |
. . . . 5
⊢
Ⅎ𝑐𝐶 |
9 | | nfcv 2917 |
. . . . 5
⊢
Ⅎ𝑑𝐶 |
10 | | nfcv 2917 |
. . . . . 6
⊢
Ⅎ𝑎𝑑 |
11 | | nfcsb1v 3825 |
. . . . . 6
⊢
Ⅎ𝑎⦋𝑐 / 𝑎⦌𝐶 |
12 | 10, 11 | nfcsbw 3827 |
. . . . 5
⊢
Ⅎ𝑎⦋𝑑 / 𝑏⦌⦋𝑐 / 𝑎⦌𝐶 |
13 | | nfcsb1v 3825 |
. . . . 5
⊢
Ⅎ𝑏⦋𝑑 / 𝑏⦌⦋𝑐 / 𝑎⦌𝐶 |
14 | | csbeq1a 3815 |
. . . . . 6
⊢ (𝑎 = 𝑐 → 𝐶 = ⦋𝑐 / 𝑎⦌𝐶) |
15 | | csbeq1a 3815 |
. . . . . 6
⊢ (𝑏 = 𝑑 → ⦋𝑐 / 𝑎⦌𝐶 = ⦋𝑑 / 𝑏⦌⦋𝑐 / 𝑎⦌𝐶) |
16 | 14, 15 | sylan9eq 2814 |
. . . . 5
⊢ ((𝑎 = 𝑐 ∧ 𝑏 = 𝑑) → 𝐶 = ⦋𝑑 / 𝑏⦌⦋𝑐 / 𝑎⦌𝐶) |
17 | 8, 9, 12, 13, 16 | cbvmpo 7235 |
. . . 4
⊢ (𝑎 ∈ 𝐴, 𝑏 ∈ 𝐵 ↦ 𝐶) = (𝑐 ∈ 𝐴, 𝑑 ∈ 𝐵 ↦ ⦋𝑑 / 𝑏⦌⦋𝑐 / 𝑎⦌𝐶) |
18 | 17 | oveqi 7156 |
. . 3
⊢ (𝑎(𝑎 ∈ 𝐴, 𝑏 ∈ 𝐵 ↦ 𝐶)𝑏) = (𝑎(𝑐 ∈ 𝐴, 𝑑 ∈ 𝐵 ↦ ⦋𝑑 / 𝑏⦌⦋𝑐 / 𝑎⦌𝐶)𝑏) |
19 | | eqidd 2760 |
. . . 4
⊢ ((𝜑 ∧ 𝑎 ∈ 𝐴 ∧ 𝑏 ∈ 𝐵) → (𝑐 ∈ 𝐴, 𝑑 ∈ 𝐵 ↦ ⦋𝑑 / 𝑏⦌⦋𝑐 / 𝑎⦌𝐶) = (𝑐 ∈ 𝐴, 𝑑 ∈ 𝐵 ↦ ⦋𝑑 / 𝑏⦌⦋𝑐 / 𝑎⦌𝐶)) |
20 | | equcom 2026 |
. . . . . . . 8
⊢ (𝑎 = 𝑐 ↔ 𝑐 = 𝑎) |
21 | | equcom 2026 |
. . . . . . . 8
⊢ (𝑏 = 𝑑 ↔ 𝑑 = 𝑏) |
22 | 20, 21 | anbi12i 630 |
. . . . . . 7
⊢ ((𝑎 = 𝑐 ∧ 𝑏 = 𝑑) ↔ (𝑐 = 𝑎 ∧ 𝑑 = 𝑏)) |
23 | 22, 16 | sylbir 238 |
. . . . . 6
⊢ ((𝑐 = 𝑎 ∧ 𝑑 = 𝑏) → 𝐶 = ⦋𝑑 / 𝑏⦌⦋𝑐 / 𝑎⦌𝐶) |
24 | 23 | eqcomd 2765 |
. . . . 5
⊢ ((𝑐 = 𝑎 ∧ 𝑑 = 𝑏) → ⦋𝑑 / 𝑏⦌⦋𝑐 / 𝑎⦌𝐶 = 𝐶) |
25 | 24 | adantl 486 |
. . . 4
⊢ (((𝜑 ∧ 𝑎 ∈ 𝐴 ∧ 𝑏 ∈ 𝐵) ∧ (𝑐 = 𝑎 ∧ 𝑑 = 𝑏)) → ⦋𝑑 / 𝑏⦌⦋𝑐 / 𝑎⦌𝐶 = 𝐶) |
26 | | simp2 1135 |
. . . 4
⊢ ((𝜑 ∧ 𝑎 ∈ 𝐴 ∧ 𝑏 ∈ 𝐵) → 𝑎 ∈ 𝐴) |
27 | | simp3 1136 |
. . . 4
⊢ ((𝜑 ∧ 𝑎 ∈ 𝐴 ∧ 𝑏 ∈ 𝐵) → 𝑏 ∈ 𝐵) |
28 | | fvmpopr2d.3 |
. . . 4
⊢ ((𝜑 ∧ 𝑎 ∈ 𝐴 ∧ 𝑏 ∈ 𝐵) → 𝐶 ∈ 𝑉) |
29 | 19, 25, 26, 27, 28 | ovmpod 7290 |
. . 3
⊢ ((𝜑 ∧ 𝑎 ∈ 𝐴 ∧ 𝑏 ∈ 𝐵) → (𝑎(𝑐 ∈ 𝐴, 𝑑 ∈ 𝐵 ↦ ⦋𝑑 / 𝑏⦌⦋𝑐 / 𝑎⦌𝐶)𝑏) = 𝐶) |
30 | 18, 29 | syl5eq 2806 |
. 2
⊢ ((𝜑 ∧ 𝑎 ∈ 𝐴 ∧ 𝑏 ∈ 𝐵) → (𝑎(𝑎 ∈ 𝐴, 𝑏 ∈ 𝐵 ↦ 𝐶)𝑏) = 𝐶) |
31 | 7, 30 | eqtr3d 2796 |
1
⊢ ((𝜑 ∧ 𝑎 ∈ 𝐴 ∧ 𝑏 ∈ 𝐵) → (𝐹‘𝑃) = 𝐶) |