| Step | Hyp | Ref | Expression | 
|---|
| 1 |  | smflimlem6.2 | . . . . . . . 8
⊢ 𝑍 =
(ℤ≥‘𝑀) | 
| 2 | 1 | fvexi 6920 | . . . . . . 7
⊢ 𝑍 ∈ V | 
| 3 |  | nnex 12272 | . . . . . . 7
⊢ ℕ
∈ V | 
| 4 | 2, 3 | xpex 7773 | . . . . . 6
⊢ (𝑍 × ℕ) ∈
V | 
| 5 | 4 | a1i 11 | . . . . 5
⊢ (𝜑 → (𝑍 × ℕ) ∈ V) | 
| 6 |  | eqid 2737 | . . . . . . . . 9
⊢ {𝑠 ∈ 𝑆 ∣ {𝑥 ∈ dom (𝐹‘𝑚) ∣ ((𝐹‘𝑚)‘𝑥) < (𝐴 + (1 / 𝑘))} = (𝑠 ∩ dom (𝐹‘𝑚))} = {𝑠 ∈ 𝑆 ∣ {𝑥 ∈ dom (𝐹‘𝑚) ∣ ((𝐹‘𝑚)‘𝑥) < (𝐴 + (1 / 𝑘))} = (𝑠 ∩ dom (𝐹‘𝑚))} | 
| 7 |  | smflimlem6.3 | . . . . . . . . 9
⊢ (𝜑 → 𝑆 ∈ SAlg) | 
| 8 | 6, 7 | rabexd 5340 | . . . . . . . 8
⊢ (𝜑 → {𝑠 ∈ 𝑆 ∣ {𝑥 ∈ dom (𝐹‘𝑚) ∣ ((𝐹‘𝑚)‘𝑥) < (𝐴 + (1 / 𝑘))} = (𝑠 ∩ dom (𝐹‘𝑚))} ∈ V) | 
| 9 | 8 | adantr 480 | . . . . . . 7
⊢ ((𝜑 ∧ (𝑚 ∈ 𝑍 ∧ 𝑘 ∈ ℕ)) → {𝑠 ∈ 𝑆 ∣ {𝑥 ∈ dom (𝐹‘𝑚) ∣ ((𝐹‘𝑚)‘𝑥) < (𝐴 + (1 / 𝑘))} = (𝑠 ∩ dom (𝐹‘𝑚))} ∈ V) | 
| 10 | 9 | ralrimivva 3202 | . . . . . 6
⊢ (𝜑 → ∀𝑚 ∈ 𝑍 ∀𝑘 ∈ ℕ {𝑠 ∈ 𝑆 ∣ {𝑥 ∈ dom (𝐹‘𝑚) ∣ ((𝐹‘𝑚)‘𝑥) < (𝐴 + (1 / 𝑘))} = (𝑠 ∩ dom (𝐹‘𝑚))} ∈ V) | 
| 11 |  | smflimlem6.8 | . . . . . . 7
⊢ 𝑃 = (𝑚 ∈ 𝑍, 𝑘 ∈ ℕ ↦ {𝑠 ∈ 𝑆 ∣ {𝑥 ∈ dom (𝐹‘𝑚) ∣ ((𝐹‘𝑚)‘𝑥) < (𝐴 + (1 / 𝑘))} = (𝑠 ∩ dom (𝐹‘𝑚))}) | 
| 12 | 11 | fnmpo 8094 | . . . . . 6
⊢
(∀𝑚 ∈
𝑍 ∀𝑘 ∈ ℕ {𝑠 ∈ 𝑆 ∣ {𝑥 ∈ dom (𝐹‘𝑚) ∣ ((𝐹‘𝑚)‘𝑥) < (𝐴 + (1 / 𝑘))} = (𝑠 ∩ dom (𝐹‘𝑚))} ∈ V → 𝑃 Fn (𝑍 × ℕ)) | 
| 13 | 10, 12 | syl 17 | . . . . 5
⊢ (𝜑 → 𝑃 Fn (𝑍 × ℕ)) | 
| 14 |  | fnrndomg 10576 | . . . . 5
⊢ ((𝑍 × ℕ) ∈ V
→ (𝑃 Fn (𝑍 × ℕ) → ran
𝑃 ≼ (𝑍 ×
ℕ))) | 
| 15 | 5, 13, 14 | sylc 65 | . . . 4
⊢ (𝜑 → ran 𝑃 ≼ (𝑍 × ℕ)) | 
| 16 | 1 | uzct 45068 | . . . . . . 7
⊢ 𝑍 ≼
ω | 
| 17 |  | nnct 14022 | . . . . . . 7
⊢ ℕ
≼ ω | 
| 18 | 16, 17 | pm3.2i 470 | . . . . . 6
⊢ (𝑍 ≼ ω ∧ ℕ
≼ ω) | 
| 19 |  | xpct 10056 | . . . . . 6
⊢ ((𝑍 ≼ ω ∧ ℕ
≼ ω) → (𝑍
× ℕ) ≼ ω) | 
| 20 | 18, 19 | ax-mp 5 | . . . . 5
⊢ (𝑍 × ℕ) ≼
ω | 
| 21 | 20 | a1i 11 | . . . 4
⊢ (𝜑 → (𝑍 × ℕ) ≼
ω) | 
| 22 |  | domtr 9047 | . . . 4
⊢ ((ran
𝑃 ≼ (𝑍 × ℕ) ∧ (𝑍 × ℕ) ≼
ω) → ran 𝑃
≼ ω) | 
| 23 | 15, 21, 22 | syl2anc 584 | . . 3
⊢ (𝜑 → ran 𝑃 ≼ ω) | 
| 24 |  | vex 3484 | . . . . . . 7
⊢ 𝑦 ∈ V | 
| 25 | 11 | elrnmpog 7568 | . . . . . . 7
⊢ (𝑦 ∈ V → (𝑦 ∈ ran 𝑃 ↔ ∃𝑚 ∈ 𝑍 ∃𝑘 ∈ ℕ 𝑦 = {𝑠 ∈ 𝑆 ∣ {𝑥 ∈ dom (𝐹‘𝑚) ∣ ((𝐹‘𝑚)‘𝑥) < (𝐴 + (1 / 𝑘))} = (𝑠 ∩ dom (𝐹‘𝑚))})) | 
| 26 | 24, 25 | ax-mp 5 | . . . . . 6
⊢ (𝑦 ∈ ran 𝑃 ↔ ∃𝑚 ∈ 𝑍 ∃𝑘 ∈ ℕ 𝑦 = {𝑠 ∈ 𝑆 ∣ {𝑥 ∈ dom (𝐹‘𝑚) ∣ ((𝐹‘𝑚)‘𝑥) < (𝐴 + (1 / 𝑘))} = (𝑠 ∩ dom (𝐹‘𝑚))}) | 
| 27 | 26 | biimpi 216 | . . . . 5
⊢ (𝑦 ∈ ran 𝑃 → ∃𝑚 ∈ 𝑍 ∃𝑘 ∈ ℕ 𝑦 = {𝑠 ∈ 𝑆 ∣ {𝑥 ∈ dom (𝐹‘𝑚) ∣ ((𝐹‘𝑚)‘𝑥) < (𝐴 + (1 / 𝑘))} = (𝑠 ∩ dom (𝐹‘𝑚))}) | 
| 28 | 27 | adantl 481 | . . . 4
⊢ ((𝜑 ∧ 𝑦 ∈ ran 𝑃) → ∃𝑚 ∈ 𝑍 ∃𝑘 ∈ ℕ 𝑦 = {𝑠 ∈ 𝑆 ∣ {𝑥 ∈ dom (𝐹‘𝑚) ∣ ((𝐹‘𝑚)‘𝑥) < (𝐴 + (1 / 𝑘))} = (𝑠 ∩ dom (𝐹‘𝑚))}) | 
| 29 |  | simp3 1139 | . . . . . . . 8
⊢ ((𝜑 ∧ (𝑚 ∈ 𝑍 ∧ 𝑘 ∈ ℕ) ∧ 𝑦 = {𝑠 ∈ 𝑆 ∣ {𝑥 ∈ dom (𝐹‘𝑚) ∣ ((𝐹‘𝑚)‘𝑥) < (𝐴 + (1 / 𝑘))} = (𝑠 ∩ dom (𝐹‘𝑚))}) → 𝑦 = {𝑠 ∈ 𝑆 ∣ {𝑥 ∈ dom (𝐹‘𝑚) ∣ ((𝐹‘𝑚)‘𝑥) < (𝐴 + (1 / 𝑘))} = (𝑠 ∩ dom (𝐹‘𝑚))}) | 
| 30 | 7 | adantr 480 | . . . . . . . . . . . 12
⊢ ((𝜑 ∧ (𝑚 ∈ 𝑍 ∧ 𝑘 ∈ ℕ)) → 𝑆 ∈ SAlg) | 
| 31 |  | smflimlem6.4 | . . . . . . . . . . . . . 14
⊢ (𝜑 → 𝐹:𝑍⟶(SMblFn‘𝑆)) | 
| 32 | 31 | ffvelcdmda 7104 | . . . . . . . . . . . . 13
⊢ ((𝜑 ∧ 𝑚 ∈ 𝑍) → (𝐹‘𝑚) ∈ (SMblFn‘𝑆)) | 
| 33 | 32 | adantrr 717 | . . . . . . . . . . . 12
⊢ ((𝜑 ∧ (𝑚 ∈ 𝑍 ∧ 𝑘 ∈ ℕ)) → (𝐹‘𝑚) ∈ (SMblFn‘𝑆)) | 
| 34 |  | eqid 2737 | . . . . . . . . . . . 12
⊢ dom
(𝐹‘𝑚) = dom (𝐹‘𝑚) | 
| 35 |  | smflimlem6.7 | . . . . . . . . . . . . . . 15
⊢ (𝜑 → 𝐴 ∈ ℝ) | 
| 36 | 35 | adantr 480 | . . . . . . . . . . . . . 14
⊢ ((𝜑 ∧ 𝑘 ∈ ℕ) → 𝐴 ∈ ℝ) | 
| 37 |  | nnrecre 12308 | . . . . . . . . . . . . . . 15
⊢ (𝑘 ∈ ℕ → (1 /
𝑘) ∈
ℝ) | 
| 38 | 37 | adantl 481 | . . . . . . . . . . . . . 14
⊢ ((𝜑 ∧ 𝑘 ∈ ℕ) → (1 / 𝑘) ∈
ℝ) | 
| 39 | 36, 38 | readdcld 11290 | . . . . . . . . . . . . 13
⊢ ((𝜑 ∧ 𝑘 ∈ ℕ) → (𝐴 + (1 / 𝑘)) ∈ ℝ) | 
| 40 | 39 | adantrl 716 | . . . . . . . . . . . 12
⊢ ((𝜑 ∧ (𝑚 ∈ 𝑍 ∧ 𝑘 ∈ ℕ)) → (𝐴 + (1 / 𝑘)) ∈ ℝ) | 
| 41 | 30, 33, 34, 40 | smfpreimalt 46746 | . . . . . . . . . . 11
⊢ ((𝜑 ∧ (𝑚 ∈ 𝑍 ∧ 𝑘 ∈ ℕ)) → {𝑥 ∈ dom (𝐹‘𝑚) ∣ ((𝐹‘𝑚)‘𝑥) < (𝐴 + (1 / 𝑘))} ∈ (𝑆 ↾t dom (𝐹‘𝑚))) | 
| 42 |  | fvex 6919 | . . . . . . . . . . . . . . 15
⊢ (𝐹‘𝑚) ∈ V | 
| 43 | 42 | dmex 7931 | . . . . . . . . . . . . . 14
⊢ dom
(𝐹‘𝑚) ∈ V | 
| 44 | 43 | a1i 11 | . . . . . . . . . . . . 13
⊢ (𝜑 → dom (𝐹‘𝑚) ∈ V) | 
| 45 |  | elrest 17472 | . . . . . . . . . . . . 13
⊢ ((𝑆 ∈ SAlg ∧ dom (𝐹‘𝑚) ∈ V) → ({𝑥 ∈ dom (𝐹‘𝑚) ∣ ((𝐹‘𝑚)‘𝑥) < (𝐴 + (1 / 𝑘))} ∈ (𝑆 ↾t dom (𝐹‘𝑚)) ↔ ∃𝑠 ∈ 𝑆 {𝑥 ∈ dom (𝐹‘𝑚) ∣ ((𝐹‘𝑚)‘𝑥) < (𝐴 + (1 / 𝑘))} = (𝑠 ∩ dom (𝐹‘𝑚)))) | 
| 46 | 7, 44, 45 | syl2anc 584 | . . . . . . . . . . . 12
⊢ (𝜑 → ({𝑥 ∈ dom (𝐹‘𝑚) ∣ ((𝐹‘𝑚)‘𝑥) < (𝐴 + (1 / 𝑘))} ∈ (𝑆 ↾t dom (𝐹‘𝑚)) ↔ ∃𝑠 ∈ 𝑆 {𝑥 ∈ dom (𝐹‘𝑚) ∣ ((𝐹‘𝑚)‘𝑥) < (𝐴 + (1 / 𝑘))} = (𝑠 ∩ dom (𝐹‘𝑚)))) | 
| 47 | 46 | adantr 480 | . . . . . . . . . . 11
⊢ ((𝜑 ∧ (𝑚 ∈ 𝑍 ∧ 𝑘 ∈ ℕ)) → ({𝑥 ∈ dom (𝐹‘𝑚) ∣ ((𝐹‘𝑚)‘𝑥) < (𝐴 + (1 / 𝑘))} ∈ (𝑆 ↾t dom (𝐹‘𝑚)) ↔ ∃𝑠 ∈ 𝑆 {𝑥 ∈ dom (𝐹‘𝑚) ∣ ((𝐹‘𝑚)‘𝑥) < (𝐴 + (1 / 𝑘))} = (𝑠 ∩ dom (𝐹‘𝑚)))) | 
| 48 | 41, 47 | mpbid 232 | . . . . . . . . . 10
⊢ ((𝜑 ∧ (𝑚 ∈ 𝑍 ∧ 𝑘 ∈ ℕ)) → ∃𝑠 ∈ 𝑆 {𝑥 ∈ dom (𝐹‘𝑚) ∣ ((𝐹‘𝑚)‘𝑥) < (𝐴 + (1 / 𝑘))} = (𝑠 ∩ dom (𝐹‘𝑚))) | 
| 49 |  | rabn0 4389 | . . . . . . . . . 10
⊢ ({𝑠 ∈ 𝑆 ∣ {𝑥 ∈ dom (𝐹‘𝑚) ∣ ((𝐹‘𝑚)‘𝑥) < (𝐴 + (1 / 𝑘))} = (𝑠 ∩ dom (𝐹‘𝑚))} ≠ ∅ ↔ ∃𝑠 ∈ 𝑆 {𝑥 ∈ dom (𝐹‘𝑚) ∣ ((𝐹‘𝑚)‘𝑥) < (𝐴 + (1 / 𝑘))} = (𝑠 ∩ dom (𝐹‘𝑚))) | 
| 50 | 48, 49 | sylibr 234 | . . . . . . . . 9
⊢ ((𝜑 ∧ (𝑚 ∈ 𝑍 ∧ 𝑘 ∈ ℕ)) → {𝑠 ∈ 𝑆 ∣ {𝑥 ∈ dom (𝐹‘𝑚) ∣ ((𝐹‘𝑚)‘𝑥) < (𝐴 + (1 / 𝑘))} = (𝑠 ∩ dom (𝐹‘𝑚))} ≠ ∅) | 
| 51 | 50 | 3adant3 1133 | . . . . . . . 8
⊢ ((𝜑 ∧ (𝑚 ∈ 𝑍 ∧ 𝑘 ∈ ℕ) ∧ 𝑦 = {𝑠 ∈ 𝑆 ∣ {𝑥 ∈ dom (𝐹‘𝑚) ∣ ((𝐹‘𝑚)‘𝑥) < (𝐴 + (1 / 𝑘))} = (𝑠 ∩ dom (𝐹‘𝑚))}) → {𝑠 ∈ 𝑆 ∣ {𝑥 ∈ dom (𝐹‘𝑚) ∣ ((𝐹‘𝑚)‘𝑥) < (𝐴 + (1 / 𝑘))} = (𝑠 ∩ dom (𝐹‘𝑚))} ≠ ∅) | 
| 52 | 29, 51 | eqnetrd 3008 | . . . . . . 7
⊢ ((𝜑 ∧ (𝑚 ∈ 𝑍 ∧ 𝑘 ∈ ℕ) ∧ 𝑦 = {𝑠 ∈ 𝑆 ∣ {𝑥 ∈ dom (𝐹‘𝑚) ∣ ((𝐹‘𝑚)‘𝑥) < (𝐴 + (1 / 𝑘))} = (𝑠 ∩ dom (𝐹‘𝑚))}) → 𝑦 ≠ ∅) | 
| 53 | 52 | 3exp 1120 | . . . . . 6
⊢ (𝜑 → ((𝑚 ∈ 𝑍 ∧ 𝑘 ∈ ℕ) → (𝑦 = {𝑠 ∈ 𝑆 ∣ {𝑥 ∈ dom (𝐹‘𝑚) ∣ ((𝐹‘𝑚)‘𝑥) < (𝐴 + (1 / 𝑘))} = (𝑠 ∩ dom (𝐹‘𝑚))} → 𝑦 ≠ ∅))) | 
| 54 | 53 | rexlimdvv 3212 | . . . . 5
⊢ (𝜑 → (∃𝑚 ∈ 𝑍 ∃𝑘 ∈ ℕ 𝑦 = {𝑠 ∈ 𝑆 ∣ {𝑥 ∈ dom (𝐹‘𝑚) ∣ ((𝐹‘𝑚)‘𝑥) < (𝐴 + (1 / 𝑘))} = (𝑠 ∩ dom (𝐹‘𝑚))} → 𝑦 ≠ ∅)) | 
| 55 | 54 | adantr 480 | . . . 4
⊢ ((𝜑 ∧ 𝑦 ∈ ran 𝑃) → (∃𝑚 ∈ 𝑍 ∃𝑘 ∈ ℕ 𝑦 = {𝑠 ∈ 𝑆 ∣ {𝑥 ∈ dom (𝐹‘𝑚) ∣ ((𝐹‘𝑚)‘𝑥) < (𝐴 + (1 / 𝑘))} = (𝑠 ∩ dom (𝐹‘𝑚))} → 𝑦 ≠ ∅)) | 
| 56 | 28, 55 | mpd 15 | . . 3
⊢ ((𝜑 ∧ 𝑦 ∈ ran 𝑃) → 𝑦 ≠ ∅) | 
| 57 | 23, 56 | axccd2 45235 | . 2
⊢ (𝜑 → ∃𝑐∀𝑦 ∈ ran 𝑃(𝑐‘𝑦) ∈ 𝑦) | 
| 58 |  | smflimlem6.1 | . . . . . 6
⊢ (𝜑 → 𝑀 ∈ ℤ) | 
| 59 | 58 | adantr 480 | . . . . 5
⊢ ((𝜑 ∧ ∀𝑦 ∈ ran 𝑃(𝑐‘𝑦) ∈ 𝑦) → 𝑀 ∈ ℤ) | 
| 60 | 7 | adantr 480 | . . . . 5
⊢ ((𝜑 ∧ ∀𝑦 ∈ ran 𝑃(𝑐‘𝑦) ∈ 𝑦) → 𝑆 ∈ SAlg) | 
| 61 | 31 | adantr 480 | . . . . 5
⊢ ((𝜑 ∧ ∀𝑦 ∈ ran 𝑃(𝑐‘𝑦) ∈ 𝑦) → 𝐹:𝑍⟶(SMblFn‘𝑆)) | 
| 62 |  | smflimlem6.5 | . . . . 5
⊢ 𝐷 = {𝑥 ∈ ∪
𝑛 ∈ 𝑍 ∩ 𝑚 ∈
(ℤ≥‘𝑛)dom (𝐹‘𝑚) ∣ (𝑚 ∈ 𝑍 ↦ ((𝐹‘𝑚)‘𝑥)) ∈ dom ⇝ } | 
| 63 |  | smflimlem6.6 | . . . . 5
⊢ 𝐺 = (𝑥 ∈ 𝐷 ↦ ( ⇝ ‘(𝑚 ∈ 𝑍 ↦ ((𝐹‘𝑚)‘𝑥)))) | 
| 64 | 35 | adantr 480 | . . . . 5
⊢ ((𝜑 ∧ ∀𝑦 ∈ ran 𝑃(𝑐‘𝑦) ∈ 𝑦) → 𝐴 ∈ ℝ) | 
| 65 |  | fvoveq1 7454 | . . . . . 6
⊢ (𝑙 = 𝑚 → (𝑐‘(𝑙𝑃𝑗)) = (𝑐‘(𝑚𝑃𝑗))) | 
| 66 |  | oveq2 7439 | . . . . . . 7
⊢ (𝑗 = 𝑘 → (𝑚𝑃𝑗) = (𝑚𝑃𝑘)) | 
| 67 | 66 | fveq2d 6910 | . . . . . 6
⊢ (𝑗 = 𝑘 → (𝑐‘(𝑚𝑃𝑗)) = (𝑐‘(𝑚𝑃𝑘))) | 
| 68 | 65, 67 | cbvmpov 7528 | . . . . 5
⊢ (𝑙 ∈ 𝑍, 𝑗 ∈ ℕ ↦ (𝑐‘(𝑙𝑃𝑗))) = (𝑚 ∈ 𝑍, 𝑘 ∈ ℕ ↦ (𝑐‘(𝑚𝑃𝑘))) | 
| 69 |  | nfcv 2905 | . . . . . 6
⊢
Ⅎ𝑘∪ 𝑛 ∈ 𝑍 ∩ 𝑖 ∈
(ℤ≥‘𝑛)(𝑖(𝑙 ∈ 𝑍, 𝑗 ∈ ℕ ↦ (𝑐‘(𝑙𝑃𝑗)))𝑗) | 
| 70 |  | nfcv 2905 | . . . . . . 7
⊢
Ⅎ𝑗𝑍 | 
| 71 |  | nfcv 2905 | . . . . . . . 8
⊢
Ⅎ𝑗(ℤ≥‘𝑛) | 
| 72 |  | nfcv 2905 | . . . . . . . . 9
⊢
Ⅎ𝑗𝑚 | 
| 73 |  | nfmpo2 7514 | . . . . . . . . 9
⊢
Ⅎ𝑗(𝑙 ∈ 𝑍, 𝑗 ∈ ℕ ↦ (𝑐‘(𝑙𝑃𝑗))) | 
| 74 |  | nfcv 2905 | . . . . . . . . 9
⊢
Ⅎ𝑗𝑘 | 
| 75 | 72, 73, 74 | nfov 7461 | . . . . . . . 8
⊢
Ⅎ𝑗(𝑚(𝑙 ∈ 𝑍, 𝑗 ∈ ℕ ↦ (𝑐‘(𝑙𝑃𝑗)))𝑘) | 
| 76 | 71, 75 | nfiin 5024 | . . . . . . 7
⊢
Ⅎ𝑗∩ 𝑚 ∈
(ℤ≥‘𝑛)(𝑚(𝑙 ∈ 𝑍, 𝑗 ∈ ℕ ↦ (𝑐‘(𝑙𝑃𝑗)))𝑘) | 
| 77 | 70, 76 | nfiun 5023 | . . . . . 6
⊢
Ⅎ𝑗∪ 𝑛 ∈ 𝑍 ∩ 𝑚 ∈
(ℤ≥‘𝑛)(𝑚(𝑙 ∈ 𝑍, 𝑗 ∈ ℕ ↦ (𝑐‘(𝑙𝑃𝑗)))𝑘) | 
| 78 |  | oveq2 7439 | . . . . . . . . . . 11
⊢ (𝑗 = 𝑘 → (𝑖(𝑙 ∈ 𝑍, 𝑗 ∈ ℕ ↦ (𝑐‘(𝑙𝑃𝑗)))𝑗) = (𝑖(𝑙 ∈ 𝑍, 𝑗 ∈ ℕ ↦ (𝑐‘(𝑙𝑃𝑗)))𝑘)) | 
| 79 | 78 | adantr 480 | . . . . . . . . . 10
⊢ ((𝑗 = 𝑘 ∧ 𝑖 ∈ (ℤ≥‘𝑛)) → (𝑖(𝑙 ∈ 𝑍, 𝑗 ∈ ℕ ↦ (𝑐‘(𝑙𝑃𝑗)))𝑗) = (𝑖(𝑙 ∈ 𝑍, 𝑗 ∈ ℕ ↦ (𝑐‘(𝑙𝑃𝑗)))𝑘)) | 
| 80 | 79 | iineq2dv 5017 | . . . . . . . . 9
⊢ (𝑗 = 𝑘 → ∩
𝑖 ∈
(ℤ≥‘𝑛)(𝑖(𝑙 ∈ 𝑍, 𝑗 ∈ ℕ ↦ (𝑐‘(𝑙𝑃𝑗)))𝑗) = ∩ 𝑖 ∈
(ℤ≥‘𝑛)(𝑖(𝑙 ∈ 𝑍, 𝑗 ∈ ℕ ↦ (𝑐‘(𝑙𝑃𝑗)))𝑘)) | 
| 81 |  | oveq1 7438 | . . . . . . . . . . 11
⊢ (𝑖 = 𝑚 → (𝑖(𝑙 ∈ 𝑍, 𝑗 ∈ ℕ ↦ (𝑐‘(𝑙𝑃𝑗)))𝑘) = (𝑚(𝑙 ∈ 𝑍, 𝑗 ∈ ℕ ↦ (𝑐‘(𝑙𝑃𝑗)))𝑘)) | 
| 82 | 81 | cbviinv 5041 | . . . . . . . . . 10
⊢ ∩ 𝑖 ∈ (ℤ≥‘𝑛)(𝑖(𝑙 ∈ 𝑍, 𝑗 ∈ ℕ ↦ (𝑐‘(𝑙𝑃𝑗)))𝑘) = ∩ 𝑚 ∈
(ℤ≥‘𝑛)(𝑚(𝑙 ∈ 𝑍, 𝑗 ∈ ℕ ↦ (𝑐‘(𝑙𝑃𝑗)))𝑘) | 
| 83 | 82 | a1i 11 | . . . . . . . . 9
⊢ (𝑗 = 𝑘 → ∩
𝑖 ∈
(ℤ≥‘𝑛)(𝑖(𝑙 ∈ 𝑍, 𝑗 ∈ ℕ ↦ (𝑐‘(𝑙𝑃𝑗)))𝑘) = ∩ 𝑚 ∈
(ℤ≥‘𝑛)(𝑚(𝑙 ∈ 𝑍, 𝑗 ∈ ℕ ↦ (𝑐‘(𝑙𝑃𝑗)))𝑘)) | 
| 84 | 80, 83 | eqtrd 2777 | . . . . . . . 8
⊢ (𝑗 = 𝑘 → ∩
𝑖 ∈
(ℤ≥‘𝑛)(𝑖(𝑙 ∈ 𝑍, 𝑗 ∈ ℕ ↦ (𝑐‘(𝑙𝑃𝑗)))𝑗) = ∩ 𝑚 ∈
(ℤ≥‘𝑛)(𝑚(𝑙 ∈ 𝑍, 𝑗 ∈ ℕ ↦ (𝑐‘(𝑙𝑃𝑗)))𝑘)) | 
| 85 | 84 | adantr 480 | . . . . . . 7
⊢ ((𝑗 = 𝑘 ∧ 𝑛 ∈ 𝑍) → ∩
𝑖 ∈
(ℤ≥‘𝑛)(𝑖(𝑙 ∈ 𝑍, 𝑗 ∈ ℕ ↦ (𝑐‘(𝑙𝑃𝑗)))𝑗) = ∩ 𝑚 ∈
(ℤ≥‘𝑛)(𝑚(𝑙 ∈ 𝑍, 𝑗 ∈ ℕ ↦ (𝑐‘(𝑙𝑃𝑗)))𝑘)) | 
| 86 | 85 | iuneq2dv 5016 | . . . . . 6
⊢ (𝑗 = 𝑘 → ∪
𝑛 ∈ 𝑍 ∩ 𝑖 ∈
(ℤ≥‘𝑛)(𝑖(𝑙 ∈ 𝑍, 𝑗 ∈ ℕ ↦ (𝑐‘(𝑙𝑃𝑗)))𝑗) = ∪ 𝑛 ∈ 𝑍 ∩ 𝑚 ∈
(ℤ≥‘𝑛)(𝑚(𝑙 ∈ 𝑍, 𝑗 ∈ ℕ ↦ (𝑐‘(𝑙𝑃𝑗)))𝑘)) | 
| 87 | 69, 77, 86 | cbviin 5037 | . . . . 5
⊢ ∩ 𝑗 ∈ ℕ ∪ 𝑛 ∈ 𝑍 ∩ 𝑖 ∈
(ℤ≥‘𝑛)(𝑖(𝑙 ∈ 𝑍, 𝑗 ∈ ℕ ↦ (𝑐‘(𝑙𝑃𝑗)))𝑗) = ∩ 𝑘 ∈ ℕ ∪ 𝑛 ∈ 𝑍 ∩ 𝑚 ∈
(ℤ≥‘𝑛)(𝑚(𝑙 ∈ 𝑍, 𝑗 ∈ ℕ ↦ (𝑐‘(𝑙𝑃𝑗)))𝑘) | 
| 88 |  | fveq2 6906 | . . . . . . . 8
⊢ (𝑦 = 𝑟 → (𝑐‘𝑦) = (𝑐‘𝑟)) | 
| 89 |  | id 22 | . . . . . . . 8
⊢ (𝑦 = 𝑟 → 𝑦 = 𝑟) | 
| 90 | 88, 89 | eleq12d 2835 | . . . . . . 7
⊢ (𝑦 = 𝑟 → ((𝑐‘𝑦) ∈ 𝑦 ↔ (𝑐‘𝑟) ∈ 𝑟)) | 
| 91 | 90 | rspccva 3621 | . . . . . 6
⊢
((∀𝑦 ∈
ran 𝑃(𝑐‘𝑦) ∈ 𝑦 ∧ 𝑟 ∈ ran 𝑃) → (𝑐‘𝑟) ∈ 𝑟) | 
| 92 | 91 | adantll 714 | . . . . 5
⊢ (((𝜑 ∧ ∀𝑦 ∈ ran 𝑃(𝑐‘𝑦) ∈ 𝑦) ∧ 𝑟 ∈ ran 𝑃) → (𝑐‘𝑟) ∈ 𝑟) | 
| 93 | 59, 1, 60, 61, 62, 63, 64, 11, 68, 87, 92 | smflimlem5 46790 | . . . 4
⊢ ((𝜑 ∧ ∀𝑦 ∈ ran 𝑃(𝑐‘𝑦) ∈ 𝑦) → {𝑥 ∈ 𝐷 ∣ (𝐺‘𝑥) ≤ 𝐴} ∈ (𝑆 ↾t 𝐷)) | 
| 94 | 93 | ex 412 | . . 3
⊢ (𝜑 → (∀𝑦 ∈ ran 𝑃(𝑐‘𝑦) ∈ 𝑦 → {𝑥 ∈ 𝐷 ∣ (𝐺‘𝑥) ≤ 𝐴} ∈ (𝑆 ↾t 𝐷))) | 
| 95 | 94 | exlimdv 1933 | . 2
⊢ (𝜑 → (∃𝑐∀𝑦 ∈ ran 𝑃(𝑐‘𝑦) ∈ 𝑦 → {𝑥 ∈ 𝐷 ∣ (𝐺‘𝑥) ≤ 𝐴} ∈ (𝑆 ↾t 𝐷))) | 
| 96 | 57, 95 | mpd 15 | 1
⊢ (𝜑 → {𝑥 ∈ 𝐷 ∣ (𝐺‘𝑥) ≤ 𝐴} ∈ (𝑆 ↾t 𝐷)) |