Step | Hyp | Ref
| Expression |
1 | | ssrab2 4018 |
. . . . . . 7
⊢ {𝑛 ∈ (1..^𝑁) ∣ 𝑥 ∈ 𝐴} ⊆ (1..^𝑁) |
2 | | fzossnn 13434 |
. . . . . . . . . 10
⊢
(1..^𝑁) ⊆
ℕ |
3 | | nnuz 12620 |
. . . . . . . . . 10
⊢ ℕ =
(ℤ≥‘1) |
4 | 2, 3 | sseqtri 3962 |
. . . . . . . . 9
⊢
(1..^𝑁) ⊆
(ℤ≥‘1) |
5 | 1, 4 | sstri 3935 |
. . . . . . . 8
⊢ {𝑛 ∈ (1..^𝑁) ∣ 𝑥 ∈ 𝐴} ⊆
(ℤ≥‘1) |
6 | | rabn0 4325 |
. . . . . . . . 9
⊢ ({𝑛 ∈ (1..^𝑁) ∣ 𝑥 ∈ 𝐴} ≠ ∅ ↔ ∃𝑛 ∈ (1..^𝑁)𝑥 ∈ 𝐴) |
7 | 6 | biimpri 227 |
. . . . . . . 8
⊢
(∃𝑛 ∈
(1..^𝑁)𝑥 ∈ 𝐴 → {𝑛 ∈ (1..^𝑁) ∣ 𝑥 ∈ 𝐴} ≠ ∅) |
8 | | infssuzcl 12671 |
. . . . . . . 8
⊢ (({𝑛 ∈ (1..^𝑁) ∣ 𝑥 ∈ 𝐴} ⊆ (ℤ≥‘1)
∧ {𝑛 ∈ (1..^𝑁) ∣ 𝑥 ∈ 𝐴} ≠ ∅) → inf({𝑛 ∈ (1..^𝑁) ∣ 𝑥 ∈ 𝐴}, ℝ, < ) ∈ {𝑛 ∈ (1..^𝑁) ∣ 𝑥 ∈ 𝐴}) |
9 | 5, 7, 8 | sylancr 587 |
. . . . . . 7
⊢
(∃𝑛 ∈
(1..^𝑁)𝑥 ∈ 𝐴 → inf({𝑛 ∈ (1..^𝑁) ∣ 𝑥 ∈ 𝐴}, ℝ, < ) ∈ {𝑛 ∈ (1..^𝑁) ∣ 𝑥 ∈ 𝐴}) |
10 | 1, 9 | sselid 3924 |
. . . . . 6
⊢
(∃𝑛 ∈
(1..^𝑁)𝑥 ∈ 𝐴 → inf({𝑛 ∈ (1..^𝑁) ∣ 𝑥 ∈ 𝐴}, ℝ, < ) ∈ (1..^𝑁)) |
11 | | nfrab1 3316 |
. . . . . . . . . . 11
⊢
Ⅎ𝑛{𝑛 ∈ (1..^𝑁) ∣ 𝑥 ∈ 𝐴} |
12 | | nfcv 2909 |
. . . . . . . . . . 11
⊢
Ⅎ𝑛ℝ |
13 | | nfcv 2909 |
. . . . . . . . . . 11
⊢
Ⅎ𝑛
< |
14 | 11, 12, 13 | nfinf 9219 |
. . . . . . . . . 10
⊢
Ⅎ𝑛inf({𝑛 ∈ (1..^𝑁) ∣ 𝑥 ∈ 𝐴}, ℝ, < ) |
15 | | nfcv 2909 |
. . . . . . . . . 10
⊢
Ⅎ𝑛(1..^𝑁) |
16 | 14 | nfcsb1 3861 |
. . . . . . . . . . 11
⊢
Ⅎ𝑛⦋inf({𝑛 ∈ (1..^𝑁) ∣ 𝑥 ∈ 𝐴}, ℝ, < ) / 𝑛⦌𝐴 |
17 | 16 | nfcri 2896 |
. . . . . . . . . 10
⊢
Ⅎ𝑛 𝑥 ∈
⦋inf({𝑛
∈ (1..^𝑁) ∣
𝑥 ∈ 𝐴}, ℝ, < ) / 𝑛⦌𝐴 |
18 | | csbeq1a 3851 |
. . . . . . . . . . 11
⊢ (𝑛 = inf({𝑛 ∈ (1..^𝑁) ∣ 𝑥 ∈ 𝐴}, ℝ, < ) → 𝐴 = ⦋inf({𝑛 ∈ (1..^𝑁) ∣ 𝑥 ∈ 𝐴}, ℝ, < ) / 𝑛⦌𝐴) |
19 | 18 | eleq2d 2826 |
. . . . . . . . . 10
⊢ (𝑛 = inf({𝑛 ∈ (1..^𝑁) ∣ 𝑥 ∈ 𝐴}, ℝ, < ) → (𝑥 ∈ 𝐴 ↔ 𝑥 ∈ ⦋inf({𝑛 ∈ (1..^𝑁) ∣ 𝑥 ∈ 𝐴}, ℝ, < ) / 𝑛⦌𝐴)) |
20 | 14, 15, 17, 19 | elrabf 3622 |
. . . . . . . . 9
⊢
(inf({𝑛 ∈
(1..^𝑁) ∣ 𝑥 ∈ 𝐴}, ℝ, < ) ∈ {𝑛 ∈ (1..^𝑁) ∣ 𝑥 ∈ 𝐴} ↔ (inf({𝑛 ∈ (1..^𝑁) ∣ 𝑥 ∈ 𝐴}, ℝ, < ) ∈ (1..^𝑁) ∧ 𝑥 ∈ ⦋inf({𝑛 ∈ (1..^𝑁) ∣ 𝑥 ∈ 𝐴}, ℝ, < ) / 𝑛⦌𝐴)) |
21 | 9, 20 | sylib 217 |
. . . . . . . 8
⊢
(∃𝑛 ∈
(1..^𝑁)𝑥 ∈ 𝐴 → (inf({𝑛 ∈ (1..^𝑁) ∣ 𝑥 ∈ 𝐴}, ℝ, < ) ∈ (1..^𝑁) ∧ 𝑥 ∈ ⦋inf({𝑛 ∈ (1..^𝑁) ∣ 𝑥 ∈ 𝐴}, ℝ, < ) / 𝑛⦌𝐴)) |
22 | 21 | simprd 496 |
. . . . . . 7
⊢
(∃𝑛 ∈
(1..^𝑁)𝑥 ∈ 𝐴 → 𝑥 ∈ ⦋inf({𝑛 ∈ (1..^𝑁) ∣ 𝑥 ∈ 𝐴}, ℝ, < ) / 𝑛⦌𝐴) |
23 | 1, 2 | sstri 3935 |
. . . . . . . . . . 11
⊢ {𝑛 ∈ (1..^𝑁) ∣ 𝑥 ∈ 𝐴} ⊆ ℕ |
24 | | nnssre 11977 |
. . . . . . . . . . 11
⊢ ℕ
⊆ ℝ |
25 | 23, 24 | sstri 3935 |
. . . . . . . . . 10
⊢ {𝑛 ∈ (1..^𝑁) ∣ 𝑥 ∈ 𝐴} ⊆ ℝ |
26 | 25, 9 | sselid 3924 |
. . . . . . . . 9
⊢
(∃𝑛 ∈
(1..^𝑁)𝑥 ∈ 𝐴 → inf({𝑛 ∈ (1..^𝑁) ∣ 𝑥 ∈ 𝐴}, ℝ, < ) ∈
ℝ) |
27 | 26 | ltnrd 11109 |
. . . . . . . 8
⊢
(∃𝑛 ∈
(1..^𝑁)𝑥 ∈ 𝐴 → ¬ inf({𝑛 ∈ (1..^𝑁) ∣ 𝑥 ∈ 𝐴}, ℝ, < ) < inf({𝑛 ∈ (1..^𝑁) ∣ 𝑥 ∈ 𝐴}, ℝ, < )) |
28 | | eliun 4934 |
. . . . . . . . 9
⊢ (𝑥 ∈ ∪ 𝑘 ∈ (1..^inf({𝑛 ∈ (1..^𝑁) ∣ 𝑥 ∈ 𝐴}, ℝ, < ))𝐵 ↔ ∃𝑘 ∈ (1..^inf({𝑛 ∈ (1..^𝑁) ∣ 𝑥 ∈ 𝐴}, ℝ, < ))𝑥 ∈ 𝐵) |
29 | 26 | ad2antrr 723 |
. . . . . . . . . . 11
⊢
(((∃𝑛 ∈
(1..^𝑁)𝑥 ∈ 𝐴 ∧ 𝑘 ∈ (1..^inf({𝑛 ∈ (1..^𝑁) ∣ 𝑥 ∈ 𝐴}, ℝ, < ))) ∧ 𝑥 ∈ 𝐵) → inf({𝑛 ∈ (1..^𝑁) ∣ 𝑥 ∈ 𝐴}, ℝ, < ) ∈
ℝ) |
30 | | elfzouz2 13400 |
. . . . . . . . . . . . . . . 16
⊢
(inf({𝑛 ∈
(1..^𝑁) ∣ 𝑥 ∈ 𝐴}, ℝ, < ) ∈ (1..^𝑁) → 𝑁 ∈
(ℤ≥‘inf({𝑛 ∈ (1..^𝑁) ∣ 𝑥 ∈ 𝐴}, ℝ, < ))) |
31 | | fzoss2 13413 |
. . . . . . . . . . . . . . . 16
⊢ (𝑁 ∈
(ℤ≥‘inf({𝑛 ∈ (1..^𝑁) ∣ 𝑥 ∈ 𝐴}, ℝ, < )) → (1..^inf({𝑛 ∈ (1..^𝑁) ∣ 𝑥 ∈ 𝐴}, ℝ, < )) ⊆ (1..^𝑁)) |
32 | 10, 30, 31 | 3syl 18 |
. . . . . . . . . . . . . . 15
⊢
(∃𝑛 ∈
(1..^𝑁)𝑥 ∈ 𝐴 → (1..^inf({𝑛 ∈ (1..^𝑁) ∣ 𝑥 ∈ 𝐴}, ℝ, < )) ⊆ (1..^𝑁)) |
33 | 32 | sselda 3926 |
. . . . . . . . . . . . . 14
⊢
((∃𝑛 ∈
(1..^𝑁)𝑥 ∈ 𝐴 ∧ 𝑘 ∈ (1..^inf({𝑛 ∈ (1..^𝑁) ∣ 𝑥 ∈ 𝐴}, ℝ, < ))) → 𝑘 ∈ (1..^𝑁)) |
34 | 33 | adantr 481 |
. . . . . . . . . . . . 13
⊢
(((∃𝑛 ∈
(1..^𝑁)𝑥 ∈ 𝐴 ∧ 𝑘 ∈ (1..^inf({𝑛 ∈ (1..^𝑁) ∣ 𝑥 ∈ 𝐴}, ℝ, < ))) ∧ 𝑥 ∈ 𝐵) → 𝑘 ∈ (1..^𝑁)) |
35 | 2, 34 | sselid 3924 |
. . . . . . . . . . . 12
⊢
(((∃𝑛 ∈
(1..^𝑁)𝑥 ∈ 𝐴 ∧ 𝑘 ∈ (1..^inf({𝑛 ∈ (1..^𝑁) ∣ 𝑥 ∈ 𝐴}, ℝ, < ))) ∧ 𝑥 ∈ 𝐵) → 𝑘 ∈ ℕ) |
36 | 35 | nnred 11988 |
. . . . . . . . . . 11
⊢
(((∃𝑛 ∈
(1..^𝑁)𝑥 ∈ 𝐴 ∧ 𝑘 ∈ (1..^inf({𝑛 ∈ (1..^𝑁) ∣ 𝑥 ∈ 𝐴}, ℝ, < ))) ∧ 𝑥 ∈ 𝐵) → 𝑘 ∈ ℝ) |
37 | | simpr 485 |
. . . . . . . . . . . . 13
⊢
(((∃𝑛 ∈
(1..^𝑁)𝑥 ∈ 𝐴 ∧ 𝑘 ∈ (1..^inf({𝑛 ∈ (1..^𝑁) ∣ 𝑥 ∈ 𝐴}, ℝ, < ))) ∧ 𝑥 ∈ 𝐵) → 𝑥 ∈ 𝐵) |
38 | | nfcv 2909 |
. . . . . . . . . . . . . 14
⊢
Ⅎ𝑛𝑘 |
39 | | iundisj3.0 |
. . . . . . . . . . . . . . 15
⊢
Ⅎ𝑛𝐵 |
40 | 39 | nfcri 2896 |
. . . . . . . . . . . . . 14
⊢
Ⅎ𝑛 𝑥 ∈ 𝐵 |
41 | | iundisj3.1 |
. . . . . . . . . . . . . . 15
⊢ (𝑛 = 𝑘 → 𝐴 = 𝐵) |
42 | 41 | eleq2d 2826 |
. . . . . . . . . . . . . 14
⊢ (𝑛 = 𝑘 → (𝑥 ∈ 𝐴 ↔ 𝑥 ∈ 𝐵)) |
43 | 38, 15, 40, 42 | elrabf 3622 |
. . . . . . . . . . . . 13
⊢ (𝑘 ∈ {𝑛 ∈ (1..^𝑁) ∣ 𝑥 ∈ 𝐴} ↔ (𝑘 ∈ (1..^𝑁) ∧ 𝑥 ∈ 𝐵)) |
44 | 34, 37, 43 | sylanbrc 583 |
. . . . . . . . . . . 12
⊢
(((∃𝑛 ∈
(1..^𝑁)𝑥 ∈ 𝐴 ∧ 𝑘 ∈ (1..^inf({𝑛 ∈ (1..^𝑁) ∣ 𝑥 ∈ 𝐴}, ℝ, < ))) ∧ 𝑥 ∈ 𝐵) → 𝑘 ∈ {𝑛 ∈ (1..^𝑁) ∣ 𝑥 ∈ 𝐴}) |
45 | | infssuzle 12670 |
. . . . . . . . . . . 12
⊢ (({𝑛 ∈ (1..^𝑁) ∣ 𝑥 ∈ 𝐴} ⊆ (ℤ≥‘1)
∧ 𝑘 ∈ {𝑛 ∈ (1..^𝑁) ∣ 𝑥 ∈ 𝐴}) → inf({𝑛 ∈ (1..^𝑁) ∣ 𝑥 ∈ 𝐴}, ℝ, < ) ≤ 𝑘) |
46 | 5, 44, 45 | sylancr 587 |
. . . . . . . . . . 11
⊢
(((∃𝑛 ∈
(1..^𝑁)𝑥 ∈ 𝐴 ∧ 𝑘 ∈ (1..^inf({𝑛 ∈ (1..^𝑁) ∣ 𝑥 ∈ 𝐴}, ℝ, < ))) ∧ 𝑥 ∈ 𝐵) → inf({𝑛 ∈ (1..^𝑁) ∣ 𝑥 ∈ 𝐴}, ℝ, < ) ≤ 𝑘) |
47 | | elfzolt2 13395 |
. . . . . . . . . . . 12
⊢ (𝑘 ∈ (1..^inf({𝑛 ∈ (1..^𝑁) ∣ 𝑥 ∈ 𝐴}, ℝ, < )) → 𝑘 < inf({𝑛 ∈ (1..^𝑁) ∣ 𝑥 ∈ 𝐴}, ℝ, < )) |
48 | 47 | ad2antlr 724 |
. . . . . . . . . . 11
⊢
(((∃𝑛 ∈
(1..^𝑁)𝑥 ∈ 𝐴 ∧ 𝑘 ∈ (1..^inf({𝑛 ∈ (1..^𝑁) ∣ 𝑥 ∈ 𝐴}, ℝ, < ))) ∧ 𝑥 ∈ 𝐵) → 𝑘 < inf({𝑛 ∈ (1..^𝑁) ∣ 𝑥 ∈ 𝐴}, ℝ, < )) |
49 | 29, 36, 29, 46, 48 | lelttrd 11133 |
. . . . . . . . . 10
⊢
(((∃𝑛 ∈
(1..^𝑁)𝑥 ∈ 𝐴 ∧ 𝑘 ∈ (1..^inf({𝑛 ∈ (1..^𝑁) ∣ 𝑥 ∈ 𝐴}, ℝ, < ))) ∧ 𝑥 ∈ 𝐵) → inf({𝑛 ∈ (1..^𝑁) ∣ 𝑥 ∈ 𝐴}, ℝ, < ) < inf({𝑛 ∈ (1..^𝑁) ∣ 𝑥 ∈ 𝐴}, ℝ, < )) |
50 | 49 | rexlimdva2 3218 |
. . . . . . . . 9
⊢
(∃𝑛 ∈
(1..^𝑁)𝑥 ∈ 𝐴 → (∃𝑘 ∈ (1..^inf({𝑛 ∈ (1..^𝑁) ∣ 𝑥 ∈ 𝐴}, ℝ, < ))𝑥 ∈ 𝐵 → inf({𝑛 ∈ (1..^𝑁) ∣ 𝑥 ∈ 𝐴}, ℝ, < ) < inf({𝑛 ∈ (1..^𝑁) ∣ 𝑥 ∈ 𝐴}, ℝ, < ))) |
51 | 28, 50 | syl5bi 241 |
. . . . . . . 8
⊢
(∃𝑛 ∈
(1..^𝑁)𝑥 ∈ 𝐴 → (𝑥 ∈ ∪
𝑘 ∈ (1..^inf({𝑛 ∈ (1..^𝑁) ∣ 𝑥 ∈ 𝐴}, ℝ, < ))𝐵 → inf({𝑛 ∈ (1..^𝑁) ∣ 𝑥 ∈ 𝐴}, ℝ, < ) < inf({𝑛 ∈ (1..^𝑁) ∣ 𝑥 ∈ 𝐴}, ℝ, < ))) |
52 | 27, 51 | mtod 197 |
. . . . . . 7
⊢
(∃𝑛 ∈
(1..^𝑁)𝑥 ∈ 𝐴 → ¬ 𝑥 ∈ ∪
𝑘 ∈ (1..^inf({𝑛 ∈ (1..^𝑁) ∣ 𝑥 ∈ 𝐴}, ℝ, < ))𝐵) |
53 | 22, 52 | eldifd 3903 |
. . . . . 6
⊢
(∃𝑛 ∈
(1..^𝑁)𝑥 ∈ 𝐴 → 𝑥 ∈ (⦋inf({𝑛 ∈ (1..^𝑁) ∣ 𝑥 ∈ 𝐴}, ℝ, < ) / 𝑛⦌𝐴 ∖ ∪
𝑘 ∈ (1..^inf({𝑛 ∈ (1..^𝑁) ∣ 𝑥 ∈ 𝐴}, ℝ, < ))𝐵)) |
54 | | csbeq1 3840 |
. . . . . . . . 9
⊢ (𝑚 = inf({𝑛 ∈ (1..^𝑁) ∣ 𝑥 ∈ 𝐴}, ℝ, < ) →
⦋𝑚 / 𝑛⦌𝐴 = ⦋inf({𝑛 ∈ (1..^𝑁) ∣ 𝑥 ∈ 𝐴}, ℝ, < ) / 𝑛⦌𝐴) |
55 | | oveq2 7279 |
. . . . . . . . . 10
⊢ (𝑚 = inf({𝑛 ∈ (1..^𝑁) ∣ 𝑥 ∈ 𝐴}, ℝ, < ) → (1..^𝑚) = (1..^inf({𝑛 ∈ (1..^𝑁) ∣ 𝑥 ∈ 𝐴}, ℝ, < ))) |
56 | 55 | iuneq1d 4957 |
. . . . . . . . 9
⊢ (𝑚 = inf({𝑛 ∈ (1..^𝑁) ∣ 𝑥 ∈ 𝐴}, ℝ, < ) → ∪ 𝑘 ∈ (1..^𝑚)𝐵 = ∪ 𝑘 ∈ (1..^inf({𝑛 ∈ (1..^𝑁) ∣ 𝑥 ∈ 𝐴}, ℝ, < ))𝐵) |
57 | 54, 56 | difeq12d 4063 |
. . . . . . . 8
⊢ (𝑚 = inf({𝑛 ∈ (1..^𝑁) ∣ 𝑥 ∈ 𝐴}, ℝ, < ) →
(⦋𝑚 / 𝑛⦌𝐴 ∖ ∪
𝑘 ∈ (1..^𝑚)𝐵) = (⦋inf({𝑛 ∈ (1..^𝑁) ∣ 𝑥 ∈ 𝐴}, ℝ, < ) / 𝑛⦌𝐴 ∖ ∪
𝑘 ∈ (1..^inf({𝑛 ∈ (1..^𝑁) ∣ 𝑥 ∈ 𝐴}, ℝ, < ))𝐵)) |
58 | 57 | eleq2d 2826 |
. . . . . . 7
⊢ (𝑚 = inf({𝑛 ∈ (1..^𝑁) ∣ 𝑥 ∈ 𝐴}, ℝ, < ) → (𝑥 ∈ (⦋𝑚 / 𝑛⦌𝐴 ∖ ∪
𝑘 ∈ (1..^𝑚)𝐵) ↔ 𝑥 ∈ (⦋inf({𝑛 ∈ (1..^𝑁) ∣ 𝑥 ∈ 𝐴}, ℝ, < ) / 𝑛⦌𝐴 ∖ ∪
𝑘 ∈ (1..^inf({𝑛 ∈ (1..^𝑁) ∣ 𝑥 ∈ 𝐴}, ℝ, < ))𝐵))) |
59 | 58 | rspcev 3561 |
. . . . . 6
⊢
((inf({𝑛 ∈
(1..^𝑁) ∣ 𝑥 ∈ 𝐴}, ℝ, < ) ∈ (1..^𝑁) ∧ 𝑥 ∈ (⦋inf({𝑛 ∈ (1..^𝑁) ∣ 𝑥 ∈ 𝐴}, ℝ, < ) / 𝑛⦌𝐴 ∖ ∪
𝑘 ∈ (1..^inf({𝑛 ∈ (1..^𝑁) ∣ 𝑥 ∈ 𝐴}, ℝ, < ))𝐵)) → ∃𝑚 ∈ (1..^𝑁)𝑥 ∈ (⦋𝑚 / 𝑛⦌𝐴 ∖ ∪
𝑘 ∈ (1..^𝑚)𝐵)) |
60 | 10, 53, 59 | syl2anc 584 |
. . . . 5
⊢
(∃𝑛 ∈
(1..^𝑁)𝑥 ∈ 𝐴 → ∃𝑚 ∈ (1..^𝑁)𝑥 ∈ (⦋𝑚 / 𝑛⦌𝐴 ∖ ∪
𝑘 ∈ (1..^𝑚)𝐵)) |
61 | | nfv 1921 |
. . . . . 6
⊢
Ⅎ𝑚 𝑥 ∈ (𝐴 ∖ ∪
𝑘 ∈ (1..^𝑛)𝐵) |
62 | | nfcsb1v 3862 |
. . . . . . . 8
⊢
Ⅎ𝑛⦋𝑚 / 𝑛⦌𝐴 |
63 | | nfcv 2909 |
. . . . . . . . 9
⊢
Ⅎ𝑛(1..^𝑚) |
64 | 63, 39 | nfiun 4960 |
. . . . . . . 8
⊢
Ⅎ𝑛∪ 𝑘 ∈ (1..^𝑚)𝐵 |
65 | 62, 64 | nfdif 4065 |
. . . . . . 7
⊢
Ⅎ𝑛(⦋𝑚 / 𝑛⦌𝐴 ∖ ∪
𝑘 ∈ (1..^𝑚)𝐵) |
66 | 65 | nfcri 2896 |
. . . . . 6
⊢
Ⅎ𝑛 𝑥 ∈ (⦋𝑚 / 𝑛⦌𝐴 ∖ ∪
𝑘 ∈ (1..^𝑚)𝐵) |
67 | | csbeq1a 3851 |
. . . . . . . 8
⊢ (𝑛 = 𝑚 → 𝐴 = ⦋𝑚 / 𝑛⦌𝐴) |
68 | | oveq2 7279 |
. . . . . . . . 9
⊢ (𝑛 = 𝑚 → (1..^𝑛) = (1..^𝑚)) |
69 | 68 | iuneq1d 4957 |
. . . . . . . 8
⊢ (𝑛 = 𝑚 → ∪
𝑘 ∈ (1..^𝑛)𝐵 = ∪ 𝑘 ∈ (1..^𝑚)𝐵) |
70 | 67, 69 | difeq12d 4063 |
. . . . . . 7
⊢ (𝑛 = 𝑚 → (𝐴 ∖ ∪
𝑘 ∈ (1..^𝑛)𝐵) = (⦋𝑚 / 𝑛⦌𝐴 ∖ ∪
𝑘 ∈ (1..^𝑚)𝐵)) |
71 | 70 | eleq2d 2826 |
. . . . . 6
⊢ (𝑛 = 𝑚 → (𝑥 ∈ (𝐴 ∖ ∪
𝑘 ∈ (1..^𝑛)𝐵) ↔ 𝑥 ∈ (⦋𝑚 / 𝑛⦌𝐴 ∖ ∪
𝑘 ∈ (1..^𝑚)𝐵))) |
72 | 61, 66, 71 | cbvrexw 3373 |
. . . . 5
⊢
(∃𝑛 ∈
(1..^𝑁)𝑥 ∈ (𝐴 ∖ ∪
𝑘 ∈ (1..^𝑛)𝐵) ↔ ∃𝑚 ∈ (1..^𝑁)𝑥 ∈ (⦋𝑚 / 𝑛⦌𝐴 ∖ ∪
𝑘 ∈ (1..^𝑚)𝐵)) |
73 | 60, 72 | sylibr 233 |
. . . 4
⊢
(∃𝑛 ∈
(1..^𝑁)𝑥 ∈ 𝐴 → ∃𝑛 ∈ (1..^𝑁)𝑥 ∈ (𝐴 ∖ ∪
𝑘 ∈ (1..^𝑛)𝐵)) |
74 | | eldifi 4066 |
. . . . 5
⊢ (𝑥 ∈ (𝐴 ∖ ∪
𝑘 ∈ (1..^𝑛)𝐵) → 𝑥 ∈ 𝐴) |
75 | 74 | reximi 3177 |
. . . 4
⊢
(∃𝑛 ∈
(1..^𝑁)𝑥 ∈ (𝐴 ∖ ∪
𝑘 ∈ (1..^𝑛)𝐵) → ∃𝑛 ∈ (1..^𝑁)𝑥 ∈ 𝐴) |
76 | 73, 75 | impbii 208 |
. . 3
⊢
(∃𝑛 ∈
(1..^𝑁)𝑥 ∈ 𝐴 ↔ ∃𝑛 ∈ (1..^𝑁)𝑥 ∈ (𝐴 ∖ ∪
𝑘 ∈ (1..^𝑛)𝐵)) |
77 | | eliun 4934 |
. . 3
⊢ (𝑥 ∈ ∪ 𝑛 ∈ (1..^𝑁)𝐴 ↔ ∃𝑛 ∈ (1..^𝑁)𝑥 ∈ 𝐴) |
78 | | eliun 4934 |
. . 3
⊢ (𝑥 ∈ ∪ 𝑛 ∈ (1..^𝑁)(𝐴 ∖ ∪
𝑘 ∈ (1..^𝑛)𝐵) ↔ ∃𝑛 ∈ (1..^𝑁)𝑥 ∈ (𝐴 ∖ ∪
𝑘 ∈ (1..^𝑛)𝐵)) |
79 | 76, 77, 78 | 3bitr4i 303 |
. 2
⊢ (𝑥 ∈ ∪ 𝑛 ∈ (1..^𝑁)𝐴 ↔ 𝑥 ∈ ∪
𝑛 ∈ (1..^𝑁)(𝐴 ∖ ∪
𝑘 ∈ (1..^𝑛)𝐵)) |
80 | 79 | eqriv 2737 |
1
⊢ ∪ 𝑛 ∈ (1..^𝑁)𝐴 = ∪ 𝑛 ∈ (1..^𝑁)(𝐴 ∖ ∪
𝑘 ∈ (1..^𝑛)𝐵) |