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	\|- ( ph -> X e. RR )
	itgsubst.y	\|- ( ph -> Y e. RR )
	itgsubst.le	\|- ( ph -> X <_ Y )
	itgsubst.z	\|- ( ph -> Z e. RR* )
	itgsubst.w	\|- ( ph -> W e. RR* )
	itgsubst.a	\|- ( ph -> ( x e. ( X [,] Y ) \|-> A ) e. ( ( X [,] Y ) -cn-> ( Z (,) W ) ) )
	itgsubst.b	\|- ( ph -> ( x e. ( X (,) Y ) \|-> B ) e. ( ( ( X (,) Y ) -cn-> CC ) i^i L^1 ) )
	itgsubst.c	\|- ( ph -> ( u e. ( Z (,) W ) \|-> C ) e. ( ( Z (,) W ) -cn-> CC ) )
	itgsubst.da	\|- ( ph -> ( RR _D ( x e. ( X [,] Y ) \|-> A ) ) = ( x e. ( X (,) Y ) \|-> B ) )
	itgsubst.e	\|- ( u = A -> C = E )
	itgsubst.k	\|- ( x = X -> A = K )
	itgsubst.l	\|- ( x = Y -> A = L )
Assertion	itgsubst	\|- ( ph -> S_ [ K -> L ] C _d u = S_ [ X -> Y ] ( E x. B ) _d x )

Proof

