| Step | Hyp | Ref
| Expression |
| 1 | | climeldmeqmpt.z |
. 2
⊢ 𝑍 =
(ℤ≥‘𝑀) |
| 2 | | climeldmeqmpt.a |
. . 3
⊢ (𝜑 → 𝐴 ∈ 𝑅) |
| 3 | 2 | mptexd 7244 |
. 2
⊢ (𝜑 → (𝑘 ∈ 𝐴 ↦ 𝐵) ∈ V) |
| 4 | | climeldmeqmpt.t |
. . 3
⊢ (𝜑 → 𝐶 ∈ 𝑆) |
| 5 | 4 | mptexd 7244 |
. 2
⊢ (𝜑 → (𝑘 ∈ 𝐶 ↦ 𝐷) ∈ V) |
| 6 | | climeldmeqmpt.m |
. 2
⊢ (𝜑 → 𝑀 ∈ ℤ) |
| 7 | | climeldmeqmpt.k |
. . . . . 6
⊢
Ⅎ𝑘𝜑 |
| 8 | | nfv 1914 |
. . . . . 6
⊢
Ⅎ𝑘 𝑗 ∈ 𝑍 |
| 9 | 7, 8 | nfan 1899 |
. . . . 5
⊢
Ⅎ𝑘(𝜑 ∧ 𝑗 ∈ 𝑍) |
| 10 | | nfcsb1v 3923 |
. . . . . 6
⊢
Ⅎ𝑘⦋𝑗 / 𝑘⦌𝐵 |
| 11 | | nfcv 2905 |
. . . . . . 7
⊢
Ⅎ𝑘𝑗 |
| 12 | 11 | nfcsb1 3922 |
. . . . . 6
⊢
Ⅎ𝑘⦋𝑗 / 𝑘⦌𝐷 |
| 13 | 10, 12 | nfeq 2919 |
. . . . 5
⊢
Ⅎ𝑘⦋𝑗 / 𝑘⦌𝐵 = ⦋𝑗 / 𝑘⦌𝐷 |
| 14 | 9, 13 | nfim 1896 |
. . . 4
⊢
Ⅎ𝑘((𝜑 ∧ 𝑗 ∈ 𝑍) → ⦋𝑗 / 𝑘⦌𝐵 = ⦋𝑗 / 𝑘⦌𝐷) |
| 15 | | eleq1w 2824 |
. . . . . 6
⊢ (𝑘 = 𝑗 → (𝑘 ∈ 𝑍 ↔ 𝑗 ∈ 𝑍)) |
| 16 | 15 | anbi2d 630 |
. . . . 5
⊢ (𝑘 = 𝑗 → ((𝜑 ∧ 𝑘 ∈ 𝑍) ↔ (𝜑 ∧ 𝑗 ∈ 𝑍))) |
| 17 | | csbeq1a 3913 |
. . . . . 6
⊢ (𝑘 = 𝑗 → 𝐵 = ⦋𝑗 / 𝑘⦌𝐵) |
| 18 | | csbeq1a 3913 |
. . . . . 6
⊢ (𝑘 = 𝑗 → 𝐷 = ⦋𝑗 / 𝑘⦌𝐷) |
| 19 | 17, 18 | eqeq12d 2753 |
. . . . 5
⊢ (𝑘 = 𝑗 → (𝐵 = 𝐷 ↔ ⦋𝑗 / 𝑘⦌𝐵 = ⦋𝑗 / 𝑘⦌𝐷)) |
| 20 | 16, 19 | imbi12d 344 |
. . . 4
⊢ (𝑘 = 𝑗 → (((𝜑 ∧ 𝑘 ∈ 𝑍) → 𝐵 = 𝐷) ↔ ((𝜑 ∧ 𝑗 ∈ 𝑍) → ⦋𝑗 / 𝑘⦌𝐵 = ⦋𝑗 / 𝑘⦌𝐷))) |
| 21 | | climeldmeqmpt.e |
. . . 4
⊢ ((𝜑 ∧ 𝑘 ∈ 𝑍) → 𝐵 = 𝐷) |
| 22 | 14, 20, 21 | chvarfv 2240 |
. . 3
⊢ ((𝜑 ∧ 𝑗 ∈ 𝑍) → ⦋𝑗 / 𝑘⦌𝐵 = ⦋𝑗 / 𝑘⦌𝐷) |
| 23 | | climeldmeqmpt.i |
. . . . 5
⊢ (𝜑 → 𝑍 ⊆ 𝐴) |
| 24 | 23 | sselda 3983 |
. . . 4
⊢ ((𝜑 ∧ 𝑗 ∈ 𝑍) → 𝑗 ∈ 𝐴) |
| 25 | | nfv 1914 |
. . . . . . . 8
⊢
Ⅎ𝑘 𝑗 ∈ 𝐴 |
| 26 | 7, 25 | nfan 1899 |
. . . . . . 7
⊢
Ⅎ𝑘(𝜑 ∧ 𝑗 ∈ 𝐴) |
| 27 | | nfcv 2905 |
. . . . . . . 8
⊢
Ⅎ𝑘𝑉 |
| 28 | 10, 27 | nfel 2920 |
. . . . . . 7
⊢
Ⅎ𝑘⦋𝑗 / 𝑘⦌𝐵 ∈ 𝑉 |
| 29 | 26, 28 | nfim 1896 |
. . . . . 6
⊢
Ⅎ𝑘((𝜑 ∧ 𝑗 ∈ 𝐴) → ⦋𝑗 / 𝑘⦌𝐵 ∈ 𝑉) |
| 30 | | eleq1w 2824 |
. . . . . . . 8
⊢ (𝑘 = 𝑗 → (𝑘 ∈ 𝐴 ↔ 𝑗 ∈ 𝐴)) |
| 31 | 30 | anbi2d 630 |
. . . . . . 7
⊢ (𝑘 = 𝑗 → ((𝜑 ∧ 𝑘 ∈ 𝐴) ↔ (𝜑 ∧ 𝑗 ∈ 𝐴))) |
| 32 | 17 | eleq1d 2826 |
. . . . . . 7
⊢ (𝑘 = 𝑗 → (𝐵 ∈ 𝑉 ↔ ⦋𝑗 / 𝑘⦌𝐵 ∈ 𝑉)) |
| 33 | 31, 32 | imbi12d 344 |
. . . . . 6
⊢ (𝑘 = 𝑗 → (((𝜑 ∧ 𝑘 ∈ 𝐴) → 𝐵 ∈ 𝑉) ↔ ((𝜑 ∧ 𝑗 ∈ 𝐴) → ⦋𝑗 / 𝑘⦌𝐵 ∈ 𝑉))) |
| 34 | | climeldmeqmpt.b |
. . . . . 6
⊢ ((𝜑 ∧ 𝑘 ∈ 𝐴) → 𝐵 ∈ 𝑉) |
| 35 | 29, 33, 34 | chvarfv 2240 |
. . . . 5
⊢ ((𝜑 ∧ 𝑗 ∈ 𝐴) → ⦋𝑗 / 𝑘⦌𝐵 ∈ 𝑉) |
| 36 | 24, 35 | syldan 591 |
. . . 4
⊢ ((𝜑 ∧ 𝑗 ∈ 𝑍) → ⦋𝑗 / 𝑘⦌𝐵 ∈ 𝑉) |
| 37 | 11 | nfcsb1 3922 |
. . . . 5
⊢
Ⅎ𝑘⦋𝑗 / 𝑘⦌𝐵 |
| 38 | | eqid 2737 |
. . . . 5
⊢ (𝑘 ∈ 𝐴 ↦ 𝐵) = (𝑘 ∈ 𝐴 ↦ 𝐵) |
| 39 | 11, 37, 17, 38 | fvmptf 7037 |
. . . 4
⊢ ((𝑗 ∈ 𝐴 ∧ ⦋𝑗 / 𝑘⦌𝐵 ∈ 𝑉) → ((𝑘 ∈ 𝐴 ↦ 𝐵)‘𝑗) = ⦋𝑗 / 𝑘⦌𝐵) |
| 40 | 24, 36, 39 | syl2anc 584 |
. . 3
⊢ ((𝜑 ∧ 𝑗 ∈ 𝑍) → ((𝑘 ∈ 𝐴 ↦ 𝐵)‘𝑗) = ⦋𝑗 / 𝑘⦌𝐵) |
| 41 | | climeldmeqmpt.l |
. . . . 5
⊢ (𝜑 → 𝑍 ⊆ 𝐶) |
| 42 | 41 | sselda 3983 |
. . . 4
⊢ ((𝜑 ∧ 𝑗 ∈ 𝑍) → 𝑗 ∈ 𝐶) |
| 43 | | nfv 1914 |
. . . . . . . 8
⊢
Ⅎ𝑘 𝑗 ∈ 𝐶 |
| 44 | 7, 43 | nfan 1899 |
. . . . . . 7
⊢
Ⅎ𝑘(𝜑 ∧ 𝑗 ∈ 𝐶) |
| 45 | | nfcv 2905 |
. . . . . . . 8
⊢
Ⅎ𝑘𝑊 |
| 46 | 12, 45 | nfel 2920 |
. . . . . . 7
⊢
Ⅎ𝑘⦋𝑗 / 𝑘⦌𝐷 ∈ 𝑊 |
| 47 | 44, 46 | nfim 1896 |
. . . . . 6
⊢
Ⅎ𝑘((𝜑 ∧ 𝑗 ∈ 𝐶) → ⦋𝑗 / 𝑘⦌𝐷 ∈ 𝑊) |
| 48 | | eleq1w 2824 |
. . . . . . . 8
⊢ (𝑘 = 𝑗 → (𝑘 ∈ 𝐶 ↔ 𝑗 ∈ 𝐶)) |
| 49 | 48 | anbi2d 630 |
. . . . . . 7
⊢ (𝑘 = 𝑗 → ((𝜑 ∧ 𝑘 ∈ 𝐶) ↔ (𝜑 ∧ 𝑗 ∈ 𝐶))) |
| 50 | 18 | eleq1d 2826 |
. . . . . . 7
⊢ (𝑘 = 𝑗 → (𝐷 ∈ 𝑊 ↔ ⦋𝑗 / 𝑘⦌𝐷 ∈ 𝑊)) |
| 51 | 49, 50 | imbi12d 344 |
. . . . . 6
⊢ (𝑘 = 𝑗 → (((𝜑 ∧ 𝑘 ∈ 𝐶) → 𝐷 ∈ 𝑊) ↔ ((𝜑 ∧ 𝑗 ∈ 𝐶) → ⦋𝑗 / 𝑘⦌𝐷 ∈ 𝑊))) |
| 52 | | climeldmeqmpt.c |
. . . . . 6
⊢ ((𝜑 ∧ 𝑘 ∈ 𝐶) → 𝐷 ∈ 𝑊) |
| 53 | 47, 51, 52 | chvarfv 2240 |
. . . . 5
⊢ ((𝜑 ∧ 𝑗 ∈ 𝐶) → ⦋𝑗 / 𝑘⦌𝐷 ∈ 𝑊) |
| 54 | 42, 53 | syldan 591 |
. . . 4
⊢ ((𝜑 ∧ 𝑗 ∈ 𝑍) → ⦋𝑗 / 𝑘⦌𝐷 ∈ 𝑊) |
| 55 | | eqid 2737 |
. . . . 5
⊢ (𝑘 ∈ 𝐶 ↦ 𝐷) = (𝑘 ∈ 𝐶 ↦ 𝐷) |
| 56 | 11, 12, 18, 55 | fvmptf 7037 |
. . . 4
⊢ ((𝑗 ∈ 𝐶 ∧ ⦋𝑗 / 𝑘⦌𝐷 ∈ 𝑊) → ((𝑘 ∈ 𝐶 ↦ 𝐷)‘𝑗) = ⦋𝑗 / 𝑘⦌𝐷) |
| 57 | 42, 54, 56 | syl2anc 584 |
. . 3
⊢ ((𝜑 ∧ 𝑗 ∈ 𝑍) → ((𝑘 ∈ 𝐶 ↦ 𝐷)‘𝑗) = ⦋𝑗 / 𝑘⦌𝐷) |
| 58 | 22, 40, 57 | 3eqtr4d 2787 |
. 2
⊢ ((𝜑 ∧ 𝑗 ∈ 𝑍) → ((𝑘 ∈ 𝐴 ↦ 𝐵)‘𝑗) = ((𝑘 ∈ 𝐶 ↦ 𝐷)‘𝑗)) |
| 59 | 1, 3, 5, 6, 58 | climeldmeq 45680 |
1
⊢ (𝜑 → ((𝑘 ∈ 𝐴 ↦ 𝐵) ∈ dom ⇝ ↔ (𝑘 ∈ 𝐶 ↦ 𝐷) ∈ dom ⇝ )) |