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 25484

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		ffvelcdm 7014	. . . . . . . . . . 11 ⊢ ((𝐹:ℕ⟶dom vol ∧ 𝑘 ∈ ℕ) → (𝐹‘𝑘) ∈ dom vol)
2	1	ad2ant2r 747	. . . . . . . . . 10 ⊢ (((𝐹:ℕ⟶dom vol ∧ ∀𝑛 ∈ ℕ (𝐹‘𝑛) ⊆ (𝐹‘(𝑛 + 1))) ∧ (𝑘 ∈ ℕ ∧ (vol‘(𝐹‘𝑘)) ∈ ℝ)) → (𝐹‘𝑘) ∈ dom vol)
3		fzofi 13881	. . . . . . . . . . 11 ⊢ (1..^𝑘) ∈ Fin
4		simpll 766	. . . . . . . . . . . . 13 ⊢ (((𝐹:ℕ⟶dom vol ∧ ∀𝑛 ∈ ℕ (𝐹‘𝑛) ⊆ (𝐹‘(𝑛 + 1))) ∧ (𝑘 ∈ ℕ ∧ (vol‘(𝐹‘𝑘)) ∈ ℝ)) → 𝐹:ℕ⟶dom vol)
5		elfzouz 13563	. . . . . . . . . . . . . 14 ⊢ (𝑚 ∈ (1..^𝑘) → 𝑚 ∈ (ℤ_≥‘1))
6		nnuz 12775	. . . . . . . . . . . . . 14 ⊢ ℕ = (ℤ_≥‘1)
7	5, 6	eleqtrrdi 2842	. . . . . . . . . . . . 13 ⊢ (𝑚 ∈ (1..^𝑘) → 𝑚 ∈ ℕ)
8		ffvelcdm 7014	. . . . . . . . . . . . 13 ⊢ ((𝐹:ℕ⟶dom vol ∧ 𝑚 ∈ ℕ) → (𝐹‘𝑚) ∈ dom vol)
9	4, 7, 8	syl2an 596	. . . . . . . . . . . 12 ⊢ ((((𝐹:ℕ⟶dom vol ∧ ∀𝑛 ∈ ℕ (𝐹‘𝑛) ⊆ (𝐹‘(𝑛 + 1))) ∧ (𝑘 ∈ ℕ ∧ (vol‘(𝐹‘𝑘)) ∈ ℝ)) ∧ 𝑚 ∈ (1..^𝑘)) → (𝐹‘𝑚) ∈ dom vol)
10	9	ralrimiva 3124	. . . . . . . . . . 11 ⊢ (((𝐹:ℕ⟶dom vol ∧ ∀𝑛 ∈ ℕ (𝐹‘𝑛) ⊆ (𝐹‘(𝑛 + 1))) ∧ (𝑘 ∈ ℕ ∧ (vol‘(𝐹‘𝑘)) ∈ ℝ)) → ∀𝑚 ∈ (1..^𝑘)(𝐹‘𝑚) ∈ dom vol)
11		finiunmbl 25472	. . . . . . . . . . 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 25471	. . . . . . . . . 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 25458	. . . . . . . . . . 11 ⊢ (((𝐹‘𝑘) ∖ ∪ 𝑚 ∈ (1..^𝑘)(𝐹‘𝑚)) ∈ dom vol → (vol‘((𝐹‘𝑘) ∖ ∪ 𝑚 ∈ (1..^𝑘)(𝐹‘𝑚))) = (vol*‘((𝐹‘𝑘) ∖ ∪ 𝑚 ∈ (1..^𝑘)(𝐹‘𝑚))))
16	14, 15	syl 17	. . . . . . . . . 10 ⊢ (((𝐹:ℕ⟶dom vol ∧ ∀𝑛 ∈ ℕ (𝐹‘𝑛) ⊆ (𝐹‘(𝑛 + 1))) ∧ (𝑘 ∈ ℕ ∧ (vol‘(𝐹‘𝑘)) ∈ ℝ)) → (vol‘((𝐹‘𝑘) ∖ ∪ 𝑚 ∈ (1..^𝑘)(𝐹‘𝑚))) = (vol*‘((𝐹‘𝑘) ∖ ∪ 𝑚 ∈ (1..^𝑘)(𝐹‘𝑚))))
17		difssd 4084	. . . . . . . . . . 11 ⊢ (((𝐹:ℕ⟶dom vol ∧ ∀𝑛 ∈ ℕ (𝐹‘𝑛) ⊆ (𝐹‘(𝑛 + 1))) ∧ (𝑘 ∈ ℕ ∧ (vol‘(𝐹‘𝑘)) ∈ ℝ)) → ((𝐹‘𝑘) ∖ ∪ 𝑚 ∈ (1..^𝑘)(𝐹‘𝑚)) ⊆ (𝐹‘𝑘))
18		mblss 25459	. . . . . . . . . . . 12 ⊢ ((𝐹‘𝑘) ∈ dom vol → (𝐹‘𝑘) ⊆ ℝ)
19	2, 18	syl 17	. . . . . . . . . . 11 ⊢ (((𝐹:ℕ⟶dom vol ∧ ∀𝑛 ∈ ℕ (𝐹‘𝑛) ⊆ (𝐹‘(𝑛 + 1))) ∧ (𝑘 ∈ ℕ ∧ (vol‘(𝐹‘𝑘)) ∈ ℝ)) → (𝐹‘𝑘) ⊆ ℝ)
20		mblvol 25458	. . . . . . . . . . . . 13 ⊢ ((𝐹‘𝑘) ∈ dom vol → (vol‘(𝐹‘𝑘)) = (vol*‘(𝐹‘𝑘)))
21	2, 20	syl 17	. . . . . . . . . . . 12 ⊢ (((𝐹:ℕ⟶dom vol ∧ ∀𝑛 ∈ ℕ (𝐹‘𝑛) ⊆ (𝐹‘(𝑛 + 1))) ∧ (𝑘 ∈ ℕ ∧ (vol‘(𝐹‘𝑘)) ∈ ℝ)) → (vol‘(𝐹‘𝑘)) = (vol*‘(𝐹‘𝑘)))
22		simprr 772	. . . . . . . . . . . 12 ⊢ (((𝐹:ℕ⟶dom vol ∧ ∀𝑛 ∈ ℕ (𝐹‘𝑛) ⊆ (𝐹‘(𝑛 + 1))) ∧ (𝑘 ∈ ℕ ∧ (vol‘(𝐹‘𝑘)) ∈ ℝ)) → (vol‘(𝐹‘𝑘)) ∈ ℝ)
23	21, 22	eqeltrrd 2832	. . . . . . . . . . 11 ⊢ (((𝐹:ℕ⟶dom vol ∧ ∀𝑛 ∈ ℕ (𝐹‘𝑛) ⊆ (𝐹‘(𝑛 + 1))) ∧ (𝑘 ∈ ℕ ∧ (vol‘(𝐹‘𝑘)) ∈ ℝ)) → (vol*‘(𝐹‘𝑘)) ∈ ℝ)
24		ovolsscl 25414	. . . . . . . . . . 11 ⊢ ((((𝐹‘𝑘) ∖ ∪ 𝑚 ∈ (1..^𝑘)(𝐹‘𝑚)) ⊆ (𝐹‘𝑘) ∧ (𝐹‘𝑘) ⊆ ℝ ∧ (vol‘(𝐹‘𝑘)) ∈ ℝ) → (vol‘((𝐹‘𝑘) ∖ ∪ 𝑚 ∈ (1..^𝑘)(𝐹‘𝑚))) ∈ ℝ)
25	17, 19, 23, 24	syl3anc 1373	. . . . . . . . . 10 ⊢ (((𝐹:ℕ⟶dom vol ∧ ∀𝑛 ∈ ℕ (𝐹‘𝑛) ⊆ (𝐹‘(𝑛 + 1))) ∧ (𝑘 ∈ ℕ ∧ (vol‘(𝐹‘𝑘)) ∈ ℝ)) → (vol*‘((𝐹‘𝑘) ∖ ∪ 𝑚 ∈ (1..^𝑘)(𝐹‘𝑚))) ∈ ℝ)
26	16, 25	eqeltrd 2831	. . . . . . . . 9 ⊢ (((𝐹:ℕ⟶dom vol ∧ ∀𝑛 ∈ ℕ (𝐹‘𝑛) ⊆ (𝐹‘(𝑛 + 1))) ∧ (𝑘 ∈ ℕ ∧ (vol‘(𝐹‘𝑘)) ∈ ℝ)) → (vol‘((𝐹‘𝑘) ∖ ∪ 𝑚 ∈ (1..^𝑘)(𝐹‘𝑚))) ∈ ℝ)
27	14, 26	jca 511	. . . . . . . 8 ⊢ (((𝐹:ℕ⟶dom vol ∧ ∀𝑛 ∈ ℕ (𝐹‘𝑛) ⊆ (𝐹‘(𝑛 + 1))) ∧ (𝑘 ∈ ℕ ∧ (vol‘(𝐹‘𝑘)) ∈ ℝ)) → (((𝐹‘𝑘) ∖ ∪ 𝑚 ∈ (1..^𝑘)(𝐹‘𝑚)) ∈ dom vol ∧ (vol‘((𝐹‘𝑘) ∖ ∪ 𝑚 ∈ (1..^𝑘)(𝐹‘𝑚))) ∈ ℝ))
28	27	expr 456	. . . . . . 7 ⊢ (((𝐹:ℕ⟶dom vol ∧ ∀𝑛 ∈ ℕ (𝐹‘𝑛) ⊆ (𝐹‘(𝑛 + 1))) ∧ 𝑘 ∈ ℕ) → ((vol‘(𝐹‘𝑘)) ∈ ℝ → (((𝐹‘𝑘) ∖ ∪ 𝑚 ∈ (1..^𝑘)(𝐹‘𝑚)) ∈ dom vol ∧ (vol‘((𝐹‘𝑘) ∖ ∪ 𝑚 ∈ (1..^𝑘)(𝐹‘𝑚))) ∈ ℝ)))
29	28	ralimdva 3144	. . . . . 6 ⊢ ((𝐹:ℕ⟶dom vol ∧ ∀𝑛 ∈ ℕ (𝐹‘𝑛) ⊆ (𝐹‘(𝑛 + 1))) → (∀𝑘 ∈ ℕ (vol‘(𝐹‘𝑘)) ∈ ℝ → ∀𝑘 ∈ ℕ (((𝐹‘𝑘) ∖ ∪ 𝑚 ∈ (1..^𝑘)(𝐹‘𝑚)) ∈ dom vol ∧ (vol‘((𝐹‘𝑘) ∖ ∪ 𝑚 ∈ (1..^𝑘)(𝐹‘𝑚))) ∈ ℝ)))
30	29	imp 406	. . . . 5 ⊢ (((𝐹:ℕ⟶dom vol ∧ ∀𝑛 ∈ ℕ (𝐹‘𝑛) ⊆ (𝐹‘(𝑛 + 1))) ∧ ∀𝑘 ∈ ℕ (vol‘(𝐹‘𝑘)) ∈ ℝ) → ∀𝑘 ∈ ℕ (((𝐹‘𝑘) ∖ ∪ 𝑚 ∈ (1..^𝑘)(𝐹‘𝑚)) ∈ dom vol ∧ (vol‘((𝐹‘𝑘) ∖ ∪ 𝑚 ∈ (1..^𝑘)(𝐹‘𝑚))) ∈ ℝ))
31		fveq2 6822	. . . . . 6 ⊢ (𝑘 = 𝑚 → (𝐹‘𝑘) = (𝐹‘𝑚))
32	31	iundisj2 25477	. . . . 5 ⊢ Disj 𝑘 ∈ ℕ ((𝐹‘𝑘) ∖ ∪ 𝑚 ∈ (1..^𝑘)(𝐹‘𝑚))
33		eqid 2731	. . . . . 6 ⊢ seq1( + , (𝑘 ∈ ℕ ↦ (vol‘((𝐹‘𝑘) ∖ ∪ 𝑚 ∈ (1..^𝑘)(𝐹‘𝑚))))) = seq1( + , (𝑘 ∈ ℕ ↦ (vol‘((𝐹‘𝑘) ∖ ∪ 𝑚 ∈ (1..^𝑘)(𝐹‘𝑚)))))
34		eqid 2731	. . . . . 6 ⊢ (𝑘 ∈ ℕ ↦ (vol‘((𝐹‘𝑘) ∖ ∪ 𝑚 ∈ (1..^𝑘)(𝐹‘𝑚)))) = (𝑘 ∈ ℕ ↦ (vol‘((𝐹‘𝑘) ∖ ∪ 𝑚 ∈ (1..^𝑘)(𝐹‘𝑚))))
35	33, 34	voliun 25482	. . . . 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 25476	. . . . . 6 ⊢ ∪ 𝑘 ∈ ℕ (𝐹‘𝑘) = ∪ 𝑘 ∈ ℕ ((𝐹‘𝑘) ∖ ∪ 𝑚 ∈ (1..^𝑘)(𝐹‘𝑚))
38		ffn 6651	. . . . . . . 8 ⊢ (𝐹:ℕ⟶dom vol → 𝐹 Fn ℕ)
39	38	ad2antrr 726	. . . . . . 7 ⊢ (((𝐹:ℕ⟶dom vol ∧ ∀𝑛 ∈ ℕ (𝐹‘𝑛) ⊆ (𝐹‘(𝑛 + 1))) ∧ ∀𝑘 ∈ ℕ (vol‘(𝐹‘𝑘)) ∈ ℝ) → 𝐹 Fn ℕ)
40		fniunfv 7181	. . . . . . 7 ⊢ (𝐹 Fn ℕ → ∪ 𝑘 ∈ ℕ (𝐹‘𝑘) = ∪ ran 𝐹)
41	39, 40	syl 17	. . . . . 6 ⊢ (((𝐹:ℕ⟶dom vol ∧ ∀𝑛 ∈ ℕ (𝐹‘𝑛) ⊆ (𝐹‘(𝑛 + 1))) ∧ ∀𝑘 ∈ ℕ (vol‘(𝐹‘𝑘)) ∈ ℝ) → ∪ 𝑘 ∈ ℕ (𝐹‘𝑘) = ∪ ran 𝐹)
42	37, 41	eqtr3id 2780	. . . . 5 ⊢ (((𝐹:ℕ⟶dom vol ∧ ∀𝑛 ∈ ℕ (𝐹‘𝑛) ⊆ (𝐹‘(𝑛 + 1))) ∧ ∀𝑘 ∈ ℕ (vol‘(𝐹‘𝑘)) ∈ ℝ) → ∪ 𝑘 ∈ ℕ ((𝐹‘𝑘) ∖ ∪ 𝑚 ∈ (1..^𝑘)(𝐹‘𝑚)) = ∪ ran 𝐹)
43	42	fveq2d 6826	. . . 4 ⊢ (((𝐹:ℕ⟶dom vol ∧ ∀𝑛 ∈ ℕ (𝐹‘𝑛) ⊆ (𝐹‘(𝑛 + 1))) ∧ ∀𝑘 ∈ ℕ (vol‘(𝐹‘𝑘)) ∈ ℝ) → (vol‘∪ 𝑘 ∈ ℕ ((𝐹‘𝑘) ∖ ∪ 𝑚 ∈ (1..^𝑘)(𝐹‘𝑚))) = (vol‘∪ ran 𝐹))
44		1z 12502	. . . . . . . . . . 11 ⊢ 1 ∈ ℤ
45		seqfn 13920	. . . . . . . . . . 11 ⊢ (1 ∈ ℤ → seq1( + , (𝑘 ∈ ℕ ↦ (vol‘((𝐹‘𝑘) ∖ ∪ 𝑚 ∈ (1..^𝑘)(𝐹‘𝑚))))) Fn (ℤ_≥‘1))
46	44, 45	ax-mp 5	. . . . . . . . . 10 ⊢ seq1( + , (𝑘 ∈ ℕ ↦ (vol‘((𝐹‘𝑘) ∖ ∪ 𝑚 ∈ (1..^𝑘)(𝐹‘𝑚))))) Fn (ℤ_≥‘1)
47	6	fneq2i 6579	. . . . . . . . . 10 ⊢ (seq1( + , (𝑘 ∈ ℕ ↦ (vol‘((𝐹‘𝑘) ∖ ∪ 𝑚 ∈ (1..^𝑘)(𝐹‘𝑚))))) Fn ℕ ↔ seq1( + , (𝑘 ∈ ℕ ↦ (vol‘((𝐹‘𝑘) ∖ ∪ 𝑚 ∈ (1..^𝑘)(𝐹‘𝑚))))) Fn (ℤ_≥‘1))
48	46, 47	mpbir 231	. . . . . . . . 9 ⊢ seq1( + , (𝑘 ∈ ℕ ↦ (vol‘((𝐹‘𝑘) ∖ ∪ 𝑚 ∈ (1..^𝑘)(𝐹‘𝑚))))) Fn ℕ
49	48	a1i 11	. . . . . . . 8 ⊢ (((𝐹:ℕ⟶dom vol ∧ ∀𝑛 ∈ ℕ (𝐹‘𝑛) ⊆ (𝐹‘(𝑛 + 1))) ∧ ∀𝑘 ∈ ℕ (vol‘(𝐹‘𝑘)) ∈ ℝ) → seq1( + , (𝑘 ∈ ℕ ↦ (vol‘((𝐹‘𝑘) ∖ ∪ 𝑚 ∈ (1..^𝑘)(𝐹‘𝑚))))) Fn ℕ)
50		volf 25457	. . . . . . . . . 10 ⊢ vol:dom vol⟶(0[,]+∞)
51		simpll 766	. . . . . . . . . 10 ⊢ (((𝐹:ℕ⟶dom vol ∧ ∀𝑛 ∈ ℕ (𝐹‘𝑛) ⊆ (𝐹‘(𝑛 + 1))) ∧ ∀𝑘 ∈ ℕ (vol‘(𝐹‘𝑘)) ∈ ℝ) → 𝐹:ℕ⟶dom vol)
52		fco 6675	. . . . . . . . . 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 6652	. . . . . . . 8 ⊢ (((𝐹:ℕ⟶dom vol ∧ ∀𝑛 ∈ ℕ (𝐹‘𝑛) ⊆ (𝐹‘(𝑛 + 1))) ∧ ∀𝑘 ∈ ℕ (vol‘(𝐹‘𝑘)) ∈ ℝ) → (vol ∘ 𝐹) Fn ℕ)
55		fveq2 6822	. . . . . . . . . . . . 13 ⊢ (𝑥 = 1 → (seq1( + , (𝑘 ∈ ℕ ↦ (vol‘((𝐹‘𝑘) ∖ ∪ 𝑚 ∈ (1..^𝑘)(𝐹‘𝑚)))))‘𝑥) = (seq1( + , (𝑘 ∈ ℕ ↦ (vol‘((𝐹‘𝑘) ∖ ∪ 𝑚 ∈ (1..^𝑘)(𝐹‘𝑚)))))‘1))
56		2fveq3 6827	. . . . . . . . . . . . 13 ⊢ (𝑥 = 1 → (vol‘(𝐹‘𝑥)) = (vol‘(𝐹‘1)))
57	55, 56	eqeq12d 2747	. . . . . . . . . . . 12 ⊢ (𝑥 = 1 → ((seq1( + , (𝑘 ∈ ℕ ↦ (vol‘((𝐹‘𝑘) ∖ ∪ 𝑚 ∈ (1..^𝑘)(𝐹‘𝑚)))))‘𝑥) = (vol‘(𝐹‘𝑥)) ↔ (seq1( + , (𝑘 ∈ ℕ ↦ (vol‘((𝐹‘𝑘) ∖ ∪ 𝑚 ∈ (1..^𝑘)(𝐹‘𝑚)))))‘1) = (vol‘(𝐹‘1))))
58	57	imbi2d 340	. . . . . . . . . . 11 ⊢ (𝑥 = 1 → ((((𝐹:ℕ⟶dom vol ∧ ∀𝑛 ∈ ℕ (𝐹‘𝑛) ⊆ (𝐹‘(𝑛 + 1))) ∧ ∀𝑘 ∈ ℕ (vol‘(𝐹‘𝑘)) ∈ ℝ) → (seq1( + , (𝑘 ∈ ℕ ↦ (vol‘((𝐹‘𝑘) ∖ ∪ 𝑚 ∈ (1..^𝑘)(𝐹‘𝑚)))))‘𝑥) = (vol‘(𝐹‘𝑥))) ↔ (((𝐹:ℕ⟶dom vol ∧ ∀𝑛 ∈ ℕ (𝐹‘𝑛) ⊆ (𝐹‘(𝑛 + 1))) ∧ ∀𝑘 ∈ ℕ (vol‘(𝐹‘𝑘)) ∈ ℝ) → (seq1( + , (𝑘 ∈ ℕ ↦ (vol‘((𝐹‘𝑘) ∖ ∪ 𝑚 ∈ (1..^𝑘)(𝐹‘𝑚)))))‘1) = (vol‘(𝐹‘1)))))
59		fveq2 6822	. . . . . . . . . . . . 13 ⊢ (𝑥 = 𝑗 → (seq1( + , (𝑘 ∈ ℕ ↦ (vol‘((𝐹‘𝑘) ∖ ∪ 𝑚 ∈ (1..^𝑘)(𝐹‘𝑚)))))‘𝑥) = (seq1( + , (𝑘 ∈ ℕ ↦ (vol‘((𝐹‘𝑘) ∖ ∪ 𝑚 ∈ (1..^𝑘)(𝐹‘𝑚)))))‘𝑗))
60		2fveq3 6827	. . . . . . . . . . . . 13 ⊢ (𝑥 = 𝑗 → (vol‘(𝐹‘𝑥)) = (vol‘(𝐹‘𝑗)))
61	59, 60	eqeq12d 2747	. . . . . . . . . . . 12 ⊢ (𝑥 = 𝑗 → ((seq1( + , (𝑘 ∈ ℕ ↦ (vol‘((𝐹‘𝑘) ∖ ∪ 𝑚 ∈ (1..^𝑘)(𝐹‘𝑚)))))‘𝑥) = (vol‘(𝐹‘𝑥)) ↔ (seq1( + , (𝑘 ∈ ℕ ↦ (vol‘((𝐹‘𝑘) ∖ ∪ 𝑚 ∈ (1..^𝑘)(𝐹‘𝑚)))))‘𝑗) = (vol‘(𝐹‘𝑗))))
62	61	imbi2d 340	. . . . . . . . . . 11 ⊢ (𝑥 = 𝑗 → ((((𝐹:ℕ⟶dom vol ∧ ∀𝑛 ∈ ℕ (𝐹‘𝑛) ⊆ (𝐹‘(𝑛 + 1))) ∧ ∀𝑘 ∈ ℕ (vol‘(𝐹‘𝑘)) ∈ ℝ) → (seq1( + , (𝑘 ∈ ℕ ↦ (vol‘((𝐹‘𝑘) ∖ ∪ 𝑚 ∈ (1..^𝑘)(𝐹‘𝑚)))))‘𝑥) = (vol‘(𝐹‘𝑥))) ↔ (((𝐹:ℕ⟶dom vol ∧ ∀𝑛 ∈ ℕ (𝐹‘𝑛) ⊆ (𝐹‘(𝑛 + 1))) ∧ ∀𝑘 ∈ ℕ (vol‘(𝐹‘𝑘)) ∈ ℝ) → (seq1( + , (𝑘 ∈ ℕ ↦ (vol‘((𝐹‘𝑘) ∖ ∪ 𝑚 ∈ (1..^𝑘)(𝐹‘𝑚)))))‘𝑗) = (vol‘(𝐹‘𝑗)))))
63		fveq2 6822	. . . . . . . . . . . . 13 ⊢ (𝑥 = (𝑗 + 1) → (seq1( + , (𝑘 ∈ ℕ ↦ (vol‘((𝐹‘𝑘) ∖ ∪ 𝑚 ∈ (1..^𝑘)(𝐹‘𝑚)))))‘𝑥) = (seq1( + , (𝑘 ∈ ℕ ↦ (vol‘((𝐹‘𝑘) ∖ ∪ 𝑚 ∈ (1..^𝑘)(𝐹‘𝑚)))))‘(𝑗 + 1)))
64		2fveq3 6827	. . . . . . . . . . . . 13 ⊢ (𝑥 = (𝑗 + 1) → (vol‘(𝐹‘𝑥)) = (vol‘(𝐹‘(𝑗 + 1))))
65	63, 64	eqeq12d 2747	. . . . . . . . . . . 12 ⊢ (𝑥 = (𝑗 + 1) → ((seq1( + , (𝑘 ∈ ℕ ↦ (vol‘((𝐹‘𝑘) ∖ ∪ 𝑚 ∈ (1..^𝑘)(𝐹‘𝑚)))))‘𝑥) = (vol‘(𝐹‘𝑥)) ↔ (seq1( + , (𝑘 ∈ ℕ ↦ (vol‘((𝐹‘𝑘) ∖ ∪ 𝑚 ∈ (1..^𝑘)(𝐹‘𝑚)))))‘(𝑗 + 1)) = (vol‘(𝐹‘(𝑗 + 1)))))
66	65	imbi2d 340	. . . . . . . . . . 11 ⊢ (𝑥 = (𝑗 + 1) → ((((𝐹:ℕ⟶dom vol ∧ ∀𝑛 ∈ ℕ (𝐹‘𝑛) ⊆ (𝐹‘(𝑛 + 1))) ∧ ∀𝑘 ∈ ℕ (vol‘(𝐹‘𝑘)) ∈ ℝ) → (seq1( + , (𝑘 ∈ ℕ ↦ (vol‘((𝐹‘𝑘) ∖ ∪ 𝑚 ∈ (1..^𝑘)(𝐹‘𝑚)))))‘𝑥) = (vol‘(𝐹‘𝑥))) ↔ (((𝐹:ℕ⟶dom vol ∧ ∀𝑛 ∈ ℕ (𝐹‘𝑛) ⊆ (𝐹‘(𝑛 + 1))) ∧ ∀𝑘 ∈ ℕ (vol‘(𝐹‘𝑘)) ∈ ℝ) → (seq1( + , (𝑘 ∈ ℕ ↦ (vol‘((𝐹‘𝑘) ∖ ∪ 𝑚 ∈ (1..^𝑘)(𝐹‘𝑚)))))‘(𝑗 + 1)) = (vol‘(𝐹‘(𝑗 + 1))))))
67		seq1 13921	. . . . . . . . . . . . . 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 12136	. . . . . . . . . . . . . 14 ⊢ 1 ∈ ℕ
70		oveq2 7354	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (𝑘 = 1 → (1..^𝑘) = (1..^1))
71		fzo0 13583	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (1..^1) = ∅
72	70, 71	eqtrdi 2782	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (𝑘 = 1 → (1..^𝑘) = ∅)
73	72	iuneq1d 4967	. . . . . . . . . . . . . . . . . . . 20 ⊢ (𝑘 = 1 → ∪ 𝑚 ∈ (1..^𝑘)(𝐹‘𝑚) = ∪ 𝑚 ∈ ∅ (𝐹‘𝑚))
74		0iun 5009	. . . . . . . . . . . . . . . . . . . 20 ⊢ ∪ 𝑚 ∈ ∅ (𝐹‘𝑚) = ∅
75	73, 74	eqtrdi 2782	. . . . . . . . . . . . . . . . . . 19 ⊢ (𝑘 = 1 → ∪ 𝑚 ∈ (1..^𝑘)(𝐹‘𝑚) = ∅)
76	75	difeq2d 4073	. . . . . . . . . . . . . . . . . 18 ⊢ (𝑘 = 1 → ((𝐹‘𝑘) ∖ ∪ 𝑚 ∈ (1..^𝑘)(𝐹‘𝑚)) = ((𝐹‘𝑘) ∖ ∅))
77		dif0 4325	. . . . . . . . . . . . . . . . . 18 ⊢ ((𝐹‘𝑘) ∖ ∅) = (𝐹‘𝑘)
78	76, 77	eqtrdi 2782	. . . . . . . . . . . . . . . . 17 ⊢ (𝑘 = 1 → ((𝐹‘𝑘) ∖ ∪ 𝑚 ∈ (1..^𝑘)(𝐹‘𝑚)) = (𝐹‘𝑘))
79		fveq2 6822	. . . . . . . . . . . . . . . . 17 ⊢ (𝑘 = 1 → (𝐹‘𝑘) = (𝐹‘1))
80	78, 79	eqtrd 2766	. . . . . . . . . . . . . . . 16 ⊢ (𝑘 = 1 → ((𝐹‘𝑘) ∖ ∪ 𝑚 ∈ (1..^𝑘)(𝐹‘𝑚)) = (𝐹‘1))
81	80	fveq2d 6826	. . . . . . . . . . . . . . 15 ⊢ (𝑘 = 1 → (vol‘((𝐹‘𝑘) ∖ ∪ 𝑚 ∈ (1..^𝑘)(𝐹‘𝑚))) = (vol‘(𝐹‘1)))
82		fvex 6835	. . . . . . . . . . . . . . 15 ⊢ (vol‘(𝐹‘1)) ∈ V
83	81, 34, 82	fvmpt 6929	. . . . . . . . . . . . . 14 ⊢ (1 ∈ ℕ → ((𝑘 ∈ ℕ ↦ (vol‘((𝐹‘𝑘) ∖ ∪ 𝑚 ∈ (1..^𝑘)(𝐹‘𝑚))))‘1) = (vol‘(𝐹‘1)))
84	69, 83	ax-mp 5	. . . . . . . . . . . . 13 ⊢ ((𝑘 ∈ ℕ ↦ (vol‘((𝐹‘𝑘) ∖ ∪ 𝑚 ∈ (1..^𝑘)(𝐹‘𝑚))))‘1) = (vol‘(𝐹‘1))
85	68, 84	eqtri 2754	. . . . . . . . . . . 12 ⊢ (seq1( + , (𝑘 ∈ ℕ ↦ (vol‘((𝐹‘𝑘) ∖ ∪ 𝑚 ∈ (1..^𝑘)(𝐹‘𝑚)))))‘1) = (vol‘(𝐹‘1))
86	85	a1i 11	. . . . . . . . . . 11 ⊢ (((𝐹:ℕ⟶dom vol ∧ ∀𝑛 ∈ ℕ (𝐹‘𝑛) ⊆ (𝐹‘(𝑛 + 1))) ∧ ∀𝑘 ∈ ℕ (vol‘(𝐹‘𝑘)) ∈ ℝ) → (seq1( + , (𝑘 ∈ ℕ ↦ (vol‘((𝐹‘𝑘) ∖ ∪ 𝑚 ∈ (1..^𝑘)(𝐹‘𝑚)))))‘1) = (vol‘(𝐹‘1)))
87		oveq1 7353	. . . . . . . . . . . . . 14 ⊢ ((seq1( + , (𝑘 ∈ ℕ ↦ (vol‘((𝐹‘𝑘) ∖ ∪ 𝑚 ∈ (1..^𝑘)(𝐹‘𝑚)))))‘𝑗) = (vol‘(𝐹‘𝑗)) → ((seq1( + , (𝑘 ∈ ℕ ↦ (vol‘((𝐹‘𝑘) ∖ ∪ 𝑚 ∈ (1..^𝑘)(𝐹‘𝑚)))))‘𝑗) + ((𝑘 ∈ ℕ ↦ (vol‘((𝐹‘𝑘) ∖ ∪ 𝑚 ∈ (1..^𝑘)(𝐹‘𝑚))))‘(𝑗 + 1))) = ((vol‘(𝐹‘𝑗)) + ((𝑘 ∈ ℕ ↦ (vol‘((𝐹‘𝑘) ∖ ∪ 𝑚 ∈ (1..^𝑘)(𝐹‘𝑚))))‘(𝑗 + 1))))
88		seqp1 13923	. . . . . . . . . . . . . . . . 17 ⊢ (𝑗 ∈ (ℤ_≥‘1) → (seq1( + , (𝑘 ∈ ℕ ↦ (vol‘((𝐹‘𝑘) ∖ ∪ 𝑚 ∈ (1..^𝑘)(𝐹‘𝑚)))))‘(𝑗 + 1)) = ((seq1( + , (𝑘 ∈ ℕ ↦ (vol‘((𝐹‘𝑘) ∖ ∪ 𝑚 ∈ (1..^𝑘)(𝐹‘𝑚)))))‘𝑗) + ((𝑘 ∈ ℕ ↦ (vol‘((𝐹‘𝑘) ∖ ∪ 𝑚 ∈ (1..^𝑘)(𝐹‘𝑚))))‘(𝑗 + 1))))
89	88, 6	eleq2s 2849	. . . . . . . . . . . . . . . 16 ⊢ (𝑗 ∈ ℕ → (seq1( + , (𝑘 ∈ ℕ ↦ (vol‘((𝐹‘𝑘) ∖ ∪ 𝑚 ∈ (1..^𝑘)(𝐹‘𝑚)))))‘(𝑗 + 1)) = ((seq1( + , (𝑘 ∈ ℕ ↦ (vol‘((𝐹‘𝑘) ∖ ∪ 𝑚 ∈ (1..^𝑘)(𝐹‘𝑚)))))‘𝑗) + ((𝑘 ∈ ℕ ↦ (vol‘((𝐹‘𝑘) ∖ ∪ 𝑚 ∈ (1..^𝑘)(𝐹‘𝑚))))‘(𝑗 + 1))))
90	89	adantl 481	. . . . . . . . . . . . . . 15 ⊢ ((((𝐹:ℕ⟶dom vol ∧ ∀𝑛 ∈ ℕ (𝐹‘𝑛) ⊆ (𝐹‘(𝑛 + 1))) ∧ ∀𝑘 ∈ ℕ (vol‘(𝐹‘𝑘)) ∈ ℝ) ∧ 𝑗 ∈ ℕ) → (seq1( + , (𝑘 ∈ ℕ ↦ (vol‘((𝐹‘𝑘) ∖ ∪ 𝑚 ∈ (1..^𝑘)(𝐹‘𝑚)))))‘(𝑗 + 1)) = ((seq1( + , (𝑘 ∈ ℕ ↦ (vol‘((𝐹‘𝑘) ∖ ∪ 𝑚 ∈ (1..^𝑘)(𝐹‘𝑚)))))‘𝑗) + ((𝑘 ∈ ℕ ↦ (vol‘((𝐹‘𝑘) ∖ ∪ 𝑚 ∈ (1..^𝑘)(𝐹‘𝑚))))‘(𝑗 + 1))))
91		undif2 4424	. . . . . . . . . . . . . . . . . 18 ⊢ ((𝐹‘𝑗) ∪ ((𝐹‘(𝑗 + 1)) ∖ (𝐹‘𝑗))) = ((𝐹‘𝑗) ∪ (𝐹‘(𝑗 + 1)))
92		fveq2 6822	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (𝑛 = 𝑗 → (𝐹‘𝑛) = (𝐹‘𝑗))
93		fvoveq1 7369	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (𝑛 = 𝑗 → (𝐹‘(𝑛 + 1)) = (𝐹‘(𝑗 + 1)))
94	92, 93	sseq12d 3963	. . . . . . . . . . . . . . . . . . . 20 ⊢ (𝑛 = 𝑗 → ((𝐹‘𝑛) ⊆ (𝐹‘(𝑛 + 1)) ↔ (𝐹‘𝑗) ⊆ (𝐹‘(𝑗 + 1))))
95		simpllr 775	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((((𝐹:ℕ⟶dom vol ∧ ∀𝑛 ∈ ℕ (𝐹‘𝑛) ⊆ (𝐹‘(𝑛 + 1))) ∧ ∀𝑘 ∈ ℕ (vol‘(𝐹‘𝑘)) ∈ ℝ) ∧ 𝑗 ∈ ℕ) → ∀𝑛 ∈ ℕ (𝐹‘𝑛) ⊆ (𝐹‘(𝑛 + 1)))
96		simpr 484	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((((𝐹:ℕ⟶dom vol ∧ ∀𝑛 ∈ ℕ (𝐹‘𝑛) ⊆ (𝐹‘(𝑛 + 1))) ∧ ∀𝑘 ∈ ℕ (vol‘(𝐹‘𝑘)) ∈ ℝ) ∧ 𝑗 ∈ ℕ) → 𝑗 ∈ ℕ)
97	94, 95, 96	rspcdva 3573	. . . . . . . . . . . . . . . . . . 19 ⊢ ((((𝐹:ℕ⟶dom vol ∧ ∀𝑛 ∈ ℕ (𝐹‘𝑛) ⊆ (𝐹‘(𝑛 + 1))) ∧ ∀𝑘 ∈ ℕ (vol‘(𝐹‘𝑘)) ∈ ℝ) ∧ 𝑗 ∈ ℕ) → (𝐹‘𝑗) ⊆ (𝐹‘(𝑗 + 1)))
98		ssequn1 4133	. . . . . . . . . . . . . . . . . . 19 ⊢ ((𝐹‘𝑗) ⊆ (𝐹‘(𝑗 + 1)) ↔ ((𝐹‘𝑗) ∪ (𝐹‘(𝑗 + 1))) = (𝐹‘(𝑗 + 1)))
99	97, 98	sylib 218	. . . . . . . . . . . . . . . . . 18 ⊢ ((((𝐹:ℕ⟶dom vol ∧ ∀𝑛 ∈ ℕ (𝐹‘𝑛) ⊆ (𝐹‘(𝑛 + 1))) ∧ ∀𝑘 ∈ ℕ (vol‘(𝐹‘𝑘)) ∈ ℝ) ∧ 𝑗 ∈ ℕ) → ((𝐹‘𝑗) ∪ (𝐹‘(𝑗 + 1))) = (𝐹‘(𝑗 + 1)))
100	91, 99	eqtr2id 2779	. . . . . . . . . . . . . . . . 17 ⊢ ((((𝐹:ℕ⟶dom vol ∧ ∀𝑛 ∈ ℕ (𝐹‘𝑛) ⊆ (𝐹‘(𝑛 + 1))) ∧ ∀𝑘 ∈ ℕ (vol‘(𝐹‘𝑘)) ∈ ℝ) ∧ 𝑗 ∈ ℕ) → (𝐹‘(𝑗 + 1)) = ((𝐹‘𝑗) ∪ ((𝐹‘(𝑗 + 1)) ∖ (𝐹‘𝑗))))
101	100	fveq2d 6826	. . . . . . . . . . . . . . . 16 ⊢ ((((𝐹:ℕ⟶dom vol ∧ ∀𝑛 ∈ ℕ (𝐹‘𝑛) ⊆ (𝐹‘(𝑛 + 1))) ∧ ∀𝑘 ∈ ℕ (vol‘(𝐹‘𝑘)) ∈ ℝ) ∧ 𝑗 ∈ ℕ) → (vol‘(𝐹‘(𝑗 + 1))) = (vol‘((𝐹‘𝑗) ∪ ((𝐹‘(𝑗 + 1)) ∖ (𝐹‘𝑗)))))
102		simplll 774	. . . . . . . . . . . . . . . . . 18 ⊢ ((((𝐹:ℕ⟶dom vol ∧ ∀𝑛 ∈ ℕ (𝐹‘𝑛) ⊆ (𝐹‘(𝑛 + 1))) ∧ ∀𝑘 ∈ ℕ (vol‘(𝐹‘𝑘)) ∈ ℝ) ∧ 𝑗 ∈ ℕ) → 𝐹:ℕ⟶dom vol)
103	102, 96	ffvelcdmd 7018	. . . . . . . . . . . . . . . . 17 ⊢ ((((𝐹:ℕ⟶dom vol ∧ ∀𝑛 ∈ ℕ (𝐹‘𝑛) ⊆ (𝐹‘(𝑛 + 1))) ∧ ∀𝑘 ∈ ℕ (vol‘(𝐹‘𝑘)) ∈ ℝ) ∧ 𝑗 ∈ ℕ) → (𝐹‘𝑗) ∈ dom vol)
104		peano2nn 12137	. . . . . . . . . . . . . . . . . . . 20 ⊢ (𝑗 ∈ ℕ → (𝑗 + 1) ∈ ℕ)
105	104	adantl 481	. . . . . . . . . . . . . . . . . . 19 ⊢ ((((𝐹:ℕ⟶dom vol ∧ ∀𝑛 ∈ ℕ (𝐹‘𝑛) ⊆ (𝐹‘(𝑛 + 1))) ∧ ∀𝑘 ∈ ℕ (vol‘(𝐹‘𝑘)) ∈ ℝ) ∧ 𝑗 ∈ ℕ) → (𝑗 + 1) ∈ ℕ)
106	102, 105	ffvelcdmd 7018	. . . . . . . . . . . . . . . . . 18 ⊢ ((((𝐹:ℕ⟶dom vol ∧ ∀𝑛 ∈ ℕ (𝐹‘𝑛) ⊆ (𝐹‘(𝑛 + 1))) ∧ ∀𝑘 ∈ ℕ (vol‘(𝐹‘𝑘)) ∈ ℝ) ∧ 𝑗 ∈ ℕ) → (𝐹‘(𝑗 + 1)) ∈ dom vol)
107		difmbl 25471	. . . . . . . . . . . . . . . . . 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 4419	. . . . . . . . . . . . . . . . . 18 ⊢ ((𝐹‘𝑗) ∩ ((𝐹‘(𝑗 + 1)) ∖ (𝐹‘𝑗))) = ∅
110	109	a1i 11	. . . . . . . . . . . . . . . . 17 ⊢ ((((𝐹:ℕ⟶dom vol ∧ ∀𝑛 ∈ ℕ (𝐹‘𝑛) ⊆ (𝐹‘(𝑛 + 1))) ∧ ∀𝑘 ∈ ℕ (vol‘(𝐹‘𝑘)) ∈ ℝ) ∧ 𝑗 ∈ ℕ) → ((𝐹‘𝑗) ∩ ((𝐹‘(𝑗 + 1)) ∖ (𝐹‘𝑗))) = ∅)
111		2fveq3 6827	. . . . . . . . . . . . . . . . . . 19 ⊢ (𝑘 = 𝑗 → (vol‘(𝐹‘𝑘)) = (vol‘(𝐹‘𝑗)))
112	111	eleq1d 2816	. . . . . . . . . . . . . . . . . 18 ⊢ (𝑘 = 𝑗 → ((vol‘(𝐹‘𝑘)) ∈ ℝ ↔ (vol‘(𝐹‘𝑗)) ∈ ℝ))
113		simplr 768	. . . . . . . . . . . . . . . . . 18 ⊢ ((((𝐹:ℕ⟶dom vol ∧ ∀𝑛 ∈ ℕ (𝐹‘𝑛) ⊆ (𝐹‘(𝑛 + 1))) ∧ ∀𝑘 ∈ ℕ (vol‘(𝐹‘𝑘)) ∈ ℝ) ∧ 𝑗 ∈ ℕ) → ∀𝑘 ∈ ℕ (vol‘(𝐹‘𝑘)) ∈ ℝ)
114	112, 113, 96	rspcdva 3573	. . . . . . . . . . . . . . . . 17 ⊢ ((((𝐹:ℕ⟶dom vol ∧ ∀𝑛 ∈ ℕ (𝐹‘𝑛) ⊆ (𝐹‘(𝑛 + 1))) ∧ ∀𝑘 ∈ ℕ (vol‘(𝐹‘𝑘)) ∈ ℝ) ∧ 𝑗 ∈ ℕ) → (vol‘(𝐹‘𝑗)) ∈ ℝ)
115		mblvol 25458	. . . . . . . . . . . . . . . . . . 19 ⊢ (((𝐹‘(𝑗 + 1)) ∖ (𝐹‘𝑗)) ∈ dom vol → (vol‘((𝐹‘(𝑗 + 1)) ∖ (𝐹‘𝑗))) = (vol*‘((𝐹‘(𝑗 + 1)) ∖ (𝐹‘𝑗))))
116	108, 115	syl 17	. . . . . . . . . . . . . . . . . 18 ⊢ ((((𝐹:ℕ⟶dom vol ∧ ∀𝑛 ∈ ℕ (𝐹‘𝑛) ⊆ (𝐹‘(𝑛 + 1))) ∧ ∀𝑘 ∈ ℕ (vol‘(𝐹‘𝑘)) ∈ ℝ) ∧ 𝑗 ∈ ℕ) → (vol‘((𝐹‘(𝑗 + 1)) ∖ (𝐹‘𝑗))) = (vol*‘((𝐹‘(𝑗 + 1)) ∖ (𝐹‘𝑗))))
117		difssd 4084	. . . . . . . . . . . . . . . . . . 19 ⊢ ((((𝐹:ℕ⟶dom vol ∧ ∀𝑛 ∈ ℕ (𝐹‘𝑛) ⊆ (𝐹‘(𝑛 + 1))) ∧ ∀𝑘 ∈ ℕ (vol‘(𝐹‘𝑘)) ∈ ℝ) ∧ 𝑗 ∈ ℕ) → ((𝐹‘(𝑗 + 1)) ∖ (𝐹‘𝑗)) ⊆ (𝐹‘(𝑗 + 1)))
118		mblss 25459	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((𝐹‘(𝑗 + 1)) ∈ dom vol → (𝐹‘(𝑗 + 1)) ⊆ ℝ)
119	106, 118	syl 17	. . . . . . . . . . . . . . . . . . 19 ⊢ ((((𝐹:ℕ⟶dom vol ∧ ∀𝑛 ∈ ℕ (𝐹‘𝑛) ⊆ (𝐹‘(𝑛 + 1))) ∧ ∀𝑘 ∈ ℕ (vol‘(𝐹‘𝑘)) ∈ ℝ) ∧ 𝑗 ∈ ℕ) → (𝐹‘(𝑗 + 1)) ⊆ ℝ)
120		mblvol 25458	. . . . . . . . . . . . . . . . . . . . 21 ⊢ ((𝐹‘(𝑗 + 1)) ∈ dom vol → (vol‘(𝐹‘(𝑗 + 1))) = (vol*‘(𝐹‘(𝑗 + 1))))
121	106, 120	syl 17	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((((𝐹:ℕ⟶dom vol ∧ ∀𝑛 ∈ ℕ (𝐹‘𝑛) ⊆ (𝐹‘(𝑛 + 1))) ∧ ∀𝑘 ∈ ℕ (vol‘(𝐹‘𝑘)) ∈ ℝ) ∧ 𝑗 ∈ ℕ) → (vol‘(𝐹‘(𝑗 + 1))) = (vol*‘(𝐹‘(𝑗 + 1))))
122		2fveq3 6827	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (𝑘 = (𝑗 + 1) → (vol‘(𝐹‘𝑘)) = (vol‘(𝐹‘(𝑗 + 1))))
123	122	eleq1d 2816	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (𝑘 = (𝑗 + 1) → ((vol‘(𝐹‘𝑘)) ∈ ℝ ↔ (vol‘(𝐹‘(𝑗 + 1))) ∈ ℝ))
124	123, 113, 105	rspcdva 3573	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((((𝐹:ℕ⟶dom vol ∧ ∀𝑛 ∈ ℕ (𝐹‘𝑛) ⊆ (𝐹‘(𝑛 + 1))) ∧ ∀𝑘 ∈ ℕ (vol‘(𝐹‘𝑘)) ∈ ℝ) ∧ 𝑗 ∈ ℕ) → (vol‘(𝐹‘(𝑗 + 1))) ∈ ℝ)
125	121, 124	eqeltrrd 2832	. . . . . . . . . . . . . . . . . . 19 ⊢ ((((𝐹:ℕ⟶dom vol ∧ ∀𝑛 ∈ ℕ (𝐹‘𝑛) ⊆ (𝐹‘(𝑛 + 1))) ∧ ∀𝑘 ∈ ℕ (vol‘(𝐹‘𝑘)) ∈ ℝ) ∧ 𝑗 ∈ ℕ) → (vol*‘(𝐹‘(𝑗 + 1))) ∈ ℝ)
126		ovolsscl 25414	. . . . . . . . . . . . . . . . . . 19 ⊢ ((((𝐹‘(𝑗 + 1)) ∖ (𝐹‘𝑗)) ⊆ (𝐹‘(𝑗 + 1)) ∧ (𝐹‘(𝑗 + 1)) ⊆ ℝ ∧ (vol‘(𝐹‘(𝑗 + 1))) ∈ ℝ) → (vol‘((𝐹‘(𝑗 + 1)) ∖ (𝐹‘𝑗))) ∈ ℝ)
127	117, 119, 125, 126	syl3anc 1373	. . . . . . . . . . . . . . . . . 18 ⊢ ((((𝐹:ℕ⟶dom vol ∧ ∀𝑛 ∈ ℕ (𝐹‘𝑛) ⊆ (𝐹‘(𝑛 + 1))) ∧ ∀𝑘 ∈ ℕ (vol‘(𝐹‘𝑘)) ∈ ℝ) ∧ 𝑗 ∈ ℕ) → (vol*‘((𝐹‘(𝑗 + 1)) ∖ (𝐹‘𝑗))) ∈ ℝ)
128	116, 127	eqeltrd 2831	. . . . . . . . . . . . . . . . 17 ⊢ ((((𝐹:ℕ⟶dom vol ∧ ∀𝑛 ∈ ℕ (𝐹‘𝑛) ⊆ (𝐹‘(𝑛 + 1))) ∧ ∀𝑘 ∈ ℕ (vol‘(𝐹‘𝑘)) ∈ ℝ) ∧ 𝑗 ∈ ℕ) → (vol‘((𝐹‘(𝑗 + 1)) ∖ (𝐹‘𝑗))) ∈ ℝ)
129		volun 25473	. . . . . . . . . . . . . . . . 17 ⊢ ((((𝐹‘𝑗) ∈ dom vol ∧ ((𝐹‘(𝑗 + 1)) ∖ (𝐹‘𝑗)) ∈ dom vol ∧ ((𝐹‘𝑗) ∩ ((𝐹‘(𝑗 + 1)) ∖ (𝐹‘𝑗))) = ∅) ∧ ((vol‘(𝐹‘𝑗)) ∈ ℝ ∧ (vol‘((𝐹‘(𝑗 + 1)) ∖ (𝐹‘𝑗))) ∈ ℝ)) → (vol‘((𝐹‘𝑗) ∪ ((𝐹‘(𝑗 + 1)) ∖ (𝐹‘𝑗)))) = ((vol‘(𝐹‘𝑗)) + (vol‘((𝐹‘(𝑗 + 1)) ∖ (𝐹‘𝑗)))))
130	103, 108, 110, 114, 128, 129	syl32anc 1380	. . . . . . . . . . . . . . . 16 ⊢ ((((𝐹:ℕ⟶dom vol ∧ ∀𝑛 ∈ ℕ (𝐹‘𝑛) ⊆ (𝐹‘(𝑛 + 1))) ∧ ∀𝑘 ∈ ℕ (vol‘(𝐹‘𝑘)) ∈ ℝ) ∧ 𝑗 ∈ ℕ) → (vol‘((𝐹‘𝑗) ∪ ((𝐹‘(𝑗 + 1)) ∖ (𝐹‘𝑗)))) = ((vol‘(𝐹‘𝑗)) + (vol‘((𝐹‘(𝑗 + 1)) ∖ (𝐹‘𝑗)))))
131	95	adantr 480	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ (((((𝐹:ℕ⟶dom vol ∧ ∀𝑛 ∈ ℕ (𝐹‘𝑛) ⊆ (𝐹‘(𝑛 + 1))) ∧ ∀𝑘 ∈ ℕ (vol‘(𝐹‘𝑘)) ∈ ℝ) ∧ 𝑗 ∈ ℕ) ∧ 𝑚 ∈ (1...𝑗)) → ∀𝑛 ∈ ℕ (𝐹‘𝑛) ⊆ (𝐹‘(𝑛 + 1)))
132		elfznn 13453	. . . . . . . . . . . . . . . . . . . . . . . . . 26 ⊢ (𝑚 ∈ (1...𝑗) → 𝑚 ∈ ℕ)
133	132	adantl 481	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ (((((𝐹:ℕ⟶dom vol ∧ ∀𝑛 ∈ ℕ (𝐹‘𝑛) ⊆ (𝐹‘(𝑛 + 1))) ∧ ∀𝑘 ∈ ℕ (vol‘(𝐹‘𝑘)) ∈ ℝ) ∧ 𝑗 ∈ ℕ) ∧ 𝑚 ∈ (1...𝑗)) → 𝑚 ∈ ℕ)
134		elfzuz3 13421	. . . . . . . . . . . . . . . . . . . . . . . . . 26 ⊢ (𝑚 ∈ (1...𝑗) → 𝑗 ∈ (ℤ_≥‘𝑚))
135	134	adantl 481	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ (((((𝐹:ℕ⟶dom vol ∧ ∀𝑛 ∈ ℕ (𝐹‘𝑛) ⊆ (𝐹‘(𝑛 + 1))) ∧ ∀𝑘 ∈ ℕ (vol‘(𝐹‘𝑘)) ∈ ℝ) ∧ 𝑗 ∈ ℕ) ∧ 𝑚 ∈ (1...𝑗)) → 𝑗 ∈ (ℤ_≥‘𝑚))
136		volsuplem 25483	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ ((∀𝑛 ∈ ℕ (𝐹‘𝑛) ⊆ (𝐹‘(𝑛 + 1)) ∧ (𝑚 ∈ ℕ ∧ 𝑗 ∈ (ℤ_≥‘𝑚))) → (𝐹‘𝑚) ⊆ (𝐹‘𝑗))
137	131, 133, 135, 136	syl12anc 836	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ (((((𝐹:ℕ⟶dom vol ∧ ∀𝑛 ∈ ℕ (𝐹‘𝑛) ⊆ (𝐹‘(𝑛 + 1))) ∧ ∀𝑘 ∈ ℕ (vol‘(𝐹‘𝑘)) ∈ ℝ) ∧ 𝑗 ∈ ℕ) ∧ 𝑚 ∈ (1...𝑗)) → (𝐹‘𝑚) ⊆ (𝐹‘𝑗))
138	137	ralrimiva 3124	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ ((((𝐹:ℕ⟶dom vol ∧ ∀𝑛 ∈ ℕ (𝐹‘𝑛) ⊆ (𝐹‘(𝑛 + 1))) ∧ ∀𝑘 ∈ ℕ (vol‘(𝐹‘𝑘)) ∈ ℝ) ∧ 𝑗 ∈ ℕ) → ∀𝑚 ∈ (1...𝑗)(𝐹‘𝑚) ⊆ (𝐹‘𝑗))
139		iunss 4992	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ (∪ 𝑚 ∈ (1...𝑗)(𝐹‘𝑚) ⊆ (𝐹‘𝑗) ↔ ∀𝑚 ∈ (1...𝑗)(𝐹‘𝑚) ⊆ (𝐹‘𝑗))
140	138, 139	sylibr 234	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ ((((𝐹:ℕ⟶dom vol ∧ ∀𝑛 ∈ ℕ (𝐹‘𝑛) ⊆ (𝐹‘(𝑛 + 1))) ∧ ∀𝑘 ∈ ℕ (vol‘(𝐹‘𝑘)) ∈ ℝ) ∧ 𝑗 ∈ ℕ) → ∪ 𝑚 ∈ (1...𝑗)(𝐹‘𝑚) ⊆ (𝐹‘𝑗))
141	96, 6	eleqtrdi 2841	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ ((((𝐹:ℕ⟶dom vol ∧ ∀𝑛 ∈ ℕ (𝐹‘𝑛) ⊆ (𝐹‘(𝑛 + 1))) ∧ ∀𝑘 ∈ ℕ (vol‘(𝐹‘𝑘)) ∈ ℝ) ∧ 𝑗 ∈ ℕ) → 𝑗 ∈ (ℤ_≥‘1))
142		eluzfz2 13432	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ (𝑗 ∈ (ℤ_≥‘1) → 𝑗 ∈ (1...𝑗))
143	141, 142	syl 17	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ ((((𝐹:ℕ⟶dom vol ∧ ∀𝑛 ∈ ℕ (𝐹‘𝑛) ⊆ (𝐹‘(𝑛 + 1))) ∧ ∀𝑘 ∈ ℕ (vol‘(𝐹‘𝑘)) ∈ ℝ) ∧ 𝑗 ∈ ℕ) → 𝑗 ∈ (1...𝑗))
144		fveq2 6822	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ (𝑚 = 𝑗 → (𝐹‘𝑚) = (𝐹‘𝑗))
145	144	ssiun2s 4995	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ (𝑗 ∈ (1...𝑗) → (𝐹‘𝑗) ⊆ ∪ 𝑚 ∈ (1...𝑗)(𝐹‘𝑚))
146	143, 145	syl 17	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ ((((𝐹:ℕ⟶dom vol ∧ ∀𝑛 ∈ ℕ (𝐹‘𝑛) ⊆ (𝐹‘(𝑛 + 1))) ∧ ∀𝑘 ∈ ℕ (vol‘(𝐹‘𝑘)) ∈ ℝ) ∧ 𝑗 ∈ ℕ) → (𝐹‘𝑗) ⊆ ∪ 𝑚 ∈ (1...𝑗)(𝐹‘𝑚))
147	140, 146	eqssd 3947	. . . . . . . . . . . . . . . . . . . . 21 ⊢ ((((𝐹:ℕ⟶dom vol ∧ ∀𝑛 ∈ ℕ (𝐹‘𝑛) ⊆ (𝐹‘(𝑛 + 1))) ∧ ∀𝑘 ∈ ℕ (vol‘(𝐹‘𝑘)) ∈ ℝ) ∧ 𝑗 ∈ ℕ) → ∪ 𝑚 ∈ (1...𝑗)(𝐹‘𝑚) = (𝐹‘𝑗))
148	96	nnzd 12495	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ ((((𝐹:ℕ⟶dom vol ∧ ∀𝑛 ∈ ℕ (𝐹‘𝑛) ⊆ (𝐹‘(𝑛 + 1))) ∧ ∀𝑘 ∈ ℕ (vol‘(𝐹‘𝑘)) ∈ ℝ) ∧ 𝑗 ∈ ℕ) → 𝑗 ∈ ℤ)
149		fzval3 13634	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ (𝑗 ∈ ℤ → (1...𝑗) = (1..^(𝑗 + 1)))
150	148, 149	syl 17	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ ((((𝐹:ℕ⟶dom vol ∧ ∀𝑛 ∈ ℕ (𝐹‘𝑛) ⊆ (𝐹‘(𝑛 + 1))) ∧ ∀𝑘 ∈ ℕ (vol‘(𝐹‘𝑘)) ∈ ℝ) ∧ 𝑗 ∈ ℕ) → (1...𝑗) = (1..^(𝑗 + 1)))
151	150	iuneq1d 4967	. . . . . . . . . . . . . . . . . . . . 21 ⊢ ((((𝐹:ℕ⟶dom vol ∧ ∀𝑛 ∈ ℕ (𝐹‘𝑛) ⊆ (𝐹‘(𝑛 + 1))) ∧ ∀𝑘 ∈ ℕ (vol‘(𝐹‘𝑘)) ∈ ℝ) ∧ 𝑗 ∈ ℕ) → ∪ 𝑚 ∈ (1...𝑗)(𝐹‘𝑚) = ∪ 𝑚 ∈ (1..^(𝑗 + 1))(𝐹‘𝑚))
152	147, 151	eqtr3d 2768	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((((𝐹:ℕ⟶dom vol ∧ ∀𝑛 ∈ ℕ (𝐹‘𝑛) ⊆ (𝐹‘(𝑛 + 1))) ∧ ∀𝑘 ∈ ℕ (vol‘(𝐹‘𝑘)) ∈ ℝ) ∧ 𝑗 ∈ ℕ) → (𝐹‘𝑗) = ∪ 𝑚 ∈ (1..^(𝑗 + 1))(𝐹‘𝑚))
153	152	difeq2d 4073	. . . . . . . . . . . . . . . . . . 19 ⊢ ((((𝐹:ℕ⟶dom vol ∧ ∀𝑛 ∈ ℕ (𝐹‘𝑛) ⊆ (𝐹‘(𝑛 + 1))) ∧ ∀𝑘 ∈ ℕ (vol‘(𝐹‘𝑘)) ∈ ℝ) ∧ 𝑗 ∈ ℕ) → ((𝐹‘(𝑗 + 1)) ∖ (𝐹‘𝑗)) = ((𝐹‘(𝑗 + 1)) ∖ ∪ 𝑚 ∈ (1..^(𝑗 + 1))(𝐹‘𝑚)))
154	153	fveq2d 6826	. . . . . . . . . . . . . . . . . 18 ⊢ ((((𝐹:ℕ⟶dom vol ∧ ∀𝑛 ∈ ℕ (𝐹‘𝑛) ⊆ (𝐹‘(𝑛 + 1))) ∧ ∀𝑘 ∈ ℕ (vol‘(𝐹‘𝑘)) ∈ ℝ) ∧ 𝑗 ∈ ℕ) → (vol‘((𝐹‘(𝑗 + 1)) ∖ (𝐹‘𝑗))) = (vol‘((𝐹‘(𝑗 + 1)) ∖ ∪ 𝑚 ∈ (1..^(𝑗 + 1))(𝐹‘𝑚))))
155		fveq2 6822	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (𝑘 = (𝑗 + 1) → (𝐹‘𝑘) = (𝐹‘(𝑗 + 1)))
156		oveq2 7354	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ (𝑘 = (𝑗 + 1) → (1..^𝑘) = (1..^(𝑗 + 1)))
157	156	iuneq1d 4967	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (𝑘 = (𝑗 + 1) → ∪ 𝑚 ∈ (1..^𝑘)(𝐹‘𝑚) = ∪ 𝑚 ∈ (1..^(𝑗 + 1))(𝐹‘𝑚))
158	155, 157	difeq12d 4074	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (𝑘 = (𝑗 + 1) → ((𝐹‘𝑘) ∖ ∪ 𝑚 ∈ (1..^𝑘)(𝐹‘𝑚)) = ((𝐹‘(𝑗 + 1)) ∖ ∪ 𝑚 ∈ (1..^(𝑗 + 1))(𝐹‘𝑚)))
159	158	fveq2d 6826	. . . . . . . . . . . . . . . . . . . 20 ⊢ (𝑘 = (𝑗 + 1) → (vol‘((𝐹‘𝑘) ∖ ∪ 𝑚 ∈ (1..^𝑘)(𝐹‘𝑚))) = (vol‘((𝐹‘(𝑗 + 1)) ∖ ∪ 𝑚 ∈ (1..^(𝑗 + 1))(𝐹‘𝑚))))
160		fvex 6835	. . . . . . . . . . . . . . . . . . . 20 ⊢ (vol‘((𝐹‘(𝑗 + 1)) ∖ ∪ 𝑚 ∈ (1..^(𝑗 + 1))(𝐹‘𝑚))) ∈ V
161	159, 34, 160	fvmpt 6929	. . . . . . . . . . . . . . . . . . 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 2769	. . . . . . . . . . . . . . . . 17 ⊢ ((((𝐹:ℕ⟶dom vol ∧ ∀𝑛 ∈ ℕ (𝐹‘𝑛) ⊆ (𝐹‘(𝑛 + 1))) ∧ ∀𝑘 ∈ ℕ (vol‘(𝐹‘𝑘)) ∈ ℝ) ∧ 𝑗 ∈ ℕ) → (vol‘((𝐹‘(𝑗 + 1)) ∖ (𝐹‘𝑗))) = ((𝑘 ∈ ℕ ↦ (vol‘((𝐹‘𝑘) ∖ ∪ 𝑚 ∈ (1..^𝑘)(𝐹‘𝑚))))‘(𝑗 + 1)))
164	163	oveq2d 7362	. . . . . . . . . . . . . . . 16 ⊢ ((((𝐹:ℕ⟶dom vol ∧ ∀𝑛 ∈ ℕ (𝐹‘𝑛) ⊆ (𝐹‘(𝑛 + 1))) ∧ ∀𝑘 ∈ ℕ (vol‘(𝐹‘𝑘)) ∈ ℝ) ∧ 𝑗 ∈ ℕ) → ((vol‘(𝐹‘𝑗)) + (vol‘((𝐹‘(𝑗 + 1)) ∖ (𝐹‘𝑗)))) = ((vol‘(𝐹‘𝑗)) + ((𝑘 ∈ ℕ ↦ (vol‘((𝐹‘𝑘) ∖ ∪ 𝑚 ∈ (1..^𝑘)(𝐹‘𝑚))))‘(𝑗 + 1))))
165	101, 130, 164	3eqtrd 2770	. . . . . . . . . . . . . . 15 ⊢ ((((𝐹:ℕ⟶dom vol ∧ ∀𝑛 ∈ ℕ (𝐹‘𝑛) ⊆ (𝐹‘(𝑛 + 1))) ∧ ∀𝑘 ∈ ℕ (vol‘(𝐹‘𝑘)) ∈ ℝ) ∧ 𝑗 ∈ ℕ) → (vol‘(𝐹‘(𝑗 + 1))) = ((vol‘(𝐹‘𝑗)) + ((𝑘 ∈ ℕ ↦ (vol‘((𝐹‘𝑘) ∖ ∪ 𝑚 ∈ (1..^𝑘)(𝐹‘𝑚))))‘(𝑗 + 1))))
166	90, 165	eqeq12d 2747	. . . . . . . . . . . . . 14 ⊢ ((((𝐹:ℕ⟶dom vol ∧ ∀𝑛 ∈ ℕ (𝐹‘𝑛) ⊆ (𝐹‘(𝑛 + 1))) ∧ ∀𝑘 ∈ ℕ (vol‘(𝐹‘𝑘)) ∈ ℝ) ∧ 𝑗 ∈ ℕ) → ((seq1( + , (𝑘 ∈ ℕ ↦ (vol‘((𝐹‘𝑘) ∖ ∪ 𝑚 ∈ (1..^𝑘)(𝐹‘𝑚)))))‘(𝑗 + 1)) = (vol‘(𝐹‘(𝑗 + 1))) ↔ ((seq1( + , (𝑘 ∈ ℕ ↦ (vol‘((𝐹‘𝑘) ∖ ∪ 𝑚 ∈ (1..^𝑘)(𝐹‘𝑚)))))‘𝑗) + ((𝑘 ∈ ℕ ↦ (vol‘((𝐹‘𝑘) ∖ ∪ 𝑚 ∈ (1..^𝑘)(𝐹‘𝑚))))‘(𝑗 + 1))) = ((vol‘(𝐹‘𝑗)) + ((𝑘 ∈ ℕ ↦ (vol‘((𝐹‘𝑘) ∖ ∪ 𝑚 ∈ (1..^𝑘)(𝐹‘𝑚))))‘(𝑗 + 1)))))
167	87, 166	imbitrrid 246	. . . . . . . . . . . . 13 ⊢ ((((𝐹:ℕ⟶dom vol ∧ ∀𝑛 ∈ ℕ (𝐹‘𝑛) ⊆ (𝐹‘(𝑛 + 1))) ∧ ∀𝑘 ∈ ℕ (vol‘(𝐹‘𝑘)) ∈ ℝ) ∧ 𝑗 ∈ ℕ) → ((seq1( + , (𝑘 ∈ ℕ ↦ (vol‘((𝐹‘𝑘) ∖ ∪ 𝑚 ∈ (1..^𝑘)(𝐹‘𝑚)))))‘𝑗) = (vol‘(𝐹‘𝑗)) → (seq1( + , (𝑘 ∈ ℕ ↦ (vol‘((𝐹‘𝑘) ∖ ∪ 𝑚 ∈ (1..^𝑘)(𝐹‘𝑚)))))‘(𝑗 + 1)) = (vol‘(𝐹‘(𝑗 + 1)))))
168	167	expcom 413	. . . . . . . . . . . 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 12143	. . . . . . . . . 10 ⊢ (𝑗 ∈ ℕ → (((𝐹:ℕ⟶dom vol ∧ ∀𝑛 ∈ ℕ (𝐹‘𝑛) ⊆ (𝐹‘(𝑛 + 1))) ∧ ∀𝑘 ∈ ℕ (vol‘(𝐹‘𝑘)) ∈ ℝ) → (seq1( + , (𝑘 ∈ ℕ ↦ (vol‘((𝐹‘𝑘) ∖ ∪ 𝑚 ∈ (1..^𝑘)(𝐹‘𝑚)))))‘𝑗) = (vol‘(𝐹‘𝑗))))
171	170	impcom 407	. . . . . . . . 9 ⊢ ((((𝐹:ℕ⟶dom vol ∧ ∀𝑛 ∈ ℕ (𝐹‘𝑛) ⊆ (𝐹‘(𝑛 + 1))) ∧ ∀𝑘 ∈ ℕ (vol‘(𝐹‘𝑘)) ∈ ℝ) ∧ 𝑗 ∈ ℕ) → (seq1( + , (𝑘 ∈ ℕ ↦ (vol‘((𝐹‘𝑘) ∖ ∪ 𝑚 ∈ (1..^𝑘)(𝐹‘𝑚)))))‘𝑗) = (vol‘(𝐹‘𝑗)))
172		fvco3 6921	. . . . . . . . . 10 ⊢ ((𝐹:ℕ⟶dom vol ∧ 𝑗 ∈ ℕ) → ((vol ∘ 𝐹)‘𝑗) = (vol‘(𝐹‘𝑗)))
173	51, 172	sylan 580	. . . . . . . . 9 ⊢ ((((𝐹:ℕ⟶dom vol ∧ ∀𝑛 ∈ ℕ (𝐹‘𝑛) ⊆ (𝐹‘(𝑛 + 1))) ∧ ∀𝑘 ∈ ℕ (vol‘(𝐹‘𝑘)) ∈ ℝ) ∧ 𝑗 ∈ ℕ) → ((vol ∘ 𝐹)‘𝑗) = (vol‘(𝐹‘𝑗)))
174	171, 173	eqtr4d 2769	. . . . . . . 8 ⊢ ((((𝐹:ℕ⟶dom vol ∧ ∀𝑛 ∈ ℕ (𝐹‘𝑛) ⊆ (𝐹‘(𝑛 + 1))) ∧ ∀𝑘 ∈ ℕ (vol‘(𝐹‘𝑘)) ∈ ℝ) ∧ 𝑗 ∈ ℕ) → (seq1( + , (𝑘 ∈ ℕ ↦ (vol‘((𝐹‘𝑘) ∖ ∪ 𝑚 ∈ (1..^𝑘)(𝐹‘𝑚)))))‘𝑗) = ((vol ∘ 𝐹)‘𝑗))
175	49, 54, 174	eqfnfvd 6967	. . . . . . 7 ⊢ (((𝐹:ℕ⟶dom vol ∧ ∀𝑛 ∈ ℕ (𝐹‘𝑛) ⊆ (𝐹‘(𝑛 + 1))) ∧ ∀𝑘 ∈ ℕ (vol‘(𝐹‘𝑘)) ∈ ℝ) → seq1( + , (𝑘 ∈ ℕ ↦ (vol‘((𝐹‘𝑘) ∖ ∪ 𝑚 ∈ (1..^𝑘)(𝐹‘𝑚))))) = (vol ∘ 𝐹))
176	175	rneqd 5877	. . . . . 6 ⊢ (((𝐹:ℕ⟶dom vol ∧ ∀𝑛 ∈ ℕ (𝐹‘𝑛) ⊆ (𝐹‘(𝑛 + 1))) ∧ ∀𝑘 ∈ ℕ (vol‘(𝐹‘𝑘)) ∈ ℝ) → ran seq1( + , (𝑘 ∈ ℕ ↦ (vol‘((𝐹‘𝑘) ∖ ∪ 𝑚 ∈ (1..^𝑘)(𝐹‘𝑚))))) = ran (vol ∘ 𝐹))
177		rnco2 6201	. . . . . 6 ⊢ ran (vol ∘ 𝐹) = (vol “ ran 𝐹)
178	176, 177	eqtrdi 2782	. . . . 5 ⊢ (((𝐹:ℕ⟶dom vol ∧ ∀𝑛 ∈ ℕ (𝐹‘𝑛) ⊆ (𝐹‘(𝑛 + 1))) ∧ ∀𝑘 ∈ ℕ (vol‘(𝐹‘𝑘)) ∈ ℝ) → ran seq1( + , (𝑘 ∈ ℕ ↦ (vol‘((𝐹‘𝑘) ∖ ∪ 𝑚 ∈ (1..^𝑘)(𝐹‘𝑚))))) = (vol “ ran 𝐹))
179	178	supeq1d 9330	. . . 4 ⊢ (((𝐹:ℕ⟶dom vol ∧ ∀𝑛 ∈ ℕ (𝐹‘𝑛) ⊆ (𝐹‘(𝑛 + 1))) ∧ ∀𝑘 ∈ ℕ (vol‘(𝐹‘𝑘)) ∈ ℝ) → sup(ran seq1( + , (𝑘 ∈ ℕ ↦ (vol‘((𝐹‘𝑘) ∖ ∪ 𝑚 ∈ (1..^𝑘)(𝐹‘𝑚))))), ℝ^, < ) = sup((vol “ ran 𝐹), ℝ^, < ))
180	36, 43, 179	3eqtr3d 2774	. . 3 ⊢ (((𝐹:ℕ⟶dom vol ∧ ∀𝑛 ∈ ℕ (𝐹‘𝑛) ⊆ (𝐹‘(𝑛 + 1))) ∧ ∀𝑘 ∈ ℕ (vol‘(𝐹‘𝑘)) ∈ ℝ) → (vol‘∪ ran 𝐹) = sup((vol “ ran 𝐹), ℝ^*, < ))
181	180	ex 412	. 2 ⊢ ((𝐹:ℕ⟶dom vol ∧ ∀𝑛 ∈ ℕ (𝐹‘𝑛) ⊆ (𝐹‘(𝑛 + 1))) → (∀𝑘 ∈ ℕ (vol‘(𝐹‘𝑘)) ∈ ℝ → (vol‘∪ ran 𝐹) = sup((vol “ ran 𝐹), ℝ^*, < )))
182		rexnal 3084	. . 3 ⊢ (∃𝑘 ∈ ℕ ¬ (vol‘(𝐹‘𝑘)) ∈ ℝ ↔ ¬ ∀𝑘 ∈ ℕ (vol‘(𝐹‘𝑘)) ∈ ℝ)
183		fniunfv 7181	. . . . . . . . . . . 12 ⊢ (𝐹 Fn ℕ → ∪ 𝑛 ∈ ℕ (𝐹‘𝑛) = ∪ ran 𝐹)
184	38, 183	syl 17	. . . . . . . . . . 11 ⊢ (𝐹:ℕ⟶dom vol → ∪ 𝑛 ∈ ℕ (𝐹‘𝑛) = ∪ ran 𝐹)
185		ffvelcdm 7014	. . . . . . . . . . . . 13 ⊢ ((𝐹:ℕ⟶dom vol ∧ 𝑛 ∈ ℕ) → (𝐹‘𝑛) ∈ dom vol)
186	185	ralrimiva 3124	. . . . . . . . . . . 12 ⊢ (𝐹:ℕ⟶dom vol → ∀𝑛 ∈ ℕ (𝐹‘𝑛) ∈ dom vol)
187		iunmbl 25481	. . . . . . . . . . . 12 ⊢ (∀𝑛 ∈ ℕ (𝐹‘𝑛) ∈ dom vol → ∪ 𝑛 ∈ ℕ (𝐹‘𝑛) ∈ dom vol)
188	186, 187	syl 17	. . . . . . . . . . 11 ⊢ (𝐹:ℕ⟶dom vol → ∪ 𝑛 ∈ ℕ (𝐹‘𝑛) ∈ dom vol)
189	184, 188	eqeltrrd 2832	. . . . . . . . . 10 ⊢ (𝐹:ℕ⟶dom vol → ∪ ran 𝐹 ∈ dom vol)
190	189	ad2antrr 726	. . . . . . . . 9 ⊢ (((𝐹:ℕ⟶dom vol ∧ ∀𝑛 ∈ ℕ (𝐹‘𝑛) ⊆ (𝐹‘(𝑛 + 1))) ∧ (𝑘 ∈ ℕ ∧ ¬ (vol‘(𝐹‘𝑘)) ∈ ℝ)) → ∪ ran 𝐹 ∈ dom vol)
191		mblss 25459	. . . . . . . . 9 ⊢ (∪ ran 𝐹 ∈ dom vol → ∪ ran 𝐹 ⊆ ℝ)
192	190, 191	syl 17	. . . . . . . 8 ⊢ (((𝐹:ℕ⟶dom vol ∧ ∀𝑛 ∈ ℕ (𝐹‘𝑛) ⊆ (𝐹‘(𝑛 + 1))) ∧ (𝑘 ∈ ℕ ∧ ¬ (vol‘(𝐹‘𝑘)) ∈ ℝ)) → ∪ ran 𝐹 ⊆ ℝ)
193		ovolcl 25406	. . . . . . . 8 ⊢ (∪ ran 𝐹 ⊆ ℝ → (vol‘∪ ran 𝐹) ∈ ℝ^)
194	192, 193	syl 17	. . . . . . 7 ⊢ (((𝐹:ℕ⟶dom vol ∧ ∀𝑛 ∈ ℕ (𝐹‘𝑛) ⊆ (𝐹‘(𝑛 + 1))) ∧ (𝑘 ∈ ℕ ∧ ¬ (vol‘(𝐹‘𝑘)) ∈ ℝ)) → (vol‘∪ ran 𝐹) ∈ ℝ^)
195		pnfge 13029	. . . . . . 7 ⊢ ((vol‘∪ ran 𝐹) ∈ ℝ^ → (vol*‘∪ ran 𝐹) ≤ +∞)
196	194, 195	syl 17	. . . . . 6 ⊢ (((𝐹:ℕ⟶dom vol ∧ ∀𝑛 ∈ ℕ (𝐹‘𝑛) ⊆ (𝐹‘(𝑛 + 1))) ∧ (𝑘 ∈ ℕ ∧ ¬ (vol‘(𝐹‘𝑘)) ∈ ℝ)) → (vol*‘∪ ran 𝐹) ≤ +∞)
197		simprr 772	. . . . . . . . 9 ⊢ (((𝐹:ℕ⟶dom vol ∧ ∀𝑛 ∈ ℕ (𝐹‘𝑛) ⊆ (𝐹‘(𝑛 + 1))) ∧ (𝑘 ∈ ℕ ∧ ¬ (vol‘(𝐹‘𝑘)) ∈ ℝ)) → ¬ (vol‘(𝐹‘𝑘)) ∈ ℝ)
198	1	ad2ant2r 747	. . . . . . . . . . . . 13 ⊢ (((𝐹:ℕ⟶dom vol ∧ ∀𝑛 ∈ ℕ (𝐹‘𝑛) ⊆ (𝐹‘(𝑛 + 1))) ∧ (𝑘 ∈ ℕ ∧ ¬ (vol‘(𝐹‘𝑘)) ∈ ℝ)) → (𝐹‘𝑘) ∈ dom vol)
199	198, 18	syl 17	. . . . . . . . . . . 12 ⊢ (((𝐹:ℕ⟶dom vol ∧ ∀𝑛 ∈ ℕ (𝐹‘𝑛) ⊆ (𝐹‘(𝑛 + 1))) ∧ (𝑘 ∈ ℕ ∧ ¬ (vol‘(𝐹‘𝑘)) ∈ ℝ)) → (𝐹‘𝑘) ⊆ ℝ)
200		ovolcl 25406	. . . . . . . . . . . 12 ⊢ ((𝐹‘𝑘) ⊆ ℝ → (vol‘(𝐹‘𝑘)) ∈ ℝ^)
201	199, 200	syl 17	. . . . . . . . . . 11 ⊢ (((𝐹:ℕ⟶dom vol ∧ ∀𝑛 ∈ ℕ (𝐹‘𝑛) ⊆ (𝐹‘(𝑛 + 1))) ∧ (𝑘 ∈ ℕ ∧ ¬ (vol‘(𝐹‘𝑘)) ∈ ℝ)) → (vol‘(𝐹‘𝑘)) ∈ ℝ^)
202		xrrebnd 13067	. . . . . . . . . . 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 2816	. . . . . . . . . 10 ⊢ (((𝐹:ℕ⟶dom vol ∧ ∀𝑛 ∈ ℕ (𝐹‘𝑛) ⊆ (𝐹‘(𝑛 + 1))) ∧ (𝑘 ∈ ℕ ∧ ¬ (vol‘(𝐹‘𝑘)) ∈ ℝ)) → ((vol‘(𝐹‘𝑘)) ∈ ℝ ↔ (vol*‘(𝐹‘𝑘)) ∈ ℝ))
206		ovolge0 25409	. . . . . . . . . . . . 13 ⊢ ((𝐹‘𝑘) ⊆ ℝ → 0 ≤ (vol*‘(𝐹‘𝑘)))
207		mnflt0 13024	. . . . . . . . . . . . . 14 ⊢ -∞ < 0
208		mnfxr 11169	. . . . . . . . . . . . . . 15 ⊢ -∞ ∈ ℝ^*
209		0xr 11159	. . . . . . . . . . . . . . 15 ⊢ 0 ∈ ℝ^*
210		xrltletr 13056	. . . . . . . . . . . . . . 15 ⊢ ((-∞ ∈ ℝ^* ∧ 0 ∈ ℝ^* ∧ (vol‘(𝐹‘𝑘)) ∈ ℝ^) → ((-∞ < 0 ∧ 0 ≤ (vol‘(𝐹‘𝑘))) → -∞ < (vol‘(𝐹‘𝑘))))
211	208, 209, 210	mp3an12 1453	. . . . . . . . . . . . . 14 ⊢ ((vol‘(𝐹‘𝑘)) ∈ ℝ^ → ((-∞ < 0 ∧ 0 ≤ (vol‘(𝐹‘𝑘))) → -∞ < (vol‘(𝐹‘𝑘))))
212	207, 211	mpani 696	. . . . . . . . . . . . 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 532	. . . . . . . . . 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 13063	. . . . . . . . 9 ⊢ ((vol‘(𝐹‘𝑘)) ∈ ℝ^ → ((vol‘(𝐹‘𝑘)) = +∞ ↔ ¬ (vol‘(𝐹‘𝑘)) < +∞))
219	201, 218	syl 17	. . . . . . . 8 ⊢ (((𝐹:ℕ⟶dom vol ∧ ∀𝑛 ∈ ℕ (𝐹‘𝑛) ⊆ (𝐹‘(𝑛 + 1))) ∧ (𝑘 ∈ ℕ ∧ ¬ (vol‘(𝐹‘𝑘)) ∈ ℝ)) → ((vol‘(𝐹‘𝑘)) = +∞ ↔ ¬ (vol‘(𝐹‘𝑘)) < +∞))
220	217, 219	mpbird 257	. . . . . . 7 ⊢ (((𝐹:ℕ⟶dom vol ∧ ∀𝑛 ∈ ℕ (𝐹‘𝑛) ⊆ (𝐹‘(𝑛 + 1))) ∧ (𝑘 ∈ ℕ ∧ ¬ (vol‘(𝐹‘𝑘)) ∈ ℝ)) → (vol*‘(𝐹‘𝑘)) = +∞)
221	38	ad2antrr 726	. . . . . . . . . 10 ⊢ (((𝐹:ℕ⟶dom vol ∧ ∀𝑛 ∈ ℕ (𝐹‘𝑛) ⊆ (𝐹‘(𝑛 + 1))) ∧ (𝑘 ∈ ℕ ∧ ¬ (vol‘(𝐹‘𝑘)) ∈ ℝ)) → 𝐹 Fn ℕ)
222		simprl 770	. . . . . . . . . 10 ⊢ (((𝐹:ℕ⟶dom vol ∧ ∀𝑛 ∈ ℕ (𝐹‘𝑛) ⊆ (𝐹‘(𝑛 + 1))) ∧ (𝑘 ∈ ℕ ∧ ¬ (vol‘(𝐹‘𝑘)) ∈ ℝ)) → 𝑘 ∈ ℕ)
223		fnfvelrn 7013	. . . . . . . . . 10 ⊢ ((𝐹 Fn ℕ ∧ 𝑘 ∈ ℕ) → (𝐹‘𝑘) ∈ ran 𝐹)
224	221, 222, 223	syl2anc 584	. . . . . . . . 9 ⊢ (((𝐹:ℕ⟶dom vol ∧ ∀𝑛 ∈ ℕ (𝐹‘𝑛) ⊆ (𝐹‘(𝑛 + 1))) ∧ (𝑘 ∈ ℕ ∧ ¬ (vol‘(𝐹‘𝑘)) ∈ ℝ)) → (𝐹‘𝑘) ∈ ran 𝐹)
225		elssuni 4887	. . . . . . . . 9 ⊢ ((𝐹‘𝑘) ∈ ran 𝐹 → (𝐹‘𝑘) ⊆ ∪ ran 𝐹)
226	224, 225	syl 17	. . . . . . . 8 ⊢ (((𝐹:ℕ⟶dom vol ∧ ∀𝑛 ∈ ℕ (𝐹‘𝑛) ⊆ (𝐹‘(𝑛 + 1))) ∧ (𝑘 ∈ ℕ ∧ ¬ (vol‘(𝐹‘𝑘)) ∈ ℝ)) → (𝐹‘𝑘) ⊆ ∪ ran 𝐹)
227		ovolss 25413	. . . . . . . 8 ⊢ (((𝐹‘𝑘) ⊆ ∪ ran 𝐹 ∧ ∪ ran 𝐹 ⊆ ℝ) → (vol‘(𝐹‘𝑘)) ≤ (vol‘∪ ran 𝐹))
228	226, 192, 227	syl2anc 584	. . . . . . 7 ⊢ (((𝐹:ℕ⟶dom vol ∧ ∀𝑛 ∈ ℕ (𝐹‘𝑛) ⊆ (𝐹‘(𝑛 + 1))) ∧ (𝑘 ∈ ℕ ∧ ¬ (vol‘(𝐹‘𝑘)) ∈ ℝ)) → (vol‘(𝐹‘𝑘)) ≤ (vol‘∪ ran 𝐹))
229	220, 228	eqbrtrrd 5113	. . . . . 6 ⊢ (((𝐹:ℕ⟶dom vol ∧ ∀𝑛 ∈ ℕ (𝐹‘𝑛) ⊆ (𝐹‘(𝑛 + 1))) ∧ (𝑘 ∈ ℕ ∧ ¬ (vol‘(𝐹‘𝑘)) ∈ ℝ)) → +∞ ≤ (vol*‘∪ ran 𝐹))
230		pnfxr 11166	. . . . . . 7 ⊢ +∞ ∈ ℝ^*
231		xrletri3 13053	. . . . . . 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 713	. . . . 5 ⊢ (((𝐹:ℕ⟶dom vol ∧ ∀𝑛 ∈ ℕ (𝐹‘𝑛) ⊆ (𝐹‘(𝑛 + 1))) ∧ (𝑘 ∈ ℕ ∧ ¬ (vol‘(𝐹‘𝑘)) ∈ ℝ)) → (vol*‘∪ ran 𝐹) = +∞)
234		mblvol 25458	. . . . . 6 ⊢ (∪ ran 𝐹 ∈ dom vol → (vol‘∪ ran 𝐹) = (vol*‘∪ ran 𝐹))
235	190, 234	syl 17	. . . . 5 ⊢ (((𝐹:ℕ⟶dom vol ∧ ∀𝑛 ∈ ℕ (𝐹‘𝑛) ⊆ (𝐹‘(𝑛 + 1))) ∧ (𝑘 ∈ ℕ ∧ ¬ (vol‘(𝐹‘𝑘)) ∈ ℝ)) → (vol‘∪ ran 𝐹) = (vol*‘∪ ran 𝐹))
236		imassrn 6019	. . . . . . 7 ⊢ (vol “ ran 𝐹) ⊆ ran vol
237		frn 6658	. . . . . . . . 9 ⊢ (vol:dom vol⟶(0[,]+∞) → ran vol ⊆ (0[,]+∞))
238	50, 237	ax-mp 5	. . . . . . . 8 ⊢ ran vol ⊆ (0[,]+∞)
239		iccssxr 13330	. . . . . . . 8 ⊢ (0[,]+∞) ⊆ ℝ^*
240	238, 239	sstri 3939	. . . . . . 7 ⊢ ran vol ⊆ ℝ^*
241	236, 240	sstri 3939	. . . . . 6 ⊢ (vol “ ran 𝐹) ⊆ ℝ^*
242	204, 220	eqtrd 2766	. . . . . . 7 ⊢ (((𝐹:ℕ⟶dom vol ∧ ∀𝑛 ∈ ℕ (𝐹‘𝑛) ⊆ (𝐹‘(𝑛 + 1))) ∧ (𝑘 ∈ ℕ ∧ ¬ (vol‘(𝐹‘𝑘)) ∈ ℝ)) → (vol‘(𝐹‘𝑘)) = +∞)
243		simpll 766	. . . . . . . 8 ⊢ (((𝐹:ℕ⟶dom vol ∧ ∀𝑛 ∈ ℕ (𝐹‘𝑛) ⊆ (𝐹‘(𝑛 + 1))) ∧ (𝑘 ∈ ℕ ∧ ¬ (vol‘(𝐹‘𝑘)) ∈ ℝ)) → 𝐹:ℕ⟶dom vol)
244		ffun 6654	. . . . . . . . . 10 ⊢ (vol:dom vol⟶(0[,]+∞) → Fun vol)
245	50, 244	ax-mp 5	. . . . . . . . 9 ⊢ Fun vol
246		frn 6658	. . . . . . . . 9 ⊢ (𝐹:ℕ⟶dom vol → ran 𝐹 ⊆ dom vol)
247		funfvima2 7165	. . . . . . . . 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 2832	. . . . . 6 ⊢ (((𝐹:ℕ⟶dom vol ∧ ∀𝑛 ∈ ℕ (𝐹‘𝑛) ⊆ (𝐹‘(𝑛 + 1))) ∧ (𝑘 ∈ ℕ ∧ ¬ (vol‘(𝐹‘𝑘)) ∈ ℝ)) → +∞ ∈ (vol “ ran 𝐹))
251		supxrpnf 13217	. . . . . 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 2776	. . . 4 ⊢ (((𝐹:ℕ⟶dom vol ∧ ∀𝑛 ∈ ℕ (𝐹‘𝑛) ⊆ (𝐹‘(𝑛 + 1))) ∧ (𝑘 ∈ ℕ ∧ ¬ (vol‘(𝐹‘𝑘)) ∈ ℝ)) → (vol‘∪ ran 𝐹) = sup((vol “ ran 𝐹), ℝ^*, < ))
254	253	rexlimdvaa 3134	. . 3 ⊢ ((𝐹:ℕ⟶dom vol ∧ ∀𝑛 ∈ ℕ (𝐹‘𝑛) ⊆ (𝐹‘(𝑛 + 1))) → (∃𝑘 ∈ ℕ ¬ (vol‘(𝐹‘𝑘)) ∈ ℝ → (vol‘∪ ran 𝐹) = sup((vol “ ran 𝐹), ℝ^*, < )))
255	182, 254	biimtrrid 243	. 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 206 ∧ wa 395 = wceq 1541 ∈ wcel 2111 ∀wral 3047 ∃wrex 3056 ∖ cdif 3894 ∪ cun 3895 ∩ cin 3896 ⊆ wss 3897 ∅c0 4280 ∪ cuni 4856 ∪ ciun 4939 Disj wdisj 5056 class class class wbr 5089 ↦ cmpt 5170 dom cdm 5614 ran crn 5615 “ cima 5617 ∘ ccom 5618 Fun wfun 6475 Fn wfn 6476 ⟶wf 6477 ‘cfv 6481 (class class class)co 7346 Fincfn 8869 supcsup 9324 ℝcr 11005 0cc0 11006 1c1 11007 + caddc 11009 +∞cpnf 11143 -∞cmnf 11144 ℝ^*cxr 11145 < clt 11146 ≤ cle 11147 ℕcn 12125 ℤcz 12468 ℤ_≥cuz 12732 [,]cicc 13248 ...cfz 13407 ..^cfzo 13554 seqcseq 13908 vol*covol 25390 volcvol 25391

