Step | Hyp | Ref
| Expression |
1 | | fiunelros.2 |
. 2
⊢ (𝜑 → 𝑁 ∈ ℕ) |
2 | | simpr 488 |
. . . . 5
⊢ ((𝜑 ∧ 𝑁 ∈ ℕ) → 𝑁 ∈ ℕ) |
3 | 2 | nnred 11845 |
. . . 4
⊢ ((𝜑 ∧ 𝑁 ∈ ℕ) → 𝑁 ∈ ℝ) |
4 | 3 | leidd 11398 |
. . 3
⊢ ((𝜑 ∧ 𝑁 ∈ ℕ) → 𝑁 ≤ 𝑁) |
5 | | breq1 5056 |
. . . . 5
⊢ (𝑛 = 1 → (𝑛 ≤ 𝑁 ↔ 1 ≤ 𝑁)) |
6 | | oveq2 7221 |
. . . . . . 7
⊢ (𝑛 = 1 → (1..^𝑛) = (1..^1)) |
7 | 6 | iuneq1d 4931 |
. . . . . 6
⊢ (𝑛 = 1 → ∪ 𝑘 ∈ (1..^𝑛)𝐵 = ∪ 𝑘 ∈ (1..^1)𝐵) |
8 | 7 | eleq1d 2822 |
. . . . 5
⊢ (𝑛 = 1 → (∪ 𝑘 ∈ (1..^𝑛)𝐵 ∈ 𝑆 ↔ ∪
𝑘 ∈ (1..^1)𝐵 ∈ 𝑆)) |
9 | 5, 8 | imbi12d 348 |
. . . 4
⊢ (𝑛 = 1 → ((𝑛 ≤ 𝑁 → ∪
𝑘 ∈ (1..^𝑛)𝐵 ∈ 𝑆) ↔ (1 ≤ 𝑁 → ∪
𝑘 ∈ (1..^1)𝐵 ∈ 𝑆))) |
10 | | breq1 5056 |
. . . . 5
⊢ (𝑛 = 𝑖 → (𝑛 ≤ 𝑁 ↔ 𝑖 ≤ 𝑁)) |
11 | | oveq2 7221 |
. . . . . . 7
⊢ (𝑛 = 𝑖 → (1..^𝑛) = (1..^𝑖)) |
12 | 11 | iuneq1d 4931 |
. . . . . 6
⊢ (𝑛 = 𝑖 → ∪
𝑘 ∈ (1..^𝑛)𝐵 = ∪ 𝑘 ∈ (1..^𝑖)𝐵) |
13 | 12 | eleq1d 2822 |
. . . . 5
⊢ (𝑛 = 𝑖 → (∪
𝑘 ∈ (1..^𝑛)𝐵 ∈ 𝑆 ↔ ∪
𝑘 ∈ (1..^𝑖)𝐵 ∈ 𝑆)) |
14 | 10, 13 | imbi12d 348 |
. . . 4
⊢ (𝑛 = 𝑖 → ((𝑛 ≤ 𝑁 → ∪
𝑘 ∈ (1..^𝑛)𝐵 ∈ 𝑆) ↔ (𝑖 ≤ 𝑁 → ∪
𝑘 ∈ (1..^𝑖)𝐵 ∈ 𝑆))) |
15 | | breq1 5056 |
. . . . 5
⊢ (𝑛 = (𝑖 + 1) → (𝑛 ≤ 𝑁 ↔ (𝑖 + 1) ≤ 𝑁)) |
16 | | oveq2 7221 |
. . . . . . 7
⊢ (𝑛 = (𝑖 + 1) → (1..^𝑛) = (1..^(𝑖 + 1))) |
17 | 16 | iuneq1d 4931 |
. . . . . 6
⊢ (𝑛 = (𝑖 + 1) → ∪ 𝑘 ∈ (1..^𝑛)𝐵 = ∪ 𝑘 ∈ (1..^(𝑖 + 1))𝐵) |
18 | 17 | eleq1d 2822 |
. . . . 5
⊢ (𝑛 = (𝑖 + 1) → (∪ 𝑘 ∈ (1..^𝑛)𝐵 ∈ 𝑆 ↔ ∪
𝑘 ∈ (1..^(𝑖 + 1))𝐵 ∈ 𝑆)) |
19 | 15, 18 | imbi12d 348 |
. . . 4
⊢ (𝑛 = (𝑖 + 1) → ((𝑛 ≤ 𝑁 → ∪
𝑘 ∈ (1..^𝑛)𝐵 ∈ 𝑆) ↔ ((𝑖 + 1) ≤ 𝑁 → ∪
𝑘 ∈ (1..^(𝑖 + 1))𝐵 ∈ 𝑆))) |
20 | | breq1 5056 |
. . . . 5
⊢ (𝑛 = 𝑁 → (𝑛 ≤ 𝑁 ↔ 𝑁 ≤ 𝑁)) |
21 | | oveq2 7221 |
. . . . . . 7
⊢ (𝑛 = 𝑁 → (1..^𝑛) = (1..^𝑁)) |
22 | 21 | iuneq1d 4931 |
. . . . . 6
⊢ (𝑛 = 𝑁 → ∪
𝑘 ∈ (1..^𝑛)𝐵 = ∪ 𝑘 ∈ (1..^𝑁)𝐵) |
23 | 22 | eleq1d 2822 |
. . . . 5
⊢ (𝑛 = 𝑁 → (∪
𝑘 ∈ (1..^𝑛)𝐵 ∈ 𝑆 ↔ ∪
𝑘 ∈ (1..^𝑁)𝐵 ∈ 𝑆)) |
24 | 20, 23 | imbi12d 348 |
. . . 4
⊢ (𝑛 = 𝑁 → ((𝑛 ≤ 𝑁 → ∪
𝑘 ∈ (1..^𝑛)𝐵 ∈ 𝑆) ↔ (𝑁 ≤ 𝑁 → ∪
𝑘 ∈ (1..^𝑁)𝐵 ∈ 𝑆))) |
25 | | fzo0 13266 |
. . . . . . . 8
⊢ (1..^1) =
∅ |
26 | | iuneq1 4920 |
. . . . . . . 8
⊢ ((1..^1)
= ∅ → ∪ 𝑘 ∈ (1..^1)𝐵 = ∪ 𝑘 ∈ ∅ 𝐵) |
27 | 25, 26 | ax-mp 5 |
. . . . . . 7
⊢ ∪ 𝑘 ∈ (1..^1)𝐵 = ∪ 𝑘 ∈ ∅ 𝐵 |
28 | | 0iun 4971 |
. . . . . . 7
⊢ ∪ 𝑘 ∈ ∅ 𝐵 = ∅ |
29 | 27, 28 | eqtri 2765 |
. . . . . 6
⊢ ∪ 𝑘 ∈ (1..^1)𝐵 = ∅ |
30 | | fiunelros.1 |
. . . . . . 7
⊢ (𝜑 → 𝑆 ∈ 𝑄) |
31 | | isros.1 |
. . . . . . . 8
⊢ 𝑄 = {𝑠 ∈ 𝒫 𝒫 𝑂 ∣ (∅ ∈ 𝑠 ∧ ∀𝑥 ∈ 𝑠 ∀𝑦 ∈ 𝑠 ((𝑥 ∪ 𝑦) ∈ 𝑠 ∧ (𝑥 ∖ 𝑦) ∈ 𝑠))} |
32 | 31 | 0elros 31850 |
. . . . . . 7
⊢ (𝑆 ∈ 𝑄 → ∅ ∈ 𝑆) |
33 | 30, 32 | syl 17 |
. . . . . 6
⊢ (𝜑 → ∅ ∈ 𝑆) |
34 | 29, 33 | eqeltrid 2842 |
. . . . 5
⊢ (𝜑 → ∪ 𝑘 ∈ (1..^1)𝐵 ∈ 𝑆) |
35 | 34 | a1d 25 |
. . . 4
⊢ (𝜑 → (1 ≤ 𝑁 → ∪
𝑘 ∈ (1..^1)𝐵 ∈ 𝑆)) |
36 | | simpllr 776 |
. . . . . . . 8
⊢ ((((𝜑 ∧ 𝑖 ∈ ℕ) ∧ (𝑖 ≤ 𝑁 → ∪
𝑘 ∈ (1..^𝑖)𝐵 ∈ 𝑆)) ∧ (𝑖 + 1) ≤ 𝑁) → 𝑖 ∈ ℕ) |
37 | | fzosplitsn 13350 |
. . . . . . . . . 10
⊢ (𝑖 ∈
(ℤ≥‘1) → (1..^(𝑖 + 1)) = ((1..^𝑖) ∪ {𝑖})) |
38 | | nnuz 12477 |
. . . . . . . . . 10
⊢ ℕ =
(ℤ≥‘1) |
39 | 37, 38 | eleq2s 2856 |
. . . . . . . . 9
⊢ (𝑖 ∈ ℕ →
(1..^(𝑖 + 1)) = ((1..^𝑖) ∪ {𝑖})) |
40 | 39 | iuneq1d 4931 |
. . . . . . . 8
⊢ (𝑖 ∈ ℕ → ∪ 𝑘 ∈ (1..^(𝑖 + 1))𝐵 = ∪ 𝑘 ∈ ((1..^𝑖) ∪ {𝑖})𝐵) |
41 | 36, 40 | syl 17 |
. . . . . . 7
⊢ ((((𝜑 ∧ 𝑖 ∈ ℕ) ∧ (𝑖 ≤ 𝑁 → ∪
𝑘 ∈ (1..^𝑖)𝐵 ∈ 𝑆)) ∧ (𝑖 + 1) ≤ 𝑁) → ∪
𝑘 ∈ (1..^(𝑖 + 1))𝐵 = ∪ 𝑘 ∈ ((1..^𝑖) ∪ {𝑖})𝐵) |
42 | | iunxun 5002 |
. . . . . . 7
⊢ ∪ 𝑘 ∈ ((1..^𝑖) ∪ {𝑖})𝐵 = (∪
𝑘 ∈ (1..^𝑖)𝐵 ∪ ∪
𝑘 ∈ {𝑖}𝐵) |
43 | 41, 42 | eqtrdi 2794 |
. . . . . 6
⊢ ((((𝜑 ∧ 𝑖 ∈ ℕ) ∧ (𝑖 ≤ 𝑁 → ∪
𝑘 ∈ (1..^𝑖)𝐵 ∈ 𝑆)) ∧ (𝑖 + 1) ≤ 𝑁) → ∪
𝑘 ∈ (1..^(𝑖 + 1))𝐵 = (∪
𝑘 ∈ (1..^𝑖)𝐵 ∪ ∪
𝑘 ∈ {𝑖}𝐵)) |
44 | 30 | ad3antrrr 730 |
. . . . . . 7
⊢ ((((𝜑 ∧ 𝑖 ∈ ℕ) ∧ (𝑖 ≤ 𝑁 → ∪
𝑘 ∈ (1..^𝑖)𝐵 ∈ 𝑆)) ∧ (𝑖 + 1) ≤ 𝑁) → 𝑆 ∈ 𝑄) |
45 | 36 | nnred 11845 |
. . . . . . . . 9
⊢ ((((𝜑 ∧ 𝑖 ∈ ℕ) ∧ (𝑖 ≤ 𝑁 → ∪
𝑘 ∈ (1..^𝑖)𝐵 ∈ 𝑆)) ∧ (𝑖 + 1) ≤ 𝑁) → 𝑖 ∈ ℝ) |
46 | 1 | ad3antrrr 730 |
. . . . . . . . . 10
⊢ ((((𝜑 ∧ 𝑖 ∈ ℕ) ∧ (𝑖 ≤ 𝑁 → ∪
𝑘 ∈ (1..^𝑖)𝐵 ∈ 𝑆)) ∧ (𝑖 + 1) ≤ 𝑁) → 𝑁 ∈ ℕ) |
47 | 46 | nnred 11845 |
. . . . . . . . 9
⊢ ((((𝜑 ∧ 𝑖 ∈ ℕ) ∧ (𝑖 ≤ 𝑁 → ∪
𝑘 ∈ (1..^𝑖)𝐵 ∈ 𝑆)) ∧ (𝑖 + 1) ≤ 𝑁) → 𝑁 ∈ ℝ) |
48 | | simpr 488 |
. . . . . . . . . 10
⊢ ((((𝜑 ∧ 𝑖 ∈ ℕ) ∧ (𝑖 ≤ 𝑁 → ∪
𝑘 ∈ (1..^𝑖)𝐵 ∈ 𝑆)) ∧ (𝑖 + 1) ≤ 𝑁) → (𝑖 + 1) ≤ 𝑁) |
49 | | nnltp1le 12233 |
. . . . . . . . . . 11
⊢ ((𝑖 ∈ ℕ ∧ 𝑁 ∈ ℕ) → (𝑖 < 𝑁 ↔ (𝑖 + 1) ≤ 𝑁)) |
50 | 36, 46, 49 | syl2anc 587 |
. . . . . . . . . 10
⊢ ((((𝜑 ∧ 𝑖 ∈ ℕ) ∧ (𝑖 ≤ 𝑁 → ∪
𝑘 ∈ (1..^𝑖)𝐵 ∈ 𝑆)) ∧ (𝑖 + 1) ≤ 𝑁) → (𝑖 < 𝑁 ↔ (𝑖 + 1) ≤ 𝑁)) |
51 | 48, 50 | mpbird 260 |
. . . . . . . . 9
⊢ ((((𝜑 ∧ 𝑖 ∈ ℕ) ∧ (𝑖 ≤ 𝑁 → ∪
𝑘 ∈ (1..^𝑖)𝐵 ∈ 𝑆)) ∧ (𝑖 + 1) ≤ 𝑁) → 𝑖 < 𝑁) |
52 | 45, 47, 51 | ltled 10980 |
. . . . . . . 8
⊢ ((((𝜑 ∧ 𝑖 ∈ ℕ) ∧ (𝑖 ≤ 𝑁 → ∪
𝑘 ∈ (1..^𝑖)𝐵 ∈ 𝑆)) ∧ (𝑖 + 1) ≤ 𝑁) → 𝑖 ≤ 𝑁) |
53 | | simplr 769 |
. . . . . . . 8
⊢ ((((𝜑 ∧ 𝑖 ∈ ℕ) ∧ (𝑖 ≤ 𝑁 → ∪
𝑘 ∈ (1..^𝑖)𝐵 ∈ 𝑆)) ∧ (𝑖 + 1) ≤ 𝑁) → (𝑖 ≤ 𝑁 → ∪
𝑘 ∈ (1..^𝑖)𝐵 ∈ 𝑆)) |
54 | 52, 53 | mpd 15 |
. . . . . . 7
⊢ ((((𝜑 ∧ 𝑖 ∈ ℕ) ∧ (𝑖 ≤ 𝑁 → ∪
𝑘 ∈ (1..^𝑖)𝐵 ∈ 𝑆)) ∧ (𝑖 + 1) ≤ 𝑁) → ∪
𝑘 ∈ (1..^𝑖)𝐵 ∈ 𝑆) |
55 | | nfcsb1v 3836 |
. . . . . . . . . 10
⊢
Ⅎ𝑘⦋𝑖 / 𝑘⦌𝐵 |
56 | | csbeq1a 3825 |
. . . . . . . . . 10
⊢ (𝑘 = 𝑖 → 𝐵 = ⦋𝑖 / 𝑘⦌𝐵) |
57 | 55, 56 | iunxsngf 5000 |
. . . . . . . . 9
⊢ (𝑖 ∈ ℕ → ∪ 𝑘 ∈ {𝑖}𝐵 = ⦋𝑖 / 𝑘⦌𝐵) |
58 | 36, 57 | syl 17 |
. . . . . . . 8
⊢ ((((𝜑 ∧ 𝑖 ∈ ℕ) ∧ (𝑖 ≤ 𝑁 → ∪
𝑘 ∈ (1..^𝑖)𝐵 ∈ 𝑆)) ∧ (𝑖 + 1) ≤ 𝑁) → ∪
𝑘 ∈ {𝑖}𝐵 = ⦋𝑖 / 𝑘⦌𝐵) |
59 | | simplll 775 |
. . . . . . . . 9
⊢ ((((𝜑 ∧ 𝑖 ∈ ℕ) ∧ (𝑖 ≤ 𝑁 → ∪
𝑘 ∈ (1..^𝑖)𝐵 ∈ 𝑆)) ∧ (𝑖 + 1) ≤ 𝑁) → 𝜑) |
60 | | elfzo1 13292 |
. . . . . . . . . 10
⊢ (𝑖 ∈ (1..^𝑁) ↔ (𝑖 ∈ ℕ ∧ 𝑁 ∈ ℕ ∧ 𝑖 < 𝑁)) |
61 | 36, 46, 51, 60 | syl3anbrc 1345 |
. . . . . . . . 9
⊢ ((((𝜑 ∧ 𝑖 ∈ ℕ) ∧ (𝑖 ≤ 𝑁 → ∪
𝑘 ∈ (1..^𝑖)𝐵 ∈ 𝑆)) ∧ (𝑖 + 1) ≤ 𝑁) → 𝑖 ∈ (1..^𝑁)) |
62 | | nfv 1922 |
. . . . . . . . . . 11
⊢
Ⅎ𝑘(𝜑 ∧ 𝑖 ∈ (1..^𝑁)) |
63 | | nfcv 2904 |
. . . . . . . . . . . 12
⊢
Ⅎ𝑘𝑆 |
64 | 55, 63 | nfel 2918 |
. . . . . . . . . . 11
⊢
Ⅎ𝑘⦋𝑖 / 𝑘⦌𝐵 ∈ 𝑆 |
65 | 62, 64 | nfim 1904 |
. . . . . . . . . 10
⊢
Ⅎ𝑘((𝜑 ∧ 𝑖 ∈ (1..^𝑁)) → ⦋𝑖 / 𝑘⦌𝐵 ∈ 𝑆) |
66 | | eleq1w 2820 |
. . . . . . . . . . . 12
⊢ (𝑘 = 𝑖 → (𝑘 ∈ (1..^𝑁) ↔ 𝑖 ∈ (1..^𝑁))) |
67 | 66 | anbi2d 632 |
. . . . . . . . . . 11
⊢ (𝑘 = 𝑖 → ((𝜑 ∧ 𝑘 ∈ (1..^𝑁)) ↔ (𝜑 ∧ 𝑖 ∈ (1..^𝑁)))) |
68 | 56 | eleq1d 2822 |
. . . . . . . . . . 11
⊢ (𝑘 = 𝑖 → (𝐵 ∈ 𝑆 ↔ ⦋𝑖 / 𝑘⦌𝐵 ∈ 𝑆)) |
69 | 67, 68 | imbi12d 348 |
. . . . . . . . . 10
⊢ (𝑘 = 𝑖 → (((𝜑 ∧ 𝑘 ∈ (1..^𝑁)) → 𝐵 ∈ 𝑆) ↔ ((𝜑 ∧ 𝑖 ∈ (1..^𝑁)) → ⦋𝑖 / 𝑘⦌𝐵 ∈ 𝑆))) |
70 | | fiunelros.3 |
. . . . . . . . . 10
⊢ ((𝜑 ∧ 𝑘 ∈ (1..^𝑁)) → 𝐵 ∈ 𝑆) |
71 | 65, 69, 70 | chvarfv 2238 |
. . . . . . . . 9
⊢ ((𝜑 ∧ 𝑖 ∈ (1..^𝑁)) → ⦋𝑖 / 𝑘⦌𝐵 ∈ 𝑆) |
72 | 59, 61, 71 | syl2anc 587 |
. . . . . . . 8
⊢ ((((𝜑 ∧ 𝑖 ∈ ℕ) ∧ (𝑖 ≤ 𝑁 → ∪
𝑘 ∈ (1..^𝑖)𝐵 ∈ 𝑆)) ∧ (𝑖 + 1) ≤ 𝑁) → ⦋𝑖 / 𝑘⦌𝐵 ∈ 𝑆) |
73 | 58, 72 | eqeltrd 2838 |
. . . . . . 7
⊢ ((((𝜑 ∧ 𝑖 ∈ ℕ) ∧ (𝑖 ≤ 𝑁 → ∪
𝑘 ∈ (1..^𝑖)𝐵 ∈ 𝑆)) ∧ (𝑖 + 1) ≤ 𝑁) → ∪
𝑘 ∈ {𝑖}𝐵 ∈ 𝑆) |
74 | 31 | unelros 31851 |
. . . . . . 7
⊢ ((𝑆 ∈ 𝑄 ∧ ∪
𝑘 ∈ (1..^𝑖)𝐵 ∈ 𝑆 ∧ ∪
𝑘 ∈ {𝑖}𝐵 ∈ 𝑆) → (∪ 𝑘 ∈ (1..^𝑖)𝐵 ∪ ∪
𝑘 ∈ {𝑖}𝐵) ∈ 𝑆) |
75 | 44, 54, 73, 74 | syl3anc 1373 |
. . . . . 6
⊢ ((((𝜑 ∧ 𝑖 ∈ ℕ) ∧ (𝑖 ≤ 𝑁 → ∪
𝑘 ∈ (1..^𝑖)𝐵 ∈ 𝑆)) ∧ (𝑖 + 1) ≤ 𝑁) → (∪ 𝑘 ∈ (1..^𝑖)𝐵 ∪ ∪
𝑘 ∈ {𝑖}𝐵) ∈ 𝑆) |
76 | 43, 75 | eqeltrd 2838 |
. . . . 5
⊢ ((((𝜑 ∧ 𝑖 ∈ ℕ) ∧ (𝑖 ≤ 𝑁 → ∪
𝑘 ∈ (1..^𝑖)𝐵 ∈ 𝑆)) ∧ (𝑖 + 1) ≤ 𝑁) → ∪
𝑘 ∈ (1..^(𝑖 + 1))𝐵 ∈ 𝑆) |
77 | 76 | ex 416 |
. . . 4
⊢ (((𝜑 ∧ 𝑖 ∈ ℕ) ∧ (𝑖 ≤ 𝑁 → ∪
𝑘 ∈ (1..^𝑖)𝐵 ∈ 𝑆)) → ((𝑖 + 1) ≤ 𝑁 → ∪
𝑘 ∈ (1..^(𝑖 + 1))𝐵 ∈ 𝑆)) |
78 | 9, 14, 19, 24, 35, 77 | nnindd 11850 |
. . 3
⊢ ((𝜑 ∧ 𝑁 ∈ ℕ) → (𝑁 ≤ 𝑁 → ∪
𝑘 ∈ (1..^𝑁)𝐵 ∈ 𝑆)) |
79 | 4, 78 | mpd 15 |
. 2
⊢ ((𝜑 ∧ 𝑁 ∈ ℕ) → ∪ 𝑘 ∈ (1..^𝑁)𝐵 ∈ 𝑆) |
80 | 1, 79 | mpdan 687 |
1
⊢ (𝜑 → ∪ 𝑘 ∈ (1..^𝑁)𝐵 ∈ 𝑆) |