Step | Hyp | Ref
| Expression |
1 | | ssrab2 3650 |
. . . . . . . . . 10
⊢ {𝑛 ∈ ℕ ∣ 𝑥 ∈ 𝐴} ⊆ ℕ |
2 | | nnuz 11599 |
. . . . . . . . . 10
⊢ ℕ =
(ℤ≥‘1) |
3 | 1, 2 | sseqtri 3600 |
. . . . . . . . 9
⊢ {𝑛 ∈ ℕ ∣ 𝑥 ∈ 𝐴} ⊆
(ℤ≥‘1) |
4 | | rabn0 3912 |
. . . . . . . . . 10
⊢ ({𝑛 ∈ ℕ ∣ 𝑥 ∈ 𝐴} ≠ ∅ ↔ ∃𝑛 ∈ ℕ 𝑥 ∈ 𝐴) |
5 | 4 | biimpri 217 |
. . . . . . . . 9
⊢
(∃𝑛 ∈
ℕ 𝑥 ∈ 𝐴 → {𝑛 ∈ ℕ ∣ 𝑥 ∈ 𝐴} ≠ ∅) |
6 | | infssuzcl 11648 |
. . . . . . . . 9
⊢ (({𝑛 ∈ ℕ ∣ 𝑥 ∈ 𝐴} ⊆ (ℤ≥‘1)
∧ {𝑛 ∈ ℕ
∣ 𝑥 ∈ 𝐴} ≠ ∅) →
inf({𝑛 ∈ ℕ
∣ 𝑥 ∈ 𝐴}, ℝ, < ) ∈ {𝑛 ∈ ℕ ∣ 𝑥 ∈ 𝐴}) |
7 | 3, 5, 6 | sylancr 694 |
. . . . . . . 8
⊢
(∃𝑛 ∈
ℕ 𝑥 ∈ 𝐴 → inf({𝑛 ∈ ℕ ∣ 𝑥 ∈ 𝐴}, ℝ, < ) ∈ {𝑛 ∈ ℕ ∣ 𝑥 ∈ 𝐴}) |
8 | | nfrab1 3099 |
. . . . . . . . . 10
⊢
Ⅎ𝑛{𝑛 ∈ ℕ ∣ 𝑥 ∈ 𝐴} |
9 | | nfcv 2751 |
. . . . . . . . . 10
⊢
Ⅎ𝑛ℝ |
10 | | nfcv 2751 |
. . . . . . . . . 10
⊢
Ⅎ𝑛
< |
11 | 8, 9, 10 | nfinf 8271 |
. . . . . . . . 9
⊢
Ⅎ𝑛inf({𝑛 ∈ ℕ ∣ 𝑥 ∈ 𝐴}, ℝ, < ) |
12 | | nfcv 2751 |
. . . . . . . . 9
⊢
Ⅎ𝑛ℕ |
13 | 11 | nfcsb1 3514 |
. . . . . . . . . 10
⊢
Ⅎ𝑛⦋inf({𝑛 ∈ ℕ ∣ 𝑥 ∈ 𝐴}, ℝ, < ) / 𝑛⦌𝐴 |
14 | 13 | nfcri 2745 |
. . . . . . . . 9
⊢
Ⅎ𝑛 𝑥 ∈
⦋inf({𝑛
∈ ℕ ∣ 𝑥
∈ 𝐴}, ℝ, < )
/ 𝑛⦌𝐴 |
15 | | csbeq1a 3508 |
. . . . . . . . . 10
⊢ (𝑛 = inf({𝑛 ∈ ℕ ∣ 𝑥 ∈ 𝐴}, ℝ, < ) → 𝐴 = ⦋inf({𝑛 ∈ ℕ ∣ 𝑥 ∈ 𝐴}, ℝ, < ) / 𝑛⦌𝐴) |
16 | 15 | eleq2d 2673 |
. . . . . . . . 9
⊢ (𝑛 = inf({𝑛 ∈ ℕ ∣ 𝑥 ∈ 𝐴}, ℝ, < ) → (𝑥 ∈ 𝐴 ↔ 𝑥 ∈ ⦋inf({𝑛 ∈ ℕ ∣ 𝑥 ∈ 𝐴}, ℝ, < ) / 𝑛⦌𝐴)) |
17 | 11, 12, 14, 16 | elrabf 3329 |
. . . . . . . 8
⊢
(inf({𝑛 ∈
ℕ ∣ 𝑥 ∈
𝐴}, ℝ, < ) ∈
{𝑛 ∈ ℕ ∣
𝑥 ∈ 𝐴} ↔ (inf({𝑛 ∈ ℕ ∣ 𝑥 ∈ 𝐴}, ℝ, < ) ∈ ℕ ∧
𝑥 ∈
⦋inf({𝑛
∈ ℕ ∣ 𝑥
∈ 𝐴}, ℝ, < )
/ 𝑛⦌𝐴)) |
18 | 7, 17 | sylib 207 |
. . . . . . 7
⊢
(∃𝑛 ∈
ℕ 𝑥 ∈ 𝐴 → (inf({𝑛 ∈ ℕ ∣ 𝑥 ∈ 𝐴}, ℝ, < ) ∈ ℕ ∧
𝑥 ∈
⦋inf({𝑛
∈ ℕ ∣ 𝑥
∈ 𝐴}, ℝ, < )
/ 𝑛⦌𝐴)) |
19 | 18 | simpld 474 |
. . . . . 6
⊢
(∃𝑛 ∈
ℕ 𝑥 ∈ 𝐴 → inf({𝑛 ∈ ℕ ∣ 𝑥 ∈ 𝐴}, ℝ, < ) ∈
ℕ) |
20 | 18 | simprd 478 |
. . . . . . 7
⊢
(∃𝑛 ∈
ℕ 𝑥 ∈ 𝐴 → 𝑥 ∈ ⦋inf({𝑛 ∈ ℕ ∣ 𝑥 ∈ 𝐴}, ℝ, < ) / 𝑛⦌𝐴) |
21 | 19 | nnred 10912 |
. . . . . . . . 9
⊢
(∃𝑛 ∈
ℕ 𝑥 ∈ 𝐴 → inf({𝑛 ∈ ℕ ∣ 𝑥 ∈ 𝐴}, ℝ, < ) ∈
ℝ) |
22 | 21 | ltnrd 10050 |
. . . . . . . 8
⊢
(∃𝑛 ∈
ℕ 𝑥 ∈ 𝐴 → ¬ inf({𝑛 ∈ ℕ ∣ 𝑥 ∈ 𝐴}, ℝ, < ) < inf({𝑛 ∈ ℕ ∣ 𝑥 ∈ 𝐴}, ℝ, < )) |
23 | | eliun 4460 |
. . . . . . . . 9
⊢ (𝑥 ∈ ∪ 𝑘 ∈ (1..^inf({𝑛 ∈ ℕ ∣ 𝑥 ∈ 𝐴}, ℝ, < ))𝐵 ↔ ∃𝑘 ∈ (1..^inf({𝑛 ∈ ℕ ∣ 𝑥 ∈ 𝐴}, ℝ, < ))𝑥 ∈ 𝐵) |
24 | 21 | ad2antrr 758 |
. . . . . . . . . . . 12
⊢
(((∃𝑛 ∈
ℕ 𝑥 ∈ 𝐴 ∧ 𝑘 ∈ (1..^inf({𝑛 ∈ ℕ ∣ 𝑥 ∈ 𝐴}, ℝ, < ))) ∧ 𝑥 ∈ 𝐵) → inf({𝑛 ∈ ℕ ∣ 𝑥 ∈ 𝐴}, ℝ, < ) ∈
ℝ) |
25 | | elfzouz 12343 |
. . . . . . . . . . . . . . 15
⊢ (𝑘 ∈ (1..^inf({𝑛 ∈ ℕ ∣ 𝑥 ∈ 𝐴}, ℝ, < )) → 𝑘 ∈
(ℤ≥‘1)) |
26 | 25, 2 | syl6eleqr 2699 |
. . . . . . . . . . . . . 14
⊢ (𝑘 ∈ (1..^inf({𝑛 ∈ ℕ ∣ 𝑥 ∈ 𝐴}, ℝ, < )) → 𝑘 ∈
ℕ) |
27 | 26 | ad2antlr 759 |
. . . . . . . . . . . . 13
⊢
(((∃𝑛 ∈
ℕ 𝑥 ∈ 𝐴 ∧ 𝑘 ∈ (1..^inf({𝑛 ∈ ℕ ∣ 𝑥 ∈ 𝐴}, ℝ, < ))) ∧ 𝑥 ∈ 𝐵) → 𝑘 ∈ ℕ) |
28 | 27 | nnred 10912 |
. . . . . . . . . . . 12
⊢
(((∃𝑛 ∈
ℕ 𝑥 ∈ 𝐴 ∧ 𝑘 ∈ (1..^inf({𝑛 ∈ ℕ ∣ 𝑥 ∈ 𝐴}, ℝ, < ))) ∧ 𝑥 ∈ 𝐵) → 𝑘 ∈ ℝ) |
29 | | simpr 476 |
. . . . . . . . . . . . . 14
⊢
(((∃𝑛 ∈
ℕ 𝑥 ∈ 𝐴 ∧ 𝑘 ∈ (1..^inf({𝑛 ∈ ℕ ∣ 𝑥 ∈ 𝐴}, ℝ, < ))) ∧ 𝑥 ∈ 𝐵) → 𝑥 ∈ 𝐵) |
30 | | iundisj.1 |
. . . . . . . . . . . . . . . 16
⊢ (𝑛 = 𝑘 → 𝐴 = 𝐵) |
31 | 30 | eleq2d 2673 |
. . . . . . . . . . . . . . 15
⊢ (𝑛 = 𝑘 → (𝑥 ∈ 𝐴 ↔ 𝑥 ∈ 𝐵)) |
32 | 31 | elrab 3331 |
. . . . . . . . . . . . . 14
⊢ (𝑘 ∈ {𝑛 ∈ ℕ ∣ 𝑥 ∈ 𝐴} ↔ (𝑘 ∈ ℕ ∧ 𝑥 ∈ 𝐵)) |
33 | 27, 29, 32 | sylanbrc 695 |
. . . . . . . . . . . . 13
⊢
(((∃𝑛 ∈
ℕ 𝑥 ∈ 𝐴 ∧ 𝑘 ∈ (1..^inf({𝑛 ∈ ℕ ∣ 𝑥 ∈ 𝐴}, ℝ, < ))) ∧ 𝑥 ∈ 𝐵) → 𝑘 ∈ {𝑛 ∈ ℕ ∣ 𝑥 ∈ 𝐴}) |
34 | | infssuzle 11647 |
. . . . . . . . . . . . 13
⊢ (({𝑛 ∈ ℕ ∣ 𝑥 ∈ 𝐴} ⊆ (ℤ≥‘1)
∧ 𝑘 ∈ {𝑛 ∈ ℕ ∣ 𝑥 ∈ 𝐴}) → inf({𝑛 ∈ ℕ ∣ 𝑥 ∈ 𝐴}, ℝ, < ) ≤ 𝑘) |
35 | 3, 33, 34 | sylancr 694 |
. . . . . . . . . . . 12
⊢
(((∃𝑛 ∈
ℕ 𝑥 ∈ 𝐴 ∧ 𝑘 ∈ (1..^inf({𝑛 ∈ ℕ ∣ 𝑥 ∈ 𝐴}, ℝ, < ))) ∧ 𝑥 ∈ 𝐵) → inf({𝑛 ∈ ℕ ∣ 𝑥 ∈ 𝐴}, ℝ, < ) ≤ 𝑘) |
36 | | elfzolt2 12348 |
. . . . . . . . . . . . 13
⊢ (𝑘 ∈ (1..^inf({𝑛 ∈ ℕ ∣ 𝑥 ∈ 𝐴}, ℝ, < )) → 𝑘 < inf({𝑛 ∈ ℕ ∣ 𝑥 ∈ 𝐴}, ℝ, < )) |
37 | 36 | ad2antlr 759 |
. . . . . . . . . . . 12
⊢
(((∃𝑛 ∈
ℕ 𝑥 ∈ 𝐴 ∧ 𝑘 ∈ (1..^inf({𝑛 ∈ ℕ ∣ 𝑥 ∈ 𝐴}, ℝ, < ))) ∧ 𝑥 ∈ 𝐵) → 𝑘 < inf({𝑛 ∈ ℕ ∣ 𝑥 ∈ 𝐴}, ℝ, < )) |
38 | 24, 28, 24, 35, 37 | lelttrd 10074 |
. . . . . . . . . . 11
⊢
(((∃𝑛 ∈
ℕ 𝑥 ∈ 𝐴 ∧ 𝑘 ∈ (1..^inf({𝑛 ∈ ℕ ∣ 𝑥 ∈ 𝐴}, ℝ, < ))) ∧ 𝑥 ∈ 𝐵) → inf({𝑛 ∈ ℕ ∣ 𝑥 ∈ 𝐴}, ℝ, < ) < inf({𝑛 ∈ ℕ ∣ 𝑥 ∈ 𝐴}, ℝ, < )) |
39 | 38 | ex 449 |
. . . . . . . . . 10
⊢
((∃𝑛 ∈
ℕ 𝑥 ∈ 𝐴 ∧ 𝑘 ∈ (1..^inf({𝑛 ∈ ℕ ∣ 𝑥 ∈ 𝐴}, ℝ, < ))) → (𝑥 ∈ 𝐵 → inf({𝑛 ∈ ℕ ∣ 𝑥 ∈ 𝐴}, ℝ, < ) < inf({𝑛 ∈ ℕ ∣ 𝑥 ∈ 𝐴}, ℝ, < ))) |
40 | 39 | rexlimdva 3013 |
. . . . . . . . 9
⊢
(∃𝑛 ∈
ℕ 𝑥 ∈ 𝐴 → (∃𝑘 ∈ (1..^inf({𝑛 ∈ ℕ ∣ 𝑥 ∈ 𝐴}, ℝ, < ))𝑥 ∈ 𝐵 → inf({𝑛 ∈ ℕ ∣ 𝑥 ∈ 𝐴}, ℝ, < ) < inf({𝑛 ∈ ℕ ∣ 𝑥 ∈ 𝐴}, ℝ, < ))) |
41 | 23, 40 | syl5bi 231 |
. . . . . . . 8
⊢
(∃𝑛 ∈
ℕ 𝑥 ∈ 𝐴 → (𝑥 ∈ ∪
𝑘 ∈ (1..^inf({𝑛 ∈ ℕ ∣ 𝑥 ∈ 𝐴}, ℝ, < ))𝐵 → inf({𝑛 ∈ ℕ ∣ 𝑥 ∈ 𝐴}, ℝ, < ) < inf({𝑛 ∈ ℕ ∣ 𝑥 ∈ 𝐴}, ℝ, < ))) |
42 | 22, 41 | mtod 188 |
. . . . . . 7
⊢
(∃𝑛 ∈
ℕ 𝑥 ∈ 𝐴 → ¬ 𝑥 ∈ ∪
𝑘 ∈ (1..^inf({𝑛 ∈ ℕ ∣ 𝑥 ∈ 𝐴}, ℝ, < ))𝐵) |
43 | 20, 42 | eldifd 3551 |
. . . . . 6
⊢
(∃𝑛 ∈
ℕ 𝑥 ∈ 𝐴 → 𝑥 ∈ (⦋inf({𝑛 ∈ ℕ ∣ 𝑥 ∈ 𝐴}, ℝ, < ) / 𝑛⦌𝐴 ∖ ∪
𝑘 ∈ (1..^inf({𝑛 ∈ ℕ ∣ 𝑥 ∈ 𝐴}, ℝ, < ))𝐵)) |
44 | | csbeq1 3502 |
. . . . . . . . 9
⊢ (𝑚 = inf({𝑛 ∈ ℕ ∣ 𝑥 ∈ 𝐴}, ℝ, < ) →
⦋𝑚 / 𝑛⦌𝐴 = ⦋inf({𝑛 ∈ ℕ ∣ 𝑥 ∈ 𝐴}, ℝ, < ) / 𝑛⦌𝐴) |
45 | | oveq2 6557 |
. . . . . . . . . 10
⊢ (𝑚 = inf({𝑛 ∈ ℕ ∣ 𝑥 ∈ 𝐴}, ℝ, < ) → (1..^𝑚) = (1..^inf({𝑛 ∈ ℕ ∣ 𝑥 ∈ 𝐴}, ℝ, < ))) |
46 | 45 | iuneq1d 4481 |
. . . . . . . . 9
⊢ (𝑚 = inf({𝑛 ∈ ℕ ∣ 𝑥 ∈ 𝐴}, ℝ, < ) → ∪ 𝑘 ∈ (1..^𝑚)𝐵 = ∪ 𝑘 ∈ (1..^inf({𝑛 ∈ ℕ ∣ 𝑥 ∈ 𝐴}, ℝ, < ))𝐵) |
47 | 44, 46 | difeq12d 3691 |
. . . . . . . 8
⊢ (𝑚 = inf({𝑛 ∈ ℕ ∣ 𝑥 ∈ 𝐴}, ℝ, < ) →
(⦋𝑚 / 𝑛⦌𝐴 ∖ ∪
𝑘 ∈ (1..^𝑚)𝐵) = (⦋inf({𝑛 ∈ ℕ ∣ 𝑥 ∈ 𝐴}, ℝ, < ) / 𝑛⦌𝐴 ∖ ∪
𝑘 ∈ (1..^inf({𝑛 ∈ ℕ ∣ 𝑥 ∈ 𝐴}, ℝ, < ))𝐵)) |
48 | 47 | eleq2d 2673 |
. . . . . . 7
⊢ (𝑚 = inf({𝑛 ∈ ℕ ∣ 𝑥 ∈ 𝐴}, ℝ, < ) → (𝑥 ∈ (⦋𝑚 / 𝑛⦌𝐴 ∖ ∪
𝑘 ∈ (1..^𝑚)𝐵) ↔ 𝑥 ∈ (⦋inf({𝑛 ∈ ℕ ∣ 𝑥 ∈ 𝐴}, ℝ, < ) / 𝑛⦌𝐴 ∖ ∪
𝑘 ∈ (1..^inf({𝑛 ∈ ℕ ∣ 𝑥 ∈ 𝐴}, ℝ, < ))𝐵))) |
49 | 48 | rspcev 3282 |
. . . . . 6
⊢
((inf({𝑛 ∈
ℕ ∣ 𝑥 ∈
𝐴}, ℝ, < ) ∈
ℕ ∧ 𝑥 ∈
(⦋inf({𝑛
∈ ℕ ∣ 𝑥
∈ 𝐴}, ℝ, < )
/ 𝑛⦌𝐴 ∖ ∪ 𝑘 ∈ (1..^inf({𝑛 ∈ ℕ ∣ 𝑥 ∈ 𝐴}, ℝ, < ))𝐵)) → ∃𝑚 ∈ ℕ 𝑥 ∈ (⦋𝑚 / 𝑛⦌𝐴 ∖ ∪
𝑘 ∈ (1..^𝑚)𝐵)) |
50 | 19, 43, 49 | syl2anc 691 |
. . . . 5
⊢
(∃𝑛 ∈
ℕ 𝑥 ∈ 𝐴 → ∃𝑚 ∈ ℕ 𝑥 ∈ (⦋𝑚 / 𝑛⦌𝐴 ∖ ∪
𝑘 ∈ (1..^𝑚)𝐵)) |
51 | | nfv 1830 |
. . . . . 6
⊢
Ⅎ𝑚 𝑥 ∈ (𝐴 ∖ ∪
𝑘 ∈ (1..^𝑛)𝐵) |
52 | | nfcsb1v 3515 |
. . . . . . . 8
⊢
Ⅎ𝑛⦋𝑚 / 𝑛⦌𝐴 |
53 | | nfcv 2751 |
. . . . . . . 8
⊢
Ⅎ𝑛∪ 𝑘 ∈ (1..^𝑚)𝐵 |
54 | 52, 53 | nfdif 3693 |
. . . . . . 7
⊢
Ⅎ𝑛(⦋𝑚 / 𝑛⦌𝐴 ∖ ∪
𝑘 ∈ (1..^𝑚)𝐵) |
55 | 54 | nfcri 2745 |
. . . . . 6
⊢
Ⅎ𝑛 𝑥 ∈ (⦋𝑚 / 𝑛⦌𝐴 ∖ ∪
𝑘 ∈ (1..^𝑚)𝐵) |
56 | | csbeq1a 3508 |
. . . . . . . 8
⊢ (𝑛 = 𝑚 → 𝐴 = ⦋𝑚 / 𝑛⦌𝐴) |
57 | | oveq2 6557 |
. . . . . . . . 9
⊢ (𝑛 = 𝑚 → (1..^𝑛) = (1..^𝑚)) |
58 | 57 | iuneq1d 4481 |
. . . . . . . 8
⊢ (𝑛 = 𝑚 → ∪
𝑘 ∈ (1..^𝑛)𝐵 = ∪ 𝑘 ∈ (1..^𝑚)𝐵) |
59 | 56, 58 | difeq12d 3691 |
. . . . . . 7
⊢ (𝑛 = 𝑚 → (𝐴 ∖ ∪
𝑘 ∈ (1..^𝑛)𝐵) = (⦋𝑚 / 𝑛⦌𝐴 ∖ ∪
𝑘 ∈ (1..^𝑚)𝐵)) |
60 | 59 | eleq2d 2673 |
. . . . . 6
⊢ (𝑛 = 𝑚 → (𝑥 ∈ (𝐴 ∖ ∪
𝑘 ∈ (1..^𝑛)𝐵) ↔ 𝑥 ∈ (⦋𝑚 / 𝑛⦌𝐴 ∖ ∪
𝑘 ∈ (1..^𝑚)𝐵))) |
61 | 51, 55, 60 | cbvrex 3144 |
. . . . 5
⊢
(∃𝑛 ∈
ℕ 𝑥 ∈ (𝐴 ∖ ∪ 𝑘 ∈ (1..^𝑛)𝐵) ↔ ∃𝑚 ∈ ℕ 𝑥 ∈ (⦋𝑚 / 𝑛⦌𝐴 ∖ ∪
𝑘 ∈ (1..^𝑚)𝐵)) |
62 | 50, 61 | sylibr 223 |
. . . 4
⊢
(∃𝑛 ∈
ℕ 𝑥 ∈ 𝐴 → ∃𝑛 ∈ ℕ 𝑥 ∈ (𝐴 ∖ ∪
𝑘 ∈ (1..^𝑛)𝐵)) |
63 | | eldifi 3694 |
. . . . 5
⊢ (𝑥 ∈ (𝐴 ∖ ∪
𝑘 ∈ (1..^𝑛)𝐵) → 𝑥 ∈ 𝐴) |
64 | 63 | reximi 2994 |
. . . 4
⊢
(∃𝑛 ∈
ℕ 𝑥 ∈ (𝐴 ∖ ∪ 𝑘 ∈ (1..^𝑛)𝐵) → ∃𝑛 ∈ ℕ 𝑥 ∈ 𝐴) |
65 | 62, 64 | impbii 198 |
. . 3
⊢
(∃𝑛 ∈
ℕ 𝑥 ∈ 𝐴 ↔ ∃𝑛 ∈ ℕ 𝑥 ∈ (𝐴 ∖ ∪
𝑘 ∈ (1..^𝑛)𝐵)) |
66 | | eliun 4460 |
. . 3
⊢ (𝑥 ∈ ∪ 𝑛 ∈ ℕ 𝐴 ↔ ∃𝑛 ∈ ℕ 𝑥 ∈ 𝐴) |
67 | | eliun 4460 |
. . 3
⊢ (𝑥 ∈ ∪ 𝑛 ∈ ℕ (𝐴 ∖ ∪
𝑘 ∈ (1..^𝑛)𝐵) ↔ ∃𝑛 ∈ ℕ 𝑥 ∈ (𝐴 ∖ ∪
𝑘 ∈ (1..^𝑛)𝐵)) |
68 | 65, 66, 67 | 3bitr4i 291 |
. 2
⊢ (𝑥 ∈ ∪ 𝑛 ∈ ℕ 𝐴 ↔ 𝑥 ∈ ∪
𝑛 ∈ ℕ (𝐴 ∖ ∪ 𝑘 ∈ (1..^𝑛)𝐵)) |
69 | 68 | eqriv 2607 |
1
⊢ ∪ 𝑛 ∈ ℕ 𝐴 = ∪ 𝑛 ∈ ℕ (𝐴 ∖ ∪ 𝑘 ∈ (1..^𝑛)𝐵) |