Step | Hyp | Ref
| Expression |
1 | | ssrab2 3687 |
. . . . . . 7
⊢ {𝑛 ∈ (1..^𝑁) ∣ 𝑥 ∈ 𝐴} ⊆ (1..^𝑁) |
2 | | fzossnn 12516 |
. . . . . . . . . 10
⊢
(1..^𝑁) ⊆
ℕ |
3 | | nnuz 11723 |
. . . . . . . . . 10
⊢ ℕ =
(ℤ≥‘1) |
4 | 2, 3 | sseqtri 3637 |
. . . . . . . . 9
⊢
(1..^𝑁) ⊆
(ℤ≥‘1) |
5 | 1, 4 | sstri 3612 |
. . . . . . . 8
⊢ {𝑛 ∈ (1..^𝑁) ∣ 𝑥 ∈ 𝐴} ⊆
(ℤ≥‘1) |
6 | | rabn0 3958 |
. . . . . . . . 9
⊢ ({𝑛 ∈ (1..^𝑁) ∣ 𝑥 ∈ 𝐴} ≠ ∅ ↔ ∃𝑛 ∈ (1..^𝑁)𝑥 ∈ 𝐴) |
7 | 6 | biimpri 218 |
. . . . . . . 8
⊢
(∃𝑛 ∈
(1..^𝑁)𝑥 ∈ 𝐴 → {𝑛 ∈ (1..^𝑁) ∣ 𝑥 ∈ 𝐴} ≠ ∅) |
8 | | infssuzcl 11772 |
. . . . . . . 8
⊢ (({𝑛 ∈ (1..^𝑁) ∣ 𝑥 ∈ 𝐴} ⊆ (ℤ≥‘1)
∧ {𝑛 ∈ (1..^𝑁) ∣ 𝑥 ∈ 𝐴} ≠ ∅) → inf({𝑛 ∈ (1..^𝑁) ∣ 𝑥 ∈ 𝐴}, ℝ, < ) ∈ {𝑛 ∈ (1..^𝑁) ∣ 𝑥 ∈ 𝐴}) |
9 | 5, 7, 8 | sylancr 695 |
. . . . . . 7
⊢
(∃𝑛 ∈
(1..^𝑁)𝑥 ∈ 𝐴 → inf({𝑛 ∈ (1..^𝑁) ∣ 𝑥 ∈ 𝐴}, ℝ, < ) ∈ {𝑛 ∈ (1..^𝑁) ∣ 𝑥 ∈ 𝐴}) |
10 | 1, 9 | sseldi 3601 |
. . . . . 6
⊢
(∃𝑛 ∈
(1..^𝑁)𝑥 ∈ 𝐴 → inf({𝑛 ∈ (1..^𝑁) ∣ 𝑥 ∈ 𝐴}, ℝ, < ) ∈ (1..^𝑁)) |
11 | | nfrab1 3122 |
. . . . . . . . . . 11
⊢
Ⅎ𝑛{𝑛 ∈ (1..^𝑁) ∣ 𝑥 ∈ 𝐴} |
12 | | nfcv 2764 |
. . . . . . . . . . 11
⊢
Ⅎ𝑛ℝ |
13 | | nfcv 2764 |
. . . . . . . . . . 11
⊢
Ⅎ𝑛
< |
14 | 11, 12, 13 | nfinf 8388 |
. . . . . . . . . 10
⊢
Ⅎ𝑛inf({𝑛 ∈ (1..^𝑁) ∣ 𝑥 ∈ 𝐴}, ℝ, < ) |
15 | | nfcv 2764 |
. . . . . . . . . 10
⊢
Ⅎ𝑛(1..^𝑁) |
16 | 14 | nfcsb1 3548 |
. . . . . . . . . . 11
⊢
Ⅎ𝑛⦋inf({𝑛 ∈ (1..^𝑁) ∣ 𝑥 ∈ 𝐴}, ℝ, < ) / 𝑛⦌𝐴 |
17 | 16 | nfcri 2758 |
. . . . . . . . . 10
⊢
Ⅎ𝑛 𝑥 ∈
⦋inf({𝑛
∈ (1..^𝑁) ∣
𝑥 ∈ 𝐴}, ℝ, < ) / 𝑛⦌𝐴 |
18 | | csbeq1a 3542 |
. . . . . . . . . . 11
⊢ (𝑛 = inf({𝑛 ∈ (1..^𝑁) ∣ 𝑥 ∈ 𝐴}, ℝ, < ) → 𝐴 = ⦋inf({𝑛 ∈ (1..^𝑁) ∣ 𝑥 ∈ 𝐴}, ℝ, < ) / 𝑛⦌𝐴) |
19 | 18 | eleq2d 2687 |
. . . . . . . . . 10
⊢ (𝑛 = inf({𝑛 ∈ (1..^𝑁) ∣ 𝑥 ∈ 𝐴}, ℝ, < ) → (𝑥 ∈ 𝐴 ↔ 𝑥 ∈ ⦋inf({𝑛 ∈ (1..^𝑁) ∣ 𝑥 ∈ 𝐴}, ℝ, < ) / 𝑛⦌𝐴)) |
20 | 14, 15, 17, 19 | elrabf 3360 |
. . . . . . . . 9
⊢
(inf({𝑛 ∈
(1..^𝑁) ∣ 𝑥 ∈ 𝐴}, ℝ, < ) ∈ {𝑛 ∈ (1..^𝑁) ∣ 𝑥 ∈ 𝐴} ↔ (inf({𝑛 ∈ (1..^𝑁) ∣ 𝑥 ∈ 𝐴}, ℝ, < ) ∈ (1..^𝑁) ∧ 𝑥 ∈ ⦋inf({𝑛 ∈ (1..^𝑁) ∣ 𝑥 ∈ 𝐴}, ℝ, < ) / 𝑛⦌𝐴)) |
21 | 9, 20 | sylib 208 |
. . . . . . . 8
⊢
(∃𝑛 ∈
(1..^𝑁)𝑥 ∈ 𝐴 → (inf({𝑛 ∈ (1..^𝑁) ∣ 𝑥 ∈ 𝐴}, ℝ, < ) ∈ (1..^𝑁) ∧ 𝑥 ∈ ⦋inf({𝑛 ∈ (1..^𝑁) ∣ 𝑥 ∈ 𝐴}, ℝ, < ) / 𝑛⦌𝐴)) |
22 | 21 | simprd 479 |
. . . . . . 7
⊢
(∃𝑛 ∈
(1..^𝑁)𝑥 ∈ 𝐴 → 𝑥 ∈ ⦋inf({𝑛 ∈ (1..^𝑁) ∣ 𝑥 ∈ 𝐴}, ℝ, < ) / 𝑛⦌𝐴) |
23 | 1, 2 | sstri 3612 |
. . . . . . . . . . 11
⊢ {𝑛 ∈ (1..^𝑁) ∣ 𝑥 ∈ 𝐴} ⊆ ℕ |
24 | | nnssre 11024 |
. . . . . . . . . . 11
⊢ ℕ
⊆ ℝ |
25 | 23, 24 | sstri 3612 |
. . . . . . . . . 10
⊢ {𝑛 ∈ (1..^𝑁) ∣ 𝑥 ∈ 𝐴} ⊆ ℝ |
26 | 25, 9 | sseldi 3601 |
. . . . . . . . 9
⊢
(∃𝑛 ∈
(1..^𝑁)𝑥 ∈ 𝐴 → inf({𝑛 ∈ (1..^𝑁) ∣ 𝑥 ∈ 𝐴}, ℝ, < ) ∈
ℝ) |
27 | 26 | ltnrd 10171 |
. . . . . . . 8
⊢
(∃𝑛 ∈
(1..^𝑁)𝑥 ∈ 𝐴 → ¬ inf({𝑛 ∈ (1..^𝑁) ∣ 𝑥 ∈ 𝐴}, ℝ, < ) < inf({𝑛 ∈ (1..^𝑁) ∣ 𝑥 ∈ 𝐴}, ℝ, < )) |
28 | | eliun 4524 |
. . . . . . . . 9
⊢ (𝑥 ∈ ∪ 𝑘 ∈ (1..^inf({𝑛 ∈ (1..^𝑁) ∣ 𝑥 ∈ 𝐴}, ℝ, < ))𝐵 ↔ ∃𝑘 ∈ (1..^inf({𝑛 ∈ (1..^𝑁) ∣ 𝑥 ∈ 𝐴}, ℝ, < ))𝑥 ∈ 𝐵) |
29 | 26 | ad2antrr 762 |
. . . . . . . . . . . 12
⊢
(((∃𝑛 ∈
(1..^𝑁)𝑥 ∈ 𝐴 ∧ 𝑘 ∈ (1..^inf({𝑛 ∈ (1..^𝑁) ∣ 𝑥 ∈ 𝐴}, ℝ, < ))) ∧ 𝑥 ∈ 𝐵) → inf({𝑛 ∈ (1..^𝑁) ∣ 𝑥 ∈ 𝐴}, ℝ, < ) ∈
ℝ) |
30 | | elfzouz2 12484 |
. . . . . . . . . . . . . . . . 17
⊢
(inf({𝑛 ∈
(1..^𝑁) ∣ 𝑥 ∈ 𝐴}, ℝ, < ) ∈ (1..^𝑁) → 𝑁 ∈
(ℤ≥‘inf({𝑛 ∈ (1..^𝑁) ∣ 𝑥 ∈ 𝐴}, ℝ, < ))) |
31 | | fzoss2 12496 |
. . . . . . . . . . . . . . . . 17
⊢ (𝑁 ∈
(ℤ≥‘inf({𝑛 ∈ (1..^𝑁) ∣ 𝑥 ∈ 𝐴}, ℝ, < )) → (1..^inf({𝑛 ∈ (1..^𝑁) ∣ 𝑥 ∈ 𝐴}, ℝ, < )) ⊆ (1..^𝑁)) |
32 | 10, 30, 31 | 3syl 18 |
. . . . . . . . . . . . . . . 16
⊢
(∃𝑛 ∈
(1..^𝑁)𝑥 ∈ 𝐴 → (1..^inf({𝑛 ∈ (1..^𝑁) ∣ 𝑥 ∈ 𝐴}, ℝ, < )) ⊆ (1..^𝑁)) |
33 | 32 | sselda 3603 |
. . . . . . . . . . . . . . 15
⊢
((∃𝑛 ∈
(1..^𝑁)𝑥 ∈ 𝐴 ∧ 𝑘 ∈ (1..^inf({𝑛 ∈ (1..^𝑁) ∣ 𝑥 ∈ 𝐴}, ℝ, < ))) → 𝑘 ∈ (1..^𝑁)) |
34 | 33 | adantr 481 |
. . . . . . . . . . . . . 14
⊢
(((∃𝑛 ∈
(1..^𝑁)𝑥 ∈ 𝐴 ∧ 𝑘 ∈ (1..^inf({𝑛 ∈ (1..^𝑁) ∣ 𝑥 ∈ 𝐴}, ℝ, < ))) ∧ 𝑥 ∈ 𝐵) → 𝑘 ∈ (1..^𝑁)) |
35 | 2, 34 | sseldi 3601 |
. . . . . . . . . . . . 13
⊢
(((∃𝑛 ∈
(1..^𝑁)𝑥 ∈ 𝐴 ∧ 𝑘 ∈ (1..^inf({𝑛 ∈ (1..^𝑁) ∣ 𝑥 ∈ 𝐴}, ℝ, < ))) ∧ 𝑥 ∈ 𝐵) → 𝑘 ∈ ℕ) |
36 | 35 | nnred 11035 |
. . . . . . . . . . . 12
⊢
(((∃𝑛 ∈
(1..^𝑁)𝑥 ∈ 𝐴 ∧ 𝑘 ∈ (1..^inf({𝑛 ∈ (1..^𝑁) ∣ 𝑥 ∈ 𝐴}, ℝ, < ))) ∧ 𝑥 ∈ 𝐵) → 𝑘 ∈ ℝ) |
37 | | simpr 477 |
. . . . . . . . . . . . . 14
⊢
(((∃𝑛 ∈
(1..^𝑁)𝑥 ∈ 𝐴 ∧ 𝑘 ∈ (1..^inf({𝑛 ∈ (1..^𝑁) ∣ 𝑥 ∈ 𝐴}, ℝ, < ))) ∧ 𝑥 ∈ 𝐵) → 𝑥 ∈ 𝐵) |
38 | | nfcv 2764 |
. . . . . . . . . . . . . . 15
⊢
Ⅎ𝑛𝑘 |
39 | | iundisj3.0 |
. . . . . . . . . . . . . . . 16
⊢
Ⅎ𝑛𝐵 |
40 | 39 | nfcri 2758 |
. . . . . . . . . . . . . . 15
⊢
Ⅎ𝑛 𝑥 ∈ 𝐵 |
41 | | iundisj3.1 |
. . . . . . . . . . . . . . . 16
⊢ (𝑛 = 𝑘 → 𝐴 = 𝐵) |
42 | 41 | eleq2d 2687 |
. . . . . . . . . . . . . . 15
⊢ (𝑛 = 𝑘 → (𝑥 ∈ 𝐴 ↔ 𝑥 ∈ 𝐵)) |
43 | 38, 15, 40, 42 | elrabf 3360 |
. . . . . . . . . . . . . 14
⊢ (𝑘 ∈ {𝑛 ∈ (1..^𝑁) ∣ 𝑥 ∈ 𝐴} ↔ (𝑘 ∈ (1..^𝑁) ∧ 𝑥 ∈ 𝐵)) |
44 | 34, 37, 43 | sylanbrc 698 |
. . . . . . . . . . . . 13
⊢
(((∃𝑛 ∈
(1..^𝑁)𝑥 ∈ 𝐴 ∧ 𝑘 ∈ (1..^inf({𝑛 ∈ (1..^𝑁) ∣ 𝑥 ∈ 𝐴}, ℝ, < ))) ∧ 𝑥 ∈ 𝐵) → 𝑘 ∈ {𝑛 ∈ (1..^𝑁) ∣ 𝑥 ∈ 𝐴}) |
45 | | infssuzle 11771 |
. . . . . . . . . . . . 13
⊢ (({𝑛 ∈ (1..^𝑁) ∣ 𝑥 ∈ 𝐴} ⊆ (ℤ≥‘1)
∧ 𝑘 ∈ {𝑛 ∈ (1..^𝑁) ∣ 𝑥 ∈ 𝐴}) → inf({𝑛 ∈ (1..^𝑁) ∣ 𝑥 ∈ 𝐴}, ℝ, < ) ≤ 𝑘) |
46 | 5, 44, 45 | sylancr 695 |
. . . . . . . . . . . 12
⊢
(((∃𝑛 ∈
(1..^𝑁)𝑥 ∈ 𝐴 ∧ 𝑘 ∈ (1..^inf({𝑛 ∈ (1..^𝑁) ∣ 𝑥 ∈ 𝐴}, ℝ, < ))) ∧ 𝑥 ∈ 𝐵) → inf({𝑛 ∈ (1..^𝑁) ∣ 𝑥 ∈ 𝐴}, ℝ, < ) ≤ 𝑘) |
47 | | elfzolt2 12479 |
. . . . . . . . . . . . 13
⊢ (𝑘 ∈ (1..^inf({𝑛 ∈ (1..^𝑁) ∣ 𝑥 ∈ 𝐴}, ℝ, < )) → 𝑘 < inf({𝑛 ∈ (1..^𝑁) ∣ 𝑥 ∈ 𝐴}, ℝ, < )) |
48 | 47 | ad2antlr 763 |
. . . . . . . . . . . 12
⊢
(((∃𝑛 ∈
(1..^𝑁)𝑥 ∈ 𝐴 ∧ 𝑘 ∈ (1..^inf({𝑛 ∈ (1..^𝑁) ∣ 𝑥 ∈ 𝐴}, ℝ, < ))) ∧ 𝑥 ∈ 𝐵) → 𝑘 < inf({𝑛 ∈ (1..^𝑁) ∣ 𝑥 ∈ 𝐴}, ℝ, < )) |
49 | 29, 36, 29, 46, 48 | lelttrd 10195 |
. . . . . . . . . . 11
⊢
(((∃𝑛 ∈
(1..^𝑁)𝑥 ∈ 𝐴 ∧ 𝑘 ∈ (1..^inf({𝑛 ∈ (1..^𝑁) ∣ 𝑥 ∈ 𝐴}, ℝ, < ))) ∧ 𝑥 ∈ 𝐵) → inf({𝑛 ∈ (1..^𝑁) ∣ 𝑥 ∈ 𝐴}, ℝ, < ) < inf({𝑛 ∈ (1..^𝑁) ∣ 𝑥 ∈ 𝐴}, ℝ, < )) |
50 | 49 | ex 450 |
. . . . . . . . . 10
⊢
((∃𝑛 ∈
(1..^𝑁)𝑥 ∈ 𝐴 ∧ 𝑘 ∈ (1..^inf({𝑛 ∈ (1..^𝑁) ∣ 𝑥 ∈ 𝐴}, ℝ, < ))) → (𝑥 ∈ 𝐵 → inf({𝑛 ∈ (1..^𝑁) ∣ 𝑥 ∈ 𝐴}, ℝ, < ) < inf({𝑛 ∈ (1..^𝑁) ∣ 𝑥 ∈ 𝐴}, ℝ, < ))) |
51 | 50 | rexlimdva 3031 |
. . . . . . . . 9
⊢
(∃𝑛 ∈
(1..^𝑁)𝑥 ∈ 𝐴 → (∃𝑘 ∈ (1..^inf({𝑛 ∈ (1..^𝑁) ∣ 𝑥 ∈ 𝐴}, ℝ, < ))𝑥 ∈ 𝐵 → inf({𝑛 ∈ (1..^𝑁) ∣ 𝑥 ∈ 𝐴}, ℝ, < ) < inf({𝑛 ∈ (1..^𝑁) ∣ 𝑥 ∈ 𝐴}, ℝ, < ))) |
52 | 28, 51 | syl5bi 232 |
. . . . . . . 8
⊢
(∃𝑛 ∈
(1..^𝑁)𝑥 ∈ 𝐴 → (𝑥 ∈ ∪
𝑘 ∈ (1..^inf({𝑛 ∈ (1..^𝑁) ∣ 𝑥 ∈ 𝐴}, ℝ, < ))𝐵 → inf({𝑛 ∈ (1..^𝑁) ∣ 𝑥 ∈ 𝐴}, ℝ, < ) < inf({𝑛 ∈ (1..^𝑁) ∣ 𝑥 ∈ 𝐴}, ℝ, < ))) |
53 | 27, 52 | mtod 189 |
. . . . . . 7
⊢
(∃𝑛 ∈
(1..^𝑁)𝑥 ∈ 𝐴 → ¬ 𝑥 ∈ ∪
𝑘 ∈ (1..^inf({𝑛 ∈ (1..^𝑁) ∣ 𝑥 ∈ 𝐴}, ℝ, < ))𝐵) |
54 | 22, 53 | eldifd 3585 |
. . . . . 6
⊢
(∃𝑛 ∈
(1..^𝑁)𝑥 ∈ 𝐴 → 𝑥 ∈ (⦋inf({𝑛 ∈ (1..^𝑁) ∣ 𝑥 ∈ 𝐴}, ℝ, < ) / 𝑛⦌𝐴 ∖ ∪
𝑘 ∈ (1..^inf({𝑛 ∈ (1..^𝑁) ∣ 𝑥 ∈ 𝐴}, ℝ, < ))𝐵)) |
55 | | csbeq1 3536 |
. . . . . . . . 9
⊢ (𝑚 = inf({𝑛 ∈ (1..^𝑁) ∣ 𝑥 ∈ 𝐴}, ℝ, < ) →
⦋𝑚 / 𝑛⦌𝐴 = ⦋inf({𝑛 ∈ (1..^𝑁) ∣ 𝑥 ∈ 𝐴}, ℝ, < ) / 𝑛⦌𝐴) |
56 | | oveq2 6658 |
. . . . . . . . . 10
⊢ (𝑚 = inf({𝑛 ∈ (1..^𝑁) ∣ 𝑥 ∈ 𝐴}, ℝ, < ) → (1..^𝑚) = (1..^inf({𝑛 ∈ (1..^𝑁) ∣ 𝑥 ∈ 𝐴}, ℝ, < ))) |
57 | 56 | iuneq1d 4545 |
. . . . . . . . 9
⊢ (𝑚 = inf({𝑛 ∈ (1..^𝑁) ∣ 𝑥 ∈ 𝐴}, ℝ, < ) → ∪ 𝑘 ∈ (1..^𝑚)𝐵 = ∪ 𝑘 ∈ (1..^inf({𝑛 ∈ (1..^𝑁) ∣ 𝑥 ∈ 𝐴}, ℝ, < ))𝐵) |
58 | 55, 57 | difeq12d 3729 |
. . . . . . . 8
⊢ (𝑚 = inf({𝑛 ∈ (1..^𝑁) ∣ 𝑥 ∈ 𝐴}, ℝ, < ) →
(⦋𝑚 / 𝑛⦌𝐴 ∖ ∪
𝑘 ∈ (1..^𝑚)𝐵) = (⦋inf({𝑛 ∈ (1..^𝑁) ∣ 𝑥 ∈ 𝐴}, ℝ, < ) / 𝑛⦌𝐴 ∖ ∪
𝑘 ∈ (1..^inf({𝑛 ∈ (1..^𝑁) ∣ 𝑥 ∈ 𝐴}, ℝ, < ))𝐵)) |
59 | 58 | eleq2d 2687 |
. . . . . . 7
⊢ (𝑚 = inf({𝑛 ∈ (1..^𝑁) ∣ 𝑥 ∈ 𝐴}, ℝ, < ) → (𝑥 ∈ (⦋𝑚 / 𝑛⦌𝐴 ∖ ∪
𝑘 ∈ (1..^𝑚)𝐵) ↔ 𝑥 ∈ (⦋inf({𝑛 ∈ (1..^𝑁) ∣ 𝑥 ∈ 𝐴}, ℝ, < ) / 𝑛⦌𝐴 ∖ ∪
𝑘 ∈ (1..^inf({𝑛 ∈ (1..^𝑁) ∣ 𝑥 ∈ 𝐴}, ℝ, < ))𝐵))) |
60 | 59 | rspcev 3309 |
. . . . . 6
⊢
((inf({𝑛 ∈
(1..^𝑁) ∣ 𝑥 ∈ 𝐴}, ℝ, < ) ∈ (1..^𝑁) ∧ 𝑥 ∈ (⦋inf({𝑛 ∈ (1..^𝑁) ∣ 𝑥 ∈ 𝐴}, ℝ, < ) / 𝑛⦌𝐴 ∖ ∪
𝑘 ∈ (1..^inf({𝑛 ∈ (1..^𝑁) ∣ 𝑥 ∈ 𝐴}, ℝ, < ))𝐵)) → ∃𝑚 ∈ (1..^𝑁)𝑥 ∈ (⦋𝑚 / 𝑛⦌𝐴 ∖ ∪
𝑘 ∈ (1..^𝑚)𝐵)) |
61 | 10, 54, 60 | syl2anc 693 |
. . . . 5
⊢
(∃𝑛 ∈
(1..^𝑁)𝑥 ∈ 𝐴 → ∃𝑚 ∈ (1..^𝑁)𝑥 ∈ (⦋𝑚 / 𝑛⦌𝐴 ∖ ∪
𝑘 ∈ (1..^𝑚)𝐵)) |
62 | | nfv 1843 |
. . . . . 6
⊢
Ⅎ𝑚 𝑥 ∈ (𝐴 ∖ ∪
𝑘 ∈ (1..^𝑛)𝐵) |
63 | | nfcsb1v 3549 |
. . . . . . . 8
⊢
Ⅎ𝑛⦋𝑚 / 𝑛⦌𝐴 |
64 | | nfcv 2764 |
. . . . . . . . 9
⊢
Ⅎ𝑛(1..^𝑚) |
65 | 64, 39 | nfiun 4548 |
. . . . . . . 8
⊢
Ⅎ𝑛∪ 𝑘 ∈ (1..^𝑚)𝐵 |
66 | 63, 65 | nfdif 3731 |
. . . . . . 7
⊢
Ⅎ𝑛(⦋𝑚 / 𝑛⦌𝐴 ∖ ∪
𝑘 ∈ (1..^𝑚)𝐵) |
67 | 66 | nfcri 2758 |
. . . . . 6
⊢
Ⅎ𝑛 𝑥 ∈ (⦋𝑚 / 𝑛⦌𝐴 ∖ ∪
𝑘 ∈ (1..^𝑚)𝐵) |
68 | | csbeq1a 3542 |
. . . . . . . 8
⊢ (𝑛 = 𝑚 → 𝐴 = ⦋𝑚 / 𝑛⦌𝐴) |
69 | | oveq2 6658 |
. . . . . . . . 9
⊢ (𝑛 = 𝑚 → (1..^𝑛) = (1..^𝑚)) |
70 | 69 | iuneq1d 4545 |
. . . . . . . 8
⊢ (𝑛 = 𝑚 → ∪
𝑘 ∈ (1..^𝑛)𝐵 = ∪ 𝑘 ∈ (1..^𝑚)𝐵) |
71 | 68, 70 | difeq12d 3729 |
. . . . . . 7
⊢ (𝑛 = 𝑚 → (𝐴 ∖ ∪
𝑘 ∈ (1..^𝑛)𝐵) = (⦋𝑚 / 𝑛⦌𝐴 ∖ ∪
𝑘 ∈ (1..^𝑚)𝐵)) |
72 | 71 | eleq2d 2687 |
. . . . . 6
⊢ (𝑛 = 𝑚 → (𝑥 ∈ (𝐴 ∖ ∪
𝑘 ∈ (1..^𝑛)𝐵) ↔ 𝑥 ∈ (⦋𝑚 / 𝑛⦌𝐴 ∖ ∪
𝑘 ∈ (1..^𝑚)𝐵))) |
73 | 62, 67, 72 | cbvrex 3168 |
. . . . 5
⊢
(∃𝑛 ∈
(1..^𝑁)𝑥 ∈ (𝐴 ∖ ∪
𝑘 ∈ (1..^𝑛)𝐵) ↔ ∃𝑚 ∈ (1..^𝑁)𝑥 ∈ (⦋𝑚 / 𝑛⦌𝐴 ∖ ∪
𝑘 ∈ (1..^𝑚)𝐵)) |
74 | 61, 73 | sylibr 224 |
. . . 4
⊢
(∃𝑛 ∈
(1..^𝑁)𝑥 ∈ 𝐴 → ∃𝑛 ∈ (1..^𝑁)𝑥 ∈ (𝐴 ∖ ∪
𝑘 ∈ (1..^𝑛)𝐵)) |
75 | | eldifi 3732 |
. . . . 5
⊢ (𝑥 ∈ (𝐴 ∖ ∪
𝑘 ∈ (1..^𝑛)𝐵) → 𝑥 ∈ 𝐴) |
76 | 75 | reximi 3011 |
. . . 4
⊢
(∃𝑛 ∈
(1..^𝑁)𝑥 ∈ (𝐴 ∖ ∪
𝑘 ∈ (1..^𝑛)𝐵) → ∃𝑛 ∈ (1..^𝑁)𝑥 ∈ 𝐴) |
77 | 74, 76 | impbii 199 |
. . 3
⊢
(∃𝑛 ∈
(1..^𝑁)𝑥 ∈ 𝐴 ↔ ∃𝑛 ∈ (1..^𝑁)𝑥 ∈ (𝐴 ∖ ∪
𝑘 ∈ (1..^𝑛)𝐵)) |
78 | | eliun 4524 |
. . 3
⊢ (𝑥 ∈ ∪ 𝑛 ∈ (1..^𝑁)𝐴 ↔ ∃𝑛 ∈ (1..^𝑁)𝑥 ∈ 𝐴) |
79 | | eliun 4524 |
. . 3
⊢ (𝑥 ∈ ∪ 𝑛 ∈ (1..^𝑁)(𝐴 ∖ ∪
𝑘 ∈ (1..^𝑛)𝐵) ↔ ∃𝑛 ∈ (1..^𝑁)𝑥 ∈ (𝐴 ∖ ∪
𝑘 ∈ (1..^𝑛)𝐵)) |
80 | 77, 78, 79 | 3bitr4i 292 |
. 2
⊢ (𝑥 ∈ ∪ 𝑛 ∈ (1..^𝑁)𝐴 ↔ 𝑥 ∈ ∪
𝑛 ∈ (1..^𝑁)(𝐴 ∖ ∪
𝑘 ∈ (1..^𝑛)𝐵)) |
81 | 80 | eqriv 2619 |
1
⊢ ∪ 𝑛 ∈ (1..^𝑁)𝐴 = ∪ 𝑛 ∈ (1..^𝑁)(𝐴 ∖ ∪
𝑘 ∈ (1..^𝑛)𝐵) |