Step | Hyp | Ref
| Expression |
1 | | lo1bdd2.4 |
. . 3
⊢ (𝜑 → (𝑥 ∈ 𝐴 ↦ 𝐵) ∈ ≤𝑂(1)) |
2 | | lo1bdd2.1 |
. . . 4
⊢ (𝜑 → 𝐴 ⊆ ℝ) |
3 | | lo1bdd2.3 |
. . . 4
⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴) → 𝐵 ∈ ℝ) |
4 | | lo1bdd2.2 |
. . . 4
⊢ (𝜑 → 𝐶 ∈ ℝ) |
5 | 2, 3, 4 | ello1mpt2 14970 |
. . 3
⊢ (𝜑 → ((𝑥 ∈ 𝐴 ↦ 𝐵) ∈ ≤𝑂(1) ↔
∃𝑦 ∈ (𝐶[,)+∞)∃𝑛 ∈ ℝ ∀𝑥 ∈ 𝐴 (𝑦 ≤ 𝑥 → 𝐵 ≤ 𝑛))) |
6 | 1, 5 | mpbid 235 |
. 2
⊢ (𝜑 → ∃𝑦 ∈ (𝐶[,)+∞)∃𝑛 ∈ ℝ ∀𝑥 ∈ 𝐴 (𝑦 ≤ 𝑥 → 𝐵 ≤ 𝑛)) |
7 | | elicopnf 12920 |
. . . . . . . . . . 11
⊢ (𝐶 ∈ ℝ → (𝑦 ∈ (𝐶[,)+∞) ↔ (𝑦 ∈ ℝ ∧ 𝐶 ≤ 𝑦))) |
8 | 4, 7 | syl 17 |
. . . . . . . . . 10
⊢ (𝜑 → (𝑦 ∈ (𝐶[,)+∞) ↔ (𝑦 ∈ ℝ ∧ 𝐶 ≤ 𝑦))) |
9 | 8 | biimpa 480 |
. . . . . . . . 9
⊢ ((𝜑 ∧ 𝑦 ∈ (𝐶[,)+∞)) → (𝑦 ∈ ℝ ∧ 𝐶 ≤ 𝑦)) |
10 | | lo1bdd2.5 |
. . . . . . . . 9
⊢ ((𝜑 ∧ (𝑦 ∈ ℝ ∧ 𝐶 ≤ 𝑦)) → 𝑀 ∈ ℝ) |
11 | 9, 10 | syldan 594 |
. . . . . . . 8
⊢ ((𝜑 ∧ 𝑦 ∈ (𝐶[,)+∞)) → 𝑀 ∈ ℝ) |
12 | 11 | ad2antrr 726 |
. . . . . . 7
⊢ ((((𝜑 ∧ 𝑦 ∈ (𝐶[,)+∞)) ∧ (𝑛 ∈ ℝ ∧ ∀𝑥 ∈ 𝐴 (𝑦 ≤ 𝑥 → 𝐵 ≤ 𝑛))) ∧ 𝑛 ≤ 𝑀) → 𝑀 ∈ ℝ) |
13 | | simplrl 777 |
. . . . . . 7
⊢ ((((𝜑 ∧ 𝑦 ∈ (𝐶[,)+∞)) ∧ (𝑛 ∈ ℝ ∧ ∀𝑥 ∈ 𝐴 (𝑦 ≤ 𝑥 → 𝐵 ≤ 𝑛))) ∧ ¬ 𝑛 ≤ 𝑀) → 𝑛 ∈ ℝ) |
14 | 12, 13 | ifclda 4450 |
. . . . . 6
⊢ (((𝜑 ∧ 𝑦 ∈ (𝐶[,)+∞)) ∧ (𝑛 ∈ ℝ ∧ ∀𝑥 ∈ 𝐴 (𝑦 ≤ 𝑥 → 𝐵 ≤ 𝑛))) → if(𝑛 ≤ 𝑀, 𝑀, 𝑛) ∈ ℝ) |
15 | 2 | ad2antrr 726 |
. . . . . . . . . . . 12
⊢ (((𝜑 ∧ 𝑦 ∈ (𝐶[,)+∞)) ∧ 𝑛 ∈ ℝ) → 𝐴 ⊆ ℝ) |
16 | 15 | sselda 3878 |
. . . . . . . . . . 11
⊢ ((((𝜑 ∧ 𝑦 ∈ (𝐶[,)+∞)) ∧ 𝑛 ∈ ℝ) ∧ 𝑥 ∈ 𝐴) → 𝑥 ∈ ℝ) |
17 | 9 | simpld 498 |
. . . . . . . . . . . 12
⊢ ((𝜑 ∧ 𝑦 ∈ (𝐶[,)+∞)) → 𝑦 ∈ ℝ) |
18 | 17 | ad2antrr 726 |
. . . . . . . . . . 11
⊢ ((((𝜑 ∧ 𝑦 ∈ (𝐶[,)+∞)) ∧ 𝑛 ∈ ℝ) ∧ 𝑥 ∈ 𝐴) → 𝑦 ∈ ℝ) |
19 | 16, 18 | ltnled 10866 |
. . . . . . . . . 10
⊢ ((((𝜑 ∧ 𝑦 ∈ (𝐶[,)+∞)) ∧ 𝑛 ∈ ℝ) ∧ 𝑥 ∈ 𝐴) → (𝑥 < 𝑦 ↔ ¬ 𝑦 ≤ 𝑥)) |
20 | | lo1bdd2.6 |
. . . . . . . . . . . . . . 15
⊢ (((𝜑 ∧ 𝑥 ∈ 𝐴) ∧ ((𝑦 ∈ ℝ ∧ 𝐶 ≤ 𝑦) ∧ 𝑥 < 𝑦)) → 𝐵 ≤ 𝑀) |
21 | 20 | expr 460 |
. . . . . . . . . . . . . 14
⊢ (((𝜑 ∧ 𝑥 ∈ 𝐴) ∧ (𝑦 ∈ ℝ ∧ 𝐶 ≤ 𝑦)) → (𝑥 < 𝑦 → 𝐵 ≤ 𝑀)) |
22 | 21 | an32s 652 |
. . . . . . . . . . . . 13
⊢ (((𝜑 ∧ (𝑦 ∈ ℝ ∧ 𝐶 ≤ 𝑦)) ∧ 𝑥 ∈ 𝐴) → (𝑥 < 𝑦 → 𝐵 ≤ 𝑀)) |
23 | 9, 22 | syldanl 605 |
. . . . . . . . . . . 12
⊢ (((𝜑 ∧ 𝑦 ∈ (𝐶[,)+∞)) ∧ 𝑥 ∈ 𝐴) → (𝑥 < 𝑦 → 𝐵 ≤ 𝑀)) |
24 | 23 | adantlr 715 |
. . . . . . . . . . 11
⊢ ((((𝜑 ∧ 𝑦 ∈ (𝐶[,)+∞)) ∧ 𝑛 ∈ ℝ) ∧ 𝑥 ∈ 𝐴) → (𝑥 < 𝑦 → 𝐵 ≤ 𝑀)) |
25 | | simplr 769 |
. . . . . . . . . . . . 13
⊢ ((((𝜑 ∧ 𝑦 ∈ (𝐶[,)+∞)) ∧ 𝑛 ∈ ℝ) ∧ 𝑥 ∈ 𝐴) → 𝑛 ∈ ℝ) |
26 | 11 | ad2antrr 726 |
. . . . . . . . . . . . 13
⊢ ((((𝜑 ∧ 𝑦 ∈ (𝐶[,)+∞)) ∧ 𝑛 ∈ ℝ) ∧ 𝑥 ∈ 𝐴) → 𝑀 ∈ ℝ) |
27 | | max2 12664 |
. . . . . . . . . . . . 13
⊢ ((𝑛 ∈ ℝ ∧ 𝑀 ∈ ℝ) → 𝑀 ≤ if(𝑛 ≤ 𝑀, 𝑀, 𝑛)) |
28 | 25, 26, 27 | syl2anc 587 |
. . . . . . . . . . . 12
⊢ ((((𝜑 ∧ 𝑦 ∈ (𝐶[,)+∞)) ∧ 𝑛 ∈ ℝ) ∧ 𝑥 ∈ 𝐴) → 𝑀 ≤ if(𝑛 ≤ 𝑀, 𝑀, 𝑛)) |
29 | 3 | ad4ant14 752 |
. . . . . . . . . . . . 13
⊢ ((((𝜑 ∧ 𝑦 ∈ (𝐶[,)+∞)) ∧ 𝑛 ∈ ℝ) ∧ 𝑥 ∈ 𝐴) → 𝐵 ∈ ℝ) |
30 | 11 | ad5ant12 756 |
. . . . . . . . . . . . . 14
⊢
(((((𝜑 ∧ 𝑦 ∈ (𝐶[,)+∞)) ∧ 𝑛 ∈ ℝ) ∧ 𝑥 ∈ 𝐴) ∧ 𝑛 ≤ 𝑀) → 𝑀 ∈ ℝ) |
31 | | simpllr 776 |
. . . . . . . . . . . . . 14
⊢
(((((𝜑 ∧ 𝑦 ∈ (𝐶[,)+∞)) ∧ 𝑛 ∈ ℝ) ∧ 𝑥 ∈ 𝐴) ∧ ¬ 𝑛 ≤ 𝑀) → 𝑛 ∈ ℝ) |
32 | 30, 31 | ifclda 4450 |
. . . . . . . . . . . . 13
⊢ ((((𝜑 ∧ 𝑦 ∈ (𝐶[,)+∞)) ∧ 𝑛 ∈ ℝ) ∧ 𝑥 ∈ 𝐴) → if(𝑛 ≤ 𝑀, 𝑀, 𝑛) ∈ ℝ) |
33 | | letr 10813 |
. . . . . . . . . . . . 13
⊢ ((𝐵 ∈ ℝ ∧ 𝑀 ∈ ℝ ∧ if(𝑛 ≤ 𝑀, 𝑀, 𝑛) ∈ ℝ) → ((𝐵 ≤ 𝑀 ∧ 𝑀 ≤ if(𝑛 ≤ 𝑀, 𝑀, 𝑛)) → 𝐵 ≤ if(𝑛 ≤ 𝑀, 𝑀, 𝑛))) |
34 | 29, 26, 32, 33 | syl3anc 1372 |
. . . . . . . . . . . 12
⊢ ((((𝜑 ∧ 𝑦 ∈ (𝐶[,)+∞)) ∧ 𝑛 ∈ ℝ) ∧ 𝑥 ∈ 𝐴) → ((𝐵 ≤ 𝑀 ∧ 𝑀 ≤ if(𝑛 ≤ 𝑀, 𝑀, 𝑛)) → 𝐵 ≤ if(𝑛 ≤ 𝑀, 𝑀, 𝑛))) |
35 | 28, 34 | mpan2d 694 |
. . . . . . . . . . 11
⊢ ((((𝜑 ∧ 𝑦 ∈ (𝐶[,)+∞)) ∧ 𝑛 ∈ ℝ) ∧ 𝑥 ∈ 𝐴) → (𝐵 ≤ 𝑀 → 𝐵 ≤ if(𝑛 ≤ 𝑀, 𝑀, 𝑛))) |
36 | 24, 35 | syld 47 |
. . . . . . . . . 10
⊢ ((((𝜑 ∧ 𝑦 ∈ (𝐶[,)+∞)) ∧ 𝑛 ∈ ℝ) ∧ 𝑥 ∈ 𝐴) → (𝑥 < 𝑦 → 𝐵 ≤ if(𝑛 ≤ 𝑀, 𝑀, 𝑛))) |
37 | 19, 36 | sylbird 263 |
. . . . . . . . 9
⊢ ((((𝜑 ∧ 𝑦 ∈ (𝐶[,)+∞)) ∧ 𝑛 ∈ ℝ) ∧ 𝑥 ∈ 𝐴) → (¬ 𝑦 ≤ 𝑥 → 𝐵 ≤ if(𝑛 ≤ 𝑀, 𝑀, 𝑛))) |
38 | | max1 12662 |
. . . . . . . . . . 11
⊢ ((𝑛 ∈ ℝ ∧ 𝑀 ∈ ℝ) → 𝑛 ≤ if(𝑛 ≤ 𝑀, 𝑀, 𝑛)) |
39 | 25, 26, 38 | syl2anc 587 |
. . . . . . . . . 10
⊢ ((((𝜑 ∧ 𝑦 ∈ (𝐶[,)+∞)) ∧ 𝑛 ∈ ℝ) ∧ 𝑥 ∈ 𝐴) → 𝑛 ≤ if(𝑛 ≤ 𝑀, 𝑀, 𝑛)) |
40 | | letr 10813 |
. . . . . . . . . . 11
⊢ ((𝐵 ∈ ℝ ∧ 𝑛 ∈ ℝ ∧ if(𝑛 ≤ 𝑀, 𝑀, 𝑛) ∈ ℝ) → ((𝐵 ≤ 𝑛 ∧ 𝑛 ≤ if(𝑛 ≤ 𝑀, 𝑀, 𝑛)) → 𝐵 ≤ if(𝑛 ≤ 𝑀, 𝑀, 𝑛))) |
41 | 29, 25, 32, 40 | syl3anc 1372 |
. . . . . . . . . 10
⊢ ((((𝜑 ∧ 𝑦 ∈ (𝐶[,)+∞)) ∧ 𝑛 ∈ ℝ) ∧ 𝑥 ∈ 𝐴) → ((𝐵 ≤ 𝑛 ∧ 𝑛 ≤ if(𝑛 ≤ 𝑀, 𝑀, 𝑛)) → 𝐵 ≤ if(𝑛 ≤ 𝑀, 𝑀, 𝑛))) |
42 | 39, 41 | mpan2d 694 |
. . . . . . . . 9
⊢ ((((𝜑 ∧ 𝑦 ∈ (𝐶[,)+∞)) ∧ 𝑛 ∈ ℝ) ∧ 𝑥 ∈ 𝐴) → (𝐵 ≤ 𝑛 → 𝐵 ≤ if(𝑛 ≤ 𝑀, 𝑀, 𝑛))) |
43 | 37, 42 | jad 190 |
. . . . . . . 8
⊢ ((((𝜑 ∧ 𝑦 ∈ (𝐶[,)+∞)) ∧ 𝑛 ∈ ℝ) ∧ 𝑥 ∈ 𝐴) → ((𝑦 ≤ 𝑥 → 𝐵 ≤ 𝑛) → 𝐵 ≤ if(𝑛 ≤ 𝑀, 𝑀, 𝑛))) |
44 | 43 | ralimdva 3091 |
. . . . . . 7
⊢ (((𝜑 ∧ 𝑦 ∈ (𝐶[,)+∞)) ∧ 𝑛 ∈ ℝ) → (∀𝑥 ∈ 𝐴 (𝑦 ≤ 𝑥 → 𝐵 ≤ 𝑛) → ∀𝑥 ∈ 𝐴 𝐵 ≤ if(𝑛 ≤ 𝑀, 𝑀, 𝑛))) |
45 | 44 | impr 458 |
. . . . . 6
⊢ (((𝜑 ∧ 𝑦 ∈ (𝐶[,)+∞)) ∧ (𝑛 ∈ ℝ ∧ ∀𝑥 ∈ 𝐴 (𝑦 ≤ 𝑥 → 𝐵 ≤ 𝑛))) → ∀𝑥 ∈ 𝐴 𝐵 ≤ if(𝑛 ≤ 𝑀, 𝑀, 𝑛)) |
46 | | brralrspcev 5091 |
. . . . . 6
⊢
((if(𝑛 ≤ 𝑀, 𝑀, 𝑛) ∈ ℝ ∧ ∀𝑥 ∈ 𝐴 𝐵 ≤ if(𝑛 ≤ 𝑀, 𝑀, 𝑛)) → ∃𝑚 ∈ ℝ ∀𝑥 ∈ 𝐴 𝐵 ≤ 𝑚) |
47 | 14, 45, 46 | syl2anc 587 |
. . . . 5
⊢ (((𝜑 ∧ 𝑦 ∈ (𝐶[,)+∞)) ∧ (𝑛 ∈ ℝ ∧ ∀𝑥 ∈ 𝐴 (𝑦 ≤ 𝑥 → 𝐵 ≤ 𝑛))) → ∃𝑚 ∈ ℝ ∀𝑥 ∈ 𝐴 𝐵 ≤ 𝑚) |
48 | 47 | expr 460 |
. . . 4
⊢ (((𝜑 ∧ 𝑦 ∈ (𝐶[,)+∞)) ∧ 𝑛 ∈ ℝ) → (∀𝑥 ∈ 𝐴 (𝑦 ≤ 𝑥 → 𝐵 ≤ 𝑛) → ∃𝑚 ∈ ℝ ∀𝑥 ∈ 𝐴 𝐵 ≤ 𝑚)) |
49 | 48 | rexlimdva 3194 |
. . 3
⊢ ((𝜑 ∧ 𝑦 ∈ (𝐶[,)+∞)) → (∃𝑛 ∈ ℝ ∀𝑥 ∈ 𝐴 (𝑦 ≤ 𝑥 → 𝐵 ≤ 𝑛) → ∃𝑚 ∈ ℝ ∀𝑥 ∈ 𝐴 𝐵 ≤ 𝑚)) |
50 | 49 | rexlimdva 3194 |
. 2
⊢ (𝜑 → (∃𝑦 ∈ (𝐶[,)+∞)∃𝑛 ∈ ℝ ∀𝑥 ∈ 𝐴 (𝑦 ≤ 𝑥 → 𝐵 ≤ 𝑛) → ∃𝑚 ∈ ℝ ∀𝑥 ∈ 𝐴 𝐵 ≤ 𝑚)) |
51 | 6, 50 | mpd 15 |
1
⊢ (𝜑 → ∃𝑚 ∈ ℝ ∀𝑥 ∈ 𝐴 𝐵 ≤ 𝑚) |