| Step | Hyp | Ref
| Expression |
| 1 | | df-ov 7434 |
. . 3
⊢ (𝑎(𝑎 ∈ 𝐴, 𝑏 ∈ 𝐵 ↦ 𝐶)𝑏) = ((𝑎 ∈ 𝐴, 𝑏 ∈ 𝐵 ↦ 𝐶)‘〈𝑎, 𝑏〉) |
| 2 | | fvmpopr2d.1 |
. . . . 5
⊢ (𝜑 → 𝐹 = (𝑎 ∈ 𝐴, 𝑏 ∈ 𝐵 ↦ 𝐶)) |
| 3 | 2 | 3ad2ant1 1134 |
. . . 4
⊢ ((𝜑 ∧ 𝑎 ∈ 𝐴 ∧ 𝑏 ∈ 𝐵) → 𝐹 = (𝑎 ∈ 𝐴, 𝑏 ∈ 𝐵 ↦ 𝐶)) |
| 4 | | fvmpopr2d.2 |
. . . . 5
⊢ (𝜑 → 𝑃 = 〈𝑎, 𝑏〉) |
| 5 | 4 | 3ad2ant1 1134 |
. . . 4
⊢ ((𝜑 ∧ 𝑎 ∈ 𝐴 ∧ 𝑏 ∈ 𝐵) → 𝑃 = 〈𝑎, 𝑏〉) |
| 6 | 3, 5 | fveq12d 6913 |
. . 3
⊢ ((𝜑 ∧ 𝑎 ∈ 𝐴 ∧ 𝑏 ∈ 𝐵) → (𝐹‘𝑃) = ((𝑎 ∈ 𝐴, 𝑏 ∈ 𝐵 ↦ 𝐶)‘〈𝑎, 𝑏〉)) |
| 7 | 1, 6 | eqtr4id 2796 |
. 2
⊢ ((𝜑 ∧ 𝑎 ∈ 𝐴 ∧ 𝑏 ∈ 𝐵) → (𝑎(𝑎 ∈ 𝐴, 𝑏 ∈ 𝐵 ↦ 𝐶)𝑏) = (𝐹‘𝑃)) |
| 8 | | nfcv 2905 |
. . . . 5
⊢
Ⅎ𝑐𝐶 |
| 9 | | nfcv 2905 |
. . . . 5
⊢
Ⅎ𝑑𝐶 |
| 10 | | nfcv 2905 |
. . . . . 6
⊢
Ⅎ𝑎𝑑 |
| 11 | | nfcsb1v 3923 |
. . . . . 6
⊢
Ⅎ𝑎⦋𝑐 / 𝑎⦌𝐶 |
| 12 | 10, 11 | nfcsbw 3925 |
. . . . 5
⊢
Ⅎ𝑎⦋𝑑 / 𝑏⦌⦋𝑐 / 𝑎⦌𝐶 |
| 13 | | nfcsb1v 3923 |
. . . . 5
⊢
Ⅎ𝑏⦋𝑑 / 𝑏⦌⦋𝑐 / 𝑎⦌𝐶 |
| 14 | | csbeq1a 3913 |
. . . . . 6
⊢ (𝑎 = 𝑐 → 𝐶 = ⦋𝑐 / 𝑎⦌𝐶) |
| 15 | | csbeq1a 3913 |
. . . . . 6
⊢ (𝑏 = 𝑑 → ⦋𝑐 / 𝑎⦌𝐶 = ⦋𝑑 / 𝑏⦌⦋𝑐 / 𝑎⦌𝐶) |
| 16 | 14, 15 | sylan9eq 2797 |
. . . . 5
⊢ ((𝑎 = 𝑐 ∧ 𝑏 = 𝑑) → 𝐶 = ⦋𝑑 / 𝑏⦌⦋𝑐 / 𝑎⦌𝐶) |
| 17 | 8, 9, 12, 13, 16 | cbvmpo 7527 |
. . . 4
⊢ (𝑎 ∈ 𝐴, 𝑏 ∈ 𝐵 ↦ 𝐶) = (𝑐 ∈ 𝐴, 𝑑 ∈ 𝐵 ↦ ⦋𝑑 / 𝑏⦌⦋𝑐 / 𝑎⦌𝐶) |
| 18 | 17 | oveqi 7444 |
. . 3
⊢ (𝑎(𝑎 ∈ 𝐴, 𝑏 ∈ 𝐵 ↦ 𝐶)𝑏) = (𝑎(𝑐 ∈ 𝐴, 𝑑 ∈ 𝐵 ↦ ⦋𝑑 / 𝑏⦌⦋𝑐 / 𝑎⦌𝐶)𝑏) |
| 19 | | eqidd 2738 |
. . . 4
⊢ ((𝜑 ∧ 𝑎 ∈ 𝐴 ∧ 𝑏 ∈ 𝐵) → (𝑐 ∈ 𝐴, 𝑑 ∈ 𝐵 ↦ ⦋𝑑 / 𝑏⦌⦋𝑐 / 𝑎⦌𝐶) = (𝑐 ∈ 𝐴, 𝑑 ∈ 𝐵 ↦ ⦋𝑑 / 𝑏⦌⦋𝑐 / 𝑎⦌𝐶)) |
| 20 | | equcom 2017 |
. . . . . . . 8
⊢ (𝑎 = 𝑐 ↔ 𝑐 = 𝑎) |
| 21 | | equcom 2017 |
. . . . . . . 8
⊢ (𝑏 = 𝑑 ↔ 𝑑 = 𝑏) |
| 22 | 20, 21 | anbi12i 628 |
. . . . . . 7
⊢ ((𝑎 = 𝑐 ∧ 𝑏 = 𝑑) ↔ (𝑐 = 𝑎 ∧ 𝑑 = 𝑏)) |
| 23 | 22, 16 | sylbir 235 |
. . . . . 6
⊢ ((𝑐 = 𝑎 ∧ 𝑑 = 𝑏) → 𝐶 = ⦋𝑑 / 𝑏⦌⦋𝑐 / 𝑎⦌𝐶) |
| 24 | 23 | eqcomd 2743 |
. . . . 5
⊢ ((𝑐 = 𝑎 ∧ 𝑑 = 𝑏) → ⦋𝑑 / 𝑏⦌⦋𝑐 / 𝑎⦌𝐶 = 𝐶) |
| 25 | 24 | adantl 481 |
. . . 4
⊢ (((𝜑 ∧ 𝑎 ∈ 𝐴 ∧ 𝑏 ∈ 𝐵) ∧ (𝑐 = 𝑎 ∧ 𝑑 = 𝑏)) → ⦋𝑑 / 𝑏⦌⦋𝑐 / 𝑎⦌𝐶 = 𝐶) |
| 26 | | simp2 1138 |
. . . 4
⊢ ((𝜑 ∧ 𝑎 ∈ 𝐴 ∧ 𝑏 ∈ 𝐵) → 𝑎 ∈ 𝐴) |
| 27 | | simp3 1139 |
. . . 4
⊢ ((𝜑 ∧ 𝑎 ∈ 𝐴 ∧ 𝑏 ∈ 𝐵) → 𝑏 ∈ 𝐵) |
| 28 | | fvmpopr2d.3 |
. . . 4
⊢ ((𝜑 ∧ 𝑎 ∈ 𝐴 ∧ 𝑏 ∈ 𝐵) → 𝐶 ∈ 𝑉) |
| 29 | 19, 25, 26, 27, 28 | ovmpod 7585 |
. . 3
⊢ ((𝜑 ∧ 𝑎 ∈ 𝐴 ∧ 𝑏 ∈ 𝐵) → (𝑎(𝑐 ∈ 𝐴, 𝑑 ∈ 𝐵 ↦ ⦋𝑑 / 𝑏⦌⦋𝑐 / 𝑎⦌𝐶)𝑏) = 𝐶) |
| 30 | 18, 29 | eqtrid 2789 |
. 2
⊢ ((𝜑 ∧ 𝑎 ∈ 𝐴 ∧ 𝑏 ∈ 𝐵) → (𝑎(𝑎 ∈ 𝐴, 𝑏 ∈ 𝐵 ↦ 𝐶)𝑏) = 𝐶) |
| 31 | 7, 30 | eqtr3d 2779 |
1
⊢ ((𝜑 ∧ 𝑎 ∈ 𝐴 ∧ 𝑏 ∈ 𝐵) → (𝐹‘𝑃) = 𝐶) |