Step | Hyp | Ref
| Expression |
1 | | lo1f 14097 |
. . . 4
⊢ (𝐹 ∈ ≤𝑂(1) →
𝐹:dom 𝐹⟶ℝ) |
2 | | lo1bdd 14099 |
. . . 4
⊢ ((𝐹 ∈ ≤𝑂(1) ∧
𝐹:dom 𝐹⟶ℝ) → ∃𝑥 ∈ ℝ ∃𝑚 ∈ ℝ ∀𝑦 ∈ dom 𝐹(𝑥 ≤ 𝑦 → (𝐹‘𝑦) ≤ 𝑚)) |
3 | 1, 2 | mpdan 699 |
. . 3
⊢ (𝐹 ∈ ≤𝑂(1) →
∃𝑥 ∈ ℝ
∃𝑚 ∈ ℝ
∀𝑦 ∈ dom 𝐹(𝑥 ≤ 𝑦 → (𝐹‘𝑦) ≤ 𝑚)) |
4 | | inss1 3795 |
. . . . . . 7
⊢ (dom
𝐹 ∩ 𝐴) ⊆ dom 𝐹 |
5 | | ssralv 3629 |
. . . . . . 7
⊢ ((dom
𝐹 ∩ 𝐴) ⊆ dom 𝐹 → (∀𝑦 ∈ dom 𝐹(𝑥 ≤ 𝑦 → (𝐹‘𝑦) ≤ 𝑚) → ∀𝑦 ∈ (dom 𝐹 ∩ 𝐴)(𝑥 ≤ 𝑦 → (𝐹‘𝑦) ≤ 𝑚))) |
6 | 4, 5 | ax-mp 5 |
. . . . . 6
⊢
(∀𝑦 ∈
dom 𝐹(𝑥 ≤ 𝑦 → (𝐹‘𝑦) ≤ 𝑚) → ∀𝑦 ∈ (dom 𝐹 ∩ 𝐴)(𝑥 ≤ 𝑦 → (𝐹‘𝑦) ≤ 𝑚)) |
7 | | inss2 3796 |
. . . . . . . . . . 11
⊢ (dom
𝐹 ∩ 𝐴) ⊆ 𝐴 |
8 | 7 | sseli 3564 |
. . . . . . . . . 10
⊢ (𝑦 ∈ (dom 𝐹 ∩ 𝐴) → 𝑦 ∈ 𝐴) |
9 | | fvres 6117 |
. . . . . . . . . 10
⊢ (𝑦 ∈ 𝐴 → ((𝐹 ↾ 𝐴)‘𝑦) = (𝐹‘𝑦)) |
10 | 8, 9 | syl 17 |
. . . . . . . . 9
⊢ (𝑦 ∈ (dom 𝐹 ∩ 𝐴) → ((𝐹 ↾ 𝐴)‘𝑦) = (𝐹‘𝑦)) |
11 | 10 | breq1d 4593 |
. . . . . . . 8
⊢ (𝑦 ∈ (dom 𝐹 ∩ 𝐴) → (((𝐹 ↾ 𝐴)‘𝑦) ≤ 𝑚 ↔ (𝐹‘𝑦) ≤ 𝑚)) |
12 | 11 | imbi2d 329 |
. . . . . . 7
⊢ (𝑦 ∈ (dom 𝐹 ∩ 𝐴) → ((𝑥 ≤ 𝑦 → ((𝐹 ↾ 𝐴)‘𝑦) ≤ 𝑚) ↔ (𝑥 ≤ 𝑦 → (𝐹‘𝑦) ≤ 𝑚))) |
13 | 12 | ralbiia 2962 |
. . . . . 6
⊢
(∀𝑦 ∈
(dom 𝐹 ∩ 𝐴)(𝑥 ≤ 𝑦 → ((𝐹 ↾ 𝐴)‘𝑦) ≤ 𝑚) ↔ ∀𝑦 ∈ (dom 𝐹 ∩ 𝐴)(𝑥 ≤ 𝑦 → (𝐹‘𝑦) ≤ 𝑚)) |
14 | 6, 13 | sylibr 223 |
. . . . 5
⊢
(∀𝑦 ∈
dom 𝐹(𝑥 ≤ 𝑦 → (𝐹‘𝑦) ≤ 𝑚) → ∀𝑦 ∈ (dom 𝐹 ∩ 𝐴)(𝑥 ≤ 𝑦 → ((𝐹 ↾ 𝐴)‘𝑦) ≤ 𝑚)) |
15 | 14 | reximi 2994 |
. . . 4
⊢
(∃𝑚 ∈
ℝ ∀𝑦 ∈
dom 𝐹(𝑥 ≤ 𝑦 → (𝐹‘𝑦) ≤ 𝑚) → ∃𝑚 ∈ ℝ ∀𝑦 ∈ (dom 𝐹 ∩ 𝐴)(𝑥 ≤ 𝑦 → ((𝐹 ↾ 𝐴)‘𝑦) ≤ 𝑚)) |
16 | 15 | reximi 2994 |
. . 3
⊢
(∃𝑥 ∈
ℝ ∃𝑚 ∈
ℝ ∀𝑦 ∈
dom 𝐹(𝑥 ≤ 𝑦 → (𝐹‘𝑦) ≤ 𝑚) → ∃𝑥 ∈ ℝ ∃𝑚 ∈ ℝ ∀𝑦 ∈ (dom 𝐹 ∩ 𝐴)(𝑥 ≤ 𝑦 → ((𝐹 ↾ 𝐴)‘𝑦) ≤ 𝑚)) |
17 | 3, 16 | syl 17 |
. 2
⊢ (𝐹 ∈ ≤𝑂(1) →
∃𝑥 ∈ ℝ
∃𝑚 ∈ ℝ
∀𝑦 ∈ (dom 𝐹 ∩ 𝐴)(𝑥 ≤ 𝑦 → ((𝐹 ↾ 𝐴)‘𝑦) ≤ 𝑚)) |
18 | | fssres 5983 |
. . . . 5
⊢ ((𝐹:dom 𝐹⟶ℝ ∧ (dom 𝐹 ∩ 𝐴) ⊆ dom 𝐹) → (𝐹 ↾ (dom 𝐹 ∩ 𝐴)):(dom 𝐹 ∩ 𝐴)⟶ℝ) |
19 | 1, 4, 18 | sylancl 693 |
. . . 4
⊢ (𝐹 ∈ ≤𝑂(1) →
(𝐹 ↾ (dom 𝐹 ∩ 𝐴)):(dom 𝐹 ∩ 𝐴)⟶ℝ) |
20 | | resres 5329 |
. . . . . 6
⊢ ((𝐹 ↾ dom 𝐹) ↾ 𝐴) = (𝐹 ↾ (dom 𝐹 ∩ 𝐴)) |
21 | | ffn 5958 |
. . . . . . . 8
⊢ (𝐹:dom 𝐹⟶ℝ → 𝐹 Fn dom 𝐹) |
22 | | fnresdm 5914 |
. . . . . . . 8
⊢ (𝐹 Fn dom 𝐹 → (𝐹 ↾ dom 𝐹) = 𝐹) |
23 | 1, 21, 22 | 3syl 18 |
. . . . . . 7
⊢ (𝐹 ∈ ≤𝑂(1) →
(𝐹 ↾ dom 𝐹) = 𝐹) |
24 | 23 | reseq1d 5316 |
. . . . . 6
⊢ (𝐹 ∈ ≤𝑂(1) →
((𝐹 ↾ dom 𝐹) ↾ 𝐴) = (𝐹 ↾ 𝐴)) |
25 | 20, 24 | syl5eqr 2658 |
. . . . 5
⊢ (𝐹 ∈ ≤𝑂(1) →
(𝐹 ↾ (dom 𝐹 ∩ 𝐴)) = (𝐹 ↾ 𝐴)) |
26 | 25 | feq1d 5943 |
. . . 4
⊢ (𝐹 ∈ ≤𝑂(1) →
((𝐹 ↾ (dom 𝐹 ∩ 𝐴)):(dom 𝐹 ∩ 𝐴)⟶ℝ ↔ (𝐹 ↾ 𝐴):(dom 𝐹 ∩ 𝐴)⟶ℝ)) |
27 | 19, 26 | mpbid 221 |
. . 3
⊢ (𝐹 ∈ ≤𝑂(1) →
(𝐹 ↾ 𝐴):(dom 𝐹 ∩ 𝐴)⟶ℝ) |
28 | | lo1dm 14098 |
. . . 4
⊢ (𝐹 ∈ ≤𝑂(1) →
dom 𝐹 ⊆
ℝ) |
29 | 4, 28 | syl5ss 3579 |
. . 3
⊢ (𝐹 ∈ ≤𝑂(1) →
(dom 𝐹 ∩ 𝐴) ⊆
ℝ) |
30 | | ello12 14095 |
. . 3
⊢ (((𝐹 ↾ 𝐴):(dom 𝐹 ∩ 𝐴)⟶ℝ ∧ (dom 𝐹 ∩ 𝐴) ⊆ ℝ) → ((𝐹 ↾ 𝐴) ∈ ≤𝑂(1) ↔
∃𝑥 ∈ ℝ
∃𝑚 ∈ ℝ
∀𝑦 ∈ (dom 𝐹 ∩ 𝐴)(𝑥 ≤ 𝑦 → ((𝐹 ↾ 𝐴)‘𝑦) ≤ 𝑚))) |
31 | 27, 29, 30 | syl2anc 691 |
. 2
⊢ (𝐹 ∈ ≤𝑂(1) →
((𝐹 ↾ 𝐴) ∈ ≤𝑂(1) ↔
∃𝑥 ∈ ℝ
∃𝑚 ∈ ℝ
∀𝑦 ∈ (dom 𝐹 ∩ 𝐴)(𝑥 ≤ 𝑦 → ((𝐹 ↾ 𝐴)‘𝑦) ≤ 𝑚))) |
32 | 17, 31 | mpbird 246 |
1
⊢ (𝐹 ∈ ≤𝑂(1) →
(𝐹 ↾ 𝐴) ∈
≤𝑂(1)) |