Step | Hyp | Ref
| Expression |
1 | | tru 1547 |
. . . 4
⊢
⊤ |
2 | | eqeq12 2754 |
. . . . . 6
⊢ ((𝑎 = 𝑥 ∧ 𝑏 = 𝑦) → (𝑎 = 𝑏 ↔ 𝑥 = 𝑦)) |
3 | | csbeq1 3814 |
. . . . . . . 8
⊢ (𝑎 = 𝑥 → ⦋𝑎 / 𝑛⦌(𝐴 ∖ ∪
𝑘 ∈ (1..^𝑛)𝐵) = ⦋𝑥 / 𝑛⦌(𝐴 ∖ ∪
𝑘 ∈ (1..^𝑛)𝐵)) |
4 | | csbeq1 3814 |
. . . . . . . 8
⊢ (𝑏 = 𝑦 → ⦋𝑏 / 𝑛⦌(𝐴 ∖ ∪
𝑘 ∈ (1..^𝑛)𝐵) = ⦋𝑦 / 𝑛⦌(𝐴 ∖ ∪
𝑘 ∈ (1..^𝑛)𝐵)) |
5 | 3, 4 | ineqan12d 4129 |
. . . . . . 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 2026 |
. . . . . . 7
⊢ (𝑦 = 𝑥 ↔ 𝑥 = 𝑦) |
10 | 8, 9 | bitrdi 290 |
. . . . . 6
⊢ ((𝑎 = 𝑦 ∧ 𝑏 = 𝑥) → (𝑎 = 𝑏 ↔ 𝑥 = 𝑦)) |
11 | | csbeq1 3814 |
. . . . . . . . 9
⊢ (𝑎 = 𝑦 → ⦋𝑎 / 𝑛⦌(𝐴 ∖ ∪
𝑘 ∈ (1..^𝑛)𝐵) = ⦋𝑦 / 𝑛⦌(𝐴 ∖ ∪
𝑘 ∈ (1..^𝑛)𝐵)) |
12 | | csbeq1 3814 |
. . . . . . . . 9
⊢ (𝑏 = 𝑥 → ⦋𝑏 / 𝑛⦌(𝐴 ∖ ∪
𝑘 ∈ (1..^𝑛)𝐵) = ⦋𝑥 / 𝑛⦌(𝐴 ∖ ∪
𝑘 ∈ (1..^𝑛)𝐵)) |
13 | 11, 12 | ineqan12d 4129 |
. . . . . . . 8
⊢ ((𝑎 = 𝑦 ∧ 𝑏 = 𝑥) → (⦋𝑎 / 𝑛⦌(𝐴 ∖ ∪
𝑘 ∈ (1..^𝑛)𝐵) ∩ ⦋𝑏 / 𝑛⦌(𝐴 ∖ ∪
𝑘 ∈ (1..^𝑛)𝐵)) = (⦋𝑦 / 𝑛⦌(𝐴 ∖ ∪
𝑘 ∈ (1..^𝑛)𝐵) ∩ ⦋𝑥 / 𝑛⦌(𝐴 ∖ ∪
𝑘 ∈ (1..^𝑛)𝐵))) |
14 | | incom 4115 |
. . . . . . . 8
⊢
(⦋𝑦 /
𝑛⦌(𝐴 ∖ ∪ 𝑘 ∈ (1..^𝑛)𝐵) ∩ ⦋𝑥 / 𝑛⦌(𝐴 ∖ ∪
𝑘 ∈ (1..^𝑛)𝐵)) = (⦋𝑥 / 𝑛⦌(𝐴 ∖ ∪
𝑘 ∈ (1..^𝑛)𝐵) ∩ ⦋𝑦 / 𝑛⦌(𝐴 ∖ ∪
𝑘 ∈ (1..^𝑛)𝐵)) |
15 | 13, 14 | eqtrdi 2794 |
. . . . . . 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 | | nnssre 11834 |
. . . . . 6
⊢ ℕ
⊆ ℝ |
19 | 18 | a1i 11 |
. . . . 5
⊢ (⊤
→ ℕ ⊆ ℝ) |
20 | | biidd 265 |
. . . . 5
⊢
((⊤ ∧ (𝑥
∈ ℕ ∧ 𝑦
∈ ℕ)) → ((𝑥
= 𝑦 ∨
(⦋𝑥 / 𝑛⦌(𝐴 ∖ ∪ 𝑘 ∈ (1..^𝑛)𝐵) ∩ ⦋𝑦 / 𝑛⦌(𝐴 ∖ ∪
𝑘 ∈ (1..^𝑛)𝐵)) = ∅) ↔ (𝑥 = 𝑦 ∨ (⦋𝑥 / 𝑛⦌(𝐴 ∖ ∪
𝑘 ∈ (1..^𝑛)𝐵) ∩ ⦋𝑦 / 𝑛⦌(𝐴 ∖ ∪
𝑘 ∈ (1..^𝑛)𝐵)) = ∅))) |
21 | | nesym 2997 |
. . . . . . . 8
⊢ (𝑦 ≠ 𝑥 ↔ ¬ 𝑥 = 𝑦) |
22 | | nnre 11837 |
. . . . . . . . . 10
⊢ (𝑥 ∈ ℕ → 𝑥 ∈
ℝ) |
23 | | nnre 11837 |
. . . . . . . . . 10
⊢ (𝑦 ∈ ℕ → 𝑦 ∈
ℝ) |
24 | | id 22 |
. . . . . . . . . 10
⊢ (𝑥 ≤ 𝑦 → 𝑥 ≤ 𝑦) |
25 | | leltne 10922 |
. . . . . . . . . 10
⊢ ((𝑥 ∈ ℝ ∧ 𝑦 ∈ ℝ ∧ 𝑥 ≤ 𝑦) → (𝑥 < 𝑦 ↔ 𝑦 ≠ 𝑥)) |
26 | 22, 23, 24, 25 | syl3an 1162 |
. . . . . . . . 9
⊢ ((𝑥 ∈ ℕ ∧ 𝑦 ∈ ℕ ∧ 𝑥 ≤ 𝑦) → (𝑥 < 𝑦 ↔ 𝑦 ≠ 𝑥)) |
27 | | vex 3412 |
. . . . . . . . . . . . . . 15
⊢ 𝑥 ∈ V |
28 | | nfcsb1v 3836 |
. . . . . . . . . . . . . . . 16
⊢
Ⅎ𝑛⦋𝑥 / 𝑛⦌𝐴 |
29 | | nfcv 2904 |
. . . . . . . . . . . . . . . 16
⊢
Ⅎ𝑛∪ 𝑘 ∈ (1..^𝑥)𝐵 |
30 | 28, 29 | nfdif 4040 |
. . . . . . . . . . . . . . 15
⊢
Ⅎ𝑛(⦋𝑥 / 𝑛⦌𝐴 ∖ ∪
𝑘 ∈ (1..^𝑥)𝐵) |
31 | | csbeq1a 3825 |
. . . . . . . . . . . . . . . 16
⊢ (𝑛 = 𝑥 → 𝐴 = ⦋𝑥 / 𝑛⦌𝐴) |
32 | | oveq2 7221 |
. . . . . . . . . . . . . . . . 17
⊢ (𝑛 = 𝑥 → (1..^𝑛) = (1..^𝑥)) |
33 | 32 | iuneq1d 4931 |
. . . . . . . . . . . . . . . 16
⊢ (𝑛 = 𝑥 → ∪
𝑘 ∈ (1..^𝑛)𝐵 = ∪ 𝑘 ∈ (1..^𝑥)𝐵) |
34 | 31, 33 | difeq12d 4038 |
. . . . . . . . . . . . . . 15
⊢ (𝑛 = 𝑥 → (𝐴 ∖ ∪
𝑘 ∈ (1..^𝑛)𝐵) = (⦋𝑥 / 𝑛⦌𝐴 ∖ ∪
𝑘 ∈ (1..^𝑥)𝐵)) |
35 | 27, 30, 34 | csbief 3846 |
. . . . . . . . . . . . . 14
⊢
⦋𝑥 /
𝑛⦌(𝐴 ∖ ∪ 𝑘 ∈ (1..^𝑛)𝐵) = (⦋𝑥 / 𝑛⦌𝐴 ∖ ∪
𝑘 ∈ (1..^𝑥)𝐵) |
36 | | vex 3412 |
. . . . . . . . . . . . . . 15
⊢ 𝑦 ∈ V |
37 | | nfcsb1v 3836 |
. . . . . . . . . . . . . . . 16
⊢
Ⅎ𝑛⦋𝑦 / 𝑛⦌𝐴 |
38 | | nfcv 2904 |
. . . . . . . . . . . . . . . 16
⊢
Ⅎ𝑛∪ 𝑘 ∈ (1..^𝑦)𝐵 |
39 | 37, 38 | nfdif 4040 |
. . . . . . . . . . . . . . 15
⊢
Ⅎ𝑛(⦋𝑦 / 𝑛⦌𝐴 ∖ ∪
𝑘 ∈ (1..^𝑦)𝐵) |
40 | | csbeq1a 3825 |
. . . . . . . . . . . . . . . 16
⊢ (𝑛 = 𝑦 → 𝐴 = ⦋𝑦 / 𝑛⦌𝐴) |
41 | | oveq2 7221 |
. . . . . . . . . . . . . . . . 17
⊢ (𝑛 = 𝑦 → (1..^𝑛) = (1..^𝑦)) |
42 | 41 | iuneq1d 4931 |
. . . . . . . . . . . . . . . 16
⊢ (𝑛 = 𝑦 → ∪
𝑘 ∈ (1..^𝑛)𝐵 = ∪ 𝑘 ∈ (1..^𝑦)𝐵) |
43 | 40, 42 | difeq12d 4038 |
. . . . . . . . . . . . . . 15
⊢ (𝑛 = 𝑦 → (𝐴 ∖ ∪
𝑘 ∈ (1..^𝑛)𝐵) = (⦋𝑦 / 𝑛⦌𝐴 ∖ ∪
𝑘 ∈ (1..^𝑦)𝐵)) |
44 | 36, 39, 43 | csbief 3846 |
. . . . . . . . . . . . . 14
⊢
⦋𝑦 /
𝑛⦌(𝐴 ∖ ∪ 𝑘 ∈ (1..^𝑛)𝐵) = (⦋𝑦 / 𝑛⦌𝐴 ∖ ∪
𝑘 ∈ (1..^𝑦)𝐵) |
45 | 35, 44 | ineq12i 4125 |
. . . . . . . . . . . . 13
⊢
(⦋𝑥 /
𝑛⦌(𝐴 ∖ ∪ 𝑘 ∈ (1..^𝑛)𝐵) ∩ ⦋𝑦 / 𝑛⦌(𝐴 ∖ ∪
𝑘 ∈ (1..^𝑛)𝐵)) = ((⦋𝑥 / 𝑛⦌𝐴 ∖ ∪
𝑘 ∈ (1..^𝑥)𝐵) ∩ (⦋𝑦 / 𝑛⦌𝐴 ∖ ∪
𝑘 ∈ (1..^𝑦)𝐵)) |
46 | | simp1 1138 |
. . . . . . . . . . . . . . . . . 18
⊢ ((𝑥 ∈ ℕ ∧ 𝑦 ∈ ℕ ∧ 𝑥 < 𝑦) → 𝑥 ∈ ℕ) |
47 | | nnuz 12477 |
. . . . . . . . . . . . . . . . . 18
⊢ ℕ =
(ℤ≥‘1) |
48 | 46, 47 | eleqtrdi 2848 |
. . . . . . . . . . . . . . . . 17
⊢ ((𝑥 ∈ ℕ ∧ 𝑦 ∈ ℕ ∧ 𝑥 < 𝑦) → 𝑥 ∈
(ℤ≥‘1)) |
49 | | simp2 1139 |
. . . . . . . . . . . . . . . . . 18
⊢ ((𝑥 ∈ ℕ ∧ 𝑦 ∈ ℕ ∧ 𝑥 < 𝑦) → 𝑦 ∈ ℕ) |
50 | 49 | nnzd 12281 |
. . . . . . . . . . . . . . . . 17
⊢ ((𝑥 ∈ ℕ ∧ 𝑦 ∈ ℕ ∧ 𝑥 < 𝑦) → 𝑦 ∈ ℤ) |
51 | | simp3 1140 |
. . . . . . . . . . . . . . . . 17
⊢ ((𝑥 ∈ ℕ ∧ 𝑦 ∈ ℕ ∧ 𝑥 < 𝑦) → 𝑥 < 𝑦) |
52 | | elfzo2 13246 |
. . . . . . . . . . . . . . . . 17
⊢ (𝑥 ∈ (1..^𝑦) ↔ (𝑥 ∈ (ℤ≥‘1)
∧ 𝑦 ∈ ℤ
∧ 𝑥 < 𝑦)) |
53 | 48, 50, 51, 52 | syl3anbrc 1345 |
. . . . . . . . . . . . . . . 16
⊢ ((𝑥 ∈ ℕ ∧ 𝑦 ∈ ℕ ∧ 𝑥 < 𝑦) → 𝑥 ∈ (1..^𝑦)) |
54 | | nfcv 2904 |
. . . . . . . . . . . . . . . . . . . 20
⊢
Ⅎ𝑛𝑘 |
55 | | nfcv 2904 |
. . . . . . . . . . . . . . . . . . . 20
⊢
Ⅎ𝑛𝐵 |
56 | | iundisj.1 |
. . . . . . . . . . . . . . . . . . . 20
⊢ (𝑛 = 𝑘 → 𝐴 = 𝐵) |
57 | 54, 55, 56 | csbhypf 3840 |
. . . . . . . . . . . . . . . . . . 19
⊢ (𝑥 = 𝑘 → ⦋𝑥 / 𝑛⦌𝐴 = 𝐵) |
58 | 57 | equcoms 2028 |
. . . . . . . . . . . . . . . . . 18
⊢ (𝑘 = 𝑥 → ⦋𝑥 / 𝑛⦌𝐴 = 𝐵) |
59 | 58 | eqcomd 2743 |
. . . . . . . . . . . . . . . . 17
⊢ (𝑘 = 𝑥 → 𝐵 = ⦋𝑥 / 𝑛⦌𝐴) |
60 | 59 | ssiun2s 4957 |
. . . . . . . . . . . . . . . 16
⊢ (𝑥 ∈ (1..^𝑦) → ⦋𝑥 / 𝑛⦌𝐴 ⊆ ∪
𝑘 ∈ (1..^𝑦)𝐵) |
61 | 53, 60 | syl 17 |
. . . . . . . . . . . . . . 15
⊢ ((𝑥 ∈ ℕ ∧ 𝑦 ∈ ℕ ∧ 𝑥 < 𝑦) → ⦋𝑥 / 𝑛⦌𝐴 ⊆ ∪
𝑘 ∈ (1..^𝑦)𝐵) |
62 | 61 | ssdifssd 4057 |
. . . . . . . . . . . . . 14
⊢ ((𝑥 ∈ ℕ ∧ 𝑦 ∈ ℕ ∧ 𝑥 < 𝑦) → (⦋𝑥 / 𝑛⦌𝐴 ∖ ∪
𝑘 ∈ (1..^𝑥)𝐵) ⊆ ∪ 𝑘 ∈ (1..^𝑦)𝐵) |
63 | 62 | ssrind 4150 |
. . . . . . . . . . . . 13
⊢ ((𝑥 ∈ ℕ ∧ 𝑦 ∈ ℕ ∧ 𝑥 < 𝑦) → ((⦋𝑥 / 𝑛⦌𝐴 ∖ ∪
𝑘 ∈ (1..^𝑥)𝐵) ∩ (⦋𝑦 / 𝑛⦌𝐴 ∖ ∪
𝑘 ∈ (1..^𝑦)𝐵)) ⊆ (∪ 𝑘 ∈ (1..^𝑦)𝐵 ∩ (⦋𝑦 / 𝑛⦌𝐴 ∖ ∪
𝑘 ∈ (1..^𝑦)𝐵))) |
64 | 45, 63 | eqsstrid 3949 |
. . . . . . . . . . . 12
⊢ ((𝑥 ∈ ℕ ∧ 𝑦 ∈ ℕ ∧ 𝑥 < 𝑦) → (⦋𝑥 / 𝑛⦌(𝐴 ∖ ∪
𝑘 ∈ (1..^𝑛)𝐵) ∩ ⦋𝑦 / 𝑛⦌(𝐴 ∖ ∪
𝑘 ∈ (1..^𝑛)𝐵)) ⊆ (∪ 𝑘 ∈ (1..^𝑦)𝐵 ∩ (⦋𝑦 / 𝑛⦌𝐴 ∖ ∪
𝑘 ∈ (1..^𝑦)𝐵))) |
65 | | disjdif 4386 |
. . . . . . . . . . . 12
⊢ (∪ 𝑘 ∈ (1..^𝑦)𝐵 ∩ (⦋𝑦 / 𝑛⦌𝐴 ∖ ∪
𝑘 ∈ (1..^𝑦)𝐵)) = ∅ |
66 | | sseq0 4314 |
. . . . . . . . . . . 12
⊢
(((⦋𝑥
/ 𝑛⦌(𝐴 ∖ ∪ 𝑘 ∈ (1..^𝑛)𝐵) ∩ ⦋𝑦 / 𝑛⦌(𝐴 ∖ ∪
𝑘 ∈ (1..^𝑛)𝐵)) ⊆ (∪ 𝑘 ∈ (1..^𝑦)𝐵 ∩ (⦋𝑦 / 𝑛⦌𝐴 ∖ ∪
𝑘 ∈ (1..^𝑦)𝐵)) ∧ (∪ 𝑘 ∈ (1..^𝑦)𝐵 ∩ (⦋𝑦 / 𝑛⦌𝐴 ∖ ∪
𝑘 ∈ (1..^𝑦)𝐵)) = ∅) → (⦋𝑥 / 𝑛⦌(𝐴 ∖ ∪
𝑘 ∈ (1..^𝑛)𝐵) ∩ ⦋𝑦 / 𝑛⦌(𝐴 ∖ ∪
𝑘 ∈ (1..^𝑛)𝐵)) = ∅) |
67 | 64, 65, 66 | sylancl 589 |
. . . . . . . . . . 11
⊢ ((𝑥 ∈ ℕ ∧ 𝑦 ∈ ℕ ∧ 𝑥 < 𝑦) → (⦋𝑥 / 𝑛⦌(𝐴 ∖ ∪
𝑘 ∈ (1..^𝑛)𝐵) ∩ ⦋𝑦 / 𝑛⦌(𝐴 ∖ ∪
𝑘 ∈ (1..^𝑛)𝐵)) = ∅) |
68 | 67 | 3expia 1123 |
. . . . . . . . . 10
⊢ ((𝑥 ∈ ℕ ∧ 𝑦 ∈ ℕ) → (𝑥 < 𝑦 → (⦋𝑥 / 𝑛⦌(𝐴 ∖ ∪
𝑘 ∈ (1..^𝑛)𝐵) ∩ ⦋𝑦 / 𝑛⦌(𝐴 ∖ ∪
𝑘 ∈ (1..^𝑛)𝐵)) = ∅)) |
69 | 68 | 3adant3 1134 |
. . . . . . . . 9
⊢ ((𝑥 ∈ ℕ ∧ 𝑦 ∈ ℕ ∧ 𝑥 ≤ 𝑦) → (𝑥 < 𝑦 → (⦋𝑥 / 𝑛⦌(𝐴 ∖ ∪
𝑘 ∈ (1..^𝑛)𝐵) ∩ ⦋𝑦 / 𝑛⦌(𝐴 ∖ ∪
𝑘 ∈ (1..^𝑛)𝐵)) = ∅)) |
70 | 26, 69 | sylbird 263 |
. . . . . . . 8
⊢ ((𝑥 ∈ ℕ ∧ 𝑦 ∈ ℕ ∧ 𝑥 ≤ 𝑦) → (𝑦 ≠ 𝑥 → (⦋𝑥 / 𝑛⦌(𝐴 ∖ ∪
𝑘 ∈ (1..^𝑛)𝐵) ∩ ⦋𝑦 / 𝑛⦌(𝐴 ∖ ∪
𝑘 ∈ (1..^𝑛)𝐵)) = ∅)) |
71 | 21, 70 | syl5bir 246 |
. . . . . . 7
⊢ ((𝑥 ∈ ℕ ∧ 𝑦 ∈ ℕ ∧ 𝑥 ≤ 𝑦) → (¬ 𝑥 = 𝑦 → (⦋𝑥 / 𝑛⦌(𝐴 ∖ ∪
𝑘 ∈ (1..^𝑛)𝐵) ∩ ⦋𝑦 / 𝑛⦌(𝐴 ∖ ∪
𝑘 ∈ (1..^𝑛)𝐵)) = ∅)) |
72 | 71 | orrd 863 |
. . . . . 6
⊢ ((𝑥 ∈ ℕ ∧ 𝑦 ∈ ℕ ∧ 𝑥 ≤ 𝑦) → (𝑥 = 𝑦 ∨ (⦋𝑥 / 𝑛⦌(𝐴 ∖ ∪
𝑘 ∈ (1..^𝑛)𝐵) ∩ ⦋𝑦 / 𝑛⦌(𝐴 ∖ ∪
𝑘 ∈ (1..^𝑛)𝐵)) = ∅)) |
73 | 72 | adantl 485 |
. . . . 5
⊢
((⊤ ∧ (𝑥
∈ ℕ ∧ 𝑦
∈ ℕ ∧ 𝑥 ≤
𝑦)) → (𝑥 = 𝑦 ∨ (⦋𝑥 / 𝑛⦌(𝐴 ∖ ∪
𝑘 ∈ (1..^𝑛)𝐵) ∩ ⦋𝑦 / 𝑛⦌(𝐴 ∖ ∪
𝑘 ∈ (1..^𝑛)𝐵)) = ∅)) |
74 | 7, 17, 19, 20, 73 | wlogle 11365 |
. . . 4
⊢
((⊤ ∧ (𝑥
∈ ℕ ∧ 𝑦
∈ ℕ)) → (𝑥
= 𝑦 ∨
(⦋𝑥 / 𝑛⦌(𝐴 ∖ ∪ 𝑘 ∈ (1..^𝑛)𝐵) ∩ ⦋𝑦 / 𝑛⦌(𝐴 ∖ ∪
𝑘 ∈ (1..^𝑛)𝐵)) = ∅)) |
75 | 1, 74 | mpan 690 |
. . 3
⊢ ((𝑥 ∈ ℕ ∧ 𝑦 ∈ ℕ) → (𝑥 = 𝑦 ∨ (⦋𝑥 / 𝑛⦌(𝐴 ∖ ∪
𝑘 ∈ (1..^𝑛)𝐵) ∩ ⦋𝑦 / 𝑛⦌(𝐴 ∖ ∪
𝑘 ∈ (1..^𝑛)𝐵)) = ∅)) |
76 | 75 | rgen2 3124 |
. 2
⊢
∀𝑥 ∈
ℕ ∀𝑦 ∈
ℕ (𝑥 = 𝑦 ∨ (⦋𝑥 / 𝑛⦌(𝐴 ∖ ∪
𝑘 ∈ (1..^𝑛)𝐵) ∩ ⦋𝑦 / 𝑛⦌(𝐴 ∖ ∪
𝑘 ∈ (1..^𝑛)𝐵)) = ∅) |
77 | | disjors 5034 |
. 2
⊢
(Disj 𝑛
∈ ℕ (𝐴 ∖
∪ 𝑘 ∈ (1..^𝑛)𝐵) ↔ ∀𝑥 ∈ ℕ ∀𝑦 ∈ ℕ (𝑥 = 𝑦 ∨ (⦋𝑥 / 𝑛⦌(𝐴 ∖ ∪
𝑘 ∈ (1..^𝑛)𝐵) ∩ ⦋𝑦 / 𝑛⦌(𝐴 ∖ ∪
𝑘 ∈ (1..^𝑛)𝐵)) = ∅)) |
78 | 76, 77 | mpbir 234 |
1
⊢
Disj 𝑛 ∈
ℕ (𝐴 ∖ ∪ 𝑘 ∈ (1..^𝑛)𝐵) |