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

Theorem uniioombllem6 24968
Description: Lemma for uniioombl 24969. (Contributed by Mario Carneiro, 26-Mar-2015.)
Hypotheses
Ref Expression
uniioombl.1 (๐œ‘ โ†’ ๐น:โ„•โŸถ( โ‰ค โˆฉ (โ„ ร— โ„)))
uniioombl.2 (๐œ‘ โ†’ Disj ๐‘ฅ โˆˆ โ„• ((,)โ€˜(๐นโ€˜๐‘ฅ)))
uniioombl.3 ๐‘† = seq1( + , ((abs โˆ˜ โˆ’ ) โˆ˜ ๐น))
uniioombl.a ๐ด = โˆช ran ((,) โˆ˜ ๐น)
uniioombl.e (๐œ‘ โ†’ (vol*โ€˜๐ธ) โˆˆ โ„)
uniioombl.c (๐œ‘ โ†’ ๐ถ โˆˆ โ„+)
uniioombl.g (๐œ‘ โ†’ ๐บ:โ„•โŸถ( โ‰ค โˆฉ (โ„ ร— โ„)))
uniioombl.s (๐œ‘ โ†’ ๐ธ โŠ† โˆช ran ((,) โˆ˜ ๐บ))
uniioombl.t ๐‘‡ = seq1( + , ((abs โˆ˜ โˆ’ ) โˆ˜ ๐บ))
uniioombl.v (๐œ‘ โ†’ sup(ran ๐‘‡, โ„*, < ) โ‰ค ((vol*โ€˜๐ธ) + ๐ถ))
Assertion
Ref Expression
uniioombllem6 (๐œ‘ โ†’ ((vol*โ€˜(๐ธ โˆฉ ๐ด)) + (vol*โ€˜(๐ธ โˆ– ๐ด))) โ‰ค ((vol*โ€˜๐ธ) + (4 ยท ๐ถ)))
Distinct variable groups:   ๐‘ฅ,๐น   ๐‘ฅ,๐บ   ๐‘ฅ,๐ด   ๐‘ฅ,๐ถ   ๐œ‘,๐‘ฅ   ๐‘ฅ,๐‘‡
Allowed substitution hints:   ๐‘†(๐‘ฅ)   ๐ธ(๐‘ฅ)

