Proof of Theorem allbutfiinf
| Step | Hyp | Ref
| Expression |
| 1 | | ssrab2 4080 |
. . 3
⊢ {𝑛 ∈ 𝑍 ∣ ∀𝑚 ∈ (ℤ≥‘𝑛)𝑋 ∈ 𝐵} ⊆ 𝑍 |
| 2 | | allbutfiinf.n |
. . . . 5
⊢ 𝑁 = inf({𝑛 ∈ 𝑍 ∣ ∀𝑚 ∈ (ℤ≥‘𝑛)𝑋 ∈ 𝐵}, ℝ, < ) |
| 3 | 2 | a1i 11 |
. . . 4
⊢ (𝜑 → 𝑁 = inf({𝑛 ∈ 𝑍 ∣ ∀𝑚 ∈ (ℤ≥‘𝑛)𝑋 ∈ 𝐵}, ℝ, < )) |
| 4 | | allbutfiinf.z |
. . . . . . 7
⊢ 𝑍 =
(ℤ≥‘𝑀) |
| 5 | 1, 4 | sseqtri 4032 |
. . . . . 6
⊢ {𝑛 ∈ 𝑍 ∣ ∀𝑚 ∈ (ℤ≥‘𝑛)𝑋 ∈ 𝐵} ⊆
(ℤ≥‘𝑀) |
| 6 | 5 | a1i 11 |
. . . . 5
⊢ (𝜑 → {𝑛 ∈ 𝑍 ∣ ∀𝑚 ∈ (ℤ≥‘𝑛)𝑋 ∈ 𝐵} ⊆
(ℤ≥‘𝑀)) |
| 7 | | allbutfiinf.x |
. . . . . . 7
⊢ (𝜑 → 𝑋 ∈ 𝐴) |
| 8 | | allbutfiinf.a |
. . . . . . . 8
⊢ 𝐴 = ∪ 𝑛 ∈ 𝑍 ∩ 𝑚 ∈
(ℤ≥‘𝑛)𝐵 |
| 9 | 4, 8 | allbutfi 45404 |
. . . . . . 7
⊢ (𝑋 ∈ 𝐴 ↔ ∃𝑛 ∈ 𝑍 ∀𝑚 ∈ (ℤ≥‘𝑛)𝑋 ∈ 𝐵) |
| 10 | 7, 9 | sylib 218 |
. . . . . 6
⊢ (𝜑 → ∃𝑛 ∈ 𝑍 ∀𝑚 ∈ (ℤ≥‘𝑛)𝑋 ∈ 𝐵) |
| 11 | | nfrab1 3457 |
. . . . . . . . 9
⊢
Ⅎ𝑛{𝑛 ∈ 𝑍 ∣ ∀𝑚 ∈ (ℤ≥‘𝑛)𝑋 ∈ 𝐵} |
| 12 | | nfcv 2905 |
. . . . . . . . 9
⊢
Ⅎ𝑛∅ |
| 13 | 11, 12 | nfne 3043 |
. . . . . . . 8
⊢
Ⅎ𝑛{𝑛 ∈ 𝑍 ∣ ∀𝑚 ∈ (ℤ≥‘𝑛)𝑋 ∈ 𝐵} ≠ ∅ |
| 14 | | rabid 3458 |
. . . . . . . . . . . 12
⊢ (𝑛 ∈ {𝑛 ∈ 𝑍 ∣ ∀𝑚 ∈ (ℤ≥‘𝑛)𝑋 ∈ 𝐵} ↔ (𝑛 ∈ 𝑍 ∧ ∀𝑚 ∈ (ℤ≥‘𝑛)𝑋 ∈ 𝐵)) |
| 15 | 14 | bicomi 224 |
. . . . . . . . . . 11
⊢ ((𝑛 ∈ 𝑍 ∧ ∀𝑚 ∈ (ℤ≥‘𝑛)𝑋 ∈ 𝐵) ↔ 𝑛 ∈ {𝑛 ∈ 𝑍 ∣ ∀𝑚 ∈ (ℤ≥‘𝑛)𝑋 ∈ 𝐵}) |
| 16 | 15 | biimpi 216 |
. . . . . . . . . 10
⊢ ((𝑛 ∈ 𝑍 ∧ ∀𝑚 ∈ (ℤ≥‘𝑛)𝑋 ∈ 𝐵) → 𝑛 ∈ {𝑛 ∈ 𝑍 ∣ ∀𝑚 ∈ (ℤ≥‘𝑛)𝑋 ∈ 𝐵}) |
| 17 | 16 | ne0d 4342 |
. . . . . . . . 9
⊢ ((𝑛 ∈ 𝑍 ∧ ∀𝑚 ∈ (ℤ≥‘𝑛)𝑋 ∈ 𝐵) → {𝑛 ∈ 𝑍 ∣ ∀𝑚 ∈ (ℤ≥‘𝑛)𝑋 ∈ 𝐵} ≠ ∅) |
| 18 | 17 | ex 412 |
. . . . . . . 8
⊢ (𝑛 ∈ 𝑍 → (∀𝑚 ∈ (ℤ≥‘𝑛)𝑋 ∈ 𝐵 → {𝑛 ∈ 𝑍 ∣ ∀𝑚 ∈ (ℤ≥‘𝑛)𝑋 ∈ 𝐵} ≠ ∅)) |
| 19 | 13, 18 | rexlimi 3259 |
. . . . . . 7
⊢
(∃𝑛 ∈
𝑍 ∀𝑚 ∈
(ℤ≥‘𝑛)𝑋 ∈ 𝐵 → {𝑛 ∈ 𝑍 ∣ ∀𝑚 ∈ (ℤ≥‘𝑛)𝑋 ∈ 𝐵} ≠ ∅) |
| 20 | 19 | a1i 11 |
. . . . . 6
⊢ (𝜑 → (∃𝑛 ∈ 𝑍 ∀𝑚 ∈ (ℤ≥‘𝑛)𝑋 ∈ 𝐵 → {𝑛 ∈ 𝑍 ∣ ∀𝑚 ∈ (ℤ≥‘𝑛)𝑋 ∈ 𝐵} ≠ ∅)) |
| 21 | 10, 20 | mpd 15 |
. . . . 5
⊢ (𝜑 → {𝑛 ∈ 𝑍 ∣ ∀𝑚 ∈ (ℤ≥‘𝑛)𝑋 ∈ 𝐵} ≠ ∅) |
| 22 | | infssuzcl 12974 |
. . . . 5
⊢ (({𝑛 ∈ 𝑍 ∣ ∀𝑚 ∈ (ℤ≥‘𝑛)𝑋 ∈ 𝐵} ⊆
(ℤ≥‘𝑀) ∧ {𝑛 ∈ 𝑍 ∣ ∀𝑚 ∈ (ℤ≥‘𝑛)𝑋 ∈ 𝐵} ≠ ∅) → inf({𝑛 ∈ 𝑍 ∣ ∀𝑚 ∈ (ℤ≥‘𝑛)𝑋 ∈ 𝐵}, ℝ, < ) ∈ {𝑛 ∈ 𝑍 ∣ ∀𝑚 ∈ (ℤ≥‘𝑛)𝑋 ∈ 𝐵}) |
| 23 | 6, 21, 22 | syl2anc 584 |
. . . 4
⊢ (𝜑 → inf({𝑛 ∈ 𝑍 ∣ ∀𝑚 ∈ (ℤ≥‘𝑛)𝑋 ∈ 𝐵}, ℝ, < ) ∈ {𝑛 ∈ 𝑍 ∣ ∀𝑚 ∈ (ℤ≥‘𝑛)𝑋 ∈ 𝐵}) |
| 24 | 3, 23 | eqeltrd 2841 |
. . 3
⊢ (𝜑 → 𝑁 ∈ {𝑛 ∈ 𝑍 ∣ ∀𝑚 ∈ (ℤ≥‘𝑛)𝑋 ∈ 𝐵}) |
| 25 | 1, 24 | sselid 3981 |
. 2
⊢ (𝜑 → 𝑁 ∈ 𝑍) |
| 26 | | nfcv 2905 |
. . . . . . . 8
⊢
Ⅎ𝑛ℝ |
| 27 | | nfcv 2905 |
. . . . . . . 8
⊢
Ⅎ𝑛
< |
| 28 | 11, 26, 27 | nfinf 9522 |
. . . . . . 7
⊢
Ⅎ𝑛inf({𝑛 ∈ 𝑍 ∣ ∀𝑚 ∈ (ℤ≥‘𝑛)𝑋 ∈ 𝐵}, ℝ, < ) |
| 29 | 2, 28 | nfcxfr 2903 |
. . . . . 6
⊢
Ⅎ𝑛𝑁 |
| 30 | | nfcv 2905 |
. . . . . 6
⊢
Ⅎ𝑛𝑍 |
| 31 | | nfcv 2905 |
. . . . . . . 8
⊢
Ⅎ𝑛ℤ≥ |
| 32 | 31, 29 | nffv 6916 |
. . . . . . 7
⊢
Ⅎ𝑛(ℤ≥‘𝑁) |
| 33 | | nfv 1914 |
. . . . . . 7
⊢
Ⅎ𝑛 𝑋 ∈ 𝐵 |
| 34 | 32, 33 | nfralw 3311 |
. . . . . 6
⊢
Ⅎ𝑛∀𝑚 ∈ (ℤ≥‘𝑁)𝑋 ∈ 𝐵 |
| 35 | | nfcv 2905 |
. . . . . . 7
⊢
Ⅎ𝑚(ℤ≥‘𝑛) |
| 36 | | nfcv 2905 |
. . . . . . . 8
⊢
Ⅎ𝑚ℤ≥ |
| 37 | | nfra1 3284 |
. . . . . . . . . . 11
⊢
Ⅎ𝑚∀𝑚 ∈ (ℤ≥‘𝑛)𝑋 ∈ 𝐵 |
| 38 | | nfcv 2905 |
. . . . . . . . . . 11
⊢
Ⅎ𝑚𝑍 |
| 39 | 37, 38 | nfrabw 3475 |
. . . . . . . . . 10
⊢
Ⅎ𝑚{𝑛 ∈ 𝑍 ∣ ∀𝑚 ∈ (ℤ≥‘𝑛)𝑋 ∈ 𝐵} |
| 40 | | nfcv 2905 |
. . . . . . . . . 10
⊢
Ⅎ𝑚ℝ |
| 41 | | nfcv 2905 |
. . . . . . . . . 10
⊢
Ⅎ𝑚
< |
| 42 | 39, 40, 41 | nfinf 9522 |
. . . . . . . . 9
⊢
Ⅎ𝑚inf({𝑛 ∈ 𝑍 ∣ ∀𝑚 ∈ (ℤ≥‘𝑛)𝑋 ∈ 𝐵}, ℝ, < ) |
| 43 | 2, 42 | nfcxfr 2903 |
. . . . . . . 8
⊢
Ⅎ𝑚𝑁 |
| 44 | 36, 43 | nffv 6916 |
. . . . . . 7
⊢
Ⅎ𝑚(ℤ≥‘𝑁) |
| 45 | | fveq2 6906 |
. . . . . . 7
⊢ (𝑛 = 𝑁 → (ℤ≥‘𝑛) =
(ℤ≥‘𝑁)) |
| 46 | 35, 44, 45 | raleqd 45142 |
. . . . . 6
⊢ (𝑛 = 𝑁 → (∀𝑚 ∈ (ℤ≥‘𝑛)𝑋 ∈ 𝐵 ↔ ∀𝑚 ∈ (ℤ≥‘𝑁)𝑋 ∈ 𝐵)) |
| 47 | 29, 30, 34, 46 | elrabf 3688 |
. . . . 5
⊢ (𝑁 ∈ {𝑛 ∈ 𝑍 ∣ ∀𝑚 ∈ (ℤ≥‘𝑛)𝑋 ∈ 𝐵} ↔ (𝑁 ∈ 𝑍 ∧ ∀𝑚 ∈ (ℤ≥‘𝑁)𝑋 ∈ 𝐵)) |
| 48 | 47 | biimpi 216 |
. . . 4
⊢ (𝑁 ∈ {𝑛 ∈ 𝑍 ∣ ∀𝑚 ∈ (ℤ≥‘𝑛)𝑋 ∈ 𝐵} → (𝑁 ∈ 𝑍 ∧ ∀𝑚 ∈ (ℤ≥‘𝑁)𝑋 ∈ 𝐵)) |
| 49 | 48 | simprd 495 |
. . 3
⊢ (𝑁 ∈ {𝑛 ∈ 𝑍 ∣ ∀𝑚 ∈ (ℤ≥‘𝑛)𝑋 ∈ 𝐵} → ∀𝑚 ∈ (ℤ≥‘𝑁)𝑋 ∈ 𝐵) |
| 50 | 24, 49 | syl 17 |
. 2
⊢ (𝜑 → ∀𝑚 ∈ (ℤ≥‘𝑁)𝑋 ∈ 𝐵) |
| 51 | 25, 50 | jca 511 |
1
⊢ (𝜑 → (𝑁 ∈ 𝑍 ∧ ∀𝑚 ∈ (ℤ≥‘𝑁)𝑋 ∈ 𝐵)) |