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 25591

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 7101	. . . . . . . . . . 11 ⊢ ((𝐹:ℕ⟶dom vol ∧ 𝑘 ∈ ℕ) → (𝐹‘𝑘) ∈ dom vol)
2	1	ad2ant2r 747	. . . . . . . . . 10 ⊢ (((𝐹:ℕ⟶dom vol ∧ ∀𝑛 ∈ ℕ (𝐹‘𝑛) ⊆ (𝐹‘(𝑛 + 1))) ∧ (𝑘 ∈ ℕ ∧ (vol‘(𝐹‘𝑘)) ∈ ℝ)) → (𝐹‘𝑘) ∈ dom vol)
3		fzofi 14015	. . . . . . . . . . 11 ⊢ (1..^𝑘) ∈ Fin
4		simpll 767	. . . . . . . . . . . . 13 ⊢ (((𝐹:ℕ⟶dom vol ∧ ∀𝑛 ∈ ℕ (𝐹‘𝑛) ⊆ (𝐹‘(𝑛 + 1))) ∧ (𝑘 ∈ ℕ ∧ (vol‘(𝐹‘𝑘)) ∈ ℝ)) → 𝐹:ℕ⟶dom vol)
5		elfzouz 13703	. . . . . . . . . . . . . 14 ⊢ (𝑚 ∈ (1..^𝑘) → 𝑚 ∈ (ℤ_≥‘1))
6		nnuz 12921	. . . . . . . . . . . . . 14 ⊢ ℕ = (ℤ_≥‘1)
7	5, 6	eleqtrrdi 2852	. . . . . . . . . . . . 13 ⊢ (𝑚 ∈ (1..^𝑘) → 𝑚 ∈ ℕ)
8		ffvelcdm 7101	. . . . . . . . . . . . 13 ⊢ ((𝐹:ℕ⟶dom vol ∧ 𝑚 ∈ ℕ) → (𝐹‘𝑚) ∈ dom vol)
9	4, 7, 8	syl2an 596	. . . . . . . . . . . 12 ⊢ ((((𝐹:ℕ⟶dom vol ∧ ∀𝑛 ∈ ℕ (𝐹‘𝑛) ⊆ (𝐹‘(𝑛 + 1))) ∧ (𝑘 ∈ ℕ ∧ (vol‘(𝐹‘𝑘)) ∈ ℝ)) ∧ 𝑚 ∈ (1..^𝑘)) → (𝐹‘𝑚) ∈ dom vol)
10	9	ralrimiva 3146	. . . . . . . . . . 11 ⊢ (((𝐹:ℕ⟶dom vol ∧ ∀𝑛 ∈ ℕ (𝐹‘𝑛) ⊆ (𝐹‘(𝑛 + 1))) ∧ (𝑘 ∈ ℕ ∧ (vol‘(𝐹‘𝑘)) ∈ ℝ)) → ∀𝑚 ∈ (1..^𝑘)(𝐹‘𝑚) ∈ dom vol)
11		finiunmbl 25579	. . . . . . . . . . 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 25578	. . . . . . . . . 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 25565	. . . . . . . . . . 11 ⊢ (((𝐹‘𝑘) ∖ ∪ 𝑚 ∈ (1..^𝑘)(𝐹‘𝑚)) ∈ dom vol → (vol‘((𝐹‘𝑘) ∖ ∪ 𝑚 ∈ (1..^𝑘)(𝐹‘𝑚))) = (vol*‘((𝐹‘𝑘) ∖ ∪ 𝑚 ∈ (1..^𝑘)(𝐹‘𝑚))))
16	14, 15	syl 17	. . . . . . . . . 10 ⊢ (((𝐹:ℕ⟶dom vol ∧ ∀𝑛 ∈ ℕ (𝐹‘𝑛) ⊆ (𝐹‘(𝑛 + 1))) ∧ (𝑘 ∈ ℕ ∧ (vol‘(𝐹‘𝑘)) ∈ ℝ)) → (vol‘((𝐹‘𝑘) ∖ ∪ 𝑚 ∈ (1..^𝑘)(𝐹‘𝑚))) = (vol*‘((𝐹‘𝑘) ∖ ∪ 𝑚 ∈ (1..^𝑘)(𝐹‘𝑚))))
17		difssd 4137	. . . . . . . . . . 11 ⊢ (((𝐹:ℕ⟶dom vol ∧ ∀𝑛 ∈ ℕ (𝐹‘𝑛) ⊆ (𝐹‘(𝑛 + 1))) ∧ (𝑘 ∈ ℕ ∧ (vol‘(𝐹‘𝑘)) ∈ ℝ)) → ((𝐹‘𝑘) ∖ ∪ 𝑚 ∈ (1..^𝑘)(𝐹‘𝑚)) ⊆ (𝐹‘𝑘))
18		mblss 25566	. . . . . . . . . . . 12 ⊢ ((𝐹‘𝑘) ∈ dom vol → (𝐹‘𝑘) ⊆ ℝ)
19	2, 18	syl 17	. . . . . . . . . . 11 ⊢ (((𝐹:ℕ⟶dom vol ∧ ∀𝑛 ∈ ℕ (𝐹‘𝑛) ⊆ (𝐹‘(𝑛 + 1))) ∧ (𝑘 ∈ ℕ ∧ (vol‘(𝐹‘𝑘)) ∈ ℝ)) → (𝐹‘𝑘) ⊆ ℝ)
20		mblvol 25565	. . . . . . . . . . . . 13 ⊢ ((𝐹‘𝑘) ∈ dom vol → (vol‘(𝐹‘𝑘)) = (vol*‘(𝐹‘𝑘)))
21	2, 20	syl 17	. . . . . . . . . . . 12 ⊢ (((𝐹:ℕ⟶dom vol ∧ ∀𝑛 ∈ ℕ (𝐹‘𝑛) ⊆ (𝐹‘(𝑛 + 1))) ∧ (𝑘 ∈ ℕ ∧ (vol‘(𝐹‘𝑘)) ∈ ℝ)) → (vol‘(𝐹‘𝑘)) = (vol*‘(𝐹‘𝑘)))
22		simprr 773	. . . . . . . . . . . 12 ⊢ (((𝐹:ℕ⟶dom vol ∧ ∀𝑛 ∈ ℕ (𝐹‘𝑛) ⊆ (𝐹‘(𝑛 + 1))) ∧ (𝑘 ∈ ℕ ∧ (vol‘(𝐹‘𝑘)) ∈ ℝ)) → (vol‘(𝐹‘𝑘)) ∈ ℝ)
23	21, 22	eqeltrrd 2842	. . . . . . . . . . 11 ⊢ (((𝐹:ℕ⟶dom vol ∧ ∀𝑛 ∈ ℕ (𝐹‘𝑛) ⊆ (𝐹‘(𝑛 + 1))) ∧ (𝑘 ∈ ℕ ∧ (vol‘(𝐹‘𝑘)) ∈ ℝ)) → (vol*‘(𝐹‘𝑘)) ∈ ℝ)
24		ovolsscl 25521	. . . . . . . . . . 11 ⊢ ((((𝐹‘𝑘) ∖ ∪ 𝑚 ∈ (1..^𝑘)(𝐹‘𝑚)) ⊆ (𝐹‘𝑘) ∧ (𝐹‘𝑘) ⊆ ℝ ∧ (vol‘(𝐹‘𝑘)) ∈ ℝ) → (vol‘((𝐹‘𝑘) ∖ ∪ 𝑚 ∈ (1..^𝑘)(𝐹‘𝑚))) ∈ ℝ)
25	17, 19, 23, 24	syl3anc 1373	. . . . . . . . . 10 ⊢ (((𝐹:ℕ⟶dom vol ∧ ∀𝑛 ∈ ℕ (𝐹‘𝑛) ⊆ (𝐹‘(𝑛 + 1))) ∧ (𝑘 ∈ ℕ ∧ (vol‘(𝐹‘𝑘)) ∈ ℝ)) → (vol*‘((𝐹‘𝑘) ∖ ∪ 𝑚 ∈ (1..^𝑘)(𝐹‘𝑚))) ∈ ℝ)
26	16, 25	eqeltrd 2841	. . . . . . . . 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 3167	. . . . . 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 6906	. . . . . 6 ⊢ (𝑘 = 𝑚 → (𝐹‘𝑘) = (𝐹‘𝑚))
32	31	iundisj2 25584	. . . . 5 ⊢ Disj 𝑘 ∈ ℕ ((𝐹‘𝑘) ∖ ∪ 𝑚 ∈ (1..^𝑘)(𝐹‘𝑚))
33		eqid 2737	. . . . . 6 ⊢ seq1( + , (𝑘 ∈ ℕ ↦ (vol‘((𝐹‘𝑘) ∖ ∪ 𝑚 ∈ (1..^𝑘)(𝐹‘𝑚))))) = seq1( + , (𝑘 ∈ ℕ ↦ (vol‘((𝐹‘𝑘) ∖ ∪ 𝑚 ∈ (1..^𝑘)(𝐹‘𝑚)))))
34		eqid 2737	. . . . . 6 ⊢ (𝑘 ∈ ℕ ↦ (vol‘((𝐹‘𝑘) ∖ ∪ 𝑚 ∈ (1..^𝑘)(𝐹‘𝑚)))) = (𝑘 ∈ ℕ ↦ (vol‘((𝐹‘𝑘) ∖ ∪ 𝑚 ∈ (1..^𝑘)(𝐹‘𝑚))))
35	33, 34	voliun 25589	. . . . 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 25583	. . . . . 6 ⊢ ∪ 𝑘 ∈ ℕ (𝐹‘𝑘) = ∪ 𝑘 ∈ ℕ ((𝐹‘𝑘) ∖ ∪ 𝑚 ∈ (1..^𝑘)(𝐹‘𝑚))
38		ffn 6736	. . . . . . . 8 ⊢ (𝐹:ℕ⟶dom vol → 𝐹 Fn ℕ)
39	38	ad2antrr 726	. . . . . . 7 ⊢ (((𝐹:ℕ⟶dom vol ∧ ∀𝑛 ∈ ℕ (𝐹‘𝑛) ⊆ (𝐹‘(𝑛 + 1))) ∧ ∀𝑘 ∈ ℕ (vol‘(𝐹‘𝑘)) ∈ ℝ) → 𝐹 Fn ℕ)
40		fniunfv 7267	. . . . . . 7 ⊢ (𝐹 Fn ℕ → ∪ 𝑘 ∈ ℕ (𝐹‘𝑘) = ∪ ran 𝐹)
41	39, 40	syl 17	. . . . . 6 ⊢ (((𝐹:ℕ⟶dom vol ∧ ∀𝑛 ∈ ℕ (𝐹‘𝑛) ⊆ (𝐹‘(𝑛 + 1))) ∧ ∀𝑘 ∈ ℕ (vol‘(𝐹‘𝑘)) ∈ ℝ) → ∪ 𝑘 ∈ ℕ (𝐹‘𝑘) = ∪ ran 𝐹)
42	37, 41	eqtr3id 2791	. . . . 5 ⊢ (((𝐹:ℕ⟶dom vol ∧ ∀𝑛 ∈ ℕ (𝐹‘𝑛) ⊆ (𝐹‘(𝑛 + 1))) ∧ ∀𝑘 ∈ ℕ (vol‘(𝐹‘𝑘)) ∈ ℝ) → ∪ 𝑘 ∈ ℕ ((𝐹‘𝑘) ∖ ∪ 𝑚 ∈ (1..^𝑘)(𝐹‘𝑚)) = ∪ ran 𝐹)
43	42	fveq2d 6910	. . . 4 ⊢ (((𝐹:ℕ⟶dom vol ∧ ∀𝑛 ∈ ℕ (𝐹‘𝑛) ⊆ (𝐹‘(𝑛 + 1))) ∧ ∀𝑘 ∈ ℕ (vol‘(𝐹‘𝑘)) ∈ ℝ) → (vol‘∪ 𝑘 ∈ ℕ ((𝐹‘𝑘) ∖ ∪ 𝑚 ∈ (1..^𝑘)(𝐹‘𝑚))) = (vol‘∪ ran 𝐹))
44		1z 12647	. . . . . . . . . . 11 ⊢ 1 ∈ ℤ
45		seqfn 14054	. . . . . . . . . . 11 ⊢ (1 ∈ ℤ → seq1( + , (𝑘 ∈ ℕ ↦ (vol‘((𝐹‘𝑘) ∖ ∪ 𝑚 ∈ (1..^𝑘)(𝐹‘𝑚))))) Fn (ℤ_≥‘1))
46	44, 45	ax-mp 5	. . . . . . . . . 10 ⊢ seq1( + , (𝑘 ∈ ℕ ↦ (vol‘((𝐹‘𝑘) ∖ ∪ 𝑚 ∈ (1..^𝑘)(𝐹‘𝑚))))) Fn (ℤ_≥‘1)
47	6	fneq2i 6666	. . . . . . . . . 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 25564	. . . . . . . . . 10 ⊢ vol:dom vol⟶(0[,]+∞)
51		simpll 767	. . . . . . . . . 10 ⊢ (((𝐹:ℕ⟶dom vol ∧ ∀𝑛 ∈ ℕ (𝐹‘𝑛) ⊆ (𝐹‘(𝑛 + 1))) ∧ ∀𝑘 ∈ ℕ (vol‘(𝐹‘𝑘)) ∈ ℝ) → 𝐹:ℕ⟶dom vol)
52		fco 6760	. . . . . . . . . 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 6737	. . . . . . . 8 ⊢ (((𝐹:ℕ⟶dom vol ∧ ∀𝑛 ∈ ℕ (𝐹‘𝑛) ⊆ (𝐹‘(𝑛 + 1))) ∧ ∀𝑘 ∈ ℕ (vol‘(𝐹‘𝑘)) ∈ ℝ) → (vol ∘ 𝐹) Fn ℕ)
55		fveq2 6906	. . . . . . . . . . . . 13 ⊢ (𝑥 = 1 → (seq1( + , (𝑘 ∈ ℕ ↦ (vol‘((𝐹‘𝑘) ∖ ∪ 𝑚 ∈ (1..^𝑘)(𝐹‘𝑚)))))‘𝑥) = (seq1( + , (𝑘 ∈ ℕ ↦ (vol‘((𝐹‘𝑘) ∖ ∪ 𝑚 ∈ (1..^𝑘)(𝐹‘𝑚)))))‘1))
56		2fveq3 6911	. . . . . . . . . . . . 13 ⊢ (𝑥 = 1 → (vol‘(𝐹‘𝑥)) = (vol‘(𝐹‘1)))
57	55, 56	eqeq12d 2753	. . . . . . . . . . . 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 6906	. . . . . . . . . . . . 13 ⊢ (𝑥 = 𝑗 → (seq1( + , (𝑘 ∈ ℕ ↦ (vol‘((𝐹‘𝑘) ∖ ∪ 𝑚 ∈ (1..^𝑘)(𝐹‘𝑚)))))‘𝑥) = (seq1( + , (𝑘 ∈ ℕ ↦ (vol‘((𝐹‘𝑘) ∖ ∪ 𝑚 ∈ (1..^𝑘)(𝐹‘𝑚)))))‘𝑗))
60		2fveq3 6911	. . . . . . . . . . . . 13 ⊢ (𝑥 = 𝑗 → (vol‘(𝐹‘𝑥)) = (vol‘(𝐹‘𝑗)))
61	59, 60	eqeq12d 2753	. . . . . . . . . . . 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 6906	. . . . . . . . . . . . 13 ⊢ (𝑥 = (𝑗 + 1) → (seq1( + , (𝑘 ∈ ℕ ↦ (vol‘((𝐹‘𝑘) ∖ ∪ 𝑚 ∈ (1..^𝑘)(𝐹‘𝑚)))))‘𝑥) = (seq1( + , (𝑘 ∈ ℕ ↦ (vol‘((𝐹‘𝑘) ∖ ∪ 𝑚 ∈ (1..^𝑘)(𝐹‘𝑚)))))‘(𝑗 + 1)))
64		2fveq3 6911	. . . . . . . . . . . . 13 ⊢ (𝑥 = (𝑗 + 1) → (vol‘(𝐹‘𝑥)) = (vol‘(𝐹‘(𝑗 + 1))))
65	63, 64	eqeq12d 2753	. . . . . . . . . . . 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 14055	. . . . . . . . . . . . . 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 12277	. . . . . . . . . . . . . 14 ⊢ 1 ∈ ℕ
70		oveq2 7439	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (𝑘 = 1 → (1..^𝑘) = (1..^1))
71		fzo0 13723	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (1..^1) = ∅
72	70, 71	eqtrdi 2793	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (𝑘 = 1 → (1..^𝑘) = ∅)
73	72	iuneq1d 5019	. . . . . . . . . . . . . . . . . . . 20 ⊢ (𝑘 = 1 → ∪ 𝑚 ∈ (1..^𝑘)(𝐹‘𝑚) = ∪ 𝑚 ∈ ∅ (𝐹‘𝑚))
74		0iun 5063	. . . . . . . . . . . . . . . . . . . 20 ⊢ ∪ 𝑚 ∈ ∅ (𝐹‘𝑚) = ∅
75	73, 74	eqtrdi 2793	. . . . . . . . . . . . . . . . . . 19 ⊢ (𝑘 = 1 → ∪ 𝑚 ∈ (1..^𝑘)(𝐹‘𝑚) = ∅)
76	75	difeq2d 4126	. . . . . . . . . . . . . . . . . 18 ⊢ (𝑘 = 1 → ((𝐹‘𝑘) ∖ ∪ 𝑚 ∈ (1..^𝑘)(𝐹‘𝑚)) = ((𝐹‘𝑘) ∖ ∅))
77		dif0 4378	. . . . . . . . . . . . . . . . . 18 ⊢ ((𝐹‘𝑘) ∖ ∅) = (𝐹‘𝑘)
78	76, 77	eqtrdi 2793	. . . . . . . . . . . . . . . . 17 ⊢ (𝑘 = 1 → ((𝐹‘𝑘) ∖ ∪ 𝑚 ∈ (1..^𝑘)(𝐹‘𝑚)) = (𝐹‘𝑘))
79		fveq2 6906	. . . . . . . . . . . . . . . . 17 ⊢ (𝑘 = 1 → (𝐹‘𝑘) = (𝐹‘1))
80	78, 79	eqtrd 2777	. . . . . . . . . . . . . . . 16 ⊢ (𝑘 = 1 → ((𝐹‘𝑘) ∖ ∪ 𝑚 ∈ (1..^𝑘)(𝐹‘𝑚)) = (𝐹‘1))
81	80	fveq2d 6910	. . . . . . . . . . . . . . 15 ⊢ (𝑘 = 1 → (vol‘((𝐹‘𝑘) ∖ ∪ 𝑚 ∈ (1..^𝑘)(𝐹‘𝑚))) = (vol‘(𝐹‘1)))
82		fvex 6919	. . . . . . . . . . . . . . 15 ⊢ (vol‘(𝐹‘1)) ∈ V
83	81, 34, 82	fvmpt 7016	. . . . . . . . . . . . . 14 ⊢ (1 ∈ ℕ → ((𝑘 ∈ ℕ ↦ (vol‘((𝐹‘𝑘) ∖ ∪ 𝑚 ∈ (1..^𝑘)(𝐹‘𝑚))))‘1) = (vol‘(𝐹‘1)))
84	69, 83	ax-mp 5	. . . . . . . . . . . . 13 ⊢ ((𝑘 ∈ ℕ ↦ (vol‘((𝐹‘𝑘) ∖ ∪ 𝑚 ∈ (1..^𝑘)(𝐹‘𝑚))))‘1) = (vol‘(𝐹‘1))
85	68, 84	eqtri 2765	. . . . . . . . . . . 12 ⊢ (seq1( + , (𝑘 ∈ ℕ ↦ (vol‘((𝐹‘𝑘) ∖ ∪ 𝑚 ∈ (1..^𝑘)(𝐹‘𝑚)))))‘1) = (vol‘(𝐹‘1))
86	85	a1i 11	. . . . . . . . . . 11 ⊢ (((𝐹:ℕ⟶dom vol ∧ ∀𝑛 ∈ ℕ (𝐹‘𝑛) ⊆ (𝐹‘(𝑛 + 1))) ∧ ∀𝑘 ∈ ℕ (vol‘(𝐹‘𝑘)) ∈ ℝ) → (seq1( + , (𝑘 ∈ ℕ ↦ (vol‘((𝐹‘𝑘) ∖ ∪ 𝑚 ∈ (1..^𝑘)(𝐹‘𝑚)))))‘1) = (vol‘(𝐹‘1)))
87		oveq1 7438	. . . . . . . . . . . . . 14 ⊢ ((seq1( + , (𝑘 ∈ ℕ ↦ (vol‘((𝐹‘𝑘) ∖ ∪ 𝑚 ∈ (1..^𝑘)(𝐹‘𝑚)))))‘𝑗) = (vol‘(𝐹‘𝑗)) → ((seq1( + , (𝑘 ∈ ℕ ↦ (vol‘((𝐹‘𝑘) ∖ ∪ 𝑚 ∈ (1..^𝑘)(𝐹‘𝑚)))))‘𝑗) + ((𝑘 ∈ ℕ ↦ (vol‘((𝐹‘𝑘) ∖ ∪ 𝑚 ∈ (1..^𝑘)(𝐹‘𝑚))))‘(𝑗 + 1))) = ((vol‘(𝐹‘𝑗)) + ((𝑘 ∈ ℕ ↦ (vol‘((𝐹‘𝑘) ∖ ∪ 𝑚 ∈ (1..^𝑘)(𝐹‘𝑚))))‘(𝑗 + 1))))
88		seqp1 14057	. . . . . . . . . . . . . . . . 17 ⊢ (𝑗 ∈ (ℤ_≥‘1) → (seq1( + , (𝑘 ∈ ℕ ↦ (vol‘((𝐹‘𝑘) ∖ ∪ 𝑚 ∈ (1..^𝑘)(𝐹‘𝑚)))))‘(𝑗 + 1)) = ((seq1( + , (𝑘 ∈ ℕ ↦ (vol‘((𝐹‘𝑘) ∖ ∪ 𝑚 ∈ (1..^𝑘)(𝐹‘𝑚)))))‘𝑗) + ((𝑘 ∈ ℕ ↦ (vol‘((𝐹‘𝑘) ∖ ∪ 𝑚 ∈ (1..^𝑘)(𝐹‘𝑚))))‘(𝑗 + 1))))
89	88, 6	eleq2s 2859	. . . . . . . . . . . . . . . 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 4477	. . . . . . . . . . . . . . . . . 18 ⊢ ((𝐹‘𝑗) ∪ ((𝐹‘(𝑗 + 1)) ∖ (𝐹‘𝑗))) = ((𝐹‘𝑗) ∪ (𝐹‘(𝑗 + 1)))
92		fveq2 6906	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (𝑛 = 𝑗 → (𝐹‘𝑛) = (𝐹‘𝑗))
93		fvoveq1 7454	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (𝑛 = 𝑗 → (𝐹‘(𝑛 + 1)) = (𝐹‘(𝑗 + 1)))
94	92, 93	sseq12d 4017	. . . . . . . . . . . . . . . . . . . 20 ⊢ (𝑛 = 𝑗 → ((𝐹‘𝑛) ⊆ (𝐹‘(𝑛 + 1)) ↔ (𝐹‘𝑗) ⊆ (𝐹‘(𝑗 + 1))))
95		simpllr 776	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((((𝐹:ℕ⟶dom vol ∧ ∀𝑛 ∈ ℕ (𝐹‘𝑛) ⊆ (𝐹‘(𝑛 + 1))) ∧ ∀𝑘 ∈ ℕ (vol‘(𝐹‘𝑘)) ∈ ℝ) ∧ 𝑗 ∈ ℕ) → ∀𝑛 ∈ ℕ (𝐹‘𝑛) ⊆ (𝐹‘(𝑛 + 1)))
96		simpr 484	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((((𝐹:ℕ⟶dom vol ∧ ∀𝑛 ∈ ℕ (𝐹‘𝑛) ⊆ (𝐹‘(𝑛 + 1))) ∧ ∀𝑘 ∈ ℕ (vol‘(𝐹‘𝑘)) ∈ ℝ) ∧ 𝑗 ∈ ℕ) → 𝑗 ∈ ℕ)
97	94, 95, 96	rspcdva 3623	. . . . . . . . . . . . . . . . . . 19 ⊢ ((((𝐹:ℕ⟶dom vol ∧ ∀𝑛 ∈ ℕ (𝐹‘𝑛) ⊆ (𝐹‘(𝑛 + 1))) ∧ ∀𝑘 ∈ ℕ (vol‘(𝐹‘𝑘)) ∈ ℝ) ∧ 𝑗 ∈ ℕ) → (𝐹‘𝑗) ⊆ (𝐹‘(𝑗 + 1)))
98		ssequn1 4186	. . . . . . . . . . . . . . . . . . 19 ⊢ ((𝐹‘𝑗) ⊆ (𝐹‘(𝑗 + 1)) ↔ ((𝐹‘𝑗) ∪ (𝐹‘(𝑗 + 1))) = (𝐹‘(𝑗 + 1)))
99	97, 98	sylib 218	. . . . . . . . . . . . . . . . . 18 ⊢ ((((𝐹:ℕ⟶dom vol ∧ ∀𝑛 ∈ ℕ (𝐹‘𝑛) ⊆ (𝐹‘(𝑛 + 1))) ∧ ∀𝑘 ∈ ℕ (vol‘(𝐹‘𝑘)) ∈ ℝ) ∧ 𝑗 ∈ ℕ) → ((𝐹‘𝑗) ∪ (𝐹‘(𝑗 + 1))) = (𝐹‘(𝑗 + 1)))
100	91, 99	eqtr2id 2790	. . . . . . . . . . . . . . . . 17 ⊢ ((((𝐹:ℕ⟶dom vol ∧ ∀𝑛 ∈ ℕ (𝐹‘𝑛) ⊆ (𝐹‘(𝑛 + 1))) ∧ ∀𝑘 ∈ ℕ (vol‘(𝐹‘𝑘)) ∈ ℝ) ∧ 𝑗 ∈ ℕ) → (𝐹‘(𝑗 + 1)) = ((𝐹‘𝑗) ∪ ((𝐹‘(𝑗 + 1)) ∖ (𝐹‘𝑗))))
101	100	fveq2d 6910	. . . . . . . . . . . . . . . 16 ⊢ ((((𝐹:ℕ⟶dom vol ∧ ∀𝑛 ∈ ℕ (𝐹‘𝑛) ⊆ (𝐹‘(𝑛 + 1))) ∧ ∀𝑘 ∈ ℕ (vol‘(𝐹‘𝑘)) ∈ ℝ) ∧ 𝑗 ∈ ℕ) → (vol‘(𝐹‘(𝑗 + 1))) = (vol‘((𝐹‘𝑗) ∪ ((𝐹‘(𝑗 + 1)) ∖ (𝐹‘𝑗)))))
102		simplll 775	. . . . . . . . . . . . . . . . . 18 ⊢ ((((𝐹:ℕ⟶dom vol ∧ ∀𝑛 ∈ ℕ (𝐹‘𝑛) ⊆ (𝐹‘(𝑛 + 1))) ∧ ∀𝑘 ∈ ℕ (vol‘(𝐹‘𝑘)) ∈ ℝ) ∧ 𝑗 ∈ ℕ) → 𝐹:ℕ⟶dom vol)
103	102, 96	ffvelcdmd 7105	. . . . . . . . . . . . . . . . 17 ⊢ ((((𝐹:ℕ⟶dom vol ∧ ∀𝑛 ∈ ℕ (𝐹‘𝑛) ⊆ (𝐹‘(𝑛 + 1))) ∧ ∀𝑘 ∈ ℕ (vol‘(𝐹‘𝑘)) ∈ ℝ) ∧ 𝑗 ∈ ℕ) → (𝐹‘𝑗) ∈ dom vol)
104		peano2nn 12278	. . . . . . . . . . . . . . . . . . . 20 ⊢ (𝑗 ∈ ℕ → (𝑗 + 1) ∈ ℕ)
105	104	adantl 481	. . . . . . . . . . . . . . . . . . 19 ⊢ ((((𝐹:ℕ⟶dom vol ∧ ∀𝑛 ∈ ℕ (𝐹‘𝑛) ⊆ (𝐹‘(𝑛 + 1))) ∧ ∀𝑘 ∈ ℕ (vol‘(𝐹‘𝑘)) ∈ ℝ) ∧ 𝑗 ∈ ℕ) → (𝑗 + 1) ∈ ℕ)
106	102, 105	ffvelcdmd 7105	. . . . . . . . . . . . . . . . . 18 ⊢ ((((𝐹:ℕ⟶dom vol ∧ ∀𝑛 ∈ ℕ (𝐹‘𝑛) ⊆ (𝐹‘(𝑛 + 1))) ∧ ∀𝑘 ∈ ℕ (vol‘(𝐹‘𝑘)) ∈ ℝ) ∧ 𝑗 ∈ ℕ) → (𝐹‘(𝑗 + 1)) ∈ dom vol)
107		difmbl 25578	. . . . . . . . . . . . . . . . . 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 4472	. . . . . . . . . . . . . . . . . 18 ⊢ ((𝐹‘𝑗) ∩ ((𝐹‘(𝑗 + 1)) ∖ (𝐹‘𝑗))) = ∅
110	109	a1i 11	. . . . . . . . . . . . . . . . 17 ⊢ ((((𝐹:ℕ⟶dom vol ∧ ∀𝑛 ∈ ℕ (𝐹‘𝑛) ⊆ (𝐹‘(𝑛 + 1))) ∧ ∀𝑘 ∈ ℕ (vol‘(𝐹‘𝑘)) ∈ ℝ) ∧ 𝑗 ∈ ℕ) → ((𝐹‘𝑗) ∩ ((𝐹‘(𝑗 + 1)) ∖ (𝐹‘𝑗))) = ∅)
111		2fveq3 6911	. . . . . . . . . . . . . . . . . . 19 ⊢ (𝑘 = 𝑗 → (vol‘(𝐹‘𝑘)) = (vol‘(𝐹‘𝑗)))
112	111	eleq1d 2826	. . . . . . . . . . . . . . . . . 18 ⊢ (𝑘 = 𝑗 → ((vol‘(𝐹‘𝑘)) ∈ ℝ ↔ (vol‘(𝐹‘𝑗)) ∈ ℝ))
113		simplr 769	. . . . . . . . . . . . . . . . . 18 ⊢ ((((𝐹:ℕ⟶dom vol ∧ ∀𝑛 ∈ ℕ (𝐹‘𝑛) ⊆ (𝐹‘(𝑛 + 1))) ∧ ∀𝑘 ∈ ℕ (vol‘(𝐹‘𝑘)) ∈ ℝ) ∧ 𝑗 ∈ ℕ) → ∀𝑘 ∈ ℕ (vol‘(𝐹‘𝑘)) ∈ ℝ)
114	112, 113, 96	rspcdva 3623	. . . . . . . . . . . . . . . . 17 ⊢ ((((𝐹:ℕ⟶dom vol ∧ ∀𝑛 ∈ ℕ (𝐹‘𝑛) ⊆ (𝐹‘(𝑛 + 1))) ∧ ∀𝑘 ∈ ℕ (vol‘(𝐹‘𝑘)) ∈ ℝ) ∧ 𝑗 ∈ ℕ) → (vol‘(𝐹‘𝑗)) ∈ ℝ)
115		mblvol 25565	. . . . . . . . . . . . . . . . . . 19 ⊢ (((𝐹‘(𝑗 + 1)) ∖ (𝐹‘𝑗)) ∈ dom vol → (vol‘((𝐹‘(𝑗 + 1)) ∖ (𝐹‘𝑗))) = (vol*‘((𝐹‘(𝑗 + 1)) ∖ (𝐹‘𝑗))))
116	108, 115	syl 17	. . . . . . . . . . . . . . . . . 18 ⊢ ((((𝐹:ℕ⟶dom vol ∧ ∀𝑛 ∈ ℕ (𝐹‘𝑛) ⊆ (𝐹‘(𝑛 + 1))) ∧ ∀𝑘 ∈ ℕ (vol‘(𝐹‘𝑘)) ∈ ℝ) ∧ 𝑗 ∈ ℕ) → (vol‘((𝐹‘(𝑗 + 1)) ∖ (𝐹‘𝑗))) = (vol*‘((𝐹‘(𝑗 + 1)) ∖ (𝐹‘𝑗))))
117		difssd 4137	. . . . . . . . . . . . . . . . . . 19 ⊢ ((((𝐹:ℕ⟶dom vol ∧ ∀𝑛 ∈ ℕ (𝐹‘𝑛) ⊆ (𝐹‘(𝑛 + 1))) ∧ ∀𝑘 ∈ ℕ (vol‘(𝐹‘𝑘)) ∈ ℝ) ∧ 𝑗 ∈ ℕ) → ((𝐹‘(𝑗 + 1)) ∖ (𝐹‘𝑗)) ⊆ (𝐹‘(𝑗 + 1)))
118		mblss 25566	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((𝐹‘(𝑗 + 1)) ∈ dom vol → (𝐹‘(𝑗 + 1)) ⊆ ℝ)
119	106, 118	syl 17	. . . . . . . . . . . . . . . . . . 19 ⊢ ((((𝐹:ℕ⟶dom vol ∧ ∀𝑛 ∈ ℕ (𝐹‘𝑛) ⊆ (𝐹‘(𝑛 + 1))) ∧ ∀𝑘 ∈ ℕ (vol‘(𝐹‘𝑘)) ∈ ℝ) ∧ 𝑗 ∈ ℕ) → (𝐹‘(𝑗 + 1)) ⊆ ℝ)
120		mblvol 25565	. . . . . . . . . . . . . . . . . . . . 21 ⊢ ((𝐹‘(𝑗 + 1)) ∈ dom vol → (vol‘(𝐹‘(𝑗 + 1))) = (vol*‘(𝐹‘(𝑗 + 1))))
121	106, 120	syl 17	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((((𝐹:ℕ⟶dom vol ∧ ∀𝑛 ∈ ℕ (𝐹‘𝑛) ⊆ (𝐹‘(𝑛 + 1))) ∧ ∀𝑘 ∈ ℕ (vol‘(𝐹‘𝑘)) ∈ ℝ) ∧ 𝑗 ∈ ℕ) → (vol‘(𝐹‘(𝑗 + 1))) = (vol*‘(𝐹‘(𝑗 + 1))))
122		2fveq3 6911	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (𝑘 = (𝑗 + 1) → (vol‘(𝐹‘𝑘)) = (vol‘(𝐹‘(𝑗 + 1))))
123	122	eleq1d 2826	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (𝑘 = (𝑗 + 1) → ((vol‘(𝐹‘𝑘)) ∈ ℝ ↔ (vol‘(𝐹‘(𝑗 + 1))) ∈ ℝ))
124	123, 113, 105	rspcdva 3623	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((((𝐹:ℕ⟶dom vol ∧ ∀𝑛 ∈ ℕ (𝐹‘𝑛) ⊆ (𝐹‘(𝑛 + 1))) ∧ ∀𝑘 ∈ ℕ (vol‘(𝐹‘𝑘)) ∈ ℝ) ∧ 𝑗 ∈ ℕ) → (vol‘(𝐹‘(𝑗 + 1))) ∈ ℝ)
125	121, 124	eqeltrrd 2842	. . . . . . . . . . . . . . . . . . 19 ⊢ ((((𝐹:ℕ⟶dom vol ∧ ∀𝑛 ∈ ℕ (𝐹‘𝑛) ⊆ (𝐹‘(𝑛 + 1))) ∧ ∀𝑘 ∈ ℕ (vol‘(𝐹‘𝑘)) ∈ ℝ) ∧ 𝑗 ∈ ℕ) → (vol*‘(𝐹‘(𝑗 + 1))) ∈ ℝ)
126		ovolsscl 25521	. . . . . . . . . . . . . . . . . . 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 2841	. . . . . . . . . . . . . . . . 17 ⊢ ((((𝐹:ℕ⟶dom vol ∧ ∀𝑛 ∈ ℕ (𝐹‘𝑛) ⊆ (𝐹‘(𝑛 + 1))) ∧ ∀𝑘 ∈ ℕ (vol‘(𝐹‘𝑘)) ∈ ℝ) ∧ 𝑗 ∈ ℕ) → (vol‘((𝐹‘(𝑗 + 1)) ∖ (𝐹‘𝑗))) ∈ ℝ)
129		volun 25580	. . . . . . . . . . . . . . . . 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 13593	. . . . . . . . . . . . . . . . . . . . . . . . . 26 ⊢ (𝑚 ∈ (1...𝑗) → 𝑚 ∈ ℕ)
133	132	adantl 481	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ (((((𝐹:ℕ⟶dom vol ∧ ∀𝑛 ∈ ℕ (𝐹‘𝑛) ⊆ (𝐹‘(𝑛 + 1))) ∧ ∀𝑘 ∈ ℕ (vol‘(𝐹‘𝑘)) ∈ ℝ) ∧ 𝑗 ∈ ℕ) ∧ 𝑚 ∈ (1...𝑗)) → 𝑚 ∈ ℕ)
134		elfzuz3 13561	. . . . . . . . . . . . . . . . . . . . . . . . . 26 ⊢ (𝑚 ∈ (1...𝑗) → 𝑗 ∈ (ℤ_≥‘𝑚))
135	134	adantl 481	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ (((((𝐹:ℕ⟶dom vol ∧ ∀𝑛 ∈ ℕ (𝐹‘𝑛) ⊆ (𝐹‘(𝑛 + 1))) ∧ ∀𝑘 ∈ ℕ (vol‘(𝐹‘𝑘)) ∈ ℝ) ∧ 𝑗 ∈ ℕ) ∧ 𝑚 ∈ (1...𝑗)) → 𝑗 ∈ (ℤ_≥‘𝑚))
136		volsuplem 25590	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ ((∀𝑛 ∈ ℕ (𝐹‘𝑛) ⊆ (𝐹‘(𝑛 + 1)) ∧ (𝑚 ∈ ℕ ∧ 𝑗 ∈ (ℤ_≥‘𝑚))) → (𝐹‘𝑚) ⊆ (𝐹‘𝑗))
137	131, 133, 135, 136	syl12anc 837	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ (((((𝐹:ℕ⟶dom vol ∧ ∀𝑛 ∈ ℕ (𝐹‘𝑛) ⊆ (𝐹‘(𝑛 + 1))) ∧ ∀𝑘 ∈ ℕ (vol‘(𝐹‘𝑘)) ∈ ℝ) ∧ 𝑗 ∈ ℕ) ∧ 𝑚 ∈ (1...𝑗)) → (𝐹‘𝑚) ⊆ (𝐹‘𝑗))
138	137	ralrimiva 3146	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ ((((𝐹:ℕ⟶dom vol ∧ ∀𝑛 ∈ ℕ (𝐹‘𝑛) ⊆ (𝐹‘(𝑛 + 1))) ∧ ∀𝑘 ∈ ℕ (vol‘(𝐹‘𝑘)) ∈ ℝ) ∧ 𝑗 ∈ ℕ) → ∀𝑚 ∈ (1...𝑗)(𝐹‘𝑚) ⊆ (𝐹‘𝑗))
139		iunss 5045	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ (∪ 𝑚 ∈ (1...𝑗)(𝐹‘𝑚) ⊆ (𝐹‘𝑗) ↔ ∀𝑚 ∈ (1...𝑗)(𝐹‘𝑚) ⊆ (𝐹‘𝑗))
140	138, 139	sylibr 234	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ ((((𝐹:ℕ⟶dom vol ∧ ∀𝑛 ∈ ℕ (𝐹‘𝑛) ⊆ (𝐹‘(𝑛 + 1))) ∧ ∀𝑘 ∈ ℕ (vol‘(𝐹‘𝑘)) ∈ ℝ) ∧ 𝑗 ∈ ℕ) → ∪ 𝑚 ∈ (1...𝑗)(𝐹‘𝑚) ⊆ (𝐹‘𝑗))
141	96, 6	eleqtrdi 2851	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ ((((𝐹:ℕ⟶dom vol ∧ ∀𝑛 ∈ ℕ (𝐹‘𝑛) ⊆ (𝐹‘(𝑛 + 1))) ∧ ∀𝑘 ∈ ℕ (vol‘(𝐹‘𝑘)) ∈ ℝ) ∧ 𝑗 ∈ ℕ) → 𝑗 ∈ (ℤ_≥‘1))
142		eluzfz2 13572	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ (𝑗 ∈ (ℤ_≥‘1) → 𝑗 ∈ (1...𝑗))
143	141, 142	syl 17	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ ((((𝐹:ℕ⟶dom vol ∧ ∀𝑛 ∈ ℕ (𝐹‘𝑛) ⊆ (𝐹‘(𝑛 + 1))) ∧ ∀𝑘 ∈ ℕ (vol‘(𝐹‘𝑘)) ∈ ℝ) ∧ 𝑗 ∈ ℕ) → 𝑗 ∈ (1...𝑗))
144		fveq2 6906	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ (𝑚 = 𝑗 → (𝐹‘𝑚) = (𝐹‘𝑗))
145	144	ssiun2s 5048	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ (𝑗 ∈ (1...𝑗) → (𝐹‘𝑗) ⊆ ∪ 𝑚 ∈ (1...𝑗)(𝐹‘𝑚))
146	143, 145	syl 17	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ ((((𝐹:ℕ⟶dom vol ∧ ∀𝑛 ∈ ℕ (𝐹‘𝑛) ⊆ (𝐹‘(𝑛 + 1))) ∧ ∀𝑘 ∈ ℕ (vol‘(𝐹‘𝑘)) ∈ ℝ) ∧ 𝑗 ∈ ℕ) → (𝐹‘𝑗) ⊆ ∪ 𝑚 ∈ (1...𝑗)(𝐹‘𝑚))
147	140, 146	eqssd 4001	. . . . . . . . . . . . . . . . . . . . 21 ⊢ ((((𝐹:ℕ⟶dom vol ∧ ∀𝑛 ∈ ℕ (𝐹‘𝑛) ⊆ (𝐹‘(𝑛 + 1))) ∧ ∀𝑘 ∈ ℕ (vol‘(𝐹‘𝑘)) ∈ ℝ) ∧ 𝑗 ∈ ℕ) → ∪ 𝑚 ∈ (1...𝑗)(𝐹‘𝑚) = (𝐹‘𝑗))
148	96	nnzd 12640	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ ((((𝐹:ℕ⟶dom vol ∧ ∀𝑛 ∈ ℕ (𝐹‘𝑛) ⊆ (𝐹‘(𝑛 + 1))) ∧ ∀𝑘 ∈ ℕ (vol‘(𝐹‘𝑘)) ∈ ℝ) ∧ 𝑗 ∈ ℕ) → 𝑗 ∈ ℤ)
149		fzval3 13773	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ (𝑗 ∈ ℤ → (1...𝑗) = (1..^(𝑗 + 1)))
150	148, 149	syl 17	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ ((((𝐹:ℕ⟶dom vol ∧ ∀𝑛 ∈ ℕ (𝐹‘𝑛) ⊆ (𝐹‘(𝑛 + 1))) ∧ ∀𝑘 ∈ ℕ (vol‘(𝐹‘𝑘)) ∈ ℝ) ∧ 𝑗 ∈ ℕ) → (1...𝑗) = (1..^(𝑗 + 1)))
151	150	iuneq1d 5019	. . . . . . . . . . . . . . . . . . . . 21 ⊢ ((((𝐹:ℕ⟶dom vol ∧ ∀𝑛 ∈ ℕ (𝐹‘𝑛) ⊆ (𝐹‘(𝑛 + 1))) ∧ ∀𝑘 ∈ ℕ (vol‘(𝐹‘𝑘)) ∈ ℝ) ∧ 𝑗 ∈ ℕ) → ∪ 𝑚 ∈ (1...𝑗)(𝐹‘𝑚) = ∪ 𝑚 ∈ (1..^(𝑗 + 1))(𝐹‘𝑚))
152	147, 151	eqtr3d 2779	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((((𝐹:ℕ⟶dom vol ∧ ∀𝑛 ∈ ℕ (𝐹‘𝑛) ⊆ (𝐹‘(𝑛 + 1))) ∧ ∀𝑘 ∈ ℕ (vol‘(𝐹‘𝑘)) ∈ ℝ) ∧ 𝑗 ∈ ℕ) → (𝐹‘𝑗) = ∪ 𝑚 ∈ (1..^(𝑗 + 1))(𝐹‘𝑚))
153	152	difeq2d 4126	. . . . . . . . . . . . . . . . . . 19 ⊢ ((((𝐹:ℕ⟶dom vol ∧ ∀𝑛 ∈ ℕ (𝐹‘𝑛) ⊆ (𝐹‘(𝑛 + 1))) ∧ ∀𝑘 ∈ ℕ (vol‘(𝐹‘𝑘)) ∈ ℝ) ∧ 𝑗 ∈ ℕ) → ((𝐹‘(𝑗 + 1)) ∖ (𝐹‘𝑗)) = ((𝐹‘(𝑗 + 1)) ∖ ∪ 𝑚 ∈ (1..^(𝑗 + 1))(𝐹‘𝑚)))
154	153	fveq2d 6910	. . . . . . . . . . . . . . . . . 18 ⊢ ((((𝐹:ℕ⟶dom vol ∧ ∀𝑛 ∈ ℕ (𝐹‘𝑛) ⊆ (𝐹‘(𝑛 + 1))) ∧ ∀𝑘 ∈ ℕ (vol‘(𝐹‘𝑘)) ∈ ℝ) ∧ 𝑗 ∈ ℕ) → (vol‘((𝐹‘(𝑗 + 1)) ∖ (𝐹‘𝑗))) = (vol‘((𝐹‘(𝑗 + 1)) ∖ ∪ 𝑚 ∈ (1..^(𝑗 + 1))(𝐹‘𝑚))))
155		fveq2 6906	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (𝑘 = (𝑗 + 1) → (𝐹‘𝑘) = (𝐹‘(𝑗 + 1)))
156		oveq2 7439	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ (𝑘 = (𝑗 + 1) → (1..^𝑘) = (1..^(𝑗 + 1)))
157	156	iuneq1d 5019	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (𝑘 = (𝑗 + 1) → ∪ 𝑚 ∈ (1..^𝑘)(𝐹‘𝑚) = ∪ 𝑚 ∈ (1..^(𝑗 + 1))(𝐹‘𝑚))
158	155, 157	difeq12d 4127	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (𝑘 = (𝑗 + 1) → ((𝐹‘𝑘) ∖ ∪ 𝑚 ∈ (1..^𝑘)(𝐹‘𝑚)) = ((𝐹‘(𝑗 + 1)) ∖ ∪ 𝑚 ∈ (1..^(𝑗 + 1))(𝐹‘𝑚)))
159	158	fveq2d 6910	. . . . . . . . . . . . . . . . . . . 20 ⊢ (𝑘 = (𝑗 + 1) → (vol‘((𝐹‘𝑘) ∖ ∪ 𝑚 ∈ (1..^𝑘)(𝐹‘𝑚))) = (vol‘((𝐹‘(𝑗 + 1)) ∖ ∪ 𝑚 ∈ (1..^(𝑗 + 1))(𝐹‘𝑚))))
160		fvex 6919	. . . . . . . . . . . . . . . . . . . 20 ⊢ (vol‘((𝐹‘(𝑗 + 1)) ∖ ∪ 𝑚 ∈ (1..^(𝑗 + 1))(𝐹‘𝑚))) ∈ V
161	159, 34, 160	fvmpt 7016	. . . . . . . . . . . . . . . . . . 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 2780	. . . . . . . . . . . . . . . . 17 ⊢ ((((𝐹:ℕ⟶dom vol ∧ ∀𝑛 ∈ ℕ (𝐹‘𝑛) ⊆ (𝐹‘(𝑛 + 1))) ∧ ∀𝑘 ∈ ℕ (vol‘(𝐹‘𝑘)) ∈ ℝ) ∧ 𝑗 ∈ ℕ) → (vol‘((𝐹‘(𝑗 + 1)) ∖ (𝐹‘𝑗))) = ((𝑘 ∈ ℕ ↦ (vol‘((𝐹‘𝑘) ∖ ∪ 𝑚 ∈ (1..^𝑘)(𝐹‘𝑚))))‘(𝑗 + 1)))
164	163	oveq2d 7447	. . . . . . . . . . . . . . . 16 ⊢ ((((𝐹:ℕ⟶dom vol ∧ ∀𝑛 ∈ ℕ (𝐹‘𝑛) ⊆ (𝐹‘(𝑛 + 1))) ∧ ∀𝑘 ∈ ℕ (vol‘(𝐹‘𝑘)) ∈ ℝ) ∧ 𝑗 ∈ ℕ) → ((vol‘(𝐹‘𝑗)) + (vol‘((𝐹‘(𝑗 + 1)) ∖ (𝐹‘𝑗)))) = ((vol‘(𝐹‘𝑗)) + ((𝑘 ∈ ℕ ↦ (vol‘((𝐹‘𝑘) ∖ ∪ 𝑚 ∈ (1..^𝑘)(𝐹‘𝑚))))‘(𝑗 + 1))))
165	101, 130, 164	3eqtrd 2781	. . . . . . . . . . . . . . 15 ⊢ ((((𝐹:ℕ⟶dom vol ∧ ∀𝑛 ∈ ℕ (𝐹‘𝑛) ⊆ (𝐹‘(𝑛 + 1))) ∧ ∀𝑘 ∈ ℕ (vol‘(𝐹‘𝑘)) ∈ ℝ) ∧ 𝑗 ∈ ℕ) → (vol‘(𝐹‘(𝑗 + 1))) = ((vol‘(𝐹‘𝑗)) + ((𝑘 ∈ ℕ ↦ (vol‘((𝐹‘𝑘) ∖ ∪ 𝑚 ∈ (1..^𝑘)(𝐹‘𝑚))))‘(𝑗 + 1))))
166	90, 165	eqeq12d 2753	. . . . . . . . . . . . . 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 12284	. . . . . . . . . 10 ⊢ (𝑗 ∈ ℕ → (((𝐹:ℕ⟶dom vol ∧ ∀𝑛 ∈ ℕ (𝐹‘𝑛) ⊆ (𝐹‘(𝑛 + 1))) ∧ ∀𝑘 ∈ ℕ (vol‘(𝐹‘𝑘)) ∈ ℝ) → (seq1( + , (𝑘 ∈ ℕ ↦ (vol‘((𝐹‘𝑘) ∖ ∪ 𝑚 ∈ (1..^𝑘)(𝐹‘𝑚)))))‘𝑗) = (vol‘(𝐹‘𝑗))))
171	170	impcom 407	. . . . . . . . 9 ⊢ ((((𝐹:ℕ⟶dom vol ∧ ∀𝑛 ∈ ℕ (𝐹‘𝑛) ⊆ (𝐹‘(𝑛 + 1))) ∧ ∀𝑘 ∈ ℕ (vol‘(𝐹‘𝑘)) ∈ ℝ) ∧ 𝑗 ∈ ℕ) → (seq1( + , (𝑘 ∈ ℕ ↦ (vol‘((𝐹‘𝑘) ∖ ∪ 𝑚 ∈ (1..^𝑘)(𝐹‘𝑚)))))‘𝑗) = (vol‘(𝐹‘𝑗)))
172		fvco3 7008	. . . . . . . . . 10 ⊢ ((𝐹:ℕ⟶dom vol ∧ 𝑗 ∈ ℕ) → ((vol ∘ 𝐹)‘𝑗) = (vol‘(𝐹‘𝑗)))
173	51, 172	sylan 580	. . . . . . . . 9 ⊢ ((((𝐹:ℕ⟶dom vol ∧ ∀𝑛 ∈ ℕ (𝐹‘𝑛) ⊆ (𝐹‘(𝑛 + 1))) ∧ ∀𝑘 ∈ ℕ (vol‘(𝐹‘𝑘)) ∈ ℝ) ∧ 𝑗 ∈ ℕ) → ((vol ∘ 𝐹)‘𝑗) = (vol‘(𝐹‘𝑗)))
174	171, 173	eqtr4d 2780	. . . . . . . 8 ⊢ ((((𝐹:ℕ⟶dom vol ∧ ∀𝑛 ∈ ℕ (𝐹‘𝑛) ⊆ (𝐹‘(𝑛 + 1))) ∧ ∀𝑘 ∈ ℕ (vol‘(𝐹‘𝑘)) ∈ ℝ) ∧ 𝑗 ∈ ℕ) → (seq1( + , (𝑘 ∈ ℕ ↦ (vol‘((𝐹‘𝑘) ∖ ∪ 𝑚 ∈ (1..^𝑘)(𝐹‘𝑚)))))‘𝑗) = ((vol ∘ 𝐹)‘𝑗))
175	49, 54, 174	eqfnfvd 7054	. . . . . . 7 ⊢ (((𝐹:ℕ⟶dom vol ∧ ∀𝑛 ∈ ℕ (𝐹‘𝑛) ⊆ (𝐹‘(𝑛 + 1))) ∧ ∀𝑘 ∈ ℕ (vol‘(𝐹‘𝑘)) ∈ ℝ) → seq1( + , (𝑘 ∈ ℕ ↦ (vol‘((𝐹‘𝑘) ∖ ∪ 𝑚 ∈ (1..^𝑘)(𝐹‘𝑚))))) = (vol ∘ 𝐹))
176	175	rneqd 5949	. . . . . 6 ⊢ (((𝐹:ℕ⟶dom vol ∧ ∀𝑛 ∈ ℕ (𝐹‘𝑛) ⊆ (𝐹‘(𝑛 + 1))) ∧ ∀𝑘 ∈ ℕ (vol‘(𝐹‘𝑘)) ∈ ℝ) → ran seq1( + , (𝑘 ∈ ℕ ↦ (vol‘((𝐹‘𝑘) ∖ ∪ 𝑚 ∈ (1..^𝑘)(𝐹‘𝑚))))) = ran (vol ∘ 𝐹))
177		rnco2 6273	. . . . . 6 ⊢ ran (vol ∘ 𝐹) = (vol “ ran 𝐹)
178	176, 177	eqtrdi 2793	. . . . 5 ⊢ (((𝐹:ℕ⟶dom vol ∧ ∀𝑛 ∈ ℕ (𝐹‘𝑛) ⊆ (𝐹‘(𝑛 + 1))) ∧ ∀𝑘 ∈ ℕ (vol‘(𝐹‘𝑘)) ∈ ℝ) → ran seq1( + , (𝑘 ∈ ℕ ↦ (vol‘((𝐹‘𝑘) ∖ ∪ 𝑚 ∈ (1..^𝑘)(𝐹‘𝑚))))) = (vol “ ran 𝐹))
179	178	supeq1d 9486	. . . 4 ⊢ (((𝐹:ℕ⟶dom vol ∧ ∀𝑛 ∈ ℕ (𝐹‘𝑛) ⊆ (𝐹‘(𝑛 + 1))) ∧ ∀𝑘 ∈ ℕ (vol‘(𝐹‘𝑘)) ∈ ℝ) → sup(ran seq1( + , (𝑘 ∈ ℕ ↦ (vol‘((𝐹‘𝑘) ∖ ∪ 𝑚 ∈ (1..^𝑘)(𝐹‘𝑚))))), ℝ^, < ) = sup((vol “ ran 𝐹), ℝ^, < ))
180	36, 43, 179	3eqtr3d 2785	. . 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 3100	. . 3 ⊢ (∃𝑘 ∈ ℕ ¬ (vol‘(𝐹‘𝑘)) ∈ ℝ ↔ ¬ ∀𝑘 ∈ ℕ (vol‘(𝐹‘𝑘)) ∈ ℝ)
183		fniunfv 7267	. . . . . . . . . . . 12 ⊢ (𝐹 Fn ℕ → ∪ 𝑛 ∈ ℕ (𝐹‘𝑛) = ∪ ran 𝐹)
184	38, 183	syl 17	. . . . . . . . . . 11 ⊢ (𝐹:ℕ⟶dom vol → ∪ 𝑛 ∈ ℕ (𝐹‘𝑛) = ∪ ran 𝐹)
185		ffvelcdm 7101	. . . . . . . . . . . . 13 ⊢ ((𝐹:ℕ⟶dom vol ∧ 𝑛 ∈ ℕ) → (𝐹‘𝑛) ∈ dom vol)
186	185	ralrimiva 3146	. . . . . . . . . . . 12 ⊢ (𝐹:ℕ⟶dom vol → ∀𝑛 ∈ ℕ (𝐹‘𝑛) ∈ dom vol)
187		iunmbl 25588	. . . . . . . . . . . 12 ⊢ (∀𝑛 ∈ ℕ (𝐹‘𝑛) ∈ dom vol → ∪ 𝑛 ∈ ℕ (𝐹‘𝑛) ∈ dom vol)
188	186, 187	syl 17	. . . . . . . . . . 11 ⊢ (𝐹:ℕ⟶dom vol → ∪ 𝑛 ∈ ℕ (𝐹‘𝑛) ∈ dom vol)
189	184, 188	eqeltrrd 2842	. . . . . . . . . 10 ⊢ (𝐹:ℕ⟶dom vol → ∪ ran 𝐹 ∈ dom vol)
190	189	ad2antrr 726	. . . . . . . . 9 ⊢ (((𝐹:ℕ⟶dom vol ∧ ∀𝑛 ∈ ℕ (𝐹‘𝑛) ⊆ (𝐹‘(𝑛 + 1))) ∧ (𝑘 ∈ ℕ ∧ ¬ (vol‘(𝐹‘𝑘)) ∈ ℝ)) → ∪ ran 𝐹 ∈ dom vol)
191		mblss 25566	. . . . . . . . 9 ⊢ (∪ ran 𝐹 ∈ dom vol → ∪ ran 𝐹 ⊆ ℝ)
192	190, 191	syl 17	. . . . . . . 8 ⊢ (((𝐹:ℕ⟶dom vol ∧ ∀𝑛 ∈ ℕ (𝐹‘𝑛) ⊆ (𝐹‘(𝑛 + 1))) ∧ (𝑘 ∈ ℕ ∧ ¬ (vol‘(𝐹‘𝑘)) ∈ ℝ)) → ∪ ran 𝐹 ⊆ ℝ)
193		ovolcl 25513	. . . . . . . 8 ⊢ (∪ ran 𝐹 ⊆ ℝ → (vol‘∪ ran 𝐹) ∈ ℝ^)
194	192, 193	syl 17	. . . . . . 7 ⊢ (((𝐹:ℕ⟶dom vol ∧ ∀𝑛 ∈ ℕ (𝐹‘𝑛) ⊆ (𝐹‘(𝑛 + 1))) ∧ (𝑘 ∈ ℕ ∧ ¬ (vol‘(𝐹‘𝑘)) ∈ ℝ)) → (vol‘∪ ran 𝐹) ∈ ℝ^)
195		pnfge 13172	. . . . . . 7 ⊢ ((vol‘∪ ran 𝐹) ∈ ℝ^ → (vol*‘∪ ran 𝐹) ≤ +∞)
196	194, 195	syl 17	. . . . . 6 ⊢ (((𝐹:ℕ⟶dom vol ∧ ∀𝑛 ∈ ℕ (𝐹‘𝑛) ⊆ (𝐹‘(𝑛 + 1))) ∧ (𝑘 ∈ ℕ ∧ ¬ (vol‘(𝐹‘𝑘)) ∈ ℝ)) → (vol*‘∪ ran 𝐹) ≤ +∞)
197		simprr 773	. . . . . . . . 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 25513	. . . . . . . . . . . 12 ⊢ ((𝐹‘𝑘) ⊆ ℝ → (vol‘(𝐹‘𝑘)) ∈ ℝ^)
201	199, 200	syl 17	. . . . . . . . . . 11 ⊢ (((𝐹:ℕ⟶dom vol ∧ ∀𝑛 ∈ ℕ (𝐹‘𝑛) ⊆ (𝐹‘(𝑛 + 1))) ∧ (𝑘 ∈ ℕ ∧ ¬ (vol‘(𝐹‘𝑘)) ∈ ℝ)) → (vol‘(𝐹‘𝑘)) ∈ ℝ^)
202		xrrebnd 13210	. . . . . . . . . . 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 2826	. . . . . . . . . 10 ⊢ (((𝐹:ℕ⟶dom vol ∧ ∀𝑛 ∈ ℕ (𝐹‘𝑛) ⊆ (𝐹‘(𝑛 + 1))) ∧ (𝑘 ∈ ℕ ∧ ¬ (vol‘(𝐹‘𝑘)) ∈ ℝ)) → ((vol‘(𝐹‘𝑘)) ∈ ℝ ↔ (vol*‘(𝐹‘𝑘)) ∈ ℝ))
206		ovolge0 25516	. . . . . . . . . . . . 13 ⊢ ((𝐹‘𝑘) ⊆ ℝ → 0 ≤ (vol*‘(𝐹‘𝑘)))
207		mnflt0 13167	. . . . . . . . . . . . . 14 ⊢ -∞ < 0
208		mnfxr 11318	. . . . . . . . . . . . . . 15 ⊢ -∞ ∈ ℝ^*
209		0xr 11308	. . . . . . . . . . . . . . 15 ⊢ 0 ∈ ℝ^*
210		xrltletr 13199	. . . . . . . . . . . . . . 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 13206	. . . . . . . . 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 771	. . . . . . . . . 10 ⊢ (((𝐹:ℕ⟶dom vol ∧ ∀𝑛 ∈ ℕ (𝐹‘𝑛) ⊆ (𝐹‘(𝑛 + 1))) ∧ (𝑘 ∈ ℕ ∧ ¬ (vol‘(𝐹‘𝑘)) ∈ ℝ)) → 𝑘 ∈ ℕ)
223		fnfvelrn 7100	. . . . . . . . . 10 ⊢ ((𝐹 Fn ℕ ∧ 𝑘 ∈ ℕ) → (𝐹‘𝑘) ∈ ran 𝐹)
224	221, 222, 223	syl2anc 584	. . . . . . . . 9 ⊢ (((𝐹:ℕ⟶dom vol ∧ ∀𝑛 ∈ ℕ (𝐹‘𝑛) ⊆ (𝐹‘(𝑛 + 1))) ∧ (𝑘 ∈ ℕ ∧ ¬ (vol‘(𝐹‘𝑘)) ∈ ℝ)) → (𝐹‘𝑘) ∈ ran 𝐹)
225		elssuni 4937	. . . . . . . . 9 ⊢ ((𝐹‘𝑘) ∈ ran 𝐹 → (𝐹‘𝑘) ⊆ ∪ ran 𝐹)
226	224, 225	syl 17	. . . . . . . 8 ⊢ (((𝐹:ℕ⟶dom vol ∧ ∀𝑛 ∈ ℕ (𝐹‘𝑛) ⊆ (𝐹‘(𝑛 + 1))) ∧ (𝑘 ∈ ℕ ∧ ¬ (vol‘(𝐹‘𝑘)) ∈ ℝ)) → (𝐹‘𝑘) ⊆ ∪ ran 𝐹)
227		ovolss 25520	. . . . . . . 8 ⊢ (((𝐹‘𝑘) ⊆ ∪ ran 𝐹 ∧ ∪ ran 𝐹 ⊆ ℝ) → (vol‘(𝐹‘𝑘)) ≤ (vol‘∪ ran 𝐹))
228	226, 192, 227	syl2anc 584	. . . . . . 7 ⊢ (((𝐹:ℕ⟶dom vol ∧ ∀𝑛 ∈ ℕ (𝐹‘𝑛) ⊆ (𝐹‘(𝑛 + 1))) ∧ (𝑘 ∈ ℕ ∧ ¬ (vol‘(𝐹‘𝑘)) ∈ ℝ)) → (vol‘(𝐹‘𝑘)) ≤ (vol‘∪ ran 𝐹))
229	220, 228	eqbrtrrd 5167	. . . . . 6 ⊢ (((𝐹:ℕ⟶dom vol ∧ ∀𝑛 ∈ ℕ (𝐹‘𝑛) ⊆ (𝐹‘(𝑛 + 1))) ∧ (𝑘 ∈ ℕ ∧ ¬ (vol‘(𝐹‘𝑘)) ∈ ℝ)) → +∞ ≤ (vol*‘∪ ran 𝐹))
230		pnfxr 11315	. . . . . . 7 ⊢ +∞ ∈ ℝ^*
231		xrletri3 13196	. . . . . . 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 25565	. . . . . 6 ⊢ (∪ ran 𝐹 ∈ dom vol → (vol‘∪ ran 𝐹) = (vol*‘∪ ran 𝐹))
235	190, 234	syl 17	. . . . 5 ⊢ (((𝐹:ℕ⟶dom vol ∧ ∀𝑛 ∈ ℕ (𝐹‘𝑛) ⊆ (𝐹‘(𝑛 + 1))) ∧ (𝑘 ∈ ℕ ∧ ¬ (vol‘(𝐹‘𝑘)) ∈ ℝ)) → (vol‘∪ ran 𝐹) = (vol*‘∪ ran 𝐹))
236		imassrn 6089	. . . . . . 7 ⊢ (vol “ ran 𝐹) ⊆ ran vol
237		frn 6743	. . . . . . . . 9 ⊢ (vol:dom vol⟶(0[,]+∞) → ran vol ⊆ (0[,]+∞))
238	50, 237	ax-mp 5	. . . . . . . 8 ⊢ ran vol ⊆ (0[,]+∞)
239		iccssxr 13470	. . . . . . . 8 ⊢ (0[,]+∞) ⊆ ℝ^*
240	238, 239	sstri 3993	. . . . . . 7 ⊢ ran vol ⊆ ℝ^*
241	236, 240	sstri 3993	. . . . . 6 ⊢ (vol “ ran 𝐹) ⊆ ℝ^*
242	204, 220	eqtrd 2777	. . . . . . 7 ⊢ (((𝐹:ℕ⟶dom vol ∧ ∀𝑛 ∈ ℕ (𝐹‘𝑛) ⊆ (𝐹‘(𝑛 + 1))) ∧ (𝑘 ∈ ℕ ∧ ¬ (vol‘(𝐹‘𝑘)) ∈ ℝ)) → (vol‘(𝐹‘𝑘)) = +∞)
243		simpll 767	. . . . . . . 8 ⊢ (((𝐹:ℕ⟶dom vol ∧ ∀𝑛 ∈ ℕ (𝐹‘𝑛) ⊆ (𝐹‘(𝑛 + 1))) ∧ (𝑘 ∈ ℕ ∧ ¬ (vol‘(𝐹‘𝑘)) ∈ ℝ)) → 𝐹:ℕ⟶dom vol)
244		ffun 6739	. . . . . . . . . 10 ⊢ (vol:dom vol⟶(0[,]+∞) → Fun vol)
245	50, 244	ax-mp 5	. . . . . . . . 9 ⊢ Fun vol
246		frn 6743	. . . . . . . . 9 ⊢ (𝐹:ℕ⟶dom vol → ran 𝐹 ⊆ dom vol)
247		funfvima2 7251	. . . . . . . . 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 2842	. . . . . 6 ⊢ (((𝐹:ℕ⟶dom vol ∧ ∀𝑛 ∈ ℕ (𝐹‘𝑛) ⊆ (𝐹‘(𝑛 + 1))) ∧ (𝑘 ∈ ℕ ∧ ¬ (vol‘(𝐹‘𝑘)) ∈ ℝ)) → +∞ ∈ (vol “ ran 𝐹))
251		supxrpnf 13360	. . . . . 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 2787	. . . 4 ⊢ (((𝐹:ℕ⟶dom vol ∧ ∀𝑛 ∈ ℕ (𝐹‘𝑛) ⊆ (𝐹‘(𝑛 + 1))) ∧ (𝑘 ∈ ℕ ∧ ¬ (vol‘(𝐹‘𝑘)) ∈ ℝ)) → (vol‘∪ ran 𝐹) = sup((vol “ ran 𝐹), ℝ^*, < ))
254	253	rexlimdvaa 3156	. . 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 1540 ∈ wcel 2108 ∀wral 3061 ∃wrex 3070 ∖ cdif 3948 ∪ cun 3949 ∩ cin 3950 ⊆ wss 3951 ∅c0 4333 ∪ cuni 4907 ∪ ciun 4991 Disj wdisj 5110 class class class wbr 5143 ↦ cmpt 5225 dom cdm 5685 ran crn 5686 “ cima 5688 ∘ ccom 5689 Fun wfun 6555 Fn wfn 6556 ⟶wf 6557 ‘cfv 6561 (class class class)co 7431 Fincfn 8985 supcsup 9480 ℝcr 11154 0cc0 11155 1c1 11156 + caddc 11158 +∞cpnf 11292 -∞cmnf 11293 ℝ^*cxr 11294 < clt 11295 ≤ cle 11296 ℕcn 12266 ℤcz 12613 ℤ_≥cuz 12878 [,]cicc 13390 ...cfz 13547 ..^cfzo 13694 seqcseq 14042 vol*covol 25497 volcvol 25498

