| Step | Hyp | Ref
| Expression |
| 1 | | fiunelros.2 |
. 2
⊢ (𝜑 → 𝑁 ∈ ℕ) |
| 2 | | simpr 484 |
. . . . 5
⊢ ((𝜑 ∧ 𝑁 ∈ ℕ) → 𝑁 ∈ ℕ) |
| 3 | 2 | nnred 12281 |
. . . 4
⊢ ((𝜑 ∧ 𝑁 ∈ ℕ) → 𝑁 ∈ ℝ) |
| 4 | 3 | leidd 11829 |
. . 3
⊢ ((𝜑 ∧ 𝑁 ∈ ℕ) → 𝑁 ≤ 𝑁) |
| 5 | | breq1 5146 |
. . . . 5
⊢ (𝑛 = 1 → (𝑛 ≤ 𝑁 ↔ 1 ≤ 𝑁)) |
| 6 | | oveq2 7439 |
. . . . . . 7
⊢ (𝑛 = 1 → (1..^𝑛) = (1..^1)) |
| 7 | 6 | iuneq1d 5019 |
. . . . . 6
⊢ (𝑛 = 1 → ∪ 𝑘 ∈ (1..^𝑛)𝐵 = ∪ 𝑘 ∈ (1..^1)𝐵) |
| 8 | 7 | eleq1d 2826 |
. . . . 5
⊢ (𝑛 = 1 → (∪ 𝑘 ∈ (1..^𝑛)𝐵 ∈ 𝑆 ↔ ∪
𝑘 ∈ (1..^1)𝐵 ∈ 𝑆)) |
| 9 | 5, 8 | imbi12d 344 |
. . . 4
⊢ (𝑛 = 1 → ((𝑛 ≤ 𝑁 → ∪
𝑘 ∈ (1..^𝑛)𝐵 ∈ 𝑆) ↔ (1 ≤ 𝑁 → ∪
𝑘 ∈ (1..^1)𝐵 ∈ 𝑆))) |
| 10 | | breq1 5146 |
. . . . 5
⊢ (𝑛 = 𝑖 → (𝑛 ≤ 𝑁 ↔ 𝑖 ≤ 𝑁)) |
| 11 | | oveq2 7439 |
. . . . . . 7
⊢ (𝑛 = 𝑖 → (1..^𝑛) = (1..^𝑖)) |
| 12 | 11 | iuneq1d 5019 |
. . . . . 6
⊢ (𝑛 = 𝑖 → ∪
𝑘 ∈ (1..^𝑛)𝐵 = ∪ 𝑘 ∈ (1..^𝑖)𝐵) |
| 13 | 12 | eleq1d 2826 |
. . . . 5
⊢ (𝑛 = 𝑖 → (∪
𝑘 ∈ (1..^𝑛)𝐵 ∈ 𝑆 ↔ ∪
𝑘 ∈ (1..^𝑖)𝐵 ∈ 𝑆)) |
| 14 | 10, 13 | imbi12d 344 |
. . . 4
⊢ (𝑛 = 𝑖 → ((𝑛 ≤ 𝑁 → ∪
𝑘 ∈ (1..^𝑛)𝐵 ∈ 𝑆) ↔ (𝑖 ≤ 𝑁 → ∪
𝑘 ∈ (1..^𝑖)𝐵 ∈ 𝑆))) |
| 15 | | breq1 5146 |
. . . . 5
⊢ (𝑛 = (𝑖 + 1) → (𝑛 ≤ 𝑁 ↔ (𝑖 + 1) ≤ 𝑁)) |
| 16 | | oveq2 7439 |
. . . . . . 7
⊢ (𝑛 = (𝑖 + 1) → (1..^𝑛) = (1..^(𝑖 + 1))) |
| 17 | 16 | iuneq1d 5019 |
. . . . . 6
⊢ (𝑛 = (𝑖 + 1) → ∪ 𝑘 ∈ (1..^𝑛)𝐵 = ∪ 𝑘 ∈ (1..^(𝑖 + 1))𝐵) |
| 18 | 17 | eleq1d 2826 |
. . . . 5
⊢ (𝑛 = (𝑖 + 1) → (∪ 𝑘 ∈ (1..^𝑛)𝐵 ∈ 𝑆 ↔ ∪
𝑘 ∈ (1..^(𝑖 + 1))𝐵 ∈ 𝑆)) |
| 19 | 15, 18 | imbi12d 344 |
. . . 4
⊢ (𝑛 = (𝑖 + 1) → ((𝑛 ≤ 𝑁 → ∪
𝑘 ∈ (1..^𝑛)𝐵 ∈ 𝑆) ↔ ((𝑖 + 1) ≤ 𝑁 → ∪
𝑘 ∈ (1..^(𝑖 + 1))𝐵 ∈ 𝑆))) |
| 20 | | breq1 5146 |
. . . . 5
⊢ (𝑛 = 𝑁 → (𝑛 ≤ 𝑁 ↔ 𝑁 ≤ 𝑁)) |
| 21 | | oveq2 7439 |
. . . . . . 7
⊢ (𝑛 = 𝑁 → (1..^𝑛) = (1..^𝑁)) |
| 22 | 21 | iuneq1d 5019 |
. . . . . 6
⊢ (𝑛 = 𝑁 → ∪
𝑘 ∈ (1..^𝑛)𝐵 = ∪ 𝑘 ∈ (1..^𝑁)𝐵) |
| 23 | 22 | eleq1d 2826 |
. . . . 5
⊢ (𝑛 = 𝑁 → (∪
𝑘 ∈ (1..^𝑛)𝐵 ∈ 𝑆 ↔ ∪
𝑘 ∈ (1..^𝑁)𝐵 ∈ 𝑆)) |
| 24 | 20, 23 | imbi12d 344 |
. . . 4
⊢ (𝑛 = 𝑁 → ((𝑛 ≤ 𝑁 → ∪
𝑘 ∈ (1..^𝑛)𝐵 ∈ 𝑆) ↔ (𝑁 ≤ 𝑁 → ∪
𝑘 ∈ (1..^𝑁)𝐵 ∈ 𝑆))) |
| 25 | | fzo0 13723 |
. . . . . . . 8
⊢ (1..^1) =
∅ |
| 26 | | iuneq1 5008 |
. . . . . . . 8
⊢ ((1..^1)
= ∅ → ∪ 𝑘 ∈ (1..^1)𝐵 = ∪ 𝑘 ∈ ∅ 𝐵) |
| 27 | 25, 26 | ax-mp 5 |
. . . . . . 7
⊢ ∪ 𝑘 ∈ (1..^1)𝐵 = ∪ 𝑘 ∈ ∅ 𝐵 |
| 28 | | 0iun 5063 |
. . . . . . 7
⊢ ∪ 𝑘 ∈ ∅ 𝐵 = ∅ |
| 29 | 27, 28 | eqtri 2765 |
. . . . . 6
⊢ ∪ 𝑘 ∈ (1..^1)𝐵 = ∅ |
| 30 | | fiunelros.1 |
. . . . . . 7
⊢ (𝜑 → 𝑆 ∈ 𝑄) |
| 31 | | isros.1 |
. . . . . . . 8
⊢ 𝑄 = {𝑠 ∈ 𝒫 𝒫 𝑂 ∣ (∅ ∈ 𝑠 ∧ ∀𝑥 ∈ 𝑠 ∀𝑦 ∈ 𝑠 ((𝑥 ∪ 𝑦) ∈ 𝑠 ∧ (𝑥 ∖ 𝑦) ∈ 𝑠))} |
| 32 | 31 | 0elros 34171 |
. . . . . . 7
⊢ (𝑆 ∈ 𝑄 → ∅ ∈ 𝑆) |
| 33 | 30, 32 | syl 17 |
. . . . . 6
⊢ (𝜑 → ∅ ∈ 𝑆) |
| 34 | 29, 33 | eqeltrid 2845 |
. . . . 5
⊢ (𝜑 → ∪ 𝑘 ∈ (1..^1)𝐵 ∈ 𝑆) |
| 35 | 34 | a1d 25 |
. . . 4
⊢ (𝜑 → (1 ≤ 𝑁 → ∪
𝑘 ∈ (1..^1)𝐵 ∈ 𝑆)) |
| 36 | | simpllr 776 |
. . . . . . . 8
⊢ ((((𝜑 ∧ 𝑖 ∈ ℕ) ∧ (𝑖 ≤ 𝑁 → ∪
𝑘 ∈ (1..^𝑖)𝐵 ∈ 𝑆)) ∧ (𝑖 + 1) ≤ 𝑁) → 𝑖 ∈ ℕ) |
| 37 | | fzosplitsn 13814 |
. . . . . . . . . 10
⊢ (𝑖 ∈
(ℤ≥‘1) → (1..^(𝑖 + 1)) = ((1..^𝑖) ∪ {𝑖})) |
| 38 | | nnuz 12921 |
. . . . . . . . . 10
⊢ ℕ =
(ℤ≥‘1) |
| 39 | 37, 38 | eleq2s 2859 |
. . . . . . . . 9
⊢ (𝑖 ∈ ℕ →
(1..^(𝑖 + 1)) = ((1..^𝑖) ∪ {𝑖})) |
| 40 | 39 | iuneq1d 5019 |
. . . . . . . 8
⊢ (𝑖 ∈ ℕ → ∪ 𝑘 ∈ (1..^(𝑖 + 1))𝐵 = ∪ 𝑘 ∈ ((1..^𝑖) ∪ {𝑖})𝐵) |
| 41 | 36, 40 | syl 17 |
. . . . . . 7
⊢ ((((𝜑 ∧ 𝑖 ∈ ℕ) ∧ (𝑖 ≤ 𝑁 → ∪
𝑘 ∈ (1..^𝑖)𝐵 ∈ 𝑆)) ∧ (𝑖 + 1) ≤ 𝑁) → ∪
𝑘 ∈ (1..^(𝑖 + 1))𝐵 = ∪ 𝑘 ∈ ((1..^𝑖) ∪ {𝑖})𝐵) |
| 42 | | iunxun 5094 |
. . . . . . 7
⊢ ∪ 𝑘 ∈ ((1..^𝑖) ∪ {𝑖})𝐵 = (∪
𝑘 ∈ (1..^𝑖)𝐵 ∪ ∪
𝑘 ∈ {𝑖}𝐵) |
| 43 | 41, 42 | eqtrdi 2793 |
. . . . . 6
⊢ ((((𝜑 ∧ 𝑖 ∈ ℕ) ∧ (𝑖 ≤ 𝑁 → ∪
𝑘 ∈ (1..^𝑖)𝐵 ∈ 𝑆)) ∧ (𝑖 + 1) ≤ 𝑁) → ∪
𝑘 ∈ (1..^(𝑖 + 1))𝐵 = (∪
𝑘 ∈ (1..^𝑖)𝐵 ∪ ∪
𝑘 ∈ {𝑖}𝐵)) |
| 44 | 30 | ad3antrrr 730 |
. . . . . . 7
⊢ ((((𝜑 ∧ 𝑖 ∈ ℕ) ∧ (𝑖 ≤ 𝑁 → ∪
𝑘 ∈ (1..^𝑖)𝐵 ∈ 𝑆)) ∧ (𝑖 + 1) ≤ 𝑁) → 𝑆 ∈ 𝑄) |
| 45 | 36 | nnred 12281 |
. . . . . . . . 9
⊢ ((((𝜑 ∧ 𝑖 ∈ ℕ) ∧ (𝑖 ≤ 𝑁 → ∪
𝑘 ∈ (1..^𝑖)𝐵 ∈ 𝑆)) ∧ (𝑖 + 1) ≤ 𝑁) → 𝑖 ∈ ℝ) |
| 46 | 1 | ad3antrrr 730 |
. . . . . . . . . 10
⊢ ((((𝜑 ∧ 𝑖 ∈ ℕ) ∧ (𝑖 ≤ 𝑁 → ∪
𝑘 ∈ (1..^𝑖)𝐵 ∈ 𝑆)) ∧ (𝑖 + 1) ≤ 𝑁) → 𝑁 ∈ ℕ) |
| 47 | 46 | nnred 12281 |
. . . . . . . . 9
⊢ ((((𝜑 ∧ 𝑖 ∈ ℕ) ∧ (𝑖 ≤ 𝑁 → ∪
𝑘 ∈ (1..^𝑖)𝐵 ∈ 𝑆)) ∧ (𝑖 + 1) ≤ 𝑁) → 𝑁 ∈ ℝ) |
| 48 | | simpr 484 |
. . . . . . . . . 10
⊢ ((((𝜑 ∧ 𝑖 ∈ ℕ) ∧ (𝑖 ≤ 𝑁 → ∪
𝑘 ∈ (1..^𝑖)𝐵 ∈ 𝑆)) ∧ (𝑖 + 1) ≤ 𝑁) → (𝑖 + 1) ≤ 𝑁) |
| 49 | | nnltp1le 12674 |
. . . . . . . . . . 11
⊢ ((𝑖 ∈ ℕ ∧ 𝑁 ∈ ℕ) → (𝑖 < 𝑁 ↔ (𝑖 + 1) ≤ 𝑁)) |
| 50 | 36, 46, 49 | syl2anc 584 |
. . . . . . . . . 10
⊢ ((((𝜑 ∧ 𝑖 ∈ ℕ) ∧ (𝑖 ≤ 𝑁 → ∪
𝑘 ∈ (1..^𝑖)𝐵 ∈ 𝑆)) ∧ (𝑖 + 1) ≤ 𝑁) → (𝑖 < 𝑁 ↔ (𝑖 + 1) ≤ 𝑁)) |
| 51 | 48, 50 | mpbird 257 |
. . . . . . . . 9
⊢ ((((𝜑 ∧ 𝑖 ∈ ℕ) ∧ (𝑖 ≤ 𝑁 → ∪
𝑘 ∈ (1..^𝑖)𝐵 ∈ 𝑆)) ∧ (𝑖 + 1) ≤ 𝑁) → 𝑖 < 𝑁) |
| 52 | 45, 47, 51 | ltled 11409 |
. . . . . . . 8
⊢ ((((𝜑 ∧ 𝑖 ∈ ℕ) ∧ (𝑖 ≤ 𝑁 → ∪
𝑘 ∈ (1..^𝑖)𝐵 ∈ 𝑆)) ∧ (𝑖 + 1) ≤ 𝑁) → 𝑖 ≤ 𝑁) |
| 53 | | simplr 769 |
. . . . . . . 8
⊢ ((((𝜑 ∧ 𝑖 ∈ ℕ) ∧ (𝑖 ≤ 𝑁 → ∪
𝑘 ∈ (1..^𝑖)𝐵 ∈ 𝑆)) ∧ (𝑖 + 1) ≤ 𝑁) → (𝑖 ≤ 𝑁 → ∪
𝑘 ∈ (1..^𝑖)𝐵 ∈ 𝑆)) |
| 54 | 52, 53 | mpd 15 |
. . . . . . 7
⊢ ((((𝜑 ∧ 𝑖 ∈ ℕ) ∧ (𝑖 ≤ 𝑁 → ∪
𝑘 ∈ (1..^𝑖)𝐵 ∈ 𝑆)) ∧ (𝑖 + 1) ≤ 𝑁) → ∪
𝑘 ∈ (1..^𝑖)𝐵 ∈ 𝑆) |
| 55 | | nfcsb1v 3923 |
. . . . . . . . . 10
⊢
Ⅎ𝑘⦋𝑖 / 𝑘⦌𝐵 |
| 56 | | csbeq1a 3913 |
. . . . . . . . . 10
⊢ (𝑘 = 𝑖 → 𝐵 = ⦋𝑖 / 𝑘⦌𝐵) |
| 57 | 55, 56 | iunxsngf 5092 |
. . . . . . . . 9
⊢ (𝑖 ∈ ℕ → ∪ 𝑘 ∈ {𝑖}𝐵 = ⦋𝑖 / 𝑘⦌𝐵) |
| 58 | 36, 57 | syl 17 |
. . . . . . . 8
⊢ ((((𝜑 ∧ 𝑖 ∈ ℕ) ∧ (𝑖 ≤ 𝑁 → ∪
𝑘 ∈ (1..^𝑖)𝐵 ∈ 𝑆)) ∧ (𝑖 + 1) ≤ 𝑁) → ∪
𝑘 ∈ {𝑖}𝐵 = ⦋𝑖 / 𝑘⦌𝐵) |
| 59 | | simplll 775 |
. . . . . . . . 9
⊢ ((((𝜑 ∧ 𝑖 ∈ ℕ) ∧ (𝑖 ≤ 𝑁 → ∪
𝑘 ∈ (1..^𝑖)𝐵 ∈ 𝑆)) ∧ (𝑖 + 1) ≤ 𝑁) → 𝜑) |
| 60 | | elfzo1 13752 |
. . . . . . . . . 10
⊢ (𝑖 ∈ (1..^𝑁) ↔ (𝑖 ∈ ℕ ∧ 𝑁 ∈ ℕ ∧ 𝑖 < 𝑁)) |
| 61 | 36, 46, 51, 60 | syl3anbrc 1344 |
. . . . . . . . 9
⊢ ((((𝜑 ∧ 𝑖 ∈ ℕ) ∧ (𝑖 ≤ 𝑁 → ∪
𝑘 ∈ (1..^𝑖)𝐵 ∈ 𝑆)) ∧ (𝑖 + 1) ≤ 𝑁) → 𝑖 ∈ (1..^𝑁)) |
| 62 | | nfv 1914 |
. . . . . . . . . . 11
⊢
Ⅎ𝑘(𝜑 ∧ 𝑖 ∈ (1..^𝑁)) |
| 63 | | nfcv 2905 |
. . . . . . . . . . . 12
⊢
Ⅎ𝑘𝑆 |
| 64 | 55, 63 | nfel 2920 |
. . . . . . . . . . 11
⊢
Ⅎ𝑘⦋𝑖 / 𝑘⦌𝐵 ∈ 𝑆 |
| 65 | 62, 64 | nfim 1896 |
. . . . . . . . . 10
⊢
Ⅎ𝑘((𝜑 ∧ 𝑖 ∈ (1..^𝑁)) → ⦋𝑖 / 𝑘⦌𝐵 ∈ 𝑆) |
| 66 | | eleq1w 2824 |
. . . . . . . . . . . 12
⊢ (𝑘 = 𝑖 → (𝑘 ∈ (1..^𝑁) ↔ 𝑖 ∈ (1..^𝑁))) |
| 67 | 66 | anbi2d 630 |
. . . . . . . . . . 11
⊢ (𝑘 = 𝑖 → ((𝜑 ∧ 𝑘 ∈ (1..^𝑁)) ↔ (𝜑 ∧ 𝑖 ∈ (1..^𝑁)))) |
| 68 | 56 | eleq1d 2826 |
. . . . . . . . . . 11
⊢ (𝑘 = 𝑖 → (𝐵 ∈ 𝑆 ↔ ⦋𝑖 / 𝑘⦌𝐵 ∈ 𝑆)) |
| 69 | 67, 68 | imbi12d 344 |
. . . . . . . . . 10
⊢ (𝑘 = 𝑖 → (((𝜑 ∧ 𝑘 ∈ (1..^𝑁)) → 𝐵 ∈ 𝑆) ↔ ((𝜑 ∧ 𝑖 ∈ (1..^𝑁)) → ⦋𝑖 / 𝑘⦌𝐵 ∈ 𝑆))) |
| 70 | | fiunelros.3 |
. . . . . . . . . 10
⊢ ((𝜑 ∧ 𝑘 ∈ (1..^𝑁)) → 𝐵 ∈ 𝑆) |
| 71 | 65, 69, 70 | chvarfv 2240 |
. . . . . . . . 9
⊢ ((𝜑 ∧ 𝑖 ∈ (1..^𝑁)) → ⦋𝑖 / 𝑘⦌𝐵 ∈ 𝑆) |
| 72 | 59, 61, 71 | syl2anc 584 |
. . . . . . . 8
⊢ ((((𝜑 ∧ 𝑖 ∈ ℕ) ∧ (𝑖 ≤ 𝑁 → ∪
𝑘 ∈ (1..^𝑖)𝐵 ∈ 𝑆)) ∧ (𝑖 + 1) ≤ 𝑁) → ⦋𝑖 / 𝑘⦌𝐵 ∈ 𝑆) |
| 73 | 58, 72 | eqeltrd 2841 |
. . . . . . 7
⊢ ((((𝜑 ∧ 𝑖 ∈ ℕ) ∧ (𝑖 ≤ 𝑁 → ∪
𝑘 ∈ (1..^𝑖)𝐵 ∈ 𝑆)) ∧ (𝑖 + 1) ≤ 𝑁) → ∪
𝑘 ∈ {𝑖}𝐵 ∈ 𝑆) |
| 74 | 31 | unelros 34172 |
. . . . . . 7
⊢ ((𝑆 ∈ 𝑄 ∧ ∪
𝑘 ∈ (1..^𝑖)𝐵 ∈ 𝑆 ∧ ∪
𝑘 ∈ {𝑖}𝐵 ∈ 𝑆) → (∪ 𝑘 ∈ (1..^𝑖)𝐵 ∪ ∪
𝑘 ∈ {𝑖}𝐵) ∈ 𝑆) |
| 75 | 44, 54, 73, 74 | syl3anc 1373 |
. . . . . 6
⊢ ((((𝜑 ∧ 𝑖 ∈ ℕ) ∧ (𝑖 ≤ 𝑁 → ∪
𝑘 ∈ (1..^𝑖)𝐵 ∈ 𝑆)) ∧ (𝑖 + 1) ≤ 𝑁) → (∪ 𝑘 ∈ (1..^𝑖)𝐵 ∪ ∪
𝑘 ∈ {𝑖}𝐵) ∈ 𝑆) |
| 76 | 43, 75 | eqeltrd 2841 |
. . . . 5
⊢ ((((𝜑 ∧ 𝑖 ∈ ℕ) ∧ (𝑖 ≤ 𝑁 → ∪
𝑘 ∈ (1..^𝑖)𝐵 ∈ 𝑆)) ∧ (𝑖 + 1) ≤ 𝑁) → ∪
𝑘 ∈ (1..^(𝑖 + 1))𝐵 ∈ 𝑆) |
| 77 | 76 | ex 412 |
. . . 4
⊢ (((𝜑 ∧ 𝑖 ∈ ℕ) ∧ (𝑖 ≤ 𝑁 → ∪
𝑘 ∈ (1..^𝑖)𝐵 ∈ 𝑆)) → ((𝑖 + 1) ≤ 𝑁 → ∪
𝑘 ∈ (1..^(𝑖 + 1))𝐵 ∈ 𝑆)) |
| 78 | 9, 14, 19, 24, 35, 77 | nnindd 12286 |
. . 3
⊢ ((𝜑 ∧ 𝑁 ∈ ℕ) → (𝑁 ≤ 𝑁 → ∪
𝑘 ∈ (1..^𝑁)𝐵 ∈ 𝑆)) |
| 79 | 4, 78 | mpd 15 |
. 2
⊢ ((𝜑 ∧ 𝑁 ∈ ℕ) → ∪ 𝑘 ∈ (1..^𝑁)𝐵 ∈ 𝑆) |
| 80 | 1, 79 | mpdan 687 |
1
⊢ (𝜑 → ∪ 𝑘 ∈ (1..^𝑁)𝐵 ∈ 𝑆) |