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→ ℂ ) ∩ 𝐿¹ ) )
	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→ ℂ ) ∩ 𝐿¹ ) )
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→ ℂ ) ∩ 𝐿¹ ) )
161	160	adantr	⊢ ( ( 𝜑 ∧ ( ( 𝑚 ∈ ( 𝑍 (,) 𝑊 ) ∧ 𝑛 ∈ ( 𝑍 (,) 𝑊 ) ) ∧ ∀ 𝑥 ∈ ( 𝑋 [,] 𝑌 ) 𝐴 ∈ ( 𝑚 (,) 𝑛 ) ) ) → ( 𝑦 ∈ ( 𝑋 (,) 𝑌 ) ↦ ⦋ 𝑦 / 𝑥 ⦌ 𝐵 ) ∈ ( ( ( 𝑋 (,) 𝑌 ) –cn→ ℂ ) ∩ 𝐿¹ ) )
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 𝑥 )

Metamath Proof Explorer

Theorem itgsubst

Proof