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 14101 |
. . 3
⊢ (𝜑 → ((𝑥 ∈ 𝐴 ↦ 𝐵) ∈ ≤𝑂(1) ↔
∃𝑦 ∈ (𝐶[,)+∞)∃𝑛 ∈ ℝ ∀𝑥 ∈ 𝐴 (𝑦 ≤ 𝑥 → 𝐵 ≤ 𝑛))) |
6 | 1, 5 | mpbid 221 |
. 2
⊢ (𝜑 → ∃𝑦 ∈ (𝐶[,)+∞)∃𝑛 ∈ ℝ ∀𝑥 ∈ 𝐴 (𝑦 ≤ 𝑥 → 𝐵 ≤ 𝑛)) |
7 | | elicopnf 12140 |
. . . . . . . . . . 11
⊢ (𝐶 ∈ ℝ → (𝑦 ∈ (𝐶[,)+∞) ↔ (𝑦 ∈ ℝ ∧ 𝐶 ≤ 𝑦))) |
8 | 4, 7 | syl 17 |
. . . . . . . . . 10
⊢ (𝜑 → (𝑦 ∈ (𝐶[,)+∞) ↔ (𝑦 ∈ ℝ ∧ 𝐶 ≤ 𝑦))) |
9 | 8 | biimpa 500 |
. . . . . . . . 9
⊢ ((𝜑 ∧ 𝑦 ∈ (𝐶[,)+∞)) → (𝑦 ∈ ℝ ∧ 𝐶 ≤ 𝑦)) |
10 | | lo1bdd2.5 |
. . . . . . . . 9
⊢ ((𝜑 ∧ (𝑦 ∈ ℝ ∧ 𝐶 ≤ 𝑦)) → 𝑀 ∈ ℝ) |
11 | 9, 10 | syldan 486 |
. . . . . . . 8
⊢ ((𝜑 ∧ 𝑦 ∈ (𝐶[,)+∞)) → 𝑀 ∈ ℝ) |
12 | 11 | ad2antrr 758 |
. . . . . . 7
⊢ ((((𝜑 ∧ 𝑦 ∈ (𝐶[,)+∞)) ∧ (𝑛 ∈ ℝ ∧ ∀𝑥 ∈ 𝐴 (𝑦 ≤ 𝑥 → 𝐵 ≤ 𝑛))) ∧ 𝑛 ≤ 𝑀) → 𝑀 ∈ ℝ) |
13 | | simplrl 796 |
. . . . . . 7
⊢ ((((𝜑 ∧ 𝑦 ∈ (𝐶[,)+∞)) ∧ (𝑛 ∈ ℝ ∧ ∀𝑥 ∈ 𝐴 (𝑦 ≤ 𝑥 → 𝐵 ≤ 𝑛))) ∧ ¬ 𝑛 ≤ 𝑀) → 𝑛 ∈ ℝ) |
14 | 12, 13 | ifclda 4070 |
. . . . . 6
⊢ (((𝜑 ∧ 𝑦 ∈ (𝐶[,)+∞)) ∧ (𝑛 ∈ ℝ ∧ ∀𝑥 ∈ 𝐴 (𝑦 ≤ 𝑥 → 𝐵 ≤ 𝑛))) → if(𝑛 ≤ 𝑀, 𝑀, 𝑛) ∈ ℝ) |
15 | 2 | ad2antrr 758 |
. . . . . . . . . . . 12
⊢ (((𝜑 ∧ 𝑦 ∈ (𝐶[,)+∞)) ∧ 𝑛 ∈ ℝ) → 𝐴 ⊆ ℝ) |
16 | 15 | sselda 3568 |
. . . . . . . . . . 11
⊢ ((((𝜑 ∧ 𝑦 ∈ (𝐶[,)+∞)) ∧ 𝑛 ∈ ℝ) ∧ 𝑥 ∈ 𝐴) → 𝑥 ∈ ℝ) |
17 | 9 | simpld 474 |
. . . . . . . . . . . 12
⊢ ((𝜑 ∧ 𝑦 ∈ (𝐶[,)+∞)) → 𝑦 ∈ ℝ) |
18 | 17 | ad2antrr 758 |
. . . . . . . . . . 11
⊢ ((((𝜑 ∧ 𝑦 ∈ (𝐶[,)+∞)) ∧ 𝑛 ∈ ℝ) ∧ 𝑥 ∈ 𝐴) → 𝑦 ∈ ℝ) |
19 | 16, 18 | ltnled 10063 |
. . . . . . . . . 10
⊢ ((((𝜑 ∧ 𝑦 ∈ (𝐶[,)+∞)) ∧ 𝑛 ∈ ℝ) ∧ 𝑥 ∈ 𝐴) → (𝑥 < 𝑦 ↔ ¬ 𝑦 ≤ 𝑥)) |
20 | | lo1bdd2.6 |
. . . . . . . . . . . . . . . . 17
⊢ (((𝜑 ∧ 𝑥 ∈ 𝐴) ∧ ((𝑦 ∈ ℝ ∧ 𝐶 ≤ 𝑦) ∧ 𝑥 < 𝑦)) → 𝐵 ≤ 𝑀) |
21 | 20 | expr 641 |
. . . . . . . . . . . . . . . 16
⊢ (((𝜑 ∧ 𝑥 ∈ 𝐴) ∧ (𝑦 ∈ ℝ ∧ 𝐶 ≤ 𝑦)) → (𝑥 < 𝑦 → 𝐵 ≤ 𝑀)) |
22 | 21 | an32s 842 |
. . . . . . . . . . . . . . 15
⊢ (((𝜑 ∧ (𝑦 ∈ ℝ ∧ 𝐶 ≤ 𝑦)) ∧ 𝑥 ∈ 𝐴) → (𝑥 < 𝑦 → 𝐵 ≤ 𝑀)) |
23 | 22 | ex 449 |
. . . . . . . . . . . . . 14
⊢ ((𝜑 ∧ (𝑦 ∈ ℝ ∧ 𝐶 ≤ 𝑦)) → (𝑥 ∈ 𝐴 → (𝑥 < 𝑦 → 𝐵 ≤ 𝑀))) |
24 | 9, 23 | syldan 486 |
. . . . . . . . . . . . 13
⊢ ((𝜑 ∧ 𝑦 ∈ (𝐶[,)+∞)) → (𝑥 ∈ 𝐴 → (𝑥 < 𝑦 → 𝐵 ≤ 𝑀))) |
25 | 24 | imp 444 |
. . . . . . . . . . . 12
⊢ (((𝜑 ∧ 𝑦 ∈ (𝐶[,)+∞)) ∧ 𝑥 ∈ 𝐴) → (𝑥 < 𝑦 → 𝐵 ≤ 𝑀)) |
26 | 25 | adantlr 747 |
. . . . . . . . . . 11
⊢ ((((𝜑 ∧ 𝑦 ∈ (𝐶[,)+∞)) ∧ 𝑛 ∈ ℝ) ∧ 𝑥 ∈ 𝐴) → (𝑥 < 𝑦 → 𝐵 ≤ 𝑀)) |
27 | | simplr 788 |
. . . . . . . . . . . . 13
⊢ ((((𝜑 ∧ 𝑦 ∈ (𝐶[,)+∞)) ∧ 𝑛 ∈ ℝ) ∧ 𝑥 ∈ 𝐴) → 𝑛 ∈ ℝ) |
28 | 11 | ad2antrr 758 |
. . . . . . . . . . . . 13
⊢ ((((𝜑 ∧ 𝑦 ∈ (𝐶[,)+∞)) ∧ 𝑛 ∈ ℝ) ∧ 𝑥 ∈ 𝐴) → 𝑀 ∈ ℝ) |
29 | | max2 11892 |
. . . . . . . . . . . . 13
⊢ ((𝑛 ∈ ℝ ∧ 𝑀 ∈ ℝ) → 𝑀 ≤ if(𝑛 ≤ 𝑀, 𝑀, 𝑛)) |
30 | 27, 28, 29 | syl2anc 691 |
. . . . . . . . . . . 12
⊢ ((((𝜑 ∧ 𝑦 ∈ (𝐶[,)+∞)) ∧ 𝑛 ∈ ℝ) ∧ 𝑥 ∈ 𝐴) → 𝑀 ≤ if(𝑛 ≤ 𝑀, 𝑀, 𝑛)) |
31 | | simpll 786 |
. . . . . . . . . . . . . 14
⊢ (((𝜑 ∧ 𝑦 ∈ (𝐶[,)+∞)) ∧ 𝑛 ∈ ℝ) → 𝜑) |
32 | 31, 3 | sylan 487 |
. . . . . . . . . . . . 13
⊢ ((((𝜑 ∧ 𝑦 ∈ (𝐶[,)+∞)) ∧ 𝑛 ∈ ℝ) ∧ 𝑥 ∈ 𝐴) → 𝐵 ∈ ℝ) |
33 | 11 | ad3antrrr 762 |
. . . . . . . . . . . . . 14
⊢
(((((𝜑 ∧ 𝑦 ∈ (𝐶[,)+∞)) ∧ 𝑛 ∈ ℝ) ∧ 𝑥 ∈ 𝐴) ∧ 𝑛 ≤ 𝑀) → 𝑀 ∈ ℝ) |
34 | | simpllr 795 |
. . . . . . . . . . . . . 14
⊢
(((((𝜑 ∧ 𝑦 ∈ (𝐶[,)+∞)) ∧ 𝑛 ∈ ℝ) ∧ 𝑥 ∈ 𝐴) ∧ ¬ 𝑛 ≤ 𝑀) → 𝑛 ∈ ℝ) |
35 | 33, 34 | ifclda 4070 |
. . . . . . . . . . . . 13
⊢ ((((𝜑 ∧ 𝑦 ∈ (𝐶[,)+∞)) ∧ 𝑛 ∈ ℝ) ∧ 𝑥 ∈ 𝐴) → if(𝑛 ≤ 𝑀, 𝑀, 𝑛) ∈ ℝ) |
36 | | letr 10010 |
. . . . . . . . . . . . 13
⊢ ((𝐵 ∈ ℝ ∧ 𝑀 ∈ ℝ ∧ if(𝑛 ≤ 𝑀, 𝑀, 𝑛) ∈ ℝ) → ((𝐵 ≤ 𝑀 ∧ 𝑀 ≤ if(𝑛 ≤ 𝑀, 𝑀, 𝑛)) → 𝐵 ≤ if(𝑛 ≤ 𝑀, 𝑀, 𝑛))) |
37 | 32, 28, 35, 36 | syl3anc 1318 |
. . . . . . . . . . . 12
⊢ ((((𝜑 ∧ 𝑦 ∈ (𝐶[,)+∞)) ∧ 𝑛 ∈ ℝ) ∧ 𝑥 ∈ 𝐴) → ((𝐵 ≤ 𝑀 ∧ 𝑀 ≤ if(𝑛 ≤ 𝑀, 𝑀, 𝑛)) → 𝐵 ≤ if(𝑛 ≤ 𝑀, 𝑀, 𝑛))) |
38 | 30, 37 | mpan2d 706 |
. . . . . . . . . . 11
⊢ ((((𝜑 ∧ 𝑦 ∈ (𝐶[,)+∞)) ∧ 𝑛 ∈ ℝ) ∧ 𝑥 ∈ 𝐴) → (𝐵 ≤ 𝑀 → 𝐵 ≤ if(𝑛 ≤ 𝑀, 𝑀, 𝑛))) |
39 | 26, 38 | syld 46 |
. . . . . . . . . 10
⊢ ((((𝜑 ∧ 𝑦 ∈ (𝐶[,)+∞)) ∧ 𝑛 ∈ ℝ) ∧ 𝑥 ∈ 𝐴) → (𝑥 < 𝑦 → 𝐵 ≤ if(𝑛 ≤ 𝑀, 𝑀, 𝑛))) |
40 | 19, 39 | sylbird 249 |
. . . . . . . . 9
⊢ ((((𝜑 ∧ 𝑦 ∈ (𝐶[,)+∞)) ∧ 𝑛 ∈ ℝ) ∧ 𝑥 ∈ 𝐴) → (¬ 𝑦 ≤ 𝑥 → 𝐵 ≤ if(𝑛 ≤ 𝑀, 𝑀, 𝑛))) |
41 | | max1 11890 |
. . . . . . . . . . 11
⊢ ((𝑛 ∈ ℝ ∧ 𝑀 ∈ ℝ) → 𝑛 ≤ if(𝑛 ≤ 𝑀, 𝑀, 𝑛)) |
42 | 27, 28, 41 | syl2anc 691 |
. . . . . . . . . 10
⊢ ((((𝜑 ∧ 𝑦 ∈ (𝐶[,)+∞)) ∧ 𝑛 ∈ ℝ) ∧ 𝑥 ∈ 𝐴) → 𝑛 ≤ if(𝑛 ≤ 𝑀, 𝑀, 𝑛)) |
43 | | letr 10010 |
. . . . . . . . . . 11
⊢ ((𝐵 ∈ ℝ ∧ 𝑛 ∈ ℝ ∧ if(𝑛 ≤ 𝑀, 𝑀, 𝑛) ∈ ℝ) → ((𝐵 ≤ 𝑛 ∧ 𝑛 ≤ if(𝑛 ≤ 𝑀, 𝑀, 𝑛)) → 𝐵 ≤ if(𝑛 ≤ 𝑀, 𝑀, 𝑛))) |
44 | 32, 27, 35, 43 | syl3anc 1318 |
. . . . . . . . . 10
⊢ ((((𝜑 ∧ 𝑦 ∈ (𝐶[,)+∞)) ∧ 𝑛 ∈ ℝ) ∧ 𝑥 ∈ 𝐴) → ((𝐵 ≤ 𝑛 ∧ 𝑛 ≤ if(𝑛 ≤ 𝑀, 𝑀, 𝑛)) → 𝐵 ≤ if(𝑛 ≤ 𝑀, 𝑀, 𝑛))) |
45 | 42, 44 | mpan2d 706 |
. . . . . . . . 9
⊢ ((((𝜑 ∧ 𝑦 ∈ (𝐶[,)+∞)) ∧ 𝑛 ∈ ℝ) ∧ 𝑥 ∈ 𝐴) → (𝐵 ≤ 𝑛 → 𝐵 ≤ if(𝑛 ≤ 𝑀, 𝑀, 𝑛))) |
46 | 40, 45 | jad 173 |
. . . . . . . 8
⊢ ((((𝜑 ∧ 𝑦 ∈ (𝐶[,)+∞)) ∧ 𝑛 ∈ ℝ) ∧ 𝑥 ∈ 𝐴) → ((𝑦 ≤ 𝑥 → 𝐵 ≤ 𝑛) → 𝐵 ≤ if(𝑛 ≤ 𝑀, 𝑀, 𝑛))) |
47 | 46 | ralimdva 2945 |
. . . . . . 7
⊢ (((𝜑 ∧ 𝑦 ∈ (𝐶[,)+∞)) ∧ 𝑛 ∈ ℝ) → (∀𝑥 ∈ 𝐴 (𝑦 ≤ 𝑥 → 𝐵 ≤ 𝑛) → ∀𝑥 ∈ 𝐴 𝐵 ≤ if(𝑛 ≤ 𝑀, 𝑀, 𝑛))) |
48 | 47 | impr 647 |
. . . . . 6
⊢ (((𝜑 ∧ 𝑦 ∈ (𝐶[,)+∞)) ∧ (𝑛 ∈ ℝ ∧ ∀𝑥 ∈ 𝐴 (𝑦 ≤ 𝑥 → 𝐵 ≤ 𝑛))) → ∀𝑥 ∈ 𝐴 𝐵 ≤ if(𝑛 ≤ 𝑀, 𝑀, 𝑛)) |
49 | | breq2 4587 |
. . . . . . . 8
⊢ (𝑚 = if(𝑛 ≤ 𝑀, 𝑀, 𝑛) → (𝐵 ≤ 𝑚 ↔ 𝐵 ≤ if(𝑛 ≤ 𝑀, 𝑀, 𝑛))) |
50 | 49 | ralbidv 2969 |
. . . . . . 7
⊢ (𝑚 = if(𝑛 ≤ 𝑀, 𝑀, 𝑛) → (∀𝑥 ∈ 𝐴 𝐵 ≤ 𝑚 ↔ ∀𝑥 ∈ 𝐴 𝐵 ≤ if(𝑛 ≤ 𝑀, 𝑀, 𝑛))) |
51 | 50 | rspcev 3282 |
. . . . . 6
⊢
((if(𝑛 ≤ 𝑀, 𝑀, 𝑛) ∈ ℝ ∧ ∀𝑥 ∈ 𝐴 𝐵 ≤ if(𝑛 ≤ 𝑀, 𝑀, 𝑛)) → ∃𝑚 ∈ ℝ ∀𝑥 ∈ 𝐴 𝐵 ≤ 𝑚) |
52 | 14, 48, 51 | syl2anc 691 |
. . . . 5
⊢ (((𝜑 ∧ 𝑦 ∈ (𝐶[,)+∞)) ∧ (𝑛 ∈ ℝ ∧ ∀𝑥 ∈ 𝐴 (𝑦 ≤ 𝑥 → 𝐵 ≤ 𝑛))) → ∃𝑚 ∈ ℝ ∀𝑥 ∈ 𝐴 𝐵 ≤ 𝑚) |
53 | 52 | expr 641 |
. . . 4
⊢ (((𝜑 ∧ 𝑦 ∈ (𝐶[,)+∞)) ∧ 𝑛 ∈ ℝ) → (∀𝑥 ∈ 𝐴 (𝑦 ≤ 𝑥 → 𝐵 ≤ 𝑛) → ∃𝑚 ∈ ℝ ∀𝑥 ∈ 𝐴 𝐵 ≤ 𝑚)) |
54 | 53 | rexlimdva 3013 |
. . 3
⊢ ((𝜑 ∧ 𝑦 ∈ (𝐶[,)+∞)) → (∃𝑛 ∈ ℝ ∀𝑥 ∈ 𝐴 (𝑦 ≤ 𝑥 → 𝐵 ≤ 𝑛) → ∃𝑚 ∈ ℝ ∀𝑥 ∈ 𝐴 𝐵 ≤ 𝑚)) |
55 | 54 | rexlimdva 3013 |
. 2
⊢ (𝜑 → (∃𝑦 ∈ (𝐶[,)+∞)∃𝑛 ∈ ℝ ∀𝑥 ∈ 𝐴 (𝑦 ≤ 𝑥 → 𝐵 ≤ 𝑛) → ∃𝑚 ∈ ℝ ∀𝑥 ∈ 𝐴 𝐵 ≤ 𝑚)) |
56 | 6, 55 | mpd 15 |
1
⊢ (𝜑 → ∃𝑚 ∈ ℝ ∀𝑥 ∈ 𝐴 𝐵 ≤ 𝑚) |