Step | Hyp | Ref
| Expression |
1 | | tru 1546 |
. . . 4
⊢
⊤ |
2 | | eqeq12 2753 |
. . . . . 6
⊢ ((𝑎 = 𝑥 ∧ 𝑏 = 𝑦) → (𝑎 = 𝑏 ↔ 𝑥 = 𝑦)) |
3 | | csbeq1 3803 |
. . . . . . . 8
⊢ (𝑎 = 𝑥 → ⦋𝑎 / 𝑛⦌(𝐴 ∖ ∪
𝑘 ∈ (1..^𝑛)𝐵) = ⦋𝑥 / 𝑛⦌(𝐴 ∖ ∪
𝑘 ∈ (1..^𝑛)𝐵)) |
4 | | csbeq1 3803 |
. . . . . . . 8
⊢ (𝑏 = 𝑦 → ⦋𝑏 / 𝑛⦌(𝐴 ∖ ∪
𝑘 ∈ (1..^𝑛)𝐵) = ⦋𝑦 / 𝑛⦌(𝐴 ∖ ∪
𝑘 ∈ (1..^𝑛)𝐵)) |
5 | 3, 4 | ineqan12d 4115 |
. . . . . . 7
⊢ ((𝑎 = 𝑥 ∧ 𝑏 = 𝑦) → (⦋𝑎 / 𝑛⦌(𝐴 ∖ ∪
𝑘 ∈ (1..^𝑛)𝐵) ∩ ⦋𝑏 / 𝑛⦌(𝐴 ∖ ∪
𝑘 ∈ (1..^𝑛)𝐵)) = (⦋𝑥 / 𝑛⦌(𝐴 ∖ ∪
𝑘 ∈ (1..^𝑛)𝐵) ∩ ⦋𝑦 / 𝑛⦌(𝐴 ∖ ∪
𝑘 ∈ (1..^𝑛)𝐵))) |
6 | 5 | eqeq1d 2741 |
. . . . . 6
⊢ ((𝑎 = 𝑥 ∧ 𝑏 = 𝑦) → ((⦋𝑎 / 𝑛⦌(𝐴 ∖ ∪
𝑘 ∈ (1..^𝑛)𝐵) ∩ ⦋𝑏 / 𝑛⦌(𝐴 ∖ ∪
𝑘 ∈ (1..^𝑛)𝐵)) = ∅ ↔ (⦋𝑥 / 𝑛⦌(𝐴 ∖ ∪
𝑘 ∈ (1..^𝑛)𝐵) ∩ ⦋𝑦 / 𝑛⦌(𝐴 ∖ ∪
𝑘 ∈ (1..^𝑛)𝐵)) = ∅)) |
7 | 2, 6 | orbi12d 918 |
. . . . 5
⊢ ((𝑎 = 𝑥 ∧ 𝑏 = 𝑦) → ((𝑎 = 𝑏 ∨ (⦋𝑎 / 𝑛⦌(𝐴 ∖ ∪
𝑘 ∈ (1..^𝑛)𝐵) ∩ ⦋𝑏 / 𝑛⦌(𝐴 ∖ ∪
𝑘 ∈ (1..^𝑛)𝐵)) = ∅) ↔ (𝑥 = 𝑦 ∨ (⦋𝑥 / 𝑛⦌(𝐴 ∖ ∪
𝑘 ∈ (1..^𝑛)𝐵) ∩ ⦋𝑦 / 𝑛⦌(𝐴 ∖ ∪
𝑘 ∈ (1..^𝑛)𝐵)) = ∅))) |
8 | | eqeq12 2753 |
. . . . . . 7
⊢ ((𝑎 = 𝑦 ∧ 𝑏 = 𝑥) → (𝑎 = 𝑏 ↔ 𝑦 = 𝑥)) |
9 | | equcom 2030 |
. . . . . . 7
⊢ (𝑦 = 𝑥 ↔ 𝑥 = 𝑦) |
10 | 8, 9 | bitrdi 290 |
. . . . . 6
⊢ ((𝑎 = 𝑦 ∧ 𝑏 = 𝑥) → (𝑎 = 𝑏 ↔ 𝑥 = 𝑦)) |
11 | | csbeq1 3803 |
. . . . . . . . 9
⊢ (𝑎 = 𝑦 → ⦋𝑎 / 𝑛⦌(𝐴 ∖ ∪
𝑘 ∈ (1..^𝑛)𝐵) = ⦋𝑦 / 𝑛⦌(𝐴 ∖ ∪
𝑘 ∈ (1..^𝑛)𝐵)) |
12 | | csbeq1 3803 |
. . . . . . . . 9
⊢ (𝑏 = 𝑥 → ⦋𝑏 / 𝑛⦌(𝐴 ∖ ∪
𝑘 ∈ (1..^𝑛)𝐵) = ⦋𝑥 / 𝑛⦌(𝐴 ∖ ∪
𝑘 ∈ (1..^𝑛)𝐵)) |
13 | 11, 12 | ineqan12d 4115 |
. . . . . . . 8
⊢ ((𝑎 = 𝑦 ∧ 𝑏 = 𝑥) → (⦋𝑎 / 𝑛⦌(𝐴 ∖ ∪
𝑘 ∈ (1..^𝑛)𝐵) ∩ ⦋𝑏 / 𝑛⦌(𝐴 ∖ ∪
𝑘 ∈ (1..^𝑛)𝐵)) = (⦋𝑦 / 𝑛⦌(𝐴 ∖ ∪
𝑘 ∈ (1..^𝑛)𝐵) ∩ ⦋𝑥 / 𝑛⦌(𝐴 ∖ ∪
𝑘 ∈ (1..^𝑛)𝐵))) |
14 | | incom 4101 |
. . . . . . . 8
⊢
(⦋𝑦 /
𝑛⦌(𝐴 ∖ ∪ 𝑘 ∈ (1..^𝑛)𝐵) ∩ ⦋𝑥 / 𝑛⦌(𝐴 ∖ ∪
𝑘 ∈ (1..^𝑛)𝐵)) = (⦋𝑥 / 𝑛⦌(𝐴 ∖ ∪
𝑘 ∈ (1..^𝑛)𝐵) ∩ ⦋𝑦 / 𝑛⦌(𝐴 ∖ ∪
𝑘 ∈ (1..^𝑛)𝐵)) |
15 | 13, 14 | eqtrdi 2790 |
. . . . . . 7
⊢ ((𝑎 = 𝑦 ∧ 𝑏 = 𝑥) → (⦋𝑎 / 𝑛⦌(𝐴 ∖ ∪
𝑘 ∈ (1..^𝑛)𝐵) ∩ ⦋𝑏 / 𝑛⦌(𝐴 ∖ ∪
𝑘 ∈ (1..^𝑛)𝐵)) = (⦋𝑥 / 𝑛⦌(𝐴 ∖ ∪
𝑘 ∈ (1..^𝑛)𝐵) ∩ ⦋𝑦 / 𝑛⦌(𝐴 ∖ ∪
𝑘 ∈ (1..^𝑛)𝐵))) |
16 | 15 | eqeq1d 2741 |
. . . . . 6
⊢ ((𝑎 = 𝑦 ∧ 𝑏 = 𝑥) → ((⦋𝑎 / 𝑛⦌(𝐴 ∖ ∪
𝑘 ∈ (1..^𝑛)𝐵) ∩ ⦋𝑏 / 𝑛⦌(𝐴 ∖ ∪
𝑘 ∈ (1..^𝑛)𝐵)) = ∅ ↔ (⦋𝑥 / 𝑛⦌(𝐴 ∖ ∪
𝑘 ∈ (1..^𝑛)𝐵) ∩ ⦋𝑦 / 𝑛⦌(𝐴 ∖ ∪
𝑘 ∈ (1..^𝑛)𝐵)) = ∅)) |
17 | 10, 16 | orbi12d 918 |
. . . . 5
⊢ ((𝑎 = 𝑦 ∧ 𝑏 = 𝑥) → ((𝑎 = 𝑏 ∨ (⦋𝑎 / 𝑛⦌(𝐴 ∖ ∪
𝑘 ∈ (1..^𝑛)𝐵) ∩ ⦋𝑏 / 𝑛⦌(𝐴 ∖ ∪
𝑘 ∈ (1..^𝑛)𝐵)) = ∅) ↔ (𝑥 = 𝑦 ∨ (⦋𝑥 / 𝑛⦌(𝐴 ∖ ∪
𝑘 ∈ (1..^𝑛)𝐵) ∩ ⦋𝑦 / 𝑛⦌(𝐴 ∖ ∪
𝑘 ∈ (1..^𝑛)𝐵)) = ∅))) |
18 | | nnssre 11733 |
. . . . . 6
⊢ ℕ
⊆ ℝ |
19 | 18 | a1i 11 |
. . . . 5
⊢ (⊤
→ ℕ ⊆ ℝ) |
20 | | biidd 265 |
. . . . 5
⊢
((⊤ ∧ (𝑥
∈ ℕ ∧ 𝑦
∈ ℕ)) → ((𝑥
= 𝑦 ∨
(⦋𝑥 / 𝑛⦌(𝐴 ∖ ∪ 𝑘 ∈ (1..^𝑛)𝐵) ∩ ⦋𝑦 / 𝑛⦌(𝐴 ∖ ∪
𝑘 ∈ (1..^𝑛)𝐵)) = ∅) ↔ (𝑥 = 𝑦 ∨ (⦋𝑥 / 𝑛⦌(𝐴 ∖ ∪
𝑘 ∈ (1..^𝑛)𝐵) ∩ ⦋𝑦 / 𝑛⦌(𝐴 ∖ ∪
𝑘 ∈ (1..^𝑛)𝐵)) = ∅))) |
21 | | nesym 2991 |
. . . . . . . 8
⊢ (𝑦 ≠ 𝑥 ↔ ¬ 𝑥 = 𝑦) |
22 | | nnre 11736 |
. . . . . . . . . 10
⊢ (𝑥 ∈ ℕ → 𝑥 ∈
ℝ) |
23 | | nnre 11736 |
. . . . . . . . . 10
⊢ (𝑦 ∈ ℕ → 𝑦 ∈
ℝ) |
24 | | id 22 |
. . . . . . . . . 10
⊢ (𝑥 ≤ 𝑦 → 𝑥 ≤ 𝑦) |
25 | | leltne 10821 |
. . . . . . . . . 10
⊢ ((𝑥 ∈ ℝ ∧ 𝑦 ∈ ℝ ∧ 𝑥 ≤ 𝑦) → (𝑥 < 𝑦 ↔ 𝑦 ≠ 𝑥)) |
26 | 22, 23, 24, 25 | syl3an 1161 |
. . . . . . . . 9
⊢ ((𝑥 ∈ ℕ ∧ 𝑦 ∈ ℕ ∧ 𝑥 ≤ 𝑦) → (𝑥 < 𝑦 ↔ 𝑦 ≠ 𝑥)) |
27 | | vex 3404 |
. . . . . . . . . . . . . . 15
⊢ 𝑥 ∈ V |
28 | | nfcsb1v 3824 |
. . . . . . . . . . . . . . . 16
⊢
Ⅎ𝑛⦋𝑥 / 𝑛⦌𝐴 |
29 | | nfcv 2900 |
. . . . . . . . . . . . . . . . 17
⊢
Ⅎ𝑛(1..^𝑥) |
30 | | iundisjf.2 |
. . . . . . . . . . . . . . . . 17
⊢
Ⅎ𝑛𝐵 |
31 | 29, 30 | nfiun 4921 |
. . . . . . . . . . . . . . . 16
⊢
Ⅎ𝑛∪ 𝑘 ∈ (1..^𝑥)𝐵 |
32 | 28, 31 | nfdif 4026 |
. . . . . . . . . . . . . . 15
⊢
Ⅎ𝑛(⦋𝑥 / 𝑛⦌𝐴 ∖ ∪
𝑘 ∈ (1..^𝑥)𝐵) |
33 | | csbeq1a 3814 |
. . . . . . . . . . . . . . . 16
⊢ (𝑛 = 𝑥 → 𝐴 = ⦋𝑥 / 𝑛⦌𝐴) |
34 | | oveq2 7191 |
. . . . . . . . . . . . . . . . 17
⊢ (𝑛 = 𝑥 → (1..^𝑛) = (1..^𝑥)) |
35 | 34 | iuneq1d 4918 |
. . . . . . . . . . . . . . . 16
⊢ (𝑛 = 𝑥 → ∪
𝑘 ∈ (1..^𝑛)𝐵 = ∪ 𝑘 ∈ (1..^𝑥)𝐵) |
36 | 33, 35 | difeq12d 4024 |
. . . . . . . . . . . . . . 15
⊢ (𝑛 = 𝑥 → (𝐴 ∖ ∪
𝑘 ∈ (1..^𝑛)𝐵) = (⦋𝑥 / 𝑛⦌𝐴 ∖ ∪
𝑘 ∈ (1..^𝑥)𝐵)) |
37 | 27, 32, 36 | csbief 3834 |
. . . . . . . . . . . . . 14
⊢
⦋𝑥 /
𝑛⦌(𝐴 ∖ ∪ 𝑘 ∈ (1..^𝑛)𝐵) = (⦋𝑥 / 𝑛⦌𝐴 ∖ ∪
𝑘 ∈ (1..^𝑥)𝐵) |
38 | | vex 3404 |
. . . . . . . . . . . . . . 15
⊢ 𝑦 ∈ V |
39 | | nfcsb1v 3824 |
. . . . . . . . . . . . . . . 16
⊢
Ⅎ𝑛⦋𝑦 / 𝑛⦌𝐴 |
40 | | nfcv 2900 |
. . . . . . . . . . . . . . . . 17
⊢
Ⅎ𝑛(1..^𝑦) |
41 | 40, 30 | nfiun 4921 |
. . . . . . . . . . . . . . . 16
⊢
Ⅎ𝑛∪ 𝑘 ∈ (1..^𝑦)𝐵 |
42 | 39, 41 | nfdif 4026 |
. . . . . . . . . . . . . . 15
⊢
Ⅎ𝑛(⦋𝑦 / 𝑛⦌𝐴 ∖ ∪
𝑘 ∈ (1..^𝑦)𝐵) |
43 | | csbeq1a 3814 |
. . . . . . . . . . . . . . . 16
⊢ (𝑛 = 𝑦 → 𝐴 = ⦋𝑦 / 𝑛⦌𝐴) |
44 | | oveq2 7191 |
. . . . . . . . . . . . . . . . 17
⊢ (𝑛 = 𝑦 → (1..^𝑛) = (1..^𝑦)) |
45 | 44 | iuneq1d 4918 |
. . . . . . . . . . . . . . . 16
⊢ (𝑛 = 𝑦 → ∪
𝑘 ∈ (1..^𝑛)𝐵 = ∪ 𝑘 ∈ (1..^𝑦)𝐵) |
46 | 43, 45 | difeq12d 4024 |
. . . . . . . . . . . . . . 15
⊢ (𝑛 = 𝑦 → (𝐴 ∖ ∪
𝑘 ∈ (1..^𝑛)𝐵) = (⦋𝑦 / 𝑛⦌𝐴 ∖ ∪
𝑘 ∈ (1..^𝑦)𝐵)) |
47 | 38, 42, 46 | csbief 3834 |
. . . . . . . . . . . . . 14
⊢
⦋𝑦 /
𝑛⦌(𝐴 ∖ ∪ 𝑘 ∈ (1..^𝑛)𝐵) = (⦋𝑦 / 𝑛⦌𝐴 ∖ ∪
𝑘 ∈ (1..^𝑦)𝐵) |
48 | 37, 47 | ineq12i 4111 |
. . . . . . . . . . . . 13
⊢
(⦋𝑥 /
𝑛⦌(𝐴 ∖ ∪ 𝑘 ∈ (1..^𝑛)𝐵) ∩ ⦋𝑦 / 𝑛⦌(𝐴 ∖ ∪
𝑘 ∈ (1..^𝑛)𝐵)) = ((⦋𝑥 / 𝑛⦌𝐴 ∖ ∪
𝑘 ∈ (1..^𝑥)𝐵) ∩ (⦋𝑦 / 𝑛⦌𝐴 ∖ ∪
𝑘 ∈ (1..^𝑦)𝐵)) |
49 | | simp1 1137 |
. . . . . . . . . . . . . . . . . 18
⊢ ((𝑥 ∈ ℕ ∧ 𝑦 ∈ ℕ ∧ 𝑥 < 𝑦) → 𝑥 ∈ ℕ) |
50 | | nnuz 12376 |
. . . . . . . . . . . . . . . . . 18
⊢ ℕ =
(ℤ≥‘1) |
51 | 49, 50 | eleqtrdi 2844 |
. . . . . . . . . . . . . . . . 17
⊢ ((𝑥 ∈ ℕ ∧ 𝑦 ∈ ℕ ∧ 𝑥 < 𝑦) → 𝑥 ∈
(ℤ≥‘1)) |
52 | | simp2 1138 |
. . . . . . . . . . . . . . . . . 18
⊢ ((𝑥 ∈ ℕ ∧ 𝑦 ∈ ℕ ∧ 𝑥 < 𝑦) → 𝑦 ∈ ℕ) |
53 | 52 | nnzd 12180 |
. . . . . . . . . . . . . . . . 17
⊢ ((𝑥 ∈ ℕ ∧ 𝑦 ∈ ℕ ∧ 𝑥 < 𝑦) → 𝑦 ∈ ℤ) |
54 | | simp3 1139 |
. . . . . . . . . . . . . . . . 17
⊢ ((𝑥 ∈ ℕ ∧ 𝑦 ∈ ℕ ∧ 𝑥 < 𝑦) → 𝑥 < 𝑦) |
55 | | elfzo2 13145 |
. . . . . . . . . . . . . . . . 17
⊢ (𝑥 ∈ (1..^𝑦) ↔ (𝑥 ∈ (ℤ≥‘1)
∧ 𝑦 ∈ ℤ
∧ 𝑥 < 𝑦)) |
56 | 51, 53, 54, 55 | syl3anbrc 1344 |
. . . . . . . . . . . . . . . 16
⊢ ((𝑥 ∈ ℕ ∧ 𝑦 ∈ ℕ ∧ 𝑥 < 𝑦) → 𝑥 ∈ (1..^𝑦)) |
57 | | nfcv 2900 |
. . . . . . . . . . . . . . . . 17
⊢
Ⅎ𝑘(1..^𝑦) |
58 | | nfcv 2900 |
. . . . . . . . . . . . . . . . 17
⊢
Ⅎ𝑘𝑥 |
59 | | iundisjf.1 |
. . . . . . . . . . . . . . . . . 18
⊢
Ⅎ𝑘𝐴 |
60 | 58, 59 | nfcsbw 3826 |
. . . . . . . . . . . . . . . . 17
⊢
Ⅎ𝑘⦋𝑥 / 𝑛⦌𝐴 |
61 | | nfcv 2900 |
. . . . . . . . . . . . . . . . . . . 20
⊢
Ⅎ𝑛𝑘 |
62 | | iundisjf.3 |
. . . . . . . . . . . . . . . . . . . 20
⊢ (𝑛 = 𝑘 → 𝐴 = 𝐵) |
63 | 61, 30, 62 | csbhypf 3828 |
. . . . . . . . . . . . . . . . . . 19
⊢ (𝑥 = 𝑘 → ⦋𝑥 / 𝑛⦌𝐴 = 𝐵) |
64 | 63 | equcoms 2032 |
. . . . . . . . . . . . . . . . . 18
⊢ (𝑘 = 𝑥 → ⦋𝑥 / 𝑛⦌𝐴 = 𝐵) |
65 | 64 | eqcomd 2745 |
. . . . . . . . . . . . . . . . 17
⊢ (𝑘 = 𝑥 → 𝐵 = ⦋𝑥 / 𝑛⦌𝐴) |
66 | 57, 58, 60, 65 | ssiun2sf 30486 |
. . . . . . . . . . . . . . . 16
⊢ (𝑥 ∈ (1..^𝑦) → ⦋𝑥 / 𝑛⦌𝐴 ⊆ ∪
𝑘 ∈ (1..^𝑦)𝐵) |
67 | 56, 66 | syl 17 |
. . . . . . . . . . . . . . 15
⊢ ((𝑥 ∈ ℕ ∧ 𝑦 ∈ ℕ ∧ 𝑥 < 𝑦) → ⦋𝑥 / 𝑛⦌𝐴 ⊆ ∪
𝑘 ∈ (1..^𝑦)𝐵) |
68 | 67 | ssdifssd 4043 |
. . . . . . . . . . . . . 14
⊢ ((𝑥 ∈ ℕ ∧ 𝑦 ∈ ℕ ∧ 𝑥 < 𝑦) → (⦋𝑥 / 𝑛⦌𝐴 ∖ ∪
𝑘 ∈ (1..^𝑥)𝐵) ⊆ ∪ 𝑘 ∈ (1..^𝑦)𝐵) |
69 | 68 | ssrind 4136 |
. . . . . . . . . . . . 13
⊢ ((𝑥 ∈ ℕ ∧ 𝑦 ∈ ℕ ∧ 𝑥 < 𝑦) → ((⦋𝑥 / 𝑛⦌𝐴 ∖ ∪
𝑘 ∈ (1..^𝑥)𝐵) ∩ (⦋𝑦 / 𝑛⦌𝐴 ∖ ∪
𝑘 ∈ (1..^𝑦)𝐵)) ⊆ (∪ 𝑘 ∈ (1..^𝑦)𝐵 ∩ (⦋𝑦 / 𝑛⦌𝐴 ∖ ∪
𝑘 ∈ (1..^𝑦)𝐵))) |
70 | 48, 69 | eqsstrid 3935 |
. . . . . . . . . . . 12
⊢ ((𝑥 ∈ ℕ ∧ 𝑦 ∈ ℕ ∧ 𝑥 < 𝑦) → (⦋𝑥 / 𝑛⦌(𝐴 ∖ ∪
𝑘 ∈ (1..^𝑛)𝐵) ∩ ⦋𝑦 / 𝑛⦌(𝐴 ∖ ∪
𝑘 ∈ (1..^𝑛)𝐵)) ⊆ (∪ 𝑘 ∈ (1..^𝑦)𝐵 ∩ (⦋𝑦 / 𝑛⦌𝐴 ∖ ∪
𝑘 ∈ (1..^𝑦)𝐵))) |
71 | | disjdif 4371 |
. . . . . . . . . . . 12
⊢ (∪ 𝑘 ∈ (1..^𝑦)𝐵 ∩ (⦋𝑦 / 𝑛⦌𝐴 ∖ ∪
𝑘 ∈ (1..^𝑦)𝐵)) = ∅ |
72 | | sseq0 4298 |
. . . . . . . . . . . 12
⊢
(((⦋𝑥
/ 𝑛⦌(𝐴 ∖ ∪ 𝑘 ∈ (1..^𝑛)𝐵) ∩ ⦋𝑦 / 𝑛⦌(𝐴 ∖ ∪
𝑘 ∈ (1..^𝑛)𝐵)) ⊆ (∪ 𝑘 ∈ (1..^𝑦)𝐵 ∩ (⦋𝑦 / 𝑛⦌𝐴 ∖ ∪
𝑘 ∈ (1..^𝑦)𝐵)) ∧ (∪ 𝑘 ∈ (1..^𝑦)𝐵 ∩ (⦋𝑦 / 𝑛⦌𝐴 ∖ ∪
𝑘 ∈ (1..^𝑦)𝐵)) = ∅) → (⦋𝑥 / 𝑛⦌(𝐴 ∖ ∪
𝑘 ∈ (1..^𝑛)𝐵) ∩ ⦋𝑦 / 𝑛⦌(𝐴 ∖ ∪
𝑘 ∈ (1..^𝑛)𝐵)) = ∅) |
73 | 70, 71, 72 | sylancl 589 |
. . . . . . . . . . 11
⊢ ((𝑥 ∈ ℕ ∧ 𝑦 ∈ ℕ ∧ 𝑥 < 𝑦) → (⦋𝑥 / 𝑛⦌(𝐴 ∖ ∪
𝑘 ∈ (1..^𝑛)𝐵) ∩ ⦋𝑦 / 𝑛⦌(𝐴 ∖ ∪
𝑘 ∈ (1..^𝑛)𝐵)) = ∅) |
74 | 73 | 3expia 1122 |
. . . . . . . . . 10
⊢ ((𝑥 ∈ ℕ ∧ 𝑦 ∈ ℕ) → (𝑥 < 𝑦 → (⦋𝑥 / 𝑛⦌(𝐴 ∖ ∪
𝑘 ∈ (1..^𝑛)𝐵) ∩ ⦋𝑦 / 𝑛⦌(𝐴 ∖ ∪
𝑘 ∈ (1..^𝑛)𝐵)) = ∅)) |
75 | 74 | 3adant3 1133 |
. . . . . . . . 9
⊢ ((𝑥 ∈ ℕ ∧ 𝑦 ∈ ℕ ∧ 𝑥 ≤ 𝑦) → (𝑥 < 𝑦 → (⦋𝑥 / 𝑛⦌(𝐴 ∖ ∪
𝑘 ∈ (1..^𝑛)𝐵) ∩ ⦋𝑦 / 𝑛⦌(𝐴 ∖ ∪
𝑘 ∈ (1..^𝑛)𝐵)) = ∅)) |
76 | 26, 75 | sylbird 263 |
. . . . . . . 8
⊢ ((𝑥 ∈ ℕ ∧ 𝑦 ∈ ℕ ∧ 𝑥 ≤ 𝑦) → (𝑦 ≠ 𝑥 → (⦋𝑥 / 𝑛⦌(𝐴 ∖ ∪
𝑘 ∈ (1..^𝑛)𝐵) ∩ ⦋𝑦 / 𝑛⦌(𝐴 ∖ ∪
𝑘 ∈ (1..^𝑛)𝐵)) = ∅)) |
77 | 21, 76 | syl5bir 246 |
. . . . . . 7
⊢ ((𝑥 ∈ ℕ ∧ 𝑦 ∈ ℕ ∧ 𝑥 ≤ 𝑦) → (¬ 𝑥 = 𝑦 → (⦋𝑥 / 𝑛⦌(𝐴 ∖ ∪
𝑘 ∈ (1..^𝑛)𝐵) ∩ ⦋𝑦 / 𝑛⦌(𝐴 ∖ ∪
𝑘 ∈ (1..^𝑛)𝐵)) = ∅)) |
78 | 77 | orrd 862 |
. . . . . 6
⊢ ((𝑥 ∈ ℕ ∧ 𝑦 ∈ ℕ ∧ 𝑥 ≤ 𝑦) → (𝑥 = 𝑦 ∨ (⦋𝑥 / 𝑛⦌(𝐴 ∖ ∪
𝑘 ∈ (1..^𝑛)𝐵) ∩ ⦋𝑦 / 𝑛⦌(𝐴 ∖ ∪
𝑘 ∈ (1..^𝑛)𝐵)) = ∅)) |
79 | 78 | adantl 485 |
. . . . 5
⊢
((⊤ ∧ (𝑥
∈ ℕ ∧ 𝑦
∈ ℕ ∧ 𝑥 ≤
𝑦)) → (𝑥 = 𝑦 ∨ (⦋𝑥 / 𝑛⦌(𝐴 ∖ ∪
𝑘 ∈ (1..^𝑛)𝐵) ∩ ⦋𝑦 / 𝑛⦌(𝐴 ∖ ∪
𝑘 ∈ (1..^𝑛)𝐵)) = ∅)) |
80 | 7, 17, 19, 20, 79 | wlogle 11264 |
. . . 4
⊢
((⊤ ∧ (𝑥
∈ ℕ ∧ 𝑦
∈ ℕ)) → (𝑥
= 𝑦 ∨
(⦋𝑥 / 𝑛⦌(𝐴 ∖ ∪ 𝑘 ∈ (1..^𝑛)𝐵) ∩ ⦋𝑦 / 𝑛⦌(𝐴 ∖ ∪
𝑘 ∈ (1..^𝑛)𝐵)) = ∅)) |
81 | 1, 80 | mpan 690 |
. . 3
⊢ ((𝑥 ∈ ℕ ∧ 𝑦 ∈ ℕ) → (𝑥 = 𝑦 ∨ (⦋𝑥 / 𝑛⦌(𝐴 ∖ ∪
𝑘 ∈ (1..^𝑛)𝐵) ∩ ⦋𝑦 / 𝑛⦌(𝐴 ∖ ∪
𝑘 ∈ (1..^𝑛)𝐵)) = ∅)) |
82 | 81 | rgen2 3116 |
. 2
⊢
∀𝑥 ∈
ℕ ∀𝑦 ∈
ℕ (𝑥 = 𝑦 ∨ (⦋𝑥 / 𝑛⦌(𝐴 ∖ ∪
𝑘 ∈ (1..^𝑛)𝐵) ∩ ⦋𝑦 / 𝑛⦌(𝐴 ∖ ∪
𝑘 ∈ (1..^𝑛)𝐵)) = ∅) |
83 | | disjors 5021 |
. 2
⊢
(Disj 𝑛
∈ ℕ (𝐴 ∖
∪ 𝑘 ∈ (1..^𝑛)𝐵) ↔ ∀𝑥 ∈ ℕ ∀𝑦 ∈ ℕ (𝑥 = 𝑦 ∨ (⦋𝑥 / 𝑛⦌(𝐴 ∖ ∪
𝑘 ∈ (1..^𝑛)𝐵) ∩ ⦋𝑦 / 𝑛⦌(𝐴 ∖ ∪
𝑘 ∈ (1..^𝑛)𝐵)) = ∅)) |
84 | 82, 83 | mpbir 234 |
1
⊢
Disj 𝑛 ∈
ℕ (𝐴 ∖ ∪ 𝑘 ∈ (1..^𝑛)𝐵) |