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 25610

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 7115	. . . . . . . . . . 11 ⊢ ((𝐹:ℕ⟶dom vol ∧ 𝑘 ∈ ℕ) → (𝐹‘𝑘) ∈ dom vol)
2	1	ad2ant2r 746	. . . . . . . . . 10 ⊢ (((𝐹:ℕ⟶dom vol ∧ ∀𝑛 ∈ ℕ (𝐹‘𝑛) ⊆ (𝐹‘(𝑛 + 1))) ∧ (𝑘 ∈ ℕ ∧ (vol‘(𝐹‘𝑘)) ∈ ℝ)) → (𝐹‘𝑘) ∈ dom vol)
3		fzofi 14025	. . . . . . . . . . 11 ⊢ (1..^𝑘) ∈ Fin
4		simpll 766	. . . . . . . . . . . . 13 ⊢ (((𝐹:ℕ⟶dom vol ∧ ∀𝑛 ∈ ℕ (𝐹‘𝑛) ⊆ (𝐹‘(𝑛 + 1))) ∧ (𝑘 ∈ ℕ ∧ (vol‘(𝐹‘𝑘)) ∈ ℝ)) → 𝐹:ℕ⟶dom vol)
5		elfzouz 13720	. . . . . . . . . . . . . 14 ⊢ (𝑚 ∈ (1..^𝑘) → 𝑚 ∈ (ℤ_≥‘1))
6		nnuz 12946	. . . . . . . . . . . . . 14 ⊢ ℕ = (ℤ_≥‘1)
7	5, 6	eleqtrrdi 2855	. . . . . . . . . . . . 13 ⊢ (𝑚 ∈ (1..^𝑘) → 𝑚 ∈ ℕ)
8		ffvelcdm 7115	. . . . . . . . . . . . 13 ⊢ ((𝐹:ℕ⟶dom vol ∧ 𝑚 ∈ ℕ) → (𝐹‘𝑚) ∈ dom vol)
9	4, 7, 8	syl2an 595	. . . . . . . . . . . 12 ⊢ ((((𝐹:ℕ⟶dom vol ∧ ∀𝑛 ∈ ℕ (𝐹‘𝑛) ⊆ (𝐹‘(𝑛 + 1))) ∧ (𝑘 ∈ ℕ ∧ (vol‘(𝐹‘𝑘)) ∈ ℝ)) ∧ 𝑚 ∈ (1..^𝑘)) → (𝐹‘𝑚) ∈ dom vol)
10	9	ralrimiva 3152	. . . . . . . . . . 11 ⊢ (((𝐹:ℕ⟶dom vol ∧ ∀𝑛 ∈ ℕ (𝐹‘𝑛) ⊆ (𝐹‘(𝑛 + 1))) ∧ (𝑘 ∈ ℕ ∧ (vol‘(𝐹‘𝑘)) ∈ ℝ)) → ∀𝑚 ∈ (1..^𝑘)(𝐹‘𝑚) ∈ dom vol)
11		finiunmbl 25598	. . . . . . . . . . 11 ⊢ (((1..^𝑘) ∈ Fin ∧ ∀𝑚 ∈ (1..^𝑘)(𝐹‘𝑚) ∈ dom vol) → ∪ 𝑚 ∈ (1..^𝑘)(𝐹‘𝑚) ∈ dom vol)
12	3, 10, 11	sylancr 586	. . . . . . . . . 10 ⊢ (((𝐹:ℕ⟶dom vol ∧ ∀𝑛 ∈ ℕ (𝐹‘𝑛) ⊆ (𝐹‘(𝑛 + 1))) ∧ (𝑘 ∈ ℕ ∧ (vol‘(𝐹‘𝑘)) ∈ ℝ)) → ∪ 𝑚 ∈ (1..^𝑘)(𝐹‘𝑚) ∈ dom vol)
13		difmbl 25597	. . . . . . . . . 10 ⊢ (((𝐹‘𝑘) ∈ dom vol ∧ ∪ 𝑚 ∈ (1..^𝑘)(𝐹‘𝑚) ∈ dom vol) → ((𝐹‘𝑘) ∖ ∪ 𝑚 ∈ (1..^𝑘)(𝐹‘𝑚)) ∈ dom vol)
14	2, 12, 13	syl2anc 583	. . . . . . . . 9 ⊢ (((𝐹:ℕ⟶dom vol ∧ ∀𝑛 ∈ ℕ (𝐹‘𝑛) ⊆ (𝐹‘(𝑛 + 1))) ∧ (𝑘 ∈ ℕ ∧ (vol‘(𝐹‘𝑘)) ∈ ℝ)) → ((𝐹‘𝑘) ∖ ∪ 𝑚 ∈ (1..^𝑘)(𝐹‘𝑚)) ∈ dom vol)
15		mblvol 25584	. . . . . . . . . . 11 ⊢ (((𝐹‘𝑘) ∖ ∪ 𝑚 ∈ (1..^𝑘)(𝐹‘𝑚)) ∈ dom vol → (vol‘((𝐹‘𝑘) ∖ ∪ 𝑚 ∈ (1..^𝑘)(𝐹‘𝑚))) = (vol*‘((𝐹‘𝑘) ∖ ∪ 𝑚 ∈ (1..^𝑘)(𝐹‘𝑚))))
16	14, 15	syl 17	. . . . . . . . . 10 ⊢ (((𝐹:ℕ⟶dom vol ∧ ∀𝑛 ∈ ℕ (𝐹‘𝑛) ⊆ (𝐹‘(𝑛 + 1))) ∧ (𝑘 ∈ ℕ ∧ (vol‘(𝐹‘𝑘)) ∈ ℝ)) → (vol‘((𝐹‘𝑘) ∖ ∪ 𝑚 ∈ (1..^𝑘)(𝐹‘𝑚))) = (vol*‘((𝐹‘𝑘) ∖ ∪ 𝑚 ∈ (1..^𝑘)(𝐹‘𝑚))))
17		difssd 4160	. . . . . . . . . . 11 ⊢ (((𝐹:ℕ⟶dom vol ∧ ∀𝑛 ∈ ℕ (𝐹‘𝑛) ⊆ (𝐹‘(𝑛 + 1))) ∧ (𝑘 ∈ ℕ ∧ (vol‘(𝐹‘𝑘)) ∈ ℝ)) → ((𝐹‘𝑘) ∖ ∪ 𝑚 ∈ (1..^𝑘)(𝐹‘𝑚)) ⊆ (𝐹‘𝑘))
18		mblss 25585	. . . . . . . . . . . 12 ⊢ ((𝐹‘𝑘) ∈ dom vol → (𝐹‘𝑘) ⊆ ℝ)
19	2, 18	syl 17	. . . . . . . . . . 11 ⊢ (((𝐹:ℕ⟶dom vol ∧ ∀𝑛 ∈ ℕ (𝐹‘𝑛) ⊆ (𝐹‘(𝑛 + 1))) ∧ (𝑘 ∈ ℕ ∧ (vol‘(𝐹‘𝑘)) ∈ ℝ)) → (𝐹‘𝑘) ⊆ ℝ)
20		mblvol 25584	. . . . . . . . . . . . 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 2845	. . . . . . . . . . 11 ⊢ (((𝐹:ℕ⟶dom vol ∧ ∀𝑛 ∈ ℕ (𝐹‘𝑛) ⊆ (𝐹‘(𝑛 + 1))) ∧ (𝑘 ∈ ℕ ∧ (vol‘(𝐹‘𝑘)) ∈ ℝ)) → (vol*‘(𝐹‘𝑘)) ∈ ℝ)
24		ovolsscl 25540	. . . . . . . . . . 11 ⊢ ((((𝐹‘𝑘) ∖ ∪ 𝑚 ∈ (1..^𝑘)(𝐹‘𝑚)) ⊆ (𝐹‘𝑘) ∧ (𝐹‘𝑘) ⊆ ℝ ∧ (vol‘(𝐹‘𝑘)) ∈ ℝ) → (vol‘((𝐹‘𝑘) ∖ ∪ 𝑚 ∈ (1..^𝑘)(𝐹‘𝑚))) ∈ ℝ)
25	17, 19, 23, 24	syl3anc 1371	. . . . . . . . . 10 ⊢ (((𝐹:ℕ⟶dom vol ∧ ∀𝑛 ∈ ℕ (𝐹‘𝑛) ⊆ (𝐹‘(𝑛 + 1))) ∧ (𝑘 ∈ ℕ ∧ (vol‘(𝐹‘𝑘)) ∈ ℝ)) → (vol*‘((𝐹‘𝑘) ∖ ∪ 𝑚 ∈ (1..^𝑘)(𝐹‘𝑚))) ∈ ℝ)
26	16, 25	eqeltrd 2844	. . . . . . . . 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 3173	. . . . . 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 6920	. . . . . 6 ⊢ (𝑘 = 𝑚 → (𝐹‘𝑘) = (𝐹‘𝑚))
32	31	iundisj2 25603	. . . . 5 ⊢ Disj 𝑘 ∈ ℕ ((𝐹‘𝑘) ∖ ∪ 𝑚 ∈ (1..^𝑘)(𝐹‘𝑚))
33		eqid 2740	. . . . . 6 ⊢ seq1( + , (𝑘 ∈ ℕ ↦ (vol‘((𝐹‘𝑘) ∖ ∪ 𝑚 ∈ (1..^𝑘)(𝐹‘𝑚))))) = seq1( + , (𝑘 ∈ ℕ ↦ (vol‘((𝐹‘𝑘) ∖ ∪ 𝑚 ∈ (1..^𝑘)(𝐹‘𝑚)))))
34		eqid 2740	. . . . . 6 ⊢ (𝑘 ∈ ℕ ↦ (vol‘((𝐹‘𝑘) ∖ ∪ 𝑚 ∈ (1..^𝑘)(𝐹‘𝑚)))) = (𝑘 ∈ ℕ ↦ (vol‘((𝐹‘𝑘) ∖ ∪ 𝑚 ∈ (1..^𝑘)(𝐹‘𝑚))))
35	33, 34	voliun 25608	. . . . 5 ⊢ ((∀𝑘 ∈ ℕ (((𝐹‘𝑘) ∖ ∪ 𝑚 ∈ (1..^𝑘)(𝐹‘𝑚)) ∈ dom vol ∧ (vol‘((𝐹‘𝑘) ∖ ∪ 𝑚 ∈ (1..^𝑘)(𝐹‘𝑚))) ∈ ℝ) ∧ Disj 𝑘 ∈ ℕ ((𝐹‘𝑘) ∖ ∪ 𝑚 ∈ (1..^𝑘)(𝐹‘𝑚))) → (vol‘∪ 𝑘 ∈ ℕ ((𝐹‘𝑘) ∖ ∪ 𝑚 ∈ (1..^𝑘)(𝐹‘𝑚))) = sup(ran seq1( + , (𝑘 ∈ ℕ ↦ (vol‘((𝐹‘𝑘) ∖ ∪ 𝑚 ∈ (1..^𝑘)(𝐹‘𝑚))))), ℝ^*, < ))
36	30, 32, 35	sylancl 585	. . . 4 ⊢ (((𝐹:ℕ⟶dom vol ∧ ∀𝑛 ∈ ℕ (𝐹‘𝑛) ⊆ (𝐹‘(𝑛 + 1))) ∧ ∀𝑘 ∈ ℕ (vol‘(𝐹‘𝑘)) ∈ ℝ) → (vol‘∪ 𝑘 ∈ ℕ ((𝐹‘𝑘) ∖ ∪ 𝑚 ∈ (1..^𝑘)(𝐹‘𝑚))) = sup(ran seq1( + , (𝑘 ∈ ℕ ↦ (vol‘((𝐹‘𝑘) ∖ ∪ 𝑚 ∈ (1..^𝑘)(𝐹‘𝑚))))), ℝ^*, < ))
37	31	iundisj 25602	. . . . . 6 ⊢ ∪ 𝑘 ∈ ℕ (𝐹‘𝑘) = ∪ 𝑘 ∈ ℕ ((𝐹‘𝑘) ∖ ∪ 𝑚 ∈ (1..^𝑘)(𝐹‘𝑚))
38		ffn 6747	. . . . . . . 8 ⊢ (𝐹:ℕ⟶dom vol → 𝐹 Fn ℕ)
39	38	ad2antrr 725	. . . . . . 7 ⊢ (((𝐹:ℕ⟶dom vol ∧ ∀𝑛 ∈ ℕ (𝐹‘𝑛) ⊆ (𝐹‘(𝑛 + 1))) ∧ ∀𝑘 ∈ ℕ (vol‘(𝐹‘𝑘)) ∈ ℝ) → 𝐹 Fn ℕ)
40		fniunfv 7284	. . . . . . 7 ⊢ (𝐹 Fn ℕ → ∪ 𝑘 ∈ ℕ (𝐹‘𝑘) = ∪ ran 𝐹)
41	39, 40	syl 17	. . . . . 6 ⊢ (((𝐹:ℕ⟶dom vol ∧ ∀𝑛 ∈ ℕ (𝐹‘𝑛) ⊆ (𝐹‘(𝑛 + 1))) ∧ ∀𝑘 ∈ ℕ (vol‘(𝐹‘𝑘)) ∈ ℝ) → ∪ 𝑘 ∈ ℕ (𝐹‘𝑘) = ∪ ran 𝐹)
42	37, 41	eqtr3id 2794	. . . . 5 ⊢ (((𝐹:ℕ⟶dom vol ∧ ∀𝑛 ∈ ℕ (𝐹‘𝑛) ⊆ (𝐹‘(𝑛 + 1))) ∧ ∀𝑘 ∈ ℕ (vol‘(𝐹‘𝑘)) ∈ ℝ) → ∪ 𝑘 ∈ ℕ ((𝐹‘𝑘) ∖ ∪ 𝑚 ∈ (1..^𝑘)(𝐹‘𝑚)) = ∪ ran 𝐹)
43	42	fveq2d 6924	. . . 4 ⊢ (((𝐹:ℕ⟶dom vol ∧ ∀𝑛 ∈ ℕ (𝐹‘𝑛) ⊆ (𝐹‘(𝑛 + 1))) ∧ ∀𝑘 ∈ ℕ (vol‘(𝐹‘𝑘)) ∈ ℝ) → (vol‘∪ 𝑘 ∈ ℕ ((𝐹‘𝑘) ∖ ∪ 𝑚 ∈ (1..^𝑘)(𝐹‘𝑚))) = (vol‘∪ ran 𝐹))
44		1z 12673	. . . . . . . . . . 11 ⊢ 1 ∈ ℤ
45		seqfn 14064	. . . . . . . . . . 11 ⊢ (1 ∈ ℤ → seq1( + , (𝑘 ∈ ℕ ↦ (vol‘((𝐹‘𝑘) ∖ ∪ 𝑚 ∈ (1..^𝑘)(𝐹‘𝑚))))) Fn (ℤ_≥‘1))
46	44, 45	ax-mp 5	. . . . . . . . . 10 ⊢ seq1( + , (𝑘 ∈ ℕ ↦ (vol‘((𝐹‘𝑘) ∖ ∪ 𝑚 ∈ (1..^𝑘)(𝐹‘𝑚))))) Fn (ℤ_≥‘1)
47	6	fneq2i 6677	. . . . . . . . . 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 25583	. . . . . . . . . 10 ⊢ vol:dom vol⟶(0[,]+∞)
51		simpll 766	. . . . . . . . . 10 ⊢ (((𝐹:ℕ⟶dom vol ∧ ∀𝑛 ∈ ℕ (𝐹‘𝑛) ⊆ (𝐹‘(𝑛 + 1))) ∧ ∀𝑘 ∈ ℕ (vol‘(𝐹‘𝑘)) ∈ ℝ) → 𝐹:ℕ⟶dom vol)
52		fco 6771	. . . . . . . . . 10 ⊢ ((vol:dom vol⟶(0[,]+∞) ∧ 𝐹:ℕ⟶dom vol) → (vol ∘ 𝐹):ℕ⟶(0[,]+∞))
53	50, 51, 52	sylancr 586	. . . . . . . . 9 ⊢ (((𝐹:ℕ⟶dom vol ∧ ∀𝑛 ∈ ℕ (𝐹‘𝑛) ⊆ (𝐹‘(𝑛 + 1))) ∧ ∀𝑘 ∈ ℕ (vol‘(𝐹‘𝑘)) ∈ ℝ) → (vol ∘ 𝐹):ℕ⟶(0[,]+∞))
54	53	ffnd 6748	. . . . . . . 8 ⊢ (((𝐹:ℕ⟶dom vol ∧ ∀𝑛 ∈ ℕ (𝐹‘𝑛) ⊆ (𝐹‘(𝑛 + 1))) ∧ ∀𝑘 ∈ ℕ (vol‘(𝐹‘𝑘)) ∈ ℝ) → (vol ∘ 𝐹) Fn ℕ)
55		fveq2 6920	. . . . . . . . . . . . 13 ⊢ (𝑥 = 1 → (seq1( + , (𝑘 ∈ ℕ ↦ (vol‘((𝐹‘𝑘) ∖ ∪ 𝑚 ∈ (1..^𝑘)(𝐹‘𝑚)))))‘𝑥) = (seq1( + , (𝑘 ∈ ℕ ↦ (vol‘((𝐹‘𝑘) ∖ ∪ 𝑚 ∈ (1..^𝑘)(𝐹‘𝑚)))))‘1))
56		2fveq3 6925	. . . . . . . . . . . . 13 ⊢ (𝑥 = 1 → (vol‘(𝐹‘𝑥)) = (vol‘(𝐹‘1)))
57	55, 56	eqeq12d 2756	. . . . . . . . . . . 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 6920	. . . . . . . . . . . . 13 ⊢ (𝑥 = 𝑗 → (seq1( + , (𝑘 ∈ ℕ ↦ (vol‘((𝐹‘𝑘) ∖ ∪ 𝑚 ∈ (1..^𝑘)(𝐹‘𝑚)))))‘𝑥) = (seq1( + , (𝑘 ∈ ℕ ↦ (vol‘((𝐹‘𝑘) ∖ ∪ 𝑚 ∈ (1..^𝑘)(𝐹‘𝑚)))))‘𝑗))
60		2fveq3 6925	. . . . . . . . . . . . 13 ⊢ (𝑥 = 𝑗 → (vol‘(𝐹‘𝑥)) = (vol‘(𝐹‘𝑗)))
61	59, 60	eqeq12d 2756	. . . . . . . . . . . 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 6920	. . . . . . . . . . . . 13 ⊢ (𝑥 = (𝑗 + 1) → (seq1( + , (𝑘 ∈ ℕ ↦ (vol‘((𝐹‘𝑘) ∖ ∪ 𝑚 ∈ (1..^𝑘)(𝐹‘𝑚)))))‘𝑥) = (seq1( + , (𝑘 ∈ ℕ ↦ (vol‘((𝐹‘𝑘) ∖ ∪ 𝑚 ∈ (1..^𝑘)(𝐹‘𝑚)))))‘(𝑗 + 1)))
64		2fveq3 6925	. . . . . . . . . . . . 13 ⊢ (𝑥 = (𝑗 + 1) → (vol‘(𝐹‘𝑥)) = (vol‘(𝐹‘(𝑗 + 1))))
65	63, 64	eqeq12d 2756	. . . . . . . . . . . 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 14065	. . . . . . . . . . . . . 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 12304	. . . . . . . . . . . . . 14 ⊢ 1 ∈ ℕ
70		oveq2 7456	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (𝑘 = 1 → (1..^𝑘) = (1..^1))
71		fzo0 13740	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (1..^1) = ∅
72	70, 71	eqtrdi 2796	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (𝑘 = 1 → (1..^𝑘) = ∅)
73	72	iuneq1d 5042	. . . . . . . . . . . . . . . . . . . 20 ⊢ (𝑘 = 1 → ∪ 𝑚 ∈ (1..^𝑘)(𝐹‘𝑚) = ∪ 𝑚 ∈ ∅ (𝐹‘𝑚))
74		0iun 5086	. . . . . . . . . . . . . . . . . . . 20 ⊢ ∪ 𝑚 ∈ ∅ (𝐹‘𝑚) = ∅
75	73, 74	eqtrdi 2796	. . . . . . . . . . . . . . . . . . 19 ⊢ (𝑘 = 1 → ∪ 𝑚 ∈ (1..^𝑘)(𝐹‘𝑚) = ∅)
76	75	difeq2d 4149	. . . . . . . . . . . . . . . . . 18 ⊢ (𝑘 = 1 → ((𝐹‘𝑘) ∖ ∪ 𝑚 ∈ (1..^𝑘)(𝐹‘𝑚)) = ((𝐹‘𝑘) ∖ ∅))
77		dif0 4400	. . . . . . . . . . . . . . . . . 18 ⊢ ((𝐹‘𝑘) ∖ ∅) = (𝐹‘𝑘)
78	76, 77	eqtrdi 2796	. . . . . . . . . . . . . . . . 17 ⊢ (𝑘 = 1 → ((𝐹‘𝑘) ∖ ∪ 𝑚 ∈ (1..^𝑘)(𝐹‘𝑚)) = (𝐹‘𝑘))
79		fveq2 6920	. . . . . . . . . . . . . . . . 17 ⊢ (𝑘 = 1 → (𝐹‘𝑘) = (𝐹‘1))
80	78, 79	eqtrd 2780	. . . . . . . . . . . . . . . 16 ⊢ (𝑘 = 1 → ((𝐹‘𝑘) ∖ ∪ 𝑚 ∈ (1..^𝑘)(𝐹‘𝑚)) = (𝐹‘1))
81	80	fveq2d 6924	. . . . . . . . . . . . . . 15 ⊢ (𝑘 = 1 → (vol‘((𝐹‘𝑘) ∖ ∪ 𝑚 ∈ (1..^𝑘)(𝐹‘𝑚))) = (vol‘(𝐹‘1)))
82		fvex 6933	. . . . . . . . . . . . . . 15 ⊢ (vol‘(𝐹‘1)) ∈ V
83	81, 34, 82	fvmpt 7029	. . . . . . . . . . . . . 14 ⊢ (1 ∈ ℕ → ((𝑘 ∈ ℕ ↦ (vol‘((𝐹‘𝑘) ∖ ∪ 𝑚 ∈ (1..^𝑘)(𝐹‘𝑚))))‘1) = (vol‘(𝐹‘1)))
84	69, 83	ax-mp 5	. . . . . . . . . . . . 13 ⊢ ((𝑘 ∈ ℕ ↦ (vol‘((𝐹‘𝑘) ∖ ∪ 𝑚 ∈ (1..^𝑘)(𝐹‘𝑚))))‘1) = (vol‘(𝐹‘1))
85	68, 84	eqtri 2768	. . . . . . . . . . . 12 ⊢ (seq1( + , (𝑘 ∈ ℕ ↦ (vol‘((𝐹‘𝑘) ∖ ∪ 𝑚 ∈ (1..^𝑘)(𝐹‘𝑚)))))‘1) = (vol‘(𝐹‘1))
86	85	a1i 11	. . . . . . . . . . 11 ⊢ (((𝐹:ℕ⟶dom vol ∧ ∀𝑛 ∈ ℕ (𝐹‘𝑛) ⊆ (𝐹‘(𝑛 + 1))) ∧ ∀𝑘 ∈ ℕ (vol‘(𝐹‘𝑘)) ∈ ℝ) → (seq1( + , (𝑘 ∈ ℕ ↦ (vol‘((𝐹‘𝑘) ∖ ∪ 𝑚 ∈ (1..^𝑘)(𝐹‘𝑚)))))‘1) = (vol‘(𝐹‘1)))
87		oveq1 7455	. . . . . . . . . . . . . 14 ⊢ ((seq1( + , (𝑘 ∈ ℕ ↦ (vol‘((𝐹‘𝑘) ∖ ∪ 𝑚 ∈ (1..^𝑘)(𝐹‘𝑚)))))‘𝑗) = (vol‘(𝐹‘𝑗)) → ((seq1( + , (𝑘 ∈ ℕ ↦ (vol‘((𝐹‘𝑘) ∖ ∪ 𝑚 ∈ (1..^𝑘)(𝐹‘𝑚)))))‘𝑗) + ((𝑘 ∈ ℕ ↦ (vol‘((𝐹‘𝑘) ∖ ∪ 𝑚 ∈ (1..^𝑘)(𝐹‘𝑚))))‘(𝑗 + 1))) = ((vol‘(𝐹‘𝑗)) + ((𝑘 ∈ ℕ ↦ (vol‘((𝐹‘𝑘) ∖ ∪ 𝑚 ∈ (1..^𝑘)(𝐹‘𝑚))))‘(𝑗 + 1))))
88		seqp1 14067	. . . . . . . . . . . . . . . . 17 ⊢ (𝑗 ∈ (ℤ_≥‘1) → (seq1( + , (𝑘 ∈ ℕ ↦ (vol‘((𝐹‘𝑘) ∖ ∪ 𝑚 ∈ (1..^𝑘)(𝐹‘𝑚)))))‘(𝑗 + 1)) = ((seq1( + , (𝑘 ∈ ℕ ↦ (vol‘((𝐹‘𝑘) ∖ ∪ 𝑚 ∈ (1..^𝑘)(𝐹‘𝑚)))))‘𝑗) + ((𝑘 ∈ ℕ ↦ (vol‘((𝐹‘𝑘) ∖ ∪ 𝑚 ∈ (1..^𝑘)(𝐹‘𝑚))))‘(𝑗 + 1))))
89	88, 6	eleq2s 2862	. . . . . . . . . . . . . . . 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 4500	. . . . . . . . . . . . . . . . . 18 ⊢ ((𝐹‘𝑗) ∪ ((𝐹‘(𝑗 + 1)) ∖ (𝐹‘𝑗))) = ((𝐹‘𝑗) ∪ (𝐹‘(𝑗 + 1)))
92		fveq2 6920	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (𝑛 = 𝑗 → (𝐹‘𝑛) = (𝐹‘𝑗))
93		fvoveq1 7471	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (𝑛 = 𝑗 → (𝐹‘(𝑛 + 1)) = (𝐹‘(𝑗 + 1)))
94	92, 93	sseq12d 4042	. . . . . . . . . . . . . . . . . . . 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 3636	. . . . . . . . . . . . . . . . . . 19 ⊢ ((((𝐹:ℕ⟶dom vol ∧ ∀𝑛 ∈ ℕ (𝐹‘𝑛) ⊆ (𝐹‘(𝑛 + 1))) ∧ ∀𝑘 ∈ ℕ (vol‘(𝐹‘𝑘)) ∈ ℝ) ∧ 𝑗 ∈ ℕ) → (𝐹‘𝑗) ⊆ (𝐹‘(𝑗 + 1)))
98		ssequn1 4209	. . . . . . . . . . . . . . . . . . 19 ⊢ ((𝐹‘𝑗) ⊆ (𝐹‘(𝑗 + 1)) ↔ ((𝐹‘𝑗) ∪ (𝐹‘(𝑗 + 1))) = (𝐹‘(𝑗 + 1)))
99	97, 98	sylib 218	. . . . . . . . . . . . . . . . . 18 ⊢ ((((𝐹:ℕ⟶dom vol ∧ ∀𝑛 ∈ ℕ (𝐹‘𝑛) ⊆ (𝐹‘(𝑛 + 1))) ∧ ∀𝑘 ∈ ℕ (vol‘(𝐹‘𝑘)) ∈ ℝ) ∧ 𝑗 ∈ ℕ) → ((𝐹‘𝑗) ∪ (𝐹‘(𝑗 + 1))) = (𝐹‘(𝑗 + 1)))
100	91, 99	eqtr2id 2793	. . . . . . . . . . . . . . . . 17 ⊢ ((((𝐹:ℕ⟶dom vol ∧ ∀𝑛 ∈ ℕ (𝐹‘𝑛) ⊆ (𝐹‘(𝑛 + 1))) ∧ ∀𝑘 ∈ ℕ (vol‘(𝐹‘𝑘)) ∈ ℝ) ∧ 𝑗 ∈ ℕ) → (𝐹‘(𝑗 + 1)) = ((𝐹‘𝑗) ∪ ((𝐹‘(𝑗 + 1)) ∖ (𝐹‘𝑗))))
101	100	fveq2d 6924	. . . . . . . . . . . . . . . 16 ⊢ ((((𝐹:ℕ⟶dom vol ∧ ∀𝑛 ∈ ℕ (𝐹‘𝑛) ⊆ (𝐹‘(𝑛 + 1))) ∧ ∀𝑘 ∈ ℕ (vol‘(𝐹‘𝑘)) ∈ ℝ) ∧ 𝑗 ∈ ℕ) → (vol‘(𝐹‘(𝑗 + 1))) = (vol‘((𝐹‘𝑗) ∪ ((𝐹‘(𝑗 + 1)) ∖ (𝐹‘𝑗)))))
102		simplll 774	. . . . . . . . . . . . . . . . . 18 ⊢ ((((𝐹:ℕ⟶dom vol ∧ ∀𝑛 ∈ ℕ (𝐹‘𝑛) ⊆ (𝐹‘(𝑛 + 1))) ∧ ∀𝑘 ∈ ℕ (vol‘(𝐹‘𝑘)) ∈ ℝ) ∧ 𝑗 ∈ ℕ) → 𝐹:ℕ⟶dom vol)
103	102, 96	ffvelcdmd 7119	. . . . . . . . . . . . . . . . 17 ⊢ ((((𝐹:ℕ⟶dom vol ∧ ∀𝑛 ∈ ℕ (𝐹‘𝑛) ⊆ (𝐹‘(𝑛 + 1))) ∧ ∀𝑘 ∈ ℕ (vol‘(𝐹‘𝑘)) ∈ ℝ) ∧ 𝑗 ∈ ℕ) → (𝐹‘𝑗) ∈ dom vol)
104		peano2nn 12305	. . . . . . . . . . . . . . . . . . . 20 ⊢ (𝑗 ∈ ℕ → (𝑗 + 1) ∈ ℕ)
105	104	adantl 481	. . . . . . . . . . . . . . . . . . 19 ⊢ ((((𝐹:ℕ⟶dom vol ∧ ∀𝑛 ∈ ℕ (𝐹‘𝑛) ⊆ (𝐹‘(𝑛 + 1))) ∧ ∀𝑘 ∈ ℕ (vol‘(𝐹‘𝑘)) ∈ ℝ) ∧ 𝑗 ∈ ℕ) → (𝑗 + 1) ∈ ℕ)
106	102, 105	ffvelcdmd 7119	. . . . . . . . . . . . . . . . . 18 ⊢ ((((𝐹:ℕ⟶dom vol ∧ ∀𝑛 ∈ ℕ (𝐹‘𝑛) ⊆ (𝐹‘(𝑛 + 1))) ∧ ∀𝑘 ∈ ℕ (vol‘(𝐹‘𝑘)) ∈ ℝ) ∧ 𝑗 ∈ ℕ) → (𝐹‘(𝑗 + 1)) ∈ dom vol)
107		difmbl 25597	. . . . . . . . . . . . . . . . . 18 ⊢ (((𝐹‘(𝑗 + 1)) ∈ dom vol ∧ (𝐹‘𝑗) ∈ dom vol) → ((𝐹‘(𝑗 + 1)) ∖ (𝐹‘𝑗)) ∈ dom vol)
108	106, 103, 107	syl2anc 583	. . . . . . . . . . . . . . . . 17 ⊢ ((((𝐹:ℕ⟶dom vol ∧ ∀𝑛 ∈ ℕ (𝐹‘𝑛) ⊆ (𝐹‘(𝑛 + 1))) ∧ ∀𝑘 ∈ ℕ (vol‘(𝐹‘𝑘)) ∈ ℝ) ∧ 𝑗 ∈ ℕ) → ((𝐹‘(𝑗 + 1)) ∖ (𝐹‘𝑗)) ∈ dom vol)
109		disjdif 4495	. . . . . . . . . . . . . . . . . 18 ⊢ ((𝐹‘𝑗) ∩ ((𝐹‘(𝑗 + 1)) ∖ (𝐹‘𝑗))) = ∅
110	109	a1i 11	. . . . . . . . . . . . . . . . 17 ⊢ ((((𝐹:ℕ⟶dom vol ∧ ∀𝑛 ∈ ℕ (𝐹‘𝑛) ⊆ (𝐹‘(𝑛 + 1))) ∧ ∀𝑘 ∈ ℕ (vol‘(𝐹‘𝑘)) ∈ ℝ) ∧ 𝑗 ∈ ℕ) → ((𝐹‘𝑗) ∩ ((𝐹‘(𝑗 + 1)) ∖ (𝐹‘𝑗))) = ∅)
111		2fveq3 6925	. . . . . . . . . . . . . . . . . . 19 ⊢ (𝑘 = 𝑗 → (vol‘(𝐹‘𝑘)) = (vol‘(𝐹‘𝑗)))
112	111	eleq1d 2829	. . . . . . . . . . . . . . . . . 18 ⊢ (𝑘 = 𝑗 → ((vol‘(𝐹‘𝑘)) ∈ ℝ ↔ (vol‘(𝐹‘𝑗)) ∈ ℝ))
113		simplr 768	. . . . . . . . . . . . . . . . . 18 ⊢ ((((𝐹:ℕ⟶dom vol ∧ ∀𝑛 ∈ ℕ (𝐹‘𝑛) ⊆ (𝐹‘(𝑛 + 1))) ∧ ∀𝑘 ∈ ℕ (vol‘(𝐹‘𝑘)) ∈ ℝ) ∧ 𝑗 ∈ ℕ) → ∀𝑘 ∈ ℕ (vol‘(𝐹‘𝑘)) ∈ ℝ)
114	112, 113, 96	rspcdva 3636	. . . . . . . . . . . . . . . . 17 ⊢ ((((𝐹:ℕ⟶dom vol ∧ ∀𝑛 ∈ ℕ (𝐹‘𝑛) ⊆ (𝐹‘(𝑛 + 1))) ∧ ∀𝑘 ∈ ℕ (vol‘(𝐹‘𝑘)) ∈ ℝ) ∧ 𝑗 ∈ ℕ) → (vol‘(𝐹‘𝑗)) ∈ ℝ)
115		mblvol 25584	. . . . . . . . . . . . . . . . . . 19 ⊢ (((𝐹‘(𝑗 + 1)) ∖ (𝐹‘𝑗)) ∈ dom vol → (vol‘((𝐹‘(𝑗 + 1)) ∖ (𝐹‘𝑗))) = (vol*‘((𝐹‘(𝑗 + 1)) ∖ (𝐹‘𝑗))))
116	108, 115	syl 17	. . . . . . . . . . . . . . . . . 18 ⊢ ((((𝐹:ℕ⟶dom vol ∧ ∀𝑛 ∈ ℕ (𝐹‘𝑛) ⊆ (𝐹‘(𝑛 + 1))) ∧ ∀𝑘 ∈ ℕ (vol‘(𝐹‘𝑘)) ∈ ℝ) ∧ 𝑗 ∈ ℕ) → (vol‘((𝐹‘(𝑗 + 1)) ∖ (𝐹‘𝑗))) = (vol*‘((𝐹‘(𝑗 + 1)) ∖ (𝐹‘𝑗))))
117		difssd 4160	. . . . . . . . . . . . . . . . . . 19 ⊢ ((((𝐹:ℕ⟶dom vol ∧ ∀𝑛 ∈ ℕ (𝐹‘𝑛) ⊆ (𝐹‘(𝑛 + 1))) ∧ ∀𝑘 ∈ ℕ (vol‘(𝐹‘𝑘)) ∈ ℝ) ∧ 𝑗 ∈ ℕ) → ((𝐹‘(𝑗 + 1)) ∖ (𝐹‘𝑗)) ⊆ (𝐹‘(𝑗 + 1)))
118		mblss 25585	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((𝐹‘(𝑗 + 1)) ∈ dom vol → (𝐹‘(𝑗 + 1)) ⊆ ℝ)
119	106, 118	syl 17	. . . . . . . . . . . . . . . . . . 19 ⊢ ((((𝐹:ℕ⟶dom vol ∧ ∀𝑛 ∈ ℕ (𝐹‘𝑛) ⊆ (𝐹‘(𝑛 + 1))) ∧ ∀𝑘 ∈ ℕ (vol‘(𝐹‘𝑘)) ∈ ℝ) ∧ 𝑗 ∈ ℕ) → (𝐹‘(𝑗 + 1)) ⊆ ℝ)
120		mblvol 25584	. . . . . . . . . . . . . . . . . . . . 21 ⊢ ((𝐹‘(𝑗 + 1)) ∈ dom vol → (vol‘(𝐹‘(𝑗 + 1))) = (vol*‘(𝐹‘(𝑗 + 1))))
121	106, 120	syl 17	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((((𝐹:ℕ⟶dom vol ∧ ∀𝑛 ∈ ℕ (𝐹‘𝑛) ⊆ (𝐹‘(𝑛 + 1))) ∧ ∀𝑘 ∈ ℕ (vol‘(𝐹‘𝑘)) ∈ ℝ) ∧ 𝑗 ∈ ℕ) → (vol‘(𝐹‘(𝑗 + 1))) = (vol*‘(𝐹‘(𝑗 + 1))))
122		2fveq3 6925	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (𝑘 = (𝑗 + 1) → (vol‘(𝐹‘𝑘)) = (vol‘(𝐹‘(𝑗 + 1))))
123	122	eleq1d 2829	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (𝑘 = (𝑗 + 1) → ((vol‘(𝐹‘𝑘)) ∈ ℝ ↔ (vol‘(𝐹‘(𝑗 + 1))) ∈ ℝ))
124	123, 113, 105	rspcdva 3636	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((((𝐹:ℕ⟶dom vol ∧ ∀𝑛 ∈ ℕ (𝐹‘𝑛) ⊆ (𝐹‘(𝑛 + 1))) ∧ ∀𝑘 ∈ ℕ (vol‘(𝐹‘𝑘)) ∈ ℝ) ∧ 𝑗 ∈ ℕ) → (vol‘(𝐹‘(𝑗 + 1))) ∈ ℝ)
125	121, 124	eqeltrrd 2845	. . . . . . . . . . . . . . . . . . 19 ⊢ ((((𝐹:ℕ⟶dom vol ∧ ∀𝑛 ∈ ℕ (𝐹‘𝑛) ⊆ (𝐹‘(𝑛 + 1))) ∧ ∀𝑘 ∈ ℕ (vol‘(𝐹‘𝑘)) ∈ ℝ) ∧ 𝑗 ∈ ℕ) → (vol*‘(𝐹‘(𝑗 + 1))) ∈ ℝ)
126		ovolsscl 25540	. . . . . . . . . . . . . . . . . . 19 ⊢ ((((𝐹‘(𝑗 + 1)) ∖ (𝐹‘𝑗)) ⊆ (𝐹‘(𝑗 + 1)) ∧ (𝐹‘(𝑗 + 1)) ⊆ ℝ ∧ (vol‘(𝐹‘(𝑗 + 1))) ∈ ℝ) → (vol‘((𝐹‘(𝑗 + 1)) ∖ (𝐹‘𝑗))) ∈ ℝ)
127	117, 119, 125, 126	syl3anc 1371	. . . . . . . . . . . . . . . . . 18 ⊢ ((((𝐹:ℕ⟶dom vol ∧ ∀𝑛 ∈ ℕ (𝐹‘𝑛) ⊆ (𝐹‘(𝑛 + 1))) ∧ ∀𝑘 ∈ ℕ (vol‘(𝐹‘𝑘)) ∈ ℝ) ∧ 𝑗 ∈ ℕ) → (vol*‘((𝐹‘(𝑗 + 1)) ∖ (𝐹‘𝑗))) ∈ ℝ)
128	116, 127	eqeltrd 2844	. . . . . . . . . . . . . . . . 17 ⊢ ((((𝐹:ℕ⟶dom vol ∧ ∀𝑛 ∈ ℕ (𝐹‘𝑛) ⊆ (𝐹‘(𝑛 + 1))) ∧ ∀𝑘 ∈ ℕ (vol‘(𝐹‘𝑘)) ∈ ℝ) ∧ 𝑗 ∈ ℕ) → (vol‘((𝐹‘(𝑗 + 1)) ∖ (𝐹‘𝑗))) ∈ ℝ)
129		volun 25599	. . . . . . . . . . . . . . . . 17 ⊢ ((((𝐹‘𝑗) ∈ dom vol ∧ ((𝐹‘(𝑗 + 1)) ∖ (𝐹‘𝑗)) ∈ dom vol ∧ ((𝐹‘𝑗) ∩ ((𝐹‘(𝑗 + 1)) ∖ (𝐹‘𝑗))) = ∅) ∧ ((vol‘(𝐹‘𝑗)) ∈ ℝ ∧ (vol‘((𝐹‘(𝑗 + 1)) ∖ (𝐹‘𝑗))) ∈ ℝ)) → (vol‘((𝐹‘𝑗) ∪ ((𝐹‘(𝑗 + 1)) ∖ (𝐹‘𝑗)))) = ((vol‘(𝐹‘𝑗)) + (vol‘((𝐹‘(𝑗 + 1)) ∖ (𝐹‘𝑗)))))
130	103, 108, 110, 114, 128, 129	syl32anc 1378	. . . . . . . . . . . . . . . 16 ⊢ ((((𝐹:ℕ⟶dom vol ∧ ∀𝑛 ∈ ℕ (𝐹‘𝑛) ⊆ (𝐹‘(𝑛 + 1))) ∧ ∀𝑘 ∈ ℕ (vol‘(𝐹‘𝑘)) ∈ ℝ) ∧ 𝑗 ∈ ℕ) → (vol‘((𝐹‘𝑗) ∪ ((𝐹‘(𝑗 + 1)) ∖ (𝐹‘𝑗)))) = ((vol‘(𝐹‘𝑗)) + (vol‘((𝐹‘(𝑗 + 1)) ∖ (𝐹‘𝑗)))))
131	95	adantr 480	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ (((((𝐹:ℕ⟶dom vol ∧ ∀𝑛 ∈ ℕ (𝐹‘𝑛) ⊆ (𝐹‘(𝑛 + 1))) ∧ ∀𝑘 ∈ ℕ (vol‘(𝐹‘𝑘)) ∈ ℝ) ∧ 𝑗 ∈ ℕ) ∧ 𝑚 ∈ (1...𝑗)) → ∀𝑛 ∈ ℕ (𝐹‘𝑛) ⊆ (𝐹‘(𝑛 + 1)))
132		elfznn 13613	. . . . . . . . . . . . . . . . . . . . . . . . . 26 ⊢ (𝑚 ∈ (1...𝑗) → 𝑚 ∈ ℕ)
133	132	adantl 481	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ (((((𝐹:ℕ⟶dom vol ∧ ∀𝑛 ∈ ℕ (𝐹‘𝑛) ⊆ (𝐹‘(𝑛 + 1))) ∧ ∀𝑘 ∈ ℕ (vol‘(𝐹‘𝑘)) ∈ ℝ) ∧ 𝑗 ∈ ℕ) ∧ 𝑚 ∈ (1...𝑗)) → 𝑚 ∈ ℕ)
134		elfzuz3 13581	. . . . . . . . . . . . . . . . . . . . . . . . . 26 ⊢ (𝑚 ∈ (1...𝑗) → 𝑗 ∈ (ℤ_≥‘𝑚))
135	134	adantl 481	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ (((((𝐹:ℕ⟶dom vol ∧ ∀𝑛 ∈ ℕ (𝐹‘𝑛) ⊆ (𝐹‘(𝑛 + 1))) ∧ ∀𝑘 ∈ ℕ (vol‘(𝐹‘𝑘)) ∈ ℝ) ∧ 𝑗 ∈ ℕ) ∧ 𝑚 ∈ (1...𝑗)) → 𝑗 ∈ (ℤ_≥‘𝑚))
136		volsuplem 25609	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ ((∀𝑛 ∈ ℕ (𝐹‘𝑛) ⊆ (𝐹‘(𝑛 + 1)) ∧ (𝑚 ∈ ℕ ∧ 𝑗 ∈ (ℤ_≥‘𝑚))) → (𝐹‘𝑚) ⊆ (𝐹‘𝑗))
137	131, 133, 135, 136	syl12anc 836	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ (((((𝐹:ℕ⟶dom vol ∧ ∀𝑛 ∈ ℕ (𝐹‘𝑛) ⊆ (𝐹‘(𝑛 + 1))) ∧ ∀𝑘 ∈ ℕ (vol‘(𝐹‘𝑘)) ∈ ℝ) ∧ 𝑗 ∈ ℕ) ∧ 𝑚 ∈ (1...𝑗)) → (𝐹‘𝑚) ⊆ (𝐹‘𝑗))
138	137	ralrimiva 3152	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ ((((𝐹:ℕ⟶dom vol ∧ ∀𝑛 ∈ ℕ (𝐹‘𝑛) ⊆ (𝐹‘(𝑛 + 1))) ∧ ∀𝑘 ∈ ℕ (vol‘(𝐹‘𝑘)) ∈ ℝ) ∧ 𝑗 ∈ ℕ) → ∀𝑚 ∈ (1...𝑗)(𝐹‘𝑚) ⊆ (𝐹‘𝑗))
139		iunss 5068	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ (∪ 𝑚 ∈ (1...𝑗)(𝐹‘𝑚) ⊆ (𝐹‘𝑗) ↔ ∀𝑚 ∈ (1...𝑗)(𝐹‘𝑚) ⊆ (𝐹‘𝑗))
140	138, 139	sylibr 234	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ ((((𝐹:ℕ⟶dom vol ∧ ∀𝑛 ∈ ℕ (𝐹‘𝑛) ⊆ (𝐹‘(𝑛 + 1))) ∧ ∀𝑘 ∈ ℕ (vol‘(𝐹‘𝑘)) ∈ ℝ) ∧ 𝑗 ∈ ℕ) → ∪ 𝑚 ∈ (1...𝑗)(𝐹‘𝑚) ⊆ (𝐹‘𝑗))
141	96, 6	eleqtrdi 2854	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ ((((𝐹:ℕ⟶dom vol ∧ ∀𝑛 ∈ ℕ (𝐹‘𝑛) ⊆ (𝐹‘(𝑛 + 1))) ∧ ∀𝑘 ∈ ℕ (vol‘(𝐹‘𝑘)) ∈ ℝ) ∧ 𝑗 ∈ ℕ) → 𝑗 ∈ (ℤ_≥‘1))
142		eluzfz2 13592	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ (𝑗 ∈ (ℤ_≥‘1) → 𝑗 ∈ (1...𝑗))
143	141, 142	syl 17	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ ((((𝐹:ℕ⟶dom vol ∧ ∀𝑛 ∈ ℕ (𝐹‘𝑛) ⊆ (𝐹‘(𝑛 + 1))) ∧ ∀𝑘 ∈ ℕ (vol‘(𝐹‘𝑘)) ∈ ℝ) ∧ 𝑗 ∈ ℕ) → 𝑗 ∈ (1...𝑗))
144		fveq2 6920	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ (𝑚 = 𝑗 → (𝐹‘𝑚) = (𝐹‘𝑗))
145	144	ssiun2s 5071	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ (𝑗 ∈ (1...𝑗) → (𝐹‘𝑗) ⊆ ∪ 𝑚 ∈ (1...𝑗)(𝐹‘𝑚))
146	143, 145	syl 17	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ ((((𝐹:ℕ⟶dom vol ∧ ∀𝑛 ∈ ℕ (𝐹‘𝑛) ⊆ (𝐹‘(𝑛 + 1))) ∧ ∀𝑘 ∈ ℕ (vol‘(𝐹‘𝑘)) ∈ ℝ) ∧ 𝑗 ∈ ℕ) → (𝐹‘𝑗) ⊆ ∪ 𝑚 ∈ (1...𝑗)(𝐹‘𝑚))
147	140, 146	eqssd 4026	. . . . . . . . . . . . . . . . . . . . 21 ⊢ ((((𝐹:ℕ⟶dom vol ∧ ∀𝑛 ∈ ℕ (𝐹‘𝑛) ⊆ (𝐹‘(𝑛 + 1))) ∧ ∀𝑘 ∈ ℕ (vol‘(𝐹‘𝑘)) ∈ ℝ) ∧ 𝑗 ∈ ℕ) → ∪ 𝑚 ∈ (1...𝑗)(𝐹‘𝑚) = (𝐹‘𝑗))
148	96	nnzd 12666	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ ((((𝐹:ℕ⟶dom vol ∧ ∀𝑛 ∈ ℕ (𝐹‘𝑛) ⊆ (𝐹‘(𝑛 + 1))) ∧ ∀𝑘 ∈ ℕ (vol‘(𝐹‘𝑘)) ∈ ℝ) ∧ 𝑗 ∈ ℕ) → 𝑗 ∈ ℤ)
149		fzval3 13785	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ (𝑗 ∈ ℤ → (1...𝑗) = (1..^(𝑗 + 1)))
150	148, 149	syl 17	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ ((((𝐹:ℕ⟶dom vol ∧ ∀𝑛 ∈ ℕ (𝐹‘𝑛) ⊆ (𝐹‘(𝑛 + 1))) ∧ ∀𝑘 ∈ ℕ (vol‘(𝐹‘𝑘)) ∈ ℝ) ∧ 𝑗 ∈ ℕ) → (1...𝑗) = (1..^(𝑗 + 1)))
151	150	iuneq1d 5042	. . . . . . . . . . . . . . . . . . . . 21 ⊢ ((((𝐹:ℕ⟶dom vol ∧ ∀𝑛 ∈ ℕ (𝐹‘𝑛) ⊆ (𝐹‘(𝑛 + 1))) ∧ ∀𝑘 ∈ ℕ (vol‘(𝐹‘𝑘)) ∈ ℝ) ∧ 𝑗 ∈ ℕ) → ∪ 𝑚 ∈ (1...𝑗)(𝐹‘𝑚) = ∪ 𝑚 ∈ (1..^(𝑗 + 1))(𝐹‘𝑚))
152	147, 151	eqtr3d 2782	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((((𝐹:ℕ⟶dom vol ∧ ∀𝑛 ∈ ℕ (𝐹‘𝑛) ⊆ (𝐹‘(𝑛 + 1))) ∧ ∀𝑘 ∈ ℕ (vol‘(𝐹‘𝑘)) ∈ ℝ) ∧ 𝑗 ∈ ℕ) → (𝐹‘𝑗) = ∪ 𝑚 ∈ (1..^(𝑗 + 1))(𝐹‘𝑚))
153	152	difeq2d 4149	. . . . . . . . . . . . . . . . . . 19 ⊢ ((((𝐹:ℕ⟶dom vol ∧ ∀𝑛 ∈ ℕ (𝐹‘𝑛) ⊆ (𝐹‘(𝑛 + 1))) ∧ ∀𝑘 ∈ ℕ (vol‘(𝐹‘𝑘)) ∈ ℝ) ∧ 𝑗 ∈ ℕ) → ((𝐹‘(𝑗 + 1)) ∖ (𝐹‘𝑗)) = ((𝐹‘(𝑗 + 1)) ∖ ∪ 𝑚 ∈ (1..^(𝑗 + 1))(𝐹‘𝑚)))
154	153	fveq2d 6924	. . . . . . . . . . . . . . . . . 18 ⊢ ((((𝐹:ℕ⟶dom vol ∧ ∀𝑛 ∈ ℕ (𝐹‘𝑛) ⊆ (𝐹‘(𝑛 + 1))) ∧ ∀𝑘 ∈ ℕ (vol‘(𝐹‘𝑘)) ∈ ℝ) ∧ 𝑗 ∈ ℕ) → (vol‘((𝐹‘(𝑗 + 1)) ∖ (𝐹‘𝑗))) = (vol‘((𝐹‘(𝑗 + 1)) ∖ ∪ 𝑚 ∈ (1..^(𝑗 + 1))(𝐹‘𝑚))))
155		fveq2 6920	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (𝑘 = (𝑗 + 1) → (𝐹‘𝑘) = (𝐹‘(𝑗 + 1)))
156		oveq2 7456	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ (𝑘 = (𝑗 + 1) → (1..^𝑘) = (1..^(𝑗 + 1)))
157	156	iuneq1d 5042	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (𝑘 = (𝑗 + 1) → ∪ 𝑚 ∈ (1..^𝑘)(𝐹‘𝑚) = ∪ 𝑚 ∈ (1..^(𝑗 + 1))(𝐹‘𝑚))
158	155, 157	difeq12d 4150	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (𝑘 = (𝑗 + 1) → ((𝐹‘𝑘) ∖ ∪ 𝑚 ∈ (1..^𝑘)(𝐹‘𝑚)) = ((𝐹‘(𝑗 + 1)) ∖ ∪ 𝑚 ∈ (1..^(𝑗 + 1))(𝐹‘𝑚)))
159	158	fveq2d 6924	. . . . . . . . . . . . . . . . . . . 20 ⊢ (𝑘 = (𝑗 + 1) → (vol‘((𝐹‘𝑘) ∖ ∪ 𝑚 ∈ (1..^𝑘)(𝐹‘𝑚))) = (vol‘((𝐹‘(𝑗 + 1)) ∖ ∪ 𝑚 ∈ (1..^(𝑗 + 1))(𝐹‘𝑚))))
160		fvex 6933	. . . . . . . . . . . . . . . . . . . 20 ⊢ (vol‘((𝐹‘(𝑗 + 1)) ∖ ∪ 𝑚 ∈ (1..^(𝑗 + 1))(𝐹‘𝑚))) ∈ V
161	159, 34, 160	fvmpt 7029	. . . . . . . . . . . . . . . . . . 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 2783	. . . . . . . . . . . . . . . . 17 ⊢ ((((𝐹:ℕ⟶dom vol ∧ ∀𝑛 ∈ ℕ (𝐹‘𝑛) ⊆ (𝐹‘(𝑛 + 1))) ∧ ∀𝑘 ∈ ℕ (vol‘(𝐹‘𝑘)) ∈ ℝ) ∧ 𝑗 ∈ ℕ) → (vol‘((𝐹‘(𝑗 + 1)) ∖ (𝐹‘𝑗))) = ((𝑘 ∈ ℕ ↦ (vol‘((𝐹‘𝑘) ∖ ∪ 𝑚 ∈ (1..^𝑘)(𝐹‘𝑚))))‘(𝑗 + 1)))
164	163	oveq2d 7464	. . . . . . . . . . . . . . . 16 ⊢ ((((𝐹:ℕ⟶dom vol ∧ ∀𝑛 ∈ ℕ (𝐹‘𝑛) ⊆ (𝐹‘(𝑛 + 1))) ∧ ∀𝑘 ∈ ℕ (vol‘(𝐹‘𝑘)) ∈ ℝ) ∧ 𝑗 ∈ ℕ) → ((vol‘(𝐹‘𝑗)) + (vol‘((𝐹‘(𝑗 + 1)) ∖ (𝐹‘𝑗)))) = ((vol‘(𝐹‘𝑗)) + ((𝑘 ∈ ℕ ↦ (vol‘((𝐹‘𝑘) ∖ ∪ 𝑚 ∈ (1..^𝑘)(𝐹‘𝑚))))‘(𝑗 + 1))))
165	101, 130, 164	3eqtrd 2784	. . . . . . . . . . . . . . 15 ⊢ ((((𝐹:ℕ⟶dom vol ∧ ∀𝑛 ∈ ℕ (𝐹‘𝑛) ⊆ (𝐹‘(𝑛 + 1))) ∧ ∀𝑘 ∈ ℕ (vol‘(𝐹‘𝑘)) ∈ ℝ) ∧ 𝑗 ∈ ℕ) → (vol‘(𝐹‘(𝑗 + 1))) = ((vol‘(𝐹‘𝑗)) + ((𝑘 ∈ ℕ ↦ (vol‘((𝐹‘𝑘) ∖ ∪ 𝑚 ∈ (1..^𝑘)(𝐹‘𝑚))))‘(𝑗 + 1))))
166	90, 165	eqeq12d 2756	. . . . . . . . . . . . . 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 12311	. . . . . . . . . 10 ⊢ (𝑗 ∈ ℕ → (((𝐹:ℕ⟶dom vol ∧ ∀𝑛 ∈ ℕ (𝐹‘𝑛) ⊆ (𝐹‘(𝑛 + 1))) ∧ ∀𝑘 ∈ ℕ (vol‘(𝐹‘𝑘)) ∈ ℝ) → (seq1( + , (𝑘 ∈ ℕ ↦ (vol‘((𝐹‘𝑘) ∖ ∪ 𝑚 ∈ (1..^𝑘)(𝐹‘𝑚)))))‘𝑗) = (vol‘(𝐹‘𝑗))))
171	170	impcom 407	. . . . . . . . 9 ⊢ ((((𝐹:ℕ⟶dom vol ∧ ∀𝑛 ∈ ℕ (𝐹‘𝑛) ⊆ (𝐹‘(𝑛 + 1))) ∧ ∀𝑘 ∈ ℕ (vol‘(𝐹‘𝑘)) ∈ ℝ) ∧ 𝑗 ∈ ℕ) → (seq1( + , (𝑘 ∈ ℕ ↦ (vol‘((𝐹‘𝑘) ∖ ∪ 𝑚 ∈ (1..^𝑘)(𝐹‘𝑚)))))‘𝑗) = (vol‘(𝐹‘𝑗)))
172		fvco3 7021	. . . . . . . . . 10 ⊢ ((𝐹:ℕ⟶dom vol ∧ 𝑗 ∈ ℕ) → ((vol ∘ 𝐹)‘𝑗) = (vol‘(𝐹‘𝑗)))
173	51, 172	sylan 579	. . . . . . . . 9 ⊢ ((((𝐹:ℕ⟶dom vol ∧ ∀𝑛 ∈ ℕ (𝐹‘𝑛) ⊆ (𝐹‘(𝑛 + 1))) ∧ ∀𝑘 ∈ ℕ (vol‘(𝐹‘𝑘)) ∈ ℝ) ∧ 𝑗 ∈ ℕ) → ((vol ∘ 𝐹)‘𝑗) = (vol‘(𝐹‘𝑗)))
174	171, 173	eqtr4d 2783	. . . . . . . 8 ⊢ ((((𝐹:ℕ⟶dom vol ∧ ∀𝑛 ∈ ℕ (𝐹‘𝑛) ⊆ (𝐹‘(𝑛 + 1))) ∧ ∀𝑘 ∈ ℕ (vol‘(𝐹‘𝑘)) ∈ ℝ) ∧ 𝑗 ∈ ℕ) → (seq1( + , (𝑘 ∈ ℕ ↦ (vol‘((𝐹‘𝑘) ∖ ∪ 𝑚 ∈ (1..^𝑘)(𝐹‘𝑚)))))‘𝑗) = ((vol ∘ 𝐹)‘𝑗))
175	49, 54, 174	eqfnfvd 7067	. . . . . . 7 ⊢ (((𝐹:ℕ⟶dom vol ∧ ∀𝑛 ∈ ℕ (𝐹‘𝑛) ⊆ (𝐹‘(𝑛 + 1))) ∧ ∀𝑘 ∈ ℕ (vol‘(𝐹‘𝑘)) ∈ ℝ) → seq1( + , (𝑘 ∈ ℕ ↦ (vol‘((𝐹‘𝑘) ∖ ∪ 𝑚 ∈ (1..^𝑘)(𝐹‘𝑚))))) = (vol ∘ 𝐹))
176	175	rneqd 5963	. . . . . 6 ⊢ (((𝐹:ℕ⟶dom vol ∧ ∀𝑛 ∈ ℕ (𝐹‘𝑛) ⊆ (𝐹‘(𝑛 + 1))) ∧ ∀𝑘 ∈ ℕ (vol‘(𝐹‘𝑘)) ∈ ℝ) → ran seq1( + , (𝑘 ∈ ℕ ↦ (vol‘((𝐹‘𝑘) ∖ ∪ 𝑚 ∈ (1..^𝑘)(𝐹‘𝑚))))) = ran (vol ∘ 𝐹))
177		rnco2 6284	. . . . . 6 ⊢ ran (vol ∘ 𝐹) = (vol “ ran 𝐹)
178	176, 177	eqtrdi 2796	. . . . 5 ⊢ (((𝐹:ℕ⟶dom vol ∧ ∀𝑛 ∈ ℕ (𝐹‘𝑛) ⊆ (𝐹‘(𝑛 + 1))) ∧ ∀𝑘 ∈ ℕ (vol‘(𝐹‘𝑘)) ∈ ℝ) → ran seq1( + , (𝑘 ∈ ℕ ↦ (vol‘((𝐹‘𝑘) ∖ ∪ 𝑚 ∈ (1..^𝑘)(𝐹‘𝑚))))) = (vol “ ran 𝐹))
179	178	supeq1d 9515	. . . 4 ⊢ (((𝐹:ℕ⟶dom vol ∧ ∀𝑛 ∈ ℕ (𝐹‘𝑛) ⊆ (𝐹‘(𝑛 + 1))) ∧ ∀𝑘 ∈ ℕ (vol‘(𝐹‘𝑘)) ∈ ℝ) → sup(ran seq1( + , (𝑘 ∈ ℕ ↦ (vol‘((𝐹‘𝑘) ∖ ∪ 𝑚 ∈ (1..^𝑘)(𝐹‘𝑚))))), ℝ^, < ) = sup((vol “ ran 𝐹), ℝ^, < ))
180	36, 43, 179	3eqtr3d 2788	. . 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 3106	. . 3 ⊢ (∃𝑘 ∈ ℕ ¬ (vol‘(𝐹‘𝑘)) ∈ ℝ ↔ ¬ ∀𝑘 ∈ ℕ (vol‘(𝐹‘𝑘)) ∈ ℝ)
183		fniunfv 7284	. . . . . . . . . . . 12 ⊢ (𝐹 Fn ℕ → ∪ 𝑛 ∈ ℕ (𝐹‘𝑛) = ∪ ran 𝐹)
184	38, 183	syl 17	. . . . . . . . . . 11 ⊢ (𝐹:ℕ⟶dom vol → ∪ 𝑛 ∈ ℕ (𝐹‘𝑛) = ∪ ran 𝐹)
185		ffvelcdm 7115	. . . . . . . . . . . . 13 ⊢ ((𝐹:ℕ⟶dom vol ∧ 𝑛 ∈ ℕ) → (𝐹‘𝑛) ∈ dom vol)
186	185	ralrimiva 3152	. . . . . . . . . . . 12 ⊢ (𝐹:ℕ⟶dom vol → ∀𝑛 ∈ ℕ (𝐹‘𝑛) ∈ dom vol)
187		iunmbl 25607	. . . . . . . . . . . 12 ⊢ (∀𝑛 ∈ ℕ (𝐹‘𝑛) ∈ dom vol → ∪ 𝑛 ∈ ℕ (𝐹‘𝑛) ∈ dom vol)
188	186, 187	syl 17	. . . . . . . . . . 11 ⊢ (𝐹:ℕ⟶dom vol → ∪ 𝑛 ∈ ℕ (𝐹‘𝑛) ∈ dom vol)
189	184, 188	eqeltrrd 2845	. . . . . . . . . 10 ⊢ (𝐹:ℕ⟶dom vol → ∪ ran 𝐹 ∈ dom vol)
190	189	ad2antrr 725	. . . . . . . . 9 ⊢ (((𝐹:ℕ⟶dom vol ∧ ∀𝑛 ∈ ℕ (𝐹‘𝑛) ⊆ (𝐹‘(𝑛 + 1))) ∧ (𝑘 ∈ ℕ ∧ ¬ (vol‘(𝐹‘𝑘)) ∈ ℝ)) → ∪ ran 𝐹 ∈ dom vol)
191		mblss 25585	. . . . . . . . 9 ⊢ (∪ ran 𝐹 ∈ dom vol → ∪ ran 𝐹 ⊆ ℝ)
192	190, 191	syl 17	. . . . . . . 8 ⊢ (((𝐹:ℕ⟶dom vol ∧ ∀𝑛 ∈ ℕ (𝐹‘𝑛) ⊆ (𝐹‘(𝑛 + 1))) ∧ (𝑘 ∈ ℕ ∧ ¬ (vol‘(𝐹‘𝑘)) ∈ ℝ)) → ∪ ran 𝐹 ⊆ ℝ)
193		ovolcl 25532	. . . . . . . 8 ⊢ (∪ ran 𝐹 ⊆ ℝ → (vol‘∪ ran 𝐹) ∈ ℝ^)
194	192, 193	syl 17	. . . . . . 7 ⊢ (((𝐹:ℕ⟶dom vol ∧ ∀𝑛 ∈ ℕ (𝐹‘𝑛) ⊆ (𝐹‘(𝑛 + 1))) ∧ (𝑘 ∈ ℕ ∧ ¬ (vol‘(𝐹‘𝑘)) ∈ ℝ)) → (vol‘∪ ran 𝐹) ∈ ℝ^)
195		pnfge 13193	. . . . . . 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 746	. . . . . . . . . . . . 13 ⊢ (((𝐹:ℕ⟶dom vol ∧ ∀𝑛 ∈ ℕ (𝐹‘𝑛) ⊆ (𝐹‘(𝑛 + 1))) ∧ (𝑘 ∈ ℕ ∧ ¬ (vol‘(𝐹‘𝑘)) ∈ ℝ)) → (𝐹‘𝑘) ∈ dom vol)
199	198, 18	syl 17	. . . . . . . . . . . 12 ⊢ (((𝐹:ℕ⟶dom vol ∧ ∀𝑛 ∈ ℕ (𝐹‘𝑛) ⊆ (𝐹‘(𝑛 + 1))) ∧ (𝑘 ∈ ℕ ∧ ¬ (vol‘(𝐹‘𝑘)) ∈ ℝ)) → (𝐹‘𝑘) ⊆ ℝ)
200		ovolcl 25532	. . . . . . . . . . . 12 ⊢ ((𝐹‘𝑘) ⊆ ℝ → (vol‘(𝐹‘𝑘)) ∈ ℝ^)
201	199, 200	syl 17	. . . . . . . . . . 11 ⊢ (((𝐹:ℕ⟶dom vol ∧ ∀𝑛 ∈ ℕ (𝐹‘𝑛) ⊆ (𝐹‘(𝑛 + 1))) ∧ (𝑘 ∈ ℕ ∧ ¬ (vol‘(𝐹‘𝑘)) ∈ ℝ)) → (vol‘(𝐹‘𝑘)) ∈ ℝ^)
202		xrrebnd 13230	. . . . . . . . . . 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 2829	. . . . . . . . . 10 ⊢ (((𝐹:ℕ⟶dom vol ∧ ∀𝑛 ∈ ℕ (𝐹‘𝑛) ⊆ (𝐹‘(𝑛 + 1))) ∧ (𝑘 ∈ ℕ ∧ ¬ (vol‘(𝐹‘𝑘)) ∈ ℝ)) → ((vol‘(𝐹‘𝑘)) ∈ ℝ ↔ (vol*‘(𝐹‘𝑘)) ∈ ℝ))
206		ovolge0 25535	. . . . . . . . . . . . 13 ⊢ ((𝐹‘𝑘) ⊆ ℝ → 0 ≤ (vol*‘(𝐹‘𝑘)))
207		mnflt0 13188	. . . . . . . . . . . . . 14 ⊢ -∞ < 0
208		mnfxr 11347	. . . . . . . . . . . . . . 15 ⊢ -∞ ∈ ℝ^*
209		0xr 11337	. . . . . . . . . . . . . . 15 ⊢ 0 ∈ ℝ^*
210		xrltletr 13219	. . . . . . . . . . . . . . 15 ⊢ ((-∞ ∈ ℝ^* ∧ 0 ∈ ℝ^* ∧ (vol‘(𝐹‘𝑘)) ∈ ℝ^) → ((-∞ < 0 ∧ 0 ≤ (vol‘(𝐹‘𝑘))) → -∞ < (vol‘(𝐹‘𝑘))))
211	208, 209, 210	mp3an12 1451	. . . . . . . . . . . . . 14 ⊢ ((vol‘(𝐹‘𝑘)) ∈ ℝ^ → ((-∞ < 0 ∧ 0 ≤ (vol‘(𝐹‘𝑘))) → -∞ < (vol‘(𝐹‘𝑘))))
212	207, 211	mpani 695	. . . . . . . . . . . . 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 13226	. . . . . . . . 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 725	. . . . . . . . . 10 ⊢ (((𝐹:ℕ⟶dom vol ∧ ∀𝑛 ∈ ℕ (𝐹‘𝑛) ⊆ (𝐹‘(𝑛 + 1))) ∧ (𝑘 ∈ ℕ ∧ ¬ (vol‘(𝐹‘𝑘)) ∈ ℝ)) → 𝐹 Fn ℕ)
222		simprl 770	. . . . . . . . . 10 ⊢ (((𝐹:ℕ⟶dom vol ∧ ∀𝑛 ∈ ℕ (𝐹‘𝑛) ⊆ (𝐹‘(𝑛 + 1))) ∧ (𝑘 ∈ ℕ ∧ ¬ (vol‘(𝐹‘𝑘)) ∈ ℝ)) → 𝑘 ∈ ℕ)
223		fnfvelrn 7114	. . . . . . . . . 10 ⊢ ((𝐹 Fn ℕ ∧ 𝑘 ∈ ℕ) → (𝐹‘𝑘) ∈ ran 𝐹)
224	221, 222, 223	syl2anc 583	. . . . . . . . 9 ⊢ (((𝐹:ℕ⟶dom vol ∧ ∀𝑛 ∈ ℕ (𝐹‘𝑛) ⊆ (𝐹‘(𝑛 + 1))) ∧ (𝑘 ∈ ℕ ∧ ¬ (vol‘(𝐹‘𝑘)) ∈ ℝ)) → (𝐹‘𝑘) ∈ ran 𝐹)
225		elssuni 4961	. . . . . . . . 9 ⊢ ((𝐹‘𝑘) ∈ ran 𝐹 → (𝐹‘𝑘) ⊆ ∪ ran 𝐹)
226	224, 225	syl 17	. . . . . . . 8 ⊢ (((𝐹:ℕ⟶dom vol ∧ ∀𝑛 ∈ ℕ (𝐹‘𝑛) ⊆ (𝐹‘(𝑛 + 1))) ∧ (𝑘 ∈ ℕ ∧ ¬ (vol‘(𝐹‘𝑘)) ∈ ℝ)) → (𝐹‘𝑘) ⊆ ∪ ran 𝐹)
227		ovolss 25539	. . . . . . . 8 ⊢ (((𝐹‘𝑘) ⊆ ∪ ran 𝐹 ∧ ∪ ran 𝐹 ⊆ ℝ) → (vol‘(𝐹‘𝑘)) ≤ (vol‘∪ ran 𝐹))
228	226, 192, 227	syl2anc 583	. . . . . . 7 ⊢ (((𝐹:ℕ⟶dom vol ∧ ∀𝑛 ∈ ℕ (𝐹‘𝑛) ⊆ (𝐹‘(𝑛 + 1))) ∧ (𝑘 ∈ ℕ ∧ ¬ (vol‘(𝐹‘𝑘)) ∈ ℝ)) → (vol‘(𝐹‘𝑘)) ≤ (vol‘∪ ran 𝐹))
229	220, 228	eqbrtrrd 5190	. . . . . 6 ⊢ (((𝐹:ℕ⟶dom vol ∧ ∀𝑛 ∈ ℕ (𝐹‘𝑛) ⊆ (𝐹‘(𝑛 + 1))) ∧ (𝑘 ∈ ℕ ∧ ¬ (vol‘(𝐹‘𝑘)) ∈ ℝ)) → +∞ ≤ (vol*‘∪ ran 𝐹))
230		pnfxr 11344	. . . . . . 7 ⊢ +∞ ∈ ℝ^*
231		xrletri3 13216	. . . . . . 7 ⊢ (((vol‘∪ ran 𝐹) ∈ ℝ^ ∧ +∞ ∈ ℝ^) → ((vol‘∪ ran 𝐹) = +∞ ↔ ((vol‘∪ ran 𝐹) ≤ +∞ ∧ +∞ ≤ (vol‘∪ ran 𝐹))))
232	194, 230, 231	sylancl 585	. . . . . 6 ⊢ (((𝐹:ℕ⟶dom vol ∧ ∀𝑛 ∈ ℕ (𝐹‘𝑛) ⊆ (𝐹‘(𝑛 + 1))) ∧ (𝑘 ∈ ℕ ∧ ¬ (vol‘(𝐹‘𝑘)) ∈ ℝ)) → ((vol‘∪ ran 𝐹) = +∞ ↔ ((vol‘∪ ran 𝐹) ≤ +∞ ∧ +∞ ≤ (vol*‘∪ ran 𝐹))))
233	196, 229, 232	mpbir2and 712	. . . . 5 ⊢ (((𝐹:ℕ⟶dom vol ∧ ∀𝑛 ∈ ℕ (𝐹‘𝑛) ⊆ (𝐹‘(𝑛 + 1))) ∧ (𝑘 ∈ ℕ ∧ ¬ (vol‘(𝐹‘𝑘)) ∈ ℝ)) → (vol*‘∪ ran 𝐹) = +∞)
234		mblvol 25584	. . . . . 6 ⊢ (∪ ran 𝐹 ∈ dom vol → (vol‘∪ ran 𝐹) = (vol*‘∪ ran 𝐹))
235	190, 234	syl 17	. . . . 5 ⊢ (((𝐹:ℕ⟶dom vol ∧ ∀𝑛 ∈ ℕ (𝐹‘𝑛) ⊆ (𝐹‘(𝑛 + 1))) ∧ (𝑘 ∈ ℕ ∧ ¬ (vol‘(𝐹‘𝑘)) ∈ ℝ)) → (vol‘∪ ran 𝐹) = (vol*‘∪ ran 𝐹))
236		imassrn 6100	. . . . . . 7 ⊢ (vol “ ran 𝐹) ⊆ ran vol
237		frn 6754	. . . . . . . . 9 ⊢ (vol:dom vol⟶(0[,]+∞) → ran vol ⊆ (0[,]+∞))
238	50, 237	ax-mp 5	. . . . . . . 8 ⊢ ran vol ⊆ (0[,]+∞)
239		iccssxr 13490	. . . . . . . 8 ⊢ (0[,]+∞) ⊆ ℝ^*
240	238, 239	sstri 4018	. . . . . . 7 ⊢ ran vol ⊆ ℝ^*
241	236, 240	sstri 4018	. . . . . 6 ⊢ (vol “ ran 𝐹) ⊆ ℝ^*
242	204, 220	eqtrd 2780	. . . . . . 7 ⊢ (((𝐹:ℕ⟶dom vol ∧ ∀𝑛 ∈ ℕ (𝐹‘𝑛) ⊆ (𝐹‘(𝑛 + 1))) ∧ (𝑘 ∈ ℕ ∧ ¬ (vol‘(𝐹‘𝑘)) ∈ ℝ)) → (vol‘(𝐹‘𝑘)) = +∞)
243		simpll 766	. . . . . . . 8 ⊢ (((𝐹:ℕ⟶dom vol ∧ ∀𝑛 ∈ ℕ (𝐹‘𝑛) ⊆ (𝐹‘(𝑛 + 1))) ∧ (𝑘 ∈ ℕ ∧ ¬ (vol‘(𝐹‘𝑘)) ∈ ℝ)) → 𝐹:ℕ⟶dom vol)
244		ffun 6750	. . . . . . . . . 10 ⊢ (vol:dom vol⟶(0[,]+∞) → Fun vol)
245	50, 244	ax-mp 5	. . . . . . . . 9 ⊢ Fun vol
246		frn 6754	. . . . . . . . 9 ⊢ (𝐹:ℕ⟶dom vol → ran 𝐹 ⊆ dom vol)
247		funfvima2 7268	. . . . . . . . 9 ⊢ ((Fun vol ∧ ran 𝐹 ⊆ dom vol) → ((𝐹‘𝑘) ∈ ran 𝐹 → (vol‘(𝐹‘𝑘)) ∈ (vol “ ran 𝐹)))
248	245, 246, 247	sylancr 586	. . . . . . . 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 2845	. . . . . 6 ⊢ (((𝐹:ℕ⟶dom vol ∧ ∀𝑛 ∈ ℕ (𝐹‘𝑛) ⊆ (𝐹‘(𝑛 + 1))) ∧ (𝑘 ∈ ℕ ∧ ¬ (vol‘(𝐹‘𝑘)) ∈ ℝ)) → +∞ ∈ (vol “ ran 𝐹))
251		supxrpnf 13380	. . . . . 6 ⊢ (((vol “ ran 𝐹) ⊆ ℝ^* ∧ +∞ ∈ (vol “ ran 𝐹)) → sup((vol “ ran 𝐹), ℝ^*, < ) = +∞)
252	241, 250, 251	sylancr 586	. . . . 5 ⊢ (((𝐹:ℕ⟶dom vol ∧ ∀𝑛 ∈ ℕ (𝐹‘𝑛) ⊆ (𝐹‘(𝑛 + 1))) ∧ (𝑘 ∈ ℕ ∧ ¬ (vol‘(𝐹‘𝑘)) ∈ ℝ)) → sup((vol “ ran 𝐹), ℝ^*, < ) = +∞)
253	233, 235, 252	3eqtr4d 2790	. . . 4 ⊢ (((𝐹:ℕ⟶dom vol ∧ ∀𝑛 ∈ ℕ (𝐹‘𝑛) ⊆ (𝐹‘(𝑛 + 1))) ∧ (𝑘 ∈ ℕ ∧ ¬ (vol‘(𝐹‘𝑘)) ∈ ℝ)) → (vol‘∪ ran 𝐹) = sup((vol “ ran 𝐹), ℝ^*, < ))
254	253	rexlimdvaa 3162	. . 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 1537 ∈ wcel 2108 ∀wral 3067 ∃wrex 3076 ∖ cdif 3973 ∪ cun 3974 ∩ cin 3975 ⊆ wss 3976 ∅c0 4352 ∪ cuni 4931 ∪ ciun 5015 Disj wdisj 5133 class class class wbr 5166 ↦ cmpt 5249 dom cdm 5700 ran crn 5701 “ cima 5703 ∘ ccom 5704 Fun wfun 6567 Fn wfn 6568 ⟶wf 6569 ‘cfv 6573 (class class class)co 7448 Fincfn 9003 supcsup 9509 ℝcr 11183 0cc0 11184 1c1 11185 + caddc 11187 +∞cpnf 11321 -∞cmnf 11322 ℝ^*cxr 11323 < clt 11324 ≤ cle 11325 ℕcn 12293 ℤcz 12639 ℤ_≥cuz 12903 [,]cicc 13410 ...cfz 13567 ..^cfzo 13711 seqcseq 14052 vol*covol 25516 volcvol 25517

