Step |
Hyp |
Ref |
Expression |
1 |
|
itgsubst.x |
⊢ ( 𝜑 → 𝑋 ∈ ℝ ) |
2 |
|
itgsubst.y |
⊢ ( 𝜑 → 𝑌 ∈ ℝ ) |
3 |
|
itgsubst.le |
⊢ ( 𝜑 → 𝑋 ≤ 𝑌 ) |
4 |
|
itgsubst.z |
⊢ ( 𝜑 → 𝑍 ∈ ℝ* ) |
5 |
|
itgsubst.w |
⊢ ( 𝜑 → 𝑊 ∈ ℝ* ) |
6 |
|
itgsubst.a |
⊢ ( 𝜑 → ( 𝑥 ∈ ( 𝑋 [,] 𝑌 ) ↦ 𝐴 ) ∈ ( ( 𝑋 [,] 𝑌 ) –cn→ ( 𝑍 (,) 𝑊 ) ) ) |
7 |
|
itgsubst.b |
⊢ ( 𝜑 → ( 𝑥 ∈ ( 𝑋 (,) 𝑌 ) ↦ 𝐵 ) ∈ ( ( ( 𝑋 (,) 𝑌 ) –cn→ ℂ ) ∩ 𝐿1 ) ) |
8 |
|
itgsubst.c |
⊢ ( 𝜑 → ( 𝑢 ∈ ( 𝑍 (,) 𝑊 ) ↦ 𝐶 ) ∈ ( ( 𝑍 (,) 𝑊 ) –cn→ ℂ ) ) |
9 |
|
itgsubst.da |
⊢ ( 𝜑 → ( ℝ D ( 𝑥 ∈ ( 𝑋 [,] 𝑌 ) ↦ 𝐴 ) ) = ( 𝑥 ∈ ( 𝑋 (,) 𝑌 ) ↦ 𝐵 ) ) |
10 |
|
itgsubst.e |
⊢ ( 𝑢 = 𝐴 → 𝐶 = 𝐸 ) |
11 |
|
itgsubst.k |
⊢ ( 𝑥 = 𝑋 → 𝐴 = 𝐾 ) |
12 |
|
itgsubst.l |
⊢ ( 𝑥 = 𝑌 → 𝐴 = 𝐿 ) |
13 |
|
ioossre |
⊢ ( 𝑍 (,) 𝑊 ) ⊆ ℝ |
14 |
|
ax-resscn |
⊢ ℝ ⊆ ℂ |
15 |
|
cncfss |
⊢ ( ( ( 𝑍 (,) 𝑊 ) ⊆ ℝ ∧ ℝ ⊆ ℂ ) → ( ( 𝑋 [,] 𝑌 ) –cn→ ( 𝑍 (,) 𝑊 ) ) ⊆ ( ( 𝑋 [,] 𝑌 ) –cn→ ℝ ) ) |
16 |
13 14 15
|
mp2an |
⊢ ( ( 𝑋 [,] 𝑌 ) –cn→ ( 𝑍 (,) 𝑊 ) ) ⊆ ( ( 𝑋 [,] 𝑌 ) –cn→ ℝ ) |
17 |
16 6
|
sseldi |
⊢ ( 𝜑 → ( 𝑥 ∈ ( 𝑋 [,] 𝑌 ) ↦ 𝐴 ) ∈ ( ( 𝑋 [,] 𝑌 ) –cn→ ℝ ) ) |
18 |
1 2 3 17
|
evthicc |
⊢ ( 𝜑 → ( ∃ 𝑦 ∈ ( 𝑋 [,] 𝑌 ) ∀ 𝑧 ∈ ( 𝑋 [,] 𝑌 ) ( ( 𝑥 ∈ ( 𝑋 [,] 𝑌 ) ↦ 𝐴 ) ‘ 𝑧 ) ≤ ( ( 𝑥 ∈ ( 𝑋 [,] 𝑌 ) ↦ 𝐴 ) ‘ 𝑦 ) ∧ ∃ 𝑦 ∈ ( 𝑋 [,] 𝑌 ) ∀ 𝑧 ∈ ( 𝑋 [,] 𝑌 ) ( ( 𝑥 ∈ ( 𝑋 [,] 𝑌 ) ↦ 𝐴 ) ‘ 𝑦 ) ≤ ( ( 𝑥 ∈ ( 𝑋 [,] 𝑌 ) ↦ 𝐴 ) ‘ 𝑧 ) ) ) |
19 |
|
ressxr |
⊢ ℝ ⊆ ℝ* |
20 |
13 19
|
sstri |
⊢ ( 𝑍 (,) 𝑊 ) ⊆ ℝ* |
21 |
|
cncff |
⊢ ( ( 𝑥 ∈ ( 𝑋 [,] 𝑌 ) ↦ 𝐴 ) ∈ ( ( 𝑋 [,] 𝑌 ) –cn→ ( 𝑍 (,) 𝑊 ) ) → ( 𝑥 ∈ ( 𝑋 [,] 𝑌 ) ↦ 𝐴 ) : ( 𝑋 [,] 𝑌 ) ⟶ ( 𝑍 (,) 𝑊 ) ) |
22 |
6 21
|
syl |
⊢ ( 𝜑 → ( 𝑥 ∈ ( 𝑋 [,] 𝑌 ) ↦ 𝐴 ) : ( 𝑋 [,] 𝑌 ) ⟶ ( 𝑍 (,) 𝑊 ) ) |
23 |
22
|
adantr |
⊢ ( ( 𝜑 ∧ ( 𝑦 ∈ ( 𝑋 [,] 𝑌 ) ∧ ∀ 𝑧 ∈ ( 𝑋 [,] 𝑌 ) ( ( 𝑥 ∈ ( 𝑋 [,] 𝑌 ) ↦ 𝐴 ) ‘ 𝑧 ) ≤ ( ( 𝑥 ∈ ( 𝑋 [,] 𝑌 ) ↦ 𝐴 ) ‘ 𝑦 ) ) ) → ( 𝑥 ∈ ( 𝑋 [,] 𝑌 ) ↦ 𝐴 ) : ( 𝑋 [,] 𝑌 ) ⟶ ( 𝑍 (,) 𝑊 ) ) |
24 |
|
simprl |
⊢ ( ( 𝜑 ∧ ( 𝑦 ∈ ( 𝑋 [,] 𝑌 ) ∧ ∀ 𝑧 ∈ ( 𝑋 [,] 𝑌 ) ( ( 𝑥 ∈ ( 𝑋 [,] 𝑌 ) ↦ 𝐴 ) ‘ 𝑧 ) ≤ ( ( 𝑥 ∈ ( 𝑋 [,] 𝑌 ) ↦ 𝐴 ) ‘ 𝑦 ) ) ) → 𝑦 ∈ ( 𝑋 [,] 𝑌 ) ) |
25 |
23 24
|
ffvelrnd |
⊢ ( ( 𝜑 ∧ ( 𝑦 ∈ ( 𝑋 [,] 𝑌 ) ∧ ∀ 𝑧 ∈ ( 𝑋 [,] 𝑌 ) ( ( 𝑥 ∈ ( 𝑋 [,] 𝑌 ) ↦ 𝐴 ) ‘ 𝑧 ) ≤ ( ( 𝑥 ∈ ( 𝑋 [,] 𝑌 ) ↦ 𝐴 ) ‘ 𝑦 ) ) ) → ( ( 𝑥 ∈ ( 𝑋 [,] 𝑌 ) ↦ 𝐴 ) ‘ 𝑦 ) ∈ ( 𝑍 (,) 𝑊 ) ) |
26 |
20 25
|
sseldi |
⊢ ( ( 𝜑 ∧ ( 𝑦 ∈ ( 𝑋 [,] 𝑌 ) ∧ ∀ 𝑧 ∈ ( 𝑋 [,] 𝑌 ) ( ( 𝑥 ∈ ( 𝑋 [,] 𝑌 ) ↦ 𝐴 ) ‘ 𝑧 ) ≤ ( ( 𝑥 ∈ ( 𝑋 [,] 𝑌 ) ↦ 𝐴 ) ‘ 𝑦 ) ) ) → ( ( 𝑥 ∈ ( 𝑋 [,] 𝑌 ) ↦ 𝐴 ) ‘ 𝑦 ) ∈ ℝ* ) |
27 |
5
|
adantr |
⊢ ( ( 𝜑 ∧ ( 𝑦 ∈ ( 𝑋 [,] 𝑌 ) ∧ ∀ 𝑧 ∈ ( 𝑋 [,] 𝑌 ) ( ( 𝑥 ∈ ( 𝑋 [,] 𝑌 ) ↦ 𝐴 ) ‘ 𝑧 ) ≤ ( ( 𝑥 ∈ ( 𝑋 [,] 𝑌 ) ↦ 𝐴 ) ‘ 𝑦 ) ) ) → 𝑊 ∈ ℝ* ) |
28 |
|
eliooord |
⊢ ( ( ( 𝑥 ∈ ( 𝑋 [,] 𝑌 ) ↦ 𝐴 ) ‘ 𝑦 ) ∈ ( 𝑍 (,) 𝑊 ) → ( 𝑍 < ( ( 𝑥 ∈ ( 𝑋 [,] 𝑌 ) ↦ 𝐴 ) ‘ 𝑦 ) ∧ ( ( 𝑥 ∈ ( 𝑋 [,] 𝑌 ) ↦ 𝐴 ) ‘ 𝑦 ) < 𝑊 ) ) |
29 |
25 28
|
syl |
⊢ ( ( 𝜑 ∧ ( 𝑦 ∈ ( 𝑋 [,] 𝑌 ) ∧ ∀ 𝑧 ∈ ( 𝑋 [,] 𝑌 ) ( ( 𝑥 ∈ ( 𝑋 [,] 𝑌 ) ↦ 𝐴 ) ‘ 𝑧 ) ≤ ( ( 𝑥 ∈ ( 𝑋 [,] 𝑌 ) ↦ 𝐴 ) ‘ 𝑦 ) ) ) → ( 𝑍 < ( ( 𝑥 ∈ ( 𝑋 [,] 𝑌 ) ↦ 𝐴 ) ‘ 𝑦 ) ∧ ( ( 𝑥 ∈ ( 𝑋 [,] 𝑌 ) ↦ 𝐴 ) ‘ 𝑦 ) < 𝑊 ) ) |
30 |
29
|
simprd |
⊢ ( ( 𝜑 ∧ ( 𝑦 ∈ ( 𝑋 [,] 𝑌 ) ∧ ∀ 𝑧 ∈ ( 𝑋 [,] 𝑌 ) ( ( 𝑥 ∈ ( 𝑋 [,] 𝑌 ) ↦ 𝐴 ) ‘ 𝑧 ) ≤ ( ( 𝑥 ∈ ( 𝑋 [,] 𝑌 ) ↦ 𝐴 ) ‘ 𝑦 ) ) ) → ( ( 𝑥 ∈ ( 𝑋 [,] 𝑌 ) ↦ 𝐴 ) ‘ 𝑦 ) < 𝑊 ) |
31 |
|
qbtwnxr |
⊢ ( ( ( ( 𝑥 ∈ ( 𝑋 [,] 𝑌 ) ↦ 𝐴 ) ‘ 𝑦 ) ∈ ℝ* ∧ 𝑊 ∈ ℝ* ∧ ( ( 𝑥 ∈ ( 𝑋 [,] 𝑌 ) ↦ 𝐴 ) ‘ 𝑦 ) < 𝑊 ) → ∃ 𝑛 ∈ ℚ ( ( ( 𝑥 ∈ ( 𝑋 [,] 𝑌 ) ↦ 𝐴 ) ‘ 𝑦 ) < 𝑛 ∧ 𝑛 < 𝑊 ) ) |
32 |
26 27 30 31
|
syl3anc |
⊢ ( ( 𝜑 ∧ ( 𝑦 ∈ ( 𝑋 [,] 𝑌 ) ∧ ∀ 𝑧 ∈ ( 𝑋 [,] 𝑌 ) ( ( 𝑥 ∈ ( 𝑋 [,] 𝑌 ) ↦ 𝐴 ) ‘ 𝑧 ) ≤ ( ( 𝑥 ∈ ( 𝑋 [,] 𝑌 ) ↦ 𝐴 ) ‘ 𝑦 ) ) ) → ∃ 𝑛 ∈ ℚ ( ( ( 𝑥 ∈ ( 𝑋 [,] 𝑌 ) ↦ 𝐴 ) ‘ 𝑦 ) < 𝑛 ∧ 𝑛 < 𝑊 ) ) |
33 |
|
qre |
⊢ ( 𝑛 ∈ ℚ → 𝑛 ∈ ℝ ) |
34 |
33
|
ad2antrl |
⊢ ( ( ( 𝜑 ∧ ( 𝑦 ∈ ( 𝑋 [,] 𝑌 ) ∧ ∀ 𝑧 ∈ ( 𝑋 [,] 𝑌 ) ( ( 𝑥 ∈ ( 𝑋 [,] 𝑌 ) ↦ 𝐴 ) ‘ 𝑧 ) ≤ ( ( 𝑥 ∈ ( 𝑋 [,] 𝑌 ) ↦ 𝐴 ) ‘ 𝑦 ) ) ) ∧ ( 𝑛 ∈ ℚ ∧ ( ( ( 𝑥 ∈ ( 𝑋 [,] 𝑌 ) ↦ 𝐴 ) ‘ 𝑦 ) < 𝑛 ∧ 𝑛 < 𝑊 ) ) ) → 𝑛 ∈ ℝ ) |
35 |
4
|
ad2antrr |
⊢ ( ( ( 𝜑 ∧ ( 𝑦 ∈ ( 𝑋 [,] 𝑌 ) ∧ ∀ 𝑧 ∈ ( 𝑋 [,] 𝑌 ) ( ( 𝑥 ∈ ( 𝑋 [,] 𝑌 ) ↦ 𝐴 ) ‘ 𝑧 ) ≤ ( ( 𝑥 ∈ ( 𝑋 [,] 𝑌 ) ↦ 𝐴 ) ‘ 𝑦 ) ) ) ∧ ( 𝑛 ∈ ℚ ∧ ( ( ( 𝑥 ∈ ( 𝑋 [,] 𝑌 ) ↦ 𝐴 ) ‘ 𝑦 ) < 𝑛 ∧ 𝑛 < 𝑊 ) ) ) → 𝑍 ∈ ℝ* ) |
36 |
26
|
adantr |
⊢ ( ( ( 𝜑 ∧ ( 𝑦 ∈ ( 𝑋 [,] 𝑌 ) ∧ ∀ 𝑧 ∈ ( 𝑋 [,] 𝑌 ) ( ( 𝑥 ∈ ( 𝑋 [,] 𝑌 ) ↦ 𝐴 ) ‘ 𝑧 ) ≤ ( ( 𝑥 ∈ ( 𝑋 [,] 𝑌 ) ↦ 𝐴 ) ‘ 𝑦 ) ) ) ∧ ( 𝑛 ∈ ℚ ∧ ( ( ( 𝑥 ∈ ( 𝑋 [,] 𝑌 ) ↦ 𝐴 ) ‘ 𝑦 ) < 𝑛 ∧ 𝑛 < 𝑊 ) ) ) → ( ( 𝑥 ∈ ( 𝑋 [,] 𝑌 ) ↦ 𝐴 ) ‘ 𝑦 ) ∈ ℝ* ) |
37 |
34
|
rexrd |
⊢ ( ( ( 𝜑 ∧ ( 𝑦 ∈ ( 𝑋 [,] 𝑌 ) ∧ ∀ 𝑧 ∈ ( 𝑋 [,] 𝑌 ) ( ( 𝑥 ∈ ( 𝑋 [,] 𝑌 ) ↦ 𝐴 ) ‘ 𝑧 ) ≤ ( ( 𝑥 ∈ ( 𝑋 [,] 𝑌 ) ↦ 𝐴 ) ‘ 𝑦 ) ) ) ∧ ( 𝑛 ∈ ℚ ∧ ( ( ( 𝑥 ∈ ( 𝑋 [,] 𝑌 ) ↦ 𝐴 ) ‘ 𝑦 ) < 𝑛 ∧ 𝑛 < 𝑊 ) ) ) → 𝑛 ∈ ℝ* ) |
38 |
29
|
simpld |
⊢ ( ( 𝜑 ∧ ( 𝑦 ∈ ( 𝑋 [,] 𝑌 ) ∧ ∀ 𝑧 ∈ ( 𝑋 [,] 𝑌 ) ( ( 𝑥 ∈ ( 𝑋 [,] 𝑌 ) ↦ 𝐴 ) ‘ 𝑧 ) ≤ ( ( 𝑥 ∈ ( 𝑋 [,] 𝑌 ) ↦ 𝐴 ) ‘ 𝑦 ) ) ) → 𝑍 < ( ( 𝑥 ∈ ( 𝑋 [,] 𝑌 ) ↦ 𝐴 ) ‘ 𝑦 ) ) |
39 |
38
|
adantr |
⊢ ( ( ( 𝜑 ∧ ( 𝑦 ∈ ( 𝑋 [,] 𝑌 ) ∧ ∀ 𝑧 ∈ ( 𝑋 [,] 𝑌 ) ( ( 𝑥 ∈ ( 𝑋 [,] 𝑌 ) ↦ 𝐴 ) ‘ 𝑧 ) ≤ ( ( 𝑥 ∈ ( 𝑋 [,] 𝑌 ) ↦ 𝐴 ) ‘ 𝑦 ) ) ) ∧ ( 𝑛 ∈ ℚ ∧ ( ( ( 𝑥 ∈ ( 𝑋 [,] 𝑌 ) ↦ 𝐴 ) ‘ 𝑦 ) < 𝑛 ∧ 𝑛 < 𝑊 ) ) ) → 𝑍 < ( ( 𝑥 ∈ ( 𝑋 [,] 𝑌 ) ↦ 𝐴 ) ‘ 𝑦 ) ) |
40 |
|
simprrl |
⊢ ( ( ( 𝜑 ∧ ( 𝑦 ∈ ( 𝑋 [,] 𝑌 ) ∧ ∀ 𝑧 ∈ ( 𝑋 [,] 𝑌 ) ( ( 𝑥 ∈ ( 𝑋 [,] 𝑌 ) ↦ 𝐴 ) ‘ 𝑧 ) ≤ ( ( 𝑥 ∈ ( 𝑋 [,] 𝑌 ) ↦ 𝐴 ) ‘ 𝑦 ) ) ) ∧ ( 𝑛 ∈ ℚ ∧ ( ( ( 𝑥 ∈ ( 𝑋 [,] 𝑌 ) ↦ 𝐴 ) ‘ 𝑦 ) < 𝑛 ∧ 𝑛 < 𝑊 ) ) ) → ( ( 𝑥 ∈ ( 𝑋 [,] 𝑌 ) ↦ 𝐴 ) ‘ 𝑦 ) < 𝑛 ) |
41 |
35 36 37 39 40
|
xrlttrd |
⊢ ( ( ( 𝜑 ∧ ( 𝑦 ∈ ( 𝑋 [,] 𝑌 ) ∧ ∀ 𝑧 ∈ ( 𝑋 [,] 𝑌 ) ( ( 𝑥 ∈ ( 𝑋 [,] 𝑌 ) ↦ 𝐴 ) ‘ 𝑧 ) ≤ ( ( 𝑥 ∈ ( 𝑋 [,] 𝑌 ) ↦ 𝐴 ) ‘ 𝑦 ) ) ) ∧ ( 𝑛 ∈ ℚ ∧ ( ( ( 𝑥 ∈ ( 𝑋 [,] 𝑌 ) ↦ 𝐴 ) ‘ 𝑦 ) < 𝑛 ∧ 𝑛 < 𝑊 ) ) ) → 𝑍 < 𝑛 ) |
42 |
|
simprrr |
⊢ ( ( ( 𝜑 ∧ ( 𝑦 ∈ ( 𝑋 [,] 𝑌 ) ∧ ∀ 𝑧 ∈ ( 𝑋 [,] 𝑌 ) ( ( 𝑥 ∈ ( 𝑋 [,] 𝑌 ) ↦ 𝐴 ) ‘ 𝑧 ) ≤ ( ( 𝑥 ∈ ( 𝑋 [,] 𝑌 ) ↦ 𝐴 ) ‘ 𝑦 ) ) ) ∧ ( 𝑛 ∈ ℚ ∧ ( ( ( 𝑥 ∈ ( 𝑋 [,] 𝑌 ) ↦ 𝐴 ) ‘ 𝑦 ) < 𝑛 ∧ 𝑛 < 𝑊 ) ) ) → 𝑛 < 𝑊 ) |
43 |
5
|
ad2antrr |
⊢ ( ( ( 𝜑 ∧ ( 𝑦 ∈ ( 𝑋 [,] 𝑌 ) ∧ ∀ 𝑧 ∈ ( 𝑋 [,] 𝑌 ) ( ( 𝑥 ∈ ( 𝑋 [,] 𝑌 ) ↦ 𝐴 ) ‘ 𝑧 ) ≤ ( ( 𝑥 ∈ ( 𝑋 [,] 𝑌 ) ↦ 𝐴 ) ‘ 𝑦 ) ) ) ∧ ( 𝑛 ∈ ℚ ∧ ( ( ( 𝑥 ∈ ( 𝑋 [,] 𝑌 ) ↦ 𝐴 ) ‘ 𝑦 ) < 𝑛 ∧ 𝑛 < 𝑊 ) ) ) → 𝑊 ∈ ℝ* ) |
44 |
|
elioo2 |
⊢ ( ( 𝑍 ∈ ℝ* ∧ 𝑊 ∈ ℝ* ) → ( 𝑛 ∈ ( 𝑍 (,) 𝑊 ) ↔ ( 𝑛 ∈ ℝ ∧ 𝑍 < 𝑛 ∧ 𝑛 < 𝑊 ) ) ) |
45 |
35 43 44
|
syl2anc |
⊢ ( ( ( 𝜑 ∧ ( 𝑦 ∈ ( 𝑋 [,] 𝑌 ) ∧ ∀ 𝑧 ∈ ( 𝑋 [,] 𝑌 ) ( ( 𝑥 ∈ ( 𝑋 [,] 𝑌 ) ↦ 𝐴 ) ‘ 𝑧 ) ≤ ( ( 𝑥 ∈ ( 𝑋 [,] 𝑌 ) ↦ 𝐴 ) ‘ 𝑦 ) ) ) ∧ ( 𝑛 ∈ ℚ ∧ ( ( ( 𝑥 ∈ ( 𝑋 [,] 𝑌 ) ↦ 𝐴 ) ‘ 𝑦 ) < 𝑛 ∧ 𝑛 < 𝑊 ) ) ) → ( 𝑛 ∈ ( 𝑍 (,) 𝑊 ) ↔ ( 𝑛 ∈ ℝ ∧ 𝑍 < 𝑛 ∧ 𝑛 < 𝑊 ) ) ) |
46 |
34 41 42 45
|
mpbir3and |
⊢ ( ( ( 𝜑 ∧ ( 𝑦 ∈ ( 𝑋 [,] 𝑌 ) ∧ ∀ 𝑧 ∈ ( 𝑋 [,] 𝑌 ) ( ( 𝑥 ∈ ( 𝑋 [,] 𝑌 ) ↦ 𝐴 ) ‘ 𝑧 ) ≤ ( ( 𝑥 ∈ ( 𝑋 [,] 𝑌 ) ↦ 𝐴 ) ‘ 𝑦 ) ) ) ∧ ( 𝑛 ∈ ℚ ∧ ( ( ( 𝑥 ∈ ( 𝑋 [,] 𝑌 ) ↦ 𝐴 ) ‘ 𝑦 ) < 𝑛 ∧ 𝑛 < 𝑊 ) ) ) → 𝑛 ∈ ( 𝑍 (,) 𝑊 ) ) |
47 |
|
anass |
⊢ ( ( ( 𝜑 ∧ 𝑦 ∈ ( 𝑋 [,] 𝑌 ) ) ∧ ∀ 𝑧 ∈ ( 𝑋 [,] 𝑌 ) ( ( 𝑥 ∈ ( 𝑋 [,] 𝑌 ) ↦ 𝐴 ) ‘ 𝑧 ) ≤ ( ( 𝑥 ∈ ( 𝑋 [,] 𝑌 ) ↦ 𝐴 ) ‘ 𝑦 ) ) ↔ ( 𝜑 ∧ ( 𝑦 ∈ ( 𝑋 [,] 𝑌 ) ∧ ∀ 𝑧 ∈ ( 𝑋 [,] 𝑌 ) ( ( 𝑥 ∈ ( 𝑋 [,] 𝑌 ) ↦ 𝐴 ) ‘ 𝑧 ) ≤ ( ( 𝑥 ∈ ( 𝑋 [,] 𝑌 ) ↦ 𝐴 ) ‘ 𝑦 ) ) ) ) |
48 |
|
simprrl |
⊢ ( ( ( 𝜑 ∧ 𝑦 ∈ ( 𝑋 [,] 𝑌 ) ) ∧ ( 𝑛 ∈ ℚ ∧ ( ( ( 𝑥 ∈ ( 𝑋 [,] 𝑌 ) ↦ 𝐴 ) ‘ 𝑦 ) < 𝑛 ∧ 𝑛 < 𝑊 ) ) ) → ( ( 𝑥 ∈ ( 𝑋 [,] 𝑌 ) ↦ 𝐴 ) ‘ 𝑦 ) < 𝑛 ) |
49 |
48
|
adantr |
⊢ ( ( ( ( 𝜑 ∧ 𝑦 ∈ ( 𝑋 [,] 𝑌 ) ) ∧ ( 𝑛 ∈ ℚ ∧ ( ( ( 𝑥 ∈ ( 𝑋 [,] 𝑌 ) ↦ 𝐴 ) ‘ 𝑦 ) < 𝑛 ∧ 𝑛 < 𝑊 ) ) ) ∧ 𝑧 ∈ ( 𝑋 [,] 𝑌 ) ) → ( ( 𝑥 ∈ ( 𝑋 [,] 𝑌 ) ↦ 𝐴 ) ‘ 𝑦 ) < 𝑛 ) |
50 |
22
|
ad2antrr |
⊢ ( ( ( 𝜑 ∧ 𝑦 ∈ ( 𝑋 [,] 𝑌 ) ) ∧ ( 𝑛 ∈ ℚ ∧ ( ( ( 𝑥 ∈ ( 𝑋 [,] 𝑌 ) ↦ 𝐴 ) ‘ 𝑦 ) < 𝑛 ∧ 𝑛 < 𝑊 ) ) ) → ( 𝑥 ∈ ( 𝑋 [,] 𝑌 ) ↦ 𝐴 ) : ( 𝑋 [,] 𝑌 ) ⟶ ( 𝑍 (,) 𝑊 ) ) |
51 |
50
|
ffvelrnda |
⊢ ( ( ( ( 𝜑 ∧ 𝑦 ∈ ( 𝑋 [,] 𝑌 ) ) ∧ ( 𝑛 ∈ ℚ ∧ ( ( ( 𝑥 ∈ ( 𝑋 [,] 𝑌 ) ↦ 𝐴 ) ‘ 𝑦 ) < 𝑛 ∧ 𝑛 < 𝑊 ) ) ) ∧ 𝑧 ∈ ( 𝑋 [,] 𝑌 ) ) → ( ( 𝑥 ∈ ( 𝑋 [,] 𝑌 ) ↦ 𝐴 ) ‘ 𝑧 ) ∈ ( 𝑍 (,) 𝑊 ) ) |
52 |
20 51
|
sseldi |
⊢ ( ( ( ( 𝜑 ∧ 𝑦 ∈ ( 𝑋 [,] 𝑌 ) ) ∧ ( 𝑛 ∈ ℚ ∧ ( ( ( 𝑥 ∈ ( 𝑋 [,] 𝑌 ) ↦ 𝐴 ) ‘ 𝑦 ) < 𝑛 ∧ 𝑛 < 𝑊 ) ) ) ∧ 𝑧 ∈ ( 𝑋 [,] 𝑌 ) ) → ( ( 𝑥 ∈ ( 𝑋 [,] 𝑌 ) ↦ 𝐴 ) ‘ 𝑧 ) ∈ ℝ* ) |
53 |
|
simplr |
⊢ ( ( ( 𝜑 ∧ 𝑦 ∈ ( 𝑋 [,] 𝑌 ) ) ∧ ( 𝑛 ∈ ℚ ∧ ( ( ( 𝑥 ∈ ( 𝑋 [,] 𝑌 ) ↦ 𝐴 ) ‘ 𝑦 ) < 𝑛 ∧ 𝑛 < 𝑊 ) ) ) → 𝑦 ∈ ( 𝑋 [,] 𝑌 ) ) |
54 |
50 53
|
ffvelrnd |
⊢ ( ( ( 𝜑 ∧ 𝑦 ∈ ( 𝑋 [,] 𝑌 ) ) ∧ ( 𝑛 ∈ ℚ ∧ ( ( ( 𝑥 ∈ ( 𝑋 [,] 𝑌 ) ↦ 𝐴 ) ‘ 𝑦 ) < 𝑛 ∧ 𝑛 < 𝑊 ) ) ) → ( ( 𝑥 ∈ ( 𝑋 [,] 𝑌 ) ↦ 𝐴 ) ‘ 𝑦 ) ∈ ( 𝑍 (,) 𝑊 ) ) |
55 |
20 54
|
sseldi |
⊢ ( ( ( 𝜑 ∧ 𝑦 ∈ ( 𝑋 [,] 𝑌 ) ) ∧ ( 𝑛 ∈ ℚ ∧ ( ( ( 𝑥 ∈ ( 𝑋 [,] 𝑌 ) ↦ 𝐴 ) ‘ 𝑦 ) < 𝑛 ∧ 𝑛 < 𝑊 ) ) ) → ( ( 𝑥 ∈ ( 𝑋 [,] 𝑌 ) ↦ 𝐴 ) ‘ 𝑦 ) ∈ ℝ* ) |
56 |
55
|
adantr |
⊢ ( ( ( ( 𝜑 ∧ 𝑦 ∈ ( 𝑋 [,] 𝑌 ) ) ∧ ( 𝑛 ∈ ℚ ∧ ( ( ( 𝑥 ∈ ( 𝑋 [,] 𝑌 ) ↦ 𝐴 ) ‘ 𝑦 ) < 𝑛 ∧ 𝑛 < 𝑊 ) ) ) ∧ 𝑧 ∈ ( 𝑋 [,] 𝑌 ) ) → ( ( 𝑥 ∈ ( 𝑋 [,] 𝑌 ) ↦ 𝐴 ) ‘ 𝑦 ) ∈ ℝ* ) |
57 |
33
|
ad2antrl |
⊢ ( ( ( 𝜑 ∧ 𝑦 ∈ ( 𝑋 [,] 𝑌 ) ) ∧ ( 𝑛 ∈ ℚ ∧ ( ( ( 𝑥 ∈ ( 𝑋 [,] 𝑌 ) ↦ 𝐴 ) ‘ 𝑦 ) < 𝑛 ∧ 𝑛 < 𝑊 ) ) ) → 𝑛 ∈ ℝ ) |
58 |
57
|
adantr |
⊢ ( ( ( ( 𝜑 ∧ 𝑦 ∈ ( 𝑋 [,] 𝑌 ) ) ∧ ( 𝑛 ∈ ℚ ∧ ( ( ( 𝑥 ∈ ( 𝑋 [,] 𝑌 ) ↦ 𝐴 ) ‘ 𝑦 ) < 𝑛 ∧ 𝑛 < 𝑊 ) ) ) ∧ 𝑧 ∈ ( 𝑋 [,] 𝑌 ) ) → 𝑛 ∈ ℝ ) |
59 |
58
|
rexrd |
⊢ ( ( ( ( 𝜑 ∧ 𝑦 ∈ ( 𝑋 [,] 𝑌 ) ) ∧ ( 𝑛 ∈ ℚ ∧ ( ( ( 𝑥 ∈ ( 𝑋 [,] 𝑌 ) ↦ 𝐴 ) ‘ 𝑦 ) < 𝑛 ∧ 𝑛 < 𝑊 ) ) ) ∧ 𝑧 ∈ ( 𝑋 [,] 𝑌 ) ) → 𝑛 ∈ ℝ* ) |
60 |
|
xrlelttr |
⊢ ( ( ( ( 𝑥 ∈ ( 𝑋 [,] 𝑌 ) ↦ 𝐴 ) ‘ 𝑧 ) ∈ ℝ* ∧ ( ( 𝑥 ∈ ( 𝑋 [,] 𝑌 ) ↦ 𝐴 ) ‘ 𝑦 ) ∈ ℝ* ∧ 𝑛 ∈ ℝ* ) → ( ( ( ( 𝑥 ∈ ( 𝑋 [,] 𝑌 ) ↦ 𝐴 ) ‘ 𝑧 ) ≤ ( ( 𝑥 ∈ ( 𝑋 [,] 𝑌 ) ↦ 𝐴 ) ‘ 𝑦 ) ∧ ( ( 𝑥 ∈ ( 𝑋 [,] 𝑌 ) ↦ 𝐴 ) ‘ 𝑦 ) < 𝑛 ) → ( ( 𝑥 ∈ ( 𝑋 [,] 𝑌 ) ↦ 𝐴 ) ‘ 𝑧 ) < 𝑛 ) ) |
61 |
52 56 59 60
|
syl3anc |
⊢ ( ( ( ( 𝜑 ∧ 𝑦 ∈ ( 𝑋 [,] 𝑌 ) ) ∧ ( 𝑛 ∈ ℚ ∧ ( ( ( 𝑥 ∈ ( 𝑋 [,] 𝑌 ) ↦ 𝐴 ) ‘ 𝑦 ) < 𝑛 ∧ 𝑛 < 𝑊 ) ) ) ∧ 𝑧 ∈ ( 𝑋 [,] 𝑌 ) ) → ( ( ( ( 𝑥 ∈ ( 𝑋 [,] 𝑌 ) ↦ 𝐴 ) ‘ 𝑧 ) ≤ ( ( 𝑥 ∈ ( 𝑋 [,] 𝑌 ) ↦ 𝐴 ) ‘ 𝑦 ) ∧ ( ( 𝑥 ∈ ( 𝑋 [,] 𝑌 ) ↦ 𝐴 ) ‘ 𝑦 ) < 𝑛 ) → ( ( 𝑥 ∈ ( 𝑋 [,] 𝑌 ) ↦ 𝐴 ) ‘ 𝑧 ) < 𝑛 ) ) |
62 |
49 61
|
mpan2d |
⊢ ( ( ( ( 𝜑 ∧ 𝑦 ∈ ( 𝑋 [,] 𝑌 ) ) ∧ ( 𝑛 ∈ ℚ ∧ ( ( ( 𝑥 ∈ ( 𝑋 [,] 𝑌 ) ↦ 𝐴 ) ‘ 𝑦 ) < 𝑛 ∧ 𝑛 < 𝑊 ) ) ) ∧ 𝑧 ∈ ( 𝑋 [,] 𝑌 ) ) → ( ( ( 𝑥 ∈ ( 𝑋 [,] 𝑌 ) ↦ 𝐴 ) ‘ 𝑧 ) ≤ ( ( 𝑥 ∈ ( 𝑋 [,] 𝑌 ) ↦ 𝐴 ) ‘ 𝑦 ) → ( ( 𝑥 ∈ ( 𝑋 [,] 𝑌 ) ↦ 𝐴 ) ‘ 𝑧 ) < 𝑛 ) ) |
63 |
62
|
ralimdva |
⊢ ( ( ( 𝜑 ∧ 𝑦 ∈ ( 𝑋 [,] 𝑌 ) ) ∧ ( 𝑛 ∈ ℚ ∧ ( ( ( 𝑥 ∈ ( 𝑋 [,] 𝑌 ) ↦ 𝐴 ) ‘ 𝑦 ) < 𝑛 ∧ 𝑛 < 𝑊 ) ) ) → ( ∀ 𝑧 ∈ ( 𝑋 [,] 𝑌 ) ( ( 𝑥 ∈ ( 𝑋 [,] 𝑌 ) ↦ 𝐴 ) ‘ 𝑧 ) ≤ ( ( 𝑥 ∈ ( 𝑋 [,] 𝑌 ) ↦ 𝐴 ) ‘ 𝑦 ) → ∀ 𝑧 ∈ ( 𝑋 [,] 𝑌 ) ( ( 𝑥 ∈ ( 𝑋 [,] 𝑌 ) ↦ 𝐴 ) ‘ 𝑧 ) < 𝑛 ) ) |
64 |
63
|
imp |
⊢ ( ( ( ( 𝜑 ∧ 𝑦 ∈ ( 𝑋 [,] 𝑌 ) ) ∧ ( 𝑛 ∈ ℚ ∧ ( ( ( 𝑥 ∈ ( 𝑋 [,] 𝑌 ) ↦ 𝐴 ) ‘ 𝑦 ) < 𝑛 ∧ 𝑛 < 𝑊 ) ) ) ∧ ∀ 𝑧 ∈ ( 𝑋 [,] 𝑌 ) ( ( 𝑥 ∈ ( 𝑋 [,] 𝑌 ) ↦ 𝐴 ) ‘ 𝑧 ) ≤ ( ( 𝑥 ∈ ( 𝑋 [,] 𝑌 ) ↦ 𝐴 ) ‘ 𝑦 ) ) → ∀ 𝑧 ∈ ( 𝑋 [,] 𝑌 ) ( ( 𝑥 ∈ ( 𝑋 [,] 𝑌 ) ↦ 𝐴 ) ‘ 𝑧 ) < 𝑛 ) |
65 |
64
|
an32s |
⊢ ( ( ( ( 𝜑 ∧ 𝑦 ∈ ( 𝑋 [,] 𝑌 ) ) ∧ ∀ 𝑧 ∈ ( 𝑋 [,] 𝑌 ) ( ( 𝑥 ∈ ( 𝑋 [,] 𝑌 ) ↦ 𝐴 ) ‘ 𝑧 ) ≤ ( ( 𝑥 ∈ ( 𝑋 [,] 𝑌 ) ↦ 𝐴 ) ‘ 𝑦 ) ) ∧ ( 𝑛 ∈ ℚ ∧ ( ( ( 𝑥 ∈ ( 𝑋 [,] 𝑌 ) ↦ 𝐴 ) ‘ 𝑦 ) < 𝑛 ∧ 𝑛 < 𝑊 ) ) ) → ∀ 𝑧 ∈ ( 𝑋 [,] 𝑌 ) ( ( 𝑥 ∈ ( 𝑋 [,] 𝑌 ) ↦ 𝐴 ) ‘ 𝑧 ) < 𝑛 ) |
66 |
47 65
|
sylanbr |
⊢ ( ( ( 𝜑 ∧ ( 𝑦 ∈ ( 𝑋 [,] 𝑌 ) ∧ ∀ 𝑧 ∈ ( 𝑋 [,] 𝑌 ) ( ( 𝑥 ∈ ( 𝑋 [,] 𝑌 ) ↦ 𝐴 ) ‘ 𝑧 ) ≤ ( ( 𝑥 ∈ ( 𝑋 [,] 𝑌 ) ↦ 𝐴 ) ‘ 𝑦 ) ) ) ∧ ( 𝑛 ∈ ℚ ∧ ( ( ( 𝑥 ∈ ( 𝑋 [,] 𝑌 ) ↦ 𝐴 ) ‘ 𝑦 ) < 𝑛 ∧ 𝑛 < 𝑊 ) ) ) → ∀ 𝑧 ∈ ( 𝑋 [,] 𝑌 ) ( ( 𝑥 ∈ ( 𝑋 [,] 𝑌 ) ↦ 𝐴 ) ‘ 𝑧 ) < 𝑛 ) |
67 |
32 46 66
|
reximssdv |
⊢ ( ( 𝜑 ∧ ( 𝑦 ∈ ( 𝑋 [,] 𝑌 ) ∧ ∀ 𝑧 ∈ ( 𝑋 [,] 𝑌 ) ( ( 𝑥 ∈ ( 𝑋 [,] 𝑌 ) ↦ 𝐴 ) ‘ 𝑧 ) ≤ ( ( 𝑥 ∈ ( 𝑋 [,] 𝑌 ) ↦ 𝐴 ) ‘ 𝑦 ) ) ) → ∃ 𝑛 ∈ ( 𝑍 (,) 𝑊 ) ∀ 𝑧 ∈ ( 𝑋 [,] 𝑌 ) ( ( 𝑥 ∈ ( 𝑋 [,] 𝑌 ) ↦ 𝐴 ) ‘ 𝑧 ) < 𝑛 ) |
68 |
67
|
rexlimdvaa |
⊢ ( 𝜑 → ( ∃ 𝑦 ∈ ( 𝑋 [,] 𝑌 ) ∀ 𝑧 ∈ ( 𝑋 [,] 𝑌 ) ( ( 𝑥 ∈ ( 𝑋 [,] 𝑌 ) ↦ 𝐴 ) ‘ 𝑧 ) ≤ ( ( 𝑥 ∈ ( 𝑋 [,] 𝑌 ) ↦ 𝐴 ) ‘ 𝑦 ) → ∃ 𝑛 ∈ ( 𝑍 (,) 𝑊 ) ∀ 𝑧 ∈ ( 𝑋 [,] 𝑌 ) ( ( 𝑥 ∈ ( 𝑋 [,] 𝑌 ) ↦ 𝐴 ) ‘ 𝑧 ) < 𝑛 ) ) |
69 |
4
|
adantr |
⊢ ( ( 𝜑 ∧ ( 𝑦 ∈ ( 𝑋 [,] 𝑌 ) ∧ ∀ 𝑧 ∈ ( 𝑋 [,] 𝑌 ) ( ( 𝑥 ∈ ( 𝑋 [,] 𝑌 ) ↦ 𝐴 ) ‘ 𝑦 ) ≤ ( ( 𝑥 ∈ ( 𝑋 [,] 𝑌 ) ↦ 𝐴 ) ‘ 𝑧 ) ) ) → 𝑍 ∈ ℝ* ) |
70 |
22
|
adantr |
⊢ ( ( 𝜑 ∧ ( 𝑦 ∈ ( 𝑋 [,] 𝑌 ) ∧ ∀ 𝑧 ∈ ( 𝑋 [,] 𝑌 ) ( ( 𝑥 ∈ ( 𝑋 [,] 𝑌 ) ↦ 𝐴 ) ‘ 𝑦 ) ≤ ( ( 𝑥 ∈ ( 𝑋 [,] 𝑌 ) ↦ 𝐴 ) ‘ 𝑧 ) ) ) → ( 𝑥 ∈ ( 𝑋 [,] 𝑌 ) ↦ 𝐴 ) : ( 𝑋 [,] 𝑌 ) ⟶ ( 𝑍 (,) 𝑊 ) ) |
71 |
|
simprl |
⊢ ( ( 𝜑 ∧ ( 𝑦 ∈ ( 𝑋 [,] 𝑌 ) ∧ ∀ 𝑧 ∈ ( 𝑋 [,] 𝑌 ) ( ( 𝑥 ∈ ( 𝑋 [,] 𝑌 ) ↦ 𝐴 ) ‘ 𝑦 ) ≤ ( ( 𝑥 ∈ ( 𝑋 [,] 𝑌 ) ↦ 𝐴 ) ‘ 𝑧 ) ) ) → 𝑦 ∈ ( 𝑋 [,] 𝑌 ) ) |
72 |
70 71
|
ffvelrnd |
⊢ ( ( 𝜑 ∧ ( 𝑦 ∈ ( 𝑋 [,] 𝑌 ) ∧ ∀ 𝑧 ∈ ( 𝑋 [,] 𝑌 ) ( ( 𝑥 ∈ ( 𝑋 [,] 𝑌 ) ↦ 𝐴 ) ‘ 𝑦 ) ≤ ( ( 𝑥 ∈ ( 𝑋 [,] 𝑌 ) ↦ 𝐴 ) ‘ 𝑧 ) ) ) → ( ( 𝑥 ∈ ( 𝑋 [,] 𝑌 ) ↦ 𝐴 ) ‘ 𝑦 ) ∈ ( 𝑍 (,) 𝑊 ) ) |
73 |
20 72
|
sseldi |
⊢ ( ( 𝜑 ∧ ( 𝑦 ∈ ( 𝑋 [,] 𝑌 ) ∧ ∀ 𝑧 ∈ ( 𝑋 [,] 𝑌 ) ( ( 𝑥 ∈ ( 𝑋 [,] 𝑌 ) ↦ 𝐴 ) ‘ 𝑦 ) ≤ ( ( 𝑥 ∈ ( 𝑋 [,] 𝑌 ) ↦ 𝐴 ) ‘ 𝑧 ) ) ) → ( ( 𝑥 ∈ ( 𝑋 [,] 𝑌 ) ↦ 𝐴 ) ‘ 𝑦 ) ∈ ℝ* ) |
74 |
72 28
|
syl |
⊢ ( ( 𝜑 ∧ ( 𝑦 ∈ ( 𝑋 [,] 𝑌 ) ∧ ∀ 𝑧 ∈ ( 𝑋 [,] 𝑌 ) ( ( 𝑥 ∈ ( 𝑋 [,] 𝑌 ) ↦ 𝐴 ) ‘ 𝑦 ) ≤ ( ( 𝑥 ∈ ( 𝑋 [,] 𝑌 ) ↦ 𝐴 ) ‘ 𝑧 ) ) ) → ( 𝑍 < ( ( 𝑥 ∈ ( 𝑋 [,] 𝑌 ) ↦ 𝐴 ) ‘ 𝑦 ) ∧ ( ( 𝑥 ∈ ( 𝑋 [,] 𝑌 ) ↦ 𝐴 ) ‘ 𝑦 ) < 𝑊 ) ) |
75 |
74
|
simpld |
⊢ ( ( 𝜑 ∧ ( 𝑦 ∈ ( 𝑋 [,] 𝑌 ) ∧ ∀ 𝑧 ∈ ( 𝑋 [,] 𝑌 ) ( ( 𝑥 ∈ ( 𝑋 [,] 𝑌 ) ↦ 𝐴 ) ‘ 𝑦 ) ≤ ( ( 𝑥 ∈ ( 𝑋 [,] 𝑌 ) ↦ 𝐴 ) ‘ 𝑧 ) ) ) → 𝑍 < ( ( 𝑥 ∈ ( 𝑋 [,] 𝑌 ) ↦ 𝐴 ) ‘ 𝑦 ) ) |
76 |
|
qbtwnxr |
⊢ ( ( 𝑍 ∈ ℝ* ∧ ( ( 𝑥 ∈ ( 𝑋 [,] 𝑌 ) ↦ 𝐴 ) ‘ 𝑦 ) ∈ ℝ* ∧ 𝑍 < ( ( 𝑥 ∈ ( 𝑋 [,] 𝑌 ) ↦ 𝐴 ) ‘ 𝑦 ) ) → ∃ 𝑚 ∈ ℚ ( 𝑍 < 𝑚 ∧ 𝑚 < ( ( 𝑥 ∈ ( 𝑋 [,] 𝑌 ) ↦ 𝐴 ) ‘ 𝑦 ) ) ) |
77 |
69 73 75 76
|
syl3anc |
⊢ ( ( 𝜑 ∧ ( 𝑦 ∈ ( 𝑋 [,] 𝑌 ) ∧ ∀ 𝑧 ∈ ( 𝑋 [,] 𝑌 ) ( ( 𝑥 ∈ ( 𝑋 [,] 𝑌 ) ↦ 𝐴 ) ‘ 𝑦 ) ≤ ( ( 𝑥 ∈ ( 𝑋 [,] 𝑌 ) ↦ 𝐴 ) ‘ 𝑧 ) ) ) → ∃ 𝑚 ∈ ℚ ( 𝑍 < 𝑚 ∧ 𝑚 < ( ( 𝑥 ∈ ( 𝑋 [,] 𝑌 ) ↦ 𝐴 ) ‘ 𝑦 ) ) ) |
78 |
|
qre |
⊢ ( 𝑚 ∈ ℚ → 𝑚 ∈ ℝ ) |
79 |
78
|
ad2antrl |
⊢ ( ( ( 𝜑 ∧ ( 𝑦 ∈ ( 𝑋 [,] 𝑌 ) ∧ ∀ 𝑧 ∈ ( 𝑋 [,] 𝑌 ) ( ( 𝑥 ∈ ( 𝑋 [,] 𝑌 ) ↦ 𝐴 ) ‘ 𝑦 ) ≤ ( ( 𝑥 ∈ ( 𝑋 [,] 𝑌 ) ↦ 𝐴 ) ‘ 𝑧 ) ) ) ∧ ( 𝑚 ∈ ℚ ∧ ( 𝑍 < 𝑚 ∧ 𝑚 < ( ( 𝑥 ∈ ( 𝑋 [,] 𝑌 ) ↦ 𝐴 ) ‘ 𝑦 ) ) ) ) → 𝑚 ∈ ℝ ) |
80 |
|
simprrl |
⊢ ( ( ( 𝜑 ∧ ( 𝑦 ∈ ( 𝑋 [,] 𝑌 ) ∧ ∀ 𝑧 ∈ ( 𝑋 [,] 𝑌 ) ( ( 𝑥 ∈ ( 𝑋 [,] 𝑌 ) ↦ 𝐴 ) ‘ 𝑦 ) ≤ ( ( 𝑥 ∈ ( 𝑋 [,] 𝑌 ) ↦ 𝐴 ) ‘ 𝑧 ) ) ) ∧ ( 𝑚 ∈ ℚ ∧ ( 𝑍 < 𝑚 ∧ 𝑚 < ( ( 𝑥 ∈ ( 𝑋 [,] 𝑌 ) ↦ 𝐴 ) ‘ 𝑦 ) ) ) ) → 𝑍 < 𝑚 ) |
81 |
79
|
rexrd |
⊢ ( ( ( 𝜑 ∧ ( 𝑦 ∈ ( 𝑋 [,] 𝑌 ) ∧ ∀ 𝑧 ∈ ( 𝑋 [,] 𝑌 ) ( ( 𝑥 ∈ ( 𝑋 [,] 𝑌 ) ↦ 𝐴 ) ‘ 𝑦 ) ≤ ( ( 𝑥 ∈ ( 𝑋 [,] 𝑌 ) ↦ 𝐴 ) ‘ 𝑧 ) ) ) ∧ ( 𝑚 ∈ ℚ ∧ ( 𝑍 < 𝑚 ∧ 𝑚 < ( ( 𝑥 ∈ ( 𝑋 [,] 𝑌 ) ↦ 𝐴 ) ‘ 𝑦 ) ) ) ) → 𝑚 ∈ ℝ* ) |
82 |
73
|
adantr |
⊢ ( ( ( 𝜑 ∧ ( 𝑦 ∈ ( 𝑋 [,] 𝑌 ) ∧ ∀ 𝑧 ∈ ( 𝑋 [,] 𝑌 ) ( ( 𝑥 ∈ ( 𝑋 [,] 𝑌 ) ↦ 𝐴 ) ‘ 𝑦 ) ≤ ( ( 𝑥 ∈ ( 𝑋 [,] 𝑌 ) ↦ 𝐴 ) ‘ 𝑧 ) ) ) ∧ ( 𝑚 ∈ ℚ ∧ ( 𝑍 < 𝑚 ∧ 𝑚 < ( ( 𝑥 ∈ ( 𝑋 [,] 𝑌 ) ↦ 𝐴 ) ‘ 𝑦 ) ) ) ) → ( ( 𝑥 ∈ ( 𝑋 [,] 𝑌 ) ↦ 𝐴 ) ‘ 𝑦 ) ∈ ℝ* ) |
83 |
5
|
ad2antrr |
⊢ ( ( ( 𝜑 ∧ ( 𝑦 ∈ ( 𝑋 [,] 𝑌 ) ∧ ∀ 𝑧 ∈ ( 𝑋 [,] 𝑌 ) ( ( 𝑥 ∈ ( 𝑋 [,] 𝑌 ) ↦ 𝐴 ) ‘ 𝑦 ) ≤ ( ( 𝑥 ∈ ( 𝑋 [,] 𝑌 ) ↦ 𝐴 ) ‘ 𝑧 ) ) ) ∧ ( 𝑚 ∈ ℚ ∧ ( 𝑍 < 𝑚 ∧ 𝑚 < ( ( 𝑥 ∈ ( 𝑋 [,] 𝑌 ) ↦ 𝐴 ) ‘ 𝑦 ) ) ) ) → 𝑊 ∈ ℝ* ) |
84 |
|
simprrr |
⊢ ( ( ( 𝜑 ∧ ( 𝑦 ∈ ( 𝑋 [,] 𝑌 ) ∧ ∀ 𝑧 ∈ ( 𝑋 [,] 𝑌 ) ( ( 𝑥 ∈ ( 𝑋 [,] 𝑌 ) ↦ 𝐴 ) ‘ 𝑦 ) ≤ ( ( 𝑥 ∈ ( 𝑋 [,] 𝑌 ) ↦ 𝐴 ) ‘ 𝑧 ) ) ) ∧ ( 𝑚 ∈ ℚ ∧ ( 𝑍 < 𝑚 ∧ 𝑚 < ( ( 𝑥 ∈ ( 𝑋 [,] 𝑌 ) ↦ 𝐴 ) ‘ 𝑦 ) ) ) ) → 𝑚 < ( ( 𝑥 ∈ ( 𝑋 [,] 𝑌 ) ↦ 𝐴 ) ‘ 𝑦 ) ) |
85 |
74
|
simprd |
⊢ ( ( 𝜑 ∧ ( 𝑦 ∈ ( 𝑋 [,] 𝑌 ) ∧ ∀ 𝑧 ∈ ( 𝑋 [,] 𝑌 ) ( ( 𝑥 ∈ ( 𝑋 [,] 𝑌 ) ↦ 𝐴 ) ‘ 𝑦 ) ≤ ( ( 𝑥 ∈ ( 𝑋 [,] 𝑌 ) ↦ 𝐴 ) ‘ 𝑧 ) ) ) → ( ( 𝑥 ∈ ( 𝑋 [,] 𝑌 ) ↦ 𝐴 ) ‘ 𝑦 ) < 𝑊 ) |
86 |
85
|
adantr |
⊢ ( ( ( 𝜑 ∧ ( 𝑦 ∈ ( 𝑋 [,] 𝑌 ) ∧ ∀ 𝑧 ∈ ( 𝑋 [,] 𝑌 ) ( ( 𝑥 ∈ ( 𝑋 [,] 𝑌 ) ↦ 𝐴 ) ‘ 𝑦 ) ≤ ( ( 𝑥 ∈ ( 𝑋 [,] 𝑌 ) ↦ 𝐴 ) ‘ 𝑧 ) ) ) ∧ ( 𝑚 ∈ ℚ ∧ ( 𝑍 < 𝑚 ∧ 𝑚 < ( ( 𝑥 ∈ ( 𝑋 [,] 𝑌 ) ↦ 𝐴 ) ‘ 𝑦 ) ) ) ) → ( ( 𝑥 ∈ ( 𝑋 [,] 𝑌 ) ↦ 𝐴 ) ‘ 𝑦 ) < 𝑊 ) |
87 |
81 82 83 84 86
|
xrlttrd |
⊢ ( ( ( 𝜑 ∧ ( 𝑦 ∈ ( 𝑋 [,] 𝑌 ) ∧ ∀ 𝑧 ∈ ( 𝑋 [,] 𝑌 ) ( ( 𝑥 ∈ ( 𝑋 [,] 𝑌 ) ↦ 𝐴 ) ‘ 𝑦 ) ≤ ( ( 𝑥 ∈ ( 𝑋 [,] 𝑌 ) ↦ 𝐴 ) ‘ 𝑧 ) ) ) ∧ ( 𝑚 ∈ ℚ ∧ ( 𝑍 < 𝑚 ∧ 𝑚 < ( ( 𝑥 ∈ ( 𝑋 [,] 𝑌 ) ↦ 𝐴 ) ‘ 𝑦 ) ) ) ) → 𝑚 < 𝑊 ) |
88 |
4
|
ad2antrr |
⊢ ( ( ( 𝜑 ∧ ( 𝑦 ∈ ( 𝑋 [,] 𝑌 ) ∧ ∀ 𝑧 ∈ ( 𝑋 [,] 𝑌 ) ( ( 𝑥 ∈ ( 𝑋 [,] 𝑌 ) ↦ 𝐴 ) ‘ 𝑦 ) ≤ ( ( 𝑥 ∈ ( 𝑋 [,] 𝑌 ) ↦ 𝐴 ) ‘ 𝑧 ) ) ) ∧ ( 𝑚 ∈ ℚ ∧ ( 𝑍 < 𝑚 ∧ 𝑚 < ( ( 𝑥 ∈ ( 𝑋 [,] 𝑌 ) ↦ 𝐴 ) ‘ 𝑦 ) ) ) ) → 𝑍 ∈ ℝ* ) |
89 |
|
elioo2 |
⊢ ( ( 𝑍 ∈ ℝ* ∧ 𝑊 ∈ ℝ* ) → ( 𝑚 ∈ ( 𝑍 (,) 𝑊 ) ↔ ( 𝑚 ∈ ℝ ∧ 𝑍 < 𝑚 ∧ 𝑚 < 𝑊 ) ) ) |
90 |
88 83 89
|
syl2anc |
⊢ ( ( ( 𝜑 ∧ ( 𝑦 ∈ ( 𝑋 [,] 𝑌 ) ∧ ∀ 𝑧 ∈ ( 𝑋 [,] 𝑌 ) ( ( 𝑥 ∈ ( 𝑋 [,] 𝑌 ) ↦ 𝐴 ) ‘ 𝑦 ) ≤ ( ( 𝑥 ∈ ( 𝑋 [,] 𝑌 ) ↦ 𝐴 ) ‘ 𝑧 ) ) ) ∧ ( 𝑚 ∈ ℚ ∧ ( 𝑍 < 𝑚 ∧ 𝑚 < ( ( 𝑥 ∈ ( 𝑋 [,] 𝑌 ) ↦ 𝐴 ) ‘ 𝑦 ) ) ) ) → ( 𝑚 ∈ ( 𝑍 (,) 𝑊 ) ↔ ( 𝑚 ∈ ℝ ∧ 𝑍 < 𝑚 ∧ 𝑚 < 𝑊 ) ) ) |
91 |
79 80 87 90
|
mpbir3and |
⊢ ( ( ( 𝜑 ∧ ( 𝑦 ∈ ( 𝑋 [,] 𝑌 ) ∧ ∀ 𝑧 ∈ ( 𝑋 [,] 𝑌 ) ( ( 𝑥 ∈ ( 𝑋 [,] 𝑌 ) ↦ 𝐴 ) ‘ 𝑦 ) ≤ ( ( 𝑥 ∈ ( 𝑋 [,] 𝑌 ) ↦ 𝐴 ) ‘ 𝑧 ) ) ) ∧ ( 𝑚 ∈ ℚ ∧ ( 𝑍 < 𝑚 ∧ 𝑚 < ( ( 𝑥 ∈ ( 𝑋 [,] 𝑌 ) ↦ 𝐴 ) ‘ 𝑦 ) ) ) ) → 𝑚 ∈ ( 𝑍 (,) 𝑊 ) ) |
92 |
|
anass |
⊢ ( ( ( 𝜑 ∧ 𝑦 ∈ ( 𝑋 [,] 𝑌 ) ) ∧ ∀ 𝑧 ∈ ( 𝑋 [,] 𝑌 ) ( ( 𝑥 ∈ ( 𝑋 [,] 𝑌 ) ↦ 𝐴 ) ‘ 𝑦 ) ≤ ( ( 𝑥 ∈ ( 𝑋 [,] 𝑌 ) ↦ 𝐴 ) ‘ 𝑧 ) ) ↔ ( 𝜑 ∧ ( 𝑦 ∈ ( 𝑋 [,] 𝑌 ) ∧ ∀ 𝑧 ∈ ( 𝑋 [,] 𝑌 ) ( ( 𝑥 ∈ ( 𝑋 [,] 𝑌 ) ↦ 𝐴 ) ‘ 𝑦 ) ≤ ( ( 𝑥 ∈ ( 𝑋 [,] 𝑌 ) ↦ 𝐴 ) ‘ 𝑧 ) ) ) ) |
93 |
|
simprrr |
⊢ ( ( ( 𝜑 ∧ 𝑦 ∈ ( 𝑋 [,] 𝑌 ) ) ∧ ( 𝑚 ∈ ℚ ∧ ( 𝑍 < 𝑚 ∧ 𝑚 < ( ( 𝑥 ∈ ( 𝑋 [,] 𝑌 ) ↦ 𝐴 ) ‘ 𝑦 ) ) ) ) → 𝑚 < ( ( 𝑥 ∈ ( 𝑋 [,] 𝑌 ) ↦ 𝐴 ) ‘ 𝑦 ) ) |
94 |
93
|
adantr |
⊢ ( ( ( ( 𝜑 ∧ 𝑦 ∈ ( 𝑋 [,] 𝑌 ) ) ∧ ( 𝑚 ∈ ℚ ∧ ( 𝑍 < 𝑚 ∧ 𝑚 < ( ( 𝑥 ∈ ( 𝑋 [,] 𝑌 ) ↦ 𝐴 ) ‘ 𝑦 ) ) ) ) ∧ 𝑧 ∈ ( 𝑋 [,] 𝑌 ) ) → 𝑚 < ( ( 𝑥 ∈ ( 𝑋 [,] 𝑌 ) ↦ 𝐴 ) ‘ 𝑦 ) ) |
95 |
78
|
ad2antrl |
⊢ ( ( ( 𝜑 ∧ 𝑦 ∈ ( 𝑋 [,] 𝑌 ) ) ∧ ( 𝑚 ∈ ℚ ∧ ( 𝑍 < 𝑚 ∧ 𝑚 < ( ( 𝑥 ∈ ( 𝑋 [,] 𝑌 ) ↦ 𝐴 ) ‘ 𝑦 ) ) ) ) → 𝑚 ∈ ℝ ) |
96 |
95
|
adantr |
⊢ ( ( ( ( 𝜑 ∧ 𝑦 ∈ ( 𝑋 [,] 𝑌 ) ) ∧ ( 𝑚 ∈ ℚ ∧ ( 𝑍 < 𝑚 ∧ 𝑚 < ( ( 𝑥 ∈ ( 𝑋 [,] 𝑌 ) ↦ 𝐴 ) ‘ 𝑦 ) ) ) ) ∧ 𝑧 ∈ ( 𝑋 [,] 𝑌 ) ) → 𝑚 ∈ ℝ ) |
97 |
96
|
rexrd |
⊢ ( ( ( ( 𝜑 ∧ 𝑦 ∈ ( 𝑋 [,] 𝑌 ) ) ∧ ( 𝑚 ∈ ℚ ∧ ( 𝑍 < 𝑚 ∧ 𝑚 < ( ( 𝑥 ∈ ( 𝑋 [,] 𝑌 ) ↦ 𝐴 ) ‘ 𝑦 ) ) ) ) ∧ 𝑧 ∈ ( 𝑋 [,] 𝑌 ) ) → 𝑚 ∈ ℝ* ) |
98 |
22
|
ad2antrr |
⊢ ( ( ( 𝜑 ∧ 𝑦 ∈ ( 𝑋 [,] 𝑌 ) ) ∧ ( 𝑚 ∈ ℚ ∧ ( 𝑍 < 𝑚 ∧ 𝑚 < ( ( 𝑥 ∈ ( 𝑋 [,] 𝑌 ) ↦ 𝐴 ) ‘ 𝑦 ) ) ) ) → ( 𝑥 ∈ ( 𝑋 [,] 𝑌 ) ↦ 𝐴 ) : ( 𝑋 [,] 𝑌 ) ⟶ ( 𝑍 (,) 𝑊 ) ) |
99 |
|
simplr |
⊢ ( ( ( 𝜑 ∧ 𝑦 ∈ ( 𝑋 [,] 𝑌 ) ) ∧ ( 𝑚 ∈ ℚ ∧ ( 𝑍 < 𝑚 ∧ 𝑚 < ( ( 𝑥 ∈ ( 𝑋 [,] 𝑌 ) ↦ 𝐴 ) ‘ 𝑦 ) ) ) ) → 𝑦 ∈ ( 𝑋 [,] 𝑌 ) ) |
100 |
98 99
|
ffvelrnd |
⊢ ( ( ( 𝜑 ∧ 𝑦 ∈ ( 𝑋 [,] 𝑌 ) ) ∧ ( 𝑚 ∈ ℚ ∧ ( 𝑍 < 𝑚 ∧ 𝑚 < ( ( 𝑥 ∈ ( 𝑋 [,] 𝑌 ) ↦ 𝐴 ) ‘ 𝑦 ) ) ) ) → ( ( 𝑥 ∈ ( 𝑋 [,] 𝑌 ) ↦ 𝐴 ) ‘ 𝑦 ) ∈ ( 𝑍 (,) 𝑊 ) ) |
101 |
20 100
|
sseldi |
⊢ ( ( ( 𝜑 ∧ 𝑦 ∈ ( 𝑋 [,] 𝑌 ) ) ∧ ( 𝑚 ∈ ℚ ∧ ( 𝑍 < 𝑚 ∧ 𝑚 < ( ( 𝑥 ∈ ( 𝑋 [,] 𝑌 ) ↦ 𝐴 ) ‘ 𝑦 ) ) ) ) → ( ( 𝑥 ∈ ( 𝑋 [,] 𝑌 ) ↦ 𝐴 ) ‘ 𝑦 ) ∈ ℝ* ) |
102 |
101
|
adantr |
⊢ ( ( ( ( 𝜑 ∧ 𝑦 ∈ ( 𝑋 [,] 𝑌 ) ) ∧ ( 𝑚 ∈ ℚ ∧ ( 𝑍 < 𝑚 ∧ 𝑚 < ( ( 𝑥 ∈ ( 𝑋 [,] 𝑌 ) ↦ 𝐴 ) ‘ 𝑦 ) ) ) ) ∧ 𝑧 ∈ ( 𝑋 [,] 𝑌 ) ) → ( ( 𝑥 ∈ ( 𝑋 [,] 𝑌 ) ↦ 𝐴 ) ‘ 𝑦 ) ∈ ℝ* ) |
103 |
98
|
ffvelrnda |
⊢ ( ( ( ( 𝜑 ∧ 𝑦 ∈ ( 𝑋 [,] 𝑌 ) ) ∧ ( 𝑚 ∈ ℚ ∧ ( 𝑍 < 𝑚 ∧ 𝑚 < ( ( 𝑥 ∈ ( 𝑋 [,] 𝑌 ) ↦ 𝐴 ) ‘ 𝑦 ) ) ) ) ∧ 𝑧 ∈ ( 𝑋 [,] 𝑌 ) ) → ( ( 𝑥 ∈ ( 𝑋 [,] 𝑌 ) ↦ 𝐴 ) ‘ 𝑧 ) ∈ ( 𝑍 (,) 𝑊 ) ) |
104 |
20 103
|
sseldi |
⊢ ( ( ( ( 𝜑 ∧ 𝑦 ∈ ( 𝑋 [,] 𝑌 ) ) ∧ ( 𝑚 ∈ ℚ ∧ ( 𝑍 < 𝑚 ∧ 𝑚 < ( ( 𝑥 ∈ ( 𝑋 [,] 𝑌 ) ↦ 𝐴 ) ‘ 𝑦 ) ) ) ) ∧ 𝑧 ∈ ( 𝑋 [,] 𝑌 ) ) → ( ( 𝑥 ∈ ( 𝑋 [,] 𝑌 ) ↦ 𝐴 ) ‘ 𝑧 ) ∈ ℝ* ) |
105 |
|
xrltletr |
⊢ ( ( 𝑚 ∈ ℝ* ∧ ( ( 𝑥 ∈ ( 𝑋 [,] 𝑌 ) ↦ 𝐴 ) ‘ 𝑦 ) ∈ ℝ* ∧ ( ( 𝑥 ∈ ( 𝑋 [,] 𝑌 ) ↦ 𝐴 ) ‘ 𝑧 ) ∈ ℝ* ) → ( ( 𝑚 < ( ( 𝑥 ∈ ( 𝑋 [,] 𝑌 ) ↦ 𝐴 ) ‘ 𝑦 ) ∧ ( ( 𝑥 ∈ ( 𝑋 [,] 𝑌 ) ↦ 𝐴 ) ‘ 𝑦 ) ≤ ( ( 𝑥 ∈ ( 𝑋 [,] 𝑌 ) ↦ 𝐴 ) ‘ 𝑧 ) ) → 𝑚 < ( ( 𝑥 ∈ ( 𝑋 [,] 𝑌 ) ↦ 𝐴 ) ‘ 𝑧 ) ) ) |
106 |
97 102 104 105
|
syl3anc |
⊢ ( ( ( ( 𝜑 ∧ 𝑦 ∈ ( 𝑋 [,] 𝑌 ) ) ∧ ( 𝑚 ∈ ℚ ∧ ( 𝑍 < 𝑚 ∧ 𝑚 < ( ( 𝑥 ∈ ( 𝑋 [,] 𝑌 ) ↦ 𝐴 ) ‘ 𝑦 ) ) ) ) ∧ 𝑧 ∈ ( 𝑋 [,] 𝑌 ) ) → ( ( 𝑚 < ( ( 𝑥 ∈ ( 𝑋 [,] 𝑌 ) ↦ 𝐴 ) ‘ 𝑦 ) ∧ ( ( 𝑥 ∈ ( 𝑋 [,] 𝑌 ) ↦ 𝐴 ) ‘ 𝑦 ) ≤ ( ( 𝑥 ∈ ( 𝑋 [,] 𝑌 ) ↦ 𝐴 ) ‘ 𝑧 ) ) → 𝑚 < ( ( 𝑥 ∈ ( 𝑋 [,] 𝑌 ) ↦ 𝐴 ) ‘ 𝑧 ) ) ) |
107 |
94 106
|
mpand |
⊢ ( ( ( ( 𝜑 ∧ 𝑦 ∈ ( 𝑋 [,] 𝑌 ) ) ∧ ( 𝑚 ∈ ℚ ∧ ( 𝑍 < 𝑚 ∧ 𝑚 < ( ( 𝑥 ∈ ( 𝑋 [,] 𝑌 ) ↦ 𝐴 ) ‘ 𝑦 ) ) ) ) ∧ 𝑧 ∈ ( 𝑋 [,] 𝑌 ) ) → ( ( ( 𝑥 ∈ ( 𝑋 [,] 𝑌 ) ↦ 𝐴 ) ‘ 𝑦 ) ≤ ( ( 𝑥 ∈ ( 𝑋 [,] 𝑌 ) ↦ 𝐴 ) ‘ 𝑧 ) → 𝑚 < ( ( 𝑥 ∈ ( 𝑋 [,] 𝑌 ) ↦ 𝐴 ) ‘ 𝑧 ) ) ) |
108 |
107
|
ralimdva |
⊢ ( ( ( 𝜑 ∧ 𝑦 ∈ ( 𝑋 [,] 𝑌 ) ) ∧ ( 𝑚 ∈ ℚ ∧ ( 𝑍 < 𝑚 ∧ 𝑚 < ( ( 𝑥 ∈ ( 𝑋 [,] 𝑌 ) ↦ 𝐴 ) ‘ 𝑦 ) ) ) ) → ( ∀ 𝑧 ∈ ( 𝑋 [,] 𝑌 ) ( ( 𝑥 ∈ ( 𝑋 [,] 𝑌 ) ↦ 𝐴 ) ‘ 𝑦 ) ≤ ( ( 𝑥 ∈ ( 𝑋 [,] 𝑌 ) ↦ 𝐴 ) ‘ 𝑧 ) → ∀ 𝑧 ∈ ( 𝑋 [,] 𝑌 ) 𝑚 < ( ( 𝑥 ∈ ( 𝑋 [,] 𝑌 ) ↦ 𝐴 ) ‘ 𝑧 ) ) ) |
109 |
108
|
imp |
⊢ ( ( ( ( 𝜑 ∧ 𝑦 ∈ ( 𝑋 [,] 𝑌 ) ) ∧ ( 𝑚 ∈ ℚ ∧ ( 𝑍 < 𝑚 ∧ 𝑚 < ( ( 𝑥 ∈ ( 𝑋 [,] 𝑌 ) ↦ 𝐴 ) ‘ 𝑦 ) ) ) ) ∧ ∀ 𝑧 ∈ ( 𝑋 [,] 𝑌 ) ( ( 𝑥 ∈ ( 𝑋 [,] 𝑌 ) ↦ 𝐴 ) ‘ 𝑦 ) ≤ ( ( 𝑥 ∈ ( 𝑋 [,] 𝑌 ) ↦ 𝐴 ) ‘ 𝑧 ) ) → ∀ 𝑧 ∈ ( 𝑋 [,] 𝑌 ) 𝑚 < ( ( 𝑥 ∈ ( 𝑋 [,] 𝑌 ) ↦ 𝐴 ) ‘ 𝑧 ) ) |
110 |
109
|
an32s |
⊢ ( ( ( ( 𝜑 ∧ 𝑦 ∈ ( 𝑋 [,] 𝑌 ) ) ∧ ∀ 𝑧 ∈ ( 𝑋 [,] 𝑌 ) ( ( 𝑥 ∈ ( 𝑋 [,] 𝑌 ) ↦ 𝐴 ) ‘ 𝑦 ) ≤ ( ( 𝑥 ∈ ( 𝑋 [,] 𝑌 ) ↦ 𝐴 ) ‘ 𝑧 ) ) ∧ ( 𝑚 ∈ ℚ ∧ ( 𝑍 < 𝑚 ∧ 𝑚 < ( ( 𝑥 ∈ ( 𝑋 [,] 𝑌 ) ↦ 𝐴 ) ‘ 𝑦 ) ) ) ) → ∀ 𝑧 ∈ ( 𝑋 [,] 𝑌 ) 𝑚 < ( ( 𝑥 ∈ ( 𝑋 [,] 𝑌 ) ↦ 𝐴 ) ‘ 𝑧 ) ) |
111 |
92 110
|
sylanbr |
⊢ ( ( ( 𝜑 ∧ ( 𝑦 ∈ ( 𝑋 [,] 𝑌 ) ∧ ∀ 𝑧 ∈ ( 𝑋 [,] 𝑌 ) ( ( 𝑥 ∈ ( 𝑋 [,] 𝑌 ) ↦ 𝐴 ) ‘ 𝑦 ) ≤ ( ( 𝑥 ∈ ( 𝑋 [,] 𝑌 ) ↦ 𝐴 ) ‘ 𝑧 ) ) ) ∧ ( 𝑚 ∈ ℚ ∧ ( 𝑍 < 𝑚 ∧ 𝑚 < ( ( 𝑥 ∈ ( 𝑋 [,] 𝑌 ) ↦ 𝐴 ) ‘ 𝑦 ) ) ) ) → ∀ 𝑧 ∈ ( 𝑋 [,] 𝑌 ) 𝑚 < ( ( 𝑥 ∈ ( 𝑋 [,] 𝑌 ) ↦ 𝐴 ) ‘ 𝑧 ) ) |
112 |
77 91 111
|
reximssdv |
⊢ ( ( 𝜑 ∧ ( 𝑦 ∈ ( 𝑋 [,] 𝑌 ) ∧ ∀ 𝑧 ∈ ( 𝑋 [,] 𝑌 ) ( ( 𝑥 ∈ ( 𝑋 [,] 𝑌 ) ↦ 𝐴 ) ‘ 𝑦 ) ≤ ( ( 𝑥 ∈ ( 𝑋 [,] 𝑌 ) ↦ 𝐴 ) ‘ 𝑧 ) ) ) → ∃ 𝑚 ∈ ( 𝑍 (,) 𝑊 ) ∀ 𝑧 ∈ ( 𝑋 [,] 𝑌 ) 𝑚 < ( ( 𝑥 ∈ ( 𝑋 [,] 𝑌 ) ↦ 𝐴 ) ‘ 𝑧 ) ) |
113 |
112
|
rexlimdvaa |
⊢ ( 𝜑 → ( ∃ 𝑦 ∈ ( 𝑋 [,] 𝑌 ) ∀ 𝑧 ∈ ( 𝑋 [,] 𝑌 ) ( ( 𝑥 ∈ ( 𝑋 [,] 𝑌 ) ↦ 𝐴 ) ‘ 𝑦 ) ≤ ( ( 𝑥 ∈ ( 𝑋 [,] 𝑌 ) ↦ 𝐴 ) ‘ 𝑧 ) → ∃ 𝑚 ∈ ( 𝑍 (,) 𝑊 ) ∀ 𝑧 ∈ ( 𝑋 [,] 𝑌 ) 𝑚 < ( ( 𝑥 ∈ ( 𝑋 [,] 𝑌 ) ↦ 𝐴 ) ‘ 𝑧 ) ) ) |
114 |
|
ancom |
⊢ ( ( ∃ 𝑛 ∈ ( 𝑍 (,) 𝑊 ) ∀ 𝑧 ∈ ( 𝑋 [,] 𝑌 ) ( ( 𝑥 ∈ ( 𝑋 [,] 𝑌 ) ↦ 𝐴 ) ‘ 𝑧 ) < 𝑛 ∧ ∃ 𝑚 ∈ ( 𝑍 (,) 𝑊 ) ∀ 𝑧 ∈ ( 𝑋 [,] 𝑌 ) 𝑚 < ( ( 𝑥 ∈ ( 𝑋 [,] 𝑌 ) ↦ 𝐴 ) ‘ 𝑧 ) ) ↔ ( ∃ 𝑚 ∈ ( 𝑍 (,) 𝑊 ) ∀ 𝑧 ∈ ( 𝑋 [,] 𝑌 ) 𝑚 < ( ( 𝑥 ∈ ( 𝑋 [,] 𝑌 ) ↦ 𝐴 ) ‘ 𝑧 ) ∧ ∃ 𝑛 ∈ ( 𝑍 (,) 𝑊 ) ∀ 𝑧 ∈ ( 𝑋 [,] 𝑌 ) ( ( 𝑥 ∈ ( 𝑋 [,] 𝑌 ) ↦ 𝐴 ) ‘ 𝑧 ) < 𝑛 ) ) |
115 |
|
reeanv |
⊢ ( ∃ 𝑚 ∈ ( 𝑍 (,) 𝑊 ) ∃ 𝑛 ∈ ( 𝑍 (,) 𝑊 ) ( ∀ 𝑧 ∈ ( 𝑋 [,] 𝑌 ) 𝑚 < ( ( 𝑥 ∈ ( 𝑋 [,] 𝑌 ) ↦ 𝐴 ) ‘ 𝑧 ) ∧ ∀ 𝑧 ∈ ( 𝑋 [,] 𝑌 ) ( ( 𝑥 ∈ ( 𝑋 [,] 𝑌 ) ↦ 𝐴 ) ‘ 𝑧 ) < 𝑛 ) ↔ ( ∃ 𝑚 ∈ ( 𝑍 (,) 𝑊 ) ∀ 𝑧 ∈ ( 𝑋 [,] 𝑌 ) 𝑚 < ( ( 𝑥 ∈ ( 𝑋 [,] 𝑌 ) ↦ 𝐴 ) ‘ 𝑧 ) ∧ ∃ 𝑛 ∈ ( 𝑍 (,) 𝑊 ) ∀ 𝑧 ∈ ( 𝑋 [,] 𝑌 ) ( ( 𝑥 ∈ ( 𝑋 [,] 𝑌 ) ↦ 𝐴 ) ‘ 𝑧 ) < 𝑛 ) ) |
116 |
114 115
|
bitr4i |
⊢ ( ( ∃ 𝑛 ∈ ( 𝑍 (,) 𝑊 ) ∀ 𝑧 ∈ ( 𝑋 [,] 𝑌 ) ( ( 𝑥 ∈ ( 𝑋 [,] 𝑌 ) ↦ 𝐴 ) ‘ 𝑧 ) < 𝑛 ∧ ∃ 𝑚 ∈ ( 𝑍 (,) 𝑊 ) ∀ 𝑧 ∈ ( 𝑋 [,] 𝑌 ) 𝑚 < ( ( 𝑥 ∈ ( 𝑋 [,] 𝑌 ) ↦ 𝐴 ) ‘ 𝑧 ) ) ↔ ∃ 𝑚 ∈ ( 𝑍 (,) 𝑊 ) ∃ 𝑛 ∈ ( 𝑍 (,) 𝑊 ) ( ∀ 𝑧 ∈ ( 𝑋 [,] 𝑌 ) 𝑚 < ( ( 𝑥 ∈ ( 𝑋 [,] 𝑌 ) ↦ 𝐴 ) ‘ 𝑧 ) ∧ ∀ 𝑧 ∈ ( 𝑋 [,] 𝑌 ) ( ( 𝑥 ∈ ( 𝑋 [,] 𝑌 ) ↦ 𝐴 ) ‘ 𝑧 ) < 𝑛 ) ) |
117 |
|
r19.26 |
⊢ ( ∀ 𝑧 ∈ ( 𝑋 [,] 𝑌 ) ( 𝑚 < ( ( 𝑥 ∈ ( 𝑋 [,] 𝑌 ) ↦ 𝐴 ) ‘ 𝑧 ) ∧ ( ( 𝑥 ∈ ( 𝑋 [,] 𝑌 ) ↦ 𝐴 ) ‘ 𝑧 ) < 𝑛 ) ↔ ( ∀ 𝑧 ∈ ( 𝑋 [,] 𝑌 ) 𝑚 < ( ( 𝑥 ∈ ( 𝑋 [,] 𝑌 ) ↦ 𝐴 ) ‘ 𝑧 ) ∧ ∀ 𝑧 ∈ ( 𝑋 [,] 𝑌 ) ( ( 𝑥 ∈ ( 𝑋 [,] 𝑌 ) ↦ 𝐴 ) ‘ 𝑧 ) < 𝑛 ) ) |
118 |
22
|
adantr |
⊢ ( ( 𝜑 ∧ ( 𝑚 ∈ ( 𝑍 (,) 𝑊 ) ∧ 𝑛 ∈ ( 𝑍 (,) 𝑊 ) ) ) → ( 𝑥 ∈ ( 𝑋 [,] 𝑌 ) ↦ 𝐴 ) : ( 𝑋 [,] 𝑌 ) ⟶ ( 𝑍 (,) 𝑊 ) ) |
119 |
118
|
ffvelrnda |
⊢ ( ( ( 𝜑 ∧ ( 𝑚 ∈ ( 𝑍 (,) 𝑊 ) ∧ 𝑛 ∈ ( 𝑍 (,) 𝑊 ) ) ) ∧ 𝑧 ∈ ( 𝑋 [,] 𝑌 ) ) → ( ( 𝑥 ∈ ( 𝑋 [,] 𝑌 ) ↦ 𝐴 ) ‘ 𝑧 ) ∈ ( 𝑍 (,) 𝑊 ) ) |
120 |
13 119
|
sseldi |
⊢ ( ( ( 𝜑 ∧ ( 𝑚 ∈ ( 𝑍 (,) 𝑊 ) ∧ 𝑛 ∈ ( 𝑍 (,) 𝑊 ) ) ) ∧ 𝑧 ∈ ( 𝑋 [,] 𝑌 ) ) → ( ( 𝑥 ∈ ( 𝑋 [,] 𝑌 ) ↦ 𝐴 ) ‘ 𝑧 ) ∈ ℝ ) |
121 |
120
|
3biant1d |
⊢ ( ( ( 𝜑 ∧ ( 𝑚 ∈ ( 𝑍 (,) 𝑊 ) ∧ 𝑛 ∈ ( 𝑍 (,) 𝑊 ) ) ) ∧ 𝑧 ∈ ( 𝑋 [,] 𝑌 ) ) → ( ( 𝑚 < ( ( 𝑥 ∈ ( 𝑋 [,] 𝑌 ) ↦ 𝐴 ) ‘ 𝑧 ) ∧ ( ( 𝑥 ∈ ( 𝑋 [,] 𝑌 ) ↦ 𝐴 ) ‘ 𝑧 ) < 𝑛 ) ↔ ( ( ( 𝑥 ∈ ( 𝑋 [,] 𝑌 ) ↦ 𝐴 ) ‘ 𝑧 ) ∈ ℝ ∧ 𝑚 < ( ( 𝑥 ∈ ( 𝑋 [,] 𝑌 ) ↦ 𝐴 ) ‘ 𝑧 ) ∧ ( ( 𝑥 ∈ ( 𝑋 [,] 𝑌 ) ↦ 𝐴 ) ‘ 𝑧 ) < 𝑛 ) ) ) |
122 |
|
simplrl |
⊢ ( ( ( 𝜑 ∧ ( 𝑚 ∈ ( 𝑍 (,) 𝑊 ) ∧ 𝑛 ∈ ( 𝑍 (,) 𝑊 ) ) ) ∧ 𝑧 ∈ ( 𝑋 [,] 𝑌 ) ) → 𝑚 ∈ ( 𝑍 (,) 𝑊 ) ) |
123 |
20 122
|
sseldi |
⊢ ( ( ( 𝜑 ∧ ( 𝑚 ∈ ( 𝑍 (,) 𝑊 ) ∧ 𝑛 ∈ ( 𝑍 (,) 𝑊 ) ) ) ∧ 𝑧 ∈ ( 𝑋 [,] 𝑌 ) ) → 𝑚 ∈ ℝ* ) |
124 |
|
simplrr |
⊢ ( ( ( 𝜑 ∧ ( 𝑚 ∈ ( 𝑍 (,) 𝑊 ) ∧ 𝑛 ∈ ( 𝑍 (,) 𝑊 ) ) ) ∧ 𝑧 ∈ ( 𝑋 [,] 𝑌 ) ) → 𝑛 ∈ ( 𝑍 (,) 𝑊 ) ) |
125 |
20 124
|
sseldi |
⊢ ( ( ( 𝜑 ∧ ( 𝑚 ∈ ( 𝑍 (,) 𝑊 ) ∧ 𝑛 ∈ ( 𝑍 (,) 𝑊 ) ) ) ∧ 𝑧 ∈ ( 𝑋 [,] 𝑌 ) ) → 𝑛 ∈ ℝ* ) |
126 |
|
elioo2 |
⊢ ( ( 𝑚 ∈ ℝ* ∧ 𝑛 ∈ ℝ* ) → ( ( ( 𝑥 ∈ ( 𝑋 [,] 𝑌 ) ↦ 𝐴 ) ‘ 𝑧 ) ∈ ( 𝑚 (,) 𝑛 ) ↔ ( ( ( 𝑥 ∈ ( 𝑋 [,] 𝑌 ) ↦ 𝐴 ) ‘ 𝑧 ) ∈ ℝ ∧ 𝑚 < ( ( 𝑥 ∈ ( 𝑋 [,] 𝑌 ) ↦ 𝐴 ) ‘ 𝑧 ) ∧ ( ( 𝑥 ∈ ( 𝑋 [,] 𝑌 ) ↦ 𝐴 ) ‘ 𝑧 ) < 𝑛 ) ) ) |
127 |
123 125 126
|
syl2anc |
⊢ ( ( ( 𝜑 ∧ ( 𝑚 ∈ ( 𝑍 (,) 𝑊 ) ∧ 𝑛 ∈ ( 𝑍 (,) 𝑊 ) ) ) ∧ 𝑧 ∈ ( 𝑋 [,] 𝑌 ) ) → ( ( ( 𝑥 ∈ ( 𝑋 [,] 𝑌 ) ↦ 𝐴 ) ‘ 𝑧 ) ∈ ( 𝑚 (,) 𝑛 ) ↔ ( ( ( 𝑥 ∈ ( 𝑋 [,] 𝑌 ) ↦ 𝐴 ) ‘ 𝑧 ) ∈ ℝ ∧ 𝑚 < ( ( 𝑥 ∈ ( 𝑋 [,] 𝑌 ) ↦ 𝐴 ) ‘ 𝑧 ) ∧ ( ( 𝑥 ∈ ( 𝑋 [,] 𝑌 ) ↦ 𝐴 ) ‘ 𝑧 ) < 𝑛 ) ) ) |
128 |
121 127
|
bitr4d |
⊢ ( ( ( 𝜑 ∧ ( 𝑚 ∈ ( 𝑍 (,) 𝑊 ) ∧ 𝑛 ∈ ( 𝑍 (,) 𝑊 ) ) ) ∧ 𝑧 ∈ ( 𝑋 [,] 𝑌 ) ) → ( ( 𝑚 < ( ( 𝑥 ∈ ( 𝑋 [,] 𝑌 ) ↦ 𝐴 ) ‘ 𝑧 ) ∧ ( ( 𝑥 ∈ ( 𝑋 [,] 𝑌 ) ↦ 𝐴 ) ‘ 𝑧 ) < 𝑛 ) ↔ ( ( 𝑥 ∈ ( 𝑋 [,] 𝑌 ) ↦ 𝐴 ) ‘ 𝑧 ) ∈ ( 𝑚 (,) 𝑛 ) ) ) |
129 |
128
|
ralbidva |
⊢ ( ( 𝜑 ∧ ( 𝑚 ∈ ( 𝑍 (,) 𝑊 ) ∧ 𝑛 ∈ ( 𝑍 (,) 𝑊 ) ) ) → ( ∀ 𝑧 ∈ ( 𝑋 [,] 𝑌 ) ( 𝑚 < ( ( 𝑥 ∈ ( 𝑋 [,] 𝑌 ) ↦ 𝐴 ) ‘ 𝑧 ) ∧ ( ( 𝑥 ∈ ( 𝑋 [,] 𝑌 ) ↦ 𝐴 ) ‘ 𝑧 ) < 𝑛 ) ↔ ∀ 𝑧 ∈ ( 𝑋 [,] 𝑌 ) ( ( 𝑥 ∈ ( 𝑋 [,] 𝑌 ) ↦ 𝐴 ) ‘ 𝑧 ) ∈ ( 𝑚 (,) 𝑛 ) ) ) |
130 |
|
nffvmpt1 |
⊢ Ⅎ 𝑥 ( ( 𝑥 ∈ ( 𝑋 [,] 𝑌 ) ↦ 𝐴 ) ‘ 𝑧 ) |
131 |
130
|
nfel1 |
⊢ Ⅎ 𝑥 ( ( 𝑥 ∈ ( 𝑋 [,] 𝑌 ) ↦ 𝐴 ) ‘ 𝑧 ) ∈ ( 𝑚 (,) 𝑛 ) |
132 |
|
nfv |
⊢ Ⅎ 𝑧 ( ( 𝑥 ∈ ( 𝑋 [,] 𝑌 ) ↦ 𝐴 ) ‘ 𝑥 ) ∈ ( 𝑚 (,) 𝑛 ) |
133 |
|
fveq2 |
⊢ ( 𝑧 = 𝑥 → ( ( 𝑥 ∈ ( 𝑋 [,] 𝑌 ) ↦ 𝐴 ) ‘ 𝑧 ) = ( ( 𝑥 ∈ ( 𝑋 [,] 𝑌 ) ↦ 𝐴 ) ‘ 𝑥 ) ) |
134 |
133
|
eleq1d |
⊢ ( 𝑧 = 𝑥 → ( ( ( 𝑥 ∈ ( 𝑋 [,] 𝑌 ) ↦ 𝐴 ) ‘ 𝑧 ) ∈ ( 𝑚 (,) 𝑛 ) ↔ ( ( 𝑥 ∈ ( 𝑋 [,] 𝑌 ) ↦ 𝐴 ) ‘ 𝑥 ) ∈ ( 𝑚 (,) 𝑛 ) ) ) |
135 |
131 132 134
|
cbvralw |
⊢ ( ∀ 𝑧 ∈ ( 𝑋 [,] 𝑌 ) ( ( 𝑥 ∈ ( 𝑋 [,] 𝑌 ) ↦ 𝐴 ) ‘ 𝑧 ) ∈ ( 𝑚 (,) 𝑛 ) ↔ ∀ 𝑥 ∈ ( 𝑋 [,] 𝑌 ) ( ( 𝑥 ∈ ( 𝑋 [,] 𝑌 ) ↦ 𝐴 ) ‘ 𝑥 ) ∈ ( 𝑚 (,) 𝑛 ) ) |
136 |
|
simpr |
⊢ ( ( 𝜑 ∧ 𝑥 ∈ ( 𝑋 [,] 𝑌 ) ) → 𝑥 ∈ ( 𝑋 [,] 𝑌 ) ) |
137 |
22
|
fvmptelrn |
⊢ ( ( 𝜑 ∧ 𝑥 ∈ ( 𝑋 [,] 𝑌 ) ) → 𝐴 ∈ ( 𝑍 (,) 𝑊 ) ) |
138 |
|
eqid |
⊢ ( 𝑥 ∈ ( 𝑋 [,] 𝑌 ) ↦ 𝐴 ) = ( 𝑥 ∈ ( 𝑋 [,] 𝑌 ) ↦ 𝐴 ) |
139 |
138
|
fvmpt2 |
⊢ ( ( 𝑥 ∈ ( 𝑋 [,] 𝑌 ) ∧ 𝐴 ∈ ( 𝑍 (,) 𝑊 ) ) → ( ( 𝑥 ∈ ( 𝑋 [,] 𝑌 ) ↦ 𝐴 ) ‘ 𝑥 ) = 𝐴 ) |
140 |
136 137 139
|
syl2anc |
⊢ ( ( 𝜑 ∧ 𝑥 ∈ ( 𝑋 [,] 𝑌 ) ) → ( ( 𝑥 ∈ ( 𝑋 [,] 𝑌 ) ↦ 𝐴 ) ‘ 𝑥 ) = 𝐴 ) |
141 |
140
|
eleq1d |
⊢ ( ( 𝜑 ∧ 𝑥 ∈ ( 𝑋 [,] 𝑌 ) ) → ( ( ( 𝑥 ∈ ( 𝑋 [,] 𝑌 ) ↦ 𝐴 ) ‘ 𝑥 ) ∈ ( 𝑚 (,) 𝑛 ) ↔ 𝐴 ∈ ( 𝑚 (,) 𝑛 ) ) ) |
142 |
141
|
ralbidva |
⊢ ( 𝜑 → ( ∀ 𝑥 ∈ ( 𝑋 [,] 𝑌 ) ( ( 𝑥 ∈ ( 𝑋 [,] 𝑌 ) ↦ 𝐴 ) ‘ 𝑥 ) ∈ ( 𝑚 (,) 𝑛 ) ↔ ∀ 𝑥 ∈ ( 𝑋 [,] 𝑌 ) 𝐴 ∈ ( 𝑚 (,) 𝑛 ) ) ) |
143 |
135 142
|
syl5bb |
⊢ ( 𝜑 → ( ∀ 𝑧 ∈ ( 𝑋 [,] 𝑌 ) ( ( 𝑥 ∈ ( 𝑋 [,] 𝑌 ) ↦ 𝐴 ) ‘ 𝑧 ) ∈ ( 𝑚 (,) 𝑛 ) ↔ ∀ 𝑥 ∈ ( 𝑋 [,] 𝑌 ) 𝐴 ∈ ( 𝑚 (,) 𝑛 ) ) ) |
144 |
143
|
adantr |
⊢ ( ( 𝜑 ∧ ( 𝑚 ∈ ( 𝑍 (,) 𝑊 ) ∧ 𝑛 ∈ ( 𝑍 (,) 𝑊 ) ) ) → ( ∀ 𝑧 ∈ ( 𝑋 [,] 𝑌 ) ( ( 𝑥 ∈ ( 𝑋 [,] 𝑌 ) ↦ 𝐴 ) ‘ 𝑧 ) ∈ ( 𝑚 (,) 𝑛 ) ↔ ∀ 𝑥 ∈ ( 𝑋 [,] 𝑌 ) 𝐴 ∈ ( 𝑚 (,) 𝑛 ) ) ) |
145 |
1
|
adantr |
⊢ ( ( 𝜑 ∧ ( ( 𝑚 ∈ ( 𝑍 (,) 𝑊 ) ∧ 𝑛 ∈ ( 𝑍 (,) 𝑊 ) ) ∧ ∀ 𝑥 ∈ ( 𝑋 [,] 𝑌 ) 𝐴 ∈ ( 𝑚 (,) 𝑛 ) ) ) → 𝑋 ∈ ℝ ) |
146 |
2
|
adantr |
⊢ ( ( 𝜑 ∧ ( ( 𝑚 ∈ ( 𝑍 (,) 𝑊 ) ∧ 𝑛 ∈ ( 𝑍 (,) 𝑊 ) ) ∧ ∀ 𝑥 ∈ ( 𝑋 [,] 𝑌 ) 𝐴 ∈ ( 𝑚 (,) 𝑛 ) ) ) → 𝑌 ∈ ℝ ) |
147 |
3
|
adantr |
⊢ ( ( 𝜑 ∧ ( ( 𝑚 ∈ ( 𝑍 (,) 𝑊 ) ∧ 𝑛 ∈ ( 𝑍 (,) 𝑊 ) ) ∧ ∀ 𝑥 ∈ ( 𝑋 [,] 𝑌 ) 𝐴 ∈ ( 𝑚 (,) 𝑛 ) ) ) → 𝑋 ≤ 𝑌 ) |
148 |
4
|
adantr |
⊢ ( ( 𝜑 ∧ ( ( 𝑚 ∈ ( 𝑍 (,) 𝑊 ) ∧ 𝑛 ∈ ( 𝑍 (,) 𝑊 ) ) ∧ ∀ 𝑥 ∈ ( 𝑋 [,] 𝑌 ) 𝐴 ∈ ( 𝑚 (,) 𝑛 ) ) ) → 𝑍 ∈ ℝ* ) |
149 |
5
|
adantr |
⊢ ( ( 𝜑 ∧ ( ( 𝑚 ∈ ( 𝑍 (,) 𝑊 ) ∧ 𝑛 ∈ ( 𝑍 (,) 𝑊 ) ) ∧ ∀ 𝑥 ∈ ( 𝑋 [,] 𝑌 ) 𝐴 ∈ ( 𝑚 (,) 𝑛 ) ) ) → 𝑊 ∈ ℝ* ) |
150 |
|
nfcv |
⊢ Ⅎ 𝑦 𝐴 |
151 |
|
nfcsb1v |
⊢ Ⅎ 𝑥 ⦋ 𝑦 / 𝑥 ⦌ 𝐴 |
152 |
|
csbeq1a |
⊢ ( 𝑥 = 𝑦 → 𝐴 = ⦋ 𝑦 / 𝑥 ⦌ 𝐴 ) |
153 |
150 151 152
|
cbvmpt |
⊢ ( 𝑥 ∈ ( 𝑋 [,] 𝑌 ) ↦ 𝐴 ) = ( 𝑦 ∈ ( 𝑋 [,] 𝑌 ) ↦ ⦋ 𝑦 / 𝑥 ⦌ 𝐴 ) |
154 |
153 6
|
eqeltrrid |
⊢ ( 𝜑 → ( 𝑦 ∈ ( 𝑋 [,] 𝑌 ) ↦ ⦋ 𝑦 / 𝑥 ⦌ 𝐴 ) ∈ ( ( 𝑋 [,] 𝑌 ) –cn→ ( 𝑍 (,) 𝑊 ) ) ) |
155 |
154
|
adantr |
⊢ ( ( 𝜑 ∧ ( ( 𝑚 ∈ ( 𝑍 (,) 𝑊 ) ∧ 𝑛 ∈ ( 𝑍 (,) 𝑊 ) ) ∧ ∀ 𝑥 ∈ ( 𝑋 [,] 𝑌 ) 𝐴 ∈ ( 𝑚 (,) 𝑛 ) ) ) → ( 𝑦 ∈ ( 𝑋 [,] 𝑌 ) ↦ ⦋ 𝑦 / 𝑥 ⦌ 𝐴 ) ∈ ( ( 𝑋 [,] 𝑌 ) –cn→ ( 𝑍 (,) 𝑊 ) ) ) |
156 |
|
nfcv |
⊢ Ⅎ 𝑦 𝐵 |
157 |
|
nfcsb1v |
⊢ Ⅎ 𝑥 ⦋ 𝑦 / 𝑥 ⦌ 𝐵 |
158 |
|
csbeq1a |
⊢ ( 𝑥 = 𝑦 → 𝐵 = ⦋ 𝑦 / 𝑥 ⦌ 𝐵 ) |
159 |
156 157 158
|
cbvmpt |
⊢ ( 𝑥 ∈ ( 𝑋 (,) 𝑌 ) ↦ 𝐵 ) = ( 𝑦 ∈ ( 𝑋 (,) 𝑌 ) ↦ ⦋ 𝑦 / 𝑥 ⦌ 𝐵 ) |
160 |
159 7
|
eqeltrrid |
⊢ ( 𝜑 → ( 𝑦 ∈ ( 𝑋 (,) 𝑌 ) ↦ ⦋ 𝑦 / 𝑥 ⦌ 𝐵 ) ∈ ( ( ( 𝑋 (,) 𝑌 ) –cn→ ℂ ) ∩ 𝐿1 ) ) |
161 |
160
|
adantr |
⊢ ( ( 𝜑 ∧ ( ( 𝑚 ∈ ( 𝑍 (,) 𝑊 ) ∧ 𝑛 ∈ ( 𝑍 (,) 𝑊 ) ) ∧ ∀ 𝑥 ∈ ( 𝑋 [,] 𝑌 ) 𝐴 ∈ ( 𝑚 (,) 𝑛 ) ) ) → ( 𝑦 ∈ ( 𝑋 (,) 𝑌 ) ↦ ⦋ 𝑦 / 𝑥 ⦌ 𝐵 ) ∈ ( ( ( 𝑋 (,) 𝑌 ) –cn→ ℂ ) ∩ 𝐿1 ) ) |
162 |
|
nfcv |
⊢ Ⅎ 𝑣 𝐶 |
163 |
|
nfcsb1v |
⊢ Ⅎ 𝑢 ⦋ 𝑣 / 𝑢 ⦌ 𝐶 |
164 |
|
csbeq1a |
⊢ ( 𝑢 = 𝑣 → 𝐶 = ⦋ 𝑣 / 𝑢 ⦌ 𝐶 ) |
165 |
162 163 164
|
cbvmpt |
⊢ ( 𝑢 ∈ ( 𝑍 (,) 𝑊 ) ↦ 𝐶 ) = ( 𝑣 ∈ ( 𝑍 (,) 𝑊 ) ↦ ⦋ 𝑣 / 𝑢 ⦌ 𝐶 ) |
166 |
165 8
|
eqeltrrid |
⊢ ( 𝜑 → ( 𝑣 ∈ ( 𝑍 (,) 𝑊 ) ↦ ⦋ 𝑣 / 𝑢 ⦌ 𝐶 ) ∈ ( ( 𝑍 (,) 𝑊 ) –cn→ ℂ ) ) |
167 |
166
|
adantr |
⊢ ( ( 𝜑 ∧ ( ( 𝑚 ∈ ( 𝑍 (,) 𝑊 ) ∧ 𝑛 ∈ ( 𝑍 (,) 𝑊 ) ) ∧ ∀ 𝑥 ∈ ( 𝑋 [,] 𝑌 ) 𝐴 ∈ ( 𝑚 (,) 𝑛 ) ) ) → ( 𝑣 ∈ ( 𝑍 (,) 𝑊 ) ↦ ⦋ 𝑣 / 𝑢 ⦌ 𝐶 ) ∈ ( ( 𝑍 (,) 𝑊 ) –cn→ ℂ ) ) |
168 |
153
|
oveq2i |
⊢ ( ℝ D ( 𝑥 ∈ ( 𝑋 [,] 𝑌 ) ↦ 𝐴 ) ) = ( ℝ D ( 𝑦 ∈ ( 𝑋 [,] 𝑌 ) ↦ ⦋ 𝑦 / 𝑥 ⦌ 𝐴 ) ) |
169 |
9 168 159
|
3eqtr3g |
⊢ ( 𝜑 → ( ℝ D ( 𝑦 ∈ ( 𝑋 [,] 𝑌 ) ↦ ⦋ 𝑦 / 𝑥 ⦌ 𝐴 ) ) = ( 𝑦 ∈ ( 𝑋 (,) 𝑌 ) ↦ ⦋ 𝑦 / 𝑥 ⦌ 𝐵 ) ) |
170 |
169
|
adantr |
⊢ ( ( 𝜑 ∧ ( ( 𝑚 ∈ ( 𝑍 (,) 𝑊 ) ∧ 𝑛 ∈ ( 𝑍 (,) 𝑊 ) ) ∧ ∀ 𝑥 ∈ ( 𝑋 [,] 𝑌 ) 𝐴 ∈ ( 𝑚 (,) 𝑛 ) ) ) → ( ℝ D ( 𝑦 ∈ ( 𝑋 [,] 𝑌 ) ↦ ⦋ 𝑦 / 𝑥 ⦌ 𝐴 ) ) = ( 𝑦 ∈ ( 𝑋 (,) 𝑌 ) ↦ ⦋ 𝑦 / 𝑥 ⦌ 𝐵 ) ) |
171 |
|
csbeq1 |
⊢ ( 𝑣 = ⦋ 𝑦 / 𝑥 ⦌ 𝐴 → ⦋ 𝑣 / 𝑢 ⦌ 𝐶 = ⦋ ⦋ 𝑦 / 𝑥 ⦌ 𝐴 / 𝑢 ⦌ 𝐶 ) |
172 |
|
csbeq1 |
⊢ ( 𝑦 = 𝑋 → ⦋ 𝑦 / 𝑥 ⦌ 𝐴 = ⦋ 𝑋 / 𝑥 ⦌ 𝐴 ) |
173 |
|
csbeq1 |
⊢ ( 𝑦 = 𝑌 → ⦋ 𝑦 / 𝑥 ⦌ 𝐴 = ⦋ 𝑌 / 𝑥 ⦌ 𝐴 ) |
174 |
|
simprll |
⊢ ( ( 𝜑 ∧ ( ( 𝑚 ∈ ( 𝑍 (,) 𝑊 ) ∧ 𝑛 ∈ ( 𝑍 (,) 𝑊 ) ) ∧ ∀ 𝑥 ∈ ( 𝑋 [,] 𝑌 ) 𝐴 ∈ ( 𝑚 (,) 𝑛 ) ) ) → 𝑚 ∈ ( 𝑍 (,) 𝑊 ) ) |
175 |
|
simprlr |
⊢ ( ( 𝜑 ∧ ( ( 𝑚 ∈ ( 𝑍 (,) 𝑊 ) ∧ 𝑛 ∈ ( 𝑍 (,) 𝑊 ) ) ∧ ∀ 𝑥 ∈ ( 𝑋 [,] 𝑌 ) 𝐴 ∈ ( 𝑚 (,) 𝑛 ) ) ) → 𝑛 ∈ ( 𝑍 (,) 𝑊 ) ) |
176 |
|
simprr |
⊢ ( ( 𝜑 ∧ ( ( 𝑚 ∈ ( 𝑍 (,) 𝑊 ) ∧ 𝑛 ∈ ( 𝑍 (,) 𝑊 ) ) ∧ ∀ 𝑥 ∈ ( 𝑋 [,] 𝑌 ) 𝐴 ∈ ( 𝑚 (,) 𝑛 ) ) ) → ∀ 𝑥 ∈ ( 𝑋 [,] 𝑌 ) 𝐴 ∈ ( 𝑚 (,) 𝑛 ) ) |
177 |
151
|
nfel1 |
⊢ Ⅎ 𝑥 ⦋ 𝑦 / 𝑥 ⦌ 𝐴 ∈ ( 𝑚 (,) 𝑛 ) |
178 |
152
|
eleq1d |
⊢ ( 𝑥 = 𝑦 → ( 𝐴 ∈ ( 𝑚 (,) 𝑛 ) ↔ ⦋ 𝑦 / 𝑥 ⦌ 𝐴 ∈ ( 𝑚 (,) 𝑛 ) ) ) |
179 |
177 178
|
rspc |
⊢ ( 𝑦 ∈ ( 𝑋 [,] 𝑌 ) → ( ∀ 𝑥 ∈ ( 𝑋 [,] 𝑌 ) 𝐴 ∈ ( 𝑚 (,) 𝑛 ) → ⦋ 𝑦 / 𝑥 ⦌ 𝐴 ∈ ( 𝑚 (,) 𝑛 ) ) ) |
180 |
176 179
|
mpan9 |
⊢ ( ( ( 𝜑 ∧ ( ( 𝑚 ∈ ( 𝑍 (,) 𝑊 ) ∧ 𝑛 ∈ ( 𝑍 (,) 𝑊 ) ) ∧ ∀ 𝑥 ∈ ( 𝑋 [,] 𝑌 ) 𝐴 ∈ ( 𝑚 (,) 𝑛 ) ) ) ∧ 𝑦 ∈ ( 𝑋 [,] 𝑌 ) ) → ⦋ 𝑦 / 𝑥 ⦌ 𝐴 ∈ ( 𝑚 (,) 𝑛 ) ) |
181 |
145 146 147 148 149 155 161 167 170 171 172 173 174 175 180
|
itgsubstlem |
⊢ ( ( 𝜑 ∧ ( ( 𝑚 ∈ ( 𝑍 (,) 𝑊 ) ∧ 𝑛 ∈ ( 𝑍 (,) 𝑊 ) ) ∧ ∀ 𝑥 ∈ ( 𝑋 [,] 𝑌 ) 𝐴 ∈ ( 𝑚 (,) 𝑛 ) ) ) → ⨜ [ ⦋ 𝑋 / 𝑥 ⦌ 𝐴 → ⦋ 𝑌 / 𝑥 ⦌ 𝐴 ] ⦋ 𝑣 / 𝑢 ⦌ 𝐶 d 𝑣 = ⨜ [ 𝑋 → 𝑌 ] ( ⦋ ⦋ 𝑦 / 𝑥 ⦌ 𝐴 / 𝑢 ⦌ 𝐶 · ⦋ 𝑦 / 𝑥 ⦌ 𝐵 ) d 𝑦 ) |
182 |
164 162 163
|
cbvditg |
⊢ ⨜ [ ⦋ 𝑋 / 𝑥 ⦌ 𝐴 → ⦋ 𝑌 / 𝑥 ⦌ 𝐴 ] 𝐶 d 𝑢 = ⨜ [ ⦋ 𝑋 / 𝑥 ⦌ 𝐴 → ⦋ 𝑌 / 𝑥 ⦌ 𝐴 ] ⦋ 𝑣 / 𝑢 ⦌ 𝐶 d 𝑣 |
183 |
|
nfcvd |
⊢ ( 𝑋 ∈ ℝ → Ⅎ 𝑥 𝐾 ) |
184 |
183 11
|
csbiegf |
⊢ ( 𝑋 ∈ ℝ → ⦋ 𝑋 / 𝑥 ⦌ 𝐴 = 𝐾 ) |
185 |
|
ditgeq1 |
⊢ ( ⦋ 𝑋 / 𝑥 ⦌ 𝐴 = 𝐾 → ⨜ [ ⦋ 𝑋 / 𝑥 ⦌ 𝐴 → ⦋ 𝑌 / 𝑥 ⦌ 𝐴 ] 𝐶 d 𝑢 = ⨜ [ 𝐾 → ⦋ 𝑌 / 𝑥 ⦌ 𝐴 ] 𝐶 d 𝑢 ) |
186 |
1 184 185
|
3syl |
⊢ ( 𝜑 → ⨜ [ ⦋ 𝑋 / 𝑥 ⦌ 𝐴 → ⦋ 𝑌 / 𝑥 ⦌ 𝐴 ] 𝐶 d 𝑢 = ⨜ [ 𝐾 → ⦋ 𝑌 / 𝑥 ⦌ 𝐴 ] 𝐶 d 𝑢 ) |
187 |
|
nfcvd |
⊢ ( 𝑌 ∈ ℝ → Ⅎ 𝑥 𝐿 ) |
188 |
187 12
|
csbiegf |
⊢ ( 𝑌 ∈ ℝ → ⦋ 𝑌 / 𝑥 ⦌ 𝐴 = 𝐿 ) |
189 |
|
ditgeq2 |
⊢ ( ⦋ 𝑌 / 𝑥 ⦌ 𝐴 = 𝐿 → ⨜ [ 𝐾 → ⦋ 𝑌 / 𝑥 ⦌ 𝐴 ] 𝐶 d 𝑢 = ⨜ [ 𝐾 → 𝐿 ] 𝐶 d 𝑢 ) |
190 |
2 188 189
|
3syl |
⊢ ( 𝜑 → ⨜ [ 𝐾 → ⦋ 𝑌 / 𝑥 ⦌ 𝐴 ] 𝐶 d 𝑢 = ⨜ [ 𝐾 → 𝐿 ] 𝐶 d 𝑢 ) |
191 |
186 190
|
eqtrd |
⊢ ( 𝜑 → ⨜ [ ⦋ 𝑋 / 𝑥 ⦌ 𝐴 → ⦋ 𝑌 / 𝑥 ⦌ 𝐴 ] 𝐶 d 𝑢 = ⨜ [ 𝐾 → 𝐿 ] 𝐶 d 𝑢 ) |
192 |
182 191
|
syl5eqr |
⊢ ( 𝜑 → ⨜ [ ⦋ 𝑋 / 𝑥 ⦌ 𝐴 → ⦋ 𝑌 / 𝑥 ⦌ 𝐴 ] ⦋ 𝑣 / 𝑢 ⦌ 𝐶 d 𝑣 = ⨜ [ 𝐾 → 𝐿 ] 𝐶 d 𝑢 ) |
193 |
192
|
adantr |
⊢ ( ( 𝜑 ∧ ( ( 𝑚 ∈ ( 𝑍 (,) 𝑊 ) ∧ 𝑛 ∈ ( 𝑍 (,) 𝑊 ) ) ∧ ∀ 𝑥 ∈ ( 𝑋 [,] 𝑌 ) 𝐴 ∈ ( 𝑚 (,) 𝑛 ) ) ) → ⨜ [ ⦋ 𝑋 / 𝑥 ⦌ 𝐴 → ⦋ 𝑌 / 𝑥 ⦌ 𝐴 ] ⦋ 𝑣 / 𝑢 ⦌ 𝐶 d 𝑣 = ⨜ [ 𝐾 → 𝐿 ] 𝐶 d 𝑢 ) |
194 |
152
|
csbeq1d |
⊢ ( 𝑥 = 𝑦 → ⦋ 𝐴 / 𝑢 ⦌ 𝐶 = ⦋ ⦋ 𝑦 / 𝑥 ⦌ 𝐴 / 𝑢 ⦌ 𝐶 ) |
195 |
194 158
|
oveq12d |
⊢ ( 𝑥 = 𝑦 → ( ⦋ 𝐴 / 𝑢 ⦌ 𝐶 · 𝐵 ) = ( ⦋ ⦋ 𝑦 / 𝑥 ⦌ 𝐴 / 𝑢 ⦌ 𝐶 · ⦋ 𝑦 / 𝑥 ⦌ 𝐵 ) ) |
196 |
|
nfcv |
⊢ Ⅎ 𝑦 ( ⦋ 𝐴 / 𝑢 ⦌ 𝐶 · 𝐵 ) |
197 |
|
nfcv |
⊢ Ⅎ 𝑥 𝐶 |
198 |
151 197
|
nfcsbw |
⊢ Ⅎ 𝑥 ⦋ ⦋ 𝑦 / 𝑥 ⦌ 𝐴 / 𝑢 ⦌ 𝐶 |
199 |
|
nfcv |
⊢ Ⅎ 𝑥 · |
200 |
198 199 157
|
nfov |
⊢ Ⅎ 𝑥 ( ⦋ ⦋ 𝑦 / 𝑥 ⦌ 𝐴 / 𝑢 ⦌ 𝐶 · ⦋ 𝑦 / 𝑥 ⦌ 𝐵 ) |
201 |
195 196 200
|
cbvditg |
⊢ ⨜ [ 𝑋 → 𝑌 ] ( ⦋ 𝐴 / 𝑢 ⦌ 𝐶 · 𝐵 ) d 𝑥 = ⨜ [ 𝑋 → 𝑌 ] ( ⦋ ⦋ 𝑦 / 𝑥 ⦌ 𝐴 / 𝑢 ⦌ 𝐶 · ⦋ 𝑦 / 𝑥 ⦌ 𝐵 ) d 𝑦 |
202 |
|
ioossicc |
⊢ ( 𝑋 (,) 𝑌 ) ⊆ ( 𝑋 [,] 𝑌 ) |
203 |
202
|
sseli |
⊢ ( 𝑥 ∈ ( 𝑋 (,) 𝑌 ) → 𝑥 ∈ ( 𝑋 [,] 𝑌 ) ) |
204 |
203 137
|
sylan2 |
⊢ ( ( 𝜑 ∧ 𝑥 ∈ ( 𝑋 (,) 𝑌 ) ) → 𝐴 ∈ ( 𝑍 (,) 𝑊 ) ) |
205 |
|
nfcvd |
⊢ ( 𝐴 ∈ ( 𝑍 (,) 𝑊 ) → Ⅎ 𝑢 𝐸 ) |
206 |
205 10
|
csbiegf |
⊢ ( 𝐴 ∈ ( 𝑍 (,) 𝑊 ) → ⦋ 𝐴 / 𝑢 ⦌ 𝐶 = 𝐸 ) |
207 |
204 206
|
syl |
⊢ ( ( 𝜑 ∧ 𝑥 ∈ ( 𝑋 (,) 𝑌 ) ) → ⦋ 𝐴 / 𝑢 ⦌ 𝐶 = 𝐸 ) |
208 |
207
|
oveq1d |
⊢ ( ( 𝜑 ∧ 𝑥 ∈ ( 𝑋 (,) 𝑌 ) ) → ( ⦋ 𝐴 / 𝑢 ⦌ 𝐶 · 𝐵 ) = ( 𝐸 · 𝐵 ) ) |
209 |
208
|
itgeq2dv |
⊢ ( 𝜑 → ∫ ( 𝑋 (,) 𝑌 ) ( ⦋ 𝐴 / 𝑢 ⦌ 𝐶 · 𝐵 ) d 𝑥 = ∫ ( 𝑋 (,) 𝑌 ) ( 𝐸 · 𝐵 ) d 𝑥 ) |
210 |
3
|
ditgpos |
⊢ ( 𝜑 → ⨜ [ 𝑋 → 𝑌 ] ( ⦋ 𝐴 / 𝑢 ⦌ 𝐶 · 𝐵 ) d 𝑥 = ∫ ( 𝑋 (,) 𝑌 ) ( ⦋ 𝐴 / 𝑢 ⦌ 𝐶 · 𝐵 ) d 𝑥 ) |
211 |
3
|
ditgpos |
⊢ ( 𝜑 → ⨜ [ 𝑋 → 𝑌 ] ( 𝐸 · 𝐵 ) d 𝑥 = ∫ ( 𝑋 (,) 𝑌 ) ( 𝐸 · 𝐵 ) d 𝑥 ) |
212 |
209 210 211
|
3eqtr4d |
⊢ ( 𝜑 → ⨜ [ 𝑋 → 𝑌 ] ( ⦋ 𝐴 / 𝑢 ⦌ 𝐶 · 𝐵 ) d 𝑥 = ⨜ [ 𝑋 → 𝑌 ] ( 𝐸 · 𝐵 ) d 𝑥 ) |
213 |
201 212
|
syl5eqr |
⊢ ( 𝜑 → ⨜ [ 𝑋 → 𝑌 ] ( ⦋ ⦋ 𝑦 / 𝑥 ⦌ 𝐴 / 𝑢 ⦌ 𝐶 · ⦋ 𝑦 / 𝑥 ⦌ 𝐵 ) d 𝑦 = ⨜ [ 𝑋 → 𝑌 ] ( 𝐸 · 𝐵 ) d 𝑥 ) |
214 |
213
|
adantr |
⊢ ( ( 𝜑 ∧ ( ( 𝑚 ∈ ( 𝑍 (,) 𝑊 ) ∧ 𝑛 ∈ ( 𝑍 (,) 𝑊 ) ) ∧ ∀ 𝑥 ∈ ( 𝑋 [,] 𝑌 ) 𝐴 ∈ ( 𝑚 (,) 𝑛 ) ) ) → ⨜ [ 𝑋 → 𝑌 ] ( ⦋ ⦋ 𝑦 / 𝑥 ⦌ 𝐴 / 𝑢 ⦌ 𝐶 · ⦋ 𝑦 / 𝑥 ⦌ 𝐵 ) d 𝑦 = ⨜ [ 𝑋 → 𝑌 ] ( 𝐸 · 𝐵 ) d 𝑥 ) |
215 |
181 193 214
|
3eqtr3d |
⊢ ( ( 𝜑 ∧ ( ( 𝑚 ∈ ( 𝑍 (,) 𝑊 ) ∧ 𝑛 ∈ ( 𝑍 (,) 𝑊 ) ) ∧ ∀ 𝑥 ∈ ( 𝑋 [,] 𝑌 ) 𝐴 ∈ ( 𝑚 (,) 𝑛 ) ) ) → ⨜ [ 𝐾 → 𝐿 ] 𝐶 d 𝑢 = ⨜ [ 𝑋 → 𝑌 ] ( 𝐸 · 𝐵 ) d 𝑥 ) |
216 |
215
|
expr |
⊢ ( ( 𝜑 ∧ ( 𝑚 ∈ ( 𝑍 (,) 𝑊 ) ∧ 𝑛 ∈ ( 𝑍 (,) 𝑊 ) ) ) → ( ∀ 𝑥 ∈ ( 𝑋 [,] 𝑌 ) 𝐴 ∈ ( 𝑚 (,) 𝑛 ) → ⨜ [ 𝐾 → 𝐿 ] 𝐶 d 𝑢 = ⨜ [ 𝑋 → 𝑌 ] ( 𝐸 · 𝐵 ) d 𝑥 ) ) |
217 |
144 216
|
sylbid |
⊢ ( ( 𝜑 ∧ ( 𝑚 ∈ ( 𝑍 (,) 𝑊 ) ∧ 𝑛 ∈ ( 𝑍 (,) 𝑊 ) ) ) → ( ∀ 𝑧 ∈ ( 𝑋 [,] 𝑌 ) ( ( 𝑥 ∈ ( 𝑋 [,] 𝑌 ) ↦ 𝐴 ) ‘ 𝑧 ) ∈ ( 𝑚 (,) 𝑛 ) → ⨜ [ 𝐾 → 𝐿 ] 𝐶 d 𝑢 = ⨜ [ 𝑋 → 𝑌 ] ( 𝐸 · 𝐵 ) d 𝑥 ) ) |
218 |
129 217
|
sylbid |
⊢ ( ( 𝜑 ∧ ( 𝑚 ∈ ( 𝑍 (,) 𝑊 ) ∧ 𝑛 ∈ ( 𝑍 (,) 𝑊 ) ) ) → ( ∀ 𝑧 ∈ ( 𝑋 [,] 𝑌 ) ( 𝑚 < ( ( 𝑥 ∈ ( 𝑋 [,] 𝑌 ) ↦ 𝐴 ) ‘ 𝑧 ) ∧ ( ( 𝑥 ∈ ( 𝑋 [,] 𝑌 ) ↦ 𝐴 ) ‘ 𝑧 ) < 𝑛 ) → ⨜ [ 𝐾 → 𝐿 ] 𝐶 d 𝑢 = ⨜ [ 𝑋 → 𝑌 ] ( 𝐸 · 𝐵 ) d 𝑥 ) ) |
219 |
117 218
|
syl5bir |
⊢ ( ( 𝜑 ∧ ( 𝑚 ∈ ( 𝑍 (,) 𝑊 ) ∧ 𝑛 ∈ ( 𝑍 (,) 𝑊 ) ) ) → ( ( ∀ 𝑧 ∈ ( 𝑋 [,] 𝑌 ) 𝑚 < ( ( 𝑥 ∈ ( 𝑋 [,] 𝑌 ) ↦ 𝐴 ) ‘ 𝑧 ) ∧ ∀ 𝑧 ∈ ( 𝑋 [,] 𝑌 ) ( ( 𝑥 ∈ ( 𝑋 [,] 𝑌 ) ↦ 𝐴 ) ‘ 𝑧 ) < 𝑛 ) → ⨜ [ 𝐾 → 𝐿 ] 𝐶 d 𝑢 = ⨜ [ 𝑋 → 𝑌 ] ( 𝐸 · 𝐵 ) d 𝑥 ) ) |
220 |
219
|
rexlimdvva |
⊢ ( 𝜑 → ( ∃ 𝑚 ∈ ( 𝑍 (,) 𝑊 ) ∃ 𝑛 ∈ ( 𝑍 (,) 𝑊 ) ( ∀ 𝑧 ∈ ( 𝑋 [,] 𝑌 ) 𝑚 < ( ( 𝑥 ∈ ( 𝑋 [,] 𝑌 ) ↦ 𝐴 ) ‘ 𝑧 ) ∧ ∀ 𝑧 ∈ ( 𝑋 [,] 𝑌 ) ( ( 𝑥 ∈ ( 𝑋 [,] 𝑌 ) ↦ 𝐴 ) ‘ 𝑧 ) < 𝑛 ) → ⨜ [ 𝐾 → 𝐿 ] 𝐶 d 𝑢 = ⨜ [ 𝑋 → 𝑌 ] ( 𝐸 · 𝐵 ) d 𝑥 ) ) |
221 |
116 220
|
syl5bi |
⊢ ( 𝜑 → ( ( ∃ 𝑛 ∈ ( 𝑍 (,) 𝑊 ) ∀ 𝑧 ∈ ( 𝑋 [,] 𝑌 ) ( ( 𝑥 ∈ ( 𝑋 [,] 𝑌 ) ↦ 𝐴 ) ‘ 𝑧 ) < 𝑛 ∧ ∃ 𝑚 ∈ ( 𝑍 (,) 𝑊 ) ∀ 𝑧 ∈ ( 𝑋 [,] 𝑌 ) 𝑚 < ( ( 𝑥 ∈ ( 𝑋 [,] 𝑌 ) ↦ 𝐴 ) ‘ 𝑧 ) ) → ⨜ [ 𝐾 → 𝐿 ] 𝐶 d 𝑢 = ⨜ [ 𝑋 → 𝑌 ] ( 𝐸 · 𝐵 ) d 𝑥 ) ) |
222 |
68 113 221
|
syl2and |
⊢ ( 𝜑 → ( ( ∃ 𝑦 ∈ ( 𝑋 [,] 𝑌 ) ∀ 𝑧 ∈ ( 𝑋 [,] 𝑌 ) ( ( 𝑥 ∈ ( 𝑋 [,] 𝑌 ) ↦ 𝐴 ) ‘ 𝑧 ) ≤ ( ( 𝑥 ∈ ( 𝑋 [,] 𝑌 ) ↦ 𝐴 ) ‘ 𝑦 ) ∧ ∃ 𝑦 ∈ ( 𝑋 [,] 𝑌 ) ∀ 𝑧 ∈ ( 𝑋 [,] 𝑌 ) ( ( 𝑥 ∈ ( 𝑋 [,] 𝑌 ) ↦ 𝐴 ) ‘ 𝑦 ) ≤ ( ( 𝑥 ∈ ( 𝑋 [,] 𝑌 ) ↦ 𝐴 ) ‘ 𝑧 ) ) → ⨜ [ 𝐾 → 𝐿 ] 𝐶 d 𝑢 = ⨜ [ 𝑋 → 𝑌 ] ( 𝐸 · 𝐵 ) d 𝑥 ) ) |
223 |
18 222
|
mpd |
⊢ ( 𝜑 → ⨜ [ 𝐾 → 𝐿 ] 𝐶 d 𝑢 = ⨜ [ 𝑋 → 𝑌 ] ( 𝐸 · 𝐵 ) d 𝑥 ) |