MPE Home Metamath Proof Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >  itgsubst Structured version   Visualization version   GIF version

Theorem itgsubst 25429
Description: Integration by ๐‘ข-substitution. If ๐ด(๐‘ฅ) is a continuous, differentiable function from [๐‘‹, ๐‘Œ] to (๐‘, ๐‘Š), whose derivative is continuous and integrable, and ๐ถ(๐‘ข) is a continuous function on (๐‘, ๐‘Š), then the integral of ๐ถ(๐‘ข) from ๐พ = ๐ด(๐‘‹) to ๐ฟ = ๐ด(๐‘Œ) is equal to the integral of ๐ถ(๐ด(๐‘ฅ)) D ๐ด(๐‘ฅ) from ๐‘‹ to ๐‘Œ. In this part of the proof we discharge the assumptions in itgsubstlem 25428, which use the fact that (๐‘, ๐‘Š) is open to shrink the interval a little to (๐‘€, ๐‘) where ๐‘ < ๐‘€ < ๐‘ < ๐‘Š- this is possible because ๐ด(๐‘ฅ) 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.)
Hypotheses
Ref Expression
itgsubst.x (๐œ‘ โ†’ ๐‘‹ โˆˆ โ„)
itgsubst.y (๐œ‘ โ†’ ๐‘Œ โˆˆ โ„)
itgsubst.le (๐œ‘ โ†’ ๐‘‹ โ‰ค ๐‘Œ)
itgsubst.z (๐œ‘ โ†’ ๐‘ โˆˆ โ„*)
itgsubst.w (๐œ‘ โ†’ ๐‘Š โˆˆ โ„*)
itgsubst.a (๐œ‘ โ†’ (๐‘ฅ โˆˆ (๐‘‹[,]๐‘Œ) โ†ฆ ๐ด) โˆˆ ((๐‘‹[,]๐‘Œ)โ€“cnโ†’(๐‘(,)๐‘Š)))
itgsubst.b (๐œ‘ โ†’ (๐‘ฅ โˆˆ (๐‘‹(,)๐‘Œ) โ†ฆ ๐ต) โˆˆ (((๐‘‹(,)๐‘Œ)โ€“cnโ†’โ„‚) โˆฉ ๐ฟ1))
itgsubst.c (๐œ‘ โ†’ (๐‘ข โˆˆ (๐‘(,)๐‘Š) โ†ฆ ๐ถ) โˆˆ ((๐‘(,)๐‘Š)โ€“cnโ†’โ„‚))
itgsubst.da (๐œ‘ โ†’ (โ„ D (๐‘ฅ โˆˆ (๐‘‹[,]๐‘Œ) โ†ฆ ๐ด)) = (๐‘ฅ โˆˆ (๐‘‹(,)๐‘Œ) โ†ฆ ๐ต))
itgsubst.e (๐‘ข = ๐ด โ†’ ๐ถ = ๐ธ)
itgsubst.k (๐‘ฅ = ๐‘‹ โ†’ ๐ด = ๐พ)
itgsubst.l (๐‘ฅ = ๐‘Œ โ†’ ๐ด = ๐ฟ)
Assertion
Ref Expression
itgsubst (๐œ‘ โ†’ โจœ[๐พ โ†’ ๐ฟ]๐ถ d๐‘ข = โจœ[๐‘‹ โ†’ ๐‘Œ](๐ธ ยท ๐ต) d๐‘ฅ)
Distinct variable groups:   ๐‘ข,๐ธ   ๐‘ฅ,๐‘ข,๐พ   ๐œ‘,๐‘ข,๐‘ฅ   ๐‘ข,๐‘‹,๐‘ฅ   ๐‘ข,๐‘Œ,๐‘ฅ   ๐‘ข,๐ด   ๐‘ฅ,๐ถ   ๐‘ข,๐‘Š,๐‘ฅ   ๐‘ข,๐ฟ,๐‘ฅ   ๐‘ข,๐‘,๐‘ฅ
Allowed substitution hints:   ๐ด(๐‘ฅ)   ๐ต(๐‘ฅ,๐‘ข)   ๐ถ(๐‘ข)   ๐ธ(๐‘ฅ)

