Metamath Proof Explorer


Theorem uniioombllem4

Description: Lemma for uniioombl . (Contributed by Mario Carneiro, 26-Mar-2015)

Ref Expression
Hypotheses uniioombl.1 โŠข ( ๐œ‘ โ†’ ๐น : โ„• โŸถ ( โ‰ค โˆฉ ( โ„ ร— โ„ ) ) )
uniioombl.2 โŠข ( ๐œ‘ โ†’ Disj ๐‘ฅ โˆˆ โ„• ( (,) โ€˜ ( ๐น โ€˜ ๐‘ฅ ) ) )
uniioombl.3 โŠข ๐‘† = seq 1 ( + , ( ( abs โˆ˜ โˆ’ ) โˆ˜ ๐น ) )
uniioombl.a โŠข ๐ด = โˆช ran ( (,) โˆ˜ ๐น )
uniioombl.e โŠข ( ๐œ‘ โ†’ ( vol* โ€˜ ๐ธ ) โˆˆ โ„ )
uniioombl.c โŠข ( ๐œ‘ โ†’ ๐ถ โˆˆ โ„+ )
uniioombl.g โŠข ( ๐œ‘ โ†’ ๐บ : โ„• โŸถ ( โ‰ค โˆฉ ( โ„ ร— โ„ ) ) )
uniioombl.s โŠข ( ๐œ‘ โ†’ ๐ธ โІ โˆช ran ( (,) โˆ˜ ๐บ ) )
uniioombl.t โŠข ๐‘‡ = seq 1 ( + , ( ( abs โˆ˜ โˆ’ ) โˆ˜ ๐บ ) )
uniioombl.v โŠข ( ๐œ‘ โ†’ sup ( ran ๐‘‡ , โ„* , < ) โ‰ค ( ( vol* โ€˜ ๐ธ ) + ๐ถ ) )
uniioombl.m โŠข ( ๐œ‘ โ†’ ๐‘€ โˆˆ โ„• )
uniioombl.m2 โŠข ( ๐œ‘ โ†’ ( abs โ€˜ ( ( ๐‘‡ โ€˜ ๐‘€ ) โˆ’ sup ( ran ๐‘‡ , โ„* , < ) ) ) < ๐ถ )
uniioombl.k โŠข ๐พ = โˆช ( ( (,) โˆ˜ ๐บ ) โ€œ ( 1 ... ๐‘€ ) )
uniioombl.n โŠข ( ๐œ‘ โ†’ ๐‘ โˆˆ โ„• )
uniioombl.n2 โŠข ( ๐œ‘ โ†’ โˆ€ ๐‘— โˆˆ ( 1 ... ๐‘€ ) ( abs โ€˜ ( ฮฃ ๐‘– โˆˆ ( 1 ... ๐‘ ) ( vol* โ€˜ ( ( (,) โ€˜ ( ๐น โ€˜ ๐‘– ) ) โˆฉ ( (,) โ€˜ ( ๐บ โ€˜ ๐‘— ) ) ) ) โˆ’ ( vol* โ€˜ ( ( (,) โ€˜ ( ๐บ โ€˜ ๐‘— ) ) โˆฉ ๐ด ) ) ) ) < ( ๐ถ / ๐‘€ ) )
uniioombl.l โŠข ๐ฟ = โˆช ( ( (,) โˆ˜ ๐น ) โ€œ ( 1 ... ๐‘ ) )
Assertion uniioombllem4 ( ๐œ‘ โ†’ ( vol* โ€˜ ( ๐พ โˆฉ ๐ด ) ) โ‰ค ( ( vol* โ€˜ ( ๐พ โˆฉ ๐ฟ ) ) + ๐ถ ) )

Proof

