Step | Hyp | Ref
| Expression |
1 | | ssel2 3598 |
. . . . . . 7
⊢ ((𝐴 ⊆ (0[,]+∞) ∧
𝑦 ∈ 𝐴) → 𝑦 ∈ (0[,]+∞)) |
2 | | 0xr 10086 |
. . . . . . . . 9
⊢ 0 ∈
ℝ* |
3 | | pnfxr 10092 |
. . . . . . . . 9
⊢ +∞
∈ ℝ* |
4 | | iccgelb 12230 |
. . . . . . . . 9
⊢ ((0
∈ ℝ* ∧ +∞ ∈ ℝ* ∧
𝑦 ∈ (0[,]+∞))
→ 0 ≤ 𝑦) |
5 | 2, 3, 4 | mp3an12 1414 |
. . . . . . . 8
⊢ (𝑦 ∈ (0[,]+∞) → 0
≤ 𝑦) |
6 | | iccssxr 12256 |
. . . . . . . . . 10
⊢
(0[,]+∞) ⊆ ℝ* |
7 | 6 | sseli 3599 |
. . . . . . . . 9
⊢ (𝑦 ∈ (0[,]+∞) →
𝑦 ∈
ℝ*) |
8 | | xrlenlt 10103 |
. . . . . . . . 9
⊢ ((0
∈ ℝ* ∧ 𝑦 ∈ ℝ*) → (0 ≤
𝑦 ↔ ¬ 𝑦 < 0)) |
9 | 2, 7, 8 | sylancr 695 |
. . . . . . . 8
⊢ (𝑦 ∈ (0[,]+∞) → (0
≤ 𝑦 ↔ ¬ 𝑦 < 0)) |
10 | 5, 9 | mpbid 222 |
. . . . . . 7
⊢ (𝑦 ∈ (0[,]+∞) →
¬ 𝑦 <
0) |
11 | 1, 10 | syl 17 |
. . . . . 6
⊢ ((𝐴 ⊆ (0[,]+∞) ∧
𝑦 ∈ 𝐴) → ¬ 𝑦 < 0) |
12 | 11 | ralrimiva 2966 |
. . . . 5
⊢ (𝐴 ⊆ (0[,]+∞) →
∀𝑦 ∈ 𝐴 ¬ 𝑦 < 0) |
13 | 12 | ad3antrrr 766 |
. . . 4
⊢ ((((𝐴 ⊆ (0[,]+∞) ∧
𝑤 ∈
ℝ*) ∧ (∀𝑦 ∈ 𝐴 ¬ 𝑦 < 𝑤 ∧ ∀𝑦 ∈ ℝ* (𝑤 < 𝑦 → ∃𝑧 ∈ 𝐴 𝑧 < 𝑦))) ∧ 𝑤 ≤ 0) → ∀𝑦 ∈ 𝐴 ¬ 𝑦 < 0) |
14 | | ssralv 3666 |
. . . . . . . . . 10
⊢
((0[,]+∞) ⊆ ℝ* → (∀𝑦 ∈ ℝ*
(𝑤 < 𝑦 → ∃𝑧 ∈ 𝐴 𝑧 < 𝑦) → ∀𝑦 ∈ (0[,]+∞)(𝑤 < 𝑦 → ∃𝑧 ∈ 𝐴 𝑧 < 𝑦))) |
15 | 6, 14 | ax-mp 5 |
. . . . . . . . 9
⊢
(∀𝑦 ∈
ℝ* (𝑤 <
𝑦 → ∃𝑧 ∈ 𝐴 𝑧 < 𝑦) → ∀𝑦 ∈ (0[,]+∞)(𝑤 < 𝑦 → ∃𝑧 ∈ 𝐴 𝑧 < 𝑦)) |
16 | | simplll 798 |
. . . . . . . . . . . . 13
⊢ ((((𝑤 ∈ ℝ*
∧ 𝑤 ≤ 0) ∧ 𝑦 ∈ (0[,]+∞)) ∧ 0
< 𝑦) → 𝑤 ∈
ℝ*) |
17 | 2 | a1i 11 |
. . . . . . . . . . . . 13
⊢ ((((𝑤 ∈ ℝ*
∧ 𝑤 ≤ 0) ∧ 𝑦 ∈ (0[,]+∞)) ∧ 0
< 𝑦) → 0 ∈
ℝ*) |
18 | | simplr 792 |
. . . . . . . . . . . . . 14
⊢ ((((𝑤 ∈ ℝ*
∧ 𝑤 ≤ 0) ∧ 𝑦 ∈ (0[,]+∞)) ∧ 0
< 𝑦) → 𝑦 ∈
(0[,]+∞)) |
19 | 6, 18 | sseldi 3601 |
. . . . . . . . . . . . 13
⊢ ((((𝑤 ∈ ℝ*
∧ 𝑤 ≤ 0) ∧ 𝑦 ∈ (0[,]+∞)) ∧ 0
< 𝑦) → 𝑦 ∈
ℝ*) |
20 | | simpllr 799 |
. . . . . . . . . . . . 13
⊢ ((((𝑤 ∈ ℝ*
∧ 𝑤 ≤ 0) ∧ 𝑦 ∈ (0[,]+∞)) ∧ 0
< 𝑦) → 𝑤 ≤ 0) |
21 | | simpr 477 |
. . . . . . . . . . . . 13
⊢ ((((𝑤 ∈ ℝ*
∧ 𝑤 ≤ 0) ∧ 𝑦 ∈ (0[,]+∞)) ∧ 0
< 𝑦) → 0 < 𝑦) |
22 | 16, 17, 19, 20, 21 | xrlelttrd 11991 |
. . . . . . . . . . . 12
⊢ ((((𝑤 ∈ ℝ*
∧ 𝑤 ≤ 0) ∧ 𝑦 ∈ (0[,]+∞)) ∧ 0
< 𝑦) → 𝑤 < 𝑦) |
23 | 22 | ex 450 |
. . . . . . . . . . 11
⊢ (((𝑤 ∈ ℝ*
∧ 𝑤 ≤ 0) ∧ 𝑦 ∈ (0[,]+∞)) →
(0 < 𝑦 → 𝑤 < 𝑦)) |
24 | 23 | imim1d 82 |
. . . . . . . . . 10
⊢ (((𝑤 ∈ ℝ*
∧ 𝑤 ≤ 0) ∧ 𝑦 ∈ (0[,]+∞)) →
((𝑤 < 𝑦 → ∃𝑧 ∈ 𝐴 𝑧 < 𝑦) → (0 < 𝑦 → ∃𝑧 ∈ 𝐴 𝑧 < 𝑦))) |
25 | 24 | ralimdva 2962 |
. . . . . . . . 9
⊢ ((𝑤 ∈ ℝ*
∧ 𝑤 ≤ 0) →
(∀𝑦 ∈
(0[,]+∞)(𝑤 < 𝑦 → ∃𝑧 ∈ 𝐴 𝑧 < 𝑦) → ∀𝑦 ∈ (0[,]+∞)(0 < 𝑦 → ∃𝑧 ∈ 𝐴 𝑧 < 𝑦))) |
26 | 15, 25 | syl5 34 |
. . . . . . . 8
⊢ ((𝑤 ∈ ℝ*
∧ 𝑤 ≤ 0) →
(∀𝑦 ∈
ℝ* (𝑤 <
𝑦 → ∃𝑧 ∈ 𝐴 𝑧 < 𝑦) → ∀𝑦 ∈ (0[,]+∞)(0 < 𝑦 → ∃𝑧 ∈ 𝐴 𝑧 < 𝑦))) |
27 | 26 | adantll 750 |
. . . . . . 7
⊢ (((𝐴 ⊆ (0[,]+∞) ∧
𝑤 ∈
ℝ*) ∧ 𝑤 ≤ 0) → (∀𝑦 ∈ ℝ* (𝑤 < 𝑦 → ∃𝑧 ∈ 𝐴 𝑧 < 𝑦) → ∀𝑦 ∈ (0[,]+∞)(0 < 𝑦 → ∃𝑧 ∈ 𝐴 𝑧 < 𝑦))) |
28 | 27 | imp 445 |
. . . . . 6
⊢ ((((𝐴 ⊆ (0[,]+∞) ∧
𝑤 ∈
ℝ*) ∧ 𝑤 ≤ 0) ∧ ∀𝑦 ∈ ℝ* (𝑤 < 𝑦 → ∃𝑧 ∈ 𝐴 𝑧 < 𝑦)) → ∀𝑦 ∈ (0[,]+∞)(0 < 𝑦 → ∃𝑧 ∈ 𝐴 𝑧 < 𝑦)) |
29 | 28 | adantrl 752 |
. . . . 5
⊢ ((((𝐴 ⊆ (0[,]+∞) ∧
𝑤 ∈
ℝ*) ∧ 𝑤 ≤ 0) ∧ (∀𝑦 ∈ 𝐴 ¬ 𝑦 < 𝑤 ∧ ∀𝑦 ∈ ℝ* (𝑤 < 𝑦 → ∃𝑧 ∈ 𝐴 𝑧 < 𝑦))) → ∀𝑦 ∈ (0[,]+∞)(0 < 𝑦 → ∃𝑧 ∈ 𝐴 𝑧 < 𝑦)) |
30 | 29 | an32s 846 |
. . . 4
⊢ ((((𝐴 ⊆ (0[,]+∞) ∧
𝑤 ∈
ℝ*) ∧ (∀𝑦 ∈ 𝐴 ¬ 𝑦 < 𝑤 ∧ ∀𝑦 ∈ ℝ* (𝑤 < 𝑦 → ∃𝑧 ∈ 𝐴 𝑧 < 𝑦))) ∧ 𝑤 ≤ 0) → ∀𝑦 ∈ (0[,]+∞)(0 < 𝑦 → ∃𝑧 ∈ 𝐴 𝑧 < 𝑦)) |
31 | | 0e0iccpnf 12283 |
. . . . 5
⊢ 0 ∈
(0[,]+∞) |
32 | | breq2 4657 |
. . . . . . . . 9
⊢ (𝑥 = 0 → (𝑦 < 𝑥 ↔ 𝑦 < 0)) |
33 | 32 | notbid 308 |
. . . . . . . 8
⊢ (𝑥 = 0 → (¬ 𝑦 < 𝑥 ↔ ¬ 𝑦 < 0)) |
34 | 33 | ralbidv 2986 |
. . . . . . 7
⊢ (𝑥 = 0 → (∀𝑦 ∈ 𝐴 ¬ 𝑦 < 𝑥 ↔ ∀𝑦 ∈ 𝐴 ¬ 𝑦 < 0)) |
35 | | breq1 4656 |
. . . . . . . . 9
⊢ (𝑥 = 0 → (𝑥 < 𝑦 ↔ 0 < 𝑦)) |
36 | 35 | imbi1d 331 |
. . . . . . . 8
⊢ (𝑥 = 0 → ((𝑥 < 𝑦 → ∃𝑧 ∈ 𝐴 𝑧 < 𝑦) ↔ (0 < 𝑦 → ∃𝑧 ∈ 𝐴 𝑧 < 𝑦))) |
37 | 36 | ralbidv 2986 |
. . . . . . 7
⊢ (𝑥 = 0 → (∀𝑦 ∈ (0[,]+∞)(𝑥 < 𝑦 → ∃𝑧 ∈ 𝐴 𝑧 < 𝑦) ↔ ∀𝑦 ∈ (0[,]+∞)(0 < 𝑦 → ∃𝑧 ∈ 𝐴 𝑧 < 𝑦))) |
38 | 34, 37 | anbi12d 747 |
. . . . . 6
⊢ (𝑥 = 0 → ((∀𝑦 ∈ 𝐴 ¬ 𝑦 < 𝑥 ∧ ∀𝑦 ∈ (0[,]+∞)(𝑥 < 𝑦 → ∃𝑧 ∈ 𝐴 𝑧 < 𝑦)) ↔ (∀𝑦 ∈ 𝐴 ¬ 𝑦 < 0 ∧ ∀𝑦 ∈ (0[,]+∞)(0 < 𝑦 → ∃𝑧 ∈ 𝐴 𝑧 < 𝑦)))) |
39 | 38 | rspcev 3309 |
. . . . 5
⊢ ((0
∈ (0[,]+∞) ∧ (∀𝑦 ∈ 𝐴 ¬ 𝑦 < 0 ∧ ∀𝑦 ∈ (0[,]+∞)(0 < 𝑦 → ∃𝑧 ∈ 𝐴 𝑧 < 𝑦))) → ∃𝑥 ∈ (0[,]+∞)(∀𝑦 ∈ 𝐴 ¬ 𝑦 < 𝑥 ∧ ∀𝑦 ∈ (0[,]+∞)(𝑥 < 𝑦 → ∃𝑧 ∈ 𝐴 𝑧 < 𝑦))) |
40 | 31, 39 | mpan 706 |
. . . 4
⊢
((∀𝑦 ∈
𝐴 ¬ 𝑦 < 0 ∧ ∀𝑦 ∈ (0[,]+∞)(0 < 𝑦 → ∃𝑧 ∈ 𝐴 𝑧 < 𝑦)) → ∃𝑥 ∈ (0[,]+∞)(∀𝑦 ∈ 𝐴 ¬ 𝑦 < 𝑥 ∧ ∀𝑦 ∈ (0[,]+∞)(𝑥 < 𝑦 → ∃𝑧 ∈ 𝐴 𝑧 < 𝑦))) |
41 | 13, 30, 40 | syl2anc 693 |
. . 3
⊢ ((((𝐴 ⊆ (0[,]+∞) ∧
𝑤 ∈
ℝ*) ∧ (∀𝑦 ∈ 𝐴 ¬ 𝑦 < 𝑤 ∧ ∀𝑦 ∈ ℝ* (𝑤 < 𝑦 → ∃𝑧 ∈ 𝐴 𝑧 < 𝑦))) ∧ 𝑤 ≤ 0) → ∃𝑥 ∈ (0[,]+∞)(∀𝑦 ∈ 𝐴 ¬ 𝑦 < 𝑥 ∧ ∀𝑦 ∈ (0[,]+∞)(𝑥 < 𝑦 → ∃𝑧 ∈ 𝐴 𝑧 < 𝑦))) |
42 | | simpllr 799 |
. . . . 5
⊢ ((((𝐴 ⊆ (0[,]+∞) ∧
𝑤 ∈
ℝ*) ∧ (∀𝑦 ∈ 𝐴 ¬ 𝑦 < 𝑤 ∧ ∀𝑦 ∈ ℝ* (𝑤 < 𝑦 → ∃𝑧 ∈ 𝐴 𝑧 < 𝑦))) ∧ 0 ≤ 𝑤) → 𝑤 ∈ ℝ*) |
43 | | simpr 477 |
. . . . 5
⊢ ((((𝐴 ⊆ (0[,]+∞) ∧
𝑤 ∈
ℝ*) ∧ (∀𝑦 ∈ 𝐴 ¬ 𝑦 < 𝑤 ∧ ∀𝑦 ∈ ℝ* (𝑤 < 𝑦 → ∃𝑧 ∈ 𝐴 𝑧 < 𝑦))) ∧ 0 ≤ 𝑤) → 0 ≤ 𝑤) |
44 | | elxrge0 12281 |
. . . . 5
⊢ (𝑤 ∈ (0[,]+∞) ↔
(𝑤 ∈
ℝ* ∧ 0 ≤ 𝑤)) |
45 | 42, 43, 44 | sylanbrc 698 |
. . . 4
⊢ ((((𝐴 ⊆ (0[,]+∞) ∧
𝑤 ∈
ℝ*) ∧ (∀𝑦 ∈ 𝐴 ¬ 𝑦 < 𝑤 ∧ ∀𝑦 ∈ ℝ* (𝑤 < 𝑦 → ∃𝑧 ∈ 𝐴 𝑧 < 𝑦))) ∧ 0 ≤ 𝑤) → 𝑤 ∈ (0[,]+∞)) |
46 | 15 | a1i 11 |
. . . . . . . 8
⊢ (𝐴 ⊆ (0[,]+∞) →
(∀𝑦 ∈
ℝ* (𝑤 <
𝑦 → ∃𝑧 ∈ 𝐴 𝑧 < 𝑦) → ∀𝑦 ∈ (0[,]+∞)(𝑤 < 𝑦 → ∃𝑧 ∈ 𝐴 𝑧 < 𝑦))) |
47 | 46 | anim2d 589 |
. . . . . . 7
⊢ (𝐴 ⊆ (0[,]+∞) →
((∀𝑦 ∈ 𝐴 ¬ 𝑦 < 𝑤 ∧ ∀𝑦 ∈ ℝ* (𝑤 < 𝑦 → ∃𝑧 ∈ 𝐴 𝑧 < 𝑦)) → (∀𝑦 ∈ 𝐴 ¬ 𝑦 < 𝑤 ∧ ∀𝑦 ∈ (0[,]+∞)(𝑤 < 𝑦 → ∃𝑧 ∈ 𝐴 𝑧 < 𝑦)))) |
48 | 47 | adantr 481 |
. . . . . 6
⊢ ((𝐴 ⊆ (0[,]+∞) ∧
𝑤 ∈
ℝ*) → ((∀𝑦 ∈ 𝐴 ¬ 𝑦 < 𝑤 ∧ ∀𝑦 ∈ ℝ* (𝑤 < 𝑦 → ∃𝑧 ∈ 𝐴 𝑧 < 𝑦)) → (∀𝑦 ∈ 𝐴 ¬ 𝑦 < 𝑤 ∧ ∀𝑦 ∈ (0[,]+∞)(𝑤 < 𝑦 → ∃𝑧 ∈ 𝐴 𝑧 < 𝑦)))) |
49 | 48 | imp 445 |
. . . . 5
⊢ (((𝐴 ⊆ (0[,]+∞) ∧
𝑤 ∈
ℝ*) ∧ (∀𝑦 ∈ 𝐴 ¬ 𝑦 < 𝑤 ∧ ∀𝑦 ∈ ℝ* (𝑤 < 𝑦 → ∃𝑧 ∈ 𝐴 𝑧 < 𝑦))) → (∀𝑦 ∈ 𝐴 ¬ 𝑦 < 𝑤 ∧ ∀𝑦 ∈ (0[,]+∞)(𝑤 < 𝑦 → ∃𝑧 ∈ 𝐴 𝑧 < 𝑦))) |
50 | 49 | adantr 481 |
. . . 4
⊢ ((((𝐴 ⊆ (0[,]+∞) ∧
𝑤 ∈
ℝ*) ∧ (∀𝑦 ∈ 𝐴 ¬ 𝑦 < 𝑤 ∧ ∀𝑦 ∈ ℝ* (𝑤 < 𝑦 → ∃𝑧 ∈ 𝐴 𝑧 < 𝑦))) ∧ 0 ≤ 𝑤) → (∀𝑦 ∈ 𝐴 ¬ 𝑦 < 𝑤 ∧ ∀𝑦 ∈ (0[,]+∞)(𝑤 < 𝑦 → ∃𝑧 ∈ 𝐴 𝑧 < 𝑦))) |
51 | | breq2 4657 |
. . . . . . . 8
⊢ (𝑥 = 𝑤 → (𝑦 < 𝑥 ↔ 𝑦 < 𝑤)) |
52 | 51 | notbid 308 |
. . . . . . 7
⊢ (𝑥 = 𝑤 → (¬ 𝑦 < 𝑥 ↔ ¬ 𝑦 < 𝑤)) |
53 | 52 | ralbidv 2986 |
. . . . . 6
⊢ (𝑥 = 𝑤 → (∀𝑦 ∈ 𝐴 ¬ 𝑦 < 𝑥 ↔ ∀𝑦 ∈ 𝐴 ¬ 𝑦 < 𝑤)) |
54 | | breq1 4656 |
. . . . . . . 8
⊢ (𝑥 = 𝑤 → (𝑥 < 𝑦 ↔ 𝑤 < 𝑦)) |
55 | 54 | imbi1d 331 |
. . . . . . 7
⊢ (𝑥 = 𝑤 → ((𝑥 < 𝑦 → ∃𝑧 ∈ 𝐴 𝑧 < 𝑦) ↔ (𝑤 < 𝑦 → ∃𝑧 ∈ 𝐴 𝑧 < 𝑦))) |
56 | 55 | ralbidv 2986 |
. . . . . 6
⊢ (𝑥 = 𝑤 → (∀𝑦 ∈ (0[,]+∞)(𝑥 < 𝑦 → ∃𝑧 ∈ 𝐴 𝑧 < 𝑦) ↔ ∀𝑦 ∈ (0[,]+∞)(𝑤 < 𝑦 → ∃𝑧 ∈ 𝐴 𝑧 < 𝑦))) |
57 | 53, 56 | anbi12d 747 |
. . . . 5
⊢ (𝑥 = 𝑤 → ((∀𝑦 ∈ 𝐴 ¬ 𝑦 < 𝑥 ∧ ∀𝑦 ∈ (0[,]+∞)(𝑥 < 𝑦 → ∃𝑧 ∈ 𝐴 𝑧 < 𝑦)) ↔ (∀𝑦 ∈ 𝐴 ¬ 𝑦 < 𝑤 ∧ ∀𝑦 ∈ (0[,]+∞)(𝑤 < 𝑦 → ∃𝑧 ∈ 𝐴 𝑧 < 𝑦)))) |
58 | 57 | rspcev 3309 |
. . . 4
⊢ ((𝑤 ∈ (0[,]+∞) ∧
(∀𝑦 ∈ 𝐴 ¬ 𝑦 < 𝑤 ∧ ∀𝑦 ∈ (0[,]+∞)(𝑤 < 𝑦 → ∃𝑧 ∈ 𝐴 𝑧 < 𝑦))) → ∃𝑥 ∈ (0[,]+∞)(∀𝑦 ∈ 𝐴 ¬ 𝑦 < 𝑥 ∧ ∀𝑦 ∈ (0[,]+∞)(𝑥 < 𝑦 → ∃𝑧 ∈ 𝐴 𝑧 < 𝑦))) |
59 | 45, 50, 58 | syl2anc 693 |
. . 3
⊢ ((((𝐴 ⊆ (0[,]+∞) ∧
𝑤 ∈
ℝ*) ∧ (∀𝑦 ∈ 𝐴 ¬ 𝑦 < 𝑤 ∧ ∀𝑦 ∈ ℝ* (𝑤 < 𝑦 → ∃𝑧 ∈ 𝐴 𝑧 < 𝑦))) ∧ 0 ≤ 𝑤) → ∃𝑥 ∈ (0[,]+∞)(∀𝑦 ∈ 𝐴 ¬ 𝑦 < 𝑥 ∧ ∀𝑦 ∈ (0[,]+∞)(𝑥 < 𝑦 → ∃𝑧 ∈ 𝐴 𝑧 < 𝑦))) |
60 | | simplr 792 |
. . . 4
⊢ (((𝐴 ⊆ (0[,]+∞) ∧
𝑤 ∈
ℝ*) ∧ (∀𝑦 ∈ 𝐴 ¬ 𝑦 < 𝑤 ∧ ∀𝑦 ∈ ℝ* (𝑤 < 𝑦 → ∃𝑧 ∈ 𝐴 𝑧 < 𝑦))) → 𝑤 ∈ ℝ*) |
61 | 2 | a1i 11 |
. . . 4
⊢ (((𝐴 ⊆ (0[,]+∞) ∧
𝑤 ∈
ℝ*) ∧ (∀𝑦 ∈ 𝐴 ¬ 𝑦 < 𝑤 ∧ ∀𝑦 ∈ ℝ* (𝑤 < 𝑦 → ∃𝑧 ∈ 𝐴 𝑧 < 𝑦))) → 0 ∈
ℝ*) |
62 | | xrletri 11984 |
. . . 4
⊢ ((𝑤 ∈ ℝ*
∧ 0 ∈ ℝ*) → (𝑤 ≤ 0 ∨ 0 ≤ 𝑤)) |
63 | 60, 61, 62 | syl2anc 693 |
. . 3
⊢ (((𝐴 ⊆ (0[,]+∞) ∧
𝑤 ∈
ℝ*) ∧ (∀𝑦 ∈ 𝐴 ¬ 𝑦 < 𝑤 ∧ ∀𝑦 ∈ ℝ* (𝑤 < 𝑦 → ∃𝑧 ∈ 𝐴 𝑧 < 𝑦))) → (𝑤 ≤ 0 ∨ 0 ≤ 𝑤)) |
64 | 41, 59, 63 | mpjaodan 827 |
. 2
⊢ (((𝐴 ⊆ (0[,]+∞) ∧
𝑤 ∈
ℝ*) ∧ (∀𝑦 ∈ 𝐴 ¬ 𝑦 < 𝑤 ∧ ∀𝑦 ∈ ℝ* (𝑤 < 𝑦 → ∃𝑧 ∈ 𝐴 𝑧 < 𝑦))) → ∃𝑥 ∈ (0[,]+∞)(∀𝑦 ∈ 𝐴 ¬ 𝑦 < 𝑥 ∧ ∀𝑦 ∈ (0[,]+∞)(𝑥 < 𝑦 → ∃𝑧 ∈ 𝐴 𝑧 < 𝑦))) |
65 | | sstr 3611 |
. . . 4
⊢ ((𝐴 ⊆ (0[,]+∞) ∧
(0[,]+∞) ⊆ ℝ*) → 𝐴 ⊆
ℝ*) |
66 | 6, 65 | mpan2 707 |
. . 3
⊢ (𝐴 ⊆ (0[,]+∞) →
𝐴 ⊆
ℝ*) |
67 | | xrinfmss 12140 |
. . 3
⊢ (𝐴 ⊆ ℝ*
→ ∃𝑤 ∈
ℝ* (∀𝑦 ∈ 𝐴 ¬ 𝑦 < 𝑤 ∧ ∀𝑦 ∈ ℝ* (𝑤 < 𝑦 → ∃𝑧 ∈ 𝐴 𝑧 < 𝑦))) |
68 | 66, 67 | syl 17 |
. 2
⊢ (𝐴 ⊆ (0[,]+∞) →
∃𝑤 ∈
ℝ* (∀𝑦 ∈ 𝐴 ¬ 𝑦 < 𝑤 ∧ ∀𝑦 ∈ ℝ* (𝑤 < 𝑦 → ∃𝑧 ∈ 𝐴 𝑧 < 𝑦))) |
69 | 64, 68 | r19.29a 3078 |
1
⊢ (𝐴 ⊆ (0[,]+∞) →
∃𝑥 ∈
(0[,]+∞)(∀𝑦
∈ 𝐴 ¬ 𝑦 < 𝑥 ∧ ∀𝑦 ∈ (0[,]+∞)(𝑥 < 𝑦 → ∃𝑧 ∈ 𝐴 𝑧 < 𝑦))) |