Proof of Theorem smfliminfmpt
Step | Hyp | Ref
| Expression |
1 | | smfliminfmpt.g |
. . . 4
⊢ 𝐺 = (𝑥 ∈ 𝐷 ↦ (lim inf‘(𝑚 ∈ 𝑍 ↦ 𝐵))) |
2 | 1 | a1i 11 |
. . 3
⊢ (𝜑 → 𝐺 = (𝑥 ∈ 𝐷 ↦ (lim inf‘(𝑚 ∈ 𝑍 ↦ 𝐵)))) |
3 | | smfliminfmpt.x |
. . . 4
⊢
Ⅎ𝑥𝜑 |
4 | | smfliminfmpt.d |
. . . . . 6
⊢ 𝐷 = {𝑥 ∈ ∪
𝑛 ∈ 𝑍 ∩ 𝑚 ∈
(ℤ≥‘𝑛)𝐴 ∣ (lim inf‘(𝑚 ∈ 𝑍 ↦ 𝐵)) ∈ ℝ} |
5 | 4 | a1i 11 |
. . . . 5
⊢ (𝜑 → 𝐷 = {𝑥 ∈ ∪
𝑛 ∈ 𝑍 ∩ 𝑚 ∈
(ℤ≥‘𝑛)𝐴 ∣ (lim inf‘(𝑚 ∈ 𝑍 ↦ 𝐵)) ∈ ℝ}) |
6 | | simpr 477 |
. . . . . . . . . 10
⊢ ((𝜑 ∧ 𝑥 ∈ ∪
𝑛 ∈ 𝑍 ∩ 𝑚 ∈
(ℤ≥‘𝑛)𝐴) → 𝑥 ∈ ∪
𝑛 ∈ 𝑍 ∩ 𝑚 ∈
(ℤ≥‘𝑛)𝐴) |
7 | | smfliminfmpt.n |
. . . . . . . . . . . 12
⊢
Ⅎ𝑛𝜑 |
8 | | smfliminfmpt.p |
. . . . . . . . . . . . . 14
⊢
Ⅎ𝑚𝜑 |
9 | | nfv 1873 |
. . . . . . . . . . . . . 14
⊢
Ⅎ𝑚 𝑛 ∈ 𝑍 |
10 | 8, 9 | nfan 1862 |
. . . . . . . . . . . . 13
⊢
Ⅎ𝑚(𝜑 ∧ 𝑛 ∈ 𝑍) |
11 | | simpll 754 |
. . . . . . . . . . . . . 14
⊢ (((𝜑 ∧ 𝑛 ∈ 𝑍) ∧ 𝑚 ∈ (ℤ≥‘𝑛)) → 𝜑) |
12 | | smfliminfmpt.z |
. . . . . . . . . . . . . . . 16
⊢ 𝑍 =
(ℤ≥‘𝑀) |
13 | 12 | uztrn2 12076 |
. . . . . . . . . . . . . . 15
⊢ ((𝑛 ∈ 𝑍 ∧ 𝑚 ∈ (ℤ≥‘𝑛)) → 𝑚 ∈ 𝑍) |
14 | 13 | adantll 701 |
. . . . . . . . . . . . . 14
⊢ (((𝜑 ∧ 𝑛 ∈ 𝑍) ∧ 𝑚 ∈ (ℤ≥‘𝑛)) → 𝑚 ∈ 𝑍) |
15 | | simpr 477 |
. . . . . . . . . . . . . . . . 17
⊢ ((𝜑 ∧ 𝑚 ∈ 𝑍) → 𝑚 ∈ 𝑍) |
16 | | smfliminfmpt.f |
. . . . . . . . . . . . . . . . . 18
⊢ ((𝜑 ∧ 𝑚 ∈ 𝑍) → (𝑥 ∈ 𝐴 ↦ 𝐵) ∈ (SMblFn‘𝑆)) |
17 | 16 | elexd 3435 |
. . . . . . . . . . . . . . . . 17
⊢ ((𝜑 ∧ 𝑚 ∈ 𝑍) → (𝑥 ∈ 𝐴 ↦ 𝐵) ∈ V) |
18 | | eqid 2778 |
. . . . . . . . . . . . . . . . . 18
⊢ (𝑚 ∈ 𝑍 ↦ (𝑥 ∈ 𝐴 ↦ 𝐵)) = (𝑚 ∈ 𝑍 ↦ (𝑥 ∈ 𝐴 ↦ 𝐵)) |
19 | 18 | fvmpt2 6605 |
. . . . . . . . . . . . . . . . 17
⊢ ((𝑚 ∈ 𝑍 ∧ (𝑥 ∈ 𝐴 ↦ 𝐵) ∈ V) → ((𝑚 ∈ 𝑍 ↦ (𝑥 ∈ 𝐴 ↦ 𝐵))‘𝑚) = (𝑥 ∈ 𝐴 ↦ 𝐵)) |
20 | 15, 17, 19 | syl2anc 576 |
. . . . . . . . . . . . . . . 16
⊢ ((𝜑 ∧ 𝑚 ∈ 𝑍) → ((𝑚 ∈ 𝑍 ↦ (𝑥 ∈ 𝐴 ↦ 𝐵))‘𝑚) = (𝑥 ∈ 𝐴 ↦ 𝐵)) |
21 | 20 | dmeqd 5624 |
. . . . . . . . . . . . . . 15
⊢ ((𝜑 ∧ 𝑚 ∈ 𝑍) → dom ((𝑚 ∈ 𝑍 ↦ (𝑥 ∈ 𝐴 ↦ 𝐵))‘𝑚) = dom (𝑥 ∈ 𝐴 ↦ 𝐵)) |
22 | | nfv 1873 |
. . . . . . . . . . . . . . . . 17
⊢
Ⅎ𝑥 𝑚 ∈ 𝑍 |
23 | 3, 22 | nfan 1862 |
. . . . . . . . . . . . . . . 16
⊢
Ⅎ𝑥(𝜑 ∧ 𝑚 ∈ 𝑍) |
24 | | eqid 2778 |
. . . . . . . . . . . . . . . 16
⊢ (𝑥 ∈ 𝐴 ↦ 𝐵) = (𝑥 ∈ 𝐴 ↦ 𝐵) |
25 | | smfliminfmpt.b |
. . . . . . . . . . . . . . . . 17
⊢ ((𝜑 ∧ 𝑚 ∈ 𝑍 ∧ 𝑥 ∈ 𝐴) → 𝐵 ∈ 𝑉) |
26 | 25 | 3expa 1098 |
. . . . . . . . . . . . . . . 16
⊢ (((𝜑 ∧ 𝑚 ∈ 𝑍) ∧ 𝑥 ∈ 𝐴) → 𝐵 ∈ 𝑉) |
27 | 23, 24, 26 | dmmptdf 40919 |
. . . . . . . . . . . . . . 15
⊢ ((𝜑 ∧ 𝑚 ∈ 𝑍) → dom (𝑥 ∈ 𝐴 ↦ 𝐵) = 𝐴) |
28 | 21, 27 | eqtr2d 2815 |
. . . . . . . . . . . . . 14
⊢ ((𝜑 ∧ 𝑚 ∈ 𝑍) → 𝐴 = dom ((𝑚 ∈ 𝑍 ↦ (𝑥 ∈ 𝐴 ↦ 𝐵))‘𝑚)) |
29 | 11, 14, 28 | syl2anc 576 |
. . . . . . . . . . . . 13
⊢ (((𝜑 ∧ 𝑛 ∈ 𝑍) ∧ 𝑚 ∈ (ℤ≥‘𝑛)) → 𝐴 = dom ((𝑚 ∈ 𝑍 ↦ (𝑥 ∈ 𝐴 ↦ 𝐵))‘𝑚)) |
30 | 10, 29 | iineq2d 4814 |
. . . . . . . . . . . 12
⊢ ((𝜑 ∧ 𝑛 ∈ 𝑍) → ∩
𝑚 ∈
(ℤ≥‘𝑛)𝐴 = ∩ 𝑚 ∈
(ℤ≥‘𝑛)dom ((𝑚 ∈ 𝑍 ↦ (𝑥 ∈ 𝐴 ↦ 𝐵))‘𝑚)) |
31 | 7, 30 | iuneq2df 40733 |
. . . . . . . . . . 11
⊢ (𝜑 → ∪ 𝑛 ∈ 𝑍 ∩ 𝑚 ∈
(ℤ≥‘𝑛)𝐴 = ∪ 𝑛 ∈ 𝑍 ∩ 𝑚 ∈
(ℤ≥‘𝑛)dom ((𝑚 ∈ 𝑍 ↦ (𝑥 ∈ 𝐴 ↦ 𝐵))‘𝑚)) |
32 | 31 | adantr 473 |
. . . . . . . . . 10
⊢ ((𝜑 ∧ 𝑥 ∈ ∪
𝑛 ∈ 𝑍 ∩ 𝑚 ∈
(ℤ≥‘𝑛)𝐴) → ∪
𝑛 ∈ 𝑍 ∩ 𝑚 ∈
(ℤ≥‘𝑛)𝐴 = ∪ 𝑛 ∈ 𝑍 ∩ 𝑚 ∈
(ℤ≥‘𝑛)dom ((𝑚 ∈ 𝑍 ↦ (𝑥 ∈ 𝐴 ↦ 𝐵))‘𝑚)) |
33 | 6, 32 | eleqtrd 2868 |
. . . . . . . . 9
⊢ ((𝜑 ∧ 𝑥 ∈ ∪
𝑛 ∈ 𝑍 ∩ 𝑚 ∈
(ℤ≥‘𝑛)𝐴) → 𝑥 ∈ ∪
𝑛 ∈ 𝑍 ∩ 𝑚 ∈
(ℤ≥‘𝑛)dom ((𝑚 ∈ 𝑍 ↦ (𝑥 ∈ 𝐴 ↦ 𝐵))‘𝑚)) |
34 | 33 | adantrr 704 |
. . . . . . . 8
⊢ ((𝜑 ∧ (𝑥 ∈ ∪
𝑛 ∈ 𝑍 ∩ 𝑚 ∈
(ℤ≥‘𝑛)𝐴 ∧ (lim inf‘(𝑚 ∈ 𝑍 ↦ 𝐵)) ∈ ℝ)) → 𝑥 ∈ ∪ 𝑛 ∈ 𝑍 ∩ 𝑚 ∈
(ℤ≥‘𝑛)dom ((𝑚 ∈ 𝑍 ↦ (𝑥 ∈ 𝐴 ↦ 𝐵))‘𝑚)) |
35 | | eliun 4796 |
. . . . . . . . . . . . 13
⊢ (𝑥 ∈ ∪ 𝑛 ∈ 𝑍 ∩ 𝑚 ∈
(ℤ≥‘𝑛)𝐴 ↔ ∃𝑛 ∈ 𝑍 𝑥 ∈ ∩
𝑚 ∈
(ℤ≥‘𝑛)𝐴) |
36 | 35 | biimpi 208 |
. . . . . . . . . . . 12
⊢ (𝑥 ∈ ∪ 𝑛 ∈ 𝑍 ∩ 𝑚 ∈
(ℤ≥‘𝑛)𝐴 → ∃𝑛 ∈ 𝑍 𝑥 ∈ ∩
𝑚 ∈
(ℤ≥‘𝑛)𝐴) |
37 | 36 | adantl 474 |
. . . . . . . . . . 11
⊢ ((𝜑 ∧ 𝑥 ∈ ∪
𝑛 ∈ 𝑍 ∩ 𝑚 ∈
(ℤ≥‘𝑛)𝐴) → ∃𝑛 ∈ 𝑍 𝑥 ∈ ∩
𝑚 ∈
(ℤ≥‘𝑛)𝐴) |
38 | | nfv 1873 |
. . . . . . . . . . . . 13
⊢
Ⅎ𝑛(lim
inf‘(𝑚 ∈ 𝑍 ↦ (((𝑚 ∈ 𝑍 ↦ (𝑥 ∈ 𝐴 ↦ 𝐵))‘𝑚)‘𝑥))) = (lim inf‘(𝑚 ∈ 𝑍 ↦ 𝐵)) |
39 | | nfcv 2932 |
. . . . . . . . . . . . . . . . . . 19
⊢
Ⅎ𝑚𝑥 |
40 | | nfii1 4824 |
. . . . . . . . . . . . . . . . . . 19
⊢
Ⅎ𝑚∩ 𝑚 ∈
(ℤ≥‘𝑛)𝐴 |
41 | 39, 40 | nfel 2944 |
. . . . . . . . . . . . . . . . . 18
⊢
Ⅎ𝑚 𝑥 ∈ ∩ 𝑚 ∈ (ℤ≥‘𝑛)𝐴 |
42 | 8, 9, 41 | nf3an 1864 |
. . . . . . . . . . . . . . . . 17
⊢
Ⅎ𝑚(𝜑 ∧ 𝑛 ∈ 𝑍 ∧ 𝑥 ∈ ∩
𝑚 ∈
(ℤ≥‘𝑛)𝐴) |
43 | 20 | fveq1d 6501 |
. . . . . . . . . . . . . . . . . . . 20
⊢ ((𝜑 ∧ 𝑚 ∈ 𝑍) → (((𝑚 ∈ 𝑍 ↦ (𝑥 ∈ 𝐴 ↦ 𝐵))‘𝑚)‘𝑥) = ((𝑥 ∈ 𝐴 ↦ 𝐵)‘𝑥)) |
44 | 11, 14, 43 | syl2anc 576 |
. . . . . . . . . . . . . . . . . . 19
⊢ (((𝜑 ∧ 𝑛 ∈ 𝑍) ∧ 𝑚 ∈ (ℤ≥‘𝑛)) → (((𝑚 ∈ 𝑍 ↦ (𝑥 ∈ 𝐴 ↦ 𝐵))‘𝑚)‘𝑥) = ((𝑥 ∈ 𝐴 ↦ 𝐵)‘𝑥)) |
45 | 44 | 3adantl3 1148 |
. . . . . . . . . . . . . . . . . 18
⊢ (((𝜑 ∧ 𝑛 ∈ 𝑍 ∧ 𝑥 ∈ ∩
𝑚 ∈
(ℤ≥‘𝑛)𝐴) ∧ 𝑚 ∈ (ℤ≥‘𝑛)) → (((𝑚 ∈ 𝑍 ↦ (𝑥 ∈ 𝐴 ↦ 𝐵))‘𝑚)‘𝑥) = ((𝑥 ∈ 𝐴 ↦ 𝐵)‘𝑥)) |
46 | | eliinid 40806 |
. . . . . . . . . . . . . . . . . . . 20
⊢ ((𝑥 ∈ ∩ 𝑚 ∈ (ℤ≥‘𝑛)𝐴 ∧ 𝑚 ∈ (ℤ≥‘𝑛)) → 𝑥 ∈ 𝐴) |
47 | 46 | 3ad2antl3 1167 |
. . . . . . . . . . . . . . . . . . 19
⊢ (((𝜑 ∧ 𝑛 ∈ 𝑍 ∧ 𝑥 ∈ ∩
𝑚 ∈
(ℤ≥‘𝑛)𝐴) ∧ 𝑚 ∈ (ℤ≥‘𝑛)) → 𝑥 ∈ 𝐴) |
48 | | simpl1 1171 |
. . . . . . . . . . . . . . . . . . . 20
⊢ (((𝜑 ∧ 𝑛 ∈ 𝑍 ∧ 𝑥 ∈ ∩
𝑚 ∈
(ℤ≥‘𝑛)𝐴) ∧ 𝑚 ∈ (ℤ≥‘𝑛)) → 𝜑) |
49 | | simp2 1117 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ ((𝜑 ∧ 𝑛 ∈ 𝑍 ∧ 𝑥 ∈ ∩
𝑚 ∈
(ℤ≥‘𝑛)𝐴) → 𝑛 ∈ 𝑍) |
50 | 49, 13 | sylan 572 |
. . . . . . . . . . . . . . . . . . . 20
⊢ (((𝜑 ∧ 𝑛 ∈ 𝑍 ∧ 𝑥 ∈ ∩
𝑚 ∈
(ℤ≥‘𝑛)𝐴) ∧ 𝑚 ∈ (ℤ≥‘𝑛)) → 𝑚 ∈ 𝑍) |
51 | 48, 50, 47, 25 | syl3anc 1351 |
. . . . . . . . . . . . . . . . . . 19
⊢ (((𝜑 ∧ 𝑛 ∈ 𝑍 ∧ 𝑥 ∈ ∩
𝑚 ∈
(ℤ≥‘𝑛)𝐴) ∧ 𝑚 ∈ (ℤ≥‘𝑛)) → 𝐵 ∈ 𝑉) |
52 | 24 | fvmpt2 6605 |
. . . . . . . . . . . . . . . . . . 19
⊢ ((𝑥 ∈ 𝐴 ∧ 𝐵 ∈ 𝑉) → ((𝑥 ∈ 𝐴 ↦ 𝐵)‘𝑥) = 𝐵) |
53 | 47, 51, 52 | syl2anc 576 |
. . . . . . . . . . . . . . . . . 18
⊢ (((𝜑 ∧ 𝑛 ∈ 𝑍 ∧ 𝑥 ∈ ∩
𝑚 ∈
(ℤ≥‘𝑛)𝐴) ∧ 𝑚 ∈ (ℤ≥‘𝑛)) → ((𝑥 ∈ 𝐴 ↦ 𝐵)‘𝑥) = 𝐵) |
54 | 45, 53 | eqtrd 2814 |
. . . . . . . . . . . . . . . . 17
⊢ (((𝜑 ∧ 𝑛 ∈ 𝑍 ∧ 𝑥 ∈ ∩
𝑚 ∈
(ℤ≥‘𝑛)𝐴) ∧ 𝑚 ∈ (ℤ≥‘𝑛)) → (((𝑚 ∈ 𝑍 ↦ (𝑥 ∈ 𝐴 ↦ 𝐵))‘𝑚)‘𝑥) = 𝐵) |
55 | 42, 54 | mpteq2da 5021 |
. . . . . . . . . . . . . . . 16
⊢ ((𝜑 ∧ 𝑛 ∈ 𝑍 ∧ 𝑥 ∈ ∩
𝑚 ∈
(ℤ≥‘𝑛)𝐴) → (𝑚 ∈ (ℤ≥‘𝑛) ↦ (((𝑚 ∈ 𝑍 ↦ (𝑥 ∈ 𝐴 ↦ 𝐵))‘𝑚)‘𝑥)) = (𝑚 ∈ (ℤ≥‘𝑛) ↦ 𝐵)) |
56 | 55 | fveq2d 6503 |
. . . . . . . . . . . . . . 15
⊢ ((𝜑 ∧ 𝑛 ∈ 𝑍 ∧ 𝑥 ∈ ∩
𝑚 ∈
(ℤ≥‘𝑛)𝐴) → (lim inf‘(𝑚 ∈ (ℤ≥‘𝑛) ↦ (((𝑚 ∈ 𝑍 ↦ (𝑥 ∈ 𝐴 ↦ 𝐵))‘𝑚)‘𝑥))) = (lim inf‘(𝑚 ∈ (ℤ≥‘𝑛) ↦ 𝐵))) |
57 | | nfcv 2932 |
. . . . . . . . . . . . . . . 16
⊢
Ⅎ𝑚𝑍 |
58 | | nfcv 2932 |
. . . . . . . . . . . . . . . 16
⊢
Ⅎ𝑚(ℤ≥‘𝑛) |
59 | | eqid 2778 |
. . . . . . . . . . . . . . . 16
⊢
(ℤ≥‘𝑛) = (ℤ≥‘𝑛) |
60 | 12 | eluzelz2 41112 |
. . . . . . . . . . . . . . . . . 18
⊢ (𝑛 ∈ 𝑍 → 𝑛 ∈ ℤ) |
61 | 60 | uzidd 41115 |
. . . . . . . . . . . . . . . . 17
⊢ (𝑛 ∈ 𝑍 → 𝑛 ∈ (ℤ≥‘𝑛)) |
62 | 61 | 3ad2ant2 1114 |
. . . . . . . . . . . . . . . 16
⊢ ((𝜑 ∧ 𝑛 ∈ 𝑍 ∧ 𝑥 ∈ ∩
𝑚 ∈
(ℤ≥‘𝑛)𝐴) → 𝑛 ∈ (ℤ≥‘𝑛)) |
63 | | fvexd 6514 |
. . . . . . . . . . . . . . . 16
⊢ (((𝜑 ∧ 𝑛 ∈ 𝑍 ∧ 𝑥 ∈ ∩
𝑚 ∈
(ℤ≥‘𝑛)𝐴) ∧ 𝑚 ∈ (ℤ≥‘𝑛)) → (((𝑚 ∈ 𝑍 ↦ (𝑥 ∈ 𝐴 ↦ 𝐵))‘𝑚)‘𝑥) ∈ V) |
64 | 42, 57, 58, 12, 59, 49, 62, 63 | liminfequzmpt2 41509 |
. . . . . . . . . . . . . . 15
⊢ ((𝜑 ∧ 𝑛 ∈ 𝑍 ∧ 𝑥 ∈ ∩
𝑚 ∈
(ℤ≥‘𝑛)𝐴) → (lim inf‘(𝑚 ∈ 𝑍 ↦ (((𝑚 ∈ 𝑍 ↦ (𝑥 ∈ 𝐴 ↦ 𝐵))‘𝑚)‘𝑥))) = (lim inf‘(𝑚 ∈ (ℤ≥‘𝑛) ↦ (((𝑚 ∈ 𝑍 ↦ (𝑥 ∈ 𝐴 ↦ 𝐵))‘𝑚)‘𝑥)))) |
65 | 42, 57, 58, 12, 59, 49, 62, 51 | liminfequzmpt2 41509 |
. . . . . . . . . . . . . . 15
⊢ ((𝜑 ∧ 𝑛 ∈ 𝑍 ∧ 𝑥 ∈ ∩
𝑚 ∈
(ℤ≥‘𝑛)𝐴) → (lim inf‘(𝑚 ∈ 𝑍 ↦ 𝐵)) = (lim inf‘(𝑚 ∈ (ℤ≥‘𝑛) ↦ 𝐵))) |
66 | 56, 64, 65 | 3eqtr4d 2824 |
. . . . . . . . . . . . . 14
⊢ ((𝜑 ∧ 𝑛 ∈ 𝑍 ∧ 𝑥 ∈ ∩
𝑚 ∈
(ℤ≥‘𝑛)𝐴) → (lim inf‘(𝑚 ∈ 𝑍 ↦ (((𝑚 ∈ 𝑍 ↦ (𝑥 ∈ 𝐴 ↦ 𝐵))‘𝑚)‘𝑥))) = (lim inf‘(𝑚 ∈ 𝑍 ↦ 𝐵))) |
67 | 66 | 3exp 1099 |
. . . . . . . . . . . . 13
⊢ (𝜑 → (𝑛 ∈ 𝑍 → (𝑥 ∈ ∩
𝑚 ∈
(ℤ≥‘𝑛)𝐴 → (lim inf‘(𝑚 ∈ 𝑍 ↦ (((𝑚 ∈ 𝑍 ↦ (𝑥 ∈ 𝐴 ↦ 𝐵))‘𝑚)‘𝑥))) = (lim inf‘(𝑚 ∈ 𝑍 ↦ 𝐵))))) |
68 | 7, 38, 67 | rexlimd 3260 |
. . . . . . . . . . . 12
⊢ (𝜑 → (∃𝑛 ∈ 𝑍 𝑥 ∈ ∩
𝑚 ∈
(ℤ≥‘𝑛)𝐴 → (lim inf‘(𝑚 ∈ 𝑍 ↦ (((𝑚 ∈ 𝑍 ↦ (𝑥 ∈ 𝐴 ↦ 𝐵))‘𝑚)‘𝑥))) = (lim inf‘(𝑚 ∈ 𝑍 ↦ 𝐵)))) |
69 | 68 | adantr 473 |
. . . . . . . . . . 11
⊢ ((𝜑 ∧ 𝑥 ∈ ∪
𝑛 ∈ 𝑍 ∩ 𝑚 ∈
(ℤ≥‘𝑛)𝐴) → (∃𝑛 ∈ 𝑍 𝑥 ∈ ∩
𝑚 ∈
(ℤ≥‘𝑛)𝐴 → (lim inf‘(𝑚 ∈ 𝑍 ↦ (((𝑚 ∈ 𝑍 ↦ (𝑥 ∈ 𝐴 ↦ 𝐵))‘𝑚)‘𝑥))) = (lim inf‘(𝑚 ∈ 𝑍 ↦ 𝐵)))) |
70 | 37, 69 | mpd 15 |
. . . . . . . . . 10
⊢ ((𝜑 ∧ 𝑥 ∈ ∪
𝑛 ∈ 𝑍 ∩ 𝑚 ∈
(ℤ≥‘𝑛)𝐴) → (lim inf‘(𝑚 ∈ 𝑍 ↦ (((𝑚 ∈ 𝑍 ↦ (𝑥 ∈ 𝐴 ↦ 𝐵))‘𝑚)‘𝑥))) = (lim inf‘(𝑚 ∈ 𝑍 ↦ 𝐵))) |
71 | 70 | adantrr 704 |
. . . . . . . . 9
⊢ ((𝜑 ∧ (𝑥 ∈ ∪
𝑛 ∈ 𝑍 ∩ 𝑚 ∈
(ℤ≥‘𝑛)𝐴 ∧ (lim inf‘(𝑚 ∈ 𝑍 ↦ 𝐵)) ∈ ℝ)) → (lim
inf‘(𝑚 ∈ 𝑍 ↦ (((𝑚 ∈ 𝑍 ↦ (𝑥 ∈ 𝐴 ↦ 𝐵))‘𝑚)‘𝑥))) = (lim inf‘(𝑚 ∈ 𝑍 ↦ 𝐵))) |
72 | | simprr 760 |
. . . . . . . . 9
⊢ ((𝜑 ∧ (𝑥 ∈ ∪
𝑛 ∈ 𝑍 ∩ 𝑚 ∈
(ℤ≥‘𝑛)𝐴 ∧ (lim inf‘(𝑚 ∈ 𝑍 ↦ 𝐵)) ∈ ℝ)) → (lim
inf‘(𝑚 ∈ 𝑍 ↦ 𝐵)) ∈ ℝ) |
73 | 71, 72 | eqeltrd 2866 |
. . . . . . . 8
⊢ ((𝜑 ∧ (𝑥 ∈ ∪
𝑛 ∈ 𝑍 ∩ 𝑚 ∈
(ℤ≥‘𝑛)𝐴 ∧ (lim inf‘(𝑚 ∈ 𝑍 ↦ 𝐵)) ∈ ℝ)) → (lim
inf‘(𝑚 ∈ 𝑍 ↦ (((𝑚 ∈ 𝑍 ↦ (𝑥 ∈ 𝐴 ↦ 𝐵))‘𝑚)‘𝑥))) ∈ ℝ) |
74 | 34, 73 | jca 504 |
. . . . . . 7
⊢ ((𝜑 ∧ (𝑥 ∈ ∪
𝑛 ∈ 𝑍 ∩ 𝑚 ∈
(ℤ≥‘𝑛)𝐴 ∧ (lim inf‘(𝑚 ∈ 𝑍 ↦ 𝐵)) ∈ ℝ)) → (𝑥 ∈ ∪ 𝑛 ∈ 𝑍 ∩ 𝑚 ∈
(ℤ≥‘𝑛)dom ((𝑚 ∈ 𝑍 ↦ (𝑥 ∈ 𝐴 ↦ 𝐵))‘𝑚) ∧ (lim inf‘(𝑚 ∈ 𝑍 ↦ (((𝑚 ∈ 𝑍 ↦ (𝑥 ∈ 𝐴 ↦ 𝐵))‘𝑚)‘𝑥))) ∈ ℝ)) |
75 | | simpl 475 |
. . . . . . . 8
⊢ ((𝜑 ∧ (𝑥 ∈ ∪
𝑛 ∈ 𝑍 ∩ 𝑚 ∈
(ℤ≥‘𝑛)dom ((𝑚 ∈ 𝑍 ↦ (𝑥 ∈ 𝐴 ↦ 𝐵))‘𝑚) ∧ (lim inf‘(𝑚 ∈ 𝑍 ↦ (((𝑚 ∈ 𝑍 ↦ (𝑥 ∈ 𝐴 ↦ 𝐵))‘𝑚)‘𝑥))) ∈ ℝ)) → 𝜑) |
76 | | simpr 477 |
. . . . . . . . . 10
⊢ ((𝜑 ∧ 𝑥 ∈ ∪
𝑛 ∈ 𝑍 ∩ 𝑚 ∈
(ℤ≥‘𝑛)dom ((𝑚 ∈ 𝑍 ↦ (𝑥 ∈ 𝐴 ↦ 𝐵))‘𝑚)) → 𝑥 ∈ ∪
𝑛 ∈ 𝑍 ∩ 𝑚 ∈
(ℤ≥‘𝑛)dom ((𝑚 ∈ 𝑍 ↦ (𝑥 ∈ 𝐴 ↦ 𝐵))‘𝑚)) |
77 | 31 | eqcomd 2784 |
. . . . . . . . . . 11
⊢ (𝜑 → ∪ 𝑛 ∈ 𝑍 ∩ 𝑚 ∈
(ℤ≥‘𝑛)dom ((𝑚 ∈ 𝑍 ↦ (𝑥 ∈ 𝐴 ↦ 𝐵))‘𝑚) = ∪ 𝑛 ∈ 𝑍 ∩ 𝑚 ∈
(ℤ≥‘𝑛)𝐴) |
78 | 77 | adantr 473 |
. . . . . . . . . 10
⊢ ((𝜑 ∧ 𝑥 ∈ ∪
𝑛 ∈ 𝑍 ∩ 𝑚 ∈
(ℤ≥‘𝑛)dom ((𝑚 ∈ 𝑍 ↦ (𝑥 ∈ 𝐴 ↦ 𝐵))‘𝑚)) → ∪
𝑛 ∈ 𝑍 ∩ 𝑚 ∈
(ℤ≥‘𝑛)dom ((𝑚 ∈ 𝑍 ↦ (𝑥 ∈ 𝐴 ↦ 𝐵))‘𝑚) = ∪ 𝑛 ∈ 𝑍 ∩ 𝑚 ∈
(ℤ≥‘𝑛)𝐴) |
79 | 76, 78 | eleqtrd 2868 |
. . . . . . . . 9
⊢ ((𝜑 ∧ 𝑥 ∈ ∪
𝑛 ∈ 𝑍 ∩ 𝑚 ∈
(ℤ≥‘𝑛)dom ((𝑚 ∈ 𝑍 ↦ (𝑥 ∈ 𝐴 ↦ 𝐵))‘𝑚)) → 𝑥 ∈ ∪
𝑛 ∈ 𝑍 ∩ 𝑚 ∈
(ℤ≥‘𝑛)𝐴) |
80 | 79 | adantrr 704 |
. . . . . . . 8
⊢ ((𝜑 ∧ (𝑥 ∈ ∪
𝑛 ∈ 𝑍 ∩ 𝑚 ∈
(ℤ≥‘𝑛)dom ((𝑚 ∈ 𝑍 ↦ (𝑥 ∈ 𝐴 ↦ 𝐵))‘𝑚) ∧ (lim inf‘(𝑚 ∈ 𝑍 ↦ (((𝑚 ∈ 𝑍 ↦ (𝑥 ∈ 𝐴 ↦ 𝐵))‘𝑚)‘𝑥))) ∈ ℝ)) → 𝑥 ∈ ∪ 𝑛 ∈ 𝑍 ∩ 𝑚 ∈
(ℤ≥‘𝑛)𝐴) |
81 | | simprr 760 |
. . . . . . . 8
⊢ ((𝜑 ∧ (𝑥 ∈ ∪
𝑛 ∈ 𝑍 ∩ 𝑚 ∈
(ℤ≥‘𝑛)dom ((𝑚 ∈ 𝑍 ↦ (𝑥 ∈ 𝐴 ↦ 𝐵))‘𝑚) ∧ (lim inf‘(𝑚 ∈ 𝑍 ↦ (((𝑚 ∈ 𝑍 ↦ (𝑥 ∈ 𝐴 ↦ 𝐵))‘𝑚)‘𝑥))) ∈ ℝ)) → (lim
inf‘(𝑚 ∈ 𝑍 ↦ (((𝑚 ∈ 𝑍 ↦ (𝑥 ∈ 𝐴 ↦ 𝐵))‘𝑚)‘𝑥))) ∈ ℝ) |
82 | | simp2 1117 |
. . . . . . . . 9
⊢ ((𝜑 ∧ 𝑥 ∈ ∪
𝑛 ∈ 𝑍 ∩ 𝑚 ∈
(ℤ≥‘𝑛)𝐴 ∧ (lim inf‘(𝑚 ∈ 𝑍 ↦ (((𝑚 ∈ 𝑍 ↦ (𝑥 ∈ 𝐴 ↦ 𝐵))‘𝑚)‘𝑥))) ∈ ℝ) → 𝑥 ∈ ∪
𝑛 ∈ 𝑍 ∩ 𝑚 ∈
(ℤ≥‘𝑛)𝐴) |
83 | 70 | eqcomd 2784 |
. . . . . . . . . . 11
⊢ ((𝜑 ∧ 𝑥 ∈ ∪
𝑛 ∈ 𝑍 ∩ 𝑚 ∈
(ℤ≥‘𝑛)𝐴) → (lim inf‘(𝑚 ∈ 𝑍 ↦ 𝐵)) = (lim inf‘(𝑚 ∈ 𝑍 ↦ (((𝑚 ∈ 𝑍 ↦ (𝑥 ∈ 𝐴 ↦ 𝐵))‘𝑚)‘𝑥)))) |
84 | 83 | 3adant3 1112 |
. . . . . . . . . 10
⊢ ((𝜑 ∧ 𝑥 ∈ ∪
𝑛 ∈ 𝑍 ∩ 𝑚 ∈
(ℤ≥‘𝑛)𝐴 ∧ (lim inf‘(𝑚 ∈ 𝑍 ↦ (((𝑚 ∈ 𝑍 ↦ (𝑥 ∈ 𝐴 ↦ 𝐵))‘𝑚)‘𝑥))) ∈ ℝ) → (lim
inf‘(𝑚 ∈ 𝑍 ↦ 𝐵)) = (lim inf‘(𝑚 ∈ 𝑍 ↦ (((𝑚 ∈ 𝑍 ↦ (𝑥 ∈ 𝐴 ↦ 𝐵))‘𝑚)‘𝑥)))) |
85 | | simp3 1118 |
. . . . . . . . . 10
⊢ ((𝜑 ∧ 𝑥 ∈ ∪
𝑛 ∈ 𝑍 ∩ 𝑚 ∈
(ℤ≥‘𝑛)𝐴 ∧ (lim inf‘(𝑚 ∈ 𝑍 ↦ (((𝑚 ∈ 𝑍 ↦ (𝑥 ∈ 𝐴 ↦ 𝐵))‘𝑚)‘𝑥))) ∈ ℝ) → (lim
inf‘(𝑚 ∈ 𝑍 ↦ (((𝑚 ∈ 𝑍 ↦ (𝑥 ∈ 𝐴 ↦ 𝐵))‘𝑚)‘𝑥))) ∈ ℝ) |
86 | 84, 85 | eqeltrd 2866 |
. . . . . . . . 9
⊢ ((𝜑 ∧ 𝑥 ∈ ∪
𝑛 ∈ 𝑍 ∩ 𝑚 ∈
(ℤ≥‘𝑛)𝐴 ∧ (lim inf‘(𝑚 ∈ 𝑍 ↦ (((𝑚 ∈ 𝑍 ↦ (𝑥 ∈ 𝐴 ↦ 𝐵))‘𝑚)‘𝑥))) ∈ ℝ) → (lim
inf‘(𝑚 ∈ 𝑍 ↦ 𝐵)) ∈ ℝ) |
87 | 82, 86 | jca 504 |
. . . . . . . 8
⊢ ((𝜑 ∧ 𝑥 ∈ ∪
𝑛 ∈ 𝑍 ∩ 𝑚 ∈
(ℤ≥‘𝑛)𝐴 ∧ (lim inf‘(𝑚 ∈ 𝑍 ↦ (((𝑚 ∈ 𝑍 ↦ (𝑥 ∈ 𝐴 ↦ 𝐵))‘𝑚)‘𝑥))) ∈ ℝ) → (𝑥 ∈ ∪ 𝑛 ∈ 𝑍 ∩ 𝑚 ∈
(ℤ≥‘𝑛)𝐴 ∧ (lim inf‘(𝑚 ∈ 𝑍 ↦ 𝐵)) ∈ ℝ)) |
88 | 75, 80, 81, 87 | syl3anc 1351 |
. . . . . . 7
⊢ ((𝜑 ∧ (𝑥 ∈ ∪
𝑛 ∈ 𝑍 ∩ 𝑚 ∈
(ℤ≥‘𝑛)dom ((𝑚 ∈ 𝑍 ↦ (𝑥 ∈ 𝐴 ↦ 𝐵))‘𝑚) ∧ (lim inf‘(𝑚 ∈ 𝑍 ↦ (((𝑚 ∈ 𝑍 ↦ (𝑥 ∈ 𝐴 ↦ 𝐵))‘𝑚)‘𝑥))) ∈ ℝ)) → (𝑥 ∈ ∪ 𝑛 ∈ 𝑍 ∩ 𝑚 ∈
(ℤ≥‘𝑛)𝐴 ∧ (lim inf‘(𝑚 ∈ 𝑍 ↦ 𝐵)) ∈ ℝ)) |
89 | 74, 88 | impbida 788 |
. . . . . 6
⊢ (𝜑 → ((𝑥 ∈ ∪
𝑛 ∈ 𝑍 ∩ 𝑚 ∈
(ℤ≥‘𝑛)𝐴 ∧ (lim inf‘(𝑚 ∈ 𝑍 ↦ 𝐵)) ∈ ℝ) ↔ (𝑥 ∈ ∪ 𝑛 ∈ 𝑍 ∩ 𝑚 ∈
(ℤ≥‘𝑛)dom ((𝑚 ∈ 𝑍 ↦ (𝑥 ∈ 𝐴 ↦ 𝐵))‘𝑚) ∧ (lim inf‘(𝑚 ∈ 𝑍 ↦ (((𝑚 ∈ 𝑍 ↦ (𝑥 ∈ 𝐴 ↦ 𝐵))‘𝑚)‘𝑥))) ∈ ℝ))) |
90 | 3, 89 | rabbida3 40830 |
. . . . 5
⊢ (𝜑 → {𝑥 ∈ ∪
𝑛 ∈ 𝑍 ∩ 𝑚 ∈
(ℤ≥‘𝑛)𝐴 ∣ (lim inf‘(𝑚 ∈ 𝑍 ↦ 𝐵)) ∈ ℝ} = {𝑥 ∈ ∪
𝑛 ∈ 𝑍 ∩ 𝑚 ∈
(ℤ≥‘𝑛)dom ((𝑚 ∈ 𝑍 ↦ (𝑥 ∈ 𝐴 ↦ 𝐵))‘𝑚) ∣ (lim inf‘(𝑚 ∈ 𝑍 ↦ (((𝑚 ∈ 𝑍 ↦ (𝑥 ∈ 𝐴 ↦ 𝐵))‘𝑚)‘𝑥))) ∈ ℝ}) |
91 | 5, 90 | eqtrd 2814 |
. . . 4
⊢ (𝜑 → 𝐷 = {𝑥 ∈ ∪
𝑛 ∈ 𝑍 ∩ 𝑚 ∈
(ℤ≥‘𝑛)dom ((𝑚 ∈ 𝑍 ↦ (𝑥 ∈ 𝐴 ↦ 𝐵))‘𝑚) ∣ (lim inf‘(𝑚 ∈ 𝑍 ↦ (((𝑚 ∈ 𝑍 ↦ (𝑥 ∈ 𝐴 ↦ 𝐵))‘𝑚)‘𝑥))) ∈ ℝ}) |
92 | 4 | eleq2i 2857 |
. . . . . . 7
⊢ (𝑥 ∈ 𝐷 ↔ 𝑥 ∈ {𝑥 ∈ ∪
𝑛 ∈ 𝑍 ∩ 𝑚 ∈
(ℤ≥‘𝑛)𝐴 ∣ (lim inf‘(𝑚 ∈ 𝑍 ↦ 𝐵)) ∈ ℝ}) |
93 | 92 | biimpi 208 |
. . . . . 6
⊢ (𝑥 ∈ 𝐷 → 𝑥 ∈ {𝑥 ∈ ∪
𝑛 ∈ 𝑍 ∩ 𝑚 ∈
(ℤ≥‘𝑛)𝐴 ∣ (lim inf‘(𝑚 ∈ 𝑍 ↦ 𝐵)) ∈ ℝ}) |
94 | | rabidim1 3319 |
. . . . . 6
⊢ (𝑥 ∈ {𝑥 ∈ ∪
𝑛 ∈ 𝑍 ∩ 𝑚 ∈
(ℤ≥‘𝑛)𝐴 ∣ (lim inf‘(𝑚 ∈ 𝑍 ↦ 𝐵)) ∈ ℝ} → 𝑥 ∈ ∪
𝑛 ∈ 𝑍 ∩ 𝑚 ∈
(ℤ≥‘𝑛)𝐴) |
95 | 93, 94 | syl 17 |
. . . . 5
⊢ (𝑥 ∈ 𝐷 → 𝑥 ∈ ∪
𝑛 ∈ 𝑍 ∩ 𝑚 ∈
(ℤ≥‘𝑛)𝐴) |
96 | 95, 83 | sylan2 583 |
. . . 4
⊢ ((𝜑 ∧ 𝑥 ∈ 𝐷) → (lim inf‘(𝑚 ∈ 𝑍 ↦ 𝐵)) = (lim inf‘(𝑚 ∈ 𝑍 ↦ (((𝑚 ∈ 𝑍 ↦ (𝑥 ∈ 𝐴 ↦ 𝐵))‘𝑚)‘𝑥)))) |
97 | 3, 91, 96 | mpteq12da 40946 |
. . 3
⊢ (𝜑 → (𝑥 ∈ 𝐷 ↦ (lim inf‘(𝑚 ∈ 𝑍 ↦ 𝐵))) = (𝑥 ∈ {𝑥 ∈ ∪
𝑛 ∈ 𝑍 ∩ 𝑚 ∈
(ℤ≥‘𝑛)dom ((𝑚 ∈ 𝑍 ↦ (𝑥 ∈ 𝐴 ↦ 𝐵))‘𝑚) ∣ (lim inf‘(𝑚 ∈ 𝑍 ↦ (((𝑚 ∈ 𝑍 ↦ (𝑥 ∈ 𝐴 ↦ 𝐵))‘𝑚)‘𝑥))) ∈ ℝ} ↦ (lim
inf‘(𝑚 ∈ 𝑍 ↦ (((𝑚 ∈ 𝑍 ↦ (𝑥 ∈ 𝐴 ↦ 𝐵))‘𝑚)‘𝑥))))) |
98 | 2, 97 | eqtrd 2814 |
. 2
⊢ (𝜑 → 𝐺 = (𝑥 ∈ {𝑥 ∈ ∪
𝑛 ∈ 𝑍 ∩ 𝑚 ∈
(ℤ≥‘𝑛)dom ((𝑚 ∈ 𝑍 ↦ (𝑥 ∈ 𝐴 ↦ 𝐵))‘𝑚) ∣ (lim inf‘(𝑚 ∈ 𝑍 ↦ (((𝑚 ∈ 𝑍 ↦ (𝑥 ∈ 𝐴 ↦ 𝐵))‘𝑚)‘𝑥))) ∈ ℝ} ↦ (lim
inf‘(𝑚 ∈ 𝑍 ↦ (((𝑚 ∈ 𝑍 ↦ (𝑥 ∈ 𝐴 ↦ 𝐵))‘𝑚)‘𝑥))))) |
99 | | nfmpt1 5025 |
. . 3
⊢
Ⅎ𝑚(𝑚 ∈ 𝑍 ↦ (𝑥 ∈ 𝐴 ↦ 𝐵)) |
100 | | nfcv 2932 |
. . . 4
⊢
Ⅎ𝑥𝑍 |
101 | | nfmpt1 5025 |
. . . 4
⊢
Ⅎ𝑥(𝑥 ∈ 𝐴 ↦ 𝐵) |
102 | 100, 101 | nfmpt 5024 |
. . 3
⊢
Ⅎ𝑥(𝑚 ∈ 𝑍 ↦ (𝑥 ∈ 𝐴 ↦ 𝐵)) |
103 | | smfliminfmpt.m |
. . 3
⊢ (𝜑 → 𝑀 ∈ ℤ) |
104 | | smfliminfmpt.s |
. . 3
⊢ (𝜑 → 𝑆 ∈ SAlg) |
105 | 8, 16 | fmptd2f 40938 |
. . 3
⊢ (𝜑 → (𝑚 ∈ 𝑍 ↦ (𝑥 ∈ 𝐴 ↦ 𝐵)):𝑍⟶(SMblFn‘𝑆)) |
106 | | eqid 2778 |
. . 3
⊢ {𝑥 ∈ ∪ 𝑛 ∈ 𝑍 ∩ 𝑚 ∈
(ℤ≥‘𝑛)dom ((𝑚 ∈ 𝑍 ↦ (𝑥 ∈ 𝐴 ↦ 𝐵))‘𝑚) ∣ (lim inf‘(𝑚 ∈ 𝑍 ↦ (((𝑚 ∈ 𝑍 ↦ (𝑥 ∈ 𝐴 ↦ 𝐵))‘𝑚)‘𝑥))) ∈ ℝ} = {𝑥 ∈ ∪
𝑛 ∈ 𝑍 ∩ 𝑚 ∈
(ℤ≥‘𝑛)dom ((𝑚 ∈ 𝑍 ↦ (𝑥 ∈ 𝐴 ↦ 𝐵))‘𝑚) ∣ (lim inf‘(𝑚 ∈ 𝑍 ↦ (((𝑚 ∈ 𝑍 ↦ (𝑥 ∈ 𝐴 ↦ 𝐵))‘𝑚)‘𝑥))) ∈ ℝ} |
107 | | eqid 2778 |
. . 3
⊢ (𝑥 ∈ {𝑥 ∈ ∪
𝑛 ∈ 𝑍 ∩ 𝑚 ∈
(ℤ≥‘𝑛)dom ((𝑚 ∈ 𝑍 ↦ (𝑥 ∈ 𝐴 ↦ 𝐵))‘𝑚) ∣ (lim inf‘(𝑚 ∈ 𝑍 ↦ (((𝑚 ∈ 𝑍 ↦ (𝑥 ∈ 𝐴 ↦ 𝐵))‘𝑚)‘𝑥))) ∈ ℝ} ↦ (lim
inf‘(𝑚 ∈ 𝑍 ↦ (((𝑚 ∈ 𝑍 ↦ (𝑥 ∈ 𝐴 ↦ 𝐵))‘𝑚)‘𝑥)))) = (𝑥 ∈ {𝑥 ∈ ∪
𝑛 ∈ 𝑍 ∩ 𝑚 ∈
(ℤ≥‘𝑛)dom ((𝑚 ∈ 𝑍 ↦ (𝑥 ∈ 𝐴 ↦ 𝐵))‘𝑚) ∣ (lim inf‘(𝑚 ∈ 𝑍 ↦ (((𝑚 ∈ 𝑍 ↦ (𝑥 ∈ 𝐴 ↦ 𝐵))‘𝑚)‘𝑥))) ∈ ℝ} ↦ (lim
inf‘(𝑚 ∈ 𝑍 ↦ (((𝑚 ∈ 𝑍 ↦ (𝑥 ∈ 𝐴 ↦ 𝐵))‘𝑚)‘𝑥)))) |
108 | 99, 102, 103, 12, 104, 105, 106, 107 | smfliminf 42542 |
. 2
⊢ (𝜑 → (𝑥 ∈ {𝑥 ∈ ∪
𝑛 ∈ 𝑍 ∩ 𝑚 ∈
(ℤ≥‘𝑛)dom ((𝑚 ∈ 𝑍 ↦ (𝑥 ∈ 𝐴 ↦ 𝐵))‘𝑚) ∣ (lim inf‘(𝑚 ∈ 𝑍 ↦ (((𝑚 ∈ 𝑍 ↦ (𝑥 ∈ 𝐴 ↦ 𝐵))‘𝑚)‘𝑥))) ∈ ℝ} ↦ (lim
inf‘(𝑚 ∈ 𝑍 ↦ (((𝑚 ∈ 𝑍 ↦ (𝑥 ∈ 𝐴 ↦ 𝐵))‘𝑚)‘𝑥)))) ∈ (SMblFn‘𝑆)) |
109 | 98, 108 | eqeltrd 2866 |
1
⊢ (𝜑 → 𝐺 ∈ (SMblFn‘𝑆)) |