Step Hyp Ref Expression
1 uniioombl.1 โŠข ( ๐œ‘ โ†’ ๐น : โ„• โŸถ ( โ‰ค โˆฉ ( โ„ ร— โ„ ) ) )
2 uniioombl.2 โŠข ( ๐œ‘ โ†’ Disj ๐‘ฅ โˆˆ โ„• ( (,) โ€˜ ( ๐น โ€˜ ๐‘ฅ ) ) )
3 uniioombl.3 โŠข ๐‘† = seq 1 ( + , ( ( abs โˆ˜ โˆ’ ) โˆ˜ ๐น ) )
4 uniioombl.a โŠข ๐ด = โˆช ran ( (,) โˆ˜ ๐น )
5 uniioombl.e โŠข ( ๐œ‘ โ†’ ( vol* โ€˜ ๐ธ ) โˆˆ โ„ )
6 uniioombl.c โŠข ( ๐œ‘ โ†’ ๐ถ โˆˆ โ„+ )
7 uniioombl.g โŠข ( ๐œ‘ โ†’ ๐บ : โ„• โŸถ ( โ‰ค โˆฉ ( โ„ ร— โ„ ) ) )
8 uniioombl.s โŠข ( ๐œ‘ โ†’ ๐ธ โІ โˆช ran ( (,) โˆ˜ ๐บ ) )
9 uniioombl.t โŠข ๐‘‡ = seq 1 ( + , ( ( abs โˆ˜ โˆ’ ) โˆ˜ ๐บ ) )
10 uniioombl.v โŠข ( ๐œ‘ โ†’ sup ( ran ๐‘‡ , โ„* , < ) โ‰ค ( ( vol* โ€˜ ๐ธ ) + ๐ถ ) )
11 uniioombl.m โŠข ( ๐œ‘ โ†’ ๐‘€ โˆˆ โ„• )
12 uniioombl.m2 โŠข ( ๐œ‘ โ†’ ( abs โ€˜ ( ( ๐‘‡ โ€˜ ๐‘€ ) โˆ’ sup ( ran ๐‘‡ , โ„* , < ) ) ) < ๐ถ )
13 uniioombl.k โŠข ๐พ = โˆช ( ( (,) โˆ˜ ๐บ ) โ€œ ( 1 ... ๐‘€ ) )
14 uniioombl.n โŠข ( ๐œ‘ โ†’ ๐‘ โˆˆ โ„• )
15 uniioombl.n2 โŠข ( ๐œ‘ โ†’ โˆ€ ๐‘— โˆˆ ( 1 ... ๐‘€ ) ( abs โ€˜ ( ฮฃ ๐‘– โˆˆ ( 1 ... ๐‘ ) ( vol* โ€˜ ( ( (,) โ€˜ ( ๐น โ€˜ ๐‘– ) ) โˆฉ ( (,) โ€˜ ( ๐บ โ€˜ ๐‘— ) ) ) ) โˆ’ ( vol* โ€˜ ( ( (,) โ€˜ ( ๐บ โ€˜ ๐‘— ) ) โˆฉ ๐ด ) ) ) ) < ( ๐ถ / ๐‘€ ) )
16 uniioombl.l โŠข ๐ฟ = โˆช ( ( (,) โˆ˜ ๐น ) โ€œ ( 1 ... ๐‘ ) )
17 inss1 โŠข ( ๐พ โˆฉ ๐ด ) โІ ๐พ
18 imassrn โŠข ( ( (,) โˆ˜ ๐บ ) โ€œ ( 1 ... ๐‘€ ) ) โІ ran ( (,) โˆ˜ ๐บ )
19 18 unissi โŠข โˆช ( ( (,) โˆ˜ ๐บ ) โ€œ ( 1 ... ๐‘€ ) ) โІ โˆช ran ( (,) โˆ˜ ๐บ )
20 13 19 eqsstri โŠข ๐พ โІ โˆช ran ( (,) โˆ˜ ๐บ )
21 7 uniiccdif โŠข ( ๐œ‘ โ†’ ( โˆช ran ( (,) โˆ˜ ๐บ ) โІ โˆช ran ( [,] โˆ˜ ๐บ ) โˆง ( vol* โ€˜ ( โˆช ran ( [,] โˆ˜ ๐บ ) โˆ– โˆช ran ( (,) โˆ˜ ๐บ ) ) ) = 0 ) )
22 21 simpld โŠข ( ๐œ‘ โ†’ โˆช ran ( (,) โˆ˜ ๐บ ) โІ โˆช ran ( [,] โˆ˜ ๐บ ) )
23 ovolficcss โŠข ( ๐บ : โ„• โŸถ ( โ‰ค โˆฉ ( โ„ ร— โ„ ) ) โ†’ โˆช ran ( [,] โˆ˜ ๐บ ) โІ โ„ )
24 7 23 syl โŠข ( ๐œ‘ โ†’ โˆช ran ( [,] โˆ˜ ๐บ ) โІ โ„ )
25 22 24 sstrd โŠข ( ๐œ‘ โ†’ โˆช ran ( (,) โˆ˜ ๐บ ) โІ โ„ )
26 20 25 sstrid โŠข ( ๐œ‘ โ†’ ๐พ โІ โ„ )
27 1 2 3 4 5 6 7 8 9 10 uniioombllem1 โŠข ( ๐œ‘ โ†’ sup ( ran ๐‘‡ , โ„* , < ) โˆˆ โ„ )
28 ssid โŠข โˆช ran ( (,) โˆ˜ ๐บ ) โІ โˆช ran ( (,) โˆ˜ ๐บ )
29 9 ovollb โŠข ( ( ๐บ : โ„• โŸถ ( โ‰ค โˆฉ ( โ„ ร— โ„ ) ) โˆง โˆช ran ( (,) โˆ˜ ๐บ ) โІ โˆช ran ( (,) โˆ˜ ๐บ ) ) โ†’ ( vol* โ€˜ โˆช ran ( (,) โˆ˜ ๐บ ) ) โ‰ค sup ( ran ๐‘‡ , โ„* , < ) )
30 7 28 29 sylancl โŠข ( ๐œ‘ โ†’ ( vol* โ€˜ โˆช ran ( (,) โˆ˜ ๐บ ) ) โ‰ค sup ( ran ๐‘‡ , โ„* , < ) )
31 ovollecl โŠข ( ( โˆช ran ( (,) โˆ˜ ๐บ ) โІ โ„ โˆง sup ( ran ๐‘‡ , โ„* , < ) โˆˆ โ„ โˆง ( vol* โ€˜ โˆช ran ( (,) โˆ˜ ๐บ ) ) โ‰ค sup ( ran ๐‘‡ , โ„* , < ) ) โ†’ ( vol* โ€˜ โˆช ran ( (,) โˆ˜ ๐บ ) ) โˆˆ โ„ )
32 25 27 30 31 syl3anc โŠข ( ๐œ‘ โ†’ ( vol* โ€˜ โˆช ran ( (,) โˆ˜ ๐บ ) ) โˆˆ โ„ )
33 ovolsscl โŠข ( ( ๐พ โІ โˆช ran ( (,) โˆ˜ ๐บ ) โˆง โˆช ran ( (,) โˆ˜ ๐บ ) โІ โ„ โˆง ( vol* โ€˜ โˆช ran ( (,) โˆ˜ ๐บ ) ) โˆˆ โ„ ) โ†’ ( vol* โ€˜ ๐พ ) โˆˆ โ„ )
34 20 25 32 33 mp3an2i โŠข ( ๐œ‘ โ†’ ( vol* โ€˜ ๐พ ) โˆˆ โ„ )
35 ovolsscl โŠข ( ( ( ๐พ โˆฉ ๐ด ) โІ ๐พ โˆง ๐พ โІ โ„ โˆง ( vol* โ€˜ ๐พ ) โˆˆ โ„ ) โ†’ ( vol* โ€˜ ( ๐พ โˆฉ ๐ด ) ) โˆˆ โ„ )
36 17 26 34 35 mp3an2i โŠข ( ๐œ‘ โ†’ ( vol* โ€˜ ( ๐พ โˆฉ ๐ด ) ) โˆˆ โ„ )
37 inss1 โŠข ( ๐พ โˆฉ ๐ฟ ) โІ ๐พ
38 ovolsscl โŠข ( ( ( ๐พ โˆฉ ๐ฟ ) โІ ๐พ โˆง ๐พ โІ โ„ โˆง ( vol* โ€˜ ๐พ ) โˆˆ โ„ ) โ†’ ( vol* โ€˜ ( ๐พ โˆฉ ๐ฟ ) ) โˆˆ โ„ )
39 37 26 34 38 mp3an2i โŠข ( ๐œ‘ โ†’ ( vol* โ€˜ ( ๐พ โˆฉ ๐ฟ ) ) โˆˆ โ„ )
40 ssun2 โŠข โˆช ๐‘— โˆˆ ( 1 ... ๐‘€ ) โˆช ๐‘– โˆˆ ( โ„คโ‰ฅ โ€˜ ( ๐‘ + 1 ) ) ( ( (,) โ€˜ ( ๐น โ€˜ ๐‘– ) ) โˆฉ ( (,) โ€˜ ( ๐บ โ€˜ ๐‘— ) ) ) โІ ( ( ๐พ โˆฉ ๐ฟ ) โˆช โˆช ๐‘— โˆˆ ( 1 ... ๐‘€ ) โˆช ๐‘– โˆˆ ( โ„คโ‰ฅ โ€˜ ( ๐‘ + 1 ) ) ( ( (,) โ€˜ ( ๐น โ€˜ ๐‘– ) ) โˆฉ ( (,) โ€˜ ( ๐บ โ€˜ ๐‘— ) ) ) )
41 nnuz โŠข โ„• = ( โ„คโ‰ฅ โ€˜ 1 )
42 14 peano2nnd โŠข ( ๐œ‘ โ†’ ( ๐‘ + 1 ) โˆˆ โ„• )
43 42 41 eleqtrdi โŠข ( ๐œ‘ โ†’ ( ๐‘ + 1 ) โˆˆ ( โ„คโ‰ฅ โ€˜ 1 ) )
44 uzsplit โŠข ( ( ๐‘ + 1 ) โˆˆ ( โ„คโ‰ฅ โ€˜ 1 ) โ†’ ( โ„คโ‰ฅ โ€˜ 1 ) = ( ( 1 ... ( ( ๐‘ + 1 ) โˆ’ 1 ) ) โˆช ( โ„คโ‰ฅ โ€˜ ( ๐‘ + 1 ) ) ) )
45 43 44 syl โŠข ( ๐œ‘ โ†’ ( โ„คโ‰ฅ โ€˜ 1 ) = ( ( 1 ... ( ( ๐‘ + 1 ) โˆ’ 1 ) ) โˆช ( โ„คโ‰ฅ โ€˜ ( ๐‘ + 1 ) ) ) )
46 41 45 eqtrid โŠข ( ๐œ‘ โ†’ โ„• = ( ( 1 ... ( ( ๐‘ + 1 ) โˆ’ 1 ) ) โˆช ( โ„คโ‰ฅ โ€˜ ( ๐‘ + 1 ) ) ) )
47 14 nncnd โŠข ( ๐œ‘ โ†’ ๐‘ โˆˆ โ„‚ )
48 ax-1cn โŠข 1 โˆˆ โ„‚
49 pncan โŠข ( ( ๐‘ โˆˆ โ„‚ โˆง 1 โˆˆ โ„‚ ) โ†’ ( ( ๐‘ + 1 ) โˆ’ 1 ) = ๐‘ )
50 47 48 49 sylancl โŠข ( ๐œ‘ โ†’ ( ( ๐‘ + 1 ) โˆ’ 1 ) = ๐‘ )
51 50 oveq2d โŠข ( ๐œ‘ โ†’ ( 1 ... ( ( ๐‘ + 1 ) โˆ’ 1 ) ) = ( 1 ... ๐‘ ) )
52 51 uneq1d โŠข ( ๐œ‘ โ†’ ( ( 1 ... ( ( ๐‘ + 1 ) โˆ’ 1 ) ) โˆช ( โ„คโ‰ฅ โ€˜ ( ๐‘ + 1 ) ) ) = ( ( 1 ... ๐‘ ) โˆช ( โ„คโ‰ฅ โ€˜ ( ๐‘ + 1 ) ) ) )
53 46 52 eqtrd โŠข ( ๐œ‘ โ†’ โ„• = ( ( 1 ... ๐‘ ) โˆช ( โ„คโ‰ฅ โ€˜ ( ๐‘ + 1 ) ) ) )
54 53 iuneq1d โŠข ( ๐œ‘ โ†’ โˆช ๐‘– โˆˆ โ„• ( (,) โ€˜ ( ๐น โ€˜ ๐‘– ) ) = โˆช ๐‘– โˆˆ ( ( 1 ... ๐‘ ) โˆช ( โ„คโ‰ฅ โ€˜ ( ๐‘ + 1 ) ) ) ( (,) โ€˜ ( ๐น โ€˜ ๐‘– ) ) )
55 iunxun โŠข โˆช ๐‘– โˆˆ ( ( 1 ... ๐‘ ) โˆช ( โ„คโ‰ฅ โ€˜ ( ๐‘ + 1 ) ) ) ( (,) โ€˜ ( ๐น โ€˜ ๐‘– ) ) = ( โˆช ๐‘– โˆˆ ( 1 ... ๐‘ ) ( (,) โ€˜ ( ๐น โ€˜ ๐‘– ) ) โˆช โˆช ๐‘– โˆˆ ( โ„คโ‰ฅ โ€˜ ( ๐‘ + 1 ) ) ( (,) โ€˜ ( ๐น โ€˜ ๐‘– ) ) )
56 54 55 eqtrdi โŠข ( ๐œ‘ โ†’ โˆช ๐‘– โˆˆ โ„• ( (,) โ€˜ ( ๐น โ€˜ ๐‘– ) ) = ( โˆช ๐‘– โˆˆ ( 1 ... ๐‘ ) ( (,) โ€˜ ( ๐น โ€˜ ๐‘– ) ) โˆช โˆช ๐‘– โˆˆ ( โ„คโ‰ฅ โ€˜ ( ๐‘ + 1 ) ) ( (,) โ€˜ ( ๐น โ€˜ ๐‘– ) ) ) )
57 ioof โŠข (,) : ( โ„* ร— โ„* ) โŸถ ๐’ซ โ„
58 inss2 โŠข ( โ‰ค โˆฉ ( โ„ ร— โ„ ) ) โІ ( โ„ ร— โ„ )
59 rexpssxrxp โŠข ( โ„ ร— โ„ ) โІ ( โ„* ร— โ„* )
60 58 59 sstri โŠข ( โ‰ค โˆฉ ( โ„ ร— โ„ ) ) โІ ( โ„* ร— โ„* )
61 fss โŠข ( ( ๐น : โ„• โŸถ ( โ‰ค โˆฉ ( โ„ ร— โ„ ) ) โˆง ( โ‰ค โˆฉ ( โ„ ร— โ„ ) ) โІ ( โ„* ร— โ„* ) ) โ†’ ๐น : โ„• โŸถ ( โ„* ร— โ„* ) )
62 1 60 61 sylancl โŠข ( ๐œ‘ โ†’ ๐น : โ„• โŸถ ( โ„* ร— โ„* ) )
63 fco โŠข ( ( (,) : ( โ„* ร— โ„* ) โŸถ ๐’ซ โ„ โˆง ๐น : โ„• โŸถ ( โ„* ร— โ„* ) ) โ†’ ( (,) โˆ˜ ๐น ) : โ„• โŸถ ๐’ซ โ„ )
64 57 62 63 sylancr โŠข ( ๐œ‘ โ†’ ( (,) โˆ˜ ๐น ) : โ„• โŸถ ๐’ซ โ„ )
65 ffn โŠข ( ( (,) โˆ˜ ๐น ) : โ„• โŸถ ๐’ซ โ„ โ†’ ( (,) โˆ˜ ๐น ) Fn โ„• )
66 fniunfv โŠข ( ( (,) โˆ˜ ๐น ) Fn โ„• โ†’ โˆช ๐‘– โˆˆ โ„• ( ( (,) โˆ˜ ๐น ) โ€˜ ๐‘– ) = โˆช ran ( (,) โˆ˜ ๐น ) )
67 64 65 66 3syl โŠข ( ๐œ‘ โ†’ โˆช ๐‘– โˆˆ โ„• ( ( (,) โˆ˜ ๐น ) โ€˜ ๐‘– ) = โˆช ran ( (,) โˆ˜ ๐น ) )
68 fvco3 โŠข ( ( ๐น : โ„• โŸถ ( โ‰ค โˆฉ ( โ„ ร— โ„ ) ) โˆง ๐‘– โˆˆ โ„• ) โ†’ ( ( (,) โˆ˜ ๐น ) โ€˜ ๐‘– ) = ( (,) โ€˜ ( ๐น โ€˜ ๐‘– ) ) )
69 1 68 sylan โŠข ( ( ๐œ‘ โˆง ๐‘– โˆˆ โ„• ) โ†’ ( ( (,) โˆ˜ ๐น ) โ€˜ ๐‘– ) = ( (,) โ€˜ ( ๐น โ€˜ ๐‘– ) ) )
70 69 iuneq2dv โŠข ( ๐œ‘ โ†’ โˆช ๐‘– โˆˆ โ„• ( ( (,) โˆ˜ ๐น ) โ€˜ ๐‘– ) = โˆช ๐‘– โˆˆ โ„• ( (,) โ€˜ ( ๐น โ€˜ ๐‘– ) ) )
71 67 70 eqtr3d โŠข ( ๐œ‘ โ†’ โˆช ran ( (,) โˆ˜ ๐น ) = โˆช ๐‘– โˆˆ โ„• ( (,) โ€˜ ( ๐น โ€˜ ๐‘– ) ) )
72 4 71 eqtrid โŠข ( ๐œ‘ โ†’ ๐ด = โˆช ๐‘– โˆˆ โ„• ( (,) โ€˜ ( ๐น โ€˜ ๐‘– ) ) )
73 ffun โŠข ( ( (,) โˆ˜ ๐น ) : โ„• โŸถ ๐’ซ โ„ โ†’ Fun ( (,) โˆ˜ ๐น ) )
74 funiunfv โŠข ( Fun ( (,) โˆ˜ ๐น ) โ†’ โˆช ๐‘– โˆˆ ( 1 ... ๐‘ ) ( ( (,) โˆ˜ ๐น ) โ€˜ ๐‘– ) = โˆช ( ( (,) โˆ˜ ๐น ) โ€œ ( 1 ... ๐‘ ) ) )
75 64 73 74 3syl โŠข ( ๐œ‘ โ†’ โˆช ๐‘– โˆˆ ( 1 ... ๐‘ ) ( ( (,) โˆ˜ ๐น ) โ€˜ ๐‘– ) = โˆช ( ( (,) โˆ˜ ๐น ) โ€œ ( 1 ... ๐‘ ) ) )
76 elfznn โŠข ( ๐‘– โˆˆ ( 1 ... ๐‘ ) โ†’ ๐‘– โˆˆ โ„• )
77 1 76 68 syl2an โŠข ( ( ๐œ‘ โˆง ๐‘– โˆˆ ( 1 ... ๐‘ ) ) โ†’ ( ( (,) โˆ˜ ๐น ) โ€˜ ๐‘– ) = ( (,) โ€˜ ( ๐น โ€˜ ๐‘– ) ) )
78 77 iuneq2dv โŠข ( ๐œ‘ โ†’ โˆช ๐‘– โˆˆ ( 1 ... ๐‘ ) ( ( (,) โˆ˜ ๐น ) โ€˜ ๐‘– ) = โˆช ๐‘– โˆˆ ( 1 ... ๐‘ ) ( (,) โ€˜ ( ๐น โ€˜ ๐‘– ) ) )
79 75 78 eqtr3d โŠข ( ๐œ‘ โ†’ โˆช ( ( (,) โˆ˜ ๐น ) โ€œ ( 1 ... ๐‘ ) ) = โˆช ๐‘– โˆˆ ( 1 ... ๐‘ ) ( (,) โ€˜ ( ๐น โ€˜ ๐‘– ) ) )
80 16 79 eqtrid โŠข ( ๐œ‘ โ†’ ๐ฟ = โˆช ๐‘– โˆˆ ( 1 ... ๐‘ ) ( (,) โ€˜ ( ๐น โ€˜ ๐‘– ) ) )
81 80 uneq1d โŠข ( ๐œ‘ โ†’ ( ๐ฟ โˆช โˆช ๐‘– โˆˆ ( โ„คโ‰ฅ โ€˜ ( ๐‘ + 1 ) ) ( (,) โ€˜ ( ๐น โ€˜ ๐‘– ) ) ) = ( โˆช ๐‘– โˆˆ ( 1 ... ๐‘ ) ( (,) โ€˜ ( ๐น โ€˜ ๐‘– ) ) โˆช โˆช ๐‘– โˆˆ ( โ„คโ‰ฅ โ€˜ ( ๐‘ + 1 ) ) ( (,) โ€˜ ( ๐น โ€˜ ๐‘– ) ) ) )
82 56 72 81 3eqtr4d โŠข ( ๐œ‘ โ†’ ๐ด = ( ๐ฟ โˆช โˆช ๐‘– โˆˆ ( โ„คโ‰ฅ โ€˜ ( ๐‘ + 1 ) ) ( (,) โ€˜ ( ๐น โ€˜ ๐‘– ) ) ) )
83 82 ineq2d โŠข ( ๐œ‘ โ†’ ( ๐พ โˆฉ ๐ด ) = ( ๐พ โˆฉ ( ๐ฟ โˆช โˆช ๐‘– โˆˆ ( โ„คโ‰ฅ โ€˜ ( ๐‘ + 1 ) ) ( (,) โ€˜ ( ๐น โ€˜ ๐‘– ) ) ) ) )
84 indi โŠข ( ๐พ โˆฉ ( ๐ฟ โˆช โˆช ๐‘– โˆˆ ( โ„คโ‰ฅ โ€˜ ( ๐‘ + 1 ) ) ( (,) โ€˜ ( ๐น โ€˜ ๐‘– ) ) ) ) = ( ( ๐พ โˆฉ ๐ฟ ) โˆช ( ๐พ โˆฉ โˆช ๐‘– โˆˆ ( โ„คโ‰ฅ โ€˜ ( ๐‘ + 1 ) ) ( (,) โ€˜ ( ๐น โ€˜ ๐‘– ) ) ) )
85 83 84 eqtrdi โŠข ( ๐œ‘ โ†’ ( ๐พ โˆฉ ๐ด ) = ( ( ๐พ โˆฉ ๐ฟ ) โˆช ( ๐พ โˆฉ โˆช ๐‘– โˆˆ ( โ„คโ‰ฅ โ€˜ ( ๐‘ + 1 ) ) ( (,) โ€˜ ( ๐น โ€˜ ๐‘– ) ) ) ) )
86 fss โŠข ( ( ๐บ : โ„• โŸถ ( โ‰ค โˆฉ ( โ„ ร— โ„ ) ) โˆง ( โ‰ค โˆฉ ( โ„ ร— โ„ ) ) โІ ( โ„* ร— โ„* ) ) โ†’ ๐บ : โ„• โŸถ ( โ„* ร— โ„* ) )
87 7 60 86 sylancl โŠข ( ๐œ‘ โ†’ ๐บ : โ„• โŸถ ( โ„* ร— โ„* ) )
88 fco โŠข ( ( (,) : ( โ„* ร— โ„* ) โŸถ ๐’ซ โ„ โˆง ๐บ : โ„• โŸถ ( โ„* ร— โ„* ) ) โ†’ ( (,) โˆ˜ ๐บ ) : โ„• โŸถ ๐’ซ โ„ )
89 57 87 88 sylancr โŠข ( ๐œ‘ โ†’ ( (,) โˆ˜ ๐บ ) : โ„• โŸถ ๐’ซ โ„ )
90 ffun โŠข ( ( (,) โˆ˜ ๐บ ) : โ„• โŸถ ๐’ซ โ„ โ†’ Fun ( (,) โˆ˜ ๐บ ) )
91 funiunfv โŠข ( Fun ( (,) โˆ˜ ๐บ ) โ†’ โˆช ๐‘— โˆˆ ( 1 ... ๐‘€ ) ( ( (,) โˆ˜ ๐บ ) โ€˜ ๐‘— ) = โˆช ( ( (,) โˆ˜ ๐บ ) โ€œ ( 1 ... ๐‘€ ) ) )
92 89 90 91 3syl โŠข ( ๐œ‘ โ†’ โˆช ๐‘— โˆˆ ( 1 ... ๐‘€ ) ( ( (,) โˆ˜ ๐บ ) โ€˜ ๐‘— ) = โˆช ( ( (,) โˆ˜ ๐บ ) โ€œ ( 1 ... ๐‘€ ) ) )
93 elfznn โŠข ( ๐‘— โˆˆ ( 1 ... ๐‘€ ) โ†’ ๐‘— โˆˆ โ„• )
94 fvco3 โŠข ( ( ๐บ : โ„• โŸถ ( โ‰ค โˆฉ ( โ„ ร— โ„ ) ) โˆง ๐‘— โˆˆ โ„• ) โ†’ ( ( (,) โˆ˜ ๐บ ) โ€˜ ๐‘— ) = ( (,) โ€˜ ( ๐บ โ€˜ ๐‘— ) ) )
95 7 93 94 syl2an โŠข ( ( ๐œ‘ โˆง ๐‘— โˆˆ ( 1 ... ๐‘€ ) ) โ†’ ( ( (,) โˆ˜ ๐บ ) โ€˜ ๐‘— ) = ( (,) โ€˜ ( ๐บ โ€˜ ๐‘— ) ) )
96 95 iuneq2dv โŠข ( ๐œ‘ โ†’ โˆช ๐‘— โˆˆ ( 1 ... ๐‘€ ) ( ( (,) โˆ˜ ๐บ ) โ€˜ ๐‘— ) = โˆช ๐‘— โˆˆ ( 1 ... ๐‘€ ) ( (,) โ€˜ ( ๐บ โ€˜ ๐‘— ) ) )
97 92 96 eqtr3d โŠข ( ๐œ‘ โ†’ โˆช ( ( (,) โˆ˜ ๐บ ) โ€œ ( 1 ... ๐‘€ ) ) = โˆช ๐‘— โˆˆ ( 1 ... ๐‘€ ) ( (,) โ€˜ ( ๐บ โ€˜ ๐‘— ) ) )
98 13 97 eqtrid โŠข ( ๐œ‘ โ†’ ๐พ = โˆช ๐‘— โˆˆ ( 1 ... ๐‘€ ) ( (,) โ€˜ ( ๐บ โ€˜ ๐‘— ) ) )
99 98 ineq2d โŠข ( ๐œ‘ โ†’ ( โˆช ๐‘– โˆˆ ( โ„คโ‰ฅ โ€˜ ( ๐‘ + 1 ) ) ( (,) โ€˜ ( ๐น โ€˜ ๐‘– ) ) โˆฉ ๐พ ) = ( โˆช ๐‘– โˆˆ ( โ„คโ‰ฅ โ€˜ ( ๐‘ + 1 ) ) ( (,) โ€˜ ( ๐น โ€˜ ๐‘– ) ) โˆฉ โˆช ๐‘— โˆˆ ( 1 ... ๐‘€ ) ( (,) โ€˜ ( ๐บ โ€˜ ๐‘— ) ) ) )
100 incom โŠข ( ๐พ โˆฉ โˆช ๐‘– โˆˆ ( โ„คโ‰ฅ โ€˜ ( ๐‘ + 1 ) ) ( (,) โ€˜ ( ๐น โ€˜ ๐‘– ) ) ) = ( โˆช ๐‘– โˆˆ ( โ„คโ‰ฅ โ€˜ ( ๐‘ + 1 ) ) ( (,) โ€˜ ( ๐น โ€˜ ๐‘– ) ) โˆฉ ๐พ )
101 iunin2 โŠข โˆช ๐‘– โˆˆ ( โ„คโ‰ฅ โ€˜ ( ๐‘ + 1 ) ) ( ( (,) โ€˜ ( ๐บ โ€˜ ๐‘— ) ) โˆฉ ( (,) โ€˜ ( ๐น โ€˜ ๐‘– ) ) ) = ( ( (,) โ€˜ ( ๐บ โ€˜ ๐‘— ) ) โˆฉ โˆช ๐‘– โˆˆ ( โ„คโ‰ฅ โ€˜ ( ๐‘ + 1 ) ) ( (,) โ€˜ ( ๐น โ€˜ ๐‘– ) ) )
102 incom โŠข ( ( (,) โ€˜ ( ๐น โ€˜ ๐‘– ) ) โˆฉ ( (,) โ€˜ ( ๐บ โ€˜ ๐‘— ) ) ) = ( ( (,) โ€˜ ( ๐บ โ€˜ ๐‘— ) ) โˆฉ ( (,) โ€˜ ( ๐น โ€˜ ๐‘– ) ) )
103 102 a1i โŠข ( ๐‘– โˆˆ ( โ„คโ‰ฅ โ€˜ ( ๐‘ + 1 ) ) โ†’ ( ( (,) โ€˜ ( ๐น โ€˜ ๐‘– ) ) โˆฉ ( (,) โ€˜ ( ๐บ โ€˜ ๐‘— ) ) ) = ( ( (,) โ€˜ ( ๐บ โ€˜ ๐‘— ) ) โˆฉ ( (,) โ€˜ ( ๐น โ€˜ ๐‘– ) ) ) )
104 103 iuneq2i โŠข โˆช ๐‘– โˆˆ ( โ„คโ‰ฅ โ€˜ ( ๐‘ + 1 ) ) ( ( (,) โ€˜ ( ๐น โ€˜ ๐‘– ) ) โˆฉ ( (,) โ€˜ ( ๐บ โ€˜ ๐‘— ) ) ) = โˆช ๐‘– โˆˆ ( โ„คโ‰ฅ โ€˜ ( ๐‘ + 1 ) ) ( ( (,) โ€˜ ( ๐บ โ€˜ ๐‘— ) ) โˆฉ ( (,) โ€˜ ( ๐น โ€˜ ๐‘– ) ) )
105 incom โŠข ( โˆช ๐‘– โˆˆ ( โ„คโ‰ฅ โ€˜ ( ๐‘ + 1 ) ) ( (,) โ€˜ ( ๐น โ€˜ ๐‘– ) ) โˆฉ ( (,) โ€˜ ( ๐บ โ€˜ ๐‘— ) ) ) = ( ( (,) โ€˜ ( ๐บ โ€˜ ๐‘— ) ) โˆฉ โˆช ๐‘– โˆˆ ( โ„คโ‰ฅ โ€˜ ( ๐‘ + 1 ) ) ( (,) โ€˜ ( ๐น โ€˜ ๐‘– ) ) )
106 101 104 105 3eqtr4ri โŠข ( โˆช ๐‘– โˆˆ ( โ„คโ‰ฅ โ€˜ ( ๐‘ + 1 ) ) ( (,) โ€˜ ( ๐น โ€˜ ๐‘– ) ) โˆฉ ( (,) โ€˜ ( ๐บ โ€˜ ๐‘— ) ) ) = โˆช ๐‘– โˆˆ ( โ„คโ‰ฅ โ€˜ ( ๐‘ + 1 ) ) ( ( (,) โ€˜ ( ๐น โ€˜ ๐‘– ) ) โˆฉ ( (,) โ€˜ ( ๐บ โ€˜ ๐‘— ) ) )
107 106 a1i โŠข ( ๐‘— โˆˆ ( 1 ... ๐‘€ ) โ†’ ( โˆช ๐‘– โˆˆ ( โ„คโ‰ฅ โ€˜ ( ๐‘ + 1 ) ) ( (,) โ€˜ ( ๐น โ€˜ ๐‘– ) ) โˆฉ ( (,) โ€˜ ( ๐บ โ€˜ ๐‘— ) ) ) = โˆช ๐‘– โˆˆ ( โ„คโ‰ฅ โ€˜ ( ๐‘ + 1 ) ) ( ( (,) โ€˜ ( ๐น โ€˜ ๐‘– ) ) โˆฉ ( (,) โ€˜ ( ๐บ โ€˜ ๐‘— ) ) ) )
108 107 iuneq2i โŠข โˆช ๐‘— โˆˆ ( 1 ... ๐‘€ ) ( โˆช ๐‘– โˆˆ ( โ„คโ‰ฅ โ€˜ ( ๐‘ + 1 ) ) ( (,) โ€˜ ( ๐น โ€˜ ๐‘– ) ) โˆฉ ( (,) โ€˜ ( ๐บ โ€˜ ๐‘— ) ) ) = โˆช ๐‘— โˆˆ ( 1 ... ๐‘€ ) โˆช ๐‘– โˆˆ ( โ„คโ‰ฅ โ€˜ ( ๐‘ + 1 ) ) ( ( (,) โ€˜ ( ๐น โ€˜ ๐‘– ) ) โˆฉ ( (,) โ€˜ ( ๐บ โ€˜ ๐‘— ) ) )
109 iunin2 โŠข โˆช ๐‘— โˆˆ ( 1 ... ๐‘€ ) ( โˆช ๐‘– โˆˆ ( โ„คโ‰ฅ โ€˜ ( ๐‘ + 1 ) ) ( (,) โ€˜ ( ๐น โ€˜ ๐‘– ) ) โˆฉ ( (,) โ€˜ ( ๐บ โ€˜ ๐‘— ) ) ) = ( โˆช ๐‘– โˆˆ ( โ„คโ‰ฅ โ€˜ ( ๐‘ + 1 ) ) ( (,) โ€˜ ( ๐น โ€˜ ๐‘– ) ) โˆฉ โˆช ๐‘— โˆˆ ( 1 ... ๐‘€ ) ( (,) โ€˜ ( ๐บ โ€˜ ๐‘— ) ) )
110 108 109 eqtr3i โŠข โˆช ๐‘— โˆˆ ( 1 ... ๐‘€ ) โˆช ๐‘– โˆˆ ( โ„คโ‰ฅ โ€˜ ( ๐‘ + 1 ) ) ( ( (,) โ€˜ ( ๐น โ€˜ ๐‘– ) ) โˆฉ ( (,) โ€˜ ( ๐บ โ€˜ ๐‘— ) ) ) = ( โˆช ๐‘– โˆˆ ( โ„คโ‰ฅ โ€˜ ( ๐‘ + 1 ) ) ( (,) โ€˜ ( ๐น โ€˜ ๐‘– ) ) โˆฉ โˆช ๐‘— โˆˆ ( 1 ... ๐‘€ ) ( (,) โ€˜ ( ๐บ โ€˜ ๐‘— ) ) )
111 99 100 110 3eqtr4g โŠข ( ๐œ‘ โ†’ ( ๐พ โˆฉ โˆช ๐‘– โˆˆ ( โ„คโ‰ฅ โ€˜ ( ๐‘ + 1 ) ) ( (,) โ€˜ ( ๐น โ€˜ ๐‘– ) ) ) = โˆช ๐‘— โˆˆ ( 1 ... ๐‘€ ) โˆช ๐‘– โˆˆ ( โ„คโ‰ฅ โ€˜ ( ๐‘ + 1 ) ) ( ( (,) โ€˜ ( ๐น โ€˜ ๐‘– ) ) โˆฉ ( (,) โ€˜ ( ๐บ โ€˜ ๐‘— ) ) ) )
112 111 uneq2d โŠข ( ๐œ‘ โ†’ ( ( ๐พ โˆฉ ๐ฟ ) โˆช ( ๐พ โˆฉ โˆช ๐‘– โˆˆ ( โ„คโ‰ฅ โ€˜ ( ๐‘ + 1 ) ) ( (,) โ€˜ ( ๐น โ€˜ ๐‘– ) ) ) ) = ( ( ๐พ โˆฉ ๐ฟ ) โˆช โˆช ๐‘— โˆˆ ( 1 ... ๐‘€ ) โˆช ๐‘– โˆˆ ( โ„คโ‰ฅ โ€˜ ( ๐‘ + 1 ) ) ( ( (,) โ€˜ ( ๐น โ€˜ ๐‘– ) ) โˆฉ ( (,) โ€˜ ( ๐บ โ€˜ ๐‘— ) ) ) ) )
113 85 112 eqtrd โŠข ( ๐œ‘ โ†’ ( ๐พ โˆฉ ๐ด ) = ( ( ๐พ โˆฉ ๐ฟ ) โˆช โˆช ๐‘— โˆˆ ( 1 ... ๐‘€ ) โˆช ๐‘– โˆˆ ( โ„คโ‰ฅ โ€˜ ( ๐‘ + 1 ) ) ( ( (,) โ€˜ ( ๐น โ€˜ ๐‘– ) ) โˆฉ ( (,) โ€˜ ( ๐บ โ€˜ ๐‘— ) ) ) ) )
114 40 113 sseqtrrid โŠข ( ๐œ‘ โ†’ โˆช ๐‘— โˆˆ ( 1 ... ๐‘€ ) โˆช ๐‘– โˆˆ ( โ„คโ‰ฅ โ€˜ ( ๐‘ + 1 ) ) ( ( (,) โ€˜ ( ๐น โ€˜ ๐‘– ) ) โˆฉ ( (,) โ€˜ ( ๐บ โ€˜ ๐‘— ) ) ) โІ ( ๐พ โˆฉ ๐ด ) )
115 114 17 sstrdi โŠข ( ๐œ‘ โ†’ โˆช ๐‘— โˆˆ ( 1 ... ๐‘€ ) โˆช ๐‘– โˆˆ ( โ„คโ‰ฅ โ€˜ ( ๐‘ + 1 ) ) ( ( (,) โ€˜ ( ๐น โ€˜ ๐‘– ) ) โˆฉ ( (,) โ€˜ ( ๐บ โ€˜ ๐‘— ) ) ) โІ ๐พ )
116 ovolsscl โŠข ( ( โˆช ๐‘— โˆˆ ( 1 ... ๐‘€ ) โˆช ๐‘– โˆˆ ( โ„คโ‰ฅ โ€˜ ( ๐‘ + 1 ) ) ( ( (,) โ€˜ ( ๐น โ€˜ ๐‘– ) ) โˆฉ ( (,) โ€˜ ( ๐บ โ€˜ ๐‘— ) ) ) โІ ๐พ โˆง ๐พ โІ โ„ โˆง ( vol* โ€˜ ๐พ ) โˆˆ โ„ ) โ†’ ( vol* โ€˜ โˆช ๐‘— โˆˆ ( 1 ... ๐‘€ ) โˆช ๐‘– โˆˆ ( โ„คโ‰ฅ โ€˜ ( ๐‘ + 1 ) ) ( ( (,) โ€˜ ( ๐น โ€˜ ๐‘– ) ) โˆฉ ( (,) โ€˜ ( ๐บ โ€˜ ๐‘— ) ) ) ) โˆˆ โ„ )
117 115 26 34 116 syl3anc โŠข ( ๐œ‘ โ†’ ( vol* โ€˜ โˆช ๐‘— โˆˆ ( 1 ... ๐‘€ ) โˆช ๐‘– โˆˆ ( โ„คโ‰ฅ โ€˜ ( ๐‘ + 1 ) ) ( ( (,) โ€˜ ( ๐น โ€˜ ๐‘– ) ) โˆฉ ( (,) โ€˜ ( ๐บ โ€˜ ๐‘— ) ) ) ) โˆˆ โ„ )
118 39 117 readdcld โŠข ( ๐œ‘ โ†’ ( ( vol* โ€˜ ( ๐พ โˆฉ ๐ฟ ) ) + ( vol* โ€˜ โˆช ๐‘— โˆˆ ( 1 ... ๐‘€ ) โˆช ๐‘– โˆˆ ( โ„คโ‰ฅ โ€˜ ( ๐‘ + 1 ) ) ( ( (,) โ€˜ ( ๐น โ€˜ ๐‘– ) ) โˆฉ ( (,) โ€˜ ( ๐บ โ€˜ ๐‘— ) ) ) ) ) โˆˆ โ„ )
119 6 rpred โŠข ( ๐œ‘ โ†’ ๐ถ โˆˆ โ„ )
120 39 119 readdcld โŠข ( ๐œ‘ โ†’ ( ( vol* โ€˜ ( ๐พ โˆฉ ๐ฟ ) ) + ๐ถ ) โˆˆ โ„ )
121 113 fveq2d โŠข ( ๐œ‘ โ†’ ( vol* โ€˜ ( ๐พ โˆฉ ๐ด ) ) = ( vol* โ€˜ ( ( ๐พ โˆฉ ๐ฟ ) โˆช โˆช ๐‘— โˆˆ ( 1 ... ๐‘€ ) โˆช ๐‘– โˆˆ ( โ„คโ‰ฅ โ€˜ ( ๐‘ + 1 ) ) ( ( (,) โ€˜ ( ๐น โ€˜ ๐‘– ) ) โˆฉ ( (,) โ€˜ ( ๐บ โ€˜ ๐‘— ) ) ) ) ) )
122 37 26 sstrid โŠข ( ๐œ‘ โ†’ ( ๐พ โˆฉ ๐ฟ ) โІ โ„ )
123 115 26 sstrd โŠข ( ๐œ‘ โ†’ โˆช ๐‘— โˆˆ ( 1 ... ๐‘€ ) โˆช ๐‘– โˆˆ ( โ„คโ‰ฅ โ€˜ ( ๐‘ + 1 ) ) ( ( (,) โ€˜ ( ๐น โ€˜ ๐‘– ) ) โˆฉ ( (,) โ€˜ ( ๐บ โ€˜ ๐‘— ) ) ) โІ โ„ )
124 ovolun โŠข ( ( ( ( ๐พ โˆฉ ๐ฟ ) โІ โ„ โˆง ( vol* โ€˜ ( ๐พ โˆฉ ๐ฟ ) ) โˆˆ โ„ ) โˆง ( โˆช ๐‘— โˆˆ ( 1 ... ๐‘€ ) โˆช ๐‘– โˆˆ ( โ„คโ‰ฅ โ€˜ ( ๐‘ + 1 ) ) ( ( (,) โ€˜ ( ๐น โ€˜ ๐‘– ) ) โˆฉ ( (,) โ€˜ ( ๐บ โ€˜ ๐‘— ) ) ) โІ โ„ โˆง ( vol* โ€˜ โˆช ๐‘— โˆˆ ( 1 ... ๐‘€ ) โˆช ๐‘– โˆˆ ( โ„คโ‰ฅ โ€˜ ( ๐‘ + 1 ) ) ( ( (,) โ€˜ ( ๐น โ€˜ ๐‘– ) ) โˆฉ ( (,) โ€˜ ( ๐บ โ€˜ ๐‘— ) ) ) ) โˆˆ โ„ ) ) โ†’ ( vol* โ€˜ ( ( ๐พ โˆฉ ๐ฟ ) โˆช โˆช ๐‘— โˆˆ ( 1 ... ๐‘€ ) โˆช ๐‘– โˆˆ ( โ„คโ‰ฅ โ€˜ ( ๐‘ + 1 ) ) ( ( (,) โ€˜ ( ๐น โ€˜ ๐‘– ) ) โˆฉ ( (,) โ€˜ ( ๐บ โ€˜ ๐‘— ) ) ) ) ) โ‰ค ( ( vol* โ€˜ ( ๐พ โˆฉ ๐ฟ ) ) + ( vol* โ€˜ โˆช ๐‘— โˆˆ ( 1 ... ๐‘€ ) โˆช ๐‘– โˆˆ ( โ„คโ‰ฅ โ€˜ ( ๐‘ + 1 ) ) ( ( (,) โ€˜ ( ๐น โ€˜ ๐‘– ) ) โˆฉ ( (,) โ€˜ ( ๐บ โ€˜ ๐‘— ) ) ) ) ) )
125 122 39 123 117 124 syl22anc โŠข ( ๐œ‘ โ†’ ( vol* โ€˜ ( ( ๐พ โˆฉ ๐ฟ ) โˆช โˆช ๐‘— โˆˆ ( 1 ... ๐‘€ ) โˆช ๐‘– โˆˆ ( โ„คโ‰ฅ โ€˜ ( ๐‘ + 1 ) ) ( ( (,) โ€˜ ( ๐น โ€˜ ๐‘– ) ) โˆฉ ( (,) โ€˜ ( ๐บ โ€˜ ๐‘— ) ) ) ) ) โ‰ค ( ( vol* โ€˜ ( ๐พ โˆฉ ๐ฟ ) ) + ( vol* โ€˜ โˆช ๐‘— โˆˆ ( 1 ... ๐‘€ ) โˆช ๐‘– โˆˆ ( โ„คโ‰ฅ โ€˜ ( ๐‘ + 1 ) ) ( ( (,) โ€˜ ( ๐น โ€˜ ๐‘– ) ) โˆฉ ( (,) โ€˜ ( ๐บ โ€˜ ๐‘— ) ) ) ) ) )
126 121 125 eqbrtrd โŠข ( ๐œ‘ โ†’ ( vol* โ€˜ ( ๐พ โˆฉ ๐ด ) ) โ‰ค ( ( vol* โ€˜ ( ๐พ โˆฉ ๐ฟ ) ) + ( vol* โ€˜ โˆช ๐‘— โˆˆ ( 1 ... ๐‘€ ) โˆช ๐‘– โˆˆ ( โ„คโ‰ฅ โ€˜ ( ๐‘ + 1 ) ) ( ( (,) โ€˜ ( ๐น โ€˜ ๐‘– ) ) โˆฉ ( (,) โ€˜ ( ๐บ โ€˜ ๐‘— ) ) ) ) ) )
127 fzfid โŠข ( ๐œ‘ โ†’ ( 1 ... ๐‘€ ) โˆˆ Fin )
128 iunss โŠข ( โˆช ๐‘— โˆˆ ( 1 ... ๐‘€ ) โˆช ๐‘– โˆˆ ( โ„คโ‰ฅ โ€˜ ( ๐‘ + 1 ) ) ( ( (,) โ€˜ ( ๐น โ€˜ ๐‘– ) ) โˆฉ ( (,) โ€˜ ( ๐บ โ€˜ ๐‘— ) ) ) โІ ๐พ โ†” โˆ€ ๐‘— โˆˆ ( 1 ... ๐‘€ ) โˆช ๐‘– โˆˆ ( โ„คโ‰ฅ โ€˜ ( ๐‘ + 1 ) ) ( ( (,) โ€˜ ( ๐น โ€˜ ๐‘– ) ) โˆฉ ( (,) โ€˜ ( ๐บ โ€˜ ๐‘— ) ) ) โІ ๐พ )
129 115 128 sylib โŠข ( ๐œ‘ โ†’ โˆ€ ๐‘— โˆˆ ( 1 ... ๐‘€ ) โˆช ๐‘– โˆˆ ( โ„คโ‰ฅ โ€˜ ( ๐‘ + 1 ) ) ( ( (,) โ€˜ ( ๐น โ€˜ ๐‘– ) ) โˆฉ ( (,) โ€˜ ( ๐บ โ€˜ ๐‘— ) ) ) โІ ๐พ )
130 129 r19.21bi โŠข ( ( ๐œ‘ โˆง ๐‘— โˆˆ ( 1 ... ๐‘€ ) ) โ†’ โˆช ๐‘– โˆˆ ( โ„คโ‰ฅ โ€˜ ( ๐‘ + 1 ) ) ( ( (,) โ€˜ ( ๐น โ€˜ ๐‘– ) ) โˆฉ ( (,) โ€˜ ( ๐บ โ€˜ ๐‘— ) ) ) โІ ๐พ )
131 26 adantr โŠข ( ( ๐œ‘ โˆง ๐‘— โˆˆ ( 1 ... ๐‘€ ) ) โ†’ ๐พ โІ โ„ )
132 34 adantr โŠข ( ( ๐œ‘ โˆง ๐‘— โˆˆ ( 1 ... ๐‘€ ) ) โ†’ ( vol* โ€˜ ๐พ ) โˆˆ โ„ )
133 ovolsscl โŠข ( ( โˆช ๐‘– โˆˆ ( โ„คโ‰ฅ โ€˜ ( ๐‘ + 1 ) ) ( ( (,) โ€˜ ( ๐น โ€˜ ๐‘– ) ) โˆฉ ( (,) โ€˜ ( ๐บ โ€˜ ๐‘— ) ) ) โІ ๐พ โˆง ๐พ โІ โ„ โˆง ( vol* โ€˜ ๐พ ) โˆˆ โ„ ) โ†’ ( vol* โ€˜ โˆช ๐‘– โˆˆ ( โ„คโ‰ฅ โ€˜ ( ๐‘ + 1 ) ) ( ( (,) โ€˜ ( ๐น โ€˜ ๐‘– ) ) โˆฉ ( (,) โ€˜ ( ๐บ โ€˜ ๐‘— ) ) ) ) โˆˆ โ„ )
134 130 131 132 133 syl3anc โŠข ( ( ๐œ‘ โˆง ๐‘— โˆˆ ( 1 ... ๐‘€ ) ) โ†’ ( vol* โ€˜ โˆช ๐‘– โˆˆ ( โ„คโ‰ฅ โ€˜ ( ๐‘ + 1 ) ) ( ( (,) โ€˜ ( ๐น โ€˜ ๐‘– ) ) โˆฉ ( (,) โ€˜ ( ๐บ โ€˜ ๐‘— ) ) ) ) โˆˆ โ„ )
135 127 134 fsumrecl โŠข ( ๐œ‘ โ†’ ฮฃ ๐‘— โˆˆ ( 1 ... ๐‘€ ) ( vol* โ€˜ โˆช ๐‘– โˆˆ ( โ„คโ‰ฅ โ€˜ ( ๐‘ + 1 ) ) ( ( (,) โ€˜ ( ๐น โ€˜ ๐‘– ) ) โˆฉ ( (,) โ€˜ ( ๐บ โ€˜ ๐‘— ) ) ) ) โˆˆ โ„ )
136 130 131 sstrd โŠข ( ( ๐œ‘ โˆง ๐‘— โˆˆ ( 1 ... ๐‘€ ) ) โ†’ โˆช ๐‘– โˆˆ ( โ„คโ‰ฅ โ€˜ ( ๐‘ + 1 ) ) ( ( (,) โ€˜ ( ๐น โ€˜ ๐‘– ) ) โˆฉ ( (,) โ€˜ ( ๐บ โ€˜ ๐‘— ) ) ) โІ โ„ )
137 136 134 jca โŠข ( ( ๐œ‘ โˆง ๐‘— โˆˆ ( 1 ... ๐‘€ ) ) โ†’ ( โˆช ๐‘– โˆˆ ( โ„คโ‰ฅ โ€˜ ( ๐‘ + 1 ) ) ( ( (,) โ€˜ ( ๐น โ€˜ ๐‘– ) ) โˆฉ ( (,) โ€˜ ( ๐บ โ€˜ ๐‘— ) ) ) โІ โ„ โˆง ( vol* โ€˜ โˆช ๐‘– โˆˆ ( โ„คโ‰ฅ โ€˜ ( ๐‘ + 1 ) ) ( ( (,) โ€˜ ( ๐น โ€˜ ๐‘– ) ) โˆฉ ( (,) โ€˜ ( ๐บ โ€˜ ๐‘— ) ) ) ) โˆˆ โ„ ) )
138 137 ralrimiva โŠข ( ๐œ‘ โ†’ โˆ€ ๐‘— โˆˆ ( 1 ... ๐‘€ ) ( โˆช ๐‘– โˆˆ ( โ„คโ‰ฅ โ€˜ ( ๐‘ + 1 ) ) ( ( (,) โ€˜ ( ๐น โ€˜ ๐‘– ) ) โˆฉ ( (,) โ€˜ ( ๐บ โ€˜ ๐‘— ) ) ) โІ โ„ โˆง ( vol* โ€˜ โˆช ๐‘– โˆˆ ( โ„คโ‰ฅ โ€˜ ( ๐‘ + 1 ) ) ( ( (,) โ€˜ ( ๐น โ€˜ ๐‘– ) ) โˆฉ ( (,) โ€˜ ( ๐บ โ€˜ ๐‘— ) ) ) ) โˆˆ โ„ ) )
139 ovolfiniun โŠข ( ( ( 1 ... ๐‘€ ) โˆˆ Fin โˆง โˆ€ ๐‘— โˆˆ ( 1 ... ๐‘€ ) ( โˆช ๐‘– โˆˆ ( โ„คโ‰ฅ โ€˜ ( ๐‘ + 1 ) ) ( ( (,) โ€˜ ( ๐น โ€˜ ๐‘– ) ) โˆฉ ( (,) โ€˜ ( ๐บ โ€˜ ๐‘— ) ) ) โІ โ„ โˆง ( vol* โ€˜ โˆช ๐‘– โˆˆ ( โ„คโ‰ฅ โ€˜ ( ๐‘ + 1 ) ) ( ( (,) โ€˜ ( ๐น โ€˜ ๐‘– ) ) โˆฉ ( (,) โ€˜ ( ๐บ โ€˜ ๐‘— ) ) ) ) โˆˆ โ„ ) ) โ†’ ( vol* โ€˜ โˆช ๐‘— โˆˆ ( 1 ... ๐‘€ ) โˆช ๐‘– โˆˆ ( โ„คโ‰ฅ โ€˜ ( ๐‘ + 1 ) ) ( ( (,) โ€˜ ( ๐น โ€˜ ๐‘– ) ) โˆฉ ( (,) โ€˜ ( ๐บ โ€˜ ๐‘— ) ) ) ) โ‰ค ฮฃ ๐‘— โˆˆ ( 1 ... ๐‘€ ) ( vol* โ€˜ โˆช ๐‘– โˆˆ ( โ„คโ‰ฅ โ€˜ ( ๐‘ + 1 ) ) ( ( (,) โ€˜ ( ๐น โ€˜ ๐‘– ) ) โˆฉ ( (,) โ€˜ ( ๐บ โ€˜ ๐‘— ) ) ) ) )
140 127 138 139 syl2anc โŠข ( ๐œ‘ โ†’ ( vol* โ€˜ โˆช ๐‘— โˆˆ ( 1 ... ๐‘€ ) โˆช ๐‘– โˆˆ ( โ„คโ‰ฅ โ€˜ ( ๐‘ + 1 ) ) ( ( (,) โ€˜ ( ๐น โ€˜ ๐‘– ) ) โˆฉ ( (,) โ€˜ ( ๐บ โ€˜ ๐‘— ) ) ) ) โ‰ค ฮฃ ๐‘— โˆˆ ( 1 ... ๐‘€ ) ( vol* โ€˜ โˆช ๐‘– โˆˆ ( โ„คโ‰ฅ โ€˜ ( ๐‘ + 1 ) ) ( ( (,) โ€˜ ( ๐น โ€˜ ๐‘– ) ) โˆฉ ( (,) โ€˜ ( ๐บ โ€˜ ๐‘— ) ) ) ) )
141 119 11 nndivred โŠข ( ๐œ‘ โ†’ ( ๐ถ / ๐‘€ ) โˆˆ โ„ )
142 141 adantr โŠข ( ( ๐œ‘ โˆง ๐‘— โˆˆ ( 1 ... ๐‘€ ) ) โ†’ ( ๐ถ / ๐‘€ ) โˆˆ โ„ )
143 80 ineq2d โŠข ( ๐œ‘ โ†’ ( ( (,) โ€˜ ( ๐บ โ€˜ ๐‘— ) ) โˆฉ ๐ฟ ) = ( ( (,) โ€˜ ( ๐บ โ€˜ ๐‘— ) ) โˆฉ โˆช ๐‘– โˆˆ ( 1 ... ๐‘ ) ( (,) โ€˜ ( ๐น โ€˜ ๐‘– ) ) ) )
144 143 adantr โŠข ( ( ๐œ‘ โˆง ๐‘— โˆˆ ( 1 ... ๐‘€ ) ) โ†’ ( ( (,) โ€˜ ( ๐บ โ€˜ ๐‘— ) ) โˆฉ ๐ฟ ) = ( ( (,) โ€˜ ( ๐บ โ€˜ ๐‘— ) ) โˆฉ โˆช ๐‘– โˆˆ ( 1 ... ๐‘ ) ( (,) โ€˜ ( ๐น โ€˜ ๐‘– ) ) ) )
145 102 a1i โŠข ( ๐‘– โˆˆ ( 1 ... ๐‘ ) โ†’ ( ( (,) โ€˜ ( ๐น โ€˜ ๐‘– ) ) โˆฉ ( (,) โ€˜ ( ๐บ โ€˜ ๐‘— ) ) ) = ( ( (,) โ€˜ ( ๐บ โ€˜ ๐‘— ) ) โˆฉ ( (,) โ€˜ ( ๐น โ€˜ ๐‘– ) ) ) )
146 145 iuneq2i โŠข โˆช ๐‘– โˆˆ ( 1 ... ๐‘ ) ( ( (,) โ€˜ ( ๐น โ€˜ ๐‘– ) ) โˆฉ ( (,) โ€˜ ( ๐บ โ€˜ ๐‘— ) ) ) = โˆช ๐‘– โˆˆ ( 1 ... ๐‘ ) ( ( (,) โ€˜ ( ๐บ โ€˜ ๐‘— ) ) โˆฉ ( (,) โ€˜ ( ๐น โ€˜ ๐‘– ) ) )
147 iunin2 โŠข โˆช ๐‘– โˆˆ ( 1 ... ๐‘ ) ( ( (,) โ€˜ ( ๐บ โ€˜ ๐‘— ) ) โˆฉ ( (,) โ€˜ ( ๐น โ€˜ ๐‘– ) ) ) = ( ( (,) โ€˜ ( ๐บ โ€˜ ๐‘— ) ) โˆฉ โˆช ๐‘– โˆˆ ( 1 ... ๐‘ ) ( (,) โ€˜ ( ๐น โ€˜ ๐‘– ) ) )
148 146 147 eqtri โŠข โˆช ๐‘– โˆˆ ( 1 ... ๐‘ ) ( ( (,) โ€˜ ( ๐น โ€˜ ๐‘– ) ) โˆฉ ( (,) โ€˜ ( ๐บ โ€˜ ๐‘— ) ) ) = ( ( (,) โ€˜ ( ๐บ โ€˜ ๐‘— ) ) โˆฉ โˆช ๐‘– โˆˆ ( 1 ... ๐‘ ) ( (,) โ€˜ ( ๐น โ€˜ ๐‘– ) ) )
149 144 148 eqtr4di โŠข ( ( ๐œ‘ โˆง ๐‘— โˆˆ ( 1 ... ๐‘€ ) ) โ†’ ( ( (,) โ€˜ ( ๐บ โ€˜ ๐‘— ) ) โˆฉ ๐ฟ ) = โˆช ๐‘– โˆˆ ( 1 ... ๐‘ ) ( ( (,) โ€˜ ( ๐น โ€˜ ๐‘– ) ) โˆฉ ( (,) โ€˜ ( ๐บ โ€˜ ๐‘— ) ) ) )
150 fzfid โŠข ( ( ๐œ‘ โˆง ๐‘— โˆˆ ( 1 ... ๐‘€ ) ) โ†’ ( 1 ... ๐‘ ) โˆˆ Fin )
151 ffvelcdm โŠข ( ( ๐น : โ„• โŸถ ( โ‰ค โˆฉ ( โ„ ร— โ„ ) ) โˆง ๐‘– โˆˆ โ„• ) โ†’ ( ๐น โ€˜ ๐‘– ) โˆˆ ( โ‰ค โˆฉ ( โ„ ร— โ„ ) ) )
152 1 76 151 syl2an โŠข ( ( ๐œ‘ โˆง ๐‘– โˆˆ ( 1 ... ๐‘ ) ) โ†’ ( ๐น โ€˜ ๐‘– ) โˆˆ ( โ‰ค โˆฉ ( โ„ ร— โ„ ) ) )
153 152 elin2d โŠข ( ( ๐œ‘ โˆง ๐‘– โˆˆ ( 1 ... ๐‘ ) ) โ†’ ( ๐น โ€˜ ๐‘– ) โˆˆ ( โ„ ร— โ„ ) )
154 1st2nd2 โŠข ( ( ๐น โ€˜ ๐‘– ) โˆˆ ( โ„ ร— โ„ ) โ†’ ( ๐น โ€˜ ๐‘– ) = โŸจ ( 1st โ€˜ ( ๐น โ€˜ ๐‘– ) ) , ( 2nd โ€˜ ( ๐น โ€˜ ๐‘– ) ) โŸฉ )
155 153 154 syl โŠข ( ( ๐œ‘ โˆง ๐‘– โˆˆ ( 1 ... ๐‘ ) ) โ†’ ( ๐น โ€˜ ๐‘– ) = โŸจ ( 1st โ€˜ ( ๐น โ€˜ ๐‘– ) ) , ( 2nd โ€˜ ( ๐น โ€˜ ๐‘– ) ) โŸฉ )
156 155 fveq2d โŠข ( ( ๐œ‘ โˆง ๐‘– โˆˆ ( 1 ... ๐‘ ) ) โ†’ ( (,) โ€˜ ( ๐น โ€˜ ๐‘– ) ) = ( (,) โ€˜ โŸจ ( 1st โ€˜ ( ๐น โ€˜ ๐‘– ) ) , ( 2nd โ€˜ ( ๐น โ€˜ ๐‘– ) ) โŸฉ ) )
157 df-ov โŠข ( ( 1st โ€˜ ( ๐น โ€˜ ๐‘– ) ) (,) ( 2nd โ€˜ ( ๐น โ€˜ ๐‘– ) ) ) = ( (,) โ€˜ โŸจ ( 1st โ€˜ ( ๐น โ€˜ ๐‘– ) ) , ( 2nd โ€˜ ( ๐น โ€˜ ๐‘– ) ) โŸฉ )
158 156 157 eqtr4di โŠข ( ( ๐œ‘ โˆง ๐‘– โˆˆ ( 1 ... ๐‘ ) ) โ†’ ( (,) โ€˜ ( ๐น โ€˜ ๐‘– ) ) = ( ( 1st โ€˜ ( ๐น โ€˜ ๐‘– ) ) (,) ( 2nd โ€˜ ( ๐น โ€˜ ๐‘– ) ) ) )
159 ioombl โŠข ( ( 1st โ€˜ ( ๐น โ€˜ ๐‘– ) ) (,) ( 2nd โ€˜ ( ๐น โ€˜ ๐‘– ) ) ) โˆˆ dom vol
160 158 159 eqeltrdi โŠข ( ( ๐œ‘ โˆง ๐‘– โˆˆ ( 1 ... ๐‘ ) ) โ†’ ( (,) โ€˜ ( ๐น โ€˜ ๐‘– ) ) โˆˆ dom vol )
161 160 adantlr โŠข ( ( ( ๐œ‘ โˆง ๐‘— โˆˆ ( 1 ... ๐‘€ ) ) โˆง ๐‘– โˆˆ ( 1 ... ๐‘ ) ) โ†’ ( (,) โ€˜ ( ๐น โ€˜ ๐‘– ) ) โˆˆ dom vol )
162 ffvelcdm โŠข ( ( ๐บ : โ„• โŸถ ( โ‰ค โˆฉ ( โ„ ร— โ„ ) ) โˆง ๐‘— โˆˆ โ„• ) โ†’ ( ๐บ โ€˜ ๐‘— ) โˆˆ ( โ‰ค โˆฉ ( โ„ ร— โ„ ) ) )
163 7 93 162 syl2an โŠข ( ( ๐œ‘ โˆง ๐‘— โˆˆ ( 1 ... ๐‘€ ) ) โ†’ ( ๐บ โ€˜ ๐‘— ) โˆˆ ( โ‰ค โˆฉ ( โ„ ร— โ„ ) ) )
164 163 elin2d โŠข ( ( ๐œ‘ โˆง ๐‘— โˆˆ ( 1 ... ๐‘€ ) ) โ†’ ( ๐บ โ€˜ ๐‘— ) โˆˆ ( โ„ ร— โ„ ) )
165 1st2nd2 โŠข ( ( ๐บ โ€˜ ๐‘— ) โˆˆ ( โ„ ร— โ„ ) โ†’ ( ๐บ โ€˜ ๐‘— ) = โŸจ ( 1st โ€˜ ( ๐บ โ€˜ ๐‘— ) ) , ( 2nd โ€˜ ( ๐บ โ€˜ ๐‘— ) ) โŸฉ )
166 164 165 syl โŠข ( ( ๐œ‘ โˆง ๐‘— โˆˆ ( 1 ... ๐‘€ ) ) โ†’ ( ๐บ โ€˜ ๐‘— ) = โŸจ ( 1st โ€˜ ( ๐บ โ€˜ ๐‘— ) ) , ( 2nd โ€˜ ( ๐บ โ€˜ ๐‘— ) ) โŸฉ )
167 166 fveq2d โŠข ( ( ๐œ‘ โˆง ๐‘— โˆˆ ( 1 ... ๐‘€ ) ) โ†’ ( (,) โ€˜ ( ๐บ โ€˜ ๐‘— ) ) = ( (,) โ€˜ โŸจ ( 1st โ€˜ ( ๐บ โ€˜ ๐‘— ) ) , ( 2nd โ€˜ ( ๐บ โ€˜ ๐‘— ) ) โŸฉ ) )
168 df-ov โŠข ( ( 1st โ€˜ ( ๐บ โ€˜ ๐‘— ) ) (,) ( 2nd โ€˜ ( ๐บ โ€˜ ๐‘— ) ) ) = ( (,) โ€˜ โŸจ ( 1st โ€˜ ( ๐บ โ€˜ ๐‘— ) ) , ( 2nd โ€˜ ( ๐บ โ€˜ ๐‘— ) ) โŸฉ )
169 167 168 eqtr4di โŠข ( ( ๐œ‘ โˆง ๐‘— โˆˆ ( 1 ... ๐‘€ ) ) โ†’ ( (,) โ€˜ ( ๐บ โ€˜ ๐‘— ) ) = ( ( 1st โ€˜ ( ๐บ โ€˜ ๐‘— ) ) (,) ( 2nd โ€˜ ( ๐บ โ€˜ ๐‘— ) ) ) )
170 ioombl โŠข ( ( 1st โ€˜ ( ๐บ โ€˜ ๐‘— ) ) (,) ( 2nd โ€˜ ( ๐บ โ€˜ ๐‘— ) ) ) โˆˆ dom vol
171 169 170 eqeltrdi โŠข ( ( ๐œ‘ โˆง ๐‘— โˆˆ ( 1 ... ๐‘€ ) ) โ†’ ( (,) โ€˜ ( ๐บ โ€˜ ๐‘— ) ) โˆˆ dom vol )
172 171 adantr โŠข ( ( ( ๐œ‘ โˆง ๐‘— โˆˆ ( 1 ... ๐‘€ ) ) โˆง ๐‘– โˆˆ ( 1 ... ๐‘ ) ) โ†’ ( (,) โ€˜ ( ๐บ โ€˜ ๐‘— ) ) โˆˆ dom vol )
173 inmbl โŠข ( ( ( (,) โ€˜ ( ๐น โ€˜ ๐‘– ) ) โˆˆ dom vol โˆง ( (,) โ€˜ ( ๐บ โ€˜ ๐‘— ) ) โˆˆ dom vol ) โ†’ ( ( (,) โ€˜ ( ๐น โ€˜ ๐‘– ) ) โˆฉ ( (,) โ€˜ ( ๐บ โ€˜ ๐‘— ) ) ) โˆˆ dom vol )
174 161 172 173 syl2anc โŠข ( ( ( ๐œ‘ โˆง ๐‘— โˆˆ ( 1 ... ๐‘€ ) ) โˆง ๐‘– โˆˆ ( 1 ... ๐‘ ) ) โ†’ ( ( (,) โ€˜ ( ๐น โ€˜ ๐‘– ) ) โˆฉ ( (,) โ€˜ ( ๐บ โ€˜ ๐‘— ) ) ) โˆˆ dom vol )
175 174 ralrimiva โŠข ( ( ๐œ‘ โˆง ๐‘— โˆˆ ( 1 ... ๐‘€ ) ) โ†’ โˆ€ ๐‘– โˆˆ ( 1 ... ๐‘ ) ( ( (,) โ€˜ ( ๐น โ€˜ ๐‘– ) ) โˆฉ ( (,) โ€˜ ( ๐บ โ€˜ ๐‘— ) ) ) โˆˆ dom vol )
176 finiunmbl โŠข ( ( ( 1 ... ๐‘ ) โˆˆ Fin โˆง โˆ€ ๐‘– โˆˆ ( 1 ... ๐‘ ) ( ( (,) โ€˜ ( ๐น โ€˜ ๐‘– ) ) โˆฉ ( (,) โ€˜ ( ๐บ โ€˜ ๐‘— ) ) ) โˆˆ dom vol ) โ†’ โˆช ๐‘– โˆˆ ( 1 ... ๐‘ ) ( ( (,) โ€˜ ( ๐น โ€˜ ๐‘– ) ) โˆฉ ( (,) โ€˜ ( ๐บ โ€˜ ๐‘— ) ) ) โˆˆ dom vol )
177 150 175 176 syl2anc โŠข ( ( ๐œ‘ โˆง ๐‘— โˆˆ ( 1 ... ๐‘€ ) ) โ†’ โˆช ๐‘– โˆˆ ( 1 ... ๐‘ ) ( ( (,) โ€˜ ( ๐น โ€˜ ๐‘– ) ) โˆฉ ( (,) โ€˜ ( ๐บ โ€˜ ๐‘— ) ) ) โˆˆ dom vol )
178 149 177 eqeltrd โŠข ( ( ๐œ‘ โˆง ๐‘— โˆˆ ( 1 ... ๐‘€ ) ) โ†’ ( ( (,) โ€˜ ( ๐บ โ€˜ ๐‘— ) ) โˆฉ ๐ฟ ) โˆˆ dom vol )
179 inss2 โŠข ( ( (,) โ€˜ ( ๐บ โ€˜ ๐‘— ) ) โˆฉ ๐ด ) โІ ๐ด
180 1 uniiccdif โŠข ( ๐œ‘ โ†’ ( โˆช ran ( (,) โˆ˜ ๐น ) โІ โˆช ran ( [,] โˆ˜ ๐น ) โˆง ( vol* โ€˜ ( โˆช ran ( [,] โˆ˜ ๐น ) โˆ– โˆช ran ( (,) โˆ˜ ๐น ) ) ) = 0 ) )
181 180 simpld โŠข ( ๐œ‘ โ†’ โˆช ran ( (,) โˆ˜ ๐น ) โІ โˆช ran ( [,] โˆ˜ ๐น ) )
182 ovolficcss โŠข ( ๐น : โ„• โŸถ ( โ‰ค โˆฉ ( โ„ ร— โ„ ) ) โ†’ โˆช ran ( [,] โˆ˜ ๐น ) โІ โ„ )
183 1 182 syl โŠข ( ๐œ‘ โ†’ โˆช ran ( [,] โˆ˜ ๐น ) โІ โ„ )
184 181 183 sstrd โŠข ( ๐œ‘ โ†’ โˆช ran ( (,) โˆ˜ ๐น ) โІ โ„ )
185 4 184 eqsstrid โŠข ( ๐œ‘ โ†’ ๐ด โІ โ„ )
186 185 adantr โŠข ( ( ๐œ‘ โˆง ๐‘— โˆˆ ( 1 ... ๐‘€ ) ) โ†’ ๐ด โІ โ„ )
187 179 186 sstrid โŠข ( ( ๐œ‘ โˆง ๐‘— โˆˆ ( 1 ... ๐‘€ ) ) โ†’ ( ( (,) โ€˜ ( ๐บ โ€˜ ๐‘— ) ) โˆฉ ๐ด ) โІ โ„ )
188 inss1 โŠข ( ( (,) โ€˜ ( ๐บ โ€˜ ๐‘— ) ) โˆฉ ๐ด ) โІ ( (,) โ€˜ ( ๐บ โ€˜ ๐‘— ) )
189 ioossre โŠข ( ( 1st โ€˜ ( ๐บ โ€˜ ๐‘— ) ) (,) ( 2nd โ€˜ ( ๐บ โ€˜ ๐‘— ) ) ) โІ โ„
190 169 189 eqsstrdi โŠข ( ( ๐œ‘ โˆง ๐‘— โˆˆ ( 1 ... ๐‘€ ) ) โ†’ ( (,) โ€˜ ( ๐บ โ€˜ ๐‘— ) ) โІ โ„ )
191 169 fveq2d โŠข ( ( ๐œ‘ โˆง ๐‘— โˆˆ ( 1 ... ๐‘€ ) ) โ†’ ( vol* โ€˜ ( (,) โ€˜ ( ๐บ โ€˜ ๐‘— ) ) ) = ( vol* โ€˜ ( ( 1st โ€˜ ( ๐บ โ€˜ ๐‘— ) ) (,) ( 2nd โ€˜ ( ๐บ โ€˜ ๐‘— ) ) ) ) )
192 ovolfcl โŠข ( ( ๐บ : โ„• โŸถ ( โ‰ค โˆฉ ( โ„ ร— โ„ ) ) โˆง ๐‘— โˆˆ โ„• ) โ†’ ( ( 1st โ€˜ ( ๐บ โ€˜ ๐‘— ) ) โˆˆ โ„ โˆง ( 2nd โ€˜ ( ๐บ โ€˜ ๐‘— ) ) โˆˆ โ„ โˆง ( 1st โ€˜ ( ๐บ โ€˜ ๐‘— ) ) โ‰ค ( 2nd โ€˜ ( ๐บ โ€˜ ๐‘— ) ) ) )
193 7 93 192 syl2an โŠข ( ( ๐œ‘ โˆง ๐‘— โˆˆ ( 1 ... ๐‘€ ) ) โ†’ ( ( 1st โ€˜ ( ๐บ โ€˜ ๐‘— ) ) โˆˆ โ„ โˆง ( 2nd โ€˜ ( ๐บ โ€˜ ๐‘— ) ) โˆˆ โ„ โˆง ( 1st โ€˜ ( ๐บ โ€˜ ๐‘— ) ) โ‰ค ( 2nd โ€˜ ( ๐บ โ€˜ ๐‘— ) ) ) )
194 ovolioo โŠข ( ( ( 1st โ€˜ ( ๐บ โ€˜ ๐‘— ) ) โˆˆ โ„ โˆง ( 2nd โ€˜ ( ๐บ โ€˜ ๐‘— ) ) โˆˆ โ„ โˆง ( 1st โ€˜ ( ๐บ โ€˜ ๐‘— ) ) โ‰ค ( 2nd โ€˜ ( ๐บ โ€˜ ๐‘— ) ) ) โ†’ ( vol* โ€˜ ( ( 1st โ€˜ ( ๐บ โ€˜ ๐‘— ) ) (,) ( 2nd โ€˜ ( ๐บ โ€˜ ๐‘— ) ) ) ) = ( ( 2nd โ€˜ ( ๐บ โ€˜ ๐‘— ) ) โˆ’ ( 1st โ€˜ ( ๐บ โ€˜ ๐‘— ) ) ) )
195 193 194 syl โŠข ( ( ๐œ‘ โˆง ๐‘— โˆˆ ( 1 ... ๐‘€ ) ) โ†’ ( vol* โ€˜ ( ( 1st โ€˜ ( ๐บ โ€˜ ๐‘— ) ) (,) ( 2nd โ€˜ ( ๐บ โ€˜ ๐‘— ) ) ) ) = ( ( 2nd โ€˜ ( ๐บ โ€˜ ๐‘— ) ) โˆ’ ( 1st โ€˜ ( ๐บ โ€˜ ๐‘— ) ) ) )
196 191 195 eqtrd โŠข ( ( ๐œ‘ โˆง ๐‘— โˆˆ ( 1 ... ๐‘€ ) ) โ†’ ( vol* โ€˜ ( (,) โ€˜ ( ๐บ โ€˜ ๐‘— ) ) ) = ( ( 2nd โ€˜ ( ๐บ โ€˜ ๐‘— ) ) โˆ’ ( 1st โ€˜ ( ๐บ โ€˜ ๐‘— ) ) ) )
197 193 simp2d โŠข ( ( ๐œ‘ โˆง ๐‘— โˆˆ ( 1 ... ๐‘€ ) ) โ†’ ( 2nd โ€˜ ( ๐บ โ€˜ ๐‘— ) ) โˆˆ โ„ )
198 193 simp1d โŠข ( ( ๐œ‘ โˆง ๐‘— โˆˆ ( 1 ... ๐‘€ ) ) โ†’ ( 1st โ€˜ ( ๐บ โ€˜ ๐‘— ) ) โˆˆ โ„ )
199 197 198 resubcld โŠข ( ( ๐œ‘ โˆง ๐‘— โˆˆ ( 1 ... ๐‘€ ) ) โ†’ ( ( 2nd โ€˜ ( ๐บ โ€˜ ๐‘— ) ) โˆ’ ( 1st โ€˜ ( ๐บ โ€˜ ๐‘— ) ) ) โˆˆ โ„ )
200 196 199 eqeltrd โŠข ( ( ๐œ‘ โˆง ๐‘— โˆˆ ( 1 ... ๐‘€ ) ) โ†’ ( vol* โ€˜ ( (,) โ€˜ ( ๐บ โ€˜ ๐‘— ) ) ) โˆˆ โ„ )
201 ovolsscl โŠข ( ( ( ( (,) โ€˜ ( ๐บ โ€˜ ๐‘— ) ) โˆฉ ๐ด ) โІ ( (,) โ€˜ ( ๐บ โ€˜ ๐‘— ) ) โˆง ( (,) โ€˜ ( ๐บ โ€˜ ๐‘— ) ) โІ โ„ โˆง ( vol* โ€˜ ( (,) โ€˜ ( ๐บ โ€˜ ๐‘— ) ) ) โˆˆ โ„ ) โ†’ ( vol* โ€˜ ( ( (,) โ€˜ ( ๐บ โ€˜ ๐‘— ) ) โˆฉ ๐ด ) ) โˆˆ โ„ )
202 188 190 200 201 mp3an2i โŠข ( ( ๐œ‘ โˆง ๐‘— โˆˆ ( 1 ... ๐‘€ ) ) โ†’ ( vol* โ€˜ ( ( (,) โ€˜ ( ๐บ โ€˜ ๐‘— ) ) โˆฉ ๐ด ) ) โˆˆ โ„ )
203 mblsplit โŠข ( ( ( ( (,) โ€˜ ( ๐บ โ€˜ ๐‘— ) ) โˆฉ ๐ฟ ) โˆˆ dom vol โˆง ( ( (,) โ€˜ ( ๐บ โ€˜ ๐‘— ) ) โˆฉ ๐ด ) โІ โ„ โˆง ( vol* โ€˜ ( ( (,) โ€˜ ( ๐บ โ€˜ ๐‘— ) ) โˆฉ ๐ด ) ) โˆˆ โ„ ) โ†’ ( vol* โ€˜ ( ( (,) โ€˜ ( ๐บ โ€˜ ๐‘— ) ) โˆฉ ๐ด ) ) = ( ( vol* โ€˜ ( ( ( (,) โ€˜ ( ๐บ โ€˜ ๐‘— ) ) โˆฉ ๐ด ) โˆฉ ( ( (,) โ€˜ ( ๐บ โ€˜ ๐‘— ) ) โˆฉ ๐ฟ ) ) ) + ( vol* โ€˜ ( ( ( (,) โ€˜ ( ๐บ โ€˜ ๐‘— ) ) โˆฉ ๐ด ) โˆ– ( ( (,) โ€˜ ( ๐บ โ€˜ ๐‘— ) ) โˆฉ ๐ฟ ) ) ) ) )
204 178 187 202 203 syl3anc โŠข ( ( ๐œ‘ โˆง ๐‘— โˆˆ ( 1 ... ๐‘€ ) ) โ†’ ( vol* โ€˜ ( ( (,) โ€˜ ( ๐บ โ€˜ ๐‘— ) ) โˆฉ ๐ด ) ) = ( ( vol* โ€˜ ( ( ( (,) โ€˜ ( ๐บ โ€˜ ๐‘— ) ) โˆฉ ๐ด ) โˆฉ ( ( (,) โ€˜ ( ๐บ โ€˜ ๐‘— ) ) โˆฉ ๐ฟ ) ) ) + ( vol* โ€˜ ( ( ( (,) โ€˜ ( ๐บ โ€˜ ๐‘— ) ) โˆฉ ๐ด ) โˆ– ( ( (,) โ€˜ ( ๐บ โ€˜ ๐‘— ) ) โˆฉ ๐ฟ ) ) ) ) )
205 imassrn โŠข ( ( (,) โˆ˜ ๐น ) โ€œ ( 1 ... ๐‘ ) ) โІ ran ( (,) โˆ˜ ๐น )
206 205 unissi โŠข โˆช ( ( (,) โˆ˜ ๐น ) โ€œ ( 1 ... ๐‘ ) ) โІ โˆช ran ( (,) โˆ˜ ๐น )
207 206 16 4 3sstr4i โŠข ๐ฟ โІ ๐ด
208 sslin โŠข ( ๐ฟ โІ ๐ด โ†’ ( ( (,) โ€˜ ( ๐บ โ€˜ ๐‘— ) ) โˆฉ ๐ฟ ) โІ ( ( (,) โ€˜ ( ๐บ โ€˜ ๐‘— ) ) โˆฉ ๐ด ) )
209 207 208 mp1i โŠข ( ( ๐œ‘ โˆง ๐‘— โˆˆ ( 1 ... ๐‘€ ) ) โ†’ ( ( (,) โ€˜ ( ๐บ โ€˜ ๐‘— ) ) โˆฉ ๐ฟ ) โІ ( ( (,) โ€˜ ( ๐บ โ€˜ ๐‘— ) ) โˆฉ ๐ด ) )
210 sseqin2 โŠข ( ( ( (,) โ€˜ ( ๐บ โ€˜ ๐‘— ) ) โˆฉ ๐ฟ ) โІ ( ( (,) โ€˜ ( ๐บ โ€˜ ๐‘— ) ) โˆฉ ๐ด ) โ†” ( ( ( (,) โ€˜ ( ๐บ โ€˜ ๐‘— ) ) โˆฉ ๐ด ) โˆฉ ( ( (,) โ€˜ ( ๐บ โ€˜ ๐‘— ) ) โˆฉ ๐ฟ ) ) = ( ( (,) โ€˜ ( ๐บ โ€˜ ๐‘— ) ) โˆฉ ๐ฟ ) )
211 209 210 sylib โŠข ( ( ๐œ‘ โˆง ๐‘— โˆˆ ( 1 ... ๐‘€ ) ) โ†’ ( ( ( (,) โ€˜ ( ๐บ โ€˜ ๐‘— ) ) โˆฉ ๐ด ) โˆฉ ( ( (,) โ€˜ ( ๐บ โ€˜ ๐‘— ) ) โˆฉ ๐ฟ ) ) = ( ( (,) โ€˜ ( ๐บ โ€˜ ๐‘— ) ) โˆฉ ๐ฟ ) )
212 211 fveq2d โŠข ( ( ๐œ‘ โˆง ๐‘— โˆˆ ( 1 ... ๐‘€ ) ) โ†’ ( vol* โ€˜ ( ( ( (,) โ€˜ ( ๐บ โ€˜ ๐‘— ) ) โˆฉ ๐ด ) โˆฉ ( ( (,) โ€˜ ( ๐บ โ€˜ ๐‘— ) ) โˆฉ ๐ฟ ) ) ) = ( vol* โ€˜ ( ( (,) โ€˜ ( ๐บ โ€˜ ๐‘— ) ) โˆฉ ๐ฟ ) ) )
213 indifdir โŠข ( ( ๐ด โˆ– ๐ฟ ) โˆฉ ( (,) โ€˜ ( ๐บ โ€˜ ๐‘— ) ) ) = ( ( ๐ด โˆฉ ( (,) โ€˜ ( ๐บ โ€˜ ๐‘— ) ) ) โˆ– ( ๐ฟ โˆฉ ( (,) โ€˜ ( ๐บ โ€˜ ๐‘— ) ) ) )
214 incom โŠข ( ๐ด โˆฉ ( (,) โ€˜ ( ๐บ โ€˜ ๐‘— ) ) ) = ( ( (,) โ€˜ ( ๐บ โ€˜ ๐‘— ) ) โˆฉ ๐ด )
215 incom โŠข ( ๐ฟ โˆฉ ( (,) โ€˜ ( ๐บ โ€˜ ๐‘— ) ) ) = ( ( (,) โ€˜ ( ๐บ โ€˜ ๐‘— ) ) โˆฉ ๐ฟ )
216 214 215 difeq12i โŠข ( ( ๐ด โˆฉ ( (,) โ€˜ ( ๐บ โ€˜ ๐‘— ) ) ) โˆ– ( ๐ฟ โˆฉ ( (,) โ€˜ ( ๐บ โ€˜ ๐‘— ) ) ) ) = ( ( ( (,) โ€˜ ( ๐บ โ€˜ ๐‘— ) ) โˆฉ ๐ด ) โˆ– ( ( (,) โ€˜ ( ๐บ โ€˜ ๐‘— ) ) โˆฉ ๐ฟ ) )
217 213 216 eqtri โŠข ( ( ๐ด โˆ– ๐ฟ ) โˆฉ ( (,) โ€˜ ( ๐บ โ€˜ ๐‘— ) ) ) = ( ( ( (,) โ€˜ ( ๐บ โ€˜ ๐‘— ) ) โˆฉ ๐ด ) โˆ– ( ( (,) โ€˜ ( ๐บ โ€˜ ๐‘— ) ) โˆฉ ๐ฟ ) )
218 82 eqcomd โŠข ( ๐œ‘ โ†’ ( ๐ฟ โˆช โˆช ๐‘– โˆˆ ( โ„คโ‰ฅ โ€˜ ( ๐‘ + 1 ) ) ( (,) โ€˜ ( ๐น โ€˜ ๐‘– ) ) ) = ๐ด )
219 80 ineq1d โŠข ( ๐œ‘ โ†’ ( ๐ฟ โˆฉ โˆช ๐‘– โˆˆ ( โ„คโ‰ฅ โ€˜ ( ๐‘ + 1 ) ) ( (,) โ€˜ ( ๐น โ€˜ ๐‘– ) ) ) = ( โˆช ๐‘– โˆˆ ( 1 ... ๐‘ ) ( (,) โ€˜ ( ๐น โ€˜ ๐‘– ) ) โˆฉ โˆช ๐‘– โˆˆ ( โ„คโ‰ฅ โ€˜ ( ๐‘ + 1 ) ) ( (,) โ€˜ ( ๐น โ€˜ ๐‘– ) ) ) )
220 2fveq3 โŠข ( ๐‘ฅ = ๐‘– โ†’ ( (,) โ€˜ ( ๐น โ€˜ ๐‘ฅ ) ) = ( (,) โ€˜ ( ๐น โ€˜ ๐‘– ) ) )
221 220 cbvdisjv โŠข ( Disj ๐‘ฅ โˆˆ โ„• ( (,) โ€˜ ( ๐น โ€˜ ๐‘ฅ ) ) โ†” Disj ๐‘– โˆˆ โ„• ( (,) โ€˜ ( ๐น โ€˜ ๐‘– ) ) )
222 2 221 sylib โŠข ( ๐œ‘ โ†’ Disj ๐‘– โˆˆ โ„• ( (,) โ€˜ ( ๐น โ€˜ ๐‘– ) ) )
223 fz1ssnn โŠข ( 1 ... ๐‘ ) โІ โ„•
224 223 a1i โŠข ( ๐œ‘ โ†’ ( 1 ... ๐‘ ) โІ โ„• )
225 uzss โŠข ( ( ๐‘ + 1 ) โˆˆ ( โ„คโ‰ฅ โ€˜ 1 ) โ†’ ( โ„คโ‰ฅ โ€˜ ( ๐‘ + 1 ) ) โІ ( โ„คโ‰ฅ โ€˜ 1 ) )
226 43 225 syl โŠข ( ๐œ‘ โ†’ ( โ„คโ‰ฅ โ€˜ ( ๐‘ + 1 ) ) โІ ( โ„คโ‰ฅ โ€˜ 1 ) )
227 226 41 sseqtrrdi โŠข ( ๐œ‘ โ†’ ( โ„คโ‰ฅ โ€˜ ( ๐‘ + 1 ) ) โІ โ„• )
228 51 ineq1d โŠข ( ๐œ‘ โ†’ ( ( 1 ... ( ( ๐‘ + 1 ) โˆ’ 1 ) ) โˆฉ ( โ„คโ‰ฅ โ€˜ ( ๐‘ + 1 ) ) ) = ( ( 1 ... ๐‘ ) โˆฉ ( โ„คโ‰ฅ โ€˜ ( ๐‘ + 1 ) ) ) )
229 uzdisj โŠข ( ( 1 ... ( ( ๐‘ + 1 ) โˆ’ 1 ) ) โˆฉ ( โ„คโ‰ฅ โ€˜ ( ๐‘ + 1 ) ) ) = โˆ…
230 228 229 eqtr3di โŠข ( ๐œ‘ โ†’ ( ( 1 ... ๐‘ ) โˆฉ ( โ„คโ‰ฅ โ€˜ ( ๐‘ + 1 ) ) ) = โˆ… )
231 disjiun โŠข ( ( Disj ๐‘– โˆˆ โ„• ( (,) โ€˜ ( ๐น โ€˜ ๐‘– ) ) โˆง ( ( 1 ... ๐‘ ) โІ โ„• โˆง ( โ„คโ‰ฅ โ€˜ ( ๐‘ + 1 ) ) โІ โ„• โˆง ( ( 1 ... ๐‘ ) โˆฉ ( โ„คโ‰ฅ โ€˜ ( ๐‘ + 1 ) ) ) = โˆ… ) ) โ†’ ( โˆช ๐‘– โˆˆ ( 1 ... ๐‘ ) ( (,) โ€˜ ( ๐น โ€˜ ๐‘– ) ) โˆฉ โˆช ๐‘– โˆˆ ( โ„คโ‰ฅ โ€˜ ( ๐‘ + 1 ) ) ( (,) โ€˜ ( ๐น โ€˜ ๐‘– ) ) ) = โˆ… )
232 222 224 227 230 231 syl13anc โŠข ( ๐œ‘ โ†’ ( โˆช ๐‘– โˆˆ ( 1 ... ๐‘ ) ( (,) โ€˜ ( ๐น โ€˜ ๐‘– ) ) โˆฉ โˆช ๐‘– โˆˆ ( โ„คโ‰ฅ โ€˜ ( ๐‘ + 1 ) ) ( (,) โ€˜ ( ๐น โ€˜ ๐‘– ) ) ) = โˆ… )
233 219 232 eqtrd โŠข ( ๐œ‘ โ†’ ( ๐ฟ โˆฉ โˆช ๐‘– โˆˆ ( โ„คโ‰ฅ โ€˜ ( ๐‘ + 1 ) ) ( (,) โ€˜ ( ๐น โ€˜ ๐‘– ) ) ) = โˆ… )
234 uneqdifeq โŠข ( ( ๐ฟ โІ ๐ด โˆง ( ๐ฟ โˆฉ โˆช ๐‘– โˆˆ ( โ„คโ‰ฅ โ€˜ ( ๐‘ + 1 ) ) ( (,) โ€˜ ( ๐น โ€˜ ๐‘– ) ) ) = โˆ… ) โ†’ ( ( ๐ฟ โˆช โˆช ๐‘– โˆˆ ( โ„คโ‰ฅ โ€˜ ( ๐‘ + 1 ) ) ( (,) โ€˜ ( ๐น โ€˜ ๐‘– ) ) ) = ๐ด โ†” ( ๐ด โˆ– ๐ฟ ) = โˆช ๐‘– โˆˆ ( โ„คโ‰ฅ โ€˜ ( ๐‘ + 1 ) ) ( (,) โ€˜ ( ๐น โ€˜ ๐‘– ) ) ) )
235 207 233 234 sylancr โŠข ( ๐œ‘ โ†’ ( ( ๐ฟ โˆช โˆช ๐‘– โˆˆ ( โ„คโ‰ฅ โ€˜ ( ๐‘ + 1 ) ) ( (,) โ€˜ ( ๐น โ€˜ ๐‘– ) ) ) = ๐ด โ†” ( ๐ด โˆ– ๐ฟ ) = โˆช ๐‘– โˆˆ ( โ„คโ‰ฅ โ€˜ ( ๐‘ + 1 ) ) ( (,) โ€˜ ( ๐น โ€˜ ๐‘– ) ) ) )
236 218 235 mpbid โŠข ( ๐œ‘ โ†’ ( ๐ด โˆ– ๐ฟ ) = โˆช ๐‘– โˆˆ ( โ„คโ‰ฅ โ€˜ ( ๐‘ + 1 ) ) ( (,) โ€˜ ( ๐น โ€˜ ๐‘– ) ) )
237 236 adantr โŠข ( ( ๐œ‘ โˆง ๐‘— โˆˆ ( 1 ... ๐‘€ ) ) โ†’ ( ๐ด โˆ– ๐ฟ ) = โˆช ๐‘– โˆˆ ( โ„คโ‰ฅ โ€˜ ( ๐‘ + 1 ) ) ( (,) โ€˜ ( ๐น โ€˜ ๐‘– ) ) )
238 237 ineq2d โŠข ( ( ๐œ‘ โˆง ๐‘— โˆˆ ( 1 ... ๐‘€ ) ) โ†’ ( ( (,) โ€˜ ( ๐บ โ€˜ ๐‘— ) ) โˆฉ ( ๐ด โˆ– ๐ฟ ) ) = ( ( (,) โ€˜ ( ๐บ โ€˜ ๐‘— ) ) โˆฉ โˆช ๐‘– โˆˆ ( โ„คโ‰ฅ โ€˜ ( ๐‘ + 1 ) ) ( (,) โ€˜ ( ๐น โ€˜ ๐‘– ) ) ) )
239 incom โŠข ( ( ๐ด โˆ– ๐ฟ ) โˆฉ ( (,) โ€˜ ( ๐บ โ€˜ ๐‘— ) ) ) = ( ( (,) โ€˜ ( ๐บ โ€˜ ๐‘— ) ) โˆฉ ( ๐ด โˆ– ๐ฟ ) )
240 104 101 eqtri โŠข โˆช ๐‘– โˆˆ ( โ„คโ‰ฅ โ€˜ ( ๐‘ + 1 ) ) ( ( (,) โ€˜ ( ๐น โ€˜ ๐‘– ) ) โˆฉ ( (,) โ€˜ ( ๐บ โ€˜ ๐‘— ) ) ) = ( ( (,) โ€˜ ( ๐บ โ€˜ ๐‘— ) ) โˆฉ โˆช ๐‘– โˆˆ ( โ„คโ‰ฅ โ€˜ ( ๐‘ + 1 ) ) ( (,) โ€˜ ( ๐น โ€˜ ๐‘– ) ) )
241 238 239 240 3eqtr4g โŠข ( ( ๐œ‘ โˆง ๐‘— โˆˆ ( 1 ... ๐‘€ ) ) โ†’ ( ( ๐ด โˆ– ๐ฟ ) โˆฉ ( (,) โ€˜ ( ๐บ โ€˜ ๐‘— ) ) ) = โˆช ๐‘– โˆˆ ( โ„คโ‰ฅ โ€˜ ( ๐‘ + 1 ) ) ( ( (,) โ€˜ ( ๐น โ€˜ ๐‘– ) ) โˆฉ ( (,) โ€˜ ( ๐บ โ€˜ ๐‘— ) ) ) )
242 217 241 eqtr3id โŠข ( ( ๐œ‘ โˆง ๐‘— โˆˆ ( 1 ... ๐‘€ ) ) โ†’ ( ( ( (,) โ€˜ ( ๐บ โ€˜ ๐‘— ) ) โˆฉ ๐ด ) โˆ– ( ( (,) โ€˜ ( ๐บ โ€˜ ๐‘— ) ) โˆฉ ๐ฟ ) ) = โˆช ๐‘– โˆˆ ( โ„คโ‰ฅ โ€˜ ( ๐‘ + 1 ) ) ( ( (,) โ€˜ ( ๐น โ€˜ ๐‘– ) ) โˆฉ ( (,) โ€˜ ( ๐บ โ€˜ ๐‘— ) ) ) )
243 242 fveq2d โŠข ( ( ๐œ‘ โˆง ๐‘— โˆˆ ( 1 ... ๐‘€ ) ) โ†’ ( vol* โ€˜ ( ( ( (,) โ€˜ ( ๐บ โ€˜ ๐‘— ) ) โˆฉ ๐ด ) โˆ– ( ( (,) โ€˜ ( ๐บ โ€˜ ๐‘— ) ) โˆฉ ๐ฟ ) ) ) = ( vol* โ€˜ โˆช ๐‘– โˆˆ ( โ„คโ‰ฅ โ€˜ ( ๐‘ + 1 ) ) ( ( (,) โ€˜ ( ๐น โ€˜ ๐‘– ) ) โˆฉ ( (,) โ€˜ ( ๐บ โ€˜ ๐‘— ) ) ) ) )
244 212 243 oveq12d โŠข ( ( ๐œ‘ โˆง ๐‘— โˆˆ ( 1 ... ๐‘€ ) ) โ†’ ( ( vol* โ€˜ ( ( ( (,) โ€˜ ( ๐บ โ€˜ ๐‘— ) ) โˆฉ ๐ด ) โˆฉ ( ( (,) โ€˜ ( ๐บ โ€˜ ๐‘— ) ) โˆฉ ๐ฟ ) ) ) + ( vol* โ€˜ ( ( ( (,) โ€˜ ( ๐บ โ€˜ ๐‘— ) ) โˆฉ ๐ด ) โˆ– ( ( (,) โ€˜ ( ๐บ โ€˜ ๐‘— ) ) โˆฉ ๐ฟ ) ) ) ) = ( ( vol* โ€˜ ( ( (,) โ€˜ ( ๐บ โ€˜ ๐‘— ) ) โˆฉ ๐ฟ ) ) + ( vol* โ€˜ โˆช ๐‘– โˆˆ ( โ„คโ‰ฅ โ€˜ ( ๐‘ + 1 ) ) ( ( (,) โ€˜ ( ๐น โ€˜ ๐‘– ) ) โˆฉ ( (,) โ€˜ ( ๐บ โ€˜ ๐‘— ) ) ) ) ) )
245 204 244 eqtrd โŠข ( ( ๐œ‘ โˆง ๐‘— โˆˆ ( 1 ... ๐‘€ ) ) โ†’ ( vol* โ€˜ ( ( (,) โ€˜ ( ๐บ โ€˜ ๐‘— ) ) โˆฉ ๐ด ) ) = ( ( vol* โ€˜ ( ( (,) โ€˜ ( ๐บ โ€˜ ๐‘— ) ) โˆฉ ๐ฟ ) ) + ( vol* โ€˜ โˆช ๐‘– โˆˆ ( โ„คโ‰ฅ โ€˜ ( ๐‘ + 1 ) ) ( ( (,) โ€˜ ( ๐น โ€˜ ๐‘– ) ) โˆฉ ( (,) โ€˜ ( ๐บ โ€˜ ๐‘— ) ) ) ) ) )
246 202 142 resubcld โŠข ( ( ๐œ‘ โˆง ๐‘— โˆˆ ( 1 ... ๐‘€ ) ) โ†’ ( ( vol* โ€˜ ( ( (,) โ€˜ ( ๐บ โ€˜ ๐‘— ) ) โˆฉ ๐ด ) ) โˆ’ ( ๐ถ / ๐‘€ ) ) โˆˆ โ„ )
247 inss2 โŠข ( ( (,) โ€˜ ( ๐น โ€˜ ๐‘– ) ) โˆฉ ( (,) โ€˜ ( ๐บ โ€˜ ๐‘— ) ) ) โІ ( (,) โ€˜ ( ๐บ โ€˜ ๐‘— ) )
248 190 adantr โŠข ( ( ( ๐œ‘ โˆง ๐‘— โˆˆ ( 1 ... ๐‘€ ) ) โˆง ๐‘– โˆˆ ( 1 ... ๐‘ ) ) โ†’ ( (,) โ€˜ ( ๐บ โ€˜ ๐‘— ) ) โІ โ„ )
249 200 adantr โŠข ( ( ( ๐œ‘ โˆง ๐‘— โˆˆ ( 1 ... ๐‘€ ) ) โˆง ๐‘– โˆˆ ( 1 ... ๐‘ ) ) โ†’ ( vol* โ€˜ ( (,) โ€˜ ( ๐บ โ€˜ ๐‘— ) ) ) โˆˆ โ„ )
250 ovolsscl โŠข ( ( ( ( (,) โ€˜ ( ๐น โ€˜ ๐‘– ) ) โˆฉ ( (,) โ€˜ ( ๐บ โ€˜ ๐‘— ) ) ) โІ ( (,) โ€˜ ( ๐บ โ€˜ ๐‘— ) ) โˆง ( (,) โ€˜ ( ๐บ โ€˜ ๐‘— ) ) โІ โ„ โˆง ( vol* โ€˜ ( (,) โ€˜ ( ๐บ โ€˜ ๐‘— ) ) ) โˆˆ โ„ ) โ†’ ( vol* โ€˜ ( ( (,) โ€˜ ( ๐น โ€˜ ๐‘– ) ) โˆฉ ( (,) โ€˜ ( ๐บ โ€˜ ๐‘— ) ) ) ) โˆˆ โ„ )
251 247 248 249 250 mp3an2i โŠข ( ( ( ๐œ‘ โˆง ๐‘— โˆˆ ( 1 ... ๐‘€ ) ) โˆง ๐‘– โˆˆ ( 1 ... ๐‘ ) ) โ†’ ( vol* โ€˜ ( ( (,) โ€˜ ( ๐น โ€˜ ๐‘– ) ) โˆฉ ( (,) โ€˜ ( ๐บ โ€˜ ๐‘— ) ) ) ) โˆˆ โ„ )
252 150 251 fsumrecl โŠข ( ( ๐œ‘ โˆง ๐‘— โˆˆ ( 1 ... ๐‘€ ) ) โ†’ ฮฃ ๐‘– โˆˆ ( 1 ... ๐‘ ) ( vol* โ€˜ ( ( (,) โ€˜ ( ๐น โ€˜ ๐‘– ) ) โˆฉ ( (,) โ€˜ ( ๐บ โ€˜ ๐‘— ) ) ) ) โˆˆ โ„ )
253 15 r19.21bi โŠข ( ( ๐œ‘ โˆง ๐‘— โˆˆ ( 1 ... ๐‘€ ) ) โ†’ ( abs โ€˜ ( ฮฃ ๐‘– โˆˆ ( 1 ... ๐‘ ) ( vol* โ€˜ ( ( (,) โ€˜ ( ๐น โ€˜ ๐‘– ) ) โˆฉ ( (,) โ€˜ ( ๐บ โ€˜ ๐‘— ) ) ) ) โˆ’ ( vol* โ€˜ ( ( (,) โ€˜ ( ๐บ โ€˜ ๐‘— ) ) โˆฉ ๐ด ) ) ) ) < ( ๐ถ / ๐‘€ ) )
254 252 202 142 absdifltd โŠข ( ( ๐œ‘ โˆง ๐‘— โˆˆ ( 1 ... ๐‘€ ) ) โ†’ ( ( abs โ€˜ ( ฮฃ ๐‘– โˆˆ ( 1 ... ๐‘ ) ( vol* โ€˜ ( ( (,) โ€˜ ( ๐น โ€˜ ๐‘– ) ) โˆฉ ( (,) โ€˜ ( ๐บ โ€˜ ๐‘— ) ) ) ) โˆ’ ( vol* โ€˜ ( ( (,) โ€˜ ( ๐บ โ€˜ ๐‘— ) ) โˆฉ ๐ด ) ) ) ) < ( ๐ถ / ๐‘€ ) โ†” ( ( ( vol* โ€˜ ( ( (,) โ€˜ ( ๐บ โ€˜ ๐‘— ) ) โˆฉ ๐ด ) ) โˆ’ ( ๐ถ / ๐‘€ ) ) < ฮฃ ๐‘– โˆˆ ( 1 ... ๐‘ ) ( vol* โ€˜ ( ( (,) โ€˜ ( ๐น โ€˜ ๐‘– ) ) โˆฉ ( (,) โ€˜ ( ๐บ โ€˜ ๐‘— ) ) ) ) โˆง ฮฃ ๐‘– โˆˆ ( 1 ... ๐‘ ) ( vol* โ€˜ ( ( (,) โ€˜ ( ๐น โ€˜ ๐‘– ) ) โˆฉ ( (,) โ€˜ ( ๐บ โ€˜ ๐‘— ) ) ) ) < ( ( vol* โ€˜ ( ( (,) โ€˜ ( ๐บ โ€˜ ๐‘— ) ) โˆฉ ๐ด ) ) + ( ๐ถ / ๐‘€ ) ) ) ) )
255 253 254 mpbid โŠข ( ( ๐œ‘ โˆง ๐‘— โˆˆ ( 1 ... ๐‘€ ) ) โ†’ ( ( ( vol* โ€˜ ( ( (,) โ€˜ ( ๐บ โ€˜ ๐‘— ) ) โˆฉ ๐ด ) ) โˆ’ ( ๐ถ / ๐‘€ ) ) < ฮฃ ๐‘– โˆˆ ( 1 ... ๐‘ ) ( vol* โ€˜ ( ( (,) โ€˜ ( ๐น โ€˜ ๐‘– ) ) โˆฉ ( (,) โ€˜ ( ๐บ โ€˜ ๐‘— ) ) ) ) โˆง ฮฃ ๐‘– โˆˆ ( 1 ... ๐‘ ) ( vol* โ€˜ ( ( (,) โ€˜ ( ๐น โ€˜ ๐‘– ) ) โˆฉ ( (,) โ€˜ ( ๐บ โ€˜ ๐‘— ) ) ) ) < ( ( vol* โ€˜ ( ( (,) โ€˜ ( ๐บ โ€˜ ๐‘— ) ) โˆฉ ๐ด ) ) + ( ๐ถ / ๐‘€ ) ) ) )
256 255 simpld โŠข ( ( ๐œ‘ โˆง ๐‘— โˆˆ ( 1 ... ๐‘€ ) ) โ†’ ( ( vol* โ€˜ ( ( (,) โ€˜ ( ๐บ โ€˜ ๐‘— ) ) โˆฉ ๐ด ) ) โˆ’ ( ๐ถ / ๐‘€ ) ) < ฮฃ ๐‘– โˆˆ ( 1 ... ๐‘ ) ( vol* โ€˜ ( ( (,) โ€˜ ( ๐น โ€˜ ๐‘– ) ) โˆฉ ( (,) โ€˜ ( ๐บ โ€˜ ๐‘— ) ) ) ) )
257 246 252 256 ltled โŠข ( ( ๐œ‘ โˆง ๐‘— โˆˆ ( 1 ... ๐‘€ ) ) โ†’ ( ( vol* โ€˜ ( ( (,) โ€˜ ( ๐บ โ€˜ ๐‘— ) ) โˆฉ ๐ด ) ) โˆ’ ( ๐ถ / ๐‘€ ) ) โ‰ค ฮฃ ๐‘– โˆˆ ( 1 ... ๐‘ ) ( vol* โ€˜ ( ( (,) โ€˜ ( ๐น โ€˜ ๐‘– ) ) โˆฉ ( (,) โ€˜ ( ๐บ โ€˜ ๐‘— ) ) ) ) )
258 149 fveq2d โŠข ( ( ๐œ‘ โˆง ๐‘— โˆˆ ( 1 ... ๐‘€ ) ) โ†’ ( vol* โ€˜ ( ( (,) โ€˜ ( ๐บ โ€˜ ๐‘— ) ) โˆฉ ๐ฟ ) ) = ( vol* โ€˜ โˆช ๐‘– โˆˆ ( 1 ... ๐‘ ) ( ( (,) โ€˜ ( ๐น โ€˜ ๐‘– ) ) โˆฉ ( (,) โ€˜ ( ๐บ โ€˜ ๐‘— ) ) ) ) )
259 mblvol โŠข ( ( ( (,) โ€˜ ( ๐น โ€˜ ๐‘– ) ) โˆฉ ( (,) โ€˜ ( ๐บ โ€˜ ๐‘— ) ) ) โˆˆ dom vol โ†’ ( vol โ€˜ ( ( (,) โ€˜ ( ๐น โ€˜ ๐‘– ) ) โˆฉ ( (,) โ€˜ ( ๐บ โ€˜ ๐‘— ) ) ) ) = ( vol* โ€˜ ( ( (,) โ€˜ ( ๐น โ€˜ ๐‘– ) ) โˆฉ ( (,) โ€˜ ( ๐บ โ€˜ ๐‘— ) ) ) ) )
260 174 259 syl โŠข ( ( ( ๐œ‘ โˆง ๐‘— โˆˆ ( 1 ... ๐‘€ ) ) โˆง ๐‘– โˆˆ ( 1 ... ๐‘ ) ) โ†’ ( vol โ€˜ ( ( (,) โ€˜ ( ๐น โ€˜ ๐‘– ) ) โˆฉ ( (,) โ€˜ ( ๐บ โ€˜ ๐‘— ) ) ) ) = ( vol* โ€˜ ( ( (,) โ€˜ ( ๐น โ€˜ ๐‘– ) ) โˆฉ ( (,) โ€˜ ( ๐บ โ€˜ ๐‘— ) ) ) ) )
261 260 251 eqeltrd โŠข ( ( ( ๐œ‘ โˆง ๐‘— โˆˆ ( 1 ... ๐‘€ ) ) โˆง ๐‘– โˆˆ ( 1 ... ๐‘ ) ) โ†’ ( vol โ€˜ ( ( (,) โ€˜ ( ๐น โ€˜ ๐‘– ) ) โˆฉ ( (,) โ€˜ ( ๐บ โ€˜ ๐‘— ) ) ) ) โˆˆ โ„ )
262 174 261 jca โŠข ( ( ( ๐œ‘ โˆง ๐‘— โˆˆ ( 1 ... ๐‘€ ) ) โˆง ๐‘– โˆˆ ( 1 ... ๐‘ ) ) โ†’ ( ( ( (,) โ€˜ ( ๐น โ€˜ ๐‘– ) ) โˆฉ ( (,) โ€˜ ( ๐บ โ€˜ ๐‘— ) ) ) โˆˆ dom vol โˆง ( vol โ€˜ ( ( (,) โ€˜ ( ๐น โ€˜ ๐‘– ) ) โˆฉ ( (,) โ€˜ ( ๐บ โ€˜ ๐‘— ) ) ) ) โˆˆ โ„ ) )
263 262 ralrimiva โŠข ( ( ๐œ‘ โˆง ๐‘— โˆˆ ( 1 ... ๐‘€ ) ) โ†’ โˆ€ ๐‘– โˆˆ ( 1 ... ๐‘ ) ( ( ( (,) โ€˜ ( ๐น โ€˜ ๐‘– ) ) โˆฉ ( (,) โ€˜ ( ๐บ โ€˜ ๐‘— ) ) ) โˆˆ dom vol โˆง ( vol โ€˜ ( ( (,) โ€˜ ( ๐น โ€˜ ๐‘– ) ) โˆฉ ( (,) โ€˜ ( ๐บ โ€˜ ๐‘— ) ) ) ) โˆˆ โ„ ) )
264 inss1 โŠข ( ( (,) โ€˜ ( ๐น โ€˜ ๐‘– ) ) โˆฉ ( (,) โ€˜ ( ๐บ โ€˜ ๐‘— ) ) ) โІ ( (,) โ€˜ ( ๐น โ€˜ ๐‘– ) )
265 264 rgenw โŠข โˆ€ ๐‘– โˆˆ โ„• ( ( (,) โ€˜ ( ๐น โ€˜ ๐‘– ) ) โˆฉ ( (,) โ€˜ ( ๐บ โ€˜ ๐‘— ) ) ) โІ ( (,) โ€˜ ( ๐น โ€˜ ๐‘– ) )
266 222 adantr โŠข ( ( ๐œ‘ โˆง ๐‘— โˆˆ ( 1 ... ๐‘€ ) ) โ†’ Disj ๐‘– โˆˆ โ„• ( (,) โ€˜ ( ๐น โ€˜ ๐‘– ) ) )
267 disjss2 โŠข ( โˆ€ ๐‘– โˆˆ โ„• ( ( (,) โ€˜ ( ๐น โ€˜ ๐‘– ) ) โˆฉ ( (,) โ€˜ ( ๐บ โ€˜ ๐‘— ) ) ) โІ ( (,) โ€˜ ( ๐น โ€˜ ๐‘– ) ) โ†’ ( Disj ๐‘– โˆˆ โ„• ( (,) โ€˜ ( ๐น โ€˜ ๐‘– ) ) โ†’ Disj ๐‘– โˆˆ โ„• ( ( (,) โ€˜ ( ๐น โ€˜ ๐‘– ) ) โˆฉ ( (,) โ€˜ ( ๐บ โ€˜ ๐‘— ) ) ) ) )
268 265 266 267 mpsyl โŠข ( ( ๐œ‘ โˆง ๐‘— โˆˆ ( 1 ... ๐‘€ ) ) โ†’ Disj ๐‘– โˆˆ โ„• ( ( (,) โ€˜ ( ๐น โ€˜ ๐‘– ) ) โˆฉ ( (,) โ€˜ ( ๐บ โ€˜ ๐‘— ) ) ) )
269 disjss1 โŠข ( ( 1 ... ๐‘ ) โІ โ„• โ†’ ( Disj ๐‘– โˆˆ โ„• ( ( (,) โ€˜ ( ๐น โ€˜ ๐‘– ) ) โˆฉ ( (,) โ€˜ ( ๐บ โ€˜ ๐‘— ) ) ) โ†’ Disj ๐‘– โˆˆ ( 1 ... ๐‘ ) ( ( (,) โ€˜ ( ๐น โ€˜ ๐‘– ) ) โˆฉ ( (,) โ€˜ ( ๐บ โ€˜ ๐‘— ) ) ) ) )
270 223 268 269 mpsyl โŠข ( ( ๐œ‘ โˆง ๐‘— โˆˆ ( 1 ... ๐‘€ ) ) โ†’ Disj ๐‘– โˆˆ ( 1 ... ๐‘ ) ( ( (,) โ€˜ ( ๐น โ€˜ ๐‘– ) ) โˆฉ ( (,) โ€˜ ( ๐บ โ€˜ ๐‘— ) ) ) )
271 volfiniun โŠข ( ( ( 1 ... ๐‘ ) โˆˆ Fin โˆง โˆ€ ๐‘– โˆˆ ( 1 ... ๐‘ ) ( ( ( (,) โ€˜ ( ๐น โ€˜ ๐‘– ) ) โˆฉ ( (,) โ€˜ ( ๐บ โ€˜ ๐‘— ) ) ) โˆˆ dom vol โˆง ( vol โ€˜ ( ( (,) โ€˜ ( ๐น โ€˜ ๐‘– ) ) โˆฉ ( (,) โ€˜ ( ๐บ โ€˜ ๐‘— ) ) ) ) โˆˆ โ„ ) โˆง Disj ๐‘– โˆˆ ( 1 ... ๐‘ ) ( ( (,) โ€˜ ( ๐น โ€˜ ๐‘– ) ) โˆฉ ( (,) โ€˜ ( ๐บ โ€˜ ๐‘— ) ) ) ) โ†’ ( vol โ€˜ โˆช ๐‘– โˆˆ ( 1 ... ๐‘ ) ( ( (,) โ€˜ ( ๐น โ€˜ ๐‘– ) ) โˆฉ ( (,) โ€˜ ( ๐บ โ€˜ ๐‘— ) ) ) ) = ฮฃ ๐‘– โˆˆ ( 1 ... ๐‘ ) ( vol โ€˜ ( ( (,) โ€˜ ( ๐น โ€˜ ๐‘– ) ) โˆฉ ( (,) โ€˜ ( ๐บ โ€˜ ๐‘— ) ) ) ) )
272 150 263 270 271 syl3anc โŠข ( ( ๐œ‘ โˆง ๐‘— โˆˆ ( 1 ... ๐‘€ ) ) โ†’ ( vol โ€˜ โˆช ๐‘– โˆˆ ( 1 ... ๐‘ ) ( ( (,) โ€˜ ( ๐น โ€˜ ๐‘– ) ) โˆฉ ( (,) โ€˜ ( ๐บ โ€˜ ๐‘— ) ) ) ) = ฮฃ ๐‘– โˆˆ ( 1 ... ๐‘ ) ( vol โ€˜ ( ( (,) โ€˜ ( ๐น โ€˜ ๐‘– ) ) โˆฉ ( (,) โ€˜ ( ๐บ โ€˜ ๐‘— ) ) ) ) )
273 mblvol โŠข ( โˆช ๐‘– โˆˆ ( 1 ... ๐‘ ) ( ( (,) โ€˜ ( ๐น โ€˜ ๐‘– ) ) โˆฉ ( (,) โ€˜ ( ๐บ โ€˜ ๐‘— ) ) ) โˆˆ dom vol โ†’ ( vol โ€˜ โˆช ๐‘– โˆˆ ( 1 ... ๐‘ ) ( ( (,) โ€˜ ( ๐น โ€˜ ๐‘– ) ) โˆฉ ( (,) โ€˜ ( ๐บ โ€˜ ๐‘— ) ) ) ) = ( vol* โ€˜ โˆช ๐‘– โˆˆ ( 1 ... ๐‘ ) ( ( (,) โ€˜ ( ๐น โ€˜ ๐‘– ) ) โˆฉ ( (,) โ€˜ ( ๐บ โ€˜ ๐‘— ) ) ) ) )
274 177 273 syl โŠข ( ( ๐œ‘ โˆง ๐‘— โˆˆ ( 1 ... ๐‘€ ) ) โ†’ ( vol โ€˜ โˆช ๐‘– โˆˆ ( 1 ... ๐‘ ) ( ( (,) โ€˜ ( ๐น โ€˜ ๐‘– ) ) โˆฉ ( (,) โ€˜ ( ๐บ โ€˜ ๐‘— ) ) ) ) = ( vol* โ€˜ โˆช ๐‘– โˆˆ ( 1 ... ๐‘ ) ( ( (,) โ€˜ ( ๐น โ€˜ ๐‘– ) ) โˆฉ ( (,) โ€˜ ( ๐บ โ€˜ ๐‘— ) ) ) ) )
275 260 sumeq2dv โŠข ( ( ๐œ‘ โˆง ๐‘— โˆˆ ( 1 ... ๐‘€ ) ) โ†’ ฮฃ ๐‘– โˆˆ ( 1 ... ๐‘ ) ( vol โ€˜ ( ( (,) โ€˜ ( ๐น โ€˜ ๐‘– ) ) โˆฉ ( (,) โ€˜ ( ๐บ โ€˜ ๐‘— ) ) ) ) = ฮฃ ๐‘– โˆˆ ( 1 ... ๐‘ ) ( vol* โ€˜ ( ( (,) โ€˜ ( ๐น โ€˜ ๐‘– ) ) โˆฉ ( (,) โ€˜ ( ๐บ โ€˜ ๐‘— ) ) ) ) )
276 272 274 275 3eqtr3d โŠข ( ( ๐œ‘ โˆง ๐‘— โˆˆ ( 1 ... ๐‘€ ) ) โ†’ ( vol* โ€˜ โˆช ๐‘– โˆˆ ( 1 ... ๐‘ ) ( ( (,) โ€˜ ( ๐น โ€˜ ๐‘– ) ) โˆฉ ( (,) โ€˜ ( ๐บ โ€˜ ๐‘— ) ) ) ) = ฮฃ ๐‘– โˆˆ ( 1 ... ๐‘ ) ( vol* โ€˜ ( ( (,) โ€˜ ( ๐น โ€˜ ๐‘– ) ) โˆฉ ( (,) โ€˜ ( ๐บ โ€˜ ๐‘— ) ) ) ) )
277 258 276 eqtrd โŠข ( ( ๐œ‘ โˆง ๐‘— โˆˆ ( 1 ... ๐‘€ ) ) โ†’ ( vol* โ€˜ ( ( (,) โ€˜ ( ๐บ โ€˜ ๐‘— ) ) โˆฉ ๐ฟ ) ) = ฮฃ ๐‘– โˆˆ ( 1 ... ๐‘ ) ( vol* โ€˜ ( ( (,) โ€˜ ( ๐น โ€˜ ๐‘– ) ) โˆฉ ( (,) โ€˜ ( ๐บ โ€˜ ๐‘— ) ) ) ) )
278 257 277 breqtrrd โŠข ( ( ๐œ‘ โˆง ๐‘— โˆˆ ( 1 ... ๐‘€ ) ) โ†’ ( ( vol* โ€˜ ( ( (,) โ€˜ ( ๐บ โ€˜ ๐‘— ) ) โˆฉ ๐ด ) ) โˆ’ ( ๐ถ / ๐‘€ ) ) โ‰ค ( vol* โ€˜ ( ( (,) โ€˜ ( ๐บ โ€˜ ๐‘— ) ) โˆฉ ๐ฟ ) ) )
279 277 252 eqeltrd โŠข ( ( ๐œ‘ โˆง ๐‘— โˆˆ ( 1 ... ๐‘€ ) ) โ†’ ( vol* โ€˜ ( ( (,) โ€˜ ( ๐บ โ€˜ ๐‘— ) ) โˆฉ ๐ฟ ) ) โˆˆ โ„ )
280 202 142 279 lesubaddd โŠข ( ( ๐œ‘ โˆง ๐‘— โˆˆ ( 1 ... ๐‘€ ) ) โ†’ ( ( ( vol* โ€˜ ( ( (,) โ€˜ ( ๐บ โ€˜ ๐‘— ) ) โˆฉ ๐ด ) ) โˆ’ ( ๐ถ / ๐‘€ ) ) โ‰ค ( vol* โ€˜ ( ( (,) โ€˜ ( ๐บ โ€˜ ๐‘— ) ) โˆฉ ๐ฟ ) ) โ†” ( vol* โ€˜ ( ( (,) โ€˜ ( ๐บ โ€˜ ๐‘— ) ) โˆฉ ๐ด ) ) โ‰ค ( ( vol* โ€˜ ( ( (,) โ€˜ ( ๐บ โ€˜ ๐‘— ) ) โˆฉ ๐ฟ ) ) + ( ๐ถ / ๐‘€ ) ) ) )
281 278 280 mpbid โŠข ( ( ๐œ‘ โˆง ๐‘— โˆˆ ( 1 ... ๐‘€ ) ) โ†’ ( vol* โ€˜ ( ( (,) โ€˜ ( ๐บ โ€˜ ๐‘— ) ) โˆฉ ๐ด ) ) โ‰ค ( ( vol* โ€˜ ( ( (,) โ€˜ ( ๐บ โ€˜ ๐‘— ) ) โˆฉ ๐ฟ ) ) + ( ๐ถ / ๐‘€ ) ) )
282 245 281 eqbrtrrd โŠข ( ( ๐œ‘ โˆง ๐‘— โˆˆ ( 1 ... ๐‘€ ) ) โ†’ ( ( vol* โ€˜ ( ( (,) โ€˜ ( ๐บ โ€˜ ๐‘— ) ) โˆฉ ๐ฟ ) ) + ( vol* โ€˜ โˆช ๐‘– โˆˆ ( โ„คโ‰ฅ โ€˜ ( ๐‘ + 1 ) ) ( ( (,) โ€˜ ( ๐น โ€˜ ๐‘– ) ) โˆฉ ( (,) โ€˜ ( ๐บ โ€˜ ๐‘— ) ) ) ) ) โ‰ค ( ( vol* โ€˜ ( ( (,) โ€˜ ( ๐บ โ€˜ ๐‘— ) ) โˆฉ ๐ฟ ) ) + ( ๐ถ / ๐‘€ ) ) )
283 134 142 279 leadd2d โŠข ( ( ๐œ‘ โˆง ๐‘— โˆˆ ( 1 ... ๐‘€ ) ) โ†’ ( ( vol* โ€˜ โˆช ๐‘– โˆˆ ( โ„คโ‰ฅ โ€˜ ( ๐‘ + 1 ) ) ( ( (,) โ€˜ ( ๐น โ€˜ ๐‘– ) ) โˆฉ ( (,) โ€˜ ( ๐บ โ€˜ ๐‘— ) ) ) ) โ‰ค ( ๐ถ / ๐‘€ ) โ†” ( ( vol* โ€˜ ( ( (,) โ€˜ ( ๐บ โ€˜ ๐‘— ) ) โˆฉ ๐ฟ ) ) + ( vol* โ€˜ โˆช ๐‘– โˆˆ ( โ„คโ‰ฅ โ€˜ ( ๐‘ + 1 ) ) ( ( (,) โ€˜ ( ๐น โ€˜ ๐‘– ) ) โˆฉ ( (,) โ€˜ ( ๐บ โ€˜ ๐‘— ) ) ) ) ) โ‰ค ( ( vol* โ€˜ ( ( (,) โ€˜ ( ๐บ โ€˜ ๐‘— ) ) โˆฉ ๐ฟ ) ) + ( ๐ถ / ๐‘€ ) ) ) )
284 282 283 mpbird โŠข ( ( ๐œ‘ โˆง ๐‘— โˆˆ ( 1 ... ๐‘€ ) ) โ†’ ( vol* โ€˜ โˆช ๐‘– โˆˆ ( โ„คโ‰ฅ โ€˜ ( ๐‘ + 1 ) ) ( ( (,) โ€˜ ( ๐น โ€˜ ๐‘– ) ) โˆฉ ( (,) โ€˜ ( ๐บ โ€˜ ๐‘— ) ) ) ) โ‰ค ( ๐ถ / ๐‘€ ) )
285 127 134 142 284 fsumle โŠข ( ๐œ‘ โ†’ ฮฃ ๐‘— โˆˆ ( 1 ... ๐‘€ ) ( vol* โ€˜ โˆช ๐‘– โˆˆ ( โ„คโ‰ฅ โ€˜ ( ๐‘ + 1 ) ) ( ( (,) โ€˜ ( ๐น โ€˜ ๐‘– ) ) โˆฉ ( (,) โ€˜ ( ๐บ โ€˜ ๐‘— ) ) ) ) โ‰ค ฮฃ ๐‘— โˆˆ ( 1 ... ๐‘€ ) ( ๐ถ / ๐‘€ ) )
286 141 recnd โŠข ( ๐œ‘ โ†’ ( ๐ถ / ๐‘€ ) โˆˆ โ„‚ )
287 fsumconst โŠข ( ( ( 1 ... ๐‘€ ) โˆˆ Fin โˆง ( ๐ถ / ๐‘€ ) โˆˆ โ„‚ ) โ†’ ฮฃ ๐‘— โˆˆ ( 1 ... ๐‘€ ) ( ๐ถ / ๐‘€ ) = ( ( โ™ฏ โ€˜ ( 1 ... ๐‘€ ) ) ยท ( ๐ถ / ๐‘€ ) ) )
288 127 286 287 syl2anc โŠข ( ๐œ‘ โ†’ ฮฃ ๐‘— โˆˆ ( 1 ... ๐‘€ ) ( ๐ถ / ๐‘€ ) = ( ( โ™ฏ โ€˜ ( 1 ... ๐‘€ ) ) ยท ( ๐ถ / ๐‘€ ) ) )
289 nnnn0 โŠข ( ๐‘€ โˆˆ โ„• โ†’ ๐‘€ โˆˆ โ„•0 )
290 hashfz1 โŠข ( ๐‘€ โˆˆ โ„•0 โ†’ ( โ™ฏ โ€˜ ( 1 ... ๐‘€ ) ) = ๐‘€ )
291 11 289 290 3syl โŠข ( ๐œ‘ โ†’ ( โ™ฏ โ€˜ ( 1 ... ๐‘€ ) ) = ๐‘€ )
292 291 oveq1d โŠข ( ๐œ‘ โ†’ ( ( โ™ฏ โ€˜ ( 1 ... ๐‘€ ) ) ยท ( ๐ถ / ๐‘€ ) ) = ( ๐‘€ ยท ( ๐ถ / ๐‘€ ) ) )
293 119 recnd โŠข ( ๐œ‘ โ†’ ๐ถ โˆˆ โ„‚ )
294 11 nncnd โŠข ( ๐œ‘ โ†’ ๐‘€ โˆˆ โ„‚ )
295 11 nnne0d โŠข ( ๐œ‘ โ†’ ๐‘€ โ‰  0 )
296 293 294 295 divcan2d โŠข ( ๐œ‘ โ†’ ( ๐‘€ ยท ( ๐ถ / ๐‘€ ) ) = ๐ถ )
297 288 292 296 3eqtrd โŠข ( ๐œ‘ โ†’ ฮฃ ๐‘— โˆˆ ( 1 ... ๐‘€ ) ( ๐ถ / ๐‘€ ) = ๐ถ )
298 285 297 breqtrd โŠข ( ๐œ‘ โ†’ ฮฃ ๐‘— โˆˆ ( 1 ... ๐‘€ ) ( vol* โ€˜ โˆช ๐‘– โˆˆ ( โ„คโ‰ฅ โ€˜ ( ๐‘ + 1 ) ) ( ( (,) โ€˜ ( ๐น โ€˜ ๐‘– ) ) โˆฉ ( (,) โ€˜ ( ๐บ โ€˜ ๐‘— ) ) ) ) โ‰ค ๐ถ )
299 117 135 119 140 298 letrd โŠข ( ๐œ‘ โ†’ ( vol* โ€˜ โˆช ๐‘— โˆˆ ( 1 ... ๐‘€ ) โˆช ๐‘– โˆˆ ( โ„คโ‰ฅ โ€˜ ( ๐‘ + 1 ) ) ( ( (,) โ€˜ ( ๐น โ€˜ ๐‘– ) ) โˆฉ ( (,) โ€˜ ( ๐บ โ€˜ ๐‘— ) ) ) ) โ‰ค ๐ถ )
300 117 119 39 299 leadd2dd โŠข ( ๐œ‘ โ†’ ( ( vol* โ€˜ ( ๐พ โˆฉ ๐ฟ ) ) + ( vol* โ€˜ โˆช ๐‘— โˆˆ ( 1 ... ๐‘€ ) โˆช ๐‘– โˆˆ ( โ„คโ‰ฅ โ€˜ ( ๐‘ + 1 ) ) ( ( (,) โ€˜ ( ๐น โ€˜ ๐‘– ) ) โˆฉ ( (,) โ€˜ ( ๐บ โ€˜ ๐‘— ) ) ) ) ) โ‰ค ( ( vol* โ€˜ ( ๐พ โˆฉ ๐ฟ ) ) + ๐ถ ) )
301 36 118 120 126 300 letrd โŠข ( ๐œ‘ โ†’ ( vol* โ€˜ ( ๐พ โˆฉ ๐ด ) ) โ‰ค ( ( vol* โ€˜ ( ๐พ โˆฉ ๐ฟ ) ) + ๐ถ ) )