Proof of Theorem liminfequzmpt2
| Step | Hyp | Ref
| Expression |
| 1 | | liminfequzmpt2.j |
. . . . . . . . 9
⊢
Ⅎ𝑗𝜑 |
| 2 | | liminfequzmpt2.a |
. . . . . . . . . . . . . . 15
⊢ 𝐴 =
(ℤ≥‘𝑀) |
| 3 | | liminfequzmpt2.k |
. . . . . . . . . . . . . . 15
⊢ (𝜑 → 𝐾 ∈ 𝐴) |
| 4 | 2, 3 | uzssd2 45428 |
. . . . . . . . . . . . . 14
⊢ (𝜑 →
(ℤ≥‘𝐾) ⊆ 𝐴) |
| 5 | 4 | adantr 480 |
. . . . . . . . . . . . 13
⊢ ((𝜑 ∧ 𝑗 ∈ (ℤ≥‘𝐾)) →
(ℤ≥‘𝐾) ⊆ 𝐴) |
| 6 | | simpr 484 |
. . . . . . . . . . . . 13
⊢ ((𝜑 ∧ 𝑗 ∈ (ℤ≥‘𝐾)) → 𝑗 ∈ (ℤ≥‘𝐾)) |
| 7 | 5, 6 | sseldd 3984 |
. . . . . . . . . . . 12
⊢ ((𝜑 ∧ 𝑗 ∈ (ℤ≥‘𝐾)) → 𝑗 ∈ 𝐴) |
| 8 | | liminfequzmpt2.c |
. . . . . . . . . . . . 13
⊢ ((𝜑 ∧ 𝑗 ∈ (ℤ≥‘𝐾)) → 𝐶 ∈ 𝑉) |
| 9 | 8 | elexd 3504 |
. . . . . . . . . . . 12
⊢ ((𝜑 ∧ 𝑗 ∈ (ℤ≥‘𝐾)) → 𝐶 ∈ V) |
| 10 | 7, 9 | jca 511 |
. . . . . . . . . . 11
⊢ ((𝜑 ∧ 𝑗 ∈ (ℤ≥‘𝐾)) → (𝑗 ∈ 𝐴 ∧ 𝐶 ∈ V)) |
| 11 | | rabid 3458 |
. . . . . . . . . . 11
⊢ (𝑗 ∈ {𝑗 ∈ 𝐴 ∣ 𝐶 ∈ V} ↔ (𝑗 ∈ 𝐴 ∧ 𝐶 ∈ V)) |
| 12 | 10, 11 | sylibr 234 |
. . . . . . . . . 10
⊢ ((𝜑 ∧ 𝑗 ∈ (ℤ≥‘𝐾)) → 𝑗 ∈ {𝑗 ∈ 𝐴 ∣ 𝐶 ∈ V}) |
| 13 | 12 | ex 412 |
. . . . . . . . 9
⊢ (𝜑 → (𝑗 ∈ (ℤ≥‘𝐾) → 𝑗 ∈ {𝑗 ∈ 𝐴 ∣ 𝐶 ∈ V})) |
| 14 | 1, 13 | ralrimi 3257 |
. . . . . . . 8
⊢ (𝜑 → ∀𝑗 ∈ (ℤ≥‘𝐾)𝑗 ∈ {𝑗 ∈ 𝐴 ∣ 𝐶 ∈ V}) |
| 15 | | nfcv 2905 |
. . . . . . . . 9
⊢
Ⅎ𝑗(ℤ≥‘𝐾) |
| 16 | | nfrab1 3457 |
. . . . . . . . 9
⊢
Ⅎ𝑗{𝑗 ∈ 𝐴 ∣ 𝐶 ∈ V} |
| 17 | 15, 16 | dfss3f 3975 |
. . . . . . . 8
⊢
((ℤ≥‘𝐾) ⊆ {𝑗 ∈ 𝐴 ∣ 𝐶 ∈ V} ↔ ∀𝑗 ∈ (ℤ≥‘𝐾)𝑗 ∈ {𝑗 ∈ 𝐴 ∣ 𝐶 ∈ V}) |
| 18 | 14, 17 | sylibr 234 |
. . . . . . 7
⊢ (𝜑 →
(ℤ≥‘𝐾) ⊆ {𝑗 ∈ 𝐴 ∣ 𝐶 ∈ V}) |
| 19 | 16, 15 | resmptf 6057 |
. . . . . . 7
⊢
((ℤ≥‘𝐾) ⊆ {𝑗 ∈ 𝐴 ∣ 𝐶 ∈ V} → ((𝑗 ∈ {𝑗 ∈ 𝐴 ∣ 𝐶 ∈ V} ↦ 𝐶) ↾
(ℤ≥‘𝐾)) = (𝑗 ∈ (ℤ≥‘𝐾) ↦ 𝐶)) |
| 20 | 18, 19 | syl 17 |
. . . . . 6
⊢ (𝜑 → ((𝑗 ∈ {𝑗 ∈ 𝐴 ∣ 𝐶 ∈ V} ↦ 𝐶) ↾
(ℤ≥‘𝐾)) = (𝑗 ∈ (ℤ≥‘𝐾) ↦ 𝐶)) |
| 21 | 20 | eqcomd 2743 |
. . . . 5
⊢ (𝜑 → (𝑗 ∈ (ℤ≥‘𝐾) ↦ 𝐶) = ((𝑗 ∈ {𝑗 ∈ 𝐴 ∣ 𝐶 ∈ V} ↦ 𝐶) ↾
(ℤ≥‘𝐾))) |
| 22 | 21 | fveq2d 6910 |
. . . 4
⊢ (𝜑 → (lim inf‘(𝑗 ∈
(ℤ≥‘𝐾) ↦ 𝐶)) = (lim inf‘((𝑗 ∈ {𝑗 ∈ 𝐴 ∣ 𝐶 ∈ V} ↦ 𝐶) ↾
(ℤ≥‘𝐾)))) |
| 23 | 2, 3 | eluzelz2d 45424 |
. . . . 5
⊢ (𝜑 → 𝐾 ∈ ℤ) |
| 24 | | eqid 2737 |
. . . . 5
⊢
(ℤ≥‘𝐾) = (ℤ≥‘𝐾) |
| 25 | | liminfequzmpt2.o |
. . . . . . . 8
⊢
Ⅎ𝑗𝐴 |
| 26 | 2 | fvexi 6920 |
. . . . . . . 8
⊢ 𝐴 ∈ V |
| 27 | 25, 26 | rabexf 45139 |
. . . . . . 7
⊢ {𝑗 ∈ 𝐴 ∣ 𝐶 ∈ V} ∈ V |
| 28 | 16, 27 | mptexf 45243 |
. . . . . 6
⊢ (𝑗 ∈ {𝑗 ∈ 𝐴 ∣ 𝐶 ∈ V} ↦ 𝐶) ∈ V |
| 29 | 28 | a1i 11 |
. . . . 5
⊢ (𝜑 → (𝑗 ∈ {𝑗 ∈ 𝐴 ∣ 𝐶 ∈ V} ↦ 𝐶) ∈ V) |
| 30 | | eqid 2737 |
. . . . . . . 8
⊢ (𝑗 ∈ {𝑗 ∈ 𝐴 ∣ 𝐶 ∈ V} ↦ 𝐶) = (𝑗 ∈ {𝑗 ∈ 𝐴 ∣ 𝐶 ∈ V} ↦ 𝐶) |
| 31 | 16, 30 | dmmptssf 45237 |
. . . . . . 7
⊢ dom
(𝑗 ∈ {𝑗 ∈ 𝐴 ∣ 𝐶 ∈ V} ↦ 𝐶) ⊆ {𝑗 ∈ 𝐴 ∣ 𝐶 ∈ V} |
| 32 | 25 | ssrab2f 45122 |
. . . . . . . 8
⊢ {𝑗 ∈ 𝐴 ∣ 𝐶 ∈ V} ⊆ 𝐴 |
| 33 | | uzssz 12899 |
. . . . . . . . 9
⊢
(ℤ≥‘𝑀) ⊆ ℤ |
| 34 | 2, 33 | eqsstri 4030 |
. . . . . . . 8
⊢ 𝐴 ⊆
ℤ |
| 35 | 32, 34 | sstri 3993 |
. . . . . . 7
⊢ {𝑗 ∈ 𝐴 ∣ 𝐶 ∈ V} ⊆ ℤ |
| 36 | 31, 35 | sstri 3993 |
. . . . . 6
⊢ dom
(𝑗 ∈ {𝑗 ∈ 𝐴 ∣ 𝐶 ∈ V} ↦ 𝐶) ⊆ ℤ |
| 37 | 36 | a1i 11 |
. . . . 5
⊢ (𝜑 → dom (𝑗 ∈ {𝑗 ∈ 𝐴 ∣ 𝐶 ∈ V} ↦ 𝐶) ⊆ ℤ) |
| 38 | 23, 24, 29, 37 | liminfresuz2 45802 |
. . . 4
⊢ (𝜑 → (lim inf‘((𝑗 ∈ {𝑗 ∈ 𝐴 ∣ 𝐶 ∈ V} ↦ 𝐶) ↾
(ℤ≥‘𝐾))) = (lim inf‘(𝑗 ∈ {𝑗 ∈ 𝐴 ∣ 𝐶 ∈ V} ↦ 𝐶))) |
| 39 | 22, 38 | eqtr2d 2778 |
. . 3
⊢ (𝜑 → (lim inf‘(𝑗 ∈ {𝑗 ∈ 𝐴 ∣ 𝐶 ∈ V} ↦ 𝐶)) = (lim inf‘(𝑗 ∈ (ℤ≥‘𝐾) ↦ 𝐶))) |
| 40 | | liminfequzmpt2.b |
. . . . . . . . . . . . . . 15
⊢ 𝐵 =
(ℤ≥‘𝑁) |
| 41 | | liminfequzmpt2.e |
. . . . . . . . . . . . . . 15
⊢ (𝜑 → 𝐾 ∈ 𝐵) |
| 42 | 40, 41 | uzssd2 45428 |
. . . . . . . . . . . . . 14
⊢ (𝜑 →
(ℤ≥‘𝐾) ⊆ 𝐵) |
| 43 | 42 | adantr 480 |
. . . . . . . . . . . . 13
⊢ ((𝜑 ∧ 𝑗 ∈ (ℤ≥‘𝐾)) →
(ℤ≥‘𝐾) ⊆ 𝐵) |
| 44 | 43, 6 | sseldd 3984 |
. . . . . . . . . . . 12
⊢ ((𝜑 ∧ 𝑗 ∈ (ℤ≥‘𝐾)) → 𝑗 ∈ 𝐵) |
| 45 | 44, 9 | jca 511 |
. . . . . . . . . . 11
⊢ ((𝜑 ∧ 𝑗 ∈ (ℤ≥‘𝐾)) → (𝑗 ∈ 𝐵 ∧ 𝐶 ∈ V)) |
| 46 | | rabid 3458 |
. . . . . . . . . . 11
⊢ (𝑗 ∈ {𝑗 ∈ 𝐵 ∣ 𝐶 ∈ V} ↔ (𝑗 ∈ 𝐵 ∧ 𝐶 ∈ V)) |
| 47 | 45, 46 | sylibr 234 |
. . . . . . . . . 10
⊢ ((𝜑 ∧ 𝑗 ∈ (ℤ≥‘𝐾)) → 𝑗 ∈ {𝑗 ∈ 𝐵 ∣ 𝐶 ∈ V}) |
| 48 | 47 | ex 412 |
. . . . . . . . 9
⊢ (𝜑 → (𝑗 ∈ (ℤ≥‘𝐾) → 𝑗 ∈ {𝑗 ∈ 𝐵 ∣ 𝐶 ∈ V})) |
| 49 | 1, 48 | ralrimi 3257 |
. . . . . . . 8
⊢ (𝜑 → ∀𝑗 ∈ (ℤ≥‘𝐾)𝑗 ∈ {𝑗 ∈ 𝐵 ∣ 𝐶 ∈ V}) |
| 50 | | nfrab1 3457 |
. . . . . . . . 9
⊢
Ⅎ𝑗{𝑗 ∈ 𝐵 ∣ 𝐶 ∈ V} |
| 51 | 15, 50 | dfss3f 3975 |
. . . . . . . 8
⊢
((ℤ≥‘𝐾) ⊆ {𝑗 ∈ 𝐵 ∣ 𝐶 ∈ V} ↔ ∀𝑗 ∈ (ℤ≥‘𝐾)𝑗 ∈ {𝑗 ∈ 𝐵 ∣ 𝐶 ∈ V}) |
| 52 | 49, 51 | sylibr 234 |
. . . . . . 7
⊢ (𝜑 →
(ℤ≥‘𝐾) ⊆ {𝑗 ∈ 𝐵 ∣ 𝐶 ∈ V}) |
| 53 | 50, 15 | resmptf 6057 |
. . . . . . 7
⊢
((ℤ≥‘𝐾) ⊆ {𝑗 ∈ 𝐵 ∣ 𝐶 ∈ V} → ((𝑗 ∈ {𝑗 ∈ 𝐵 ∣ 𝐶 ∈ V} ↦ 𝐶) ↾
(ℤ≥‘𝐾)) = (𝑗 ∈ (ℤ≥‘𝐾) ↦ 𝐶)) |
| 54 | 52, 53 | syl 17 |
. . . . . 6
⊢ (𝜑 → ((𝑗 ∈ {𝑗 ∈ 𝐵 ∣ 𝐶 ∈ V} ↦ 𝐶) ↾
(ℤ≥‘𝐾)) = (𝑗 ∈ (ℤ≥‘𝐾) ↦ 𝐶)) |
| 55 | 54 | eqcomd 2743 |
. . . . 5
⊢ (𝜑 → (𝑗 ∈ (ℤ≥‘𝐾) ↦ 𝐶) = ((𝑗 ∈ {𝑗 ∈ 𝐵 ∣ 𝐶 ∈ V} ↦ 𝐶) ↾
(ℤ≥‘𝐾))) |
| 56 | 55 | fveq2d 6910 |
. . . 4
⊢ (𝜑 → (lim inf‘(𝑗 ∈
(ℤ≥‘𝐾) ↦ 𝐶)) = (lim inf‘((𝑗 ∈ {𝑗 ∈ 𝐵 ∣ 𝐶 ∈ V} ↦ 𝐶) ↾
(ℤ≥‘𝐾)))) |
| 57 | | liminfequzmpt2.p |
. . . . . . . 8
⊢
Ⅎ𝑗𝐵 |
| 58 | 40 | fvexi 6920 |
. . . . . . . 8
⊢ 𝐵 ∈ V |
| 59 | 57, 58 | rabexf 45139 |
. . . . . . 7
⊢ {𝑗 ∈ 𝐵 ∣ 𝐶 ∈ V} ∈ V |
| 60 | 50, 59 | mptexf 45243 |
. . . . . 6
⊢ (𝑗 ∈ {𝑗 ∈ 𝐵 ∣ 𝐶 ∈ V} ↦ 𝐶) ∈ V |
| 61 | 60 | a1i 11 |
. . . . 5
⊢ (𝜑 → (𝑗 ∈ {𝑗 ∈ 𝐵 ∣ 𝐶 ∈ V} ↦ 𝐶) ∈ V) |
| 62 | | eqid 2737 |
. . . . . . . 8
⊢ (𝑗 ∈ {𝑗 ∈ 𝐵 ∣ 𝐶 ∈ V} ↦ 𝐶) = (𝑗 ∈ {𝑗 ∈ 𝐵 ∣ 𝐶 ∈ V} ↦ 𝐶) |
| 63 | 50, 62 | dmmptssf 45237 |
. . . . . . 7
⊢ dom
(𝑗 ∈ {𝑗 ∈ 𝐵 ∣ 𝐶 ∈ V} ↦ 𝐶) ⊆ {𝑗 ∈ 𝐵 ∣ 𝐶 ∈ V} |
| 64 | 57 | ssrab2f 45122 |
. . . . . . . 8
⊢ {𝑗 ∈ 𝐵 ∣ 𝐶 ∈ V} ⊆ 𝐵 |
| 65 | | uzssz 12899 |
. . . . . . . . 9
⊢
(ℤ≥‘𝑁) ⊆ ℤ |
| 66 | 40, 65 | eqsstri 4030 |
. . . . . . . 8
⊢ 𝐵 ⊆
ℤ |
| 67 | 64, 66 | sstri 3993 |
. . . . . . 7
⊢ {𝑗 ∈ 𝐵 ∣ 𝐶 ∈ V} ⊆ ℤ |
| 68 | 63, 67 | sstri 3993 |
. . . . . 6
⊢ dom
(𝑗 ∈ {𝑗 ∈ 𝐵 ∣ 𝐶 ∈ V} ↦ 𝐶) ⊆ ℤ |
| 69 | 68 | a1i 11 |
. . . . 5
⊢ (𝜑 → dom (𝑗 ∈ {𝑗 ∈ 𝐵 ∣ 𝐶 ∈ V} ↦ 𝐶) ⊆ ℤ) |
| 70 | 23, 24, 61, 69 | liminfresuz2 45802 |
. . . 4
⊢ (𝜑 → (lim inf‘((𝑗 ∈ {𝑗 ∈ 𝐵 ∣ 𝐶 ∈ V} ↦ 𝐶) ↾
(ℤ≥‘𝐾))) = (lim inf‘(𝑗 ∈ {𝑗 ∈ 𝐵 ∣ 𝐶 ∈ V} ↦ 𝐶))) |
| 71 | 56, 70 | eqtr2d 2778 |
. . 3
⊢ (𝜑 → (lim inf‘(𝑗 ∈ {𝑗 ∈ 𝐵 ∣ 𝐶 ∈ V} ↦ 𝐶)) = (lim inf‘(𝑗 ∈ (ℤ≥‘𝐾) ↦ 𝐶))) |
| 72 | 39, 71 | eqtr4d 2780 |
. 2
⊢ (𝜑 → (lim inf‘(𝑗 ∈ {𝑗 ∈ 𝐴 ∣ 𝐶 ∈ V} ↦ 𝐶)) = (lim inf‘(𝑗 ∈ {𝑗 ∈ 𝐵 ∣ 𝐶 ∈ V} ↦ 𝐶))) |
| 73 | | eqid 2737 |
. . . . 5
⊢ {𝑗 ∈ 𝐴 ∣ 𝐶 ∈ V} = {𝑗 ∈ 𝐴 ∣ 𝐶 ∈ V} |
| 74 | 25, 73 | mptssid 45247 |
. . . 4
⊢ (𝑗 ∈ 𝐴 ↦ 𝐶) = (𝑗 ∈ {𝑗 ∈ 𝐴 ∣ 𝐶 ∈ V} ↦ 𝐶) |
| 75 | 74 | fveq2i 6909 |
. . 3
⊢ (lim
inf‘(𝑗 ∈ 𝐴 ↦ 𝐶)) = (lim inf‘(𝑗 ∈ {𝑗 ∈ 𝐴 ∣ 𝐶 ∈ V} ↦ 𝐶)) |
| 76 | 75 | a1i 11 |
. 2
⊢ (𝜑 → (lim inf‘(𝑗 ∈ 𝐴 ↦ 𝐶)) = (lim inf‘(𝑗 ∈ {𝑗 ∈ 𝐴 ∣ 𝐶 ∈ V} ↦ 𝐶))) |
| 77 | | eqid 2737 |
. . . . 5
⊢ {𝑗 ∈ 𝐵 ∣ 𝐶 ∈ V} = {𝑗 ∈ 𝐵 ∣ 𝐶 ∈ V} |
| 78 | 57, 77 | mptssid 45247 |
. . . 4
⊢ (𝑗 ∈ 𝐵 ↦ 𝐶) = (𝑗 ∈ {𝑗 ∈ 𝐵 ∣ 𝐶 ∈ V} ↦ 𝐶) |
| 79 | 78 | fveq2i 6909 |
. . 3
⊢ (lim
inf‘(𝑗 ∈ 𝐵 ↦ 𝐶)) = (lim inf‘(𝑗 ∈ {𝑗 ∈ 𝐵 ∣ 𝐶 ∈ V} ↦ 𝐶)) |
| 80 | 79 | a1i 11 |
. 2
⊢ (𝜑 → (lim inf‘(𝑗 ∈ 𝐵 ↦ 𝐶)) = (lim inf‘(𝑗 ∈ {𝑗 ∈ 𝐵 ∣ 𝐶 ∈ V} ↦ 𝐶))) |
| 81 | 72, 76, 80 | 3eqtr4d 2787 |
1
⊢ (𝜑 → (lim inf‘(𝑗 ∈ 𝐴 ↦ 𝐶)) = (lim inf‘(𝑗 ∈ 𝐵 ↦ 𝐶))) |