| Step | Hyp | Ref
| Expression |
| 1 | | ssrab2 4080 |
. . . . . . . . . 10
⊢ {𝑛 ∈ ℕ ∣ 𝑥 ∈ 𝐴} ⊆ ℕ |
| 2 | | nnuz 12921 |
. . . . . . . . . 10
⊢ ℕ =
(ℤ≥‘1) |
| 3 | 1, 2 | sseqtri 4032 |
. . . . . . . . 9
⊢ {𝑛 ∈ ℕ ∣ 𝑥 ∈ 𝐴} ⊆
(ℤ≥‘1) |
| 4 | | rabn0 4389 |
. . . . . . . . . 10
⊢ ({𝑛 ∈ ℕ ∣ 𝑥 ∈ 𝐴} ≠ ∅ ↔ ∃𝑛 ∈ ℕ 𝑥 ∈ 𝐴) |
| 5 | 4 | biimpri 228 |
. . . . . . . . 9
⊢
(∃𝑛 ∈
ℕ 𝑥 ∈ 𝐴 → {𝑛 ∈ ℕ ∣ 𝑥 ∈ 𝐴} ≠ ∅) |
| 6 | | infssuzcl 12974 |
. . . . . . . . 9
⊢ (({𝑛 ∈ ℕ ∣ 𝑥 ∈ 𝐴} ⊆ (ℤ≥‘1)
∧ {𝑛 ∈ ℕ
∣ 𝑥 ∈ 𝐴} ≠ ∅) →
inf({𝑛 ∈ ℕ
∣ 𝑥 ∈ 𝐴}, ℝ, < ) ∈ {𝑛 ∈ ℕ ∣ 𝑥 ∈ 𝐴}) |
| 7 | 3, 5, 6 | sylancr 587 |
. . . . . . . 8
⊢
(∃𝑛 ∈
ℕ 𝑥 ∈ 𝐴 → inf({𝑛 ∈ ℕ ∣ 𝑥 ∈ 𝐴}, ℝ, < ) ∈ {𝑛 ∈ ℕ ∣ 𝑥 ∈ 𝐴}) |
| 8 | | nfrab1 3457 |
. . . . . . . . . 10
⊢
Ⅎ𝑛{𝑛 ∈ ℕ ∣ 𝑥 ∈ 𝐴} |
| 9 | | nfcv 2905 |
. . . . . . . . . 10
⊢
Ⅎ𝑛ℝ |
| 10 | | nfcv 2905 |
. . . . . . . . . 10
⊢
Ⅎ𝑛
< |
| 11 | 8, 9, 10 | nfinf 9522 |
. . . . . . . . 9
⊢
Ⅎ𝑛inf({𝑛 ∈ ℕ ∣ 𝑥 ∈ 𝐴}, ℝ, < ) |
| 12 | | nfcv 2905 |
. . . . . . . . 9
⊢
Ⅎ𝑛ℕ |
| 13 | 11 | nfcsb1 3922 |
. . . . . . . . . 10
⊢
Ⅎ𝑛⦋inf({𝑛 ∈ ℕ ∣ 𝑥 ∈ 𝐴}, ℝ, < ) / 𝑛⦌𝐴 |
| 14 | 13 | nfcri 2897 |
. . . . . . . . 9
⊢
Ⅎ𝑛 𝑥 ∈
⦋inf({𝑛
∈ ℕ ∣ 𝑥
∈ 𝐴}, ℝ, < )
/ 𝑛⦌𝐴 |
| 15 | | csbeq1a 3913 |
. . . . . . . . . 10
⊢ (𝑛 = inf({𝑛 ∈ ℕ ∣ 𝑥 ∈ 𝐴}, ℝ, < ) → 𝐴 = ⦋inf({𝑛 ∈ ℕ ∣ 𝑥 ∈ 𝐴}, ℝ, < ) / 𝑛⦌𝐴) |
| 16 | 15 | eleq2d 2827 |
. . . . . . . . 9
⊢ (𝑛 = inf({𝑛 ∈ ℕ ∣ 𝑥 ∈ 𝐴}, ℝ, < ) → (𝑥 ∈ 𝐴 ↔ 𝑥 ∈ ⦋inf({𝑛 ∈ ℕ ∣ 𝑥 ∈ 𝐴}, ℝ, < ) / 𝑛⦌𝐴)) |
| 17 | 11, 12, 14, 16 | elrabf 3688 |
. . . . . . . 8
⊢
(inf({𝑛 ∈
ℕ ∣ 𝑥 ∈
𝐴}, ℝ, < ) ∈
{𝑛 ∈ ℕ ∣
𝑥 ∈ 𝐴} ↔ (inf({𝑛 ∈ ℕ ∣ 𝑥 ∈ 𝐴}, ℝ, < ) ∈ ℕ ∧
𝑥 ∈
⦋inf({𝑛
∈ ℕ ∣ 𝑥
∈ 𝐴}, ℝ, < )
/ 𝑛⦌𝐴)) |
| 18 | 7, 17 | sylib 218 |
. . . . . . 7
⊢
(∃𝑛 ∈
ℕ 𝑥 ∈ 𝐴 → (inf({𝑛 ∈ ℕ ∣ 𝑥 ∈ 𝐴}, ℝ, < ) ∈ ℕ ∧
𝑥 ∈
⦋inf({𝑛
∈ ℕ ∣ 𝑥
∈ 𝐴}, ℝ, < )
/ 𝑛⦌𝐴)) |
| 19 | 18 | simpld 494 |
. . . . . 6
⊢
(∃𝑛 ∈
ℕ 𝑥 ∈ 𝐴 → inf({𝑛 ∈ ℕ ∣ 𝑥 ∈ 𝐴}, ℝ, < ) ∈
ℕ) |
| 20 | 18 | simprd 495 |
. . . . . . 7
⊢
(∃𝑛 ∈
ℕ 𝑥 ∈ 𝐴 → 𝑥 ∈ ⦋inf({𝑛 ∈ ℕ ∣ 𝑥 ∈ 𝐴}, ℝ, < ) / 𝑛⦌𝐴) |
| 21 | 19 | nnred 12281 |
. . . . . . . . 9
⊢
(∃𝑛 ∈
ℕ 𝑥 ∈ 𝐴 → inf({𝑛 ∈ ℕ ∣ 𝑥 ∈ 𝐴}, ℝ, < ) ∈
ℝ) |
| 22 | 21 | ltnrd 11395 |
. . . . . . . 8
⊢
(∃𝑛 ∈
ℕ 𝑥 ∈ 𝐴 → ¬ inf({𝑛 ∈ ℕ ∣ 𝑥 ∈ 𝐴}, ℝ, < ) < inf({𝑛 ∈ ℕ ∣ 𝑥 ∈ 𝐴}, ℝ, < )) |
| 23 | | eliun 4995 |
. . . . . . . . 9
⊢ (𝑥 ∈ ∪ 𝑘 ∈ (1..^inf({𝑛 ∈ ℕ ∣ 𝑥 ∈ 𝐴}, ℝ, < ))𝐵 ↔ ∃𝑘 ∈ (1..^inf({𝑛 ∈ ℕ ∣ 𝑥 ∈ 𝐴}, ℝ, < ))𝑥 ∈ 𝐵) |
| 24 | 21 | ad2antrr 726 |
. . . . . . . . . . 11
⊢
(((∃𝑛 ∈
ℕ 𝑥 ∈ 𝐴 ∧ 𝑘 ∈ (1..^inf({𝑛 ∈ ℕ ∣ 𝑥 ∈ 𝐴}, ℝ, < ))) ∧ 𝑥 ∈ 𝐵) → inf({𝑛 ∈ ℕ ∣ 𝑥 ∈ 𝐴}, ℝ, < ) ∈
ℝ) |
| 25 | | elfzouz 13703 |
. . . . . . . . . . . . . 14
⊢ (𝑘 ∈ (1..^inf({𝑛 ∈ ℕ ∣ 𝑥 ∈ 𝐴}, ℝ, < )) → 𝑘 ∈
(ℤ≥‘1)) |
| 26 | 25, 2 | eleqtrrdi 2852 |
. . . . . . . . . . . . 13
⊢ (𝑘 ∈ (1..^inf({𝑛 ∈ ℕ ∣ 𝑥 ∈ 𝐴}, ℝ, < )) → 𝑘 ∈
ℕ) |
| 27 | 26 | ad2antlr 727 |
. . . . . . . . . . . 12
⊢
(((∃𝑛 ∈
ℕ 𝑥 ∈ 𝐴 ∧ 𝑘 ∈ (1..^inf({𝑛 ∈ ℕ ∣ 𝑥 ∈ 𝐴}, ℝ, < ))) ∧ 𝑥 ∈ 𝐵) → 𝑘 ∈ ℕ) |
| 28 | 27 | nnred 12281 |
. . . . . . . . . . 11
⊢
(((∃𝑛 ∈
ℕ 𝑥 ∈ 𝐴 ∧ 𝑘 ∈ (1..^inf({𝑛 ∈ ℕ ∣ 𝑥 ∈ 𝐴}, ℝ, < ))) ∧ 𝑥 ∈ 𝐵) → 𝑘 ∈ ℝ) |
| 29 | | iundisj.1 |
. . . . . . . . . . . . . 14
⊢ (𝑛 = 𝑘 → 𝐴 = 𝐵) |
| 30 | 29 | eleq2d 2827 |
. . . . . . . . . . . . 13
⊢ (𝑛 = 𝑘 → (𝑥 ∈ 𝐴 ↔ 𝑥 ∈ 𝐵)) |
| 31 | | simpr 484 |
. . . . . . . . . . . . 13
⊢
(((∃𝑛 ∈
ℕ 𝑥 ∈ 𝐴 ∧ 𝑘 ∈ (1..^inf({𝑛 ∈ ℕ ∣ 𝑥 ∈ 𝐴}, ℝ, < ))) ∧ 𝑥 ∈ 𝐵) → 𝑥 ∈ 𝐵) |
| 32 | 30, 27, 31 | elrabd 3694 |
. . . . . . . . . . . 12
⊢
(((∃𝑛 ∈
ℕ 𝑥 ∈ 𝐴 ∧ 𝑘 ∈ (1..^inf({𝑛 ∈ ℕ ∣ 𝑥 ∈ 𝐴}, ℝ, < ))) ∧ 𝑥 ∈ 𝐵) → 𝑘 ∈ {𝑛 ∈ ℕ ∣ 𝑥 ∈ 𝐴}) |
| 33 | | infssuzle 12973 |
. . . . . . . . . . . 12
⊢ (({𝑛 ∈ ℕ ∣ 𝑥 ∈ 𝐴} ⊆ (ℤ≥‘1)
∧ 𝑘 ∈ {𝑛 ∈ ℕ ∣ 𝑥 ∈ 𝐴}) → inf({𝑛 ∈ ℕ ∣ 𝑥 ∈ 𝐴}, ℝ, < ) ≤ 𝑘) |
| 34 | 3, 32, 33 | sylancr 587 |
. . . . . . . . . . 11
⊢
(((∃𝑛 ∈
ℕ 𝑥 ∈ 𝐴 ∧ 𝑘 ∈ (1..^inf({𝑛 ∈ ℕ ∣ 𝑥 ∈ 𝐴}, ℝ, < ))) ∧ 𝑥 ∈ 𝐵) → inf({𝑛 ∈ ℕ ∣ 𝑥 ∈ 𝐴}, ℝ, < ) ≤ 𝑘) |
| 35 | | elfzolt2 13708 |
. . . . . . . . . . . 12
⊢ (𝑘 ∈ (1..^inf({𝑛 ∈ ℕ ∣ 𝑥 ∈ 𝐴}, ℝ, < )) → 𝑘 < inf({𝑛 ∈ ℕ ∣ 𝑥 ∈ 𝐴}, ℝ, < )) |
| 36 | 35 | ad2antlr 727 |
. . . . . . . . . . 11
⊢
(((∃𝑛 ∈
ℕ 𝑥 ∈ 𝐴 ∧ 𝑘 ∈ (1..^inf({𝑛 ∈ ℕ ∣ 𝑥 ∈ 𝐴}, ℝ, < ))) ∧ 𝑥 ∈ 𝐵) → 𝑘 < inf({𝑛 ∈ ℕ ∣ 𝑥 ∈ 𝐴}, ℝ, < )) |
| 37 | 24, 28, 24, 34, 36 | lelttrd 11419 |
. . . . . . . . . 10
⊢
(((∃𝑛 ∈
ℕ 𝑥 ∈ 𝐴 ∧ 𝑘 ∈ (1..^inf({𝑛 ∈ ℕ ∣ 𝑥 ∈ 𝐴}, ℝ, < ))) ∧ 𝑥 ∈ 𝐵) → inf({𝑛 ∈ ℕ ∣ 𝑥 ∈ 𝐴}, ℝ, < ) < inf({𝑛 ∈ ℕ ∣ 𝑥 ∈ 𝐴}, ℝ, < )) |
| 38 | 37 | rexlimdva2 3157 |
. . . . . . . . 9
⊢
(∃𝑛 ∈
ℕ 𝑥 ∈ 𝐴 → (∃𝑘 ∈ (1..^inf({𝑛 ∈ ℕ ∣ 𝑥 ∈ 𝐴}, ℝ, < ))𝑥 ∈ 𝐵 → inf({𝑛 ∈ ℕ ∣ 𝑥 ∈ 𝐴}, ℝ, < ) < inf({𝑛 ∈ ℕ ∣ 𝑥 ∈ 𝐴}, ℝ, < ))) |
| 39 | 23, 38 | biimtrid 242 |
. . . . . . . 8
⊢
(∃𝑛 ∈
ℕ 𝑥 ∈ 𝐴 → (𝑥 ∈ ∪
𝑘 ∈ (1..^inf({𝑛 ∈ ℕ ∣ 𝑥 ∈ 𝐴}, ℝ, < ))𝐵 → inf({𝑛 ∈ ℕ ∣ 𝑥 ∈ 𝐴}, ℝ, < ) < inf({𝑛 ∈ ℕ ∣ 𝑥 ∈ 𝐴}, ℝ, < ))) |
| 40 | 22, 39 | mtod 198 |
. . . . . . 7
⊢
(∃𝑛 ∈
ℕ 𝑥 ∈ 𝐴 → ¬ 𝑥 ∈ ∪
𝑘 ∈ (1..^inf({𝑛 ∈ ℕ ∣ 𝑥 ∈ 𝐴}, ℝ, < ))𝐵) |
| 41 | 20, 40 | eldifd 3962 |
. . . . . 6
⊢
(∃𝑛 ∈
ℕ 𝑥 ∈ 𝐴 → 𝑥 ∈ (⦋inf({𝑛 ∈ ℕ ∣ 𝑥 ∈ 𝐴}, ℝ, < ) / 𝑛⦌𝐴 ∖ ∪
𝑘 ∈ (1..^inf({𝑛 ∈ ℕ ∣ 𝑥 ∈ 𝐴}, ℝ, < ))𝐵)) |
| 42 | | csbeq1 3902 |
. . . . . . . . 9
⊢ (𝑚 = inf({𝑛 ∈ ℕ ∣ 𝑥 ∈ 𝐴}, ℝ, < ) →
⦋𝑚 / 𝑛⦌𝐴 = ⦋inf({𝑛 ∈ ℕ ∣ 𝑥 ∈ 𝐴}, ℝ, < ) / 𝑛⦌𝐴) |
| 43 | | oveq2 7439 |
. . . . . . . . . 10
⊢ (𝑚 = inf({𝑛 ∈ ℕ ∣ 𝑥 ∈ 𝐴}, ℝ, < ) → (1..^𝑚) = (1..^inf({𝑛 ∈ ℕ ∣ 𝑥 ∈ 𝐴}, ℝ, < ))) |
| 44 | 43 | iuneq1d 5019 |
. . . . . . . . 9
⊢ (𝑚 = inf({𝑛 ∈ ℕ ∣ 𝑥 ∈ 𝐴}, ℝ, < ) → ∪ 𝑘 ∈ (1..^𝑚)𝐵 = ∪ 𝑘 ∈ (1..^inf({𝑛 ∈ ℕ ∣ 𝑥 ∈ 𝐴}, ℝ, < ))𝐵) |
| 45 | 42, 44 | difeq12d 4127 |
. . . . . . . 8
⊢ (𝑚 = inf({𝑛 ∈ ℕ ∣ 𝑥 ∈ 𝐴}, ℝ, < ) →
(⦋𝑚 / 𝑛⦌𝐴 ∖ ∪
𝑘 ∈ (1..^𝑚)𝐵) = (⦋inf({𝑛 ∈ ℕ ∣ 𝑥 ∈ 𝐴}, ℝ, < ) / 𝑛⦌𝐴 ∖ ∪
𝑘 ∈ (1..^inf({𝑛 ∈ ℕ ∣ 𝑥 ∈ 𝐴}, ℝ, < ))𝐵)) |
| 46 | 45 | eleq2d 2827 |
. . . . . . 7
⊢ (𝑚 = inf({𝑛 ∈ ℕ ∣ 𝑥 ∈ 𝐴}, ℝ, < ) → (𝑥 ∈ (⦋𝑚 / 𝑛⦌𝐴 ∖ ∪
𝑘 ∈ (1..^𝑚)𝐵) ↔ 𝑥 ∈ (⦋inf({𝑛 ∈ ℕ ∣ 𝑥 ∈ 𝐴}, ℝ, < ) / 𝑛⦌𝐴 ∖ ∪
𝑘 ∈ (1..^inf({𝑛 ∈ ℕ ∣ 𝑥 ∈ 𝐴}, ℝ, < ))𝐵))) |
| 47 | 46 | rspcev 3622 |
. . . . . 6
⊢
((inf({𝑛 ∈
ℕ ∣ 𝑥 ∈
𝐴}, ℝ, < ) ∈
ℕ ∧ 𝑥 ∈
(⦋inf({𝑛
∈ ℕ ∣ 𝑥
∈ 𝐴}, ℝ, < )
/ 𝑛⦌𝐴 ∖ ∪ 𝑘 ∈ (1..^inf({𝑛 ∈ ℕ ∣ 𝑥 ∈ 𝐴}, ℝ, < ))𝐵)) → ∃𝑚 ∈ ℕ 𝑥 ∈ (⦋𝑚 / 𝑛⦌𝐴 ∖ ∪
𝑘 ∈ (1..^𝑚)𝐵)) |
| 48 | 19, 41, 47 | syl2anc 584 |
. . . . 5
⊢
(∃𝑛 ∈
ℕ 𝑥 ∈ 𝐴 → ∃𝑚 ∈ ℕ 𝑥 ∈ (⦋𝑚 / 𝑛⦌𝐴 ∖ ∪
𝑘 ∈ (1..^𝑚)𝐵)) |
| 49 | | nfv 1914 |
. . . . . 6
⊢
Ⅎ𝑚 𝑥 ∈ (𝐴 ∖ ∪
𝑘 ∈ (1..^𝑛)𝐵) |
| 50 | | nfcsb1v 3923 |
. . . . . . . 8
⊢
Ⅎ𝑛⦋𝑚 / 𝑛⦌𝐴 |
| 51 | | nfcv 2905 |
. . . . . . . 8
⊢
Ⅎ𝑛∪ 𝑘 ∈ (1..^𝑚)𝐵 |
| 52 | 50, 51 | nfdif 4129 |
. . . . . . 7
⊢
Ⅎ𝑛(⦋𝑚 / 𝑛⦌𝐴 ∖ ∪
𝑘 ∈ (1..^𝑚)𝐵) |
| 53 | 52 | nfcri 2897 |
. . . . . 6
⊢
Ⅎ𝑛 𝑥 ∈ (⦋𝑚 / 𝑛⦌𝐴 ∖ ∪
𝑘 ∈ (1..^𝑚)𝐵) |
| 54 | | csbeq1a 3913 |
. . . . . . . 8
⊢ (𝑛 = 𝑚 → 𝐴 = ⦋𝑚 / 𝑛⦌𝐴) |
| 55 | | oveq2 7439 |
. . . . . . . . 9
⊢ (𝑛 = 𝑚 → (1..^𝑛) = (1..^𝑚)) |
| 56 | 55 | iuneq1d 5019 |
. . . . . . . 8
⊢ (𝑛 = 𝑚 → ∪
𝑘 ∈ (1..^𝑛)𝐵 = ∪ 𝑘 ∈ (1..^𝑚)𝐵) |
| 57 | 54, 56 | difeq12d 4127 |
. . . . . . 7
⊢ (𝑛 = 𝑚 → (𝐴 ∖ ∪
𝑘 ∈ (1..^𝑛)𝐵) = (⦋𝑚 / 𝑛⦌𝐴 ∖ ∪
𝑘 ∈ (1..^𝑚)𝐵)) |
| 58 | 57 | eleq2d 2827 |
. . . . . 6
⊢ (𝑛 = 𝑚 → (𝑥 ∈ (𝐴 ∖ ∪
𝑘 ∈ (1..^𝑛)𝐵) ↔ 𝑥 ∈ (⦋𝑚 / 𝑛⦌𝐴 ∖ ∪
𝑘 ∈ (1..^𝑚)𝐵))) |
| 59 | 49, 53, 58 | cbvrexw 3307 |
. . . . 5
⊢
(∃𝑛 ∈
ℕ 𝑥 ∈ (𝐴 ∖ ∪ 𝑘 ∈ (1..^𝑛)𝐵) ↔ ∃𝑚 ∈ ℕ 𝑥 ∈ (⦋𝑚 / 𝑛⦌𝐴 ∖ ∪
𝑘 ∈ (1..^𝑚)𝐵)) |
| 60 | 48, 59 | sylibr 234 |
. . . 4
⊢
(∃𝑛 ∈
ℕ 𝑥 ∈ 𝐴 → ∃𝑛 ∈ ℕ 𝑥 ∈ (𝐴 ∖ ∪
𝑘 ∈ (1..^𝑛)𝐵)) |
| 61 | | eldifi 4131 |
. . . . 5
⊢ (𝑥 ∈ (𝐴 ∖ ∪
𝑘 ∈ (1..^𝑛)𝐵) → 𝑥 ∈ 𝐴) |
| 62 | 61 | reximi 3084 |
. . . 4
⊢
(∃𝑛 ∈
ℕ 𝑥 ∈ (𝐴 ∖ ∪ 𝑘 ∈ (1..^𝑛)𝐵) → ∃𝑛 ∈ ℕ 𝑥 ∈ 𝐴) |
| 63 | 60, 62 | impbii 209 |
. . 3
⊢
(∃𝑛 ∈
ℕ 𝑥 ∈ 𝐴 ↔ ∃𝑛 ∈ ℕ 𝑥 ∈ (𝐴 ∖ ∪
𝑘 ∈ (1..^𝑛)𝐵)) |
| 64 | | eliun 4995 |
. . 3
⊢ (𝑥 ∈ ∪ 𝑛 ∈ ℕ 𝐴 ↔ ∃𝑛 ∈ ℕ 𝑥 ∈ 𝐴) |
| 65 | | eliun 4995 |
. . 3
⊢ (𝑥 ∈ ∪ 𝑛 ∈ ℕ (𝐴 ∖ ∪
𝑘 ∈ (1..^𝑛)𝐵) ↔ ∃𝑛 ∈ ℕ 𝑥 ∈ (𝐴 ∖ ∪
𝑘 ∈ (1..^𝑛)𝐵)) |
| 66 | 63, 64, 65 | 3bitr4i 303 |
. 2
⊢ (𝑥 ∈ ∪ 𝑛 ∈ ℕ 𝐴 ↔ 𝑥 ∈ ∪
𝑛 ∈ ℕ (𝐴 ∖ ∪ 𝑘 ∈ (1..^𝑛)𝐵)) |
| 67 | 66 | eqriv 2734 |
1
⊢ ∪ 𝑛 ∈ ℕ 𝐴 = ∪ 𝑛 ∈ ℕ (𝐴 ∖ ∪ 𝑘 ∈ (1..^𝑛)𝐵) |