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

Theorem voliunlem3 23717
 Description: Lemma for voliun 23719. (Contributed by Mario Carneiro, 20-Mar-2014.)
Hypotheses
Ref Expression
voliunlem.3 (𝜑𝐹:ℕ⟶dom vol)
voliunlem.5 (𝜑Disj 𝑖 ∈ ℕ (𝐹𝑖))
voliunlem.6 𝐻 = (𝑛 ∈ ℕ ↦ (vol*‘(𝑥 ∩ (𝐹𝑛))))
voliunlem3.1 𝑆 = seq1( + , 𝐺)
voliunlem3.2 𝐺 = (𝑛 ∈ ℕ ↦ (vol‘(𝐹𝑛)))
voliunlem3.4 (𝜑 → ∀𝑖 ∈ ℕ (vol‘(𝐹𝑖)) ∈ ℝ)
Assertion
Ref Expression
voliunlem3 (𝜑 → (vol‘ ran 𝐹) = sup(ran 𝑆, ℝ*, < ))
Distinct variable groups:   𝑖,𝑛,𝑥,𝐹   𝑥,𝑆   𝜑,𝑛,𝑥
Allowed substitution hints:   𝜑(𝑖)   𝑆(𝑖,𝑛)   𝐺(𝑥,𝑖,𝑛)   𝐻(𝑥,𝑖,𝑛)

