Metamath Proof Explorer

Theorem voliunlem3

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

Ref Expression
Hypotheses voliunlem.3 ⊢ ( 𝜑 → 𝐹 : ℕ ⟶ dom vol )
voliunlem.5 ⊢ ( 𝜑 → Disj 𝑖 ∈ ℕ ( 𝐹 ‘ 𝑖 ) )
voliunlem.6 ⊢ 𝐻 = ( 𝑛 ∈ ℕ ↦ ( vol* ‘ ( 𝑥 ∩ ( 𝐹 ‘ 𝑛 ) ) ) )
voliunlem3.1 ⊢ 𝑆 = seq 1 ( + , 𝐺 )
voliunlem3.2 ⊢ 𝐺 = ( 𝑛 ∈ ℕ ↦ ( vol ‘ ( 𝐹 ‘ 𝑛 ) ) )
voliunlem3.4 ⊢ ( 𝜑 → ∀ 𝑖 ∈ ℕ ( vol ‘ ( 𝐹 ‘ 𝑖 ) ) ∈ ℝ )
Assertion voliunlem3 ( 𝜑 → ( vol ‘ ∪ ran 𝐹 ) = sup ( ran 𝑆 , ℝ* , < ) )

Proof

Step Hyp Ref Expression
1 voliunlem.3 ⊢ ( 𝜑 → 𝐹 : ℕ ⟶ dom vol )
2 voliunlem.5 ⊢ ( 𝜑 → Disj 𝑖 ∈ ℕ ( 𝐹 ‘ 𝑖 ) )
3 voliunlem.6 ⊢ 𝐻 = ( 𝑛 ∈ ℕ ↦ ( vol* ‘ ( 𝑥 ∩ ( 𝐹 ‘ 𝑛 ) ) ) )
4 voliunlem3.1 ⊢ 𝑆 = seq 1 ( + , 𝐺 )
5 voliunlem3.2 ⊢ 𝐺 = ( 𝑛 ∈ ℕ ↦ ( vol ‘ ( 𝐹 ‘ 𝑛 ) ) )
6 voliunlem3.4 ⊢ ( 𝜑 → ∀ 𝑖 ∈ ℕ ( vol ‘ ( 𝐹 ‘ 𝑖 ) ) ∈ ℝ )
7 1 2 3 voliunlem2 ⊢ ( 𝜑 → ∪ ran 𝐹 ∈ dom vol )
8 mblvol ⊢ ( ∪ ran 𝐹 ∈ dom vol → ( vol ‘ ∪ ran 𝐹 ) = ( vol* ‘ ∪ ran 𝐹 ) )
9 7 8 syl ⊢ ( 𝜑 → ( vol ‘ ∪ ran 𝐹 ) = ( vol* ‘ ∪ ran 𝐹 ) )
10 1 frnd ⊢ ( 𝜑 → ran 𝐹 ⊆ dom vol )
11 mblss ⊢ ( 𝑥 ∈ dom vol → 𝑥 ⊆ ℝ )
12 reex ⊢ ℝ ∈ V
13 12 elpw2 ⊢ ( 𝑥 ∈ 𝒫 ℝ ↔ 𝑥 ⊆ ℝ )
14 11 13 sylibr ⊢ ( 𝑥 ∈ dom vol → 𝑥 ∈ 𝒫 ℝ )
15 14 ssriv ⊢ dom vol ⊆ 𝒫 ℝ
16 10 15 sstrdi ⊢ ( 𝜑 → ran 𝐹 ⊆ 𝒫 ℝ )
17 sspwuni ⊢ ( ran 𝐹 ⊆ 𝒫 ℝ ↔ ∪ ran 𝐹 ⊆ ℝ )
18 16 17 sylib ⊢ ( 𝜑 → ∪ ran 𝐹 ⊆ ℝ )
19 ovolcl ⊢ ( ∪ ran 𝐹 ⊆ ℝ → ( vol* ‘ ∪ ran 𝐹 ) ∈ ℝ* )
20 18 19 syl ⊢ ( 𝜑 → ( vol* ‘ ∪ ran 𝐹 ) ∈ ℝ* )
21 nnuz ⊢ ℕ = ( ℤ≥ ‘ 1 )
22 1zzd ⊢ ( 𝜑 → 1 ∈ ℤ )
23 2fveq3 ⊢ ( 𝑛 = 𝑘 → ( vol ‘ ( 𝐹 ‘ 𝑛 ) ) = ( vol ‘ ( 𝐹 ‘ 𝑘 ) ) )
24 fvex ⊢ ( vol ‘ ( 𝐹 ‘ 𝑘 ) ) ∈ V
25 23 5 24 fvmpt ⊢ ( 𝑘 ∈ ℕ → ( 𝐺 ‘ 𝑘 ) = ( vol ‘ ( 𝐹 ‘ 𝑘 ) ) )
26 25 adantl ⊢ ( ( 𝜑 ∧ 𝑘 ∈ ℕ ) → ( 𝐺 ‘ 𝑘 ) = ( vol ‘ ( 𝐹 ‘ 𝑘 ) ) )
27 2fveq3 ⊢ ( 𝑖 = 𝑘 → ( vol ‘ ( 𝐹 ‘ 𝑖 ) ) = ( vol ‘ ( 𝐹 ‘ 𝑘 ) ) )
28 27 eleq1d ⊢ ( 𝑖 = 𝑘 → ( ( vol ‘ ( 𝐹 ‘ 𝑖 ) ) ∈ ℝ ↔ ( vol ‘ ( 𝐹 ‘ 𝑘 ) ) ∈ ℝ ) )
29 28 rspccva ⊢ ( ( ∀ 𝑖 ∈ ℕ ( vol ‘ ( 𝐹 ‘ 𝑖 ) ) ∈ ℝ ∧ 𝑘 ∈ ℕ ) → ( vol ‘ ( 𝐹 ‘ 𝑘 ) ) ∈ ℝ )
30 6 29 sylan ⊢ ( ( 𝜑 ∧ 𝑘 ∈ ℕ ) → ( vol ‘ ( 𝐹 ‘ 𝑘 ) ) ∈ ℝ )
31 26 30 eqeltrd ⊢ ( ( 𝜑 ∧ 𝑘 ∈ ℕ ) → ( 𝐺 ‘ 𝑘 ) ∈ ℝ )
32 21 22 31 serfre ⊢ ( 𝜑 → seq 1 ( + , 𝐺 ) : ℕ ⟶ ℝ )
33 4 feq1i ⊢ ( 𝑆 : ℕ ⟶ ℝ ↔ seq 1 ( + , 𝐺 ) : ℕ ⟶ ℝ )
34 32 33 sylibr ⊢ ( 𝜑 → 𝑆 : ℕ ⟶ ℝ )
35 34 frnd ⊢ ( 𝜑 → ran 𝑆 ⊆ ℝ )
36 ressxr ⊢ ℝ ⊆ ℝ*
37 35 36 sstrdi ⊢ ( 𝜑 → ran 𝑆 ⊆ ℝ* )
38 supxrcl ⊢ ( ran 𝑆 ⊆ ℝ* → sup ( ran 𝑆 , ℝ* , < ) ∈ ℝ* )
39 37 38 syl ⊢ ( 𝜑 → sup ( ran 𝑆 , ℝ* , < ) ∈ ℝ* )
40 eqid ⊢ seq 1 ( + , ( 𝑛 ∈ ℕ ↦ ( vol* ‘ ( 𝐹 ‘ 𝑛 ) ) ) ) = seq 1 ( + , ( 𝑛 ∈ ℕ ↦ ( vol* ‘ ( 𝐹 ‘ 𝑛 ) ) ) )
41 eqid ⊢ ( 𝑛 ∈ ℕ ↦ ( vol* ‘ ( 𝐹 ‘ 𝑛 ) ) ) = ( 𝑛 ∈ ℕ ↦ ( vol* ‘ ( 𝐹 ‘ 𝑛 ) ) )
42 1 ffvelcdmda ⊢ ( ( 𝜑 ∧ 𝑛 ∈ ℕ ) → ( 𝐹 ‘ 𝑛 ) ∈ dom vol )
43 mblss ⊢ ( ( 𝐹 ‘ 𝑛 ) ∈ dom vol → ( 𝐹 ‘ 𝑛 ) ⊆ ℝ )
44 42 43 syl ⊢ ( ( 𝜑 ∧ 𝑛 ∈ ℕ ) → ( 𝐹 ‘ 𝑛 ) ⊆ ℝ )
45 mblvol ⊢ ( ( 𝐹 ‘ 𝑛 ) ∈ dom vol → ( vol ‘ ( 𝐹 ‘ 𝑛 ) ) = ( vol* ‘ ( 𝐹 ‘ 𝑛 ) ) )
46 42 45 syl ⊢ ( ( 𝜑 ∧ 𝑛 ∈ ℕ ) → ( vol ‘ ( 𝐹 ‘ 𝑛 ) ) = ( vol* ‘ ( 𝐹 ‘ 𝑛 ) ) )
47 2fveq3 ⊢ ( 𝑖 = 𝑛 → ( vol ‘ ( 𝐹 ‘ 𝑖 ) ) = ( vol ‘ ( 𝐹 ‘ 𝑛 ) ) )
48 47 eleq1d ⊢ ( 𝑖 = 𝑛 → ( ( vol ‘ ( 𝐹 ‘ 𝑖 ) ) ∈ ℝ ↔ ( vol ‘ ( 𝐹 ‘ 𝑛 ) ) ∈ ℝ ) )
49 48 rspccva ⊢ ( ( ∀ 𝑖 ∈ ℕ ( vol ‘ ( 𝐹 ‘ 𝑖 ) ) ∈ ℝ ∧ 𝑛 ∈ ℕ ) → ( vol ‘ ( 𝐹 ‘ 𝑛 ) ) ∈ ℝ )
50 6 49 sylan ⊢ ( ( 𝜑 ∧ 𝑛 ∈ ℕ ) → ( vol ‘ ( 𝐹 ‘ 𝑛 ) ) ∈ ℝ )
51 46 50 eqeltrrd ⊢ ( ( 𝜑 ∧ 𝑛 ∈ ℕ ) → ( vol* ‘ ( 𝐹 ‘ 𝑛 ) ) ∈ ℝ )
52 40 41 44 51 ovoliun ⊢ ( 𝜑 → ( vol* ‘ ∪ 𝑛 ∈ ℕ ( 𝐹 ‘ 𝑛 ) ) ≤ sup ( ran seq 1 ( + , ( 𝑛 ∈ ℕ ↦ ( vol* ‘ ( 𝐹 ‘ 𝑛 ) ) ) ) , ℝ* , < ) )
53 1 ffnd ⊢ ( 𝜑 → 𝐹 Fn ℕ )
54 fniunfv ⊢ ( 𝐹 Fn ℕ → ∪ 𝑛 ∈ ℕ ( 𝐹 ‘ 𝑛 ) = ∪ ran 𝐹 )
55 53 54 syl ⊢ ( 𝜑 → ∪ 𝑛 ∈ ℕ ( 𝐹 ‘ 𝑛 ) = ∪ ran 𝐹 )
56 55 fveq2d ⊢ ( 𝜑 → ( vol* ‘ ∪ 𝑛 ∈ ℕ ( 𝐹 ‘ 𝑛 ) ) = ( vol* ‘ ∪ ran 𝐹 ) )
57 46 mpteq2dva ⊢ ( 𝜑 → ( 𝑛 ∈ ℕ ↦ ( vol ‘ ( 𝐹 ‘ 𝑛 ) ) ) = ( 𝑛 ∈ ℕ ↦ ( vol* ‘ ( 𝐹 ‘ 𝑛 ) ) ) )
58 5 57 eqtrid ⊢ ( 𝜑 → 𝐺 = ( 𝑛 ∈ ℕ ↦ ( vol* ‘ ( 𝐹 ‘ 𝑛 ) ) ) )
59 58 seqeq3d ⊢ ( 𝜑 → seq 1 ( + , 𝐺 ) = seq 1 ( + , ( 𝑛 ∈ ℕ ↦ ( vol* ‘ ( 𝐹 ‘ 𝑛 ) ) ) ) )
60 4 59 eqtr2id ⊢ ( 𝜑 → seq 1 ( + , ( 𝑛 ∈ ℕ ↦ ( vol* ‘ ( 𝐹 ‘ 𝑛 ) ) ) ) = 𝑆 )
61 60 rneqd ⊢ ( 𝜑 → ran seq 1 ( + , ( 𝑛 ∈ ℕ ↦ ( vol* ‘ ( 𝐹 ‘ 𝑛 ) ) ) ) = ran 𝑆 )
62 61 supeq1d ⊢ ( 𝜑 → sup ( ran seq 1 ( + , ( 𝑛 ∈ ℕ ↦ ( vol* ‘ ( 𝐹 ‘ 𝑛 ) ) ) ) , ℝ* , < ) = sup ( ran 𝑆 , ℝ* , < ) )
63 52 56 62 3brtr3d ⊢ ( 𝜑 → ( vol* ‘ ∪ ran 𝐹 ) ≤ sup ( ran 𝑆 , ℝ* , < ) )
64 ovolge0 ⊢ ( ∪ ran 𝐹 ⊆ ℝ → 0 ≤ ( vol* ‘ ∪ ran 𝐹 ) )
65 18 64 syl ⊢ ( 𝜑 → 0 ≤ ( vol* ‘ ∪ ran 𝐹 ) )
66 mnflt0 ⊢ -∞ < 0
67 mnfxr ⊢ -∞ ∈ ℝ*
68 0xr ⊢ 0 ∈ ℝ*
69 xrltletr ⊢ ( ( -∞ ∈ ℝ* ∧ 0 ∈ ℝ* ∧ ( vol* ‘ ∪ ran 𝐹 ) ∈ ℝ* ) → ( ( -∞ < 0 ∧ 0 ≤ ( vol* ‘ ∪ ran 𝐹 ) ) → -∞ < ( vol* ‘ ∪ ran 𝐹 ) ) )
70 67 68 69 mp3an12 ⊢ ( ( vol* ‘ ∪ ran 𝐹 ) ∈ ℝ* → ( ( -∞ < 0 ∧ 0 ≤ ( vol* ‘ ∪ ran 𝐹 ) ) → -∞ < ( vol* ‘ ∪ ran 𝐹 ) ) )
71 66 70 mpani ⊢ ( ( vol* ‘ ∪ ran 𝐹 ) ∈ ℝ* → ( 0 ≤ ( vol* ‘ ∪ ran 𝐹 ) → -∞ < ( vol* ‘ ∪ ran 𝐹 ) ) )
72 20 65 71 sylc ⊢ ( 𝜑 → -∞ < ( vol* ‘ ∪ ran 𝐹 ) )
73 xrrebnd ⊢ ( ( vol* ‘ ∪ ran 𝐹 ) ∈ ℝ* → ( ( vol* ‘ ∪ ran 𝐹 ) ∈ ℝ ↔ ( -∞ < ( vol* ‘ ∪ ran 𝐹 ) ∧ ( vol* ‘ ∪ ran 𝐹 ) < +∞ ) ) )
74 20 73 syl ⊢ ( 𝜑 → ( ( vol* ‘ ∪ ran 𝐹 ) ∈ ℝ ↔ ( -∞ < ( vol* ‘ ∪ ran 𝐹 ) ∧ ( vol* ‘ ∪ ran 𝐹 ) < +∞ ) ) )
75 12 elpw2 ⊢ ( ∪ ran 𝐹 ∈ 𝒫 ℝ ↔ ∪ ran 𝐹 ⊆ ℝ )
76 18 75 sylibr ⊢ ( 𝜑 → ∪ ran 𝐹 ∈ 𝒫 ℝ )
77 simpl ⊢ ( ( 𝑥 = ∪ ran 𝐹 ∧ 𝜑 ) → 𝑥 = ∪ ran 𝐹 )
78 77 sseq1d ⊢ ( ( 𝑥 = ∪ ran 𝐹 ∧ 𝜑 ) → ( 𝑥 ⊆ ℝ ↔ ∪ ran 𝐹 ⊆ ℝ ) )
79 77 fveq2d ⊢ ( ( 𝑥 = ∪ ran 𝐹 ∧ 𝜑 ) → ( vol* ‘ 𝑥 ) = ( vol* ‘ ∪ ran 𝐹 ) )
80 79 eleq1d ⊢ ( ( 𝑥 = ∪ ran 𝐹 ∧ 𝜑 ) → ( ( vol* ‘ 𝑥 ) ∈ ℝ ↔ ( vol* ‘ ∪ ran 𝐹 ) ∈ ℝ ) )
81 simpll ⊢ ( ( ( 𝑥 = ∪ ran 𝐹 ∧ 𝜑 ) ∧ 𝑛 ∈ ℕ ) → 𝑥 = ∪ ran 𝐹 )
82 81 ineq1d ⊢ ( ( ( 𝑥 = ∪ ran 𝐹 ∧ 𝜑 ) ∧ 𝑛 ∈ ℕ ) → ( 𝑥 ∩ ( 𝐹 ‘ 𝑛 ) ) = ( ∪ ran 𝐹 ∩ ( 𝐹 ‘ 𝑛 ) ) )
83 fnfvelrn ⊢ ( ( 𝐹 Fn ℕ ∧ 𝑛 ∈ ℕ ) → ( 𝐹 ‘ 𝑛 ) ∈ ran 𝐹 )
84 53 83 sylan ⊢ ( ( 𝜑 ∧ 𝑛 ∈ ℕ ) → ( 𝐹 ‘ 𝑛 ) ∈ ran 𝐹 )
85 elssuni ⊢ ( ( 𝐹 ‘ 𝑛 ) ∈ ran 𝐹 → ( 𝐹 ‘ 𝑛 ) ⊆ ∪ ran 𝐹 )
86 84 85 syl ⊢ ( ( 𝜑 ∧ 𝑛 ∈ ℕ ) → ( 𝐹 ‘ 𝑛 ) ⊆ ∪ ran 𝐹 )
87 86 adantll ⊢ ( ( ( 𝑥 = ∪ ran 𝐹 ∧ 𝜑 ) ∧ 𝑛 ∈ ℕ ) → ( 𝐹 ‘ 𝑛 ) ⊆ ∪ ran 𝐹 )
88 sseqin2 ⊢ ( ( 𝐹 ‘ 𝑛 ) ⊆ ∪ ran 𝐹 ↔ ( ∪ ran 𝐹 ∩ ( 𝐹 ‘ 𝑛 ) ) = ( 𝐹 ‘ 𝑛 ) )
89 87 88 sylib ⊢ ( ( ( 𝑥 = ∪ ran 𝐹 ∧ 𝜑 ) ∧ 𝑛 ∈ ℕ ) → ( ∪ ran 𝐹 ∩ ( 𝐹 ‘ 𝑛 ) ) = ( 𝐹 ‘ 𝑛 ) )
90 82 89 eqtrd ⊢ ( ( ( 𝑥 = ∪ ran 𝐹 ∧ 𝜑 ) ∧ 𝑛 ∈ ℕ ) → ( 𝑥 ∩ ( 𝐹 ‘ 𝑛 ) ) = ( 𝐹 ‘ 𝑛 ) )
91 90 fveq2d ⊢ ( ( ( 𝑥 = ∪ ran 𝐹 ∧ 𝜑 ) ∧ 𝑛 ∈ ℕ ) → ( vol* ‘ ( 𝑥 ∩ ( 𝐹 ‘ 𝑛 ) ) ) = ( vol* ‘ ( 𝐹 ‘ 𝑛 ) ) )
92 46 adantll ⊢ ( ( ( 𝑥 = ∪ ran 𝐹 ∧ 𝜑 ) ∧ 𝑛 ∈ ℕ ) → ( vol ‘ ( 𝐹 ‘ 𝑛 ) ) = ( vol* ‘ ( 𝐹 ‘ 𝑛 ) ) )
93 91 92 eqtr4d ⊢ ( ( ( 𝑥 = ∪ ran 𝐹 ∧ 𝜑 ) ∧ 𝑛 ∈ ℕ ) → ( vol* ‘ ( 𝑥 ∩ ( 𝐹 ‘ 𝑛 ) ) ) = ( vol ‘ ( 𝐹 ‘ 𝑛 ) ) )
94 93 mpteq2dva ⊢ ( ( 𝑥 = ∪ ran 𝐹 ∧ 𝜑 ) → ( 𝑛 ∈ ℕ ↦ ( vol* ‘ ( 𝑥 ∩ ( 𝐹 ‘ 𝑛 ) ) ) ) = ( 𝑛 ∈ ℕ ↦ ( vol ‘ ( 𝐹 ‘ 𝑛 ) ) ) )
95 94 adantrr ⊢ ( ( 𝑥 = ∪ ran 𝐹 ∧ ( 𝜑 ∧ 𝑘 ∈ ℕ ) ) → ( 𝑛 ∈ ℕ ↦ ( vol* ‘ ( 𝑥 ∩ ( 𝐹 ‘ 𝑛 ) ) ) ) = ( 𝑛 ∈ ℕ ↦ ( vol ‘ ( 𝐹 ‘ 𝑛 ) ) ) )
96 95 3 5 3eqtr4g ⊢ ( ( 𝑥 = ∪ ran 𝐹 ∧ ( 𝜑 ∧ 𝑘 ∈ ℕ ) ) → 𝐻 = 𝐺 )
97 96 seqeq3d ⊢ ( ( 𝑥 = ∪ ran 𝐹 ∧ ( 𝜑 ∧ 𝑘 ∈ ℕ ) ) → seq 1 ( + , 𝐻 ) = seq 1 ( + , 𝐺 ) )
98 97 4 eqtr4di ⊢ ( ( 𝑥 = ∪ ran 𝐹 ∧ ( 𝜑 ∧ 𝑘 ∈ ℕ ) ) → seq 1 ( + , 𝐻 ) = 𝑆 )
99 98 fveq1d ⊢ ( ( 𝑥 = ∪ ran 𝐹 ∧ ( 𝜑 ∧ 𝑘 ∈ ℕ ) ) → ( seq 1 ( + , 𝐻 ) ‘ 𝑘 ) = ( 𝑆 ‘ 𝑘 ) )
100 difeq1 ⊢ ( 𝑥 = ∪ ran 𝐹 → ( 𝑥 ∖ ∪ ran 𝐹 ) = ( ∪ ran 𝐹 ∖ ∪ ran 𝐹 ) )
101 difid ⊢ ( ∪ ran 𝐹 ∖ ∪ ran 𝐹 ) = ∅
102 100 101 eqtrdi ⊢ ( 𝑥 = ∪ ran 𝐹 → ( 𝑥 ∖ ∪ ran 𝐹 ) = ∅ )
103 102 fveq2d ⊢ ( 𝑥 = ∪ ran 𝐹 → ( vol* ‘ ( 𝑥 ∖ ∪ ran 𝐹 ) ) = ( vol* ‘ ∅ ) )
104 ovol0 ⊢ ( vol* ‘ ∅ ) = 0
105 103 104 eqtrdi ⊢ ( 𝑥 = ∪ ran 𝐹 → ( vol* ‘ ( 𝑥 ∖ ∪ ran 𝐹 ) ) = 0 )
106 105 adantr ⊢ ( ( 𝑥 = ∪ ran 𝐹 ∧ ( 𝜑 ∧ 𝑘 ∈ ℕ ) ) → ( vol* ‘ ( 𝑥 ∖ ∪ ran 𝐹 ) ) = 0 )
107 99 106 oveq12d ⊢ ( ( 𝑥 = ∪ ran 𝐹 ∧ ( 𝜑 ∧ 𝑘 ∈ ℕ ) ) → ( ( seq 1 ( + , 𝐻 ) ‘ 𝑘 ) + ( vol* ‘ ( 𝑥 ∖ ∪ ran 𝐹 ) ) ) = ( ( 𝑆 ‘ 𝑘 ) + 0 ) )
108 34 ffvelcdmda ⊢ ( ( 𝜑 ∧ 𝑘 ∈ ℕ ) → ( 𝑆 ‘ 𝑘 ) ∈ ℝ )
109 108 adantl ⊢ ( ( 𝑥 = ∪ ran 𝐹 ∧ ( 𝜑 ∧ 𝑘 ∈ ℕ ) ) → ( 𝑆 ‘ 𝑘 ) ∈ ℝ )
110 109 recnd ⊢ ( ( 𝑥 = ∪ ran 𝐹 ∧ ( 𝜑 ∧ 𝑘 ∈ ℕ ) ) → ( 𝑆 ‘ 𝑘 ) ∈ ℂ )
111 110 addridd ⊢ ( ( 𝑥 = ∪ ran 𝐹 ∧ ( 𝜑 ∧ 𝑘 ∈ ℕ ) ) → ( ( 𝑆 ‘ 𝑘 ) + 0 ) = ( 𝑆 ‘ 𝑘 ) )
112 107 111 eqtrd ⊢ ( ( 𝑥 = ∪ ran 𝐹 ∧ ( 𝜑 ∧ 𝑘 ∈ ℕ ) ) → ( ( seq 1 ( + , 𝐻 ) ‘ 𝑘 ) + ( vol* ‘ ( 𝑥 ∖ ∪ ran 𝐹 ) ) ) = ( 𝑆 ‘ 𝑘 ) )
113 fveq2 ⊢ ( 𝑥 = ∪ ran 𝐹 → ( vol* ‘ 𝑥 ) = ( vol* ‘ ∪ ran 𝐹 ) )
114 113 adantr ⊢ ( ( 𝑥 = ∪ ran 𝐹 ∧ ( 𝜑 ∧ 𝑘 ∈ ℕ ) ) → ( vol* ‘ 𝑥 ) = ( vol* ‘ ∪ ran 𝐹 ) )
115 112 114 breq12d ⊢ ( ( 𝑥 = ∪ ran 𝐹 ∧ ( 𝜑 ∧ 𝑘 ∈ ℕ ) ) → ( ( ( seq 1 ( + , 𝐻 ) ‘ 𝑘 ) + ( vol* ‘ ( 𝑥 ∖ ∪ ran 𝐹 ) ) ) ≤ ( vol* ‘ 𝑥 ) ↔ ( 𝑆 ‘ 𝑘 ) ≤ ( vol* ‘ ∪ ran 𝐹 ) ) )
116 115 expr ⊢ ( ( 𝑥 = ∪ ran 𝐹 ∧ 𝜑 ) → ( 𝑘 ∈ ℕ → ( ( ( seq 1 ( + , 𝐻 ) ‘ 𝑘 ) + ( vol* ‘ ( 𝑥 ∖ ∪ ran 𝐹 ) ) ) ≤ ( vol* ‘ 𝑥 ) ↔ ( 𝑆 ‘ 𝑘 ) ≤ ( vol* ‘ ∪ ran 𝐹 ) ) ) )
117 116 pm5.74d ⊢ ( ( 𝑥 = ∪ ran 𝐹 ∧ 𝜑 ) → ( ( 𝑘 ∈ ℕ → ( ( seq 1 ( + , 𝐻 ) ‘ 𝑘 ) + ( vol* ‘ ( 𝑥 ∖ ∪ ran 𝐹 ) ) ) ≤ ( vol* ‘ 𝑥 ) ) ↔ ( 𝑘 ∈ ℕ → ( 𝑆 ‘ 𝑘 ) ≤ ( vol* ‘ ∪ ran 𝐹 ) ) ) )
118 80 117 imbi12d ⊢ ( ( 𝑥 = ∪ ran 𝐹 ∧ 𝜑 ) → ( ( ( vol* ‘ 𝑥 ) ∈ ℝ → ( 𝑘 ∈ ℕ → ( ( seq 1 ( + , 𝐻 ) ‘ 𝑘 ) + ( vol* ‘ ( 𝑥 ∖ ∪ ran 𝐹 ) ) ) ≤ ( vol* ‘ 𝑥 ) ) ) ↔ ( ( vol* ‘ ∪ ran 𝐹 ) ∈ ℝ → ( 𝑘 ∈ ℕ → ( 𝑆 ‘ 𝑘 ) ≤ ( vol* ‘ ∪ ran 𝐹 ) ) ) ) )
119 78 118 imbi12d ⊢ ( ( 𝑥 = ∪ ran 𝐹 ∧ 𝜑 ) → ( ( 𝑥 ⊆ ℝ → ( ( vol* ‘ 𝑥 ) ∈ ℝ → ( 𝑘 ∈ ℕ → ( ( seq 1 ( + , 𝐻 ) ‘ 𝑘 ) + ( vol* ‘ ( 𝑥 ∖ ∪ ran 𝐹 ) ) ) ≤ ( vol* ‘ 𝑥 ) ) ) ) ↔ ( ∪ ran 𝐹 ⊆ ℝ → ( ( vol* ‘ ∪ ran 𝐹 ) ∈ ℝ → ( 𝑘 ∈ ℕ → ( 𝑆 ‘ 𝑘 ) ≤ ( vol* ‘ ∪ ran 𝐹 ) ) ) ) ) )
120 119 pm5.74da ⊢ ( 𝑥 = ∪ ran 𝐹 → ( ( 𝜑 → ( 𝑥 ⊆ ℝ → ( ( vol* ‘ 𝑥 ) ∈ ℝ → ( 𝑘 ∈ ℕ → ( ( seq 1 ( + , 𝐻 ) ‘ 𝑘 ) + ( vol* ‘ ( 𝑥 ∖ ∪ ran 𝐹 ) ) ) ≤ ( vol* ‘ 𝑥 ) ) ) ) ) ↔ ( 𝜑 → ( ∪ ran 𝐹 ⊆ ℝ → ( ( vol* ‘ ∪ ran 𝐹 ) ∈ ℝ → ( 𝑘 ∈ ℕ → ( 𝑆 ‘ 𝑘 ) ≤ ( vol* ‘ ∪ ran 𝐹 ) ) ) ) ) ) )
121 1 3ad2ant1 ⊢ ( ( 𝜑 ∧ 𝑥 ⊆ ℝ ∧ ( vol* ‘ 𝑥 ) ∈ ℝ ) → 𝐹 : ℕ ⟶ dom vol )
122 2 3ad2ant1 ⊢ ( ( 𝜑 ∧ 𝑥 ⊆ ℝ ∧ ( vol* ‘ 𝑥 ) ∈ ℝ ) → Disj 𝑖 ∈ ℕ ( 𝐹 ‘ 𝑖 ) )
123 simp2 ⊢ ( ( 𝜑 ∧ 𝑥 ⊆ ℝ ∧ ( vol* ‘ 𝑥 ) ∈ ℝ ) → 𝑥 ⊆ ℝ )
124 simp3 ⊢ ( ( 𝜑 ∧ 𝑥 ⊆ ℝ ∧ ( vol* ‘ 𝑥 ) ∈ ℝ ) → ( vol* ‘ 𝑥 ) ∈ ℝ )
125 121 122 3 123 124 voliunlem1 ⊢ ( ( ( 𝜑 ∧ 𝑥 ⊆ ℝ ∧ ( vol* ‘ 𝑥 ) ∈ ℝ ) ∧ 𝑘 ∈ ℕ ) → ( ( seq 1 ( + , 𝐻 ) ‘ 𝑘 ) + ( vol* ‘ ( 𝑥 ∖ ∪ ran 𝐹 ) ) ) ≤ ( vol* ‘ 𝑥 ) )
126 125 3exp1 ⊢ ( 𝜑 → ( 𝑥 ⊆ ℝ → ( ( vol* ‘ 𝑥 ) ∈ ℝ → ( 𝑘 ∈ ℕ → ( ( seq 1 ( + , 𝐻 ) ‘ 𝑘 ) + ( vol* ‘ ( 𝑥 ∖ ∪ ran 𝐹 ) ) ) ≤ ( vol* ‘ 𝑥 ) ) ) ) )
127 120 126 vtoclg ⊢ ( ∪ ran 𝐹 ∈ 𝒫 ℝ → ( 𝜑 → ( ∪ ran 𝐹 ⊆ ℝ → ( ( vol* ‘ ∪ ran 𝐹 ) ∈ ℝ → ( 𝑘 ∈ ℕ → ( 𝑆 ‘ 𝑘 ) ≤ ( vol* ‘ ∪ ran 𝐹 ) ) ) ) ) )
128 76 127 mpcom ⊢ ( 𝜑 → ( ∪ ran 𝐹 ⊆ ℝ → ( ( vol* ‘ ∪ ran 𝐹 ) ∈ ℝ → ( 𝑘 ∈ ℕ → ( 𝑆 ‘ 𝑘 ) ≤ ( vol* ‘ ∪ ran 𝐹 ) ) ) ) )
129 18 128 mpd ⊢ ( 𝜑 → ( ( vol* ‘ ∪ ran 𝐹 ) ∈ ℝ → ( 𝑘 ∈ ℕ → ( 𝑆 ‘ 𝑘 ) ≤ ( vol* ‘ ∪ ran 𝐹 ) ) ) )
130 74 129 sylbird ⊢ ( 𝜑 → ( ( -∞ < ( vol* ‘ ∪ ran 𝐹 ) ∧ ( vol* ‘ ∪ ran 𝐹 ) < +∞ ) → ( 𝑘 ∈ ℕ → ( 𝑆 ‘ 𝑘 ) ≤ ( vol* ‘ ∪ ran 𝐹 ) ) ) )
131 72 130 mpand ⊢ ( 𝜑 → ( ( vol* ‘ ∪ ran 𝐹 ) < +∞ → ( 𝑘 ∈ ℕ → ( 𝑆 ‘ 𝑘 ) ≤ ( vol* ‘ ∪ ran 𝐹 ) ) ) )
132 nltpnft ⊢ ( ( vol* ‘ ∪ ran 𝐹 ) ∈ ℝ* → ( ( vol* ‘ ∪ ran 𝐹 ) = +∞ ↔ ¬ ( vol* ‘ ∪ ran 𝐹 ) < +∞ ) )
133 20 132 syl ⊢ ( 𝜑 → ( ( vol* ‘ ∪ ran 𝐹 ) = +∞ ↔ ¬ ( vol* ‘ ∪ ran 𝐹 ) < +∞ ) )
134 rexr ⊢ ( ( 𝑆 ‘ 𝑘 ) ∈ ℝ → ( 𝑆 ‘ 𝑘 ) ∈ ℝ* )
135 pnfge ⊢ ( ( 𝑆 ‘ 𝑘 ) ∈ ℝ* → ( 𝑆 ‘ 𝑘 ) ≤ +∞ )
136 108 134 135 3syl ⊢ ( ( 𝜑 ∧ 𝑘 ∈ ℕ ) → ( 𝑆 ‘ 𝑘 ) ≤ +∞ )
137 136 ex ⊢ ( 𝜑 → ( 𝑘 ∈ ℕ → ( 𝑆 ‘ 𝑘 ) ≤ +∞ ) )
138 breq2 ⊢ ( ( vol* ‘ ∪ ran 𝐹 ) = +∞ → ( ( 𝑆 ‘ 𝑘 ) ≤ ( vol* ‘ ∪ ran 𝐹 ) ↔ ( 𝑆 ‘ 𝑘 ) ≤ +∞ ) )
139 138 imbi2d ⊢ ( ( vol* ‘ ∪ ran 𝐹 ) = +∞ → ( ( 𝑘 ∈ ℕ → ( 𝑆 ‘ 𝑘 ) ≤ ( vol* ‘ ∪ ran 𝐹 ) ) ↔ ( 𝑘 ∈ ℕ → ( 𝑆 ‘ 𝑘 ) ≤ +∞ ) ) )
140 137 139 syl5ibrcom ⊢ ( 𝜑 → ( ( vol* ‘ ∪ ran 𝐹 ) = +∞ → ( 𝑘 ∈ ℕ → ( 𝑆 ‘ 𝑘 ) ≤ ( vol* ‘ ∪ ran 𝐹 ) ) ) )
141 133 140 sylbird ⊢ ( 𝜑 → ( ¬ ( vol* ‘ ∪ ran 𝐹 ) < +∞ → ( 𝑘 ∈ ℕ → ( 𝑆 ‘ 𝑘 ) ≤ ( vol* ‘ ∪ ran 𝐹 ) ) ) )
142 131 141 pm2.61d ⊢ ( 𝜑 → ( 𝑘 ∈ ℕ → ( 𝑆 ‘ 𝑘 ) ≤ ( vol* ‘ ∪ ran 𝐹 ) ) )
143 142 ralrimiv ⊢ ( 𝜑 → ∀ 𝑘 ∈ ℕ ( 𝑆 ‘ 𝑘 ) ≤ ( vol* ‘ ∪ ran 𝐹 ) )
144 34 ffnd ⊢ ( 𝜑 → 𝑆 Fn ℕ )
145 breq1 ⊢ ( 𝑧 = ( 𝑆 ‘ 𝑘 ) → ( 𝑧 ≤ ( vol* ‘ ∪ ran 𝐹 ) ↔ ( 𝑆 ‘ 𝑘 ) ≤ ( vol* ‘ ∪ ran 𝐹 ) ) )
146 145 ralrn ⊢ ( 𝑆 Fn ℕ → ( ∀ 𝑧 ∈ ran 𝑆 𝑧 ≤ ( vol* ‘ ∪ ran 𝐹 ) ↔ ∀ 𝑘 ∈ ℕ ( 𝑆 ‘ 𝑘 ) ≤ ( vol* ‘ ∪ ran 𝐹 ) ) )
147 144 146 syl ⊢ ( 𝜑 → ( ∀ 𝑧 ∈ ran 𝑆 𝑧 ≤ ( vol* ‘ ∪ ran 𝐹 ) ↔ ∀ 𝑘 ∈ ℕ ( 𝑆 ‘ 𝑘 ) ≤ ( vol* ‘ ∪ ran 𝐹 ) ) )
148 143 147 mpbird ⊢ ( 𝜑 → ∀ 𝑧 ∈ ran 𝑆 𝑧 ≤ ( vol* ‘ ∪ ran 𝐹 ) )
149 supxrleub ⊢ ( ( ran 𝑆 ⊆ ℝ* ∧ ( vol* ‘ ∪ ran 𝐹 ) ∈ ℝ* ) → ( sup ( ran 𝑆 , ℝ* , < ) ≤ ( vol* ‘ ∪ ran 𝐹 ) ↔ ∀ 𝑧 ∈ ran 𝑆 𝑧 ≤ ( vol* ‘ ∪ ran 𝐹 ) ) )
150 37 20 149 syl2anc ⊢ ( 𝜑 → ( sup ( ran 𝑆 , ℝ* , < ) ≤ ( vol* ‘ ∪ ran 𝐹 ) ↔ ∀ 𝑧 ∈ ran 𝑆 𝑧 ≤ ( vol* ‘ ∪ ran 𝐹 ) ) )
151 148 150 mpbird ⊢ ( 𝜑 → sup ( ran 𝑆 , ℝ* , < ) ≤ ( vol* ‘ ∪ ran 𝐹 ) )
152 20 39 63 151 xrletrid ⊢ ( 𝜑 → ( vol* ‘ ∪ ran 𝐹 ) = sup ( ran 𝑆 , ℝ* , < ) )
153 9 152 eqtrd ⊢ ( 𝜑 → ( vol ‘ ∪ ran 𝐹 ) = sup ( ran 𝑆 , ℝ* , < ) )