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 3457 |
. . . . . . . . . . 11
⊢
Ⅎ𝑥{𝑥 ∈ dom (𝐹‘𝑛) ∣ -𝑚 < ((𝐹‘𝑛)‘𝑥)} |
| 7 | 3, 6 | nfmpt 5249 |
. . . . . . . . . 10
⊢
Ⅎ𝑥(𝑚 ∈ ℕ ↦ {𝑥 ∈ dom (𝐹‘𝑛) ∣ -𝑚 < ((𝐹‘𝑛)‘𝑥)}) |
| 8 | 4, 7 | nfmpt 5249 |
. . . . . . . . 9
⊢
Ⅎ𝑥(𝑛 ∈ 𝑍 ↦ (𝑚 ∈ ℕ ↦ {𝑥 ∈ dom (𝐹‘𝑛) ∣ -𝑚 < ((𝐹‘𝑛)‘𝑥)})) |
| 9 | 5, 8 | nfcxfr 2903 |
. . . . . . . 8
⊢
Ⅎ𝑥𝐻 |
| 10 | | nfcv 2905 |
. . . . . . . 8
⊢
Ⅎ𝑥𝑛 |
| 11 | 9, 10 | nffv 6916 |
. . . . . . 7
⊢
Ⅎ𝑥(𝐻‘𝑛) |
| 12 | | nfcv 2905 |
. . . . . . 7
⊢
Ⅎ𝑥𝑚 |
| 13 | 11, 12 | nffv 6916 |
. . . . . 6
⊢
Ⅎ𝑥((𝐻‘𝑛)‘𝑚) |
| 14 | 4, 13 | nfiin 5024 |
. . . . 5
⊢
Ⅎ𝑥∩ 𝑛 ∈ 𝑍 ((𝐻‘𝑛)‘𝑚) |
| 15 | 3, 14 | nfiun 5023 |
. . . 4
⊢
Ⅎ𝑥∪ 𝑚 ∈ ℕ ∩ 𝑛 ∈ 𝑍 ((𝐻‘𝑛)‘𝑚) |
| 16 | | finfdm.3 |
. . . . . . . . . . 11
⊢
Ⅎ𝑚𝜑 |
| 17 | | nfv 1914 |
. . . . . . . . . . 11
⊢
Ⅎ𝑚 𝑥 ∈ ∩ 𝑛 ∈ 𝑍 dom (𝐹‘𝑛) |
| 18 | 16, 17 | nfan 1899 |
. . . . . . . . . 10
⊢
Ⅎ𝑚(𝜑 ∧ 𝑥 ∈ ∩
𝑛 ∈ 𝑍 dom (𝐹‘𝑛)) |
| 19 | | nfv 1914 |
. . . . . . . . . 10
⊢
Ⅎ𝑚 𝑦 ∈ ℝ |
| 20 | 18, 19 | nfan 1899 |
. . . . . . . . 9
⊢
Ⅎ𝑚((𝜑 ∧ 𝑥 ∈ ∩
𝑛 ∈ 𝑍 dom (𝐹‘𝑛)) ∧ 𝑦 ∈ ℝ) |
| 21 | | nfv 1914 |
. . . . . . . . 9
⊢
Ⅎ𝑚∀𝑛 ∈ 𝑍 𝑦 ≤ ((𝐹‘𝑛)‘𝑥) |
| 22 | 20, 21 | nfan 1899 |
. . . . . . . 8
⊢
Ⅎ𝑚(((𝜑 ∧ 𝑥 ∈ ∩
𝑛 ∈ 𝑍 dom (𝐹‘𝑛)) ∧ 𝑦 ∈ ℝ) ∧ ∀𝑛 ∈ 𝑍 𝑦 ≤ ((𝐹‘𝑛)‘𝑥)) |
| 23 | | finfdm.1 |
. . . . . . . . . . . . 13
⊢
Ⅎ𝑛𝜑 |
| 24 | | nfii1 5029 |
. . . . . . . . . . . . . 14
⊢
Ⅎ𝑛∩ 𝑛 ∈ 𝑍 dom (𝐹‘𝑛) |
| 25 | 24 | nfel2 2924 |
. . . . . . . . . . . . 13
⊢
Ⅎ𝑛 𝑥 ∈ ∩ 𝑛 ∈ 𝑍 dom (𝐹‘𝑛) |
| 26 | 23, 25 | nfan 1899 |
. . . . . . . . . . . 12
⊢
Ⅎ𝑛(𝜑 ∧ 𝑥 ∈ ∩
𝑛 ∈ 𝑍 dom (𝐹‘𝑛)) |
| 27 | | nfv 1914 |
. . . . . . . . . . . 12
⊢
Ⅎ𝑛 𝑦 ∈ ℝ |
| 28 | 26, 27 | nfan 1899 |
. . . . . . . . . . 11
⊢
Ⅎ𝑛((𝜑 ∧ 𝑥 ∈ ∩
𝑛 ∈ 𝑍 dom (𝐹‘𝑛)) ∧ 𝑦 ∈ ℝ) |
| 29 | | nfra1 3284 |
. . . . . . . . . . 11
⊢
Ⅎ𝑛∀𝑛 ∈ 𝑍 𝑦 ≤ ((𝐹‘𝑛)‘𝑥) |
| 30 | 28, 29 | nfan 1899 |
. . . . . . . . . 10
⊢
Ⅎ𝑛(((𝜑 ∧ 𝑥 ∈ ∩
𝑛 ∈ 𝑍 dom (𝐹‘𝑛)) ∧ 𝑦 ∈ ℝ) ∧ ∀𝑛 ∈ 𝑍 𝑦 ≤ ((𝐹‘𝑛)‘𝑥)) |
| 31 | | nfv 1914 |
. . . . . . . . . 10
⊢
Ⅎ𝑛 𝑚 ∈ ℕ |
| 32 | | nfv 1914 |
. . . . . . . . . 10
⊢
Ⅎ𝑛-𝑦 < 𝑚 |
| 33 | 30, 31, 32 | nf3an 1901 |
. . . . . . . . 9
⊢
Ⅎ𝑛((((𝜑 ∧ 𝑥 ∈ ∩
𝑛 ∈ 𝑍 dom (𝐹‘𝑛)) ∧ 𝑦 ∈ ℝ) ∧ ∀𝑛 ∈ 𝑍 𝑦 ≤ ((𝐹‘𝑛)‘𝑥)) ∧ 𝑚 ∈ ℕ ∧ -𝑦 < 𝑚) |
| 34 | | vex 3484 |
. . . . . . . . . 10
⊢ 𝑥 ∈ V |
| 35 | 34 | a1i 11 |
. . . . . . . . 9
⊢
(((((𝜑 ∧ 𝑥 ∈ ∩ 𝑛 ∈ 𝑍 dom (𝐹‘𝑛)) ∧ 𝑦 ∈ ℝ) ∧ ∀𝑛 ∈ 𝑍 𝑦 ≤ ((𝐹‘𝑛)‘𝑥)) ∧ 𝑚 ∈ ℕ ∧ -𝑦 < 𝑚) → 𝑥 ∈ V) |
| 36 | | simp-4r 784 |
. . . . . . . . . . . . 13
⊢
(((((𝜑 ∧ 𝑥 ∈ ∩ 𝑛 ∈ 𝑍 dom (𝐹‘𝑛)) ∧ 𝑦 ∈ ℝ) ∧ ∀𝑛 ∈ 𝑍 𝑦 ≤ ((𝐹‘𝑛)‘𝑥)) ∧ 𝑛 ∈ 𝑍) → 𝑥 ∈ ∩
𝑛 ∈ 𝑍 dom (𝐹‘𝑛)) |
| 37 | 36 | 3ad2antl1 1186 |
. . . . . . . . . . . 12
⊢
((((((𝜑 ∧ 𝑥 ∈ ∩ 𝑛 ∈ 𝑍 dom (𝐹‘𝑛)) ∧ 𝑦 ∈ ℝ) ∧ ∀𝑛 ∈ 𝑍 𝑦 ≤ ((𝐹‘𝑛)‘𝑥)) ∧ 𝑚 ∈ ℕ ∧ -𝑦 < 𝑚) ∧ 𝑛 ∈ 𝑍) → 𝑥 ∈ ∩
𝑛 ∈ 𝑍 dom (𝐹‘𝑛)) |
| 38 | | simpr 484 |
. . . . . . . . . . . 12
⊢
((((((𝜑 ∧ 𝑥 ∈ ∩ 𝑛 ∈ 𝑍 dom (𝐹‘𝑛)) ∧ 𝑦 ∈ ℝ) ∧ ∀𝑛 ∈ 𝑍 𝑦 ≤ ((𝐹‘𝑛)‘𝑥)) ∧ 𝑚 ∈ ℕ ∧ -𝑦 < 𝑚) ∧ 𝑛 ∈ 𝑍) → 𝑛 ∈ 𝑍) |
| 39 | | eliinid 45116 |
. . . . . . . . . . . 12
⊢ ((𝑥 ∈ ∩ 𝑛 ∈ 𝑍 dom (𝐹‘𝑛) ∧ 𝑛 ∈ 𝑍) → 𝑥 ∈ dom (𝐹‘𝑛)) |
| 40 | 37, 38, 39 | syl2anc 584 |
. . . . . . . . . . 11
⊢
((((((𝜑 ∧ 𝑥 ∈ ∩ 𝑛 ∈ 𝑍 dom (𝐹‘𝑛)) ∧ 𝑦 ∈ ℝ) ∧ ∀𝑛 ∈ 𝑍 𝑦 ≤ ((𝐹‘𝑛)‘𝑥)) ∧ 𝑚 ∈ ℕ ∧ -𝑦 < 𝑚) ∧ 𝑛 ∈ 𝑍) → 𝑥 ∈ dom (𝐹‘𝑛)) |
| 41 | | simpl2 1193 |
. . . . . . . . . . . . 13
⊢
((((((𝜑 ∧ 𝑥 ∈ ∩ 𝑛 ∈ 𝑍 dom (𝐹‘𝑛)) ∧ 𝑦 ∈ ℝ) ∧ ∀𝑛 ∈ 𝑍 𝑦 ≤ ((𝐹‘𝑛)‘𝑥)) ∧ 𝑚 ∈ ℕ ∧ -𝑦 < 𝑚) ∧ 𝑛 ∈ 𝑍) → 𝑚 ∈ ℕ) |
| 42 | | nnre 12273 |
. . . . . . . . . . . . . . 15
⊢ (𝑚 ∈ ℕ → 𝑚 ∈
ℝ) |
| 43 | 42 | renegcld 11690 |
. . . . . . . . . . . . . 14
⊢ (𝑚 ∈ ℕ → -𝑚 ∈
ℝ) |
| 44 | 43 | rexrd 11311 |
. . . . . . . . . . . . 13
⊢ (𝑚 ∈ ℕ → -𝑚 ∈
ℝ*) |
| 45 | 41, 44 | syl 17 |
. . . . . . . . . . . 12
⊢
((((((𝜑 ∧ 𝑥 ∈ ∩ 𝑛 ∈ 𝑍 dom (𝐹‘𝑛)) ∧ 𝑦 ∈ ℝ) ∧ ∀𝑛 ∈ 𝑍 𝑦 ≤ ((𝐹‘𝑛)‘𝑥)) ∧ 𝑚 ∈ ℕ ∧ -𝑦 < 𝑚) ∧ 𝑛 ∈ 𝑍) → -𝑚 ∈ ℝ*) |
| 46 | | simpllr 776 |
. . . . . . . . . . . . . 14
⊢
(((((𝜑 ∧ 𝑥 ∈ ∩ 𝑛 ∈ 𝑍 dom (𝐹‘𝑛)) ∧ 𝑦 ∈ ℝ) ∧ ∀𝑛 ∈ 𝑍 𝑦 ≤ ((𝐹‘𝑛)‘𝑥)) ∧ 𝑛 ∈ 𝑍) → 𝑦 ∈ ℝ) |
| 47 | | rexr 11307 |
. . . . . . . . . . . . . 14
⊢ (𝑦 ∈ ℝ → 𝑦 ∈
ℝ*) |
| 48 | 46, 47 | syl 17 |
. . . . . . . . . . . . 13
⊢
(((((𝜑 ∧ 𝑥 ∈ ∩ 𝑛 ∈ 𝑍 dom (𝐹‘𝑛)) ∧ 𝑦 ∈ ℝ) ∧ ∀𝑛 ∈ 𝑍 𝑦 ≤ ((𝐹‘𝑛)‘𝑥)) ∧ 𝑛 ∈ 𝑍) → 𝑦 ∈ ℝ*) |
| 49 | 48 | 3ad2antl1 1186 |
. . . . . . . . . . . 12
⊢
((((((𝜑 ∧ 𝑥 ∈ ∩ 𝑛 ∈ 𝑍 dom (𝐹‘𝑛)) ∧ 𝑦 ∈ ℝ) ∧ ∀𝑛 ∈ 𝑍 𝑦 ≤ ((𝐹‘𝑛)‘𝑥)) ∧ 𝑚 ∈ ℕ ∧ -𝑦 < 𝑚) ∧ 𝑛 ∈ 𝑍) → 𝑦 ∈ ℝ*) |
| 50 | | simp-4l 783 |
. . . . . . . . . . . . . 14
⊢
(((((𝜑 ∧ 𝑥 ∈ ∩ 𝑛 ∈ 𝑍 dom (𝐹‘𝑛)) ∧ 𝑦 ∈ ℝ) ∧ ∀𝑛 ∈ 𝑍 𝑦 ≤ ((𝐹‘𝑛)‘𝑥)) ∧ 𝑛 ∈ 𝑍) → 𝜑) |
| 51 | 50 | 3ad2antl1 1186 |
. . . . . . . . . . . . 13
⊢
((((((𝜑 ∧ 𝑥 ∈ ∩ 𝑛 ∈ 𝑍 dom (𝐹‘𝑛)) ∧ 𝑦 ∈ ℝ) ∧ ∀𝑛 ∈ 𝑍 𝑦 ≤ ((𝐹‘𝑛)‘𝑥)) ∧ 𝑚 ∈ ℕ ∧ -𝑦 < 𝑚) ∧ 𝑛 ∈ 𝑍) → 𝜑) |
| 52 | | finfdm.5 |
. . . . . . . . . . . . . . 15
⊢ ((𝜑 ∧ 𝑛 ∈ 𝑍) → (𝐹‘𝑛):dom (𝐹‘𝑛)⟶ℝ*) |
| 53 | 52 | 3adant3 1133 |
. . . . . . . . . . . . . 14
⊢ ((𝜑 ∧ 𝑛 ∈ 𝑍 ∧ 𝑥 ∈ dom (𝐹‘𝑛)) → (𝐹‘𝑛):dom (𝐹‘𝑛)⟶ℝ*) |
| 54 | | simp3 1139 |
. . . . . . . . . . . . . 14
⊢ ((𝜑 ∧ 𝑛 ∈ 𝑍 ∧ 𝑥 ∈ dom (𝐹‘𝑛)) → 𝑥 ∈ dom (𝐹‘𝑛)) |
| 55 | 53, 54 | ffvelcdmd 7105 |
. . . . . . . . . . . . 13
⊢ ((𝜑 ∧ 𝑛 ∈ 𝑍 ∧ 𝑥 ∈ dom (𝐹‘𝑛)) → ((𝐹‘𝑛)‘𝑥) ∈
ℝ*) |
| 56 | 51, 38, 40, 55 | syl3anc 1373 |
. . . . . . . . . . . 12
⊢
((((((𝜑 ∧ 𝑥 ∈ ∩ 𝑛 ∈ 𝑍 dom (𝐹‘𝑛)) ∧ 𝑦 ∈ ℝ) ∧ ∀𝑛 ∈ 𝑍 𝑦 ≤ ((𝐹‘𝑛)‘𝑥)) ∧ 𝑚 ∈ ℕ ∧ -𝑦 < 𝑚) ∧ 𝑛 ∈ 𝑍) → ((𝐹‘𝑛)‘𝑥) ∈
ℝ*) |
| 57 | 46 | 3ad2antl1 1186 |
. . . . . . . . . . . . 13
⊢
((((((𝜑 ∧ 𝑥 ∈ ∩ 𝑛 ∈ 𝑍 dom (𝐹‘𝑛)) ∧ 𝑦 ∈ ℝ) ∧ ∀𝑛 ∈ 𝑍 𝑦 ≤ ((𝐹‘𝑛)‘𝑥)) ∧ 𝑚 ∈ ℕ ∧ -𝑦 < 𝑚) ∧ 𝑛 ∈ 𝑍) → 𝑦 ∈ ℝ) |
| 58 | | simpl3 1194 |
. . . . . . . . . . . . 13
⊢
((((((𝜑 ∧ 𝑥 ∈ ∩ 𝑛 ∈ 𝑍 dom (𝐹‘𝑛)) ∧ 𝑦 ∈ ℝ) ∧ ∀𝑛 ∈ 𝑍 𝑦 ≤ ((𝐹‘𝑛)‘𝑥)) ∧ 𝑚 ∈ ℕ ∧ -𝑦 < 𝑚) ∧ 𝑛 ∈ 𝑍) → -𝑦 < 𝑚) |
| 59 | | simp1 1137 |
. . . . . . . . . . . . . 14
⊢ ((𝑦 ∈ ℝ ∧ 𝑚 ∈ ℕ ∧ -𝑦 < 𝑚) → 𝑦 ∈ ℝ) |
| 60 | 42 | 3ad2ant2 1135 |
. . . . . . . . . . . . . 14
⊢ ((𝑦 ∈ ℝ ∧ 𝑚 ∈ ℕ ∧ -𝑦 < 𝑚) → 𝑚 ∈ ℝ) |
| 61 | | simp3 1139 |
. . . . . . . . . . . . . 14
⊢ ((𝑦 ∈ ℝ ∧ 𝑚 ∈ ℕ ∧ -𝑦 < 𝑚) → -𝑦 < 𝑚) |
| 62 | 59, 60, 61 | ltnegcon1d 11843 |
. . . . . . . . . . . . 13
⊢ ((𝑦 ∈ ℝ ∧ 𝑚 ∈ ℕ ∧ -𝑦 < 𝑚) → -𝑚 < 𝑦) |
| 63 | 57, 41, 58, 62 | syl3anc 1373 |
. . . . . . . . . . . 12
⊢
((((((𝜑 ∧ 𝑥 ∈ ∩ 𝑛 ∈ 𝑍 dom (𝐹‘𝑛)) ∧ 𝑦 ∈ ℝ) ∧ ∀𝑛 ∈ 𝑍 𝑦 ≤ ((𝐹‘𝑛)‘𝑥)) ∧ 𝑚 ∈ ℕ ∧ -𝑦 < 𝑚) ∧ 𝑛 ∈ 𝑍) → -𝑚 < 𝑦) |
| 64 | | simpl1r 1226 |
. . . . . . . . . . . . 13
⊢
((((((𝜑 ∧ 𝑥 ∈ ∩ 𝑛 ∈ 𝑍 dom (𝐹‘𝑛)) ∧ 𝑦 ∈ ℝ) ∧ ∀𝑛 ∈ 𝑍 𝑦 ≤ ((𝐹‘𝑛)‘𝑥)) ∧ 𝑚 ∈ ℕ ∧ -𝑦 < 𝑚) ∧ 𝑛 ∈ 𝑍) → ∀𝑛 ∈ 𝑍 𝑦 ≤ ((𝐹‘𝑛)‘𝑥)) |
| 65 | | rspa 3248 |
. . . . . . . . . . . . 13
⊢
((∀𝑛 ∈
𝑍 𝑦 ≤ ((𝐹‘𝑛)‘𝑥) ∧ 𝑛 ∈ 𝑍) → 𝑦 ≤ ((𝐹‘𝑛)‘𝑥)) |
| 66 | 64, 38, 65 | syl2anc 584 |
. . . . . . . . . . . 12
⊢
((((((𝜑 ∧ 𝑥 ∈ ∩ 𝑛 ∈ 𝑍 dom (𝐹‘𝑛)) ∧ 𝑦 ∈ ℝ) ∧ ∀𝑛 ∈ 𝑍 𝑦 ≤ ((𝐹‘𝑛)‘𝑥)) ∧ 𝑚 ∈ ℕ ∧ -𝑦 < 𝑚) ∧ 𝑛 ∈ 𝑍) → 𝑦 ≤ ((𝐹‘𝑛)‘𝑥)) |
| 67 | 45, 49, 56, 63, 66 | xrltletrd 13203 |
. . . . . . . . . . 11
⊢
((((((𝜑 ∧ 𝑥 ∈ ∩ 𝑛 ∈ 𝑍 dom (𝐹‘𝑛)) ∧ 𝑦 ∈ ℝ) ∧ ∀𝑛 ∈ 𝑍 𝑦 ≤ ((𝐹‘𝑛)‘𝑥)) ∧ 𝑚 ∈ ℕ ∧ -𝑦 < 𝑚) ∧ 𝑛 ∈ 𝑍) → -𝑚 < ((𝐹‘𝑛)‘𝑥)) |
| 68 | 40, 67 | rabidd 45160 |
. . . . . . . . . 10
⊢
((((((𝜑 ∧ 𝑥 ∈ ∩ 𝑛 ∈ 𝑍 dom (𝐹‘𝑛)) ∧ 𝑦 ∈ ℝ) ∧ ∀𝑛 ∈ 𝑍 𝑦 ≤ ((𝐹‘𝑛)‘𝑥)) ∧ 𝑚 ∈ ℕ ∧ -𝑦 < 𝑚) ∧ 𝑛 ∈ 𝑍) → 𝑥 ∈ {𝑥 ∈ dom (𝐹‘𝑛) ∣ -𝑚 < ((𝐹‘𝑛)‘𝑥)}) |
| 69 | | id 22 |
. . . . . . . . . . . . . 14
⊢ (𝑛 ∈ 𝑍 → 𝑛 ∈ 𝑍) |
| 70 | | nnex 12272 |
. . . . . . . . . . . . . . . 16
⊢ ℕ
∈ V |
| 71 | 70 | mptex 7243 |
. . . . . . . . . . . . . . 15
⊢ (𝑚 ∈ ℕ ↦ {𝑥 ∈ dom (𝐹‘𝑛) ∣ -𝑚 < ((𝐹‘𝑛)‘𝑥)}) ∈ V |
| 72 | 71 | a1i 11 |
. . . . . . . . . . . . . 14
⊢ (𝑛 ∈ 𝑍 → (𝑚 ∈ ℕ ↦ {𝑥 ∈ dom (𝐹‘𝑛) ∣ -𝑚 < ((𝐹‘𝑛)‘𝑥)}) ∈ V) |
| 73 | 5 | fvmpt2 7027 |
. . . . . . . . . . . . . 14
⊢ ((𝑛 ∈ 𝑍 ∧ (𝑚 ∈ ℕ ↦ {𝑥 ∈ dom (𝐹‘𝑛) ∣ -𝑚 < ((𝐹‘𝑛)‘𝑥)}) ∈ V) → (𝐻‘𝑛) = (𝑚 ∈ ℕ ↦ {𝑥 ∈ dom (𝐹‘𝑛) ∣ -𝑚 < ((𝐹‘𝑛)‘𝑥)})) |
| 74 | 69, 72, 73 | syl2anc 584 |
. . . . . . . . . . . . 13
⊢ (𝑛 ∈ 𝑍 → (𝐻‘𝑛) = (𝑚 ∈ ℕ ↦ {𝑥 ∈ dom (𝐹‘𝑛) ∣ -𝑚 < ((𝐹‘𝑛)‘𝑥)})) |
| 75 | | finfdm.4 |
. . . . . . . . . . . . . . . . 17
⊢
Ⅎ𝑥𝐹 |
| 76 | 75, 10 | nffv 6916 |
. . . . . . . . . . . . . . . 16
⊢
Ⅎ𝑥(𝐹‘𝑛) |
| 77 | 76 | nfdm 5962 |
. . . . . . . . . . . . . . 15
⊢
Ⅎ𝑥dom
(𝐹‘𝑛) |
| 78 | | fvex 6919 |
. . . . . . . . . . . . . . . 16
⊢ (𝐹‘𝑛) ∈ V |
| 79 | 78 | dmex 7931 |
. . . . . . . . . . . . . . 15
⊢ dom
(𝐹‘𝑛) ∈ V |
| 80 | 77, 79 | rabexf 45139 |
. . . . . . . . . . . . . 14
⊢ {𝑥 ∈ dom (𝐹‘𝑛) ∣ -𝑚 < ((𝐹‘𝑛)‘𝑥)} ∈ V |
| 81 | 80 | a1i 11 |
. . . . . . . . . . . . 13
⊢ ((𝑛 ∈ 𝑍 ∧ 𝑚 ∈ ℕ) → {𝑥 ∈ dom (𝐹‘𝑛) ∣ -𝑚 < ((𝐹‘𝑛)‘𝑥)} ∈ V) |
| 82 | 74, 81 | fvmpt2d 7029 |
. . . . . . . . . . . 12
⊢ ((𝑛 ∈ 𝑍 ∧ 𝑚 ∈ ℕ) → ((𝐻‘𝑛)‘𝑚) = {𝑥 ∈ dom (𝐹‘𝑛) ∣ -𝑚 < ((𝐹‘𝑛)‘𝑥)}) |
| 83 | 82 | eqcomd 2743 |
. . . . . . . . . . 11
⊢ ((𝑛 ∈ 𝑍 ∧ 𝑚 ∈ ℕ) → {𝑥 ∈ dom (𝐹‘𝑛) ∣ -𝑚 < ((𝐹‘𝑛)‘𝑥)} = ((𝐻‘𝑛)‘𝑚)) |
| 84 | 38, 41, 83 | syl2anc 584 |
. . . . . . . . . 10
⊢
((((((𝜑 ∧ 𝑥 ∈ ∩ 𝑛 ∈ 𝑍 dom (𝐹‘𝑛)) ∧ 𝑦 ∈ ℝ) ∧ ∀𝑛 ∈ 𝑍 𝑦 ≤ ((𝐹‘𝑛)‘𝑥)) ∧ 𝑚 ∈ ℕ ∧ -𝑦 < 𝑚) ∧ 𝑛 ∈ 𝑍) → {𝑥 ∈ dom (𝐹‘𝑛) ∣ -𝑚 < ((𝐹‘𝑛)‘𝑥)} = ((𝐻‘𝑛)‘𝑚)) |
| 85 | 68, 84 | eleqtrd 2843 |
. . . . . . . . 9
⊢
((((((𝜑 ∧ 𝑥 ∈ ∩ 𝑛 ∈ 𝑍 dom (𝐹‘𝑛)) ∧ 𝑦 ∈ ℝ) ∧ ∀𝑛 ∈ 𝑍 𝑦 ≤ ((𝐹‘𝑛)‘𝑥)) ∧ 𝑚 ∈ ℕ ∧ -𝑦 < 𝑚) ∧ 𝑛 ∈ 𝑍) → 𝑥 ∈ ((𝐻‘𝑛)‘𝑚)) |
| 86 | 33, 35, 85 | eliind2 45135 |
. . . . . . . 8
⊢
(((((𝜑 ∧ 𝑥 ∈ ∩ 𝑛 ∈ 𝑍 dom (𝐹‘𝑛)) ∧ 𝑦 ∈ ℝ) ∧ ∀𝑛 ∈ 𝑍 𝑦 ≤ ((𝐹‘𝑛)‘𝑥)) ∧ 𝑚 ∈ ℕ ∧ -𝑦 < 𝑚) → 𝑥 ∈ ∩
𝑛 ∈ 𝑍 ((𝐻‘𝑛)‘𝑚)) |
| 87 | | renegcl 11572 |
. . . . . . . . . 10
⊢ (𝑦 ∈ ℝ → -𝑦 ∈
ℝ) |
| 88 | 87 | archd 45167 |
. . . . . . . . 9
⊢ (𝑦 ∈ ℝ →
∃𝑚 ∈ ℕ
-𝑦 < 𝑚) |
| 89 | 88 | ad2antlr 727 |
. . . . . . . 8
⊢ ((((𝜑 ∧ 𝑥 ∈ ∩
𝑛 ∈ 𝑍 dom (𝐹‘𝑛)) ∧ 𝑦 ∈ ℝ) ∧ ∀𝑛 ∈ 𝑍 𝑦 ≤ ((𝐹‘𝑛)‘𝑥)) → ∃𝑚 ∈ ℕ -𝑦 < 𝑚) |
| 90 | 22, 86, 89 | reximdd 45153 |
. . . . . . 7
⊢ ((((𝜑 ∧ 𝑥 ∈ ∩
𝑛 ∈ 𝑍 dom (𝐹‘𝑛)) ∧ 𝑦 ∈ ℝ) ∧ ∀𝑛 ∈ 𝑍 𝑦 ≤ ((𝐹‘𝑛)‘𝑥)) → ∃𝑚 ∈ ℕ 𝑥 ∈ ∩
𝑛 ∈ 𝑍 ((𝐻‘𝑛)‘𝑚)) |
| 91 | 90 | rexlimdva2 3157 |
. . . . . 6
⊢ ((𝜑 ∧ 𝑥 ∈ ∩
𝑛 ∈ 𝑍 dom (𝐹‘𝑛)) → (∃𝑦 ∈ ℝ ∀𝑛 ∈ 𝑍 𝑦 ≤ ((𝐹‘𝑛)‘𝑥) → ∃𝑚 ∈ ℕ 𝑥 ∈ ∩
𝑛 ∈ 𝑍 ((𝐻‘𝑛)‘𝑚))) |
| 92 | 91 | 3impia 1118 |
. . . . 5
⊢ ((𝜑 ∧ 𝑥 ∈ ∩
𝑛 ∈ 𝑍 dom (𝐹‘𝑛) ∧ ∃𝑦 ∈ ℝ ∀𝑛 ∈ 𝑍 𝑦 ≤ ((𝐹‘𝑛)‘𝑥)) → ∃𝑚 ∈ ℕ 𝑥 ∈ ∩
𝑛 ∈ 𝑍 ((𝐻‘𝑛)‘𝑚)) |
| 93 | | eliun 4995 |
. . . . 5
⊢ (𝑥 ∈ ∪ 𝑚 ∈ ℕ ∩ 𝑛 ∈ 𝑍 ((𝐻‘𝑛)‘𝑚) ↔ ∃𝑚 ∈ ℕ 𝑥 ∈ ∩
𝑛 ∈ 𝑍 ((𝐻‘𝑛)‘𝑚)) |
| 94 | 92, 93 | sylibr 234 |
. . . 4
⊢ ((𝜑 ∧ 𝑥 ∈ ∩
𝑛 ∈ 𝑍 dom (𝐹‘𝑛) ∧ ∃𝑦 ∈ ℝ ∀𝑛 ∈ 𝑍 𝑦 ≤ ((𝐹‘𝑛)‘𝑥)) → 𝑥 ∈ ∪
𝑚 ∈ ℕ ∩ 𝑛 ∈ 𝑍 ((𝐻‘𝑛)‘𝑚)) |
| 95 | 2, 15, 94 | rabssd 45147 |
. . 3
⊢ (𝜑 → {𝑥 ∈ ∩
𝑛 ∈ 𝑍 dom (𝐹‘𝑛) ∣ ∃𝑦 ∈ ℝ ∀𝑛 ∈ 𝑍 𝑦 ≤ ((𝐹‘𝑛)‘𝑥)} ⊆ ∪ 𝑚 ∈ ℕ ∩ 𝑛 ∈ 𝑍 ((𝐻‘𝑛)‘𝑚)) |
| 96 | 1, 95 | eqsstrid 4022 |
. 2
⊢ (𝜑 → 𝐷 ⊆ ∪
𝑚 ∈ ℕ ∩ 𝑛 ∈ 𝑍 ((𝐻‘𝑛)‘𝑚)) |
| 97 | | nfcv 2905 |
. . 3
⊢
Ⅎ𝑚𝐷 |
| 98 | | nfv 1914 |
. . . . 5
⊢
Ⅎ𝑥 𝑚 ∈ ℕ |
| 99 | 2, 98 | nfan 1899 |
. . . 4
⊢
Ⅎ𝑥(𝜑 ∧ 𝑚 ∈ ℕ) |
| 100 | | nfrab1 3457 |
. . . . 5
⊢
Ⅎ𝑥{𝑥 ∈ ∩
𝑛 ∈ 𝑍 dom (𝐹‘𝑛) ∣ ∃𝑦 ∈ ℝ ∀𝑛 ∈ 𝑍 𝑦 ≤ ((𝐹‘𝑛)‘𝑥)} |
| 101 | 1, 100 | nfcxfr 2903 |
. . . 4
⊢
Ⅎ𝑥𝐷 |
| 102 | 23, 31 | nfan 1899 |
. . . . . . . 8
⊢
Ⅎ𝑛(𝜑 ∧ 𝑚 ∈ ℕ) |
| 103 | | nfii1 5029 |
. . . . . . . . 9
⊢
Ⅎ𝑛∩ 𝑛 ∈ 𝑍 ((𝐻‘𝑛)‘𝑚) |
| 104 | 103 | nfel2 2924 |
. . . . . . . 8
⊢
Ⅎ𝑛 𝑥 ∈ ∩ 𝑛 ∈ 𝑍 ((𝐻‘𝑛)‘𝑚) |
| 105 | 102, 104 | nfan 1899 |
. . . . . . 7
⊢
Ⅎ𝑛((𝜑 ∧ 𝑚 ∈ ℕ) ∧ 𝑥 ∈ ∩
𝑛 ∈ 𝑍 ((𝐻‘𝑛)‘𝑚)) |
| 106 | | simpr 484 |
. . . . . . 7
⊢ (((𝜑 ∧ 𝑚 ∈ ℕ) ∧ 𝑥 ∈ ∩
𝑛 ∈ 𝑍 ((𝐻‘𝑛)‘𝑚)) → 𝑥 ∈ ∩
𝑛 ∈ 𝑍 ((𝐻‘𝑛)‘𝑚)) |
| 107 | | eliinid 45116 |
. . . . . . . . . 10
⊢ ((𝑥 ∈ ∩ 𝑛 ∈ 𝑍 ((𝐻‘𝑛)‘𝑚) ∧ 𝑛 ∈ 𝑍) → 𝑥 ∈ ((𝐻‘𝑛)‘𝑚)) |
| 108 | 107 | adantll 714 |
. . . . . . . . 9
⊢ ((((𝜑 ∧ 𝑚 ∈ ℕ) ∧ 𝑥 ∈ ∩
𝑛 ∈ 𝑍 ((𝐻‘𝑛)‘𝑚)) ∧ 𝑛 ∈ 𝑍) → 𝑥 ∈ ((𝐻‘𝑛)‘𝑚)) |
| 109 | 69 | adantl 481 |
. . . . . . . . . 10
⊢ ((((𝜑 ∧ 𝑚 ∈ ℕ) ∧ 𝑥 ∈ ∩
𝑛 ∈ 𝑍 ((𝐻‘𝑛)‘𝑚)) ∧ 𝑛 ∈ 𝑍) → 𝑛 ∈ 𝑍) |
| 110 | | simpllr 776 |
. . . . . . . . . 10
⊢ ((((𝜑 ∧ 𝑚 ∈ ℕ) ∧ 𝑥 ∈ ∩
𝑛 ∈ 𝑍 ((𝐻‘𝑛)‘𝑚)) ∧ 𝑛 ∈ 𝑍) → 𝑚 ∈ ℕ) |
| 111 | 109, 110,
82 | syl2anc 584 |
. . . . . . . . 9
⊢ ((((𝜑 ∧ 𝑚 ∈ ℕ) ∧ 𝑥 ∈ ∩
𝑛 ∈ 𝑍 ((𝐻‘𝑛)‘𝑚)) ∧ 𝑛 ∈ 𝑍) → ((𝐻‘𝑛)‘𝑚) = {𝑥 ∈ dom (𝐹‘𝑛) ∣ -𝑚 < ((𝐹‘𝑛)‘𝑥)}) |
| 112 | 108, 111 | eleqtrd 2843 |
. . . . . . . 8
⊢ ((((𝜑 ∧ 𝑚 ∈ ℕ) ∧ 𝑥 ∈ ∩
𝑛 ∈ 𝑍 ((𝐻‘𝑛)‘𝑚)) ∧ 𝑛 ∈ 𝑍) → 𝑥 ∈ {𝑥 ∈ dom (𝐹‘𝑛) ∣ -𝑚 < ((𝐹‘𝑛)‘𝑥)}) |
| 113 | | rabidim1 3459 |
. . . . . . . 8
⊢ (𝑥 ∈ {𝑥 ∈ dom (𝐹‘𝑛) ∣ -𝑚 < ((𝐹‘𝑛)‘𝑥)} → 𝑥 ∈ dom (𝐹‘𝑛)) |
| 114 | 112, 113 | syl 17 |
. . . . . . 7
⊢ ((((𝜑 ∧ 𝑚 ∈ ℕ) ∧ 𝑥 ∈ ∩
𝑛 ∈ 𝑍 ((𝐻‘𝑛)‘𝑚)) ∧ 𝑛 ∈ 𝑍) → 𝑥 ∈ dom (𝐹‘𝑛)) |
| 115 | 105, 106,
114 | eliind2 45135 |
. . . . . 6
⊢ (((𝜑 ∧ 𝑚 ∈ ℕ) ∧ 𝑥 ∈ ∩
𝑛 ∈ 𝑍 ((𝐻‘𝑛)‘𝑚)) → 𝑥 ∈ ∩
𝑛 ∈ 𝑍 dom (𝐹‘𝑛)) |
| 116 | 43 | ad2antlr 727 |
. . . . . . 7
⊢ (((𝜑 ∧ 𝑚 ∈ ℕ) ∧ 𝑥 ∈ ∩
𝑛 ∈ 𝑍 ((𝐻‘𝑛)‘𝑚)) → -𝑚 ∈ ℝ) |
| 117 | | breq1 5146 |
. . . . . . . . 9
⊢ (𝑦 = -𝑚 → (𝑦 ≤ ((𝐹‘𝑛)‘𝑥) ↔ -𝑚 ≤ ((𝐹‘𝑛)‘𝑥))) |
| 118 | 117 | ralbidv 3178 |
. . . . . . . 8
⊢ (𝑦 = -𝑚 → (∀𝑛 ∈ 𝑍 𝑦 ≤ ((𝐹‘𝑛)‘𝑥) ↔ ∀𝑛 ∈ 𝑍 -𝑚 ≤ ((𝐹‘𝑛)‘𝑥))) |
| 119 | 118 | adantl 481 |
. . . . . . 7
⊢ ((((𝜑 ∧ 𝑚 ∈ ℕ) ∧ 𝑥 ∈ ∩
𝑛 ∈ 𝑍 ((𝐻‘𝑛)‘𝑚)) ∧ 𝑦 = -𝑚) → (∀𝑛 ∈ 𝑍 𝑦 ≤ ((𝐹‘𝑛)‘𝑥) ↔ ∀𝑛 ∈ 𝑍 -𝑚 ≤ ((𝐹‘𝑛)‘𝑥))) |
| 120 | 110, 44 | syl 17 |
. . . . . . . . 9
⊢ ((((𝜑 ∧ 𝑚 ∈ ℕ) ∧ 𝑥 ∈ ∩
𝑛 ∈ 𝑍 ((𝐻‘𝑛)‘𝑚)) ∧ 𝑛 ∈ 𝑍) → -𝑚 ∈ ℝ*) |
| 121 | | simplll 775 |
. . . . . . . . . 10
⊢ ((((𝜑 ∧ 𝑚 ∈ ℕ) ∧ 𝑥 ∈ ∩
𝑛 ∈ 𝑍 ((𝐻‘𝑛)‘𝑚)) ∧ 𝑛 ∈ 𝑍) → 𝜑) |
| 122 | 121, 109,
114, 55 | syl3anc 1373 |
. . . . . . . . 9
⊢ ((((𝜑 ∧ 𝑚 ∈ ℕ) ∧ 𝑥 ∈ ∩
𝑛 ∈ 𝑍 ((𝐻‘𝑛)‘𝑚)) ∧ 𝑛 ∈ 𝑍) → ((𝐹‘𝑛)‘𝑥) ∈
ℝ*) |
| 123 | | rabidim2 45107 |
. . . . . . . . . 10
⊢ (𝑥 ∈ {𝑥 ∈ dom (𝐹‘𝑛) ∣ -𝑚 < ((𝐹‘𝑛)‘𝑥)} → -𝑚 < ((𝐹‘𝑛)‘𝑥)) |
| 124 | 112, 123 | syl 17 |
. . . . . . . . 9
⊢ ((((𝜑 ∧ 𝑚 ∈ ℕ) ∧ 𝑥 ∈ ∩
𝑛 ∈ 𝑍 ((𝐻‘𝑛)‘𝑚)) ∧ 𝑛 ∈ 𝑍) → -𝑚 < ((𝐹‘𝑛)‘𝑥)) |
| 125 | 120, 122,
124 | xrltled 13192 |
. . . . . . . 8
⊢ ((((𝜑 ∧ 𝑚 ∈ ℕ) ∧ 𝑥 ∈ ∩
𝑛 ∈ 𝑍 ((𝐻‘𝑛)‘𝑚)) ∧ 𝑛 ∈ 𝑍) → -𝑚 ≤ ((𝐹‘𝑛)‘𝑥)) |
| 126 | 105, 125 | ralrimia 3258 |
. . . . . . 7
⊢ (((𝜑 ∧ 𝑚 ∈ ℕ) ∧ 𝑥 ∈ ∩
𝑛 ∈ 𝑍 ((𝐻‘𝑛)‘𝑚)) → ∀𝑛 ∈ 𝑍 -𝑚 ≤ ((𝐹‘𝑛)‘𝑥)) |
| 127 | 116, 119,
126 | rspcedvd 3624 |
. . . . . 6
⊢ (((𝜑 ∧ 𝑚 ∈ ℕ) ∧ 𝑥 ∈ ∩
𝑛 ∈ 𝑍 ((𝐻‘𝑛)‘𝑚)) → ∃𝑦 ∈ ℝ ∀𝑛 ∈ 𝑍 𝑦 ≤ ((𝐹‘𝑛)‘𝑥)) |
| 128 | 115, 127 | rabidd 45160 |
. . . . 5
⊢ (((𝜑 ∧ 𝑚 ∈ ℕ) ∧ 𝑥 ∈ ∩
𝑛 ∈ 𝑍 ((𝐻‘𝑛)‘𝑚)) → 𝑥 ∈ {𝑥 ∈ ∩
𝑛 ∈ 𝑍 dom (𝐹‘𝑛) ∣ ∃𝑦 ∈ ℝ ∀𝑛 ∈ 𝑍 𝑦 ≤ ((𝐹‘𝑛)‘𝑥)}) |
| 129 | 128, 1 | eleqtrrdi 2852 |
. . . 4
⊢ (((𝜑 ∧ 𝑚 ∈ ℕ) ∧ 𝑥 ∈ ∩
𝑛 ∈ 𝑍 ((𝐻‘𝑛)‘𝑚)) → 𝑥 ∈ 𝐷) |
| 130 | 99, 14, 101, 129 | ssdf2 45146 |
. . 3
⊢ ((𝜑 ∧ 𝑚 ∈ ℕ) → ∩ 𝑛 ∈ 𝑍 ((𝐻‘𝑛)‘𝑚) ⊆ 𝐷) |
| 131 | 16, 97, 130 | iunssdf 45161 |
. 2
⊢ (𝜑 → ∪ 𝑚 ∈ ℕ ∩ 𝑛 ∈ 𝑍 ((𝐻‘𝑛)‘𝑚) ⊆ 𝐷) |
| 132 | 96, 131 | eqssd 4001 |
1
⊢ (𝜑 → 𝐷 = ∪ 𝑚 ∈ ℕ ∩ 𝑛 ∈ 𝑍 ((𝐻‘𝑛)‘𝑚)) |