This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1795 ax-4 1809 ax-5 1910 ax-6 1967 ax-7 2007 ax-8 2110 ax-9 2118 ax-10 2141 ax-11 2157 ax-12 2177 ax-ext 2708 ax-rep 5279 ax-sep 5296 ax-nul 5306 ax-pow 5365 ax-pr 5432 ax-un 7755 ax-inf2 9681 ax-cc 10475 ax-cnex 11211 ax-resscn 11212 ax-1cn 11213 ax-icn 11214 ax-addcl 11215 ax-addrcl 11216 ax-mulcl 11217 ax-mulrcl 11218 ax-mulcom 11219 ax-addass 11220 ax-mulass 11221 ax-distr 11222 ax-i2m1 11223 ax-1ne0 11224 ax-1rid 11225 ax-rnegex 11226 ax-rrecex 11227 ax-cnre 11228 ax-pre-lttri 11229 ax-pre-lttrn 11230 ax-pre-ltadd 11231 ax-pre-mulgt0 11232 ax-pre-sup 11233

This theorem depends on definitions: df-bi 207 df-an 396 df-or 849 df-3or 1088 df-3an 1089 df-tru 1543 df-fal 1553 df-ex 1780 df-nf 1784 df-sb 2065 df-mo 2540 df-eu 2569 df-clab 2715 df-cleq 2729 df-clel 2816 df-nfc 2892 df-ne 2941 df-nel 3047 df-ral 3062 df-rex 3071 df-rmo 3380 df-reu 3381 df-rab 3437 df-v 3482 df-sbc 3789 df-csb 3900 df-dif 3954 df-un 3956 df-in 3958 df-ss 3968 df-pss 3971 df-nul 4334 df-if 4526 df-pw 4602 df-sn 4627 df-pr 4629 df-op 4633 df-uni 4908 df-int 4947 df-iun 4993 df-disj 5111 df-br 5144 df-opab 5206 df-mpt 5226 df-tr 5260 df-id 5578 df-eprel 5584 df-po 5592 df-so 5593 df-fr 5637 df-se 5638 df-we 5639 df-xp 5691 df-rel 5692 df-cnv 5693 df-co 5694 df-dm 5695 df-rn 5696 df-res 5697 df-ima 5698 df-pred 6321 df-ord 6387 df-on 6388 df-lim 6389 df-suc 6390 df-iota 6514 df-fun 6563 df-fn 6564 df-f 6565 df-f1 6566 df-fo 6567 df-f1o 6568 df-fv 6569 df-isom 6570 df-riota 7388 df-ov 7434 df-oprab 7435 df-mpo 7436 df-of 7697 df-om 7888 df-1st 8014 df-2nd 8015 df-frecs 8306 df-wrecs 8337 df-recs 8411 df-rdg 8450 df-1o 8506 df-2o 8507 df-er 8745 df-map 8868 df-pm 8869 df-en 8986 df-dom 8987 df-sdom 8988 df-fin 8989 df-sup 9482 df-inf 9483 df-oi 9550 df-dju 9941 df-card 9979 df-pnf 11297 df-mnf 11298 df-xr 11299 df-ltxr 11300 df-le 11301 df-sub 11494 df-neg 11495 df-div 11921 df-nn 12267 df-2 12329 df-3 12330 df-n0 12527 df-z 12614 df-uz 12879 df-q 12991 df-rp 13035 df-xadd 13155 df-ioo 13391 df-ico 13393 df-icc 13394 df-fz 13548 df-fzo 13695 df-fl 13832 df-seq 14043 df-exp 14103 df-hash 14370 df-cj 15138 df-re 15139 df-im 15140 df-sqrt 15274 df-abs 15275 df-clim 15524 df-rlim 15525 df-sum 15723 df-xmet 21357 df-met 21358 df-ovol 25499 df-vol 25500

This theorem is referenced by: volsup2 25640 itg1climres 25749 itg2gt0 25795

W3C validator