This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1793 ax-4 1807 ax-5 1909 ax-6 1967 ax-7 2007 ax-8 2110 ax-9 2118 ax-10 2141 ax-11 2158 ax-12 2178 ax-ext 2711 ax-rep 5303 ax-sep 5317 ax-nul 5324 ax-pow 5383 ax-pr 5447 ax-un 7770 ax-inf2 9710 ax-cc 10504 ax-cnex 11240 ax-resscn 11241 ax-1cn 11242 ax-icn 11243 ax-addcl 11244 ax-addrcl 11245 ax-mulcl 11246 ax-mulrcl 11247 ax-mulcom 11248 ax-addass 11249 ax-mulass 11250 ax-distr 11251 ax-i2m1 11252 ax-1ne0 11253 ax-1rid 11254 ax-rnegex 11255 ax-rrecex 11256 ax-cnre 11257 ax-pre-lttri 11258 ax-pre-lttrn 11259 ax-pre-ltadd 11260 ax-pre-mulgt0 11261 ax-pre-sup 11262

This theorem depends on definitions: df-bi 207 df-an 396 df-or 847 df-3or 1088 df-3an 1089 df-tru 1540 df-fal 1550 df-ex 1778 df-nf 1782 df-sb 2065 df-mo 2543 df-eu 2572 df-clab 2718 df-cleq 2732 df-clel 2819 df-nfc 2895 df-ne 2947 df-nel 3053 df-ral 3068 df-rex 3077 df-rmo 3388 df-reu 3389 df-rab 3444 df-v 3490 df-sbc 3805 df-csb 3922 df-dif 3979 df-un 3981 df-in 3983 df-ss 3993 df-pss 3996 df-nul 4353 df-if 4549 df-pw 4624 df-sn 4649 df-pr 4651 df-op 4655 df-uni 4932 df-int 4971 df-iun 5017 df-disj 5134 df-br 5167 df-opab 5229 df-mpt 5250 df-tr 5284 df-id 5593 df-eprel 5599 df-po 5607 df-so 5608 df-fr 5652 df-se 5653 df-we 5654 df-xp 5706 df-rel 5707 df-cnv 5708 df-co 5709 df-dm 5710 df-rn 5711 df-res 5712 df-ima 5713 df-pred 6332 df-ord 6398 df-on 6399 df-lim 6400 df-suc 6401 df-iota 6525 df-fun 6575 df-fn 6576 df-f 6577 df-f1 6578 df-fo 6579 df-f1o 6580 df-fv 6581 df-isom 6582 df-riota 7404 df-ov 7451 df-oprab 7452 df-mpo 7453 df-of 7714 df-om 7904 df-1st 8030 df-2nd 8031 df-frecs 8322 df-wrecs 8353 df-recs 8427 df-rdg 8466 df-1o 8522 df-2o 8523 df-er 8763 df-map 8886 df-pm 8887 df-en 9004 df-dom 9005 df-sdom 9006 df-fin 9007 df-sup 9511 df-inf 9512 df-oi 9579 df-dju 9970 df-card 10008 df-pnf 11326 df-mnf 11327 df-xr 11328 df-ltxr 11329 df-le 11330 df-sub 11522 df-neg 11523 df-div 11948 df-nn 12294 df-2 12356 df-3 12357 df-n0 12554 df-z 12640 df-uz 12904 df-q 13014 df-rp 13058 df-xadd 13176 df-ioo 13411 df-ico 13413 df-icc 13414 df-fz 13568 df-fzo 13712 df-fl 13843 df-seq 14053 df-exp 14113 df-hash 14380 df-cj 15148 df-re 15149 df-im 15150 df-sqrt 15284 df-abs 15285 df-clim 15534 df-rlim 15535 df-sum 15735 df-xmet 21380 df-met 21381 df-ovol 25518 df-vol 25519

This theorem is referenced by: volsup2 25659 itg1climres 25769 itg2gt0 25815

W3C validator