volsup - Metamath Proof Explorer

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

Theorem volsup 24720

Description: The volume of the limit of an increasing sequence of measurable sets is the limit of the volumes. (Contributed by Mario Carneiro, 14-Aug-2014.) (Revised by Mario Carneiro, 11-Dec-2016.)

**Assertion**
Ref	Expression
volsup	⊢ ((𝐹:ℕ⟶dom vol ∧ ∀𝑛 ∈ ℕ (𝐹‘𝑛) ⊆ (𝐹‘(𝑛 + 1))) → (vol‘∪ ran 𝐹) = sup((vol “ ran 𝐹), ℝ^*, < ))

Distinct variable group: 𝑛,𝐹

Proof of Theorem volsup Dummy variables 𝑗 𝑘 𝑚 𝑥 are mutually distinct and distinct from all other variables.

Step	Hyp	Ref	Expression
1		ffvelrn 6959	. . . . . . . . . . 11 ⊢ ((𝐹:ℕ⟶dom vol ∧ 𝑘 ∈ ℕ) → (𝐹‘𝑘) ∈ dom vol)
2	1	ad2ant2r 744	. . . . . . . . . 10 ⊢ (((𝐹:ℕ⟶dom vol ∧ ∀𝑛 ∈ ℕ (𝐹‘𝑛) ⊆ (𝐹‘(𝑛 + 1))) ∧ (𝑘 ∈ ℕ ∧ (vol‘(𝐹‘𝑘)) ∈ ℝ)) → (𝐹‘𝑘) ∈ dom vol)
3		fzofi 13694	. . . . . . . . . . 11 ⊢ (1..^𝑘) ∈ Fin
4		simpll 764	. . . . . . . . . . . . 13 ⊢ (((𝐹:ℕ⟶dom vol ∧ ∀𝑛 ∈ ℕ (𝐹‘𝑛) ⊆ (𝐹‘(𝑛 + 1))) ∧ (𝑘 ∈ ℕ ∧ (vol‘(𝐹‘𝑘)) ∈ ℝ)) → 𝐹:ℕ⟶dom vol)
5		elfzouz 13391	. . . . . . . . . . . . . 14 ⊢ (𝑚 ∈ (1..^𝑘) → 𝑚 ∈ (ℤ_≥‘1))
6		nnuz 12621	. . . . . . . . . . . . . 14 ⊢ ℕ = (ℤ_≥‘1)
7	5, 6	eleqtrrdi 2850	. . . . . . . . . . . . 13 ⊢ (𝑚 ∈ (1..^𝑘) → 𝑚 ∈ ℕ)
8		ffvelrn 6959	. . . . . . . . . . . . 13 ⊢ ((𝐹:ℕ⟶dom vol ∧ 𝑚 ∈ ℕ) → (𝐹‘𝑚) ∈ dom vol)
9	4, 7, 8	syl2an 596	. . . . . . . . . . . 12 ⊢ ((((𝐹:ℕ⟶dom vol ∧ ∀𝑛 ∈ ℕ (𝐹‘𝑛) ⊆ (𝐹‘(𝑛 + 1))) ∧ (𝑘 ∈ ℕ ∧ (vol‘(𝐹‘𝑘)) ∈ ℝ)) ∧ 𝑚 ∈ (1..^𝑘)) → (𝐹‘𝑚) ∈ dom vol)
10	9	ralrimiva 3103	. . . . . . . . . . 11 ⊢ (((𝐹:ℕ⟶dom vol ∧ ∀𝑛 ∈ ℕ (𝐹‘𝑛) ⊆ (𝐹‘(𝑛 + 1))) ∧ (𝑘 ∈ ℕ ∧ (vol‘(𝐹‘𝑘)) ∈ ℝ)) → ∀𝑚 ∈ (1..^𝑘)(𝐹‘𝑚) ∈ dom vol)
11		finiunmbl 24708	. . . . . . . . . . 11 ⊢ (((1..^𝑘) ∈ Fin ∧ ∀𝑚 ∈ (1..^𝑘)(𝐹‘𝑚) ∈ dom vol) → ∪ 𝑚 ∈ (1..^𝑘)(𝐹‘𝑚) ∈ dom vol)
12	3, 10, 11	sylancr 587	. . . . . . . . . 10 ⊢ (((𝐹:ℕ⟶dom vol ∧ ∀𝑛 ∈ ℕ (𝐹‘𝑛) ⊆ (𝐹‘(𝑛 + 1))) ∧ (𝑘 ∈ ℕ ∧ (vol‘(𝐹‘𝑘)) ∈ ℝ)) → ∪ 𝑚 ∈ (1..^𝑘)(𝐹‘𝑚) ∈ dom vol)
13		difmbl 24707	. . . . . . . . . 10 ⊢ (((𝐹‘𝑘) ∈ dom vol ∧ ∪ 𝑚 ∈ (1..^𝑘)(𝐹‘𝑚) ∈ dom vol) → ((𝐹‘𝑘) ∖ ∪ 𝑚 ∈ (1..^𝑘)(𝐹‘𝑚)) ∈ dom vol)
14	2, 12, 13	syl2anc 584	. . . . . . . . 9 ⊢ (((𝐹:ℕ⟶dom vol ∧ ∀𝑛 ∈ ℕ (𝐹‘𝑛) ⊆ (𝐹‘(𝑛 + 1))) ∧ (𝑘 ∈ ℕ ∧ (vol‘(𝐹‘𝑘)) ∈ ℝ)) → ((𝐹‘𝑘) ∖ ∪ 𝑚 ∈ (1..^𝑘)(𝐹‘𝑚)) ∈ dom vol)
15		mblvol 24694	. . . . . . . . . . 11 ⊢ (((𝐹‘𝑘) ∖ ∪ 𝑚 ∈ (1..^𝑘)(𝐹‘𝑚)) ∈ dom vol → (vol‘((𝐹‘𝑘) ∖ ∪ 𝑚 ∈ (1..^𝑘)(𝐹‘𝑚))) = (vol*‘((𝐹‘𝑘) ∖ ∪ 𝑚 ∈ (1..^𝑘)(𝐹‘𝑚))))
16	14, 15	syl 17	. . . . . . . . . 10 ⊢ (((𝐹:ℕ⟶dom vol ∧ ∀𝑛 ∈ ℕ (𝐹‘𝑛) ⊆ (𝐹‘(𝑛 + 1))) ∧ (𝑘 ∈ ℕ ∧ (vol‘(𝐹‘𝑘)) ∈ ℝ)) → (vol‘((𝐹‘𝑘) ∖ ∪ 𝑚 ∈ (1..^𝑘)(𝐹‘𝑚))) = (vol*‘((𝐹‘𝑘) ∖ ∪ 𝑚 ∈ (1..^𝑘)(𝐹‘𝑚))))
17		difssd 4067	. . . . . . . . . . 11 ⊢ (((𝐹:ℕ⟶dom vol ∧ ∀𝑛 ∈ ℕ (𝐹‘𝑛) ⊆ (𝐹‘(𝑛 + 1))) ∧ (𝑘 ∈ ℕ ∧ (vol‘(𝐹‘𝑘)) ∈ ℝ)) → ((𝐹‘𝑘) ∖ ∪ 𝑚 ∈ (1..^𝑘)(𝐹‘𝑚)) ⊆ (𝐹‘𝑘))
18		mblss 24695	. . . . . . . . . . . 12 ⊢ ((𝐹‘𝑘) ∈ dom vol → (𝐹‘𝑘) ⊆ ℝ)
19	2, 18	syl 17	. . . . . . . . . . 11 ⊢ (((𝐹:ℕ⟶dom vol ∧ ∀𝑛 ∈ ℕ (𝐹‘𝑛) ⊆ (𝐹‘(𝑛 + 1))) ∧ (𝑘 ∈ ℕ ∧ (vol‘(𝐹‘𝑘)) ∈ ℝ)) → (𝐹‘𝑘) ⊆ ℝ)
20		mblvol 24694	. . . . . . . . . . . . 13 ⊢ ((𝐹‘𝑘) ∈ dom vol → (vol‘(𝐹‘𝑘)) = (vol*‘(𝐹‘𝑘)))
21	2, 20	syl 17	. . . . . . . . . . . 12 ⊢ (((𝐹:ℕ⟶dom vol ∧ ∀𝑛 ∈ ℕ (𝐹‘𝑛) ⊆ (𝐹‘(𝑛 + 1))) ∧ (𝑘 ∈ ℕ ∧ (vol‘(𝐹‘𝑘)) ∈ ℝ)) → (vol‘(𝐹‘𝑘)) = (vol*‘(𝐹‘𝑘)))
22		simprr 770	. . . . . . . . . . . 12 ⊢ (((𝐹:ℕ⟶dom vol ∧ ∀𝑛 ∈ ℕ (𝐹‘𝑛) ⊆ (𝐹‘(𝑛 + 1))) ∧ (𝑘 ∈ ℕ ∧ (vol‘(𝐹‘𝑘)) ∈ ℝ)) → (vol‘(𝐹‘𝑘)) ∈ ℝ)
23	21, 22	eqeltrrd 2840	. . . . . . . . . . 11 ⊢ (((𝐹:ℕ⟶dom vol ∧ ∀𝑛 ∈ ℕ (𝐹‘𝑛) ⊆ (𝐹‘(𝑛 + 1))) ∧ (𝑘 ∈ ℕ ∧ (vol‘(𝐹‘𝑘)) ∈ ℝ)) → (vol*‘(𝐹‘𝑘)) ∈ ℝ)
24		ovolsscl 24650	. . . . . . . . . . 11 ⊢ ((((𝐹‘𝑘) ∖ ∪ 𝑚 ∈ (1..^𝑘)(𝐹‘𝑚)) ⊆ (𝐹‘𝑘) ∧ (𝐹‘𝑘) ⊆ ℝ ∧ (vol‘(𝐹‘𝑘)) ∈ ℝ) → (vol‘((𝐹‘𝑘) ∖ ∪ 𝑚 ∈ (1..^𝑘)(𝐹‘𝑚))) ∈ ℝ)
25	17, 19, 23, 24	syl3anc 1370	. . . . . . . . . 10 ⊢ (((𝐹:ℕ⟶dom vol ∧ ∀𝑛 ∈ ℕ (𝐹‘𝑛) ⊆ (𝐹‘(𝑛 + 1))) ∧ (𝑘 ∈ ℕ ∧ (vol‘(𝐹‘𝑘)) ∈ ℝ)) → (vol*‘((𝐹‘𝑘) ∖ ∪ 𝑚 ∈ (1..^𝑘)(𝐹‘𝑚))) ∈ ℝ)
26	16, 25	eqeltrd 2839	. . . . . . . . 9 ⊢ (((𝐹:ℕ⟶dom vol ∧ ∀𝑛 ∈ ℕ (𝐹‘𝑛) ⊆ (𝐹‘(𝑛 + 1))) ∧ (𝑘 ∈ ℕ ∧ (vol‘(𝐹‘𝑘)) ∈ ℝ)) → (vol‘((𝐹‘𝑘) ∖ ∪ 𝑚 ∈ (1..^𝑘)(𝐹‘𝑚))) ∈ ℝ)
27	14, 26	jca 512	. . . . . . . 8 ⊢ (((𝐹:ℕ⟶dom vol ∧ ∀𝑛 ∈ ℕ (𝐹‘𝑛) ⊆ (𝐹‘(𝑛 + 1))) ∧ (𝑘 ∈ ℕ ∧ (vol‘(𝐹‘𝑘)) ∈ ℝ)) → (((𝐹‘𝑘) ∖ ∪ 𝑚 ∈ (1..^𝑘)(𝐹‘𝑚)) ∈ dom vol ∧ (vol‘((𝐹‘𝑘) ∖ ∪ 𝑚 ∈ (1..^𝑘)(𝐹‘𝑚))) ∈ ℝ))
28	27	expr 457	. . . . . . 7 ⊢ (((𝐹:ℕ⟶dom vol ∧ ∀𝑛 ∈ ℕ (𝐹‘𝑛) ⊆ (𝐹‘(𝑛 + 1))) ∧ 𝑘 ∈ ℕ) → ((vol‘(𝐹‘𝑘)) ∈ ℝ → (((𝐹‘𝑘) ∖ ∪ 𝑚 ∈ (1..^𝑘)(𝐹‘𝑚)) ∈ dom vol ∧ (vol‘((𝐹‘𝑘) ∖ ∪ 𝑚 ∈ (1..^𝑘)(𝐹‘𝑚))) ∈ ℝ)))
29	28	ralimdva 3108	. . . . . 6 ⊢ ((𝐹:ℕ⟶dom vol ∧ ∀𝑛 ∈ ℕ (𝐹‘𝑛) ⊆ (𝐹‘(𝑛 + 1))) → (∀𝑘 ∈ ℕ (vol‘(𝐹‘𝑘)) ∈ ℝ → ∀𝑘 ∈ ℕ (((𝐹‘𝑘) ∖ ∪ 𝑚 ∈ (1..^𝑘)(𝐹‘𝑚)) ∈ dom vol ∧ (vol‘((𝐹‘𝑘) ∖ ∪ 𝑚 ∈ (1..^𝑘)(𝐹‘𝑚))) ∈ ℝ)))
30	29	imp 407	. . . . 5 ⊢ (((𝐹:ℕ⟶dom vol ∧ ∀𝑛 ∈ ℕ (𝐹‘𝑛) ⊆ (𝐹‘(𝑛 + 1))) ∧ ∀𝑘 ∈ ℕ (vol‘(𝐹‘𝑘)) ∈ ℝ) → ∀𝑘 ∈ ℕ (((𝐹‘𝑘) ∖ ∪ 𝑚 ∈ (1..^𝑘)(𝐹‘𝑚)) ∈ dom vol ∧ (vol‘((𝐹‘𝑘) ∖ ∪ 𝑚 ∈ (1..^𝑘)(𝐹‘𝑚))) ∈ ℝ))
31		fveq2 6774	. . . . . 6 ⊢ (𝑘 = 𝑚 → (𝐹‘𝑘) = (𝐹‘𝑚))
32	31	iundisj2 24713	. . . . 5 ⊢ Disj 𝑘 ∈ ℕ ((𝐹‘𝑘) ∖ ∪ 𝑚 ∈ (1..^𝑘)(𝐹‘𝑚))
33		eqid 2738	. . . . . 6 ⊢ seq1( + , (𝑘 ∈ ℕ ↦ (vol‘((𝐹‘𝑘) ∖ ∪ 𝑚 ∈ (1..^𝑘)(𝐹‘𝑚))))) = seq1( + , (𝑘 ∈ ℕ ↦ (vol‘((𝐹‘𝑘) ∖ ∪ 𝑚 ∈ (1..^𝑘)(𝐹‘𝑚)))))
34		eqid 2738	. . . . . 6 ⊢ (𝑘 ∈ ℕ ↦ (vol‘((𝐹‘𝑘) ∖ ∪ 𝑚 ∈ (1..^𝑘)(𝐹‘𝑚)))) = (𝑘 ∈ ℕ ↦ (vol‘((𝐹‘𝑘) ∖ ∪ 𝑚 ∈ (1..^𝑘)(𝐹‘𝑚))))
35	33, 34	voliun 24718	. . . . 5 ⊢ ((∀𝑘 ∈ ℕ (((𝐹‘𝑘) ∖ ∪ 𝑚 ∈ (1..^𝑘)(𝐹‘𝑚)) ∈ dom vol ∧ (vol‘((𝐹‘𝑘) ∖ ∪ 𝑚 ∈ (1..^𝑘)(𝐹‘𝑚))) ∈ ℝ) ∧ Disj 𝑘 ∈ ℕ ((𝐹‘𝑘) ∖ ∪ 𝑚 ∈ (1..^𝑘)(𝐹‘𝑚))) → (vol‘∪ 𝑘 ∈ ℕ ((𝐹‘𝑘) ∖ ∪ 𝑚 ∈ (1..^𝑘)(𝐹‘𝑚))) = sup(ran seq1( + , (𝑘 ∈ ℕ ↦ (vol‘((𝐹‘𝑘) ∖ ∪ 𝑚 ∈ (1..^𝑘)(𝐹‘𝑚))))), ℝ^*, < ))
36	30, 32, 35	sylancl 586	. . . 4 ⊢ (((𝐹:ℕ⟶dom vol ∧ ∀𝑛 ∈ ℕ (𝐹‘𝑛) ⊆ (𝐹‘(𝑛 + 1))) ∧ ∀𝑘 ∈ ℕ (vol‘(𝐹‘𝑘)) ∈ ℝ) → (vol‘∪ 𝑘 ∈ ℕ ((𝐹‘𝑘) ∖ ∪ 𝑚 ∈ (1..^𝑘)(𝐹‘𝑚))) = sup(ran seq1( + , (𝑘 ∈ ℕ ↦ (vol‘((𝐹‘𝑘) ∖ ∪ 𝑚 ∈ (1..^𝑘)(𝐹‘𝑚))))), ℝ^*, < ))
37	31	iundisj 24712	. . . . . 6 ⊢ ∪ 𝑘 ∈ ℕ (𝐹‘𝑘) = ∪ 𝑘 ∈ ℕ ((𝐹‘𝑘) ∖ ∪ 𝑚 ∈ (1..^𝑘)(𝐹‘𝑚))
38		ffn 6600	. . . . . . . 8 ⊢ (𝐹:ℕ⟶dom vol → 𝐹 Fn ℕ)
39	38	ad2antrr 723	. . . . . . 7 ⊢ (((𝐹:ℕ⟶dom vol ∧ ∀𝑛 ∈ ℕ (𝐹‘𝑛) ⊆ (𝐹‘(𝑛 + 1))) ∧ ∀𝑘 ∈ ℕ (vol‘(𝐹‘𝑘)) ∈ ℝ) → 𝐹 Fn ℕ)
40		fniunfv 7120	. . . . . . 7 ⊢ (𝐹 Fn ℕ → ∪ 𝑘 ∈ ℕ (𝐹‘𝑘) = ∪ ran 𝐹)
41	39, 40	syl 17	. . . . . 6 ⊢ (((𝐹:ℕ⟶dom vol ∧ ∀𝑛 ∈ ℕ (𝐹‘𝑛) ⊆ (𝐹‘(𝑛 + 1))) ∧ ∀𝑘 ∈ ℕ (vol‘(𝐹‘𝑘)) ∈ ℝ) → ∪ 𝑘 ∈ ℕ (𝐹‘𝑘) = ∪ ran 𝐹)
42	37, 41	eqtr3id 2792	. . . . 5 ⊢ (((𝐹:ℕ⟶dom vol ∧ ∀𝑛 ∈ ℕ (𝐹‘𝑛) ⊆ (𝐹‘(𝑛 + 1))) ∧ ∀𝑘 ∈ ℕ (vol‘(𝐹‘𝑘)) ∈ ℝ) → ∪ 𝑘 ∈ ℕ ((𝐹‘𝑘) ∖ ∪ 𝑚 ∈ (1..^𝑘)(𝐹‘𝑚)) = ∪ ran 𝐹)
43	42	fveq2d 6778	. . . 4 ⊢ (((𝐹:ℕ⟶dom vol ∧ ∀𝑛 ∈ ℕ (𝐹‘𝑛) ⊆ (𝐹‘(𝑛 + 1))) ∧ ∀𝑘 ∈ ℕ (vol‘(𝐹‘𝑘)) ∈ ℝ) → (vol‘∪ 𝑘 ∈ ℕ ((𝐹‘𝑘) ∖ ∪ 𝑚 ∈ (1..^𝑘)(𝐹‘𝑚))) = (vol‘∪ ran 𝐹))
44		1z 12350	. . . . . . . . . . 11 ⊢ 1 ∈ ℤ
45		seqfn 13733	. . . . . . . . . . 11 ⊢ (1 ∈ ℤ → seq1( + , (𝑘 ∈ ℕ ↦ (vol‘((𝐹‘𝑘) ∖ ∪ 𝑚 ∈ (1..^𝑘)(𝐹‘𝑚))))) Fn (ℤ_≥‘1))
46	44, 45	ax-mp 5	. . . . . . . . . 10 ⊢ seq1( + , (𝑘 ∈ ℕ ↦ (vol‘((𝐹‘𝑘) ∖ ∪ 𝑚 ∈ (1..^𝑘)(𝐹‘𝑚))))) Fn (ℤ_≥‘1)
47	6	fneq2i 6531	. . . . . . . . . 10 ⊢ (seq1( + , (𝑘 ∈ ℕ ↦ (vol‘((𝐹‘𝑘) ∖ ∪ 𝑚 ∈ (1..^𝑘)(𝐹‘𝑚))))) Fn ℕ ↔ seq1( + , (𝑘 ∈ ℕ ↦ (vol‘((𝐹‘𝑘) ∖ ∪ 𝑚 ∈ (1..^𝑘)(𝐹‘𝑚))))) Fn (ℤ_≥‘1))
48	46, 47	mpbir 230	. . . . . . . . 9 ⊢ seq1( + , (𝑘 ∈ ℕ ↦ (vol‘((𝐹‘𝑘) ∖ ∪ 𝑚 ∈ (1..^𝑘)(𝐹‘𝑚))))) Fn ℕ
49	48	a1i 11	. . . . . . . 8 ⊢ (((𝐹:ℕ⟶dom vol ∧ ∀𝑛 ∈ ℕ (𝐹‘𝑛) ⊆ (𝐹‘(𝑛 + 1))) ∧ ∀𝑘 ∈ ℕ (vol‘(𝐹‘𝑘)) ∈ ℝ) → seq1( + , (𝑘 ∈ ℕ ↦ (vol‘((𝐹‘𝑘) ∖ ∪ 𝑚 ∈ (1..^𝑘)(𝐹‘𝑚))))) Fn ℕ)
50		volf 24693	. . . . . . . . . 10 ⊢ vol:dom vol⟶(0[,]+∞)
51		simpll 764	. . . . . . . . . 10 ⊢ (((𝐹:ℕ⟶dom vol ∧ ∀𝑛 ∈ ℕ (𝐹‘𝑛) ⊆ (𝐹‘(𝑛 + 1))) ∧ ∀𝑘 ∈ ℕ (vol‘(𝐹‘𝑘)) ∈ ℝ) → 𝐹:ℕ⟶dom vol)
52		fco 6624	. . . . . . . . . 10 ⊢ ((vol:dom vol⟶(0[,]+∞) ∧ 𝐹:ℕ⟶dom vol) → (vol ∘ 𝐹):ℕ⟶(0[,]+∞))
53	50, 51, 52	sylancr 587	. . . . . . . . 9 ⊢ (((𝐹:ℕ⟶dom vol ∧ ∀𝑛 ∈ ℕ (𝐹‘𝑛) ⊆ (𝐹‘(𝑛 + 1))) ∧ ∀𝑘 ∈ ℕ (vol‘(𝐹‘𝑘)) ∈ ℝ) → (vol ∘ 𝐹):ℕ⟶(0[,]+∞))
54	53	ffnd 6601	. . . . . . . 8 ⊢ (((𝐹:ℕ⟶dom vol ∧ ∀𝑛 ∈ ℕ (𝐹‘𝑛) ⊆ (𝐹‘(𝑛 + 1))) ∧ ∀𝑘 ∈ ℕ (vol‘(𝐹‘𝑘)) ∈ ℝ) → (vol ∘ 𝐹) Fn ℕ)
55		fveq2 6774	. . . . . . . . . . . . 13 ⊢ (𝑥 = 1 → (seq1( + , (𝑘 ∈ ℕ ↦ (vol‘((𝐹‘𝑘) ∖ ∪ 𝑚 ∈ (1..^𝑘)(𝐹‘𝑚)))))‘𝑥) = (seq1( + , (𝑘 ∈ ℕ ↦ (vol‘((𝐹‘𝑘) ∖ ∪ 𝑚 ∈ (1..^𝑘)(𝐹‘𝑚)))))‘1))
56		2fveq3 6779	. . . . . . . . . . . . 13 ⊢ (𝑥 = 1 → (vol‘(𝐹‘𝑥)) = (vol‘(𝐹‘1)))
57	55, 56	eqeq12d 2754	. . . . . . . . . . . 12 ⊢ (𝑥 = 1 → ((seq1( + , (𝑘 ∈ ℕ ↦ (vol‘((𝐹‘𝑘) ∖ ∪ 𝑚 ∈ (1..^𝑘)(𝐹‘𝑚)))))‘𝑥) = (vol‘(𝐹‘𝑥)) ↔ (seq1( + , (𝑘 ∈ ℕ ↦ (vol‘((𝐹‘𝑘) ∖ ∪ 𝑚 ∈ (1..^𝑘)(𝐹‘𝑚)))))‘1) = (vol‘(𝐹‘1))))
58	57	imbi2d 341	. . . . . . . . . . 11 ⊢ (𝑥 = 1 → ((((𝐹:ℕ⟶dom vol ∧ ∀𝑛 ∈ ℕ (𝐹‘𝑛) ⊆ (𝐹‘(𝑛 + 1))) ∧ ∀𝑘 ∈ ℕ (vol‘(𝐹‘𝑘)) ∈ ℝ) → (seq1( + , (𝑘 ∈ ℕ ↦ (vol‘((𝐹‘𝑘) ∖ ∪ 𝑚 ∈ (1..^𝑘)(𝐹‘𝑚)))))‘𝑥) = (vol‘(𝐹‘𝑥))) ↔ (((𝐹:ℕ⟶dom vol ∧ ∀𝑛 ∈ ℕ (𝐹‘𝑛) ⊆ (𝐹‘(𝑛 + 1))) ∧ ∀𝑘 ∈ ℕ (vol‘(𝐹‘𝑘)) ∈ ℝ) → (seq1( + , (𝑘 ∈ ℕ ↦ (vol‘((𝐹‘𝑘) ∖ ∪ 𝑚 ∈ (1..^𝑘)(𝐹‘𝑚)))))‘1) = (vol‘(𝐹‘1)))))
59		fveq2 6774	. . . . . . . . . . . . 13 ⊢ (𝑥 = 𝑗 → (seq1( + , (𝑘 ∈ ℕ ↦ (vol‘((𝐹‘𝑘) ∖ ∪ 𝑚 ∈ (1..^𝑘)(𝐹‘𝑚)))))‘𝑥) = (seq1( + , (𝑘 ∈ ℕ ↦ (vol‘((𝐹‘𝑘) ∖ ∪ 𝑚 ∈ (1..^𝑘)(𝐹‘𝑚)))))‘𝑗))
60		2fveq3 6779	. . . . . . . . . . . . 13 ⊢ (𝑥 = 𝑗 → (vol‘(𝐹‘𝑥)) = (vol‘(𝐹‘𝑗)))
61	59, 60	eqeq12d 2754	. . . . . . . . . . . 12 ⊢ (𝑥 = 𝑗 → ((seq1( + , (𝑘 ∈ ℕ ↦ (vol‘((𝐹‘𝑘) ∖ ∪ 𝑚 ∈ (1..^𝑘)(𝐹‘𝑚)))))‘𝑥) = (vol‘(𝐹‘𝑥)) ↔ (seq1( + , (𝑘 ∈ ℕ ↦ (vol‘((𝐹‘𝑘) ∖ ∪ 𝑚 ∈ (1..^𝑘)(𝐹‘𝑚)))))‘𝑗) = (vol‘(𝐹‘𝑗))))
62	61	imbi2d 341	. . . . . . . . . . 11 ⊢ (𝑥 = 𝑗 → ((((𝐹:ℕ⟶dom vol ∧ ∀𝑛 ∈ ℕ (𝐹‘𝑛) ⊆ (𝐹‘(𝑛 + 1))) ∧ ∀𝑘 ∈ ℕ (vol‘(𝐹‘𝑘)) ∈ ℝ) → (seq1( + , (𝑘 ∈ ℕ ↦ (vol‘((𝐹‘𝑘) ∖ ∪ 𝑚 ∈ (1..^𝑘)(𝐹‘𝑚)))))‘𝑥) = (vol‘(𝐹‘𝑥))) ↔ (((𝐹:ℕ⟶dom vol ∧ ∀𝑛 ∈ ℕ (𝐹‘𝑛) ⊆ (𝐹‘(𝑛 + 1))) ∧ ∀𝑘 ∈ ℕ (vol‘(𝐹‘𝑘)) ∈ ℝ) → (seq1( + , (𝑘 ∈ ℕ ↦ (vol‘((𝐹‘𝑘) ∖ ∪ 𝑚 ∈ (1..^𝑘)(𝐹‘𝑚)))))‘𝑗) = (vol‘(𝐹‘𝑗)))))
63		fveq2 6774	. . . . . . . . . . . . 13 ⊢ (𝑥 = (𝑗 + 1) → (seq1( + , (𝑘 ∈ ℕ ↦ (vol‘((𝐹‘𝑘) ∖ ∪ 𝑚 ∈ (1..^𝑘)(𝐹‘𝑚)))))‘𝑥) = (seq1( + , (𝑘 ∈ ℕ ↦ (vol‘((𝐹‘𝑘) ∖ ∪ 𝑚 ∈ (1..^𝑘)(𝐹‘𝑚)))))‘(𝑗 + 1)))
64		2fveq3 6779	. . . . . . . . . . . . 13 ⊢ (𝑥 = (𝑗 + 1) → (vol‘(𝐹‘𝑥)) = (vol‘(𝐹‘(𝑗 + 1))))
65	63, 64	eqeq12d 2754	. . . . . . . . . . . 12 ⊢ (𝑥 = (𝑗 + 1) → ((seq1( + , (𝑘 ∈ ℕ ↦ (vol‘((𝐹‘𝑘) ∖ ∪ 𝑚 ∈ (1..^𝑘)(𝐹‘𝑚)))))‘𝑥) = (vol‘(𝐹‘𝑥)) ↔ (seq1( + , (𝑘 ∈ ℕ ↦ (vol‘((𝐹‘𝑘) ∖ ∪ 𝑚 ∈ (1..^𝑘)(𝐹‘𝑚)))))‘(𝑗 + 1)) = (vol‘(𝐹‘(𝑗 + 1)))))
66	65	imbi2d 341	. . . . . . . . . . 11 ⊢ (𝑥 = (𝑗 + 1) → ((((𝐹:ℕ⟶dom vol ∧ ∀𝑛 ∈ ℕ (𝐹‘𝑛) ⊆ (𝐹‘(𝑛 + 1))) ∧ ∀𝑘 ∈ ℕ (vol‘(𝐹‘𝑘)) ∈ ℝ) → (seq1( + , (𝑘 ∈ ℕ ↦ (vol‘((𝐹‘𝑘) ∖ ∪ 𝑚 ∈ (1..^𝑘)(𝐹‘𝑚)))))‘𝑥) = (vol‘(𝐹‘𝑥))) ↔ (((𝐹:ℕ⟶dom vol ∧ ∀𝑛 ∈ ℕ (𝐹‘𝑛) ⊆ (𝐹‘(𝑛 + 1))) ∧ ∀𝑘 ∈ ℕ (vol‘(𝐹‘𝑘)) ∈ ℝ) → (seq1( + , (𝑘 ∈ ℕ ↦ (vol‘((𝐹‘𝑘) ∖ ∪ 𝑚 ∈ (1..^𝑘)(𝐹‘𝑚)))))‘(𝑗 + 1)) = (vol‘(𝐹‘(𝑗 + 1))))))
67		seq1 13734	. . . . . . . . . . . . . 14 ⊢ (1 ∈ ℤ → (seq1( + , (𝑘 ∈ ℕ ↦ (vol‘((𝐹‘𝑘) ∖ ∪ 𝑚 ∈ (1..^𝑘)(𝐹‘𝑚)))))‘1) = ((𝑘 ∈ ℕ ↦ (vol‘((𝐹‘𝑘) ∖ ∪ 𝑚 ∈ (1..^𝑘)(𝐹‘𝑚))))‘1))
68	44, 67	ax-mp 5	. . . . . . . . . . . . 13 ⊢ (seq1( + , (𝑘 ∈ ℕ ↦ (vol‘((𝐹‘𝑘) ∖ ∪ 𝑚 ∈ (1..^𝑘)(𝐹‘𝑚)))))‘1) = ((𝑘 ∈ ℕ ↦ (vol‘((𝐹‘𝑘) ∖ ∪ 𝑚 ∈ (1..^𝑘)(𝐹‘𝑚))))‘1)
69		1nn 11984	. . . . . . . . . . . . . 14 ⊢ 1 ∈ ℕ
70		oveq2 7283	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (𝑘 = 1 → (1..^𝑘) = (1..^1))
71		fzo0 13411	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (1..^1) = ∅
72	70, 71	eqtrdi 2794	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (𝑘 = 1 → (1..^𝑘) = ∅)
73	72	iuneq1d 4951	. . . . . . . . . . . . . . . . . . . 20 ⊢ (𝑘 = 1 → ∪ 𝑚 ∈ (1..^𝑘)(𝐹‘𝑚) = ∪ 𝑚 ∈ ∅ (𝐹‘𝑚))
74		0iun 4992	. . . . . . . . . . . . . . . . . . . 20 ⊢ ∪ 𝑚 ∈ ∅ (𝐹‘𝑚) = ∅
75	73, 74	eqtrdi 2794	. . . . . . . . . . . . . . . . . . 19 ⊢ (𝑘 = 1 → ∪ 𝑚 ∈ (1..^𝑘)(𝐹‘𝑚) = ∅)
76	75	difeq2d 4057	. . . . . . . . . . . . . . . . . 18 ⊢ (𝑘 = 1 → ((𝐹‘𝑘) ∖ ∪ 𝑚 ∈ (1..^𝑘)(𝐹‘𝑚)) = ((𝐹‘𝑘) ∖ ∅))
77		dif0 4306	. . . . . . . . . . . . . . . . . 18 ⊢ ((𝐹‘𝑘) ∖ ∅) = (𝐹‘𝑘)
78	76, 77	eqtrdi 2794	. . . . . . . . . . . . . . . . 17 ⊢ (𝑘 = 1 → ((𝐹‘𝑘) ∖ ∪ 𝑚 ∈ (1..^𝑘)(𝐹‘𝑚)) = (𝐹‘𝑘))
79		fveq2 6774	. . . . . . . . . . . . . . . . 17 ⊢ (𝑘 = 1 → (𝐹‘𝑘) = (𝐹‘1))
80	78, 79	eqtrd 2778	. . . . . . . . . . . . . . . 16 ⊢ (𝑘 = 1 → ((𝐹‘𝑘) ∖ ∪ 𝑚 ∈ (1..^𝑘)(𝐹‘𝑚)) = (𝐹‘1))
81	80	fveq2d 6778	. . . . . . . . . . . . . . 15 ⊢ (𝑘 = 1 → (vol‘((𝐹‘𝑘) ∖ ∪ 𝑚 ∈ (1..^𝑘)(𝐹‘𝑚))) = (vol‘(𝐹‘1)))
82		fvex 6787	. . . . . . . . . . . . . . 15 ⊢ (vol‘(𝐹‘1)) ∈ V
83	81, 34, 82	fvmpt 6875	. . . . . . . . . . . . . 14 ⊢ (1 ∈ ℕ → ((𝑘 ∈ ℕ ↦ (vol‘((𝐹‘𝑘) ∖ ∪ 𝑚 ∈ (1..^𝑘)(𝐹‘𝑚))))‘1) = (vol‘(𝐹‘1)))
84	69, 83	ax-mp 5	. . . . . . . . . . . . 13 ⊢ ((𝑘 ∈ ℕ ↦ (vol‘((𝐹‘𝑘) ∖ ∪ 𝑚 ∈ (1..^𝑘)(𝐹‘𝑚))))‘1) = (vol‘(𝐹‘1))
85	68, 84	eqtri 2766	. . . . . . . . . . . 12 ⊢ (seq1( + , (𝑘 ∈ ℕ ↦ (vol‘((𝐹‘𝑘) ∖ ∪ 𝑚 ∈ (1..^𝑘)(𝐹‘𝑚)))))‘1) = (vol‘(𝐹‘1))
86	85	a1i 11	. . . . . . . . . . 11 ⊢ (((𝐹:ℕ⟶dom vol ∧ ∀𝑛 ∈ ℕ (𝐹‘𝑛) ⊆ (𝐹‘(𝑛 + 1))) ∧ ∀𝑘 ∈ ℕ (vol‘(𝐹‘𝑘)) ∈ ℝ) → (seq1( + , (𝑘 ∈ ℕ ↦ (vol‘((𝐹‘𝑘) ∖ ∪ 𝑚 ∈ (1..^𝑘)(𝐹‘𝑚)))))‘1) = (vol‘(𝐹‘1)))
87		oveq1 7282	. . . . . . . . . . . . . 14 ⊢ ((seq1( + , (𝑘 ∈ ℕ ↦ (vol‘((𝐹‘𝑘) ∖ ∪ 𝑚 ∈ (1..^𝑘)(𝐹‘𝑚)))))‘𝑗) = (vol‘(𝐹‘𝑗)) → ((seq1( + , (𝑘 ∈ ℕ ↦ (vol‘((𝐹‘𝑘) ∖ ∪ 𝑚 ∈ (1..^𝑘)(𝐹‘𝑚)))))‘𝑗) + ((𝑘 ∈ ℕ ↦ (vol‘((𝐹‘𝑘) ∖ ∪ 𝑚 ∈ (1..^𝑘)(𝐹‘𝑚))))‘(𝑗 + 1))) = ((vol‘(𝐹‘𝑗)) + ((𝑘 ∈ ℕ ↦ (vol‘((𝐹‘𝑘) ∖ ∪ 𝑚 ∈ (1..^𝑘)(𝐹‘𝑚))))‘(𝑗 + 1))))
88		seqp1 13736	. . . . . . . . . . . . . . . . 17 ⊢ (𝑗 ∈ (ℤ_≥‘1) → (seq1( + , (𝑘 ∈ ℕ ↦ (vol‘((𝐹‘𝑘) ∖ ∪ 𝑚 ∈ (1..^𝑘)(𝐹‘𝑚)))))‘(𝑗 + 1)) = ((seq1( + , (𝑘 ∈ ℕ ↦ (vol‘((𝐹‘𝑘) ∖ ∪ 𝑚 ∈ (1..^𝑘)(𝐹‘𝑚)))))‘𝑗) + ((𝑘 ∈ ℕ ↦ (vol‘((𝐹‘𝑘) ∖ ∪ 𝑚 ∈ (1..^𝑘)(𝐹‘𝑚))))‘(𝑗 + 1))))
89	88, 6	eleq2s 2857	. . . . . . . . . . . . . . . 16 ⊢ (𝑗 ∈ ℕ → (seq1( + , (𝑘 ∈ ℕ ↦ (vol‘((𝐹‘𝑘) ∖ ∪ 𝑚 ∈ (1..^𝑘)(𝐹‘𝑚)))))‘(𝑗 + 1)) = ((seq1( + , (𝑘 ∈ ℕ ↦ (vol‘((𝐹‘𝑘) ∖ ∪ 𝑚 ∈ (1..^𝑘)(𝐹‘𝑚)))))‘𝑗) + ((𝑘 ∈ ℕ ↦ (vol‘((𝐹‘𝑘) ∖ ∪ 𝑚 ∈ (1..^𝑘)(𝐹‘𝑚))))‘(𝑗 + 1))))
90	89	adantl 482	. . . . . . . . . . . . . . 15 ⊢ ((((𝐹:ℕ⟶dom vol ∧ ∀𝑛 ∈ ℕ (𝐹‘𝑛) ⊆ (𝐹‘(𝑛 + 1))) ∧ ∀𝑘 ∈ ℕ (vol‘(𝐹‘𝑘)) ∈ ℝ) ∧ 𝑗 ∈ ℕ) → (seq1( + , (𝑘 ∈ ℕ ↦ (vol‘((𝐹‘𝑘) ∖ ∪ 𝑚 ∈ (1..^𝑘)(𝐹‘𝑚)))))‘(𝑗 + 1)) = ((seq1( + , (𝑘 ∈ ℕ ↦ (vol‘((𝐹‘𝑘) ∖ ∪ 𝑚 ∈ (1..^𝑘)(𝐹‘𝑚)))))‘𝑗) + ((𝑘 ∈ ℕ ↦ (vol‘((𝐹‘𝑘) ∖ ∪ 𝑚 ∈ (1..^𝑘)(𝐹‘𝑚))))‘(𝑗 + 1))))
91		undif2 4410	. . . . . . . . . . . . . . . . . 18 ⊢ ((𝐹‘𝑗) ∪ ((𝐹‘(𝑗 + 1)) ∖ (𝐹‘𝑗))) = ((𝐹‘𝑗) ∪ (𝐹‘(𝑗 + 1)))
92		fveq2 6774	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (𝑛 = 𝑗 → (𝐹‘𝑛) = (𝐹‘𝑗))
93		fvoveq1 7298	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (𝑛 = 𝑗 → (𝐹‘(𝑛 + 1)) = (𝐹‘(𝑗 + 1)))
94	92, 93	sseq12d 3954	. . . . . . . . . . . . . . . . . . . 20 ⊢ (𝑛 = 𝑗 → ((𝐹‘𝑛) ⊆ (𝐹‘(𝑛 + 1)) ↔ (𝐹‘𝑗) ⊆ (𝐹‘(𝑗 + 1))))
95		simpllr 773	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((((𝐹:ℕ⟶dom vol ∧ ∀𝑛 ∈ ℕ (𝐹‘𝑛) ⊆ (𝐹‘(𝑛 + 1))) ∧ ∀𝑘 ∈ ℕ (vol‘(𝐹‘𝑘)) ∈ ℝ) ∧ 𝑗 ∈ ℕ) → ∀𝑛 ∈ ℕ (𝐹‘𝑛) ⊆ (𝐹‘(𝑛 + 1)))
96		simpr 485	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((((𝐹:ℕ⟶dom vol ∧ ∀𝑛 ∈ ℕ (𝐹‘𝑛) ⊆ (𝐹‘(𝑛 + 1))) ∧ ∀𝑘 ∈ ℕ (vol‘(𝐹‘𝑘)) ∈ ℝ) ∧ 𝑗 ∈ ℕ) → 𝑗 ∈ ℕ)
97	94, 95, 96	rspcdva 3562	. . . . . . . . . . . . . . . . . . 19 ⊢ ((((𝐹:ℕ⟶dom vol ∧ ∀𝑛 ∈ ℕ (𝐹‘𝑛) ⊆ (𝐹‘(𝑛 + 1))) ∧ ∀𝑘 ∈ ℕ (vol‘(𝐹‘𝑘)) ∈ ℝ) ∧ 𝑗 ∈ ℕ) → (𝐹‘𝑗) ⊆ (𝐹‘(𝑗 + 1)))
98		ssequn1 4114	. . . . . . . . . . . . . . . . . . 19 ⊢ ((𝐹‘𝑗) ⊆ (𝐹‘(𝑗 + 1)) ↔ ((𝐹‘𝑗) ∪ (𝐹‘(𝑗 + 1))) = (𝐹‘(𝑗 + 1)))
99	97, 98	sylib 217	. . . . . . . . . . . . . . . . . 18 ⊢ ((((𝐹:ℕ⟶dom vol ∧ ∀𝑛 ∈ ℕ (𝐹‘𝑛) ⊆ (𝐹‘(𝑛 + 1))) ∧ ∀𝑘 ∈ ℕ (vol‘(𝐹‘𝑘)) ∈ ℝ) ∧ 𝑗 ∈ ℕ) → ((𝐹‘𝑗) ∪ (𝐹‘(𝑗 + 1))) = (𝐹‘(𝑗 + 1)))
100	91, 99	eqtr2id 2791	. . . . . . . . . . . . . . . . 17 ⊢ ((((𝐹:ℕ⟶dom vol ∧ ∀𝑛 ∈ ℕ (𝐹‘𝑛) ⊆ (𝐹‘(𝑛 + 1))) ∧ ∀𝑘 ∈ ℕ (vol‘(𝐹‘𝑘)) ∈ ℝ) ∧ 𝑗 ∈ ℕ) → (𝐹‘(𝑗 + 1)) = ((𝐹‘𝑗) ∪ ((𝐹‘(𝑗 + 1)) ∖ (𝐹‘𝑗))))
101	100	fveq2d 6778	. . . . . . . . . . . . . . . 16 ⊢ ((((𝐹:ℕ⟶dom vol ∧ ∀𝑛 ∈ ℕ (𝐹‘𝑛) ⊆ (𝐹‘(𝑛 + 1))) ∧ ∀𝑘 ∈ ℕ (vol‘(𝐹‘𝑘)) ∈ ℝ) ∧ 𝑗 ∈ ℕ) → (vol‘(𝐹‘(𝑗 + 1))) = (vol‘((𝐹‘𝑗) ∪ ((𝐹‘(𝑗 + 1)) ∖ (𝐹‘𝑗)))))
102		simplll 772	. . . . . . . . . . . . . . . . . 18 ⊢ ((((𝐹:ℕ⟶dom vol ∧ ∀𝑛 ∈ ℕ (𝐹‘𝑛) ⊆ (𝐹‘(𝑛 + 1))) ∧ ∀𝑘 ∈ ℕ (vol‘(𝐹‘𝑘)) ∈ ℝ) ∧ 𝑗 ∈ ℕ) → 𝐹:ℕ⟶dom vol)
103	102, 96	ffvelrnd 6962	. . . . . . . . . . . . . . . . 17 ⊢ ((((𝐹:ℕ⟶dom vol ∧ ∀𝑛 ∈ ℕ (𝐹‘𝑛) ⊆ (𝐹‘(𝑛 + 1))) ∧ ∀𝑘 ∈ ℕ (vol‘(𝐹‘𝑘)) ∈ ℝ) ∧ 𝑗 ∈ ℕ) → (𝐹‘𝑗) ∈ dom vol)
104		peano2nn 11985	. . . . . . . . . . . . . . . . . . . 20 ⊢ (𝑗 ∈ ℕ → (𝑗 + 1) ∈ ℕ)
105	104	adantl 482	. . . . . . . . . . . . . . . . . . 19 ⊢ ((((𝐹:ℕ⟶dom vol ∧ ∀𝑛 ∈ ℕ (𝐹‘𝑛) ⊆ (𝐹‘(𝑛 + 1))) ∧ ∀𝑘 ∈ ℕ (vol‘(𝐹‘𝑘)) ∈ ℝ) ∧ 𝑗 ∈ ℕ) → (𝑗 + 1) ∈ ℕ)
106	102, 105	ffvelrnd 6962	. . . . . . . . . . . . . . . . . 18 ⊢ ((((𝐹:ℕ⟶dom vol ∧ ∀𝑛 ∈ ℕ (𝐹‘𝑛) ⊆ (𝐹‘(𝑛 + 1))) ∧ ∀𝑘 ∈ ℕ (vol‘(𝐹‘𝑘)) ∈ ℝ) ∧ 𝑗 ∈ ℕ) → (𝐹‘(𝑗 + 1)) ∈ dom vol)
107		difmbl 24707	. . . . . . . . . . . . . . . . . 18 ⊢ (((𝐹‘(𝑗 + 1)) ∈ dom vol ∧ (𝐹‘𝑗) ∈ dom vol) → ((𝐹‘(𝑗 + 1)) ∖ (𝐹‘𝑗)) ∈ dom vol)
108	106, 103, 107	syl2anc 584	. . . . . . . . . . . . . . . . 17 ⊢ ((((𝐹:ℕ⟶dom vol ∧ ∀𝑛 ∈ ℕ (𝐹‘𝑛) ⊆ (𝐹‘(𝑛 + 1))) ∧ ∀𝑘 ∈ ℕ (vol‘(𝐹‘𝑘)) ∈ ℝ) ∧ 𝑗 ∈ ℕ) → ((𝐹‘(𝑗 + 1)) ∖ (𝐹‘𝑗)) ∈ dom vol)
109		disjdif 4405	. . . . . . . . . . . . . . . . . 18 ⊢ ((𝐹‘𝑗) ∩ ((𝐹‘(𝑗 + 1)) ∖ (𝐹‘𝑗))) = ∅
110	109	a1i 11	. . . . . . . . . . . . . . . . 17 ⊢ ((((𝐹:ℕ⟶dom vol ∧ ∀𝑛 ∈ ℕ (𝐹‘𝑛) ⊆ (𝐹‘(𝑛 + 1))) ∧ ∀𝑘 ∈ ℕ (vol‘(𝐹‘𝑘)) ∈ ℝ) ∧ 𝑗 ∈ ℕ) → ((𝐹‘𝑗) ∩ ((𝐹‘(𝑗 + 1)) ∖ (𝐹‘𝑗))) = ∅)
111		2fveq3 6779	. . . . . . . . . . . . . . . . . . 19 ⊢ (𝑘 = 𝑗 → (vol‘(𝐹‘𝑘)) = (vol‘(𝐹‘𝑗)))
112	111	eleq1d 2823	. . . . . . . . . . . . . . . . . 18 ⊢ (𝑘 = 𝑗 → ((vol‘(𝐹‘𝑘)) ∈ ℝ ↔ (vol‘(𝐹‘𝑗)) ∈ ℝ))
113		simplr 766	. . . . . . . . . . . . . . . . . 18 ⊢ ((((𝐹:ℕ⟶dom vol ∧ ∀𝑛 ∈ ℕ (𝐹‘𝑛) ⊆ (𝐹‘(𝑛 + 1))) ∧ ∀𝑘 ∈ ℕ (vol‘(𝐹‘𝑘)) ∈ ℝ) ∧ 𝑗 ∈ ℕ) → ∀𝑘 ∈ ℕ (vol‘(𝐹‘𝑘)) ∈ ℝ)
114	112, 113, 96	rspcdva 3562	. . . . . . . . . . . . . . . . 17 ⊢ ((((𝐹:ℕ⟶dom vol ∧ ∀𝑛 ∈ ℕ (𝐹‘𝑛) ⊆ (𝐹‘(𝑛 + 1))) ∧ ∀𝑘 ∈ ℕ (vol‘(𝐹‘𝑘)) ∈ ℝ) ∧ 𝑗 ∈ ℕ) → (vol‘(𝐹‘𝑗)) ∈ ℝ)
115		mblvol 24694	. . . . . . . . . . . . . . . . . . 19 ⊢ (((𝐹‘(𝑗 + 1)) ∖ (𝐹‘𝑗)) ∈ dom vol → (vol‘((𝐹‘(𝑗 + 1)) ∖ (𝐹‘𝑗))) = (vol*‘((𝐹‘(𝑗 + 1)) ∖ (𝐹‘𝑗))))
116	108, 115	syl 17	. . . . . . . . . . . . . . . . . 18 ⊢ ((((𝐹:ℕ⟶dom vol ∧ ∀𝑛 ∈ ℕ (𝐹‘𝑛) ⊆ (𝐹‘(𝑛 + 1))) ∧ ∀𝑘 ∈ ℕ (vol‘(𝐹‘𝑘)) ∈ ℝ) ∧ 𝑗 ∈ ℕ) → (vol‘((𝐹‘(𝑗 + 1)) ∖ (𝐹‘𝑗))) = (vol*‘((𝐹‘(𝑗 + 1)) ∖ (𝐹‘𝑗))))
117		difssd 4067	. . . . . . . . . . . . . . . . . . 19 ⊢ ((((𝐹:ℕ⟶dom vol ∧ ∀𝑛 ∈ ℕ (𝐹‘𝑛) ⊆ (𝐹‘(𝑛 + 1))) ∧ ∀𝑘 ∈ ℕ (vol‘(𝐹‘𝑘)) ∈ ℝ) ∧ 𝑗 ∈ ℕ) → ((𝐹‘(𝑗 + 1)) ∖ (𝐹‘𝑗)) ⊆ (𝐹‘(𝑗 + 1)))
118		mblss 24695	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((𝐹‘(𝑗 + 1)) ∈ dom vol → (𝐹‘(𝑗 + 1)) ⊆ ℝ)
119	106, 118	syl 17	. . . . . . . . . . . . . . . . . . 19 ⊢ ((((𝐹:ℕ⟶dom vol ∧ ∀𝑛 ∈ ℕ (𝐹‘𝑛) ⊆ (𝐹‘(𝑛 + 1))) ∧ ∀𝑘 ∈ ℕ (vol‘(𝐹‘𝑘)) ∈ ℝ) ∧ 𝑗 ∈ ℕ) → (𝐹‘(𝑗 + 1)) ⊆ ℝ)
120		mblvol 24694	. . . . . . . . . . . . . . . . . . . . 21 ⊢ ((𝐹‘(𝑗 + 1)) ∈ dom vol → (vol‘(𝐹‘(𝑗 + 1))) = (vol*‘(𝐹‘(𝑗 + 1))))
121	106, 120	syl 17	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((((𝐹:ℕ⟶dom vol ∧ ∀𝑛 ∈ ℕ (𝐹‘𝑛) ⊆ (𝐹‘(𝑛 + 1))) ∧ ∀𝑘 ∈ ℕ (vol‘(𝐹‘𝑘)) ∈ ℝ) ∧ 𝑗 ∈ ℕ) → (vol‘(𝐹‘(𝑗 + 1))) = (vol*‘(𝐹‘(𝑗 + 1))))
122		2fveq3 6779	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (𝑘 = (𝑗 + 1) → (vol‘(𝐹‘𝑘)) = (vol‘(𝐹‘(𝑗 + 1))))
123	122	eleq1d 2823	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (𝑘 = (𝑗 + 1) → ((vol‘(𝐹‘𝑘)) ∈ ℝ ↔ (vol‘(𝐹‘(𝑗 + 1))) ∈ ℝ))
124	123, 113, 105	rspcdva 3562	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((((𝐹:ℕ⟶dom vol ∧ ∀𝑛 ∈ ℕ (𝐹‘𝑛) ⊆ (𝐹‘(𝑛 + 1))) ∧ ∀𝑘 ∈ ℕ (vol‘(𝐹‘𝑘)) ∈ ℝ) ∧ 𝑗 ∈ ℕ) → (vol‘(𝐹‘(𝑗 + 1))) ∈ ℝ)
125	121, 124	eqeltrrd 2840	. . . . . . . . . . . . . . . . . . 19 ⊢ ((((𝐹:ℕ⟶dom vol ∧ ∀𝑛 ∈ ℕ (𝐹‘𝑛) ⊆ (𝐹‘(𝑛 + 1))) ∧ ∀𝑘 ∈ ℕ (vol‘(𝐹‘𝑘)) ∈ ℝ) ∧ 𝑗 ∈ ℕ) → (vol*‘(𝐹‘(𝑗 + 1))) ∈ ℝ)
126		ovolsscl 24650	. . . . . . . . . . . . . . . . . . 19 ⊢ ((((𝐹‘(𝑗 + 1)) ∖ (𝐹‘𝑗)) ⊆ (𝐹‘(𝑗 + 1)) ∧ (𝐹‘(𝑗 + 1)) ⊆ ℝ ∧ (vol‘(𝐹‘(𝑗 + 1))) ∈ ℝ) → (vol‘((𝐹‘(𝑗 + 1)) ∖ (𝐹‘𝑗))) ∈ ℝ)
127	117, 119, 125, 126	syl3anc 1370	. . . . . . . . . . . . . . . . . 18 ⊢ ((((𝐹:ℕ⟶dom vol ∧ ∀𝑛 ∈ ℕ (𝐹‘𝑛) ⊆ (𝐹‘(𝑛 + 1))) ∧ ∀𝑘 ∈ ℕ (vol‘(𝐹‘𝑘)) ∈ ℝ) ∧ 𝑗 ∈ ℕ) → (vol*‘((𝐹‘(𝑗 + 1)) ∖ (𝐹‘𝑗))) ∈ ℝ)
128	116, 127	eqeltrd 2839	. . . . . . . . . . . . . . . . 17 ⊢ ((((𝐹:ℕ⟶dom vol ∧ ∀𝑛 ∈ ℕ (𝐹‘𝑛) ⊆ (𝐹‘(𝑛 + 1))) ∧ ∀𝑘 ∈ ℕ (vol‘(𝐹‘𝑘)) ∈ ℝ) ∧ 𝑗 ∈ ℕ) → (vol‘((𝐹‘(𝑗 + 1)) ∖ (𝐹‘𝑗))) ∈ ℝ)
129		volun 24709	. . . . . . . . . . . . . . . . 17 ⊢ ((((𝐹‘𝑗) ∈ dom vol ∧ ((𝐹‘(𝑗 + 1)) ∖ (𝐹‘𝑗)) ∈ dom vol ∧ ((𝐹‘𝑗) ∩ ((𝐹‘(𝑗 + 1)) ∖ (𝐹‘𝑗))) = ∅) ∧ ((vol‘(𝐹‘𝑗)) ∈ ℝ ∧ (vol‘((𝐹‘(𝑗 + 1)) ∖ (𝐹‘𝑗))) ∈ ℝ)) → (vol‘((𝐹‘𝑗) ∪ ((𝐹‘(𝑗 + 1)) ∖ (𝐹‘𝑗)))) = ((vol‘(𝐹‘𝑗)) + (vol‘((𝐹‘(𝑗 + 1)) ∖ (𝐹‘𝑗)))))
130	103, 108, 110, 114, 128, 129	syl32anc 1377	. . . . . . . . . . . . . . . 16 ⊢ ((((𝐹:ℕ⟶dom vol ∧ ∀𝑛 ∈ ℕ (𝐹‘𝑛) ⊆ (𝐹‘(𝑛 + 1))) ∧ ∀𝑘 ∈ ℕ (vol‘(𝐹‘𝑘)) ∈ ℝ) ∧ 𝑗 ∈ ℕ) → (vol‘((𝐹‘𝑗) ∪ ((𝐹‘(𝑗 + 1)) ∖ (𝐹‘𝑗)))) = ((vol‘(𝐹‘𝑗)) + (vol‘((𝐹‘(𝑗 + 1)) ∖ (𝐹‘𝑗)))))
131	95	adantr 481	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ (((((𝐹:ℕ⟶dom vol ∧ ∀𝑛 ∈ ℕ (𝐹‘𝑛) ⊆ (𝐹‘(𝑛 + 1))) ∧ ∀𝑘 ∈ ℕ (vol‘(𝐹‘𝑘)) ∈ ℝ) ∧ 𝑗 ∈ ℕ) ∧ 𝑚 ∈ (1...𝑗)) → ∀𝑛 ∈ ℕ (𝐹‘𝑛) ⊆ (𝐹‘(𝑛 + 1)))
132		elfznn 13285	. . . . . . . . . . . . . . . . . . . . . . . . . 26 ⊢ (𝑚 ∈ (1...𝑗) → 𝑚 ∈ ℕ)
133	132	adantl 482	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ (((((𝐹:ℕ⟶dom vol ∧ ∀𝑛 ∈ ℕ (𝐹‘𝑛) ⊆ (𝐹‘(𝑛 + 1))) ∧ ∀𝑘 ∈ ℕ (vol‘(𝐹‘𝑘)) ∈ ℝ) ∧ 𝑗 ∈ ℕ) ∧ 𝑚 ∈ (1...𝑗)) → 𝑚 ∈ ℕ)
134		elfzuz3 13253	. . . . . . . . . . . . . . . . . . . . . . . . . 26 ⊢ (𝑚 ∈ (1...𝑗) → 𝑗 ∈ (ℤ_≥‘𝑚))
135	134	adantl 482	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ (((((𝐹:ℕ⟶dom vol ∧ ∀𝑛 ∈ ℕ (𝐹‘𝑛) ⊆ (𝐹‘(𝑛 + 1))) ∧ ∀𝑘 ∈ ℕ (vol‘(𝐹‘𝑘)) ∈ ℝ) ∧ 𝑗 ∈ ℕ) ∧ 𝑚 ∈ (1...𝑗)) → 𝑗 ∈ (ℤ_≥‘𝑚))
136		volsuplem 24719	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ ((∀𝑛 ∈ ℕ (𝐹‘𝑛) ⊆ (𝐹‘(𝑛 + 1)) ∧ (𝑚 ∈ ℕ ∧ 𝑗 ∈ (ℤ_≥‘𝑚))) → (𝐹‘𝑚) ⊆ (𝐹‘𝑗))
137	131, 133, 135, 136	syl12anc 834	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ (((((𝐹:ℕ⟶dom vol ∧ ∀𝑛 ∈ ℕ (𝐹‘𝑛) ⊆ (𝐹‘(𝑛 + 1))) ∧ ∀𝑘 ∈ ℕ (vol‘(𝐹‘𝑘)) ∈ ℝ) ∧ 𝑗 ∈ ℕ) ∧ 𝑚 ∈ (1...𝑗)) → (𝐹‘𝑚) ⊆ (𝐹‘𝑗))
138	137	ralrimiva 3103	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ ((((𝐹:ℕ⟶dom vol ∧ ∀𝑛 ∈ ℕ (𝐹‘𝑛) ⊆ (𝐹‘(𝑛 + 1))) ∧ ∀𝑘 ∈ ℕ (vol‘(𝐹‘𝑘)) ∈ ℝ) ∧ 𝑗 ∈ ℕ) → ∀𝑚 ∈ (1...𝑗)(𝐹‘𝑚) ⊆ (𝐹‘𝑗))
139		iunss 4975	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ (∪ 𝑚 ∈ (1...𝑗)(𝐹‘𝑚) ⊆ (𝐹‘𝑗) ↔ ∀𝑚 ∈ (1...𝑗)(𝐹‘𝑚) ⊆ (𝐹‘𝑗))
140	138, 139	sylibr 233	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ ((((𝐹:ℕ⟶dom vol ∧ ∀𝑛 ∈ ℕ (𝐹‘𝑛) ⊆ (𝐹‘(𝑛 + 1))) ∧ ∀𝑘 ∈ ℕ (vol‘(𝐹‘𝑘)) ∈ ℝ) ∧ 𝑗 ∈ ℕ) → ∪ 𝑚 ∈ (1...𝑗)(𝐹‘𝑚) ⊆ (𝐹‘𝑗))
141	96, 6	eleqtrdi 2849	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ ((((𝐹:ℕ⟶dom vol ∧ ∀𝑛 ∈ ℕ (𝐹‘𝑛) ⊆ (𝐹‘(𝑛 + 1))) ∧ ∀𝑘 ∈ ℕ (vol‘(𝐹‘𝑘)) ∈ ℝ) ∧ 𝑗 ∈ ℕ) → 𝑗 ∈ (ℤ_≥‘1))
142		eluzfz2 13264	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ (𝑗 ∈ (ℤ_≥‘1) → 𝑗 ∈ (1...𝑗))
143	141, 142	syl 17	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ ((((𝐹:ℕ⟶dom vol ∧ ∀𝑛 ∈ ℕ (𝐹‘𝑛) ⊆ (𝐹‘(𝑛 + 1))) ∧ ∀𝑘 ∈ ℕ (vol‘(𝐹‘𝑘)) ∈ ℝ) ∧ 𝑗 ∈ ℕ) → 𝑗 ∈ (1...𝑗))
144		fveq2 6774	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ (𝑚 = 𝑗 → (𝐹‘𝑚) = (𝐹‘𝑗))
145	144	ssiun2s 4978	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ (𝑗 ∈ (1...𝑗) → (𝐹‘𝑗) ⊆ ∪ 𝑚 ∈ (1...𝑗)(𝐹‘𝑚))
146	143, 145	syl 17	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ ((((𝐹:ℕ⟶dom vol ∧ ∀𝑛 ∈ ℕ (𝐹‘𝑛) ⊆ (𝐹‘(𝑛 + 1))) ∧ ∀𝑘 ∈ ℕ (vol‘(𝐹‘𝑘)) ∈ ℝ) ∧ 𝑗 ∈ ℕ) → (𝐹‘𝑗) ⊆ ∪ 𝑚 ∈ (1...𝑗)(𝐹‘𝑚))
147	140, 146	eqssd 3938	. . . . . . . . . . . . . . . . . . . . 21 ⊢ ((((𝐹:ℕ⟶dom vol ∧ ∀𝑛 ∈ ℕ (𝐹‘𝑛) ⊆ (𝐹‘(𝑛 + 1))) ∧ ∀𝑘 ∈ ℕ (vol‘(𝐹‘𝑘)) ∈ ℝ) ∧ 𝑗 ∈ ℕ) → ∪ 𝑚 ∈ (1...𝑗)(𝐹‘𝑚) = (𝐹‘𝑗))
148	96	nnzd 12425	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ ((((𝐹:ℕ⟶dom vol ∧ ∀𝑛 ∈ ℕ (𝐹‘𝑛) ⊆ (𝐹‘(𝑛 + 1))) ∧ ∀𝑘 ∈ ℕ (vol‘(𝐹‘𝑘)) ∈ ℝ) ∧ 𝑗 ∈ ℕ) → 𝑗 ∈ ℤ)
149		fzval3 13456	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ (𝑗 ∈ ℤ → (1...𝑗) = (1..^(𝑗 + 1)))
150	148, 149	syl 17	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ ((((𝐹:ℕ⟶dom vol ∧ ∀𝑛 ∈ ℕ (𝐹‘𝑛) ⊆ (𝐹‘(𝑛 + 1))) ∧ ∀𝑘 ∈ ℕ (vol‘(𝐹‘𝑘)) ∈ ℝ) ∧ 𝑗 ∈ ℕ) → (1...𝑗) = (1..^(𝑗 + 1)))
151	150	iuneq1d 4951	. . . . . . . . . . . . . . . . . . . . 21 ⊢ ((((𝐹:ℕ⟶dom vol ∧ ∀𝑛 ∈ ℕ (𝐹‘𝑛) ⊆ (𝐹‘(𝑛 + 1))) ∧ ∀𝑘 ∈ ℕ (vol‘(𝐹‘𝑘)) ∈ ℝ) ∧ 𝑗 ∈ ℕ) → ∪ 𝑚 ∈ (1...𝑗)(𝐹‘𝑚) = ∪ 𝑚 ∈ (1..^(𝑗 + 1))(𝐹‘𝑚))
152	147, 151	eqtr3d 2780	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((((𝐹:ℕ⟶dom vol ∧ ∀𝑛 ∈ ℕ (𝐹‘𝑛) ⊆ (𝐹‘(𝑛 + 1))) ∧ ∀𝑘 ∈ ℕ (vol‘(𝐹‘𝑘)) ∈ ℝ) ∧ 𝑗 ∈ ℕ) → (𝐹‘𝑗) = ∪ 𝑚 ∈ (1..^(𝑗 + 1))(𝐹‘𝑚))
153	152	difeq2d 4057	. . . . . . . . . . . . . . . . . . 19 ⊢ ((((𝐹:ℕ⟶dom vol ∧ ∀𝑛 ∈ ℕ (𝐹‘𝑛) ⊆ (𝐹‘(𝑛 + 1))) ∧ ∀𝑘 ∈ ℕ (vol‘(𝐹‘𝑘)) ∈ ℝ) ∧ 𝑗 ∈ ℕ) → ((𝐹‘(𝑗 + 1)) ∖ (𝐹‘𝑗)) = ((𝐹‘(𝑗 + 1)) ∖ ∪ 𝑚 ∈ (1..^(𝑗 + 1))(𝐹‘𝑚)))
154	153	fveq2d 6778	. . . . . . . . . . . . . . . . . 18 ⊢ ((((𝐹:ℕ⟶dom vol ∧ ∀𝑛 ∈ ℕ (𝐹‘𝑛) ⊆ (𝐹‘(𝑛 + 1))) ∧ ∀𝑘 ∈ ℕ (vol‘(𝐹‘𝑘)) ∈ ℝ) ∧ 𝑗 ∈ ℕ) → (vol‘((𝐹‘(𝑗 + 1)) ∖ (𝐹‘𝑗))) = (vol‘((𝐹‘(𝑗 + 1)) ∖ ∪ 𝑚 ∈ (1..^(𝑗 + 1))(𝐹‘𝑚))))
155		fveq2 6774	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (𝑘 = (𝑗 + 1) → (𝐹‘𝑘) = (𝐹‘(𝑗 + 1)))
156		oveq2 7283	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ (𝑘 = (𝑗 + 1) → (1..^𝑘) = (1..^(𝑗 + 1)))
157	156	iuneq1d 4951	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (𝑘 = (𝑗 + 1) → ∪ 𝑚 ∈ (1..^𝑘)(𝐹‘𝑚) = ∪ 𝑚 ∈ (1..^(𝑗 + 1))(𝐹‘𝑚))
158	155, 157	difeq12d 4058	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (𝑘 = (𝑗 + 1) → ((𝐹‘𝑘) ∖ ∪ 𝑚 ∈ (1..^𝑘)(𝐹‘𝑚)) = ((𝐹‘(𝑗 + 1)) ∖ ∪ 𝑚 ∈ (1..^(𝑗 + 1))(𝐹‘𝑚)))
159	158	fveq2d 6778	. . . . . . . . . . . . . . . . . . . 20 ⊢ (𝑘 = (𝑗 + 1) → (vol‘((𝐹‘𝑘) ∖ ∪ 𝑚 ∈ (1..^𝑘)(𝐹‘𝑚))) = (vol‘((𝐹‘(𝑗 + 1)) ∖ ∪ 𝑚 ∈ (1..^(𝑗 + 1))(𝐹‘𝑚))))
160		fvex 6787	. . . . . . . . . . . . . . . . . . . 20 ⊢ (vol‘((𝐹‘(𝑗 + 1)) ∖ ∪ 𝑚 ∈ (1..^(𝑗 + 1))(𝐹‘𝑚))) ∈ V
161	159, 34, 160	fvmpt 6875	. . . . . . . . . . . . . . . . . . 19 ⊢ ((𝑗 + 1) ∈ ℕ → ((𝑘 ∈ ℕ ↦ (vol‘((𝐹‘𝑘) ∖ ∪ 𝑚 ∈ (1..^𝑘)(𝐹‘𝑚))))‘(𝑗 + 1)) = (vol‘((𝐹‘(𝑗 + 1)) ∖ ∪ 𝑚 ∈ (1..^(𝑗 + 1))(𝐹‘𝑚))))
162	105, 161	syl 17	. . . . . . . . . . . . . . . . . 18 ⊢ ((((𝐹:ℕ⟶dom vol ∧ ∀𝑛 ∈ ℕ (𝐹‘𝑛) ⊆ (𝐹‘(𝑛 + 1))) ∧ ∀𝑘 ∈ ℕ (vol‘(𝐹‘𝑘)) ∈ ℝ) ∧ 𝑗 ∈ ℕ) → ((𝑘 ∈ ℕ ↦ (vol‘((𝐹‘𝑘) ∖ ∪ 𝑚 ∈ (1..^𝑘)(𝐹‘𝑚))))‘(𝑗 + 1)) = (vol‘((𝐹‘(𝑗 + 1)) ∖ ∪ 𝑚 ∈ (1..^(𝑗 + 1))(𝐹‘𝑚))))
163	154, 162	eqtr4d 2781	. . . . . . . . . . . . . . . . 17 ⊢ ((((𝐹:ℕ⟶dom vol ∧ ∀𝑛 ∈ ℕ (𝐹‘𝑛) ⊆ (𝐹‘(𝑛 + 1))) ∧ ∀𝑘 ∈ ℕ (vol‘(𝐹‘𝑘)) ∈ ℝ) ∧ 𝑗 ∈ ℕ) → (vol‘((𝐹‘(𝑗 + 1)) ∖ (𝐹‘𝑗))) = ((𝑘 ∈ ℕ ↦ (vol‘((𝐹‘𝑘) ∖ ∪ 𝑚 ∈ (1..^𝑘)(𝐹‘𝑚))))‘(𝑗 + 1)))
164	163	oveq2d 7291	. . . . . . . . . . . . . . . 16 ⊢ ((((𝐹:ℕ⟶dom vol ∧ ∀𝑛 ∈ ℕ (𝐹‘𝑛) ⊆ (𝐹‘(𝑛 + 1))) ∧ ∀𝑘 ∈ ℕ (vol‘(𝐹‘𝑘)) ∈ ℝ) ∧ 𝑗 ∈ ℕ) → ((vol‘(𝐹‘𝑗)) + (vol‘((𝐹‘(𝑗 + 1)) ∖ (𝐹‘𝑗)))) = ((vol‘(𝐹‘𝑗)) + ((𝑘 ∈ ℕ ↦ (vol‘((𝐹‘𝑘) ∖ ∪ 𝑚 ∈ (1..^𝑘)(𝐹‘𝑚))))‘(𝑗 + 1))))
165	101, 130, 164	3eqtrd 2782	. . . . . . . . . . . . . . 15 ⊢ ((((𝐹:ℕ⟶dom vol ∧ ∀𝑛 ∈ ℕ (𝐹‘𝑛) ⊆ (𝐹‘(𝑛 + 1))) ∧ ∀𝑘 ∈ ℕ (vol‘(𝐹‘𝑘)) ∈ ℝ) ∧ 𝑗 ∈ ℕ) → (vol‘(𝐹‘(𝑗 + 1))) = ((vol‘(𝐹‘𝑗)) + ((𝑘 ∈ ℕ ↦ (vol‘((𝐹‘𝑘) ∖ ∪ 𝑚 ∈ (1..^𝑘)(𝐹‘𝑚))))‘(𝑗 + 1))))
166	90, 165	eqeq12d 2754	. . . . . . . . . . . . . 14 ⊢ ((((𝐹:ℕ⟶dom vol ∧ ∀𝑛 ∈ ℕ (𝐹‘𝑛) ⊆ (𝐹‘(𝑛 + 1))) ∧ ∀𝑘 ∈ ℕ (vol‘(𝐹‘𝑘)) ∈ ℝ) ∧ 𝑗 ∈ ℕ) → ((seq1( + , (𝑘 ∈ ℕ ↦ (vol‘((𝐹‘𝑘) ∖ ∪ 𝑚 ∈ (1..^𝑘)(𝐹‘𝑚)))))‘(𝑗 + 1)) = (vol‘(𝐹‘(𝑗 + 1))) ↔ ((seq1( + , (𝑘 ∈ ℕ ↦ (vol‘((𝐹‘𝑘) ∖ ∪ 𝑚 ∈ (1..^𝑘)(𝐹‘𝑚)))))‘𝑗) + ((𝑘 ∈ ℕ ↦ (vol‘((𝐹‘𝑘) ∖ ∪ 𝑚 ∈ (1..^𝑘)(𝐹‘𝑚))))‘(𝑗 + 1))) = ((vol‘(𝐹‘𝑗)) + ((𝑘 ∈ ℕ ↦ (vol‘((𝐹‘𝑘) ∖ ∪ 𝑚 ∈ (1..^𝑘)(𝐹‘𝑚))))‘(𝑗 + 1)))))
167	87, 166	syl5ibr 245	. . . . . . . . . . . . 13 ⊢ ((((𝐹:ℕ⟶dom vol ∧ ∀𝑛 ∈ ℕ (𝐹‘𝑛) ⊆ (𝐹‘(𝑛 + 1))) ∧ ∀𝑘 ∈ ℕ (vol‘(𝐹‘𝑘)) ∈ ℝ) ∧ 𝑗 ∈ ℕ) → ((seq1( + , (𝑘 ∈ ℕ ↦ (vol‘((𝐹‘𝑘) ∖ ∪ 𝑚 ∈ (1..^𝑘)(𝐹‘𝑚)))))‘𝑗) = (vol‘(𝐹‘𝑗)) → (seq1( + , (𝑘 ∈ ℕ ↦ (vol‘((𝐹‘𝑘) ∖ ∪ 𝑚 ∈ (1..^𝑘)(𝐹‘𝑚)))))‘(𝑗 + 1)) = (vol‘(𝐹‘(𝑗 + 1)))))
168	167	expcom 414	. . . . . . . . . . . 12 ⊢ (𝑗 ∈ ℕ → (((𝐹:ℕ⟶dom vol ∧ ∀𝑛 ∈ ℕ (𝐹‘𝑛) ⊆ (𝐹‘(𝑛 + 1))) ∧ ∀𝑘 ∈ ℕ (vol‘(𝐹‘𝑘)) ∈ ℝ) → ((seq1( + , (𝑘 ∈ ℕ ↦ (vol‘((𝐹‘𝑘) ∖ ∪ 𝑚 ∈ (1..^𝑘)(𝐹‘𝑚)))))‘𝑗) = (vol‘(𝐹‘𝑗)) → (seq1( + , (𝑘 ∈ ℕ ↦ (vol‘((𝐹‘𝑘) ∖ ∪ 𝑚 ∈ (1..^𝑘)(𝐹‘𝑚)))))‘(𝑗 + 1)) = (vol‘(𝐹‘(𝑗 + 1))))))
169	168	a2d 29	. . . . . . . . . . 11 ⊢ (𝑗 ∈ ℕ → ((((𝐹:ℕ⟶dom vol ∧ ∀𝑛 ∈ ℕ (𝐹‘𝑛) ⊆ (𝐹‘(𝑛 + 1))) ∧ ∀𝑘 ∈ ℕ (vol‘(𝐹‘𝑘)) ∈ ℝ) → (seq1( + , (𝑘 ∈ ℕ ↦ (vol‘((𝐹‘𝑘) ∖ ∪ 𝑚 ∈ (1..^𝑘)(𝐹‘𝑚)))))‘𝑗) = (vol‘(𝐹‘𝑗))) → (((𝐹:ℕ⟶dom vol ∧ ∀𝑛 ∈ ℕ (𝐹‘𝑛) ⊆ (𝐹‘(𝑛 + 1))) ∧ ∀𝑘 ∈ ℕ (vol‘(𝐹‘𝑘)) ∈ ℝ) → (seq1( + , (𝑘 ∈ ℕ ↦ (vol‘((𝐹‘𝑘) ∖ ∪ 𝑚 ∈ (1..^𝑘)(𝐹‘𝑚)))))‘(𝑗 + 1)) = (vol‘(𝐹‘(𝑗 + 1))))))
170	58, 62, 66, 62, 86, 169	nnind 11991	. . . . . . . . . 10 ⊢ (𝑗 ∈ ℕ → (((𝐹:ℕ⟶dom vol ∧ ∀𝑛 ∈ ℕ (𝐹‘𝑛) ⊆ (𝐹‘(𝑛 + 1))) ∧ ∀𝑘 ∈ ℕ (vol‘(𝐹‘𝑘)) ∈ ℝ) → (seq1( + , (𝑘 ∈ ℕ ↦ (vol‘((𝐹‘𝑘) ∖ ∪ 𝑚 ∈ (1..^𝑘)(𝐹‘𝑚)))))‘𝑗) = (vol‘(𝐹‘𝑗))))
171	170	impcom 408	. . . . . . . . 9 ⊢ ((((𝐹:ℕ⟶dom vol ∧ ∀𝑛 ∈ ℕ (𝐹‘𝑛) ⊆ (𝐹‘(𝑛 + 1))) ∧ ∀𝑘 ∈ ℕ (vol‘(𝐹‘𝑘)) ∈ ℝ) ∧ 𝑗 ∈ ℕ) → (seq1( + , (𝑘 ∈ ℕ ↦ (vol‘((𝐹‘𝑘) ∖ ∪ 𝑚 ∈ (1..^𝑘)(𝐹‘𝑚)))))‘𝑗) = (vol‘(𝐹‘𝑗)))
172		fvco3 6867	. . . . . . . . . 10 ⊢ ((𝐹:ℕ⟶dom vol ∧ 𝑗 ∈ ℕ) → ((vol ∘ 𝐹)‘𝑗) = (vol‘(𝐹‘𝑗)))
173	51, 172	sylan 580	. . . . . . . . 9 ⊢ ((((𝐹:ℕ⟶dom vol ∧ ∀𝑛 ∈ ℕ (𝐹‘𝑛) ⊆ (𝐹‘(𝑛 + 1))) ∧ ∀𝑘 ∈ ℕ (vol‘(𝐹‘𝑘)) ∈ ℝ) ∧ 𝑗 ∈ ℕ) → ((vol ∘ 𝐹)‘𝑗) = (vol‘(𝐹‘𝑗)))
174	171, 173	eqtr4d 2781	. . . . . . . 8 ⊢ ((((𝐹:ℕ⟶dom vol ∧ ∀𝑛 ∈ ℕ (𝐹‘𝑛) ⊆ (𝐹‘(𝑛 + 1))) ∧ ∀𝑘 ∈ ℕ (vol‘(𝐹‘𝑘)) ∈ ℝ) ∧ 𝑗 ∈ ℕ) → (seq1( + , (𝑘 ∈ ℕ ↦ (vol‘((𝐹‘𝑘) ∖ ∪ 𝑚 ∈ (1..^𝑘)(𝐹‘𝑚)))))‘𝑗) = ((vol ∘ 𝐹)‘𝑗))
175	49, 54, 174	eqfnfvd 6912	. . . . . . 7 ⊢ (((𝐹:ℕ⟶dom vol ∧ ∀𝑛 ∈ ℕ (𝐹‘𝑛) ⊆ (𝐹‘(𝑛 + 1))) ∧ ∀𝑘 ∈ ℕ (vol‘(𝐹‘𝑘)) ∈ ℝ) → seq1( + , (𝑘 ∈ ℕ ↦ (vol‘((𝐹‘𝑘) ∖ ∪ 𝑚 ∈ (1..^𝑘)(𝐹‘𝑚))))) = (vol ∘ 𝐹))
176	175	rneqd 5847	. . . . . 6 ⊢ (((𝐹:ℕ⟶dom vol ∧ ∀𝑛 ∈ ℕ (𝐹‘𝑛) ⊆ (𝐹‘(𝑛 + 1))) ∧ ∀𝑘 ∈ ℕ (vol‘(𝐹‘𝑘)) ∈ ℝ) → ran seq1( + , (𝑘 ∈ ℕ ↦ (vol‘((𝐹‘𝑘) ∖ ∪ 𝑚 ∈ (1..^𝑘)(𝐹‘𝑚))))) = ran (vol ∘ 𝐹))
177		rnco2 6157	. . . . . 6 ⊢ ran (vol ∘ 𝐹) = (vol “ ran 𝐹)
178	176, 177	eqtrdi 2794	. . . . 5 ⊢ (((𝐹:ℕ⟶dom vol ∧ ∀𝑛 ∈ ℕ (𝐹‘𝑛) ⊆ (𝐹‘(𝑛 + 1))) ∧ ∀𝑘 ∈ ℕ (vol‘(𝐹‘𝑘)) ∈ ℝ) → ran seq1( + , (𝑘 ∈ ℕ ↦ (vol‘((𝐹‘𝑘) ∖ ∪ 𝑚 ∈ (1..^𝑘)(𝐹‘𝑚))))) = (vol “ ran 𝐹))
179	178	supeq1d 9205	. . . 4 ⊢ (((𝐹:ℕ⟶dom vol ∧ ∀𝑛 ∈ ℕ (𝐹‘𝑛) ⊆ (𝐹‘(𝑛 + 1))) ∧ ∀𝑘 ∈ ℕ (vol‘(𝐹‘𝑘)) ∈ ℝ) → sup(ran seq1( + , (𝑘 ∈ ℕ ↦ (vol‘((𝐹‘𝑘) ∖ ∪ 𝑚 ∈ (1..^𝑘)(𝐹‘𝑚))))), ℝ^, < ) = sup((vol “ ran 𝐹), ℝ^, < ))
180	36, 43, 179	3eqtr3d 2786	. . 3 ⊢ (((𝐹:ℕ⟶dom vol ∧ ∀𝑛 ∈ ℕ (𝐹‘𝑛) ⊆ (𝐹‘(𝑛 + 1))) ∧ ∀𝑘 ∈ ℕ (vol‘(𝐹‘𝑘)) ∈ ℝ) → (vol‘∪ ran 𝐹) = sup((vol “ ran 𝐹), ℝ^*, < ))
181	180	ex 413	. 2 ⊢ ((𝐹:ℕ⟶dom vol ∧ ∀𝑛 ∈ ℕ (𝐹‘𝑛) ⊆ (𝐹‘(𝑛 + 1))) → (∀𝑘 ∈ ℕ (vol‘(𝐹‘𝑘)) ∈ ℝ → (vol‘∪ ran 𝐹) = sup((vol “ ran 𝐹), ℝ^*, < )))
182		rexnal 3169	. . 3 ⊢ (∃𝑘 ∈ ℕ ¬ (vol‘(𝐹‘𝑘)) ∈ ℝ ↔ ¬ ∀𝑘 ∈ ℕ (vol‘(𝐹‘𝑘)) ∈ ℝ)
183		fniunfv 7120	. . . . . . . . . . . 12 ⊢ (𝐹 Fn ℕ → ∪ 𝑛 ∈ ℕ (𝐹‘𝑛) = ∪ ran 𝐹)
184	38, 183	syl 17	. . . . . . . . . . 11 ⊢ (𝐹:ℕ⟶dom vol → ∪ 𝑛 ∈ ℕ (𝐹‘𝑛) = ∪ ran 𝐹)
185		ffvelrn 6959	. . . . . . . . . . . . 13 ⊢ ((𝐹:ℕ⟶dom vol ∧ 𝑛 ∈ ℕ) → (𝐹‘𝑛) ∈ dom vol)
186	185	ralrimiva 3103	. . . . . . . . . . . 12 ⊢ (𝐹:ℕ⟶dom vol → ∀𝑛 ∈ ℕ (𝐹‘𝑛) ∈ dom vol)
187		iunmbl 24717	. . . . . . . . . . . 12 ⊢ (∀𝑛 ∈ ℕ (𝐹‘𝑛) ∈ dom vol → ∪ 𝑛 ∈ ℕ (𝐹‘𝑛) ∈ dom vol)
188	186, 187	syl 17	. . . . . . . . . . 11 ⊢ (𝐹:ℕ⟶dom vol → ∪ 𝑛 ∈ ℕ (𝐹‘𝑛) ∈ dom vol)
189	184, 188	eqeltrrd 2840	. . . . . . . . . 10 ⊢ (𝐹:ℕ⟶dom vol → ∪ ran 𝐹 ∈ dom vol)
190	189	ad2antrr 723	. . . . . . . . 9 ⊢ (((𝐹:ℕ⟶dom vol ∧ ∀𝑛 ∈ ℕ (𝐹‘𝑛) ⊆ (𝐹‘(𝑛 + 1))) ∧ (𝑘 ∈ ℕ ∧ ¬ (vol‘(𝐹‘𝑘)) ∈ ℝ)) → ∪ ran 𝐹 ∈ dom vol)
191		mblss 24695	. . . . . . . . 9 ⊢ (∪ ran 𝐹 ∈ dom vol → ∪ ran 𝐹 ⊆ ℝ)
192	190, 191	syl 17	. . . . . . . 8 ⊢ (((𝐹:ℕ⟶dom vol ∧ ∀𝑛 ∈ ℕ (𝐹‘𝑛) ⊆ (𝐹‘(𝑛 + 1))) ∧ (𝑘 ∈ ℕ ∧ ¬ (vol‘(𝐹‘𝑘)) ∈ ℝ)) → ∪ ran 𝐹 ⊆ ℝ)
193		ovolcl 24642	. . . . . . . 8 ⊢ (∪ ran 𝐹 ⊆ ℝ → (vol‘∪ ran 𝐹) ∈ ℝ^)
194	192, 193	syl 17	. . . . . . 7 ⊢ (((𝐹:ℕ⟶dom vol ∧ ∀𝑛 ∈ ℕ (𝐹‘𝑛) ⊆ (𝐹‘(𝑛 + 1))) ∧ (𝑘 ∈ ℕ ∧ ¬ (vol‘(𝐹‘𝑘)) ∈ ℝ)) → (vol‘∪ ran 𝐹) ∈ ℝ^)
195		pnfge 12866	. . . . . . 7 ⊢ ((vol‘∪ ran 𝐹) ∈ ℝ^ → (vol*‘∪ ran 𝐹) ≤ +∞)
196	194, 195	syl 17	. . . . . 6 ⊢ (((𝐹:ℕ⟶dom vol ∧ ∀𝑛 ∈ ℕ (𝐹‘𝑛) ⊆ (𝐹‘(𝑛 + 1))) ∧ (𝑘 ∈ ℕ ∧ ¬ (vol‘(𝐹‘𝑘)) ∈ ℝ)) → (vol*‘∪ ran 𝐹) ≤ +∞)
197		simprr 770	. . . . . . . . 9 ⊢ (((𝐹:ℕ⟶dom vol ∧ ∀𝑛 ∈ ℕ (𝐹‘𝑛) ⊆ (𝐹‘(𝑛 + 1))) ∧ (𝑘 ∈ ℕ ∧ ¬ (vol‘(𝐹‘𝑘)) ∈ ℝ)) → ¬ (vol‘(𝐹‘𝑘)) ∈ ℝ)
198	1	ad2ant2r 744	. . . . . . . . . . . . 13 ⊢ (((𝐹:ℕ⟶dom vol ∧ ∀𝑛 ∈ ℕ (𝐹‘𝑛) ⊆ (𝐹‘(𝑛 + 1))) ∧ (𝑘 ∈ ℕ ∧ ¬ (vol‘(𝐹‘𝑘)) ∈ ℝ)) → (𝐹‘𝑘) ∈ dom vol)
199	198, 18	syl 17	. . . . . . . . . . . 12 ⊢ (((𝐹:ℕ⟶dom vol ∧ ∀𝑛 ∈ ℕ (𝐹‘𝑛) ⊆ (𝐹‘(𝑛 + 1))) ∧ (𝑘 ∈ ℕ ∧ ¬ (vol‘(𝐹‘𝑘)) ∈ ℝ)) → (𝐹‘𝑘) ⊆ ℝ)
200		ovolcl 24642	. . . . . . . . . . . 12 ⊢ ((𝐹‘𝑘) ⊆ ℝ → (vol‘(𝐹‘𝑘)) ∈ ℝ^)
201	199, 200	syl 17	. . . . . . . . . . 11 ⊢ (((𝐹:ℕ⟶dom vol ∧ ∀𝑛 ∈ ℕ (𝐹‘𝑛) ⊆ (𝐹‘(𝑛 + 1))) ∧ (𝑘 ∈ ℕ ∧ ¬ (vol‘(𝐹‘𝑘)) ∈ ℝ)) → (vol‘(𝐹‘𝑘)) ∈ ℝ^)
202		xrrebnd 12902	. . . . . . . . . . 11 ⊢ ((vol‘(𝐹‘𝑘)) ∈ ℝ^ → ((vol‘(𝐹‘𝑘)) ∈ ℝ ↔ (-∞ < (vol‘(𝐹‘𝑘)) ∧ (vol*‘(𝐹‘𝑘)) < +∞)))
203	201, 202	syl 17	. . . . . . . . . 10 ⊢ (((𝐹:ℕ⟶dom vol ∧ ∀𝑛 ∈ ℕ (𝐹‘𝑛) ⊆ (𝐹‘(𝑛 + 1))) ∧ (𝑘 ∈ ℕ ∧ ¬ (vol‘(𝐹‘𝑘)) ∈ ℝ)) → ((vol‘(𝐹‘𝑘)) ∈ ℝ ↔ (-∞ < (vol‘(𝐹‘𝑘)) ∧ (vol*‘(𝐹‘𝑘)) < +∞)))
204	198, 20	syl 17	. . . . . . . . . . 11 ⊢ (((𝐹:ℕ⟶dom vol ∧ ∀𝑛 ∈ ℕ (𝐹‘𝑛) ⊆ (𝐹‘(𝑛 + 1))) ∧ (𝑘 ∈ ℕ ∧ ¬ (vol‘(𝐹‘𝑘)) ∈ ℝ)) → (vol‘(𝐹‘𝑘)) = (vol*‘(𝐹‘𝑘)))
205	204	eleq1d 2823	. . . . . . . . . 10 ⊢ (((𝐹:ℕ⟶dom vol ∧ ∀𝑛 ∈ ℕ (𝐹‘𝑛) ⊆ (𝐹‘(𝑛 + 1))) ∧ (𝑘 ∈ ℕ ∧ ¬ (vol‘(𝐹‘𝑘)) ∈ ℝ)) → ((vol‘(𝐹‘𝑘)) ∈ ℝ ↔ (vol*‘(𝐹‘𝑘)) ∈ ℝ))
206		ovolge0 24645	. . . . . . . . . . . . 13 ⊢ ((𝐹‘𝑘) ⊆ ℝ → 0 ≤ (vol*‘(𝐹‘𝑘)))
207		mnflt0 12861	. . . . . . . . . . . . . 14 ⊢ -∞ < 0
208		mnfxr 11032	. . . . . . . . . . . . . . 15 ⊢ -∞ ∈ ℝ^*
209		0xr 11022	. . . . . . . . . . . . . . 15 ⊢ 0 ∈ ℝ^*
210		xrltletr 12891	. . . . . . . . . . . . . . 15 ⊢ ((-∞ ∈ ℝ^* ∧ 0 ∈ ℝ^* ∧ (vol‘(𝐹‘𝑘)) ∈ ℝ^) → ((-∞ < 0 ∧ 0 ≤ (vol‘(𝐹‘𝑘))) → -∞ < (vol‘(𝐹‘𝑘))))
211	208, 209, 210	mp3an12 1450	. . . . . . . . . . . . . 14 ⊢ ((vol‘(𝐹‘𝑘)) ∈ ℝ^ → ((-∞ < 0 ∧ 0 ≤ (vol‘(𝐹‘𝑘))) → -∞ < (vol‘(𝐹‘𝑘))))
212	207, 211	mpani 693	. . . . . . . . . . . . 13 ⊢ ((vol‘(𝐹‘𝑘)) ∈ ℝ^ → (0 ≤ (vol‘(𝐹‘𝑘)) → -∞ < (vol‘(𝐹‘𝑘))))
213	200, 206, 212	sylc 65	. . . . . . . . . . . 12 ⊢ ((𝐹‘𝑘) ⊆ ℝ → -∞ < (vol*‘(𝐹‘𝑘)))
214	199, 213	syl 17	. . . . . . . . . . 11 ⊢ (((𝐹:ℕ⟶dom vol ∧ ∀𝑛 ∈ ℕ (𝐹‘𝑛) ⊆ (𝐹‘(𝑛 + 1))) ∧ (𝑘 ∈ ℕ ∧ ¬ (vol‘(𝐹‘𝑘)) ∈ ℝ)) → -∞ < (vol*‘(𝐹‘𝑘)))
215	214	biantrurd 533	. . . . . . . . . 10 ⊢ (((𝐹:ℕ⟶dom vol ∧ ∀𝑛 ∈ ℕ (𝐹‘𝑛) ⊆ (𝐹‘(𝑛 + 1))) ∧ (𝑘 ∈ ℕ ∧ ¬ (vol‘(𝐹‘𝑘)) ∈ ℝ)) → ((vol‘(𝐹‘𝑘)) < +∞ ↔ (-∞ < (vol‘(𝐹‘𝑘)) ∧ (vol*‘(𝐹‘𝑘)) < +∞)))
216	203, 205, 215	3bitr4d 311	. . . . . . . . 9 ⊢ (((𝐹:ℕ⟶dom vol ∧ ∀𝑛 ∈ ℕ (𝐹‘𝑛) ⊆ (𝐹‘(𝑛 + 1))) ∧ (𝑘 ∈ ℕ ∧ ¬ (vol‘(𝐹‘𝑘)) ∈ ℝ)) → ((vol‘(𝐹‘𝑘)) ∈ ℝ ↔ (vol*‘(𝐹‘𝑘)) < +∞))
217	197, 216	mtbid 324	. . . . . . . 8 ⊢ (((𝐹:ℕ⟶dom vol ∧ ∀𝑛 ∈ ℕ (𝐹‘𝑛) ⊆ (𝐹‘(𝑛 + 1))) ∧ (𝑘 ∈ ℕ ∧ ¬ (vol‘(𝐹‘𝑘)) ∈ ℝ)) → ¬ (vol*‘(𝐹‘𝑘)) < +∞)
218		nltpnft 12898	. . . . . . . . 9 ⊢ ((vol‘(𝐹‘𝑘)) ∈ ℝ^ → ((vol‘(𝐹‘𝑘)) = +∞ ↔ ¬ (vol‘(𝐹‘𝑘)) < +∞))
219	201, 218	syl 17	. . . . . . . 8 ⊢ (((𝐹:ℕ⟶dom vol ∧ ∀𝑛 ∈ ℕ (𝐹‘𝑛) ⊆ (𝐹‘(𝑛 + 1))) ∧ (𝑘 ∈ ℕ ∧ ¬ (vol‘(𝐹‘𝑘)) ∈ ℝ)) → ((vol‘(𝐹‘𝑘)) = +∞ ↔ ¬ (vol‘(𝐹‘𝑘)) < +∞))
220	217, 219	mpbird 256	. . . . . . 7 ⊢ (((𝐹:ℕ⟶dom vol ∧ ∀𝑛 ∈ ℕ (𝐹‘𝑛) ⊆ (𝐹‘(𝑛 + 1))) ∧ (𝑘 ∈ ℕ ∧ ¬ (vol‘(𝐹‘𝑘)) ∈ ℝ)) → (vol*‘(𝐹‘𝑘)) = +∞)
221	38	ad2antrr 723	. . . . . . . . . 10 ⊢ (((𝐹:ℕ⟶dom vol ∧ ∀𝑛 ∈ ℕ (𝐹‘𝑛) ⊆ (𝐹‘(𝑛 + 1))) ∧ (𝑘 ∈ ℕ ∧ ¬ (vol‘(𝐹‘𝑘)) ∈ ℝ)) → 𝐹 Fn ℕ)
222		simprl 768	. . . . . . . . . 10 ⊢ (((𝐹:ℕ⟶dom vol ∧ ∀𝑛 ∈ ℕ (𝐹‘𝑛) ⊆ (𝐹‘(𝑛 + 1))) ∧ (𝑘 ∈ ℕ ∧ ¬ (vol‘(𝐹‘𝑘)) ∈ ℝ)) → 𝑘 ∈ ℕ)
223		fnfvelrn 6958	. . . . . . . . . 10 ⊢ ((𝐹 Fn ℕ ∧ 𝑘 ∈ ℕ) → (𝐹‘𝑘) ∈ ran 𝐹)
224	221, 222, 223	syl2anc 584	. . . . . . . . 9 ⊢ (((𝐹:ℕ⟶dom vol ∧ ∀𝑛 ∈ ℕ (𝐹‘𝑛) ⊆ (𝐹‘(𝑛 + 1))) ∧ (𝑘 ∈ ℕ ∧ ¬ (vol‘(𝐹‘𝑘)) ∈ ℝ)) → (𝐹‘𝑘) ∈ ran 𝐹)
225		elssuni 4871	. . . . . . . . 9 ⊢ ((𝐹‘𝑘) ∈ ran 𝐹 → (𝐹‘𝑘) ⊆ ∪ ran 𝐹)
226	224, 225	syl 17	. . . . . . . 8 ⊢ (((𝐹:ℕ⟶dom vol ∧ ∀𝑛 ∈ ℕ (𝐹‘𝑛) ⊆ (𝐹‘(𝑛 + 1))) ∧ (𝑘 ∈ ℕ ∧ ¬ (vol‘(𝐹‘𝑘)) ∈ ℝ)) → (𝐹‘𝑘) ⊆ ∪ ran 𝐹)
227		ovolss 24649	. . . . . . . 8 ⊢ (((𝐹‘𝑘) ⊆ ∪ ran 𝐹 ∧ ∪ ran 𝐹 ⊆ ℝ) → (vol‘(𝐹‘𝑘)) ≤ (vol‘∪ ran 𝐹))
228	226, 192, 227	syl2anc 584	. . . . . . 7 ⊢ (((𝐹:ℕ⟶dom vol ∧ ∀𝑛 ∈ ℕ (𝐹‘𝑛) ⊆ (𝐹‘(𝑛 + 1))) ∧ (𝑘 ∈ ℕ ∧ ¬ (vol‘(𝐹‘𝑘)) ∈ ℝ)) → (vol‘(𝐹‘𝑘)) ≤ (vol‘∪ ran 𝐹))
229	220, 228	eqbrtrrd 5098	. . . . . 6 ⊢ (((𝐹:ℕ⟶dom vol ∧ ∀𝑛 ∈ ℕ (𝐹‘𝑛) ⊆ (𝐹‘(𝑛 + 1))) ∧ (𝑘 ∈ ℕ ∧ ¬ (vol‘(𝐹‘𝑘)) ∈ ℝ)) → +∞ ≤ (vol*‘∪ ran 𝐹))
230		pnfxr 11029	. . . . . . 7 ⊢ +∞ ∈ ℝ^*
231		xrletri3 12888	. . . . . . 7 ⊢ (((vol‘∪ ran 𝐹) ∈ ℝ^ ∧ +∞ ∈ ℝ^) → ((vol‘∪ ran 𝐹) = +∞ ↔ ((vol‘∪ ran 𝐹) ≤ +∞ ∧ +∞ ≤ (vol‘∪ ran 𝐹))))
232	194, 230, 231	sylancl 586	. . . . . 6 ⊢ (((𝐹:ℕ⟶dom vol ∧ ∀𝑛 ∈ ℕ (𝐹‘𝑛) ⊆ (𝐹‘(𝑛 + 1))) ∧ (𝑘 ∈ ℕ ∧ ¬ (vol‘(𝐹‘𝑘)) ∈ ℝ)) → ((vol‘∪ ran 𝐹) = +∞ ↔ ((vol‘∪ ran 𝐹) ≤ +∞ ∧ +∞ ≤ (vol*‘∪ ran 𝐹))))
233	196, 229, 232	mpbir2and 710	. . . . 5 ⊢ (((𝐹:ℕ⟶dom vol ∧ ∀𝑛 ∈ ℕ (𝐹‘𝑛) ⊆ (𝐹‘(𝑛 + 1))) ∧ (𝑘 ∈ ℕ ∧ ¬ (vol‘(𝐹‘𝑘)) ∈ ℝ)) → (vol*‘∪ ran 𝐹) = +∞)
234		mblvol 24694	. . . . . 6 ⊢ (∪ ran 𝐹 ∈ dom vol → (vol‘∪ ran 𝐹) = (vol*‘∪ ran 𝐹))
235	190, 234	syl 17	. . . . 5 ⊢ (((𝐹:ℕ⟶dom vol ∧ ∀𝑛 ∈ ℕ (𝐹‘𝑛) ⊆ (𝐹‘(𝑛 + 1))) ∧ (𝑘 ∈ ℕ ∧ ¬ (vol‘(𝐹‘𝑘)) ∈ ℝ)) → (vol‘∪ ran 𝐹) = (vol*‘∪ ran 𝐹))
236		imassrn 5980	. . . . . . 7 ⊢ (vol “ ran 𝐹) ⊆ ran vol
237		frn 6607	. . . . . . . . 9 ⊢ (vol:dom vol⟶(0[,]+∞) → ran vol ⊆ (0[,]+∞))
238	50, 237	ax-mp 5	. . . . . . . 8 ⊢ ran vol ⊆ (0[,]+∞)
239		iccssxr 13162	. . . . . . . 8 ⊢ (0[,]+∞) ⊆ ℝ^*
240	238, 239	sstri 3930	. . . . . . 7 ⊢ ran vol ⊆ ℝ^*
241	236, 240	sstri 3930	. . . . . 6 ⊢ (vol “ ran 𝐹) ⊆ ℝ^*
242	204, 220	eqtrd 2778	. . . . . . 7 ⊢ (((𝐹:ℕ⟶dom vol ∧ ∀𝑛 ∈ ℕ (𝐹‘𝑛) ⊆ (𝐹‘(𝑛 + 1))) ∧ (𝑘 ∈ ℕ ∧ ¬ (vol‘(𝐹‘𝑘)) ∈ ℝ)) → (vol‘(𝐹‘𝑘)) = +∞)
243		simpll 764	. . . . . . . 8 ⊢ (((𝐹:ℕ⟶dom vol ∧ ∀𝑛 ∈ ℕ (𝐹‘𝑛) ⊆ (𝐹‘(𝑛 + 1))) ∧ (𝑘 ∈ ℕ ∧ ¬ (vol‘(𝐹‘𝑘)) ∈ ℝ)) → 𝐹:ℕ⟶dom vol)
244		ffun 6603	. . . . . . . . . 10 ⊢ (vol:dom vol⟶(0[,]+∞) → Fun vol)
245	50, 244	ax-mp 5	. . . . . . . . 9 ⊢ Fun vol
246		frn 6607	. . . . . . . . 9 ⊢ (𝐹:ℕ⟶dom vol → ran 𝐹 ⊆ dom vol)
247		funfvima2 7107	. . . . . . . . 9 ⊢ ((Fun vol ∧ ran 𝐹 ⊆ dom vol) → ((𝐹‘𝑘) ∈ ran 𝐹 → (vol‘(𝐹‘𝑘)) ∈ (vol “ ran 𝐹)))
248	245, 246, 247	sylancr 587	. . . . . . . 8 ⊢ (𝐹:ℕ⟶dom vol → ((𝐹‘𝑘) ∈ ran 𝐹 → (vol‘(𝐹‘𝑘)) ∈ (vol “ ran 𝐹)))
249	243, 224, 248	sylc 65	. . . . . . 7 ⊢ (((𝐹:ℕ⟶dom vol ∧ ∀𝑛 ∈ ℕ (𝐹‘𝑛) ⊆ (𝐹‘(𝑛 + 1))) ∧ (𝑘 ∈ ℕ ∧ ¬ (vol‘(𝐹‘𝑘)) ∈ ℝ)) → (vol‘(𝐹‘𝑘)) ∈ (vol “ ran 𝐹))
250	242, 249	eqeltrrd 2840	. . . . . 6 ⊢ (((𝐹:ℕ⟶dom vol ∧ ∀𝑛 ∈ ℕ (𝐹‘𝑛) ⊆ (𝐹‘(𝑛 + 1))) ∧ (𝑘 ∈ ℕ ∧ ¬ (vol‘(𝐹‘𝑘)) ∈ ℝ)) → +∞ ∈ (vol “ ran 𝐹))
251		supxrpnf 13052	. . . . . 6 ⊢ (((vol “ ran 𝐹) ⊆ ℝ^* ∧ +∞ ∈ (vol “ ran 𝐹)) → sup((vol “ ran 𝐹), ℝ^*, < ) = +∞)
252	241, 250, 251	sylancr 587	. . . . 5 ⊢ (((𝐹:ℕ⟶dom vol ∧ ∀𝑛 ∈ ℕ (𝐹‘𝑛) ⊆ (𝐹‘(𝑛 + 1))) ∧ (𝑘 ∈ ℕ ∧ ¬ (vol‘(𝐹‘𝑘)) ∈ ℝ)) → sup((vol “ ran 𝐹), ℝ^*, < ) = +∞)
253	233, 235, 252	3eqtr4d 2788	. . . 4 ⊢ (((𝐹:ℕ⟶dom vol ∧ ∀𝑛 ∈ ℕ (𝐹‘𝑛) ⊆ (𝐹‘(𝑛 + 1))) ∧ (𝑘 ∈ ℕ ∧ ¬ (vol‘(𝐹‘𝑘)) ∈ ℝ)) → (vol‘∪ ran 𝐹) = sup((vol “ ran 𝐹), ℝ^*, < ))
254	253	rexlimdvaa 3214	. . 3 ⊢ ((𝐹:ℕ⟶dom vol ∧ ∀𝑛 ∈ ℕ (𝐹‘𝑛) ⊆ (𝐹‘(𝑛 + 1))) → (∃𝑘 ∈ ℕ ¬ (vol‘(𝐹‘𝑘)) ∈ ℝ → (vol‘∪ ran 𝐹) = sup((vol “ ran 𝐹), ℝ^*, < )))
255	182, 254	syl5bir 242	. 2 ⊢ ((𝐹:ℕ⟶dom vol ∧ ∀𝑛 ∈ ℕ (𝐹‘𝑛) ⊆ (𝐹‘(𝑛 + 1))) → (¬ ∀𝑘 ∈ ℕ (vol‘(𝐹‘𝑘)) ∈ ℝ → (vol‘∪ ran 𝐹) = sup((vol “ ran 𝐹), ℝ^*, < )))
256	181, 255	pm2.61d 179	1 ⊢ ((𝐹:ℕ⟶dom vol ∧ ∀𝑛 ∈ ℕ (𝐹‘𝑛) ⊆ (𝐹‘(𝑛 + 1))) → (vol‘∪ ran 𝐹) = sup((vol “ ran 𝐹), ℝ^*, < ))

