Proof of Theorem ello12
Step | Hyp | Ref
| Expression |
1 | | reex 9906 |
. . . 4
⊢ ℝ
∈ V |
2 | | elpm2r 7761 |
. . . 4
⊢
(((ℝ ∈ V ∧ ℝ ∈ V) ∧ (𝐹:𝐴⟶ℝ ∧ 𝐴 ⊆ ℝ)) → 𝐹 ∈ (ℝ ↑pm
ℝ)) |
3 | 1, 1, 2 | mpanl12 714 |
. . 3
⊢ ((𝐹:𝐴⟶ℝ ∧ 𝐴 ⊆ ℝ) → 𝐹 ∈ (ℝ ↑pm
ℝ)) |
4 | | ello1 14094 |
. . . 4
⊢ (𝐹 ∈ ≤𝑂(1) ↔
(𝐹 ∈ (ℝ
↑pm ℝ) ∧ ∃𝑥 ∈ ℝ ∃𝑚 ∈ ℝ ∀𝑦 ∈ (dom 𝐹 ∩ (𝑥[,)+∞))(𝐹‘𝑦) ≤ 𝑚)) |
5 | 4 | baib 942 |
. . 3
⊢ (𝐹 ∈ (ℝ
↑pm ℝ) → (𝐹 ∈ ≤𝑂(1) ↔ ∃𝑥 ∈ ℝ ∃𝑚 ∈ ℝ ∀𝑦 ∈ (dom 𝐹 ∩ (𝑥[,)+∞))(𝐹‘𝑦) ≤ 𝑚)) |
6 | 3, 5 | syl 17 |
. 2
⊢ ((𝐹:𝐴⟶ℝ ∧ 𝐴 ⊆ ℝ) → (𝐹 ∈ ≤𝑂(1) ↔ ∃𝑥 ∈ ℝ ∃𝑚 ∈ ℝ ∀𝑦 ∈ (dom 𝐹 ∩ (𝑥[,)+∞))(𝐹‘𝑦) ≤ 𝑚)) |
7 | | elin 3758 |
. . . . . . . 8
⊢ (𝑦 ∈ (dom 𝐹 ∩ (𝑥[,)+∞)) ↔ (𝑦 ∈ dom 𝐹 ∧ 𝑦 ∈ (𝑥[,)+∞))) |
8 | | fdm 5964 |
. . . . . . . . . . . 12
⊢ (𝐹:𝐴⟶ℝ → dom 𝐹 = 𝐴) |
9 | 8 | ad3antrrr 762 |
. . . . . . . . . . 11
⊢ ((((𝐹:𝐴⟶ℝ ∧ 𝐴 ⊆ ℝ) ∧ 𝑥 ∈ ℝ) ∧ 𝑚 ∈ ℝ) → dom 𝐹 = 𝐴) |
10 | 9 | eleq2d 2673 |
. . . . . . . . . 10
⊢ ((((𝐹:𝐴⟶ℝ ∧ 𝐴 ⊆ ℝ) ∧ 𝑥 ∈ ℝ) ∧ 𝑚 ∈ ℝ) → (𝑦 ∈ dom 𝐹 ↔ 𝑦 ∈ 𝐴)) |
11 | 10 | anbi1d 737 |
. . . . . . . . 9
⊢ ((((𝐹:𝐴⟶ℝ ∧ 𝐴 ⊆ ℝ) ∧ 𝑥 ∈ ℝ) ∧ 𝑚 ∈ ℝ) → ((𝑦 ∈ dom 𝐹 ∧ 𝑦 ∈ (𝑥[,)+∞)) ↔ (𝑦 ∈ 𝐴 ∧ 𝑦 ∈ (𝑥[,)+∞)))) |
12 | | simpllr 795 |
. . . . . . . . . . . 12
⊢
(((((𝐹:𝐴⟶ℝ ∧ 𝐴 ⊆ ℝ) ∧ 𝑥 ∈ ℝ) ∧ 𝑚 ∈ ℝ) ∧ 𝑦 ∈ 𝐴) → 𝑥 ∈ ℝ) |
13 | | elicopnf 12140 |
. . . . . . . . . . . 12
⊢ (𝑥 ∈ ℝ → (𝑦 ∈ (𝑥[,)+∞) ↔ (𝑦 ∈ ℝ ∧ 𝑥 ≤ 𝑦))) |
14 | 12, 13 | syl 17 |
. . . . . . . . . . 11
⊢
(((((𝐹:𝐴⟶ℝ ∧ 𝐴 ⊆ ℝ) ∧ 𝑥 ∈ ℝ) ∧ 𝑚 ∈ ℝ) ∧ 𝑦 ∈ 𝐴) → (𝑦 ∈ (𝑥[,)+∞) ↔ (𝑦 ∈ ℝ ∧ 𝑥 ≤ 𝑦))) |
15 | | simpllr 795 |
. . . . . . . . . . . . 13
⊢ ((((𝐹:𝐴⟶ℝ ∧ 𝐴 ⊆ ℝ) ∧ 𝑥 ∈ ℝ) ∧ 𝑚 ∈ ℝ) → 𝐴 ⊆ ℝ) |
16 | 15 | sselda 3568 |
. . . . . . . . . . . 12
⊢
(((((𝐹:𝐴⟶ℝ ∧ 𝐴 ⊆ ℝ) ∧ 𝑥 ∈ ℝ) ∧ 𝑚 ∈ ℝ) ∧ 𝑦 ∈ 𝐴) → 𝑦 ∈ ℝ) |
17 | 16 | biantrurd 528 |
. . . . . . . . . . 11
⊢
(((((𝐹:𝐴⟶ℝ ∧ 𝐴 ⊆ ℝ) ∧ 𝑥 ∈ ℝ) ∧ 𝑚 ∈ ℝ) ∧ 𝑦 ∈ 𝐴) → (𝑥 ≤ 𝑦 ↔ (𝑦 ∈ ℝ ∧ 𝑥 ≤ 𝑦))) |
18 | 14, 17 | bitr4d 270 |
. . . . . . . . . 10
⊢
(((((𝐹:𝐴⟶ℝ ∧ 𝐴 ⊆ ℝ) ∧ 𝑥 ∈ ℝ) ∧ 𝑚 ∈ ℝ) ∧ 𝑦 ∈ 𝐴) → (𝑦 ∈ (𝑥[,)+∞) ↔ 𝑥 ≤ 𝑦)) |
19 | 18 | pm5.32da 671 |
. . . . . . . . 9
⊢ ((((𝐹:𝐴⟶ℝ ∧ 𝐴 ⊆ ℝ) ∧ 𝑥 ∈ ℝ) ∧ 𝑚 ∈ ℝ) → ((𝑦 ∈ 𝐴 ∧ 𝑦 ∈ (𝑥[,)+∞)) ↔ (𝑦 ∈ 𝐴 ∧ 𝑥 ≤ 𝑦))) |
20 | 11, 19 | bitrd 267 |
. . . . . . . 8
⊢ ((((𝐹:𝐴⟶ℝ ∧ 𝐴 ⊆ ℝ) ∧ 𝑥 ∈ ℝ) ∧ 𝑚 ∈ ℝ) → ((𝑦 ∈ dom 𝐹 ∧ 𝑦 ∈ (𝑥[,)+∞)) ↔ (𝑦 ∈ 𝐴 ∧ 𝑥 ≤ 𝑦))) |
21 | 7, 20 | syl5bb 271 |
. . . . . . 7
⊢ ((((𝐹:𝐴⟶ℝ ∧ 𝐴 ⊆ ℝ) ∧ 𝑥 ∈ ℝ) ∧ 𝑚 ∈ ℝ) → (𝑦 ∈ (dom 𝐹 ∩ (𝑥[,)+∞)) ↔ (𝑦 ∈ 𝐴 ∧ 𝑥 ≤ 𝑦))) |
22 | 21 | imbi1d 330 |
. . . . . 6
⊢ ((((𝐹:𝐴⟶ℝ ∧ 𝐴 ⊆ ℝ) ∧ 𝑥 ∈ ℝ) ∧ 𝑚 ∈ ℝ) → ((𝑦 ∈ (dom 𝐹 ∩ (𝑥[,)+∞)) → (𝐹‘𝑦) ≤ 𝑚) ↔ ((𝑦 ∈ 𝐴 ∧ 𝑥 ≤ 𝑦) → (𝐹‘𝑦) ≤ 𝑚))) |
23 | | impexp 461 |
. . . . . 6
⊢ (((𝑦 ∈ 𝐴 ∧ 𝑥 ≤ 𝑦) → (𝐹‘𝑦) ≤ 𝑚) ↔ (𝑦 ∈ 𝐴 → (𝑥 ≤ 𝑦 → (𝐹‘𝑦) ≤ 𝑚))) |
24 | 22, 23 | syl6bb 275 |
. . . . 5
⊢ ((((𝐹:𝐴⟶ℝ ∧ 𝐴 ⊆ ℝ) ∧ 𝑥 ∈ ℝ) ∧ 𝑚 ∈ ℝ) → ((𝑦 ∈ (dom 𝐹 ∩ (𝑥[,)+∞)) → (𝐹‘𝑦) ≤ 𝑚) ↔ (𝑦 ∈ 𝐴 → (𝑥 ≤ 𝑦 → (𝐹‘𝑦) ≤ 𝑚)))) |
25 | 24 | ralbidv2 2967 |
. . . 4
⊢ ((((𝐹:𝐴⟶ℝ ∧ 𝐴 ⊆ ℝ) ∧ 𝑥 ∈ ℝ) ∧ 𝑚 ∈ ℝ) → (∀𝑦 ∈ (dom 𝐹 ∩ (𝑥[,)+∞))(𝐹‘𝑦) ≤ 𝑚 ↔ ∀𝑦 ∈ 𝐴 (𝑥 ≤ 𝑦 → (𝐹‘𝑦) ≤ 𝑚))) |
26 | 25 | rexbidva 3031 |
. . 3
⊢ (((𝐹:𝐴⟶ℝ ∧ 𝐴 ⊆ ℝ) ∧ 𝑥 ∈ ℝ) → (∃𝑚 ∈ ℝ ∀𝑦 ∈ (dom 𝐹 ∩ (𝑥[,)+∞))(𝐹‘𝑦) ≤ 𝑚 ↔ ∃𝑚 ∈ ℝ ∀𝑦 ∈ 𝐴 (𝑥 ≤ 𝑦 → (𝐹‘𝑦) ≤ 𝑚))) |
27 | 26 | rexbidva 3031 |
. 2
⊢ ((𝐹:𝐴⟶ℝ ∧ 𝐴 ⊆ ℝ) → (∃𝑥 ∈ ℝ ∃𝑚 ∈ ℝ ∀𝑦 ∈ (dom 𝐹 ∩ (𝑥[,)+∞))(𝐹‘𝑦) ≤ 𝑚 ↔ ∃𝑥 ∈ ℝ ∃𝑚 ∈ ℝ ∀𝑦 ∈ 𝐴 (𝑥 ≤ 𝑦 → (𝐹‘𝑦) ≤ 𝑚))) |
28 | 6, 27 | bitrd 267 |
1
⊢ ((𝐹:𝐴⟶ℝ ∧ 𝐴 ⊆ ℝ) → (𝐹 ∈ ≤𝑂(1) ↔ ∃𝑥 ∈ ℝ ∃𝑚 ∈ ℝ ∀𝑦 ∈ 𝐴 (𝑥 ≤ 𝑦 → (𝐹‘𝑦) ≤ 𝑚))) |