Step |
Hyp |
Ref |
Expression |
1 |
|
lo1le.1 |
⊢ ( 𝜑 → 𝑀 ∈ ℝ ) |
2 |
|
lo1le.2 |
⊢ ( 𝜑 → ( 𝑥 ∈ 𝐴 ↦ 𝐵 ) ∈ ≤𝑂(1) ) |
3 |
|
lo1le.3 |
⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝐴 ) → 𝐵 ∈ 𝑉 ) |
4 |
|
lo1le.4 |
⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝐴 ) → 𝐶 ∈ ℝ ) |
5 |
|
lo1le.5 |
⊢ ( ( 𝜑 ∧ ( 𝑥 ∈ 𝐴 ∧ 𝑀 ≤ 𝑥 ) ) → 𝐶 ≤ 𝐵 ) |
6 |
|
simpr |
⊢ ( ( 𝜑 ∧ 𝑦 ∈ ℝ ) → 𝑦 ∈ ℝ ) |
7 |
1
|
adantr |
⊢ ( ( 𝜑 ∧ 𝑦 ∈ ℝ ) → 𝑀 ∈ ℝ ) |
8 |
6 7
|
ifcld |
⊢ ( ( 𝜑 ∧ 𝑦 ∈ ℝ ) → if ( 𝑀 ≤ 𝑦 , 𝑦 , 𝑀 ) ∈ ℝ ) |
9 |
1
|
ad2antrr |
⊢ ( ( ( 𝜑 ∧ 𝑦 ∈ ℝ ) ∧ ( 𝑚 ∈ ℝ ∧ 𝑥 ∈ 𝐴 ) ) → 𝑀 ∈ ℝ ) |
10 |
|
simplr |
⊢ ( ( ( 𝜑 ∧ 𝑦 ∈ ℝ ) ∧ ( 𝑚 ∈ ℝ ∧ 𝑥 ∈ 𝐴 ) ) → 𝑦 ∈ ℝ ) |
11 |
3
|
ralrimiva |
⊢ ( 𝜑 → ∀ 𝑥 ∈ 𝐴 𝐵 ∈ 𝑉 ) |
12 |
|
dmmptg |
⊢ ( ∀ 𝑥 ∈ 𝐴 𝐵 ∈ 𝑉 → dom ( 𝑥 ∈ 𝐴 ↦ 𝐵 ) = 𝐴 ) |
13 |
11 12
|
syl |
⊢ ( 𝜑 → dom ( 𝑥 ∈ 𝐴 ↦ 𝐵 ) = 𝐴 ) |
14 |
|
lo1dm |
⊢ ( ( 𝑥 ∈ 𝐴 ↦ 𝐵 ) ∈ ≤𝑂(1) → dom ( 𝑥 ∈ 𝐴 ↦ 𝐵 ) ⊆ ℝ ) |
15 |
2 14
|
syl |
⊢ ( 𝜑 → dom ( 𝑥 ∈ 𝐴 ↦ 𝐵 ) ⊆ ℝ ) |
16 |
13 15
|
eqsstrrd |
⊢ ( 𝜑 → 𝐴 ⊆ ℝ ) |
17 |
16
|
ad2antrr |
⊢ ( ( ( 𝜑 ∧ 𝑦 ∈ ℝ ) ∧ ( 𝑚 ∈ ℝ ∧ 𝑥 ∈ 𝐴 ) ) → 𝐴 ⊆ ℝ ) |
18 |
|
simprr |
⊢ ( ( ( 𝜑 ∧ 𝑦 ∈ ℝ ) ∧ ( 𝑚 ∈ ℝ ∧ 𝑥 ∈ 𝐴 ) ) → 𝑥 ∈ 𝐴 ) |
19 |
17 18
|
sseldd |
⊢ ( ( ( 𝜑 ∧ 𝑦 ∈ ℝ ) ∧ ( 𝑚 ∈ ℝ ∧ 𝑥 ∈ 𝐴 ) ) → 𝑥 ∈ ℝ ) |
20 |
|
maxle |
⊢ ( ( 𝑀 ∈ ℝ ∧ 𝑦 ∈ ℝ ∧ 𝑥 ∈ ℝ ) → ( if ( 𝑀 ≤ 𝑦 , 𝑦 , 𝑀 ) ≤ 𝑥 ↔ ( 𝑀 ≤ 𝑥 ∧ 𝑦 ≤ 𝑥 ) ) ) |
21 |
9 10 19 20
|
syl3anc |
⊢ ( ( ( 𝜑 ∧ 𝑦 ∈ ℝ ) ∧ ( 𝑚 ∈ ℝ ∧ 𝑥 ∈ 𝐴 ) ) → ( if ( 𝑀 ≤ 𝑦 , 𝑦 , 𝑀 ) ≤ 𝑥 ↔ ( 𝑀 ≤ 𝑥 ∧ 𝑦 ≤ 𝑥 ) ) ) |
22 |
|
simpr |
⊢ ( ( 𝑀 ≤ 𝑥 ∧ 𝑦 ≤ 𝑥 ) → 𝑦 ≤ 𝑥 ) |
23 |
21 22
|
syl6bi |
⊢ ( ( ( 𝜑 ∧ 𝑦 ∈ ℝ ) ∧ ( 𝑚 ∈ ℝ ∧ 𝑥 ∈ 𝐴 ) ) → ( if ( 𝑀 ≤ 𝑦 , 𝑦 , 𝑀 ) ≤ 𝑥 → 𝑦 ≤ 𝑥 ) ) |
24 |
23
|
imim1d |
⊢ ( ( ( 𝜑 ∧ 𝑦 ∈ ℝ ) ∧ ( 𝑚 ∈ ℝ ∧ 𝑥 ∈ 𝐴 ) ) → ( ( 𝑦 ≤ 𝑥 → 𝐵 ≤ 𝑚 ) → ( if ( 𝑀 ≤ 𝑦 , 𝑦 , 𝑀 ) ≤ 𝑥 → 𝐵 ≤ 𝑚 ) ) ) |
25 |
5
|
adantlr |
⊢ ( ( ( 𝜑 ∧ 𝑦 ∈ ℝ ) ∧ ( 𝑥 ∈ 𝐴 ∧ 𝑀 ≤ 𝑥 ) ) → 𝐶 ≤ 𝐵 ) |
26 |
25
|
adantrll |
⊢ ( ( ( 𝜑 ∧ 𝑦 ∈ ℝ ) ∧ ( ( 𝑚 ∈ ℝ ∧ 𝑥 ∈ 𝐴 ) ∧ 𝑀 ≤ 𝑥 ) ) → 𝐶 ≤ 𝐵 ) |
27 |
|
simpl |
⊢ ( ( 𝜑 ∧ 𝑦 ∈ ℝ ) → 𝜑 ) |
28 |
|
simplr |
⊢ ( ( ( 𝑚 ∈ ℝ ∧ 𝑥 ∈ 𝐴 ) ∧ 𝑀 ≤ 𝑥 ) → 𝑥 ∈ 𝐴 ) |
29 |
27 28 4
|
syl2an |
⊢ ( ( ( 𝜑 ∧ 𝑦 ∈ ℝ ) ∧ ( ( 𝑚 ∈ ℝ ∧ 𝑥 ∈ 𝐴 ) ∧ 𝑀 ≤ 𝑥 ) ) → 𝐶 ∈ ℝ ) |
30 |
3 2
|
lo1mptrcl |
⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝐴 ) → 𝐵 ∈ ℝ ) |
31 |
27 28 30
|
syl2an |
⊢ ( ( ( 𝜑 ∧ 𝑦 ∈ ℝ ) ∧ ( ( 𝑚 ∈ ℝ ∧ 𝑥 ∈ 𝐴 ) ∧ 𝑀 ≤ 𝑥 ) ) → 𝐵 ∈ ℝ ) |
32 |
|
simprll |
⊢ ( ( ( 𝜑 ∧ 𝑦 ∈ ℝ ) ∧ ( ( 𝑚 ∈ ℝ ∧ 𝑥 ∈ 𝐴 ) ∧ 𝑀 ≤ 𝑥 ) ) → 𝑚 ∈ ℝ ) |
33 |
|
letr |
⊢ ( ( 𝐶 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 𝑚 ∈ ℝ ) → ( ( 𝐶 ≤ 𝐵 ∧ 𝐵 ≤ 𝑚 ) → 𝐶 ≤ 𝑚 ) ) |
34 |
29 31 32 33
|
syl3anc |
⊢ ( ( ( 𝜑 ∧ 𝑦 ∈ ℝ ) ∧ ( ( 𝑚 ∈ ℝ ∧ 𝑥 ∈ 𝐴 ) ∧ 𝑀 ≤ 𝑥 ) ) → ( ( 𝐶 ≤ 𝐵 ∧ 𝐵 ≤ 𝑚 ) → 𝐶 ≤ 𝑚 ) ) |
35 |
26 34
|
mpand |
⊢ ( ( ( 𝜑 ∧ 𝑦 ∈ ℝ ) ∧ ( ( 𝑚 ∈ ℝ ∧ 𝑥 ∈ 𝐴 ) ∧ 𝑀 ≤ 𝑥 ) ) → ( 𝐵 ≤ 𝑚 → 𝐶 ≤ 𝑚 ) ) |
36 |
35
|
expr |
⊢ ( ( ( 𝜑 ∧ 𝑦 ∈ ℝ ) ∧ ( 𝑚 ∈ ℝ ∧ 𝑥 ∈ 𝐴 ) ) → ( 𝑀 ≤ 𝑥 → ( 𝐵 ≤ 𝑚 → 𝐶 ≤ 𝑚 ) ) ) |
37 |
36
|
adantrd |
⊢ ( ( ( 𝜑 ∧ 𝑦 ∈ ℝ ) ∧ ( 𝑚 ∈ ℝ ∧ 𝑥 ∈ 𝐴 ) ) → ( ( 𝑀 ≤ 𝑥 ∧ 𝑦 ≤ 𝑥 ) → ( 𝐵 ≤ 𝑚 → 𝐶 ≤ 𝑚 ) ) ) |
38 |
21 37
|
sylbid |
⊢ ( ( ( 𝜑 ∧ 𝑦 ∈ ℝ ) ∧ ( 𝑚 ∈ ℝ ∧ 𝑥 ∈ 𝐴 ) ) → ( if ( 𝑀 ≤ 𝑦 , 𝑦 , 𝑀 ) ≤ 𝑥 → ( 𝐵 ≤ 𝑚 → 𝐶 ≤ 𝑚 ) ) ) |
39 |
38
|
a2d |
⊢ ( ( ( 𝜑 ∧ 𝑦 ∈ ℝ ) ∧ ( 𝑚 ∈ ℝ ∧ 𝑥 ∈ 𝐴 ) ) → ( ( if ( 𝑀 ≤ 𝑦 , 𝑦 , 𝑀 ) ≤ 𝑥 → 𝐵 ≤ 𝑚 ) → ( if ( 𝑀 ≤ 𝑦 , 𝑦 , 𝑀 ) ≤ 𝑥 → 𝐶 ≤ 𝑚 ) ) ) |
40 |
24 39
|
syld |
⊢ ( ( ( 𝜑 ∧ 𝑦 ∈ ℝ ) ∧ ( 𝑚 ∈ ℝ ∧ 𝑥 ∈ 𝐴 ) ) → ( ( 𝑦 ≤ 𝑥 → 𝐵 ≤ 𝑚 ) → ( if ( 𝑀 ≤ 𝑦 , 𝑦 , 𝑀 ) ≤ 𝑥 → 𝐶 ≤ 𝑚 ) ) ) |
41 |
40
|
anassrs |
⊢ ( ( ( ( 𝜑 ∧ 𝑦 ∈ ℝ ) ∧ 𝑚 ∈ ℝ ) ∧ 𝑥 ∈ 𝐴 ) → ( ( 𝑦 ≤ 𝑥 → 𝐵 ≤ 𝑚 ) → ( if ( 𝑀 ≤ 𝑦 , 𝑦 , 𝑀 ) ≤ 𝑥 → 𝐶 ≤ 𝑚 ) ) ) |
42 |
41
|
ralimdva |
⊢ ( ( ( 𝜑 ∧ 𝑦 ∈ ℝ ) ∧ 𝑚 ∈ ℝ ) → ( ∀ 𝑥 ∈ 𝐴 ( 𝑦 ≤ 𝑥 → 𝐵 ≤ 𝑚 ) → ∀ 𝑥 ∈ 𝐴 ( if ( 𝑀 ≤ 𝑦 , 𝑦 , 𝑀 ) ≤ 𝑥 → 𝐶 ≤ 𝑚 ) ) ) |
43 |
42
|
reximdva |
⊢ ( ( 𝜑 ∧ 𝑦 ∈ ℝ ) → ( ∃ 𝑚 ∈ ℝ ∀ 𝑥 ∈ 𝐴 ( 𝑦 ≤ 𝑥 → 𝐵 ≤ 𝑚 ) → ∃ 𝑚 ∈ ℝ ∀ 𝑥 ∈ 𝐴 ( if ( 𝑀 ≤ 𝑦 , 𝑦 , 𝑀 ) ≤ 𝑥 → 𝐶 ≤ 𝑚 ) ) ) |
44 |
|
breq1 |
⊢ ( 𝑧 = if ( 𝑀 ≤ 𝑦 , 𝑦 , 𝑀 ) → ( 𝑧 ≤ 𝑥 ↔ if ( 𝑀 ≤ 𝑦 , 𝑦 , 𝑀 ) ≤ 𝑥 ) ) |
45 |
44
|
imbi1d |
⊢ ( 𝑧 = if ( 𝑀 ≤ 𝑦 , 𝑦 , 𝑀 ) → ( ( 𝑧 ≤ 𝑥 → 𝐶 ≤ 𝑚 ) ↔ ( if ( 𝑀 ≤ 𝑦 , 𝑦 , 𝑀 ) ≤ 𝑥 → 𝐶 ≤ 𝑚 ) ) ) |
46 |
45
|
rexralbidv |
⊢ ( 𝑧 = if ( 𝑀 ≤ 𝑦 , 𝑦 , 𝑀 ) → ( ∃ 𝑚 ∈ ℝ ∀ 𝑥 ∈ 𝐴 ( 𝑧 ≤ 𝑥 → 𝐶 ≤ 𝑚 ) ↔ ∃ 𝑚 ∈ ℝ ∀ 𝑥 ∈ 𝐴 ( if ( 𝑀 ≤ 𝑦 , 𝑦 , 𝑀 ) ≤ 𝑥 → 𝐶 ≤ 𝑚 ) ) ) |
47 |
46
|
rspcev |
⊢ ( ( if ( 𝑀 ≤ 𝑦 , 𝑦 , 𝑀 ) ∈ ℝ ∧ ∃ 𝑚 ∈ ℝ ∀ 𝑥 ∈ 𝐴 ( if ( 𝑀 ≤ 𝑦 , 𝑦 , 𝑀 ) ≤ 𝑥 → 𝐶 ≤ 𝑚 ) ) → ∃ 𝑧 ∈ ℝ ∃ 𝑚 ∈ ℝ ∀ 𝑥 ∈ 𝐴 ( 𝑧 ≤ 𝑥 → 𝐶 ≤ 𝑚 ) ) |
48 |
8 43 47
|
syl6an |
⊢ ( ( 𝜑 ∧ 𝑦 ∈ ℝ ) → ( ∃ 𝑚 ∈ ℝ ∀ 𝑥 ∈ 𝐴 ( 𝑦 ≤ 𝑥 → 𝐵 ≤ 𝑚 ) → ∃ 𝑧 ∈ ℝ ∃ 𝑚 ∈ ℝ ∀ 𝑥 ∈ 𝐴 ( 𝑧 ≤ 𝑥 → 𝐶 ≤ 𝑚 ) ) ) |
49 |
48
|
rexlimdva |
⊢ ( 𝜑 → ( ∃ 𝑦 ∈ ℝ ∃ 𝑚 ∈ ℝ ∀ 𝑥 ∈ 𝐴 ( 𝑦 ≤ 𝑥 → 𝐵 ≤ 𝑚 ) → ∃ 𝑧 ∈ ℝ ∃ 𝑚 ∈ ℝ ∀ 𝑥 ∈ 𝐴 ( 𝑧 ≤ 𝑥 → 𝐶 ≤ 𝑚 ) ) ) |
50 |
16 30
|
ello1mpt |
⊢ ( 𝜑 → ( ( 𝑥 ∈ 𝐴 ↦ 𝐵 ) ∈ ≤𝑂(1) ↔ ∃ 𝑦 ∈ ℝ ∃ 𝑚 ∈ ℝ ∀ 𝑥 ∈ 𝐴 ( 𝑦 ≤ 𝑥 → 𝐵 ≤ 𝑚 ) ) ) |
51 |
16 4
|
ello1mpt |
⊢ ( 𝜑 → ( ( 𝑥 ∈ 𝐴 ↦ 𝐶 ) ∈ ≤𝑂(1) ↔ ∃ 𝑧 ∈ ℝ ∃ 𝑚 ∈ ℝ ∀ 𝑥 ∈ 𝐴 ( 𝑧 ≤ 𝑥 → 𝐶 ≤ 𝑚 ) ) ) |
52 |
49 50 51
|
3imtr4d |
⊢ ( 𝜑 → ( ( 𝑥 ∈ 𝐴 ↦ 𝐵 ) ∈ ≤𝑂(1) → ( 𝑥 ∈ 𝐴 ↦ 𝐶 ) ∈ ≤𝑂(1) ) ) |
53 |
2 52
|
mpd |
⊢ ( 𝜑 → ( 𝑥 ∈ 𝐴 ↦ 𝐶 ) ∈ ≤𝑂(1) ) |