Proof of Theorem allbutfiinf
Step | Hyp | Ref
| Expression |
1 | | ssrab2 3687 |
. . 3
⊢ {𝑛 ∈ 𝑍 ∣ ∀𝑚 ∈ (ℤ≥‘𝑛)𝑋 ∈ 𝐵} ⊆ 𝑍 |
2 | | allbutfiinf.n |
. . . . 5
⊢ 𝑁 = inf({𝑛 ∈ 𝑍 ∣ ∀𝑚 ∈ (ℤ≥‘𝑛)𝑋 ∈ 𝐵}, ℝ, < ) |
3 | 2 | a1i 11 |
. . . 4
⊢ (𝜑 → 𝑁 = inf({𝑛 ∈ 𝑍 ∣ ∀𝑚 ∈ (ℤ≥‘𝑛)𝑋 ∈ 𝐵}, ℝ, < )) |
4 | | allbutfiinf.z |
. . . . . . 7
⊢ 𝑍 =
(ℤ≥‘𝑀) |
5 | 1, 4 | sseqtri 3637 |
. . . . . 6
⊢ {𝑛 ∈ 𝑍 ∣ ∀𝑚 ∈ (ℤ≥‘𝑛)𝑋 ∈ 𝐵} ⊆
(ℤ≥‘𝑀) |
6 | 5 | a1i 11 |
. . . . 5
⊢ (𝜑 → {𝑛 ∈ 𝑍 ∣ ∀𝑚 ∈ (ℤ≥‘𝑛)𝑋 ∈ 𝐵} ⊆
(ℤ≥‘𝑀)) |
7 | | allbutfiinf.x |
. . . . . . 7
⊢ (𝜑 → 𝑋 ∈ 𝐴) |
8 | | allbutfiinf.a |
. . . . . . . 8
⊢ 𝐴 = ∪ 𝑛 ∈ 𝑍 ∩ 𝑚 ∈
(ℤ≥‘𝑛)𝐵 |
9 | 4, 8 | allbutfi 39616 |
. . . . . . 7
⊢ (𝑋 ∈ 𝐴 ↔ ∃𝑛 ∈ 𝑍 ∀𝑚 ∈ (ℤ≥‘𝑛)𝑋 ∈ 𝐵) |
10 | 7, 9 | sylib 208 |
. . . . . 6
⊢ (𝜑 → ∃𝑛 ∈ 𝑍 ∀𝑚 ∈ (ℤ≥‘𝑛)𝑋 ∈ 𝐵) |
11 | | nfrab1 3122 |
. . . . . . . . 9
⊢
Ⅎ𝑛{𝑛 ∈ 𝑍 ∣ ∀𝑚 ∈ (ℤ≥‘𝑛)𝑋 ∈ 𝐵} |
12 | | nfcv 2764 |
. . . . . . . . 9
⊢
Ⅎ𝑛∅ |
13 | 11, 12 | nfne 2894 |
. . . . . . . 8
⊢
Ⅎ𝑛{𝑛 ∈ 𝑍 ∣ ∀𝑚 ∈ (ℤ≥‘𝑛)𝑋 ∈ 𝐵} ≠ ∅ |
14 | | rabid 3116 |
. . . . . . . . . . . 12
⊢ (𝑛 ∈ {𝑛 ∈ 𝑍 ∣ ∀𝑚 ∈ (ℤ≥‘𝑛)𝑋 ∈ 𝐵} ↔ (𝑛 ∈ 𝑍 ∧ ∀𝑚 ∈ (ℤ≥‘𝑛)𝑋 ∈ 𝐵)) |
15 | 14 | bicomi 214 |
. . . . . . . . . . 11
⊢ ((𝑛 ∈ 𝑍 ∧ ∀𝑚 ∈ (ℤ≥‘𝑛)𝑋 ∈ 𝐵) ↔ 𝑛 ∈ {𝑛 ∈ 𝑍 ∣ ∀𝑚 ∈ (ℤ≥‘𝑛)𝑋 ∈ 𝐵}) |
16 | 15 | biimpi 206 |
. . . . . . . . . 10
⊢ ((𝑛 ∈ 𝑍 ∧ ∀𝑚 ∈ (ℤ≥‘𝑛)𝑋 ∈ 𝐵) → 𝑛 ∈ {𝑛 ∈ 𝑍 ∣ ∀𝑚 ∈ (ℤ≥‘𝑛)𝑋 ∈ 𝐵}) |
17 | | ne0i 3921 |
. . . . . . . . . 10
⊢ (𝑛 ∈ {𝑛 ∈ 𝑍 ∣ ∀𝑚 ∈ (ℤ≥‘𝑛)𝑋 ∈ 𝐵} → {𝑛 ∈ 𝑍 ∣ ∀𝑚 ∈ (ℤ≥‘𝑛)𝑋 ∈ 𝐵} ≠ ∅) |
18 | 16, 17 | syl 17 |
. . . . . . . . 9
⊢ ((𝑛 ∈ 𝑍 ∧ ∀𝑚 ∈ (ℤ≥‘𝑛)𝑋 ∈ 𝐵) → {𝑛 ∈ 𝑍 ∣ ∀𝑚 ∈ (ℤ≥‘𝑛)𝑋 ∈ 𝐵} ≠ ∅) |
19 | 18 | ex 450 |
. . . . . . . 8
⊢ (𝑛 ∈ 𝑍 → (∀𝑚 ∈ (ℤ≥‘𝑛)𝑋 ∈ 𝐵 → {𝑛 ∈ 𝑍 ∣ ∀𝑚 ∈ (ℤ≥‘𝑛)𝑋 ∈ 𝐵} ≠ ∅)) |
20 | 13, 19 | rexlimi 3024 |
. . . . . . 7
⊢
(∃𝑛 ∈
𝑍 ∀𝑚 ∈
(ℤ≥‘𝑛)𝑋 ∈ 𝐵 → {𝑛 ∈ 𝑍 ∣ ∀𝑚 ∈ (ℤ≥‘𝑛)𝑋 ∈ 𝐵} ≠ ∅) |
21 | 20 | a1i 11 |
. . . . . 6
⊢ (𝜑 → (∃𝑛 ∈ 𝑍 ∀𝑚 ∈ (ℤ≥‘𝑛)𝑋 ∈ 𝐵 → {𝑛 ∈ 𝑍 ∣ ∀𝑚 ∈ (ℤ≥‘𝑛)𝑋 ∈ 𝐵} ≠ ∅)) |
22 | 10, 21 | mpd 15 |
. . . . 5
⊢ (𝜑 → {𝑛 ∈ 𝑍 ∣ ∀𝑚 ∈ (ℤ≥‘𝑛)𝑋 ∈ 𝐵} ≠ ∅) |
23 | | infssuzcl 11772 |
. . . . 5
⊢ (({𝑛 ∈ 𝑍 ∣ ∀𝑚 ∈ (ℤ≥‘𝑛)𝑋 ∈ 𝐵} ⊆
(ℤ≥‘𝑀) ∧ {𝑛 ∈ 𝑍 ∣ ∀𝑚 ∈ (ℤ≥‘𝑛)𝑋 ∈ 𝐵} ≠ ∅) → inf({𝑛 ∈ 𝑍 ∣ ∀𝑚 ∈ (ℤ≥‘𝑛)𝑋 ∈ 𝐵}, ℝ, < ) ∈ {𝑛 ∈ 𝑍 ∣ ∀𝑚 ∈ (ℤ≥‘𝑛)𝑋 ∈ 𝐵}) |
24 | 6, 22, 23 | syl2anc 693 |
. . . 4
⊢ (𝜑 → inf({𝑛 ∈ 𝑍 ∣ ∀𝑚 ∈ (ℤ≥‘𝑛)𝑋 ∈ 𝐵}, ℝ, < ) ∈ {𝑛 ∈ 𝑍 ∣ ∀𝑚 ∈ (ℤ≥‘𝑛)𝑋 ∈ 𝐵}) |
25 | 3, 24 | eqeltrd 2701 |
. . 3
⊢ (𝜑 → 𝑁 ∈ {𝑛 ∈ 𝑍 ∣ ∀𝑚 ∈ (ℤ≥‘𝑛)𝑋 ∈ 𝐵}) |
26 | 1, 25 | sseldi 3601 |
. 2
⊢ (𝜑 → 𝑁 ∈ 𝑍) |
27 | | nfcv 2764 |
. . . . . . . 8
⊢
Ⅎ𝑛ℝ |
28 | | nfcv 2764 |
. . . . . . . 8
⊢
Ⅎ𝑛
< |
29 | 11, 27, 28 | nfinf 8388 |
. . . . . . 7
⊢
Ⅎ𝑛inf({𝑛 ∈ 𝑍 ∣ ∀𝑚 ∈ (ℤ≥‘𝑛)𝑋 ∈ 𝐵}, ℝ, < ) |
30 | 2, 29 | nfcxfr 2762 |
. . . . . 6
⊢
Ⅎ𝑛𝑁 |
31 | | nfcv 2764 |
. . . . . 6
⊢
Ⅎ𝑛𝑍 |
32 | | nfcv 2764 |
. . . . . . . 8
⊢
Ⅎ𝑛ℤ≥ |
33 | 32, 30 | nffv 6198 |
. . . . . . 7
⊢
Ⅎ𝑛(ℤ≥‘𝑁) |
34 | | nfv 1843 |
. . . . . . 7
⊢
Ⅎ𝑛 𝑋 ∈ 𝐵 |
35 | 33, 34 | nfral 2945 |
. . . . . 6
⊢
Ⅎ𝑛∀𝑚 ∈ (ℤ≥‘𝑁)𝑋 ∈ 𝐵 |
36 | | nfcv 2764 |
. . . . . . 7
⊢
Ⅎ𝑚(ℤ≥‘𝑛) |
37 | | nfcv 2764 |
. . . . . . . 8
⊢
Ⅎ𝑚ℤ≥ |
38 | | nfra1 2941 |
. . . . . . . . . . 11
⊢
Ⅎ𝑚∀𝑚 ∈ (ℤ≥‘𝑛)𝑋 ∈ 𝐵 |
39 | | nfcv 2764 |
. . . . . . . . . . 11
⊢
Ⅎ𝑚𝑍 |
40 | 38, 39 | nfrab 3123 |
. . . . . . . . . 10
⊢
Ⅎ𝑚{𝑛 ∈ 𝑍 ∣ ∀𝑚 ∈ (ℤ≥‘𝑛)𝑋 ∈ 𝐵} |
41 | | nfcv 2764 |
. . . . . . . . . 10
⊢
Ⅎ𝑚ℝ |
42 | | nfcv 2764 |
. . . . . . . . . 10
⊢
Ⅎ𝑚
< |
43 | 40, 41, 42 | nfinf 8388 |
. . . . . . . . 9
⊢
Ⅎ𝑚inf({𝑛 ∈ 𝑍 ∣ ∀𝑚 ∈ (ℤ≥‘𝑛)𝑋 ∈ 𝐵}, ℝ, < ) |
44 | 2, 43 | nfcxfr 2762 |
. . . . . . . 8
⊢
Ⅎ𝑚𝑁 |
45 | 37, 44 | nffv 6198 |
. . . . . . 7
⊢
Ⅎ𝑚(ℤ≥‘𝑁) |
46 | | fveq2 6191 |
. . . . . . 7
⊢ (𝑛 = 𝑁 → (ℤ≥‘𝑛) =
(ℤ≥‘𝑁)) |
47 | 36, 45, 46 | raleqd 39325 |
. . . . . 6
⊢ (𝑛 = 𝑁 → (∀𝑚 ∈ (ℤ≥‘𝑛)𝑋 ∈ 𝐵 ↔ ∀𝑚 ∈ (ℤ≥‘𝑁)𝑋 ∈ 𝐵)) |
48 | 30, 31, 35, 47 | elrabf 3360 |
. . . . 5
⊢ (𝑁 ∈ {𝑛 ∈ 𝑍 ∣ ∀𝑚 ∈ (ℤ≥‘𝑛)𝑋 ∈ 𝐵} ↔ (𝑁 ∈ 𝑍 ∧ ∀𝑚 ∈ (ℤ≥‘𝑁)𝑋 ∈ 𝐵)) |
49 | 48 | biimpi 206 |
. . . 4
⊢ (𝑁 ∈ {𝑛 ∈ 𝑍 ∣ ∀𝑚 ∈ (ℤ≥‘𝑛)𝑋 ∈ 𝐵} → (𝑁 ∈ 𝑍 ∧ ∀𝑚 ∈ (ℤ≥‘𝑁)𝑋 ∈ 𝐵)) |
50 | 49 | simprd 479 |
. . 3
⊢ (𝑁 ∈ {𝑛 ∈ 𝑍 ∣ ∀𝑚 ∈ (ℤ≥‘𝑛)𝑋 ∈ 𝐵} → ∀𝑚 ∈ (ℤ≥‘𝑁)𝑋 ∈ 𝐵) |
51 | 25, 50 | syl 17 |
. 2
⊢ (𝜑 → ∀𝑚 ∈ (ℤ≥‘𝑁)𝑋 ∈ 𝐵) |
52 | 26, 51 | jca 554 |
1
⊢ (𝜑 → (𝑁 ∈ 𝑍 ∧ ∀𝑚 ∈ (ℤ≥‘𝑁)𝑋 ∈ 𝐵)) |