| Step | Hyp | Ref
| Expression |
| 1 | | smflimlem1.2 |
. 2
⊢ (𝜑 → 𝑆 ∈ SAlg) |
| 2 | | smflimlem1.3 |
. . . 4
⊢ 𝐷 = {𝑥 ∈ ∪
𝑛 ∈ 𝑍 ∩ 𝑚 ∈
(ℤ≥‘𝑛)dom (𝐹‘𝑚) ∣ (𝑚 ∈ 𝑍 ↦ ((𝐹‘𝑚)‘𝑥)) ∈ dom ⇝ } |
| 3 | | smflimlem1.1 |
. . . . . . 7
⊢ 𝑍 =
(ℤ≥‘𝑀) |
| 4 | | fvex 6919 |
. . . . . . 7
⊢
(ℤ≥‘𝑀) ∈ V |
| 5 | 3, 4 | eqeltri 2837 |
. . . . . 6
⊢ 𝑍 ∈ V |
| 6 | | uzssz 12899 |
. . . . . . . . . . 11
⊢
(ℤ≥‘𝑀) ⊆ ℤ |
| 7 | 3 | eleq2i 2833 |
. . . . . . . . . . . 12
⊢ (𝑛 ∈ 𝑍 ↔ 𝑛 ∈ (ℤ≥‘𝑀)) |
| 8 | 7 | biimpi 216 |
. . . . . . . . . . 11
⊢ (𝑛 ∈ 𝑍 → 𝑛 ∈ (ℤ≥‘𝑀)) |
| 9 | 6, 8 | sselid 3981 |
. . . . . . . . . 10
⊢ (𝑛 ∈ 𝑍 → 𝑛 ∈ ℤ) |
| 10 | | uzid 12893 |
. . . . . . . . . 10
⊢ (𝑛 ∈ ℤ → 𝑛 ∈
(ℤ≥‘𝑛)) |
| 11 | 9, 10 | syl 17 |
. . . . . . . . 9
⊢ (𝑛 ∈ 𝑍 → 𝑛 ∈ (ℤ≥‘𝑛)) |
| 12 | 11 | ne0d 4342 |
. . . . . . . 8
⊢ (𝑛 ∈ 𝑍 → (ℤ≥‘𝑛) ≠ ∅) |
| 13 | | fvex 6919 |
. . . . . . . . . . 11
⊢ (𝐹‘𝑚) ∈ V |
| 14 | 13 | dmex 7931 |
. . . . . . . . . 10
⊢ dom
(𝐹‘𝑚) ∈ V |
| 15 | 14 | rgenw 3065 |
. . . . . . . . 9
⊢
∀𝑚 ∈
(ℤ≥‘𝑛)dom (𝐹‘𝑚) ∈ V |
| 16 | 15 | a1i 11 |
. . . . . . . 8
⊢ (𝑛 ∈ 𝑍 → ∀𝑚 ∈ (ℤ≥‘𝑛)dom (𝐹‘𝑚) ∈ V) |
| 17 | | iinexg 5348 |
. . . . . . . 8
⊢
(((ℤ≥‘𝑛) ≠ ∅ ∧ ∀𝑚 ∈
(ℤ≥‘𝑛)dom (𝐹‘𝑚) ∈ V) → ∩ 𝑚 ∈ (ℤ≥‘𝑛)dom (𝐹‘𝑚) ∈ V) |
| 18 | 12, 16, 17 | syl2anc 584 |
. . . . . . 7
⊢ (𝑛 ∈ 𝑍 → ∩
𝑚 ∈
(ℤ≥‘𝑛)dom (𝐹‘𝑚) ∈ V) |
| 19 | 18 | rgen 3063 |
. . . . . 6
⊢
∀𝑛 ∈
𝑍 ∩ 𝑚 ∈ (ℤ≥‘𝑛)dom (𝐹‘𝑚) ∈ V |
| 20 | | iunexg 7988 |
. . . . . 6
⊢ ((𝑍 ∈ V ∧ ∀𝑛 ∈ 𝑍 ∩ 𝑚 ∈
(ℤ≥‘𝑛)dom (𝐹‘𝑚) ∈ V) → ∪ 𝑛 ∈ 𝑍 ∩ 𝑚 ∈
(ℤ≥‘𝑛)dom (𝐹‘𝑚) ∈ V) |
| 21 | 5, 19, 20 | mp2an 692 |
. . . . 5
⊢ ∪ 𝑛 ∈ 𝑍 ∩ 𝑚 ∈
(ℤ≥‘𝑛)dom (𝐹‘𝑚) ∈ V |
| 22 | 21 | rabex 5339 |
. . . 4
⊢ {𝑥 ∈ ∪ 𝑛 ∈ 𝑍 ∩ 𝑚 ∈
(ℤ≥‘𝑛)dom (𝐹‘𝑚) ∣ (𝑚 ∈ 𝑍 ↦ ((𝐹‘𝑚)‘𝑥)) ∈ dom ⇝ } ∈
V |
| 23 | 2, 22 | eqeltri 2837 |
. . 3
⊢ 𝐷 ∈ V |
| 24 | 23 | a1i 11 |
. 2
⊢ (𝜑 → 𝐷 ∈ V) |
| 25 | | smflimlem1.6 |
. . 3
⊢ 𝐼 = ∩ 𝑘 ∈ ℕ ∪ 𝑛 ∈ 𝑍 ∩ 𝑚 ∈
(ℤ≥‘𝑛)(𝑚𝐻𝑘) |
| 26 | | nnct 14022 |
. . . . 5
⊢ ℕ
≼ ω |
| 27 | 26 | a1i 11 |
. . . 4
⊢ (𝜑 → ℕ ≼
ω) |
| 28 | | nnn0 45389 |
. . . . 5
⊢ ℕ
≠ ∅ |
| 29 | 28 | a1i 11 |
. . . 4
⊢ (𝜑 → ℕ ≠
∅) |
| 30 | 1 | adantr 480 |
. . . . 5
⊢ ((𝜑 ∧ 𝑘 ∈ ℕ) → 𝑆 ∈ SAlg) |
| 31 | 3 | uzct 45068 |
. . . . . 6
⊢ 𝑍 ≼
ω |
| 32 | 31 | a1i 11 |
. . . . 5
⊢ ((𝜑 ∧ 𝑘 ∈ ℕ) → 𝑍 ≼ ω) |
| 33 | 30 | adantr 480 |
. . . . . 6
⊢ (((𝜑 ∧ 𝑘 ∈ ℕ) ∧ 𝑛 ∈ 𝑍) → 𝑆 ∈ SAlg) |
| 34 | | eqid 2737 |
. . . . . . . 8
⊢
(ℤ≥‘𝑛) = (ℤ≥‘𝑛) |
| 35 | 34 | uzct 45068 |
. . . . . . 7
⊢
(ℤ≥‘𝑛) ≼ ω |
| 36 | 35 | a1i 11 |
. . . . . 6
⊢ (((𝜑 ∧ 𝑘 ∈ ℕ) ∧ 𝑛 ∈ 𝑍) → (ℤ≥‘𝑛) ≼
ω) |
| 37 | 12 | adantl 481 |
. . . . . 6
⊢ (((𝜑 ∧ 𝑘 ∈ ℕ) ∧ 𝑛 ∈ 𝑍) → (ℤ≥‘𝑛) ≠ ∅) |
| 38 | | simpll 767 |
. . . . . . . 8
⊢ (((𝜑 ∧ 𝑛 ∈ 𝑍) ∧ 𝑚 ∈ (ℤ≥‘𝑛)) → 𝜑) |
| 39 | 38 | adantllr 719 |
. . . . . . 7
⊢ ((((𝜑 ∧ 𝑘 ∈ ℕ) ∧ 𝑛 ∈ 𝑍) ∧ 𝑚 ∈ (ℤ≥‘𝑛)) → 𝜑) |
| 40 | | simpll 767 |
. . . . . . . 8
⊢ (((𝑘 ∈ ℕ ∧ 𝑛 ∈ 𝑍) ∧ 𝑚 ∈ (ℤ≥‘𝑛)) → 𝑘 ∈ ℕ) |
| 41 | 40 | adantlll 718 |
. . . . . . 7
⊢ ((((𝜑 ∧ 𝑘 ∈ ℕ) ∧ 𝑛 ∈ 𝑍) ∧ 𝑚 ∈ (ℤ≥‘𝑛)) → 𝑘 ∈ ℕ) |
| 42 | 3 | uztrn2 12897 |
. . . . . . . . . 10
⊢ ((𝑛 ∈ 𝑍 ∧ 𝑗 ∈ (ℤ≥‘𝑛)) → 𝑗 ∈ 𝑍) |
| 43 | 42 | ssd 45085 |
. . . . . . . . 9
⊢ (𝑛 ∈ 𝑍 → (ℤ≥‘𝑛) ⊆ 𝑍) |
| 44 | 43 | sselda 3983 |
. . . . . . . 8
⊢ ((𝑛 ∈ 𝑍 ∧ 𝑚 ∈ (ℤ≥‘𝑛)) → 𝑚 ∈ 𝑍) |
| 45 | 44 | adantll 714 |
. . . . . . 7
⊢ ((((𝜑 ∧ 𝑘 ∈ ℕ) ∧ 𝑛 ∈ 𝑍) ∧ 𝑚 ∈ (ℤ≥‘𝑛)) → 𝑚 ∈ 𝑍) |
| 46 | | simp3 1139 |
. . . . . . . . 9
⊢ ((𝜑 ∧ 𝑘 ∈ ℕ ∧ 𝑚 ∈ 𝑍) → 𝑚 ∈ 𝑍) |
| 47 | | simp2 1138 |
. . . . . . . . 9
⊢ ((𝜑 ∧ 𝑘 ∈ ℕ ∧ 𝑚 ∈ 𝑍) → 𝑘 ∈ ℕ) |
| 48 | | fvex 6919 |
. . . . . . . . . 10
⊢ (𝐶‘(𝑚𝑃𝑘)) ∈ V |
| 49 | 48 | a1i 11 |
. . . . . . . . 9
⊢ ((𝜑 ∧ 𝑘 ∈ ℕ ∧ 𝑚 ∈ 𝑍) → (𝐶‘(𝑚𝑃𝑘)) ∈ V) |
| 50 | | smflimlem1.5 |
. . . . . . . . . 10
⊢ 𝐻 = (𝑚 ∈ 𝑍, 𝑘 ∈ ℕ ↦ (𝐶‘(𝑚𝑃𝑘))) |
| 51 | 50 | ovmpt4g 7580 |
. . . . . . . . 9
⊢ ((𝑚 ∈ 𝑍 ∧ 𝑘 ∈ ℕ ∧ (𝐶‘(𝑚𝑃𝑘)) ∈ V) → (𝑚𝐻𝑘) = (𝐶‘(𝑚𝑃𝑘))) |
| 52 | 46, 47, 49, 51 | syl3anc 1373 |
. . . . . . . 8
⊢ ((𝜑 ∧ 𝑘 ∈ ℕ ∧ 𝑚 ∈ 𝑍) → (𝑚𝐻𝑘) = (𝐶‘(𝑚𝑃𝑘))) |
| 53 | | simp1 1137 |
. . . . . . . . . . . 12
⊢ ((𝜑 ∧ 𝑘 ∈ ℕ ∧ 𝑚 ∈ 𝑍) → 𝜑) |
| 54 | | eqid 2737 |
. . . . . . . . . . . . 13
⊢ {𝑠 ∈ 𝑆 ∣ {𝑥 ∈ dom (𝐹‘𝑚) ∣ ((𝐹‘𝑚)‘𝑥) < (𝐴 + (1 / 𝑘))} = (𝑠 ∩ dom (𝐹‘𝑚))} = {𝑠 ∈ 𝑆 ∣ {𝑥 ∈ dom (𝐹‘𝑚) ∣ ((𝐹‘𝑚)‘𝑥) < (𝐴 + (1 / 𝑘))} = (𝑠 ∩ dom (𝐹‘𝑚))} |
| 55 | 54, 1 | rabexd 5340 |
. . . . . . . . . . . 12
⊢ (𝜑 → {𝑠 ∈ 𝑆 ∣ {𝑥 ∈ dom (𝐹‘𝑚) ∣ ((𝐹‘𝑚)‘𝑥) < (𝐴 + (1 / 𝑘))} = (𝑠 ∩ dom (𝐹‘𝑚))} ∈ V) |
| 56 | 53, 55 | syl 17 |
. . . . . . . . . . 11
⊢ ((𝜑 ∧ 𝑘 ∈ ℕ ∧ 𝑚 ∈ 𝑍) → {𝑠 ∈ 𝑆 ∣ {𝑥 ∈ dom (𝐹‘𝑚) ∣ ((𝐹‘𝑚)‘𝑥) < (𝐴 + (1 / 𝑘))} = (𝑠 ∩ dom (𝐹‘𝑚))} ∈ V) |
| 57 | | smflimlem1.4 |
. . . . . . . . . . . 12
⊢ 𝑃 = (𝑚 ∈ 𝑍, 𝑘 ∈ ℕ ↦ {𝑠 ∈ 𝑆 ∣ {𝑥 ∈ dom (𝐹‘𝑚) ∣ ((𝐹‘𝑚)‘𝑥) < (𝐴 + (1 / 𝑘))} = (𝑠 ∩ dom (𝐹‘𝑚))}) |
| 58 | 57 | ovmpt4g 7580 |
. . . . . . . . . . 11
⊢ ((𝑚 ∈ 𝑍 ∧ 𝑘 ∈ ℕ ∧ {𝑠 ∈ 𝑆 ∣ {𝑥 ∈ dom (𝐹‘𝑚) ∣ ((𝐹‘𝑚)‘𝑥) < (𝐴 + (1 / 𝑘))} = (𝑠 ∩ dom (𝐹‘𝑚))} ∈ V) → (𝑚𝑃𝑘) = {𝑠 ∈ 𝑆 ∣ {𝑥 ∈ dom (𝐹‘𝑚) ∣ ((𝐹‘𝑚)‘𝑥) < (𝐴 + (1 / 𝑘))} = (𝑠 ∩ dom (𝐹‘𝑚))}) |
| 59 | 46, 47, 56, 58 | syl3anc 1373 |
. . . . . . . . . 10
⊢ ((𝜑 ∧ 𝑘 ∈ ℕ ∧ 𝑚 ∈ 𝑍) → (𝑚𝑃𝑘) = {𝑠 ∈ 𝑆 ∣ {𝑥 ∈ dom (𝐹‘𝑚) ∣ ((𝐹‘𝑚)‘𝑥) < (𝐴 + (1 / 𝑘))} = (𝑠 ∩ dom (𝐹‘𝑚))}) |
| 60 | | ssrab2 4080 |
. . . . . . . . . 10
⊢ {𝑠 ∈ 𝑆 ∣ {𝑥 ∈ dom (𝐹‘𝑚) ∣ ((𝐹‘𝑚)‘𝑥) < (𝐴 + (1 / 𝑘))} = (𝑠 ∩ dom (𝐹‘𝑚))} ⊆ 𝑆 |
| 61 | 59, 60 | eqsstrdi 4028 |
. . . . . . . . 9
⊢ ((𝜑 ∧ 𝑘 ∈ ℕ ∧ 𝑚 ∈ 𝑍) → (𝑚𝑃𝑘) ⊆ 𝑆) |
| 62 | 55 | ralrimivw 3150 |
. . . . . . . . . . . . 13
⊢ (𝜑 → ∀𝑘 ∈ ℕ {𝑠 ∈ 𝑆 ∣ {𝑥 ∈ dom (𝐹‘𝑚) ∣ ((𝐹‘𝑚)‘𝑥) < (𝐴 + (1 / 𝑘))} = (𝑠 ∩ dom (𝐹‘𝑚))} ∈ V) |
| 63 | 62 | ralrimivw 3150 |
. . . . . . . . . . . 12
⊢ (𝜑 → ∀𝑚 ∈ 𝑍 ∀𝑘 ∈ ℕ {𝑠 ∈ 𝑆 ∣ {𝑥 ∈ dom (𝐹‘𝑚) ∣ ((𝐹‘𝑚)‘𝑥) < (𝐴 + (1 / 𝑘))} = (𝑠 ∩ dom (𝐹‘𝑚))} ∈ V) |
| 64 | 63 | 3ad2ant1 1134 |
. . . . . . . . . . 11
⊢ ((𝜑 ∧ 𝑘 ∈ ℕ ∧ 𝑚 ∈ 𝑍) → ∀𝑚 ∈ 𝑍 ∀𝑘 ∈ ℕ {𝑠 ∈ 𝑆 ∣ {𝑥 ∈ dom (𝐹‘𝑚) ∣ ((𝐹‘𝑚)‘𝑥) < (𝐴 + (1 / 𝑘))} = (𝑠 ∩ dom (𝐹‘𝑚))} ∈ V) |
| 65 | 57 | elrnmpoid 45233 |
. . . . . . . . . . 11
⊢ ((𝑚 ∈ 𝑍 ∧ 𝑘 ∈ ℕ ∧ ∀𝑚 ∈ 𝑍 ∀𝑘 ∈ ℕ {𝑠 ∈ 𝑆 ∣ {𝑥 ∈ dom (𝐹‘𝑚) ∣ ((𝐹‘𝑚)‘𝑥) < (𝐴 + (1 / 𝑘))} = (𝑠 ∩ dom (𝐹‘𝑚))} ∈ V) → (𝑚𝑃𝑘) ∈ ran 𝑃) |
| 66 | 46, 47, 64, 65 | syl3anc 1373 |
. . . . . . . . . 10
⊢ ((𝜑 ∧ 𝑘 ∈ ℕ ∧ 𝑚 ∈ 𝑍) → (𝑚𝑃𝑘) ∈ ran 𝑃) |
| 67 | | ovex 7464 |
. . . . . . . . . . 11
⊢ (𝑚𝑃𝑘) ∈ V |
| 68 | | eleq1 2829 |
. . . . . . . . . . . . 13
⊢ (𝑟 = (𝑚𝑃𝑘) → (𝑟 ∈ ran 𝑃 ↔ (𝑚𝑃𝑘) ∈ ran 𝑃)) |
| 69 | 68 | anbi2d 630 |
. . . . . . . . . . . 12
⊢ (𝑟 = (𝑚𝑃𝑘) → ((𝜑 ∧ 𝑟 ∈ ran 𝑃) ↔ (𝜑 ∧ (𝑚𝑃𝑘) ∈ ran 𝑃))) |
| 70 | | fveq2 6906 |
. . . . . . . . . . . . 13
⊢ (𝑟 = (𝑚𝑃𝑘) → (𝐶‘𝑟) = (𝐶‘(𝑚𝑃𝑘))) |
| 71 | | id 22 |
. . . . . . . . . . . . 13
⊢ (𝑟 = (𝑚𝑃𝑘) → 𝑟 = (𝑚𝑃𝑘)) |
| 72 | 70, 71 | eleq12d 2835 |
. . . . . . . . . . . 12
⊢ (𝑟 = (𝑚𝑃𝑘) → ((𝐶‘𝑟) ∈ 𝑟 ↔ (𝐶‘(𝑚𝑃𝑘)) ∈ (𝑚𝑃𝑘))) |
| 73 | 69, 72 | imbi12d 344 |
. . . . . . . . . . 11
⊢ (𝑟 = (𝑚𝑃𝑘) → (((𝜑 ∧ 𝑟 ∈ ran 𝑃) → (𝐶‘𝑟) ∈ 𝑟) ↔ ((𝜑 ∧ (𝑚𝑃𝑘) ∈ ran 𝑃) → (𝐶‘(𝑚𝑃𝑘)) ∈ (𝑚𝑃𝑘)))) |
| 74 | | smflimlem1.7 |
. . . . . . . . . . 11
⊢ ((𝜑 ∧ 𝑟 ∈ ran 𝑃) → (𝐶‘𝑟) ∈ 𝑟) |
| 75 | 67, 73, 74 | vtocl 3558 |
. . . . . . . . . 10
⊢ ((𝜑 ∧ (𝑚𝑃𝑘) ∈ ran 𝑃) → (𝐶‘(𝑚𝑃𝑘)) ∈ (𝑚𝑃𝑘)) |
| 76 | 53, 66, 75 | syl2anc 584 |
. . . . . . . . 9
⊢ ((𝜑 ∧ 𝑘 ∈ ℕ ∧ 𝑚 ∈ 𝑍) → (𝐶‘(𝑚𝑃𝑘)) ∈ (𝑚𝑃𝑘)) |
| 77 | 61, 76 | sseldd 3984 |
. . . . . . . 8
⊢ ((𝜑 ∧ 𝑘 ∈ ℕ ∧ 𝑚 ∈ 𝑍) → (𝐶‘(𝑚𝑃𝑘)) ∈ 𝑆) |
| 78 | 52, 77 | eqeltrd 2841 |
. . . . . . 7
⊢ ((𝜑 ∧ 𝑘 ∈ ℕ ∧ 𝑚 ∈ 𝑍) → (𝑚𝐻𝑘) ∈ 𝑆) |
| 79 | 39, 41, 45, 78 | syl3anc 1373 |
. . . . . 6
⊢ ((((𝜑 ∧ 𝑘 ∈ ℕ) ∧ 𝑛 ∈ 𝑍) ∧ 𝑚 ∈ (ℤ≥‘𝑛)) → (𝑚𝐻𝑘) ∈ 𝑆) |
| 80 | 33, 36, 37, 79 | saliincl 46342 |
. . . . 5
⊢ (((𝜑 ∧ 𝑘 ∈ ℕ) ∧ 𝑛 ∈ 𝑍) → ∩
𝑚 ∈
(ℤ≥‘𝑛)(𝑚𝐻𝑘) ∈ 𝑆) |
| 81 | 30, 32, 80 | saliuncl 46338 |
. . . 4
⊢ ((𝜑 ∧ 𝑘 ∈ ℕ) → ∪ 𝑛 ∈ 𝑍 ∩ 𝑚 ∈
(ℤ≥‘𝑛)(𝑚𝐻𝑘) ∈ 𝑆) |
| 82 | 1, 27, 29, 81 | saliincl 46342 |
. . 3
⊢ (𝜑 → ∩ 𝑘 ∈ ℕ ∪ 𝑛 ∈ 𝑍 ∩ 𝑚 ∈
(ℤ≥‘𝑛)(𝑚𝐻𝑘) ∈ 𝑆) |
| 83 | 25, 82 | eqeltrid 2845 |
. 2
⊢ (𝜑 → 𝐼 ∈ 𝑆) |
| 84 | | incom 4209 |
. 2
⊢ (𝐷 ∩ 𝐼) = (𝐼 ∩ 𝐷) |
| 85 | 1, 24, 83, 84 | elrestd 45113 |
1
⊢ (𝜑 → (𝐷 ∩ 𝐼) ∈ (𝑆 ↾t 𝐷)) |