Proof of Theorem uniioombllem6
Dummy variables ๐‘Ž ๐‘– ๐‘— ๐‘˜ ๐‘› ๐‘ฆ ๐‘ง ๐‘š are mutually distinct and distinct from all other variables.
StepHypRef Expression
1 nnuz 12811 . . . 4 โ„• = (โ„คโ‰ฅโ€˜1)
2 1zzd 12539 . . . 4 (๐œ‘ โ†’ 1 โˆˆ โ„ค)
3 uniioombl.c . . . 4 (๐œ‘ โ†’ ๐ถ โˆˆ โ„+)
4 eqidd 2734 . . . 4 ((๐œ‘ โˆง ๐‘š โˆˆ โ„•) โ†’ (๐‘‡โ€˜๐‘š) = (๐‘‡โ€˜๐‘š))
5 uniioombl.t . . . . . 6 ๐‘‡ = seq1( + , ((abs โˆ˜ โˆ’ ) โˆ˜ ๐บ))
6 eqidd 2734 . . . . . 6 ((๐œ‘ โˆง ๐‘Ž โˆˆ โ„•) โ†’ (((abs โˆ˜ โˆ’ ) โˆ˜ ๐บ)โ€˜๐‘Ž) = (((abs โˆ˜ โˆ’ ) โˆ˜ ๐บ)โ€˜๐‘Ž))
7 uniioombl.g . . . . . . . . . 10 (๐œ‘ โ†’ ๐บ:โ„•โŸถ( โ‰ค โˆฉ (โ„ ร— โ„)))
8 eqid 2733 . . . . . . . . . . 11 ((abs โˆ˜ โˆ’ ) โˆ˜ ๐บ) = ((abs โˆ˜ โˆ’ ) โˆ˜ ๐บ)
98ovolfsf 24851 . . . . . . . . . 10 (๐บ:โ„•โŸถ( โ‰ค โˆฉ (โ„ ร— โ„)) โ†’ ((abs โˆ˜ โˆ’ ) โˆ˜ ๐บ):โ„•โŸถ(0[,)+โˆž))
107, 9syl 17 . . . . . . . . 9 (๐œ‘ โ†’ ((abs โˆ˜ โˆ’ ) โˆ˜ ๐บ):โ„•โŸถ(0[,)+โˆž))
1110ffvelcdmda 7036 . . . . . . . 8 ((๐œ‘ โˆง ๐‘Ž โˆˆ โ„•) โ†’ (((abs โˆ˜ โˆ’ ) โˆ˜ ๐บ)โ€˜๐‘Ž) โˆˆ (0[,)+โˆž))
12 elrege0 13377 . . . . . . . 8 ((((abs โˆ˜ โˆ’ ) โˆ˜ ๐บ)โ€˜๐‘Ž) โˆˆ (0[,)+โˆž) โ†” ((((abs โˆ˜ โˆ’ ) โˆ˜ ๐บ)โ€˜๐‘Ž) โˆˆ โ„ โˆง 0 โ‰ค (((abs โˆ˜ โˆ’ ) โˆ˜ ๐บ)โ€˜๐‘Ž)))
1311, 12sylib 217 . . . . . . 7 ((๐œ‘ โˆง ๐‘Ž โˆˆ โ„•) โ†’ ((((abs โˆ˜ โˆ’ ) โˆ˜ ๐บ)โ€˜๐‘Ž) โˆˆ โ„ โˆง 0 โ‰ค (((abs โˆ˜ โˆ’ ) โˆ˜ ๐บ)โ€˜๐‘Ž)))
1413simpld 496 . . . . . 6 ((๐œ‘ โˆง ๐‘Ž โˆˆ โ„•) โ†’ (((abs โˆ˜ โˆ’ ) โˆ˜ ๐บ)โ€˜๐‘Ž) โˆˆ โ„)
1513simprd 497 . . . . . 6 ((๐œ‘ โˆง ๐‘Ž โˆˆ โ„•) โ†’ 0 โ‰ค (((abs โˆ˜ โˆ’ ) โˆ˜ ๐บ)โ€˜๐‘Ž))
16 uniioombl.1 . . . . . . . 8 (๐œ‘ โ†’ ๐น:โ„•โŸถ( โ‰ค โˆฉ (โ„ ร— โ„)))
17 uniioombl.2 . . . . . . . 8 (๐œ‘ โ†’ Disj ๐‘ฅ โˆˆ โ„• ((,)โ€˜(๐นโ€˜๐‘ฅ)))
18 uniioombl.3 . . . . . . . 8 ๐‘† = seq1( + , ((abs โˆ˜ โˆ’ ) โˆ˜ ๐น))
19 uniioombl.a . . . . . . . 8 ๐ด = โˆช ran ((,) โˆ˜ ๐น)
20 uniioombl.e . . . . . . . 8 (๐œ‘ โ†’ (vol*โ€˜๐ธ) โˆˆ โ„)
21 uniioombl.s . . . . . . . 8 (๐œ‘ โ†’ ๐ธ โŠ† โˆช ran ((,) โˆ˜ ๐บ))
22 uniioombl.v . . . . . . . 8 (๐œ‘ โ†’ sup(ran ๐‘‡, โ„*, < ) โ‰ค ((vol*โ€˜๐ธ) + ๐ถ))
2316, 17, 18, 19, 20, 3, 7, 21, 5, 22uniioombllem1 24961 . . . . . . 7 (๐œ‘ โ†’ sup(ran ๐‘‡, โ„*, < ) โˆˆ โ„)
248, 5ovolsf 24852 . . . . . . . . . . . . 13 (๐บ:โ„•โŸถ( โ‰ค โˆฉ (โ„ ร— โ„)) โ†’ ๐‘‡:โ„•โŸถ(0[,)+โˆž))
257, 24syl 17 . . . . . . . . . . . 12 (๐œ‘ โ†’ ๐‘‡:โ„•โŸถ(0[,)+โˆž))
2625frnd 6677 . . . . . . . . . . 11 (๐œ‘ โ†’ ran ๐‘‡ โŠ† (0[,)+โˆž))
27 icossxr 13355 . . . . . . . . . . 11 (0[,)+โˆž) โŠ† โ„*
2826, 27sstrdi 3957 . . . . . . . . . 10 (๐œ‘ โ†’ ran ๐‘‡ โŠ† โ„*)
29 supxrub 13249 . . . . . . . . . 10 ((ran ๐‘‡ โŠ† โ„* โˆง ๐‘ฅ โˆˆ ran ๐‘‡) โ†’ ๐‘ฅ โ‰ค sup(ran ๐‘‡, โ„*, < ))
3028, 29sylan 581 . . . . . . . . 9 ((๐œ‘ โˆง ๐‘ฅ โˆˆ ran ๐‘‡) โ†’ ๐‘ฅ โ‰ค sup(ran ๐‘‡, โ„*, < ))
3130ralrimiva 3140 . . . . . . . 8 (๐œ‘ โ†’ โˆ€๐‘ฅ โˆˆ ran ๐‘‡ ๐‘ฅ โ‰ค sup(ran ๐‘‡, โ„*, < ))
3225ffnd 6670 . . . . . . . . 9 (๐œ‘ โ†’ ๐‘‡ Fn โ„•)
33 breq1 5109 . . . . . . . . . 10 (๐‘ฅ = (๐‘‡โ€˜๐‘š) โ†’ (๐‘ฅ โ‰ค sup(ran ๐‘‡, โ„*, < ) โ†” (๐‘‡โ€˜๐‘š) โ‰ค sup(ran ๐‘‡, โ„*, < )))
3433ralrn 7039 . . . . . . . . 9 (๐‘‡ Fn โ„• โ†’ (โˆ€๐‘ฅ โˆˆ ran ๐‘‡ ๐‘ฅ โ‰ค sup(ran ๐‘‡, โ„*, < ) โ†” โˆ€๐‘š โˆˆ โ„• (๐‘‡โ€˜๐‘š) โ‰ค sup(ran ๐‘‡, โ„*, < )))
3532, 34syl 17 . . . . . . . 8 (๐œ‘ โ†’ (โˆ€๐‘ฅ โˆˆ ran ๐‘‡ ๐‘ฅ โ‰ค sup(ran ๐‘‡, โ„*, < ) โ†” โˆ€๐‘š โˆˆ โ„• (๐‘‡โ€˜๐‘š) โ‰ค sup(ran ๐‘‡, โ„*, < )))
3631, 35mpbid 231 . . . . . . 7 (๐œ‘ โ†’ โˆ€๐‘š โˆˆ โ„• (๐‘‡โ€˜๐‘š) โ‰ค sup(ran ๐‘‡, โ„*, < ))
37 brralrspcev 5166 . . . . . . 7 ((sup(ran ๐‘‡, โ„*, < ) โˆˆ โ„ โˆง โˆ€๐‘š โˆˆ โ„• (๐‘‡โ€˜๐‘š) โ‰ค sup(ran ๐‘‡, โ„*, < )) โ†’ โˆƒ๐‘ฅ โˆˆ โ„ โˆ€๐‘š โˆˆ โ„• (๐‘‡โ€˜๐‘š) โ‰ค ๐‘ฅ)
3823, 36, 37syl2anc 585 . . . . . 6 (๐œ‘ โ†’ โˆƒ๐‘ฅ โˆˆ โ„ โˆ€๐‘š โˆˆ โ„• (๐‘‡โ€˜๐‘š) โ‰ค ๐‘ฅ)
391, 5, 2, 6, 14, 15, 38isumsup2 15736 . . . . 5 (๐œ‘ โ†’ ๐‘‡ โ‡ sup(ran ๐‘‡, โ„, < ))
40 rge0ssre 13379 . . . . . . 7 (0[,)+โˆž) โŠ† โ„
4126, 40sstrdi 3957 . . . . . 6 (๐œ‘ โ†’ ran ๐‘‡ โŠ† โ„)
42 1nn 12169 . . . . . . . . 9 1 โˆˆ โ„•
4325fdmd 6680 . . . . . . . . 9 (๐œ‘ โ†’ dom ๐‘‡ = โ„•)
4442, 43eleqtrrid 2841 . . . . . . . 8 (๐œ‘ โ†’ 1 โˆˆ dom ๐‘‡)
4544ne0d 4296 . . . . . . 7 (๐œ‘ โ†’ dom ๐‘‡ โ‰  โˆ…)
46 dm0rn0 5881 . . . . . . . 8 (dom ๐‘‡ = โˆ… โ†” ran ๐‘‡ = โˆ…)
4746necon3bii 2993 . . . . . . 7 (dom ๐‘‡ โ‰  โˆ… โ†” ran ๐‘‡ โ‰  โˆ…)
4845, 47sylib 217 . . . . . 6 (๐œ‘ โ†’ ran ๐‘‡ โ‰  โˆ…)
49 brralrspcev 5166 . . . . . . 7 ((sup(ran ๐‘‡, โ„*, < ) โˆˆ โ„ โˆง โˆ€๐‘ฅ โˆˆ ran ๐‘‡ ๐‘ฅ โ‰ค sup(ran ๐‘‡, โ„*, < )) โ†’ โˆƒ๐‘ฆ โˆˆ โ„ โˆ€๐‘ฅ โˆˆ ran ๐‘‡ ๐‘ฅ โ‰ค ๐‘ฆ)
5023, 31, 49syl2anc 585 . . . . . 6 (๐œ‘ โ†’ โˆƒ๐‘ฆ โˆˆ โ„ โˆ€๐‘ฅ โˆˆ ran ๐‘‡ ๐‘ฅ โ‰ค ๐‘ฆ)
51 supxrre 13252 . . . . . 6 ((ran ๐‘‡ โŠ† โ„ โˆง ran ๐‘‡ โ‰  โˆ… โˆง โˆƒ๐‘ฆ โˆˆ โ„ โˆ€๐‘ฅ โˆˆ ran ๐‘‡ ๐‘ฅ โ‰ค ๐‘ฆ) โ†’ sup(ran ๐‘‡, โ„*, < ) = sup(ran ๐‘‡, โ„, < ))
5241, 48, 50, 51syl3anc 1372 . . . . 5 (๐œ‘ โ†’ sup(ran ๐‘‡, โ„*, < ) = sup(ran ๐‘‡, โ„, < ))
5339, 52breqtrrd 5134 . . . 4 (๐œ‘ โ†’ ๐‘‡ โ‡ sup(ran ๐‘‡, โ„*, < ))
541, 2, 3, 4, 53climi2 15399 . . 3 (๐œ‘ โ†’ โˆƒ๐‘— โˆˆ โ„• โˆ€๐‘š โˆˆ (โ„คโ‰ฅโ€˜๐‘—)(absโ€˜((๐‘‡โ€˜๐‘š) โˆ’ sup(ran ๐‘‡, โ„*, < ))) < ๐ถ)
551r19.2uz 15242 . . 3 (โˆƒ๐‘— โˆˆ โ„• โˆ€๐‘š โˆˆ (โ„คโ‰ฅโ€˜๐‘—)(absโ€˜((๐‘‡โ€˜๐‘š) โˆ’ sup(ran ๐‘‡, โ„*, < ))) < ๐ถ โ†’ โˆƒ๐‘š โˆˆ โ„• (absโ€˜((๐‘‡โ€˜๐‘š) โˆ’ sup(ran ๐‘‡, โ„*, < ))) < ๐ถ)
5654, 55syl 17 . 2 (๐œ‘ โ†’ โˆƒ๐‘š โˆˆ โ„• (absโ€˜((๐‘‡โ€˜๐‘š) โˆ’ sup(ran ๐‘‡, โ„*, < ))) < ๐ถ)
57 1zzd 12539 . . . . . . . . 9 (((๐œ‘ โˆง (๐‘š โˆˆ โ„• โˆง (absโ€˜((๐‘‡โ€˜๐‘š) โˆ’ sup(ran ๐‘‡, โ„*, < ))) < ๐ถ)) โˆง ๐‘— โˆˆ (1...๐‘š)) โ†’ 1 โˆˆ โ„ค)
583ad2antrr 725 . . . . . . . . . 10 (((๐œ‘ โˆง (๐‘š โˆˆ โ„• โˆง (absโ€˜((๐‘‡โ€˜๐‘š) โˆ’ sup(ran ๐‘‡, โ„*, < ))) < ๐ถ)) โˆง ๐‘— โˆˆ (1...๐‘š)) โ†’ ๐ถ โˆˆ โ„+)
59 simplrl 776 . . . . . . . . . . 11 (((๐œ‘ โˆง (๐‘š โˆˆ โ„• โˆง (absโ€˜((๐‘‡โ€˜๐‘š) โˆ’ sup(ran ๐‘‡, โ„*, < ))) < ๐ถ)) โˆง ๐‘— โˆˆ (1...๐‘š)) โ†’ ๐‘š โˆˆ โ„•)
6059nnrpd 12960 . . . . . . . . . 10 (((๐œ‘ โˆง (๐‘š โˆˆ โ„• โˆง (absโ€˜((๐‘‡โ€˜๐‘š) โˆ’ sup(ran ๐‘‡, โ„*, < ))) < ๐ถ)) โˆง ๐‘— โˆˆ (1...๐‘š)) โ†’ ๐‘š โˆˆ โ„+)
6158, 60rpdivcld 12979 . . . . . . . . 9 (((๐œ‘ โˆง (๐‘š โˆˆ โ„• โˆง (absโ€˜((๐‘‡โ€˜๐‘š) โˆ’ sup(ran ๐‘‡, โ„*, < ))) < ๐ถ)) โˆง ๐‘— โˆˆ (1...๐‘š)) โ†’ (๐ถ / ๐‘š) โˆˆ โ„+)
62 fvex 6856 . . . . . . . . . . . . . . . 16 ((,)โ€˜(๐นโ€˜๐‘ง)) โˆˆ V
6362inex1 5275 . . . . . . . . . . . . . . 15 (((,)โ€˜(๐นโ€˜๐‘ง)) โˆฉ ((,)โ€˜(๐บโ€˜๐‘—))) โˆˆ V
6463rgenw 3065 . . . . . . . . . . . . . 14 โˆ€๐‘ง โˆˆ โ„• (((,)โ€˜(๐นโ€˜๐‘ง)) โˆฉ ((,)โ€˜(๐บโ€˜๐‘—))) โˆˆ V
65 eqid 2733 . . . . . . . . . . . . . . 15 (๐‘ง โˆˆ โ„• โ†ฆ (((,)โ€˜(๐นโ€˜๐‘ง)) โˆฉ ((,)โ€˜(๐บโ€˜๐‘—)))) = (๐‘ง โˆˆ โ„• โ†ฆ (((,)โ€˜(๐นโ€˜๐‘ง)) โˆฉ ((,)โ€˜(๐บโ€˜๐‘—))))
6665fnmpt 6642 . . . . . . . . . . . . . 14 (โˆ€๐‘ง โˆˆ โ„• (((,)โ€˜(๐นโ€˜๐‘ง)) โˆฉ ((,)โ€˜(๐บโ€˜๐‘—))) โˆˆ V โ†’ (๐‘ง โˆˆ โ„• โ†ฆ (((,)โ€˜(๐นโ€˜๐‘ง)) โˆฉ ((,)โ€˜(๐บโ€˜๐‘—)))) Fn โ„•)
6764, 66mp1i 13 . . . . . . . . . . . . 13 ((((๐œ‘ โˆง (๐‘š โˆˆ โ„• โˆง (absโ€˜((๐‘‡โ€˜๐‘š) โˆ’ sup(ran ๐‘‡, โ„*, < ))) < ๐ถ)) โˆง ๐‘— โˆˆ (1...๐‘š)) โˆง ๐‘› โˆˆ โ„•) โ†’ (๐‘ง โˆˆ โ„• โ†ฆ (((,)โ€˜(๐นโ€˜๐‘ง)) โˆฉ ((,)โ€˜(๐บโ€˜๐‘—)))) Fn โ„•)
68 elfznn 13476 . . . . . . . . . . . . 13 (๐‘– โˆˆ (1...๐‘›) โ†’ ๐‘– โˆˆ โ„•)
69 fvco2 6939 . . . . . . . . . . . . 13 (((๐‘ง โˆˆ โ„• โ†ฆ (((,)โ€˜(๐นโ€˜๐‘ง)) โˆฉ ((,)โ€˜(๐บโ€˜๐‘—)))) Fn โ„• โˆง ๐‘– โˆˆ โ„•) โ†’ ((vol* โˆ˜ (๐‘ง โˆˆ โ„• โ†ฆ (((,)โ€˜(๐นโ€˜๐‘ง)) โˆฉ ((,)โ€˜(๐บโ€˜๐‘—)))))โ€˜๐‘–) = (vol*โ€˜((๐‘ง โˆˆ โ„• โ†ฆ (((,)โ€˜(๐นโ€˜๐‘ง)) โˆฉ ((,)โ€˜(๐บโ€˜๐‘—))))โ€˜๐‘–)))
7067, 68, 69syl2an 597 . . . . . . . . . . . 12 (((((๐œ‘ โˆง (๐‘š โˆˆ โ„• โˆง (absโ€˜((๐‘‡โ€˜๐‘š) โˆ’ sup(ran ๐‘‡, โ„*, < ))) < ๐ถ)) โˆง ๐‘— โˆˆ (1...๐‘š)) โˆง ๐‘› โˆˆ โ„•) โˆง ๐‘– โˆˆ (1...๐‘›)) โ†’ ((vol* โˆ˜ (๐‘ง โˆˆ โ„• โ†ฆ (((,)โ€˜(๐นโ€˜๐‘ง)) โˆฉ ((,)โ€˜(๐บโ€˜๐‘—)))))โ€˜๐‘–) = (vol*โ€˜((๐‘ง โˆˆ โ„• โ†ฆ (((,)โ€˜(๐นโ€˜๐‘ง)) โˆฉ ((,)โ€˜(๐บโ€˜๐‘—))))โ€˜๐‘–)))
7168adantl 483 . . . . . . . . . . . . . 14 (((((๐œ‘ โˆง (๐‘š โˆˆ โ„• โˆง (absโ€˜((๐‘‡โ€˜๐‘š) โˆ’ sup(ran ๐‘‡, โ„*, < ))) < ๐ถ)) โˆง ๐‘— โˆˆ (1...๐‘š)) โˆง ๐‘› โˆˆ โ„•) โˆง ๐‘– โˆˆ (1...๐‘›)) โ†’ ๐‘– โˆˆ โ„•)
72 2fveq3 6848 . . . . . . . . . . . . . . . 16 (๐‘ง = ๐‘– โ†’ ((,)โ€˜(๐นโ€˜๐‘ง)) = ((,)โ€˜(๐นโ€˜๐‘–)))
7372ineq1d 4172 . . . . . . . . . . . . . . 15 (๐‘ง = ๐‘– โ†’ (((,)โ€˜(๐นโ€˜๐‘ง)) โˆฉ ((,)โ€˜(๐บโ€˜๐‘—))) = (((,)โ€˜(๐นโ€˜๐‘–)) โˆฉ ((,)โ€˜(๐บโ€˜๐‘—))))
74 fvex 6856 . . . . . . . . . . . . . . . 16 ((,)โ€˜(๐นโ€˜๐‘–)) โˆˆ V
7574inex1 5275 . . . . . . . . . . . . . . 15 (((,)โ€˜(๐นโ€˜๐‘–)) โˆฉ ((,)โ€˜(๐บโ€˜๐‘—))) โˆˆ V
7673, 65, 75fvmpt 6949 . . . . . . . . . . . . . 14 (๐‘– โˆˆ โ„• โ†’ ((๐‘ง โˆˆ โ„• โ†ฆ (((,)โ€˜(๐นโ€˜๐‘ง)) โˆฉ ((,)โ€˜(๐บโ€˜๐‘—))))โ€˜๐‘–) = (((,)โ€˜(๐นโ€˜๐‘–)) โˆฉ ((,)โ€˜(๐บโ€˜๐‘—))))
7771, 76syl 17 . . . . . . . . . . . . 13 (((((๐œ‘ โˆง (๐‘š โˆˆ โ„• โˆง (absโ€˜((๐‘‡โ€˜๐‘š) โˆ’ sup(ran ๐‘‡, โ„*, < ))) < ๐ถ)) โˆง ๐‘— โˆˆ (1...๐‘š)) โˆง ๐‘› โˆˆ โ„•) โˆง ๐‘– โˆˆ (1...๐‘›)) โ†’ ((๐‘ง โˆˆ โ„• โ†ฆ (((,)โ€˜(๐นโ€˜๐‘ง)) โˆฉ ((,)โ€˜(๐บโ€˜๐‘—))))โ€˜๐‘–) = (((,)โ€˜(๐นโ€˜๐‘–)) โˆฉ ((,)โ€˜(๐บโ€˜๐‘—))))
7877fveq2d 6847 . . . . . . . . . . . 12 (((((๐œ‘ โˆง (๐‘š โˆˆ โ„• โˆง (absโ€˜((๐‘‡โ€˜๐‘š) โˆ’ sup(ran ๐‘‡, โ„*, < ))) < ๐ถ)) โˆง ๐‘— โˆˆ (1...๐‘š)) โˆง ๐‘› โˆˆ โ„•) โˆง ๐‘– โˆˆ (1...๐‘›)) โ†’ (vol*โ€˜((๐‘ง โˆˆ โ„• โ†ฆ (((,)โ€˜(๐นโ€˜๐‘ง)) โˆฉ ((,)โ€˜(๐บโ€˜๐‘—))))โ€˜๐‘–)) = (vol*โ€˜(((,)โ€˜(๐นโ€˜๐‘–)) โˆฉ ((,)โ€˜(๐บโ€˜๐‘—)))))
7970, 78eqtrd 2773 . . . . . . . . . . 11 (((((๐œ‘ โˆง (๐‘š โˆˆ โ„• โˆง (absโ€˜((๐‘‡โ€˜๐‘š) โˆ’ sup(ran ๐‘‡, โ„*, < ))) < ๐ถ)) โˆง ๐‘— โˆˆ (1...๐‘š)) โˆง ๐‘› โˆˆ โ„•) โˆง ๐‘– โˆˆ (1...๐‘›)) โ†’ ((vol* โˆ˜ (๐‘ง โˆˆ โ„• โ†ฆ (((,)โ€˜(๐นโ€˜๐‘ง)) โˆฉ ((,)โ€˜(๐บโ€˜๐‘—)))))โ€˜๐‘–) = (vol*โ€˜(((,)โ€˜(๐นโ€˜๐‘–)) โˆฉ ((,)โ€˜(๐บโ€˜๐‘—)))))
80 simpr 486 . . . . . . . . . . . 12 ((((๐œ‘ โˆง (๐‘š โˆˆ โ„• โˆง (absโ€˜((๐‘‡โ€˜๐‘š) โˆ’ sup(ran ๐‘‡, โ„*, < ))) < ๐ถ)) โˆง ๐‘— โˆˆ (1...๐‘š)) โˆง ๐‘› โˆˆ โ„•) โ†’ ๐‘› โˆˆ โ„•)
8180, 1eleqtrdi 2844 . . . . . . . . . . 11 ((((๐œ‘ โˆง (๐‘š โˆˆ โ„• โˆง (absโ€˜((๐‘‡โ€˜๐‘š) โˆ’ sup(ran ๐‘‡, โ„*, < ))) < ๐ถ)) โˆง ๐‘— โˆˆ (1...๐‘š)) โˆง ๐‘› โˆˆ โ„•) โ†’ ๐‘› โˆˆ (โ„คโ‰ฅโ€˜1))
82 inss2 4190 . . . . . . . . . . . . 13 (((,)โ€˜(๐นโ€˜๐‘–)) โˆฉ ((,)โ€˜(๐บโ€˜๐‘—))) โŠ† ((,)โ€˜(๐บโ€˜๐‘—))
837adantr 482 . . . . . . . . . . . . . . . . . . . 20 ((๐œ‘ โˆง (๐‘š โˆˆ โ„• โˆง (absโ€˜((๐‘‡โ€˜๐‘š) โˆ’ sup(ran ๐‘‡, โ„*, < ))) < ๐ถ)) โ†’ ๐บ:โ„•โŸถ( โ‰ค โˆฉ (โ„ ร— โ„)))
84 elfznn 13476 . . . . . . . . . . . . . . . . . . . 20 (๐‘— โˆˆ (1...๐‘š) โ†’ ๐‘— โˆˆ โ„•)
85 ffvelcdm 7033 . . . . . . . . . . . . . . . . . . . 20 ((๐บ:โ„•โŸถ( โ‰ค โˆฉ (โ„ ร— โ„)) โˆง ๐‘— โˆˆ โ„•) โ†’ (๐บโ€˜๐‘—) โˆˆ ( โ‰ค โˆฉ (โ„ ร— โ„)))
8683, 84, 85syl2an 597 . . . . . . . . . . . . . . . . . . 19 (((๐œ‘ โˆง (๐‘š โˆˆ โ„• โˆง (absโ€˜((๐‘‡โ€˜๐‘š) โˆ’ sup(ran ๐‘‡, โ„*, < ))) < ๐ถ)) โˆง ๐‘— โˆˆ (1...๐‘š)) โ†’ (๐บโ€˜๐‘—) โˆˆ ( โ‰ค โˆฉ (โ„ ร— โ„)))
8786elin2d 4160 . . . . . . . . . . . . . . . . . 18 (((๐œ‘ โˆง (๐‘š โˆˆ โ„• โˆง (absโ€˜((๐‘‡โ€˜๐‘š) โˆ’ sup(ran ๐‘‡, โ„*, < ))) < ๐ถ)) โˆง ๐‘— โˆˆ (1...๐‘š)) โ†’ (๐บโ€˜๐‘—) โˆˆ (โ„ ร— โ„))
88 1st2nd2 7961 . . . . . . . . . . . . . . . . . 18 ((๐บโ€˜๐‘—) โˆˆ (โ„ ร— โ„) โ†’ (๐บโ€˜๐‘—) = โŸจ(1st โ€˜(๐บโ€˜๐‘—)), (2nd โ€˜(๐บโ€˜๐‘—))โŸฉ)
8987, 88syl 17 . . . . . . . . . . . . . . . . 17 (((๐œ‘ โˆง (๐‘š โˆˆ โ„• โˆง (absโ€˜((๐‘‡โ€˜๐‘š) โˆ’ sup(ran ๐‘‡, โ„*, < ))) < ๐ถ)) โˆง ๐‘— โˆˆ (1...๐‘š)) โ†’ (๐บโ€˜๐‘—) = โŸจ(1st โ€˜(๐บโ€˜๐‘—)), (2nd โ€˜(๐บโ€˜๐‘—))โŸฉ)
9089fveq2d 6847 . . . . . . . . . . . . . . . 16 (((๐œ‘ โˆง (๐‘š โˆˆ โ„• โˆง (absโ€˜((๐‘‡โ€˜๐‘š) โˆ’ sup(ran ๐‘‡, โ„*, < ))) < ๐ถ)) โˆง ๐‘— โˆˆ (1...๐‘š)) โ†’ ((,)โ€˜(๐บโ€˜๐‘—)) = ((,)โ€˜โŸจ(1st โ€˜(๐บโ€˜๐‘—)), (2nd โ€˜(๐บโ€˜๐‘—))โŸฉ))
91 df-ov 7361 . . . . . . . . . . . . . . . 16 ((1st โ€˜(๐บโ€˜๐‘—))(,)(2nd โ€˜(๐บโ€˜๐‘—))) = ((,)โ€˜โŸจ(1st โ€˜(๐บโ€˜๐‘—)), (2nd โ€˜(๐บโ€˜๐‘—))โŸฉ)
9290, 91eqtr4di 2791 . . . . . . . . . . . . . . 15 (((๐œ‘ โˆง (๐‘š โˆˆ โ„• โˆง (absโ€˜((๐‘‡โ€˜๐‘š) โˆ’ sup(ran ๐‘‡, โ„*, < ))) < ๐ถ)) โˆง ๐‘— โˆˆ (1...๐‘š)) โ†’ ((,)โ€˜(๐บโ€˜๐‘—)) = ((1st โ€˜(๐บโ€˜๐‘—))(,)(2nd โ€˜(๐บโ€˜๐‘—))))
93 ioossre 13331 . . . . . . . . . . . . . . 15 ((1st โ€˜(๐บโ€˜๐‘—))(,)(2nd โ€˜(๐บโ€˜๐‘—))) โŠ† โ„
9492, 93eqsstrdi 3999 . . . . . . . . . . . . . 14 (((๐œ‘ โˆง (๐‘š โˆˆ โ„• โˆง (absโ€˜((๐‘‡โ€˜๐‘š) โˆ’ sup(ran ๐‘‡, โ„*, < ))) < ๐ถ)) โˆง ๐‘— โˆˆ (1...๐‘š)) โ†’ ((,)โ€˜(๐บโ€˜๐‘—)) โŠ† โ„)
9594ad2antrr 725 . . . . . . . . . . . . 13 (((((๐œ‘ โˆง (๐‘š โˆˆ โ„• โˆง (absโ€˜((๐‘‡โ€˜๐‘š) โˆ’ sup(ran ๐‘‡, โ„*, < ))) < ๐ถ)) โˆง ๐‘— โˆˆ (1...๐‘š)) โˆง ๐‘› โˆˆ โ„•) โˆง ๐‘– โˆˆ (1...๐‘›)) โ†’ ((,)โ€˜(๐บโ€˜๐‘—)) โŠ† โ„)
9692fveq2d 6847 . . . . . . . . . . . . . . . 16 (((๐œ‘ โˆง (๐‘š โˆˆ โ„• โˆง (absโ€˜((๐‘‡โ€˜๐‘š) โˆ’ sup(ran ๐‘‡, โ„*, < ))) < ๐ถ)) โˆง ๐‘— โˆˆ (1...๐‘š)) โ†’ (vol*โ€˜((,)โ€˜(๐บโ€˜๐‘—))) = (vol*โ€˜((1st โ€˜(๐บโ€˜๐‘—))(,)(2nd โ€˜(๐บโ€˜๐‘—)))))
97 ovolfcl 24846 . . . . . . . . . . . . . . . . . 18 ((๐บ:โ„•โŸถ( โ‰ค โˆฉ (โ„ ร— โ„)) โˆง ๐‘— โˆˆ โ„•) โ†’ ((1st โ€˜(๐บโ€˜๐‘—)) โˆˆ โ„ โˆง (2nd โ€˜(๐บโ€˜๐‘—)) โˆˆ โ„ โˆง (1st โ€˜(๐บโ€˜๐‘—)) โ‰ค (2nd โ€˜(๐บโ€˜๐‘—))))
9883, 84, 97syl2an 597 . . . . . . . . . . . . . . . . 17 (((๐œ‘ โˆง (๐‘š โˆˆ โ„• โˆง (absโ€˜((๐‘‡โ€˜๐‘š) โˆ’ sup(ran ๐‘‡, โ„*, < ))) < ๐ถ)) โˆง ๐‘— โˆˆ (1...๐‘š)) โ†’ ((1st โ€˜(๐บโ€˜๐‘—)) โˆˆ โ„ โˆง (2nd โ€˜(๐บโ€˜๐‘—)) โˆˆ โ„ โˆง (1st โ€˜(๐บโ€˜๐‘—)) โ‰ค (2nd โ€˜(๐บโ€˜๐‘—))))
99 ovolioo 24948 . . . . . . . . . . . . . . . . 17 (((1st โ€˜(๐บโ€˜๐‘—)) โˆˆ โ„ โˆง (2nd โ€˜(๐บโ€˜๐‘—)) โˆˆ โ„ โˆง (1st โ€˜(๐บโ€˜๐‘—)) โ‰ค (2nd โ€˜(๐บโ€˜๐‘—))) โ†’ (vol*โ€˜((1st โ€˜(๐บโ€˜๐‘—))(,)(2nd โ€˜(๐บโ€˜๐‘—)))) = ((2nd โ€˜(๐บโ€˜๐‘—)) โˆ’ (1st โ€˜(๐บโ€˜๐‘—))))
10098, 99syl 17 . . . . . . . . . . . . . . . 16 (((๐œ‘ โˆง (๐‘š โˆˆ โ„• โˆง (absโ€˜((๐‘‡โ€˜๐‘š) โˆ’ sup(ran ๐‘‡, โ„*, < ))) < ๐ถ)) โˆง ๐‘— โˆˆ (1...๐‘š)) โ†’ (vol*โ€˜((1st โ€˜(๐บโ€˜๐‘—))(,)(2nd โ€˜(๐บโ€˜๐‘—)))) = ((2nd โ€˜(๐บโ€˜๐‘—)) โˆ’ (1st โ€˜(๐บโ€˜๐‘—))))
10196, 100eqtrd 2773 . . . . . . . . . . . . . . 15 (((๐œ‘ โˆง (๐‘š โˆˆ โ„• โˆง (absโ€˜((๐‘‡โ€˜๐‘š) โˆ’ sup(ran ๐‘‡, โ„*, < ))) < ๐ถ)) โˆง ๐‘— โˆˆ (1...๐‘š)) โ†’ (vol*โ€˜((,)โ€˜(๐บโ€˜๐‘—))) = ((2nd โ€˜(๐บโ€˜๐‘—)) โˆ’ (1st โ€˜(๐บโ€˜๐‘—))))
10298simp2d 1144 . . . . . . . . . . . . . . . 16 (((๐œ‘ โˆง (๐‘š โˆˆ โ„• โˆง (absโ€˜((๐‘‡โ€˜๐‘š) โˆ’ sup(ran ๐‘‡, โ„*, < ))) < ๐ถ)) โˆง ๐‘— โˆˆ (1...๐‘š)) โ†’ (2nd โ€˜(๐บโ€˜๐‘—)) โˆˆ โ„)
10398simp1d 1143 . . . . . . . . . . . . . . . 16 (((๐œ‘ โˆง (๐‘š โˆˆ โ„• โˆง (absโ€˜((๐‘‡โ€˜๐‘š) โˆ’ sup(ran ๐‘‡, โ„*, < ))) < ๐ถ)) โˆง ๐‘— โˆˆ (1...๐‘š)) โ†’ (1st โ€˜(๐บโ€˜๐‘—)) โˆˆ โ„)
104102, 103resubcld 11588 . . . . . . . . . . . . . . 15 (((๐œ‘ โˆง (๐‘š โˆˆ โ„• โˆง (absโ€˜((๐‘‡โ€˜๐‘š) โˆ’ sup(ran ๐‘‡, โ„*, < ))) < ๐ถ)) โˆง ๐‘— โˆˆ (1...๐‘š)) โ†’ ((2nd โ€˜(๐บโ€˜๐‘—)) โˆ’ (1st โ€˜(๐บโ€˜๐‘—))) โˆˆ โ„)
105101, 104eqeltrd 2834 . . . . . . . . . . . . . 14 (((๐œ‘ โˆง (๐‘š โˆˆ โ„• โˆง (absโ€˜((๐‘‡โ€˜๐‘š) โˆ’ sup(ran ๐‘‡, โ„*, < ))) < ๐ถ)) โˆง ๐‘— โˆˆ (1...๐‘š)) โ†’ (vol*โ€˜((,)โ€˜(๐บโ€˜๐‘—))) โˆˆ โ„)
106105ad2antrr 725 . . . . . . . . . . . . 13 (((((๐œ‘ โˆง (๐‘š โˆˆ โ„• โˆง (absโ€˜((๐‘‡โ€˜๐‘š) โˆ’ sup(ran ๐‘‡, โ„*, < ))) < ๐ถ)) โˆง ๐‘— โˆˆ (1...๐‘š)) โˆง ๐‘› โˆˆ โ„•) โˆง ๐‘– โˆˆ (1...๐‘›)) โ†’ (vol*โ€˜((,)โ€˜(๐บโ€˜๐‘—))) โˆˆ โ„)
107 ovolsscl 24866 . . . . . . . . . . . . 13 (((((,)โ€˜(๐นโ€˜๐‘–)) โˆฉ ((,)โ€˜(๐บโ€˜๐‘—))) โŠ† ((,)โ€˜(๐บโ€˜๐‘—)) โˆง ((,)โ€˜(๐บโ€˜๐‘—)) โŠ† โ„ โˆง (vol*โ€˜((,)โ€˜(๐บโ€˜๐‘—))) โˆˆ โ„) โ†’ (vol*โ€˜(((,)โ€˜(๐นโ€˜๐‘–)) โˆฉ ((,)โ€˜(๐บโ€˜๐‘—)))) โˆˆ โ„)
10882, 95, 106, 107mp3an2i 1467 . . . . . . . . . . . 12 (((((๐œ‘ โˆง (๐‘š โˆˆ โ„• โˆง (absโ€˜((๐‘‡โ€˜๐‘š) โˆ’ sup(ran ๐‘‡, โ„*, < ))) < ๐ถ)) โˆง ๐‘— โˆˆ (1...๐‘š)) โˆง ๐‘› โˆˆ โ„•) โˆง ๐‘– โˆˆ (1...๐‘›)) โ†’ (vol*โ€˜(((,)โ€˜(๐นโ€˜๐‘–)) โˆฉ ((,)โ€˜(๐บโ€˜๐‘—)))) โˆˆ โ„)
109108recnd 11188 . . . . . . . . . . 11 (((((๐œ‘ โˆง (๐‘š โˆˆ โ„• โˆง (absโ€˜((๐‘‡โ€˜๐‘š) โˆ’ sup(ran ๐‘‡, โ„*, < ))) < ๐ถ)) โˆง ๐‘— โˆˆ (1...๐‘š)) โˆง ๐‘› โˆˆ โ„•) โˆง ๐‘– โˆˆ (1...๐‘›)) โ†’ (vol*โ€˜(((,)โ€˜(๐นโ€˜๐‘–)) โˆฉ ((,)โ€˜(๐บโ€˜๐‘—)))) โˆˆ โ„‚)
11079, 81, 109fsumser 15620 . . . . . . . . . 10 ((((๐œ‘ โˆง (๐‘š โˆˆ โ„• โˆง (absโ€˜((๐‘‡โ€˜๐‘š) โˆ’ sup(ran ๐‘‡, โ„*, < ))) < ๐ถ)) โˆง ๐‘— โˆˆ (1...๐‘š)) โˆง ๐‘› โˆˆ โ„•) โ†’ ฮฃ๐‘– โˆˆ (1...๐‘›)(vol*โ€˜(((,)โ€˜(๐นโ€˜๐‘–)) โˆฉ ((,)โ€˜(๐บโ€˜๐‘—)))) = (seq1( + , (vol* โˆ˜ (๐‘ง โˆˆ โ„• โ†ฆ (((,)โ€˜(๐นโ€˜๐‘ง)) โˆฉ ((,)โ€˜(๐บโ€˜๐‘—))))))โ€˜๐‘›))
111110eqcomd 2739 . . . . . . . . 9 ((((๐œ‘ โˆง (๐‘š โˆˆ โ„• โˆง (absโ€˜((๐‘‡โ€˜๐‘š) โˆ’ sup(ran ๐‘‡, โ„*, < ))) < ๐ถ)) โˆง ๐‘— โˆˆ (1...๐‘š)) โˆง ๐‘› โˆˆ โ„•) โ†’ (seq1( + , (vol* โˆ˜ (๐‘ง โˆˆ โ„• โ†ฆ (((,)โ€˜(๐นโ€˜๐‘ง)) โˆฉ ((,)โ€˜(๐บโ€˜๐‘—))))))โ€˜๐‘›) = ฮฃ๐‘– โˆˆ (1...๐‘›)(vol*โ€˜(((,)โ€˜(๐นโ€˜๐‘–)) โˆฉ ((,)โ€˜(๐บโ€˜๐‘—)))))
112 2fveq3 6848 . . . . . . . . . . . . . 14 (๐‘ง = ๐‘˜ โ†’ ((,)โ€˜(๐นโ€˜๐‘ง)) = ((,)โ€˜(๐นโ€˜๐‘˜)))
113112ineq1d 4172 . . . . . . . . . . . . 13 (๐‘ง = ๐‘˜ โ†’ (((,)โ€˜(๐นโ€˜๐‘ง)) โˆฉ ((,)โ€˜(๐บโ€˜๐‘—))) = (((,)โ€˜(๐นโ€˜๐‘˜)) โˆฉ ((,)โ€˜(๐บโ€˜๐‘—))))
114113cbvmptv 5219 . . . . . . . . . . . 12 (๐‘ง โˆˆ โ„• โ†ฆ (((,)โ€˜(๐นโ€˜๐‘ง)) โˆฉ ((,)โ€˜(๐บโ€˜๐‘—)))) = (๐‘˜ โˆˆ โ„• โ†ฆ (((,)โ€˜(๐นโ€˜๐‘˜)) โˆฉ ((,)โ€˜(๐บโ€˜๐‘—))))
115 eqeq1 2737 . . . . . . . . . . . . . 14 (๐‘ง = ๐‘ฅ โ†’ (๐‘ง = โˆ… โ†” ๐‘ฅ = โˆ…))
116 infeq1 9417 . . . . . . . . . . . . . . 15 (๐‘ง = ๐‘ฅ โ†’ inf(๐‘ง, โ„*, < ) = inf(๐‘ฅ, โ„*, < ))
117 supeq1 9386 . . . . . . . . . . . . . . 15 (๐‘ง = ๐‘ฅ โ†’ sup(๐‘ง, โ„*, < ) = sup(๐‘ฅ, โ„*, < ))
118116, 117opeq12d 4839 . . . . . . . . . . . . . 14 (๐‘ง = ๐‘ฅ โ†’ โŸจinf(๐‘ง, โ„*, < ), sup(๐‘ง, โ„*, < )โŸฉ = โŸจinf(๐‘ฅ, โ„*, < ), sup(๐‘ฅ, โ„*, < )โŸฉ)
119115, 118ifbieq2d 4513 . . . . . . . . . . . . 13 (๐‘ง = ๐‘ฅ โ†’ if(๐‘ง = โˆ…, โŸจ0, 0โŸฉ, โŸจinf(๐‘ง, โ„*, < ), sup(๐‘ง, โ„*, < )โŸฉ) = if(๐‘ฅ = โˆ…, โŸจ0, 0โŸฉ, โŸจinf(๐‘ฅ, โ„*, < ), sup(๐‘ฅ, โ„*, < )โŸฉ))
120119cbvmptv 5219 . . . . . . . . . . . 12 (๐‘ง โˆˆ ran (,) โ†ฆ if(๐‘ง = โˆ…, โŸจ0, 0โŸฉ, โŸจinf(๐‘ง, โ„*, < ), sup(๐‘ง, โ„*, < )โŸฉ)) = (๐‘ฅ โˆˆ ran (,) โ†ฆ if(๐‘ฅ = โˆ…, โŸจ0, 0โŸฉ, โŸจinf(๐‘ฅ, โ„*, < ), sup(๐‘ฅ, โ„*, < )โŸฉ))
12116, 17, 18, 19, 20, 3, 7, 21, 5, 22, 114, 120uniioombllem2 24963 . . . . . . . . . . 11 ((๐œ‘ โˆง ๐‘— โˆˆ โ„•) โ†’ seq1( + , (vol* โˆ˜ (๐‘ง โˆˆ โ„• โ†ฆ (((,)โ€˜(๐นโ€˜๐‘ง)) โˆฉ ((,)โ€˜(๐บโ€˜๐‘—)))))) โ‡ (vol*โ€˜(((,)โ€˜(๐บโ€˜๐‘—)) โˆฉ ๐ด)))
12284, 121sylan2 594 . . . . . . . . . 10 ((๐œ‘ โˆง ๐‘— โˆˆ (1...๐‘š)) โ†’ seq1( + , (vol* โˆ˜ (๐‘ง โˆˆ โ„• โ†ฆ (((,)โ€˜(๐นโ€˜๐‘ง)) โˆฉ ((,)โ€˜(๐บโ€˜๐‘—)))))) โ‡ (vol*โ€˜(((,)โ€˜(๐บโ€˜๐‘—)) โˆฉ ๐ด)))
123122adantlr 714 . . . . . . . . 9 (((๐œ‘ โˆง (๐‘š โˆˆ โ„• โˆง (absโ€˜((๐‘‡โ€˜๐‘š) โˆ’ sup(ran ๐‘‡, โ„*, < ))) < ๐ถ)) โˆง ๐‘— โˆˆ (1...๐‘š)) โ†’ seq1( + , (vol* โˆ˜ (๐‘ง โˆˆ โ„• โ†ฆ (((,)โ€˜(๐นโ€˜๐‘ง)) โˆฉ ((,)โ€˜(๐บโ€˜๐‘—)))))) โ‡ (vol*โ€˜(((,)โ€˜(๐บโ€˜๐‘—)) โˆฉ ๐ด)))
1241, 57, 61, 111, 123climi2 15399 . . . . . . . 8 (((๐œ‘ โˆง (๐‘š โˆˆ โ„• โˆง (absโ€˜((๐‘‡โ€˜๐‘š) โˆ’ sup(ran ๐‘‡, โ„*, < ))) < ๐ถ)) โˆง ๐‘— โˆˆ (1...๐‘š)) โ†’ โˆƒ๐‘Ž โˆˆ โ„• โˆ€๐‘› โˆˆ (โ„คโ‰ฅโ€˜๐‘Ž)(absโ€˜(ฮฃ๐‘– โˆˆ (1...๐‘›)(vol*โ€˜(((,)โ€˜(๐นโ€˜๐‘–)) โˆฉ ((,)โ€˜(๐บโ€˜๐‘—)))) โˆ’ (vol*โ€˜(((,)โ€˜(๐บโ€˜๐‘—)) โˆฉ ๐ด)))) < (๐ถ / ๐‘š))
125 1z 12538 . . . . . . . . 9 1 โˆˆ โ„ค
1261rexuz3 15239 . . . . . . . . 9 (1 โˆˆ โ„ค โ†’ (โˆƒ๐‘Ž โˆˆ โ„• โˆ€๐‘› โˆˆ (โ„คโ‰ฅโ€˜๐‘Ž)(absโ€˜(ฮฃ๐‘– โˆˆ (1...๐‘›)(vol*โ€˜(((,)โ€˜(๐นโ€˜๐‘–)) โˆฉ ((,)โ€˜(๐บโ€˜๐‘—)))) โˆ’ (vol*โ€˜(((,)โ€˜(๐บโ€˜๐‘—)) โˆฉ ๐ด)))) < (๐ถ / ๐‘š) โ†” โˆƒ๐‘Ž โˆˆ โ„ค โˆ€๐‘› โˆˆ (โ„คโ‰ฅโ€˜๐‘Ž)(absโ€˜(ฮฃ๐‘– โˆˆ (1...๐‘›)(vol*โ€˜(((,)โ€˜(๐นโ€˜๐‘–)) โˆฉ ((,)โ€˜(๐บโ€˜๐‘—)))) โˆ’ (vol*โ€˜(((,)โ€˜(๐บโ€˜๐‘—)) โˆฉ ๐ด)))) < (๐ถ / ๐‘š)))
127125, 126ax-mp 5 . . . . . . . 8 (โˆƒ๐‘Ž โˆˆ โ„• โˆ€๐‘› โˆˆ (โ„คโ‰ฅโ€˜๐‘Ž)(absโ€˜(ฮฃ๐‘– โˆˆ (1...๐‘›)(vol*โ€˜(((,)โ€˜(๐นโ€˜๐‘–)) โˆฉ ((,)โ€˜(๐บโ€˜๐‘—)))) โˆ’ (vol*โ€˜(((,)โ€˜(๐บโ€˜๐‘—)) โˆฉ ๐ด)))) < (๐ถ / ๐‘š) โ†” โˆƒ๐‘Ž โˆˆ โ„ค โˆ€๐‘› โˆˆ (โ„คโ‰ฅโ€˜๐‘Ž)(absโ€˜(ฮฃ๐‘– โˆˆ (1...๐‘›)(vol*โ€˜(((,)โ€˜(๐นโ€˜๐‘–)) โˆฉ ((,)โ€˜(๐บโ€˜๐‘—)))) โˆ’ (vol*โ€˜(((,)โ€˜(๐บโ€˜๐‘—)) โˆฉ ๐ด)))) < (๐ถ / ๐‘š))
128124, 127sylib 217 . . . . . . 7 (((๐œ‘ โˆง (๐‘š โˆˆ โ„• โˆง (absโ€˜((๐‘‡โ€˜๐‘š) โˆ’ sup(ran ๐‘‡, โ„*, < ))) < ๐ถ)) โˆง ๐‘— โˆˆ (1...๐‘š)) โ†’ โˆƒ๐‘Ž โˆˆ โ„ค โˆ€๐‘› โˆˆ (โ„คโ‰ฅโ€˜๐‘Ž)(absโ€˜(ฮฃ๐‘– โˆˆ (1...๐‘›)(vol*โ€˜(((,)โ€˜(๐นโ€˜๐‘–)) โˆฉ ((,)โ€˜(๐บโ€˜๐‘—)))) โˆ’ (vol*โ€˜(((,)โ€˜(๐บโ€˜๐‘—)) โˆฉ ๐ด)))) < (๐ถ / ๐‘š))
129128ralrimiva 3140 . . . . . 6 ((๐œ‘ โˆง (๐‘š โˆˆ โ„• โˆง (absโ€˜((๐‘‡โ€˜๐‘š) โˆ’ sup(ran ๐‘‡, โ„*, < ))) < ๐ถ)) โ†’ โˆ€๐‘— โˆˆ (1...๐‘š)โˆƒ๐‘Ž โˆˆ โ„ค โˆ€๐‘› โˆˆ (โ„คโ‰ฅโ€˜๐‘Ž)(absโ€˜(ฮฃ๐‘– โˆˆ (1...๐‘›)(vol*โ€˜(((,)โ€˜(๐นโ€˜๐‘–)) โˆฉ ((,)โ€˜(๐บโ€˜๐‘—)))) โˆ’ (vol*โ€˜(((,)โ€˜(๐บโ€˜๐‘—)) โˆฉ ๐ด)))) < (๐ถ / ๐‘š))
130 fzfi 13883 . . . . . . 7 (1...๐‘š) โˆˆ Fin
131 rexfiuz 15238 . . . . . . 7 ((1...๐‘š) โˆˆ Fin โ†’ (โˆƒ๐‘Ž โˆˆ โ„ค โˆ€๐‘› โˆˆ (โ„คโ‰ฅโ€˜๐‘Ž)โˆ€๐‘— โˆˆ (1...๐‘š)(absโ€˜(ฮฃ๐‘– โˆˆ (1...๐‘›)(vol*โ€˜(((,)โ€˜(๐นโ€˜๐‘–)) โˆฉ ((,)โ€˜(๐บโ€˜๐‘—)))) โˆ’ (vol*โ€˜(((,)โ€˜(๐บโ€˜๐‘—)) โˆฉ ๐ด)))) < (๐ถ / ๐‘š) โ†” โˆ€๐‘— โˆˆ (1...๐‘š)โˆƒ๐‘Ž โˆˆ โ„ค โˆ€๐‘› โˆˆ (โ„คโ‰ฅโ€˜๐‘Ž)(absโ€˜(ฮฃ๐‘– โˆˆ (1...๐‘›)(vol*โ€˜(((,)โ€˜(๐นโ€˜๐‘–)) โˆฉ ((,)โ€˜(๐บโ€˜๐‘—)))) โˆ’ (vol*โ€˜(((,)โ€˜(๐บโ€˜๐‘—)) โˆฉ ๐ด)))) < (๐ถ / ๐‘š)))
132130, 131ax-mp 5 . . . . . 6 (โˆƒ๐‘Ž โˆˆ โ„ค โˆ€๐‘› โˆˆ (โ„คโ‰ฅโ€˜๐‘Ž)โˆ€๐‘— โˆˆ (1...๐‘š)(absโ€˜(ฮฃ๐‘– โˆˆ (1...๐‘›)(vol*โ€˜(((,)โ€˜(๐นโ€˜๐‘–)) โˆฉ ((,)โ€˜(๐บโ€˜๐‘—)))) โˆ’ (vol*โ€˜(((,)โ€˜(๐บโ€˜๐‘—)) โˆฉ ๐ด)))) < (๐ถ / ๐‘š) โ†” โˆ€๐‘— โˆˆ (1...๐‘š)โˆƒ๐‘Ž โˆˆ โ„ค โˆ€๐‘› โˆˆ (โ„คโ‰ฅโ€˜๐‘Ž)(absโ€˜(ฮฃ๐‘– โˆˆ (1...๐‘›)(vol*โ€˜(((,)โ€˜(๐นโ€˜๐‘–)) โˆฉ ((,)โ€˜(๐บโ€˜๐‘—)))) โˆ’ (vol*โ€˜(((,)โ€˜(๐บโ€˜๐‘—)) โˆฉ ๐ด)))) < (๐ถ / ๐‘š))
133129, 132sylibr 233 . . . . 5 ((๐œ‘ โˆง (๐‘š โˆˆ โ„• โˆง (absโ€˜((๐‘‡โ€˜๐‘š) โˆ’ sup(ran ๐‘‡, โ„*, < ))) < ๐ถ)) โ†’ โˆƒ๐‘Ž โˆˆ โ„ค โˆ€๐‘› โˆˆ (โ„คโ‰ฅโ€˜๐‘Ž)โˆ€๐‘— โˆˆ (1...๐‘š)(absโ€˜(ฮฃ๐‘– โˆˆ (1...๐‘›)(vol*โ€˜(((,)โ€˜(๐นโ€˜๐‘–)) โˆฉ ((,)โ€˜(๐บโ€˜๐‘—)))) โˆ’ (vol*โ€˜(((,)โ€˜(๐บโ€˜๐‘—)) โˆฉ ๐ด)))) < (๐ถ / ๐‘š))
1341rexuz3 15239 . . . . . 6 (1 โˆˆ โ„ค โ†’ (โˆƒ๐‘Ž โˆˆ โ„• โˆ€๐‘› โˆˆ (โ„คโ‰ฅโ€˜๐‘Ž)โˆ€๐‘— โˆˆ (1...๐‘š)(absโ€˜(ฮฃ๐‘– โˆˆ (1...๐‘›)(vol*โ€˜(((,)โ€˜(๐นโ€˜๐‘–)) โˆฉ ((,)โ€˜(๐บโ€˜๐‘—)))) โˆ’ (vol*โ€˜(((,)โ€˜(๐บโ€˜๐‘—)) โˆฉ ๐ด)))) < (๐ถ / ๐‘š) โ†” โˆƒ๐‘Ž โˆˆ โ„ค โˆ€๐‘› โˆˆ (โ„คโ‰ฅโ€˜๐‘Ž)โˆ€๐‘— โˆˆ (1...๐‘š)(absโ€˜(ฮฃ๐‘– โˆˆ (1...๐‘›)(vol*โ€˜(((,)โ€˜(๐นโ€˜๐‘–)) โˆฉ ((,)โ€˜(๐บโ€˜๐‘—)))) โˆ’ (vol*โ€˜(((,)โ€˜(๐บโ€˜๐‘—)) โˆฉ ๐ด)))) < (๐ถ / ๐‘š)))
135125, 134ax-mp 5 . . . . 5 (โˆƒ๐‘Ž โˆˆ โ„• โˆ€๐‘› โˆˆ (โ„คโ‰ฅโ€˜๐‘Ž)โˆ€๐‘— โˆˆ (1...๐‘š)(absโ€˜(ฮฃ๐‘– โˆˆ (1...๐‘›)(vol*โ€˜(((,)โ€˜(๐นโ€˜๐‘–)) โˆฉ ((,)โ€˜(๐บโ€˜๐‘—)))) โˆ’ (vol*โ€˜(((,)โ€˜(๐บโ€˜๐‘—)) โˆฉ ๐ด)))) < (๐ถ / ๐‘š) โ†” โˆƒ๐‘Ž โˆˆ โ„ค โˆ€๐‘› โˆˆ (โ„คโ‰ฅโ€˜๐‘Ž)โˆ€๐‘— โˆˆ (1...๐‘š)(absโ€˜(ฮฃ๐‘– โˆˆ (1...๐‘›)(vol*โ€˜(((,)โ€˜(๐นโ€˜๐‘–)) โˆฉ ((,)โ€˜(๐บโ€˜๐‘—)))) โˆ’ (vol*โ€˜(((,)โ€˜(๐บโ€˜๐‘—)) โˆฉ ๐ด)))) < (๐ถ / ๐‘š))
136133, 135sylibr 233 . . . 4 ((๐œ‘ โˆง (๐‘š โˆˆ โ„• โˆง (absโ€˜((๐‘‡โ€˜๐‘š) โˆ’ sup(ran ๐‘‡, โ„*, < ))) < ๐ถ)) โ†’ โˆƒ๐‘Ž โˆˆ โ„• โˆ€๐‘› โˆˆ (โ„คโ‰ฅโ€˜๐‘Ž)โˆ€๐‘— โˆˆ (1...๐‘š)(absโ€˜(ฮฃ๐‘– โˆˆ (1...๐‘›)(vol*โ€˜(((,)โ€˜(๐นโ€˜๐‘–)) โˆฉ ((,)โ€˜(๐บโ€˜๐‘—)))) โˆ’ (vol*โ€˜(((,)โ€˜(๐บโ€˜๐‘—)) โˆฉ ๐ด)))) < (๐ถ / ๐‘š))
1371r19.2uz 15242 . . . 4 (โˆƒ๐‘Ž โˆˆ โ„• โˆ€๐‘› โˆˆ (โ„คโ‰ฅโ€˜๐‘Ž)โˆ€๐‘— โˆˆ (1...๐‘š)(absโ€˜(ฮฃ๐‘– โˆˆ (1...๐‘›)(vol*โ€˜(((,)โ€˜(๐นโ€˜๐‘–)) โˆฉ ((,)โ€˜(๐บโ€˜๐‘—)))) โˆ’ (vol*โ€˜(((,)โ€˜(๐บโ€˜๐‘—)) โˆฉ ๐ด)))) < (๐ถ / ๐‘š) โ†’ โˆƒ๐‘› โˆˆ โ„• โˆ€๐‘— โˆˆ (1...๐‘š)(absโ€˜(ฮฃ๐‘– โˆˆ (1...๐‘›)(vol*โ€˜(((,)โ€˜(๐นโ€˜๐‘–)) โˆฉ ((,)โ€˜(๐บโ€˜๐‘—)))) โˆ’ (vol*โ€˜(((,)โ€˜(๐บโ€˜๐‘—)) โˆฉ ๐ด)))) < (๐ถ / ๐‘š))
138136, 137syl 17 . . 3 ((๐œ‘ โˆง (๐‘š โˆˆ โ„• โˆง (absโ€˜((๐‘‡โ€˜๐‘š) โˆ’ sup(ran ๐‘‡, โ„*, < ))) < ๐ถ)) โ†’ โˆƒ๐‘› โˆˆ โ„• โˆ€๐‘— โˆˆ (1...๐‘š)(absโ€˜(ฮฃ๐‘– โˆˆ (1...๐‘›)(vol*โ€˜(((,)โ€˜(๐นโ€˜๐‘–)) โˆฉ ((,)โ€˜(๐บโ€˜๐‘—)))) โˆ’ (vol*โ€˜(((,)โ€˜(๐บโ€˜๐‘—)) โˆฉ ๐ด)))) < (๐ถ / ๐‘š))
13916adantr 482 . . . . 5 ((๐œ‘ โˆง ((๐‘š โˆˆ โ„• โˆง (absโ€˜((๐‘‡โ€˜๐‘š) โˆ’ sup(ran ๐‘‡, โ„*, < ))) < ๐ถ) โˆง (๐‘› โˆˆ โ„• โˆง โˆ€๐‘— โˆˆ (1...๐‘š)(absโ€˜(ฮฃ๐‘– โˆˆ (1...๐‘›)(vol*โ€˜(((,)โ€˜(๐นโ€˜๐‘–)) โˆฉ ((,)โ€˜(๐บโ€˜๐‘—)))) โˆ’ (vol*โ€˜(((,)โ€˜(๐บโ€˜๐‘—)) โˆฉ ๐ด)))) < (๐ถ / ๐‘š)))) โ†’ ๐น:โ„•โŸถ( โ‰ค โˆฉ (โ„ ร— โ„)))
14017adantr 482 . . . . 5 ((๐œ‘ โˆง ((๐‘š โˆˆ โ„• โˆง (absโ€˜((๐‘‡โ€˜๐‘š) โˆ’ sup(ran ๐‘‡, โ„*, < ))) < ๐ถ) โˆง (๐‘› โˆˆ โ„• โˆง โˆ€๐‘— โˆˆ (1...๐‘š)(absโ€˜(ฮฃ๐‘– โˆˆ (1...๐‘›)(vol*โ€˜(((,)โ€˜(๐นโ€˜๐‘–)) โˆฉ ((,)โ€˜(๐บโ€˜๐‘—)))) โˆ’ (vol*โ€˜(((,)โ€˜(๐บโ€˜๐‘—)) โˆฉ ๐ด)))) < (๐ถ / ๐‘š)))) โ†’ Disj ๐‘ฅ โˆˆ โ„• ((,)โ€˜(๐นโ€˜๐‘ฅ)))
14120adantr 482 . . . . 5 ((๐œ‘ โˆง ((๐‘š โˆˆ โ„• โˆง (absโ€˜((๐‘‡โ€˜๐‘š) โˆ’ sup(ran ๐‘‡, โ„*, < ))) < ๐ถ) โˆง (๐‘› โˆˆ โ„• โˆง โˆ€๐‘— โˆˆ (1...๐‘š)(absโ€˜(ฮฃ๐‘– โˆˆ (1...๐‘›)(vol*โ€˜(((,)โ€˜(๐นโ€˜๐‘–)) โˆฉ ((,)โ€˜(๐บโ€˜๐‘—)))) โˆ’ (vol*โ€˜(((,)โ€˜(๐บโ€˜๐‘—)) โˆฉ ๐ด)))) < (๐ถ / ๐‘š)))) โ†’ (vol*โ€˜๐ธ) โˆˆ โ„)
1423adantr 482 . . . . 5 ((๐œ‘ โˆง ((๐‘š โˆˆ โ„• โˆง (absโ€˜((๐‘‡โ€˜๐‘š) โˆ’ sup(ran ๐‘‡, โ„*, < ))) < ๐ถ) โˆง (๐‘› โˆˆ โ„• โˆง โˆ€๐‘— โˆˆ (1...๐‘š)(absโ€˜(ฮฃ๐‘– โˆˆ (1...๐‘›)(vol*โ€˜(((,)โ€˜(๐นโ€˜๐‘–)) โˆฉ ((,)โ€˜(๐บโ€˜๐‘—)))) โˆ’ (vol*โ€˜(((,)โ€˜(๐บโ€˜๐‘—)) โˆฉ ๐ด)))) < (๐ถ / ๐‘š)))) โ†’ ๐ถ โˆˆ โ„+)
1437adantr 482 . . . . 5 ((๐œ‘ โˆง ((๐‘š โˆˆ โ„• โˆง (absโ€˜((๐‘‡โ€˜๐‘š) โˆ’ sup(ran ๐‘‡, โ„*, < ))) < ๐ถ) โˆง (๐‘› โˆˆ โ„• โˆง โˆ€๐‘— โˆˆ (1...๐‘š)(absโ€˜(ฮฃ๐‘– โˆˆ (1...๐‘›)(vol*โ€˜(((,)โ€˜(๐นโ€˜๐‘–)) โˆฉ ((,)โ€˜(๐บโ€˜๐‘—)))) โˆ’ (vol*โ€˜(((,)โ€˜(๐บโ€˜๐‘—)) โˆฉ ๐ด)))) < (๐ถ / ๐‘š)))) โ†’ ๐บ:โ„•โŸถ( โ‰ค โˆฉ (โ„ ร— โ„)))
14421adantr 482 . . . . 5 ((๐œ‘ โˆง ((๐‘š โˆˆ โ„• โˆง (absโ€˜((๐‘‡โ€˜๐‘š) โˆ’ sup(ran ๐‘‡, โ„*, < ))) < ๐ถ) โˆง (๐‘› โˆˆ โ„• โˆง โˆ€๐‘— โˆˆ (1...๐‘š)(absโ€˜(ฮฃ๐‘– โˆˆ (1...๐‘›)(vol*โ€˜(((,)โ€˜(๐นโ€˜๐‘–)) โˆฉ ((,)โ€˜(๐บโ€˜๐‘—)))) โˆ’ (vol*โ€˜(((,)โ€˜(๐บโ€˜๐‘—)) โˆฉ ๐ด)))) < (๐ถ / ๐‘š)))) โ†’ ๐ธ โŠ† โˆช ran ((,) โˆ˜ ๐บ))
14522adantr 482 . . . . 5 ((๐œ‘ โˆง ((๐‘š โˆˆ โ„• โˆง (absโ€˜((๐‘‡โ€˜๐‘š) โˆ’ sup(ran ๐‘‡, โ„*, < ))) < ๐ถ) โˆง (๐‘› โˆˆ โ„• โˆง โˆ€๐‘— โˆˆ (1...๐‘š)(absโ€˜(ฮฃ๐‘– โˆˆ (1...๐‘›)(vol*โ€˜(((,)โ€˜(๐นโ€˜๐‘–)) โˆฉ ((,)โ€˜(๐บโ€˜๐‘—)))) โˆ’ (vol*โ€˜(((,)โ€˜(๐บโ€˜๐‘—)) โˆฉ ๐ด)))) < (๐ถ / ๐‘š)))) โ†’ sup(ran ๐‘‡, โ„*, < ) โ‰ค ((vol*โ€˜๐ธ) + ๐ถ))
146 simprll 778 . . . . 5 ((๐œ‘ โˆง ((๐‘š โˆˆ โ„• โˆง (absโ€˜((๐‘‡โ€˜๐‘š) โˆ’ sup(ran ๐‘‡, โ„*, < ))) < ๐ถ) โˆง (๐‘› โˆˆ โ„• โˆง โˆ€๐‘— โˆˆ (1...๐‘š)(absโ€˜(ฮฃ๐‘– โˆˆ (1...๐‘›)(vol*โ€˜(((,)โ€˜(๐นโ€˜๐‘–)) โˆฉ ((,)โ€˜(๐บโ€˜๐‘—)))) โˆ’ (vol*โ€˜(((,)โ€˜(๐บโ€˜๐‘—)) โˆฉ ๐ด)))) < (๐ถ / ๐‘š)))) โ†’ ๐‘š โˆˆ โ„•)
147 simprlr 779 . . . . 5 ((๐œ‘ โˆง ((๐‘š โˆˆ โ„• โˆง (absโ€˜((๐‘‡โ€˜๐‘š) โˆ’ sup(ran ๐‘‡, โ„*, < ))) < ๐ถ) โˆง (๐‘› โˆˆ โ„• โˆง โˆ€๐‘— โˆˆ (1...๐‘š)(absโ€˜(ฮฃ๐‘– โˆˆ (1...๐‘›)(vol*โ€˜(((,)โ€˜(๐นโ€˜๐‘–)) โˆฉ ((,)โ€˜(๐บโ€˜๐‘—)))) โˆ’ (vol*โ€˜(((,)โ€˜(๐บโ€˜๐‘—)) โˆฉ ๐ด)))) < (๐ถ / ๐‘š)))) โ†’ (absโ€˜((๐‘‡โ€˜๐‘š) โˆ’ sup(ran ๐‘‡, โ„*, < ))) < ๐ถ)
148 eqid 2733 . . . . 5 โˆช (((,) โˆ˜ ๐บ) โ€œ (1...๐‘š)) = โˆช (((,) โˆ˜ ๐บ) โ€œ (1...๐‘š))
149 simprrl 780 . . . . 5 ((๐œ‘ โˆง ((๐‘š โˆˆ โ„• โˆง (absโ€˜((๐‘‡โ€˜๐‘š) โˆ’ sup(ran ๐‘‡, โ„*, < ))) < ๐ถ) โˆง (๐‘› โˆˆ โ„• โˆง โˆ€๐‘— โˆˆ (1...๐‘š)(absโ€˜(ฮฃ๐‘– โˆˆ (1...๐‘›)(vol*โ€˜(((,)โ€˜(๐นโ€˜๐‘–)) โˆฉ ((,)โ€˜(๐บโ€˜๐‘—)))) โˆ’ (vol*โ€˜(((,)โ€˜(๐บโ€˜๐‘—)) โˆฉ ๐ด)))) < (๐ถ / ๐‘š)))) โ†’ ๐‘› โˆˆ โ„•)
150 simprrr 781 . . . . . 6 ((๐œ‘ โˆง ((๐‘š โˆˆ โ„• โˆง (absโ€˜((๐‘‡โ€˜๐‘š) โˆ’ sup(ran ๐‘‡, โ„*, < ))) < ๐ถ) โˆง (๐‘› โˆˆ โ„• โˆง โˆ€๐‘— โˆˆ (1...๐‘š)(absโ€˜(ฮฃ๐‘– โˆˆ (1...๐‘›)(vol*โ€˜(((,)โ€˜(๐นโ€˜๐‘–)) โˆฉ ((,)โ€˜(๐บโ€˜๐‘—)))) โˆ’ (vol*โ€˜(((,)โ€˜(๐บโ€˜๐‘—)) โˆฉ ๐ด)))) < (๐ถ / ๐‘š)))) โ†’ โˆ€๐‘— โˆˆ (1...๐‘š)(absโ€˜(ฮฃ๐‘– โˆˆ (1...๐‘›)(vol*โ€˜(((,)โ€˜(๐นโ€˜๐‘–)) โˆฉ ((,)โ€˜(๐บโ€˜๐‘—)))) โˆ’ (vol*โ€˜(((,)โ€˜(๐บโ€˜๐‘—)) โˆฉ ๐ด)))) < (๐ถ / ๐‘š))
151 2fveq3 6848 . . . . . . . . . . . . . 14 (๐‘– = ๐‘ง โ†’ ((,)โ€˜(๐นโ€˜๐‘–)) = ((,)โ€˜(๐นโ€˜๐‘ง)))
152151ineq1d 4172 . . . . . . . . . . . . 13 (๐‘– = ๐‘ง โ†’ (((,)โ€˜(๐นโ€˜๐‘–)) โˆฉ ((,)โ€˜(๐บโ€˜๐‘—))) = (((,)โ€˜(๐นโ€˜๐‘ง)) โˆฉ ((,)โ€˜(๐บโ€˜๐‘—))))
153152fveq2d 6847 . . . . . . . . . . . 12 (๐‘– = ๐‘ง โ†’ (vol*โ€˜(((,)โ€˜(๐นโ€˜๐‘–)) โˆฉ ((,)โ€˜(๐บโ€˜๐‘—)))) = (vol*โ€˜(((,)โ€˜(๐นโ€˜๐‘ง)) โˆฉ ((,)โ€˜(๐บโ€˜๐‘—)))))
154153cbvsumv 15586 . . . . . . . . . . 11 ฮฃ๐‘– โˆˆ (1...๐‘›)(vol*โ€˜(((,)โ€˜(๐นโ€˜๐‘–)) โˆฉ ((,)โ€˜(๐บโ€˜๐‘—)))) = ฮฃ๐‘ง โˆˆ (1...๐‘›)(vol*โ€˜(((,)โ€˜(๐นโ€˜๐‘ง)) โˆฉ ((,)โ€˜(๐บโ€˜๐‘—))))
155 2fveq3 6848 . . . . . . . . . . . . . 14 (๐‘— = ๐‘˜ โ†’ ((,)โ€˜(๐บโ€˜๐‘—)) = ((,)โ€˜(๐บโ€˜๐‘˜)))
156155ineq2d 4173 . . . . . . . . . . . . 13 (๐‘— = ๐‘˜ โ†’ (((,)โ€˜(๐นโ€˜๐‘ง)) โˆฉ ((,)โ€˜(๐บโ€˜๐‘—))) = (((,)โ€˜(๐นโ€˜๐‘ง)) โˆฉ ((,)โ€˜(๐บโ€˜๐‘˜))))
157156fveq2d 6847 . . . . . . . . . . . 12 (๐‘— = ๐‘˜ โ†’ (vol*โ€˜(((,)โ€˜(๐นโ€˜๐‘ง)) โˆฉ ((,)โ€˜(๐บโ€˜๐‘—)))) = (vol*โ€˜(((,)โ€˜(๐นโ€˜๐‘ง)) โˆฉ ((,)โ€˜(๐บโ€˜๐‘˜)))))
158157sumeq2sdv 15594 . . . . . . . . . . 11 (๐‘— = ๐‘˜ โ†’ ฮฃ๐‘ง โˆˆ (1...๐‘›)(vol*โ€˜(((,)โ€˜(๐นโ€˜๐‘ง)) โˆฉ ((,)โ€˜(๐บโ€˜๐‘—)))) = ฮฃ๐‘ง โˆˆ (1...๐‘›)(vol*โ€˜(((,)โ€˜(๐นโ€˜๐‘ง)) โˆฉ ((,)โ€˜(๐บโ€˜๐‘˜)))))
159154, 158eqtrid 2785 . . . . . . . . . 10 (๐‘— = ๐‘˜ โ†’ ฮฃ๐‘– โˆˆ (1...๐‘›)(vol*โ€˜(((,)โ€˜(๐นโ€˜๐‘–)) โˆฉ ((,)โ€˜(๐บโ€˜๐‘—)))) = ฮฃ๐‘ง โˆˆ (1...๐‘›)(vol*โ€˜(((,)โ€˜(๐นโ€˜๐‘ง)) โˆฉ ((,)โ€˜(๐บโ€˜๐‘˜)))))
160155ineq1d 4172 . . . . . . . . . . 11 (๐‘— = ๐‘˜ โ†’ (((,)โ€˜(๐บโ€˜๐‘—)) โˆฉ ๐ด) = (((,)โ€˜(๐บโ€˜๐‘˜)) โˆฉ ๐ด))
161160fveq2d 6847 . . . . . . . . . 10 (๐‘— = ๐‘˜ โ†’ (vol*โ€˜(((,)โ€˜(๐บโ€˜๐‘—)) โˆฉ ๐ด)) = (vol*โ€˜(((,)โ€˜(๐บโ€˜๐‘˜)) โˆฉ ๐ด)))
162159, 161oveq12d 7376 . . . . . . . . 9 (๐‘— = ๐‘˜ โ†’ (ฮฃ๐‘– โˆˆ (1...๐‘›)(vol*โ€˜(((,)โ€˜(๐นโ€˜๐‘–)) โˆฉ ((,)โ€˜(๐บโ€˜๐‘—)))) โˆ’ (vol*โ€˜(((,)โ€˜(๐บโ€˜๐‘—)) โˆฉ ๐ด))) = (ฮฃ๐‘ง โˆˆ (1...๐‘›)(vol*โ€˜(((,)โ€˜(๐นโ€˜๐‘ง)) โˆฉ ((,)โ€˜(๐บโ€˜๐‘˜)))) โˆ’ (vol*โ€˜(((,)โ€˜(๐บโ€˜๐‘˜)) โˆฉ ๐ด))))
163162fveq2d 6847 . . . . . . . 8 (๐‘— = ๐‘˜ โ†’ (absโ€˜(ฮฃ๐‘– โˆˆ (1...๐‘›)(vol*โ€˜(((,)โ€˜(๐นโ€˜๐‘–)) โˆฉ ((,)โ€˜(๐บโ€˜๐‘—)))) โˆ’ (vol*โ€˜(((,)โ€˜(๐บโ€˜๐‘—)) โˆฉ ๐ด)))) = (absโ€˜(ฮฃ๐‘ง โˆˆ (1...๐‘›)(vol*โ€˜(((,)โ€˜(๐นโ€˜๐‘ง)) โˆฉ ((,)โ€˜(๐บโ€˜๐‘˜)))) โˆ’ (vol*โ€˜(((,)โ€˜(๐บโ€˜๐‘˜)) โˆฉ ๐ด)))))
164163breq1d 5116 . . . . . . 7 (๐‘— = ๐‘˜ โ†’ ((absโ€˜(ฮฃ๐‘– โˆˆ (1...๐‘›)(vol*โ€˜(((,)โ€˜(๐นโ€˜๐‘–)) โˆฉ ((,)โ€˜(๐บโ€˜๐‘—)))) โˆ’ (vol*โ€˜(((,)โ€˜(๐บโ€˜๐‘—)) โˆฉ ๐ด)))) < (๐ถ / ๐‘š) โ†” (absโ€˜(ฮฃ๐‘ง โˆˆ (1...๐‘›)(vol*โ€˜(((,)โ€˜(๐นโ€˜๐‘ง)) โˆฉ ((,)โ€˜(๐บโ€˜๐‘˜)))) โˆ’ (vol*โ€˜(((,)โ€˜(๐บโ€˜๐‘˜)) โˆฉ ๐ด)))) < (๐ถ / ๐‘š)))
165164cbvralvw 3224 . . . . . 6 (โˆ€๐‘— โˆˆ (1...๐‘š)(absโ€˜(ฮฃ๐‘– โˆˆ (1...๐‘›)(vol*โ€˜(((,)โ€˜(๐นโ€˜๐‘–)) โˆฉ ((,)โ€˜(๐บโ€˜๐‘—)))) โˆ’ (vol*โ€˜(((,)โ€˜(๐บโ€˜๐‘—)) โˆฉ ๐ด)))) < (๐ถ / ๐‘š) โ†” โˆ€๐‘˜ โˆˆ (1...๐‘š)(absโ€˜(ฮฃ๐‘ง โˆˆ (1...๐‘›)(vol*โ€˜(((,)โ€˜(๐นโ€˜๐‘ง)) โˆฉ ((,)โ€˜(๐บโ€˜๐‘˜)))) โˆ’ (vol*โ€˜(((,)โ€˜(๐บโ€˜๐‘˜)) โˆฉ ๐ด)))) < (๐ถ / ๐‘š))
166150, 165sylib 217 . . . . 5 ((๐œ‘ โˆง ((๐‘š โˆˆ โ„• โˆง (absโ€˜((๐‘‡โ€˜๐‘š) โˆ’ sup(ran ๐‘‡, โ„*, < ))) < ๐ถ) โˆง (๐‘› โˆˆ โ„• โˆง โˆ€๐‘— โˆˆ (1...๐‘š)(absโ€˜(ฮฃ๐‘– โˆˆ (1...๐‘›)(vol*โ€˜(((,)โ€˜(๐นโ€˜๐‘–)) โˆฉ ((,)โ€˜(๐บโ€˜๐‘—)))) โˆ’ (vol*โ€˜(((,)โ€˜(๐บโ€˜๐‘—)) โˆฉ ๐ด)))) < (๐ถ / ๐‘š)))) โ†’ โˆ€๐‘˜ โˆˆ (1...๐‘š)(absโ€˜(ฮฃ๐‘ง โˆˆ (1...๐‘›)(vol*โ€˜(((,)โ€˜(๐นโ€˜๐‘ง)) โˆฉ ((,)โ€˜(๐บโ€˜๐‘˜)))) โˆ’ (vol*โ€˜(((,)โ€˜(๐บโ€˜๐‘˜)) โˆฉ ๐ด)))) < (๐ถ / ๐‘š))
167 eqid 2733 . . . . 5 โˆช (((,) โˆ˜ ๐น) โ€œ (1...๐‘›)) = โˆช (((,) โˆ˜ ๐น) โ€œ (1...๐‘›))
168139, 140, 18, 19, 141, 142, 143, 144, 5, 145, 146, 147, 148, 149, 166, 167uniioombllem5 24967 . . . 4 ((๐œ‘ โˆง ((๐‘š โˆˆ โ„• โˆง (absโ€˜((๐‘‡โ€˜๐‘š) โˆ’ sup(ran ๐‘‡, โ„*, < ))) < ๐ถ) โˆง (๐‘› โˆˆ โ„• โˆง โˆ€๐‘— โˆˆ (1...๐‘š)(absโ€˜(ฮฃ๐‘– โˆˆ (1...๐‘›)(vol*โ€˜(((,)โ€˜(๐นโ€˜๐‘–)) โˆฉ ((,)โ€˜(๐บโ€˜๐‘—)))) โˆ’ (vol*โ€˜(((,)โ€˜(๐บโ€˜๐‘—)) โˆฉ ๐ด)))) < (๐ถ / ๐‘š)))) โ†’ ((vol*โ€˜(๐ธ โˆฉ ๐ด)) + (vol*โ€˜(๐ธ โˆ– ๐ด))) โ‰ค ((vol*โ€˜๐ธ) + (4 ยท ๐ถ)))
169168anassrs 469 . . 3 (((๐œ‘ โˆง (๐‘š โˆˆ โ„• โˆง (absโ€˜((๐‘‡โ€˜๐‘š) โˆ’ sup(ran ๐‘‡, โ„*, < ))) < ๐ถ)) โˆง (๐‘› โˆˆ โ„• โˆง โˆ€๐‘— โˆˆ (1...๐‘š)(absโ€˜(ฮฃ๐‘– โˆˆ (1...๐‘›)(vol*โ€˜(((,)โ€˜(๐นโ€˜๐‘–)) โˆฉ ((,)โ€˜(๐บโ€˜๐‘—)))) โˆ’ (vol*โ€˜(((,)โ€˜(๐บโ€˜๐‘—)) โˆฉ ๐ด)))) < (๐ถ / ๐‘š))) โ†’ ((vol*โ€˜(๐ธ โˆฉ ๐ด)) + (vol*โ€˜(๐ธ โˆ– ๐ด))) โ‰ค ((vol*โ€˜๐ธ) + (4 ยท ๐ถ)))
170138, 169rexlimddv 3155 . 2 ((๐œ‘ โˆง (๐‘š โˆˆ โ„• โˆง (absโ€˜((๐‘‡โ€˜๐‘š) โˆ’ sup(ran ๐‘‡, โ„*, < ))) < ๐ถ)) โ†’ ((vol*โ€˜(๐ธ โˆฉ ๐ด)) + (vol*โ€˜(๐ธ โˆ– ๐ด))) โ‰ค ((vol*โ€˜๐ธ) + (4 ยท ๐ถ)))
17156, 170rexlimddv 3155 1 (๐œ‘ โ†’ ((vol*โ€˜(๐ธ โˆฉ ๐ด)) + (vol*โ€˜(๐ธ โˆ– ๐ด))) โ‰ค ((vol*โ€˜๐ธ) + (4 ยท ๐ถ)))
Colors of variables: wff setvar class
Syntax hints:   โ†’ wi 4   โ†” wb 205   โˆง wa 397   โˆง w3a 1088   = wceq 1542   โˆˆ wcel 2107   โ‰  wne 2940  โˆ€wral 3061  โˆƒwrex 3070  Vcvv 3444   โˆ– cdif 3908   โˆฉ cin 3910   โŠ† wss 3911  โˆ…c0 4283  ifcif 4487  โŸจcop 4593  โˆช cuni 4866  Disj wdisj 5071   class class class wbr 5106   โ†ฆ cmpt 5189   ร— cxp 5632  dom cdm 5634  ran crn 5635   โ€œ cima 5637   โˆ˜ ccom 5638   Fn wfn 6492  โŸถwf 6493  โ€˜cfv 6497  (class class class)co 7358  1st c1st 7920  2nd c2nd 7921  Fincfn 8886  supcsup 9381  infcinf 9382  โ„cr 11055  0cc0 11056  1c1 11057   + caddc 11059   ยท cmul 11061  +โˆžcpnf 11191  โ„*cxr 11193   < clt 11194   โ‰ค cle 11195   โˆ’ cmin 11390   / cdiv 11817  โ„•cn 12158  4c4 12215  โ„คcz 12504  โ„คโ‰ฅcuz 12768  โ„+crp 12920  (,)cioo 13270  [,)cico 13272  ...cfz 13430  seqcseq 13912  abscabs 15125   โ‡ cli 15372  ฮฃcsu 15576  vol*covol 24842
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-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
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-nul 4284  df-if 4488  df-pw 4563  df-sn 4588  df-pr 4590  df-op 4594  df-uni 4867  df-int 4909  df-iun 4957  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-om 7804  df-1st 7922  df-2nd 7923  df-frecs 8213  df-wrecs 8244  df-recs 8318  df-rdg 8357  df-1o 8413  df-2o 8414  df-er 8651  df-map 8770  df-pm 8771  df-en 8887  df-dom 8888  df-sdom 8889  df-fin 8890  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-n0 12419  df-z 12505  df-uz 12769  df-q 12879  df-rp 12921  df-xneg 13038  df-xadd 13039  df-xmul 13040  df-ioo 13274  df-ico 13276  df-icc 13277  df-fz 13431  df-fzo 13574  df-fl 13703  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-clim 15376  df-rlim 15377  df-sum 15577  df-rest 17309  df-topgen 17330  df-psmet 20804  df-xmet 20805  df-met 20806  df-bl 20807  df-mopn 20808  df-top 22259  df-topon 22276  df-bases 22312  df-cmp 22754  df-ovol 24844  df-vol 24845
This theorem is referenced by:  uniioombl  24969
  Copyright terms: Public domain W3C validator