Metamath Proof Explorer

Theorem voliunlem2

Description: Lemma for voliun . (Contributed by Mario Carneiro, 20-Mar-2014)

Ref Expression
Hypotheses voliunlem.3 ⊢ ( 𝜑 → 𝐹 : ℕ ⟶ dom vol )
voliunlem.5 ⊢ ( 𝜑 → Disj 𝑖 ∈ ℕ ( 𝐹 ‘ 𝑖 ) )
voliunlem.6 ⊢ 𝐻 = ( 𝑛 ∈ ℕ ↦ ( vol* ‘ ( 𝑥 ∩ ( 𝐹 ‘ 𝑛 ) ) ) )
Assertion voliunlem2 ( 𝜑 → ∪ ran 𝐹 ∈ dom vol )

Proof

Step Hyp Ref Expression
1 voliunlem.3 ⊢ ( 𝜑 → 𝐹 : ℕ ⟶ dom vol )
2 voliunlem.5 ⊢ ( 𝜑 → Disj 𝑖 ∈ ℕ ( 𝐹 ‘ 𝑖 ) )
3 voliunlem.6 ⊢ 𝐻 = ( 𝑛 ∈ ℕ ↦ ( vol* ‘ ( 𝑥 ∩ ( 𝐹 ‘ 𝑛 ) ) ) )
4 1 frnd ⊢ ( 𝜑 → ran 𝐹 ⊆ dom vol )
5 mblss ⊢ ( 𝑥 ∈ dom vol → 𝑥 ⊆ ℝ )
6 velpw ⊢ ( 𝑥 ∈ 𝒫 ℝ ↔ 𝑥 ⊆ ℝ )
7 5 6 sylibr ⊢ ( 𝑥 ∈ dom vol → 𝑥 ∈ 𝒫 ℝ )
8 7 ssriv ⊢ dom vol ⊆ 𝒫 ℝ
9 4 8 sstrdi ⊢ ( 𝜑 → ran 𝐹 ⊆ 𝒫 ℝ )
10 sspwuni ⊢ ( ran 𝐹 ⊆ 𝒫 ℝ ↔ ∪ ran 𝐹 ⊆ ℝ )
11 9 10 sylib ⊢ ( 𝜑 → ∪ ran 𝐹 ⊆ ℝ )
12 elpwi ⊢ ( 𝑥 ∈ 𝒫 ℝ → 𝑥 ⊆ ℝ )
13 inundif ⊢ ( ( 𝑥 ∩ ∪ ran 𝐹 ) ∪ ( 𝑥 ∖ ∪ ran 𝐹 ) ) = 𝑥
14 13 fveq2i ⊢ ( vol* ‘ ( ( 𝑥 ∩ ∪ ran 𝐹 ) ∪ ( 𝑥 ∖ ∪ ran 𝐹 ) ) ) = ( vol* ‘ 𝑥 )
15 inss1 ⊢ ( 𝑥 ∩ ∪ ran 𝐹 ) ⊆ 𝑥
16 simp2 ⊢ ( ( 𝜑 ∧ 𝑥 ⊆ ℝ ∧ ( vol* ‘ 𝑥 ) ∈ ℝ ) → 𝑥 ⊆ ℝ )
17 15 16 sstrid ⊢ ( ( 𝜑 ∧ 𝑥 ⊆ ℝ ∧ ( vol* ‘ 𝑥 ) ∈ ℝ ) → ( 𝑥 ∩ ∪ ran 𝐹 ) ⊆ ℝ )
18 ovolsscl ⊢ ( ( ( 𝑥 ∩ ∪ ran 𝐹 ) ⊆ 𝑥 ∧ 𝑥 ⊆ ℝ ∧ ( vol* ‘ 𝑥 ) ∈ ℝ ) → ( vol* ‘ ( 𝑥 ∩ ∪ ran 𝐹 ) ) ∈ ℝ )
19 15 18 mp3an1 ⊢ ( ( 𝑥 ⊆ ℝ ∧ ( vol* ‘ 𝑥 ) ∈ ℝ ) → ( vol* ‘ ( 𝑥 ∩ ∪ ran 𝐹 ) ) ∈ ℝ )
20 19 3adant1 ⊢ ( ( 𝜑 ∧ 𝑥 ⊆ ℝ ∧ ( vol* ‘ 𝑥 ) ∈ ℝ ) → ( vol* ‘ ( 𝑥 ∩ ∪ ran 𝐹 ) ) ∈ ℝ )
21 difss ⊢ ( 𝑥 ∖ ∪ ran 𝐹 ) ⊆ 𝑥
22 21 16 sstrid ⊢ ( ( 𝜑 ∧ 𝑥 ⊆ ℝ ∧ ( vol* ‘ 𝑥 ) ∈ ℝ ) → ( 𝑥 ∖ ∪ ran 𝐹 ) ⊆ ℝ )
23 ovolsscl ⊢ ( ( ( 𝑥 ∖ ∪ ran 𝐹 ) ⊆ 𝑥 ∧ 𝑥 ⊆ ℝ ∧ ( vol* ‘ 𝑥 ) ∈ ℝ ) → ( vol* ‘ ( 𝑥 ∖ ∪ ran 𝐹 ) ) ∈ ℝ )
24 21 23 mp3an1 ⊢ ( ( 𝑥 ⊆ ℝ ∧ ( vol* ‘ 𝑥 ) ∈ ℝ ) → ( vol* ‘ ( 𝑥 ∖ ∪ ran 𝐹 ) ) ∈ ℝ )
25 24 3adant1 ⊢ ( ( 𝜑 ∧ 𝑥 ⊆ ℝ ∧ ( vol* ‘ 𝑥 ) ∈ ℝ ) → ( vol* ‘ ( 𝑥 ∖ ∪ ran 𝐹 ) ) ∈ ℝ )
26 ovolun ⊢ ( ( ( ( 𝑥 ∩ ∪ ran 𝐹 ) ⊆ ℝ ∧ ( vol* ‘ ( 𝑥 ∩ ∪ ran 𝐹 ) ) ∈ ℝ ) ∧ ( ( 𝑥 ∖ ∪ ran 𝐹 ) ⊆ ℝ ∧ ( vol* ‘ ( 𝑥 ∖ ∪ ran 𝐹 ) ) ∈ ℝ ) ) → ( vol* ‘ ( ( 𝑥 ∩ ∪ ran 𝐹 ) ∪ ( 𝑥 ∖ ∪ ran 𝐹 ) ) ) ≤ ( ( vol* ‘ ( 𝑥 ∩ ∪ ran 𝐹 ) ) + ( vol* ‘ ( 𝑥 ∖ ∪ ran 𝐹 ) ) ) )
27 17 20 22 25 26 syl22anc ⊢ ( ( 𝜑 ∧ 𝑥 ⊆ ℝ ∧ ( vol* ‘ 𝑥 ) ∈ ℝ ) → ( vol* ‘ ( ( 𝑥 ∩ ∪ ran 𝐹 ) ∪ ( 𝑥 ∖ ∪ ran 𝐹 ) ) ) ≤ ( ( vol* ‘ ( 𝑥 ∩ ∪ ran 𝐹 ) ) + ( vol* ‘ ( 𝑥 ∖ ∪ ran 𝐹 ) ) ) )
28 14 27 eqbrtrrid ⊢ ( ( 𝜑 ∧ 𝑥 ⊆ ℝ ∧ ( vol* ‘ 𝑥 ) ∈ ℝ ) → ( vol* ‘ 𝑥 ) ≤ ( ( vol* ‘ ( 𝑥 ∩ ∪ ran 𝐹 ) ) + ( vol* ‘ ( 𝑥 ∖ ∪ ran 𝐹 ) ) ) )
29 20 rexrd ⊢ ( ( 𝜑 ∧ 𝑥 ⊆ ℝ ∧ ( vol* ‘ 𝑥 ) ∈ ℝ ) → ( vol* ‘ ( 𝑥 ∩ ∪ ran 𝐹 ) ) ∈ ℝ* )
30 nnuz ⊢ ℕ = ( ℤ≥ ‘ 1 )
31 1zzd ⊢ ( ( 𝜑 ∧ 𝑥 ⊆ ℝ ∧ ( vol* ‘ 𝑥 ) ∈ ℝ ) → 1 ∈ ℤ )
32 fveq2 ⊢ ( 𝑛 = 𝑘 → ( 𝐹 ‘ 𝑛 ) = ( 𝐹 ‘ 𝑘 ) )
33 32 ineq2d ⊢ ( 𝑛 = 𝑘 → ( 𝑥 ∩ ( 𝐹 ‘ 𝑛 ) ) = ( 𝑥 ∩ ( 𝐹 ‘ 𝑘 ) ) )
34 33 fveq2d ⊢ ( 𝑛 = 𝑘 → ( vol* ‘ ( 𝑥 ∩ ( 𝐹 ‘ 𝑛 ) ) ) = ( vol* ‘ ( 𝑥 ∩ ( 𝐹 ‘ 𝑘 ) ) ) )
35 fvex ⊢ ( vol* ‘ ( 𝑥 ∩ ( 𝐹 ‘ 𝑘 ) ) ) ∈ V
36 34 3 35 fvmpt ⊢ ( 𝑘 ∈ ℕ → ( 𝐻 ‘ 𝑘 ) = ( vol* ‘ ( 𝑥 ∩ ( 𝐹 ‘ 𝑘 ) ) ) )
37 36 adantl ⊢ ( ( ( 𝜑 ∧ 𝑥 ⊆ ℝ ∧ ( vol* ‘ 𝑥 ) ∈ ℝ ) ∧ 𝑘 ∈ ℕ ) → ( 𝐻 ‘ 𝑘 ) = ( vol* ‘ ( 𝑥 ∩ ( 𝐹 ‘ 𝑘 ) ) ) )
38 inss1 ⊢ ( 𝑥 ∩ ( 𝐹 ‘ 𝑘 ) ) ⊆ 𝑥
39 ovolsscl ⊢ ( ( ( 𝑥 ∩ ( 𝐹 ‘ 𝑘 ) ) ⊆ 𝑥 ∧ 𝑥 ⊆ ℝ ∧ ( vol* ‘ 𝑥 ) ∈ ℝ ) → ( vol* ‘ ( 𝑥 ∩ ( 𝐹 ‘ 𝑘 ) ) ) ∈ ℝ )
40 38 39 mp3an1 ⊢ ( ( 𝑥 ⊆ ℝ ∧ ( vol* ‘ 𝑥 ) ∈ ℝ ) → ( vol* ‘ ( 𝑥 ∩ ( 𝐹 ‘ 𝑘 ) ) ) ∈ ℝ )
41 40 3adant1 ⊢ ( ( 𝜑 ∧ 𝑥 ⊆ ℝ ∧ ( vol* ‘ 𝑥 ) ∈ ℝ ) → ( vol* ‘ ( 𝑥 ∩ ( 𝐹 ‘ 𝑘 ) ) ) ∈ ℝ )
42 41 adantr ⊢ ( ( ( 𝜑 ∧ 𝑥 ⊆ ℝ ∧ ( vol* ‘ 𝑥 ) ∈ ℝ ) ∧ 𝑘 ∈ ℕ ) → ( vol* ‘ ( 𝑥 ∩ ( 𝐹 ‘ 𝑘 ) ) ) ∈ ℝ )
43 37 42 eqeltrd ⊢ ( ( ( 𝜑 ∧ 𝑥 ⊆ ℝ ∧ ( vol* ‘ 𝑥 ) ∈ ℝ ) ∧ 𝑘 ∈ ℕ ) → ( 𝐻 ‘ 𝑘 ) ∈ ℝ )
44 30 31 43 serfre ⊢ ( ( 𝜑 ∧ 𝑥 ⊆ ℝ ∧ ( vol* ‘ 𝑥 ) ∈ ℝ ) → seq 1 ( + , 𝐻 ) : ℕ ⟶ ℝ )
45 44 frnd ⊢ ( ( 𝜑 ∧ 𝑥 ⊆ ℝ ∧ ( vol* ‘ 𝑥 ) ∈ ℝ ) → ran seq 1 ( + , 𝐻 ) ⊆ ℝ )
46 ressxr ⊢ ℝ ⊆ ℝ*
47 45 46 sstrdi ⊢ ( ( 𝜑 ∧ 𝑥 ⊆ ℝ ∧ ( vol* ‘ 𝑥 ) ∈ ℝ ) → ran seq 1 ( + , 𝐻 ) ⊆ ℝ* )
48 supxrcl ⊢ ( ran seq 1 ( + , 𝐻 ) ⊆ ℝ* → sup ( ran seq 1 ( + , 𝐻 ) , ℝ* , < ) ∈ ℝ* )
49 47 48 syl ⊢ ( ( 𝜑 ∧ 𝑥 ⊆ ℝ ∧ ( vol* ‘ 𝑥 ) ∈ ℝ ) → sup ( ran seq 1 ( + , 𝐻 ) , ℝ* , < ) ∈ ℝ* )
50 simp3 ⊢ ( ( 𝜑 ∧ 𝑥 ⊆ ℝ ∧ ( vol* ‘ 𝑥 ) ∈ ℝ ) → ( vol* ‘ 𝑥 ) ∈ ℝ )
51 50 25 resubcld ⊢ ( ( 𝜑 ∧ 𝑥 ⊆ ℝ ∧ ( vol* ‘ 𝑥 ) ∈ ℝ ) → ( ( vol* ‘ 𝑥 ) − ( vol* ‘ ( 𝑥 ∖ ∪ ran 𝐹 ) ) ) ∈ ℝ )
52 51 rexrd ⊢ ( ( 𝜑 ∧ 𝑥 ⊆ ℝ ∧ ( vol* ‘ 𝑥 ) ∈ ℝ ) → ( ( vol* ‘ 𝑥 ) − ( vol* ‘ ( 𝑥 ∖ ∪ ran 𝐹 ) ) ) ∈ ℝ* )
53 iunin2 ⊢ ∪ 𝑛 ∈ ℕ ( 𝑥 ∩ ( 𝐹 ‘ 𝑛 ) ) = ( 𝑥 ∩ ∪ 𝑛 ∈ ℕ ( 𝐹 ‘ 𝑛 ) )
54 ffn ⊢ ( 𝐹 : ℕ ⟶ dom vol → 𝐹 Fn ℕ )
55 fniunfv ⊢ ( 𝐹 Fn ℕ → ∪ 𝑛 ∈ ℕ ( 𝐹 ‘ 𝑛 ) = ∪ ran 𝐹 )
56 1 54 55 3syl ⊢ ( 𝜑 → ∪ 𝑛 ∈ ℕ ( 𝐹 ‘ 𝑛 ) = ∪ ran 𝐹 )
57 56 3ad2ant1 ⊢ ( ( 𝜑 ∧ 𝑥 ⊆ ℝ ∧ ( vol* ‘ 𝑥 ) ∈ ℝ ) → ∪ 𝑛 ∈ ℕ ( 𝐹 ‘ 𝑛 ) = ∪ ran 𝐹 )
58 57 ineq2d ⊢ ( ( 𝜑 ∧ 𝑥 ⊆ ℝ ∧ ( vol* ‘ 𝑥 ) ∈ ℝ ) → ( 𝑥 ∩ ∪ 𝑛 ∈ ℕ ( 𝐹 ‘ 𝑛 ) ) = ( 𝑥 ∩ ∪ ran 𝐹 ) )
59 53 58 syl5eq ⊢ ( ( 𝜑 ∧ 𝑥 ⊆ ℝ ∧ ( vol* ‘ 𝑥 ) ∈ ℝ ) → ∪ 𝑛 ∈ ℕ ( 𝑥 ∩ ( 𝐹 ‘ 𝑛 ) ) = ( 𝑥 ∩ ∪ ran 𝐹 ) )
60 59 fveq2d ⊢ ( ( 𝜑 ∧ 𝑥 ⊆ ℝ ∧ ( vol* ‘ 𝑥 ) ∈ ℝ ) → ( vol* ‘ ∪ 𝑛 ∈ ℕ ( 𝑥 ∩ ( 𝐹 ‘ 𝑛 ) ) ) = ( vol* ‘ ( 𝑥 ∩ ∪ ran 𝐹 ) ) )
61 eqid ⊢ seq 1 ( + , 𝐻 ) = seq 1 ( + , 𝐻 )
62 inss1 ⊢ ( 𝑥 ∩ ( 𝐹 ‘ 𝑛 ) ) ⊆ 𝑥
63 62 16 sstrid ⊢ ( ( 𝜑 ∧ 𝑥 ⊆ ℝ ∧ ( vol* ‘ 𝑥 ) ∈ ℝ ) → ( 𝑥 ∩ ( 𝐹 ‘ 𝑛 ) ) ⊆ ℝ )
64 63 adantr ⊢ ( ( ( 𝜑 ∧ 𝑥 ⊆ ℝ ∧ ( vol* ‘ 𝑥 ) ∈ ℝ ) ∧ 𝑛 ∈ ℕ ) → ( 𝑥 ∩ ( 𝐹 ‘ 𝑛 ) ) ⊆ ℝ )
65 ovolsscl ⊢ ( ( ( 𝑥 ∩ ( 𝐹 ‘ 𝑛 ) ) ⊆ 𝑥 ∧ 𝑥 ⊆ ℝ ∧ ( vol* ‘ 𝑥 ) ∈ ℝ ) → ( vol* ‘ ( 𝑥 ∩ ( 𝐹 ‘ 𝑛 ) ) ) ∈ ℝ )
66 62 65 mp3an1 ⊢ ( ( 𝑥 ⊆ ℝ ∧ ( vol* ‘ 𝑥 ) ∈ ℝ ) → ( vol* ‘ ( 𝑥 ∩ ( 𝐹 ‘ 𝑛 ) ) ) ∈ ℝ )
67 66 3adant1 ⊢ ( ( 𝜑 ∧ 𝑥 ⊆ ℝ ∧ ( vol* ‘ 𝑥 ) ∈ ℝ ) → ( vol* ‘ ( 𝑥 ∩ ( 𝐹 ‘ 𝑛 ) ) ) ∈ ℝ )
68 67 adantr ⊢ ( ( ( 𝜑 ∧ 𝑥 ⊆ ℝ ∧ ( vol* ‘ 𝑥 ) ∈ ℝ ) ∧ 𝑛 ∈ ℕ ) → ( vol* ‘ ( 𝑥 ∩ ( 𝐹 ‘ 𝑛 ) ) ) ∈ ℝ )
69 61 3 64 68 ovoliun ⊢ ( ( 𝜑 ∧ 𝑥 ⊆ ℝ ∧ ( vol* ‘ 𝑥 ) ∈ ℝ ) → ( vol* ‘ ∪ 𝑛 ∈ ℕ ( 𝑥 ∩ ( 𝐹 ‘ 𝑛 ) ) ) ≤ sup ( ran seq 1 ( + , 𝐻 ) , ℝ* , < ) )
70 60 69 eqbrtrrd ⊢ ( ( 𝜑 ∧ 𝑥 ⊆ ℝ ∧ ( vol* ‘ 𝑥 ) ∈ ℝ ) → ( vol* ‘ ( 𝑥 ∩ ∪ ran 𝐹 ) ) ≤ sup ( ran seq 1 ( + , 𝐻 ) , ℝ* , < ) )
71 1 3ad2ant1 ⊢ ( ( 𝜑 ∧ 𝑥 ⊆ ℝ ∧ ( vol* ‘ 𝑥 ) ∈ ℝ ) → 𝐹 : ℕ ⟶ dom vol )
72 2 3ad2ant1 ⊢ ( ( 𝜑 ∧ 𝑥 ⊆ ℝ ∧ ( vol* ‘ 𝑥 ) ∈ ℝ ) → Disj 𝑖 ∈ ℕ ( 𝐹 ‘ 𝑖 ) )
73 71 72 3 16 50 voliunlem1 ⊢ ( ( ( 𝜑 ∧ 𝑥 ⊆ ℝ ∧ ( vol* ‘ 𝑥 ) ∈ ℝ ) ∧ 𝑘 ∈ ℕ ) → ( ( seq 1 ( + , 𝐻 ) ‘ 𝑘 ) + ( vol* ‘ ( 𝑥 ∖ ∪ ran 𝐹 ) ) ) ≤ ( vol* ‘ 𝑥 ) )
74 44 ffvelrnda ⊢ ( ( ( 𝜑 ∧ 𝑥 ⊆ ℝ ∧ ( vol* ‘ 𝑥 ) ∈ ℝ ) ∧ 𝑘 ∈ ℕ ) → ( seq 1 ( + , 𝐻 ) ‘ 𝑘 ) ∈ ℝ )
75 25 adantr ⊢ ( ( ( 𝜑 ∧ 𝑥 ⊆ ℝ ∧ ( vol* ‘ 𝑥 ) ∈ ℝ ) ∧ 𝑘 ∈ ℕ ) → ( vol* ‘ ( 𝑥 ∖ ∪ ran 𝐹 ) ) ∈ ℝ )
76 simpl3 ⊢ ( ( ( 𝜑 ∧ 𝑥 ⊆ ℝ ∧ ( vol* ‘ 𝑥 ) ∈ ℝ ) ∧ 𝑘 ∈ ℕ ) → ( vol* ‘ 𝑥 ) ∈ ℝ )
77 leaddsub ⊢ ( ( ( seq 1 ( + , 𝐻 ) ‘ 𝑘 ) ∈ ℝ ∧ ( vol* ‘ ( 𝑥 ∖ ∪ ran 𝐹 ) ) ∈ ℝ ∧ ( vol* ‘ 𝑥 ) ∈ ℝ ) → ( ( ( seq 1 ( + , 𝐻 ) ‘ 𝑘 ) + ( vol* ‘ ( 𝑥 ∖ ∪ ran 𝐹 ) ) ) ≤ ( vol* ‘ 𝑥 ) ↔ ( seq 1 ( + , 𝐻 ) ‘ 𝑘 ) ≤ ( ( vol* ‘ 𝑥 ) − ( vol* ‘ ( 𝑥 ∖ ∪ ran 𝐹 ) ) ) ) )
78 74 75 76 77 syl3anc ⊢ ( ( ( 𝜑 ∧ 𝑥 ⊆ ℝ ∧ ( vol* ‘ 𝑥 ) ∈ ℝ ) ∧ 𝑘 ∈ ℕ ) → ( ( ( seq 1 ( + , 𝐻 ) ‘ 𝑘 ) + ( vol* ‘ ( 𝑥 ∖ ∪ ran 𝐹 ) ) ) ≤ ( vol* ‘ 𝑥 ) ↔ ( seq 1 ( + , 𝐻 ) ‘ 𝑘 ) ≤ ( ( vol* ‘ 𝑥 ) − ( vol* ‘ ( 𝑥 ∖ ∪ ran 𝐹 ) ) ) ) )
79 73 78 mpbid ⊢ ( ( ( 𝜑 ∧ 𝑥 ⊆ ℝ ∧ ( vol* ‘ 𝑥 ) ∈ ℝ ) ∧ 𝑘 ∈ ℕ ) → ( seq 1 ( + , 𝐻 ) ‘ 𝑘 ) ≤ ( ( vol* ‘ 𝑥 ) − ( vol* ‘ ( 𝑥 ∖ ∪ ran 𝐹 ) ) ) )
80 79 ralrimiva ⊢ ( ( 𝜑 ∧ 𝑥 ⊆ ℝ ∧ ( vol* ‘ 𝑥 ) ∈ ℝ ) → ∀ 𝑘 ∈ ℕ ( seq 1 ( + , 𝐻 ) ‘ 𝑘 ) ≤ ( ( vol* ‘ 𝑥 ) − ( vol* ‘ ( 𝑥 ∖ ∪ ran 𝐹 ) ) ) )
81 ffn ⊢ ( seq 1 ( + , 𝐻 ) : ℕ ⟶ ℝ → seq 1 ( + , 𝐻 ) Fn ℕ )
82 breq1 ⊢ ( 𝑧 = ( seq 1 ( + , 𝐻 ) ‘ 𝑘 ) → ( 𝑧 ≤ ( ( vol* ‘ 𝑥 ) − ( vol* ‘ ( 𝑥 ∖ ∪ ran 𝐹 ) ) ) ↔ ( seq 1 ( + , 𝐻 ) ‘ 𝑘 ) ≤ ( ( vol* ‘ 𝑥 ) − ( vol* ‘ ( 𝑥 ∖ ∪ ran 𝐹 ) ) ) ) )
83 82 ralrn ⊢ ( seq 1 ( + , 𝐻 ) Fn ℕ → ( ∀ 𝑧 ∈ ran seq 1 ( + , 𝐻 ) 𝑧 ≤ ( ( vol* ‘ 𝑥 ) − ( vol* ‘ ( 𝑥 ∖ ∪ ran 𝐹 ) ) ) ↔ ∀ 𝑘 ∈ ℕ ( seq 1 ( + , 𝐻 ) ‘ 𝑘 ) ≤ ( ( vol* ‘ 𝑥 ) − ( vol* ‘ ( 𝑥 ∖ ∪ ran 𝐹 ) ) ) ) )
84 44 81 83 3syl ⊢ ( ( 𝜑 ∧ 𝑥 ⊆ ℝ ∧ ( vol* ‘ 𝑥 ) ∈ ℝ ) → ( ∀ 𝑧 ∈ ran seq 1 ( + , 𝐻 ) 𝑧 ≤ ( ( vol* ‘ 𝑥 ) − ( vol* ‘ ( 𝑥 ∖ ∪ ran 𝐹 ) ) ) ↔ ∀ 𝑘 ∈ ℕ ( seq 1 ( + , 𝐻 ) ‘ 𝑘 ) ≤ ( ( vol* ‘ 𝑥 ) − ( vol* ‘ ( 𝑥 ∖ ∪ ran 𝐹 ) ) ) ) )
85 80 84 mpbird ⊢ ( ( 𝜑 ∧ 𝑥 ⊆ ℝ ∧ ( vol* ‘ 𝑥 ) ∈ ℝ ) → ∀ 𝑧 ∈ ran seq 1 ( + , 𝐻 ) 𝑧 ≤ ( ( vol* ‘ 𝑥 ) − ( vol* ‘ ( 𝑥 ∖ ∪ ran 𝐹 ) ) ) )
86 supxrleub ⊢ ( ( ran seq 1 ( + , 𝐻 ) ⊆ ℝ* ∧ ( ( vol* ‘ 𝑥 ) − ( vol* ‘ ( 𝑥 ∖ ∪ ran 𝐹 ) ) ) ∈ ℝ* ) → ( sup ( ran seq 1 ( + , 𝐻 ) , ℝ* , < ) ≤ ( ( vol* ‘ 𝑥 ) − ( vol* ‘ ( 𝑥 ∖ ∪ ran 𝐹 ) ) ) ↔ ∀ 𝑧 ∈ ran seq 1 ( + , 𝐻 ) 𝑧 ≤ ( ( vol* ‘ 𝑥 ) − ( vol* ‘ ( 𝑥 ∖ ∪ ran 𝐹 ) ) ) ) )
87 47 52 86 syl2anc ⊢ ( ( 𝜑 ∧ 𝑥 ⊆ ℝ ∧ ( vol* ‘ 𝑥 ) ∈ ℝ ) → ( sup ( ran seq 1 ( + , 𝐻 ) , ℝ* , < ) ≤ ( ( vol* ‘ 𝑥 ) − ( vol* ‘ ( 𝑥 ∖ ∪ ran 𝐹 ) ) ) ↔ ∀ 𝑧 ∈ ran seq 1 ( + , 𝐻 ) 𝑧 ≤ ( ( vol* ‘ 𝑥 ) − ( vol* ‘ ( 𝑥 ∖ ∪ ran 𝐹 ) ) ) ) )
88 85 87 mpbird ⊢ ( ( 𝜑 ∧ 𝑥 ⊆ ℝ ∧ ( vol* ‘ 𝑥 ) ∈ ℝ ) → sup ( ran seq 1 ( + , 𝐻 ) , ℝ* , < ) ≤ ( ( vol* ‘ 𝑥 ) − ( vol* ‘ ( 𝑥 ∖ ∪ ran 𝐹 ) ) ) )
89 29 49 52 70 88 xrletrd ⊢ ( ( 𝜑 ∧ 𝑥 ⊆ ℝ ∧ ( vol* ‘ 𝑥 ) ∈ ℝ ) → ( vol* ‘ ( 𝑥 ∩ ∪ ran 𝐹 ) ) ≤ ( ( vol* ‘ 𝑥 ) − ( vol* ‘ ( 𝑥 ∖ ∪ ran 𝐹 ) ) ) )
90 leaddsub ⊢ ( ( ( vol* ‘ ( 𝑥 ∩ ∪ ran 𝐹 ) ) ∈ ℝ ∧ ( vol* ‘ ( 𝑥 ∖ ∪ ran 𝐹 ) ) ∈ ℝ ∧ ( vol* ‘ 𝑥 ) ∈ ℝ ) → ( ( ( vol* ‘ ( 𝑥 ∩ ∪ ran 𝐹 ) ) + ( vol* ‘ ( 𝑥 ∖ ∪ ran 𝐹 ) ) ) ≤ ( vol* ‘ 𝑥 ) ↔ ( vol* ‘ ( 𝑥 ∩ ∪ ran 𝐹 ) ) ≤ ( ( vol* ‘ 𝑥 ) − ( vol* ‘ ( 𝑥 ∖ ∪ ran 𝐹 ) ) ) ) )
91 20 25 50 90 syl3anc ⊢ ( ( 𝜑 ∧ 𝑥 ⊆ ℝ ∧ ( vol* ‘ 𝑥 ) ∈ ℝ ) → ( ( ( vol* ‘ ( 𝑥 ∩ ∪ ran 𝐹 ) ) + ( vol* ‘ ( 𝑥 ∖ ∪ ran 𝐹 ) ) ) ≤ ( vol* ‘ 𝑥 ) ↔ ( vol* ‘ ( 𝑥 ∩ ∪ ran 𝐹 ) ) ≤ ( ( vol* ‘ 𝑥 ) − ( vol* ‘ ( 𝑥 ∖ ∪ ran 𝐹 ) ) ) ) )
92 89 91 mpbird ⊢ ( ( 𝜑 ∧ 𝑥 ⊆ ℝ ∧ ( vol* ‘ 𝑥 ) ∈ ℝ ) → ( ( vol* ‘ ( 𝑥 ∩ ∪ ran 𝐹 ) ) + ( vol* ‘ ( 𝑥 ∖ ∪ ran 𝐹 ) ) ) ≤ ( vol* ‘ 𝑥 ) )
93 20 25 readdcld ⊢ ( ( 𝜑 ∧ 𝑥 ⊆ ℝ ∧ ( vol* ‘ 𝑥 ) ∈ ℝ ) → ( ( vol* ‘ ( 𝑥 ∩ ∪ ran 𝐹 ) ) + ( vol* ‘ ( 𝑥 ∖ ∪ ran 𝐹 ) ) ) ∈ ℝ )
94 50 93 letri3d ⊢ ( ( 𝜑 ∧ 𝑥 ⊆ ℝ ∧ ( vol* ‘ 𝑥 ) ∈ ℝ ) → ( ( vol* ‘ 𝑥 ) = ( ( vol* ‘ ( 𝑥 ∩ ∪ ran 𝐹 ) ) + ( vol* ‘ ( 𝑥 ∖ ∪ ran 𝐹 ) ) ) ↔ ( ( vol* ‘ 𝑥 ) ≤ ( ( vol* ‘ ( 𝑥 ∩ ∪ ran 𝐹 ) ) + ( vol* ‘ ( 𝑥 ∖ ∪ ran 𝐹 ) ) ) ∧ ( ( vol* ‘ ( 𝑥 ∩ ∪ ran 𝐹 ) ) + ( vol* ‘ ( 𝑥 ∖ ∪ ran 𝐹 ) ) ) ≤ ( vol* ‘ 𝑥 ) ) ) )
95 28 92 94 mpbir2and ⊢ ( ( 𝜑 ∧ 𝑥 ⊆ ℝ ∧ ( vol* ‘ 𝑥 ) ∈ ℝ ) → ( vol* ‘ 𝑥 ) = ( ( vol* ‘ ( 𝑥 ∩ ∪ ran 𝐹 ) ) + ( vol* ‘ ( 𝑥 ∖ ∪ ran 𝐹 ) ) ) )
96 95 3expia ⊢ ( ( 𝜑 ∧ 𝑥 ⊆ ℝ ) → ( ( vol* ‘ 𝑥 ) ∈ ℝ → ( vol* ‘ 𝑥 ) = ( ( vol* ‘ ( 𝑥 ∩ ∪ ran 𝐹 ) ) + ( vol* ‘ ( 𝑥 ∖ ∪ ran 𝐹 ) ) ) ) )
97 12 96 sylan2 ⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝒫 ℝ ) → ( ( vol* ‘ 𝑥 ) ∈ ℝ → ( vol* ‘ 𝑥 ) = ( ( vol* ‘ ( 𝑥 ∩ ∪ ran 𝐹 ) ) + ( vol* ‘ ( 𝑥 ∖ ∪ ran 𝐹 ) ) ) ) )
98 97 ralrimiva ⊢ ( 𝜑 → ∀ 𝑥 ∈ 𝒫 ℝ ( ( vol* ‘ 𝑥 ) ∈ ℝ → ( vol* ‘ 𝑥 ) = ( ( vol* ‘ ( 𝑥 ∩ ∪ ran 𝐹 ) ) + ( vol* ‘ ( 𝑥 ∖ ∪ ran 𝐹 ) ) ) ) )
99 ismbl ⊢ ( ∪ ran 𝐹 ∈ dom vol ↔ ( ∪ ran 𝐹 ⊆ ℝ ∧ ∀ 𝑥 ∈ 𝒫 ℝ ( ( vol* ‘ 𝑥 ) ∈ ℝ → ( vol* ‘ 𝑥 ) = ( ( vol* ‘ ( 𝑥 ∩ ∪ ran 𝐹 ) ) + ( vol* ‘ ( 𝑥 ∖ ∪ ran 𝐹 ) ) ) ) ) )
100 11 98 99 sylanbrc ⊢ ( 𝜑 → ∪ ran 𝐹 ∈ dom vol )