Step | Hyp | Ref
| Expression |
1 | | smflimlem6.2 |
. . . . . . . 8
⊢ 𝑍 =
(ℤ≥‘𝑀) |
2 | | fvex 6201 |
. . . . . . . 8
⊢
(ℤ≥‘𝑀) ∈ V |
3 | 1, 2 | eqeltri 2697 |
. . . . . . 7
⊢ 𝑍 ∈ V |
4 | | nnex 11026 |
. . . . . . 7
⊢ ℕ
∈ V |
5 | 3, 4 | xpex 6962 |
. . . . . 6
⊢ (𝑍 × ℕ) ∈
V |
6 | 5 | a1i 11 |
. . . . 5
⊢ (𝜑 → (𝑍 × ℕ) ∈ V) |
7 | | eqid 2622 |
. . . . . . . . 9
⊢ {𝑠 ∈ 𝑆 ∣ {𝑥 ∈ dom (𝐹‘𝑚) ∣ ((𝐹‘𝑚)‘𝑥) < (𝐴 + (1 / 𝑘))} = (𝑠 ∩ dom (𝐹‘𝑚))} = {𝑠 ∈ 𝑆 ∣ {𝑥 ∈ dom (𝐹‘𝑚) ∣ ((𝐹‘𝑚)‘𝑥) < (𝐴 + (1 / 𝑘))} = (𝑠 ∩ dom (𝐹‘𝑚))} |
8 | | smflimlem6.3 |
. . . . . . . . 9
⊢ (𝜑 → 𝑆 ∈ SAlg) |
9 | 7, 8 | rabexd 4814 |
. . . . . . . 8
⊢ (𝜑 → {𝑠 ∈ 𝑆 ∣ {𝑥 ∈ dom (𝐹‘𝑚) ∣ ((𝐹‘𝑚)‘𝑥) < (𝐴 + (1 / 𝑘))} = (𝑠 ∩ dom (𝐹‘𝑚))} ∈ V) |
10 | 9 | adantr 481 |
. . . . . . 7
⊢ ((𝜑 ∧ (𝑚 ∈ 𝑍 ∧ 𝑘 ∈ ℕ)) → {𝑠 ∈ 𝑆 ∣ {𝑥 ∈ dom (𝐹‘𝑚) ∣ ((𝐹‘𝑚)‘𝑥) < (𝐴 + (1 / 𝑘))} = (𝑠 ∩ dom (𝐹‘𝑚))} ∈ V) |
11 | 10 | ralrimivva 2971 |
. . . . . 6
⊢ (𝜑 → ∀𝑚 ∈ 𝑍 ∀𝑘 ∈ ℕ {𝑠 ∈ 𝑆 ∣ {𝑥 ∈ dom (𝐹‘𝑚) ∣ ((𝐹‘𝑚)‘𝑥) < (𝐴 + (1 / 𝑘))} = (𝑠 ∩ dom (𝐹‘𝑚))} ∈ V) |
12 | | smflimlem6.8 |
. . . . . . 7
⊢ 𝑃 = (𝑚 ∈ 𝑍, 𝑘 ∈ ℕ ↦ {𝑠 ∈ 𝑆 ∣ {𝑥 ∈ dom (𝐹‘𝑚) ∣ ((𝐹‘𝑚)‘𝑥) < (𝐴 + (1 / 𝑘))} = (𝑠 ∩ dom (𝐹‘𝑚))}) |
13 | 12 | fnmpt2 7238 |
. . . . . 6
⊢
(∀𝑚 ∈
𝑍 ∀𝑘 ∈ ℕ {𝑠 ∈ 𝑆 ∣ {𝑥 ∈ dom (𝐹‘𝑚) ∣ ((𝐹‘𝑚)‘𝑥) < (𝐴 + (1 / 𝑘))} = (𝑠 ∩ dom (𝐹‘𝑚))} ∈ V → 𝑃 Fn (𝑍 × ℕ)) |
14 | 11, 13 | syl 17 |
. . . . 5
⊢ (𝜑 → 𝑃 Fn (𝑍 × ℕ)) |
15 | | fnrndomg 9358 |
. . . . 5
⊢ ((𝑍 × ℕ) ∈ V
→ (𝑃 Fn (𝑍 × ℕ) → ran
𝑃 ≼ (𝑍 ×
ℕ))) |
16 | 6, 14, 15 | sylc 65 |
. . . 4
⊢ (𝜑 → ran 𝑃 ≼ (𝑍 × ℕ)) |
17 | 1 | uzct 39232 |
. . . . . . 7
⊢ 𝑍 ≼
ω |
18 | | nnct 12780 |
. . . . . . 7
⊢ ℕ
≼ ω |
19 | 17, 18 | pm3.2i 471 |
. . . . . 6
⊢ (𝑍 ≼ ω ∧ ℕ
≼ ω) |
20 | | xpct 8839 |
. . . . . 6
⊢ ((𝑍 ≼ ω ∧ ℕ
≼ ω) → (𝑍
× ℕ) ≼ ω) |
21 | 19, 20 | ax-mp 5 |
. . . . 5
⊢ (𝑍 × ℕ) ≼
ω |
22 | 21 | a1i 11 |
. . . 4
⊢ (𝜑 → (𝑍 × ℕ) ≼
ω) |
23 | | domtr 8009 |
. . . 4
⊢ ((ran
𝑃 ≼ (𝑍 × ℕ) ∧ (𝑍 × ℕ) ≼
ω) → ran 𝑃
≼ ω) |
24 | 16, 22, 23 | syl2anc 693 |
. . 3
⊢ (𝜑 → ran 𝑃 ≼ ω) |
25 | | vex 3203 |
. . . . . . 7
⊢ 𝑦 ∈ V |
26 | 12 | elrnmpt2g 6772 |
. . . . . . 7
⊢ (𝑦 ∈ V → (𝑦 ∈ ran 𝑃 ↔ ∃𝑚 ∈ 𝑍 ∃𝑘 ∈ ℕ 𝑦 = {𝑠 ∈ 𝑆 ∣ {𝑥 ∈ dom (𝐹‘𝑚) ∣ ((𝐹‘𝑚)‘𝑥) < (𝐴 + (1 / 𝑘))} = (𝑠 ∩ dom (𝐹‘𝑚))})) |
27 | 25, 26 | ax-mp 5 |
. . . . . 6
⊢ (𝑦 ∈ ran 𝑃 ↔ ∃𝑚 ∈ 𝑍 ∃𝑘 ∈ ℕ 𝑦 = {𝑠 ∈ 𝑆 ∣ {𝑥 ∈ dom (𝐹‘𝑚) ∣ ((𝐹‘𝑚)‘𝑥) < (𝐴 + (1 / 𝑘))} = (𝑠 ∩ dom (𝐹‘𝑚))}) |
28 | 27 | biimpi 206 |
. . . . 5
⊢ (𝑦 ∈ ran 𝑃 → ∃𝑚 ∈ 𝑍 ∃𝑘 ∈ ℕ 𝑦 = {𝑠 ∈ 𝑆 ∣ {𝑥 ∈ dom (𝐹‘𝑚) ∣ ((𝐹‘𝑚)‘𝑥) < (𝐴 + (1 / 𝑘))} = (𝑠 ∩ dom (𝐹‘𝑚))}) |
29 | 28 | adantl 482 |
. . . 4
⊢ ((𝜑 ∧ 𝑦 ∈ ran 𝑃) → ∃𝑚 ∈ 𝑍 ∃𝑘 ∈ ℕ 𝑦 = {𝑠 ∈ 𝑆 ∣ {𝑥 ∈ dom (𝐹‘𝑚) ∣ ((𝐹‘𝑚)‘𝑥) < (𝐴 + (1 / 𝑘))} = (𝑠 ∩ dom (𝐹‘𝑚))}) |
30 | | simp3 1063 |
. . . . . . . 8
⊢ ((𝜑 ∧ (𝑚 ∈ 𝑍 ∧ 𝑘 ∈ ℕ) ∧ 𝑦 = {𝑠 ∈ 𝑆 ∣ {𝑥 ∈ dom (𝐹‘𝑚) ∣ ((𝐹‘𝑚)‘𝑥) < (𝐴 + (1 / 𝑘))} = (𝑠 ∩ dom (𝐹‘𝑚))}) → 𝑦 = {𝑠 ∈ 𝑆 ∣ {𝑥 ∈ dom (𝐹‘𝑚) ∣ ((𝐹‘𝑚)‘𝑥) < (𝐴 + (1 / 𝑘))} = (𝑠 ∩ dom (𝐹‘𝑚))}) |
31 | 8 | adantr 481 |
. . . . . . . . . . . 12
⊢ ((𝜑 ∧ (𝑚 ∈ 𝑍 ∧ 𝑘 ∈ ℕ)) → 𝑆 ∈ SAlg) |
32 | | smflimlem6.4 |
. . . . . . . . . . . . . 14
⊢ (𝜑 → 𝐹:𝑍⟶(SMblFn‘𝑆)) |
33 | 32 | ffvelrnda 6359 |
. . . . . . . . . . . . 13
⊢ ((𝜑 ∧ 𝑚 ∈ 𝑍) → (𝐹‘𝑚) ∈ (SMblFn‘𝑆)) |
34 | 33 | adantrr 753 |
. . . . . . . . . . . 12
⊢ ((𝜑 ∧ (𝑚 ∈ 𝑍 ∧ 𝑘 ∈ ℕ)) → (𝐹‘𝑚) ∈ (SMblFn‘𝑆)) |
35 | | eqid 2622 |
. . . . . . . . . . . 12
⊢ dom
(𝐹‘𝑚) = dom (𝐹‘𝑚) |
36 | | smflimlem6.7 |
. . . . . . . . . . . . . . 15
⊢ (𝜑 → 𝐴 ∈ ℝ) |
37 | 36 | adantr 481 |
. . . . . . . . . . . . . 14
⊢ ((𝜑 ∧ 𝑘 ∈ ℕ) → 𝐴 ∈ ℝ) |
38 | | nnrecre 11057 |
. . . . . . . . . . . . . . 15
⊢ (𝑘 ∈ ℕ → (1 /
𝑘) ∈
ℝ) |
39 | 38 | adantl 482 |
. . . . . . . . . . . . . 14
⊢ ((𝜑 ∧ 𝑘 ∈ ℕ) → (1 / 𝑘) ∈
ℝ) |
40 | 37, 39 | readdcld 10069 |
. . . . . . . . . . . . 13
⊢ ((𝜑 ∧ 𝑘 ∈ ℕ) → (𝐴 + (1 / 𝑘)) ∈ ℝ) |
41 | 40 | adantrl 752 |
. . . . . . . . . . . 12
⊢ ((𝜑 ∧ (𝑚 ∈ 𝑍 ∧ 𝑘 ∈ ℕ)) → (𝐴 + (1 / 𝑘)) ∈ ℝ) |
42 | 31, 34, 35, 41 | smfpreimalt 40940 |
. . . . . . . . . . 11
⊢ ((𝜑 ∧ (𝑚 ∈ 𝑍 ∧ 𝑘 ∈ ℕ)) → {𝑥 ∈ dom (𝐹‘𝑚) ∣ ((𝐹‘𝑚)‘𝑥) < (𝐴 + (1 / 𝑘))} ∈ (𝑆 ↾t dom (𝐹‘𝑚))) |
43 | | fvex 6201 |
. . . . . . . . . . . . . . 15
⊢ (𝐹‘𝑚) ∈ V |
44 | 43 | dmex 7099 |
. . . . . . . . . . . . . 14
⊢ dom
(𝐹‘𝑚) ∈ V |
45 | 44 | a1i 11 |
. . . . . . . . . . . . 13
⊢ (𝜑 → dom (𝐹‘𝑚) ∈ V) |
46 | | elrest 16088 |
. . . . . . . . . . . . 13
⊢ ((𝑆 ∈ SAlg ∧ dom (𝐹‘𝑚) ∈ V) → ({𝑥 ∈ dom (𝐹‘𝑚) ∣ ((𝐹‘𝑚)‘𝑥) < (𝐴 + (1 / 𝑘))} ∈ (𝑆 ↾t dom (𝐹‘𝑚)) ↔ ∃𝑠 ∈ 𝑆 {𝑥 ∈ dom (𝐹‘𝑚) ∣ ((𝐹‘𝑚)‘𝑥) < (𝐴 + (1 / 𝑘))} = (𝑠 ∩ dom (𝐹‘𝑚)))) |
47 | 8, 45, 46 | syl2anc 693 |
. . . . . . . . . . . 12
⊢ (𝜑 → ({𝑥 ∈ dom (𝐹‘𝑚) ∣ ((𝐹‘𝑚)‘𝑥) < (𝐴 + (1 / 𝑘))} ∈ (𝑆 ↾t dom (𝐹‘𝑚)) ↔ ∃𝑠 ∈ 𝑆 {𝑥 ∈ dom (𝐹‘𝑚) ∣ ((𝐹‘𝑚)‘𝑥) < (𝐴 + (1 / 𝑘))} = (𝑠 ∩ dom (𝐹‘𝑚)))) |
48 | 47 | adantr 481 |
. . . . . . . . . . 11
⊢ ((𝜑 ∧ (𝑚 ∈ 𝑍 ∧ 𝑘 ∈ ℕ)) → ({𝑥 ∈ dom (𝐹‘𝑚) ∣ ((𝐹‘𝑚)‘𝑥) < (𝐴 + (1 / 𝑘))} ∈ (𝑆 ↾t dom (𝐹‘𝑚)) ↔ ∃𝑠 ∈ 𝑆 {𝑥 ∈ dom (𝐹‘𝑚) ∣ ((𝐹‘𝑚)‘𝑥) < (𝐴 + (1 / 𝑘))} = (𝑠 ∩ dom (𝐹‘𝑚)))) |
49 | 42, 48 | mpbid 222 |
. . . . . . . . . 10
⊢ ((𝜑 ∧ (𝑚 ∈ 𝑍 ∧ 𝑘 ∈ ℕ)) → ∃𝑠 ∈ 𝑆 {𝑥 ∈ dom (𝐹‘𝑚) ∣ ((𝐹‘𝑚)‘𝑥) < (𝐴 + (1 / 𝑘))} = (𝑠 ∩ dom (𝐹‘𝑚))) |
50 | | rabn0 3958 |
. . . . . . . . . 10
⊢ ({𝑠 ∈ 𝑆 ∣ {𝑥 ∈ dom (𝐹‘𝑚) ∣ ((𝐹‘𝑚)‘𝑥) < (𝐴 + (1 / 𝑘))} = (𝑠 ∩ dom (𝐹‘𝑚))} ≠ ∅ ↔ ∃𝑠 ∈ 𝑆 {𝑥 ∈ dom (𝐹‘𝑚) ∣ ((𝐹‘𝑚)‘𝑥) < (𝐴 + (1 / 𝑘))} = (𝑠 ∩ dom (𝐹‘𝑚))) |
51 | 49, 50 | sylibr 224 |
. . . . . . . . 9
⊢ ((𝜑 ∧ (𝑚 ∈ 𝑍 ∧ 𝑘 ∈ ℕ)) → {𝑠 ∈ 𝑆 ∣ {𝑥 ∈ dom (𝐹‘𝑚) ∣ ((𝐹‘𝑚)‘𝑥) < (𝐴 + (1 / 𝑘))} = (𝑠 ∩ dom (𝐹‘𝑚))} ≠ ∅) |
52 | 51 | 3adant3 1081 |
. . . . . . . 8
⊢ ((𝜑 ∧ (𝑚 ∈ 𝑍 ∧ 𝑘 ∈ ℕ) ∧ 𝑦 = {𝑠 ∈ 𝑆 ∣ {𝑥 ∈ dom (𝐹‘𝑚) ∣ ((𝐹‘𝑚)‘𝑥) < (𝐴 + (1 / 𝑘))} = (𝑠 ∩ dom (𝐹‘𝑚))}) → {𝑠 ∈ 𝑆 ∣ {𝑥 ∈ dom (𝐹‘𝑚) ∣ ((𝐹‘𝑚)‘𝑥) < (𝐴 + (1 / 𝑘))} = (𝑠 ∩ dom (𝐹‘𝑚))} ≠ ∅) |
53 | 30, 52 | eqnetrd 2861 |
. . . . . . 7
⊢ ((𝜑 ∧ (𝑚 ∈ 𝑍 ∧ 𝑘 ∈ ℕ) ∧ 𝑦 = {𝑠 ∈ 𝑆 ∣ {𝑥 ∈ dom (𝐹‘𝑚) ∣ ((𝐹‘𝑚)‘𝑥) < (𝐴 + (1 / 𝑘))} = (𝑠 ∩ dom (𝐹‘𝑚))}) → 𝑦 ≠ ∅) |
54 | 53 | 3exp 1264 |
. . . . . 6
⊢ (𝜑 → ((𝑚 ∈ 𝑍 ∧ 𝑘 ∈ ℕ) → (𝑦 = {𝑠 ∈ 𝑆 ∣ {𝑥 ∈ dom (𝐹‘𝑚) ∣ ((𝐹‘𝑚)‘𝑥) < (𝐴 + (1 / 𝑘))} = (𝑠 ∩ dom (𝐹‘𝑚))} → 𝑦 ≠ ∅))) |
55 | 54 | rexlimdvv 3037 |
. . . . 5
⊢ (𝜑 → (∃𝑚 ∈ 𝑍 ∃𝑘 ∈ ℕ 𝑦 = {𝑠 ∈ 𝑆 ∣ {𝑥 ∈ dom (𝐹‘𝑚) ∣ ((𝐹‘𝑚)‘𝑥) < (𝐴 + (1 / 𝑘))} = (𝑠 ∩ dom (𝐹‘𝑚))} → 𝑦 ≠ ∅)) |
56 | 55 | adantr 481 |
. . . 4
⊢ ((𝜑 ∧ 𝑦 ∈ ran 𝑃) → (∃𝑚 ∈ 𝑍 ∃𝑘 ∈ ℕ 𝑦 = {𝑠 ∈ 𝑆 ∣ {𝑥 ∈ dom (𝐹‘𝑚) ∣ ((𝐹‘𝑚)‘𝑥) < (𝐴 + (1 / 𝑘))} = (𝑠 ∩ dom (𝐹‘𝑚))} → 𝑦 ≠ ∅)) |
57 | 29, 56 | mpd 15 |
. . 3
⊢ ((𝜑 ∧ 𝑦 ∈ ran 𝑃) → 𝑦 ≠ ∅) |
58 | 24, 57 | axccd2 39430 |
. 2
⊢ (𝜑 → ∃𝑐∀𝑦 ∈ ran 𝑃(𝑐‘𝑦) ∈ 𝑦) |
59 | | smflimlem6.1 |
. . . . . 6
⊢ (𝜑 → 𝑀 ∈ ℤ) |
60 | 59 | adantr 481 |
. . . . 5
⊢ ((𝜑 ∧ ∀𝑦 ∈ ran 𝑃(𝑐‘𝑦) ∈ 𝑦) → 𝑀 ∈ ℤ) |
61 | 8 | adantr 481 |
. . . . 5
⊢ ((𝜑 ∧ ∀𝑦 ∈ ran 𝑃(𝑐‘𝑦) ∈ 𝑦) → 𝑆 ∈ SAlg) |
62 | 32 | adantr 481 |
. . . . 5
⊢ ((𝜑 ∧ ∀𝑦 ∈ ran 𝑃(𝑐‘𝑦) ∈ 𝑦) → 𝐹:𝑍⟶(SMblFn‘𝑆)) |
63 | | smflimlem6.5 |
. . . . 5
⊢ 𝐷 = {𝑥 ∈ ∪
𝑛 ∈ 𝑍 ∩ 𝑚 ∈
(ℤ≥‘𝑛)dom (𝐹‘𝑚) ∣ (𝑚 ∈ 𝑍 ↦ ((𝐹‘𝑚)‘𝑥)) ∈ dom ⇝ } |
64 | | smflimlem6.6 |
. . . . 5
⊢ 𝐺 = (𝑥 ∈ 𝐷 ↦ ( ⇝ ‘(𝑚 ∈ 𝑍 ↦ ((𝐹‘𝑚)‘𝑥)))) |
65 | 36 | adantr 481 |
. . . . 5
⊢ ((𝜑 ∧ ∀𝑦 ∈ ran 𝑃(𝑐‘𝑦) ∈ 𝑦) → 𝐴 ∈ ℝ) |
66 | | oveq1 6657 |
. . . . . . 7
⊢ (𝑙 = 𝑚 → (𝑙𝑃𝑗) = (𝑚𝑃𝑗)) |
67 | 66 | fveq2d 6195 |
. . . . . 6
⊢ (𝑙 = 𝑚 → (𝑐‘(𝑙𝑃𝑗)) = (𝑐‘(𝑚𝑃𝑗))) |
68 | | oveq2 6658 |
. . . . . . 7
⊢ (𝑗 = 𝑘 → (𝑚𝑃𝑗) = (𝑚𝑃𝑘)) |
69 | 68 | fveq2d 6195 |
. . . . . 6
⊢ (𝑗 = 𝑘 → (𝑐‘(𝑚𝑃𝑗)) = (𝑐‘(𝑚𝑃𝑘))) |
70 | 67, 69 | cbvmpt2v 6735 |
. . . . 5
⊢ (𝑙 ∈ 𝑍, 𝑗 ∈ ℕ ↦ (𝑐‘(𝑙𝑃𝑗))) = (𝑚 ∈ 𝑍, 𝑘 ∈ ℕ ↦ (𝑐‘(𝑚𝑃𝑘))) |
71 | | nfcv 2764 |
. . . . . 6
⊢
Ⅎ𝑘∪ 𝑛 ∈ 𝑍 ∩ 𝑖 ∈
(ℤ≥‘𝑛)(𝑖(𝑙 ∈ 𝑍, 𝑗 ∈ ℕ ↦ (𝑐‘(𝑙𝑃𝑗)))𝑗) |
72 | | nfcv 2764 |
. . . . . . 7
⊢
Ⅎ𝑗𝑍 |
73 | | nfcv 2764 |
. . . . . . . 8
⊢
Ⅎ𝑗(ℤ≥‘𝑛) |
74 | | nfcv 2764 |
. . . . . . . . 9
⊢
Ⅎ𝑗𝑚 |
75 | | nfmpt22 6723 |
. . . . . . . . 9
⊢
Ⅎ𝑗(𝑙 ∈ 𝑍, 𝑗 ∈ ℕ ↦ (𝑐‘(𝑙𝑃𝑗))) |
76 | | nfcv 2764 |
. . . . . . . . 9
⊢
Ⅎ𝑗𝑘 |
77 | 74, 75, 76 | nfov 6676 |
. . . . . . . 8
⊢
Ⅎ𝑗(𝑚(𝑙 ∈ 𝑍, 𝑗 ∈ ℕ ↦ (𝑐‘(𝑙𝑃𝑗)))𝑘) |
78 | 73, 77 | nfiin 4549 |
. . . . . . 7
⊢
Ⅎ𝑗∩ 𝑚 ∈
(ℤ≥‘𝑛)(𝑚(𝑙 ∈ 𝑍, 𝑗 ∈ ℕ ↦ (𝑐‘(𝑙𝑃𝑗)))𝑘) |
79 | 72, 78 | nfiun 4548 |
. . . . . 6
⊢
Ⅎ𝑗∪ 𝑛 ∈ 𝑍 ∩ 𝑚 ∈
(ℤ≥‘𝑛)(𝑚(𝑙 ∈ 𝑍, 𝑗 ∈ ℕ ↦ (𝑐‘(𝑙𝑃𝑗)))𝑘) |
80 | | oveq2 6658 |
. . . . . . . . . . 11
⊢ (𝑗 = 𝑘 → (𝑖(𝑙 ∈ 𝑍, 𝑗 ∈ ℕ ↦ (𝑐‘(𝑙𝑃𝑗)))𝑗) = (𝑖(𝑙 ∈ 𝑍, 𝑗 ∈ ℕ ↦ (𝑐‘(𝑙𝑃𝑗)))𝑘)) |
81 | 80 | adantr 481 |
. . . . . . . . . 10
⊢ ((𝑗 = 𝑘 ∧ 𝑖 ∈ (ℤ≥‘𝑛)) → (𝑖(𝑙 ∈ 𝑍, 𝑗 ∈ ℕ ↦ (𝑐‘(𝑙𝑃𝑗)))𝑗) = (𝑖(𝑙 ∈ 𝑍, 𝑗 ∈ ℕ ↦ (𝑐‘(𝑙𝑃𝑗)))𝑘)) |
82 | 81 | iineq2dv 4543 |
. . . . . . . . 9
⊢ (𝑗 = 𝑘 → ∩
𝑖 ∈
(ℤ≥‘𝑛)(𝑖(𝑙 ∈ 𝑍, 𝑗 ∈ ℕ ↦ (𝑐‘(𝑙𝑃𝑗)))𝑗) = ∩ 𝑖 ∈
(ℤ≥‘𝑛)(𝑖(𝑙 ∈ 𝑍, 𝑗 ∈ ℕ ↦ (𝑐‘(𝑙𝑃𝑗)))𝑘)) |
83 | | oveq1 6657 |
. . . . . . . . . . 11
⊢ (𝑖 = 𝑚 → (𝑖(𝑙 ∈ 𝑍, 𝑗 ∈ ℕ ↦ (𝑐‘(𝑙𝑃𝑗)))𝑘) = (𝑚(𝑙 ∈ 𝑍, 𝑗 ∈ ℕ ↦ (𝑐‘(𝑙𝑃𝑗)))𝑘)) |
84 | 83 | cbviinv 4560 |
. . . . . . . . . 10
⊢ ∩ 𝑖 ∈ (ℤ≥‘𝑛)(𝑖(𝑙 ∈ 𝑍, 𝑗 ∈ ℕ ↦ (𝑐‘(𝑙𝑃𝑗)))𝑘) = ∩ 𝑚 ∈
(ℤ≥‘𝑛)(𝑚(𝑙 ∈ 𝑍, 𝑗 ∈ ℕ ↦ (𝑐‘(𝑙𝑃𝑗)))𝑘) |
85 | 84 | a1i 11 |
. . . . . . . . 9
⊢ (𝑗 = 𝑘 → ∩
𝑖 ∈
(ℤ≥‘𝑛)(𝑖(𝑙 ∈ 𝑍, 𝑗 ∈ ℕ ↦ (𝑐‘(𝑙𝑃𝑗)))𝑘) = ∩ 𝑚 ∈
(ℤ≥‘𝑛)(𝑚(𝑙 ∈ 𝑍, 𝑗 ∈ ℕ ↦ (𝑐‘(𝑙𝑃𝑗)))𝑘)) |
86 | 82, 85 | eqtrd 2656 |
. . . . . . . 8
⊢ (𝑗 = 𝑘 → ∩
𝑖 ∈
(ℤ≥‘𝑛)(𝑖(𝑙 ∈ 𝑍, 𝑗 ∈ ℕ ↦ (𝑐‘(𝑙𝑃𝑗)))𝑗) = ∩ 𝑚 ∈
(ℤ≥‘𝑛)(𝑚(𝑙 ∈ 𝑍, 𝑗 ∈ ℕ ↦ (𝑐‘(𝑙𝑃𝑗)))𝑘)) |
87 | 86 | adantr 481 |
. . . . . . 7
⊢ ((𝑗 = 𝑘 ∧ 𝑛 ∈ 𝑍) → ∩
𝑖 ∈
(ℤ≥‘𝑛)(𝑖(𝑙 ∈ 𝑍, 𝑗 ∈ ℕ ↦ (𝑐‘(𝑙𝑃𝑗)))𝑗) = ∩ 𝑚 ∈
(ℤ≥‘𝑛)(𝑚(𝑙 ∈ 𝑍, 𝑗 ∈ ℕ ↦ (𝑐‘(𝑙𝑃𝑗)))𝑘)) |
88 | 87 | iuneq2dv 4542 |
. . . . . 6
⊢ (𝑗 = 𝑘 → ∪
𝑛 ∈ 𝑍 ∩ 𝑖 ∈
(ℤ≥‘𝑛)(𝑖(𝑙 ∈ 𝑍, 𝑗 ∈ ℕ ↦ (𝑐‘(𝑙𝑃𝑗)))𝑗) = ∪ 𝑛 ∈ 𝑍 ∩ 𝑚 ∈
(ℤ≥‘𝑛)(𝑚(𝑙 ∈ 𝑍, 𝑗 ∈ ℕ ↦ (𝑐‘(𝑙𝑃𝑗)))𝑘)) |
89 | 71, 79, 88 | cbviin 4558 |
. . . . 5
⊢ ∩ 𝑗 ∈ ℕ ∪ 𝑛 ∈ 𝑍 ∩ 𝑖 ∈
(ℤ≥‘𝑛)(𝑖(𝑙 ∈ 𝑍, 𝑗 ∈ ℕ ↦ (𝑐‘(𝑙𝑃𝑗)))𝑗) = ∩ 𝑘 ∈ ℕ ∪ 𝑛 ∈ 𝑍 ∩ 𝑚 ∈
(ℤ≥‘𝑛)(𝑚(𝑙 ∈ 𝑍, 𝑗 ∈ ℕ ↦ (𝑐‘(𝑙𝑃𝑗)))𝑘) |
90 | | fveq2 6191 |
. . . . . . . 8
⊢ (𝑦 = 𝑟 → (𝑐‘𝑦) = (𝑐‘𝑟)) |
91 | | id 22 |
. . . . . . . 8
⊢ (𝑦 = 𝑟 → 𝑦 = 𝑟) |
92 | 90, 91 | eleq12d 2695 |
. . . . . . 7
⊢ (𝑦 = 𝑟 → ((𝑐‘𝑦) ∈ 𝑦 ↔ (𝑐‘𝑟) ∈ 𝑟)) |
93 | 92 | rspccva 3308 |
. . . . . 6
⊢
((∀𝑦 ∈
ran 𝑃(𝑐‘𝑦) ∈ 𝑦 ∧ 𝑟 ∈ ran 𝑃) → (𝑐‘𝑟) ∈ 𝑟) |
94 | 93 | adantll 750 |
. . . . 5
⊢ (((𝜑 ∧ ∀𝑦 ∈ ran 𝑃(𝑐‘𝑦) ∈ 𝑦) ∧ 𝑟 ∈ ran 𝑃) → (𝑐‘𝑟) ∈ 𝑟) |
95 | 60, 1, 61, 62, 63, 64, 65, 12, 70, 89, 94 | smflimlem5 40983 |
. . . 4
⊢ ((𝜑 ∧ ∀𝑦 ∈ ran 𝑃(𝑐‘𝑦) ∈ 𝑦) → {𝑥 ∈ 𝐷 ∣ (𝐺‘𝑥) ≤ 𝐴} ∈ (𝑆 ↾t 𝐷)) |
96 | 95 | ex 450 |
. . 3
⊢ (𝜑 → (∀𝑦 ∈ ran 𝑃(𝑐‘𝑦) ∈ 𝑦 → {𝑥 ∈ 𝐷 ∣ (𝐺‘𝑥) ≤ 𝐴} ∈ (𝑆 ↾t 𝐷))) |
97 | 96 | exlimdv 1861 |
. 2
⊢ (𝜑 → (∃𝑐∀𝑦 ∈ ran 𝑃(𝑐‘𝑦) ∈ 𝑦 → {𝑥 ∈ 𝐷 ∣ (𝐺‘𝑥) ≤ 𝐴} ∈ (𝑆 ↾t 𝐷))) |
98 | 58, 97 | mpd 15 |
1
⊢ (𝜑 → {𝑥 ∈ 𝐷 ∣ (𝐺‘𝑥) ≤ 𝐴} ∈ (𝑆 ↾t 𝐷)) |