Metamath Proof Explorer

Theorem uniioovol

Description: A disjoint union of open intervals has volume equal to the sum of the volume of the intervals. (This proof does not use countable choice, unlike voliun .) Lemma 565Ca of Fremlin5 p. 213. (Contributed by Mario Carneiro, 26-Mar-2015)

Ref Expression
Hypotheses uniioombl.1 ⊢ ( 𝜑 → 𝐹 : ℕ ⟶ ( ≤ ∩ ( ℝ × ℝ ) ) )
uniioombl.2 ⊢ ( 𝜑 → Disj 𝑥 ∈ ℕ ( (,) ‘ ( 𝐹 ‘ 𝑥 ) ) )
uniioombl.3 ⊢ 𝑆 = seq 1 ( + , ( ( abs ∘ − ) ∘ 𝐹 ) )
Assertion uniioovol ( 𝜑 → ( vol* ‘ ∪ ran ( (,) ∘ 𝐹 ) ) = sup ( ran 𝑆 , ℝ* , < ) )

Proof

Step Hyp Ref Expression
1 uniioombl.1 ⊢ ( 𝜑 → 𝐹 : ℕ ⟶ ( ≤ ∩ ( ℝ × ℝ ) ) )
2 uniioombl.2 ⊢ ( 𝜑 → Disj 𝑥 ∈ ℕ ( (,) ‘ ( 𝐹 ‘ 𝑥 ) ) )
3 uniioombl.3 ⊢ 𝑆 = seq 1 ( + , ( ( abs ∘ − ) ∘ 𝐹 ) )
4 ioof ⊢ (,) : ( ℝ* × ℝ* ) ⟶ 𝒫 ℝ
5 inss2 ⊢ ( ≤ ∩ ( ℝ × ℝ ) ) ⊆ ( ℝ × ℝ )
6 rexpssxrxp ⊢ ( ℝ × ℝ ) ⊆ ( ℝ* × ℝ* )
7 5 6 sstri ⊢ ( ≤ ∩ ( ℝ × ℝ ) ) ⊆ ( ℝ* × ℝ* )
8 fss ⊢ ( ( 𝐹 : ℕ ⟶ ( ≤ ∩ ( ℝ × ℝ ) ) ∧ ( ≤ ∩ ( ℝ × ℝ ) ) ⊆ ( ℝ* × ℝ* ) ) → 𝐹 : ℕ ⟶ ( ℝ* × ℝ* ) )
9 1 7 8 sylancl ⊢ ( 𝜑 → 𝐹 : ℕ ⟶ ( ℝ* × ℝ* ) )
10 fco ⊢ ( ( (,) : ( ℝ* × ℝ* ) ⟶ 𝒫 ℝ ∧ 𝐹 : ℕ ⟶ ( ℝ* × ℝ* ) ) → ( (,) ∘ 𝐹 ) : ℕ ⟶ 𝒫 ℝ )
11 4 9 10 sylancr ⊢ ( 𝜑 → ( (,) ∘ 𝐹 ) : ℕ ⟶ 𝒫 ℝ )
12 11 frnd ⊢ ( 𝜑 → ran ( (,) ∘ 𝐹 ) ⊆ 𝒫 ℝ )
13 sspwuni ⊢ ( ran ( (,) ∘ 𝐹 ) ⊆ 𝒫 ℝ ↔ ∪ ran ( (,) ∘ 𝐹 ) ⊆ ℝ )
14 12 13 sylib ⊢ ( 𝜑 → ∪ ran ( (,) ∘ 𝐹 ) ⊆ ℝ )
15 ovolcl ⊢ ( ∪ ran ( (,) ∘ 𝐹 ) ⊆ ℝ → ( vol* ‘ ∪ ran ( (,) ∘ 𝐹 ) ) ∈ ℝ* )
16 14 15 syl ⊢ ( 𝜑 → ( vol* ‘ ∪ ran ( (,) ∘ 𝐹 ) ) ∈ ℝ* )
17 eqid ⊢ ( ( abs ∘ − ) ∘ 𝐹 ) = ( ( abs ∘ − ) ∘ 𝐹 )
18 17 3 ovolsf ⊢ ( 𝐹 : ℕ ⟶ ( ≤ ∩ ( ℝ × ℝ ) ) → 𝑆 : ℕ ⟶ ( 0 [,) +∞ ) )
19 frn ⊢ ( 𝑆 : ℕ ⟶ ( 0 [,) +∞ ) → ran 𝑆 ⊆ ( 0 [,) +∞ ) )
20 1 18 19 3syl ⊢ ( 𝜑 → ran 𝑆 ⊆ ( 0 [,) +∞ ) )
21 icossxr ⊢ ( 0 [,) +∞ ) ⊆ ℝ*
22 20 21 sstrdi ⊢ ( 𝜑 → ran 𝑆 ⊆ ℝ* )
23 supxrcl ⊢ ( ran 𝑆 ⊆ ℝ* → sup ( ran 𝑆 , ℝ* , < ) ∈ ℝ* )
24 22 23 syl ⊢ ( 𝜑 → sup ( ran 𝑆 , ℝ* , < ) ∈ ℝ* )
25 ssid ⊢ ∪ ran ( (,) ∘ 𝐹 ) ⊆ ∪ ran ( (,) ∘ 𝐹 )
26 3 ovollb ⊢ ( ( 𝐹 : ℕ ⟶ ( ≤ ∩ ( ℝ × ℝ ) ) ∧ ∪ ran ( (,) ∘ 𝐹 ) ⊆ ∪ ran ( (,) ∘ 𝐹 ) ) → ( vol* ‘ ∪ ran ( (,) ∘ 𝐹 ) ) ≤ sup ( ran 𝑆 , ℝ* , < ) )
27 1 25 26 sylancl ⊢ ( 𝜑 → ( vol* ‘ ∪ ran ( (,) ∘ 𝐹 ) ) ≤ sup ( ran 𝑆 , ℝ* , < ) )
28 3 fveq1i ⊢ ( 𝑆 ‘ 𝑛 ) = ( seq 1 ( + , ( ( abs ∘ − ) ∘ 𝐹 ) ) ‘ 𝑛 )
29 1 adantr ⊢ ( ( 𝜑 ∧ 𝑛 ∈ ℕ ) → 𝐹 : ℕ ⟶ ( ≤ ∩ ( ℝ × ℝ ) ) )
30 elfznn ⊢ ( 𝑥 ∈ ( 1 ... 𝑛 ) → 𝑥 ∈ ℕ )
31 17 ovolfsval ⊢ ( ( 𝐹 : ℕ ⟶ ( ≤ ∩ ( ℝ × ℝ ) ) ∧ 𝑥 ∈ ℕ ) → ( ( ( abs ∘ − ) ∘ 𝐹 ) ‘ 𝑥 ) = ( ( 2nd ‘ ( 𝐹 ‘ 𝑥 ) ) − ( 1st ‘ ( 𝐹 ‘ 𝑥 ) ) ) )
32 29 30 31 syl2an ⊢ ( ( ( 𝜑 ∧ 𝑛 ∈ ℕ ) ∧ 𝑥 ∈ ( 1 ... 𝑛 ) ) → ( ( ( abs ∘ − ) ∘ 𝐹 ) ‘ 𝑥 ) = ( ( 2nd ‘ ( 𝐹 ‘ 𝑥 ) ) − ( 1st ‘ ( 𝐹 ‘ 𝑥 ) ) ) )
33 fvco3 ⊢ ( ( 𝐹 : ℕ ⟶ ( ≤ ∩ ( ℝ × ℝ ) ) ∧ 𝑥 ∈ ℕ ) → ( ( (,) ∘ 𝐹 ) ‘ 𝑥 ) = ( (,) ‘ ( 𝐹 ‘ 𝑥 ) ) )
34 29 30 33 syl2an ⊢ ( ( ( 𝜑 ∧ 𝑛 ∈ ℕ ) ∧ 𝑥 ∈ ( 1 ... 𝑛 ) ) → ( ( (,) ∘ 𝐹 ) ‘ 𝑥 ) = ( (,) ‘ ( 𝐹 ‘ 𝑥 ) ) )
35 ffvelcdm ⊢ ( ( 𝐹 : ℕ ⟶ ( ≤ ∩ ( ℝ × ℝ ) ) ∧ 𝑥 ∈ ℕ ) → ( 𝐹 ‘ 𝑥 ) ∈ ( ≤ ∩ ( ℝ × ℝ ) ) )
36 29 30 35 syl2an ⊢ ( ( ( 𝜑 ∧ 𝑛 ∈ ℕ ) ∧ 𝑥 ∈ ( 1 ... 𝑛 ) ) → ( 𝐹 ‘ 𝑥 ) ∈ ( ≤ ∩ ( ℝ × ℝ ) ) )
37 36 elin2d ⊢ ( ( ( 𝜑 ∧ 𝑛 ∈ ℕ ) ∧ 𝑥 ∈ ( 1 ... 𝑛 ) ) → ( 𝐹 ‘ 𝑥 ) ∈ ( ℝ × ℝ ) )
38 1st2nd2 ⊢ ( ( 𝐹 ‘ 𝑥 ) ∈ ( ℝ × ℝ ) → ( 𝐹 ‘ 𝑥 ) = ⟨ ( 1st ‘ ( 𝐹 ‘ 𝑥 ) ) , ( 2nd ‘ ( 𝐹 ‘ 𝑥 ) ) ⟩ )
39 37 38 syl ⊢ ( ( ( 𝜑 ∧ 𝑛 ∈ ℕ ) ∧ 𝑥 ∈ ( 1 ... 𝑛 ) ) → ( 𝐹 ‘ 𝑥 ) = ⟨ ( 1st ‘ ( 𝐹 ‘ 𝑥 ) ) , ( 2nd ‘ ( 𝐹 ‘ 𝑥 ) ) ⟩ )
40 39 fveq2d ⊢ ( ( ( 𝜑 ∧ 𝑛 ∈ ℕ ) ∧ 𝑥 ∈ ( 1 ... 𝑛 ) ) → ( (,) ‘ ( 𝐹 ‘ 𝑥 ) ) = ( (,) ‘ ⟨ ( 1st ‘ ( 𝐹 ‘ 𝑥 ) ) , ( 2nd ‘ ( 𝐹 ‘ 𝑥 ) ) ⟩ ) )
41 df-ov ⊢ ( ( 1st ‘ ( 𝐹 ‘ 𝑥 ) ) (,) ( 2nd ‘ ( 𝐹 ‘ 𝑥 ) ) ) = ( (,) ‘ ⟨ ( 1st ‘ ( 𝐹 ‘ 𝑥 ) ) , ( 2nd ‘ ( 𝐹 ‘ 𝑥 ) ) ⟩ )
42 40 41 eqtr4di ⊢ ( ( ( 𝜑 ∧ 𝑛 ∈ ℕ ) ∧ 𝑥 ∈ ( 1 ... 𝑛 ) ) → ( (,) ‘ ( 𝐹 ‘ 𝑥 ) ) = ( ( 1st ‘ ( 𝐹 ‘ 𝑥 ) ) (,) ( 2nd ‘ ( 𝐹 ‘ 𝑥 ) ) ) )
43 34 42 eqtrd ⊢ ( ( ( 𝜑 ∧ 𝑛 ∈ ℕ ) ∧ 𝑥 ∈ ( 1 ... 𝑛 ) ) → ( ( (,) ∘ 𝐹 ) ‘ 𝑥 ) = ( ( 1st ‘ ( 𝐹 ‘ 𝑥 ) ) (,) ( 2nd ‘ ( 𝐹 ‘ 𝑥 ) ) ) )
44 ioombl ⊢ ( ( 1st ‘ ( 𝐹 ‘ 𝑥 ) ) (,) ( 2nd ‘ ( 𝐹 ‘ 𝑥 ) ) ) ∈ dom vol
45 43 44 eqeltrdi ⊢ ( ( ( 𝜑 ∧ 𝑛 ∈ ℕ ) ∧ 𝑥 ∈ ( 1 ... 𝑛 ) ) → ( ( (,) ∘ 𝐹 ) ‘ 𝑥 ) ∈ dom vol )
46 mblvol ⊢ ( ( ( (,) ∘ 𝐹 ) ‘ 𝑥 ) ∈ dom vol → ( vol ‘ ( ( (,) ∘ 𝐹 ) ‘ 𝑥 ) ) = ( vol* ‘ ( ( (,) ∘ 𝐹 ) ‘ 𝑥 ) ) )
47 45 46 syl ⊢ ( ( ( 𝜑 ∧ 𝑛 ∈ ℕ ) ∧ 𝑥 ∈ ( 1 ... 𝑛 ) ) → ( vol ‘ ( ( (,) ∘ 𝐹 ) ‘ 𝑥 ) ) = ( vol* ‘ ( ( (,) ∘ 𝐹 ) ‘ 𝑥 ) ) )
48 43 fveq2d ⊢ ( ( ( 𝜑 ∧ 𝑛 ∈ ℕ ) ∧ 𝑥 ∈ ( 1 ... 𝑛 ) ) → ( vol* ‘ ( ( (,) ∘ 𝐹 ) ‘ 𝑥 ) ) = ( vol* ‘ ( ( 1st ‘ ( 𝐹 ‘ 𝑥 ) ) (,) ( 2nd ‘ ( 𝐹 ‘ 𝑥 ) ) ) ) )
49 ovolfcl ⊢ ( ( 𝐹 : ℕ ⟶ ( ≤ ∩ ( ℝ × ℝ ) ) ∧ 𝑥 ∈ ℕ ) → ( ( 1st ‘ ( 𝐹 ‘ 𝑥 ) ) ∈ ℝ ∧ ( 2nd ‘ ( 𝐹 ‘ 𝑥 ) ) ∈ ℝ ∧ ( 1st ‘ ( 𝐹 ‘ 𝑥 ) ) ≤ ( 2nd ‘ ( 𝐹 ‘ 𝑥 ) ) ) )
50 29 30 49 syl2an ⊢ ( ( ( 𝜑 ∧ 𝑛 ∈ ℕ ) ∧ 𝑥 ∈ ( 1 ... 𝑛 ) ) → ( ( 1st ‘ ( 𝐹 ‘ 𝑥 ) ) ∈ ℝ ∧ ( 2nd ‘ ( 𝐹 ‘ 𝑥 ) ) ∈ ℝ ∧ ( 1st ‘ ( 𝐹 ‘ 𝑥 ) ) ≤ ( 2nd ‘ ( 𝐹 ‘ 𝑥 ) ) ) )
51 ovolioo ⊢ ( ( ( 1st ‘ ( 𝐹 ‘ 𝑥 ) ) ∈ ℝ ∧ ( 2nd ‘ ( 𝐹 ‘ 𝑥 ) ) ∈ ℝ ∧ ( 1st ‘ ( 𝐹 ‘ 𝑥 ) ) ≤ ( 2nd ‘ ( 𝐹 ‘ 𝑥 ) ) ) → ( vol* ‘ ( ( 1st ‘ ( 𝐹 ‘ 𝑥 ) ) (,) ( 2nd ‘ ( 𝐹 ‘ 𝑥 ) ) ) ) = ( ( 2nd ‘ ( 𝐹 ‘ 𝑥 ) ) − ( 1st ‘ ( 𝐹 ‘ 𝑥 ) ) ) )
52 50 51 syl ⊢ ( ( ( 𝜑 ∧ 𝑛 ∈ ℕ ) ∧ 𝑥 ∈ ( 1 ... 𝑛 ) ) → ( vol* ‘ ( ( 1st ‘ ( 𝐹 ‘ 𝑥 ) ) (,) ( 2nd ‘ ( 𝐹 ‘ 𝑥 ) ) ) ) = ( ( 2nd ‘ ( 𝐹 ‘ 𝑥 ) ) − ( 1st ‘ ( 𝐹 ‘ 𝑥 ) ) ) )
53 47 48 52 3eqtrd ⊢ ( ( ( 𝜑 ∧ 𝑛 ∈ ℕ ) ∧ 𝑥 ∈ ( 1 ... 𝑛 ) ) → ( vol ‘ ( ( (,) ∘ 𝐹 ) ‘ 𝑥 ) ) = ( ( 2nd ‘ ( 𝐹 ‘ 𝑥 ) ) − ( 1st ‘ ( 𝐹 ‘ 𝑥 ) ) ) )
54 32 53 eqtr4d ⊢ ( ( ( 𝜑 ∧ 𝑛 ∈ ℕ ) ∧ 𝑥 ∈ ( 1 ... 𝑛 ) ) → ( ( ( abs ∘ − ) ∘ 𝐹 ) ‘ 𝑥 ) = ( vol ‘ ( ( (,) ∘ 𝐹 ) ‘ 𝑥 ) ) )
55 simpr ⊢ ( ( 𝜑 ∧ 𝑛 ∈ ℕ ) → 𝑛 ∈ ℕ )
56 nnuz ⊢ ℕ = ( ℤ≥ ‘ 1 )
57 55 56 eleqtrdi ⊢ ( ( 𝜑 ∧ 𝑛 ∈ ℕ ) → 𝑛 ∈ ( ℤ≥ ‘ 1 ) )
58 50 simp2d ⊢ ( ( ( 𝜑 ∧ 𝑛 ∈ ℕ ) ∧ 𝑥 ∈ ( 1 ... 𝑛 ) ) → ( 2nd ‘ ( 𝐹 ‘ 𝑥 ) ) ∈ ℝ )
59 50 simp1d ⊢ ( ( ( 𝜑 ∧ 𝑛 ∈ ℕ ) ∧ 𝑥 ∈ ( 1 ... 𝑛 ) ) → ( 1st ‘ ( 𝐹 ‘ 𝑥 ) ) ∈ ℝ )
60 58 59 resubcld ⊢ ( ( ( 𝜑 ∧ 𝑛 ∈ ℕ ) ∧ 𝑥 ∈ ( 1 ... 𝑛 ) ) → ( ( 2nd ‘ ( 𝐹 ‘ 𝑥 ) ) − ( 1st ‘ ( 𝐹 ‘ 𝑥 ) ) ) ∈ ℝ )
61 53 60 eqeltrd ⊢ ( ( ( 𝜑 ∧ 𝑛 ∈ ℕ ) ∧ 𝑥 ∈ ( 1 ... 𝑛 ) ) → ( vol ‘ ( ( (,) ∘ 𝐹 ) ‘ 𝑥 ) ) ∈ ℝ )
62 61 recnd ⊢ ( ( ( 𝜑 ∧ 𝑛 ∈ ℕ ) ∧ 𝑥 ∈ ( 1 ... 𝑛 ) ) → ( vol ‘ ( ( (,) ∘ 𝐹 ) ‘ 𝑥 ) ) ∈ ℂ )
63 54 57 62 fsumser ⊢ ( ( 𝜑 ∧ 𝑛 ∈ ℕ ) → Σ 𝑥 ∈ ( 1 ... 𝑛 ) ( vol ‘ ( ( (,) ∘ 𝐹 ) ‘ 𝑥 ) ) = ( seq 1 ( + , ( ( abs ∘ − ) ∘ 𝐹 ) ) ‘ 𝑛 ) )
64 28 63 eqtr4id ⊢ ( ( 𝜑 ∧ 𝑛 ∈ ℕ ) → ( 𝑆 ‘ 𝑛 ) = Σ 𝑥 ∈ ( 1 ... 𝑛 ) ( vol ‘ ( ( (,) ∘ 𝐹 ) ‘ 𝑥 ) ) )
65 fzfid ⊢ ( ( 𝜑 ∧ 𝑛 ∈ ℕ ) → ( 1 ... 𝑛 ) ∈ Fin )
66 45 61 jca ⊢ ( ( ( 𝜑 ∧ 𝑛 ∈ ℕ ) ∧ 𝑥 ∈ ( 1 ... 𝑛 ) ) → ( ( ( (,) ∘ 𝐹 ) ‘ 𝑥 ) ∈ dom vol ∧ ( vol ‘ ( ( (,) ∘ 𝐹 ) ‘ 𝑥 ) ) ∈ ℝ ) )
67 66 ralrimiva ⊢ ( ( 𝜑 ∧ 𝑛 ∈ ℕ ) → ∀ 𝑥 ∈ ( 1 ... 𝑛 ) ( ( ( (,) ∘ 𝐹 ) ‘ 𝑥 ) ∈ dom vol ∧ ( vol ‘ ( ( (,) ∘ 𝐹 ) ‘ 𝑥 ) ) ∈ ℝ ) )
68 fz1ssnn ⊢ ( 1 ... 𝑛 ) ⊆ ℕ
69 1 33 sylan ⊢ ( ( 𝜑 ∧ 𝑥 ∈ ℕ ) → ( ( (,) ∘ 𝐹 ) ‘ 𝑥 ) = ( (,) ‘ ( 𝐹 ‘ 𝑥 ) ) )
70 69 disjeq2dv ⊢ ( 𝜑 → ( Disj 𝑥 ∈ ℕ ( ( (,) ∘ 𝐹 ) ‘ 𝑥 ) ↔ Disj 𝑥 ∈ ℕ ( (,) ‘ ( 𝐹 ‘ 𝑥 ) ) ) )
71 2 70 mpbird ⊢ ( 𝜑 → Disj 𝑥 ∈ ℕ ( ( (,) ∘ 𝐹 ) ‘ 𝑥 ) )
72 71 adantr ⊢ ( ( 𝜑 ∧ 𝑛 ∈ ℕ ) → Disj 𝑥 ∈ ℕ ( ( (,) ∘ 𝐹 ) ‘ 𝑥 ) )
73 disjss1 ⊢ ( ( 1 ... 𝑛 ) ⊆ ℕ → ( Disj 𝑥 ∈ ℕ ( ( (,) ∘ 𝐹 ) ‘ 𝑥 ) → Disj 𝑥 ∈ ( 1 ... 𝑛 ) ( ( (,) ∘ 𝐹 ) ‘ 𝑥 ) ) )
74 68 72 73 mpsyl ⊢ ( ( 𝜑 ∧ 𝑛 ∈ ℕ ) → Disj 𝑥 ∈ ( 1 ... 𝑛 ) ( ( (,) ∘ 𝐹 ) ‘ 𝑥 ) )
75 volfiniun ⊢ ( ( ( 1 ... 𝑛 ) ∈ Fin ∧ ∀ 𝑥 ∈ ( 1 ... 𝑛 ) ( ( ( (,) ∘ 𝐹 ) ‘ 𝑥 ) ∈ dom vol ∧ ( vol ‘ ( ( (,) ∘ 𝐹 ) ‘ 𝑥 ) ) ∈ ℝ ) ∧ Disj 𝑥 ∈ ( 1 ... 𝑛 ) ( ( (,) ∘ 𝐹 ) ‘ 𝑥 ) ) → ( vol ‘ ∪ 𝑥 ∈ ( 1 ... 𝑛 ) ( ( (,) ∘ 𝐹 ) ‘ 𝑥 ) ) = Σ 𝑥 ∈ ( 1 ... 𝑛 ) ( vol ‘ ( ( (,) ∘ 𝐹 ) ‘ 𝑥 ) ) )
76 65 67 74 75 syl3anc ⊢ ( ( 𝜑 ∧ 𝑛 ∈ ℕ ) → ( vol ‘ ∪ 𝑥 ∈ ( 1 ... 𝑛 ) ( ( (,) ∘ 𝐹 ) ‘ 𝑥 ) ) = Σ 𝑥 ∈ ( 1 ... 𝑛 ) ( vol ‘ ( ( (,) ∘ 𝐹 ) ‘ 𝑥 ) ) )
77 45 ralrimiva ⊢ ( ( 𝜑 ∧ 𝑛 ∈ ℕ ) → ∀ 𝑥 ∈ ( 1 ... 𝑛 ) ( ( (,) ∘ 𝐹 ) ‘ 𝑥 ) ∈ dom vol )
78 finiunmbl ⊢ ( ( ( 1 ... 𝑛 ) ∈ Fin ∧ ∀ 𝑥 ∈ ( 1 ... 𝑛 ) ( ( (,) ∘ 𝐹 ) ‘ 𝑥 ) ∈ dom vol ) → ∪ 𝑥 ∈ ( 1 ... 𝑛 ) ( ( (,) ∘ 𝐹 ) ‘ 𝑥 ) ∈ dom vol )
79 65 77 78 syl2anc ⊢ ( ( 𝜑 ∧ 𝑛 ∈ ℕ ) → ∪ 𝑥 ∈ ( 1 ... 𝑛 ) ( ( (,) ∘ 𝐹 ) ‘ 𝑥 ) ∈ dom vol )
80 mblvol ⊢ ( ∪ 𝑥 ∈ ( 1 ... 𝑛 ) ( ( (,) ∘ 𝐹 ) ‘ 𝑥 ) ∈ dom vol → ( vol ‘ ∪ 𝑥 ∈ ( 1 ... 𝑛 ) ( ( (,) ∘ 𝐹 ) ‘ 𝑥 ) ) = ( vol* ‘ ∪ 𝑥 ∈ ( 1 ... 𝑛 ) ( ( (,) ∘ 𝐹 ) ‘ 𝑥 ) ) )
81 79 80 syl ⊢ ( ( 𝜑 ∧ 𝑛 ∈ ℕ ) → ( vol ‘ ∪ 𝑥 ∈ ( 1 ... 𝑛 ) ( ( (,) ∘ 𝐹 ) ‘ 𝑥 ) ) = ( vol* ‘ ∪ 𝑥 ∈ ( 1 ... 𝑛 ) ( ( (,) ∘ 𝐹 ) ‘ 𝑥 ) ) )
82 64 76 81 3eqtr2d ⊢ ( ( 𝜑 ∧ 𝑛 ∈ ℕ ) → ( 𝑆 ‘ 𝑛 ) = ( vol* ‘ ∪ 𝑥 ∈ ( 1 ... 𝑛 ) ( ( (,) ∘ 𝐹 ) ‘ 𝑥 ) ) )
83 iunss1 ⊢ ( ( 1 ... 𝑛 ) ⊆ ℕ → ∪ 𝑥 ∈ ( 1 ... 𝑛 ) ( ( (,) ∘ 𝐹 ) ‘ 𝑥 ) ⊆ ∪ 𝑥 ∈ ℕ ( ( (,) ∘ 𝐹 ) ‘ 𝑥 ) )
84 68 83 mp1i ⊢ ( ( 𝜑 ∧ 𝑛 ∈ ℕ ) → ∪ 𝑥 ∈ ( 1 ... 𝑛 ) ( ( (,) ∘ 𝐹 ) ‘ 𝑥 ) ⊆ ∪ 𝑥 ∈ ℕ ( ( (,) ∘ 𝐹 ) ‘ 𝑥 ) )
85 11 adantr ⊢ ( ( 𝜑 ∧ 𝑛 ∈ ℕ ) → ( (,) ∘ 𝐹 ) : ℕ ⟶ 𝒫 ℝ )
86 ffn ⊢ ( ( (,) ∘ 𝐹 ) : ℕ ⟶ 𝒫 ℝ → ( (,) ∘ 𝐹 ) Fn ℕ )
87 fniunfv ⊢ ( ( (,) ∘ 𝐹 ) Fn ℕ → ∪ 𝑥 ∈ ℕ ( ( (,) ∘ 𝐹 ) ‘ 𝑥 ) = ∪ ran ( (,) ∘ 𝐹 ) )
88 85 86 87 3syl ⊢ ( ( 𝜑 ∧ 𝑛 ∈ ℕ ) → ∪ 𝑥 ∈ ℕ ( ( (,) ∘ 𝐹 ) ‘ 𝑥 ) = ∪ ran ( (,) ∘ 𝐹 ) )
89 84 88 sseqtrd ⊢ ( ( 𝜑 ∧ 𝑛 ∈ ℕ ) → ∪ 𝑥 ∈ ( 1 ... 𝑛 ) ( ( (,) ∘ 𝐹 ) ‘ 𝑥 ) ⊆ ∪ ran ( (,) ∘ 𝐹 ) )
90 14 adantr ⊢ ( ( 𝜑 ∧ 𝑛 ∈ ℕ ) → ∪ ran ( (,) ∘ 𝐹 ) ⊆ ℝ )
91 ovolss ⊢ ( ( ∪ 𝑥 ∈ ( 1 ... 𝑛 ) ( ( (,) ∘ 𝐹 ) ‘ 𝑥 ) ⊆ ∪ ran ( (,) ∘ 𝐹 ) ∧ ∪ ran ( (,) ∘ 𝐹 ) ⊆ ℝ ) → ( vol* ‘ ∪ 𝑥 ∈ ( 1 ... 𝑛 ) ( ( (,) ∘ 𝐹 ) ‘ 𝑥 ) ) ≤ ( vol* ‘ ∪ ran ( (,) ∘ 𝐹 ) ) )
92 89 90 91 syl2anc ⊢ ( ( 𝜑 ∧ 𝑛 ∈ ℕ ) → ( vol* ‘ ∪ 𝑥 ∈ ( 1 ... 𝑛 ) ( ( (,) ∘ 𝐹 ) ‘ 𝑥 ) ) ≤ ( vol* ‘ ∪ ran ( (,) ∘ 𝐹 ) ) )
93 82 92 eqbrtrd ⊢ ( ( 𝜑 ∧ 𝑛 ∈ ℕ ) → ( 𝑆 ‘ 𝑛 ) ≤ ( vol* ‘ ∪ ran ( (,) ∘ 𝐹 ) ) )
94 93 ralrimiva ⊢ ( 𝜑 → ∀ 𝑛 ∈ ℕ ( 𝑆 ‘ 𝑛 ) ≤ ( vol* ‘ ∪ ran ( (,) ∘ 𝐹 ) ) )
95 1 18 syl ⊢ ( 𝜑 → 𝑆 : ℕ ⟶ ( 0 [,) +∞ ) )
96 ffn ⊢ ( 𝑆 : ℕ ⟶ ( 0 [,) +∞ ) → 𝑆 Fn ℕ )
97 breq1 ⊢ ( 𝑦 = ( 𝑆 ‘ 𝑛 ) → ( 𝑦 ≤ ( vol* ‘ ∪ ran ( (,) ∘ 𝐹 ) ) ↔ ( 𝑆 ‘ 𝑛 ) ≤ ( vol* ‘ ∪ ran ( (,) ∘ 𝐹 ) ) ) )
98 97 ralrn ⊢ ( 𝑆 Fn ℕ → ( ∀ 𝑦 ∈ ran 𝑆 𝑦 ≤ ( vol* ‘ ∪ ran ( (,) ∘ 𝐹 ) ) ↔ ∀ 𝑛 ∈ ℕ ( 𝑆 ‘ 𝑛 ) ≤ ( vol* ‘ ∪ ran ( (,) ∘ 𝐹 ) ) ) )
99 95 96 98 3syl ⊢ ( 𝜑 → ( ∀ 𝑦 ∈ ran 𝑆 𝑦 ≤ ( vol* ‘ ∪ ran ( (,) ∘ 𝐹 ) ) ↔ ∀ 𝑛 ∈ ℕ ( 𝑆 ‘ 𝑛 ) ≤ ( vol* ‘ ∪ ran ( (,) ∘ 𝐹 ) ) ) )
100 94 99 mpbird ⊢ ( 𝜑 → ∀ 𝑦 ∈ ran 𝑆 𝑦 ≤ ( vol* ‘ ∪ ran ( (,) ∘ 𝐹 ) ) )
101 supxrleub ⊢ ( ( ran 𝑆 ⊆ ℝ* ∧ ( vol* ‘ ∪ ran ( (,) ∘ 𝐹 ) ) ∈ ℝ* ) → ( sup ( ran 𝑆 , ℝ* , < ) ≤ ( vol* ‘ ∪ ran ( (,) ∘ 𝐹 ) ) ↔ ∀ 𝑦 ∈ ran 𝑆 𝑦 ≤ ( vol* ‘ ∪ ran ( (,) ∘ 𝐹 ) ) ) )
102 22 16 101 syl2anc ⊢ ( 𝜑 → ( sup ( ran 𝑆 , ℝ* , < ) ≤ ( vol* ‘ ∪ ran ( (,) ∘ 𝐹 ) ) ↔ ∀ 𝑦 ∈ ran 𝑆 𝑦 ≤ ( vol* ‘ ∪ ran ( (,) ∘ 𝐹 ) ) ) )
103 100 102 mpbird ⊢ ( 𝜑 → sup ( ran 𝑆 , ℝ* , < ) ≤ ( vol* ‘ ∪ ran ( (,) ∘ 𝐹 ) ) )
104 16 24 27 103 xrletrid ⊢ ( 𝜑 → ( vol* ‘ ∪ ran ( (,) ∘ 𝐹 ) ) = sup ( ran 𝑆 , ℝ* , < ) )