Colors of variables: wff setvar class

Syntax hints: ¬ wn 3 → wi 4 ↔ wb 205 ∧ wa 396 = wceq 1539 ∈ wcel 2106 ∀wral 3064 ∃wrex 3065 ∖ cdif 3884 ∪ cun 3885 ∩ cin 3886 ⊆ wss 3887 ∅c0 4256 ∪ cuni 4839 ∪ ciun 4924 Disj wdisj 5039 class class class wbr 5074 ↦ cmpt 5157 dom cdm 5589 ran crn 5590 “ cima 5592 ∘ ccom 5593 Fun wfun 6427 Fn wfn 6428 ⟶wf 6429 ‘cfv 6433 (class class class)co 7275 Fincfn 8733 supcsup 9199 ℝcr 10870 0cc0 10871 1c1 10872 + caddc 10874 +∞cpnf 11006 -∞cmnf 11007 ℝ^*cxr 11008 < clt 11009 ≤ cle 11010 ℕcn 11973 ℤcz 12319 ℤ_≥cuz 12582 [,]cicc 13082 ...cfz 13239 ..^cfzo 13382 seqcseq 13721 vol*covol 24626 volcvol 24627

This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1798 ax-4 1812 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 2709 ax-rep 5209 ax-sep 5223 ax-nul 5230 ax-pow 5288 ax-pr 5352 ax-un 7588 ax-inf2 9399 ax-cc 10191 ax-cnex 10927 ax-resscn 10928 ax-1cn 10929 ax-icn 10930 ax-addcl 10931 ax-addrcl 10932 ax-mulcl 10933 ax-mulrcl 10934 ax-mulcom 10935 ax-addass 10936 ax-mulass 10937 ax-distr 10938 ax-i2m1 10939 ax-1ne0 10940 ax-1rid 10941 ax-rnegex 10942 ax-rrecex 10943 ax-cnre 10944 ax-pre-lttri 10945 ax-pre-lttrn 10946 ax-pre-ltadd 10947 ax-pre-mulgt0 10948 ax-pre-sup 10949