Proof of Theorem voliunlem3
Dummy variables 𝑘 𝑧 are mutually distinct and distinct from all other variables.
StepHypRef Expression
1 voliunlem.3 . . . 4 (𝜑𝐹:ℕ⟶dom vol)
2 voliunlem.5 . . . 4 (𝜑Disj 𝑖 ∈ ℕ (𝐹𝑖))
3 voliunlem.6 . . . 4 𝐻 = (𝑛 ∈ ℕ ↦ (vol*‘(𝑥 ∩ (𝐹𝑛))))
41, 2, 3voliunlem2 23716 . . 3 (𝜑 ran 𝐹 ∈ dom vol)
5 mblvol 23695 . . 3 ( ran 𝐹 ∈ dom vol → (vol‘ ran 𝐹) = (vol*‘ ran 𝐹))
64, 5syl 17 . 2 (𝜑 → (vol‘ ran 𝐹) = (vol*‘ ran 𝐹))
7 eqid 2824 . . . . 5 seq1( + , (𝑛 ∈ ℕ ↦ (vol*‘(𝐹𝑛)))) = seq1( + , (𝑛 ∈ ℕ ↦ (vol*‘(𝐹𝑛))))
8 eqid 2824 . . . . 5 (𝑛 ∈ ℕ ↦ (vol*‘(𝐹𝑛))) = (𝑛 ∈ ℕ ↦ (vol*‘(𝐹𝑛)))
91ffvelrnda 6607 . . . . . 6 ((𝜑𝑛 ∈ ℕ) → (𝐹𝑛) ∈ dom vol)
10 mblss 23696 . . . . . 6 ((𝐹𝑛) ∈ dom vol → (𝐹𝑛) ⊆ ℝ)
119, 10syl 17 . . . . 5 ((𝜑𝑛 ∈ ℕ) → (𝐹𝑛) ⊆ ℝ)
12 mblvol 23695 . . . . . . 7 ((𝐹𝑛) ∈ dom vol → (vol‘(𝐹𝑛)) = (vol*‘(𝐹𝑛)))
139, 12syl 17 . . . . . 6 ((𝜑𝑛 ∈ ℕ) → (vol‘(𝐹𝑛)) = (vol*‘(𝐹𝑛)))
14 voliunlem3.4 . . . . . . 7 (𝜑 → ∀𝑖 ∈ ℕ (vol‘(𝐹𝑖)) ∈ ℝ)
15 2fveq3 6437 . . . . . . . . 9 (𝑖 = 𝑛 → (vol‘(𝐹𝑖)) = (vol‘(𝐹𝑛)))
1615eleq1d 2890 . . . . . . . 8 (𝑖 = 𝑛 → ((vol‘(𝐹𝑖)) ∈ ℝ ↔ (vol‘(𝐹𝑛)) ∈ ℝ))
1716rspccva 3524 . . . . . . 7 ((∀𝑖 ∈ ℕ (vol‘(𝐹𝑖)) ∈ ℝ ∧ 𝑛 ∈ ℕ) → (vol‘(𝐹𝑛)) ∈ ℝ)
1814, 17sylan 577 . . . . . 6 ((𝜑𝑛 ∈ ℕ) → (vol‘(𝐹𝑛)) ∈ ℝ)
1913, 18eqeltrrd 2906 . . . . 5 ((𝜑𝑛 ∈ ℕ) → (vol*‘(𝐹𝑛)) ∈ ℝ)
207, 8, 11, 19ovoliun 23670 . . . 4 (𝜑 → (vol*‘ 𝑛 ∈ ℕ (𝐹𝑛)) ≤ sup(ran seq1( + , (𝑛 ∈ ℕ ↦ (vol*‘(𝐹𝑛)))), ℝ*, < ))
211ffnd 6278 . . . . . 6 (𝜑𝐹 Fn ℕ)
22 fniunfv 6759 . . . . . 6 (𝐹 Fn ℕ → 𝑛 ∈ ℕ (𝐹𝑛) = ran 𝐹)
2321, 22syl 17 . . . . 5 (𝜑 𝑛 ∈ ℕ (𝐹𝑛) = ran 𝐹)
2423fveq2d 6436 . . . 4 (𝜑 → (vol*‘ 𝑛 ∈ ℕ (𝐹𝑛)) = (vol*‘ ran 𝐹))
25 voliunlem3.1 . . . . . . 7 𝑆 = seq1( + , 𝐺)
26 voliunlem3.2 . . . . . . . . 9 𝐺 = (𝑛 ∈ ℕ ↦ (vol‘(𝐹𝑛)))
2713mpteq2dva 4966 . . . . . . . . 9 (𝜑 → (𝑛 ∈ ℕ ↦ (vol‘(𝐹𝑛))) = (𝑛 ∈ ℕ ↦ (vol*‘(𝐹𝑛))))
2826, 27syl5eq 2872 . . . . . . . 8 (𝜑𝐺 = (𝑛 ∈ ℕ ↦ (vol*‘(𝐹𝑛))))
2928seqeq3d 13102 . . . . . . 7 (𝜑 → seq1( + , 𝐺) = seq1( + , (𝑛 ∈ ℕ ↦ (vol*‘(𝐹𝑛)))))
3025, 29syl5req 2873 . . . . . 6 (𝜑 → seq1( + , (𝑛 ∈ ℕ ↦ (vol*‘(𝐹𝑛)))) = 𝑆)
3130rneqd 5584 . . . . 5 (𝜑 → ran seq1( + , (𝑛 ∈ ℕ ↦ (vol*‘(𝐹𝑛)))) = ran 𝑆)
3231supeq1d 8620 . . . 4 (𝜑 → sup(ran seq1( + , (𝑛 ∈ ℕ ↦ (vol*‘(𝐹𝑛)))), ℝ*, < ) = sup(ran 𝑆, ℝ*, < ))
3320, 24, 323brtr3d 4903 . . 3 (𝜑 → (vol*‘ ran 𝐹) ≤ sup(ran 𝑆, ℝ*, < ))
341frnd 6284 . . . . . . . . . . . 12 (𝜑 → ran 𝐹 ⊆ dom vol)
35 mblss 23696 . . . . . . . . . . . . . 14 (𝑥 ∈ dom vol → 𝑥 ⊆ ℝ)
36 reex 10342 . . . . . . . . . . . . . . 15 ℝ ∈ V
3736elpw2 5049 . . . . . . . . . . . . . 14 (𝑥 ∈ 𝒫 ℝ ↔ 𝑥 ⊆ ℝ)
3835, 37sylibr 226 . . . . . . . . . . . . 13 (𝑥 ∈ dom vol → 𝑥 ∈ 𝒫 ℝ)
3938ssriv 3830 . . . . . . . . . . . 12 dom vol ⊆ 𝒫 ℝ
4034, 39syl6ss 3838 . . . . . . . . . . 11 (𝜑 → ran 𝐹 ⊆ 𝒫 ℝ)
41 sspwuni 4831 . . . . . . . . . . 11 (ran 𝐹 ⊆ 𝒫 ℝ ↔ ran 𝐹 ⊆ ℝ)
4240, 41sylib 210 . . . . . . . . . 10 (𝜑 ran 𝐹 ⊆ ℝ)
43 ovolcl 23643 . . . . . . . . . 10 ( ran 𝐹 ⊆ ℝ → (vol*‘ ran 𝐹) ∈ ℝ*)
4442, 43syl 17 . . . . . . . . 9 (𝜑 → (vol*‘ ran 𝐹) ∈ ℝ*)
45 ovolge0 23646 . . . . . . . . . 10 ( ran 𝐹 ⊆ ℝ → 0 ≤ (vol*‘ ran 𝐹))
4642, 45syl 17 . . . . . . . . 9 (𝜑 → 0 ≤ (vol*‘ ran 𝐹))
47 mnflt0 12244 . . . . . . . . . 10 -∞ < 0
48 mnfxr 10413 . . . . . . . . . . 11 -∞ ∈ ℝ*
49 0xr 10402 . . . . . . . . . . 11 0 ∈ ℝ*
50 xrltletr 12275 . . . . . . . . . . 11 ((-∞ ∈ ℝ* ∧ 0 ∈ ℝ* ∧ (vol*‘ ran 𝐹) ∈ ℝ*) → ((-∞ < 0 ∧ 0 ≤ (vol*‘ ran 𝐹)) → -∞ < (vol*‘ ran 𝐹)))
5148, 49, 50mp3an12 1581 . . . . . . . . . 10 ((vol*‘ ran 𝐹) ∈ ℝ* → ((-∞ < 0 ∧ 0 ≤ (vol*‘ ran 𝐹)) → -∞ < (vol*‘ ran 𝐹)))
5247, 51mpani 689 . . . . . . . . 9 ((vol*‘ ran 𝐹) ∈ ℝ* → (0 ≤ (vol*‘ ran 𝐹) → -∞ < (vol*‘ ran 𝐹)))
5344, 46, 52sylc 65 . . . . . . . 8 (𝜑 → -∞ < (vol*‘ ran 𝐹))
54 xrrebnd 12286 . . . . . . . . . 10 ((vol*‘ ran 𝐹) ∈ ℝ* → ((vol*‘ ran 𝐹) ∈ ℝ ↔ (-∞ < (vol*‘ ran 𝐹) ∧ (vol*‘ ran 𝐹) < +∞)))
5544, 54syl 17 . . . . . . . . 9 (𝜑 → ((vol*‘ ran 𝐹) ∈ ℝ ↔ (-∞ < (vol*‘ ran 𝐹) ∧ (vol*‘ ran 𝐹) < +∞)))
5636elpw2 5049 . . . . . . . . . . . 12 ( ran 𝐹 ∈ 𝒫 ℝ ↔ ran 𝐹 ⊆ ℝ)
5742, 56sylibr 226 . . . . . . . . . . 11 (𝜑 ran 𝐹 ∈ 𝒫 ℝ)
58 simpl 476 . . . . . . . . . . . . . . 15 ((𝑥 = ran 𝐹𝜑) → 𝑥 = ran 𝐹)
5958sseq1d 3856 . . . . . . . . . . . . . 14 ((𝑥 = ran 𝐹𝜑) → (𝑥 ⊆ ℝ ↔ ran 𝐹 ⊆ ℝ))
6058fveq2d 6436 . . . . . . . . . . . . . . . 16 ((𝑥 = ran 𝐹𝜑) → (vol*‘𝑥) = (vol*‘ ran 𝐹))
6160eleq1d 2890 . . . . . . . . . . . . . . 15 ((𝑥 = ran 𝐹𝜑) → ((vol*‘𝑥) ∈ ℝ ↔ (vol*‘ ran 𝐹) ∈ ℝ))
62 simpll 785 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 (((𝑥 = ran 𝐹𝜑) ∧ 𝑛 ∈ ℕ) → 𝑥 = ran 𝐹)
6362ineq1d 4039 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 (((𝑥 = ran 𝐹𝜑) ∧ 𝑛 ∈ ℕ) → (𝑥 ∩ (𝐹𝑛)) = ( ran 𝐹 ∩ (𝐹𝑛)))
64 fnfvelrn 6604 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33 ((𝐹 Fn ℕ ∧ 𝑛 ∈ ℕ) → (𝐹𝑛) ∈ ran 𝐹)
6521, 64sylan 577 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32 ((𝜑𝑛 ∈ ℕ) → (𝐹𝑛) ∈ ran 𝐹)
66 elssuni 4688 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32 ((𝐹𝑛) ∈ ran 𝐹 → (𝐹𝑛) ⊆ ran 𝐹)
6765, 66syl 17 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 ((𝜑𝑛 ∈ ℕ) → (𝐹𝑛) ⊆ ran 𝐹)
6867adantll 707 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 (((𝑥 = ran 𝐹𝜑) ∧ 𝑛 ∈ ℕ) → (𝐹𝑛) ⊆ ran 𝐹)
69 sseqin2 4043 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 ((𝐹𝑛) ⊆ ran 𝐹 ↔ ( ran 𝐹 ∩ (𝐹𝑛)) = (𝐹𝑛))
7068, 69sylib 210 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 (((𝑥 = ran 𝐹𝜑) ∧ 𝑛 ∈ ℕ) → ( ran 𝐹 ∩ (𝐹𝑛)) = (𝐹𝑛))
7163, 70eqtrd 2860 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28 (((𝑥 = ran 𝐹𝜑) ∧ 𝑛 ∈ ℕ) → (𝑥 ∩ (𝐹𝑛)) = (𝐹𝑛))
7271fveq2d 6436 . . . . . . . . . . . . . . . . . . . . . . . . . . 27 (((𝑥 = ran 𝐹𝜑) ∧ 𝑛 ∈ ℕ) → (vol*‘(𝑥 ∩ (𝐹𝑛))) = (vol*‘(𝐹𝑛)))
7313adantll 707 . . . . . . . . . . . . . . . . . . . . . . . . . . 27 (((𝑥 = ran 𝐹𝜑) ∧ 𝑛 ∈ ℕ) → (vol‘(𝐹𝑛)) = (vol*‘(𝐹𝑛)))
7472, 73eqtr4d 2863 . . . . . . . . . . . . . . . . . . . . . . . . . 26 (((𝑥 = ran 𝐹𝜑) ∧ 𝑛 ∈ ℕ) → (vol*‘(𝑥 ∩ (𝐹𝑛))) = (vol‘(𝐹𝑛)))
7574mpteq2dva 4966 . . . . . . . . . . . . . . . . . . . . . . . . 25 ((𝑥 = ran 𝐹𝜑) → (𝑛 ∈ ℕ ↦ (vol*‘(𝑥 ∩ (𝐹𝑛)))) = (𝑛 ∈ ℕ ↦ (vol‘(𝐹𝑛))))
7675adantrr 710 . . . . . . . . . . . . . . . . . . . . . . . 24 ((𝑥 = ran 𝐹 ∧ (𝜑𝑘 ∈ ℕ)) → (𝑛 ∈ ℕ ↦ (vol*‘(𝑥 ∩ (𝐹𝑛)))) = (𝑛 ∈ ℕ ↦ (vol‘(𝐹𝑛))))
7776, 3, 263eqtr4g 2885 . . . . . . . . . . . . . . . . . . . . . . 23 ((𝑥 = ran 𝐹 ∧ (𝜑𝑘 ∈ ℕ)) → 𝐻 = 𝐺)
7877seqeq3d 13102 . . . . . . . . . . . . . . . . . . . . . 22 ((𝑥 = ran 𝐹 ∧ (𝜑𝑘 ∈ ℕ)) → seq1( + , 𝐻) = seq1( + , 𝐺))
7978, 25syl6eqr 2878 . . . . . . . . . . . . . . . . . . . . 21 ((𝑥 = ran 𝐹 ∧ (𝜑𝑘 ∈ ℕ)) → seq1( + , 𝐻) = 𝑆)
8079fveq1d 6434 . . . . . . . . . . . . . . . . . . . 20 ((𝑥 = ran 𝐹 ∧ (𝜑𝑘 ∈ ℕ)) → (seq1( + , 𝐻)‘𝑘) = (𝑆𝑘))
81 difeq1 3947 . . . . . . . . . . . . . . . . . . . . . . . 24 (𝑥 = ran 𝐹 → (𝑥 ran 𝐹) = ( ran 𝐹 ran 𝐹))
82 difid 4177 . . . . . . . . . . . . . . . . . . . . . . . 24 ( ran 𝐹 ran 𝐹) = ∅
8381, 82syl6eq 2876 . . . . . . . . . . . . . . . . . . . . . . 23 (𝑥 = ran 𝐹 → (𝑥 ran 𝐹) = ∅)
8483fveq2d 6436 . . . . . . . . . . . . . . . . . . . . . 22 (𝑥 = ran 𝐹 → (vol*‘(𝑥 ran 𝐹)) = (vol*‘∅))
85 ovol0 23658 . . . . . . . . . . . . . . . . . . . . . 22 (vol*‘∅) = 0
8684, 85syl6eq 2876 . . . . . . . . . . . . . . . . . . . . 21 (𝑥 = ran 𝐹 → (vol*‘(𝑥 ran 𝐹)) = 0)
8786adantr 474 . . . . . . . . . . . . . . . . . . . 20 ((𝑥 = ran 𝐹 ∧ (𝜑𝑘 ∈ ℕ)) → (vol*‘(𝑥 ran 𝐹)) = 0)
8880, 87oveq12d 6922 . . . . . . . . . . . . . . . . . . 19 ((𝑥 = ran 𝐹 ∧ (𝜑𝑘 ∈ ℕ)) → ((seq1( + , 𝐻)‘𝑘) + (vol*‘(𝑥 ran 𝐹))) = ((𝑆𝑘) + 0))
89 nnuz 12004 . . . . . . . . . . . . . . . . . . . . . . . . 25 ℕ = (ℤ‘1)
90 1zzd 11735 . . . . . . . . . . . . . . . . . . . . . . . . 25 (𝜑 → 1 ∈ ℤ)
91 2fveq3 6437 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28 (𝑛 = 𝑘 → (vol‘(𝐹𝑛)) = (vol‘(𝐹𝑘)))
92 fvex 6445 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28 (vol‘(𝐹𝑘)) ∈ V
9391, 26, 92fvmpt 6528 . . . . . . . . . . . . . . . . . . . . . . . . . . 27 (𝑘 ∈ ℕ → (𝐺𝑘) = (vol‘(𝐹𝑘)))
9493adantl 475 . . . . . . . . . . . . . . . . . . . . . . . . . 26 ((𝜑𝑘 ∈ ℕ) → (𝐺𝑘) = (vol‘(𝐹𝑘)))
95 2fveq3 6437 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 (𝑖 = 𝑘 → (vol‘(𝐹𝑖)) = (vol‘(𝐹𝑘)))
9695eleq1d 2890 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28 (𝑖 = 𝑘 → ((vol‘(𝐹𝑖)) ∈ ℝ ↔ (vol‘(𝐹𝑘)) ∈ ℝ))
9796rspccva 3524 . . . . . . . . . . . . . . . . . . . . . . . . . . 27 ((∀𝑖 ∈ ℕ (vol‘(𝐹𝑖)) ∈ ℝ ∧ 𝑘 ∈ ℕ) → (vol‘(𝐹𝑘)) ∈ ℝ)
9814, 97sylan 577 . . . . . . . . . . . . . . . . . . . . . . . . . 26 ((𝜑𝑘 ∈ ℕ) → (vol‘(𝐹𝑘)) ∈ ℝ)
9994, 98eqeltrd 2905 . . . . . . . . . . . . . . . . . . . . . . . . 25 ((𝜑𝑘 ∈ ℕ) → (𝐺𝑘) ∈ ℝ)
10089, 90, 99serfre 13123 . . . . . . . . . . . . . . . . . . . . . . . 24 (𝜑 → seq1( + , 𝐺):ℕ⟶ℝ)
10125feq1i 6268 . . . . . . . . . . . . . . . . . . . . . . . 24 (𝑆:ℕ⟶ℝ ↔ seq1( + , 𝐺):ℕ⟶ℝ)
102100, 101sylibr 226 . . . . . . . . . . . . . . . . . . . . . . 23 (𝜑𝑆:ℕ⟶ℝ)
103102ffvelrnda 6607 . . . . . . . . . . . . . . . . . . . . . 22 ((𝜑𝑘 ∈ ℕ) → (𝑆𝑘) ∈ ℝ)
104103adantl 475 . . . . . . . . . . . . . . . . . . . . 21 ((𝑥 = ran 𝐹 ∧ (𝜑𝑘 ∈ ℕ)) → (𝑆𝑘) ∈ ℝ)
105104recnd 10384 . . . . . . . . . . . . . . . . . . . 20 ((𝑥 = ran 𝐹 ∧ (𝜑𝑘 ∈ ℕ)) → (𝑆𝑘) ∈ ℂ)
106105addid1d 10554 . . . . . . . . . . . . . . . . . . 19 ((𝑥 = ran 𝐹 ∧ (𝜑𝑘 ∈ ℕ)) → ((𝑆𝑘) + 0) = (𝑆𝑘))
10788, 106eqtrd 2860 . . . . . . . . . . . . . . . . . 18 ((𝑥 = ran 𝐹 ∧ (𝜑𝑘 ∈ ℕ)) → ((seq1( + , 𝐻)‘𝑘) + (vol*‘(𝑥 ran 𝐹))) = (𝑆𝑘))
108 fveq2 6432 . . . . . . . . . . . . . . . . . . 19 (𝑥 = ran 𝐹 → (vol*‘𝑥) = (vol*‘ ran 𝐹))
109108adantr 474 . . . . . . . . . . . . . . . . . 18 ((𝑥 = ran 𝐹 ∧ (𝜑𝑘 ∈ ℕ)) → (vol*‘𝑥) = (vol*‘ ran 𝐹))
110107, 109breq12d 4885 . . . . . . . . . . . . . . . . 17 ((𝑥 = ran 𝐹 ∧ (𝜑𝑘 ∈ ℕ)) → (((seq1( + , 𝐻)‘𝑘) + (vol*‘(𝑥 ran 𝐹))) ≤ (vol*‘𝑥) ↔ (𝑆𝑘) ≤ (vol*‘ ran 𝐹)))
111110expr 450 . . . . . . . . . . . . . . . 16 ((𝑥 = ran 𝐹𝜑) → (𝑘 ∈ ℕ → (((seq1( + , 𝐻)‘𝑘) + (vol*‘(𝑥 ran 𝐹))) ≤ (vol*‘𝑥) ↔ (𝑆𝑘) ≤ (vol*‘ ran 𝐹))))
112111pm5.74d 265 . . . . . . . . . . . . . . 15 ((𝑥 = ran 𝐹𝜑) → ((𝑘 ∈ ℕ → ((seq1( + , 𝐻)‘𝑘) + (vol*‘(𝑥 ran 𝐹))) ≤ (vol*‘𝑥)) ↔ (𝑘 ∈ ℕ → (𝑆𝑘) ≤ (vol*‘ ran 𝐹))))
11361, 112imbi12d 336 . . . . . . . . . . . . . 14 ((𝑥 = ran 𝐹𝜑) → (((vol*‘𝑥) ∈ ℝ → (𝑘 ∈ ℕ → ((seq1( + , 𝐻)‘𝑘) + (vol*‘(𝑥 ran 𝐹))) ≤ (vol*‘𝑥))) ↔ ((vol*‘ ran 𝐹) ∈ ℝ → (𝑘 ∈ ℕ → (𝑆𝑘) ≤ (vol*‘ ran 𝐹)))))
11459, 113imbi12d 336 . . . . . . . . . . . . 13 ((𝑥 = ran 𝐹𝜑) → ((𝑥 ⊆ ℝ → ((vol*‘𝑥) ∈ ℝ → (𝑘 ∈ ℕ → ((seq1( + , 𝐻)‘𝑘) + (vol*‘(𝑥 ran 𝐹))) ≤ (vol*‘𝑥)))) ↔ ( ran 𝐹 ⊆ ℝ → ((vol*‘ ran 𝐹) ∈ ℝ → (𝑘 ∈ ℕ → (𝑆𝑘) ≤ (vol*‘ ran 𝐹))))))
115114pm5.74da 840 . . . . . . . . . . . 12 (𝑥 = ran 𝐹 → ((𝜑 → (𝑥 ⊆ ℝ → ((vol*‘𝑥) ∈ ℝ → (𝑘 ∈ ℕ → ((seq1( + , 𝐻)‘𝑘) + (vol*‘(𝑥 ran 𝐹))) ≤ (vol*‘𝑥))))) ↔ (𝜑 → ( ran 𝐹 ⊆ ℝ → ((vol*‘ ran 𝐹) ∈ ℝ → (𝑘 ∈ ℕ → (𝑆𝑘) ≤ (vol*‘ ran 𝐹)))))))
11613ad2ant1 1169 . . . . . . . . . . . . . 14 ((𝜑𝑥 ⊆ ℝ ∧ (vol*‘𝑥) ∈ ℝ) → 𝐹:ℕ⟶dom vol)
11723ad2ant1 1169 . . . . . . . . . . . . . 14 ((𝜑𝑥 ⊆ ℝ ∧ (vol*‘𝑥) ∈ ℝ) → Disj 𝑖 ∈ ℕ (𝐹𝑖))
118 simp2 1173 . . . . . . . . . . . . . 14 ((𝜑𝑥 ⊆ ℝ ∧ (vol*‘𝑥) ∈ ℝ) → 𝑥 ⊆ ℝ)
119 simp3 1174 . . . . . . . . . . . . . 14 ((𝜑𝑥 ⊆ ℝ ∧ (vol*‘𝑥) ∈ ℝ) → (vol*‘𝑥) ∈ ℝ)
120116, 117, 3, 118, 119voliunlem1 23715 . . . . . . . . . . . . 13 (((𝜑𝑥 ⊆ ℝ ∧ (vol*‘𝑥) ∈ ℝ) ∧ 𝑘 ∈ ℕ) → ((seq1( + , 𝐻)‘𝑘) + (vol*‘(𝑥 ran 𝐹))) ≤ (vol*‘𝑥))
1211203exp1 1467 . . . . . . . . . . . 12 (𝜑 → (𝑥 ⊆ ℝ → ((vol*‘𝑥) ∈ ℝ → (𝑘 ∈ ℕ → ((seq1( + , 𝐻)‘𝑘) + (vol*‘(𝑥 ran 𝐹))) ≤ (vol*‘𝑥)))))
122115, 121vtoclg 3481 . . . . . . . . . . 11 ( ran 𝐹 ∈ 𝒫 ℝ → (𝜑 → ( ran 𝐹 ⊆ ℝ → ((vol*‘ ran 𝐹) ∈ ℝ → (𝑘 ∈ ℕ → (𝑆𝑘) ≤ (vol*‘ ran 𝐹))))))
12357, 122mpcom 38 . . . . . . . . . 10 (𝜑 → ( ran 𝐹 ⊆ ℝ → ((vol*‘ ran 𝐹) ∈ ℝ → (𝑘 ∈ ℕ → (𝑆𝑘) ≤ (vol*‘ ran 𝐹)))))
12442, 123mpd 15 . . . . . . . . 9 (𝜑 → ((vol*‘ ran 𝐹) ∈ ℝ → (𝑘 ∈ ℕ → (𝑆𝑘) ≤ (vol*‘ ran 𝐹))))
12555, 124sylbird 252 . . . . . . . 8 (𝜑 → ((-∞ < (vol*‘ ran 𝐹) ∧ (vol*‘ ran 𝐹) < +∞) → (𝑘 ∈ ℕ → (𝑆𝑘) ≤ (vol*‘ ran 𝐹))))
12653, 125mpand 688 . . . . . . 7 (𝜑 → ((vol*‘ ran 𝐹) < +∞ → (𝑘 ∈ ℕ → (𝑆𝑘) ≤ (vol*‘ ran 𝐹))))
127 nltpnft 12282 . . . . . . . . 9 ((vol*‘ ran 𝐹) ∈ ℝ* → ((vol*‘ ran 𝐹) = +∞ ↔ ¬ (vol*‘ ran 𝐹) < +∞))
12844, 127syl 17 . . . . . . . 8 (𝜑 → ((vol*‘ ran 𝐹) = +∞ ↔ ¬ (vol*‘ ran 𝐹) < +∞))
129 rexr 10401 . . . . . . . . . . 11 ((𝑆𝑘) ∈ ℝ → (𝑆𝑘) ∈ ℝ*)
130 pnfge 12249 . . . . . . . . . . 11 ((𝑆𝑘) ∈ ℝ* → (𝑆𝑘) ≤ +∞)
131103, 129, 1303syl 18 . . . . . . . . . 10 ((𝜑𝑘 ∈ ℕ) → (𝑆𝑘) ≤ +∞)
132131ex 403 . . . . . . . . 9 (𝜑 → (𝑘 ∈ ℕ → (𝑆𝑘) ≤ +∞))
133 breq2 4876 . . . . . . . . . 10 ((vol*‘ ran 𝐹) = +∞ → ((𝑆𝑘) ≤ (vol*‘ ran 𝐹) ↔ (𝑆𝑘) ≤ +∞))
134133imbi2d 332 . . . . . . . . 9 ((vol*‘ ran 𝐹) = +∞ → ((𝑘 ∈ ℕ → (𝑆𝑘) ≤ (vol*‘ ran 𝐹)) ↔ (𝑘 ∈ ℕ → (𝑆𝑘) ≤ +∞)))
135132, 134syl5ibrcom 239 . . . . . . . 8 (𝜑 → ((vol*‘ ran 𝐹) = +∞ → (𝑘 ∈ ℕ → (𝑆𝑘) ≤ (vol*‘ ran 𝐹))))
136128, 135sylbird 252 . . . . . . 7 (𝜑 → (¬ (vol*‘ ran 𝐹) < +∞ → (𝑘 ∈ ℕ → (𝑆𝑘) ≤ (vol*‘ ran 𝐹))))
137126, 136pm2.61d 172 . . . . . 6 (𝜑 → (𝑘 ∈ ℕ → (𝑆𝑘) ≤ (vol*‘ ran 𝐹)))
138137ralrimiv 3173 . . . . 5 (𝜑 → ∀𝑘 ∈ ℕ (𝑆𝑘) ≤ (vol*‘ ran 𝐹))
139102ffnd 6278 . . . . . 6 (𝜑𝑆 Fn ℕ)
140 breq1 4875 . . . . . . 7 (𝑧 = (𝑆𝑘) → (𝑧 ≤ (vol*‘ ran 𝐹) ↔ (𝑆𝑘) ≤ (vol*‘ ran 𝐹)))
141140ralrn 6610 . . . . . 6 (𝑆 Fn ℕ → (∀𝑧 ∈ ran 𝑆 𝑧 ≤ (vol*‘ ran 𝐹) ↔ ∀𝑘 ∈ ℕ (𝑆𝑘) ≤ (vol*‘ ran 𝐹)))
142139, 141syl 17 . . . . 5 (𝜑 → (∀𝑧 ∈ ran 𝑆 𝑧 ≤ (vol*‘ ran 𝐹) ↔ ∀𝑘 ∈ ℕ (𝑆𝑘) ≤ (vol*‘ ran 𝐹)))
143138, 142mpbird 249 . . . 4 (𝜑 → ∀𝑧 ∈ ran 𝑆 𝑧 ≤ (vol*‘ ran 𝐹))
144102frnd 6284 . . . . . 6 (𝜑 → ran 𝑆 ⊆ ℝ)
145 ressxr 10399 . . . . . 6 ℝ ⊆ ℝ*
146144, 145syl6ss 3838 . . . . 5 (𝜑 → ran 𝑆 ⊆ ℝ*)
147 supxrleub 12443 . . . . 5 ((ran 𝑆 ⊆ ℝ* ∧ (vol*‘ ran 𝐹) ∈ ℝ*) → (sup(ran 𝑆, ℝ*, < ) ≤ (vol*‘ ran 𝐹) ↔ ∀𝑧 ∈ ran 𝑆 𝑧 ≤ (vol*‘ ran 𝐹)))
148146, 44, 147syl2anc 581 . . . 4 (𝜑 → (sup(ran 𝑆, ℝ*, < ) ≤ (vol*‘ ran 𝐹) ↔ ∀𝑧 ∈ ran 𝑆 𝑧 ≤ (vol*‘ ran 𝐹)))
149143, 148mpbird 249 . . 3 (𝜑 → sup(ran 𝑆, ℝ*, < ) ≤ (vol*‘ ran 𝐹))
150 supxrcl 12432 . . . . 5 (ran 𝑆 ⊆ ℝ* → sup(ran 𝑆, ℝ*, < ) ∈ ℝ*)
151146, 150syl 17 . . . 4 (𝜑 → sup(ran 𝑆, ℝ*, < ) ∈ ℝ*)
152 xrletri3 12272 . . . 4 (((vol*‘ ran 𝐹) ∈ ℝ* ∧ sup(ran 𝑆, ℝ*, < ) ∈ ℝ*) → ((vol*‘ ran 𝐹) = sup(ran 𝑆, ℝ*, < ) ↔ ((vol*‘ ran 𝐹) ≤ sup(ran 𝑆, ℝ*, < ) ∧ sup(ran 𝑆, ℝ*, < ) ≤ (vol*‘ ran 𝐹))))
15344, 151, 152syl2anc 581 . . 3 (𝜑 → ((vol*‘ ran 𝐹) = sup(ran 𝑆, ℝ*, < ) ↔ ((vol*‘ ran 𝐹) ≤ sup(ran 𝑆, ℝ*, < ) ∧ sup(ran 𝑆, ℝ*, < ) ≤ (vol*‘ ran 𝐹))))
15433, 149, 153mpbir2and 706 . 2 (𝜑 → (vol*‘ ran 𝐹) = sup(ran 𝑆, ℝ*, < ))
1556, 154eqtrd 2860 1 (𝜑 → (vol‘ ran 𝐹) = sup(ran 𝑆, ℝ*, < ))
 Colors of variables: wff setvar class Syntax hints:  ¬ wn 3   → wi 4   ↔ wb 198   ∧ wa 386   ∧ w3a 1113   = wceq 1658   ∈ wcel 2166  ∀wral 3116   ∖ cdif 3794   ∩ cin 3796   ⊆ wss 3797  ∅c0 4143  𝒫 cpw 4377  ∪ cuni 4657  ∪ ciun 4739  Disj wdisj 4840   class class class wbr 4872   ↦ cmpt 4951  dom cdm 5341  ran crn 5342   Fn wfn 6117  ⟶wf 6118  ‘cfv 6122  (class class class)co 6904  supcsup 8614  ℝcr 10250  0cc0 10251  1c1 10252   + caddc 10254  +∞cpnf 10387  -∞cmnf 10388  ℝ*cxr 10389   < clt 10390   ≤ cle 10391  ℕcn 11349  seqcseq 13094  vol*covol 23627  volcvol 23628 This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1896  ax-4 1910  ax-5 2011  ax-6 2077  ax-7 2114  ax-8 2168  ax-9 2175  ax-10 2194  ax-11 2209  ax-12 2222  ax-13 2390  ax-ext 2802  ax-rep 4993  ax-sep 5004  ax-nul 5012  ax-pow 5064  ax-pr 5126  ax-un 7208  ax-inf2 8814  ax-cc 9571  ax-cnex 10307  ax-resscn 10308  ax-1cn 10309  ax-icn 10310  ax-addcl 10311  ax-addrcl 10312  ax-mulcl 10313  ax-mulrcl 10314  ax-mulcom 10315  ax-addass 10316  ax-mulass 10317  ax-distr 10318  ax-i2m1 10319  ax-1ne0 10320  ax-1rid 10321  ax-rnegex 10322  ax-rrecex 10323  ax-cnre 10324  ax-pre-lttri 10325  ax-pre-lttrn 10326  ax-pre-ltadd 10327  ax-pre-mulgt0 10328  ax-pre-sup 10329 This theorem depends on definitions:  df-bi 199  df-an 387  df-or 881  df-3or 1114  df-3an 1115  df-tru 1662  df-fal 1672  df-ex 1881  df-nf 1885  df-sb 2070  df-mo 2604  df-eu 2639  df-clab 2811  df-cleq 2817  df-clel 2820  df-nfc 2957  df-ne 2999  df-nel 3102  df-ral 3121  df-rex 3122  df-reu 3123  df-rmo 3124  df-rab 3125  df-v 3415  df-sbc 3662  df-csb 3757  df-dif 3800  df-un 3802  df-in 3804  df-ss 3811  df-pss 3813  df-nul 4144  df-if 4306  df-pw 4379  df-sn 4397  df-pr 4399  df-tp 4401  df-op 4403  df-uni 4658  df-int 4697  df-iun 4741  df-disj 4841  df-br 4873  df-opab 4935  df-mpt 4952  df-tr 4975  df-id 5249  df-eprel 5254  df-po 5262  df-so 5263  df-fr 5300  df-se 5301  df-we 5302  df-xp 5347  df-rel 5348  df-cnv 5349  df-co 5350  df-dm 5351  df-rn 5352  df-res 5353  df-ima 5354  df-pred 5919  df-ord 5965  df-on 5966  df-lim 5967  df-suc 5968  df-iota 6085  df-fun 6124  df-fn 6125  df-f 6126  df-f1 6127  df-fo 6128  df-f1o 6129  df-fv 6130  df-isom 6131  df-riota 6865  df-ov 6907  df-oprab 6908  df-mpt2 6909  df-of 7156  df-om 7326  df-1st 7427  df-2nd 7428  df-wrecs 7671  df-recs 7733  df-rdg 7771  df-1o 7825  df-2o 7826  df-oadd 7829  df-er 8008  df-map 8123  df-pm 8124  df-en 8222  df-dom 8223  df-sdom 8224  df-fin 8225  df-sup 8616  df-inf 8617  df-oi 8683  df-card 9077  df-cda 9304  df-pnf 10392  df-mnf 10393  df-xr 10394  df-ltxr 10395  df-le 10396  df-sub 10586  df-neg 10587  df-div 11009  df-nn 11350  df-2 11413  df-3 11414  df-n0 11618  df-z 11704  df-uz 11968  df-q 12071  df-rp 12112  df-xadd 12232  df-ioo 12466  df-ico 12468  df-icc 12469  df-fz 12619  df-fzo 12760  df-fl 12887  df-seq 13095  df-exp 13154  df-hash 13410  df-cj 14215  df-re 14216  df-im 14217  df-sqrt 14351  df-abs 14352  df-clim 14595  df-rlim 14596  df-sum 14793  df-xmet 20098  df-met 20099  df-ovol 23629  df-vol 23630 This theorem is referenced by:  voliun  23719
 Copyright terms: Public domain W3C validator