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
|
sseldi |
|- ( 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
|
ffvelrnd |
|- ( ( 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
|
sseldi |
|- ( ( 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
|
ffvelrnda |
|- ( ( ( ( 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
|
sseldi |
|- ( ( ( ( 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
|
ffvelrnd |
|- ( ( ( 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
|
sseldi |
|- ( ( ( 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
|
ffvelrnd |
|- ( ( 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
|
sseldi |
|- ( ( 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
|
ffvelrnd |
|- ( ( ( 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
|
sseldi |
|- ( ( ( 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
|
ffvelrnda |
|- ( ( ( ( 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
|
sseldi |
|- ( ( ( ( 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
|
ffvelrnda |
|- ( ( ( 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
|
sseldi |
|- ( ( ( 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
|
sseldi |
|- ( ( ( 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
|
sseldi |
|- ( ( ( 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
|
fvmptelrn |
|- ( ( 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
|
syl5bb |
|- ( 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
|
syl5eqr |
|- ( 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
|
syl5eqr |
|- ( 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
|
syl5bir |
|- ( ( 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
|
syl5bi |
|- ( 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 ) |