Proof of Theorem fsupdm
Step | Hyp | Ref
| Expression |
1 | | fsupdm.6 |
. . 3
⊢ 𝐷 = {𝑥 ∈ ∩
𝑛 ∈ 𝑍 dom (𝐹‘𝑛) ∣ ∃𝑦 ∈ ℝ ∀𝑛 ∈ 𝑍 ((𝐹‘𝑛)‘𝑥) ≤ 𝑦} |
2 | | fsupdm.2 |
. . . 4
⊢
Ⅎ𝑥𝜑 |
3 | | nfcv 2905 |
. . . . 5
⊢
Ⅎ𝑥ℕ |
4 | | nfcv 2905 |
. . . . . 6
⊢
Ⅎ𝑥𝑍 |
5 | | fsupdm.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 | | fsupdm.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 | | fsupdm.1 |
. . . . . . . . . . . . 13
⊢
Ⅎ𝑛𝜑 |
24 | | nfii1 4987 |
. . . . . . . . . . . . . 14
⊢
Ⅎ𝑛∩ 𝑛 ∈ 𝑍 dom (𝐹‘𝑛) |
25 | 24 | nfcri 2892 |
. . . . . . . . . . . . 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 | | simp-4l 781 |
. . . . . . . . . . . . . . 15
⊢
(((((𝜑 ∧ 𝑥 ∈ ∩ 𝑛 ∈ 𝑍 dom (𝐹‘𝑛)) ∧ 𝑦 ∈ ℝ) ∧ ∀𝑛 ∈ 𝑍 ((𝐹‘𝑛)‘𝑥) ≤ 𝑦) ∧ 𝑛 ∈ 𝑍) → 𝜑) |
42 | 41 | 3ad2antl1 1185 |
. . . . . . . . . . . . . 14
⊢
((((((𝜑 ∧ 𝑥 ∈ ∩ 𝑛 ∈ 𝑍 dom (𝐹‘𝑛)) ∧ 𝑦 ∈ ℝ) ∧ ∀𝑛 ∈ 𝑍 ((𝐹‘𝑛)‘𝑥) ≤ 𝑦) ∧ 𝑚 ∈ ℕ ∧ 𝑦 < 𝑚) ∧ 𝑛 ∈ 𝑍) → 𝜑) |
43 | | fsupdm.5 |
. . . . . . . . . . . . . 14
⊢ ((𝜑 ∧ 𝑛 ∈ 𝑍) → (𝐹‘𝑛):dom (𝐹‘𝑛)⟶ℝ*) |
44 | 42, 38, 43 | syl2anc 584 |
. . . . . . . . . . . . 13
⊢
((((((𝜑 ∧ 𝑥 ∈ ∩ 𝑛 ∈ 𝑍 dom (𝐹‘𝑛)) ∧ 𝑦 ∈ ℝ) ∧ ∀𝑛 ∈ 𝑍 ((𝐹‘𝑛)‘𝑥) ≤ 𝑦) ∧ 𝑚 ∈ ℕ ∧ 𝑦 < 𝑚) ∧ 𝑛 ∈ 𝑍) → (𝐹‘𝑛):dom (𝐹‘𝑛)⟶ℝ*) |
45 | 44, 40 | ffvelcdmd 7032 |
. . . . . . . . . . . 12
⊢
((((((𝜑 ∧ 𝑥 ∈ ∩ 𝑛 ∈ 𝑍 dom (𝐹‘𝑛)) ∧ 𝑦 ∈ ℝ) ∧ ∀𝑛 ∈ 𝑍 ((𝐹‘𝑛)‘𝑥) ≤ 𝑦) ∧ 𝑚 ∈ ℕ ∧ 𝑦 < 𝑚) ∧ 𝑛 ∈ 𝑍) → ((𝐹‘𝑛)‘𝑥) ∈
ℝ*) |
46 | | simpllr 774 |
. . . . . . . . . . . . . 14
⊢
(((((𝜑 ∧ 𝑥 ∈ ∩ 𝑛 ∈ 𝑍 dom (𝐹‘𝑛)) ∧ 𝑦 ∈ ℝ) ∧ ∀𝑛 ∈ 𝑍 ((𝐹‘𝑛)‘𝑥) ≤ 𝑦) ∧ 𝑛 ∈ 𝑍) → 𝑦 ∈ ℝ) |
47 | 46 | rexrd 11163 |
. . . . . . . . . . . . 13
⊢
(((((𝜑 ∧ 𝑥 ∈ ∩ 𝑛 ∈ 𝑍 dom (𝐹‘𝑛)) ∧ 𝑦 ∈ ℝ) ∧ ∀𝑛 ∈ 𝑍 ((𝐹‘𝑛)‘𝑥) ≤ 𝑦) ∧ 𝑛 ∈ 𝑍) → 𝑦 ∈ ℝ*) |
48 | 47 | 3ad2antl1 1185 |
. . . . . . . . . . . 12
⊢
((((((𝜑 ∧ 𝑥 ∈ ∩ 𝑛 ∈ 𝑍 dom (𝐹‘𝑛)) ∧ 𝑦 ∈ ℝ) ∧ ∀𝑛 ∈ 𝑍 ((𝐹‘𝑛)‘𝑥) ≤ 𝑦) ∧ 𝑚 ∈ ℕ ∧ 𝑦 < 𝑚) ∧ 𝑛 ∈ 𝑍) → 𝑦 ∈ ℝ*) |
49 | | simpl2 1192 |
. . . . . . . . . . . . 13
⊢
((((((𝜑 ∧ 𝑥 ∈ ∩ 𝑛 ∈ 𝑍 dom (𝐹‘𝑛)) ∧ 𝑦 ∈ ℝ) ∧ ∀𝑛 ∈ 𝑍 ((𝐹‘𝑛)‘𝑥) ≤ 𝑦) ∧ 𝑚 ∈ ℕ ∧ 𝑦 < 𝑚) ∧ 𝑛 ∈ 𝑍) → 𝑚 ∈ ℕ) |
50 | 49 | nnxrd 43405 |
. . . . . . . . . . . 12
⊢
((((((𝜑 ∧ 𝑥 ∈ ∩ 𝑛 ∈ 𝑍 dom (𝐹‘𝑛)) ∧ 𝑦 ∈ ℝ) ∧ ∀𝑛 ∈ 𝑍 ((𝐹‘𝑛)‘𝑥) ≤ 𝑦) ∧ 𝑚 ∈ ℕ ∧ 𝑦 < 𝑚) ∧ 𝑛 ∈ 𝑍) → 𝑚 ∈ ℝ*) |
51 | | simpl1r 1225 |
. . . . . . . . . . . . 13
⊢
((((((𝜑 ∧ 𝑥 ∈ ∩ 𝑛 ∈ 𝑍 dom (𝐹‘𝑛)) ∧ 𝑦 ∈ ℝ) ∧ ∀𝑛 ∈ 𝑍 ((𝐹‘𝑛)‘𝑥) ≤ 𝑦) ∧ 𝑚 ∈ ℕ ∧ 𝑦 < 𝑚) ∧ 𝑛 ∈ 𝑍) → ∀𝑛 ∈ 𝑍 ((𝐹‘𝑛)‘𝑥) ≤ 𝑦) |
52 | | rspa 3229 |
. . . . . . . . . . . . 13
⊢
((∀𝑛 ∈
𝑍 ((𝐹‘𝑛)‘𝑥) ≤ 𝑦 ∧ 𝑛 ∈ 𝑍) → ((𝐹‘𝑛)‘𝑥) ≤ 𝑦) |
53 | 51, 38, 52 | syl2anc 584 |
. . . . . . . . . . . 12
⊢
((((((𝜑 ∧ 𝑥 ∈ ∩ 𝑛 ∈ 𝑍 dom (𝐹‘𝑛)) ∧ 𝑦 ∈ ℝ) ∧ ∀𝑛 ∈ 𝑍 ((𝐹‘𝑛)‘𝑥) ≤ 𝑦) ∧ 𝑚 ∈ ℕ ∧ 𝑦 < 𝑚) ∧ 𝑛 ∈ 𝑍) → ((𝐹‘𝑛)‘𝑥) ≤ 𝑦) |
54 | | simpl3 1193 |
. . . . . . . . . . . 12
⊢
((((((𝜑 ∧ 𝑥 ∈ ∩ 𝑛 ∈ 𝑍 dom (𝐹‘𝑛)) ∧ 𝑦 ∈ ℝ) ∧ ∀𝑛 ∈ 𝑍 ((𝐹‘𝑛)‘𝑥) ≤ 𝑦) ∧ 𝑚 ∈ ℕ ∧ 𝑦 < 𝑚) ∧ 𝑛 ∈ 𝑍) → 𝑦 < 𝑚) |
55 | 45, 48, 50, 53, 54 | xrlelttrd 13033 |
. . . . . . . . . . 11
⊢
((((((𝜑 ∧ 𝑥 ∈ ∩ 𝑛 ∈ 𝑍 dom (𝐹‘𝑛)) ∧ 𝑦 ∈ ℝ) ∧ ∀𝑛 ∈ 𝑍 ((𝐹‘𝑛)‘𝑥) ≤ 𝑦) ∧ 𝑚 ∈ ℕ ∧ 𝑦 < 𝑚) ∧ 𝑛 ∈ 𝑍) → ((𝐹‘𝑛)‘𝑥) < 𝑚) |
56 | 40, 55 | rabidd 43274 |
. . . . . . . . . 10
⊢
((((((𝜑 ∧ 𝑥 ∈ ∩ 𝑛 ∈ 𝑍 dom (𝐹‘𝑛)) ∧ 𝑦 ∈ ℝ) ∧ ∀𝑛 ∈ 𝑍 ((𝐹‘𝑛)‘𝑥) ≤ 𝑦) ∧ 𝑚 ∈ ℕ ∧ 𝑦 < 𝑚) ∧ 𝑛 ∈ 𝑍) → 𝑥 ∈ {𝑥 ∈ dom (𝐹‘𝑛) ∣ ((𝐹‘𝑛)‘𝑥) < 𝑚}) |
57 | | trud 1551 |
. . . . . . . . . . . . . 14
⊢ (𝑛 ∈ 𝑍 → ⊤) |
58 | | id 22 |
. . . . . . . . . . . . . 14
⊢ (𝑛 ∈ 𝑍 → 𝑛 ∈ 𝑍) |
59 | | nfcv 2905 |
. . . . . . . . . . . . . . 15
⊢
Ⅎ𝑛𝑍 |
60 | | nnex 12117 |
. . . . . . . . . . . . . . . . 17
⊢ ℕ
∈ V |
61 | 60 | mptex 7169 |
. . . . . . . . . . . . . . . 16
⊢ (𝑚 ∈ ℕ ↦ {𝑥 ∈ dom (𝐹‘𝑛) ∣ ((𝐹‘𝑛)‘𝑥) < 𝑚}) ∈ V |
62 | 61 | a1i 11 |
. . . . . . . . . . . . . . 15
⊢
((⊤ ∧ 𝑛
∈ 𝑍) → (𝑚 ∈ ℕ ↦ {𝑥 ∈ dom (𝐹‘𝑛) ∣ ((𝐹‘𝑛)‘𝑥) < 𝑚}) ∈ V) |
63 | 59, 5, 62 | fvmpt2df 43400 |
. . . . . . . . . . . . . 14
⊢
((⊤ ∧ 𝑛
∈ 𝑍) → (𝐻‘𝑛) = (𝑚 ∈ ℕ ↦ {𝑥 ∈ dom (𝐹‘𝑛) ∣ ((𝐹‘𝑛)‘𝑥) < 𝑚})) |
64 | 57, 58, 63 | syl2anc 584 |
. . . . . . . . . . . . 13
⊢ (𝑛 ∈ 𝑍 → (𝐻‘𝑛) = (𝑚 ∈ ℕ ↦ {𝑥 ∈ dom (𝐹‘𝑛) ∣ ((𝐹‘𝑛)‘𝑥) < 𝑚})) |
65 | | fsupdm.4 |
. . . . . . . . . . . . . . . . 17
⊢
Ⅎ𝑥𝐹 |
66 | 65, 10 | nffv 6849 |
. . . . . . . . . . . . . . . 16
⊢
Ⅎ𝑥(𝐹‘𝑛) |
67 | 66 | nfdm 5904 |
. . . . . . . . . . . . . . 15
⊢
Ⅎ𝑥dom
(𝐹‘𝑛) |
68 | | fvex 6852 |
. . . . . . . . . . . . . . . 16
⊢ (𝐹‘𝑛) ∈ V |
69 | 68 | dmex 7840 |
. . . . . . . . . . . . . . 15
⊢ dom
(𝐹‘𝑛) ∈ V |
70 | 67, 69 | rabexf 43248 |
. . . . . . . . . . . . . 14
⊢ {𝑥 ∈ dom (𝐹‘𝑛) ∣ ((𝐹‘𝑛)‘𝑥) < 𝑚} ∈ V |
71 | 70 | a1i 11 |
. . . . . . . . . . . . 13
⊢ ((𝑛 ∈ 𝑍 ∧ 𝑚 ∈ ℕ) → {𝑥 ∈ dom (𝐹‘𝑛) ∣ ((𝐹‘𝑛)‘𝑥) < 𝑚} ∈ V) |
72 | 64, 71 | fvmpt2d 6958 |
. . . . . . . . . . . 12
⊢ ((𝑛 ∈ 𝑍 ∧ 𝑚 ∈ ℕ) → ((𝐻‘𝑛)‘𝑚) = {𝑥 ∈ dom (𝐹‘𝑛) ∣ ((𝐹‘𝑛)‘𝑥) < 𝑚}) |
73 | 72 | eqcomd 2743 |
. . . . . . . . . . 11
⊢ ((𝑛 ∈ 𝑍 ∧ 𝑚 ∈ ℕ) → {𝑥 ∈ dom (𝐹‘𝑛) ∣ ((𝐹‘𝑛)‘𝑥) < 𝑚} = ((𝐻‘𝑛)‘𝑚)) |
74 | 38, 49, 73 | syl2anc 584 |
. . . . . . . . . 10
⊢
((((((𝜑 ∧ 𝑥 ∈ ∩ 𝑛 ∈ 𝑍 dom (𝐹‘𝑛)) ∧ 𝑦 ∈ ℝ) ∧ ∀𝑛 ∈ 𝑍 ((𝐹‘𝑛)‘𝑥) ≤ 𝑦) ∧ 𝑚 ∈ ℕ ∧ 𝑦 < 𝑚) ∧ 𝑛 ∈ 𝑍) → {𝑥 ∈ dom (𝐹‘𝑛) ∣ ((𝐹‘𝑛)‘𝑥) < 𝑚} = ((𝐻‘𝑛)‘𝑚)) |
75 | 56, 74 | eleqtrd 2840 |
. . . . . . . . 9
⊢
((((((𝜑 ∧ 𝑥 ∈ ∩ 𝑛 ∈ 𝑍 dom (𝐹‘𝑛)) ∧ 𝑦 ∈ ℝ) ∧ ∀𝑛 ∈ 𝑍 ((𝐹‘𝑛)‘𝑥) ≤ 𝑦) ∧ 𝑚 ∈ ℕ ∧ 𝑦 < 𝑚) ∧ 𝑛 ∈ 𝑍) → 𝑥 ∈ ((𝐻‘𝑛)‘𝑚)) |
76 | 33, 35, 75 | eliind2 43244 |
. . . . . . . 8
⊢
(((((𝜑 ∧ 𝑥 ∈ ∩ 𝑛 ∈ 𝑍 dom (𝐹‘𝑛)) ∧ 𝑦 ∈ ℝ) ∧ ∀𝑛 ∈ 𝑍 ((𝐹‘𝑛)‘𝑥) ≤ 𝑦) ∧ 𝑚 ∈ ℕ ∧ 𝑦 < 𝑚) → 𝑥 ∈ ∩
𝑛 ∈ 𝑍 ((𝐻‘𝑛)‘𝑚)) |
77 | | arch 12368 |
. . . . . . . . 9
⊢ (𝑦 ∈ ℝ →
∃𝑚 ∈ ℕ
𝑦 < 𝑚) |
78 | 77 | ad2antlr 725 |
. . . . . . . 8
⊢ ((((𝜑 ∧ 𝑥 ∈ ∩
𝑛 ∈ 𝑍 dom (𝐹‘𝑛)) ∧ 𝑦 ∈ ℝ) ∧ ∀𝑛 ∈ 𝑍 ((𝐹‘𝑛)‘𝑥) ≤ 𝑦) → ∃𝑚 ∈ ℕ 𝑦 < 𝑚) |
79 | 22, 76, 78 | reximdd 43266 |
. . . . . . 7
⊢ ((((𝜑 ∧ 𝑥 ∈ ∩
𝑛 ∈ 𝑍 dom (𝐹‘𝑛)) ∧ 𝑦 ∈ ℝ) ∧ ∀𝑛 ∈ 𝑍 ((𝐹‘𝑛)‘𝑥) ≤ 𝑦) → ∃𝑚 ∈ ℕ 𝑥 ∈ ∩
𝑛 ∈ 𝑍 ((𝐻‘𝑛)‘𝑚)) |
80 | 79 | rexlimdva2 3152 |
. . . . . 6
⊢ ((𝜑 ∧ 𝑥 ∈ ∩
𝑛 ∈ 𝑍 dom (𝐹‘𝑛)) → (∃𝑦 ∈ ℝ ∀𝑛 ∈ 𝑍 ((𝐹‘𝑛)‘𝑥) ≤ 𝑦 → ∃𝑚 ∈ ℕ 𝑥 ∈ ∩
𝑛 ∈ 𝑍 ((𝐻‘𝑛)‘𝑚))) |
81 | 80 | 3impia 1117 |
. . . . 5
⊢ ((𝜑 ∧ 𝑥 ∈ ∩
𝑛 ∈ 𝑍 dom (𝐹‘𝑛) ∧ ∃𝑦 ∈ ℝ ∀𝑛 ∈ 𝑍 ((𝐹‘𝑛)‘𝑥) ≤ 𝑦) → ∃𝑚 ∈ ℕ 𝑥 ∈ ∩
𝑛 ∈ 𝑍 ((𝐻‘𝑛)‘𝑚)) |
82 | | eliun 4956 |
. . . . 5
⊢ (𝑥 ∈ ∪ 𝑚 ∈ ℕ ∩ 𝑛 ∈ 𝑍 ((𝐻‘𝑛)‘𝑚) ↔ ∃𝑚 ∈ ℕ 𝑥 ∈ ∩
𝑛 ∈ 𝑍 ((𝐻‘𝑛)‘𝑚)) |
83 | 81, 82 | sylibr 233 |
. . . 4
⊢ ((𝜑 ∧ 𝑥 ∈ ∩
𝑛 ∈ 𝑍 dom (𝐹‘𝑛) ∧ ∃𝑦 ∈ ℝ ∀𝑛 ∈ 𝑍 ((𝐹‘𝑛)‘𝑥) ≤ 𝑦) → 𝑥 ∈ ∪
𝑚 ∈ ℕ ∩ 𝑛 ∈ 𝑍 ((𝐻‘𝑛)‘𝑚)) |
84 | 2, 15, 83 | rabssd 43256 |
. . 3
⊢ (𝜑 → {𝑥 ∈ ∩
𝑛 ∈ 𝑍 dom (𝐹‘𝑛) ∣ ∃𝑦 ∈ ℝ ∀𝑛 ∈ 𝑍 ((𝐹‘𝑛)‘𝑥) ≤ 𝑦} ⊆ ∪
𝑚 ∈ ℕ ∩ 𝑛 ∈ 𝑍 ((𝐻‘𝑛)‘𝑚)) |
85 | 1, 84 | eqsstrid 3990 |
. 2
⊢ (𝜑 → 𝐷 ⊆ ∪
𝑚 ∈ ℕ ∩ 𝑛 ∈ 𝑍 ((𝐻‘𝑛)‘𝑚)) |
86 | | nfcv 2905 |
. . 3
⊢
Ⅎ𝑚𝐷 |
87 | | nfv 1917 |
. . . . 5
⊢
Ⅎ𝑥 𝑚 ∈ ℕ |
88 | 2, 87 | nfan 1902 |
. . . 4
⊢
Ⅎ𝑥(𝜑 ∧ 𝑚 ∈ ℕ) |
89 | | nfrab1 3424 |
. . . . 5
⊢
Ⅎ𝑥{𝑥 ∈ ∩
𝑛 ∈ 𝑍 dom (𝐹‘𝑛) ∣ ∃𝑦 ∈ ℝ ∀𝑛 ∈ 𝑍 ((𝐹‘𝑛)‘𝑥) ≤ 𝑦} |
90 | 1, 89 | nfcxfr 2903 |
. . . 4
⊢
Ⅎ𝑥𝐷 |
91 | 23, 31 | nfan 1902 |
. . . . . . . 8
⊢
Ⅎ𝑛(𝜑 ∧ 𝑚 ∈ ℕ) |
92 | | nfii1 4987 |
. . . . . . . . 9
⊢
Ⅎ𝑛∩ 𝑛 ∈ 𝑍 ((𝐻‘𝑛)‘𝑚) |
93 | 92 | nfcri 2892 |
. . . . . . . 8
⊢
Ⅎ𝑛 𝑥 ∈ ∩ 𝑛 ∈ 𝑍 ((𝐻‘𝑛)‘𝑚) |
94 | 91, 93 | nfan 1902 |
. . . . . . 7
⊢
Ⅎ𝑛((𝜑 ∧ 𝑚 ∈ ℕ) ∧ 𝑥 ∈ ∩
𝑛 ∈ 𝑍 ((𝐻‘𝑛)‘𝑚)) |
95 | 34 | a1i 11 |
. . . . . . 7
⊢ (((𝜑 ∧ 𝑚 ∈ ℕ) ∧ 𝑥 ∈ ∩
𝑛 ∈ 𝑍 ((𝐻‘𝑛)‘𝑚)) → 𝑥 ∈ V) |
96 | | eliinid 43225 |
. . . . . . . . . 10
⊢ ((𝑥 ∈ ∩ 𝑛 ∈ 𝑍 ((𝐻‘𝑛)‘𝑚) ∧ 𝑛 ∈ 𝑍) → 𝑥 ∈ ((𝐻‘𝑛)‘𝑚)) |
97 | 96 | adantll 712 |
. . . . . . . . 9
⊢ ((((𝜑 ∧ 𝑚 ∈ ℕ) ∧ 𝑥 ∈ ∩
𝑛 ∈ 𝑍 ((𝐻‘𝑛)‘𝑚)) ∧ 𝑛 ∈ 𝑍) → 𝑥 ∈ ((𝐻‘𝑛)‘𝑚)) |
98 | | simpr 485 |
. . . . . . . . . 10
⊢ ((((𝜑 ∧ 𝑚 ∈ ℕ) ∧ 𝑥 ∈ ∩
𝑛 ∈ 𝑍 ((𝐻‘𝑛)‘𝑚)) ∧ 𝑛 ∈ 𝑍) → 𝑛 ∈ 𝑍) |
99 | | simpllr 774 |
. . . . . . . . . 10
⊢ ((((𝜑 ∧ 𝑚 ∈ ℕ) ∧ 𝑥 ∈ ∩
𝑛 ∈ 𝑍 ((𝐻‘𝑛)‘𝑚)) ∧ 𝑛 ∈ 𝑍) → 𝑚 ∈ ℕ) |
100 | 98, 99, 72 | syl2anc 584 |
. . . . . . . . 9
⊢ ((((𝜑 ∧ 𝑚 ∈ ℕ) ∧ 𝑥 ∈ ∩
𝑛 ∈ 𝑍 ((𝐻‘𝑛)‘𝑚)) ∧ 𝑛 ∈ 𝑍) → ((𝐻‘𝑛)‘𝑚) = {𝑥 ∈ dom (𝐹‘𝑛) ∣ ((𝐹‘𝑛)‘𝑥) < 𝑚}) |
101 | 97, 100 | eleqtrd 2840 |
. . . . . . . 8
⊢ ((((𝜑 ∧ 𝑚 ∈ ℕ) ∧ 𝑥 ∈ ∩
𝑛 ∈ 𝑍 ((𝐻‘𝑛)‘𝑚)) ∧ 𝑛 ∈ 𝑍) → 𝑥 ∈ {𝑥 ∈ dom (𝐹‘𝑛) ∣ ((𝐹‘𝑛)‘𝑥) < 𝑚}) |
102 | | rabidim1 3426 |
. . . . . . . 8
⊢ (𝑥 ∈ {𝑥 ∈ dom (𝐹‘𝑛) ∣ ((𝐹‘𝑛)‘𝑥) < 𝑚} → 𝑥 ∈ dom (𝐹‘𝑛)) |
103 | 101, 102 | syl 17 |
. . . . . . 7
⊢ ((((𝜑 ∧ 𝑚 ∈ ℕ) ∧ 𝑥 ∈ ∩
𝑛 ∈ 𝑍 ((𝐻‘𝑛)‘𝑚)) ∧ 𝑛 ∈ 𝑍) → 𝑥 ∈ dom (𝐹‘𝑛)) |
104 | 94, 95, 103 | eliind2 43244 |
. . . . . 6
⊢ (((𝜑 ∧ 𝑚 ∈ ℕ) ∧ 𝑥 ∈ ∩
𝑛 ∈ 𝑍 ((𝐻‘𝑛)‘𝑚)) → 𝑥 ∈ ∩
𝑛 ∈ 𝑍 dom (𝐹‘𝑛)) |
105 | | nnre 12118 |
. . . . . . . 8
⊢ (𝑚 ∈ ℕ → 𝑚 ∈
ℝ) |
106 | 105 | ad2antlr 725 |
. . . . . . 7
⊢ (((𝜑 ∧ 𝑚 ∈ ℕ) ∧ 𝑥 ∈ ∩
𝑛 ∈ 𝑍 ((𝐻‘𝑛)‘𝑚)) → 𝑚 ∈ ℝ) |
107 | | breq2 5107 |
. . . . . . . . 9
⊢ (𝑦 = 𝑚 → (((𝐹‘𝑛)‘𝑥) ≤ 𝑦 ↔ ((𝐹‘𝑛)‘𝑥) ≤ 𝑚)) |
108 | 107 | ralbidv 3172 |
. . . . . . . 8
⊢ (𝑦 = 𝑚 → (∀𝑛 ∈ 𝑍 ((𝐹‘𝑛)‘𝑥) ≤ 𝑦 ↔ ∀𝑛 ∈ 𝑍 ((𝐹‘𝑛)‘𝑥) ≤ 𝑚)) |
109 | 108 | adantl 482 |
. . . . . . 7
⊢ ((((𝜑 ∧ 𝑚 ∈ ℕ) ∧ 𝑥 ∈ ∩
𝑛 ∈ 𝑍 ((𝐻‘𝑛)‘𝑚)) ∧ 𝑦 = 𝑚) → (∀𝑛 ∈ 𝑍 ((𝐹‘𝑛)‘𝑥) ≤ 𝑦 ↔ ∀𝑛 ∈ 𝑍 ((𝐹‘𝑛)‘𝑥) ≤ 𝑚)) |
110 | | simplll 773 |
. . . . . . . . . 10
⊢ ((((𝜑 ∧ 𝑚 ∈ ℕ) ∧ 𝑥 ∈ ∩
𝑛 ∈ 𝑍 ((𝐻‘𝑛)‘𝑚)) ∧ 𝑛 ∈ 𝑍) → 𝜑) |
111 | 43 | 3adant3 1132 |
. . . . . . . . . . 11
⊢ ((𝜑 ∧ 𝑛 ∈ 𝑍 ∧ 𝑥 ∈ dom (𝐹‘𝑛)) → (𝐹‘𝑛):dom (𝐹‘𝑛)⟶ℝ*) |
112 | | simp3 1138 |
. . . . . . . . . . 11
⊢ ((𝜑 ∧ 𝑛 ∈ 𝑍 ∧ 𝑥 ∈ dom (𝐹‘𝑛)) → 𝑥 ∈ dom (𝐹‘𝑛)) |
113 | 111, 112 | ffvelcdmd 7032 |
. . . . . . . . . 10
⊢ ((𝜑 ∧ 𝑛 ∈ 𝑍 ∧ 𝑥 ∈ dom (𝐹‘𝑛)) → ((𝐹‘𝑛)‘𝑥) ∈
ℝ*) |
114 | 110, 98, 103, 113 | syl3anc 1371 |
. . . . . . . . 9
⊢ ((((𝜑 ∧ 𝑚 ∈ ℕ) ∧ 𝑥 ∈ ∩
𝑛 ∈ 𝑍 ((𝐻‘𝑛)‘𝑚)) ∧ 𝑛 ∈ 𝑍) → ((𝐹‘𝑛)‘𝑥) ∈
ℝ*) |
115 | 99 | nnxrd 43405 |
. . . . . . . . 9
⊢ ((((𝜑 ∧ 𝑚 ∈ ℕ) ∧ 𝑥 ∈ ∩
𝑛 ∈ 𝑍 ((𝐻‘𝑛)‘𝑚)) ∧ 𝑛 ∈ 𝑍) → 𝑚 ∈ ℝ*) |
116 | | rabidim2 43216 |
. . . . . . . . . 10
⊢ (𝑥 ∈ {𝑥 ∈ dom (𝐹‘𝑛) ∣ ((𝐹‘𝑛)‘𝑥) < 𝑚} → ((𝐹‘𝑛)‘𝑥) < 𝑚) |
117 | 101, 116 | syl 17 |
. . . . . . . . 9
⊢ ((((𝜑 ∧ 𝑚 ∈ ℕ) ∧ 𝑥 ∈ ∩
𝑛 ∈ 𝑍 ((𝐻‘𝑛)‘𝑚)) ∧ 𝑛 ∈ 𝑍) → ((𝐹‘𝑛)‘𝑥) < 𝑚) |
118 | 114, 115,
117 | xrltled 13023 |
. . . . . . . 8
⊢ ((((𝜑 ∧ 𝑚 ∈ ℕ) ∧ 𝑥 ∈ ∩
𝑛 ∈ 𝑍 ((𝐻‘𝑛)‘𝑚)) ∧ 𝑛 ∈ 𝑍) → ((𝐹‘𝑛)‘𝑥) ≤ 𝑚) |
119 | 94, 118 | ralrimia 3239 |
. . . . . . 7
⊢ (((𝜑 ∧ 𝑚 ∈ ℕ) ∧ 𝑥 ∈ ∩
𝑛 ∈ 𝑍 ((𝐻‘𝑛)‘𝑚)) → ∀𝑛 ∈ 𝑍 ((𝐹‘𝑛)‘𝑥) ≤ 𝑚) |
120 | 106, 109,
119 | rspcedvd 3581 |
. . . . . 6
⊢ (((𝜑 ∧ 𝑚 ∈ ℕ) ∧ 𝑥 ∈ ∩
𝑛 ∈ 𝑍 ((𝐻‘𝑛)‘𝑚)) → ∃𝑦 ∈ ℝ ∀𝑛 ∈ 𝑍 ((𝐹‘𝑛)‘𝑥) ≤ 𝑦) |
121 | 104, 120 | rabidd 43274 |
. . . . 5
⊢ (((𝜑 ∧ 𝑚 ∈ ℕ) ∧ 𝑥 ∈ ∩
𝑛 ∈ 𝑍 ((𝐻‘𝑛)‘𝑚)) → 𝑥 ∈ {𝑥 ∈ ∩
𝑛 ∈ 𝑍 dom (𝐹‘𝑛) ∣ ∃𝑦 ∈ ℝ ∀𝑛 ∈ 𝑍 ((𝐹‘𝑛)‘𝑥) ≤ 𝑦}) |
122 | 121, 1 | eleqtrrdi 2849 |
. . . 4
⊢ (((𝜑 ∧ 𝑚 ∈ ℕ) ∧ 𝑥 ∈ ∩
𝑛 ∈ 𝑍 ((𝐻‘𝑛)‘𝑚)) → 𝑥 ∈ 𝐷) |
123 | 88, 14, 90, 122 | ssdf2 43255 |
. . 3
⊢ ((𝜑 ∧ 𝑚 ∈ ℕ) → ∩ 𝑛 ∈ 𝑍 ((𝐻‘𝑛)‘𝑚) ⊆ 𝐷) |
124 | 16, 86, 123 | iunssdf 43275 |
. 2
⊢ (𝜑 → ∪ 𝑚 ∈ ℕ ∩ 𝑛 ∈ 𝑍 ((𝐻‘𝑛)‘𝑚) ⊆ 𝐷) |
125 | 85, 124 | eqssd 3959 |
1
⊢ (𝜑 → 𝐷 = ∪ 𝑚 ∈ ℕ ∩ 𝑛 ∈ 𝑍 ((𝐻‘𝑛)‘𝑚)) |