Step | Hyp | Ref
| Expression |
1 | | fvmpt2curryd.b |
. . 3
⊢ (𝜑 → 𝐵 ∈ 𝑌) |
2 | | csbcom 3994 |
. . . . 5
⊢
⦋𝐵 /
𝑏⦌⦋𝐴 / 𝑎⦌⦋𝑏 / 𝑦⦌⦋𝑎 / 𝑥⦌𝐶 = ⦋𝐴 / 𝑎⦌⦋𝐵 / 𝑏⦌⦋𝑏 / 𝑦⦌⦋𝑎 / 𝑥⦌𝐶 |
3 | | csbco 3543 |
. . . . . 6
⊢
⦋𝐵 /
𝑏⦌⦋𝑏 / 𝑦⦌⦋𝑎 / 𝑥⦌𝐶 = ⦋𝐵 / 𝑦⦌⦋𝑎 / 𝑥⦌𝐶 |
4 | 3 | csbeq2i 3993 |
. . . . 5
⊢
⦋𝐴 /
𝑎⦌⦋𝐵 / 𝑏⦌⦋𝑏 / 𝑦⦌⦋𝑎 / 𝑥⦌𝐶 = ⦋𝐴 / 𝑎⦌⦋𝐵 / 𝑦⦌⦋𝑎 / 𝑥⦌𝐶 |
5 | | csbcom 3994 |
. . . . . 6
⊢
⦋𝐴 /
𝑎⦌⦋𝐵 / 𝑦⦌⦋𝑎 / 𝑥⦌𝐶 = ⦋𝐵 / 𝑦⦌⦋𝐴 / 𝑎⦌⦋𝑎 / 𝑥⦌𝐶 |
6 | | csbco 3543 |
. . . . . . 7
⊢
⦋𝐴 /
𝑎⦌⦋𝑎 / 𝑥⦌𝐶 = ⦋𝐴 / 𝑥⦌𝐶 |
7 | 6 | csbeq2i 3993 |
. . . . . 6
⊢
⦋𝐵 /
𝑦⦌⦋𝐴 / 𝑎⦌⦋𝑎 / 𝑥⦌𝐶 = ⦋𝐵 / 𝑦⦌⦋𝐴 / 𝑥⦌𝐶 |
8 | 5, 7 | eqtri 2644 |
. . . . 5
⊢
⦋𝐴 /
𝑎⦌⦋𝐵 / 𝑦⦌⦋𝑎 / 𝑥⦌𝐶 = ⦋𝐵 / 𝑦⦌⦋𝐴 / 𝑥⦌𝐶 |
9 | 2, 4, 8 | 3eqtri 2648 |
. . . 4
⊢
⦋𝐵 /
𝑏⦌⦋𝐴 / 𝑎⦌⦋𝑏 / 𝑦⦌⦋𝑎 / 𝑥⦌𝐶 = ⦋𝐵 / 𝑦⦌⦋𝐴 / 𝑥⦌𝐶 |
10 | | fvmpt2curryd.a |
. . . . 5
⊢ (𝜑 → 𝐴 ∈ 𝑋) |
11 | | fvmpt2curryd.c |
. . . . 5
⊢ (𝜑 → ∀𝑥 ∈ 𝑋 ∀𝑦 ∈ 𝑌 𝐶 ∈ 𝑉) |
12 | | nfcsb1v 3549 |
. . . . . . . 8
⊢
Ⅎ𝑥⦋𝐴 / 𝑥⦌𝐶 |
13 | 12 | nfel1 2779 |
. . . . . . 7
⊢
Ⅎ𝑥⦋𝐴 / 𝑥⦌𝐶 ∈ 𝑉 |
14 | | nfcsb1v 3549 |
. . . . . . . 8
⊢
Ⅎ𝑦⦋𝐵 / 𝑦⦌⦋𝐴 / 𝑥⦌𝐶 |
15 | 14 | nfel1 2779 |
. . . . . . 7
⊢
Ⅎ𝑦⦋𝐵 / 𝑦⦌⦋𝐴 / 𝑥⦌𝐶 ∈ 𝑉 |
16 | | csbeq1a 3542 |
. . . . . . . 8
⊢ (𝑥 = 𝐴 → 𝐶 = ⦋𝐴 / 𝑥⦌𝐶) |
17 | 16 | eleq1d 2686 |
. . . . . . 7
⊢ (𝑥 = 𝐴 → (𝐶 ∈ 𝑉 ↔ ⦋𝐴 / 𝑥⦌𝐶 ∈ 𝑉)) |
18 | | csbeq1a 3542 |
. . . . . . . 8
⊢ (𝑦 = 𝐵 → ⦋𝐴 / 𝑥⦌𝐶 = ⦋𝐵 / 𝑦⦌⦋𝐴 / 𝑥⦌𝐶) |
19 | 18 | eleq1d 2686 |
. . . . . . 7
⊢ (𝑦 = 𝐵 → (⦋𝐴 / 𝑥⦌𝐶 ∈ 𝑉 ↔ ⦋𝐵 / 𝑦⦌⦋𝐴 / 𝑥⦌𝐶 ∈ 𝑉)) |
20 | 13, 15, 17, 19 | rspc2 3320 |
. . . . . 6
⊢ ((𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑌) → (∀𝑥 ∈ 𝑋 ∀𝑦 ∈ 𝑌 𝐶 ∈ 𝑉 → ⦋𝐵 / 𝑦⦌⦋𝐴 / 𝑥⦌𝐶 ∈ 𝑉)) |
21 | 20 | imp 445 |
. . . . 5
⊢ (((𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑌) ∧ ∀𝑥 ∈ 𝑋 ∀𝑦 ∈ 𝑌 𝐶 ∈ 𝑉) → ⦋𝐵 / 𝑦⦌⦋𝐴 / 𝑥⦌𝐶 ∈ 𝑉) |
22 | 10, 1, 11, 21 | syl21anc 1325 |
. . . 4
⊢ (𝜑 → ⦋𝐵 / 𝑦⦌⦋𝐴 / 𝑥⦌𝐶 ∈ 𝑉) |
23 | 9, 22 | syl5eqel 2705 |
. . 3
⊢ (𝜑 → ⦋𝐵 / 𝑏⦌⦋𝐴 / 𝑎⦌⦋𝑏 / 𝑦⦌⦋𝑎 / 𝑥⦌𝐶 ∈ 𝑉) |
24 | | eqid 2622 |
. . . 4
⊢ (𝑏 ∈ 𝑌 ↦ ⦋𝐴 / 𝑎⦌⦋𝑏 / 𝑦⦌⦋𝑎 / 𝑥⦌𝐶) = (𝑏 ∈ 𝑌 ↦ ⦋𝐴 / 𝑎⦌⦋𝑏 / 𝑦⦌⦋𝑎 / 𝑥⦌𝐶) |
25 | 24 | fvmpts 6285 |
. . 3
⊢ ((𝐵 ∈ 𝑌 ∧ ⦋𝐵 / 𝑏⦌⦋𝐴 / 𝑎⦌⦋𝑏 / 𝑦⦌⦋𝑎 / 𝑥⦌𝐶 ∈ 𝑉) → ((𝑏 ∈ 𝑌 ↦ ⦋𝐴 / 𝑎⦌⦋𝑏 / 𝑦⦌⦋𝑎 / 𝑥⦌𝐶)‘𝐵) = ⦋𝐵 / 𝑏⦌⦋𝐴 / 𝑎⦌⦋𝑏 / 𝑦⦌⦋𝑎 / 𝑥⦌𝐶) |
26 | 1, 23, 25 | syl2anc 693 |
. 2
⊢ (𝜑 → ((𝑏 ∈ 𝑌 ↦ ⦋𝐴 / 𝑎⦌⦋𝑏 / 𝑦⦌⦋𝑎 / 𝑥⦌𝐶)‘𝐵) = ⦋𝐵 / 𝑏⦌⦋𝐴 / 𝑎⦌⦋𝑏 / 𝑦⦌⦋𝑎 / 𝑥⦌𝐶) |
27 | | fvmpt2curryd.f |
. . . . 5
⊢ 𝐹 = (𝑥 ∈ 𝑋, 𝑦 ∈ 𝑌 ↦ 𝐶) |
28 | | nfcv 2764 |
. . . . . 6
⊢
Ⅎ𝑎𝐶 |
29 | | nfcv 2764 |
. . . . . 6
⊢
Ⅎ𝑏𝐶 |
30 | | nfcv 2764 |
. . . . . . 7
⊢
Ⅎ𝑥𝑏 |
31 | | nfcsb1v 3549 |
. . . . . . 7
⊢
Ⅎ𝑥⦋𝑎 / 𝑥⦌𝐶 |
32 | 30, 31 | nfcsb 3551 |
. . . . . 6
⊢
Ⅎ𝑥⦋𝑏 / 𝑦⦌⦋𝑎 / 𝑥⦌𝐶 |
33 | | nfcsb1v 3549 |
. . . . . 6
⊢
Ⅎ𝑦⦋𝑏 / 𝑦⦌⦋𝑎 / 𝑥⦌𝐶 |
34 | | csbeq1a 3542 |
. . . . . . 7
⊢ (𝑥 = 𝑎 → 𝐶 = ⦋𝑎 / 𝑥⦌𝐶) |
35 | | csbeq1a 3542 |
. . . . . . 7
⊢ (𝑦 = 𝑏 → ⦋𝑎 / 𝑥⦌𝐶 = ⦋𝑏 / 𝑦⦌⦋𝑎 / 𝑥⦌𝐶) |
36 | 34, 35 | sylan9eq 2676 |
. . . . . 6
⊢ ((𝑥 = 𝑎 ∧ 𝑦 = 𝑏) → 𝐶 = ⦋𝑏 / 𝑦⦌⦋𝑎 / 𝑥⦌𝐶) |
37 | 28, 29, 32, 33, 36 | cbvmpt2 6734 |
. . . . 5
⊢ (𝑥 ∈ 𝑋, 𝑦 ∈ 𝑌 ↦ 𝐶) = (𝑎 ∈ 𝑋, 𝑏 ∈ 𝑌 ↦ ⦋𝑏 / 𝑦⦌⦋𝑎 / 𝑥⦌𝐶) |
38 | 27, 37 | eqtri 2644 |
. . . 4
⊢ 𝐹 = (𝑎 ∈ 𝑋, 𝑏 ∈ 𝑌 ↦ ⦋𝑏 / 𝑦⦌⦋𝑎 / 𝑥⦌𝐶) |
39 | 31 | nfel1 2779 |
. . . . . . 7
⊢
Ⅎ𝑥⦋𝑎 / 𝑥⦌𝐶 ∈ 𝑉 |
40 | 33 | nfel1 2779 |
. . . . . . 7
⊢
Ⅎ𝑦⦋𝑏 / 𝑦⦌⦋𝑎 / 𝑥⦌𝐶 ∈ 𝑉 |
41 | 34 | eleq1d 2686 |
. . . . . . 7
⊢ (𝑥 = 𝑎 → (𝐶 ∈ 𝑉 ↔ ⦋𝑎 / 𝑥⦌𝐶 ∈ 𝑉)) |
42 | 35 | eleq1d 2686 |
. . . . . . 7
⊢ (𝑦 = 𝑏 → (⦋𝑎 / 𝑥⦌𝐶 ∈ 𝑉 ↔ ⦋𝑏 / 𝑦⦌⦋𝑎 / 𝑥⦌𝐶 ∈ 𝑉)) |
43 | 39, 40, 41, 42 | rspc2 3320 |
. . . . . 6
⊢ ((𝑎 ∈ 𝑋 ∧ 𝑏 ∈ 𝑌) → (∀𝑥 ∈ 𝑋 ∀𝑦 ∈ 𝑌 𝐶 ∈ 𝑉 → ⦋𝑏 / 𝑦⦌⦋𝑎 / 𝑥⦌𝐶 ∈ 𝑉)) |
44 | 11, 43 | mpan9 486 |
. . . . 5
⊢ ((𝜑 ∧ (𝑎 ∈ 𝑋 ∧ 𝑏 ∈ 𝑌)) → ⦋𝑏 / 𝑦⦌⦋𝑎 / 𝑥⦌𝐶 ∈ 𝑉) |
45 | 44 | ralrimivva 2971 |
. . . 4
⊢ (𝜑 → ∀𝑎 ∈ 𝑋 ∀𝑏 ∈ 𝑌 ⦋𝑏 / 𝑦⦌⦋𝑎 / 𝑥⦌𝐶 ∈ 𝑉) |
46 | | ne0i 3921 |
. . . . 5
⊢ (𝐵 ∈ 𝑌 → 𝑌 ≠ ∅) |
47 | 1, 46 | syl 17 |
. . . 4
⊢ (𝜑 → 𝑌 ≠ ∅) |
48 | | fvmpt2curryd.y |
. . . 4
⊢ (𝜑 → 𝑌 ∈ 𝑊) |
49 | 38, 45, 47, 48, 10 | mpt2curryvald 7396 |
. . 3
⊢ (𝜑 → (curry 𝐹‘𝐴) = (𝑏 ∈ 𝑌 ↦ ⦋𝐴 / 𝑎⦌⦋𝑏 / 𝑦⦌⦋𝑎 / 𝑥⦌𝐶)) |
50 | 49 | fveq1d 6193 |
. 2
⊢ (𝜑 → ((curry 𝐹‘𝐴)‘𝐵) = ((𝑏 ∈ 𝑌 ↦ ⦋𝐴 / 𝑎⦌⦋𝑏 / 𝑦⦌⦋𝑎 / 𝑥⦌𝐶)‘𝐵)) |
51 | 27 | a1i 11 |
. . 3
⊢ (𝜑 → 𝐹 = (𝑥 ∈ 𝑋, 𝑦 ∈ 𝑌 ↦ 𝐶)) |
52 | | csbco 3543 |
. . . . . . . 8
⊢
⦋𝑦 /
𝑏⦌⦋𝑏 / 𝑦⦌⦋𝑎 / 𝑥⦌𝐶 = ⦋𝑦 / 𝑦⦌⦋𝑎 / 𝑥⦌𝐶 |
53 | | csbid 3541 |
. . . . . . . 8
⊢
⦋𝑦 /
𝑦⦌⦋𝑎 / 𝑥⦌𝐶 = ⦋𝑎 / 𝑥⦌𝐶 |
54 | 52, 53 | eqtr2i 2645 |
. . . . . . 7
⊢
⦋𝑎 /
𝑥⦌𝐶 = ⦋𝑦 / 𝑏⦌⦋𝑏 / 𝑦⦌⦋𝑎 / 𝑥⦌𝐶 |
55 | 54 | a1i 11 |
. . . . . 6
⊢ (𝜑 → ⦋𝑎 / 𝑥⦌𝐶 = ⦋𝑦 / 𝑏⦌⦋𝑏 / 𝑦⦌⦋𝑎 / 𝑥⦌𝐶) |
56 | 55 | csbeq2dv 3992 |
. . . . 5
⊢ (𝜑 → ⦋𝑥 / 𝑎⦌⦋𝑎 / 𝑥⦌𝐶 = ⦋𝑥 / 𝑎⦌⦋𝑦 / 𝑏⦌⦋𝑏 / 𝑦⦌⦋𝑎 / 𝑥⦌𝐶) |
57 | | csbco 3543 |
. . . . . 6
⊢
⦋𝑥 /
𝑎⦌⦋𝑎 / 𝑥⦌𝐶 = ⦋𝑥 / 𝑥⦌𝐶 |
58 | | csbid 3541 |
. . . . . 6
⊢
⦋𝑥 /
𝑥⦌𝐶 = 𝐶 |
59 | 57, 58 | eqtri 2644 |
. . . . 5
⊢
⦋𝑥 /
𝑎⦌⦋𝑎 / 𝑥⦌𝐶 = 𝐶 |
60 | | csbcom 3994 |
. . . . 5
⊢
⦋𝑥 /
𝑎⦌⦋𝑦 / 𝑏⦌⦋𝑏 / 𝑦⦌⦋𝑎 / 𝑥⦌𝐶 = ⦋𝑦 / 𝑏⦌⦋𝑥 / 𝑎⦌⦋𝑏 / 𝑦⦌⦋𝑎 / 𝑥⦌𝐶 |
61 | 56, 59, 60 | 3eqtr3g 2679 |
. . . 4
⊢ (𝜑 → 𝐶 = ⦋𝑦 / 𝑏⦌⦋𝑥 / 𝑎⦌⦋𝑏 / 𝑦⦌⦋𝑎 / 𝑥⦌𝐶) |
62 | | csbeq1 3536 |
. . . . . . 7
⊢ (𝑥 = 𝐴 → ⦋𝑥 / 𝑎⦌⦋𝑏 / 𝑦⦌⦋𝑎 / 𝑥⦌𝐶 = ⦋𝐴 / 𝑎⦌⦋𝑏 / 𝑦⦌⦋𝑎 / 𝑥⦌𝐶) |
63 | 62 | adantr 481 |
. . . . . 6
⊢ ((𝑥 = 𝐴 ∧ 𝑦 = 𝐵) → ⦋𝑥 / 𝑎⦌⦋𝑏 / 𝑦⦌⦋𝑎 / 𝑥⦌𝐶 = ⦋𝐴 / 𝑎⦌⦋𝑏 / 𝑦⦌⦋𝑎 / 𝑥⦌𝐶) |
64 | 63 | csbeq2dv 3992 |
. . . . 5
⊢ ((𝑥 = 𝐴 ∧ 𝑦 = 𝐵) → ⦋𝑦 / 𝑏⦌⦋𝑥 / 𝑎⦌⦋𝑏 / 𝑦⦌⦋𝑎 / 𝑥⦌𝐶 = ⦋𝑦 / 𝑏⦌⦋𝐴 / 𝑎⦌⦋𝑏 / 𝑦⦌⦋𝑎 / 𝑥⦌𝐶) |
65 | | csbeq1 3536 |
. . . . . 6
⊢ (𝑦 = 𝐵 → ⦋𝑦 / 𝑏⦌⦋𝐴 / 𝑎⦌⦋𝑏 / 𝑦⦌⦋𝑎 / 𝑥⦌𝐶 = ⦋𝐵 / 𝑏⦌⦋𝐴 / 𝑎⦌⦋𝑏 / 𝑦⦌⦋𝑎 / 𝑥⦌𝐶) |
66 | 65 | adantl 482 |
. . . . 5
⊢ ((𝑥 = 𝐴 ∧ 𝑦 = 𝐵) → ⦋𝑦 / 𝑏⦌⦋𝐴 / 𝑎⦌⦋𝑏 / 𝑦⦌⦋𝑎 / 𝑥⦌𝐶 = ⦋𝐵 / 𝑏⦌⦋𝐴 / 𝑎⦌⦋𝑏 / 𝑦⦌⦋𝑎 / 𝑥⦌𝐶) |
67 | 64, 66 | eqtrd 2656 |
. . . 4
⊢ ((𝑥 = 𝐴 ∧ 𝑦 = 𝐵) → ⦋𝑦 / 𝑏⦌⦋𝑥 / 𝑎⦌⦋𝑏 / 𝑦⦌⦋𝑎 / 𝑥⦌𝐶 = ⦋𝐵 / 𝑏⦌⦋𝐴 / 𝑎⦌⦋𝑏 / 𝑦⦌⦋𝑎 / 𝑥⦌𝐶) |
68 | 61, 67 | sylan9eq 2676 |
. . 3
⊢ ((𝜑 ∧ (𝑥 = 𝐴 ∧ 𝑦 = 𝐵)) → 𝐶 = ⦋𝐵 / 𝑏⦌⦋𝐴 / 𝑎⦌⦋𝑏 / 𝑦⦌⦋𝑎 / 𝑥⦌𝐶) |
69 | | eqidd 2623 |
. . 3
⊢ ((𝜑 ∧ 𝑥 = 𝐴) → 𝑌 = 𝑌) |
70 | | nfv 1843 |
. . 3
⊢
Ⅎ𝑥𝜑 |
71 | | nfv 1843 |
. . 3
⊢
Ⅎ𝑦𝜑 |
72 | | nfcv 2764 |
. . 3
⊢
Ⅎ𝑦𝐴 |
73 | | nfcv 2764 |
. . 3
⊢
Ⅎ𝑥𝐵 |
74 | | nfcv 2764 |
. . . . 5
⊢
Ⅎ𝑥𝐴 |
75 | 74, 32 | nfcsb 3551 |
. . . 4
⊢
Ⅎ𝑥⦋𝐴 / 𝑎⦌⦋𝑏 / 𝑦⦌⦋𝑎 / 𝑥⦌𝐶 |
76 | 73, 75 | nfcsb 3551 |
. . 3
⊢
Ⅎ𝑥⦋𝐵 / 𝑏⦌⦋𝐴 / 𝑎⦌⦋𝑏 / 𝑦⦌⦋𝑎 / 𝑥⦌𝐶 |
77 | 9, 14 | nfcxfr 2762 |
. . 3
⊢
Ⅎ𝑦⦋𝐵 / 𝑏⦌⦋𝐴 / 𝑎⦌⦋𝑏 / 𝑦⦌⦋𝑎 / 𝑥⦌𝐶 |
78 | 51, 68, 69, 10, 1, 23, 70, 71, 72, 73, 76, 77 | ovmpt2dxf 6786 |
. 2
⊢ (𝜑 → (𝐴𝐹𝐵) = ⦋𝐵 / 𝑏⦌⦋𝐴 / 𝑎⦌⦋𝑏 / 𝑦⦌⦋𝑎 / 𝑥⦌𝐶) |
79 | 26, 50, 78 | 3eqtr4d 2666 |
1
⊢ (𝜑 → ((curry 𝐹‘𝐴)‘𝐵) = (𝐴𝐹𝐵)) |