Proof of Theorem allbutfi
Step | Hyp | Ref
| Expression |
1 | | allbutfi.a |
. . . . . 6
⊢ 𝐴 = ∪ 𝑛 ∈ 𝑍 ∩ 𝑚 ∈
(ℤ≥‘𝑛)𝐵 |
2 | 1 | eleq2i 2680 |
. . . . 5
⊢ (𝑋 ∈ 𝐴 ↔ 𝑋 ∈ ∪
𝑛 ∈ 𝑍 ∩ 𝑚 ∈
(ℤ≥‘𝑛)𝐵) |
3 | 2 | biimpi 205 |
. . . 4
⊢ (𝑋 ∈ 𝐴 → 𝑋 ∈ ∪
𝑛 ∈ 𝑍 ∩ 𝑚 ∈
(ℤ≥‘𝑛)𝐵) |
4 | | eliun 4460 |
. . . 4
⊢ (𝑋 ∈ ∪ 𝑛 ∈ 𝑍 ∩ 𝑚 ∈
(ℤ≥‘𝑛)𝐵 ↔ ∃𝑛 ∈ 𝑍 𝑋 ∈ ∩
𝑚 ∈
(ℤ≥‘𝑛)𝐵) |
5 | 3, 4 | sylib 207 |
. . 3
⊢ (𝑋 ∈ 𝐴 → ∃𝑛 ∈ 𝑍 𝑋 ∈ ∩
𝑚 ∈
(ℤ≥‘𝑛)𝐵) |
6 | | nfcv 2751 |
. . . . 5
⊢
Ⅎ𝑛𝑋 |
7 | | nfiu1 4486 |
. . . . . 6
⊢
Ⅎ𝑛∪ 𝑛 ∈ 𝑍 ∩ 𝑚 ∈
(ℤ≥‘𝑛)𝐵 |
8 | 1, 7 | nfcxfr 2749 |
. . . . 5
⊢
Ⅎ𝑛𝐴 |
9 | 6, 8 | nfel 2763 |
. . . 4
⊢
Ⅎ𝑛 𝑋 ∈ 𝐴 |
10 | | eliin 4461 |
. . . . . 6
⊢ (𝑋 ∈ 𝐴 → (𝑋 ∈ ∩
𝑚 ∈
(ℤ≥‘𝑛)𝐵 ↔ ∀𝑚 ∈ (ℤ≥‘𝑛)𝑋 ∈ 𝐵)) |
11 | 10 | biimpd 218 |
. . . . 5
⊢ (𝑋 ∈ 𝐴 → (𝑋 ∈ ∩
𝑚 ∈
(ℤ≥‘𝑛)𝐵 → ∀𝑚 ∈ (ℤ≥‘𝑛)𝑋 ∈ 𝐵)) |
12 | 11 | a1d 25 |
. . . 4
⊢ (𝑋 ∈ 𝐴 → (𝑛 ∈ 𝑍 → (𝑋 ∈ ∩
𝑚 ∈
(ℤ≥‘𝑛)𝐵 → ∀𝑚 ∈ (ℤ≥‘𝑛)𝑋 ∈ 𝐵))) |
13 | 9, 12 | reximdai 2995 |
. . 3
⊢ (𝑋 ∈ 𝐴 → (∃𝑛 ∈ 𝑍 𝑋 ∈ ∩
𝑚 ∈
(ℤ≥‘𝑛)𝐵 → ∃𝑛 ∈ 𝑍 ∀𝑚 ∈ (ℤ≥‘𝑛)𝑋 ∈ 𝐵)) |
14 | 5, 13 | mpd 15 |
. 2
⊢ (𝑋 ∈ 𝐴 → ∃𝑛 ∈ 𝑍 ∀𝑚 ∈ (ℤ≥‘𝑛)𝑋 ∈ 𝐵) |
15 | | simpr 476 |
. . . . . . 7
⊢ ((𝑛 ∈ 𝑍 ∧ ∀𝑚 ∈ (ℤ≥‘𝑛)𝑋 ∈ 𝐵) → ∀𝑚 ∈ (ℤ≥‘𝑛)𝑋 ∈ 𝐵) |
16 | | allbutfi.z |
. . . . . . . . . . . . 13
⊢ 𝑍 =
(ℤ≥‘𝑀) |
17 | 16 | eleq2i 2680 |
. . . . . . . . . . . 12
⊢ (𝑛 ∈ 𝑍 ↔ 𝑛 ∈ (ℤ≥‘𝑀)) |
18 | 17 | biimpi 205 |
. . . . . . . . . . 11
⊢ (𝑛 ∈ 𝑍 → 𝑛 ∈ (ℤ≥‘𝑀)) |
19 | | eluzelz 11573 |
. . . . . . . . . . 11
⊢ (𝑛 ∈
(ℤ≥‘𝑀) → 𝑛 ∈ ℤ) |
20 | | uzid 11578 |
. . . . . . . . . . 11
⊢ (𝑛 ∈ ℤ → 𝑛 ∈
(ℤ≥‘𝑛)) |
21 | 18, 19, 20 | 3syl 18 |
. . . . . . . . . 10
⊢ (𝑛 ∈ 𝑍 → 𝑛 ∈ (ℤ≥‘𝑛)) |
22 | | ne0i 3880 |
. . . . . . . . . 10
⊢ (𝑛 ∈
(ℤ≥‘𝑛) → (ℤ≥‘𝑛) ≠ ∅) |
23 | 21, 22 | syl 17 |
. . . . . . . . 9
⊢ (𝑛 ∈ 𝑍 → (ℤ≥‘𝑛) ≠ ∅) |
24 | | eliin2 38330 |
. . . . . . . . 9
⊢
((ℤ≥‘𝑛) ≠ ∅ → (𝑋 ∈ ∩
𝑚 ∈
(ℤ≥‘𝑛)𝐵 ↔ ∀𝑚 ∈ (ℤ≥‘𝑛)𝑋 ∈ 𝐵)) |
25 | 23, 24 | syl 17 |
. . . . . . . 8
⊢ (𝑛 ∈ 𝑍 → (𝑋 ∈ ∩
𝑚 ∈
(ℤ≥‘𝑛)𝐵 ↔ ∀𝑚 ∈ (ℤ≥‘𝑛)𝑋 ∈ 𝐵)) |
26 | 25 | adantr 480 |
. . . . . . 7
⊢ ((𝑛 ∈ 𝑍 ∧ ∀𝑚 ∈ (ℤ≥‘𝑛)𝑋 ∈ 𝐵) → (𝑋 ∈ ∩
𝑚 ∈
(ℤ≥‘𝑛)𝐵 ↔ ∀𝑚 ∈ (ℤ≥‘𝑛)𝑋 ∈ 𝐵)) |
27 | 15, 26 | mpbird 246 |
. . . . . 6
⊢ ((𝑛 ∈ 𝑍 ∧ ∀𝑚 ∈ (ℤ≥‘𝑛)𝑋 ∈ 𝐵) → 𝑋 ∈ ∩
𝑚 ∈
(ℤ≥‘𝑛)𝐵) |
28 | 27 | ex 449 |
. . . . 5
⊢ (𝑛 ∈ 𝑍 → (∀𝑚 ∈ (ℤ≥‘𝑛)𝑋 ∈ 𝐵 → 𝑋 ∈ ∩
𝑚 ∈
(ℤ≥‘𝑛)𝐵)) |
29 | 28 | reximia 2992 |
. . . 4
⊢
(∃𝑛 ∈
𝑍 ∀𝑚 ∈
(ℤ≥‘𝑛)𝑋 ∈ 𝐵 → ∃𝑛 ∈ 𝑍 𝑋 ∈ ∩
𝑚 ∈
(ℤ≥‘𝑛)𝐵) |
30 | 29, 4 | sylibr 223 |
. . 3
⊢
(∃𝑛 ∈
𝑍 ∀𝑚 ∈
(ℤ≥‘𝑛)𝑋 ∈ 𝐵 → 𝑋 ∈ ∪
𝑛 ∈ 𝑍 ∩ 𝑚 ∈
(ℤ≥‘𝑛)𝐵) |
31 | 30, 1 | syl6eleqr 2699 |
. 2
⊢
(∃𝑛 ∈
𝑍 ∀𝑚 ∈
(ℤ≥‘𝑛)𝑋 ∈ 𝐵 → 𝑋 ∈ 𝐴) |
32 | 14, 31 | impbii 198 |
1
⊢ (𝑋 ∈ 𝐴 ↔ ∃𝑛 ∈ 𝑍 ∀𝑚 ∈ (ℤ≥‘𝑛)𝑋 ∈ 𝐵) |