Metamath Proof Explorer

Theorem itgsubst

Description: Integration by u -substitution. If A ( x ) is a continuous, differentiable function from [ X , Y ] to ( Z , W ) , whose derivative is continuous and integrable, and C ( u ) is a continuous function on ( Z , W ) , then the integral of C ( u ) from K = A ( X ) to L = A ( Y ) is equal to the integral of C ( A ( x ) ) _D A ( x ) from X to Y . In this part of the proof we discharge the assumptions in itgsubstlem , which use the fact that ( Z , W ) is open to shrink the interval a little to ( M , N ) where Z < M < N < W - this is possible because A ( x ) is a continuous function on a closed interval, so its range is in fact a closed interval, and we have some wiggle room on the edges. (Contributed by Mario Carneiro, 7-Sep-2014)

Ref Expression
Hypotheses itgsubst.x ⊢ ( 𝜑 → 𝑋 ∈ ℝ )
itgsubst.y ⊢ ( 𝜑 → 𝑌 ∈ ℝ )
itgsubst.le ⊢ ( 𝜑 → 𝑋 ≤ 𝑌 )
itgsubst.z ⊢ ( 𝜑 → 𝑍 ∈ ℝ* )
itgsubst.w ⊢ ( 𝜑 → 𝑊 ∈ ℝ* )
itgsubst.a ⊢ ( 𝜑 → ( 𝑥 ∈ ( 𝑋 [,] 𝑌 ) ↦ 𝐴 ) ∈ ( ( 𝑋 [,] 𝑌 ) –cn→ ( 𝑍 (,) 𝑊 ) ) )
itgsubst.b ⊢ ( 𝜑 → ( 𝑥 ∈ ( 𝑋 (,) 𝑌 ) ↦ 𝐵 ) ∈ ( ( ( 𝑋 (,) 𝑌 ) –cn→ ℂ ) ∩ 𝐿1 ) )
itgsubst.c ⊢ ( 𝜑 → ( 𝑢 ∈ ( 𝑍 (,) 𝑊 ) ↦ 𝐶 ) ∈ ( ( 𝑍 (,) 𝑊 ) –cn→ ℂ ) )
itgsubst.da ⊢ ( 𝜑 → ( ℝ D ( 𝑥 ∈ ( 𝑋 [,] 𝑌 ) ↦ 𝐴 ) ) = ( 𝑥 ∈ ( 𝑋 (,) 𝑌 ) ↦ 𝐵 ) )
itgsubst.e ⊢ ( 𝑢 = 𝐴 → 𝐶 = 𝐸 )
itgsubst.k ⊢ ( 𝑥 = 𝑋 → 𝐴 = 𝐾 )
itgsubst.l ⊢ ( 𝑥 = 𝑌 → 𝐴 = 𝐿 )
Assertion itgsubst ( 𝜑 → ⨜ [ 𝐾 → 𝐿 ] 𝐶 d 𝑢 = ⨜ [ 𝑋 → 𝑌 ] ( 𝐸 · 𝐵 ) d 𝑥 )