This theorem depends on definitions: df-bi 206 df-an 397 df-or 845 df-3or 1087 df-3an 1088 df-tru 1542 df-fal 1552 df-ex 1783 df-nf 1787 df-sb 2068 df-mo 2540 df-eu 2569 df-clab 2716 df-cleq 2730 df-clel 2816 df-nfc 2889 df-ne 2944 df-nel 3050 df-ral 3069 df-rex 3070 df-rmo 3071 df-reu 3072 df-rab 3073 df-v 3434 df-sbc 3717 df-csb 3833 df-dif 3890 df-un 3892 df-in 3894 df-ss 3904 df-pss 3906 df-nul 4257 df-if 4460 df-pw 4535 df-sn 4562 df-pr 4564 df-op 4568 df-uni 4840 df-int 4880 df-iun 4926 df-disj 5040 df-br 5075 df-opab 5137 df-mpt 5158 df-tr 5192 df-id 5489 df-eprel 5495 df-po 5503 df-so 5504 df-fr 5544 df-se 5545 df-we 5546 df-xp 5595 df-rel 5596 df-cnv 5597 df-co 5598 df-dm 5599 df-rn 5600 df-res 5601 df-ima 5602 df-pred 6202 df-ord 6269 df-on 6270 df-lim 6271 df-suc 6272 df-iota 6391 df-fun 6435 df-fn 6436 df-f 6437 df-f1 6438 df-fo 6439 df-f1o 6440 df-fv 6441 df-isom 6442 df-riota 7232 df-ov 7278 df-oprab 7279 df-mpo 7280 df-of 7533 df-om 7713 df-1st 7831 df-2nd 7832 df-frecs 8097 df-wrecs 8128 df-recs 8202 df-rdg 8241 df-1o 8297 df-2o 8298 df-er 8498 df-map 8617 df-pm 8618 df-en 8734 df-dom 8735 df-sdom 8736 df-fin 8737 df-sup 9201 df-inf 9202 df-oi 9269 df-dju 9659 df-card 9697 df-pnf 11011 df-mnf 11012 df-xr 11013 df-ltxr 11014 df-le 11015 df-sub 11207 df-neg 11208 df-div 11633 df-nn 11974 df-2 12036 df-3 12037 df-n0 12234 df-z 12320 df-uz 12583 df-q 12689 df-rp 12731 df-xadd 12849 df-ioo 13083 df-ico 13085 df-icc 13086 df-fz 13240 df-fzo 13383 df-fl 13512 df-seq 13722 df-exp 13783 df-hash 14045 df-cj 14810 df-re 14811 df-im 14812 df-sqrt 14946 df-abs 14947 df-clim 15197 df-rlim 15198 df-sum 15398 df-xmet 20590 df-met 20591 df-ovol 24628 df-vol 24629

This theorem is referenced by: volsup2 24769 itg1climres 24879 itg2gt0 24925

W3C validator