Step	Hyp	Ref	Expression
1		itgsubst.x	\|- ( ph -> X e. RR )
2		itgsubst.y	\|- ( ph -> Y e. RR )
3		itgsubst.le	\|- ( ph -> X <_ Y )
4		itgsubst.z	\|- ( ph -> Z e. RR* )
5		itgsubst.w	\|- ( ph -> W e. RR* )
6		itgsubst.a	\|- ( ph -> ( x e. ( X [,] Y ) \|-> A ) e. ( ( X [,] Y ) -cn-> ( Z (,) W ) ) )
7		itgsubst.b	\|- ( ph -> ( x e. ( X (,) Y ) \|-> B ) e. ( ( ( X (,) Y ) -cn-> CC ) i^i L^1 ) )
8		itgsubst.c	\|- ( ph -> ( u e. ( Z (,) W ) \|-> C ) e. ( ( Z (,) W ) -cn-> CC ) )
9		itgsubst.da	\|- ( ph -> ( RR _D ( x e. ( X [,] Y ) \|-> A ) ) = ( x e. ( X (,) Y ) \|-> B ) )
10		itgsubst.e	\|- ( u = A -> C = E )
11		itgsubst.k	\|- ( x = X -> A = K )
12		itgsubst.l	\|- ( x = Y -> A = L )
13		ioossre	\|- ( Z (,) W ) C_ RR
14		ax-resscn	\|- RR C_ CC
15		cncfss	\|- ( ( ( Z (,) W ) C_ RR /\ RR C_ CC ) -> ( ( X [,] Y ) -cn-> ( Z (,) W ) ) C_ ( ( X [,] Y ) -cn-> RR ) )
16	13 14 15	mp2an	\|- ( ( X [,] Y ) -cn-> ( Z (,) W ) ) C_ ( ( X [,] Y ) -cn-> RR )
17	16 6	sselid	\|- ( ph -> ( x e. ( X [,] Y ) \|-> A ) e. ( ( X [,] Y ) -cn-> RR ) )
18	1 2 3 17	evthicc	\|- ( ph -> ( E. y e. ( X [,] Y ) A. z e. ( X [,] Y ) ( ( x e. ( X [,] Y ) \|-> A ) ` z ) <_ ( ( x e. ( X [,] Y ) \|-> A ) ` y ) /\ E. y e. ( X [,] Y ) A. z e. ( X [,] Y ) ( ( x e. ( X [,] Y ) \|-> A ) ` y ) <_ ( ( x e. ( X [,] Y ) \|-> A ) ` z ) ) )
19		ressxr	\|- RR C_ RR*
20	13 19	sstri	\|- ( Z (,) W ) C_ RR*
21		cncff	\|- ( ( x e. ( X [,] Y ) \|-> A ) e. ( ( X [,] Y ) -cn-> ( Z (,) W ) ) -> ( x e. ( X [,] Y ) \|-> A ) : ( X [,] Y ) --> ( Z (,) W ) )
22	6 21	syl	\|- ( ph -> ( x e. ( X [,] Y ) \|-> A ) : ( X [,] Y ) --> ( Z (,) W ) )
23	22	adantr	\|- ( ( ph /\ ( y e. ( X [,] Y ) /\ A. z e. ( X [,] Y ) ( ( x e. ( X [,] Y ) \|-> A ) ` z ) <_ ( ( x e. ( X [,] Y ) \|-> A ) ` y ) ) ) -> ( x e. ( X [,] Y ) \|-> A ) : ( X [,] Y ) --> ( Z (,) W ) )
24		simprl	\|- ( ( ph /\ ( y e. ( X [,] Y ) /\ A. z e. ( X [,] Y ) ( ( x e. ( X [,] Y ) \|-> A ) ` z ) <_ ( ( x e. ( X [,] Y ) \|-> A ) ` y ) ) ) -> y e. ( X [,] Y ) )
25	23 24	ffvelcdmd	\|- ( ( ph /\ ( y e. ( X [,] Y ) /\ A. z e. ( X [,] Y ) ( ( x e. ( X [,] Y ) \|-> A ) ` z ) <_ ( ( x e. ( X [,] Y ) \|-> A ) ` y ) ) ) -> ( ( x e. ( X [,] Y ) \|-> A ) ` y ) e. ( Z (,) W ) )
26	20 25	sselid	\|- ( ( ph /\ ( y e. ( X [,] Y ) /\ A. z e. ( X [,] Y ) ( ( x e. ( X [,] Y ) \|-> A ) ` z ) <_ ( ( x e. ( X [,] Y ) \|-> A ) ` y ) ) ) -> ( ( x e. ( X [,] Y ) \|-> A ) ` y ) e. RR* )
27	5	adantr	\|- ( ( ph /\ ( y e. ( X [,] Y ) /\ A. z e. ( X [,] Y ) ( ( x e. ( X [,] Y ) \|-> A ) ` z ) <_ ( ( x e. ( X [,] Y ) \|-> A ) ` y ) ) ) -> W e. RR* )
28		eliooord	\|- ( ( ( x e. ( X [,] Y ) \|-> A ) ` y ) e. ( Z (,) W ) -> ( Z < ( ( x e. ( X [,] Y ) \|-> A ) ` y ) /\ ( ( x e. ( X [,] Y ) \|-> A ) ` y ) < W ) )
29	25 28	syl	\|- ( ( ph /\ ( y e. ( X [,] Y ) /\ A. z e. ( X [,] Y ) ( ( x e. ( X [,] Y ) \|-> A ) ` z ) <_ ( ( x e. ( X [,] Y ) \|-> A ) ` y ) ) ) -> ( Z < ( ( x e. ( X [,] Y ) \|-> A ) ` y ) /\ ( ( x e. ( X [,] Y ) \|-> A ) ` y ) < W ) )
30	29	simprd	\|- ( ( ph /\ ( y e. ( X [,] Y ) /\ A. z e. ( X [,] Y ) ( ( x e. ( X [,] Y ) \|-> A ) ` z ) <_ ( ( x e. ( X [,] Y ) \|-> A ) ` y ) ) ) -> ( ( x e. ( X [,] Y ) \|-> A ) ` y ) < W )
31		qbtwnxr	\|- ( ( ( ( x e. ( X [,] Y ) \|-> A ) ` y ) e. RR* /\ W e. RR* /\ ( ( x e. ( X [,] Y ) \|-> A ) ` y ) < W ) -> E. n e. QQ ( ( ( x e. ( X [,] Y ) \|-> A ) ` y ) < n /\ n < W ) )
32	26 27 30 31	syl3anc	\|- ( ( ph /\ ( y e. ( X [,] Y ) /\ A. z e. ( X [,] Y ) ( ( x e. ( X [,] Y ) \|-> A ) ` z ) <_ ( ( x e. ( X [,] Y ) \|-> A ) ` y ) ) ) -> E. n e. QQ ( ( ( x e. ( X [,] Y ) \|-> A ) ` y ) < n /\ n < W ) )
33		qre	\|- ( n e. QQ -> n e. RR )
34	33	ad2antrl	\|- ( ( ( ph /\ ( y e. ( X [,] Y ) /\ A. z e. ( X [,] Y ) ( ( x e. ( X [,] Y ) \|-> A ) ` z ) <_ ( ( x e. ( X [,] Y ) \|-> A ) ` y ) ) ) /\ ( n e. QQ /\ ( ( ( x e. ( X [,] Y ) \|-> A ) ` y ) < n /\ n < W ) ) ) -> n e. RR )
35	4	ad2antrr	\|- ( ( ( ph /\ ( y e. ( X [,] Y ) /\ A. z e. ( X [,] Y ) ( ( x e. ( X [,] Y ) \|-> A ) ` z ) <_ ( ( x e. ( X [,] Y ) \|-> A ) ` y ) ) ) /\ ( n e. QQ /\ ( ( ( x e. ( X [,] Y ) \|-> A ) ` y ) < n /\ n < W ) ) ) -> Z e. RR* )
36	26	adantr	\|- ( ( ( ph /\ ( y e. ( X [,] Y ) /\ A. z e. ( X [,] Y ) ( ( x e. ( X [,] Y ) \|-> A ) ` z ) <_ ( ( x e. ( X [,] Y ) \|-> A ) ` y ) ) ) /\ ( n e. QQ /\ ( ( ( x e. ( X [,] Y ) \|-> A ) ` y ) < n /\ n < W ) ) ) -> ( ( x e. ( X [,] Y ) \|-> A ) ` y ) e. RR* )
37	34	rexrd	\|- ( ( ( ph /\ ( y e. ( X [,] Y ) /\ A. z e. ( X [,] Y ) ( ( x e. ( X [,] Y ) \|-> A ) ` z ) <_ ( ( x e. ( X [,] Y ) \|-> A ) ` y ) ) ) /\ ( n e. QQ /\ ( ( ( x e. ( X [,] Y ) \|-> A ) ` y ) < n /\ n < W ) ) ) -> n e. RR* )
38	29	simpld	\|- ( ( ph /\ ( y e. ( X [,] Y ) /\ A. z e. ( X [,] Y ) ( ( x e. ( X [,] Y ) \|-> A ) ` z ) <_ ( ( x e. ( X [,] Y ) \|-> A ) ` y ) ) ) -> Z < ( ( x e. ( X [,] Y ) \|-> A ) ` y ) )
39	38	adantr	\|- ( ( ( ph /\ ( y e. ( X [,] Y ) /\ A. z e. ( X [,] Y ) ( ( x e. ( X [,] Y ) \|-> A ) ` z ) <_ ( ( x e. ( X [,] Y ) \|-> A ) ` y ) ) ) /\ ( n e. QQ /\ ( ( ( x e. ( X [,] Y ) \|-> A ) ` y ) < n /\ n < W ) ) ) -> Z < ( ( x e. ( X [,] Y ) \|-> A ) ` y ) )
40		simprrl	\|- ( ( ( ph /\ ( y e. ( X [,] Y ) /\ A. z e. ( X [,] Y ) ( ( x e. ( X [,] Y ) \|-> A ) ` z ) <_ ( ( x e. ( X [,] Y ) \|-> A ) ` y ) ) ) /\ ( n e. QQ /\ ( ( ( x e. ( X [,] Y ) \|-> A ) ` y ) < n /\ n < W ) ) ) -> ( ( x e. ( X [,] Y ) \|-> A ) ` y ) < n )
41	35 36 37 39 40	xrlttrd	\|- ( ( ( ph /\ ( y e. ( X [,] Y ) /\ A. z e. ( X [,] Y ) ( ( x e. ( X [,] Y ) \|-> A ) ` z ) <_ ( ( x e. ( X [,] Y ) \|-> A ) ` y ) ) ) /\ ( n e. QQ /\ ( ( ( x e. ( X [,] Y ) \|-> A ) ` y ) < n /\ n < W ) ) ) -> Z < n )
42		simprrr	\|- ( ( ( ph /\ ( y e. ( X [,] Y ) /\ A. z e. ( X [,] Y ) ( ( x e. ( X [,] Y ) \|-> A ) ` z ) <_ ( ( x e. ( X [,] Y ) \|-> A ) ` y ) ) ) /\ ( n e. QQ /\ ( ( ( x e. ( X [,] Y ) \|-> A ) ` y ) < n /\ n < W ) ) ) -> n < W )
43	5	ad2antrr	\|- ( ( ( ph /\ ( y e. ( X [,] Y ) /\ A. z e. ( X [,] Y ) ( ( x e. ( X [,] Y ) \|-> A ) ` z ) <_ ( ( x e. ( X [,] Y ) \|-> A ) ` y ) ) ) /\ ( n e. QQ /\ ( ( ( x e. ( X [,] Y ) \|-> A ) ` y ) < n /\ n < W ) ) ) -> W e. RR* )
44		elioo2	\|- ( ( Z e. RR* /\ W e. RR* ) -> ( n e. ( Z (,) W ) <-> ( n e. RR /\ Z < n /\ n < W ) ) )
45	35 43 44	syl2anc	\|- ( ( ( ph /\ ( y e. ( X [,] Y ) /\ A. z e. ( X [,] Y ) ( ( x e. ( X [,] Y ) \|-> A ) ` z ) <_ ( ( x e. ( X [,] Y ) \|-> A ) ` y ) ) ) /\ ( n e. QQ /\ ( ( ( x e. ( X [,] Y ) \|-> A ) ` y ) < n /\ n < W ) ) ) -> ( n e. ( Z (,) W ) <-> ( n e. RR /\ Z < n /\ n < W ) ) )
46	34 41 42 45	mpbir3and	\|- ( ( ( ph /\ ( y e. ( X [,] Y ) /\ A. z e. ( X [,] Y ) ( ( x e. ( X [,] Y ) \|-> A ) ` z ) <_ ( ( x e. ( X [,] Y ) \|-> A ) ` y ) ) ) /\ ( n e. QQ /\ ( ( ( x e. ( X [,] Y ) \|-> A ) ` y ) < n /\ n < W ) ) ) -> n e. ( Z (,) W ) )
47		anass	\|- ( ( ( ph /\ y e. ( X [,] Y ) ) /\ A. z e. ( X [,] Y ) ( ( x e. ( X [,] Y ) \|-> A ) ` z ) <_ ( ( x e. ( X [,] Y ) \|-> A ) ` y ) ) <-> ( ph /\ ( y e. ( X [,] Y ) /\ A. z e. ( X [,] Y ) ( ( x e. ( X [,] Y ) \|-> A ) ` z ) <_ ( ( x e. ( X [,] Y ) \|-> A ) ` y ) ) ) )
48		simprrl	\|- ( ( ( ph /\ y e. ( X [,] Y ) ) /\ ( n e. QQ /\ ( ( ( x e. ( X [,] Y ) \|-> A ) ` y ) < n /\ n < W ) ) ) -> ( ( x e. ( X [,] Y ) \|-> A ) ` y ) < n )
49	48	adantr	\|- ( ( ( ( ph /\ y e. ( X [,] Y ) ) /\ ( n e. QQ /\ ( ( ( x e. ( X [,] Y ) \|-> A ) ` y ) < n /\ n < W ) ) ) /\ z e. ( X [,] Y ) ) -> ( ( x e. ( X [,] Y ) \|-> A ) ` y ) < n )
50	22	ad2antrr	\|- ( ( ( ph /\ y e. ( X [,] Y ) ) /\ ( n e. QQ /\ ( ( ( x e. ( X [,] Y ) \|-> A ) ` y ) < n /\ n < W ) ) ) -> ( x e. ( X [,] Y ) \|-> A ) : ( X [,] Y ) --> ( Z (,) W ) )
51	50	ffvelcdmda	\|- ( ( ( ( ph /\ y e. ( X [,] Y ) ) /\ ( n e. QQ /\ ( ( ( x e. ( X [,] Y ) \|-> A ) ` y ) < n /\ n < W ) ) ) /\ z e. ( X [,] Y ) ) -> ( ( x e. ( X [,] Y ) \|-> A ) ` z ) e. ( Z (,) W ) )
52	20 51	sselid	\|- ( ( ( ( ph /\ y e. ( X [,] Y ) ) /\ ( n e. QQ /\ ( ( ( x e. ( X [,] Y ) \|-> A ) ` y ) < n /\ n < W ) ) ) /\ z e. ( X [,] Y ) ) -> ( ( x e. ( X [,] Y ) \|-> A ) ` z ) e. RR* )
53		simplr	\|- ( ( ( ph /\ y e. ( X [,] Y ) ) /\ ( n e. QQ /\ ( ( ( x e. ( X [,] Y ) \|-> A ) ` y ) < n /\ n < W ) ) ) -> y e. ( X [,] Y ) )
54	50 53	ffvelcdmd	\|- ( ( ( ph /\ y e. ( X [,] Y ) ) /\ ( n e. QQ /\ ( ( ( x e. ( X [,] Y ) \|-> A ) ` y ) < n /\ n < W ) ) ) -> ( ( x e. ( X [,] Y ) \|-> A ) ` y ) e. ( Z (,) W ) )
55	20 54	sselid	\|- ( ( ( ph /\ y e. ( X [,] Y ) ) /\ ( n e. QQ /\ ( ( ( x e. ( X [,] Y ) \|-> A ) ` y ) < n /\ n < W ) ) ) -> ( ( x e. ( X [,] Y ) \|-> A ) ` y ) e. RR* )
56	55	adantr	\|- ( ( ( ( ph /\ y e. ( X [,] Y ) ) /\ ( n e. QQ /\ ( ( ( x e. ( X [,] Y ) \|-> A ) ` y ) < n /\ n < W ) ) ) /\ z e. ( X [,] Y ) ) -> ( ( x e. ( X [,] Y ) \|-> A ) ` y ) e. RR* )
57	33	ad2antrl	\|- ( ( ( ph /\ y e. ( X [,] Y ) ) /\ ( n e. QQ /\ ( ( ( x e. ( X [,] Y ) \|-> A ) ` y ) < n /\ n < W ) ) ) -> n e. RR )
58	57	adantr	\|- ( ( ( ( ph /\ y e. ( X [,] Y ) ) /\ ( n e. QQ /\ ( ( ( x e. ( X [,] Y ) \|-> A ) ` y ) < n /\ n < W ) ) ) /\ z e. ( X [,] Y ) ) -> n e. RR )
59	58	rexrd	\|- ( ( ( ( ph /\ y e. ( X [,] Y ) ) /\ ( n e. QQ /\ ( ( ( x e. ( X [,] Y ) \|-> A ) ` y ) < n /\ n < W ) ) ) /\ z e. ( X [,] Y ) ) -> n e. RR* )
60		xrlelttr	\|- ( ( ( ( x e. ( X [,] Y ) \|-> A ) ` z ) e. RR* /\ ( ( x e. ( X [,] Y ) \|-> A ) ` y ) e. RR* /\ n e. RR* ) -> ( ( ( ( x e. ( X [,] Y ) \|-> A ) ` z ) <_ ( ( x e. ( X [,] Y ) \|-> A ) ` y ) /\ ( ( x e. ( X [,] Y ) \|-> A ) ` y ) < n ) -> ( ( x e. ( X [,] Y ) \|-> A ) ` z ) < n ) )
61	52 56 59 60	syl3anc	\|- ( ( ( ( ph /\ y e. ( X [,] Y ) ) /\ ( n e. QQ /\ ( ( ( x e. ( X [,] Y ) \|-> A ) ` y ) < n /\ n < W ) ) ) /\ z e. ( X [,] Y ) ) -> ( ( ( ( x e. ( X [,] Y ) \|-> A ) ` z ) <_ ( ( x e. ( X [,] Y ) \|-> A ) ` y ) /\ ( ( x e. ( X [,] Y ) \|-> A ) ` y ) < n ) -> ( ( x e. ( X [,] Y ) \|-> A ) ` z ) < n ) )
62	49 61	mpan2d	\|- ( ( ( ( ph /\ y e. ( X [,] Y ) ) /\ ( n e. QQ /\ ( ( ( x e. ( X [,] Y ) \|-> A ) ` y ) < n /\ n < W ) ) ) /\ z e. ( X [,] Y ) ) -> ( ( ( x e. ( X [,] Y ) \|-> A ) ` z ) <_ ( ( x e. ( X [,] Y ) \|-> A ) ` y ) -> ( ( x e. ( X [,] Y ) \|-> A ) ` z ) < n ) )
63	62	ralimdva	\|- ( ( ( ph /\ y e. ( X [,] Y ) ) /\ ( n e. QQ /\ ( ( ( x e. ( X [,] Y ) \|-> A ) ` y ) < n /\ n < W ) ) ) -> ( A. z e. ( X [,] Y ) ( ( x e. ( X [,] Y ) \|-> A ) ` z ) <_ ( ( x e. ( X [,] Y ) \|-> A ) ` y ) -> A. z e. ( X [,] Y ) ( ( x e. ( X [,] Y ) \|-> A ) ` z ) < n ) )
64	63	imp	\|- ( ( ( ( ph /\ y e. ( X [,] Y ) ) /\ ( n e. QQ /\ ( ( ( x e. ( X [,] Y ) \|-> A ) ` y ) < n /\ n < W ) ) ) /\ A. z e. ( X [,] Y ) ( ( x e. ( X [,] Y ) \|-> A ) ` z ) <_ ( ( x e. ( X [,] Y ) \|-> A ) ` y ) ) -> A. z e. ( X [,] Y ) ( ( x e. ( X [,] Y ) \|-> A ) ` z ) < n )
65	64	an32s	\|- ( ( ( ( ph /\ y e. ( X [,] Y ) ) /\ A. z e. ( X [,] Y ) ( ( x e. ( X [,] Y ) \|-> A ) ` z ) <_ ( ( x e. ( X [,] Y ) \|-> A ) ` y ) ) /\ ( n e. QQ /\ ( ( ( x e. ( X [,] Y ) \|-> A ) ` y ) < n /\ n < W ) ) ) -> A. z e. ( X [,] Y ) ( ( x e. ( X [,] Y ) \|-> A ) ` z ) < n )
66	47 65	sylanbr	\|- ( ( ( ph /\ ( y e. ( X [,] Y ) /\ A. z e. ( X [,] Y ) ( ( x e. ( X [,] Y ) \|-> A ) ` z ) <_ ( ( x e. ( X [,] Y ) \|-> A ) ` y ) ) ) /\ ( n e. QQ /\ ( ( ( x e. ( X [,] Y ) \|-> A ) ` y ) < n /\ n < W ) ) ) -> A. z e. ( X [,] Y ) ( ( x e. ( X [,] Y ) \|-> A ) ` z ) < n )
67	32 46 66	reximssdv	\|- ( ( ph /\ ( y e. ( X [,] Y ) /\ A. z e. ( X [,] Y ) ( ( x e. ( X [,] Y ) \|-> A ) ` z ) <_ ( ( x e. ( X [,] Y ) \|-> A ) ` y ) ) ) -> E. n e. ( Z (,) W ) A. z e. ( X [,] Y ) ( ( x e. ( X [,] Y ) \|-> A ) ` z ) < n )
68	67	rexlimdvaa	\|- ( ph -> ( E. y e. ( X [,] Y ) A. z e. ( X [,] Y ) ( ( x e. ( X [,] Y ) \|-> A ) ` z ) <_ ( ( x e. ( X [,] Y ) \|-> A ) ` y ) -> E. n e. ( Z (,) W ) A. z e. ( X [,] Y ) ( ( x e. ( X [,] Y ) \|-> A ) ` z ) < n ) )
69	4	adantr	\|- ( ( ph /\ ( y e. ( X [,] Y ) /\ A. z e. ( X [,] Y ) ( ( x e. ( X [,] Y ) \|-> A ) ` y ) <_ ( ( x e. ( X [,] Y ) \|-> A ) ` z ) ) ) -> Z e. RR* )
70	22	adantr	\|- ( ( ph /\ ( y e. ( X [,] Y ) /\ A. z e. ( X [,] Y ) ( ( x e. ( X [,] Y ) \|-> A ) ` y ) <_ ( ( x e. ( X [,] Y ) \|-> A ) ` z ) ) ) -> ( x e. ( X [,] Y ) \|-> A ) : ( X [,] Y ) --> ( Z (,) W ) )
71		simprl	\|- ( ( ph /\ ( y e. ( X [,] Y ) /\ A. z e. ( X [,] Y ) ( ( x e. ( X [,] Y ) \|-> A ) ` y ) <_ ( ( x e. ( X [,] Y ) \|-> A ) ` z ) ) ) -> y e. ( X [,] Y ) )
72	70 71	ffvelcdmd	\|- ( ( ph /\ ( y e. ( X [,] Y ) /\ A. z e. ( X [,] Y ) ( ( x e. ( X [,] Y ) \|-> A ) ` y ) <_ ( ( x e. ( X [,] Y ) \|-> A ) ` z ) ) ) -> ( ( x e. ( X [,] Y ) \|-> A ) ` y ) e. ( Z (,) W ) )
73	20 72	sselid	\|- ( ( ph /\ ( y e. ( X [,] Y ) /\ A. z e. ( X [,] Y ) ( ( x e. ( X [,] Y ) \|-> A ) ` y ) <_ ( ( x e. ( X [,] Y ) \|-> A ) ` z ) ) ) -> ( ( x e. ( X [,] Y ) \|-> A ) ` y ) e. RR* )
74	72 28	syl	\|- ( ( ph /\ ( y e. ( X [,] Y ) /\ A. z e. ( X [,] Y ) ( ( x e. ( X [,] Y ) \|-> A ) ` y ) <_ ( ( x e. ( X [,] Y ) \|-> A ) ` z ) ) ) -> ( Z < ( ( x e. ( X [,] Y ) \|-> A ) ` y ) /\ ( ( x e. ( X [,] Y ) \|-> A ) ` y ) < W ) )
75	74	simpld	\|- ( ( ph /\ ( y e. ( X [,] Y ) /\ A. z e. ( X [,] Y ) ( ( x e. ( X [,] Y ) \|-> A ) ` y ) <_ ( ( x e. ( X [,] Y ) \|-> A ) ` z ) ) ) -> Z < ( ( x e. ( X [,] Y ) \|-> A ) ` y ) )
76		qbtwnxr	\|- ( ( Z e. RR* /\ ( ( x e. ( X [,] Y ) \|-> A ) ` y ) e. RR* /\ Z < ( ( x e. ( X [,] Y ) \|-> A ) ` y ) ) -> E. m e. QQ ( Z < m /\ m < ( ( x e. ( X [,] Y ) \|-> A ) ` y ) ) )
77	69 73 75 76	syl3anc	\|- ( ( ph /\ ( y e. ( X [,] Y ) /\ A. z e. ( X [,] Y ) ( ( x e. ( X [,] Y ) \|-> A ) ` y ) <_ ( ( x e. ( X [,] Y ) \|-> A ) ` z ) ) ) -> E. m e. QQ ( Z < m /\ m < ( ( x e. ( X [,] Y ) \|-> A ) ` y ) ) )
78		qre	\|- ( m e. QQ -> m e. RR )
79	78	ad2antrl	\|- ( ( ( ph /\ ( y e. ( X [,] Y ) /\ A. z e. ( X [,] Y ) ( ( x e. ( X [,] Y ) \|-> A ) ` y ) <_ ( ( x e. ( X [,] Y ) \|-> A ) ` z ) ) ) /\ ( m e. QQ /\ ( Z < m /\ m < ( ( x e. ( X [,] Y ) \|-> A ) ` y ) ) ) ) -> m e. RR )
80		simprrl	\|- ( ( ( ph /\ ( y e. ( X [,] Y ) /\ A. z e. ( X [,] Y ) ( ( x e. ( X [,] Y ) \|-> A ) ` y ) <_ ( ( x e. ( X [,] Y ) \|-> A ) ` z ) ) ) /\ ( m e. QQ /\ ( Z < m /\ m < ( ( x e. ( X [,] Y ) \|-> A ) ` y ) ) ) ) -> Z < m )
81	79	rexrd	\|- ( ( ( ph /\ ( y e. ( X [,] Y ) /\ A. z e. ( X [,] Y ) ( ( x e. ( X [,] Y ) \|-> A ) ` y ) <_ ( ( x e. ( X [,] Y ) \|-> A ) ` z ) ) ) /\ ( m e. QQ /\ ( Z < m /\ m < ( ( x e. ( X [,] Y ) \|-> A ) ` y ) ) ) ) -> m e. RR* )
82	73	adantr	\|- ( ( ( ph /\ ( y e. ( X [,] Y ) /\ A. z e. ( X [,] Y ) ( ( x e. ( X [,] Y ) \|-> A ) ` y ) <_ ( ( x e. ( X [,] Y ) \|-> A ) ` z ) ) ) /\ ( m e. QQ /\ ( Z < m /\ m < ( ( x e. ( X [,] Y ) \|-> A ) ` y ) ) ) ) -> ( ( x e. ( X [,] Y ) \|-> A ) ` y ) e. RR* )
83	5	ad2antrr	\|- ( ( ( ph /\ ( y e. ( X [,] Y ) /\ A. z e. ( X [,] Y ) ( ( x e. ( X [,] Y ) \|-> A ) ` y ) <_ ( ( x e. ( X [,] Y ) \|-> A ) ` z ) ) ) /\ ( m e. QQ /\ ( Z < m /\ m < ( ( x e. ( X [,] Y ) \|-> A ) ` y ) ) ) ) -> W e. RR* )
84		simprrr	\|- ( ( ( ph /\ ( y e. ( X [,] Y ) /\ A. z e. ( X [,] Y ) ( ( x e. ( X [,] Y ) \|-> A ) ` y ) <_ ( ( x e. ( X [,] Y ) \|-> A ) ` z ) ) ) /\ ( m e. QQ /\ ( Z < m /\ m < ( ( x e. ( X [,] Y ) \|-> A ) ` y ) ) ) ) -> m < ( ( x e. ( X [,] Y ) \|-> A ) ` y ) )
85	74	simprd	\|- ( ( ph /\ ( y e. ( X [,] Y ) /\ A. z e. ( X [,] Y ) ( ( x e. ( X [,] Y ) \|-> A ) ` y ) <_ ( ( x e. ( X [,] Y ) \|-> A ) ` z ) ) ) -> ( ( x e. ( X [,] Y ) \|-> A ) ` y ) < W )
86	85	adantr	\|- ( ( ( ph /\ ( y e. ( X [,] Y ) /\ A. z e. ( X [,] Y ) ( ( x e. ( X [,] Y ) \|-> A ) ` y ) <_ ( ( x e. ( X [,] Y ) \|-> A ) ` z ) ) ) /\ ( m e. QQ /\ ( Z < m /\ m < ( ( x e. ( X [,] Y ) \|-> A ) ` y ) ) ) ) -> ( ( x e. ( X [,] Y ) \|-> A ) ` y ) < W )
87	81 82 83 84 86	xrlttrd	\|- ( ( ( ph /\ ( y e. ( X [,] Y ) /\ A. z e. ( X [,] Y ) ( ( x e. ( X [,] Y ) \|-> A ) ` y ) <_ ( ( x e. ( X [,] Y ) \|-> A ) ` z ) ) ) /\ ( m e. QQ /\ ( Z < m /\ m < ( ( x e. ( X [,] Y ) \|-> A ) ` y ) ) ) ) -> m < W )
88	4	ad2antrr	\|- ( ( ( ph /\ ( y e. ( X [,] Y ) /\ A. z e. ( X [,] Y ) ( ( x e. ( X [,] Y ) \|-> A ) ` y ) <_ ( ( x e. ( X [,] Y ) \|-> A ) ` z ) ) ) /\ ( m e. QQ /\ ( Z < m /\ m < ( ( x e. ( X [,] Y ) \|-> A ) ` y ) ) ) ) -> Z e. RR* )
89		elioo2	\|- ( ( Z e. RR* /\ W e. RR* ) -> ( m e. ( Z (,) W ) <-> ( m e. RR /\ Z < m /\ m < W ) ) )
90	88 83 89	syl2anc	\|- ( ( ( ph /\ ( y e. ( X [,] Y ) /\ A. z e. ( X [,] Y ) ( ( x e. ( X [,] Y ) \|-> A ) ` y ) <_ ( ( x e. ( X [,] Y ) \|-> A ) ` z ) ) ) /\ ( m e. QQ /\ ( Z < m /\ m < ( ( x e. ( X [,] Y ) \|-> A ) ` y ) ) ) ) -> ( m e. ( Z (,) W ) <-> ( m e. RR /\ Z < m /\ m < W ) ) )
91	79 80 87 90	mpbir3and	\|- ( ( ( ph /\ ( y e. ( X [,] Y ) /\ A. z e. ( X [,] Y ) ( ( x e. ( X [,] Y ) \|-> A ) ` y ) <_ ( ( x e. ( X [,] Y ) \|-> A ) ` z ) ) ) /\ ( m e. QQ /\ ( Z < m /\ m < ( ( x e. ( X [,] Y ) \|-> A ) ` y ) ) ) ) -> m e. ( Z (,) W ) )
92		anass	\|- ( ( ( ph /\ y e. ( X [,] Y ) ) /\ A. z e. ( X [,] Y ) ( ( x e. ( X [,] Y ) \|-> A ) ` y ) <_ ( ( x e. ( X [,] Y ) \|-> A ) ` z ) ) <-> ( ph /\ ( y e. ( X [,] Y ) /\ A. z e. ( X [,] Y ) ( ( x e. ( X [,] Y ) \|-> A ) ` y ) <_ ( ( x e. ( X [,] Y ) \|-> A ) ` z ) ) ) )
93		simprrr	\|- ( ( ( ph /\ y e. ( X [,] Y ) ) /\ ( m e. QQ /\ ( Z < m /\ m < ( ( x e. ( X [,] Y ) \|-> A ) ` y ) ) ) ) -> m < ( ( x e. ( X [,] Y ) \|-> A ) ` y ) )
94	93	adantr	\|- ( ( ( ( ph /\ y e. ( X [,] Y ) ) /\ ( m e. QQ /\ ( Z < m /\ m < ( ( x e. ( X [,] Y ) \|-> A ) ` y ) ) ) ) /\ z e. ( X [,] Y ) ) -> m < ( ( x e. ( X [,] Y ) \|-> A ) ` y ) )
95	78	ad2antrl	\|- ( ( ( ph /\ y e. ( X [,] Y ) ) /\ ( m e. QQ /\ ( Z < m /\ m < ( ( x e. ( X [,] Y ) \|-> A ) ` y ) ) ) ) -> m e. RR )
96	95	adantr	\|- ( ( ( ( ph /\ y e. ( X [,] Y ) ) /\ ( m e. QQ /\ ( Z < m /\ m < ( ( x e. ( X [,] Y ) \|-> A ) ` y ) ) ) ) /\ z e. ( X [,] Y ) ) -> m e. RR )
97	96	rexrd	\|- ( ( ( ( ph /\ y e. ( X [,] Y ) ) /\ ( m e. QQ /\ ( Z < m /\ m < ( ( x e. ( X [,] Y ) \|-> A ) ` y ) ) ) ) /\ z e. ( X [,] Y ) ) -> m e. RR* )
98	22	ad2antrr	\|- ( ( ( ph /\ y e. ( X [,] Y ) ) /\ ( m e. QQ /\ ( Z < m /\ m < ( ( x e. ( X [,] Y ) \|-> A ) ` y ) ) ) ) -> ( x e. ( X [,] Y ) \|-> A ) : ( X [,] Y ) --> ( Z (,) W ) )
99		simplr	\|- ( ( ( ph /\ y e. ( X [,] Y ) ) /\ ( m e. QQ /\ ( Z < m /\ m < ( ( x e. ( X [,] Y ) \|-> A ) ` y ) ) ) ) -> y e. ( X [,] Y ) )
100	98 99	ffvelcdmd	\|- ( ( ( ph /\ y e. ( X [,] Y ) ) /\ ( m e. QQ /\ ( Z < m /\ m < ( ( x e. ( X [,] Y ) \|-> A ) ` y ) ) ) ) -> ( ( x e. ( X [,] Y ) \|-> A ) ` y ) e. ( Z (,) W ) )
101	20 100	sselid	\|- ( ( ( ph /\ y e. ( X [,] Y ) ) /\ ( m e. QQ /\ ( Z < m /\ m < ( ( x e. ( X [,] Y ) \|-> A ) ` y ) ) ) ) -> ( ( x e. ( X [,] Y ) \|-> A ) ` y ) e. RR* )
102	101	adantr	\|- ( ( ( ( ph /\ y e. ( X [,] Y ) ) /\ ( m e. QQ /\ ( Z < m /\ m < ( ( x e. ( X [,] Y ) \|-> A ) ` y ) ) ) ) /\ z e. ( X [,] Y ) ) -> ( ( x e. ( X [,] Y ) \|-> A ) ` y ) e. RR* )
103	98	ffvelcdmda	\|- ( ( ( ( ph /\ y e. ( X [,] Y ) ) /\ ( m e. QQ /\ ( Z < m /\ m < ( ( x e. ( X [,] Y ) \|-> A ) ` y ) ) ) ) /\ z e. ( X [,] Y ) ) -> ( ( x e. ( X [,] Y ) \|-> A ) ` z ) e. ( Z (,) W ) )
104	20 103	sselid	\|- ( ( ( ( ph /\ y e. ( X [,] Y ) ) /\ ( m e. QQ /\ ( Z < m /\ m < ( ( x e. ( X [,] Y ) \|-> A ) ` y ) ) ) ) /\ z e. ( X [,] Y ) ) -> ( ( x e. ( X [,] Y ) \|-> A ) ` z ) e. RR* )
105		xrltletr	\|- ( ( m e. RR* /\ ( ( x e. ( X [,] Y ) \|-> A ) ` y ) e. RR* /\ ( ( x e. ( X [,] Y ) \|-> A ) ` z ) e. RR* ) -> ( ( m < ( ( x e. ( X [,] Y ) \|-> A ) ` y ) /\ ( ( x e. ( X [,] Y ) \|-> A ) ` y ) <_ ( ( x e. ( X [,] Y ) \|-> A ) ` z ) ) -> m < ( ( x e. ( X [,] Y ) \|-> A ) ` z ) ) )
106	97 102 104 105	syl3anc	\|- ( ( ( ( ph /\ y e. ( X [,] Y ) ) /\ ( m e. QQ /\ ( Z < m /\ m < ( ( x e. ( X [,] Y ) \|-> A ) ` y ) ) ) ) /\ z e. ( X [,] Y ) ) -> ( ( m < ( ( x e. ( X [,] Y ) \|-> A ) ` y ) /\ ( ( x e. ( X [,] Y ) \|-> A ) ` y ) <_ ( ( x e. ( X [,] Y ) \|-> A ) ` z ) ) -> m < ( ( x e. ( X [,] Y ) \|-> A ) ` z ) ) )
107	94 106	mpand	\|- ( ( ( ( ph /\ y e. ( X [,] Y ) ) /\ ( m e. QQ /\ ( Z < m /\ m < ( ( x e. ( X [,] Y ) \|-> A ) ` y ) ) ) ) /\ z e. ( X [,] Y ) ) -> ( ( ( x e. ( X [,] Y ) \|-> A ) ` y ) <_ ( ( x e. ( X [,] Y ) \|-> A ) ` z ) -> m < ( ( x e. ( X [,] Y ) \|-> A ) ` z ) ) )
108	107	ralimdva	\|- ( ( ( ph /\ y e. ( X [,] Y ) ) /\ ( m e. QQ /\ ( Z < m /\ m < ( ( x e. ( X [,] Y ) \|-> A ) ` y ) ) ) ) -> ( A. z e. ( X [,] Y ) ( ( x e. ( X [,] Y ) \|-> A ) ` y ) <_ ( ( x e. ( X [,] Y ) \|-> A ) ` z ) -> A. z e. ( X [,] Y ) m < ( ( x e. ( X [,] Y ) \|-> A ) ` z ) ) )
109	108	imp	\|- ( ( ( ( ph /\ y e. ( X [,] Y ) ) /\ ( m e. QQ /\ ( Z < m /\ m < ( ( x e. ( X [,] Y ) \|-> A ) ` y ) ) ) ) /\ A. z e. ( X [,] Y ) ( ( x e. ( X [,] Y ) \|-> A ) ` y ) <_ ( ( x e. ( X [,] Y ) \|-> A ) ` z ) ) -> A. z e. ( X [,] Y ) m < ( ( x e. ( X [,] Y ) \|-> A ) ` z ) )
110	109	an32s	\|- ( ( ( ( ph /\ y e. ( X [,] Y ) ) /\ A. z e. ( X [,] Y ) ( ( x e. ( X [,] Y ) \|-> A ) ` y ) <_ ( ( x e. ( X [,] Y ) \|-> A ) ` z ) ) /\ ( m e. QQ /\ ( Z < m /\ m < ( ( x e. ( X [,] Y ) \|-> A ) ` y ) ) ) ) -> A. z e. ( X [,] Y ) m < ( ( x e. ( X [,] Y ) \|-> A ) ` z ) )
111	92 110	sylanbr	\|- ( ( ( ph /\ ( y e. ( X [,] Y ) /\ A. z e. ( X [,] Y ) ( ( x e. ( X [,] Y ) \|-> A ) ` y ) <_ ( ( x e. ( X [,] Y ) \|-> A ) ` z ) ) ) /\ ( m e. QQ /\ ( Z < m /\ m < ( ( x e. ( X [,] Y ) \|-> A ) ` y ) ) ) ) -> A. z e. ( X [,] Y ) m < ( ( x e. ( X [,] Y ) \|-> A ) ` z ) )
112	77 91 111	reximssdv	\|- ( ( ph /\ ( y e. ( X [,] Y ) /\ A. z e. ( X [,] Y ) ( ( x e. ( X [,] Y ) \|-> A ) ` y ) <_ ( ( x e. ( X [,] Y ) \|-> A ) ` z ) ) ) -> E. m e. ( Z (,) W ) A. z e. ( X [,] Y ) m < ( ( x e. ( X [,] Y ) \|-> A ) ` z ) )
113	112	rexlimdvaa	\|- ( ph -> ( E. y e. ( X [,] Y ) A. z e. ( X [,] Y ) ( ( x e. ( X [,] Y ) \|-> A ) ` y ) <_ ( ( x e. ( X [,] Y ) \|-> A ) ` z ) -> E. m e. ( Z (,) W ) A. z e. ( X [,] Y ) m < ( ( x e. ( X [,] Y ) \|-> A ) ` z ) ) )
114		ancom	\|- ( ( E. n e. ( Z (,) W ) A. z e. ( X [,] Y ) ( ( x e. ( X [,] Y ) \|-> A ) ` z ) < n /\ E. m e. ( Z (,) W ) A. z e. ( X [,] Y ) m < ( ( x e. ( X [,] Y ) \|-> A ) ` z ) ) <-> ( E. m e. ( Z (,) W ) A. z e. ( X [,] Y ) m < ( ( x e. ( X [,] Y ) \|-> A ) ` z ) /\ E. n e. ( Z (,) W ) A. z e. ( X [,] Y ) ( ( x e. ( X [,] Y ) \|-> A ) ` z ) < n ) )
115		reeanv	\|- ( E. m e. ( Z (,) W ) E. n e. ( Z (,) W ) ( A. z e. ( X [,] Y ) m < ( ( x e. ( X [,] Y ) \|-> A ) ` z ) /\ A. z e. ( X [,] Y ) ( ( x e. ( X [,] Y ) \|-> A ) ` z ) < n ) <-> ( E. m e. ( Z (,) W ) A. z e. ( X [,] Y ) m < ( ( x e. ( X [,] Y ) \|-> A ) ` z ) /\ E. n e. ( Z (,) W ) A. z e. ( X [,] Y ) ( ( x e. ( X [,] Y ) \|-> A ) ` z ) < n ) )
116	114 115	bitr4i	\|- ( ( E. n e. ( Z (,) W ) A. z e. ( X [,] Y ) ( ( x e. ( X [,] Y ) \|-> A ) ` z ) < n /\ E. m e. ( Z (,) W ) A. z e. ( X [,] Y ) m < ( ( x e. ( X [,] Y ) \|-> A ) ` z ) ) <-> E. m e. ( Z (,) W ) E. n e. ( Z (,) W ) ( A. z e. ( X [,] Y ) m < ( ( x e. ( X [,] Y ) \|-> A ) ` z ) /\ A. z e. ( X [,] Y ) ( ( x e. ( X [,] Y ) \|-> A ) ` z ) < n ) )
117		r19.26	\|- ( A. z e. ( X [,] Y ) ( m < ( ( x e. ( X [,] Y ) \|-> A ) ` z ) /\ ( ( x e. ( X [,] Y ) \|-> A ) ` z ) < n ) <-> ( A. z e. ( X [,] Y ) m < ( ( x e. ( X [,] Y ) \|-> A ) ` z ) /\ A. z e. ( X [,] Y ) ( ( x e. ( X [,] Y ) \|-> A ) ` z ) < n ) )
118	22	adantr	\|- ( ( ph /\ ( m e. ( Z (,) W ) /\ n e. ( Z (,) W ) ) ) -> ( x e. ( X [,] Y ) \|-> A ) : ( X [,] Y ) --> ( Z (,) W ) )
119	118	ffvelcdmda	\|- ( ( ( ph /\ ( m e. ( Z (,) W ) /\ n e. ( Z (,) W ) ) ) /\ z e. ( X [,] Y ) ) -> ( ( x e. ( X [,] Y ) \|-> A ) ` z ) e. ( Z (,) W ) )
120	13 119	sselid	\|- ( ( ( ph /\ ( m e. ( Z (,) W ) /\ n e. ( Z (,) W ) ) ) /\ z e. ( X [,] Y ) ) -> ( ( x e. ( X [,] Y ) \|-> A ) ` z ) e. RR )
121	120	3biant1d	\|- ( ( ( ph /\ ( m e. ( Z (,) W ) /\ n e. ( Z (,) W ) ) ) /\ z e. ( X [,] Y ) ) -> ( ( m < ( ( x e. ( X [,] Y ) \|-> A ) ` z ) /\ ( ( x e. ( X [,] Y ) \|-> A ) ` z ) < n ) <-> ( ( ( x e. ( X [,] Y ) \|-> A ) ` z ) e. RR /\ m < ( ( x e. ( X [,] Y ) \|-> A ) ` z ) /\ ( ( x e. ( X [,] Y ) \|-> A ) ` z ) < n ) ) )
122		simplrl	\|- ( ( ( ph /\ ( m e. ( Z (,) W ) /\ n e. ( Z (,) W ) ) ) /\ z e. ( X [,] Y ) ) -> m e. ( Z (,) W ) )
123	20 122	sselid	\|- ( ( ( ph /\ ( m e. ( Z (,) W ) /\ n e. ( Z (,) W ) ) ) /\ z e. ( X [,] Y ) ) -> m e. RR* )
124		simplrr	\|- ( ( ( ph /\ ( m e. ( Z (,) W ) /\ n e. ( Z (,) W ) ) ) /\ z e. ( X [,] Y ) ) -> n e. ( Z (,) W ) )
125	20 124	sselid	\|- ( ( ( ph /\ ( m e. ( Z (,) W ) /\ n e. ( Z (,) W ) ) ) /\ z e. ( X [,] Y ) ) -> n e. RR* )
126		elioo2	\|- ( ( m e. RR* /\ n e. RR* ) -> ( ( ( x e. ( X [,] Y ) \|-> A ) ` z ) e. ( m (,) n ) <-> ( ( ( x e. ( X [,] Y ) \|-> A ) ` z ) e. RR /\ m < ( ( x e. ( X [,] Y ) \|-> A ) ` z ) /\ ( ( x e. ( X [,] Y ) \|-> A ) ` z ) < n ) ) )
127	123 125 126	syl2anc	\|- ( ( ( ph /\ ( m e. ( Z (,) W ) /\ n e. ( Z (,) W ) ) ) /\ z e. ( X [,] Y ) ) -> ( ( ( x e. ( X [,] Y ) \|-> A ) ` z ) e. ( m (,) n ) <-> ( ( ( x e. ( X [,] Y ) \|-> A ) ` z ) e. RR /\ m < ( ( x e. ( X [,] Y ) \|-> A ) ` z ) /\ ( ( x e. ( X [,] Y ) \|-> A ) ` z ) < n ) ) )
128	121 127	bitr4d	\|- ( ( ( ph /\ ( m e. ( Z (,) W ) /\ n e. ( Z (,) W ) ) ) /\ z e. ( X [,] Y ) ) -> ( ( m < ( ( x e. ( X [,] Y ) \|-> A ) ` z ) /\ ( ( x e. ( X [,] Y ) \|-> A ) ` z ) < n ) <-> ( ( x e. ( X [,] Y ) \|-> A ) ` z ) e. ( m (,) n ) ) )
129	128	ralbidva	\|- ( ( ph /\ ( m e. ( Z (,) W ) /\ n e. ( Z (,) W ) ) ) -> ( A. z e. ( X [,] Y ) ( m < ( ( x e. ( X [,] Y ) \|-> A ) ` z ) /\ ( ( x e. ( X [,] Y ) \|-> A ) ` z ) < n ) <-> A. z e. ( X [,] Y ) ( ( x e. ( X [,] Y ) \|-> A ) ` z ) e. ( m (,) n ) ) )
130		nffvmpt1	\|- F/_ x ( ( x e. ( X [,] Y ) \|-> A ) ` z )
131	130	nfel1	\|- F/ x ( ( x e. ( X [,] Y ) \|-> A ) ` z ) e. ( m (,) n )
132		nfv	\|- F/ z ( ( x e. ( X [,] Y ) \|-> A ) ` x ) e. ( m (,) n )
133		fveq2	\|- ( z = x -> ( ( x e. ( X [,] Y ) \|-> A ) ` z ) = ( ( x e. ( X [,] Y ) \|-> A ) ` x ) )
134	133	eleq1d	\|- ( z = x -> ( ( ( x e. ( X [,] Y ) \|-> A ) ` z ) e. ( m (,) n ) <-> ( ( x e. ( X [,] Y ) \|-> A ) ` x ) e. ( m (,) n ) ) )
135	131 132 134	cbvralw	\|- ( A. z e. ( X [,] Y ) ( ( x e. ( X [,] Y ) \|-> A ) ` z ) e. ( m (,) n ) <-> A. x e. ( X [,] Y ) ( ( x e. ( X [,] Y ) \|-> A ) ` x ) e. ( m (,) n ) )
136		simpr	\|- ( ( ph /\ x e. ( X [,] Y ) ) -> x e. ( X [,] Y ) )
137	22	fvmptelcdm	\|- ( ( ph /\ x e. ( X [,] Y ) ) -> A e. ( Z (,) W ) )
138		eqid	\|- ( x e. ( X [,] Y ) \|-> A ) = ( x e. ( X [,] Y ) \|-> A )
139	138	fvmpt2	\|- ( ( x e. ( X [,] Y ) /\ A e. ( Z (,) W ) ) -> ( ( x e. ( X [,] Y ) \|-> A ) ` x ) = A )
140	136 137 139	syl2anc	\|- ( ( ph /\ x e. ( X [,] Y ) ) -> ( ( x e. ( X [,] Y ) \|-> A ) ` x ) = A )
141	140	eleq1d	\|- ( ( ph /\ x e. ( X [,] Y ) ) -> ( ( ( x e. ( X [,] Y ) \|-> A ) ` x ) e. ( m (,) n ) <-> A e. ( m (,) n ) ) )
142	141	ralbidva	\|- ( ph -> ( A. x e. ( X [,] Y ) ( ( x e. ( X [,] Y ) \|-> A ) ` x ) e. ( m (,) n ) <-> A. x e. ( X [,] Y ) A e. ( m (,) n ) ) )
143	135 142	bitrid	\|- ( ph -> ( A. z e. ( X [,] Y ) ( ( x e. ( X [,] Y ) \|-> A ) ` z ) e. ( m (,) n ) <-> A. x e. ( X [,] Y ) A e. ( m (,) n ) ) )
144	143	adantr	\|- ( ( ph /\ ( m e. ( Z (,) W ) /\ n e. ( Z (,) W ) ) ) -> ( A. z e. ( X [,] Y ) ( ( x e. ( X [,] Y ) \|-> A ) ` z ) e. ( m (,) n ) <-> A. x e. ( X [,] Y ) A e. ( m (,) n ) ) )
145	1	adantr	\|- ( ( ph /\ ( ( m e. ( Z (,) W ) /\ n e. ( Z (,) W ) ) /\ A. x e. ( X [,] Y ) A e. ( m (,) n ) ) ) -> X e. RR )
146	2	adantr	\|- ( ( ph /\ ( ( m e. ( Z (,) W ) /\ n e. ( Z (,) W ) ) /\ A. x e. ( X [,] Y ) A e. ( m (,) n ) ) ) -> Y e. RR )
147	3	adantr	\|- ( ( ph /\ ( ( m e. ( Z (,) W ) /\ n e. ( Z (,) W ) ) /\ A. x e. ( X [,] Y ) A e. ( m (,) n ) ) ) -> X <_ Y )
148	4	adantr	\|- ( ( ph /\ ( ( m e. ( Z (,) W ) /\ n e. ( Z (,) W ) ) /\ A. x e. ( X [,] Y ) A e. ( m (,) n ) ) ) -> Z e. RR* )
149	5	adantr	\|- ( ( ph /\ ( ( m e. ( Z (,) W ) /\ n e. ( Z (,) W ) ) /\ A. x e. ( X [,] Y ) A e. ( m (,) n ) ) ) -> W e. RR* )
150		nfcv	\|- F/_ y A
151		nfcsb1v	\|- F/_ x [_ y / x ]_ A
152		csbeq1a	\|- ( x = y -> A = [_ y / x ]_ A )
153	150 151 152	cbvmpt	\|- ( x e. ( X [,] Y ) \|-> A ) = ( y e. ( X [,] Y ) \|-> [_ y / x ]_ A )
154	153 6	eqeltrrid	\|- ( ph -> ( y e. ( X [,] Y ) \|-> [_ y / x ]_ A ) e. ( ( X [,] Y ) -cn-> ( Z (,) W ) ) )
155	154	adantr	\|- ( ( ph /\ ( ( m e. ( Z (,) W ) /\ n e. ( Z (,) W ) ) /\ A. x e. ( X [,] Y ) A e. ( m (,) n ) ) ) -> ( y e. ( X [,] Y ) \|-> [_ y / x ]_ A ) e. ( ( X [,] Y ) -cn-> ( Z (,) W ) ) )
156		nfcv	\|- F/_ y B
157		nfcsb1v	\|- F/_ x [_ y / x ]_ B
158		csbeq1a	\|- ( x = y -> B = [_ y / x ]_ B )
159	156 157 158	cbvmpt	\|- ( x e. ( X (,) Y ) \|-> B ) = ( y e. ( X (,) Y ) \|-> [_ y / x ]_ B )
160	159 7	eqeltrrid	\|- ( ph -> ( y e. ( X (,) Y ) \|-> [_ y / x ]_ B ) e. ( ( ( X (,) Y ) -cn-> CC ) i^i L^1 ) )
161	160	adantr	\|- ( ( ph /\ ( ( m e. ( Z (,) W ) /\ n e. ( Z (,) W ) ) /\ A. x e. ( X [,] Y ) A e. ( m (,) n ) ) ) -> ( y e. ( X (,) Y ) \|-> [_ y / x ]_ B ) e. ( ( ( X (,) Y ) -cn-> CC ) i^i L^1 ) )
162		nfcv	\|- F/_ v C
163		nfcsb1v	\|- F/_ u [_ v / u ]_ C
164		csbeq1a	\|- ( u = v -> C = [_ v / u ]_ C )
165	162 163 164	cbvmpt	\|- ( u e. ( Z (,) W ) \|-> C ) = ( v e. ( Z (,) W ) \|-> [_ v / u ]_ C )
166	165 8	eqeltrrid	\|- ( ph -> ( v e. ( Z (,) W ) \|-> [_ v / u ]_ C ) e. ( ( Z (,) W ) -cn-> CC ) )
167	166	adantr	\|- ( ( ph /\ ( ( m e. ( Z (,) W ) /\ n e. ( Z (,) W ) ) /\ A. x e. ( X [,] Y ) A e. ( m (,) n ) ) ) -> ( v e. ( Z (,) W ) \|-> [_ v / u ]_ C ) e. ( ( Z (,) W ) -cn-> CC ) )
168	153	oveq2i	\|- ( RR _D ( x e. ( X [,] Y ) \|-> A ) ) = ( RR _D ( y e. ( X [,] Y ) \|-> [_ y / x ]_ A ) )
169	9 168 159	3eqtr3g	\|- ( ph -> ( RR _D ( y e. ( X [,] Y ) \|-> [_ y / x ]_ A ) ) = ( y e. ( X (,) Y ) \|-> [_ y / x ]_ B ) )
170	169	adantr	\|- ( ( ph /\ ( ( m e. ( Z (,) W ) /\ n e. ( Z (,) W ) ) /\ A. x e. ( X [,] Y ) A e. ( m (,) n ) ) ) -> ( RR _D ( y e. ( X [,] Y ) \|-> [_ y / x ]_ A ) ) = ( y e. ( X (,) Y ) \|-> [_ y / x ]_ B ) )
171		csbeq1	\|- ( v = [_ y / x ]_ A -> [_ v / u ]_ C = [_ [_ y / x ]_ A / u ]_ C )
172		csbeq1	\|- ( y = X -> [_ y / x ]_ A = [_ X / x ]_ A )
173		csbeq1	\|- ( y = Y -> [_ y / x ]_ A = [_ Y / x ]_ A )
174		simprll	\|- ( ( ph /\ ( ( m e. ( Z (,) W ) /\ n e. ( Z (,) W ) ) /\ A. x e. ( X [,] Y ) A e. ( m (,) n ) ) ) -> m e. ( Z (,) W ) )
175		simprlr	\|- ( ( ph /\ ( ( m e. ( Z (,) W ) /\ n e. ( Z (,) W ) ) /\ A. x e. ( X [,] Y ) A e. ( m (,) n ) ) ) -> n e. ( Z (,) W ) )
176		simprr	\|- ( ( ph /\ ( ( m e. ( Z (,) W ) /\ n e. ( Z (,) W ) ) /\ A. x e. ( X [,] Y ) A e. ( m (,) n ) ) ) -> A. x e. ( X [,] Y ) A e. ( m (,) n ) )
177	151	nfel1	\|- F/ x [_ y / x ]_ A e. ( m (,) n )
178	152	eleq1d	\|- ( x = y -> ( A e. ( m (,) n ) <-> [_ y / x ]_ A e. ( m (,) n ) ) )
179	177 178	rspc	\|- ( y e. ( X [,] Y ) -> ( A. x e. ( X [,] Y ) A e. ( m (,) n ) -> [_ y / x ]_ A e. ( m (,) n ) ) )
180	176 179	mpan9	\|- ( ( ( ph /\ ( ( m e. ( Z (,) W ) /\ n e. ( Z (,) W ) ) /\ A. x e. ( X [,] Y ) A e. ( m (,) n ) ) ) /\ y e. ( X [,] Y ) ) -> [_ y / x ]_ A e. ( m (,) n ) )
181	145 146 147 148 149 155 161 167 170 171 172 173 174 175 180	itgsubstlem	\|- ( ( ph /\ ( ( m e. ( Z (,) W ) /\ n e. ( Z (,) W ) ) /\ A. x e. ( X [,] Y ) A e. ( m (,) n ) ) ) -> S_ [ [_ X / x ]_ A -> [_ Y / x ]_ A ] [_ v / u ]_ C _d v = S_ [ X -> Y ] ( [_ [_ y / x ]_ A / u ]_ C x. [_ y / x ]_ B ) _d y )
182	164 162 163	cbvditg	\|- S_ [ [_ X / x ]_ A -> [_ Y / x ]_ A ] C _d u = S_ [ [_ X / x ]_ A -> [_ Y / x ]_ A ] [_ v / u ]_ C _d v
183		nfcvd	\|- ( X e. RR -> F/_ x K )
184	183 11	csbiegf	\|- ( X e. RR -> [_ X / x ]_ A = K )
185		ditgeq1	\|- ( [_ X / x ]_ A = K -> S_ [ [_ X / x ]_ A -> [_ Y / x ]_ A ] C _d u = S_ [ K -> [_ Y / x ]_ A ] C _d u )
186	1 184 185	3syl	\|- ( ph -> S_ [ [_ X / x ]_ A -> [_ Y / x ]_ A ] C _d u = S_ [ K -> [_ Y / x ]_ A ] C _d u )
187		nfcvd	\|- ( Y e. RR -> F/_ x L )
188	187 12	csbiegf	\|- ( Y e. RR -> [_ Y / x ]_ A = L )
189		ditgeq2	\|- ( [_ Y / x ]_ A = L -> S_ [ K -> [_ Y / x ]_ A ] C _d u = S_ [ K -> L ] C _d u )
190	2 188 189	3syl	\|- ( ph -> S_ [ K -> [_ Y / x ]_ A ] C _d u = S_ [ K -> L ] C _d u )
191	186 190	eqtrd	\|- ( ph -> S_ [ [_ X / x ]_ A -> [_ Y / x ]_ A ] C _d u = S_ [ K -> L ] C _d u )
192	182 191	eqtr3id	\|- ( ph -> S_ [ [_ X / x ]_ A -> [_ Y / x ]_ A ] [_ v / u ]_ C _d v = S_ [ K -> L ] C _d u )
193	192	adantr	\|- ( ( ph /\ ( ( m e. ( Z (,) W ) /\ n e. ( Z (,) W ) ) /\ A. x e. ( X [,] Y ) A e. ( m (,) n ) ) ) -> S_ [ [_ X / x ]_ A -> [_ Y / x ]_ A ] [_ v / u ]_ C _d v = S_ [ K -> L ] C _d u )
194	152	csbeq1d	\|- ( x = y -> [_ A / u ]_ C = [_ [_ y / x ]_ A / u ]_ C )
195	194 158	oveq12d	\|- ( x = y -> ( [_ A / u ]_ C x. B ) = ( [_ [_ y / x ]_ A / u ]_ C x. [_ y / x ]_ B ) )
196		nfcv	\|- F/_ y ( [_ A / u ]_ C x. B )
197		nfcv	\|- F/_ x C
198	151 197	nfcsbw	\|- F/_ x [_ [_ y / x ]_ A / u ]_ C
199		nfcv	\|- F/_ x x.
200	198 199 157	nfov	\|- F/_ x ( [_ [_ y / x ]_ A / u ]_ C x. [_ y / x ]_ B )
201	195 196 200	cbvditg	\|- S_ [ X -> Y ] ( [_ A / u ]_ C x. B ) _d x = S_ [ X -> Y ] ( [_ [_ y / x ]_ A / u ]_ C x. [_ y / x ]_ B ) _d y
202		ioossicc	\|- ( X (,) Y ) C_ ( X [,] Y )
203	202	sseli	\|- ( x e. ( X (,) Y ) -> x e. ( X [,] Y ) )
204	203 137	sylan2	\|- ( ( ph /\ x e. ( X (,) Y ) ) -> A e. ( Z (,) W ) )
205		nfcvd	\|- ( A e. ( Z (,) W ) -> F/_ u E )
206	205 10	csbiegf	\|- ( A e. ( Z (,) W ) -> [_ A / u ]_ C = E )
207	204 206	syl	\|- ( ( ph /\ x e. ( X (,) Y ) ) -> [_ A / u ]_ C = E )
208	207	oveq1d	\|- ( ( ph /\ x e. ( X (,) Y ) ) -> ( [_ A / u ]_ C x. B ) = ( E x. B ) )
209	208	itgeq2dv	\|- ( ph -> S. ( X (,) Y ) ( [_ A / u ]_ C x. B ) _d x = S. ( X (,) Y ) ( E x. B ) _d x )
210	3	ditgpos	\|- ( ph -> S_ [ X -> Y ] ( [_ A / u ]_ C x. B ) _d x = S. ( X (,) Y ) ( [_ A / u ]_ C x. B ) _d x )
211	3	ditgpos	\|- ( ph -> S_ [ X -> Y ] ( E x. B ) _d x = S. ( X (,) Y ) ( E x. B ) _d x )
212	209 210 211	3eqtr4d	\|- ( ph -> S_ [ X -> Y ] ( [_ A / u ]_ C x. B ) _d x = S_ [ X -> Y ] ( E x. B ) _d x )
213	201 212	eqtr3id	\|- ( ph -> S_ [ X -> Y ] ( [_ [_ y / x ]_ A / u ]_ C x. [_ y / x ]_ B ) _d y = S_ [ X -> Y ] ( E x. B ) _d x )
214	213	adantr	\|- ( ( ph /\ ( ( m e. ( Z (,) W ) /\ n e. ( Z (,) W ) ) /\ A. x e. ( X [,] Y ) A e. ( m (,) n ) ) ) -> S_ [ X -> Y ] ( [_ [_ y / x ]_ A / u ]_ C x. [_ y / x ]_ B ) _d y = S_ [ X -> Y ] ( E x. B ) _d x )
215	181 193 214	3eqtr3d	\|- ( ( ph /\ ( ( m e. ( Z (,) W ) /\ n e. ( Z (,) W ) ) /\ A. x e. ( X [,] Y ) A e. ( m (,) n ) ) ) -> S_ [ K -> L ] C _d u = S_ [ X -> Y ] ( E x. B ) _d x )
216	215	expr	\|- ( ( ph /\ ( m e. ( Z (,) W ) /\ n e. ( Z (,) W ) ) ) -> ( A. x e. ( X [,] Y ) A e. ( m (,) n ) -> S_ [ K -> L ] C _d u = S_ [ X -> Y ] ( E x. B ) _d x ) )
217	144 216	sylbid	\|- ( ( ph /\ ( m e. ( Z (,) W ) /\ n e. ( Z (,) W ) ) ) -> ( A. z e. ( X [,] Y ) ( ( x e. ( X [,] Y ) \|-> A ) ` z ) e. ( m (,) n ) -> S_ [ K -> L ] C _d u = S_ [ X -> Y ] ( E x. B ) _d x ) )
218	129 217	sylbid	\|- ( ( ph /\ ( m e. ( Z (,) W ) /\ n e. ( Z (,) W ) ) ) -> ( A. z e. ( X [,] Y ) ( m < ( ( x e. ( X [,] Y ) \|-> A ) ` z ) /\ ( ( x e. ( X [,] Y ) \|-> A ) ` z ) < n ) -> S_ [ K -> L ] C _d u = S_ [ X -> Y ] ( E x. B ) _d x ) )
219	117 218	biimtrrid	\|- ( ( ph /\ ( m e. ( Z (,) W ) /\ n e. ( Z (,) W ) ) ) -> ( ( A. z e. ( X [,] Y ) m < ( ( x e. ( X [,] Y ) \|-> A ) ` z ) /\ A. z e. ( X [,] Y ) ( ( x e. ( X [,] Y ) \|-> A ) ` z ) < n ) -> S_ [ K -> L ] C _d u = S_ [ X -> Y ] ( E x. B ) _d x ) )
220	219	rexlimdvva	\|- ( ph -> ( E. m e. ( Z (,) W ) E. n e. ( Z (,) W ) ( A. z e. ( X [,] Y ) m < ( ( x e. ( X [,] Y ) \|-> A ) ` z ) /\ A. z e. ( X [,] Y ) ( ( x e. ( X [,] Y ) \|-> A ) ` z ) < n ) -> S_ [ K -> L ] C _d u = S_ [ X -> Y ] ( E x. B ) _d x ) )
221	116 220	biimtrid	\|- ( ph -> ( ( E. n e. ( Z (,) W ) A. z e. ( X [,] Y ) ( ( x e. ( X [,] Y ) \|-> A ) ` z ) < n /\ E. m e. ( Z (,) W ) A. z e. ( X [,] Y ) m < ( ( x e. ( X [,] Y ) \|-> A ) ` z ) ) -> S_ [ K -> L ] C _d u = S_ [ X -> Y ] ( E x. B ) _d x ) )
222	68 113 221	syl2and	\|- ( ph -> ( ( E. y e. ( X [,] Y ) A. z e. ( X [,] Y ) ( ( x e. ( X [,] Y ) \|-> A ) ` z ) <_ ( ( x e. ( X [,] Y ) \|-> A ) ` y ) /\ E. y e. ( X [,] Y ) A. z e. ( X [,] Y ) ( ( x e. ( X [,] Y ) \|-> A ) ` y ) <_ ( ( x e. ( X [,] Y ) \|-> A ) ` z ) ) -> S_ [ K -> L ] C _d u = S_ [ X -> Y ] ( E x. B ) _d x ) )
223	18 222	mpd	\|- ( ph -> S_ [ K -> L ] C _d u = S_ [ X -> Y ] ( E x. B ) _d x )

Metamath Proof Explorer

Theorem itgsubst

Proof