Proof

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 sselid ⊢ ( 𝜑 → ( 𝑥 ∈ ( 𝑋 [,] 𝑌 ) ↦ 𝐴 ) ∈ ( ( 𝑋 [,] 𝑌 ) –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 ffvelcdmd ⊢ ( ( 𝜑 ∧ ( 𝑦 ∈ ( 𝑋 [,] 𝑌 ) ∧ ∀ 𝑧 ∈ ( 𝑋 [,] 𝑌 ) ( ( 𝑥 ∈ ( 𝑋 [,] 𝑌 ) ↦ 𝐴 ) ‘ 𝑧 ) ≤ ( ( 𝑥 ∈ ( 𝑋 [,] 𝑌 ) ↦ 𝐴 ) ‘ 𝑦 ) ) ) → ( ( 𝑥 ∈ ( 𝑋 [,] 𝑌 ) ↦ 𝐴 ) ‘ 𝑦 ) ∈ ( 𝑍 (,) 𝑊 ) )
26 20 25 sselid ⊢ ( ( 𝜑 ∧ ( 𝑦 ∈ ( 𝑋 [,] 𝑌 ) ∧ ∀ 𝑧 ∈ ( 𝑋 [,] 𝑌 ) ( ( 𝑥 ∈ ( 𝑋 [,] 𝑌 ) ↦ 𝐴 ) ‘ 𝑧 ) ≤ ( ( 𝑥 ∈ ( 𝑋 [,] 𝑌 ) ↦ 𝐴 ) ‘ 𝑦 ) ) ) → ( ( 𝑥 ∈ ( 𝑋 [,] 𝑌 ) ↦ 𝐴 ) ‘ 𝑦 ) ∈ ℝ* )
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 ffvelcdmda ⊢ ( ( ( ( 𝜑 ∧ 𝑦 ∈ ( 𝑋 [,] 𝑌 ) ) ∧ ( 𝑛 ∈ ℚ ∧ ( ( ( 𝑥 ∈ ( 𝑋 [,] 𝑌 ) ↦ 𝐴 ) ‘ 𝑦 ) < 𝑛 ∧ 𝑛 < 𝑊 ) ) ) ∧ 𝑧 ∈ ( 𝑋 [,] 𝑌 ) ) → ( ( 𝑥 ∈ ( 𝑋 [,] 𝑌 ) ↦ 𝐴 ) ‘ 𝑧 ) ∈ ( 𝑍 (,) 𝑊 ) )
52 20 51 sselid ⊢ ( ( ( ( 𝜑 ∧ 𝑦 ∈ ( 𝑋 [,] 𝑌 ) ) ∧ ( 𝑛 ∈ ℚ ∧ ( ( ( 𝑥 ∈ ( 𝑋 [,] 𝑌 ) ↦ 𝐴 ) ‘ 𝑦 ) < 𝑛 ∧ 𝑛 < 𝑊 ) ) ) ∧ 𝑧 ∈ ( 𝑋 [,] 𝑌 ) ) → ( ( 𝑥 ∈ ( 𝑋 [,] 𝑌 ) ↦ 𝐴 ) ‘ 𝑧 ) ∈ ℝ* )
53 simplr ⊢ ( ( ( 𝜑 ∧ 𝑦 ∈ ( 𝑋 [,] 𝑌 ) ) ∧ ( 𝑛 ∈ ℚ ∧ ( ( ( 𝑥 ∈ ( 𝑋 [,] 𝑌 ) ↦ 𝐴 ) ‘ 𝑦 ) < 𝑛 ∧ 𝑛 < 𝑊 ) ) ) → 𝑦 ∈ ( 𝑋 [,] 𝑌 ) )
54 50 53 ffvelcdmd ⊢ ( ( ( 𝜑 ∧ 𝑦 ∈ ( 𝑋 [,] 𝑌 ) ) ∧ ( 𝑛 ∈ ℚ ∧ ( ( ( 𝑥 ∈ ( 𝑋 [,] 𝑌 ) ↦ 𝐴 ) ‘ 𝑦 ) < 𝑛 ∧ 𝑛 < 𝑊 ) ) ) → ( ( 𝑥 ∈ ( 𝑋 [,] 𝑌 ) ↦ 𝐴 ) ‘ 𝑦 ) ∈ ( 𝑍 (,) 𝑊 ) )
55 20 54 sselid ⊢ ( ( ( 𝜑 ∧ 𝑦 ∈ ( 𝑋 [,] 𝑌 ) ) ∧ ( 𝑛 ∈ ℚ ∧ ( ( ( 𝑥 ∈ ( 𝑋 [,] 𝑌 ) ↦ 𝐴 ) ‘ 𝑦 ) < 𝑛 ∧ 𝑛 < 𝑊 ) ) ) → ( ( 𝑥 ∈ ( 𝑋 [,] 𝑌 ) ↦ 𝐴 ) ‘ 𝑦 ) ∈ ℝ* )
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 ffvelcdmd ⊢ ( ( 𝜑 ∧ ( 𝑦 ∈ ( 𝑋 [,] 𝑌 ) ∧ ∀ 𝑧 ∈ ( 𝑋 [,] 𝑌 ) ( ( 𝑥 ∈ ( 𝑋 [,] 𝑌 ) ↦ 𝐴 ) ‘ 𝑦 ) ≤ ( ( 𝑥 ∈ ( 𝑋 [,] 𝑌 ) ↦ 𝐴 ) ‘ 𝑧 ) ) ) → ( ( 𝑥 ∈ ( 𝑋 [,] 𝑌 ) ↦ 𝐴 ) ‘ 𝑦 ) ∈ ( 𝑍 (,) 𝑊 ) )
73 20 72 sselid ⊢ ( ( 𝜑 ∧ ( 𝑦 ∈ ( 𝑋 [,] 𝑌 ) ∧ ∀ 𝑧 ∈ ( 𝑋 [,] 𝑌 ) ( ( 𝑥 ∈ ( 𝑋 [,] 𝑌 ) ↦ 𝐴 ) ‘ 𝑦 ) ≤ ( ( 𝑥 ∈ ( 𝑋 [,] 𝑌 ) ↦ 𝐴 ) ‘ 𝑧 ) ) ) → ( ( 𝑥 ∈ ( 𝑋 [,] 𝑌 ) ↦ 𝐴 ) ‘ 𝑦 ) ∈ ℝ* )
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 ffvelcdmd ⊢ ( ( ( 𝜑 ∧ 𝑦 ∈ ( 𝑋 [,] 𝑌 ) ) ∧ ( 𝑚 ∈ ℚ ∧ ( 𝑍 < 𝑚 ∧ 𝑚 < ( ( 𝑥 ∈ ( 𝑋 [,] 𝑌 ) ↦ 𝐴 ) ‘ 𝑦 ) ) ) ) → ( ( 𝑥 ∈ ( 𝑋 [,] 𝑌 ) ↦ 𝐴 ) ‘ 𝑦 ) ∈ ( 𝑍 (,) 𝑊 ) )
101 20 100 sselid ⊢ ( ( ( 𝜑 ∧ 𝑦 ∈ ( 𝑋 [,] 𝑌 ) ) ∧ ( 𝑚 ∈ ℚ ∧ ( 𝑍 < 𝑚 ∧ 𝑚 < ( ( 𝑥 ∈ ( 𝑋 [,] 𝑌 ) ↦ 𝐴 ) ‘ 𝑦 ) ) ) ) → ( ( 𝑥 ∈ ( 𝑋 [,] 𝑌 ) ↦ 𝐴 ) ‘ 𝑦 ) ∈ ℝ* )
102 101 adantr ⊢ ( ( ( ( 𝜑 ∧ 𝑦 ∈ ( 𝑋 [,] 𝑌 ) ) ∧ ( 𝑚 ∈ ℚ ∧ ( 𝑍 < 𝑚 ∧ 𝑚 < ( ( 𝑥 ∈ ( 𝑋 [,] 𝑌 ) ↦ 𝐴 ) ‘ 𝑦 ) ) ) ) ∧ 𝑧 ∈ ( 𝑋 [,] 𝑌 ) ) → ( ( 𝑥 ∈ ( 𝑋 [,] 𝑌 ) ↦ 𝐴 ) ‘ 𝑦 ) ∈ ℝ* )
103 98 ffvelcdmda ⊢ ( ( ( ( 𝜑 ∧ 𝑦 ∈ ( 𝑋 [,] 𝑌 ) ) ∧ ( 𝑚 ∈ ℚ ∧ ( 𝑍 < 𝑚 ∧ 𝑚 < ( ( 𝑥 ∈ ( 𝑋 [,] 𝑌 ) ↦ 𝐴 ) ‘ 𝑦 ) ) ) ) ∧ 𝑧 ∈ ( 𝑋 [,] 𝑌 ) ) → ( ( 𝑥 ∈ ( 𝑋 [,] 𝑌 ) ↦ 𝐴 ) ‘ 𝑧 ) ∈ ( 𝑍 (,) 𝑊 ) )
104 20 103 sselid ⊢ ( ( ( ( 𝜑 ∧ 𝑦 ∈ ( 𝑋 [,] 𝑌 ) ) ∧ ( 𝑚 ∈ ℚ ∧ ( 𝑍 < 𝑚 ∧ 𝑚 < ( ( 𝑥 ∈ ( 𝑋 [,] 𝑌 ) ↦ 𝐴 ) ‘ 𝑦 ) ) ) ) ∧ 𝑧 ∈ ( 𝑋 [,] 𝑌 ) ) → ( ( 𝑥 ∈ ( 𝑋 [,] 𝑌 ) ↦ 𝐴 ) ‘ 𝑧 ) ∈ ℝ* )
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 ffvelcdmda ⊢ ( ( ( 𝜑 ∧ ( 𝑚 ∈ ( 𝑍 (,) 𝑊 ) ∧ 𝑛 ∈ ( 𝑍 (,) 𝑊 ) ) ) ∧ 𝑧 ∈ ( 𝑋 [,] 𝑌 ) ) → ( ( 𝑥 ∈ ( 𝑋 [,] 𝑌 ) ↦ 𝐴 ) ‘ 𝑧 ) ∈ ( 𝑍 (,) 𝑊 ) )
120 13 119 sselid ⊢ ( ( ( 𝜑 ∧ ( 𝑚 ∈ ( 𝑍 (,) 𝑊 ) ∧ 𝑛 ∈ ( 𝑍 (,) 𝑊 ) ) ) ∧ 𝑧 ∈ ( 𝑋 [,] 𝑌 ) ) → ( ( 𝑥 ∈ ( 𝑋 [,] 𝑌 ) ↦ 𝐴 ) ‘ 𝑧 ) ∈ ℝ )
121 120 3biant1d ⊢ ( ( ( 𝜑 ∧ ( 𝑚 ∈ ( 𝑍 (,) 𝑊 ) ∧ 𝑛 ∈ ( 𝑍 (,) 𝑊 ) ) ) ∧ 𝑧 ∈ ( 𝑋 [,] 𝑌 ) ) → ( ( 𝑚 < ( ( 𝑥 ∈ ( 𝑋 [,] 𝑌 ) ↦ 𝐴 ) ‘ 𝑧 ) ∧ ( ( 𝑥 ∈ ( 𝑋 [,] 𝑌 ) ↦ 𝐴 ) ‘ 𝑧 ) < 𝑛 ) ↔ ( ( ( 𝑥 ∈ ( 𝑋 [,] 𝑌 ) ↦ 𝐴 ) ‘ 𝑧 ) ∈ ℝ ∧ 𝑚 < ( ( 𝑥 ∈ ( 𝑋 [,] 𝑌 ) ↦ 𝐴 ) ‘ 𝑧 ) ∧ ( ( 𝑥 ∈ ( 𝑋 [,] 𝑌 ) ↦ 𝐴 ) ‘ 𝑧 ) < 𝑛 ) ) )
122 simplrl ⊢ ( ( ( 𝜑 ∧ ( 𝑚 ∈ ( 𝑍 (,) 𝑊 ) ∧ 𝑛 ∈ ( 𝑍 (,) 𝑊 ) ) ) ∧ 𝑧 ∈ ( 𝑋 [,] 𝑌 ) ) → 𝑚 ∈ ( 𝑍 (,) 𝑊 ) )
123 20 122 sselid ⊢ ( ( ( 𝜑 ∧ ( 𝑚 ∈ ( 𝑍 (,) 𝑊 ) ∧ 𝑛 ∈ ( 𝑍 (,) 𝑊 ) ) ) ∧ 𝑧 ∈ ( 𝑋 [,] 𝑌 ) ) → 𝑚 ∈ ℝ* )
124 simplrr ⊢ ( ( ( 𝜑 ∧ ( 𝑚 ∈ ( 𝑍 (,) 𝑊 ) ∧ 𝑛 ∈ ( 𝑍 (,) 𝑊 ) ) ) ∧ 𝑧 ∈ ( 𝑋 [,] 𝑌 ) ) → 𝑛 ∈ ( 𝑍 (,) 𝑊 ) )
125 20 124 sselid ⊢ ( ( ( 𝜑 ∧ ( 𝑚 ∈ ( 𝑍 (,) 𝑊 ) ∧ 𝑛 ∈ ( 𝑍 (,) 𝑊 ) ) ) ∧ 𝑧 ∈ ( 𝑋 [,] 𝑌 ) ) → 𝑛 ∈ ℝ* )
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 fvmptelcdm ⊢ ( ( 𝜑 ∧ 𝑥 ∈ ( 𝑋 [,] 𝑌 ) ) → 𝐴 ∈ ( 𝑍 (,) 𝑊 ) )
138 eqid ⊢ ( 𝑥 ∈ ( 𝑋 [,] 𝑌 ) ↦ 𝐴 ) = ( 𝑥 ∈ ( 𝑋 [,] 𝑌 ) ↦ 𝐴 )
139 138 fvmpt2 ⊢ ( ( 𝑥 ∈ ( 𝑋 [,] 𝑌 ) ∧ 𝐴 ∈ ( 𝑍 (,) 𝑊 ) ) → ( ( 𝑥 ∈ ( 𝑋 [,] 𝑌 ) ↦ 𝐴 ) ‘ 𝑥 ) = 𝐴 )
140 136 137 139 syl2anc ⊢ ( ( 𝜑 ∧ 𝑥 ∈ ( 𝑋 [,] 𝑌 ) ) → ( ( 𝑥 ∈ ( 𝑋 [,] 𝑌 ) ↦ 𝐴 ) ‘ 𝑥 ) = 𝐴 )
141 140 eleq1d ⊢ ( ( 𝜑 ∧ 𝑥 ∈ ( 𝑋 [,] 𝑌 ) ) → ( ( ( 𝑥 ∈ ( 𝑋 [,] 𝑌 ) ↦ 𝐴 ) ‘ 𝑥 ) ∈ ( 𝑚 (,) 𝑛 ) ↔ 𝐴 ∈ ( 𝑚 (,) 𝑛 ) ) )
142 141 ralbidva ⊢ ( 𝜑 → ( ∀ 𝑥 ∈ ( 𝑋 [,] 𝑌 ) ( ( 𝑥 ∈ ( 𝑋 [,] 𝑌 ) ↦ 𝐴 ) ‘ 𝑥 ) ∈ ( 𝑚 (,) 𝑛 ) ↔ ∀ 𝑥 ∈ ( 𝑋 [,] 𝑌 ) 𝐴 ∈ ( 𝑚 (,) 𝑛 ) ) )
143 135 142 bitrid ⊢ ( 𝜑 → ( ∀ 𝑧 ∈ ( 𝑋 [,] 𝑌 ) ( ( 𝑥 ∈ ( 𝑋 [,] 𝑌 ) ↦ 𝐴 ) ‘ 𝑧 ) ∈ ( 𝑚 (,) 𝑛 ) ↔ ∀ 𝑥 ∈ ( 𝑋 [,] 𝑌 ) 𝐴 ∈ ( 𝑚 (,) 𝑛 ) ) )
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 eqtr3id ⊢ ( 𝜑 → ⨜ [ ⦋ 𝑋 / 𝑥 ⦌ 𝐴 → ⦋ 𝑌 / 𝑥 ⦌ 𝐴 ] ⦋ 𝑣 / 𝑢 ⦌ 𝐶 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 eqtr3id ⊢ ( 𝜑 → ⨜ [ 𝑋 → 𝑌 ] ( ⦋ ⦋ 𝑦 / 𝑥 ⦌ 𝐴 / 𝑢 ⦌ 𝐶 · ⦋ 𝑦 / 𝑥 ⦌ 𝐵 ) 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 biimtrrid ⊢ ( ( 𝜑 ∧ ( 𝑚 ∈ ( 𝑍 (,) 𝑊 ) ∧ 𝑛 ∈ ( 𝑍 (,) 𝑊 ) ) ) → ( ( ∀ 𝑧 ∈ ( 𝑋 [,] 𝑌 ) 𝑚 < ( ( 𝑥 ∈ ( 𝑋 [,] 𝑌 ) ↦ 𝐴 ) ‘ 𝑧 ) ∧ ∀ 𝑧 ∈ ( 𝑋 [,] 𝑌 ) ( ( 𝑥 ∈ ( 𝑋 [,] 𝑌 ) ↦ 𝐴 ) ‘ 𝑧 ) < 𝑛 ) → ⨜ [ 𝐾 → 𝐿 ] 𝐶 d 𝑢 = ⨜ [ 𝑋 → 𝑌 ] ( 𝐸 · 𝐵 ) d 𝑥 ) )
220 219 rexlimdvva ⊢ ( 𝜑 → ( ∃ 𝑚 ∈ ( 𝑍 (,) 𝑊 ) ∃ 𝑛 ∈ ( 𝑍 (,) 𝑊 ) ( ∀ 𝑧 ∈ ( 𝑋 [,] 𝑌 ) 𝑚 < ( ( 𝑥 ∈ ( 𝑋 [,] 𝑌 ) ↦ 𝐴 ) ‘ 𝑧 ) ∧ ∀ 𝑧 ∈ ( 𝑋 [,] 𝑌 ) ( ( 𝑥 ∈ ( 𝑋 [,] 𝑌 ) ↦ 𝐴 ) ‘ 𝑧 ) < 𝑛 ) → ⨜ [ 𝐾 → 𝐿 ] 𝐶 d 𝑢 = ⨜ [ 𝑋 → 𝑌 ] ( 𝐸 · 𝐵 ) d 𝑥 ) )
221 116 220 biimtrid ⊢ ( 𝜑 → ( ( ∃ 𝑛 ∈ ( 𝑍 (,) 𝑊 ) ∀ 𝑧 ∈ ( 𝑋 [,] 𝑌 ) ( ( 𝑥 ∈ ( 𝑋 [,] 𝑌 ) ↦ 𝐴 ) ‘ 𝑧 ) < 𝑛 ∧ ∃ 𝑚 ∈ ( 𝑍 (,) 𝑊 ) ∀ 𝑧 ∈ ( 𝑋 [,] 𝑌 ) 𝑚 < ( ( 𝑥 ∈ ( 𝑋 [,] 𝑌 ) ↦ 𝐴 ) ‘ 𝑧 ) ) → ⨜ [ 𝐾 → 𝐿 ] 𝐶 d 𝑢 = ⨜ [ 𝑋 → 𝑌 ] ( 𝐸 · 𝐵 ) d 𝑥 ) )
222 68 113 221 syl2and ⊢ ( 𝜑 → ( ( ∃ 𝑦 ∈ ( 𝑋 [,] 𝑌 ) ∀ 𝑧 ∈ ( 𝑋 [,] 𝑌 ) ( ( 𝑥 ∈ ( 𝑋 [,] 𝑌 ) ↦ 𝐴 ) ‘ 𝑧 ) ≤ ( ( 𝑥 ∈ ( 𝑋 [,] 𝑌 ) ↦ 𝐴 ) ‘ 𝑦 ) ∧ ∃ 𝑦 ∈ ( 𝑋 [,] 𝑌 ) ∀ 𝑧 ∈ ( 𝑋 [,] 𝑌 ) ( ( 𝑥 ∈ ( 𝑋 [,] 𝑌 ) ↦ 𝐴 ) ‘ 𝑦 ) ≤ ( ( 𝑥 ∈ ( 𝑋 [,] 𝑌 ) ↦ 𝐴 ) ‘ 𝑧 ) ) → ⨜ [ 𝐾 → 𝐿 ] 𝐶 d 𝑢 = ⨜ [ 𝑋 → 𝑌 ] ( 𝐸 · 𝐵 ) d 𝑥 ) )
223 18 222 mpd ⊢ ( 𝜑 → ⨜ [ 𝐾 → 𝐿 ] 𝐶 d 𝑢 = ⨜ [ 𝑋 → 𝑌 ] ( 𝐸 · 𝐵 ) d 𝑥 )