| Step | Hyp | Ref
| Expression |
| 1 | | tru 1544 |
. . . 4
⊢
⊤ |
| 2 | | eqeq12 2754 |
. . . . . 6
⊢ ((𝑎 = 𝑥 ∧ 𝑏 = 𝑦) → (𝑎 = 𝑏 ↔ 𝑥 = 𝑦)) |
| 3 | | csbeq1 3902 |
. . . . . . . 8
⊢ (𝑎 = 𝑥 → ⦋𝑎 / 𝑛⦌(𝐴 ∖ ∪
𝑘 ∈ (1..^𝑛)𝐵) = ⦋𝑥 / 𝑛⦌(𝐴 ∖ ∪
𝑘 ∈ (1..^𝑛)𝐵)) |
| 4 | | csbeq1 3902 |
. . . . . . . 8
⊢ (𝑏 = 𝑦 → ⦋𝑏 / 𝑛⦌(𝐴 ∖ ∪
𝑘 ∈ (1..^𝑛)𝐵) = ⦋𝑦 / 𝑛⦌(𝐴 ∖ ∪
𝑘 ∈ (1..^𝑛)𝐵)) |
| 5 | 3, 4 | ineqan12d 4222 |
. . . . . . 7
⊢ ((𝑎 = 𝑥 ∧ 𝑏 = 𝑦) → (⦋𝑎 / 𝑛⦌(𝐴 ∖ ∪
𝑘 ∈ (1..^𝑛)𝐵) ∩ ⦋𝑏 / 𝑛⦌(𝐴 ∖ ∪
𝑘 ∈ (1..^𝑛)𝐵)) = (⦋𝑥 / 𝑛⦌(𝐴 ∖ ∪
𝑘 ∈ (1..^𝑛)𝐵) ∩ ⦋𝑦 / 𝑛⦌(𝐴 ∖ ∪
𝑘 ∈ (1..^𝑛)𝐵))) |
| 6 | 5 | eqeq1d 2739 |
. . . . . 6
⊢ ((𝑎 = 𝑥 ∧ 𝑏 = 𝑦) → ((⦋𝑎 / 𝑛⦌(𝐴 ∖ ∪
𝑘 ∈ (1..^𝑛)𝐵) ∩ ⦋𝑏 / 𝑛⦌(𝐴 ∖ ∪
𝑘 ∈ (1..^𝑛)𝐵)) = ∅ ↔ (⦋𝑥 / 𝑛⦌(𝐴 ∖ ∪
𝑘 ∈ (1..^𝑛)𝐵) ∩ ⦋𝑦 / 𝑛⦌(𝐴 ∖ ∪
𝑘 ∈ (1..^𝑛)𝐵)) = ∅)) |
| 7 | 2, 6 | orbi12d 919 |
. . . . 5
⊢ ((𝑎 = 𝑥 ∧ 𝑏 = 𝑦) → ((𝑎 = 𝑏 ∨ (⦋𝑎 / 𝑛⦌(𝐴 ∖ ∪
𝑘 ∈ (1..^𝑛)𝐵) ∩ ⦋𝑏 / 𝑛⦌(𝐴 ∖ ∪
𝑘 ∈ (1..^𝑛)𝐵)) = ∅) ↔ (𝑥 = 𝑦 ∨ (⦋𝑥 / 𝑛⦌(𝐴 ∖ ∪
𝑘 ∈ (1..^𝑛)𝐵) ∩ ⦋𝑦 / 𝑛⦌(𝐴 ∖ ∪
𝑘 ∈ (1..^𝑛)𝐵)) = ∅))) |
| 8 | | eqeq12 2754 |
. . . . . . 7
⊢ ((𝑎 = 𝑦 ∧ 𝑏 = 𝑥) → (𝑎 = 𝑏 ↔ 𝑦 = 𝑥)) |
| 9 | | equcom 2017 |
. . . . . . 7
⊢ (𝑦 = 𝑥 ↔ 𝑥 = 𝑦) |
| 10 | 8, 9 | bitrdi 287 |
. . . . . 6
⊢ ((𝑎 = 𝑦 ∧ 𝑏 = 𝑥) → (𝑎 = 𝑏 ↔ 𝑥 = 𝑦)) |
| 11 | | csbeq1 3902 |
. . . . . . . . 9
⊢ (𝑎 = 𝑦 → ⦋𝑎 / 𝑛⦌(𝐴 ∖ ∪
𝑘 ∈ (1..^𝑛)𝐵) = ⦋𝑦 / 𝑛⦌(𝐴 ∖ ∪
𝑘 ∈ (1..^𝑛)𝐵)) |
| 12 | | csbeq1 3902 |
. . . . . . . . 9
⊢ (𝑏 = 𝑥 → ⦋𝑏 / 𝑛⦌(𝐴 ∖ ∪
𝑘 ∈ (1..^𝑛)𝐵) = ⦋𝑥 / 𝑛⦌(𝐴 ∖ ∪
𝑘 ∈ (1..^𝑛)𝐵)) |
| 13 | 11, 12 | ineqan12d 4222 |
. . . . . . . 8
⊢ ((𝑎 = 𝑦 ∧ 𝑏 = 𝑥) → (⦋𝑎 / 𝑛⦌(𝐴 ∖ ∪
𝑘 ∈ (1..^𝑛)𝐵) ∩ ⦋𝑏 / 𝑛⦌(𝐴 ∖ ∪
𝑘 ∈ (1..^𝑛)𝐵)) = (⦋𝑦 / 𝑛⦌(𝐴 ∖ ∪
𝑘 ∈ (1..^𝑛)𝐵) ∩ ⦋𝑥 / 𝑛⦌(𝐴 ∖ ∪
𝑘 ∈ (1..^𝑛)𝐵))) |
| 14 | | incom 4209 |
. . . . . . . 8
⊢
(⦋𝑦 /
𝑛⦌(𝐴 ∖ ∪ 𝑘 ∈ (1..^𝑛)𝐵) ∩ ⦋𝑥 / 𝑛⦌(𝐴 ∖ ∪
𝑘 ∈ (1..^𝑛)𝐵)) = (⦋𝑥 / 𝑛⦌(𝐴 ∖ ∪
𝑘 ∈ (1..^𝑛)𝐵) ∩ ⦋𝑦 / 𝑛⦌(𝐴 ∖ ∪
𝑘 ∈ (1..^𝑛)𝐵)) |
| 15 | 13, 14 | eqtrdi 2793 |
. . . . . . 7
⊢ ((𝑎 = 𝑦 ∧ 𝑏 = 𝑥) → (⦋𝑎 / 𝑛⦌(𝐴 ∖ ∪
𝑘 ∈ (1..^𝑛)𝐵) ∩ ⦋𝑏 / 𝑛⦌(𝐴 ∖ ∪
𝑘 ∈ (1..^𝑛)𝐵)) = (⦋𝑥 / 𝑛⦌(𝐴 ∖ ∪
𝑘 ∈ (1..^𝑛)𝐵) ∩ ⦋𝑦 / 𝑛⦌(𝐴 ∖ ∪
𝑘 ∈ (1..^𝑛)𝐵))) |
| 16 | 15 | eqeq1d 2739 |
. . . . . 6
⊢ ((𝑎 = 𝑦 ∧ 𝑏 = 𝑥) → ((⦋𝑎 / 𝑛⦌(𝐴 ∖ ∪
𝑘 ∈ (1..^𝑛)𝐵) ∩ ⦋𝑏 / 𝑛⦌(𝐴 ∖ ∪
𝑘 ∈ (1..^𝑛)𝐵)) = ∅ ↔ (⦋𝑥 / 𝑛⦌(𝐴 ∖ ∪
𝑘 ∈ (1..^𝑛)𝐵) ∩ ⦋𝑦 / 𝑛⦌(𝐴 ∖ ∪
𝑘 ∈ (1..^𝑛)𝐵)) = ∅)) |
| 17 | 10, 16 | orbi12d 919 |
. . . . 5
⊢ ((𝑎 = 𝑦 ∧ 𝑏 = 𝑥) → ((𝑎 = 𝑏 ∨ (⦋𝑎 / 𝑛⦌(𝐴 ∖ ∪
𝑘 ∈ (1..^𝑛)𝐵) ∩ ⦋𝑏 / 𝑛⦌(𝐴 ∖ ∪
𝑘 ∈ (1..^𝑛)𝐵)) = ∅) ↔ (𝑥 = 𝑦 ∨ (⦋𝑥 / 𝑛⦌(𝐴 ∖ ∪
𝑘 ∈ (1..^𝑛)𝐵) ∩ ⦋𝑦 / 𝑛⦌(𝐴 ∖ ∪
𝑘 ∈ (1..^𝑛)𝐵)) = ∅))) |
| 18 | | fzossnn 13751 |
. . . . . . 7
⊢
(1..^𝑁) ⊆
ℕ |
| 19 | | nnssre 12270 |
. . . . . . 7
⊢ ℕ
⊆ ℝ |
| 20 | 18, 19 | sstri 3993 |
. . . . . 6
⊢
(1..^𝑁) ⊆
ℝ |
| 21 | 20 | a1i 11 |
. . . . 5
⊢ (⊤
→ (1..^𝑁) ⊆
ℝ) |
| 22 | | biidd 262 |
. . . . 5
⊢
((⊤ ∧ (𝑥
∈ (1..^𝑁) ∧ 𝑦 ∈ (1..^𝑁))) → ((𝑥 = 𝑦 ∨ (⦋𝑥 / 𝑛⦌(𝐴 ∖ ∪
𝑘 ∈ (1..^𝑛)𝐵) ∩ ⦋𝑦 / 𝑛⦌(𝐴 ∖ ∪
𝑘 ∈ (1..^𝑛)𝐵)) = ∅) ↔ (𝑥 = 𝑦 ∨ (⦋𝑥 / 𝑛⦌(𝐴 ∖ ∪
𝑘 ∈ (1..^𝑛)𝐵) ∩ ⦋𝑦 / 𝑛⦌(𝐴 ∖ ∪
𝑘 ∈ (1..^𝑛)𝐵)) = ∅))) |
| 23 | | nesym 2997 |
. . . . . . . 8
⊢ (𝑦 ≠ 𝑥 ↔ ¬ 𝑥 = 𝑦) |
| 24 | 20 | sseli 3979 |
. . . . . . . . . 10
⊢ (𝑥 ∈ (1..^𝑁) → 𝑥 ∈ ℝ) |
| 25 | 20 | sseli 3979 |
. . . . . . . . . 10
⊢ (𝑦 ∈ (1..^𝑁) → 𝑦 ∈ ℝ) |
| 26 | | id 22 |
. . . . . . . . . 10
⊢ (𝑥 ≤ 𝑦 → 𝑥 ≤ 𝑦) |
| 27 | | leltne 11350 |
. . . . . . . . . 10
⊢ ((𝑥 ∈ ℝ ∧ 𝑦 ∈ ℝ ∧ 𝑥 ≤ 𝑦) → (𝑥 < 𝑦 ↔ 𝑦 ≠ 𝑥)) |
| 28 | 24, 25, 26, 27 | syl3an 1161 |
. . . . . . . . 9
⊢ ((𝑥 ∈ (1..^𝑁) ∧ 𝑦 ∈ (1..^𝑁) ∧ 𝑥 ≤ 𝑦) → (𝑥 < 𝑦 ↔ 𝑦 ≠ 𝑥)) |
| 29 | | vex 3484 |
. . . . . . . . . . . . . . 15
⊢ 𝑥 ∈ V |
| 30 | | nfcsb1v 3923 |
. . . . . . . . . . . . . . . 16
⊢
Ⅎ𝑛⦋𝑥 / 𝑛⦌𝐴 |
| 31 | | nfcv 2905 |
. . . . . . . . . . . . . . . . 17
⊢
Ⅎ𝑛(1..^𝑥) |
| 32 | | iundisj2fi.0 |
. . . . . . . . . . . . . . . . 17
⊢
Ⅎ𝑛𝐵 |
| 33 | 31, 32 | nfiun 5023 |
. . . . . . . . . . . . . . . 16
⊢
Ⅎ𝑛∪ 𝑘 ∈ (1..^𝑥)𝐵 |
| 34 | 30, 33 | nfdif 4129 |
. . . . . . . . . . . . . . 15
⊢
Ⅎ𝑛(⦋𝑥 / 𝑛⦌𝐴 ∖ ∪
𝑘 ∈ (1..^𝑥)𝐵) |
| 35 | | csbeq1a 3913 |
. . . . . . . . . . . . . . . 16
⊢ (𝑛 = 𝑥 → 𝐴 = ⦋𝑥 / 𝑛⦌𝐴) |
| 36 | | oveq2 7439 |
. . . . . . . . . . . . . . . . 17
⊢ (𝑛 = 𝑥 → (1..^𝑛) = (1..^𝑥)) |
| 37 | 36 | iuneq1d 5019 |
. . . . . . . . . . . . . . . 16
⊢ (𝑛 = 𝑥 → ∪
𝑘 ∈ (1..^𝑛)𝐵 = ∪ 𝑘 ∈ (1..^𝑥)𝐵) |
| 38 | 35, 37 | difeq12d 4127 |
. . . . . . . . . . . . . . 15
⊢ (𝑛 = 𝑥 → (𝐴 ∖ ∪
𝑘 ∈ (1..^𝑛)𝐵) = (⦋𝑥 / 𝑛⦌𝐴 ∖ ∪
𝑘 ∈ (1..^𝑥)𝐵)) |
| 39 | 29, 34, 38 | csbief 3933 |
. . . . . . . . . . . . . 14
⊢
⦋𝑥 /
𝑛⦌(𝐴 ∖ ∪ 𝑘 ∈ (1..^𝑛)𝐵) = (⦋𝑥 / 𝑛⦌𝐴 ∖ ∪
𝑘 ∈ (1..^𝑥)𝐵) |
| 40 | | vex 3484 |
. . . . . . . . . . . . . . 15
⊢ 𝑦 ∈ V |
| 41 | | nfcsb1v 3923 |
. . . . . . . . . . . . . . . 16
⊢
Ⅎ𝑛⦋𝑦 / 𝑛⦌𝐴 |
| 42 | | nfcv 2905 |
. . . . . . . . . . . . . . . . 17
⊢
Ⅎ𝑛(1..^𝑦) |
| 43 | 42, 32 | nfiun 5023 |
. . . . . . . . . . . . . . . 16
⊢
Ⅎ𝑛∪ 𝑘 ∈ (1..^𝑦)𝐵 |
| 44 | 41, 43 | nfdif 4129 |
. . . . . . . . . . . . . . 15
⊢
Ⅎ𝑛(⦋𝑦 / 𝑛⦌𝐴 ∖ ∪
𝑘 ∈ (1..^𝑦)𝐵) |
| 45 | | csbeq1a 3913 |
. . . . . . . . . . . . . . . 16
⊢ (𝑛 = 𝑦 → 𝐴 = ⦋𝑦 / 𝑛⦌𝐴) |
| 46 | | oveq2 7439 |
. . . . . . . . . . . . . . . . 17
⊢ (𝑛 = 𝑦 → (1..^𝑛) = (1..^𝑦)) |
| 47 | 46 | iuneq1d 5019 |
. . . . . . . . . . . . . . . 16
⊢ (𝑛 = 𝑦 → ∪
𝑘 ∈ (1..^𝑛)𝐵 = ∪ 𝑘 ∈ (1..^𝑦)𝐵) |
| 48 | 45, 47 | difeq12d 4127 |
. . . . . . . . . . . . . . 15
⊢ (𝑛 = 𝑦 → (𝐴 ∖ ∪
𝑘 ∈ (1..^𝑛)𝐵) = (⦋𝑦 / 𝑛⦌𝐴 ∖ ∪
𝑘 ∈ (1..^𝑦)𝐵)) |
| 49 | 40, 44, 48 | csbief 3933 |
. . . . . . . . . . . . . 14
⊢
⦋𝑦 /
𝑛⦌(𝐴 ∖ ∪ 𝑘 ∈ (1..^𝑛)𝐵) = (⦋𝑦 / 𝑛⦌𝐴 ∖ ∪
𝑘 ∈ (1..^𝑦)𝐵) |
| 50 | 39, 49 | ineq12i 4218 |
. . . . . . . . . . . . 13
⊢
(⦋𝑥 /
𝑛⦌(𝐴 ∖ ∪ 𝑘 ∈ (1..^𝑛)𝐵) ∩ ⦋𝑦 / 𝑛⦌(𝐴 ∖ ∪
𝑘 ∈ (1..^𝑛)𝐵)) = ((⦋𝑥 / 𝑛⦌𝐴 ∖ ∪
𝑘 ∈ (1..^𝑥)𝐵) ∩ (⦋𝑦 / 𝑛⦌𝐴 ∖ ∪
𝑘 ∈ (1..^𝑦)𝐵)) |
| 51 | | simp1 1137 |
. . . . . . . . . . . . . . . . . . 19
⊢ ((𝑥 ∈ (1..^𝑁) ∧ 𝑦 ∈ (1..^𝑁) ∧ 𝑥 < 𝑦) → 𝑥 ∈ (1..^𝑁)) |
| 52 | 18, 51 | sselid 3981 |
. . . . . . . . . . . . . . . . . 18
⊢ ((𝑥 ∈ (1..^𝑁) ∧ 𝑦 ∈ (1..^𝑁) ∧ 𝑥 < 𝑦) → 𝑥 ∈ ℕ) |
| 53 | | nnuz 12921 |
. . . . . . . . . . . . . . . . . 18
⊢ ℕ =
(ℤ≥‘1) |
| 54 | 52, 53 | eleqtrdi 2851 |
. . . . . . . . . . . . . . . . 17
⊢ ((𝑥 ∈ (1..^𝑁) ∧ 𝑦 ∈ (1..^𝑁) ∧ 𝑥 < 𝑦) → 𝑥 ∈
(ℤ≥‘1)) |
| 55 | | simp2 1138 |
. . . . . . . . . . . . . . . . . . 19
⊢ ((𝑥 ∈ (1..^𝑁) ∧ 𝑦 ∈ (1..^𝑁) ∧ 𝑥 < 𝑦) → 𝑦 ∈ (1..^𝑁)) |
| 56 | 18, 55 | sselid 3981 |
. . . . . . . . . . . . . . . . . 18
⊢ ((𝑥 ∈ (1..^𝑁) ∧ 𝑦 ∈ (1..^𝑁) ∧ 𝑥 < 𝑦) → 𝑦 ∈ ℕ) |
| 57 | 56 | nnzd 12640 |
. . . . . . . . . . . . . . . . 17
⊢ ((𝑥 ∈ (1..^𝑁) ∧ 𝑦 ∈ (1..^𝑁) ∧ 𝑥 < 𝑦) → 𝑦 ∈ ℤ) |
| 58 | | simp3 1139 |
. . . . . . . . . . . . . . . . 17
⊢ ((𝑥 ∈ (1..^𝑁) ∧ 𝑦 ∈ (1..^𝑁) ∧ 𝑥 < 𝑦) → 𝑥 < 𝑦) |
| 59 | | elfzo2 13702 |
. . . . . . . . . . . . . . . . 17
⊢ (𝑥 ∈ (1..^𝑦) ↔ (𝑥 ∈ (ℤ≥‘1)
∧ 𝑦 ∈ ℤ
∧ 𝑥 < 𝑦)) |
| 60 | 54, 57, 58, 59 | syl3anbrc 1344 |
. . . . . . . . . . . . . . . 16
⊢ ((𝑥 ∈ (1..^𝑁) ∧ 𝑦 ∈ (1..^𝑁) ∧ 𝑥 < 𝑦) → 𝑥 ∈ (1..^𝑦)) |
| 61 | | nfcv 2905 |
. . . . . . . . . . . . . . . . . . . 20
⊢
Ⅎ𝑛𝑘 |
| 62 | | iundisj2fi.1 |
. . . . . . . . . . . . . . . . . . . 20
⊢ (𝑛 = 𝑘 → 𝐴 = 𝐵) |
| 63 | 61, 32, 62 | csbhypf 3927 |
. . . . . . . . . . . . . . . . . . 19
⊢ (𝑥 = 𝑘 → ⦋𝑥 / 𝑛⦌𝐴 = 𝐵) |
| 64 | 63 | equcoms 2019 |
. . . . . . . . . . . . . . . . . 18
⊢ (𝑘 = 𝑥 → ⦋𝑥 / 𝑛⦌𝐴 = 𝐵) |
| 65 | 64 | eqcomd 2743 |
. . . . . . . . . . . . . . . . 17
⊢ (𝑘 = 𝑥 → 𝐵 = ⦋𝑥 / 𝑛⦌𝐴) |
| 66 | 65 | ssiun2s 5048 |
. . . . . . . . . . . . . . . 16
⊢ (𝑥 ∈ (1..^𝑦) → ⦋𝑥 / 𝑛⦌𝐴 ⊆ ∪
𝑘 ∈ (1..^𝑦)𝐵) |
| 67 | 60, 66 | syl 17 |
. . . . . . . . . . . . . . 15
⊢ ((𝑥 ∈ (1..^𝑁) ∧ 𝑦 ∈ (1..^𝑁) ∧ 𝑥 < 𝑦) → ⦋𝑥 / 𝑛⦌𝐴 ⊆ ∪
𝑘 ∈ (1..^𝑦)𝐵) |
| 68 | 67 | ssdifssd 4147 |
. . . . . . . . . . . . . 14
⊢ ((𝑥 ∈ (1..^𝑁) ∧ 𝑦 ∈ (1..^𝑁) ∧ 𝑥 < 𝑦) → (⦋𝑥 / 𝑛⦌𝐴 ∖ ∪
𝑘 ∈ (1..^𝑥)𝐵) ⊆ ∪ 𝑘 ∈ (1..^𝑦)𝐵) |
| 69 | 68 | ssrind 4244 |
. . . . . . . . . . . . 13
⊢ ((𝑥 ∈ (1..^𝑁) ∧ 𝑦 ∈ (1..^𝑁) ∧ 𝑥 < 𝑦) → ((⦋𝑥 / 𝑛⦌𝐴 ∖ ∪
𝑘 ∈ (1..^𝑥)𝐵) ∩ (⦋𝑦 / 𝑛⦌𝐴 ∖ ∪
𝑘 ∈ (1..^𝑦)𝐵)) ⊆ (∪ 𝑘 ∈ (1..^𝑦)𝐵 ∩ (⦋𝑦 / 𝑛⦌𝐴 ∖ ∪
𝑘 ∈ (1..^𝑦)𝐵))) |
| 70 | 50, 69 | eqsstrid 4022 |
. . . . . . . . . . . 12
⊢ ((𝑥 ∈ (1..^𝑁) ∧ 𝑦 ∈ (1..^𝑁) ∧ 𝑥 < 𝑦) → (⦋𝑥 / 𝑛⦌(𝐴 ∖ ∪
𝑘 ∈ (1..^𝑛)𝐵) ∩ ⦋𝑦 / 𝑛⦌(𝐴 ∖ ∪
𝑘 ∈ (1..^𝑛)𝐵)) ⊆ (∪ 𝑘 ∈ (1..^𝑦)𝐵 ∩ (⦋𝑦 / 𝑛⦌𝐴 ∖ ∪
𝑘 ∈ (1..^𝑦)𝐵))) |
| 71 | | disjdif 4472 |
. . . . . . . . . . . 12
⊢ (∪ 𝑘 ∈ (1..^𝑦)𝐵 ∩ (⦋𝑦 / 𝑛⦌𝐴 ∖ ∪
𝑘 ∈ (1..^𝑦)𝐵)) = ∅ |
| 72 | | sseq0 4403 |
. . . . . . . . . . . 12
⊢
(((⦋𝑥
/ 𝑛⦌(𝐴 ∖ ∪ 𝑘 ∈ (1..^𝑛)𝐵) ∩ ⦋𝑦 / 𝑛⦌(𝐴 ∖ ∪
𝑘 ∈ (1..^𝑛)𝐵)) ⊆ (∪ 𝑘 ∈ (1..^𝑦)𝐵 ∩ (⦋𝑦 / 𝑛⦌𝐴 ∖ ∪
𝑘 ∈ (1..^𝑦)𝐵)) ∧ (∪ 𝑘 ∈ (1..^𝑦)𝐵 ∩ (⦋𝑦 / 𝑛⦌𝐴 ∖ ∪
𝑘 ∈ (1..^𝑦)𝐵)) = ∅) → (⦋𝑥 / 𝑛⦌(𝐴 ∖ ∪
𝑘 ∈ (1..^𝑛)𝐵) ∩ ⦋𝑦 / 𝑛⦌(𝐴 ∖ ∪
𝑘 ∈ (1..^𝑛)𝐵)) = ∅) |
| 73 | 70, 71, 72 | sylancl 586 |
. . . . . . . . . . 11
⊢ ((𝑥 ∈ (1..^𝑁) ∧ 𝑦 ∈ (1..^𝑁) ∧ 𝑥 < 𝑦) → (⦋𝑥 / 𝑛⦌(𝐴 ∖ ∪
𝑘 ∈ (1..^𝑛)𝐵) ∩ ⦋𝑦 / 𝑛⦌(𝐴 ∖ ∪
𝑘 ∈ (1..^𝑛)𝐵)) = ∅) |
| 74 | 73 | 3expia 1122 |
. . . . . . . . . 10
⊢ ((𝑥 ∈ (1..^𝑁) ∧ 𝑦 ∈ (1..^𝑁)) → (𝑥 < 𝑦 → (⦋𝑥 / 𝑛⦌(𝐴 ∖ ∪
𝑘 ∈ (1..^𝑛)𝐵) ∩ ⦋𝑦 / 𝑛⦌(𝐴 ∖ ∪
𝑘 ∈ (1..^𝑛)𝐵)) = ∅)) |
| 75 | 74 | 3adant3 1133 |
. . . . . . . . 9
⊢ ((𝑥 ∈ (1..^𝑁) ∧ 𝑦 ∈ (1..^𝑁) ∧ 𝑥 ≤ 𝑦) → (𝑥 < 𝑦 → (⦋𝑥 / 𝑛⦌(𝐴 ∖ ∪
𝑘 ∈ (1..^𝑛)𝐵) ∩ ⦋𝑦 / 𝑛⦌(𝐴 ∖ ∪
𝑘 ∈ (1..^𝑛)𝐵)) = ∅)) |
| 76 | 28, 75 | sylbird 260 |
. . . . . . . 8
⊢ ((𝑥 ∈ (1..^𝑁) ∧ 𝑦 ∈ (1..^𝑁) ∧ 𝑥 ≤ 𝑦) → (𝑦 ≠ 𝑥 → (⦋𝑥 / 𝑛⦌(𝐴 ∖ ∪
𝑘 ∈ (1..^𝑛)𝐵) ∩ ⦋𝑦 / 𝑛⦌(𝐴 ∖ ∪
𝑘 ∈ (1..^𝑛)𝐵)) = ∅)) |
| 77 | 23, 76 | biimtrrid 243 |
. . . . . . 7
⊢ ((𝑥 ∈ (1..^𝑁) ∧ 𝑦 ∈ (1..^𝑁) ∧ 𝑥 ≤ 𝑦) → (¬ 𝑥 = 𝑦 → (⦋𝑥 / 𝑛⦌(𝐴 ∖ ∪
𝑘 ∈ (1..^𝑛)𝐵) ∩ ⦋𝑦 / 𝑛⦌(𝐴 ∖ ∪
𝑘 ∈ (1..^𝑛)𝐵)) = ∅)) |
| 78 | 77 | orrd 864 |
. . . . . 6
⊢ ((𝑥 ∈ (1..^𝑁) ∧ 𝑦 ∈ (1..^𝑁) ∧ 𝑥 ≤ 𝑦) → (𝑥 = 𝑦 ∨ (⦋𝑥 / 𝑛⦌(𝐴 ∖ ∪
𝑘 ∈ (1..^𝑛)𝐵) ∩ ⦋𝑦 / 𝑛⦌(𝐴 ∖ ∪
𝑘 ∈ (1..^𝑛)𝐵)) = ∅)) |
| 79 | 78 | adantl 481 |
. . . . 5
⊢
((⊤ ∧ (𝑥
∈ (1..^𝑁) ∧ 𝑦 ∈ (1..^𝑁) ∧ 𝑥 ≤ 𝑦)) → (𝑥 = 𝑦 ∨ (⦋𝑥 / 𝑛⦌(𝐴 ∖ ∪
𝑘 ∈ (1..^𝑛)𝐵) ∩ ⦋𝑦 / 𝑛⦌(𝐴 ∖ ∪
𝑘 ∈ (1..^𝑛)𝐵)) = ∅)) |
| 80 | 7, 17, 21, 22, 79 | wlogle 11796 |
. . . 4
⊢
((⊤ ∧ (𝑥
∈ (1..^𝑁) ∧ 𝑦 ∈ (1..^𝑁))) → (𝑥 = 𝑦 ∨ (⦋𝑥 / 𝑛⦌(𝐴 ∖ ∪
𝑘 ∈ (1..^𝑛)𝐵) ∩ ⦋𝑦 / 𝑛⦌(𝐴 ∖ ∪
𝑘 ∈ (1..^𝑛)𝐵)) = ∅)) |
| 81 | 1, 80 | mpan 690 |
. . 3
⊢ ((𝑥 ∈ (1..^𝑁) ∧ 𝑦 ∈ (1..^𝑁)) → (𝑥 = 𝑦 ∨ (⦋𝑥 / 𝑛⦌(𝐴 ∖ ∪
𝑘 ∈ (1..^𝑛)𝐵) ∩ ⦋𝑦 / 𝑛⦌(𝐴 ∖ ∪
𝑘 ∈ (1..^𝑛)𝐵)) = ∅)) |
| 82 | 81 | rgen2 3199 |
. 2
⊢
∀𝑥 ∈
(1..^𝑁)∀𝑦 ∈ (1..^𝑁)(𝑥 = 𝑦 ∨ (⦋𝑥 / 𝑛⦌(𝐴 ∖ ∪
𝑘 ∈ (1..^𝑛)𝐵) ∩ ⦋𝑦 / 𝑛⦌(𝐴 ∖ ∪
𝑘 ∈ (1..^𝑛)𝐵)) = ∅) |
| 83 | | disjors 5126 |
. 2
⊢
(Disj 𝑛
∈ (1..^𝑁)(𝐴 ∖ ∪ 𝑘 ∈ (1..^𝑛)𝐵) ↔ ∀𝑥 ∈ (1..^𝑁)∀𝑦 ∈ (1..^𝑁)(𝑥 = 𝑦 ∨ (⦋𝑥 / 𝑛⦌(𝐴 ∖ ∪
𝑘 ∈ (1..^𝑛)𝐵) ∩ ⦋𝑦 / 𝑛⦌(𝐴 ∖ ∪
𝑘 ∈ (1..^𝑛)𝐵)) = ∅)) |
| 84 | 82, 83 | mpbir 231 |
1
⊢
Disj 𝑛 ∈
(1..^𝑁)(𝐴 ∖ ∪
𝑘 ∈ (1..^𝑛)𝐵) |