Step | Hyp | Ref
| Expression |
1 | | simpr 109 |
. . . 4
⊢ ((𝐴 ⊆ ℝ ∧ 𝐵 ∈ ℝ) → 𝐵 ∈
ℝ) |
2 | | pnfxr 7961 |
. . . 4
⊢ +∞
∈ ℝ* |
3 | | icossre 9900 |
. . . 4
⊢ ((𝐵 ∈ ℝ ∧ +∞
∈ ℝ*) → (𝐵[,)+∞) ⊆
ℝ) |
4 | 1, 2, 3 | sylancl 411 |
. . 3
⊢ ((𝐴 ⊆ ℝ ∧ 𝐵 ∈ ℝ) → (𝐵[,)+∞) ⊆
ℝ) |
5 | | ssrexv 3212 |
. . 3
⊢ ((𝐵[,)+∞) ⊆ ℝ
→ (∃𝑗 ∈
(𝐵[,)+∞)∀𝑘 ∈ 𝐴 (𝑗 ≤ 𝑘 → 𝜑) → ∃𝑗 ∈ ℝ ∀𝑘 ∈ 𝐴 (𝑗 ≤ 𝑘 → 𝜑))) |
6 | 4, 5 | syl 14 |
. 2
⊢ ((𝐴 ⊆ ℝ ∧ 𝐵 ∈ ℝ) →
(∃𝑗 ∈ (𝐵[,)+∞)∀𝑘 ∈ 𝐴 (𝑗 ≤ 𝑘 → 𝜑) → ∃𝑗 ∈ ℝ ∀𝑘 ∈ 𝐴 (𝑗 ≤ 𝑘 → 𝜑))) |
7 | | maxcl 11163 |
. . . . . . 7
⊢ ((𝐵 ∈ ℝ ∧ 𝑗 ∈ ℝ) →
sup({𝐵, 𝑗}, ℝ, < ) ∈
ℝ) |
8 | 7 | adantll 473 |
. . . . . 6
⊢ (((𝐴 ⊆ ℝ ∧ 𝐵 ∈ ℝ) ∧ 𝑗 ∈ ℝ) →
sup({𝐵, 𝑗}, ℝ, < ) ∈
ℝ) |
9 | | maxle1 11164 |
. . . . . . 7
⊢ ((𝐵 ∈ ℝ ∧ 𝑗 ∈ ℝ) → 𝐵 ≤ sup({𝐵, 𝑗}, ℝ, < )) |
10 | 9 | adantll 473 |
. . . . . 6
⊢ (((𝐴 ⊆ ℝ ∧ 𝐵 ∈ ℝ) ∧ 𝑗 ∈ ℝ) → 𝐵 ≤ sup({𝐵, 𝑗}, ℝ, < )) |
11 | | elicopnf 9915 |
. . . . . . 7
⊢ (𝐵 ∈ ℝ →
(sup({𝐵, 𝑗}, ℝ, < ) ∈ (𝐵[,)+∞) ↔ (sup({𝐵, 𝑗}, ℝ, < ) ∈ ℝ ∧ 𝐵 ≤ sup({𝐵, 𝑗}, ℝ, < )))) |
12 | 11 | ad2antlr 486 |
. . . . . 6
⊢ (((𝐴 ⊆ ℝ ∧ 𝐵 ∈ ℝ) ∧ 𝑗 ∈ ℝ) →
(sup({𝐵, 𝑗}, ℝ, < ) ∈ (𝐵[,)+∞) ↔ (sup({𝐵, 𝑗}, ℝ, < ) ∈ ℝ ∧ 𝐵 ≤ sup({𝐵, 𝑗}, ℝ, < )))) |
13 | 8, 10, 12 | mpbir2and 939 |
. . . . 5
⊢ (((𝐴 ⊆ ℝ ∧ 𝐵 ∈ ℝ) ∧ 𝑗 ∈ ℝ) →
sup({𝐵, 𝑗}, ℝ, < ) ∈ (𝐵[,)+∞)) |
14 | | simpllr 529 |
. . . . . . . . 9
⊢ ((((𝐴 ⊆ ℝ ∧ 𝐵 ∈ ℝ) ∧ 𝑗 ∈ ℝ) ∧ 𝑘 ∈ 𝐴) → 𝐵 ∈ ℝ) |
15 | | simplr 525 |
. . . . . . . . 9
⊢ ((((𝐴 ⊆ ℝ ∧ 𝐵 ∈ ℝ) ∧ 𝑗 ∈ ℝ) ∧ 𝑘 ∈ 𝐴) → 𝑗 ∈ ℝ) |
16 | | simpll 524 |
. . . . . . . . . 10
⊢ (((𝐴 ⊆ ℝ ∧ 𝐵 ∈ ℝ) ∧ 𝑗 ∈ ℝ) → 𝐴 ⊆
ℝ) |
17 | 16 | sselda 3147 |
. . . . . . . . 9
⊢ ((((𝐴 ⊆ ℝ ∧ 𝐵 ∈ ℝ) ∧ 𝑗 ∈ ℝ) ∧ 𝑘 ∈ 𝐴) → 𝑘 ∈ ℝ) |
18 | | maxleastb 11167 |
. . . . . . . . 9
⊢ ((𝐵 ∈ ℝ ∧ 𝑗 ∈ ℝ ∧ 𝑘 ∈ ℝ) →
(sup({𝐵, 𝑗}, ℝ, < ) ≤ 𝑘 ↔ (𝐵 ≤ 𝑘 ∧ 𝑗 ≤ 𝑘))) |
19 | 14, 15, 17, 18 | syl3anc 1233 |
. . . . . . . 8
⊢ ((((𝐴 ⊆ ℝ ∧ 𝐵 ∈ ℝ) ∧ 𝑗 ∈ ℝ) ∧ 𝑘 ∈ 𝐴) → (sup({𝐵, 𝑗}, ℝ, < ) ≤ 𝑘 ↔ (𝐵 ≤ 𝑘 ∧ 𝑗 ≤ 𝑘))) |
20 | | simpr 109 |
. . . . . . . 8
⊢ ((𝐵 ≤ 𝑘 ∧ 𝑗 ≤ 𝑘) → 𝑗 ≤ 𝑘) |
21 | 19, 20 | syl6bi 162 |
. . . . . . 7
⊢ ((((𝐴 ⊆ ℝ ∧ 𝐵 ∈ ℝ) ∧ 𝑗 ∈ ℝ) ∧ 𝑘 ∈ 𝐴) → (sup({𝐵, 𝑗}, ℝ, < ) ≤ 𝑘 → 𝑗 ≤ 𝑘)) |
22 | 21 | imim1d 75 |
. . . . . 6
⊢ ((((𝐴 ⊆ ℝ ∧ 𝐵 ∈ ℝ) ∧ 𝑗 ∈ ℝ) ∧ 𝑘 ∈ 𝐴) → ((𝑗 ≤ 𝑘 → 𝜑) → (sup({𝐵, 𝑗}, ℝ, < ) ≤ 𝑘 → 𝜑))) |
23 | 22 | ralimdva 2537 |
. . . . 5
⊢ (((𝐴 ⊆ ℝ ∧ 𝐵 ∈ ℝ) ∧ 𝑗 ∈ ℝ) →
(∀𝑘 ∈ 𝐴 (𝑗 ≤ 𝑘 → 𝜑) → ∀𝑘 ∈ 𝐴 (sup({𝐵, 𝑗}, ℝ, < ) ≤ 𝑘 → 𝜑))) |
24 | | breq1 3990 |
. . . . . . . 8
⊢ (𝑛 = sup({𝐵, 𝑗}, ℝ, < ) → (𝑛 ≤ 𝑘 ↔ sup({𝐵, 𝑗}, ℝ, < ) ≤ 𝑘)) |
25 | 24 | imbi1d 230 |
. . . . . . 7
⊢ (𝑛 = sup({𝐵, 𝑗}, ℝ, < ) → ((𝑛 ≤ 𝑘 → 𝜑) ↔ (sup({𝐵, 𝑗}, ℝ, < ) ≤ 𝑘 → 𝜑))) |
26 | 25 | ralbidv 2470 |
. . . . . 6
⊢ (𝑛 = sup({𝐵, 𝑗}, ℝ, < ) → (∀𝑘 ∈ 𝐴 (𝑛 ≤ 𝑘 → 𝜑) ↔ ∀𝑘 ∈ 𝐴 (sup({𝐵, 𝑗}, ℝ, < ) ≤ 𝑘 → 𝜑))) |
27 | 26 | rspcev 2834 |
. . . . 5
⊢
((sup({𝐵, 𝑗}, ℝ, < ) ∈ (𝐵[,)+∞) ∧ ∀𝑘 ∈ 𝐴 (sup({𝐵, 𝑗}, ℝ, < ) ≤ 𝑘 → 𝜑)) → ∃𝑛 ∈ (𝐵[,)+∞)∀𝑘 ∈ 𝐴 (𝑛 ≤ 𝑘 → 𝜑)) |
28 | 13, 23, 27 | syl6an 1427 |
. . . 4
⊢ (((𝐴 ⊆ ℝ ∧ 𝐵 ∈ ℝ) ∧ 𝑗 ∈ ℝ) →
(∀𝑘 ∈ 𝐴 (𝑗 ≤ 𝑘 → 𝜑) → ∃𝑛 ∈ (𝐵[,)+∞)∀𝑘 ∈ 𝐴 (𝑛 ≤ 𝑘 → 𝜑))) |
29 | 28 | rexlimdva 2587 |
. . 3
⊢ ((𝐴 ⊆ ℝ ∧ 𝐵 ∈ ℝ) →
(∃𝑗 ∈ ℝ
∀𝑘 ∈ 𝐴 (𝑗 ≤ 𝑘 → 𝜑) → ∃𝑛 ∈ (𝐵[,)+∞)∀𝑘 ∈ 𝐴 (𝑛 ≤ 𝑘 → 𝜑))) |
30 | | breq1 3990 |
. . . . . 6
⊢ (𝑛 = 𝑗 → (𝑛 ≤ 𝑘 ↔ 𝑗 ≤ 𝑘)) |
31 | 30 | imbi1d 230 |
. . . . 5
⊢ (𝑛 = 𝑗 → ((𝑛 ≤ 𝑘 → 𝜑) ↔ (𝑗 ≤ 𝑘 → 𝜑))) |
32 | 31 | ralbidv 2470 |
. . . 4
⊢ (𝑛 = 𝑗 → (∀𝑘 ∈ 𝐴 (𝑛 ≤ 𝑘 → 𝜑) ↔ ∀𝑘 ∈ 𝐴 (𝑗 ≤ 𝑘 → 𝜑))) |
33 | 32 | cbvrexv 2697 |
. . 3
⊢
(∃𝑛 ∈
(𝐵[,)+∞)∀𝑘 ∈ 𝐴 (𝑛 ≤ 𝑘 → 𝜑) ↔ ∃𝑗 ∈ (𝐵[,)+∞)∀𝑘 ∈ 𝐴 (𝑗 ≤ 𝑘 → 𝜑)) |
34 | 29, 33 | syl6ib 160 |
. 2
⊢ ((𝐴 ⊆ ℝ ∧ 𝐵 ∈ ℝ) →
(∃𝑗 ∈ ℝ
∀𝑘 ∈ 𝐴 (𝑗 ≤ 𝑘 → 𝜑) → ∃𝑗 ∈ (𝐵[,)+∞)∀𝑘 ∈ 𝐴 (𝑗 ≤ 𝑘 → 𝜑))) |
35 | 6, 34 | impbid 128 |
1
⊢ ((𝐴 ⊆ ℝ ∧ 𝐵 ∈ ℝ) →
(∃𝑗 ∈ (𝐵[,)+∞)∀𝑘 ∈ 𝐴 (𝑗 ≤ 𝑘 → 𝜑) ↔ ∃𝑗 ∈ ℝ ∀𝑘 ∈ 𝐴 (𝑗 ≤ 𝑘 → 𝜑))) |