Proof of Theorem itgsubst
Dummy variables ๐‘š ๐‘› ๐‘ฆ ๐‘ง ๐‘ฃ are mutually distinct and distinct from all other variables.
StepHypRef Expression
1 itgsubst.x . . 3 (๐œ‘ โ†’ ๐‘‹ โˆˆ โ„)
2 itgsubst.y . . 3 (๐œ‘ โ†’ ๐‘Œ โˆˆ โ„)
3 itgsubst.le . . 3 (๐œ‘ โ†’ ๐‘‹ โ‰ค ๐‘Œ)
4 ioossre 13331 . . . . 5 (๐‘(,)๐‘Š) โŠ† โ„
5 ax-resscn 11113 . . . . 5 โ„ โŠ† โ„‚
6 cncfss 24278 . . . . 5 (((๐‘(,)๐‘Š) โŠ† โ„ โˆง โ„ โŠ† โ„‚) โ†’ ((๐‘‹[,]๐‘Œ)โ€“cnโ†’(๐‘(,)๐‘Š)) โŠ† ((๐‘‹[,]๐‘Œ)โ€“cnโ†’โ„))
74, 5, 6mp2an 691 . . . 4 ((๐‘‹[,]๐‘Œ)โ€“cnโ†’(๐‘(,)๐‘Š)) โŠ† ((๐‘‹[,]๐‘Œ)โ€“cnโ†’โ„)
8 itgsubst.a . . . 4 (๐œ‘ โ†’ (๐‘ฅ โˆˆ (๐‘‹[,]๐‘Œ) โ†ฆ ๐ด) โˆˆ ((๐‘‹[,]๐‘Œ)โ€“cnโ†’(๐‘(,)๐‘Š)))
97, 8sselid 3943 . . 3 (๐œ‘ โ†’ (๐‘ฅ โˆˆ (๐‘‹[,]๐‘Œ) โ†ฆ ๐ด) โˆˆ ((๐‘‹[,]๐‘Œ)โ€“cnโ†’โ„))
101, 2, 3, 9evthicc 24839 . 2 (๐œ‘ โ†’ (โˆƒ๐‘ฆ โˆˆ (๐‘‹[,]๐‘Œ)โˆ€๐‘ง โˆˆ (๐‘‹[,]๐‘Œ)((๐‘ฅ โˆˆ (๐‘‹[,]๐‘Œ) โ†ฆ ๐ด)โ€˜๐‘ง) โ‰ค ((๐‘ฅ โˆˆ (๐‘‹[,]๐‘Œ) โ†ฆ ๐ด)โ€˜๐‘ฆ) โˆง โˆƒ๐‘ฆ โˆˆ (๐‘‹[,]๐‘Œ)โˆ€๐‘ง โˆˆ (๐‘‹[,]๐‘Œ)((๐‘ฅ โˆˆ (๐‘‹[,]๐‘Œ) โ†ฆ ๐ด)โ€˜๐‘ฆ) โ‰ค ((๐‘ฅ โˆˆ (๐‘‹[,]๐‘Œ) โ†ฆ ๐ด)โ€˜๐‘ง)))
11 ressxr 11204 . . . . . . . 8 โ„ โŠ† โ„*
124, 11sstri 3954 . . . . . . 7 (๐‘(,)๐‘Š) โŠ† โ„*
13 cncff 24272 . . . . . . . . . 10 ((๐‘ฅ โˆˆ (๐‘‹[,]๐‘Œ) โ†ฆ ๐ด) โˆˆ ((๐‘‹[,]๐‘Œ)โ€“cnโ†’(๐‘(,)๐‘Š)) โ†’ (๐‘ฅ โˆˆ (๐‘‹[,]๐‘Œ) โ†ฆ ๐ด):(๐‘‹[,]๐‘Œ)โŸถ(๐‘(,)๐‘Š))
148, 13syl 17 . . . . . . . . 9 (๐œ‘ โ†’ (๐‘ฅ โˆˆ (๐‘‹[,]๐‘Œ) โ†ฆ ๐ด):(๐‘‹[,]๐‘Œ)โŸถ(๐‘(,)๐‘Š))
1514adantr 482 . . . . . . . 8 ((๐œ‘ โˆง (๐‘ฆ โˆˆ (๐‘‹[,]๐‘Œ) โˆง โˆ€๐‘ง โˆˆ (๐‘‹[,]๐‘Œ)((๐‘ฅ โˆˆ (๐‘‹[,]๐‘Œ) โ†ฆ ๐ด)โ€˜๐‘ง) โ‰ค ((๐‘ฅ โˆˆ (๐‘‹[,]๐‘Œ) โ†ฆ ๐ด)โ€˜๐‘ฆ))) โ†’ (๐‘ฅ โˆˆ (๐‘‹[,]๐‘Œ) โ†ฆ ๐ด):(๐‘‹[,]๐‘Œ)โŸถ(๐‘(,)๐‘Š))
16 simprl 770 . . . . . . . 8 ((๐œ‘ โˆง (๐‘ฆ โˆˆ (๐‘‹[,]๐‘Œ) โˆง โˆ€๐‘ง โˆˆ (๐‘‹[,]๐‘Œ)((๐‘ฅ โˆˆ (๐‘‹[,]๐‘Œ) โ†ฆ ๐ด)โ€˜๐‘ง) โ‰ค ((๐‘ฅ โˆˆ (๐‘‹[,]๐‘Œ) โ†ฆ ๐ด)โ€˜๐‘ฆ))) โ†’ ๐‘ฆ โˆˆ (๐‘‹[,]๐‘Œ))
1715, 16ffvelcdmd 7037 . . . . . . 7 ((๐œ‘ โˆง (๐‘ฆ โˆˆ (๐‘‹[,]๐‘Œ) โˆง โˆ€๐‘ง โˆˆ (๐‘‹[,]๐‘Œ)((๐‘ฅ โˆˆ (๐‘‹[,]๐‘Œ) โ†ฆ ๐ด)โ€˜๐‘ง) โ‰ค ((๐‘ฅ โˆˆ (๐‘‹[,]๐‘Œ) โ†ฆ ๐ด)โ€˜๐‘ฆ))) โ†’ ((๐‘ฅ โˆˆ (๐‘‹[,]๐‘Œ) โ†ฆ ๐ด)โ€˜๐‘ฆ) โˆˆ (๐‘(,)๐‘Š))
1812, 17sselid 3943 . . . . . 6 ((๐œ‘ โˆง (๐‘ฆ โˆˆ (๐‘‹[,]๐‘Œ) โˆง โˆ€๐‘ง โˆˆ (๐‘‹[,]๐‘Œ)((๐‘ฅ โˆˆ (๐‘‹[,]๐‘Œ) โ†ฆ ๐ด)โ€˜๐‘ง) โ‰ค ((๐‘ฅ โˆˆ (๐‘‹[,]๐‘Œ) โ†ฆ ๐ด)โ€˜๐‘ฆ))) โ†’ ((๐‘ฅ โˆˆ (๐‘‹[,]๐‘Œ) โ†ฆ ๐ด)โ€˜๐‘ฆ) โˆˆ โ„*)
19 itgsubst.w . . . . . . 7 (๐œ‘ โ†’ ๐‘Š โˆˆ โ„*)
2019adantr 482 . . . . . 6 ((๐œ‘ โˆง (๐‘ฆ โˆˆ (๐‘‹[,]๐‘Œ) โˆง โˆ€๐‘ง โˆˆ (๐‘‹[,]๐‘Œ)((๐‘ฅ โˆˆ (๐‘‹[,]๐‘Œ) โ†ฆ ๐ด)โ€˜๐‘ง) โ‰ค ((๐‘ฅ โˆˆ (๐‘‹[,]๐‘Œ) โ†ฆ ๐ด)โ€˜๐‘ฆ))) โ†’ ๐‘Š โˆˆ โ„*)
21 eliooord 13329 . . . . . . . 8 (((๐‘ฅ โˆˆ (๐‘‹[,]๐‘Œ) โ†ฆ ๐ด)โ€˜๐‘ฆ) โˆˆ (๐‘(,)๐‘Š) โ†’ (๐‘ < ((๐‘ฅ โˆˆ (๐‘‹[,]๐‘Œ) โ†ฆ ๐ด)โ€˜๐‘ฆ) โˆง ((๐‘ฅ โˆˆ (๐‘‹[,]๐‘Œ) โ†ฆ ๐ด)โ€˜๐‘ฆ) < ๐‘Š))
2217, 21syl 17 . . . . . . 7 ((๐œ‘ โˆง (๐‘ฆ โˆˆ (๐‘‹[,]๐‘Œ) โˆง โˆ€๐‘ง โˆˆ (๐‘‹[,]๐‘Œ)((๐‘ฅ โˆˆ (๐‘‹[,]๐‘Œ) โ†ฆ ๐ด)โ€˜๐‘ง) โ‰ค ((๐‘ฅ โˆˆ (๐‘‹[,]๐‘Œ) โ†ฆ ๐ด)โ€˜๐‘ฆ))) โ†’ (๐‘ < ((๐‘ฅ โˆˆ (๐‘‹[,]๐‘Œ) โ†ฆ ๐ด)โ€˜๐‘ฆ) โˆง ((๐‘ฅ โˆˆ (๐‘‹[,]๐‘Œ) โ†ฆ ๐ด)โ€˜๐‘ฆ) < ๐‘Š))
2322simprd 497 . . . . . 6 ((๐œ‘ โˆง (๐‘ฆ โˆˆ (๐‘‹[,]๐‘Œ) โˆง โˆ€๐‘ง โˆˆ (๐‘‹[,]๐‘Œ)((๐‘ฅ โˆˆ (๐‘‹[,]๐‘Œ) โ†ฆ ๐ด)โ€˜๐‘ง) โ‰ค ((๐‘ฅ โˆˆ (๐‘‹[,]๐‘Œ) โ†ฆ ๐ด)โ€˜๐‘ฆ))) โ†’ ((๐‘ฅ โˆˆ (๐‘‹[,]๐‘Œ) โ†ฆ ๐ด)โ€˜๐‘ฆ) < ๐‘Š)
24 qbtwnxr 13125 . . . . . 6 ((((๐‘ฅ โˆˆ (๐‘‹[,]๐‘Œ) โ†ฆ ๐ด)โ€˜๐‘ฆ) โˆˆ โ„* โˆง ๐‘Š โˆˆ โ„* โˆง ((๐‘ฅ โˆˆ (๐‘‹[,]๐‘Œ) โ†ฆ ๐ด)โ€˜๐‘ฆ) < ๐‘Š) โ†’ โˆƒ๐‘› โˆˆ โ„š (((๐‘ฅ โˆˆ (๐‘‹[,]๐‘Œ) โ†ฆ ๐ด)โ€˜๐‘ฆ) < ๐‘› โˆง ๐‘› < ๐‘Š))
2518, 20, 23, 24syl3anc 1372 . . . . 5 ((๐œ‘ โˆง (๐‘ฆ โˆˆ (๐‘‹[,]๐‘Œ) โˆง โˆ€๐‘ง โˆˆ (๐‘‹[,]๐‘Œ)((๐‘ฅ โˆˆ (๐‘‹[,]๐‘Œ) โ†ฆ ๐ด)โ€˜๐‘ง) โ‰ค ((๐‘ฅ โˆˆ (๐‘‹[,]๐‘Œ) โ†ฆ ๐ด)โ€˜๐‘ฆ))) โ†’ โˆƒ๐‘› โˆˆ โ„š (((๐‘ฅ โˆˆ (๐‘‹[,]๐‘Œ) โ†ฆ ๐ด)โ€˜๐‘ฆ) < ๐‘› โˆง ๐‘› < ๐‘Š))
26 qre 12883 . . . . . . 7 (๐‘› โˆˆ โ„š โ†’ ๐‘› โˆˆ โ„)
2726ad2antrl 727 . . . . . 6 (((๐œ‘ โˆง (๐‘ฆ โˆˆ (๐‘‹[,]๐‘Œ) โˆง โˆ€๐‘ง โˆˆ (๐‘‹[,]๐‘Œ)((๐‘ฅ โˆˆ (๐‘‹[,]๐‘Œ) โ†ฆ ๐ด)โ€˜๐‘ง) โ‰ค ((๐‘ฅ โˆˆ (๐‘‹[,]๐‘Œ) โ†ฆ ๐ด)โ€˜๐‘ฆ))) โˆง (๐‘› โˆˆ โ„š โˆง (((๐‘ฅ โˆˆ (๐‘‹[,]๐‘Œ) โ†ฆ ๐ด)โ€˜๐‘ฆ) < ๐‘› โˆง ๐‘› < ๐‘Š))) โ†’ ๐‘› โˆˆ โ„)
28 itgsubst.z . . . . . . . 8 (๐œ‘ โ†’ ๐‘ โˆˆ โ„*)
2928ad2antrr 725 . . . . . . 7 (((๐œ‘ โˆง (๐‘ฆ โˆˆ (๐‘‹[,]๐‘Œ) โˆง โˆ€๐‘ง โˆˆ (๐‘‹[,]๐‘Œ)((๐‘ฅ โˆˆ (๐‘‹[,]๐‘Œ) โ†ฆ ๐ด)โ€˜๐‘ง) โ‰ค ((๐‘ฅ โˆˆ (๐‘‹[,]๐‘Œ) โ†ฆ ๐ด)โ€˜๐‘ฆ))) โˆง (๐‘› โˆˆ โ„š โˆง (((๐‘ฅ โˆˆ (๐‘‹[,]๐‘Œ) โ†ฆ ๐ด)โ€˜๐‘ฆ) < ๐‘› โˆง ๐‘› < ๐‘Š))) โ†’ ๐‘ โˆˆ โ„*)
3018adantr 482 . . . . . . 7 (((๐œ‘ โˆง (๐‘ฆ โˆˆ (๐‘‹[,]๐‘Œ) โˆง โˆ€๐‘ง โˆˆ (๐‘‹[,]๐‘Œ)((๐‘ฅ โˆˆ (๐‘‹[,]๐‘Œ) โ†ฆ ๐ด)โ€˜๐‘ง) โ‰ค ((๐‘ฅ โˆˆ (๐‘‹[,]๐‘Œ) โ†ฆ ๐ด)โ€˜๐‘ฆ))) โˆง (๐‘› โˆˆ โ„š โˆง (((๐‘ฅ โˆˆ (๐‘‹[,]๐‘Œ) โ†ฆ ๐ด)โ€˜๐‘ฆ) < ๐‘› โˆง ๐‘› < ๐‘Š))) โ†’ ((๐‘ฅ โˆˆ (๐‘‹[,]๐‘Œ) โ†ฆ ๐ด)โ€˜๐‘ฆ) โˆˆ โ„*)
3127rexrd 11210 . . . . . . 7 (((๐œ‘ โˆง (๐‘ฆ โˆˆ (๐‘‹[,]๐‘Œ) โˆง โˆ€๐‘ง โˆˆ (๐‘‹[,]๐‘Œ)((๐‘ฅ โˆˆ (๐‘‹[,]๐‘Œ) โ†ฆ ๐ด)โ€˜๐‘ง) โ‰ค ((๐‘ฅ โˆˆ (๐‘‹[,]๐‘Œ) โ†ฆ ๐ด)โ€˜๐‘ฆ))) โˆง (๐‘› โˆˆ โ„š โˆง (((๐‘ฅ โˆˆ (๐‘‹[,]๐‘Œ) โ†ฆ ๐ด)โ€˜๐‘ฆ) < ๐‘› โˆง ๐‘› < ๐‘Š))) โ†’ ๐‘› โˆˆ โ„*)
3222simpld 496 . . . . . . . 8 ((๐œ‘ โˆง (๐‘ฆ โˆˆ (๐‘‹[,]๐‘Œ) โˆง โˆ€๐‘ง โˆˆ (๐‘‹[,]๐‘Œ)((๐‘ฅ โˆˆ (๐‘‹[,]๐‘Œ) โ†ฆ ๐ด)โ€˜๐‘ง) โ‰ค ((๐‘ฅ โˆˆ (๐‘‹[,]๐‘Œ) โ†ฆ ๐ด)โ€˜๐‘ฆ))) โ†’ ๐‘ < ((๐‘ฅ โˆˆ (๐‘‹[,]๐‘Œ) โ†ฆ ๐ด)โ€˜๐‘ฆ))
3332adantr 482 . . . . . . 7 (((๐œ‘ โˆง (๐‘ฆ โˆˆ (๐‘‹[,]๐‘Œ) โˆง โˆ€๐‘ง โˆˆ (๐‘‹[,]๐‘Œ)((๐‘ฅ โˆˆ (๐‘‹[,]๐‘Œ) โ†ฆ ๐ด)โ€˜๐‘ง) โ‰ค ((๐‘ฅ โˆˆ (๐‘‹[,]๐‘Œ) โ†ฆ ๐ด)โ€˜๐‘ฆ))) โˆง (๐‘› โˆˆ โ„š โˆง (((๐‘ฅ โˆˆ (๐‘‹[,]๐‘Œ) โ†ฆ ๐ด)โ€˜๐‘ฆ) < ๐‘› โˆง ๐‘› < ๐‘Š))) โ†’ ๐‘ < ((๐‘ฅ โˆˆ (๐‘‹[,]๐‘Œ) โ†ฆ ๐ด)โ€˜๐‘ฆ))
34 simprrl 780 . . . . . . 7 (((๐œ‘ โˆง (๐‘ฆ โˆˆ (๐‘‹[,]๐‘Œ) โˆง โˆ€๐‘ง โˆˆ (๐‘‹[,]๐‘Œ)((๐‘ฅ โˆˆ (๐‘‹[,]๐‘Œ) โ†ฆ ๐ด)โ€˜๐‘ง) โ‰ค ((๐‘ฅ โˆˆ (๐‘‹[,]๐‘Œ) โ†ฆ ๐ด)โ€˜๐‘ฆ))) โˆง (๐‘› โˆˆ โ„š โˆง (((๐‘ฅ โˆˆ (๐‘‹[,]๐‘Œ) โ†ฆ ๐ด)โ€˜๐‘ฆ) < ๐‘› โˆง ๐‘› < ๐‘Š))) โ†’ ((๐‘ฅ โˆˆ (๐‘‹[,]๐‘Œ) โ†ฆ ๐ด)โ€˜๐‘ฆ) < ๐‘›)
3529, 30, 31, 33, 34xrlttrd 13084 . . . . . 6 (((๐œ‘ โˆง (๐‘ฆ โˆˆ (๐‘‹[,]๐‘Œ) โˆง โˆ€๐‘ง โˆˆ (๐‘‹[,]๐‘Œ)((๐‘ฅ โˆˆ (๐‘‹[,]๐‘Œ) โ†ฆ ๐ด)โ€˜๐‘ง) โ‰ค ((๐‘ฅ โˆˆ (๐‘‹[,]๐‘Œ) โ†ฆ ๐ด)โ€˜๐‘ฆ))) โˆง (๐‘› โˆˆ โ„š โˆง (((๐‘ฅ โˆˆ (๐‘‹[,]๐‘Œ) โ†ฆ ๐ด)โ€˜๐‘ฆ) < ๐‘› โˆง ๐‘› < ๐‘Š))) โ†’ ๐‘ < ๐‘›)
36 simprrr 781 . . . . . 6 (((๐œ‘ โˆง (๐‘ฆ โˆˆ (๐‘‹[,]๐‘Œ) โˆง โˆ€๐‘ง โˆˆ (๐‘‹[,]๐‘Œ)((๐‘ฅ โˆˆ (๐‘‹[,]๐‘Œ) โ†ฆ ๐ด)โ€˜๐‘ง) โ‰ค ((๐‘ฅ โˆˆ (๐‘‹[,]๐‘Œ) โ†ฆ ๐ด)โ€˜๐‘ฆ))) โˆง (๐‘› โˆˆ โ„š โˆง (((๐‘ฅ โˆˆ (๐‘‹[,]๐‘Œ) โ†ฆ ๐ด)โ€˜๐‘ฆ) < ๐‘› โˆง ๐‘› < ๐‘Š))) โ†’ ๐‘› < ๐‘Š)
3719ad2antrr 725 . . . . . . 7 (((๐œ‘ โˆง (๐‘ฆ โˆˆ (๐‘‹[,]๐‘Œ) โˆง โˆ€๐‘ง โˆˆ (๐‘‹[,]๐‘Œ)((๐‘ฅ โˆˆ (๐‘‹[,]๐‘Œ) โ†ฆ ๐ด)โ€˜๐‘ง) โ‰ค ((๐‘ฅ โˆˆ (๐‘‹[,]๐‘Œ) โ†ฆ ๐ด)โ€˜๐‘ฆ))) โˆง (๐‘› โˆˆ โ„š โˆง (((๐‘ฅ โˆˆ (๐‘‹[,]๐‘Œ) โ†ฆ ๐ด)โ€˜๐‘ฆ) < ๐‘› โˆง ๐‘› < ๐‘Š))) โ†’ ๐‘Š โˆˆ โ„*)
38 elioo2 13311 . . . . . . 7 ((๐‘ โˆˆ โ„* โˆง ๐‘Š โˆˆ โ„*) โ†’ (๐‘› โˆˆ (๐‘(,)๐‘Š) โ†” (๐‘› โˆˆ โ„ โˆง ๐‘ < ๐‘› โˆง ๐‘› < ๐‘Š)))
3929, 37, 38syl2anc 585 . . . . . 6 (((๐œ‘ โˆง (๐‘ฆ โˆˆ (๐‘‹[,]๐‘Œ) โˆง โˆ€๐‘ง โˆˆ (๐‘‹[,]๐‘Œ)((๐‘ฅ โˆˆ (๐‘‹[,]๐‘Œ) โ†ฆ ๐ด)โ€˜๐‘ง) โ‰ค ((๐‘ฅ โˆˆ (๐‘‹[,]๐‘Œ) โ†ฆ ๐ด)โ€˜๐‘ฆ))) โˆง (๐‘› โˆˆ โ„š โˆง (((๐‘ฅ โˆˆ (๐‘‹[,]๐‘Œ) โ†ฆ ๐ด)โ€˜๐‘ฆ) < ๐‘› โˆง ๐‘› < ๐‘Š))) โ†’ (๐‘› โˆˆ (๐‘(,)๐‘Š) โ†” (๐‘› โˆˆ โ„ โˆง ๐‘ < ๐‘› โˆง ๐‘› < ๐‘Š)))
4027, 35, 36, 39mpbir3and 1343 . . . . 5 (((๐œ‘ โˆง (๐‘ฆ โˆˆ (๐‘‹[,]๐‘Œ) โˆง โˆ€๐‘ง โˆˆ (๐‘‹[,]๐‘Œ)((๐‘ฅ โˆˆ (๐‘‹[,]๐‘Œ) โ†ฆ ๐ด)โ€˜๐‘ง) โ‰ค ((๐‘ฅ โˆˆ (๐‘‹[,]๐‘Œ) โ†ฆ ๐ด)โ€˜๐‘ฆ))) โˆง (๐‘› โˆˆ โ„š โˆง (((๐‘ฅ โˆˆ (๐‘‹[,]๐‘Œ) โ†ฆ ๐ด)โ€˜๐‘ฆ) < ๐‘› โˆง ๐‘› < ๐‘Š))) โ†’ ๐‘› โˆˆ (๐‘(,)๐‘Š))
41 anass 470 . . . . . 6 (((๐œ‘ โˆง ๐‘ฆ โˆˆ (๐‘‹[,]๐‘Œ)) โˆง โˆ€๐‘ง โˆˆ (๐‘‹[,]๐‘Œ)((๐‘ฅ โˆˆ (๐‘‹[,]๐‘Œ) โ†ฆ ๐ด)โ€˜๐‘ง) โ‰ค ((๐‘ฅ โˆˆ (๐‘‹[,]๐‘Œ) โ†ฆ ๐ด)โ€˜๐‘ฆ)) โ†” (๐œ‘ โˆง (๐‘ฆ โˆˆ (๐‘‹[,]๐‘Œ) โˆง โˆ€๐‘ง โˆˆ (๐‘‹[,]๐‘Œ)((๐‘ฅ โˆˆ (๐‘‹[,]๐‘Œ) โ†ฆ ๐ด)โ€˜๐‘ง) โ‰ค ((๐‘ฅ โˆˆ (๐‘‹[,]๐‘Œ) โ†ฆ ๐ด)โ€˜๐‘ฆ))))
42 simprrl 780 . . . . . . . . . . 11 (((๐œ‘ โˆง ๐‘ฆ โˆˆ (๐‘‹[,]๐‘Œ)) โˆง (๐‘› โˆˆ โ„š โˆง (((๐‘ฅ โˆˆ (๐‘‹[,]๐‘Œ) โ†ฆ ๐ด)โ€˜๐‘ฆ) < ๐‘› โˆง ๐‘› < ๐‘Š))) โ†’ ((๐‘ฅ โˆˆ (๐‘‹[,]๐‘Œ) โ†ฆ ๐ด)โ€˜๐‘ฆ) < ๐‘›)
4342adantr 482 . . . . . . . . . 10 ((((๐œ‘ โˆง ๐‘ฆ โˆˆ (๐‘‹[,]๐‘Œ)) โˆง (๐‘› โˆˆ โ„š โˆง (((๐‘ฅ โˆˆ (๐‘‹[,]๐‘Œ) โ†ฆ ๐ด)โ€˜๐‘ฆ) < ๐‘› โˆง ๐‘› < ๐‘Š))) โˆง ๐‘ง โˆˆ (๐‘‹[,]๐‘Œ)) โ†’ ((๐‘ฅ โˆˆ (๐‘‹[,]๐‘Œ) โ†ฆ ๐ด)โ€˜๐‘ฆ) < ๐‘›)
4414ad2antrr 725 . . . . . . . . . . . . 13 (((๐œ‘ โˆง ๐‘ฆ โˆˆ (๐‘‹[,]๐‘Œ)) โˆง (๐‘› โˆˆ โ„š โˆง (((๐‘ฅ โˆˆ (๐‘‹[,]๐‘Œ) โ†ฆ ๐ด)โ€˜๐‘ฆ) < ๐‘› โˆง ๐‘› < ๐‘Š))) โ†’ (๐‘ฅ โˆˆ (๐‘‹[,]๐‘Œ) โ†ฆ ๐ด):(๐‘‹[,]๐‘Œ)โŸถ(๐‘(,)๐‘Š))
4544ffvelcdmda 7036 . . . . . . . . . . . 12 ((((๐œ‘ โˆง ๐‘ฆ โˆˆ (๐‘‹[,]๐‘Œ)) โˆง (๐‘› โˆˆ โ„š โˆง (((๐‘ฅ โˆˆ (๐‘‹[,]๐‘Œ) โ†ฆ ๐ด)โ€˜๐‘ฆ) < ๐‘› โˆง ๐‘› < ๐‘Š))) โˆง ๐‘ง โˆˆ (๐‘‹[,]๐‘Œ)) โ†’ ((๐‘ฅ โˆˆ (๐‘‹[,]๐‘Œ) โ†ฆ ๐ด)โ€˜๐‘ง) โˆˆ (๐‘(,)๐‘Š))
4612, 45sselid 3943 . . . . . . . . . . 11 ((((๐œ‘ โˆง ๐‘ฆ โˆˆ (๐‘‹[,]๐‘Œ)) โˆง (๐‘› โˆˆ โ„š โˆง (((๐‘ฅ โˆˆ (๐‘‹[,]๐‘Œ) โ†ฆ ๐ด)โ€˜๐‘ฆ) < ๐‘› โˆง ๐‘› < ๐‘Š))) โˆง ๐‘ง โˆˆ (๐‘‹[,]๐‘Œ)) โ†’ ((๐‘ฅ โˆˆ (๐‘‹[,]๐‘Œ) โ†ฆ ๐ด)โ€˜๐‘ง) โˆˆ โ„*)
47 simplr 768 . . . . . . . . . . . . . 14 (((๐œ‘ โˆง ๐‘ฆ โˆˆ (๐‘‹[,]๐‘Œ)) โˆง (๐‘› โˆˆ โ„š โˆง (((๐‘ฅ โˆˆ (๐‘‹[,]๐‘Œ) โ†ฆ ๐ด)โ€˜๐‘ฆ) < ๐‘› โˆง ๐‘› < ๐‘Š))) โ†’ ๐‘ฆ โˆˆ (๐‘‹[,]๐‘Œ))
4844, 47ffvelcdmd 7037 . . . . . . . . . . . . 13 (((๐œ‘ โˆง ๐‘ฆ โˆˆ (๐‘‹[,]๐‘Œ)) โˆง (๐‘› โˆˆ โ„š โˆง (((๐‘ฅ โˆˆ (๐‘‹[,]๐‘Œ) โ†ฆ ๐ด)โ€˜๐‘ฆ) < ๐‘› โˆง ๐‘› < ๐‘Š))) โ†’ ((๐‘ฅ โˆˆ (๐‘‹[,]๐‘Œ) โ†ฆ ๐ด)โ€˜๐‘ฆ) โˆˆ (๐‘(,)๐‘Š))
4912, 48sselid 3943 . . . . . . . . . . . 12 (((๐œ‘ โˆง ๐‘ฆ โˆˆ (๐‘‹[,]๐‘Œ)) โˆง (๐‘› โˆˆ โ„š โˆง (((๐‘ฅ โˆˆ (๐‘‹[,]๐‘Œ) โ†ฆ ๐ด)โ€˜๐‘ฆ) < ๐‘› โˆง ๐‘› < ๐‘Š))) โ†’ ((๐‘ฅ โˆˆ (๐‘‹[,]๐‘Œ) โ†ฆ ๐ด)โ€˜๐‘ฆ) โˆˆ โ„*)
5049adantr 482 . . . . . . . . . . 11 ((((๐œ‘ โˆง ๐‘ฆ โˆˆ (๐‘‹[,]๐‘Œ)) โˆง (๐‘› โˆˆ โ„š โˆง (((๐‘ฅ โˆˆ (๐‘‹[,]๐‘Œ) โ†ฆ ๐ด)โ€˜๐‘ฆ) < ๐‘› โˆง ๐‘› < ๐‘Š))) โˆง ๐‘ง โˆˆ (๐‘‹[,]๐‘Œ)) โ†’ ((๐‘ฅ โˆˆ (๐‘‹[,]๐‘Œ) โ†ฆ ๐ด)โ€˜๐‘ฆ) โˆˆ โ„*)
5126ad2antrl 727 . . . . . . . . . . . . 13 (((๐œ‘ โˆง ๐‘ฆ โˆˆ (๐‘‹[,]๐‘Œ)) โˆง (๐‘› โˆˆ โ„š โˆง (((๐‘ฅ โˆˆ (๐‘‹[,]๐‘Œ) โ†ฆ ๐ด)โ€˜๐‘ฆ) < ๐‘› โˆง ๐‘› < ๐‘Š))) โ†’ ๐‘› โˆˆ โ„)
5251adantr 482 . . . . . . . . . . . 12 ((((๐œ‘ โˆง ๐‘ฆ โˆˆ (๐‘‹[,]๐‘Œ)) โˆง (๐‘› โˆˆ โ„š โˆง (((๐‘ฅ โˆˆ (๐‘‹[,]๐‘Œ) โ†ฆ ๐ด)โ€˜๐‘ฆ) < ๐‘› โˆง ๐‘› < ๐‘Š))) โˆง ๐‘ง โˆˆ (๐‘‹[,]๐‘Œ)) โ†’ ๐‘› โˆˆ โ„)
5352rexrd 11210 . . . . . . . . . . 11 ((((๐œ‘ โˆง ๐‘ฆ โˆˆ (๐‘‹[,]๐‘Œ)) โˆง (๐‘› โˆˆ โ„š โˆง (((๐‘ฅ โˆˆ (๐‘‹[,]๐‘Œ) โ†ฆ ๐ด)โ€˜๐‘ฆ) < ๐‘› โˆง ๐‘› < ๐‘Š))) โˆง ๐‘ง โˆˆ (๐‘‹[,]๐‘Œ)) โ†’ ๐‘› โˆˆ โ„*)
54 xrlelttr 13081 . . . . . . . . . . 11 ((((๐‘ฅ โˆˆ (๐‘‹[,]๐‘Œ) โ†ฆ ๐ด)โ€˜๐‘ง) โˆˆ โ„* โˆง ((๐‘ฅ โˆˆ (๐‘‹[,]๐‘Œ) โ†ฆ ๐ด)โ€˜๐‘ฆ) โˆˆ โ„* โˆง ๐‘› โˆˆ โ„*) โ†’ ((((๐‘ฅ โˆˆ (๐‘‹[,]๐‘Œ) โ†ฆ ๐ด)โ€˜๐‘ง) โ‰ค ((๐‘ฅ โˆˆ (๐‘‹[,]๐‘Œ) โ†ฆ ๐ด)โ€˜๐‘ฆ) โˆง ((๐‘ฅ โˆˆ (๐‘‹[,]๐‘Œ) โ†ฆ ๐ด)โ€˜๐‘ฆ) < ๐‘›) โ†’ ((๐‘ฅ โˆˆ (๐‘‹[,]๐‘Œ) โ†ฆ ๐ด)โ€˜๐‘ง) < ๐‘›))
5546, 50, 53, 54syl3anc 1372 . . . . . . . . . 10 ((((๐œ‘ โˆง ๐‘ฆ โˆˆ (๐‘‹[,]๐‘Œ)) โˆง (๐‘› โˆˆ โ„š โˆง (((๐‘ฅ โˆˆ (๐‘‹[,]๐‘Œ) โ†ฆ ๐ด)โ€˜๐‘ฆ) < ๐‘› โˆง ๐‘› < ๐‘Š))) โˆง ๐‘ง โˆˆ (๐‘‹[,]๐‘Œ)) โ†’ ((((๐‘ฅ โˆˆ (๐‘‹[,]๐‘Œ) โ†ฆ ๐ด)โ€˜๐‘ง) โ‰ค ((๐‘ฅ โˆˆ (๐‘‹[,]๐‘Œ) โ†ฆ ๐ด)โ€˜๐‘ฆ) โˆง ((๐‘ฅ โˆˆ (๐‘‹[,]๐‘Œ) โ†ฆ ๐ด)โ€˜๐‘ฆ) < ๐‘›) โ†’ ((๐‘ฅ โˆˆ (๐‘‹[,]๐‘Œ) โ†ฆ ๐ด)โ€˜๐‘ง) < ๐‘›))
5643, 55mpan2d 693 . . . . . . . . 9 ((((๐œ‘ โˆง ๐‘ฆ โˆˆ (๐‘‹[,]๐‘Œ)) โˆง (๐‘› โˆˆ โ„š โˆง (((๐‘ฅ โˆˆ (๐‘‹[,]๐‘Œ) โ†ฆ ๐ด)โ€˜๐‘ฆ) < ๐‘› โˆง ๐‘› < ๐‘Š))) โˆง ๐‘ง โˆˆ (๐‘‹[,]๐‘Œ)) โ†’ (((๐‘ฅ โˆˆ (๐‘‹[,]๐‘Œ) โ†ฆ ๐ด)โ€˜๐‘ง) โ‰ค ((๐‘ฅ โˆˆ (๐‘‹[,]๐‘Œ) โ†ฆ ๐ด)โ€˜๐‘ฆ) โ†’ ((๐‘ฅ โˆˆ (๐‘‹[,]๐‘Œ) โ†ฆ ๐ด)โ€˜๐‘ง) < ๐‘›))
5756ralimdva 3161 . . . . . . . 8 (((๐œ‘ โˆง ๐‘ฆ โˆˆ (๐‘‹[,]๐‘Œ)) โˆง (๐‘› โˆˆ โ„š โˆง (((๐‘ฅ โˆˆ (๐‘‹[,]๐‘Œ) โ†ฆ ๐ด)โ€˜๐‘ฆ) < ๐‘› โˆง ๐‘› < ๐‘Š))) โ†’ (โˆ€๐‘ง โˆˆ (๐‘‹[,]๐‘Œ)((๐‘ฅ โˆˆ (๐‘‹[,]๐‘Œ) โ†ฆ ๐ด)โ€˜๐‘ง) โ‰ค ((๐‘ฅ โˆˆ (๐‘‹[,]๐‘Œ) โ†ฆ ๐ด)โ€˜๐‘ฆ) โ†’ โˆ€๐‘ง โˆˆ (๐‘‹[,]๐‘Œ)((๐‘ฅ โˆˆ (๐‘‹[,]๐‘Œ) โ†ฆ ๐ด)โ€˜๐‘ง) < ๐‘›))
5857imp 408 . . . . . . 7 ((((๐œ‘ โˆง ๐‘ฆ โˆˆ (๐‘‹[,]๐‘Œ)) โˆง (๐‘› โˆˆ โ„š โˆง (((๐‘ฅ โˆˆ (๐‘‹[,]๐‘Œ) โ†ฆ ๐ด)โ€˜๐‘ฆ) < ๐‘› โˆง ๐‘› < ๐‘Š))) โˆง โˆ€๐‘ง โˆˆ (๐‘‹[,]๐‘Œ)((๐‘ฅ โˆˆ (๐‘‹[,]๐‘Œ) โ†ฆ ๐ด)โ€˜๐‘ง) โ‰ค ((๐‘ฅ โˆˆ (๐‘‹[,]๐‘Œ) โ†ฆ ๐ด)โ€˜๐‘ฆ)) โ†’ โˆ€๐‘ง โˆˆ (๐‘‹[,]๐‘Œ)((๐‘ฅ โˆˆ (๐‘‹[,]๐‘Œ) โ†ฆ ๐ด)โ€˜๐‘ง) < ๐‘›)
5958an32s 651 . . . . . 6 ((((๐œ‘ โˆง ๐‘ฆ โˆˆ (๐‘‹[,]๐‘Œ)) โˆง โˆ€๐‘ง โˆˆ (๐‘‹[,]๐‘Œ)((๐‘ฅ โˆˆ (๐‘‹[,]๐‘Œ) โ†ฆ ๐ด)โ€˜๐‘ง) โ‰ค ((๐‘ฅ โˆˆ (๐‘‹[,]๐‘Œ) โ†ฆ ๐ด)โ€˜๐‘ฆ)) โˆง (๐‘› โˆˆ โ„š โˆง (((๐‘ฅ โˆˆ (๐‘‹[,]๐‘Œ) โ†ฆ ๐ด)โ€˜๐‘ฆ) < ๐‘› โˆง ๐‘› < ๐‘Š))) โ†’ โˆ€๐‘ง โˆˆ (๐‘‹[,]๐‘Œ)((๐‘ฅ โˆˆ (๐‘‹[,]๐‘Œ) โ†ฆ ๐ด)โ€˜๐‘ง) < ๐‘›)
6041, 59sylanbr 583 . . . . 5 (((๐œ‘ โˆง (๐‘ฆ โˆˆ (๐‘‹[,]๐‘Œ) โˆง โˆ€๐‘ง โˆˆ (๐‘‹[,]๐‘Œ)((๐‘ฅ โˆˆ (๐‘‹[,]๐‘Œ) โ†ฆ ๐ด)โ€˜๐‘ง) โ‰ค ((๐‘ฅ โˆˆ (๐‘‹[,]๐‘Œ) โ†ฆ ๐ด)โ€˜๐‘ฆ))) โˆง (๐‘› โˆˆ โ„š โˆง (((๐‘ฅ โˆˆ (๐‘‹[,]๐‘Œ) โ†ฆ ๐ด)โ€˜๐‘ฆ) < ๐‘› โˆง ๐‘› < ๐‘Š))) โ†’ โˆ€๐‘ง โˆˆ (๐‘‹[,]๐‘Œ)((๐‘ฅ โˆˆ (๐‘‹[,]๐‘Œ) โ†ฆ ๐ด)โ€˜๐‘ง) < ๐‘›)
6125, 40, 60reximssdv 3166 . . . 4 ((๐œ‘ โˆง (๐‘ฆ โˆˆ (๐‘‹[,]๐‘Œ) โˆง โˆ€๐‘ง โˆˆ (๐‘‹[,]๐‘Œ)((๐‘ฅ โˆˆ (๐‘‹[,]๐‘Œ) โ†ฆ ๐ด)โ€˜๐‘ง) โ‰ค ((๐‘ฅ โˆˆ (๐‘‹[,]๐‘Œ) โ†ฆ ๐ด)โ€˜๐‘ฆ))) โ†’ โˆƒ๐‘› โˆˆ (๐‘(,)๐‘Š)โˆ€๐‘ง โˆˆ (๐‘‹[,]๐‘Œ)((๐‘ฅ โˆˆ (๐‘‹[,]๐‘Œ) โ†ฆ ๐ด)โ€˜๐‘ง) < ๐‘›)
6261rexlimdvaa 3150 . . 3 (๐œ‘ โ†’ (โˆƒ๐‘ฆ โˆˆ (๐‘‹[,]๐‘Œ)โˆ€๐‘ง โˆˆ (๐‘‹[,]๐‘Œ)((๐‘ฅ โˆˆ (๐‘‹[,]๐‘Œ) โ†ฆ ๐ด)โ€˜๐‘ง) โ‰ค ((๐‘ฅ โˆˆ (๐‘‹[,]๐‘Œ) โ†ฆ ๐ด)โ€˜๐‘ฆ) โ†’ โˆƒ๐‘› โˆˆ (๐‘(,)๐‘Š)โˆ€๐‘ง โˆˆ (๐‘‹[,]๐‘Œ)((๐‘ฅ โˆˆ (๐‘‹[,]๐‘Œ) โ†ฆ ๐ด)โ€˜๐‘ง) < ๐‘›))
6328adantr 482 . . . . . 6 ((๐œ‘ โˆง (๐‘ฆ โˆˆ (๐‘‹[,]๐‘Œ) โˆง โˆ€๐‘ง โˆˆ (๐‘‹[,]๐‘Œ)((๐‘ฅ โˆˆ (๐‘‹[,]๐‘Œ) โ†ฆ ๐ด)โ€˜๐‘ฆ) โ‰ค ((๐‘ฅ โˆˆ (๐‘‹[,]๐‘Œ) โ†ฆ ๐ด)โ€˜๐‘ง))) โ†’ ๐‘ โˆˆ โ„*)
6414adantr 482 . . . . . . . 8 ((๐œ‘ โˆง (๐‘ฆ โˆˆ (๐‘‹[,]๐‘Œ) โˆง โˆ€๐‘ง โˆˆ (๐‘‹[,]๐‘Œ)((๐‘ฅ โˆˆ (๐‘‹[,]๐‘Œ) โ†ฆ ๐ด)โ€˜๐‘ฆ) โ‰ค ((๐‘ฅ โˆˆ (๐‘‹[,]๐‘Œ) โ†ฆ ๐ด)โ€˜๐‘ง))) โ†’ (๐‘ฅ โˆˆ (๐‘‹[,]๐‘Œ) โ†ฆ ๐ด):(๐‘‹[,]๐‘Œ)โŸถ(๐‘(,)๐‘Š))
65 simprl 770 . . . . . . . 8 ((๐œ‘ โˆง (๐‘ฆ โˆˆ (๐‘‹[,]๐‘Œ) โˆง โˆ€๐‘ง โˆˆ (๐‘‹[,]๐‘Œ)((๐‘ฅ โˆˆ (๐‘‹[,]๐‘Œ) โ†ฆ ๐ด)โ€˜๐‘ฆ) โ‰ค ((๐‘ฅ โˆˆ (๐‘‹[,]๐‘Œ) โ†ฆ ๐ด)โ€˜๐‘ง))) โ†’ ๐‘ฆ โˆˆ (๐‘‹[,]๐‘Œ))
6664, 65ffvelcdmd 7037 . . . . . . 7 ((๐œ‘ โˆง (๐‘ฆ โˆˆ (๐‘‹[,]๐‘Œ) โˆง โˆ€๐‘ง โˆˆ (๐‘‹[,]๐‘Œ)((๐‘ฅ โˆˆ (๐‘‹[,]๐‘Œ) โ†ฆ ๐ด)โ€˜๐‘ฆ) โ‰ค ((๐‘ฅ โˆˆ (๐‘‹[,]๐‘Œ) โ†ฆ ๐ด)โ€˜๐‘ง))) โ†’ ((๐‘ฅ โˆˆ (๐‘‹[,]๐‘Œ) โ†ฆ ๐ด)โ€˜๐‘ฆ) โˆˆ (๐‘(,)๐‘Š))
6712, 66sselid 3943 . . . . . 6 ((๐œ‘ โˆง (๐‘ฆ โˆˆ (๐‘‹[,]๐‘Œ) โˆง โˆ€๐‘ง โˆˆ (๐‘‹[,]๐‘Œ)((๐‘ฅ โˆˆ (๐‘‹[,]๐‘Œ) โ†ฆ ๐ด)โ€˜๐‘ฆ) โ‰ค ((๐‘ฅ โˆˆ (๐‘‹[,]๐‘Œ) โ†ฆ ๐ด)โ€˜๐‘ง))) โ†’ ((๐‘ฅ โˆˆ (๐‘‹[,]๐‘Œ) โ†ฆ ๐ด)โ€˜๐‘ฆ) โˆˆ โ„*)
6866, 21syl 17 . . . . . . 7 ((๐œ‘ โˆง (๐‘ฆ โˆˆ (๐‘‹[,]๐‘Œ) โˆง โˆ€๐‘ง โˆˆ (๐‘‹[,]๐‘Œ)((๐‘ฅ โˆˆ (๐‘‹[,]๐‘Œ) โ†ฆ ๐ด)โ€˜๐‘ฆ) โ‰ค ((๐‘ฅ โˆˆ (๐‘‹[,]๐‘Œ) โ†ฆ ๐ด)โ€˜๐‘ง))) โ†’ (๐‘ < ((๐‘ฅ โˆˆ (๐‘‹[,]๐‘Œ) โ†ฆ ๐ด)โ€˜๐‘ฆ) โˆง ((๐‘ฅ โˆˆ (๐‘‹[,]๐‘Œ) โ†ฆ ๐ด)โ€˜๐‘ฆ) < ๐‘Š))
6968simpld 496 . . . . . 6 ((๐œ‘ โˆง (๐‘ฆ โˆˆ (๐‘‹[,]๐‘Œ) โˆง โˆ€๐‘ง โˆˆ (๐‘‹[,]๐‘Œ)((๐‘ฅ โˆˆ (๐‘‹[,]๐‘Œ) โ†ฆ ๐ด)โ€˜๐‘ฆ) โ‰ค ((๐‘ฅ โˆˆ (๐‘‹[,]๐‘Œ) โ†ฆ ๐ด)โ€˜๐‘ง))) โ†’ ๐‘ < ((๐‘ฅ โˆˆ (๐‘‹[,]๐‘Œ) โ†ฆ ๐ด)โ€˜๐‘ฆ))
70 qbtwnxr 13125 . . . . . 6 ((๐‘ โˆˆ โ„* โˆง ((๐‘ฅ โˆˆ (๐‘‹[,]๐‘Œ) โ†ฆ ๐ด)โ€˜๐‘ฆ) โˆˆ โ„* โˆง ๐‘ < ((๐‘ฅ โˆˆ (๐‘‹[,]๐‘Œ) โ†ฆ ๐ด)โ€˜๐‘ฆ)) โ†’ โˆƒ๐‘š โˆˆ โ„š (๐‘ < ๐‘š โˆง ๐‘š < ((๐‘ฅ โˆˆ (๐‘‹[,]๐‘Œ) โ†ฆ ๐ด)โ€˜๐‘ฆ)))
7163, 67, 69, 70syl3anc 1372 . . . . 5 ((๐œ‘ โˆง (๐‘ฆ โˆˆ (๐‘‹[,]๐‘Œ) โˆง โˆ€๐‘ง โˆˆ (๐‘‹[,]๐‘Œ)((๐‘ฅ โˆˆ (๐‘‹[,]๐‘Œ) โ†ฆ ๐ด)โ€˜๐‘ฆ) โ‰ค ((๐‘ฅ โˆˆ (๐‘‹[,]๐‘Œ) โ†ฆ ๐ด)โ€˜๐‘ง))) โ†’ โˆƒ๐‘š โˆˆ โ„š (๐‘ < ๐‘š โˆง ๐‘š < ((๐‘ฅ โˆˆ (๐‘‹[,]๐‘Œ) โ†ฆ ๐ด)โ€˜๐‘ฆ)))
72 qre 12883 . . . . . . 7 (๐‘š โˆˆ โ„š โ†’ ๐‘š โˆˆ โ„)
7372ad2antrl 727 . . . . . 6 (((๐œ‘ โˆง (๐‘ฆ โˆˆ (๐‘‹[,]๐‘Œ) โˆง โˆ€๐‘ง โˆˆ (๐‘‹[,]๐‘Œ)((๐‘ฅ โˆˆ (๐‘‹[,]๐‘Œ) โ†ฆ ๐ด)โ€˜๐‘ฆ) โ‰ค ((๐‘ฅ โˆˆ (๐‘‹[,]๐‘Œ) โ†ฆ ๐ด)โ€˜๐‘ง))) โˆง (๐‘š โˆˆ โ„š โˆง (๐‘ < ๐‘š โˆง ๐‘š < ((๐‘ฅ โˆˆ (๐‘‹[,]๐‘Œ) โ†ฆ ๐ด)โ€˜๐‘ฆ)))) โ†’ ๐‘š โˆˆ โ„)
74 simprrl 780 . . . . . 6 (((๐œ‘ โˆง (๐‘ฆ โˆˆ (๐‘‹[,]๐‘Œ) โˆง โˆ€๐‘ง โˆˆ (๐‘‹[,]๐‘Œ)((๐‘ฅ โˆˆ (๐‘‹[,]๐‘Œ) โ†ฆ ๐ด)โ€˜๐‘ฆ) โ‰ค ((๐‘ฅ โˆˆ (๐‘‹[,]๐‘Œ) โ†ฆ ๐ด)โ€˜๐‘ง))) โˆง (๐‘š โˆˆ โ„š โˆง (๐‘ < ๐‘š โˆง ๐‘š < ((๐‘ฅ โˆˆ (๐‘‹[,]๐‘Œ) โ†ฆ ๐ด)โ€˜๐‘ฆ)))) โ†’ ๐‘ < ๐‘š)
7573rexrd 11210 . . . . . . 7 (((๐œ‘ โˆง (๐‘ฆ โˆˆ (๐‘‹[,]๐‘Œ) โˆง โˆ€๐‘ง โˆˆ (๐‘‹[,]๐‘Œ)((๐‘ฅ โˆˆ (๐‘‹[,]๐‘Œ) โ†ฆ ๐ด)โ€˜๐‘ฆ) โ‰ค ((๐‘ฅ โˆˆ (๐‘‹[,]๐‘Œ) โ†ฆ ๐ด)โ€˜๐‘ง))) โˆง (๐‘š โˆˆ โ„š โˆง (๐‘ < ๐‘š โˆง ๐‘š < ((๐‘ฅ โˆˆ (๐‘‹[,]๐‘Œ) โ†ฆ ๐ด)โ€˜๐‘ฆ)))) โ†’ ๐‘š โˆˆ โ„*)
7667adantr 482 . . . . . . 7 (((๐œ‘ โˆง (๐‘ฆ โˆˆ (๐‘‹[,]๐‘Œ) โˆง โˆ€๐‘ง โˆˆ (๐‘‹[,]๐‘Œ)((๐‘ฅ โˆˆ (๐‘‹[,]๐‘Œ) โ†ฆ ๐ด)โ€˜๐‘ฆ) โ‰ค ((๐‘ฅ โˆˆ (๐‘‹[,]๐‘Œ) โ†ฆ ๐ด)โ€˜๐‘ง))) โˆง (๐‘š โˆˆ โ„š โˆง (๐‘ < ๐‘š โˆง ๐‘š < ((๐‘ฅ โˆˆ (๐‘‹[,]๐‘Œ) โ†ฆ ๐ด)โ€˜๐‘ฆ)))) โ†’ ((๐‘ฅ โˆˆ (๐‘‹[,]๐‘Œ) โ†ฆ ๐ด)โ€˜๐‘ฆ) โˆˆ โ„*)
7719ad2antrr 725 . . . . . . 7 (((๐œ‘ โˆง (๐‘ฆ โˆˆ (๐‘‹[,]๐‘Œ) โˆง โˆ€๐‘ง โˆˆ (๐‘‹[,]๐‘Œ)((๐‘ฅ โˆˆ (๐‘‹[,]๐‘Œ) โ†ฆ ๐ด)โ€˜๐‘ฆ) โ‰ค ((๐‘ฅ โˆˆ (๐‘‹[,]๐‘Œ) โ†ฆ ๐ด)โ€˜๐‘ง))) โˆง (๐‘š โˆˆ โ„š โˆง (๐‘ < ๐‘š โˆง ๐‘š < ((๐‘ฅ โˆˆ (๐‘‹[,]๐‘Œ) โ†ฆ ๐ด)โ€˜๐‘ฆ)))) โ†’ ๐‘Š โˆˆ โ„*)
78 simprrr 781 . . . . . . 7 (((๐œ‘ โˆง (๐‘ฆ โˆˆ (๐‘‹[,]๐‘Œ) โˆง โˆ€๐‘ง โˆˆ (๐‘‹[,]๐‘Œ)((๐‘ฅ โˆˆ (๐‘‹[,]๐‘Œ) โ†ฆ ๐ด)โ€˜๐‘ฆ) โ‰ค ((๐‘ฅ โˆˆ (๐‘‹[,]๐‘Œ) โ†ฆ ๐ด)โ€˜๐‘ง))) โˆง (๐‘š โˆˆ โ„š โˆง (๐‘ < ๐‘š โˆง ๐‘š < ((๐‘ฅ โˆˆ (๐‘‹[,]๐‘Œ) โ†ฆ ๐ด)โ€˜๐‘ฆ)))) โ†’ ๐‘š < ((๐‘ฅ โˆˆ (๐‘‹[,]๐‘Œ) โ†ฆ ๐ด)โ€˜๐‘ฆ))
7968simprd 497 . . . . . . . 8 ((๐œ‘ โˆง (๐‘ฆ โˆˆ (๐‘‹[,]๐‘Œ) โˆง โˆ€๐‘ง โˆˆ (๐‘‹[,]๐‘Œ)((๐‘ฅ โˆˆ (๐‘‹[,]๐‘Œ) โ†ฆ ๐ด)โ€˜๐‘ฆ) โ‰ค ((๐‘ฅ โˆˆ (๐‘‹[,]๐‘Œ) โ†ฆ ๐ด)โ€˜๐‘ง))) โ†’ ((๐‘ฅ โˆˆ (๐‘‹[,]๐‘Œ) โ†ฆ ๐ด)โ€˜๐‘ฆ) < ๐‘Š)
8079adantr 482 . . . . . . 7 (((๐œ‘ โˆง (๐‘ฆ โˆˆ (๐‘‹[,]๐‘Œ) โˆง โˆ€๐‘ง โˆˆ (๐‘‹[,]๐‘Œ)((๐‘ฅ โˆˆ (๐‘‹[,]๐‘Œ) โ†ฆ ๐ด)โ€˜๐‘ฆ) โ‰ค ((๐‘ฅ โˆˆ (๐‘‹[,]๐‘Œ) โ†ฆ ๐ด)โ€˜๐‘ง))) โˆง (๐‘š โˆˆ โ„š โˆง (๐‘ < ๐‘š โˆง ๐‘š < ((๐‘ฅ โˆˆ (๐‘‹[,]๐‘Œ) โ†ฆ ๐ด)โ€˜๐‘ฆ)))) โ†’ ((๐‘ฅ โˆˆ (๐‘‹[,]๐‘Œ) โ†ฆ ๐ด)โ€˜๐‘ฆ) < ๐‘Š)
8175, 76, 77, 78, 80xrlttrd 13084 . . . . . 6 (((๐œ‘ โˆง (๐‘ฆ โˆˆ (๐‘‹[,]๐‘Œ) โˆง โˆ€๐‘ง โˆˆ (๐‘‹[,]๐‘Œ)((๐‘ฅ โˆˆ (๐‘‹[,]๐‘Œ) โ†ฆ ๐ด)โ€˜๐‘ฆ) โ‰ค ((๐‘ฅ โˆˆ (๐‘‹[,]๐‘Œ) โ†ฆ ๐ด)โ€˜๐‘ง))) โˆง (๐‘š โˆˆ โ„š โˆง (๐‘ < ๐‘š โˆง ๐‘š < ((๐‘ฅ โˆˆ (๐‘‹[,]๐‘Œ) โ†ฆ ๐ด)โ€˜๐‘ฆ)))) โ†’ ๐‘š < ๐‘Š)
8228ad2antrr 725 . . . . . . 7 (((๐œ‘ โˆง (๐‘ฆ โˆˆ (๐‘‹[,]๐‘Œ) โˆง โˆ€๐‘ง โˆˆ (๐‘‹[,]๐‘Œ)((๐‘ฅ โˆˆ (๐‘‹[,]๐‘Œ) โ†ฆ ๐ด)โ€˜๐‘ฆ) โ‰ค ((๐‘ฅ โˆˆ (๐‘‹[,]๐‘Œ) โ†ฆ ๐ด)โ€˜๐‘ง))) โˆง (๐‘š โˆˆ โ„š โˆง (๐‘ < ๐‘š โˆง ๐‘š < ((๐‘ฅ โˆˆ (๐‘‹[,]๐‘Œ) โ†ฆ ๐ด)โ€˜๐‘ฆ)))) โ†’ ๐‘ โˆˆ โ„*)
83 elioo2 13311 . . . . . . 7 ((๐‘ โˆˆ โ„* โˆง ๐‘Š โˆˆ โ„*) โ†’ (๐‘š โˆˆ (๐‘(,)๐‘Š) โ†” (๐‘š โˆˆ โ„ โˆง ๐‘ < ๐‘š โˆง ๐‘š < ๐‘Š)))
8482, 77, 83syl2anc 585 . . . . . 6 (((๐œ‘ โˆง (๐‘ฆ โˆˆ (๐‘‹[,]๐‘Œ) โˆง โˆ€๐‘ง โˆˆ (๐‘‹[,]๐‘Œ)((๐‘ฅ โˆˆ (๐‘‹[,]๐‘Œ) โ†ฆ ๐ด)โ€˜๐‘ฆ) โ‰ค ((๐‘ฅ โˆˆ (๐‘‹[,]๐‘Œ) โ†ฆ ๐ด)โ€˜๐‘ง))) โˆง (๐‘š โˆˆ โ„š โˆง (๐‘ < ๐‘š โˆง ๐‘š < ((๐‘ฅ โˆˆ (๐‘‹[,]๐‘Œ) โ†ฆ ๐ด)โ€˜๐‘ฆ)))) โ†’ (๐‘š โˆˆ (๐‘(,)๐‘Š) โ†” (๐‘š โˆˆ โ„ โˆง ๐‘ < ๐‘š โˆง ๐‘š < ๐‘Š)))
8573, 74, 81, 84mpbir3and 1343 . . . . 5 (((๐œ‘ โˆง (๐‘ฆ โˆˆ (๐‘‹[,]๐‘Œ) โˆง โˆ€๐‘ง โˆˆ (๐‘‹[,]๐‘Œ)((๐‘ฅ โˆˆ (๐‘‹[,]๐‘Œ) โ†ฆ ๐ด)โ€˜๐‘ฆ) โ‰ค ((๐‘ฅ โˆˆ (๐‘‹[,]๐‘Œ) โ†ฆ ๐ด)โ€˜๐‘ง))) โˆง (๐‘š โˆˆ โ„š โˆง (๐‘ < ๐‘š โˆง ๐‘š < ((๐‘ฅ โˆˆ (๐‘‹[,]๐‘Œ) โ†ฆ ๐ด)โ€˜๐‘ฆ)))) โ†’ ๐‘š โˆˆ (๐‘(,)๐‘Š))
86 anass 470 . . . . . 6 (((๐œ‘ โˆง ๐‘ฆ โˆˆ (๐‘‹[,]๐‘Œ)) โˆง โˆ€๐‘ง โˆˆ (๐‘‹[,]๐‘Œ)((๐‘ฅ โˆˆ (๐‘‹[,]๐‘Œ) โ†ฆ ๐ด)โ€˜๐‘ฆ) โ‰ค ((๐‘ฅ โˆˆ (๐‘‹[,]๐‘Œ) โ†ฆ ๐ด)โ€˜๐‘ง)) โ†” (๐œ‘ โˆง (๐‘ฆ โˆˆ (๐‘‹[,]๐‘Œ) โˆง โˆ€๐‘ง โˆˆ (๐‘‹[,]๐‘Œ)((๐‘ฅ โˆˆ (๐‘‹[,]๐‘Œ) โ†ฆ ๐ด)โ€˜๐‘ฆ) โ‰ค ((๐‘ฅ โˆˆ (๐‘‹[,]๐‘Œ) โ†ฆ ๐ด)โ€˜๐‘ง))))
87 simprrr 781 . . . . . . . . . . 11 (((๐œ‘ โˆง ๐‘ฆ โˆˆ (๐‘‹[,]๐‘Œ)) โˆง (๐‘š โˆˆ โ„š โˆง (๐‘ < ๐‘š โˆง ๐‘š < ((๐‘ฅ โˆˆ (๐‘‹[,]๐‘Œ) โ†ฆ ๐ด)โ€˜๐‘ฆ)))) โ†’ ๐‘š < ((๐‘ฅ โˆˆ (๐‘‹[,]๐‘Œ) โ†ฆ ๐ด)โ€˜๐‘ฆ))
8887adantr 482 . . . . . . . . . 10 ((((๐œ‘ โˆง ๐‘ฆ โˆˆ (๐‘‹[,]๐‘Œ)) โˆง (๐‘š โˆˆ โ„š โˆง (๐‘ < ๐‘š โˆง ๐‘š < ((๐‘ฅ โˆˆ (๐‘‹[,]๐‘Œ) โ†ฆ ๐ด)โ€˜๐‘ฆ)))) โˆง ๐‘ง โˆˆ (๐‘‹[,]๐‘Œ)) โ†’ ๐‘š < ((๐‘ฅ โˆˆ (๐‘‹[,]๐‘Œ) โ†ฆ ๐ด)โ€˜๐‘ฆ))
8972ad2antrl 727 . . . . . . . . . . . . 13 (((๐œ‘ โˆง ๐‘ฆ โˆˆ (๐‘‹[,]๐‘Œ)) โˆง (๐‘š โˆˆ โ„š โˆง (๐‘ < ๐‘š โˆง ๐‘š < ((๐‘ฅ โˆˆ (๐‘‹[,]๐‘Œ) โ†ฆ ๐ด)โ€˜๐‘ฆ)))) โ†’ ๐‘š โˆˆ โ„)
9089adantr 482 . . . . . . . . . . . 12 ((((๐œ‘ โˆง ๐‘ฆ โˆˆ (๐‘‹[,]๐‘Œ)) โˆง (๐‘š โˆˆ โ„š โˆง (๐‘ < ๐‘š โˆง ๐‘š < ((๐‘ฅ โˆˆ (๐‘‹[,]๐‘Œ) โ†ฆ ๐ด)โ€˜๐‘ฆ)))) โˆง ๐‘ง โˆˆ (๐‘‹[,]๐‘Œ)) โ†’ ๐‘š โˆˆ โ„)
9190rexrd 11210 . . . . . . . . . . 11 ((((๐œ‘ โˆง ๐‘ฆ โˆˆ (๐‘‹[,]๐‘Œ)) โˆง (๐‘š โˆˆ โ„š โˆง (๐‘ < ๐‘š โˆง ๐‘š < ((๐‘ฅ โˆˆ (๐‘‹[,]๐‘Œ) โ†ฆ ๐ด)โ€˜๐‘ฆ)))) โˆง ๐‘ง โˆˆ (๐‘‹[,]๐‘Œ)) โ†’ ๐‘š โˆˆ โ„*)
9214ad2antrr 725 . . . . . . . . . . . . . 14 (((๐œ‘ โˆง ๐‘ฆ โˆˆ (๐‘‹[,]๐‘Œ)) โˆง (๐‘š โˆˆ โ„š โˆง (๐‘ < ๐‘š โˆง ๐‘š < ((๐‘ฅ โˆˆ (๐‘‹[,]๐‘Œ) โ†ฆ ๐ด)โ€˜๐‘ฆ)))) โ†’ (๐‘ฅ โˆˆ (๐‘‹[,]๐‘Œ) โ†ฆ ๐ด):(๐‘‹[,]๐‘Œ)โŸถ(๐‘(,)๐‘Š))
93 simplr 768 . . . . . . . . . . . . . 14 (((๐œ‘ โˆง ๐‘ฆ โˆˆ (๐‘‹[,]๐‘Œ)) โˆง (๐‘š โˆˆ โ„š โˆง (๐‘ < ๐‘š โˆง ๐‘š < ((๐‘ฅ โˆˆ (๐‘‹[,]๐‘Œ) โ†ฆ ๐ด)โ€˜๐‘ฆ)))) โ†’ ๐‘ฆ โˆˆ (๐‘‹[,]๐‘Œ))
9492, 93ffvelcdmd 7037 . . . . . . . . . . . . 13 (((๐œ‘ โˆง ๐‘ฆ โˆˆ (๐‘‹[,]๐‘Œ)) โˆง (๐‘š โˆˆ โ„š โˆง (๐‘ < ๐‘š โˆง ๐‘š < ((๐‘ฅ โˆˆ (๐‘‹[,]๐‘Œ) โ†ฆ ๐ด)โ€˜๐‘ฆ)))) โ†’ ((๐‘ฅ โˆˆ (๐‘‹[,]๐‘Œ) โ†ฆ ๐ด)โ€˜๐‘ฆ) โˆˆ (๐‘(,)๐‘Š))
9512, 94sselid 3943 . . . . . . . . . . . 12 (((๐œ‘ โˆง ๐‘ฆ โˆˆ (๐‘‹[,]๐‘Œ)) โˆง (๐‘š โˆˆ โ„š โˆง (๐‘ < ๐‘š โˆง ๐‘š < ((๐‘ฅ โˆˆ (๐‘‹[,]๐‘Œ) โ†ฆ ๐ด)โ€˜๐‘ฆ)))) โ†’ ((๐‘ฅ โˆˆ (๐‘‹[,]๐‘Œ) โ†ฆ ๐ด)โ€˜๐‘ฆ) โˆˆ โ„*)
9695adantr 482 . . . . . . . . . . 11 ((((๐œ‘ โˆง ๐‘ฆ โˆˆ (๐‘‹[,]๐‘Œ)) โˆง (๐‘š โˆˆ โ„š โˆง (๐‘ < ๐‘š โˆง ๐‘š < ((๐‘ฅ โˆˆ (๐‘‹[,]๐‘Œ) โ†ฆ ๐ด)โ€˜๐‘ฆ)))) โˆง ๐‘ง โˆˆ (๐‘‹[,]๐‘Œ)) โ†’ ((๐‘ฅ โˆˆ (๐‘‹[,]๐‘Œ) โ†ฆ ๐ด)โ€˜๐‘ฆ) โˆˆ โ„*)
9792ffvelcdmda 7036 . . . . . . . . . . . 12 ((((๐œ‘ โˆง ๐‘ฆ โˆˆ (๐‘‹[,]๐‘Œ)) โˆง (๐‘š โˆˆ โ„š โˆง (๐‘ < ๐‘š โˆง ๐‘š < ((๐‘ฅ โˆˆ (๐‘‹[,]๐‘Œ) โ†ฆ ๐ด)โ€˜๐‘ฆ)))) โˆง ๐‘ง โˆˆ (๐‘‹[,]๐‘Œ)) โ†’ ((๐‘ฅ โˆˆ (๐‘‹[,]๐‘Œ) โ†ฆ ๐ด)โ€˜๐‘ง) โˆˆ (๐‘(,)๐‘Š))
9812, 97sselid 3943 . . . . . . . . . . 11 ((((๐œ‘ โˆง ๐‘ฆ โˆˆ (๐‘‹[,]๐‘Œ)) โˆง (๐‘š โˆˆ โ„š โˆง (๐‘ < ๐‘š โˆง ๐‘š < ((๐‘ฅ โˆˆ (๐‘‹[,]๐‘Œ) โ†ฆ ๐ด)โ€˜๐‘ฆ)))) โˆง ๐‘ง โˆˆ (๐‘‹[,]๐‘Œ)) โ†’ ((๐‘ฅ โˆˆ (๐‘‹[,]๐‘Œ) โ†ฆ ๐ด)โ€˜๐‘ง) โˆˆ โ„*)
99 xrltletr 13082 . . . . . . . . . . 11 ((๐‘š โˆˆ โ„* โˆง ((๐‘ฅ โˆˆ (๐‘‹[,]๐‘Œ) โ†ฆ ๐ด)โ€˜๐‘ฆ) โˆˆ โ„* โˆง ((๐‘ฅ โˆˆ (๐‘‹[,]๐‘Œ) โ†ฆ ๐ด)โ€˜๐‘ง) โˆˆ โ„*) โ†’ ((๐‘š < ((๐‘ฅ โˆˆ (๐‘‹[,]๐‘Œ) โ†ฆ ๐ด)โ€˜๐‘ฆ) โˆง ((๐‘ฅ โˆˆ (๐‘‹[,]๐‘Œ) โ†ฆ ๐ด)โ€˜๐‘ฆ) โ‰ค ((๐‘ฅ โˆˆ (๐‘‹[,]๐‘Œ) โ†ฆ ๐ด)โ€˜๐‘ง)) โ†’ ๐‘š < ((๐‘ฅ โˆˆ (๐‘‹[,]๐‘Œ) โ†ฆ ๐ด)โ€˜๐‘ง)))
10091, 96, 98, 99syl3anc 1372 . . . . . . . . . 10 ((((๐œ‘ โˆง ๐‘ฆ โˆˆ (๐‘‹[,]๐‘Œ)) โˆง (๐‘š โˆˆ โ„š โˆง (๐‘ < ๐‘š โˆง ๐‘š < ((๐‘ฅ โˆˆ (๐‘‹[,]๐‘Œ) โ†ฆ ๐ด)โ€˜๐‘ฆ)))) โˆง ๐‘ง โˆˆ (๐‘‹[,]๐‘Œ)) โ†’ ((๐‘š < ((๐‘ฅ โˆˆ (๐‘‹[,]๐‘Œ) โ†ฆ ๐ด)โ€˜๐‘ฆ) โˆง ((๐‘ฅ โˆˆ (๐‘‹[,]๐‘Œ) โ†ฆ ๐ด)โ€˜๐‘ฆ) โ‰ค ((๐‘ฅ โˆˆ (๐‘‹[,]๐‘Œ) โ†ฆ ๐ด)โ€˜๐‘ง)) โ†’ ๐‘š < ((๐‘ฅ โˆˆ (๐‘‹[,]๐‘Œ) โ†ฆ ๐ด)โ€˜๐‘ง)))
10188, 100mpand 694 . . . . . . . . 9 ((((๐œ‘ โˆง ๐‘ฆ โˆˆ (๐‘‹[,]๐‘Œ)) โˆง (๐‘š โˆˆ โ„š โˆง (๐‘ < ๐‘š โˆง ๐‘š < ((๐‘ฅ โˆˆ (๐‘‹[,]๐‘Œ) โ†ฆ ๐ด)โ€˜๐‘ฆ)))) โˆง ๐‘ง โˆˆ (๐‘‹[,]๐‘Œ)) โ†’ (((๐‘ฅ โˆˆ (๐‘‹[,]๐‘Œ) โ†ฆ ๐ด)โ€˜๐‘ฆ) โ‰ค ((๐‘ฅ โˆˆ (๐‘‹[,]๐‘Œ) โ†ฆ ๐ด)โ€˜๐‘ง) โ†’ ๐‘š < ((๐‘ฅ โˆˆ (๐‘‹[,]๐‘Œ) โ†ฆ ๐ด)โ€˜๐‘ง)))
102101ralimdva 3161 . . . . . . . 8 (((๐œ‘ โˆง ๐‘ฆ โˆˆ (๐‘‹[,]๐‘Œ)) โˆง (๐‘š โˆˆ โ„š โˆง (๐‘ < ๐‘š โˆง ๐‘š < ((๐‘ฅ โˆˆ (๐‘‹[,]๐‘Œ) โ†ฆ ๐ด)โ€˜๐‘ฆ)))) โ†’ (โˆ€๐‘ง โˆˆ (๐‘‹[,]๐‘Œ)((๐‘ฅ โˆˆ (๐‘‹[,]๐‘Œ) โ†ฆ ๐ด)โ€˜๐‘ฆ) โ‰ค ((๐‘ฅ โˆˆ (๐‘‹[,]๐‘Œ) โ†ฆ ๐ด)โ€˜๐‘ง) โ†’ โˆ€๐‘ง โˆˆ (๐‘‹[,]๐‘Œ)๐‘š < ((๐‘ฅ โˆˆ (๐‘‹[,]๐‘Œ) โ†ฆ ๐ด)โ€˜๐‘ง)))
103102imp 408 . . . . . . 7 ((((๐œ‘ โˆง ๐‘ฆ โˆˆ (๐‘‹[,]๐‘Œ)) โˆง (๐‘š โˆˆ โ„š โˆง (๐‘ < ๐‘š โˆง ๐‘š < ((๐‘ฅ โˆˆ (๐‘‹[,]๐‘Œ) โ†ฆ ๐ด)โ€˜๐‘ฆ)))) โˆง โˆ€๐‘ง โˆˆ (๐‘‹[,]๐‘Œ)((๐‘ฅ โˆˆ (๐‘‹[,]๐‘Œ) โ†ฆ ๐ด)โ€˜๐‘ฆ) โ‰ค ((๐‘ฅ โˆˆ (๐‘‹[,]๐‘Œ) โ†ฆ ๐ด)โ€˜๐‘ง)) โ†’ โˆ€๐‘ง โˆˆ (๐‘‹[,]๐‘Œ)๐‘š < ((๐‘ฅ โˆˆ (๐‘‹[,]๐‘Œ) โ†ฆ ๐ด)โ€˜๐‘ง))
104103an32s 651 . . . . . 6 ((((๐œ‘ โˆง ๐‘ฆ โˆˆ (๐‘‹[,]๐‘Œ)) โˆง โˆ€๐‘ง โˆˆ (๐‘‹[,]๐‘Œ)((๐‘ฅ โˆˆ (๐‘‹[,]๐‘Œ) โ†ฆ ๐ด)โ€˜๐‘ฆ) โ‰ค ((๐‘ฅ โˆˆ (๐‘‹[,]๐‘Œ) โ†ฆ ๐ด)โ€˜๐‘ง)) โˆง (๐‘š โˆˆ โ„š โˆง (๐‘ < ๐‘š โˆง ๐‘š < ((๐‘ฅ โˆˆ (๐‘‹[,]๐‘Œ) โ†ฆ ๐ด)โ€˜๐‘ฆ)))) โ†’ โˆ€๐‘ง โˆˆ (๐‘‹[,]๐‘Œ)๐‘š < ((๐‘ฅ โˆˆ (๐‘‹[,]๐‘Œ) โ†ฆ ๐ด)โ€˜๐‘ง))
10586, 104sylanbr 583 . . . . 5 (((๐œ‘ โˆง (๐‘ฆ โˆˆ (๐‘‹[,]๐‘Œ) โˆง โˆ€๐‘ง โˆˆ (๐‘‹[,]๐‘Œ)((๐‘ฅ โˆˆ (๐‘‹[,]๐‘Œ) โ†ฆ ๐ด)โ€˜๐‘ฆ) โ‰ค ((๐‘ฅ โˆˆ (๐‘‹[,]๐‘Œ) โ†ฆ ๐ด)โ€˜๐‘ง))) โˆง (๐‘š โˆˆ โ„š โˆง (๐‘ < ๐‘š โˆง ๐‘š < ((๐‘ฅ โˆˆ (๐‘‹[,]๐‘Œ) โ†ฆ ๐ด)โ€˜๐‘ฆ)))) โ†’ โˆ€๐‘ง โˆˆ (๐‘‹[,]๐‘Œ)๐‘š < ((๐‘ฅ โˆˆ (๐‘‹[,]๐‘Œ) โ†ฆ ๐ด)โ€˜๐‘ง))
10671, 85, 105reximssdv 3166 . . . 4 ((๐œ‘ โˆง (๐‘ฆ โˆˆ (๐‘‹[,]๐‘Œ) โˆง โˆ€๐‘ง โˆˆ (๐‘‹[,]๐‘Œ)((๐‘ฅ โˆˆ (๐‘‹[,]๐‘Œ) โ†ฆ ๐ด)โ€˜๐‘ฆ) โ‰ค ((๐‘ฅ โˆˆ (๐‘‹[,]๐‘Œ) โ†ฆ ๐ด)โ€˜๐‘ง))) โ†’ โˆƒ๐‘š โˆˆ (๐‘(,)๐‘Š)โˆ€๐‘ง โˆˆ (๐‘‹[,]๐‘Œ)๐‘š < ((๐‘ฅ โˆˆ (๐‘‹[,]๐‘Œ) โ†ฆ ๐ด)โ€˜๐‘ง))
107106rexlimdvaa 3150 . . 3 (๐œ‘ โ†’ (โˆƒ๐‘ฆ โˆˆ (๐‘‹[,]๐‘Œ)โˆ€๐‘ง โˆˆ (๐‘‹[,]๐‘Œ)((๐‘ฅ โˆˆ (๐‘‹[,]๐‘Œ) โ†ฆ ๐ด)โ€˜๐‘ฆ) โ‰ค ((๐‘ฅ โˆˆ (๐‘‹[,]๐‘Œ) โ†ฆ ๐ด)โ€˜๐‘ง) โ†’ โˆƒ๐‘š โˆˆ (๐‘(,)๐‘Š)โˆ€๐‘ง โˆˆ (๐‘‹[,]๐‘Œ)๐‘š < ((๐‘ฅ โˆˆ (๐‘‹[,]๐‘Œ) โ†ฆ ๐ด)โ€˜๐‘ง)))
108 ancom 462 . . . . 5 ((โˆƒ๐‘› โˆˆ (๐‘(,)๐‘Š)โˆ€๐‘ง โˆˆ (๐‘‹[,]๐‘Œ)((๐‘ฅ โˆˆ (๐‘‹[,]๐‘Œ) โ†ฆ ๐ด)โ€˜๐‘ง) < ๐‘› โˆง โˆƒ๐‘š โˆˆ (๐‘(,)๐‘Š)โˆ€๐‘ง โˆˆ (๐‘‹[,]๐‘Œ)๐‘š < ((๐‘ฅ โˆˆ (๐‘‹[,]๐‘Œ) โ†ฆ ๐ด)โ€˜๐‘ง)) โ†” (โˆƒ๐‘š โˆˆ (๐‘(,)๐‘Š)โˆ€๐‘ง โˆˆ (๐‘‹[,]๐‘Œ)๐‘š < ((๐‘ฅ โˆˆ (๐‘‹[,]๐‘Œ) โ†ฆ ๐ด)โ€˜๐‘ง) โˆง โˆƒ๐‘› โˆˆ (๐‘(,)๐‘Š)โˆ€๐‘ง โˆˆ (๐‘‹[,]๐‘Œ)((๐‘ฅ โˆˆ (๐‘‹[,]๐‘Œ) โ†ฆ ๐ด)โ€˜๐‘ง) < ๐‘›))
109 reeanv 3216 . . . . 5 (โˆƒ๐‘š โˆˆ (๐‘(,)๐‘Š)โˆƒ๐‘› โˆˆ (๐‘(,)๐‘Š)(โˆ€๐‘ง โˆˆ (๐‘‹[,]๐‘Œ)๐‘š < ((๐‘ฅ โˆˆ (๐‘‹[,]๐‘Œ) โ†ฆ ๐ด)โ€˜๐‘ง) โˆง โˆ€๐‘ง โˆˆ (๐‘‹[,]๐‘Œ)((๐‘ฅ โˆˆ (๐‘‹[,]๐‘Œ) โ†ฆ ๐ด)โ€˜๐‘ง) < ๐‘›) โ†” (โˆƒ๐‘š โˆˆ (๐‘(,)๐‘Š)โˆ€๐‘ง โˆˆ (๐‘‹[,]๐‘Œ)๐‘š < ((๐‘ฅ โˆˆ (๐‘‹[,]๐‘Œ) โ†ฆ ๐ด)โ€˜๐‘ง) โˆง โˆƒ๐‘› โˆˆ (๐‘(,)๐‘Š)โˆ€๐‘ง โˆˆ (๐‘‹[,]๐‘Œ)((๐‘ฅ โˆˆ (๐‘‹[,]๐‘Œ) โ†ฆ ๐ด)โ€˜๐‘ง) < ๐‘›))
110108, 109bitr4i 278 . . . 4 ((โˆƒ๐‘› โˆˆ (๐‘(,)๐‘Š)โˆ€๐‘ง โˆˆ (๐‘‹[,]๐‘Œ)((๐‘ฅ โˆˆ (๐‘‹[,]๐‘Œ) โ†ฆ ๐ด)โ€˜๐‘ง) < ๐‘› โˆง โˆƒ๐‘š โˆˆ (๐‘(,)๐‘Š)โˆ€๐‘ง โˆˆ (๐‘‹[,]๐‘Œ)๐‘š < ((๐‘ฅ โˆˆ (๐‘‹[,]๐‘Œ) โ†ฆ ๐ด)โ€˜๐‘ง)) โ†” โˆƒ๐‘š โˆˆ (๐‘(,)๐‘Š)โˆƒ๐‘› โˆˆ (๐‘(,)๐‘Š)(โˆ€๐‘ง โˆˆ (๐‘‹[,]๐‘Œ)๐‘š < ((๐‘ฅ โˆˆ (๐‘‹[,]๐‘Œ) โ†ฆ ๐ด)โ€˜๐‘ง) โˆง โˆ€๐‘ง โˆˆ (๐‘‹[,]๐‘Œ)((๐‘ฅ โˆˆ (๐‘‹[,]๐‘Œ) โ†ฆ ๐ด)โ€˜๐‘ง) < ๐‘›))
111 r19.26 3111 . . . . . 6 (โˆ€๐‘ง โˆˆ (๐‘‹[,]๐‘Œ)(๐‘š < ((๐‘ฅ โˆˆ (๐‘‹[,]๐‘Œ) โ†ฆ ๐ด)โ€˜๐‘ง) โˆง ((๐‘ฅ โˆˆ (๐‘‹[,]๐‘Œ) โ†ฆ ๐ด)โ€˜๐‘ง) < ๐‘›) โ†” (โˆ€๐‘ง โˆˆ (๐‘‹[,]๐‘Œ)๐‘š < ((๐‘ฅ โˆˆ (๐‘‹[,]๐‘Œ) โ†ฆ ๐ด)โ€˜๐‘ง) โˆง โˆ€๐‘ง โˆˆ (๐‘‹[,]๐‘Œ)((๐‘ฅ โˆˆ (๐‘‹[,]๐‘Œ) โ†ฆ ๐ด)โ€˜๐‘ง) < ๐‘›))
11214adantr 482 . . . . . . . . . . . 12 ((๐œ‘ โˆง (๐‘š โˆˆ (๐‘(,)๐‘Š) โˆง ๐‘› โˆˆ (๐‘(,)๐‘Š))) โ†’ (๐‘ฅ โˆˆ (๐‘‹[,]๐‘Œ) โ†ฆ ๐ด):(๐‘‹[,]๐‘Œ)โŸถ(๐‘(,)๐‘Š))
113112ffvelcdmda 7036 . . . . . . . . . . 11 (((๐œ‘ โˆง (๐‘š โˆˆ (๐‘(,)๐‘Š) โˆง ๐‘› โˆˆ (๐‘(,)๐‘Š))) โˆง ๐‘ง โˆˆ (๐‘‹[,]๐‘Œ)) โ†’ ((๐‘ฅ โˆˆ (๐‘‹[,]๐‘Œ) โ†ฆ ๐ด)โ€˜๐‘ง) โˆˆ (๐‘(,)๐‘Š))
1144, 113sselid 3943 . . . . . . . . . 10 (((๐œ‘ โˆง (๐‘š โˆˆ (๐‘(,)๐‘Š) โˆง ๐‘› โˆˆ (๐‘(,)๐‘Š))) โˆง ๐‘ง โˆˆ (๐‘‹[,]๐‘Œ)) โ†’ ((๐‘ฅ โˆˆ (๐‘‹[,]๐‘Œ) โ†ฆ ๐ด)โ€˜๐‘ง) โˆˆ โ„)
1151143biant1d 1479 . . . . . . . . 9 (((๐œ‘ โˆง (๐‘š โˆˆ (๐‘(,)๐‘Š) โˆง ๐‘› โˆˆ (๐‘(,)๐‘Š))) โˆง ๐‘ง โˆˆ (๐‘‹[,]๐‘Œ)) โ†’ ((๐‘š < ((๐‘ฅ โˆˆ (๐‘‹[,]๐‘Œ) โ†ฆ ๐ด)โ€˜๐‘ง) โˆง ((๐‘ฅ โˆˆ (๐‘‹[,]๐‘Œ) โ†ฆ ๐ด)โ€˜๐‘ง) < ๐‘›) โ†” (((๐‘ฅ โˆˆ (๐‘‹[,]๐‘Œ) โ†ฆ ๐ด)โ€˜๐‘ง) โˆˆ โ„ โˆง ๐‘š < ((๐‘ฅ โˆˆ (๐‘‹[,]๐‘Œ) โ†ฆ ๐ด)โ€˜๐‘ง) โˆง ((๐‘ฅ โˆˆ (๐‘‹[,]๐‘Œ) โ†ฆ ๐ด)โ€˜๐‘ง) < ๐‘›)))
116 simplrl 776 . . . . . . . . . . 11 (((๐œ‘ โˆง (๐‘š โˆˆ (๐‘(,)๐‘Š) โˆง ๐‘› โˆˆ (๐‘(,)๐‘Š))) โˆง ๐‘ง โˆˆ (๐‘‹[,]๐‘Œ)) โ†’ ๐‘š โˆˆ (๐‘(,)๐‘Š))
11712, 116sselid 3943 . . . . . . . . . 10 (((๐œ‘ โˆง (๐‘š โˆˆ (๐‘(,)๐‘Š) โˆง ๐‘› โˆˆ (๐‘(,)๐‘Š))) โˆง ๐‘ง โˆˆ (๐‘‹[,]๐‘Œ)) โ†’ ๐‘š โˆˆ โ„*)
118 simplrr 777 . . . . . . . . . . 11 (((๐œ‘ โˆง (๐‘š โˆˆ (๐‘(,)๐‘Š) โˆง ๐‘› โˆˆ (๐‘(,)๐‘Š))) โˆง ๐‘ง โˆˆ (๐‘‹[,]๐‘Œ)) โ†’ ๐‘› โˆˆ (๐‘(,)๐‘Š))
11912, 118sselid 3943 . . . . . . . . . 10 (((๐œ‘ โˆง (๐‘š โˆˆ (๐‘(,)๐‘Š) โˆง ๐‘› โˆˆ (๐‘(,)๐‘Š))) โˆง ๐‘ง โˆˆ (๐‘‹[,]๐‘Œ)) โ†’ ๐‘› โˆˆ โ„*)
120 elioo2 13311 . . . . . . . . . 10 ((๐‘š โˆˆ โ„* โˆง ๐‘› โˆˆ โ„*) โ†’ (((๐‘ฅ โˆˆ (๐‘‹[,]๐‘Œ) โ†ฆ ๐ด)โ€˜๐‘ง) โˆˆ (๐‘š(,)๐‘›) โ†” (((๐‘ฅ โˆˆ (๐‘‹[,]๐‘Œ) โ†ฆ ๐ด)โ€˜๐‘ง) โˆˆ โ„ โˆง ๐‘š < ((๐‘ฅ โˆˆ (๐‘‹[,]๐‘Œ) โ†ฆ ๐ด)โ€˜๐‘ง) โˆง ((๐‘ฅ โˆˆ (๐‘‹[,]๐‘Œ) โ†ฆ ๐ด)โ€˜๐‘ง) < ๐‘›)))
121117, 119, 120syl2anc 585 . . . . . . . . 9 (((๐œ‘ โˆง (๐‘š โˆˆ (๐‘(,)๐‘Š) โˆง ๐‘› โˆˆ (๐‘(,)๐‘Š))) โˆง ๐‘ง โˆˆ (๐‘‹[,]๐‘Œ)) โ†’ (((๐‘ฅ โˆˆ (๐‘‹[,]๐‘Œ) โ†ฆ ๐ด)โ€˜๐‘ง) โˆˆ (๐‘š(,)๐‘›) โ†” (((๐‘ฅ โˆˆ (๐‘‹[,]๐‘Œ) โ†ฆ ๐ด)โ€˜๐‘ง) โˆˆ โ„ โˆง ๐‘š < ((๐‘ฅ โˆˆ (๐‘‹[,]๐‘Œ) โ†ฆ ๐ด)โ€˜๐‘ง) โˆง ((๐‘ฅ โˆˆ (๐‘‹[,]๐‘Œ) โ†ฆ ๐ด)โ€˜๐‘ง) < ๐‘›)))
122115, 121bitr4d 282 . . . . . . . 8 (((๐œ‘ โˆง (๐‘š โˆˆ (๐‘(,)๐‘Š) โˆง ๐‘› โˆˆ (๐‘(,)๐‘Š))) โˆง ๐‘ง โˆˆ (๐‘‹[,]๐‘Œ)) โ†’ ((๐‘š < ((๐‘ฅ โˆˆ (๐‘‹[,]๐‘Œ) โ†ฆ ๐ด)โ€˜๐‘ง) โˆง ((๐‘ฅ โˆˆ (๐‘‹[,]๐‘Œ) โ†ฆ ๐ด)โ€˜๐‘ง) < ๐‘›) โ†” ((๐‘ฅ โˆˆ (๐‘‹[,]๐‘Œ) โ†ฆ ๐ด)โ€˜๐‘ง) โˆˆ (๐‘š(,)๐‘›)))
123122ralbidva 3169 . . . . . . 7 ((๐œ‘ โˆง (๐‘š โˆˆ (๐‘(,)๐‘Š) โˆง ๐‘› โˆˆ (๐‘(,)๐‘Š))) โ†’ (โˆ€๐‘ง โˆˆ (๐‘‹[,]๐‘Œ)(๐‘š < ((๐‘ฅ โˆˆ (๐‘‹[,]๐‘Œ) โ†ฆ ๐ด)โ€˜๐‘ง) โˆง ((๐‘ฅ โˆˆ (๐‘‹[,]๐‘Œ) โ†ฆ ๐ด)โ€˜๐‘ง) < ๐‘›) โ†” โˆ€๐‘ง โˆˆ (๐‘‹[,]๐‘Œ)((๐‘ฅ โˆˆ (๐‘‹[,]๐‘Œ) โ†ฆ ๐ด)โ€˜๐‘ง) โˆˆ (๐‘š(,)๐‘›)))
124 nffvmpt1 6854 . . . . . . . . . . . 12 โ„ฒ๐‘ฅ((๐‘ฅ โˆˆ (๐‘‹[,]๐‘Œ) โ†ฆ ๐ด)โ€˜๐‘ง)
125124nfel1 2920 . . . . . . . . . . 11 โ„ฒ๐‘ฅ((๐‘ฅ โˆˆ (๐‘‹[,]๐‘Œ) โ†ฆ ๐ด)โ€˜๐‘ง) โˆˆ (๐‘š(,)๐‘›)
126 nfv 1918 . . . . . . . . . . 11 โ„ฒ๐‘ง((๐‘ฅ โˆˆ (๐‘‹[,]๐‘Œ) โ†ฆ ๐ด)โ€˜๐‘ฅ) โˆˆ (๐‘š(,)๐‘›)
127 fveq2 6843 . . . . . . . . . . . 12 (๐‘ง = ๐‘ฅ โ†’ ((๐‘ฅ โˆˆ (๐‘‹[,]๐‘Œ) โ†ฆ ๐ด)โ€˜๐‘ง) = ((๐‘ฅ โˆˆ (๐‘‹[,]๐‘Œ) โ†ฆ ๐ด)โ€˜๐‘ฅ))
128127eleq1d 2819 . . . . . . . . . . 11 (๐‘ง = ๐‘ฅ โ†’ (((๐‘ฅ โˆˆ (๐‘‹[,]๐‘Œ) โ†ฆ ๐ด)โ€˜๐‘ง) โˆˆ (๐‘š(,)๐‘›) โ†” ((๐‘ฅ โˆˆ (๐‘‹[,]๐‘Œ) โ†ฆ ๐ด)โ€˜๐‘ฅ) โˆˆ (๐‘š(,)๐‘›)))
129125, 126, 128cbvralw 3288 . . . . . . . . . 10 (โˆ€๐‘ง โˆˆ (๐‘‹[,]๐‘Œ)((๐‘ฅ โˆˆ (๐‘‹[,]๐‘Œ) โ†ฆ ๐ด)โ€˜๐‘ง) โˆˆ (๐‘š(,)๐‘›) โ†” โˆ€๐‘ฅ โˆˆ (๐‘‹[,]๐‘Œ)((๐‘ฅ โˆˆ (๐‘‹[,]๐‘Œ) โ†ฆ ๐ด)โ€˜๐‘ฅ) โˆˆ (๐‘š(,)๐‘›))
130 simpr 486 . . . . . . . . . . . . 13 ((๐œ‘ โˆง ๐‘ฅ โˆˆ (๐‘‹[,]๐‘Œ)) โ†’ ๐‘ฅ โˆˆ (๐‘‹[,]๐‘Œ))
13114fvmptelcdm 7062 . . . . . . . . . . . . 13 ((๐œ‘ โˆง ๐‘ฅ โˆˆ (๐‘‹[,]๐‘Œ)) โ†’ ๐ด โˆˆ (๐‘(,)๐‘Š))
132 eqid 2733 . . . . . . . . . . . . . 14 (๐‘ฅ โˆˆ (๐‘‹[,]๐‘Œ) โ†ฆ ๐ด) = (๐‘ฅ โˆˆ (๐‘‹[,]๐‘Œ) โ†ฆ ๐ด)
133132fvmpt2 6960 . . . . . . . . . . . . 13 ((๐‘ฅ โˆˆ (๐‘‹[,]๐‘Œ) โˆง ๐ด โˆˆ (๐‘(,)๐‘Š)) โ†’ ((๐‘ฅ โˆˆ (๐‘‹[,]๐‘Œ) โ†ฆ ๐ด)โ€˜๐‘ฅ) = ๐ด)
134130, 131, 133syl2anc 585 . . . . . . . . . . . 12 ((๐œ‘ โˆง ๐‘ฅ โˆˆ (๐‘‹[,]๐‘Œ)) โ†’ ((๐‘ฅ โˆˆ (๐‘‹[,]๐‘Œ) โ†ฆ ๐ด)โ€˜๐‘ฅ) = ๐ด)
135134eleq1d 2819 . . . . . . . . . . 11 ((๐œ‘ โˆง ๐‘ฅ โˆˆ (๐‘‹[,]๐‘Œ)) โ†’ (((๐‘ฅ โˆˆ (๐‘‹[,]๐‘Œ) โ†ฆ ๐ด)โ€˜๐‘ฅ) โˆˆ (๐‘š(,)๐‘›) โ†” ๐ด โˆˆ (๐‘š(,)๐‘›)))
136135ralbidva 3169 . . . . . . . . . 10 (๐œ‘ โ†’ (โˆ€๐‘ฅ โˆˆ (๐‘‹[,]๐‘Œ)((๐‘ฅ โˆˆ (๐‘‹[,]๐‘Œ) โ†ฆ ๐ด)โ€˜๐‘ฅ) โˆˆ (๐‘š(,)๐‘›) โ†” โˆ€๐‘ฅ โˆˆ (๐‘‹[,]๐‘Œ)๐ด โˆˆ (๐‘š(,)๐‘›)))
137129, 136bitrid 283 . . . . . . . . 9 (๐œ‘ โ†’ (โˆ€๐‘ง โˆˆ (๐‘‹[,]๐‘Œ)((๐‘ฅ โˆˆ (๐‘‹[,]๐‘Œ) โ†ฆ ๐ด)โ€˜๐‘ง) โˆˆ (๐‘š(,)๐‘›) โ†” โˆ€๐‘ฅ โˆˆ (๐‘‹[,]๐‘Œ)๐ด โˆˆ (๐‘š(,)๐‘›)))
138137adantr 482 . . . . . . . 8 ((๐œ‘ โˆง (๐‘š โˆˆ (๐‘(,)๐‘Š) โˆง ๐‘› โˆˆ (๐‘(,)๐‘Š))) โ†’ (โˆ€๐‘ง โˆˆ (๐‘‹[,]๐‘Œ)((๐‘ฅ โˆˆ (๐‘‹[,]๐‘Œ) โ†ฆ ๐ด)โ€˜๐‘ง) โˆˆ (๐‘š(,)๐‘›) โ†” โˆ€๐‘ฅ โˆˆ (๐‘‹[,]๐‘Œ)๐ด โˆˆ (๐‘š(,)๐‘›)))
1391adantr 482 . . . . . . . . . . 11 ((๐œ‘ โˆง ((๐‘š โˆˆ (๐‘(,)๐‘Š) โˆง ๐‘› โˆˆ (๐‘(,)๐‘Š)) โˆง โˆ€๐‘ฅ โˆˆ (๐‘‹[,]๐‘Œ)๐ด โˆˆ (๐‘š(,)๐‘›))) โ†’ ๐‘‹ โˆˆ โ„)
1402adantr 482 . . . . . . . . . . 11 ((๐œ‘ โˆง ((๐‘š โˆˆ (๐‘(,)๐‘Š) โˆง ๐‘› โˆˆ (๐‘(,)๐‘Š)) โˆง โˆ€๐‘ฅ โˆˆ (๐‘‹[,]๐‘Œ)๐ด โˆˆ (๐‘š(,)๐‘›))) โ†’ ๐‘Œ โˆˆ โ„)
1413adantr 482 . . . . . . . . . . 11 ((๐œ‘ โˆง ((๐‘š โˆˆ (๐‘(,)๐‘Š) โˆง ๐‘› โˆˆ (๐‘(,)๐‘Š)) โˆง โˆ€๐‘ฅ โˆˆ (๐‘‹[,]๐‘Œ)๐ด โˆˆ (๐‘š(,)๐‘›))) โ†’ ๐‘‹ โ‰ค ๐‘Œ)
14228adantr 482 . . . . . . . . . . 11 ((๐œ‘ โˆง ((๐‘š โˆˆ (๐‘(,)๐‘Š) โˆง ๐‘› โˆˆ (๐‘(,)๐‘Š)) โˆง โˆ€๐‘ฅ โˆˆ (๐‘‹[,]๐‘Œ)๐ด โˆˆ (๐‘š(,)๐‘›))) โ†’ ๐‘ โˆˆ โ„*)
14319adantr 482 . . . . . . . . . . 11 ((๐œ‘ โˆง ((๐‘š โˆˆ (๐‘(,)๐‘Š) โˆง ๐‘› โˆˆ (๐‘(,)๐‘Š)) โˆง โˆ€๐‘ฅ โˆˆ (๐‘‹[,]๐‘Œ)๐ด โˆˆ (๐‘š(,)๐‘›))) โ†’ ๐‘Š โˆˆ โ„*)
144 nfcv 2904 . . . . . . . . . . . . . 14 โ„ฒ๐‘ฆ๐ด
145 nfcsb1v 3881 . . . . . . . . . . . . . 14 โ„ฒ๐‘ฅโฆ‹๐‘ฆ / ๐‘ฅโฆŒ๐ด
146 csbeq1a 3870 . . . . . . . . . . . . . 14 (๐‘ฅ = ๐‘ฆ โ†’ ๐ด = โฆ‹๐‘ฆ / ๐‘ฅโฆŒ๐ด)
147144, 145, 146cbvmpt 5217 . . . . . . . . . . . . 13 (๐‘ฅ โˆˆ (๐‘‹[,]๐‘Œ) โ†ฆ ๐ด) = (๐‘ฆ โˆˆ (๐‘‹[,]๐‘Œ) โ†ฆ โฆ‹๐‘ฆ / ๐‘ฅโฆŒ๐ด)
148147, 8eqeltrrid 2839 . . . . . . . . . . . 12 (๐œ‘ โ†’ (๐‘ฆ โˆˆ (๐‘‹[,]๐‘Œ) โ†ฆ โฆ‹๐‘ฆ / ๐‘ฅโฆŒ๐ด) โˆˆ ((๐‘‹[,]๐‘Œ)โ€“cnโ†’(๐‘(,)๐‘Š)))
149148adantr 482 . . . . . . . . . . 11 ((๐œ‘ โˆง ((๐‘š โˆˆ (๐‘(,)๐‘Š) โˆง ๐‘› โˆˆ (๐‘(,)๐‘Š)) โˆง โˆ€๐‘ฅ โˆˆ (๐‘‹[,]๐‘Œ)๐ด โˆˆ (๐‘š(,)๐‘›))) โ†’ (๐‘ฆ โˆˆ (๐‘‹[,]๐‘Œ) โ†ฆ โฆ‹๐‘ฆ / ๐‘ฅโฆŒ๐ด) โˆˆ ((๐‘‹[,]๐‘Œ)โ€“cnโ†’(๐‘(,)๐‘Š)))
150 nfcv 2904 . . . . . . . . . . . . . 14 โ„ฒ๐‘ฆ๐ต
151 nfcsb1v 3881 . . . . . . . . . . . . . 14 โ„ฒ๐‘ฅโฆ‹๐‘ฆ / ๐‘ฅโฆŒ๐ต
152 csbeq1a 3870 . . . . . . . . . . . . . 14 (๐‘ฅ = ๐‘ฆ โ†’ ๐ต = โฆ‹๐‘ฆ / ๐‘ฅโฆŒ๐ต)
153150, 151, 152cbvmpt 5217 . . . . . . . . . . . . 13 (๐‘ฅ โˆˆ (๐‘‹(,)๐‘Œ) โ†ฆ ๐ต) = (๐‘ฆ โˆˆ (๐‘‹(,)๐‘Œ) โ†ฆ โฆ‹๐‘ฆ / ๐‘ฅโฆŒ๐ต)
154 itgsubst.b . . . . . . . . . . . . 13 (๐œ‘ โ†’ (๐‘ฅ โˆˆ (๐‘‹(,)๐‘Œ) โ†ฆ ๐ต) โˆˆ (((๐‘‹(,)๐‘Œ)โ€“cnโ†’โ„‚) โˆฉ ๐ฟ1))
155153, 154eqeltrrid 2839 . . . . . . . . . . . 12 (๐œ‘ โ†’ (๐‘ฆ โˆˆ (๐‘‹(,)๐‘Œ) โ†ฆ โฆ‹๐‘ฆ / ๐‘ฅโฆŒ๐ต) โˆˆ (((๐‘‹(,)๐‘Œ)โ€“cnโ†’โ„‚) โˆฉ ๐ฟ1))
156155adantr 482 . . . . . . . . . . 11 ((๐œ‘ โˆง ((๐‘š โˆˆ (๐‘(,)๐‘Š) โˆง ๐‘› โˆˆ (๐‘(,)๐‘Š)) โˆง โˆ€๐‘ฅ โˆˆ (๐‘‹[,]๐‘Œ)๐ด โˆˆ (๐‘š(,)๐‘›))) โ†’ (๐‘ฆ โˆˆ (๐‘‹(,)๐‘Œ) โ†ฆ โฆ‹๐‘ฆ / ๐‘ฅโฆŒ๐ต) โˆˆ (((๐‘‹(,)๐‘Œ)โ€“cnโ†’โ„‚) โˆฉ ๐ฟ1))
157 nfcv 2904 . . . . . . . . . . . . . 14 โ„ฒ๐‘ฃ๐ถ
158 nfcsb1v 3881 . . . . . . . . . . . . . 14 โ„ฒ๐‘ขโฆ‹๐‘ฃ / ๐‘ขโฆŒ๐ถ
159 csbeq1a 3870 . . . . . . . . . . . . . 14 (๐‘ข = ๐‘ฃ โ†’ ๐ถ = โฆ‹๐‘ฃ / ๐‘ขโฆŒ๐ถ)
160157, 158, 159cbvmpt 5217 . . . . . . . . . . . . 13 (๐‘ข โˆˆ (๐‘(,)๐‘Š) โ†ฆ ๐ถ) = (๐‘ฃ โˆˆ (๐‘(,)๐‘Š) โ†ฆ โฆ‹๐‘ฃ / ๐‘ขโฆŒ๐ถ)
161 itgsubst.c . . . . . . . . . . . . 13 (๐œ‘ โ†’ (๐‘ข โˆˆ (๐‘(,)๐‘Š) โ†ฆ ๐ถ) โˆˆ ((๐‘(,)๐‘Š)โ€“cnโ†’โ„‚))
162160, 161eqeltrrid 2839 . . . . . . . . . . . 12 (๐œ‘ โ†’ (๐‘ฃ โˆˆ (๐‘(,)๐‘Š) โ†ฆ โฆ‹๐‘ฃ / ๐‘ขโฆŒ๐ถ) โˆˆ ((๐‘(,)๐‘Š)โ€“cnโ†’โ„‚))
163162adantr 482 . . . . . . . . . . 11 ((๐œ‘ โˆง ((๐‘š โˆˆ (๐‘(,)๐‘Š) โˆง ๐‘› โˆˆ (๐‘(,)๐‘Š)) โˆง โˆ€๐‘ฅ โˆˆ (๐‘‹[,]๐‘Œ)๐ด โˆˆ (๐‘š(,)๐‘›))) โ†’ (๐‘ฃ โˆˆ (๐‘(,)๐‘Š) โ†ฆ โฆ‹๐‘ฃ / ๐‘ขโฆŒ๐ถ) โˆˆ ((๐‘(,)๐‘Š)โ€“cnโ†’โ„‚))
164 itgsubst.da . . . . . . . . . . . . 13 (๐œ‘ โ†’ (โ„ D (๐‘ฅ โˆˆ (๐‘‹[,]๐‘Œ) โ†ฆ ๐ด)) = (๐‘ฅ โˆˆ (๐‘‹(,)๐‘Œ) โ†ฆ ๐ต))
165147oveq2i 7369 . . . . . . . . . . . . 13 (โ„ D (๐‘ฅ โˆˆ (๐‘‹[,]๐‘Œ) โ†ฆ ๐ด)) = (โ„ D (๐‘ฆ โˆˆ (๐‘‹[,]๐‘Œ) โ†ฆ โฆ‹๐‘ฆ / ๐‘ฅโฆŒ๐ด))
166164, 165, 1533eqtr3g 2796 . . . . . . . . . . . 12 (๐œ‘ โ†’ (โ„ D (๐‘ฆ โˆˆ (๐‘‹[,]๐‘Œ) โ†ฆ โฆ‹๐‘ฆ / ๐‘ฅโฆŒ๐ด)) = (๐‘ฆ โˆˆ (๐‘‹(,)๐‘Œ) โ†ฆ โฆ‹๐‘ฆ / ๐‘ฅโฆŒ๐ต))
167166adantr 482 . . . . . . . . . . 11 ((๐œ‘ โˆง ((๐‘š โˆˆ (๐‘(,)๐‘Š) โˆง ๐‘› โˆˆ (๐‘(,)๐‘Š)) โˆง โˆ€๐‘ฅ โˆˆ (๐‘‹[,]๐‘Œ)๐ด โˆˆ (๐‘š(,)๐‘›))) โ†’ (โ„ D (๐‘ฆ โˆˆ (๐‘‹[,]๐‘Œ) โ†ฆ โฆ‹๐‘ฆ / ๐‘ฅโฆŒ๐ด)) = (๐‘ฆ โˆˆ (๐‘‹(,)๐‘Œ) โ†ฆ โฆ‹๐‘ฆ / ๐‘ฅโฆŒ๐ต))
168 csbeq1 3859 . . . . . . . . . . 11 (๐‘ฃ = โฆ‹๐‘ฆ / ๐‘ฅโฆŒ๐ด โ†’ โฆ‹๐‘ฃ / ๐‘ขโฆŒ๐ถ = โฆ‹โฆ‹๐‘ฆ / ๐‘ฅโฆŒ๐ด / ๐‘ขโฆŒ๐ถ)
169 csbeq1 3859 . . . . . . . . . . 11 (๐‘ฆ = ๐‘‹ โ†’ โฆ‹๐‘ฆ / ๐‘ฅโฆŒ๐ด = โฆ‹๐‘‹ / ๐‘ฅโฆŒ๐ด)
170 csbeq1 3859 . . . . . . . . . . 11 (๐‘ฆ = ๐‘Œ โ†’ โฆ‹๐‘ฆ / ๐‘ฅโฆŒ๐ด = โฆ‹๐‘Œ / ๐‘ฅโฆŒ๐ด)
171 simprll 778 . . . . . . . . . . 11 ((๐œ‘ โˆง ((๐‘š โˆˆ (๐‘(,)๐‘Š) โˆง ๐‘› โˆˆ (๐‘(,)๐‘Š)) โˆง โˆ€๐‘ฅ โˆˆ (๐‘‹[,]๐‘Œ)๐ด โˆˆ (๐‘š(,)๐‘›))) โ†’ ๐‘š โˆˆ (๐‘(,)๐‘Š))
172 simprlr 779 . . . . . . . . . . 11 ((๐œ‘ โˆง ((๐‘š โˆˆ (๐‘(,)๐‘Š) โˆง ๐‘› โˆˆ (๐‘(,)๐‘Š)) โˆง โˆ€๐‘ฅ โˆˆ (๐‘‹[,]๐‘Œ)๐ด โˆˆ (๐‘š(,)๐‘›))) โ†’ ๐‘› โˆˆ (๐‘(,)๐‘Š))
173 simprr 772 . . . . . . . . . . . 12 ((๐œ‘ โˆง ((๐‘š โˆˆ (๐‘(,)๐‘Š) โˆง ๐‘› โˆˆ (๐‘(,)๐‘Š)) โˆง โˆ€๐‘ฅ โˆˆ (๐‘‹[,]๐‘Œ)๐ด โˆˆ (๐‘š(,)๐‘›))) โ†’ โˆ€๐‘ฅ โˆˆ (๐‘‹[,]๐‘Œ)๐ด โˆˆ (๐‘š(,)๐‘›))
174145nfel1 2920 . . . . . . . . . . . . 13 โ„ฒ๐‘ฅโฆ‹๐‘ฆ / ๐‘ฅโฆŒ๐ด โˆˆ (๐‘š(,)๐‘›)
175146eleq1d 2819 . . . . . . . . . . . . 13 (๐‘ฅ = ๐‘ฆ โ†’ (๐ด โˆˆ (๐‘š(,)๐‘›) โ†” โฆ‹๐‘ฆ / ๐‘ฅโฆŒ๐ด โˆˆ (๐‘š(,)๐‘›)))
176174, 175rspc 3568 . . . . . . . . . . . 12 (๐‘ฆ โˆˆ (๐‘‹[,]๐‘Œ) โ†’ (โˆ€๐‘ฅ โˆˆ (๐‘‹[,]๐‘Œ)๐ด โˆˆ (๐‘š(,)๐‘›) โ†’ โฆ‹๐‘ฆ / ๐‘ฅโฆŒ๐ด โˆˆ (๐‘š(,)๐‘›)))
177173, 176mpan9 508 . . . . . . . . . . 11 (((๐œ‘ โˆง ((๐‘š โˆˆ (๐‘(,)๐‘Š) โˆง ๐‘› โˆˆ (๐‘(,)๐‘Š)) โˆง โˆ€๐‘ฅ โˆˆ (๐‘‹[,]๐‘Œ)๐ด โˆˆ (๐‘š(,)๐‘›))) โˆง ๐‘ฆ โˆˆ (๐‘‹[,]๐‘Œ)) โ†’ โฆ‹๐‘ฆ / ๐‘ฅโฆŒ๐ด โˆˆ (๐‘š(,)๐‘›))
178139, 140, 141, 142, 143, 149, 156, 163, 167, 168, 169, 170, 171, 172, 177itgsubstlem 25428 . . . . . . . . . 10 ((๐œ‘ โˆง ((๐‘š โˆˆ (๐‘(,)๐‘Š) โˆง ๐‘› โˆˆ (๐‘(,)๐‘Š)) โˆง โˆ€๐‘ฅ โˆˆ (๐‘‹[,]๐‘Œ)๐ด โˆˆ (๐‘š(,)๐‘›))) โ†’ โจœ[โฆ‹๐‘‹ / ๐‘ฅโฆŒ๐ด โ†’ โฆ‹๐‘Œ / ๐‘ฅโฆŒ๐ด]โฆ‹๐‘ฃ / ๐‘ขโฆŒ๐ถ d๐‘ฃ = โจœ[๐‘‹ โ†’ ๐‘Œ](โฆ‹โฆ‹๐‘ฆ / ๐‘ฅโฆŒ๐ด / ๐‘ขโฆŒ๐ถ ยท โฆ‹๐‘ฆ / ๐‘ฅโฆŒ๐ต) d๐‘ฆ)
179159, 157, 158cbvditg 25234 . . . . . . . . . . . 12 โจœ[โฆ‹๐‘‹ / ๐‘ฅโฆŒ๐ด โ†’ โฆ‹๐‘Œ / ๐‘ฅโฆŒ๐ด]๐ถ d๐‘ข = โจœ[โฆ‹๐‘‹ / ๐‘ฅโฆŒ๐ด โ†’ โฆ‹๐‘Œ / ๐‘ฅโฆŒ๐ด]โฆ‹๐‘ฃ / ๐‘ขโฆŒ๐ถ d๐‘ฃ
180 nfcvd 2905 . . . . . . . . . . . . . . 15 (๐‘‹ โˆˆ โ„ โ†’ โ„ฒ๐‘ฅ๐พ)
181 itgsubst.k . . . . . . . . . . . . . . 15 (๐‘ฅ = ๐‘‹ โ†’ ๐ด = ๐พ)
182180, 181csbiegf 3890 . . . . . . . . . . . . . 14 (๐‘‹ โˆˆ โ„ โ†’ โฆ‹๐‘‹ / ๐‘ฅโฆŒ๐ด = ๐พ)
183 ditgeq1 25228 . . . . . . . . . . . . . 14 (โฆ‹๐‘‹ / ๐‘ฅโฆŒ๐ด = ๐พ โ†’ โจœ[โฆ‹๐‘‹ / ๐‘ฅโฆŒ๐ด โ†’ โฆ‹๐‘Œ / ๐‘ฅโฆŒ๐ด]๐ถ d๐‘ข = โจœ[๐พ โ†’ โฆ‹๐‘Œ / ๐‘ฅโฆŒ๐ด]๐ถ d๐‘ข)
1841, 182, 1833syl 18 . . . . . . . . . . . . 13 (๐œ‘ โ†’ โจœ[โฆ‹๐‘‹ / ๐‘ฅโฆŒ๐ด โ†’ โฆ‹๐‘Œ / ๐‘ฅโฆŒ๐ด]๐ถ d๐‘ข = โจœ[๐พ โ†’ โฆ‹๐‘Œ / ๐‘ฅโฆŒ๐ด]๐ถ d๐‘ข)
185 nfcvd 2905 . . . . . . . . . . . . . . 15 (๐‘Œ โˆˆ โ„ โ†’ โ„ฒ๐‘ฅ๐ฟ)
186 itgsubst.l . . . . . . . . . . . . . . 15 (๐‘ฅ = ๐‘Œ โ†’ ๐ด = ๐ฟ)
187185, 186csbiegf 3890 . . . . . . . . . . . . . 14 (๐‘Œ โˆˆ โ„ โ†’ โฆ‹๐‘Œ / ๐‘ฅโฆŒ๐ด = ๐ฟ)
188 ditgeq2 25229 . . . . . . . . . . . . . 14 (โฆ‹๐‘Œ / ๐‘ฅโฆŒ๐ด = ๐ฟ โ†’ โจœ[๐พ โ†’ โฆ‹๐‘Œ / ๐‘ฅโฆŒ๐ด]๐ถ d๐‘ข = โจœ[๐พ โ†’ ๐ฟ]๐ถ d๐‘ข)
1892, 187, 1883syl 18 . . . . . . . . . . . . 13 (๐œ‘ โ†’ โจœ[๐พ โ†’ โฆ‹๐‘Œ / ๐‘ฅโฆŒ๐ด]๐ถ d๐‘ข = โจœ[๐พ โ†’ ๐ฟ]๐ถ d๐‘ข)
190184, 189eqtrd 2773 . . . . . . . . . . . 12 (๐œ‘ โ†’ โจœ[โฆ‹๐‘‹ / ๐‘ฅโฆŒ๐ด โ†’ โฆ‹๐‘Œ / ๐‘ฅโฆŒ๐ด]๐ถ d๐‘ข = โจœ[๐พ โ†’ ๐ฟ]๐ถ d๐‘ข)
191179, 190eqtr3id 2787 . . . . . . . . . . 11 (๐œ‘ โ†’ โจœ[โฆ‹๐‘‹ / ๐‘ฅโฆŒ๐ด โ†’ โฆ‹๐‘Œ / ๐‘ฅโฆŒ๐ด]โฆ‹๐‘ฃ / ๐‘ขโฆŒ๐ถ d๐‘ฃ = โจœ[๐พ โ†’ ๐ฟ]๐ถ d๐‘ข)
192191adantr 482 . . . . . . . . . 10 ((๐œ‘ โˆง ((๐‘š โˆˆ (๐‘(,)๐‘Š) โˆง ๐‘› โˆˆ (๐‘(,)๐‘Š)) โˆง โˆ€๐‘ฅ โˆˆ (๐‘‹[,]๐‘Œ)๐ด โˆˆ (๐‘š(,)๐‘›))) โ†’ โจœ[โฆ‹๐‘‹ / ๐‘ฅโฆŒ๐ด โ†’ โฆ‹๐‘Œ / ๐‘ฅโฆŒ๐ด]โฆ‹๐‘ฃ / ๐‘ขโฆŒ๐ถ d๐‘ฃ = โจœ[๐พ โ†’ ๐ฟ]๐ถ d๐‘ข)
193146csbeq1d 3860 . . . . . . . . . . . . . 14 (๐‘ฅ = ๐‘ฆ โ†’ โฆ‹๐ด / ๐‘ขโฆŒ๐ถ = โฆ‹โฆ‹๐‘ฆ / ๐‘ฅโฆŒ๐ด / ๐‘ขโฆŒ๐ถ)
194193, 152oveq12d 7376 . . . . . . . . . . . . 13 (๐‘ฅ = ๐‘ฆ โ†’ (โฆ‹๐ด / ๐‘ขโฆŒ๐ถ ยท ๐ต) = (โฆ‹โฆ‹๐‘ฆ / ๐‘ฅโฆŒ๐ด / ๐‘ขโฆŒ๐ถ ยท โฆ‹๐‘ฆ / ๐‘ฅโฆŒ๐ต))
195 nfcv 2904 . . . . . . . . . . . . 13 โ„ฒ๐‘ฆ(โฆ‹๐ด / ๐‘ขโฆŒ๐ถ ยท ๐ต)
196 nfcv 2904 . . . . . . . . . . . . . . 15 โ„ฒ๐‘ฅ๐ถ
197145, 196nfcsbw 3883 . . . . . . . . . . . . . 14 โ„ฒ๐‘ฅโฆ‹โฆ‹๐‘ฆ / ๐‘ฅโฆŒ๐ด / ๐‘ขโฆŒ๐ถ
198 nfcv 2904 . . . . . . . . . . . . . 14 โ„ฒ๐‘ฅ ยท
199197, 198, 151nfov 7388 . . . . . . . . . . . . 13 โ„ฒ๐‘ฅ(โฆ‹โฆ‹๐‘ฆ / ๐‘ฅโฆŒ๐ด / ๐‘ขโฆŒ๐ถ ยท โฆ‹๐‘ฆ / ๐‘ฅโฆŒ๐ต)
200194, 195, 199cbvditg 25234 . . . . . . . . . . . 12 โจœ[๐‘‹ โ†’ ๐‘Œ](โฆ‹๐ด / ๐‘ขโฆŒ๐ถ ยท ๐ต) d๐‘ฅ = โจœ[๐‘‹ โ†’ ๐‘Œ](โฆ‹โฆ‹๐‘ฆ / ๐‘ฅโฆŒ๐ด / ๐‘ขโฆŒ๐ถ ยท โฆ‹๐‘ฆ / ๐‘ฅโฆŒ๐ต) d๐‘ฆ
201 ioossicc 13356 . . . . . . . . . . . . . . . . . 18 (๐‘‹(,)๐‘Œ) โŠ† (๐‘‹[,]๐‘Œ)
202201sseli 3941 . . . . . . . . . . . . . . . . 17 (๐‘ฅ โˆˆ (๐‘‹(,)๐‘Œ) โ†’ ๐‘ฅ โˆˆ (๐‘‹[,]๐‘Œ))
203202, 131sylan2 594 . . . . . . . . . . . . . . . 16 ((๐œ‘ โˆง ๐‘ฅ โˆˆ (๐‘‹(,)๐‘Œ)) โ†’ ๐ด โˆˆ (๐‘(,)๐‘Š))
204 nfcvd 2905 . . . . . . . . . . . . . . . . 17 (๐ด โˆˆ (๐‘(,)๐‘Š) โ†’ โ„ฒ๐‘ข๐ธ)
205 itgsubst.e . . . . . . . . . . . . . . . . 17 (๐‘ข = ๐ด โ†’ ๐ถ = ๐ธ)
206204, 205csbiegf 3890 . . . . . . . . . . . . . . . 16 (๐ด โˆˆ (๐‘(,)๐‘Š) โ†’ โฆ‹๐ด / ๐‘ขโฆŒ๐ถ = ๐ธ)
207203, 206syl 17 . . . . . . . . . . . . . . 15 ((๐œ‘ โˆง ๐‘ฅ โˆˆ (๐‘‹(,)๐‘Œ)) โ†’ โฆ‹๐ด / ๐‘ขโฆŒ๐ถ = ๐ธ)
208207oveq1d 7373 . . . . . . . . . . . . . 14 ((๐œ‘ โˆง ๐‘ฅ โˆˆ (๐‘‹(,)๐‘Œ)) โ†’ (โฆ‹๐ด / ๐‘ขโฆŒ๐ถ ยท ๐ต) = (๐ธ ยท ๐ต))
209208itgeq2dv 25162 . . . . . . . . . . . . 13 (๐œ‘ โ†’ โˆซ(๐‘‹(,)๐‘Œ)(โฆ‹๐ด / ๐‘ขโฆŒ๐ถ ยท ๐ต) d๐‘ฅ = โˆซ(๐‘‹(,)๐‘Œ)(๐ธ ยท ๐ต) d๐‘ฅ)
2103ditgpos 25236 . . . . . . . . . . . . 13 (๐œ‘ โ†’ โจœ[๐‘‹ โ†’ ๐‘Œ](โฆ‹๐ด / ๐‘ขโฆŒ๐ถ ยท ๐ต) d๐‘ฅ = โˆซ(๐‘‹(,)๐‘Œ)(โฆ‹๐ด / ๐‘ขโฆŒ๐ถ ยท ๐ต) d๐‘ฅ)
2113ditgpos 25236 . . . . . . . . . . . . 13 (๐œ‘ โ†’ โจœ[๐‘‹ โ†’ ๐‘Œ](๐ธ ยท ๐ต) d๐‘ฅ = โˆซ(๐‘‹(,)๐‘Œ)(๐ธ ยท ๐ต) d๐‘ฅ)
212209, 210, 2113eqtr4d 2783 . . . . . . . . . . . 12 (๐œ‘ โ†’ โจœ[๐‘‹ โ†’ ๐‘Œ](โฆ‹๐ด / ๐‘ขโฆŒ๐ถ ยท ๐ต) d๐‘ฅ = โจœ[๐‘‹ โ†’ ๐‘Œ](๐ธ ยท ๐ต) d๐‘ฅ)
213200, 212eqtr3id 2787 . . . . . . . . . . 11 (๐œ‘ โ†’ โจœ[๐‘‹ โ†’ ๐‘Œ](โฆ‹โฆ‹๐‘ฆ / ๐‘ฅโฆŒ๐ด / ๐‘ขโฆŒ๐ถ ยท โฆ‹๐‘ฆ / ๐‘ฅโฆŒ๐ต) d๐‘ฆ = โจœ[๐‘‹ โ†’ ๐‘Œ](๐ธ ยท ๐ต) d๐‘ฅ)
214213adantr 482 . . . . . . . . . 10 ((๐œ‘ โˆง ((๐‘š โˆˆ (๐‘(,)๐‘Š) โˆง ๐‘› โˆˆ (๐‘(,)๐‘Š)) โˆง โˆ€๐‘ฅ โˆˆ (๐‘‹[,]๐‘Œ)๐ด โˆˆ (๐‘š(,)๐‘›))) โ†’ โจœ[๐‘‹ โ†’ ๐‘Œ](โฆ‹โฆ‹๐‘ฆ / ๐‘ฅโฆŒ๐ด / ๐‘ขโฆŒ๐ถ ยท โฆ‹๐‘ฆ / ๐‘ฅโฆŒ๐ต) d๐‘ฆ = โจœ[๐‘‹ โ†’ ๐‘Œ](๐ธ ยท ๐ต) d๐‘ฅ)
215178, 192, 2143eqtr3d 2781 . . . . . . . . 9 ((๐œ‘ โˆง ((๐‘š โˆˆ (๐‘(,)๐‘Š) โˆง ๐‘› โˆˆ (๐‘(,)๐‘Š)) โˆง โˆ€๐‘ฅ โˆˆ (๐‘‹[,]๐‘Œ)๐ด โˆˆ (๐‘š(,)๐‘›))) โ†’ โจœ[๐พ โ†’ ๐ฟ]๐ถ d๐‘ข = โจœ[๐‘‹ โ†’ ๐‘Œ](๐ธ ยท ๐ต) d๐‘ฅ)
216215expr 458 . . . . . . . 8 ((๐œ‘ โˆง (๐‘š โˆˆ (๐‘(,)๐‘Š) โˆง ๐‘› โˆˆ (๐‘(,)๐‘Š))) โ†’ (โˆ€๐‘ฅ โˆˆ (๐‘‹[,]๐‘Œ)๐ด โˆˆ (๐‘š(,)๐‘›) โ†’ โจœ[๐พ โ†’ ๐ฟ]๐ถ d๐‘ข = โจœ[๐‘‹ โ†’ ๐‘Œ](๐ธ ยท ๐ต) d๐‘ฅ))
217138, 216sylbid 239 . . . . . . 7 ((๐œ‘ โˆง (๐‘š โˆˆ (๐‘(,)๐‘Š) โˆง ๐‘› โˆˆ (๐‘(,)๐‘Š))) โ†’ (โˆ€๐‘ง โˆˆ (๐‘‹[,]๐‘Œ)((๐‘ฅ โˆˆ (๐‘‹[,]๐‘Œ) โ†ฆ ๐ด)โ€˜๐‘ง) โˆˆ (๐‘š(,)๐‘›) โ†’ โจœ[๐พ โ†’ ๐ฟ]๐ถ d๐‘ข = โจœ[๐‘‹ โ†’ ๐‘Œ](๐ธ ยท ๐ต) d๐‘ฅ))
218123, 217sylbid 239 . . . . . 6 ((๐œ‘ โˆง (๐‘š โˆˆ (๐‘(,)๐‘Š) โˆง ๐‘› โˆˆ (๐‘(,)๐‘Š))) โ†’ (โˆ€๐‘ง โˆˆ (๐‘‹[,]๐‘Œ)(๐‘š < ((๐‘ฅ โˆˆ (๐‘‹[,]๐‘Œ) โ†ฆ ๐ด)โ€˜๐‘ง) โˆง ((๐‘ฅ โˆˆ (๐‘‹[,]๐‘Œ) โ†ฆ ๐ด)โ€˜๐‘ง) < ๐‘›) โ†’ โจœ[๐พ โ†’ ๐ฟ]๐ถ d๐‘ข = โจœ[๐‘‹ โ†’ ๐‘Œ](๐ธ ยท ๐ต) d๐‘ฅ))
219111, 218biimtrrid 242 . . . . 5 ((๐œ‘ โˆง (๐‘š โˆˆ (๐‘(,)๐‘Š) โˆง ๐‘› โˆˆ (๐‘(,)๐‘Š))) โ†’ ((โˆ€๐‘ง โˆˆ (๐‘‹[,]๐‘Œ)๐‘š < ((๐‘ฅ โˆˆ (๐‘‹[,]๐‘Œ) โ†ฆ ๐ด)โ€˜๐‘ง) โˆง โˆ€๐‘ง โˆˆ (๐‘‹[,]๐‘Œ)((๐‘ฅ โˆˆ (๐‘‹[,]๐‘Œ) โ†ฆ ๐ด)โ€˜๐‘ง) < ๐‘›) โ†’ โจœ[๐พ โ†’ ๐ฟ]๐ถ d๐‘ข = โจœ[๐‘‹ โ†’ ๐‘Œ](๐ธ ยท ๐ต) d๐‘ฅ))
220219rexlimdvva 3202 . . . 4 (๐œ‘ โ†’ (โˆƒ๐‘š โˆˆ (๐‘(,)๐‘Š)โˆƒ๐‘› โˆˆ (๐‘(,)๐‘Š)(โˆ€๐‘ง โˆˆ (๐‘‹[,]๐‘Œ)๐‘š < ((๐‘ฅ โˆˆ (๐‘‹[,]๐‘Œ) โ†ฆ ๐ด)โ€˜๐‘ง) โˆง โˆ€๐‘ง โˆˆ (๐‘‹[,]๐‘Œ)((๐‘ฅ โˆˆ (๐‘‹[,]๐‘Œ) โ†ฆ ๐ด)โ€˜๐‘ง) < ๐‘›) โ†’ โจœ[๐พ โ†’ ๐ฟ]๐ถ d๐‘ข = โจœ[๐‘‹ โ†’ ๐‘Œ](๐ธ ยท ๐ต) d๐‘ฅ))
221110, 220biimtrid 241 . . 3 (๐œ‘ โ†’ ((โˆƒ๐‘› โˆˆ (๐‘(,)๐‘Š)โˆ€๐‘ง โˆˆ (๐‘‹[,]๐‘Œ)((๐‘ฅ โˆˆ (๐‘‹[,]๐‘Œ) โ†ฆ ๐ด)โ€˜๐‘ง) < ๐‘› โˆง โˆƒ๐‘š โˆˆ (๐‘(,)๐‘Š)โˆ€๐‘ง โˆˆ (๐‘‹[,]๐‘Œ)๐‘š < ((๐‘ฅ โˆˆ (๐‘‹[,]๐‘Œ) โ†ฆ ๐ด)โ€˜๐‘ง)) โ†’ โจœ[๐พ โ†’ ๐ฟ]๐ถ d๐‘ข = โจœ[๐‘‹ โ†’ ๐‘Œ](๐ธ ยท ๐ต) d๐‘ฅ))
22262, 107, 221syl2and 609 . 2 (๐œ‘ โ†’ ((โˆƒ๐‘ฆ โˆˆ (๐‘‹[,]๐‘Œ)โˆ€๐‘ง โˆˆ (๐‘‹[,]๐‘Œ)((๐‘ฅ โˆˆ (๐‘‹[,]๐‘Œ) โ†ฆ ๐ด)โ€˜๐‘ง) โ‰ค ((๐‘ฅ โˆˆ (๐‘‹[,]๐‘Œ) โ†ฆ ๐ด)โ€˜๐‘ฆ) โˆง โˆƒ๐‘ฆ โˆˆ (๐‘‹[,]๐‘Œ)โˆ€๐‘ง โˆˆ (๐‘‹[,]๐‘Œ)((๐‘ฅ โˆˆ (๐‘‹[,]๐‘Œ) โ†ฆ ๐ด)โ€˜๐‘ฆ) โ‰ค ((๐‘ฅ โˆˆ (๐‘‹[,]๐‘Œ) โ†ฆ ๐ด)โ€˜๐‘ง)) โ†’ โจœ[๐พ โ†’ ๐ฟ]๐ถ d๐‘ข = โจœ[๐‘‹ โ†’ ๐‘Œ](๐ธ ยท ๐ต) d๐‘ฅ))
22310, 222mpd 15 1 (๐œ‘ โ†’ โจœ[๐พ โ†’ ๐ฟ]๐ถ d๐‘ข = โจœ[๐‘‹ โ†’ ๐‘Œ](๐ธ ยท ๐ต) d๐‘ฅ)
Colors of variables: wff setvar class
Syntax hints:   โ†’ wi 4   โ†” wb 205   โˆง wa 397   โˆง w3a 1088   = wceq 1542   โˆˆ wcel 2107  โˆ€wral 3061  โˆƒwrex 3070  โฆ‹csb 3856   โˆฉ cin 3910   โŠ† wss 3911   class class class wbr 5106   โ†ฆ cmpt 5189  โŸถwf 6493  โ€˜cfv 6497  (class class class)co 7358  โ„‚cc 11054  โ„cr 11055   ยท cmul 11061  โ„*cxr 11193   < clt 11194   โ‰ค cle 11195  โ„šcq 12878  (,)cioo 13270  [,]cicc 13273  โ€“cnโ†’ccncf 24255  ๐ฟ1cibl 24997  โˆซcitg 24998  โจœcdit 25226   D cdv 25243
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1798  ax-4 1812  ax-5 1914  ax-6 1972  ax-7 2012  ax-8 2109  ax-9 2117  ax-10 2138  ax-11 2155  ax-12 2172  ax-ext 2704  ax-rep 5243  ax-sep 5257  ax-nul 5264  ax-pow 5321  ax-pr 5385  ax-un 7673  ax-inf2 9582  ax-cc 10376  ax-cnex 11112  ax-resscn 11113  ax-1cn 11114  ax-icn 11115  ax-addcl 11116  ax-addrcl 11117  ax-mulcl 11118  ax-mulrcl 11119  ax-mulcom 11120  ax-addass 11121  ax-mulass 11122  ax-distr 11123  ax-i2m1 11124  ax-1ne0 11125  ax-1rid 11126  ax-rnegex 11127  ax-rrecex 11128  ax-cnre 11129  ax-pre-lttri 11130  ax-pre-lttrn 11131  ax-pre-ltadd 11132  ax-pre-mulgt0 11133  ax-pre-sup 11134  ax-addf 11135  ax-mulf 11136
This theorem depends on definitions:  df-bi 206  df-an 398  df-or 847  df-3or 1089  df-3an 1090  df-tru 1545  df-fal 1555  df-ex 1783  df-nf 1787  df-sb 2069  df-mo 2535  df-eu 2564  df-clab 2711  df-cleq 2725  df-clel 2811  df-nfc 2886  df-ne 2941  df-nel 3047  df-ral 3062  df-rex 3071  df-rmo 3352  df-reu 3353  df-rab 3407  df-v 3446  df-sbc 3741  df-csb 3857  df-dif 3914  df-un 3916  df-in 3918  df-ss 3928  df-pss 3930  df-symdif 4203  df-nul 4284  df-if 4488  df-pw 4563  df-sn 4588  df-pr 4590  df-tp 4592  df-op 4594  df-uni 4867  df-int 4909  df-iun 4957  df-iin 4958  df-disj 5072  df-br 5107  df-opab 5169  df-mpt 5190  df-tr 5224  df-id 5532  df-eprel 5538  df-po 5546  df-so 5547  df-fr 5589  df-se 5590  df-we 5591  df-xp 5640  df-rel 5641  df-cnv 5642  df-co 5643  df-dm 5644  df-rn 5645  df-res 5646  df-ima 5647  df-pred 6254  df-ord 6321  df-on 6322  df-lim 6323  df-suc 6324  df-iota 6449  df-fun 6499  df-fn 6500  df-f 6501  df-f1 6502  df-fo 6503  df-f1o 6504  df-fv 6505  df-isom 6506  df-riota 7314  df-ov 7361  df-oprab 7362  df-mpo 7363  df-of 7618  df-ofr 7619  df-om 7804  df-1st 7922  df-2nd 7923  df-supp 8094  df-frecs 8213  df-wrecs 8244  df-recs 8318  df-rdg 8357  df-1o 8413  df-2o 8414  df-oadd 8417  df-omul 8418  df-er 8651  df-map 8770  df-pm 8771  df-ixp 8839  df-en 8887  df-dom 8888  df-sdom 8889  df-fin 8890  df-fsupp 9309  df-fi 9352  df-sup 9383  df-inf 9384  df-oi 9451  df-dju 9842  df-card 9880  df-acn 9883  df-pnf 11196  df-mnf 11197  df-xr 11198  df-ltxr 11199  df-le 11200  df-sub 11392  df-neg 11393  df-div 11818  df-nn 12159  df-2 12221  df-3 12222  df-4 12223  df-5 12224  df-6 12225  df-7 12226  df-8 12227  df-9 12228  df-n0 12419  df-z 12505  df-dec 12624  df-uz 12769  df-q 12879  df-rp 12921  df-xneg 13038  df-xadd 13039  df-xmul 13040  df-ioo 13274  df-ioc 13275  df-ico 13276  df-icc 13277  df-fz 13431  df-fzo 13574  df-fl 13703  df-mod 13781  df-seq 13913  df-exp 13974  df-hash 14237  df-cj 14990  df-re 14991  df-im 14992  df-sqrt 15126  df-abs 15127  df-limsup 15359  df-clim 15376  df-rlim 15377  df-sum 15577  df-struct 17024  df-sets 17041  df-slot 17059  df-ndx 17071  df-base 17089  df-ress 17118  df-plusg 17151  df-mulr 17152  df-starv 17153  df-sca 17154  df-vsca 17155  df-ip 17156  df-tset 17157  df-ple 17158  df-ds 17160  df-unif 17161  df-hom 17162  df-cco 17163  df-rest 17309  df-topn 17310  df-0g 17328  df-gsum 17329  df-topgen 17330  df-pt 17331  df-prds 17334  df-xrs 17389  df-qtop 17394  df-imas 17395  df-xps 17397  df-mre 17471  df-mrc 17472  df-acs 17474  df-mgm 18502  df-sgrp 18551  df-mnd 18562  df-submnd 18607  df-mulg 18878  df-cntz 19102  df-cmn 19569  df-psmet 20804  df-xmet 20805  df-met 20806  df-bl 20807  df-mopn 20808  df-fbas 20809  df-fg 20810  df-cnfld 20813  df-top 22259  df-topon 22276  df-topsp 22298  df-bases 22312  df-cld 22386  df-ntr 22387  df-cls 22388  df-nei 22465  df-lp 22503  df-perf 22504  df-cn 22594  df-cnp 22595  df-haus 22682  df-cmp 22754  df-tx 22929  df-hmeo 23122  df-fil 23213  df-fm 23305  df-flim 23306  df-flf 23307  df-xms 23689  df-ms 23690  df-tms 23691  df-cncf 24257  df-ovol 24844  df-vol 24845  df-mbf 24999  df-itg1 25000  df-itg2 25001  df-ibl 25002  df-itg 25003  df-0p 25050  df-ditg 25227  df-limc 25246  df-dv 25247
This theorem is referenced by:  itgsubsticclem  44302
  Copyright terms: Public domain W3C validator