Step | Hyp | Ref
| Expression |
1 | | uzfissfz.m |
. . . . . 6
⊢ (𝜑 → 𝑀 ∈ ℤ) |
2 | | uzid 12453 |
. . . . . 6
⊢ (𝑀 ∈ ℤ → 𝑀 ∈
(ℤ≥‘𝑀)) |
3 | 1, 2 | syl 17 |
. . . . 5
⊢ (𝜑 → 𝑀 ∈ (ℤ≥‘𝑀)) |
4 | | uzfissfz.z |
. . . . . . 7
⊢ 𝑍 =
(ℤ≥‘𝑀) |
5 | 4 | a1i 11 |
. . . . . 6
⊢ (𝜑 → 𝑍 = (ℤ≥‘𝑀)) |
6 | 5 | eqcomd 2743 |
. . . . 5
⊢ (𝜑 →
(ℤ≥‘𝑀) = 𝑍) |
7 | 3, 6 | eleqtrd 2840 |
. . . 4
⊢ (𝜑 → 𝑀 ∈ 𝑍) |
8 | 7 | adantr 484 |
. . 3
⊢ ((𝜑 ∧ 𝐴 = ∅) → 𝑀 ∈ 𝑍) |
9 | | id 22 |
. . . . 5
⊢ (𝐴 = ∅ → 𝐴 = ∅) |
10 | | 0ss 4311 |
. . . . . 6
⊢ ∅
⊆ (𝑀...𝑀) |
11 | 10 | a1i 11 |
. . . . 5
⊢ (𝐴 = ∅ → ∅
⊆ (𝑀...𝑀)) |
12 | 9, 11 | eqsstrd 3939 |
. . . 4
⊢ (𝐴 = ∅ → 𝐴 ⊆ (𝑀...𝑀)) |
13 | 12 | adantl 485 |
. . 3
⊢ ((𝜑 ∧ 𝐴 = ∅) → 𝐴 ⊆ (𝑀...𝑀)) |
14 | | oveq2 7221 |
. . . . 5
⊢ (𝑘 = 𝑀 → (𝑀...𝑘) = (𝑀...𝑀)) |
15 | 14 | sseq2d 3933 |
. . . 4
⊢ (𝑘 = 𝑀 → (𝐴 ⊆ (𝑀...𝑘) ↔ 𝐴 ⊆ (𝑀...𝑀))) |
16 | 15 | rspcev 3537 |
. . 3
⊢ ((𝑀 ∈ 𝑍 ∧ 𝐴 ⊆ (𝑀...𝑀)) → ∃𝑘 ∈ 𝑍 𝐴 ⊆ (𝑀...𝑘)) |
17 | 8, 13, 16 | syl2anc 587 |
. 2
⊢ ((𝜑 ∧ 𝐴 = ∅) → ∃𝑘 ∈ 𝑍 𝐴 ⊆ (𝑀...𝑘)) |
18 | | uzfissfz.a |
. . . . 5
⊢ (𝜑 → 𝐴 ⊆ 𝑍) |
19 | 18 | adantr 484 |
. . . 4
⊢ ((𝜑 ∧ ¬ 𝐴 = ∅) → 𝐴 ⊆ 𝑍) |
20 | | uzssz 12459 |
. . . . . . . . 9
⊢
(ℤ≥‘𝑀) ⊆ ℤ |
21 | 4, 20 | eqsstri 3935 |
. . . . . . . 8
⊢ 𝑍 ⊆
ℤ |
22 | 21 | a1i 11 |
. . . . . . 7
⊢ (𝜑 → 𝑍 ⊆ ℤ) |
23 | 18, 22 | sstrd 3911 |
. . . . . 6
⊢ (𝜑 → 𝐴 ⊆ ℤ) |
24 | 23 | adantr 484 |
. . . . 5
⊢ ((𝜑 ∧ ¬ 𝐴 = ∅) → 𝐴 ⊆ ℤ) |
25 | 9 | necon3bi 2967 |
. . . . . 6
⊢ (¬
𝐴 = ∅ → 𝐴 ≠ ∅) |
26 | 25 | adantl 485 |
. . . . 5
⊢ ((𝜑 ∧ ¬ 𝐴 = ∅) → 𝐴 ≠ ∅) |
27 | | uzfissfz.fi |
. . . . . 6
⊢ (𝜑 → 𝐴 ∈ Fin) |
28 | 27 | adantr 484 |
. . . . 5
⊢ ((𝜑 ∧ ¬ 𝐴 = ∅) → 𝐴 ∈ Fin) |
29 | | suprfinzcl 12292 |
. . . . 5
⊢ ((𝐴 ⊆ ℤ ∧ 𝐴 ≠ ∅ ∧ 𝐴 ∈ Fin) → sup(𝐴, ℝ, < ) ∈ 𝐴) |
30 | 24, 26, 28, 29 | syl3anc 1373 |
. . . 4
⊢ ((𝜑 ∧ ¬ 𝐴 = ∅) → sup(𝐴, ℝ, < ) ∈ 𝐴) |
31 | 19, 30 | sseldd 3902 |
. . 3
⊢ ((𝜑 ∧ ¬ 𝐴 = ∅) → sup(𝐴, ℝ, < ) ∈ 𝑍) |
32 | 1 | ad2antrr 726 |
. . . . . 6
⊢ (((𝜑 ∧ ¬ 𝐴 = ∅) ∧ 𝑗 ∈ 𝐴) → 𝑀 ∈ ℤ) |
33 | 21, 31 | sseldi 3899 |
. . . . . . 7
⊢ ((𝜑 ∧ ¬ 𝐴 = ∅) → sup(𝐴, ℝ, < ) ∈
ℤ) |
34 | 33 | adantr 484 |
. . . . . 6
⊢ (((𝜑 ∧ ¬ 𝐴 = ∅) ∧ 𝑗 ∈ 𝐴) → sup(𝐴, ℝ, < ) ∈
ℤ) |
35 | 24 | sselda 3901 |
. . . . . 6
⊢ (((𝜑 ∧ ¬ 𝐴 = ∅) ∧ 𝑗 ∈ 𝐴) → 𝑗 ∈ ℤ) |
36 | 18 | sselda 3901 |
. . . . . . . . 9
⊢ ((𝜑 ∧ 𝑗 ∈ 𝐴) → 𝑗 ∈ 𝑍) |
37 | 4 | a1i 11 |
. . . . . . . . 9
⊢ ((𝜑 ∧ 𝑗 ∈ 𝐴) → 𝑍 = (ℤ≥‘𝑀)) |
38 | 36, 37 | eleqtrd 2840 |
. . . . . . . 8
⊢ ((𝜑 ∧ 𝑗 ∈ 𝐴) → 𝑗 ∈ (ℤ≥‘𝑀)) |
39 | | eluzle 12451 |
. . . . . . . 8
⊢ (𝑗 ∈
(ℤ≥‘𝑀) → 𝑀 ≤ 𝑗) |
40 | 38, 39 | syl 17 |
. . . . . . 7
⊢ ((𝜑 ∧ 𝑗 ∈ 𝐴) → 𝑀 ≤ 𝑗) |
41 | 40 | adantlr 715 |
. . . . . 6
⊢ (((𝜑 ∧ ¬ 𝐴 = ∅) ∧ 𝑗 ∈ 𝐴) → 𝑀 ≤ 𝑗) |
42 | | zssre 12183 |
. . . . . . . . 9
⊢ ℤ
⊆ ℝ |
43 | 23, 42 | sstrdi 3913 |
. . . . . . . 8
⊢ (𝜑 → 𝐴 ⊆ ℝ) |
44 | 43 | ad2antrr 726 |
. . . . . . 7
⊢ (((𝜑 ∧ ¬ 𝐴 = ∅) ∧ 𝑗 ∈ 𝐴) → 𝐴 ⊆ ℝ) |
45 | 26 | adantr 484 |
. . . . . . 7
⊢ (((𝜑 ∧ ¬ 𝐴 = ∅) ∧ 𝑗 ∈ 𝐴) → 𝐴 ≠ ∅) |
46 | | fimaxre2 11777 |
. . . . . . . . 9
⊢ ((𝐴 ⊆ ℝ ∧ 𝐴 ∈ Fin) → ∃𝑥 ∈ ℝ ∀𝑦 ∈ 𝐴 𝑦 ≤ 𝑥) |
47 | 43, 27, 46 | syl2anc 587 |
. . . . . . . 8
⊢ (𝜑 → ∃𝑥 ∈ ℝ ∀𝑦 ∈ 𝐴 𝑦 ≤ 𝑥) |
48 | 47 | ad2antrr 726 |
. . . . . . 7
⊢ (((𝜑 ∧ ¬ 𝐴 = ∅) ∧ 𝑗 ∈ 𝐴) → ∃𝑥 ∈ ℝ ∀𝑦 ∈ 𝐴 𝑦 ≤ 𝑥) |
49 | | simpr 488 |
. . . . . . 7
⊢ (((𝜑 ∧ ¬ 𝐴 = ∅) ∧ 𝑗 ∈ 𝐴) → 𝑗 ∈ 𝐴) |
50 | | suprub 11793 |
. . . . . . 7
⊢ (((𝐴 ⊆ ℝ ∧ 𝐴 ≠ ∅ ∧ ∃𝑥 ∈ ℝ ∀𝑦 ∈ 𝐴 𝑦 ≤ 𝑥) ∧ 𝑗 ∈ 𝐴) → 𝑗 ≤ sup(𝐴, ℝ, < )) |
51 | 44, 45, 48, 49, 50 | syl31anc 1375 |
. . . . . 6
⊢ (((𝜑 ∧ ¬ 𝐴 = ∅) ∧ 𝑗 ∈ 𝐴) → 𝑗 ≤ sup(𝐴, ℝ, < )) |
52 | 32, 34, 35, 41, 51 | elfzd 13103 |
. . . . 5
⊢ (((𝜑 ∧ ¬ 𝐴 = ∅) ∧ 𝑗 ∈ 𝐴) → 𝑗 ∈ (𝑀...sup(𝐴, ℝ, < ))) |
53 | 52 | ralrimiva 3105 |
. . . 4
⊢ ((𝜑 ∧ ¬ 𝐴 = ∅) → ∀𝑗 ∈ 𝐴 𝑗 ∈ (𝑀...sup(𝐴, ℝ, < ))) |
54 | | dfss3 3888 |
. . . 4
⊢ (𝐴 ⊆ (𝑀...sup(𝐴, ℝ, < )) ↔ ∀𝑗 ∈ 𝐴 𝑗 ∈ (𝑀...sup(𝐴, ℝ, < ))) |
55 | 53, 54 | sylibr 237 |
. . 3
⊢ ((𝜑 ∧ ¬ 𝐴 = ∅) → 𝐴 ⊆ (𝑀...sup(𝐴, ℝ, < ))) |
56 | | oveq2 7221 |
. . . . 5
⊢ (𝑘 = sup(𝐴, ℝ, < ) → (𝑀...𝑘) = (𝑀...sup(𝐴, ℝ, < ))) |
57 | 56 | sseq2d 3933 |
. . . 4
⊢ (𝑘 = sup(𝐴, ℝ, < ) → (𝐴 ⊆ (𝑀...𝑘) ↔ 𝐴 ⊆ (𝑀...sup(𝐴, ℝ, < )))) |
58 | 57 | rspcev 3537 |
. . 3
⊢
((sup(𝐴, ℝ,
< ) ∈ 𝑍 ∧ 𝐴 ⊆ (𝑀...sup(𝐴, ℝ, < ))) → ∃𝑘 ∈ 𝑍 𝐴 ⊆ (𝑀...𝑘)) |
59 | 31, 55, 58 | syl2anc 587 |
. 2
⊢ ((𝜑 ∧ ¬ 𝐴 = ∅) → ∃𝑘 ∈ 𝑍 𝐴 ⊆ (𝑀...𝑘)) |
60 | 17, 59 | pm2.61dan 813 |
1
⊢ (𝜑 → ∃𝑘 ∈ 𝑍 𝐴 ⊆ (𝑀...𝑘)) |