Step | Hyp | Ref
| Expression |
1 | | ssrab2 3908 |
. . . . . . . . . 10
⊢ {𝑛 ∈ ℕ ∣ 𝑥 ∈ 𝐴} ⊆ ℕ |
2 | | nnuz 12033 |
. . . . . . . . . 10
⊢ ℕ =
(ℤ≥‘1) |
3 | 1, 2 | sseqtri 3856 |
. . . . . . . . 9
⊢ {𝑛 ∈ ℕ ∣ 𝑥 ∈ 𝐴} ⊆
(ℤ≥‘1) |
4 | | rabn0 4188 |
. . . . . . . . . 10
⊢ ({𝑛 ∈ ℕ ∣ 𝑥 ∈ 𝐴} ≠ ∅ ↔ ∃𝑛 ∈ ℕ 𝑥 ∈ 𝐴) |
5 | 4 | biimpri 220 |
. . . . . . . . 9
⊢
(∃𝑛 ∈
ℕ 𝑥 ∈ 𝐴 → {𝑛 ∈ ℕ ∣ 𝑥 ∈ 𝐴} ≠ ∅) |
6 | | infssuzcl 12083 |
. . . . . . . . 9
⊢ (({𝑛 ∈ ℕ ∣ 𝑥 ∈ 𝐴} ⊆ (ℤ≥‘1)
∧ {𝑛 ∈ ℕ
∣ 𝑥 ∈ 𝐴} ≠ ∅) →
inf({𝑛 ∈ ℕ
∣ 𝑥 ∈ 𝐴}, ℝ, < ) ∈ {𝑛 ∈ ℕ ∣ 𝑥 ∈ 𝐴}) |
7 | 3, 5, 6 | sylancr 581 |
. . . . . . . 8
⊢
(∃𝑛 ∈
ℕ 𝑥 ∈ 𝐴 → inf({𝑛 ∈ ℕ ∣ 𝑥 ∈ 𝐴}, ℝ, < ) ∈ {𝑛 ∈ ℕ ∣ 𝑥 ∈ 𝐴}) |
8 | | nfrab1 3309 |
. . . . . . . . . 10
⊢
Ⅎ𝑛{𝑛 ∈ ℕ ∣ 𝑥 ∈ 𝐴} |
9 | | nfcv 2934 |
. . . . . . . . . 10
⊢
Ⅎ𝑛ℝ |
10 | | nfcv 2934 |
. . . . . . . . . 10
⊢
Ⅎ𝑛
< |
11 | 8, 9, 10 | nfinf 8678 |
. . . . . . . . 9
⊢
Ⅎ𝑛inf({𝑛 ∈ ℕ ∣ 𝑥 ∈ 𝐴}, ℝ, < ) |
12 | | nfcv 2934 |
. . . . . . . . 9
⊢
Ⅎ𝑛ℕ |
13 | 11 | nfcsb1 3766 |
. . . . . . . . . 10
⊢
Ⅎ𝑛⦋inf({𝑛 ∈ ℕ ∣ 𝑥 ∈ 𝐴}, ℝ, < ) / 𝑛⦌𝐴 |
14 | 13 | nfcri 2929 |
. . . . . . . . 9
⊢
Ⅎ𝑛 𝑥 ∈
⦋inf({𝑛
∈ ℕ ∣ 𝑥
∈ 𝐴}, ℝ, < )
/ 𝑛⦌𝐴 |
15 | | csbeq1a 3760 |
. . . . . . . . . 10
⊢ (𝑛 = inf({𝑛 ∈ ℕ ∣ 𝑥 ∈ 𝐴}, ℝ, < ) → 𝐴 = ⦋inf({𝑛 ∈ ℕ ∣ 𝑥 ∈ 𝐴}, ℝ, < ) / 𝑛⦌𝐴) |
16 | 15 | eleq2d 2845 |
. . . . . . . . 9
⊢ (𝑛 = inf({𝑛 ∈ ℕ ∣ 𝑥 ∈ 𝐴}, ℝ, < ) → (𝑥 ∈ 𝐴 ↔ 𝑥 ∈ ⦋inf({𝑛 ∈ ℕ ∣ 𝑥 ∈ 𝐴}, ℝ, < ) / 𝑛⦌𝐴)) |
17 | 11, 12, 14, 16 | elrabf 3568 |
. . . . . . . 8
⊢
(inf({𝑛 ∈
ℕ ∣ 𝑥 ∈
𝐴}, ℝ, < ) ∈
{𝑛 ∈ ℕ ∣
𝑥 ∈ 𝐴} ↔ (inf({𝑛 ∈ ℕ ∣ 𝑥 ∈ 𝐴}, ℝ, < ) ∈ ℕ ∧
𝑥 ∈
⦋inf({𝑛
∈ ℕ ∣ 𝑥
∈ 𝐴}, ℝ, < )
/ 𝑛⦌𝐴)) |
18 | 7, 17 | sylib 210 |
. . . . . . 7
⊢
(∃𝑛 ∈
ℕ 𝑥 ∈ 𝐴 → (inf({𝑛 ∈ ℕ ∣ 𝑥 ∈ 𝐴}, ℝ, < ) ∈ ℕ ∧
𝑥 ∈
⦋inf({𝑛
∈ ℕ ∣ 𝑥
∈ 𝐴}, ℝ, < )
/ 𝑛⦌𝐴)) |
19 | 18 | simpld 490 |
. . . . . 6
⊢
(∃𝑛 ∈
ℕ 𝑥 ∈ 𝐴 → inf({𝑛 ∈ ℕ ∣ 𝑥 ∈ 𝐴}, ℝ, < ) ∈
ℕ) |
20 | 18 | simprd 491 |
. . . . . . 7
⊢
(∃𝑛 ∈
ℕ 𝑥 ∈ 𝐴 → 𝑥 ∈ ⦋inf({𝑛 ∈ ℕ ∣ 𝑥 ∈ 𝐴}, ℝ, < ) / 𝑛⦌𝐴) |
21 | 19 | nnred 11395 |
. . . . . . . . 9
⊢
(∃𝑛 ∈
ℕ 𝑥 ∈ 𝐴 → inf({𝑛 ∈ ℕ ∣ 𝑥 ∈ 𝐴}, ℝ, < ) ∈
ℝ) |
22 | 21 | ltnrd 10512 |
. . . . . . . 8
⊢
(∃𝑛 ∈
ℕ 𝑥 ∈ 𝐴 → ¬ inf({𝑛 ∈ ℕ ∣ 𝑥 ∈ 𝐴}, ℝ, < ) < inf({𝑛 ∈ ℕ ∣ 𝑥 ∈ 𝐴}, ℝ, < )) |
23 | | eliun 4759 |
. . . . . . . . 9
⊢ (𝑥 ∈ ∪ 𝑘 ∈ (1..^inf({𝑛 ∈ ℕ ∣ 𝑥 ∈ 𝐴}, ℝ, < ))𝐵 ↔ ∃𝑘 ∈ (1..^inf({𝑛 ∈ ℕ ∣ 𝑥 ∈ 𝐴}, ℝ, < ))𝑥 ∈ 𝐵) |
24 | 21 | ad2antrr 716 |
. . . . . . . . . . 11
⊢
(((∃𝑛 ∈
ℕ 𝑥 ∈ 𝐴 ∧ 𝑘 ∈ (1..^inf({𝑛 ∈ ℕ ∣ 𝑥 ∈ 𝐴}, ℝ, < ))) ∧ 𝑥 ∈ 𝐵) → inf({𝑛 ∈ ℕ ∣ 𝑥 ∈ 𝐴}, ℝ, < ) ∈
ℝ) |
25 | | elfzouz 12797 |
. . . . . . . . . . . . . 14
⊢ (𝑘 ∈ (1..^inf({𝑛 ∈ ℕ ∣ 𝑥 ∈ 𝐴}, ℝ, < )) → 𝑘 ∈
(ℤ≥‘1)) |
26 | 25, 2 | syl6eleqr 2870 |
. . . . . . . . . . . . 13
⊢ (𝑘 ∈ (1..^inf({𝑛 ∈ ℕ ∣ 𝑥 ∈ 𝐴}, ℝ, < )) → 𝑘 ∈
ℕ) |
27 | 26 | ad2antlr 717 |
. . . . . . . . . . . 12
⊢
(((∃𝑛 ∈
ℕ 𝑥 ∈ 𝐴 ∧ 𝑘 ∈ (1..^inf({𝑛 ∈ ℕ ∣ 𝑥 ∈ 𝐴}, ℝ, < ))) ∧ 𝑥 ∈ 𝐵) → 𝑘 ∈ ℕ) |
28 | 27 | nnred 11395 |
. . . . . . . . . . 11
⊢
(((∃𝑛 ∈
ℕ 𝑥 ∈ 𝐴 ∧ 𝑘 ∈ (1..^inf({𝑛 ∈ ℕ ∣ 𝑥 ∈ 𝐴}, ℝ, < ))) ∧ 𝑥 ∈ 𝐵) → 𝑘 ∈ ℝ) |
29 | | simpr 479 |
. . . . . . . . . . . . 13
⊢
(((∃𝑛 ∈
ℕ 𝑥 ∈ 𝐴 ∧ 𝑘 ∈ (1..^inf({𝑛 ∈ ℕ ∣ 𝑥 ∈ 𝐴}, ℝ, < ))) ∧ 𝑥 ∈ 𝐵) → 𝑥 ∈ 𝐵) |
30 | | iundisj.1 |
. . . . . . . . . . . . . . 15
⊢ (𝑛 = 𝑘 → 𝐴 = 𝐵) |
31 | 30 | eleq2d 2845 |
. . . . . . . . . . . . . 14
⊢ (𝑛 = 𝑘 → (𝑥 ∈ 𝐴 ↔ 𝑥 ∈ 𝐵)) |
32 | 31 | elrab 3572 |
. . . . . . . . . . . . 13
⊢ (𝑘 ∈ {𝑛 ∈ ℕ ∣ 𝑥 ∈ 𝐴} ↔ (𝑘 ∈ ℕ ∧ 𝑥 ∈ 𝐵)) |
33 | 27, 29, 32 | sylanbrc 578 |
. . . . . . . . . . . 12
⊢
(((∃𝑛 ∈
ℕ 𝑥 ∈ 𝐴 ∧ 𝑘 ∈ (1..^inf({𝑛 ∈ ℕ ∣ 𝑥 ∈ 𝐴}, ℝ, < ))) ∧ 𝑥 ∈ 𝐵) → 𝑘 ∈ {𝑛 ∈ ℕ ∣ 𝑥 ∈ 𝐴}) |
34 | | infssuzle 12082 |
. . . . . . . . . . . 12
⊢ (({𝑛 ∈ ℕ ∣ 𝑥 ∈ 𝐴} ⊆ (ℤ≥‘1)
∧ 𝑘 ∈ {𝑛 ∈ ℕ ∣ 𝑥 ∈ 𝐴}) → inf({𝑛 ∈ ℕ ∣ 𝑥 ∈ 𝐴}, ℝ, < ) ≤ 𝑘) |
35 | 3, 33, 34 | sylancr 581 |
. . . . . . . . . . 11
⊢
(((∃𝑛 ∈
ℕ 𝑥 ∈ 𝐴 ∧ 𝑘 ∈ (1..^inf({𝑛 ∈ ℕ ∣ 𝑥 ∈ 𝐴}, ℝ, < ))) ∧ 𝑥 ∈ 𝐵) → inf({𝑛 ∈ ℕ ∣ 𝑥 ∈ 𝐴}, ℝ, < ) ≤ 𝑘) |
36 | | elfzolt2 12802 |
. . . . . . . . . . . 12
⊢ (𝑘 ∈ (1..^inf({𝑛 ∈ ℕ ∣ 𝑥 ∈ 𝐴}, ℝ, < )) → 𝑘 < inf({𝑛 ∈ ℕ ∣ 𝑥 ∈ 𝐴}, ℝ, < )) |
37 | 36 | ad2antlr 717 |
. . . . . . . . . . 11
⊢
(((∃𝑛 ∈
ℕ 𝑥 ∈ 𝐴 ∧ 𝑘 ∈ (1..^inf({𝑛 ∈ ℕ ∣ 𝑥 ∈ 𝐴}, ℝ, < ))) ∧ 𝑥 ∈ 𝐵) → 𝑘 < inf({𝑛 ∈ ℕ ∣ 𝑥 ∈ 𝐴}, ℝ, < )) |
38 | 24, 28, 24, 35, 37 | lelttrd 10536 |
. . . . . . . . . 10
⊢
(((∃𝑛 ∈
ℕ 𝑥 ∈ 𝐴 ∧ 𝑘 ∈ (1..^inf({𝑛 ∈ ℕ ∣ 𝑥 ∈ 𝐴}, ℝ, < ))) ∧ 𝑥 ∈ 𝐵) → inf({𝑛 ∈ ℕ ∣ 𝑥 ∈ 𝐴}, ℝ, < ) < inf({𝑛 ∈ ℕ ∣ 𝑥 ∈ 𝐴}, ℝ, < )) |
39 | 38 | rexlimdva2 3216 |
. . . . . . . . 9
⊢
(∃𝑛 ∈
ℕ 𝑥 ∈ 𝐴 → (∃𝑘 ∈ (1..^inf({𝑛 ∈ ℕ ∣ 𝑥 ∈ 𝐴}, ℝ, < ))𝑥 ∈ 𝐵 → inf({𝑛 ∈ ℕ ∣ 𝑥 ∈ 𝐴}, ℝ, < ) < inf({𝑛 ∈ ℕ ∣ 𝑥 ∈ 𝐴}, ℝ, < ))) |
40 | 23, 39 | syl5bi 234 |
. . . . . . . 8
⊢
(∃𝑛 ∈
ℕ 𝑥 ∈ 𝐴 → (𝑥 ∈ ∪
𝑘 ∈ (1..^inf({𝑛 ∈ ℕ ∣ 𝑥 ∈ 𝐴}, ℝ, < ))𝐵 → inf({𝑛 ∈ ℕ ∣ 𝑥 ∈ 𝐴}, ℝ, < ) < inf({𝑛 ∈ ℕ ∣ 𝑥 ∈ 𝐴}, ℝ, < ))) |
41 | 22, 40 | mtod 190 |
. . . . . . 7
⊢
(∃𝑛 ∈
ℕ 𝑥 ∈ 𝐴 → ¬ 𝑥 ∈ ∪
𝑘 ∈ (1..^inf({𝑛 ∈ ℕ ∣ 𝑥 ∈ 𝐴}, ℝ, < ))𝐵) |
42 | 20, 41 | eldifd 3803 |
. . . . . 6
⊢
(∃𝑛 ∈
ℕ 𝑥 ∈ 𝐴 → 𝑥 ∈ (⦋inf({𝑛 ∈ ℕ ∣ 𝑥 ∈ 𝐴}, ℝ, < ) / 𝑛⦌𝐴 ∖ ∪
𝑘 ∈ (1..^inf({𝑛 ∈ ℕ ∣ 𝑥 ∈ 𝐴}, ℝ, < ))𝐵)) |
43 | | csbeq1 3754 |
. . . . . . . . 9
⊢ (𝑚 = inf({𝑛 ∈ ℕ ∣ 𝑥 ∈ 𝐴}, ℝ, < ) →
⦋𝑚 / 𝑛⦌𝐴 = ⦋inf({𝑛 ∈ ℕ ∣ 𝑥 ∈ 𝐴}, ℝ, < ) / 𝑛⦌𝐴) |
44 | | oveq2 6932 |
. . . . . . . . . 10
⊢ (𝑚 = inf({𝑛 ∈ ℕ ∣ 𝑥 ∈ 𝐴}, ℝ, < ) → (1..^𝑚) = (1..^inf({𝑛 ∈ ℕ ∣ 𝑥 ∈ 𝐴}, ℝ, < ))) |
45 | 44 | iuneq1d 4780 |
. . . . . . . . 9
⊢ (𝑚 = inf({𝑛 ∈ ℕ ∣ 𝑥 ∈ 𝐴}, ℝ, < ) → ∪ 𝑘 ∈ (1..^𝑚)𝐵 = ∪ 𝑘 ∈ (1..^inf({𝑛 ∈ ℕ ∣ 𝑥 ∈ 𝐴}, ℝ, < ))𝐵) |
46 | 43, 45 | difeq12d 3952 |
. . . . . . . 8
⊢ (𝑚 = inf({𝑛 ∈ ℕ ∣ 𝑥 ∈ 𝐴}, ℝ, < ) →
(⦋𝑚 / 𝑛⦌𝐴 ∖ ∪
𝑘 ∈ (1..^𝑚)𝐵) = (⦋inf({𝑛 ∈ ℕ ∣ 𝑥 ∈ 𝐴}, ℝ, < ) / 𝑛⦌𝐴 ∖ ∪
𝑘 ∈ (1..^inf({𝑛 ∈ ℕ ∣ 𝑥 ∈ 𝐴}, ℝ, < ))𝐵)) |
47 | 46 | eleq2d 2845 |
. . . . . . 7
⊢ (𝑚 = inf({𝑛 ∈ ℕ ∣ 𝑥 ∈ 𝐴}, ℝ, < ) → (𝑥 ∈ (⦋𝑚 / 𝑛⦌𝐴 ∖ ∪
𝑘 ∈ (1..^𝑚)𝐵) ↔ 𝑥 ∈ (⦋inf({𝑛 ∈ ℕ ∣ 𝑥 ∈ 𝐴}, ℝ, < ) / 𝑛⦌𝐴 ∖ ∪
𝑘 ∈ (1..^inf({𝑛 ∈ ℕ ∣ 𝑥 ∈ 𝐴}, ℝ, < ))𝐵))) |
48 | 47 | rspcev 3511 |
. . . . . 6
⊢
((inf({𝑛 ∈
ℕ ∣ 𝑥 ∈
𝐴}, ℝ, < ) ∈
ℕ ∧ 𝑥 ∈
(⦋inf({𝑛
∈ ℕ ∣ 𝑥
∈ 𝐴}, ℝ, < )
/ 𝑛⦌𝐴 ∖ ∪ 𝑘 ∈ (1..^inf({𝑛 ∈ ℕ ∣ 𝑥 ∈ 𝐴}, ℝ, < ))𝐵)) → ∃𝑚 ∈ ℕ 𝑥 ∈ (⦋𝑚 / 𝑛⦌𝐴 ∖ ∪
𝑘 ∈ (1..^𝑚)𝐵)) |
49 | 19, 42, 48 | syl2anc 579 |
. . . . 5
⊢
(∃𝑛 ∈
ℕ 𝑥 ∈ 𝐴 → ∃𝑚 ∈ ℕ 𝑥 ∈ (⦋𝑚 / 𝑛⦌𝐴 ∖ ∪
𝑘 ∈ (1..^𝑚)𝐵)) |
50 | | nfv 1957 |
. . . . . 6
⊢
Ⅎ𝑚 𝑥 ∈ (𝐴 ∖ ∪
𝑘 ∈ (1..^𝑛)𝐵) |
51 | | nfcsb1v 3767 |
. . . . . . . 8
⊢
Ⅎ𝑛⦋𝑚 / 𝑛⦌𝐴 |
52 | | nfcv 2934 |
. . . . . . . 8
⊢
Ⅎ𝑛∪ 𝑘 ∈ (1..^𝑚)𝐵 |
53 | 51, 52 | nfdif 3954 |
. . . . . . 7
⊢
Ⅎ𝑛(⦋𝑚 / 𝑛⦌𝐴 ∖ ∪
𝑘 ∈ (1..^𝑚)𝐵) |
54 | 53 | nfcri 2929 |
. . . . . 6
⊢
Ⅎ𝑛 𝑥 ∈ (⦋𝑚 / 𝑛⦌𝐴 ∖ ∪
𝑘 ∈ (1..^𝑚)𝐵) |
55 | | csbeq1a 3760 |
. . . . . . . 8
⊢ (𝑛 = 𝑚 → 𝐴 = ⦋𝑚 / 𝑛⦌𝐴) |
56 | | oveq2 6932 |
. . . . . . . . 9
⊢ (𝑛 = 𝑚 → (1..^𝑛) = (1..^𝑚)) |
57 | 56 | iuneq1d 4780 |
. . . . . . . 8
⊢ (𝑛 = 𝑚 → ∪
𝑘 ∈ (1..^𝑛)𝐵 = ∪ 𝑘 ∈ (1..^𝑚)𝐵) |
58 | 55, 57 | difeq12d 3952 |
. . . . . . 7
⊢ (𝑛 = 𝑚 → (𝐴 ∖ ∪
𝑘 ∈ (1..^𝑛)𝐵) = (⦋𝑚 / 𝑛⦌𝐴 ∖ ∪
𝑘 ∈ (1..^𝑚)𝐵)) |
59 | 58 | eleq2d 2845 |
. . . . . 6
⊢ (𝑛 = 𝑚 → (𝑥 ∈ (𝐴 ∖ ∪
𝑘 ∈ (1..^𝑛)𝐵) ↔ 𝑥 ∈ (⦋𝑚 / 𝑛⦌𝐴 ∖ ∪
𝑘 ∈ (1..^𝑚)𝐵))) |
60 | 50, 54, 59 | cbvrex 3364 |
. . . . 5
⊢
(∃𝑛 ∈
ℕ 𝑥 ∈ (𝐴 ∖ ∪ 𝑘 ∈ (1..^𝑛)𝐵) ↔ ∃𝑚 ∈ ℕ 𝑥 ∈ (⦋𝑚 / 𝑛⦌𝐴 ∖ ∪
𝑘 ∈ (1..^𝑚)𝐵)) |
61 | 49, 60 | sylibr 226 |
. . . 4
⊢
(∃𝑛 ∈
ℕ 𝑥 ∈ 𝐴 → ∃𝑛 ∈ ℕ 𝑥 ∈ (𝐴 ∖ ∪
𝑘 ∈ (1..^𝑛)𝐵)) |
62 | | eldifi 3955 |
. . . . 5
⊢ (𝑥 ∈ (𝐴 ∖ ∪
𝑘 ∈ (1..^𝑛)𝐵) → 𝑥 ∈ 𝐴) |
63 | 62 | reximi 3192 |
. . . 4
⊢
(∃𝑛 ∈
ℕ 𝑥 ∈ (𝐴 ∖ ∪ 𝑘 ∈ (1..^𝑛)𝐵) → ∃𝑛 ∈ ℕ 𝑥 ∈ 𝐴) |
64 | 61, 63 | impbii 201 |
. . 3
⊢
(∃𝑛 ∈
ℕ 𝑥 ∈ 𝐴 ↔ ∃𝑛 ∈ ℕ 𝑥 ∈ (𝐴 ∖ ∪
𝑘 ∈ (1..^𝑛)𝐵)) |
65 | | eliun 4759 |
. . 3
⊢ (𝑥 ∈ ∪ 𝑛 ∈ ℕ 𝐴 ↔ ∃𝑛 ∈ ℕ 𝑥 ∈ 𝐴) |
66 | | eliun 4759 |
. . 3
⊢ (𝑥 ∈ ∪ 𝑛 ∈ ℕ (𝐴 ∖ ∪
𝑘 ∈ (1..^𝑛)𝐵) ↔ ∃𝑛 ∈ ℕ 𝑥 ∈ (𝐴 ∖ ∪
𝑘 ∈ (1..^𝑛)𝐵)) |
67 | 64, 65, 66 | 3bitr4i 295 |
. 2
⊢ (𝑥 ∈ ∪ 𝑛 ∈ ℕ 𝐴 ↔ 𝑥 ∈ ∪
𝑛 ∈ ℕ (𝐴 ∖ ∪ 𝑘 ∈ (1..^𝑛)𝐵)) |
68 | 67 | eqriv 2775 |
1
⊢ ∪ 𝑛 ∈ ℕ 𝐴 = ∪ 𝑛 ∈ ℕ (𝐴 ∖ ∪ 𝑘 ∈ (1..^𝑛)𝐵) |