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

Theorem uniioovol 24941
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 24916.) Lemma 565Ca of [Fremlin5] p. 213. (Contributed by Mario Carneiro, 26-Mar-2015.)
Hypotheses
Ref Expression
uniioombl.1 (𝜑𝐹:ℕ⟶( ≤ ∩ (ℝ × ℝ)))
uniioombl.2 (𝜑Disj 𝑥 ∈ ℕ ((,)‘(𝐹𝑥)))
uniioombl.3 𝑆 = seq1( + , ((abs ∘ − ) ∘ 𝐹))
Assertion
Ref Expression
uniioovol (𝜑 → (vol*‘ ran ((,) ∘ 𝐹)) = sup(ran 𝑆, ℝ*, < ))
Distinct variable groups:   𝑥,𝐹   𝜑,𝑥
Allowed substitution hint:   𝑆(𝑥)

Proof of Theorem uniioovol
Dummy variables 𝑛 𝑦 are mutually distinct and distinct from all other variables.
StepHypRef Expression
1 ioof 13363 . . . . . 6 (,):(ℝ* × ℝ*)⟶𝒫 ℝ
2 uniioombl.1 . . . . . . 7 (𝜑𝐹:ℕ⟶( ≤ ∩ (ℝ × ℝ)))
3 inss2 4189 . . . . . . . 8 ( ≤ ∩ (ℝ × ℝ)) ⊆ (ℝ × ℝ)
4 rexpssxrxp 11199 . . . . . . . 8 (ℝ × ℝ) ⊆ (ℝ* × ℝ*)
53, 4sstri 3953 . . . . . . 7 ( ≤ ∩ (ℝ × ℝ)) ⊆ (ℝ* × ℝ*)
6 fss 6685 . . . . . . 7 ((𝐹:ℕ⟶( ≤ ∩ (ℝ × ℝ)) ∧ ( ≤ ∩ (ℝ × ℝ)) ⊆ (ℝ* × ℝ*)) → 𝐹:ℕ⟶(ℝ* × ℝ*))
72, 5, 6sylancl 586 . . . . . 6 (𝜑𝐹:ℕ⟶(ℝ* × ℝ*))
8 fco 6692 . . . . . 6 (((,):(ℝ* × ℝ*)⟶𝒫 ℝ ∧ 𝐹:ℕ⟶(ℝ* × ℝ*)) → ((,) ∘ 𝐹):ℕ⟶𝒫 ℝ)
91, 7, 8sylancr 587 . . . . 5 (𝜑 → ((,) ∘ 𝐹):ℕ⟶𝒫 ℝ)
109frnd 6676 . . . 4 (𝜑 → ran ((,) ∘ 𝐹) ⊆ 𝒫 ℝ)
11 sspwuni 5060 . . . 4 (ran ((,) ∘ 𝐹) ⊆ 𝒫 ℝ ↔ ran ((,) ∘ 𝐹) ⊆ ℝ)
1210, 11sylib 217 . . 3 (𝜑 ran ((,) ∘ 𝐹) ⊆ ℝ)
13 ovolcl 24840 . . 3 ( ran ((,) ∘ 𝐹) ⊆ ℝ → (vol*‘ ran ((,) ∘ 𝐹)) ∈ ℝ*)
1412, 13syl 17 . 2 (𝜑 → (vol*‘ ran ((,) ∘ 𝐹)) ∈ ℝ*)
15 eqid 2736 . . . . . 6 ((abs ∘ − ) ∘ 𝐹) = ((abs ∘ − ) ∘ 𝐹)
16 uniioombl.3 . . . . . 6 𝑆 = seq1( + , ((abs ∘ − ) ∘ 𝐹))
1715, 16ovolsf 24834 . . . . 5 (𝐹:ℕ⟶( ≤ ∩ (ℝ × ℝ)) → 𝑆:ℕ⟶(0[,)+∞))
18 frn 6675 . . . . 5 (𝑆:ℕ⟶(0[,)+∞) → ran 𝑆 ⊆ (0[,)+∞))
192, 17, 183syl 18 . . . 4 (𝜑 → ran 𝑆 ⊆ (0[,)+∞))
20 icossxr 13348 . . . 4 (0[,)+∞) ⊆ ℝ*
2119, 20sstrdi 3956 . . 3 (𝜑 → ran 𝑆 ⊆ ℝ*)
22 supxrcl 13233 . . 3 (ran 𝑆 ⊆ ℝ* → sup(ran 𝑆, ℝ*, < ) ∈ ℝ*)
2321, 22syl 17 . 2 (𝜑 → sup(ran 𝑆, ℝ*, < ) ∈ ℝ*)
24 ssid 3966 . . 3 ran ((,) ∘ 𝐹) ⊆ ran ((,) ∘ 𝐹)
2516ovollb 24841 . . 3 ((𝐹:ℕ⟶( ≤ ∩ (ℝ × ℝ)) ∧ ran ((,) ∘ 𝐹) ⊆ ran ((,) ∘ 𝐹)) → (vol*‘ ran ((,) ∘ 𝐹)) ≤ sup(ran 𝑆, ℝ*, < ))
262, 24, 25sylancl 586 . 2 (𝜑 → (vol*‘ ran ((,) ∘ 𝐹)) ≤ sup(ran 𝑆, ℝ*, < ))
2716fveq1i 6843 . . . . . . . 8 (𝑆𝑛) = (seq1( + , ((abs ∘ − ) ∘ 𝐹))‘𝑛)
282adantr 481 . . . . . . . . . . 11 ((𝜑𝑛 ∈ ℕ) → 𝐹:ℕ⟶( ≤ ∩ (ℝ × ℝ)))
29 elfznn 13469 . . . . . . . . . . 11 (𝑥 ∈ (1...𝑛) → 𝑥 ∈ ℕ)
3015ovolfsval 24832 . . . . . . . . . . 11 ((𝐹:ℕ⟶( ≤ ∩ (ℝ × ℝ)) ∧ 𝑥 ∈ ℕ) → (((abs ∘ − ) ∘ 𝐹)‘𝑥) = ((2nd ‘(𝐹𝑥)) − (1st ‘(𝐹𝑥))))
3128, 29, 30syl2an 596 . . . . . . . . . 10 (((𝜑𝑛 ∈ ℕ) ∧ 𝑥 ∈ (1...𝑛)) → (((abs ∘ − ) ∘ 𝐹)‘𝑥) = ((2nd ‘(𝐹𝑥)) − (1st ‘(𝐹𝑥))))
32 fvco3 6940 . . . . . . . . . . . . . . 15 ((𝐹:ℕ⟶( ≤ ∩ (ℝ × ℝ)) ∧ 𝑥 ∈ ℕ) → (((,) ∘ 𝐹)‘𝑥) = ((,)‘(𝐹𝑥)))
3328, 29, 32syl2an 596 . . . . . . . . . . . . . 14 (((𝜑𝑛 ∈ ℕ) ∧ 𝑥 ∈ (1...𝑛)) → (((,) ∘ 𝐹)‘𝑥) = ((,)‘(𝐹𝑥)))
34 ffvelcdm 7032 . . . . . . . . . . . . . . . . . . 19 ((𝐹:ℕ⟶( ≤ ∩ (ℝ × ℝ)) ∧ 𝑥 ∈ ℕ) → (𝐹𝑥) ∈ ( ≤ ∩ (ℝ × ℝ)))
3528, 29, 34syl2an 596 . . . . . . . . . . . . . . . . . 18 (((𝜑𝑛 ∈ ℕ) ∧ 𝑥 ∈ (1...𝑛)) → (𝐹𝑥) ∈ ( ≤ ∩ (ℝ × ℝ)))
3635elin2d 4159 . . . . . . . . . . . . . . . . 17 (((𝜑𝑛 ∈ ℕ) ∧ 𝑥 ∈ (1...𝑛)) → (𝐹𝑥) ∈ (ℝ × ℝ))
37 1st2nd2 7959 . . . . . . . . . . . . . . . . 17 ((𝐹𝑥) ∈ (ℝ × ℝ) → (𝐹𝑥) = ⟨(1st ‘(𝐹𝑥)), (2nd ‘(𝐹𝑥))⟩)
3836, 37syl 17 . . . . . . . . . . . . . . . 16 (((𝜑𝑛 ∈ ℕ) ∧ 𝑥 ∈ (1...𝑛)) → (𝐹𝑥) = ⟨(1st ‘(𝐹𝑥)), (2nd ‘(𝐹𝑥))⟩)
3938fveq2d 6846 . . . . . . . . . . . . . . 15 (((𝜑𝑛 ∈ ℕ) ∧ 𝑥 ∈ (1...𝑛)) → ((,)‘(𝐹𝑥)) = ((,)‘⟨(1st ‘(𝐹𝑥)), (2nd ‘(𝐹𝑥))⟩))
40 df-ov 7359 . . . . . . . . . . . . . . 15 ((1st ‘(𝐹𝑥))(,)(2nd ‘(𝐹𝑥))) = ((,)‘⟨(1st ‘(𝐹𝑥)), (2nd ‘(𝐹𝑥))⟩)
4139, 40eqtr4di 2794 . . . . . . . . . . . . . 14 (((𝜑𝑛 ∈ ℕ) ∧ 𝑥 ∈ (1...𝑛)) → ((,)‘(𝐹𝑥)) = ((1st ‘(𝐹𝑥))(,)(2nd ‘(𝐹𝑥))))
4233, 41eqtrd 2776 . . . . . . . . . . . . 13 (((𝜑𝑛 ∈ ℕ) ∧ 𝑥 ∈ (1...𝑛)) → (((,) ∘ 𝐹)‘𝑥) = ((1st ‘(𝐹𝑥))(,)(2nd ‘(𝐹𝑥))))
43 ioombl 24927 . . . . . . . . . . . . 13 ((1st ‘(𝐹𝑥))(,)(2nd ‘(𝐹𝑥))) ∈ dom vol
4442, 43eqeltrdi 2846 . . . . . . . . . . . 12 (((𝜑𝑛 ∈ ℕ) ∧ 𝑥 ∈ (1...𝑛)) → (((,) ∘ 𝐹)‘𝑥) ∈ dom vol)
45 mblvol 24892 . . . . . . . . . . . 12 ((((,) ∘ 𝐹)‘𝑥) ∈ dom vol → (vol‘(((,) ∘ 𝐹)‘𝑥)) = (vol*‘(((,) ∘ 𝐹)‘𝑥)))
4644, 45syl 17 . . . . . . . . . . 11 (((𝜑𝑛 ∈ ℕ) ∧ 𝑥 ∈ (1...𝑛)) → (vol‘(((,) ∘ 𝐹)‘𝑥)) = (vol*‘(((,) ∘ 𝐹)‘𝑥)))
4742fveq2d 6846 . . . . . . . . . . 11 (((𝜑𝑛 ∈ ℕ) ∧ 𝑥 ∈ (1...𝑛)) → (vol*‘(((,) ∘ 𝐹)‘𝑥)) = (vol*‘((1st ‘(𝐹𝑥))(,)(2nd ‘(𝐹𝑥)))))
48 ovolfcl 24828 . . . . . . . . . . . . 13 ((𝐹:ℕ⟶( ≤ ∩ (ℝ × ℝ)) ∧ 𝑥 ∈ ℕ) → ((1st ‘(𝐹𝑥)) ∈ ℝ ∧ (2nd ‘(𝐹𝑥)) ∈ ℝ ∧ (1st ‘(𝐹𝑥)) ≤ (2nd ‘(𝐹𝑥))))
4928, 29, 48syl2an 596 . . . . . . . . . . . 12 (((𝜑𝑛 ∈ ℕ) ∧ 𝑥 ∈ (1...𝑛)) → ((1st ‘(𝐹𝑥)) ∈ ℝ ∧ (2nd ‘(𝐹𝑥)) ∈ ℝ ∧ (1st ‘(𝐹𝑥)) ≤ (2nd ‘(𝐹𝑥))))
50 ovolioo 24930 . . . . . . . . . . . 12 (((1st ‘(𝐹𝑥)) ∈ ℝ ∧ (2nd ‘(𝐹𝑥)) ∈ ℝ ∧ (1st ‘(𝐹𝑥)) ≤ (2nd ‘(𝐹𝑥))) → (vol*‘((1st ‘(𝐹𝑥))(,)(2nd ‘(𝐹𝑥)))) = ((2nd ‘(𝐹𝑥)) − (1st ‘(𝐹𝑥))))
5149, 50syl 17 . . . . . . . . . . 11 (((𝜑𝑛 ∈ ℕ) ∧ 𝑥 ∈ (1...𝑛)) → (vol*‘((1st ‘(𝐹𝑥))(,)(2nd ‘(𝐹𝑥)))) = ((2nd ‘(𝐹𝑥)) − (1st ‘(𝐹𝑥))))
5246, 47, 513eqtrd 2780 . . . . . . . . . 10 (((𝜑𝑛 ∈ ℕ) ∧ 𝑥 ∈ (1...𝑛)) → (vol‘(((,) ∘ 𝐹)‘𝑥)) = ((2nd ‘(𝐹𝑥)) − (1st ‘(𝐹𝑥))))
5331, 52eqtr4d 2779 . . . . . . . . 9 (((𝜑𝑛 ∈ ℕ) ∧ 𝑥 ∈ (1...𝑛)) → (((abs ∘ − ) ∘ 𝐹)‘𝑥) = (vol‘(((,) ∘ 𝐹)‘𝑥)))
54 simpr 485 . . . . . . . . . 10 ((𝜑𝑛 ∈ ℕ) → 𝑛 ∈ ℕ)
55 nnuz 12805 . . . . . . . . . 10 ℕ = (ℤ‘1)
5654, 55eleqtrdi 2848 . . . . . . . . 9 ((𝜑𝑛 ∈ ℕ) → 𝑛 ∈ (ℤ‘1))
5749simp2d 1143 . . . . . . . . . . . 12 (((𝜑𝑛 ∈ ℕ) ∧ 𝑥 ∈ (1...𝑛)) → (2nd ‘(𝐹𝑥)) ∈ ℝ)
5849simp1d 1142 . . . . . . . . . . . 12 (((𝜑𝑛 ∈ ℕ) ∧ 𝑥 ∈ (1...𝑛)) → (1st ‘(𝐹𝑥)) ∈ ℝ)
5957, 58resubcld 11582 . . . . . . . . . . 11 (((𝜑𝑛 ∈ ℕ) ∧ 𝑥 ∈ (1...𝑛)) → ((2nd ‘(𝐹𝑥)) − (1st ‘(𝐹𝑥))) ∈ ℝ)
6052, 59eqeltrd 2838 . . . . . . . . . 10 (((𝜑𝑛 ∈ ℕ) ∧ 𝑥 ∈ (1...𝑛)) → (vol‘(((,) ∘ 𝐹)‘𝑥)) ∈ ℝ)
6160recnd 11182 . . . . . . . . 9 (((𝜑𝑛 ∈ ℕ) ∧ 𝑥 ∈ (1...𝑛)) → (vol‘(((,) ∘ 𝐹)‘𝑥)) ∈ ℂ)
6253, 56, 61fsumser 15614 . . . . . . . 8 ((𝜑𝑛 ∈ ℕ) → Σ𝑥 ∈ (1...𝑛)(vol‘(((,) ∘ 𝐹)‘𝑥)) = (seq1( + , ((abs ∘ − ) ∘ 𝐹))‘𝑛))
6327, 62eqtr4id 2795 . . . . . . 7 ((𝜑𝑛 ∈ ℕ) → (𝑆𝑛) = Σ𝑥 ∈ (1...𝑛)(vol‘(((,) ∘ 𝐹)‘𝑥)))
64 fzfid 13877 . . . . . . . 8 ((𝜑𝑛 ∈ ℕ) → (1...𝑛) ∈ Fin)
6544, 60jca 512 . . . . . . . . 9 (((𝜑𝑛 ∈ ℕ) ∧ 𝑥 ∈ (1...𝑛)) → ((((,) ∘ 𝐹)‘𝑥) ∈ dom vol ∧ (vol‘(((,) ∘ 𝐹)‘𝑥)) ∈ ℝ))
6665ralrimiva 3143 . . . . . . . 8 ((𝜑𝑛 ∈ ℕ) → ∀𝑥 ∈ (1...𝑛)((((,) ∘ 𝐹)‘𝑥) ∈ dom vol ∧ (vol‘(((,) ∘ 𝐹)‘𝑥)) ∈ ℝ))
67 fz1ssnn 13471 . . . . . . . . 9 (1...𝑛) ⊆ ℕ
68 uniioombl.2 . . . . . . . . . . 11 (𝜑Disj 𝑥 ∈ ℕ ((,)‘(𝐹𝑥)))
692, 32sylan 580 . . . . . . . . . . . 12 ((𝜑𝑥 ∈ ℕ) → (((,) ∘ 𝐹)‘𝑥) = ((,)‘(𝐹𝑥)))
7069disjeq2dv 5075 . . . . . . . . . . 11 (𝜑 → (Disj 𝑥 ∈ ℕ (((,) ∘ 𝐹)‘𝑥) ↔ Disj 𝑥 ∈ ℕ ((,)‘(𝐹𝑥))))
7168, 70mpbird 256 . . . . . . . . . 10 (𝜑Disj 𝑥 ∈ ℕ (((,) ∘ 𝐹)‘𝑥))
7271adantr 481 . . . . . . . . 9 ((𝜑𝑛 ∈ ℕ) → Disj 𝑥 ∈ ℕ (((,) ∘ 𝐹)‘𝑥))
73 disjss1 5076 . . . . . . . . 9 ((1...𝑛) ⊆ ℕ → (Disj 𝑥 ∈ ℕ (((,) ∘ 𝐹)‘𝑥) → Disj 𝑥 ∈ (1...𝑛)(((,) ∘ 𝐹)‘𝑥)))
7467, 72, 73mpsyl 68 . . . . . . . 8 ((𝜑𝑛 ∈ ℕ) → Disj 𝑥 ∈ (1...𝑛)(((,) ∘ 𝐹)‘𝑥))
75 volfiniun 24909 . . . . . . . 8 (((1...𝑛) ∈ Fin ∧ ∀𝑥 ∈ (1...𝑛)((((,) ∘ 𝐹)‘𝑥) ∈ dom vol ∧ (vol‘(((,) ∘ 𝐹)‘𝑥)) ∈ ℝ) ∧ Disj 𝑥 ∈ (1...𝑛)(((,) ∘ 𝐹)‘𝑥)) → (vol‘ 𝑥 ∈ (1...𝑛)(((,) ∘ 𝐹)‘𝑥)) = Σ𝑥 ∈ (1...𝑛)(vol‘(((,) ∘ 𝐹)‘𝑥)))
7664, 66, 74, 75syl3anc 1371 . . . . . . 7 ((𝜑𝑛 ∈ ℕ) → (vol‘ 𝑥 ∈ (1...𝑛)(((,) ∘ 𝐹)‘𝑥)) = Σ𝑥 ∈ (1...𝑛)(vol‘(((,) ∘ 𝐹)‘𝑥)))
7744ralrimiva 3143 . . . . . . . . 9 ((𝜑𝑛 ∈ ℕ) → ∀𝑥 ∈ (1...𝑛)(((,) ∘ 𝐹)‘𝑥) ∈ dom vol)
78 finiunmbl 24906 . . . . . . . . 9 (((1...𝑛) ∈ Fin ∧ ∀𝑥 ∈ (1...𝑛)(((,) ∘ 𝐹)‘𝑥) ∈ dom vol) → 𝑥 ∈ (1...𝑛)(((,) ∘ 𝐹)‘𝑥) ∈ dom vol)
7964, 77, 78syl2anc 584 . . . . . . . 8 ((𝜑𝑛 ∈ ℕ) → 𝑥 ∈ (1...𝑛)(((,) ∘ 𝐹)‘𝑥) ∈ dom vol)
80 mblvol 24892 . . . . . . . 8 ( 𝑥 ∈ (1...𝑛)(((,) ∘ 𝐹)‘𝑥) ∈ dom vol → (vol‘ 𝑥 ∈ (1...𝑛)(((,) ∘ 𝐹)‘𝑥)) = (vol*‘ 𝑥 ∈ (1...𝑛)(((,) ∘ 𝐹)‘𝑥)))
8179, 80syl 17 . . . . . . 7 ((𝜑𝑛 ∈ ℕ) → (vol‘ 𝑥 ∈ (1...𝑛)(((,) ∘ 𝐹)‘𝑥)) = (vol*‘ 𝑥 ∈ (1...𝑛)(((,) ∘ 𝐹)‘𝑥)))
8263, 76, 813eqtr2d 2782 . . . . . 6 ((𝜑𝑛 ∈ ℕ) → (𝑆𝑛) = (vol*‘ 𝑥 ∈ (1...𝑛)(((,) ∘ 𝐹)‘𝑥)))
83 iunss1 4968 . . . . . . . . 9 ((1...𝑛) ⊆ ℕ → 𝑥 ∈ (1...𝑛)(((,) ∘ 𝐹)‘𝑥) ⊆ 𝑥 ∈ ℕ (((,) ∘ 𝐹)‘𝑥))
8467, 83mp1i 13 . . . . . . . 8 ((𝜑𝑛 ∈ ℕ) → 𝑥 ∈ (1...𝑛)(((,) ∘ 𝐹)‘𝑥) ⊆ 𝑥 ∈ ℕ (((,) ∘ 𝐹)‘𝑥))
859adantr 481 . . . . . . . . 9 ((𝜑𝑛 ∈ ℕ) → ((,) ∘ 𝐹):ℕ⟶𝒫 ℝ)
86 ffn 6668 . . . . . . . . 9 (((,) ∘ 𝐹):ℕ⟶𝒫 ℝ → ((,) ∘ 𝐹) Fn ℕ)
87 fniunfv 7193 . . . . . . . . 9 (((,) ∘ 𝐹) Fn ℕ → 𝑥 ∈ ℕ (((,) ∘ 𝐹)‘𝑥) = ran ((,) ∘ 𝐹))
8885, 86, 873syl 18 . . . . . . . 8 ((𝜑𝑛 ∈ ℕ) → 𝑥 ∈ ℕ (((,) ∘ 𝐹)‘𝑥) = ran ((,) ∘ 𝐹))
8984, 88sseqtrd 3984 . . . . . . 7 ((𝜑𝑛 ∈ ℕ) → 𝑥 ∈ (1...𝑛)(((,) ∘ 𝐹)‘𝑥) ⊆ ran ((,) ∘ 𝐹))
9012adantr 481 . . . . . . 7 ((𝜑𝑛 ∈ ℕ) → ran ((,) ∘ 𝐹) ⊆ ℝ)
91 ovolss 24847 . . . . . . 7 (( 𝑥 ∈ (1...𝑛)(((,) ∘ 𝐹)‘𝑥) ⊆ ran ((,) ∘ 𝐹) ∧ ran ((,) ∘ 𝐹) ⊆ ℝ) → (vol*‘ 𝑥 ∈ (1...𝑛)(((,) ∘ 𝐹)‘𝑥)) ≤ (vol*‘ ran ((,) ∘ 𝐹)))
9289, 90, 91syl2anc 584 . . . . . 6 ((𝜑𝑛 ∈ ℕ) → (vol*‘ 𝑥 ∈ (1...𝑛)(((,) ∘ 𝐹)‘𝑥)) ≤ (vol*‘ ran ((,) ∘ 𝐹)))
9382, 92eqbrtrd 5127 . . . . 5 ((𝜑𝑛 ∈ ℕ) → (𝑆𝑛) ≤ (vol*‘ ran ((,) ∘ 𝐹)))
9493ralrimiva 3143 . . . 4 (𝜑 → ∀𝑛 ∈ ℕ (𝑆𝑛) ≤ (vol*‘ ran ((,) ∘ 𝐹)))
952, 17syl 17 . . . . 5 (𝜑𝑆:ℕ⟶(0[,)+∞))
96 ffn 6668 . . . . 5 (𝑆:ℕ⟶(0[,)+∞) → 𝑆 Fn ℕ)
97 breq1 5108 . . . . . 6 (𝑦 = (𝑆𝑛) → (𝑦 ≤ (vol*‘ ran ((,) ∘ 𝐹)) ↔ (𝑆𝑛) ≤ (vol*‘ ran ((,) ∘ 𝐹))))
9897ralrn 7037 . . . . 5 (𝑆 Fn ℕ → (∀𝑦 ∈ ran 𝑆 𝑦 ≤ (vol*‘ ran ((,) ∘ 𝐹)) ↔ ∀𝑛 ∈ ℕ (𝑆𝑛) ≤ (vol*‘ ran ((,) ∘ 𝐹))))
9995, 96, 983syl 18 . . . 4 (𝜑 → (∀𝑦 ∈ ran 𝑆 𝑦 ≤ (vol*‘ ran ((,) ∘ 𝐹)) ↔ ∀𝑛 ∈ ℕ (𝑆𝑛) ≤ (vol*‘ ran ((,) ∘ 𝐹))))
10094, 99mpbird 256 . . 3 (𝜑 → ∀𝑦 ∈ ran 𝑆 𝑦 ≤ (vol*‘ ran ((,) ∘ 𝐹)))
101 supxrleub 13244 . . . 4 ((ran 𝑆 ⊆ ℝ* ∧ (vol*‘ ran ((,) ∘ 𝐹)) ∈ ℝ*) → (sup(ran 𝑆, ℝ*, < ) ≤ (vol*‘ ran ((,) ∘ 𝐹)) ↔ ∀𝑦 ∈ ran 𝑆 𝑦 ≤ (vol*‘ ran ((,) ∘ 𝐹))))
10221, 14, 101syl2anc 584 . . 3 (𝜑 → (sup(ran 𝑆, ℝ*, < ) ≤ (vol*‘ ran ((,) ∘ 𝐹)) ↔ ∀𝑦 ∈ ran 𝑆 𝑦 ≤ (vol*‘ ran ((,) ∘ 𝐹))))
103100, 102mpbird 256 . 2 (𝜑 → sup(ran 𝑆, ℝ*, < ) ≤ (vol*‘ ran ((,) ∘ 𝐹)))
10414, 23, 26, 103xrletrid 13073 1 (𝜑 → (vol*‘ ran ((,) ∘ 𝐹)) = sup(ran 𝑆, ℝ*, < ))
Colors of variables: wff setvar class
Syntax hints:  wi 4  wb 205  wa 396  w3a 1087   = wceq 1541  wcel 2106  wral 3064  cin 3909  wss 3910  𝒫 cpw 4560  cop 4592   cuni 4865   ciun 4954  Disj wdisj 5070   class class class wbr 5105   × cxp 5631  dom cdm 5633  ran crn 5634  ccom 5637   Fn wfn 6491  wf 6492  cfv 6496  (class class class)co 7356  1st c1st 7918  2nd c2nd 7919  Fincfn 8882  supcsup 9375  cr 11049  0cc0 11050  1c1 11051   + caddc 11053  +∞cpnf 11185  *cxr 11187   < clt 11188  cle 11189  cmin 11384  cn 12152  cuz 12762  (,)cioo 13263  [,)cico 13265  ...cfz 13423  seqcseq 13905  abscabs 15118  Σcsu 15569  vol*covol 24824  volcvol 24825
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1797  ax-4 1811  ax-5 1913  ax-6 1971  ax-7 2011  ax-8 2108  ax-9 2116  ax-10 2137  ax-11 2154  ax-12 2171  ax-ext 2707  ax-rep 5242  ax-sep 5256  ax-nul 5263  ax-pow 5320  ax-pr 5384  ax-un 7671  ax-inf2 9576  ax-cnex 11106  ax-resscn 11107  ax-1cn 11108  ax-icn 11109  ax-addcl 11110  ax-addrcl 11111  ax-mulcl 11112  ax-mulrcl 11113  ax-mulcom 11114  ax-addass 11115  ax-mulass 11116  ax-distr 11117  ax-i2m1 11118  ax-1ne0 11119  ax-1rid 11120  ax-rnegex 11121  ax-rrecex 11122  ax-cnre 11123  ax-pre-lttri 11124  ax-pre-lttrn 11125  ax-pre-ltadd 11126  ax-pre-mulgt0 11127  ax-pre-sup 11128
This theorem depends on definitions:  df-bi 206  df-an 397  df-or 846  df-3or 1088  df-3an 1089  df-tru 1544  df-fal 1554  df-ex 1782  df-nf 1786  df-sb 2068  df-mo 2538  df-eu 2567  df-clab 2714  df-cleq 2728  df-clel 2814  df-nfc 2889  df-ne 2944  df-nel 3050  df-ral 3065  df-rex 3074  df-rmo 3353  df-reu 3354  df-rab 3408  df-v 3447  df-sbc 3740  df-csb 3856  df-dif 3913  df-un 3915  df-in 3917  df-ss 3927  df-pss 3929  df-nul 4283  df-if 4487  df-pw 4562  df-sn 4587  df-pr 4589  df-op 4593  df-uni 4866  df-int 4908  df-iun 4956  df-disj 5071  df-br 5106  df-opab 5168  df-mpt 5189  df-tr 5223  df-id 5531  df-eprel 5537  df-po 5545  df-so 5546  df-fr 5588  df-se 5589  df-we 5590  df-xp 5639  df-rel 5640  df-cnv 5641  df-co 5642  df-dm 5643  df-rn 5644  df-res 5645  df-ima 5646  df-pred 6253  df-ord 6320  df-on 6321  df-lim 6322  df-suc 6323  df-iota 6448  df-fun 6498  df-fn 6499  df-f 6500  df-f1 6501  df-fo 6502  df-f1o 6503  df-fv 6504  df-isom 6505  df-riota 7312  df-ov 7359  df-oprab 7360  df-mpo 7361  df-of 7616  df-om 7802  df-1st 7920  df-2nd 7921  df-frecs 8211  df-wrecs 8242  df-recs 8316  df-rdg 8355  df-1o 8411  df-2o 8412  df-er 8647  df-map 8766  df-pm 8767  df-en 8883  df-dom 8884  df-sdom 8885  df-fin 8886  df-fi 9346  df-sup 9377  df-inf 9378  df-oi 9445  df-dju 9836  df-card 9874  df-pnf 11190  df-mnf 11191  df-xr 11192  df-ltxr 11193  df-le 11194  df-sub 11386  df-neg 11387  df-div 11812  df-nn 12153  df-2 12215  df-3 12216  df-n0 12413  df-z 12499  df-uz 12763  df-q 12873  df-rp 12915  df-xneg 13032  df-xadd 13033  df-xmul 13034  df-ioo 13267  df-ico 13269  df-icc 13270  df-fz 13424  df-fzo 13567  df-fl 13696  df-seq 13906  df-exp 13967  df-hash 14230  df-cj 14983  df-re 14984  df-im 14985  df-sqrt 15119  df-abs 15120  df-clim 15369  df-rlim 15370  df-sum 15570  df-rest 17303  df-topgen 17324  df-psmet 20786  df-xmet 20787  df-met 20788  df-bl 20789  df-mopn 20790  df-top 22241  df-topon 22258  df-bases 22294  df-cmp 22736  df-ovol 24826  df-vol 24827
This theorem is referenced by:  uniiccvol  24942  uniioombllem2  24945
  Copyright terms: Public domain W3C validator