This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1796 ax-4 1810 ax-5 1911 ax-6 1968 ax-7 2009 ax-8 2113 ax-9 2121 ax-10 2144 ax-11 2160 ax-12 2180 ax-ext 2703 ax-rep 5215 ax-sep 5232 ax-nul 5242 ax-pow 5301 ax-pr 5368 ax-un 7668 ax-inf2 9531 ax-cc 10326 ax-cnex 11062 ax-resscn 11063 ax-1cn 11064 ax-icn 11065 ax-addcl 11066 ax-addrcl 11067 ax-mulcl 11068 ax-mulrcl 11069 ax-mulcom 11070 ax-addass 11071 ax-mulass 11072 ax-distr 11073 ax-i2m1 11074 ax-1ne0 11075 ax-1rid 11076 ax-rnegex 11077 ax-rrecex 11078 ax-cnre 11079 ax-pre-lttri 11080 ax-pre-lttrn 11081 ax-pre-ltadd 11082 ax-pre-mulgt0 11083 ax-pre-sup 11084

This theorem depends on definitions: df-bi 207 df-an 396 df-or 848 df-3or 1087 df-3an 1088 df-tru 1544 df-fal 1554 df-ex 1781 df-nf 1785 df-sb 2068 df-mo 2535 df-eu 2564 df-clab 2710 df-cleq 2723 df-clel 2806 df-nfc 2881 df-ne 2929 df-nel 3033 df-ral 3048 df-rex 3057 df-rmo 3346 df-reu 3347 df-rab 3396 df-v 3438 df-sbc 3737 df-csb 3846 df-dif 3900 df-un 3902 df-in 3904 df-ss 3914 df-pss 3917 df-nul 4281 df-if 4473 df-pw 4549 df-sn 4574 df-pr 4576 df-op 4580 df-uni 4857 df-int 4896 df-iun 4941 df-disj 5057 df-br 5090 df-opab 5152 df-mpt 5171 df-tr 5197 df-id 5509 df-eprel 5514 df-po 5522 df-so 5523 df-fr 5567 df-se 5568 df-we 5569 df-xp 5620 df-rel 5621 df-cnv 5622 df-co 5623 df-dm 5624 df-rn 5625 df-res 5626 df-ima 5627 df-pred 6248 df-ord 6309 df-on 6310 df-lim 6311 df-suc 6312 df-iota 6437 df-fun 6483 df-fn 6484 df-f 6485 df-f1 6486 df-fo 6487 df-f1o 6488 df-fv 6489 df-isom 6490 df-riota 7303 df-ov 7349 df-oprab 7350 df-mpo 7351 df-of 7610 df-om 7797 df-1st 7921 df-2nd 7922 df-frecs 8211 df-wrecs 8242 df-recs 8291 df-rdg 8329 df-1o 8385 df-2o 8386 df-er 8622 df-map 8752 df-pm 8753 df-en 8870 df-dom 8871 df-sdom 8872 df-fin 8873 df-sup 9326 df-inf 9327 df-oi 9396 df-dju 9794 df-card 9832 df-pnf 11148 df-mnf 11149 df-xr 11150 df-ltxr 11151 df-le 11152 df-sub 11346 df-neg 11347 df-div 11775 df-nn 12126 df-2 12188 df-3 12189 df-n0 12382 df-z 12469 df-uz 12733 df-q 12847 df-rp 12891 df-xadd 13012 df-ioo 13249 df-ico 13251 df-icc 13252 df-fz 13408 df-fzo 13555 df-fl 13696 df-seq 13909 df-exp 13969 df-hash 14238 df-cj 15006 df-re 15007 df-im 15008 df-sqrt 15142 df-abs 15143 df-clim 15395 df-rlim 15396 df-sum 15594 df-xmet 21284 df-met 21285 df-ovol 25392 df-vol 25393

This theorem is referenced by: volsup2 25533 itg1climres 25642 itg2gt0 25688

W3C validator