Step | Hyp | Ref
| Expression |
1 | | ssel2 3912 |
. . . . . . 7
⊢ ((𝐴 ⊆ (0[,]+∞) ∧
𝑦 ∈ 𝐴) → 𝑦 ∈ (0[,]+∞)) |
2 | | 0xr 10910 |
. . . . . . . . 9
⊢ 0 ∈
ℝ* |
3 | | pnfxr 10917 |
. . . . . . . . 9
⊢ +∞
∈ ℝ* |
4 | | iccgelb 13021 |
. . . . . . . . 9
⊢ ((0
∈ ℝ* ∧ +∞ ∈ ℝ* ∧
𝑦 ∈ (0[,]+∞))
→ 0 ≤ 𝑦) |
5 | 2, 3, 4 | mp3an12 1453 |
. . . . . . . 8
⊢ (𝑦 ∈ (0[,]+∞) → 0
≤ 𝑦) |
6 | | eliccxr 13053 |
. . . . . . . . 9
⊢ (𝑦 ∈ (0[,]+∞) →
𝑦 ∈
ℝ*) |
7 | | xrlenlt 10928 |
. . . . . . . . 9
⊢ ((0
∈ ℝ* ∧ 𝑦 ∈ ℝ*) → (0 ≤
𝑦 ↔ ¬ 𝑦 < 0)) |
8 | 2, 6, 7 | sylancr 590 |
. . . . . . . 8
⊢ (𝑦 ∈ (0[,]+∞) → (0
≤ 𝑦 ↔ ¬ 𝑦 < 0)) |
9 | 5, 8 | mpbid 235 |
. . . . . . 7
⊢ (𝑦 ∈ (0[,]+∞) →
¬ 𝑦 <
0) |
10 | 1, 9 | syl 17 |
. . . . . 6
⊢ ((𝐴 ⊆ (0[,]+∞) ∧
𝑦 ∈ 𝐴) → ¬ 𝑦 < 0) |
11 | 10 | ralrimiva 3108 |
. . . . 5
⊢ (𝐴 ⊆ (0[,]+∞) →
∀𝑦 ∈ 𝐴 ¬ 𝑦 < 0) |
12 | 11 | ad3antrrr 730 |
. . . 4
⊢ ((((𝐴 ⊆ (0[,]+∞) ∧
𝑤 ∈
ℝ*) ∧ (∀𝑦 ∈ 𝐴 ¬ 𝑦 < 𝑤 ∧ ∀𝑦 ∈ ℝ* (𝑤 < 𝑦 → ∃𝑧 ∈ 𝐴 𝑧 < 𝑦))) ∧ 𝑤 ≤ 0) → ∀𝑦 ∈ 𝐴 ¬ 𝑦 < 0) |
13 | | iccssxr 13048 |
. . . . . . . . . 10
⊢
(0[,]+∞) ⊆ ℝ* |
14 | | ssralv 3984 |
. . . . . . . . . 10
⊢
((0[,]+∞) ⊆ ℝ* → (∀𝑦 ∈ ℝ*
(𝑤 < 𝑦 → ∃𝑧 ∈ 𝐴 𝑧 < 𝑦) → ∀𝑦 ∈ (0[,]+∞)(𝑤 < 𝑦 → ∃𝑧 ∈ 𝐴 𝑧 < 𝑦))) |
15 | 13, 14 | ax-mp 5 |
. . . . . . . . 9
⊢
(∀𝑦 ∈
ℝ* (𝑤 <
𝑦 → ∃𝑧 ∈ 𝐴 𝑧 < 𝑦) → ∀𝑦 ∈ (0[,]+∞)(𝑤 < 𝑦 → ∃𝑧 ∈ 𝐴 𝑧 < 𝑦)) |
16 | | simplll 775 |
. . . . . . . . . . . . 13
⊢ ((((𝑤 ∈ ℝ*
∧ 𝑤 ≤ 0) ∧ 𝑦 ∈ (0[,]+∞)) ∧ 0
< 𝑦) → 𝑤 ∈
ℝ*) |
17 | 2 | a1i 11 |
. . . . . . . . . . . . 13
⊢ ((((𝑤 ∈ ℝ*
∧ 𝑤 ≤ 0) ∧ 𝑦 ∈ (0[,]+∞)) ∧ 0
< 𝑦) → 0 ∈
ℝ*) |
18 | | simplr 769 |
. . . . . . . . . . . . . 14
⊢ ((((𝑤 ∈ ℝ*
∧ 𝑤 ≤ 0) ∧ 𝑦 ∈ (0[,]+∞)) ∧ 0
< 𝑦) → 𝑦 ∈
(0[,]+∞)) |
19 | 13, 18 | sselid 3915 |
. . . . . . . . . . . . 13
⊢ ((((𝑤 ∈ ℝ*
∧ 𝑤 ≤ 0) ∧ 𝑦 ∈ (0[,]+∞)) ∧ 0
< 𝑦) → 𝑦 ∈
ℝ*) |
20 | | simpllr 776 |
. . . . . . . . . . . . 13
⊢ ((((𝑤 ∈ ℝ*
∧ 𝑤 ≤ 0) ∧ 𝑦 ∈ (0[,]+∞)) ∧ 0
< 𝑦) → 𝑤 ≤ 0) |
21 | | simpr 488 |
. . . . . . . . . . . . 13
⊢ ((((𝑤 ∈ ℝ*
∧ 𝑤 ≤ 0) ∧ 𝑦 ∈ (0[,]+∞)) ∧ 0
< 𝑦) → 0 < 𝑦) |
22 | 16, 17, 19, 20, 21 | xrlelttrd 12780 |
. . . . . . . . . . . 12
⊢ ((((𝑤 ∈ ℝ*
∧ 𝑤 ≤ 0) ∧ 𝑦 ∈ (0[,]+∞)) ∧ 0
< 𝑦) → 𝑤 < 𝑦) |
23 | 22 | ex 416 |
. . . . . . . . . . 11
⊢ (((𝑤 ∈ ℝ*
∧ 𝑤 ≤ 0) ∧ 𝑦 ∈ (0[,]+∞)) →
(0 < 𝑦 → 𝑤 < 𝑦)) |
24 | 23 | imim1d 82 |
. . . . . . . . . 10
⊢ (((𝑤 ∈ ℝ*
∧ 𝑤 ≤ 0) ∧ 𝑦 ∈ (0[,]+∞)) →
((𝑤 < 𝑦 → ∃𝑧 ∈ 𝐴 𝑧 < 𝑦) → (0 < 𝑦 → ∃𝑧 ∈ 𝐴 𝑧 < 𝑦))) |
25 | 24 | ralimdva 3103 |
. . . . . . . . 9
⊢ ((𝑤 ∈ ℝ*
∧ 𝑤 ≤ 0) →
(∀𝑦 ∈
(0[,]+∞)(𝑤 < 𝑦 → ∃𝑧 ∈ 𝐴 𝑧 < 𝑦) → ∀𝑦 ∈ (0[,]+∞)(0 < 𝑦 → ∃𝑧 ∈ 𝐴 𝑧 < 𝑦))) |
26 | 15, 25 | syl5 34 |
. . . . . . . 8
⊢ ((𝑤 ∈ ℝ*
∧ 𝑤 ≤ 0) →
(∀𝑦 ∈
ℝ* (𝑤 <
𝑦 → ∃𝑧 ∈ 𝐴 𝑧 < 𝑦) → ∀𝑦 ∈ (0[,]+∞)(0 < 𝑦 → ∃𝑧 ∈ 𝐴 𝑧 < 𝑦))) |
27 | 26 | adantll 714 |
. . . . . . 7
⊢ (((𝐴 ⊆ (0[,]+∞) ∧
𝑤 ∈
ℝ*) ∧ 𝑤 ≤ 0) → (∀𝑦 ∈ ℝ* (𝑤 < 𝑦 → ∃𝑧 ∈ 𝐴 𝑧 < 𝑦) → ∀𝑦 ∈ (0[,]+∞)(0 < 𝑦 → ∃𝑧 ∈ 𝐴 𝑧 < 𝑦))) |
28 | 27 | imp 410 |
. . . . . 6
⊢ ((((𝐴 ⊆ (0[,]+∞) ∧
𝑤 ∈
ℝ*) ∧ 𝑤 ≤ 0) ∧ ∀𝑦 ∈ ℝ* (𝑤 < 𝑦 → ∃𝑧 ∈ 𝐴 𝑧 < 𝑦)) → ∀𝑦 ∈ (0[,]+∞)(0 < 𝑦 → ∃𝑧 ∈ 𝐴 𝑧 < 𝑦)) |
29 | 28 | adantrl 716 |
. . . . 5
⊢ ((((𝐴 ⊆ (0[,]+∞) ∧
𝑤 ∈
ℝ*) ∧ 𝑤 ≤ 0) ∧ (∀𝑦 ∈ 𝐴 ¬ 𝑦 < 𝑤 ∧ ∀𝑦 ∈ ℝ* (𝑤 < 𝑦 → ∃𝑧 ∈ 𝐴 𝑧 < 𝑦))) → ∀𝑦 ∈ (0[,]+∞)(0 < 𝑦 → ∃𝑧 ∈ 𝐴 𝑧 < 𝑦)) |
30 | 29 | an32s 652 |
. . . 4
⊢ ((((𝐴 ⊆ (0[,]+∞) ∧
𝑤 ∈
ℝ*) ∧ (∀𝑦 ∈ 𝐴 ¬ 𝑦 < 𝑤 ∧ ∀𝑦 ∈ ℝ* (𝑤 < 𝑦 → ∃𝑧 ∈ 𝐴 𝑧 < 𝑦))) ∧ 𝑤 ≤ 0) → ∀𝑦 ∈ (0[,]+∞)(0 < 𝑦 → ∃𝑧 ∈ 𝐴 𝑧 < 𝑦)) |
31 | | 0e0iccpnf 13077 |
. . . . 5
⊢ 0 ∈
(0[,]+∞) |
32 | | breq2 5074 |
. . . . . . . . 9
⊢ (𝑥 = 0 → (𝑦 < 𝑥 ↔ 𝑦 < 0)) |
33 | 32 | notbid 321 |
. . . . . . . 8
⊢ (𝑥 = 0 → (¬ 𝑦 < 𝑥 ↔ ¬ 𝑦 < 0)) |
34 | 33 | ralbidv 3121 |
. . . . . . 7
⊢ (𝑥 = 0 → (∀𝑦 ∈ 𝐴 ¬ 𝑦 < 𝑥 ↔ ∀𝑦 ∈ 𝐴 ¬ 𝑦 < 0)) |
35 | | breq1 5073 |
. . . . . . . . 9
⊢ (𝑥 = 0 → (𝑥 < 𝑦 ↔ 0 < 𝑦)) |
36 | 35 | imbi1d 345 |
. . . . . . . 8
⊢ (𝑥 = 0 → ((𝑥 < 𝑦 → ∃𝑧 ∈ 𝐴 𝑧 < 𝑦) ↔ (0 < 𝑦 → ∃𝑧 ∈ 𝐴 𝑧 < 𝑦))) |
37 | 36 | ralbidv 3121 |
. . . . . . 7
⊢ (𝑥 = 0 → (∀𝑦 ∈ (0[,]+∞)(𝑥 < 𝑦 → ∃𝑧 ∈ 𝐴 𝑧 < 𝑦) ↔ ∀𝑦 ∈ (0[,]+∞)(0 < 𝑦 → ∃𝑧 ∈ 𝐴 𝑧 < 𝑦))) |
38 | 34, 37 | anbi12d 634 |
. . . . . 6
⊢ (𝑥 = 0 → ((∀𝑦 ∈ 𝐴 ¬ 𝑦 < 𝑥 ∧ ∀𝑦 ∈ (0[,]+∞)(𝑥 < 𝑦 → ∃𝑧 ∈ 𝐴 𝑧 < 𝑦)) ↔ (∀𝑦 ∈ 𝐴 ¬ 𝑦 < 0 ∧ ∀𝑦 ∈ (0[,]+∞)(0 < 𝑦 → ∃𝑧 ∈ 𝐴 𝑧 < 𝑦)))) |
39 | 38 | rspcev 3552 |
. . . . 5
⊢ ((0
∈ (0[,]+∞) ∧ (∀𝑦 ∈ 𝐴 ¬ 𝑦 < 0 ∧ ∀𝑦 ∈ (0[,]+∞)(0 < 𝑦 → ∃𝑧 ∈ 𝐴 𝑧 < 𝑦))) → ∃𝑥 ∈ (0[,]+∞)(∀𝑦 ∈ 𝐴 ¬ 𝑦 < 𝑥 ∧ ∀𝑦 ∈ (0[,]+∞)(𝑥 < 𝑦 → ∃𝑧 ∈ 𝐴 𝑧 < 𝑦))) |
40 | 31, 39 | mpan 690 |
. . . 4
⊢
((∀𝑦 ∈
𝐴 ¬ 𝑦 < 0 ∧ ∀𝑦 ∈ (0[,]+∞)(0 < 𝑦 → ∃𝑧 ∈ 𝐴 𝑧 < 𝑦)) → ∃𝑥 ∈ (0[,]+∞)(∀𝑦 ∈ 𝐴 ¬ 𝑦 < 𝑥 ∧ ∀𝑦 ∈ (0[,]+∞)(𝑥 < 𝑦 → ∃𝑧 ∈ 𝐴 𝑧 < 𝑦))) |
41 | 12, 30, 40 | syl2anc 587 |
. . 3
⊢ ((((𝐴 ⊆ (0[,]+∞) ∧
𝑤 ∈
ℝ*) ∧ (∀𝑦 ∈ 𝐴 ¬ 𝑦 < 𝑤 ∧ ∀𝑦 ∈ ℝ* (𝑤 < 𝑦 → ∃𝑧 ∈ 𝐴 𝑧 < 𝑦))) ∧ 𝑤 ≤ 0) → ∃𝑥 ∈ (0[,]+∞)(∀𝑦 ∈ 𝐴 ¬ 𝑦 < 𝑥 ∧ ∀𝑦 ∈ (0[,]+∞)(𝑥 < 𝑦 → ∃𝑧 ∈ 𝐴 𝑧 < 𝑦))) |
42 | | simpllr 776 |
. . . . 5
⊢ ((((𝐴 ⊆ (0[,]+∞) ∧
𝑤 ∈
ℝ*) ∧ (∀𝑦 ∈ 𝐴 ¬ 𝑦 < 𝑤 ∧ ∀𝑦 ∈ ℝ* (𝑤 < 𝑦 → ∃𝑧 ∈ 𝐴 𝑧 < 𝑦))) ∧ 0 ≤ 𝑤) → 𝑤 ∈ ℝ*) |
43 | | simpr 488 |
. . . . 5
⊢ ((((𝐴 ⊆ (0[,]+∞) ∧
𝑤 ∈
ℝ*) ∧ (∀𝑦 ∈ 𝐴 ¬ 𝑦 < 𝑤 ∧ ∀𝑦 ∈ ℝ* (𝑤 < 𝑦 → ∃𝑧 ∈ 𝐴 𝑧 < 𝑦))) ∧ 0 ≤ 𝑤) → 0 ≤ 𝑤) |
44 | | elxrge0 13075 |
. . . . 5
⊢ (𝑤 ∈ (0[,]+∞) ↔
(𝑤 ∈
ℝ* ∧ 0 ≤ 𝑤)) |
45 | 42, 43, 44 | sylanbrc 586 |
. . . 4
⊢ ((((𝐴 ⊆ (0[,]+∞) ∧
𝑤 ∈
ℝ*) ∧ (∀𝑦 ∈ 𝐴 ¬ 𝑦 < 𝑤 ∧ ∀𝑦 ∈ ℝ* (𝑤 < 𝑦 → ∃𝑧 ∈ 𝐴 𝑧 < 𝑦))) ∧ 0 ≤ 𝑤) → 𝑤 ∈ (0[,]+∞)) |
46 | 15 | a1i 11 |
. . . . . . . 8
⊢ (𝐴 ⊆ (0[,]+∞) →
(∀𝑦 ∈
ℝ* (𝑤 <
𝑦 → ∃𝑧 ∈ 𝐴 𝑧 < 𝑦) → ∀𝑦 ∈ (0[,]+∞)(𝑤 < 𝑦 → ∃𝑧 ∈ 𝐴 𝑧 < 𝑦))) |
47 | 46 | anim2d 615 |
. . . . . . 7
⊢ (𝐴 ⊆ (0[,]+∞) →
((∀𝑦 ∈ 𝐴 ¬ 𝑦 < 𝑤 ∧ ∀𝑦 ∈ ℝ* (𝑤 < 𝑦 → ∃𝑧 ∈ 𝐴 𝑧 < 𝑦)) → (∀𝑦 ∈ 𝐴 ¬ 𝑦 < 𝑤 ∧ ∀𝑦 ∈ (0[,]+∞)(𝑤 < 𝑦 → ∃𝑧 ∈ 𝐴 𝑧 < 𝑦)))) |
48 | 47 | adantr 484 |
. . . . . 6
⊢ ((𝐴 ⊆ (0[,]+∞) ∧
𝑤 ∈
ℝ*) → ((∀𝑦 ∈ 𝐴 ¬ 𝑦 < 𝑤 ∧ ∀𝑦 ∈ ℝ* (𝑤 < 𝑦 → ∃𝑧 ∈ 𝐴 𝑧 < 𝑦)) → (∀𝑦 ∈ 𝐴 ¬ 𝑦 < 𝑤 ∧ ∀𝑦 ∈ (0[,]+∞)(𝑤 < 𝑦 → ∃𝑧 ∈ 𝐴 𝑧 < 𝑦)))) |
49 | 48 | imp 410 |
. . . . 5
⊢ (((𝐴 ⊆ (0[,]+∞) ∧
𝑤 ∈
ℝ*) ∧ (∀𝑦 ∈ 𝐴 ¬ 𝑦 < 𝑤 ∧ ∀𝑦 ∈ ℝ* (𝑤 < 𝑦 → ∃𝑧 ∈ 𝐴 𝑧 < 𝑦))) → (∀𝑦 ∈ 𝐴 ¬ 𝑦 < 𝑤 ∧ ∀𝑦 ∈ (0[,]+∞)(𝑤 < 𝑦 → ∃𝑧 ∈ 𝐴 𝑧 < 𝑦))) |
50 | 49 | adantr 484 |
. . . 4
⊢ ((((𝐴 ⊆ (0[,]+∞) ∧
𝑤 ∈
ℝ*) ∧ (∀𝑦 ∈ 𝐴 ¬ 𝑦 < 𝑤 ∧ ∀𝑦 ∈ ℝ* (𝑤 < 𝑦 → ∃𝑧 ∈ 𝐴 𝑧 < 𝑦))) ∧ 0 ≤ 𝑤) → (∀𝑦 ∈ 𝐴 ¬ 𝑦 < 𝑤 ∧ ∀𝑦 ∈ (0[,]+∞)(𝑤 < 𝑦 → ∃𝑧 ∈ 𝐴 𝑧 < 𝑦))) |
51 | | breq2 5074 |
. . . . . . . 8
⊢ (𝑥 = 𝑤 → (𝑦 < 𝑥 ↔ 𝑦 < 𝑤)) |
52 | 51 | notbid 321 |
. . . . . . 7
⊢ (𝑥 = 𝑤 → (¬ 𝑦 < 𝑥 ↔ ¬ 𝑦 < 𝑤)) |
53 | 52 | ralbidv 3121 |
. . . . . 6
⊢ (𝑥 = 𝑤 → (∀𝑦 ∈ 𝐴 ¬ 𝑦 < 𝑥 ↔ ∀𝑦 ∈ 𝐴 ¬ 𝑦 < 𝑤)) |
54 | | breq1 5073 |
. . . . . . . 8
⊢ (𝑥 = 𝑤 → (𝑥 < 𝑦 ↔ 𝑤 < 𝑦)) |
55 | 54 | imbi1d 345 |
. . . . . . 7
⊢ (𝑥 = 𝑤 → ((𝑥 < 𝑦 → ∃𝑧 ∈ 𝐴 𝑧 < 𝑦) ↔ (𝑤 < 𝑦 → ∃𝑧 ∈ 𝐴 𝑧 < 𝑦))) |
56 | 55 | ralbidv 3121 |
. . . . . 6
⊢ (𝑥 = 𝑤 → (∀𝑦 ∈ (0[,]+∞)(𝑥 < 𝑦 → ∃𝑧 ∈ 𝐴 𝑧 < 𝑦) ↔ ∀𝑦 ∈ (0[,]+∞)(𝑤 < 𝑦 → ∃𝑧 ∈ 𝐴 𝑧 < 𝑦))) |
57 | 53, 56 | anbi12d 634 |
. . . . 5
⊢ (𝑥 = 𝑤 → ((∀𝑦 ∈ 𝐴 ¬ 𝑦 < 𝑥 ∧ ∀𝑦 ∈ (0[,]+∞)(𝑥 < 𝑦 → ∃𝑧 ∈ 𝐴 𝑧 < 𝑦)) ↔ (∀𝑦 ∈ 𝐴 ¬ 𝑦 < 𝑤 ∧ ∀𝑦 ∈ (0[,]+∞)(𝑤 < 𝑦 → ∃𝑧 ∈ 𝐴 𝑧 < 𝑦)))) |
58 | 57 | rspcev 3552 |
. . . 4
⊢ ((𝑤 ∈ (0[,]+∞) ∧
(∀𝑦 ∈ 𝐴 ¬ 𝑦 < 𝑤 ∧ ∀𝑦 ∈ (0[,]+∞)(𝑤 < 𝑦 → ∃𝑧 ∈ 𝐴 𝑧 < 𝑦))) → ∃𝑥 ∈ (0[,]+∞)(∀𝑦 ∈ 𝐴 ¬ 𝑦 < 𝑥 ∧ ∀𝑦 ∈ (0[,]+∞)(𝑥 < 𝑦 → ∃𝑧 ∈ 𝐴 𝑧 < 𝑦))) |
59 | 45, 50, 58 | syl2anc 587 |
. . 3
⊢ ((((𝐴 ⊆ (0[,]+∞) ∧
𝑤 ∈
ℝ*) ∧ (∀𝑦 ∈ 𝐴 ¬ 𝑦 < 𝑤 ∧ ∀𝑦 ∈ ℝ* (𝑤 < 𝑦 → ∃𝑧 ∈ 𝐴 𝑧 < 𝑦))) ∧ 0 ≤ 𝑤) → ∃𝑥 ∈ (0[,]+∞)(∀𝑦 ∈ 𝐴 ¬ 𝑦 < 𝑥 ∧ ∀𝑦 ∈ (0[,]+∞)(𝑥 < 𝑦 → ∃𝑧 ∈ 𝐴 𝑧 < 𝑦))) |
60 | | simplr 769 |
. . . 4
⊢ (((𝐴 ⊆ (0[,]+∞) ∧
𝑤 ∈
ℝ*) ∧ (∀𝑦 ∈ 𝐴 ¬ 𝑦 < 𝑤 ∧ ∀𝑦 ∈ ℝ* (𝑤 < 𝑦 → ∃𝑧 ∈ 𝐴 𝑧 < 𝑦))) → 𝑤 ∈ ℝ*) |
61 | 2 | a1i 11 |
. . . 4
⊢ (((𝐴 ⊆ (0[,]+∞) ∧
𝑤 ∈
ℝ*) ∧ (∀𝑦 ∈ 𝐴 ¬ 𝑦 < 𝑤 ∧ ∀𝑦 ∈ ℝ* (𝑤 < 𝑦 → ∃𝑧 ∈ 𝐴 𝑧 < 𝑦))) → 0 ∈
ℝ*) |
62 | | xrletri 12773 |
. . . 4
⊢ ((𝑤 ∈ ℝ*
∧ 0 ∈ ℝ*) → (𝑤 ≤ 0 ∨ 0 ≤ 𝑤)) |
63 | 60, 61, 62 | syl2anc 587 |
. . 3
⊢ (((𝐴 ⊆ (0[,]+∞) ∧
𝑤 ∈
ℝ*) ∧ (∀𝑦 ∈ 𝐴 ¬ 𝑦 < 𝑤 ∧ ∀𝑦 ∈ ℝ* (𝑤 < 𝑦 → ∃𝑧 ∈ 𝐴 𝑧 < 𝑦))) → (𝑤 ≤ 0 ∨ 0 ≤ 𝑤)) |
64 | 41, 59, 63 | mpjaodan 959 |
. 2
⊢ (((𝐴 ⊆ (0[,]+∞) ∧
𝑤 ∈
ℝ*) ∧ (∀𝑦 ∈ 𝐴 ¬ 𝑦 < 𝑤 ∧ ∀𝑦 ∈ ℝ* (𝑤 < 𝑦 → ∃𝑧 ∈ 𝐴 𝑧 < 𝑦))) → ∃𝑥 ∈ (0[,]+∞)(∀𝑦 ∈ 𝐴 ¬ 𝑦 < 𝑥 ∧ ∀𝑦 ∈ (0[,]+∞)(𝑥 < 𝑦 → ∃𝑧 ∈ 𝐴 𝑧 < 𝑦))) |
65 | | sstr 3926 |
. . . 4
⊢ ((𝐴 ⊆ (0[,]+∞) ∧
(0[,]+∞) ⊆ ℝ*) → 𝐴 ⊆
ℝ*) |
66 | 13, 65 | mpan2 691 |
. . 3
⊢ (𝐴 ⊆ (0[,]+∞) →
𝐴 ⊆
ℝ*) |
67 | | xrinfmss 12930 |
. . 3
⊢ (𝐴 ⊆ ℝ*
→ ∃𝑤 ∈
ℝ* (∀𝑦 ∈ 𝐴 ¬ 𝑦 < 𝑤 ∧ ∀𝑦 ∈ ℝ* (𝑤 < 𝑦 → ∃𝑧 ∈ 𝐴 𝑧 < 𝑦))) |
68 | 66, 67 | syl 17 |
. 2
⊢ (𝐴 ⊆ (0[,]+∞) →
∃𝑤 ∈
ℝ* (∀𝑦 ∈ 𝐴 ¬ 𝑦 < 𝑤 ∧ ∀𝑦 ∈ ℝ* (𝑤 < 𝑦 → ∃𝑧 ∈ 𝐴 𝑧 < 𝑦))) |
69 | 64, 68 | r19.29a 3218 |
1
⊢ (𝐴 ⊆ (0[,]+∞) →
∃𝑥 ∈
(0[,]+∞)(∀𝑦
∈ 𝐴 ¬ 𝑦 < 𝑥 ∧ ∀𝑦 ∈ (0[,]+∞)(𝑥 < 𝑦 → ∃𝑧 ∈ 𝐴 𝑧 < 𝑦))) |