Proof of Theorem finfdm
Step | Hyp | Ref
| Expression |
1 | | finfdm.6 |
. . 3
⊢ 𝐷 = {𝑥 ∈ ∩
𝑛 ∈ 𝑍 dom (𝐹‘𝑛) ∣ ∃𝑦 ∈ ℝ ∀𝑛 ∈ 𝑍 𝑦 ≤ ((𝐹‘𝑛)‘𝑥)} |
2 | | finfdm.2 |
. . . 4
⊢
Ⅎ𝑥𝜑 |
3 | | nfcv 2905 |
. . . . 5
⊢
Ⅎ𝑥ℕ |
4 | | nfcv 2905 |
. . . . . 6
⊢
Ⅎ𝑥𝑍 |
5 | | finfdm.7 |
. . . . . . . . 9
⊢ 𝐻 = (𝑛 ∈ 𝑍 ↦ (𝑚 ∈ ℕ ↦ {𝑥 ∈ dom (𝐹‘𝑛) ∣ -𝑚 < ((𝐹‘𝑛)‘𝑥)})) |
6 | | nfrab1 3424 |
. . . . . . . . . . 11
⊢
Ⅎ𝑥{𝑥 ∈ dom (𝐹‘𝑛) ∣ -𝑚 < ((𝐹‘𝑛)‘𝑥)} |
7 | 3, 6 | nfmpt 5210 |
. . . . . . . . . 10
⊢
Ⅎ𝑥(𝑚 ∈ ℕ ↦ {𝑥 ∈ dom (𝐹‘𝑛) ∣ -𝑚 < ((𝐹‘𝑛)‘𝑥)}) |
8 | 4, 7 | nfmpt 5210 |
. . . . . . . . 9
⊢
Ⅎ𝑥(𝑛 ∈ 𝑍 ↦ (𝑚 ∈ ℕ ↦ {𝑥 ∈ dom (𝐹‘𝑛) ∣ -𝑚 < ((𝐹‘𝑛)‘𝑥)})) |
9 | 5, 8 | nfcxfr 2903 |
. . . . . . . 8
⊢
Ⅎ𝑥𝐻 |
10 | | nfcv 2905 |
. . . . . . . 8
⊢
Ⅎ𝑥𝑛 |
11 | 9, 10 | nffv 6849 |
. . . . . . 7
⊢
Ⅎ𝑥(𝐻‘𝑛) |
12 | | nfcv 2905 |
. . . . . . 7
⊢
Ⅎ𝑥𝑚 |
13 | 11, 12 | nffv 6849 |
. . . . . 6
⊢
Ⅎ𝑥((𝐻‘𝑛)‘𝑚) |
14 | 4, 13 | nfiin 4983 |
. . . . 5
⊢
Ⅎ𝑥∩ 𝑛 ∈ 𝑍 ((𝐻‘𝑛)‘𝑚) |
15 | 3, 14 | nfiun 4982 |
. . . 4
⊢
Ⅎ𝑥∪ 𝑚 ∈ ℕ ∩ 𝑛 ∈ 𝑍 ((𝐻‘𝑛)‘𝑚) |
16 | | finfdm.3 |
. . . . . . . . . . 11
⊢
Ⅎ𝑚𝜑 |
17 | | nfv 1917 |
. . . . . . . . . . 11
⊢
Ⅎ𝑚 𝑥 ∈ ∩ 𝑛 ∈ 𝑍 dom (𝐹‘𝑛) |
18 | 16, 17 | nfan 1902 |
. . . . . . . . . 10
⊢
Ⅎ𝑚(𝜑 ∧ 𝑥 ∈ ∩
𝑛 ∈ 𝑍 dom (𝐹‘𝑛)) |
19 | | nfv 1917 |
. . . . . . . . . 10
⊢
Ⅎ𝑚 𝑦 ∈ ℝ |
20 | 18, 19 | nfan 1902 |
. . . . . . . . 9
⊢
Ⅎ𝑚((𝜑 ∧ 𝑥 ∈ ∩
𝑛 ∈ 𝑍 dom (𝐹‘𝑛)) ∧ 𝑦 ∈ ℝ) |
21 | | nfv 1917 |
. . . . . . . . 9
⊢
Ⅎ𝑚∀𝑛 ∈ 𝑍 𝑦 ≤ ((𝐹‘𝑛)‘𝑥) |
22 | 20, 21 | nfan 1902 |
. . . . . . . 8
⊢
Ⅎ𝑚(((𝜑 ∧ 𝑥 ∈ ∩
𝑛 ∈ 𝑍 dom (𝐹‘𝑛)) ∧ 𝑦 ∈ ℝ) ∧ ∀𝑛 ∈ 𝑍 𝑦 ≤ ((𝐹‘𝑛)‘𝑥)) |
23 | | finfdm.1 |
. . . . . . . . . . . . 13
⊢
Ⅎ𝑛𝜑 |
24 | | nfii1 4987 |
. . . . . . . . . . . . . 14
⊢
Ⅎ𝑛∩ 𝑛 ∈ 𝑍 dom (𝐹‘𝑛) |
25 | 24 | nfel2 2923 |
. . . . . . . . . . . . 13
⊢
Ⅎ𝑛 𝑥 ∈ ∩ 𝑛 ∈ 𝑍 dom (𝐹‘𝑛) |
26 | 23, 25 | nfan 1902 |
. . . . . . . . . . . 12
⊢
Ⅎ𝑛(𝜑 ∧ 𝑥 ∈ ∩
𝑛 ∈ 𝑍 dom (𝐹‘𝑛)) |
27 | | nfv 1917 |
. . . . . . . . . . . 12
⊢
Ⅎ𝑛 𝑦 ∈ ℝ |
28 | 26, 27 | nfan 1902 |
. . . . . . . . . . 11
⊢
Ⅎ𝑛((𝜑 ∧ 𝑥 ∈ ∩
𝑛 ∈ 𝑍 dom (𝐹‘𝑛)) ∧ 𝑦 ∈ ℝ) |
29 | | nfra1 3265 |
. . . . . . . . . . 11
⊢
Ⅎ𝑛∀𝑛 ∈ 𝑍 𝑦 ≤ ((𝐹‘𝑛)‘𝑥) |
30 | 28, 29 | nfan 1902 |
. . . . . . . . . 10
⊢
Ⅎ𝑛(((𝜑 ∧ 𝑥 ∈ ∩
𝑛 ∈ 𝑍 dom (𝐹‘𝑛)) ∧ 𝑦 ∈ ℝ) ∧ ∀𝑛 ∈ 𝑍 𝑦 ≤ ((𝐹‘𝑛)‘𝑥)) |
31 | | nfv 1917 |
. . . . . . . . . 10
⊢
Ⅎ𝑛 𝑚 ∈ ℕ |
32 | | nfv 1917 |
. . . . . . . . . 10
⊢
Ⅎ𝑛-𝑦 < 𝑚 |
33 | 30, 31, 32 | nf3an 1904 |
. . . . . . . . 9
⊢
Ⅎ𝑛((((𝜑 ∧ 𝑥 ∈ ∩
𝑛 ∈ 𝑍 dom (𝐹‘𝑛)) ∧ 𝑦 ∈ ℝ) ∧ ∀𝑛 ∈ 𝑍 𝑦 ≤ ((𝐹‘𝑛)‘𝑥)) ∧ 𝑚 ∈ ℕ ∧ -𝑦 < 𝑚) |
34 | | vex 3447 |
. . . . . . . . . 10
⊢ 𝑥 ∈ V |
35 | 34 | a1i 11 |
. . . . . . . . 9
⊢
(((((𝜑 ∧ 𝑥 ∈ ∩ 𝑛 ∈ 𝑍 dom (𝐹‘𝑛)) ∧ 𝑦 ∈ ℝ) ∧ ∀𝑛 ∈ 𝑍 𝑦 ≤ ((𝐹‘𝑛)‘𝑥)) ∧ 𝑚 ∈ ℕ ∧ -𝑦 < 𝑚) → 𝑥 ∈ V) |
36 | | simp-4r 782 |
. . . . . . . . . . . . 13
⊢
(((((𝜑 ∧ 𝑥 ∈ ∩ 𝑛 ∈ 𝑍 dom (𝐹‘𝑛)) ∧ 𝑦 ∈ ℝ) ∧ ∀𝑛 ∈ 𝑍 𝑦 ≤ ((𝐹‘𝑛)‘𝑥)) ∧ 𝑛 ∈ 𝑍) → 𝑥 ∈ ∩
𝑛 ∈ 𝑍 dom (𝐹‘𝑛)) |
37 | 36 | 3ad2antl1 1185 |
. . . . . . . . . . . 12
⊢
((((((𝜑 ∧ 𝑥 ∈ ∩ 𝑛 ∈ 𝑍 dom (𝐹‘𝑛)) ∧ 𝑦 ∈ ℝ) ∧ ∀𝑛 ∈ 𝑍 𝑦 ≤ ((𝐹‘𝑛)‘𝑥)) ∧ 𝑚 ∈ ℕ ∧ -𝑦 < 𝑚) ∧ 𝑛 ∈ 𝑍) → 𝑥 ∈ ∩
𝑛 ∈ 𝑍 dom (𝐹‘𝑛)) |
38 | | simpr 485 |
. . . . . . . . . . . 12
⊢
((((((𝜑 ∧ 𝑥 ∈ ∩ 𝑛 ∈ 𝑍 dom (𝐹‘𝑛)) ∧ 𝑦 ∈ ℝ) ∧ ∀𝑛 ∈ 𝑍 𝑦 ≤ ((𝐹‘𝑛)‘𝑥)) ∧ 𝑚 ∈ ℕ ∧ -𝑦 < 𝑚) ∧ 𝑛 ∈ 𝑍) → 𝑛 ∈ 𝑍) |
39 | | eliinid 43225 |
. . . . . . . . . . . 12
⊢ ((𝑥 ∈ ∩ 𝑛 ∈ 𝑍 dom (𝐹‘𝑛) ∧ 𝑛 ∈ 𝑍) → 𝑥 ∈ dom (𝐹‘𝑛)) |
40 | 37, 38, 39 | syl2anc 584 |
. . . . . . . . . . 11
⊢
((((((𝜑 ∧ 𝑥 ∈ ∩ 𝑛 ∈ 𝑍 dom (𝐹‘𝑛)) ∧ 𝑦 ∈ ℝ) ∧ ∀𝑛 ∈ 𝑍 𝑦 ≤ ((𝐹‘𝑛)‘𝑥)) ∧ 𝑚 ∈ ℕ ∧ -𝑦 < 𝑚) ∧ 𝑛 ∈ 𝑍) → 𝑥 ∈ dom (𝐹‘𝑛)) |
41 | | simpl2 1192 |
. . . . . . . . . . . . 13
⊢
((((((𝜑 ∧ 𝑥 ∈ ∩ 𝑛 ∈ 𝑍 dom (𝐹‘𝑛)) ∧ 𝑦 ∈ ℝ) ∧ ∀𝑛 ∈ 𝑍 𝑦 ≤ ((𝐹‘𝑛)‘𝑥)) ∧ 𝑚 ∈ ℕ ∧ -𝑦 < 𝑚) ∧ 𝑛 ∈ 𝑍) → 𝑚 ∈ ℕ) |
42 | | nnre 12118 |
. . . . . . . . . . . . . . 15
⊢ (𝑚 ∈ ℕ → 𝑚 ∈
ℝ) |
43 | 42 | renegcld 11540 |
. . . . . . . . . . . . . 14
⊢ (𝑚 ∈ ℕ → -𝑚 ∈
ℝ) |
44 | 43 | rexrd 11163 |
. . . . . . . . . . . . 13
⊢ (𝑚 ∈ ℕ → -𝑚 ∈
ℝ*) |
45 | 41, 44 | syl 17 |
. . . . . . . . . . . 12
⊢
((((((𝜑 ∧ 𝑥 ∈ ∩ 𝑛 ∈ 𝑍 dom (𝐹‘𝑛)) ∧ 𝑦 ∈ ℝ) ∧ ∀𝑛 ∈ 𝑍 𝑦 ≤ ((𝐹‘𝑛)‘𝑥)) ∧ 𝑚 ∈ ℕ ∧ -𝑦 < 𝑚) ∧ 𝑛 ∈ 𝑍) → -𝑚 ∈ ℝ*) |
46 | | simpllr 774 |
. . . . . . . . . . . . . 14
⊢
(((((𝜑 ∧ 𝑥 ∈ ∩ 𝑛 ∈ 𝑍 dom (𝐹‘𝑛)) ∧ 𝑦 ∈ ℝ) ∧ ∀𝑛 ∈ 𝑍 𝑦 ≤ ((𝐹‘𝑛)‘𝑥)) ∧ 𝑛 ∈ 𝑍) → 𝑦 ∈ ℝ) |
47 | | rexr 11159 |
. . . . . . . . . . . . . 14
⊢ (𝑦 ∈ ℝ → 𝑦 ∈
ℝ*) |
48 | 46, 47 | syl 17 |
. . . . . . . . . . . . 13
⊢
(((((𝜑 ∧ 𝑥 ∈ ∩ 𝑛 ∈ 𝑍 dom (𝐹‘𝑛)) ∧ 𝑦 ∈ ℝ) ∧ ∀𝑛 ∈ 𝑍 𝑦 ≤ ((𝐹‘𝑛)‘𝑥)) ∧ 𝑛 ∈ 𝑍) → 𝑦 ∈ ℝ*) |
49 | 48 | 3ad2antl1 1185 |
. . . . . . . . . . . 12
⊢
((((((𝜑 ∧ 𝑥 ∈ ∩ 𝑛 ∈ 𝑍 dom (𝐹‘𝑛)) ∧ 𝑦 ∈ ℝ) ∧ ∀𝑛 ∈ 𝑍 𝑦 ≤ ((𝐹‘𝑛)‘𝑥)) ∧ 𝑚 ∈ ℕ ∧ -𝑦 < 𝑚) ∧ 𝑛 ∈ 𝑍) → 𝑦 ∈ ℝ*) |
50 | | simp-4l 781 |
. . . . . . . . . . . . . 14
⊢
(((((𝜑 ∧ 𝑥 ∈ ∩ 𝑛 ∈ 𝑍 dom (𝐹‘𝑛)) ∧ 𝑦 ∈ ℝ) ∧ ∀𝑛 ∈ 𝑍 𝑦 ≤ ((𝐹‘𝑛)‘𝑥)) ∧ 𝑛 ∈ 𝑍) → 𝜑) |
51 | 50 | 3ad2antl1 1185 |
. . . . . . . . . . . . 13
⊢
((((((𝜑 ∧ 𝑥 ∈ ∩ 𝑛 ∈ 𝑍 dom (𝐹‘𝑛)) ∧ 𝑦 ∈ ℝ) ∧ ∀𝑛 ∈ 𝑍 𝑦 ≤ ((𝐹‘𝑛)‘𝑥)) ∧ 𝑚 ∈ ℕ ∧ -𝑦 < 𝑚) ∧ 𝑛 ∈ 𝑍) → 𝜑) |
52 | | finfdm.5 |
. . . . . . . . . . . . . . 15
⊢ ((𝜑 ∧ 𝑛 ∈ 𝑍) → (𝐹‘𝑛):dom (𝐹‘𝑛)⟶ℝ*) |
53 | 52 | 3adant3 1132 |
. . . . . . . . . . . . . 14
⊢ ((𝜑 ∧ 𝑛 ∈ 𝑍 ∧ 𝑥 ∈ dom (𝐹‘𝑛)) → (𝐹‘𝑛):dom (𝐹‘𝑛)⟶ℝ*) |
54 | | simp3 1138 |
. . . . . . . . . . . . . 14
⊢ ((𝜑 ∧ 𝑛 ∈ 𝑍 ∧ 𝑥 ∈ dom (𝐹‘𝑛)) → 𝑥 ∈ dom (𝐹‘𝑛)) |
55 | 53, 54 | ffvelcdmd 7032 |
. . . . . . . . . . . . 13
⊢ ((𝜑 ∧ 𝑛 ∈ 𝑍 ∧ 𝑥 ∈ dom (𝐹‘𝑛)) → ((𝐹‘𝑛)‘𝑥) ∈
ℝ*) |
56 | 51, 38, 40, 55 | syl3anc 1371 |
. . . . . . . . . . . 12
⊢
((((((𝜑 ∧ 𝑥 ∈ ∩ 𝑛 ∈ 𝑍 dom (𝐹‘𝑛)) ∧ 𝑦 ∈ ℝ) ∧ ∀𝑛 ∈ 𝑍 𝑦 ≤ ((𝐹‘𝑛)‘𝑥)) ∧ 𝑚 ∈ ℕ ∧ -𝑦 < 𝑚) ∧ 𝑛 ∈ 𝑍) → ((𝐹‘𝑛)‘𝑥) ∈
ℝ*) |
57 | 46 | 3ad2antl1 1185 |
. . . . . . . . . . . . 13
⊢
((((((𝜑 ∧ 𝑥 ∈ ∩ 𝑛 ∈ 𝑍 dom (𝐹‘𝑛)) ∧ 𝑦 ∈ ℝ) ∧ ∀𝑛 ∈ 𝑍 𝑦 ≤ ((𝐹‘𝑛)‘𝑥)) ∧ 𝑚 ∈ ℕ ∧ -𝑦 < 𝑚) ∧ 𝑛 ∈ 𝑍) → 𝑦 ∈ ℝ) |
58 | | simpl3 1193 |
. . . . . . . . . . . . 13
⊢
((((((𝜑 ∧ 𝑥 ∈ ∩ 𝑛 ∈ 𝑍 dom (𝐹‘𝑛)) ∧ 𝑦 ∈ ℝ) ∧ ∀𝑛 ∈ 𝑍 𝑦 ≤ ((𝐹‘𝑛)‘𝑥)) ∧ 𝑚 ∈ ℕ ∧ -𝑦 < 𝑚) ∧ 𝑛 ∈ 𝑍) → -𝑦 < 𝑚) |
59 | | simp1 1136 |
. . . . . . . . . . . . . 14
⊢ ((𝑦 ∈ ℝ ∧ 𝑚 ∈ ℕ ∧ -𝑦 < 𝑚) → 𝑦 ∈ ℝ) |
60 | 42 | 3ad2ant2 1134 |
. . . . . . . . . . . . . 14
⊢ ((𝑦 ∈ ℝ ∧ 𝑚 ∈ ℕ ∧ -𝑦 < 𝑚) → 𝑚 ∈ ℝ) |
61 | | simp3 1138 |
. . . . . . . . . . . . . 14
⊢ ((𝑦 ∈ ℝ ∧ 𝑚 ∈ ℕ ∧ -𝑦 < 𝑚) → -𝑦 < 𝑚) |
62 | 59, 60, 61 | ltnegcon1d 11693 |
. . . . . . . . . . . . 13
⊢ ((𝑦 ∈ ℝ ∧ 𝑚 ∈ ℕ ∧ -𝑦 < 𝑚) → -𝑚 < 𝑦) |
63 | 57, 41, 58, 62 | syl3anc 1371 |
. . . . . . . . . . . 12
⊢
((((((𝜑 ∧ 𝑥 ∈ ∩ 𝑛 ∈ 𝑍 dom (𝐹‘𝑛)) ∧ 𝑦 ∈ ℝ) ∧ ∀𝑛 ∈ 𝑍 𝑦 ≤ ((𝐹‘𝑛)‘𝑥)) ∧ 𝑚 ∈ ℕ ∧ -𝑦 < 𝑚) ∧ 𝑛 ∈ 𝑍) → -𝑚 < 𝑦) |
64 | | simpl1r 1225 |
. . . . . . . . . . . . 13
⊢
((((((𝜑 ∧ 𝑥 ∈ ∩ 𝑛 ∈ 𝑍 dom (𝐹‘𝑛)) ∧ 𝑦 ∈ ℝ) ∧ ∀𝑛 ∈ 𝑍 𝑦 ≤ ((𝐹‘𝑛)‘𝑥)) ∧ 𝑚 ∈ ℕ ∧ -𝑦 < 𝑚) ∧ 𝑛 ∈ 𝑍) → ∀𝑛 ∈ 𝑍 𝑦 ≤ ((𝐹‘𝑛)‘𝑥)) |
65 | | rspa 3229 |
. . . . . . . . . . . . 13
⊢
((∀𝑛 ∈
𝑍 𝑦 ≤ ((𝐹‘𝑛)‘𝑥) ∧ 𝑛 ∈ 𝑍) → 𝑦 ≤ ((𝐹‘𝑛)‘𝑥)) |
66 | 64, 38, 65 | syl2anc 584 |
. . . . . . . . . . . 12
⊢
((((((𝜑 ∧ 𝑥 ∈ ∩ 𝑛 ∈ 𝑍 dom (𝐹‘𝑛)) ∧ 𝑦 ∈ ℝ) ∧ ∀𝑛 ∈ 𝑍 𝑦 ≤ ((𝐹‘𝑛)‘𝑥)) ∧ 𝑚 ∈ ℕ ∧ -𝑦 < 𝑚) ∧ 𝑛 ∈ 𝑍) → 𝑦 ≤ ((𝐹‘𝑛)‘𝑥)) |
67 | 45, 49, 56, 63, 66 | xrltletrd 13034 |
. . . . . . . . . . 11
⊢
((((((𝜑 ∧ 𝑥 ∈ ∩ 𝑛 ∈ 𝑍 dom (𝐹‘𝑛)) ∧ 𝑦 ∈ ℝ) ∧ ∀𝑛 ∈ 𝑍 𝑦 ≤ ((𝐹‘𝑛)‘𝑥)) ∧ 𝑚 ∈ ℕ ∧ -𝑦 < 𝑚) ∧ 𝑛 ∈ 𝑍) → -𝑚 < ((𝐹‘𝑛)‘𝑥)) |
68 | 40, 67 | rabidd 43274 |
. . . . . . . . . 10
⊢
((((((𝜑 ∧ 𝑥 ∈ ∩ 𝑛 ∈ 𝑍 dom (𝐹‘𝑛)) ∧ 𝑦 ∈ ℝ) ∧ ∀𝑛 ∈ 𝑍 𝑦 ≤ ((𝐹‘𝑛)‘𝑥)) ∧ 𝑚 ∈ ℕ ∧ -𝑦 < 𝑚) ∧ 𝑛 ∈ 𝑍) → 𝑥 ∈ {𝑥 ∈ dom (𝐹‘𝑛) ∣ -𝑚 < ((𝐹‘𝑛)‘𝑥)}) |
69 | | id 22 |
. . . . . . . . . . . . . 14
⊢ (𝑛 ∈ 𝑍 → 𝑛 ∈ 𝑍) |
70 | | nnex 12117 |
. . . . . . . . . . . . . . . 16
⊢ ℕ
∈ V |
71 | 70 | mptex 7169 |
. . . . . . . . . . . . . . 15
⊢ (𝑚 ∈ ℕ ↦ {𝑥 ∈ dom (𝐹‘𝑛) ∣ -𝑚 < ((𝐹‘𝑛)‘𝑥)}) ∈ V |
72 | 71 | a1i 11 |
. . . . . . . . . . . . . 14
⊢ (𝑛 ∈ 𝑍 → (𝑚 ∈ ℕ ↦ {𝑥 ∈ dom (𝐹‘𝑛) ∣ -𝑚 < ((𝐹‘𝑛)‘𝑥)}) ∈ V) |
73 | 5 | fvmpt2 6956 |
. . . . . . . . . . . . . 14
⊢ ((𝑛 ∈ 𝑍 ∧ (𝑚 ∈ ℕ ↦ {𝑥 ∈ dom (𝐹‘𝑛) ∣ -𝑚 < ((𝐹‘𝑛)‘𝑥)}) ∈ V) → (𝐻‘𝑛) = (𝑚 ∈ ℕ ↦ {𝑥 ∈ dom (𝐹‘𝑛) ∣ -𝑚 < ((𝐹‘𝑛)‘𝑥)})) |
74 | 69, 72, 73 | syl2anc 584 |
. . . . . . . . . . . . 13
⊢ (𝑛 ∈ 𝑍 → (𝐻‘𝑛) = (𝑚 ∈ ℕ ↦ {𝑥 ∈ dom (𝐹‘𝑛) ∣ -𝑚 < ((𝐹‘𝑛)‘𝑥)})) |
75 | | finfdm.4 |
. . . . . . . . . . . . . . . . 17
⊢
Ⅎ𝑥𝐹 |
76 | 75, 10 | nffv 6849 |
. . . . . . . . . . . . . . . 16
⊢
Ⅎ𝑥(𝐹‘𝑛) |
77 | 76 | nfdm 5904 |
. . . . . . . . . . . . . . 15
⊢
Ⅎ𝑥dom
(𝐹‘𝑛) |
78 | | fvex 6852 |
. . . . . . . . . . . . . . . 16
⊢ (𝐹‘𝑛) ∈ V |
79 | 78 | dmex 7840 |
. . . . . . . . . . . . . . 15
⊢ dom
(𝐹‘𝑛) ∈ V |
80 | 77, 79 | rabexf 43248 |
. . . . . . . . . . . . . 14
⊢ {𝑥 ∈ dom (𝐹‘𝑛) ∣ -𝑚 < ((𝐹‘𝑛)‘𝑥)} ∈ V |
81 | 80 | a1i 11 |
. . . . . . . . . . . . 13
⊢ ((𝑛 ∈ 𝑍 ∧ 𝑚 ∈ ℕ) → {𝑥 ∈ dom (𝐹‘𝑛) ∣ -𝑚 < ((𝐹‘𝑛)‘𝑥)} ∈ V) |
82 | 74, 81 | fvmpt2d 6958 |
. . . . . . . . . . . 12
⊢ ((𝑛 ∈ 𝑍 ∧ 𝑚 ∈ ℕ) → ((𝐻‘𝑛)‘𝑚) = {𝑥 ∈ dom (𝐹‘𝑛) ∣ -𝑚 < ((𝐹‘𝑛)‘𝑥)}) |
83 | 82 | eqcomd 2743 |
. . . . . . . . . . 11
⊢ ((𝑛 ∈ 𝑍 ∧ 𝑚 ∈ ℕ) → {𝑥 ∈ dom (𝐹‘𝑛) ∣ -𝑚 < ((𝐹‘𝑛)‘𝑥)} = ((𝐻‘𝑛)‘𝑚)) |
84 | 38, 41, 83 | syl2anc 584 |
. . . . . . . . . 10
⊢
((((((𝜑 ∧ 𝑥 ∈ ∩ 𝑛 ∈ 𝑍 dom (𝐹‘𝑛)) ∧ 𝑦 ∈ ℝ) ∧ ∀𝑛 ∈ 𝑍 𝑦 ≤ ((𝐹‘𝑛)‘𝑥)) ∧ 𝑚 ∈ ℕ ∧ -𝑦 < 𝑚) ∧ 𝑛 ∈ 𝑍) → {𝑥 ∈ dom (𝐹‘𝑛) ∣ -𝑚 < ((𝐹‘𝑛)‘𝑥)} = ((𝐻‘𝑛)‘𝑚)) |
85 | 68, 84 | eleqtrd 2840 |
. . . . . . . . 9
⊢
((((((𝜑 ∧ 𝑥 ∈ ∩ 𝑛 ∈ 𝑍 dom (𝐹‘𝑛)) ∧ 𝑦 ∈ ℝ) ∧ ∀𝑛 ∈ 𝑍 𝑦 ≤ ((𝐹‘𝑛)‘𝑥)) ∧ 𝑚 ∈ ℕ ∧ -𝑦 < 𝑚) ∧ 𝑛 ∈ 𝑍) → 𝑥 ∈ ((𝐻‘𝑛)‘𝑚)) |
86 | 33, 35, 85 | eliind2 43244 |
. . . . . . . 8
⊢
(((((𝜑 ∧ 𝑥 ∈ ∩ 𝑛 ∈ 𝑍 dom (𝐹‘𝑛)) ∧ 𝑦 ∈ ℝ) ∧ ∀𝑛 ∈ 𝑍 𝑦 ≤ ((𝐹‘𝑛)‘𝑥)) ∧ 𝑚 ∈ ℕ ∧ -𝑦 < 𝑚) → 𝑥 ∈ ∩
𝑛 ∈ 𝑍 ((𝐻‘𝑛)‘𝑚)) |
87 | | renegcl 11422 |
. . . . . . . . . 10
⊢ (𝑦 ∈ ℝ → -𝑦 ∈
ℝ) |
88 | 87 | archd 43281 |
. . . . . . . . 9
⊢ (𝑦 ∈ ℝ →
∃𝑚 ∈ ℕ
-𝑦 < 𝑚) |
89 | 88 | ad2antlr 725 |
. . . . . . . 8
⊢ ((((𝜑 ∧ 𝑥 ∈ ∩
𝑛 ∈ 𝑍 dom (𝐹‘𝑛)) ∧ 𝑦 ∈ ℝ) ∧ ∀𝑛 ∈ 𝑍 𝑦 ≤ ((𝐹‘𝑛)‘𝑥)) → ∃𝑚 ∈ ℕ -𝑦 < 𝑚) |
90 | 22, 86, 89 | reximdd 43266 |
. . . . . . 7
⊢ ((((𝜑 ∧ 𝑥 ∈ ∩
𝑛 ∈ 𝑍 dom (𝐹‘𝑛)) ∧ 𝑦 ∈ ℝ) ∧ ∀𝑛 ∈ 𝑍 𝑦 ≤ ((𝐹‘𝑛)‘𝑥)) → ∃𝑚 ∈ ℕ 𝑥 ∈ ∩
𝑛 ∈ 𝑍 ((𝐻‘𝑛)‘𝑚)) |
91 | 90 | rexlimdva2 3152 |
. . . . . 6
⊢ ((𝜑 ∧ 𝑥 ∈ ∩
𝑛 ∈ 𝑍 dom (𝐹‘𝑛)) → (∃𝑦 ∈ ℝ ∀𝑛 ∈ 𝑍 𝑦 ≤ ((𝐹‘𝑛)‘𝑥) → ∃𝑚 ∈ ℕ 𝑥 ∈ ∩
𝑛 ∈ 𝑍 ((𝐻‘𝑛)‘𝑚))) |
92 | 91 | 3impia 1117 |
. . . . 5
⊢ ((𝜑 ∧ 𝑥 ∈ ∩
𝑛 ∈ 𝑍 dom (𝐹‘𝑛) ∧ ∃𝑦 ∈ ℝ ∀𝑛 ∈ 𝑍 𝑦 ≤ ((𝐹‘𝑛)‘𝑥)) → ∃𝑚 ∈ ℕ 𝑥 ∈ ∩
𝑛 ∈ 𝑍 ((𝐻‘𝑛)‘𝑚)) |
93 | | eliun 4956 |
. . . . 5
⊢ (𝑥 ∈ ∪ 𝑚 ∈ ℕ ∩ 𝑛 ∈ 𝑍 ((𝐻‘𝑛)‘𝑚) ↔ ∃𝑚 ∈ ℕ 𝑥 ∈ ∩
𝑛 ∈ 𝑍 ((𝐻‘𝑛)‘𝑚)) |
94 | 92, 93 | sylibr 233 |
. . . 4
⊢ ((𝜑 ∧ 𝑥 ∈ ∩
𝑛 ∈ 𝑍 dom (𝐹‘𝑛) ∧ ∃𝑦 ∈ ℝ ∀𝑛 ∈ 𝑍 𝑦 ≤ ((𝐹‘𝑛)‘𝑥)) → 𝑥 ∈ ∪
𝑚 ∈ ℕ ∩ 𝑛 ∈ 𝑍 ((𝐻‘𝑛)‘𝑚)) |
95 | 2, 15, 94 | rabssd 43256 |
. . 3
⊢ (𝜑 → {𝑥 ∈ ∩
𝑛 ∈ 𝑍 dom (𝐹‘𝑛) ∣ ∃𝑦 ∈ ℝ ∀𝑛 ∈ 𝑍 𝑦 ≤ ((𝐹‘𝑛)‘𝑥)} ⊆ ∪ 𝑚 ∈ ℕ ∩ 𝑛 ∈ 𝑍 ((𝐻‘𝑛)‘𝑚)) |
96 | 1, 95 | eqsstrid 3990 |
. 2
⊢ (𝜑 → 𝐷 ⊆ ∪
𝑚 ∈ ℕ ∩ 𝑛 ∈ 𝑍 ((𝐻‘𝑛)‘𝑚)) |
97 | | nfcv 2905 |
. . 3
⊢
Ⅎ𝑚𝐷 |
98 | | nfv 1917 |
. . . . 5
⊢
Ⅎ𝑥 𝑚 ∈ ℕ |
99 | 2, 98 | nfan 1902 |
. . . 4
⊢
Ⅎ𝑥(𝜑 ∧ 𝑚 ∈ ℕ) |
100 | | nfrab1 3424 |
. . . . 5
⊢
Ⅎ𝑥{𝑥 ∈ ∩
𝑛 ∈ 𝑍 dom (𝐹‘𝑛) ∣ ∃𝑦 ∈ ℝ ∀𝑛 ∈ 𝑍 𝑦 ≤ ((𝐹‘𝑛)‘𝑥)} |
101 | 1, 100 | nfcxfr 2903 |
. . . 4
⊢
Ⅎ𝑥𝐷 |
102 | 23, 31 | nfan 1902 |
. . . . . . . 8
⊢
Ⅎ𝑛(𝜑 ∧ 𝑚 ∈ ℕ) |
103 | | nfii1 4987 |
. . . . . . . . 9
⊢
Ⅎ𝑛∩ 𝑛 ∈ 𝑍 ((𝐻‘𝑛)‘𝑚) |
104 | 103 | nfel2 2923 |
. . . . . . . 8
⊢
Ⅎ𝑛 𝑥 ∈ ∩ 𝑛 ∈ 𝑍 ((𝐻‘𝑛)‘𝑚) |
105 | 102, 104 | nfan 1902 |
. . . . . . 7
⊢
Ⅎ𝑛((𝜑 ∧ 𝑚 ∈ ℕ) ∧ 𝑥 ∈ ∩
𝑛 ∈ 𝑍 ((𝐻‘𝑛)‘𝑚)) |
106 | | simpr 485 |
. . . . . . 7
⊢ (((𝜑 ∧ 𝑚 ∈ ℕ) ∧ 𝑥 ∈ ∩
𝑛 ∈ 𝑍 ((𝐻‘𝑛)‘𝑚)) → 𝑥 ∈ ∩
𝑛 ∈ 𝑍 ((𝐻‘𝑛)‘𝑚)) |
107 | | eliinid 43225 |
. . . . . . . . . 10
⊢ ((𝑥 ∈ ∩ 𝑛 ∈ 𝑍 ((𝐻‘𝑛)‘𝑚) ∧ 𝑛 ∈ 𝑍) → 𝑥 ∈ ((𝐻‘𝑛)‘𝑚)) |
108 | 107 | adantll 712 |
. . . . . . . . 9
⊢ ((((𝜑 ∧ 𝑚 ∈ ℕ) ∧ 𝑥 ∈ ∩
𝑛 ∈ 𝑍 ((𝐻‘𝑛)‘𝑚)) ∧ 𝑛 ∈ 𝑍) → 𝑥 ∈ ((𝐻‘𝑛)‘𝑚)) |
109 | 69 | adantl 482 |
. . . . . . . . . 10
⊢ ((((𝜑 ∧ 𝑚 ∈ ℕ) ∧ 𝑥 ∈ ∩
𝑛 ∈ 𝑍 ((𝐻‘𝑛)‘𝑚)) ∧ 𝑛 ∈ 𝑍) → 𝑛 ∈ 𝑍) |
110 | | simpllr 774 |
. . . . . . . . . 10
⊢ ((((𝜑 ∧ 𝑚 ∈ ℕ) ∧ 𝑥 ∈ ∩
𝑛 ∈ 𝑍 ((𝐻‘𝑛)‘𝑚)) ∧ 𝑛 ∈ 𝑍) → 𝑚 ∈ ℕ) |
111 | 109, 110,
82 | syl2anc 584 |
. . . . . . . . 9
⊢ ((((𝜑 ∧ 𝑚 ∈ ℕ) ∧ 𝑥 ∈ ∩
𝑛 ∈ 𝑍 ((𝐻‘𝑛)‘𝑚)) ∧ 𝑛 ∈ 𝑍) → ((𝐻‘𝑛)‘𝑚) = {𝑥 ∈ dom (𝐹‘𝑛) ∣ -𝑚 < ((𝐹‘𝑛)‘𝑥)}) |
112 | 108, 111 | eleqtrd 2840 |
. . . . . . . 8
⊢ ((((𝜑 ∧ 𝑚 ∈ ℕ) ∧ 𝑥 ∈ ∩
𝑛 ∈ 𝑍 ((𝐻‘𝑛)‘𝑚)) ∧ 𝑛 ∈ 𝑍) → 𝑥 ∈ {𝑥 ∈ dom (𝐹‘𝑛) ∣ -𝑚 < ((𝐹‘𝑛)‘𝑥)}) |
113 | | rabidim1 3426 |
. . . . . . . 8
⊢ (𝑥 ∈ {𝑥 ∈ dom (𝐹‘𝑛) ∣ -𝑚 < ((𝐹‘𝑛)‘𝑥)} → 𝑥 ∈ dom (𝐹‘𝑛)) |
114 | 112, 113 | syl 17 |
. . . . . . 7
⊢ ((((𝜑 ∧ 𝑚 ∈ ℕ) ∧ 𝑥 ∈ ∩
𝑛 ∈ 𝑍 ((𝐻‘𝑛)‘𝑚)) ∧ 𝑛 ∈ 𝑍) → 𝑥 ∈ dom (𝐹‘𝑛)) |
115 | 105, 106,
114 | eliind2 43244 |
. . . . . 6
⊢ (((𝜑 ∧ 𝑚 ∈ ℕ) ∧ 𝑥 ∈ ∩
𝑛 ∈ 𝑍 ((𝐻‘𝑛)‘𝑚)) → 𝑥 ∈ ∩
𝑛 ∈ 𝑍 dom (𝐹‘𝑛)) |
116 | 43 | ad2antlr 725 |
. . . . . . 7
⊢ (((𝜑 ∧ 𝑚 ∈ ℕ) ∧ 𝑥 ∈ ∩
𝑛 ∈ 𝑍 ((𝐻‘𝑛)‘𝑚)) → -𝑚 ∈ ℝ) |
117 | | breq1 5106 |
. . . . . . . . 9
⊢ (𝑦 = -𝑚 → (𝑦 ≤ ((𝐹‘𝑛)‘𝑥) ↔ -𝑚 ≤ ((𝐹‘𝑛)‘𝑥))) |
118 | 117 | ralbidv 3172 |
. . . . . . . 8
⊢ (𝑦 = -𝑚 → (∀𝑛 ∈ 𝑍 𝑦 ≤ ((𝐹‘𝑛)‘𝑥) ↔ ∀𝑛 ∈ 𝑍 -𝑚 ≤ ((𝐹‘𝑛)‘𝑥))) |
119 | 118 | adantl 482 |
. . . . . . 7
⊢ ((((𝜑 ∧ 𝑚 ∈ ℕ) ∧ 𝑥 ∈ ∩
𝑛 ∈ 𝑍 ((𝐻‘𝑛)‘𝑚)) ∧ 𝑦 = -𝑚) → (∀𝑛 ∈ 𝑍 𝑦 ≤ ((𝐹‘𝑛)‘𝑥) ↔ ∀𝑛 ∈ 𝑍 -𝑚 ≤ ((𝐹‘𝑛)‘𝑥))) |
120 | 110, 44 | syl 17 |
. . . . . . . . 9
⊢ ((((𝜑 ∧ 𝑚 ∈ ℕ) ∧ 𝑥 ∈ ∩
𝑛 ∈ 𝑍 ((𝐻‘𝑛)‘𝑚)) ∧ 𝑛 ∈ 𝑍) → -𝑚 ∈ ℝ*) |
121 | | simplll 773 |
. . . . . . . . . 10
⊢ ((((𝜑 ∧ 𝑚 ∈ ℕ) ∧ 𝑥 ∈ ∩
𝑛 ∈ 𝑍 ((𝐻‘𝑛)‘𝑚)) ∧ 𝑛 ∈ 𝑍) → 𝜑) |
122 | 121, 109,
114, 55 | syl3anc 1371 |
. . . . . . . . 9
⊢ ((((𝜑 ∧ 𝑚 ∈ ℕ) ∧ 𝑥 ∈ ∩
𝑛 ∈ 𝑍 ((𝐻‘𝑛)‘𝑚)) ∧ 𝑛 ∈ 𝑍) → ((𝐹‘𝑛)‘𝑥) ∈
ℝ*) |
123 | | rabidim2 43216 |
. . . . . . . . . 10
⊢ (𝑥 ∈ {𝑥 ∈ dom (𝐹‘𝑛) ∣ -𝑚 < ((𝐹‘𝑛)‘𝑥)} → -𝑚 < ((𝐹‘𝑛)‘𝑥)) |
124 | 112, 123 | syl 17 |
. . . . . . . . 9
⊢ ((((𝜑 ∧ 𝑚 ∈ ℕ) ∧ 𝑥 ∈ ∩
𝑛 ∈ 𝑍 ((𝐻‘𝑛)‘𝑚)) ∧ 𝑛 ∈ 𝑍) → -𝑚 < ((𝐹‘𝑛)‘𝑥)) |
125 | 120, 122,
124 | xrltled 13023 |
. . . . . . . 8
⊢ ((((𝜑 ∧ 𝑚 ∈ ℕ) ∧ 𝑥 ∈ ∩
𝑛 ∈ 𝑍 ((𝐻‘𝑛)‘𝑚)) ∧ 𝑛 ∈ 𝑍) → -𝑚 ≤ ((𝐹‘𝑛)‘𝑥)) |
126 | 105, 125 | ralrimia 3239 |
. . . . . . 7
⊢ (((𝜑 ∧ 𝑚 ∈ ℕ) ∧ 𝑥 ∈ ∩
𝑛 ∈ 𝑍 ((𝐻‘𝑛)‘𝑚)) → ∀𝑛 ∈ 𝑍 -𝑚 ≤ ((𝐹‘𝑛)‘𝑥)) |
127 | 116, 119,
126 | rspcedvd 3581 |
. . . . . 6
⊢ (((𝜑 ∧ 𝑚 ∈ ℕ) ∧ 𝑥 ∈ ∩
𝑛 ∈ 𝑍 ((𝐻‘𝑛)‘𝑚)) → ∃𝑦 ∈ ℝ ∀𝑛 ∈ 𝑍 𝑦 ≤ ((𝐹‘𝑛)‘𝑥)) |
128 | 115, 127 | rabidd 43274 |
. . . . 5
⊢ (((𝜑 ∧ 𝑚 ∈ ℕ) ∧ 𝑥 ∈ ∩
𝑛 ∈ 𝑍 ((𝐻‘𝑛)‘𝑚)) → 𝑥 ∈ {𝑥 ∈ ∩
𝑛 ∈ 𝑍 dom (𝐹‘𝑛) ∣ ∃𝑦 ∈ ℝ ∀𝑛 ∈ 𝑍 𝑦 ≤ ((𝐹‘𝑛)‘𝑥)}) |
129 | 128, 1 | eleqtrrdi 2849 |
. . . 4
⊢ (((𝜑 ∧ 𝑚 ∈ ℕ) ∧ 𝑥 ∈ ∩
𝑛 ∈ 𝑍 ((𝐻‘𝑛)‘𝑚)) → 𝑥 ∈ 𝐷) |
130 | 99, 14, 101, 129 | ssdf2 43255 |
. . 3
⊢ ((𝜑 ∧ 𝑚 ∈ ℕ) → ∩ 𝑛 ∈ 𝑍 ((𝐻‘𝑛)‘𝑚) ⊆ 𝐷) |
131 | 16, 97, 130 | iunssdf 43275 |
. 2
⊢ (𝜑 → ∪ 𝑚 ∈ ℕ ∩ 𝑛 ∈ 𝑍 ((𝐻‘𝑛)‘𝑚) ⊆ 𝐷) |
132 | 96, 131 | eqssd 3959 |
1
⊢ (𝜑 → 𝐷 = ∪ 𝑚 ∈ ℕ ∩ 𝑛 ∈ 𝑍 ((𝐻‘𝑛)‘𝑚)) |