Step | Hyp | Ref
| Expression |
1 | | climeldmeqmpt.z |
. 2
⊢ 𝑍 =
(ℤ≥‘𝑀) |
2 | | climeldmeqmpt.a |
. . 3
⊢ (𝜑 → 𝐴 ∈ 𝑅) |
3 | 2 | mptexd 6997 |
. 2
⊢ (𝜑 → (𝑘 ∈ 𝐴 ↦ 𝐵) ∈ V) |
4 | | climeldmeqmpt.t |
. . 3
⊢ (𝜑 → 𝐶 ∈ 𝑆) |
5 | 4 | mptexd 6997 |
. 2
⊢ (𝜑 → (𝑘 ∈ 𝐶 ↦ 𝐷) ∈ V) |
6 | | climeldmeqmpt.m |
. 2
⊢ (𝜑 → 𝑀 ∈ ℤ) |
7 | | climeldmeqmpt.k |
. . . . . 6
⊢
Ⅎ𝑘𝜑 |
8 | | nfv 1921 |
. . . . . 6
⊢
Ⅎ𝑘 𝑗 ∈ 𝑍 |
9 | 7, 8 | nfan 1906 |
. . . . 5
⊢
Ⅎ𝑘(𝜑 ∧ 𝑗 ∈ 𝑍) |
10 | | nfcsb1v 3814 |
. . . . . 6
⊢
Ⅎ𝑘⦋𝑗 / 𝑘⦌𝐵 |
11 | | nfcv 2899 |
. . . . . . 7
⊢
Ⅎ𝑘𝑗 |
12 | 11 | nfcsb1 3813 |
. . . . . 6
⊢
Ⅎ𝑘⦋𝑗 / 𝑘⦌𝐷 |
13 | 10, 12 | nfeq 2912 |
. . . . 5
⊢
Ⅎ𝑘⦋𝑗 / 𝑘⦌𝐵 = ⦋𝑗 / 𝑘⦌𝐷 |
14 | 9, 13 | nfim 1903 |
. . . 4
⊢
Ⅎ𝑘((𝜑 ∧ 𝑗 ∈ 𝑍) → ⦋𝑗 / 𝑘⦌𝐵 = ⦋𝑗 / 𝑘⦌𝐷) |
15 | | eleq1w 2815 |
. . . . . 6
⊢ (𝑘 = 𝑗 → (𝑘 ∈ 𝑍 ↔ 𝑗 ∈ 𝑍)) |
16 | 15 | anbi2d 632 |
. . . . 5
⊢ (𝑘 = 𝑗 → ((𝜑 ∧ 𝑘 ∈ 𝑍) ↔ (𝜑 ∧ 𝑗 ∈ 𝑍))) |
17 | | csbeq1a 3804 |
. . . . . 6
⊢ (𝑘 = 𝑗 → 𝐵 = ⦋𝑗 / 𝑘⦌𝐵) |
18 | | csbeq1a 3804 |
. . . . . 6
⊢ (𝑘 = 𝑗 → 𝐷 = ⦋𝑗 / 𝑘⦌𝐷) |
19 | 17, 18 | eqeq12d 2754 |
. . . . 5
⊢ (𝑘 = 𝑗 → (𝐵 = 𝐷 ↔ ⦋𝑗 / 𝑘⦌𝐵 = ⦋𝑗 / 𝑘⦌𝐷)) |
20 | 16, 19 | imbi12d 348 |
. . . 4
⊢ (𝑘 = 𝑗 → (((𝜑 ∧ 𝑘 ∈ 𝑍) → 𝐵 = 𝐷) ↔ ((𝜑 ∧ 𝑗 ∈ 𝑍) → ⦋𝑗 / 𝑘⦌𝐵 = ⦋𝑗 / 𝑘⦌𝐷))) |
21 | | climeldmeqmpt.e |
. . . 4
⊢ ((𝜑 ∧ 𝑘 ∈ 𝑍) → 𝐵 = 𝐷) |
22 | 14, 20, 21 | chvarfv 2242 |
. . 3
⊢ ((𝜑 ∧ 𝑗 ∈ 𝑍) → ⦋𝑗 / 𝑘⦌𝐵 = ⦋𝑗 / 𝑘⦌𝐷) |
23 | | climeldmeqmpt.i |
. . . . 5
⊢ (𝜑 → 𝑍 ⊆ 𝐴) |
24 | 23 | sselda 3877 |
. . . 4
⊢ ((𝜑 ∧ 𝑗 ∈ 𝑍) → 𝑗 ∈ 𝐴) |
25 | | nfv 1921 |
. . . . . . . 8
⊢
Ⅎ𝑘 𝑗 ∈ 𝐴 |
26 | 7, 25 | nfan 1906 |
. . . . . . 7
⊢
Ⅎ𝑘(𝜑 ∧ 𝑗 ∈ 𝐴) |
27 | | nfcv 2899 |
. . . . . . . 8
⊢
Ⅎ𝑘𝑉 |
28 | 10, 27 | nfel 2913 |
. . . . . . 7
⊢
Ⅎ𝑘⦋𝑗 / 𝑘⦌𝐵 ∈ 𝑉 |
29 | 26, 28 | nfim 1903 |
. . . . . 6
⊢
Ⅎ𝑘((𝜑 ∧ 𝑗 ∈ 𝐴) → ⦋𝑗 / 𝑘⦌𝐵 ∈ 𝑉) |
30 | | eleq1w 2815 |
. . . . . . . 8
⊢ (𝑘 = 𝑗 → (𝑘 ∈ 𝐴 ↔ 𝑗 ∈ 𝐴)) |
31 | 30 | anbi2d 632 |
. . . . . . 7
⊢ (𝑘 = 𝑗 → ((𝜑 ∧ 𝑘 ∈ 𝐴) ↔ (𝜑 ∧ 𝑗 ∈ 𝐴))) |
32 | 17 | eleq1d 2817 |
. . . . . . 7
⊢ (𝑘 = 𝑗 → (𝐵 ∈ 𝑉 ↔ ⦋𝑗 / 𝑘⦌𝐵 ∈ 𝑉)) |
33 | 31, 32 | imbi12d 348 |
. . . . . 6
⊢ (𝑘 = 𝑗 → (((𝜑 ∧ 𝑘 ∈ 𝐴) → 𝐵 ∈ 𝑉) ↔ ((𝜑 ∧ 𝑗 ∈ 𝐴) → ⦋𝑗 / 𝑘⦌𝐵 ∈ 𝑉))) |
34 | | climeldmeqmpt.b |
. . . . . 6
⊢ ((𝜑 ∧ 𝑘 ∈ 𝐴) → 𝐵 ∈ 𝑉) |
35 | 29, 33, 34 | chvarfv 2242 |
. . . . 5
⊢ ((𝜑 ∧ 𝑗 ∈ 𝐴) → ⦋𝑗 / 𝑘⦌𝐵 ∈ 𝑉) |
36 | 24, 35 | syldan 594 |
. . . 4
⊢ ((𝜑 ∧ 𝑗 ∈ 𝑍) → ⦋𝑗 / 𝑘⦌𝐵 ∈ 𝑉) |
37 | 11 | nfcsb1 3813 |
. . . . 5
⊢
Ⅎ𝑘⦋𝑗 / 𝑘⦌𝐵 |
38 | | eqid 2738 |
. . . . 5
⊢ (𝑘 ∈ 𝐴 ↦ 𝐵) = (𝑘 ∈ 𝐴 ↦ 𝐵) |
39 | 11, 37, 17, 38 | fvmptf 6796 |
. . . 4
⊢ ((𝑗 ∈ 𝐴 ∧ ⦋𝑗 / 𝑘⦌𝐵 ∈ 𝑉) → ((𝑘 ∈ 𝐴 ↦ 𝐵)‘𝑗) = ⦋𝑗 / 𝑘⦌𝐵) |
40 | 24, 36, 39 | syl2anc 587 |
. . 3
⊢ ((𝜑 ∧ 𝑗 ∈ 𝑍) → ((𝑘 ∈ 𝐴 ↦ 𝐵)‘𝑗) = ⦋𝑗 / 𝑘⦌𝐵) |
41 | | climeldmeqmpt.l |
. . . . 5
⊢ (𝜑 → 𝑍 ⊆ 𝐶) |
42 | 41 | sselda 3877 |
. . . 4
⊢ ((𝜑 ∧ 𝑗 ∈ 𝑍) → 𝑗 ∈ 𝐶) |
43 | | nfv 1921 |
. . . . . . . 8
⊢
Ⅎ𝑘 𝑗 ∈ 𝐶 |
44 | 7, 43 | nfan 1906 |
. . . . . . 7
⊢
Ⅎ𝑘(𝜑 ∧ 𝑗 ∈ 𝐶) |
45 | | nfcv 2899 |
. . . . . . . 8
⊢
Ⅎ𝑘𝑊 |
46 | 12, 45 | nfel 2913 |
. . . . . . 7
⊢
Ⅎ𝑘⦋𝑗 / 𝑘⦌𝐷 ∈ 𝑊 |
47 | 44, 46 | nfim 1903 |
. . . . . 6
⊢
Ⅎ𝑘((𝜑 ∧ 𝑗 ∈ 𝐶) → ⦋𝑗 / 𝑘⦌𝐷 ∈ 𝑊) |
48 | | eleq1w 2815 |
. . . . . . . 8
⊢ (𝑘 = 𝑗 → (𝑘 ∈ 𝐶 ↔ 𝑗 ∈ 𝐶)) |
49 | 48 | anbi2d 632 |
. . . . . . 7
⊢ (𝑘 = 𝑗 → ((𝜑 ∧ 𝑘 ∈ 𝐶) ↔ (𝜑 ∧ 𝑗 ∈ 𝐶))) |
50 | 18 | eleq1d 2817 |
. . . . . . 7
⊢ (𝑘 = 𝑗 → (𝐷 ∈ 𝑊 ↔ ⦋𝑗 / 𝑘⦌𝐷 ∈ 𝑊)) |
51 | 49, 50 | imbi12d 348 |
. . . . . 6
⊢ (𝑘 = 𝑗 → (((𝜑 ∧ 𝑘 ∈ 𝐶) → 𝐷 ∈ 𝑊) ↔ ((𝜑 ∧ 𝑗 ∈ 𝐶) → ⦋𝑗 / 𝑘⦌𝐷 ∈ 𝑊))) |
52 | | climeldmeqmpt.c |
. . . . . 6
⊢ ((𝜑 ∧ 𝑘 ∈ 𝐶) → 𝐷 ∈ 𝑊) |
53 | 47, 51, 52 | chvarfv 2242 |
. . . . 5
⊢ ((𝜑 ∧ 𝑗 ∈ 𝐶) → ⦋𝑗 / 𝑘⦌𝐷 ∈ 𝑊) |
54 | 42, 53 | syldan 594 |
. . . 4
⊢ ((𝜑 ∧ 𝑗 ∈ 𝑍) → ⦋𝑗 / 𝑘⦌𝐷 ∈ 𝑊) |
55 | | eqid 2738 |
. . . . 5
⊢ (𝑘 ∈ 𝐶 ↦ 𝐷) = (𝑘 ∈ 𝐶 ↦ 𝐷) |
56 | 11, 12, 18, 55 | fvmptf 6796 |
. . . 4
⊢ ((𝑗 ∈ 𝐶 ∧ ⦋𝑗 / 𝑘⦌𝐷 ∈ 𝑊) → ((𝑘 ∈ 𝐶 ↦ 𝐷)‘𝑗) = ⦋𝑗 / 𝑘⦌𝐷) |
57 | 42, 54, 56 | syl2anc 587 |
. . 3
⊢ ((𝜑 ∧ 𝑗 ∈ 𝑍) → ((𝑘 ∈ 𝐶 ↦ 𝐷)‘𝑗) = ⦋𝑗 / 𝑘⦌𝐷) |
58 | 22, 40, 57 | 3eqtr4d 2783 |
. 2
⊢ ((𝜑 ∧ 𝑗 ∈ 𝑍) → ((𝑘 ∈ 𝐴 ↦ 𝐵)‘𝑗) = ((𝑘 ∈ 𝐶 ↦ 𝐷)‘𝑗)) |
59 | 1, 3, 5, 6, 58 | climeldmeq 42748 |
1
⊢ (𝜑 → ((𝑘 ∈ 𝐴 ↦ 𝐵) ∈ dom ⇝ ↔ (𝑘 ∈ 𝐶 ↦ 𝐷) ∈ dom ⇝ )) |