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 25511

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 7024	. . . . . . . . . . 11 ⊢ ((𝐹:ℕ⟶dom vol ∧ 𝑘 ∈ ℕ) → (𝐹‘𝑘) ∈ dom vol)
2	1	ad2ant2r 747	. . . . . . . . . 10 ⊢ (((𝐹:ℕ⟶dom vol ∧ ∀𝑛 ∈ ℕ (𝐹‘𝑛) ⊆ (𝐹‘(𝑛 + 1))) ∧ (𝑘 ∈ ℕ ∧ (vol‘(𝐹‘𝑘)) ∈ ℝ)) → (𝐹‘𝑘) ∈ dom vol)
3		fzofi 13895	. . . . . . . . . . 11 ⊢ (1..^𝑘) ∈ Fin
4		simpll 766	. . . . . . . . . . . . 13 ⊢ (((𝐹:ℕ⟶dom vol ∧ ∀𝑛 ∈ ℕ (𝐹‘𝑛) ⊆ (𝐹‘(𝑛 + 1))) ∧ (𝑘 ∈ ℕ ∧ (vol‘(𝐹‘𝑘)) ∈ ℝ)) → 𝐹:ℕ⟶dom vol)
5		elfzouz 13577	. . . . . . . . . . . . . 14 ⊢ (𝑚 ∈ (1..^𝑘) → 𝑚 ∈ (ℤ_≥‘1))
6		nnuz 12788	. . . . . . . . . . . . . 14 ⊢ ℕ = (ℤ_≥‘1)
7	5, 6	eleqtrrdi 2845	. . . . . . . . . . . . 13 ⊢ (𝑚 ∈ (1..^𝑘) → 𝑚 ∈ ℕ)
8		ffvelcdm 7024	. . . . . . . . . . . . 13 ⊢ ((𝐹:ℕ⟶dom vol ∧ 𝑚 ∈ ℕ) → (𝐹‘𝑚) ∈ dom vol)
9	4, 7, 8	syl2an 596	. . . . . . . . . . . 12 ⊢ ((((𝐹:ℕ⟶dom vol ∧ ∀𝑛 ∈ ℕ (𝐹‘𝑛) ⊆ (𝐹‘(𝑛 + 1))) ∧ (𝑘 ∈ ℕ ∧ (vol‘(𝐹‘𝑘)) ∈ ℝ)) ∧ 𝑚 ∈ (1..^𝑘)) → (𝐹‘𝑚) ∈ dom vol)
10	9	ralrimiva 3126	. . . . . . . . . . 11 ⊢ (((𝐹:ℕ⟶dom vol ∧ ∀𝑛 ∈ ℕ (𝐹‘𝑛) ⊆ (𝐹‘(𝑛 + 1))) ∧ (𝑘 ∈ ℕ ∧ (vol‘(𝐹‘𝑘)) ∈ ℝ)) → ∀𝑚 ∈ (1..^𝑘)(𝐹‘𝑚) ∈ dom vol)
11		finiunmbl 25499	. . . . . . . . . . 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 25498	. . . . . . . . . 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 25485	. . . . . . . . . . 11 ⊢ (((𝐹‘𝑘) ∖ ∪ 𝑚 ∈ (1..^𝑘)(𝐹‘𝑚)) ∈ dom vol → (vol‘((𝐹‘𝑘) ∖ ∪ 𝑚 ∈ (1..^𝑘)(𝐹‘𝑚))) = (vol*‘((𝐹‘𝑘) ∖ ∪ 𝑚 ∈ (1..^𝑘)(𝐹‘𝑚))))
16	14, 15	syl 17	. . . . . . . . . 10 ⊢ (((𝐹:ℕ⟶dom vol ∧ ∀𝑛 ∈ ℕ (𝐹‘𝑛) ⊆ (𝐹‘(𝑛 + 1))) ∧ (𝑘 ∈ ℕ ∧ (vol‘(𝐹‘𝑘)) ∈ ℝ)) → (vol‘((𝐹‘𝑘) ∖ ∪ 𝑚 ∈ (1..^𝑘)(𝐹‘𝑚))) = (vol*‘((𝐹‘𝑘) ∖ ∪ 𝑚 ∈ (1..^𝑘)(𝐹‘𝑚))))
17		difssd 4087	. . . . . . . . . . 11 ⊢ (((𝐹:ℕ⟶dom vol ∧ ∀𝑛 ∈ ℕ (𝐹‘𝑛) ⊆ (𝐹‘(𝑛 + 1))) ∧ (𝑘 ∈ ℕ ∧ (vol‘(𝐹‘𝑘)) ∈ ℝ)) → ((𝐹‘𝑘) ∖ ∪ 𝑚 ∈ (1..^𝑘)(𝐹‘𝑚)) ⊆ (𝐹‘𝑘))
18		mblss 25486	. . . . . . . . . . . 12 ⊢ ((𝐹‘𝑘) ∈ dom vol → (𝐹‘𝑘) ⊆ ℝ)
19	2, 18	syl 17	. . . . . . . . . . 11 ⊢ (((𝐹:ℕ⟶dom vol ∧ ∀𝑛 ∈ ℕ (𝐹‘𝑛) ⊆ (𝐹‘(𝑛 + 1))) ∧ (𝑘 ∈ ℕ ∧ (vol‘(𝐹‘𝑘)) ∈ ℝ)) → (𝐹‘𝑘) ⊆ ℝ)
20		mblvol 25485	. . . . . . . . . . . . 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 2835	. . . . . . . . . . 11 ⊢ (((𝐹:ℕ⟶dom vol ∧ ∀𝑛 ∈ ℕ (𝐹‘𝑛) ⊆ (𝐹‘(𝑛 + 1))) ∧ (𝑘 ∈ ℕ ∧ (vol‘(𝐹‘𝑘)) ∈ ℝ)) → (vol*‘(𝐹‘𝑘)) ∈ ℝ)
24		ovolsscl 25441	. . . . . . . . . . 11 ⊢ ((((𝐹‘𝑘) ∖ ∪ 𝑚 ∈ (1..^𝑘)(𝐹‘𝑚)) ⊆ (𝐹‘𝑘) ∧ (𝐹‘𝑘) ⊆ ℝ ∧ (vol‘(𝐹‘𝑘)) ∈ ℝ) → (vol‘((𝐹‘𝑘) ∖ ∪ 𝑚 ∈ (1..^𝑘)(𝐹‘𝑚))) ∈ ℝ)
25	17, 19, 23, 24	syl3anc 1373	. . . . . . . . . 10 ⊢ (((𝐹:ℕ⟶dom vol ∧ ∀𝑛 ∈ ℕ (𝐹‘𝑛) ⊆ (𝐹‘(𝑛 + 1))) ∧ (𝑘 ∈ ℕ ∧ (vol‘(𝐹‘𝑘)) ∈ ℝ)) → (vol*‘((𝐹‘𝑘) ∖ ∪ 𝑚 ∈ (1..^𝑘)(𝐹‘𝑚))) ∈ ℝ)
26	16, 25	eqeltrd 2834	. . . . . . . . 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 3146	. . . . . 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 6832	. . . . . 6 ⊢ (𝑘 = 𝑚 → (𝐹‘𝑘) = (𝐹‘𝑚))
32	31	iundisj2 25504	. . . . 5 ⊢ Disj 𝑘 ∈ ℕ ((𝐹‘𝑘) ∖ ∪ 𝑚 ∈ (1..^𝑘)(𝐹‘𝑚))
33		eqid 2734	. . . . . 6 ⊢ seq1( + , (𝑘 ∈ ℕ ↦ (vol‘((𝐹‘𝑘) ∖ ∪ 𝑚 ∈ (1..^𝑘)(𝐹‘𝑚))))) = seq1( + , (𝑘 ∈ ℕ ↦ (vol‘((𝐹‘𝑘) ∖ ∪ 𝑚 ∈ (1..^𝑘)(𝐹‘𝑚)))))
34		eqid 2734	. . . . . 6 ⊢ (𝑘 ∈ ℕ ↦ (vol‘((𝐹‘𝑘) ∖ ∪ 𝑚 ∈ (1..^𝑘)(𝐹‘𝑚)))) = (𝑘 ∈ ℕ ↦ (vol‘((𝐹‘𝑘) ∖ ∪ 𝑚 ∈ (1..^𝑘)(𝐹‘𝑚))))
35	33, 34	voliun 25509	. . . . 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 25503	. . . . . 6 ⊢ ∪ 𝑘 ∈ ℕ (𝐹‘𝑘) = ∪ 𝑘 ∈ ℕ ((𝐹‘𝑘) ∖ ∪ 𝑚 ∈ (1..^𝑘)(𝐹‘𝑚))
38		ffn 6660	. . . . . . . 8 ⊢ (𝐹:ℕ⟶dom vol → 𝐹 Fn ℕ)
39	38	ad2antrr 726	. . . . . . 7 ⊢ (((𝐹:ℕ⟶dom vol ∧ ∀𝑛 ∈ ℕ (𝐹‘𝑛) ⊆ (𝐹‘(𝑛 + 1))) ∧ ∀𝑘 ∈ ℕ (vol‘(𝐹‘𝑘)) ∈ ℝ) → 𝐹 Fn ℕ)
40		fniunfv 7191	. . . . . . 7 ⊢ (𝐹 Fn ℕ → ∪ 𝑘 ∈ ℕ (𝐹‘𝑘) = ∪ ran 𝐹)
41	39, 40	syl 17	. . . . . 6 ⊢ (((𝐹:ℕ⟶dom vol ∧ ∀𝑛 ∈ ℕ (𝐹‘𝑛) ⊆ (𝐹‘(𝑛 + 1))) ∧ ∀𝑘 ∈ ℕ (vol‘(𝐹‘𝑘)) ∈ ℝ) → ∪ 𝑘 ∈ ℕ (𝐹‘𝑘) = ∪ ran 𝐹)
42	37, 41	eqtr3id 2783	. . . . 5 ⊢ (((𝐹:ℕ⟶dom vol ∧ ∀𝑛 ∈ ℕ (𝐹‘𝑛) ⊆ (𝐹‘(𝑛 + 1))) ∧ ∀𝑘 ∈ ℕ (vol‘(𝐹‘𝑘)) ∈ ℝ) → ∪ 𝑘 ∈ ℕ ((𝐹‘𝑘) ∖ ∪ 𝑚 ∈ (1..^𝑘)(𝐹‘𝑚)) = ∪ ran 𝐹)
43	42	fveq2d 6836	. . . 4 ⊢ (((𝐹:ℕ⟶dom vol ∧ ∀𝑛 ∈ ℕ (𝐹‘𝑛) ⊆ (𝐹‘(𝑛 + 1))) ∧ ∀𝑘 ∈ ℕ (vol‘(𝐹‘𝑘)) ∈ ℝ) → (vol‘∪ 𝑘 ∈ ℕ ((𝐹‘𝑘) ∖ ∪ 𝑚 ∈ (1..^𝑘)(𝐹‘𝑚))) = (vol‘∪ ran 𝐹))
44		1z 12519	. . . . . . . . . . 11 ⊢ 1 ∈ ℤ
45		seqfn 13934	. . . . . . . . . . 11 ⊢ (1 ∈ ℤ → seq1( + , (𝑘 ∈ ℕ ↦ (vol‘((𝐹‘𝑘) ∖ ∪ 𝑚 ∈ (1..^𝑘)(𝐹‘𝑚))))) Fn (ℤ_≥‘1))
46	44, 45	ax-mp 5	. . . . . . . . . 10 ⊢ seq1( + , (𝑘 ∈ ℕ ↦ (vol‘((𝐹‘𝑘) ∖ ∪ 𝑚 ∈ (1..^𝑘)(𝐹‘𝑚))))) Fn (ℤ_≥‘1)
47	6	fneq2i 6588	. . . . . . . . . 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 25484	. . . . . . . . . 10 ⊢ vol:dom vol⟶(0[,]+∞)
51		simpll 766	. . . . . . . . . 10 ⊢ (((𝐹:ℕ⟶dom vol ∧ ∀𝑛 ∈ ℕ (𝐹‘𝑛) ⊆ (𝐹‘(𝑛 + 1))) ∧ ∀𝑘 ∈ ℕ (vol‘(𝐹‘𝑘)) ∈ ℝ) → 𝐹:ℕ⟶dom vol)
52		fco 6684	. . . . . . . . . 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 6661	. . . . . . . 8 ⊢ (((𝐹:ℕ⟶dom vol ∧ ∀𝑛 ∈ ℕ (𝐹‘𝑛) ⊆ (𝐹‘(𝑛 + 1))) ∧ ∀𝑘 ∈ ℕ (vol‘(𝐹‘𝑘)) ∈ ℝ) → (vol ∘ 𝐹) Fn ℕ)
55		fveq2 6832	. . . . . . . . . . . . 13 ⊢ (𝑥 = 1 → (seq1( + , (𝑘 ∈ ℕ ↦ (vol‘((𝐹‘𝑘) ∖ ∪ 𝑚 ∈ (1..^𝑘)(𝐹‘𝑚)))))‘𝑥) = (seq1( + , (𝑘 ∈ ℕ ↦ (vol‘((𝐹‘𝑘) ∖ ∪ 𝑚 ∈ (1..^𝑘)(𝐹‘𝑚)))))‘1))
56		2fveq3 6837	. . . . . . . . . . . . 13 ⊢ (𝑥 = 1 → (vol‘(𝐹‘𝑥)) = (vol‘(𝐹‘1)))
57	55, 56	eqeq12d 2750	. . . . . . . . . . . 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 6832	. . . . . . . . . . . . 13 ⊢ (𝑥 = 𝑗 → (seq1( + , (𝑘 ∈ ℕ ↦ (vol‘((𝐹‘𝑘) ∖ ∪ 𝑚 ∈ (1..^𝑘)(𝐹‘𝑚)))))‘𝑥) = (seq1( + , (𝑘 ∈ ℕ ↦ (vol‘((𝐹‘𝑘) ∖ ∪ 𝑚 ∈ (1..^𝑘)(𝐹‘𝑚)))))‘𝑗))
60		2fveq3 6837	. . . . . . . . . . . . 13 ⊢ (𝑥 = 𝑗 → (vol‘(𝐹‘𝑥)) = (vol‘(𝐹‘𝑗)))
61	59, 60	eqeq12d 2750	. . . . . . . . . . . 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 6832	. . . . . . . . . . . . 13 ⊢ (𝑥 = (𝑗 + 1) → (seq1( + , (𝑘 ∈ ℕ ↦ (vol‘((𝐹‘𝑘) ∖ ∪ 𝑚 ∈ (1..^𝑘)(𝐹‘𝑚)))))‘𝑥) = (seq1( + , (𝑘 ∈ ℕ ↦ (vol‘((𝐹‘𝑘) ∖ ∪ 𝑚 ∈ (1..^𝑘)(𝐹‘𝑚)))))‘(𝑗 + 1)))
64		2fveq3 6837	. . . . . . . . . . . . 13 ⊢ (𝑥 = (𝑗 + 1) → (vol‘(𝐹‘𝑥)) = (vol‘(𝐹‘(𝑗 + 1))))
65	63, 64	eqeq12d 2750	. . . . . . . . . . . 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 13935	. . . . . . . . . . . . . 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 12154	. . . . . . . . . . . . . 14 ⊢ 1 ∈ ℕ
70		oveq2 7364	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (𝑘 = 1 → (1..^𝑘) = (1..^1))
71		fzo0 13597	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (1..^1) = ∅
72	70, 71	eqtrdi 2785	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (𝑘 = 1 → (1..^𝑘) = ∅)
73	72	iuneq1d 4972	. . . . . . . . . . . . . . . . . . . 20 ⊢ (𝑘 = 1 → ∪ 𝑚 ∈ (1..^𝑘)(𝐹‘𝑚) = ∪ 𝑚 ∈ ∅ (𝐹‘𝑚))
74		0iun 5016	. . . . . . . . . . . . . . . . . . . 20 ⊢ ∪ 𝑚 ∈ ∅ (𝐹‘𝑚) = ∅
75	73, 74	eqtrdi 2785	. . . . . . . . . . . . . . . . . . 19 ⊢ (𝑘 = 1 → ∪ 𝑚 ∈ (1..^𝑘)(𝐹‘𝑚) = ∅)
76	75	difeq2d 4076	. . . . . . . . . . . . . . . . . 18 ⊢ (𝑘 = 1 → ((𝐹‘𝑘) ∖ ∪ 𝑚 ∈ (1..^𝑘)(𝐹‘𝑚)) = ((𝐹‘𝑘) ∖ ∅))
77		dif0 4328	. . . . . . . . . . . . . . . . . 18 ⊢ ((𝐹‘𝑘) ∖ ∅) = (𝐹‘𝑘)
78	76, 77	eqtrdi 2785	. . . . . . . . . . . . . . . . 17 ⊢ (𝑘 = 1 → ((𝐹‘𝑘) ∖ ∪ 𝑚 ∈ (1..^𝑘)(𝐹‘𝑚)) = (𝐹‘𝑘))
79		fveq2 6832	. . . . . . . . . . . . . . . . 17 ⊢ (𝑘 = 1 → (𝐹‘𝑘) = (𝐹‘1))
80	78, 79	eqtrd 2769	. . . . . . . . . . . . . . . 16 ⊢ (𝑘 = 1 → ((𝐹‘𝑘) ∖ ∪ 𝑚 ∈ (1..^𝑘)(𝐹‘𝑚)) = (𝐹‘1))
81	80	fveq2d 6836	. . . . . . . . . . . . . . 15 ⊢ (𝑘 = 1 → (vol‘((𝐹‘𝑘) ∖ ∪ 𝑚 ∈ (1..^𝑘)(𝐹‘𝑚))) = (vol‘(𝐹‘1)))
82		fvex 6845	. . . . . . . . . . . . . . 15 ⊢ (vol‘(𝐹‘1)) ∈ V
83	81, 34, 82	fvmpt 6939	. . . . . . . . . . . . . 14 ⊢ (1 ∈ ℕ → ((𝑘 ∈ ℕ ↦ (vol‘((𝐹‘𝑘) ∖ ∪ 𝑚 ∈ (1..^𝑘)(𝐹‘𝑚))))‘1) = (vol‘(𝐹‘1)))
84	69, 83	ax-mp 5	. . . . . . . . . . . . 13 ⊢ ((𝑘 ∈ ℕ ↦ (vol‘((𝐹‘𝑘) ∖ ∪ 𝑚 ∈ (1..^𝑘)(𝐹‘𝑚))))‘1) = (vol‘(𝐹‘1))
85	68, 84	eqtri 2757	. . . . . . . . . . . 12 ⊢ (seq1( + , (𝑘 ∈ ℕ ↦ (vol‘((𝐹‘𝑘) ∖ ∪ 𝑚 ∈ (1..^𝑘)(𝐹‘𝑚)))))‘1) = (vol‘(𝐹‘1))
86	85	a1i 11	. . . . . . . . . . 11 ⊢ (((𝐹:ℕ⟶dom vol ∧ ∀𝑛 ∈ ℕ (𝐹‘𝑛) ⊆ (𝐹‘(𝑛 + 1))) ∧ ∀𝑘 ∈ ℕ (vol‘(𝐹‘𝑘)) ∈ ℝ) → (seq1( + , (𝑘 ∈ ℕ ↦ (vol‘((𝐹‘𝑘) ∖ ∪ 𝑚 ∈ (1..^𝑘)(𝐹‘𝑚)))))‘1) = (vol‘(𝐹‘1)))
87		oveq1 7363	. . . . . . . . . . . . . 14 ⊢ ((seq1( + , (𝑘 ∈ ℕ ↦ (vol‘((𝐹‘𝑘) ∖ ∪ 𝑚 ∈ (1..^𝑘)(𝐹‘𝑚)))))‘𝑗) = (vol‘(𝐹‘𝑗)) → ((seq1( + , (𝑘 ∈ ℕ ↦ (vol‘((𝐹‘𝑘) ∖ ∪ 𝑚 ∈ (1..^𝑘)(𝐹‘𝑚)))))‘𝑗) + ((𝑘 ∈ ℕ ↦ (vol‘((𝐹‘𝑘) ∖ ∪ 𝑚 ∈ (1..^𝑘)(𝐹‘𝑚))))‘(𝑗 + 1))) = ((vol‘(𝐹‘𝑗)) + ((𝑘 ∈ ℕ ↦ (vol‘((𝐹‘𝑘) ∖ ∪ 𝑚 ∈ (1..^𝑘)(𝐹‘𝑚))))‘(𝑗 + 1))))
88		seqp1 13937	. . . . . . . . . . . . . . . . 17 ⊢ (𝑗 ∈ (ℤ_≥‘1) → (seq1( + , (𝑘 ∈ ℕ ↦ (vol‘((𝐹‘𝑘) ∖ ∪ 𝑚 ∈ (1..^𝑘)(𝐹‘𝑚)))))‘(𝑗 + 1)) = ((seq1( + , (𝑘 ∈ ℕ ↦ (vol‘((𝐹‘𝑘) ∖ ∪ 𝑚 ∈ (1..^𝑘)(𝐹‘𝑚)))))‘𝑗) + ((𝑘 ∈ ℕ ↦ (vol‘((𝐹‘𝑘) ∖ ∪ 𝑚 ∈ (1..^𝑘)(𝐹‘𝑚))))‘(𝑗 + 1))))
89	88, 6	eleq2s 2852	. . . . . . . . . . . . . . . 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 4427	. . . . . . . . . . . . . . . . . 18 ⊢ ((𝐹‘𝑗) ∪ ((𝐹‘(𝑗 + 1)) ∖ (𝐹‘𝑗))) = ((𝐹‘𝑗) ∪ (𝐹‘(𝑗 + 1)))
92		fveq2 6832	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (𝑛 = 𝑗 → (𝐹‘𝑛) = (𝐹‘𝑗))
93		fvoveq1 7379	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (𝑛 = 𝑗 → (𝐹‘(𝑛 + 1)) = (𝐹‘(𝑗 + 1)))
94	92, 93	sseq12d 3965	. . . . . . . . . . . . . . . . . . . 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 3575	. . . . . . . . . . . . . . . . . . 19 ⊢ ((((𝐹:ℕ⟶dom vol ∧ ∀𝑛 ∈ ℕ (𝐹‘𝑛) ⊆ (𝐹‘(𝑛 + 1))) ∧ ∀𝑘 ∈ ℕ (vol‘(𝐹‘𝑘)) ∈ ℝ) ∧ 𝑗 ∈ ℕ) → (𝐹‘𝑗) ⊆ (𝐹‘(𝑗 + 1)))
98		ssequn1 4136	. . . . . . . . . . . . . . . . . . 19 ⊢ ((𝐹‘𝑗) ⊆ (𝐹‘(𝑗 + 1)) ↔ ((𝐹‘𝑗) ∪ (𝐹‘(𝑗 + 1))) = (𝐹‘(𝑗 + 1)))
99	97, 98	sylib 218	. . . . . . . . . . . . . . . . . 18 ⊢ ((((𝐹:ℕ⟶dom vol ∧ ∀𝑛 ∈ ℕ (𝐹‘𝑛) ⊆ (𝐹‘(𝑛 + 1))) ∧ ∀𝑘 ∈ ℕ (vol‘(𝐹‘𝑘)) ∈ ℝ) ∧ 𝑗 ∈ ℕ) → ((𝐹‘𝑗) ∪ (𝐹‘(𝑗 + 1))) = (𝐹‘(𝑗 + 1)))
100	91, 99	eqtr2id 2782	. . . . . . . . . . . . . . . . 17 ⊢ ((((𝐹:ℕ⟶dom vol ∧ ∀𝑛 ∈ ℕ (𝐹‘𝑛) ⊆ (𝐹‘(𝑛 + 1))) ∧ ∀𝑘 ∈ ℕ (vol‘(𝐹‘𝑘)) ∈ ℝ) ∧ 𝑗 ∈ ℕ) → (𝐹‘(𝑗 + 1)) = ((𝐹‘𝑗) ∪ ((𝐹‘(𝑗 + 1)) ∖ (𝐹‘𝑗))))
101	100	fveq2d 6836	. . . . . . . . . . . . . . . 16 ⊢ ((((𝐹:ℕ⟶dom vol ∧ ∀𝑛 ∈ ℕ (𝐹‘𝑛) ⊆ (𝐹‘(𝑛 + 1))) ∧ ∀𝑘 ∈ ℕ (vol‘(𝐹‘𝑘)) ∈ ℝ) ∧ 𝑗 ∈ ℕ) → (vol‘(𝐹‘(𝑗 + 1))) = (vol‘((𝐹‘𝑗) ∪ ((𝐹‘(𝑗 + 1)) ∖ (𝐹‘𝑗)))))
102		simplll 774	. . . . . . . . . . . . . . . . . 18 ⊢ ((((𝐹:ℕ⟶dom vol ∧ ∀𝑛 ∈ ℕ (𝐹‘𝑛) ⊆ (𝐹‘(𝑛 + 1))) ∧ ∀𝑘 ∈ ℕ (vol‘(𝐹‘𝑘)) ∈ ℝ) ∧ 𝑗 ∈ ℕ) → 𝐹:ℕ⟶dom vol)
103	102, 96	ffvelcdmd 7028	. . . . . . . . . . . . . . . . 17 ⊢ ((((𝐹:ℕ⟶dom vol ∧ ∀𝑛 ∈ ℕ (𝐹‘𝑛) ⊆ (𝐹‘(𝑛 + 1))) ∧ ∀𝑘 ∈ ℕ (vol‘(𝐹‘𝑘)) ∈ ℝ) ∧ 𝑗 ∈ ℕ) → (𝐹‘𝑗) ∈ dom vol)
104		peano2nn 12155	. . . . . . . . . . . . . . . . . . . 20 ⊢ (𝑗 ∈ ℕ → (𝑗 + 1) ∈ ℕ)
105	104	adantl 481	. . . . . . . . . . . . . . . . . . 19 ⊢ ((((𝐹:ℕ⟶dom vol ∧ ∀𝑛 ∈ ℕ (𝐹‘𝑛) ⊆ (𝐹‘(𝑛 + 1))) ∧ ∀𝑘 ∈ ℕ (vol‘(𝐹‘𝑘)) ∈ ℝ) ∧ 𝑗 ∈ ℕ) → (𝑗 + 1) ∈ ℕ)
106	102, 105	ffvelcdmd 7028	. . . . . . . . . . . . . . . . . 18 ⊢ ((((𝐹:ℕ⟶dom vol ∧ ∀𝑛 ∈ ℕ (𝐹‘𝑛) ⊆ (𝐹‘(𝑛 + 1))) ∧ ∀𝑘 ∈ ℕ (vol‘(𝐹‘𝑘)) ∈ ℝ) ∧ 𝑗 ∈ ℕ) → (𝐹‘(𝑗 + 1)) ∈ dom vol)
107		difmbl 25498	. . . . . . . . . . . . . . . . . 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 4422	. . . . . . . . . . . . . . . . . 18 ⊢ ((𝐹‘𝑗) ∩ ((𝐹‘(𝑗 + 1)) ∖ (𝐹‘𝑗))) = ∅
110	109	a1i 11	. . . . . . . . . . . . . . . . 17 ⊢ ((((𝐹:ℕ⟶dom vol ∧ ∀𝑛 ∈ ℕ (𝐹‘𝑛) ⊆ (𝐹‘(𝑛 + 1))) ∧ ∀𝑘 ∈ ℕ (vol‘(𝐹‘𝑘)) ∈ ℝ) ∧ 𝑗 ∈ ℕ) → ((𝐹‘𝑗) ∩ ((𝐹‘(𝑗 + 1)) ∖ (𝐹‘𝑗))) = ∅)
111		2fveq3 6837	. . . . . . . . . . . . . . . . . . 19 ⊢ (𝑘 = 𝑗 → (vol‘(𝐹‘𝑘)) = (vol‘(𝐹‘𝑗)))
112	111	eleq1d 2819	. . . . . . . . . . . . . . . . . 18 ⊢ (𝑘 = 𝑗 → ((vol‘(𝐹‘𝑘)) ∈ ℝ ↔ (vol‘(𝐹‘𝑗)) ∈ ℝ))
113		simplr 768	. . . . . . . . . . . . . . . . . 18 ⊢ ((((𝐹:ℕ⟶dom vol ∧ ∀𝑛 ∈ ℕ (𝐹‘𝑛) ⊆ (𝐹‘(𝑛 + 1))) ∧ ∀𝑘 ∈ ℕ (vol‘(𝐹‘𝑘)) ∈ ℝ) ∧ 𝑗 ∈ ℕ) → ∀𝑘 ∈ ℕ (vol‘(𝐹‘𝑘)) ∈ ℝ)
114	112, 113, 96	rspcdva 3575	. . . . . . . . . . . . . . . . 17 ⊢ ((((𝐹:ℕ⟶dom vol ∧ ∀𝑛 ∈ ℕ (𝐹‘𝑛) ⊆ (𝐹‘(𝑛 + 1))) ∧ ∀𝑘 ∈ ℕ (vol‘(𝐹‘𝑘)) ∈ ℝ) ∧ 𝑗 ∈ ℕ) → (vol‘(𝐹‘𝑗)) ∈ ℝ)
115		mblvol 25485	. . . . . . . . . . . . . . . . . . 19 ⊢ (((𝐹‘(𝑗 + 1)) ∖ (𝐹‘𝑗)) ∈ dom vol → (vol‘((𝐹‘(𝑗 + 1)) ∖ (𝐹‘𝑗))) = (vol*‘((𝐹‘(𝑗 + 1)) ∖ (𝐹‘𝑗))))
116	108, 115	syl 17	. . . . . . . . . . . . . . . . . 18 ⊢ ((((𝐹:ℕ⟶dom vol ∧ ∀𝑛 ∈ ℕ (𝐹‘𝑛) ⊆ (𝐹‘(𝑛 + 1))) ∧ ∀𝑘 ∈ ℕ (vol‘(𝐹‘𝑘)) ∈ ℝ) ∧ 𝑗 ∈ ℕ) → (vol‘((𝐹‘(𝑗 + 1)) ∖ (𝐹‘𝑗))) = (vol*‘((𝐹‘(𝑗 + 1)) ∖ (𝐹‘𝑗))))
117		difssd 4087	. . . . . . . . . . . . . . . . . . 19 ⊢ ((((𝐹:ℕ⟶dom vol ∧ ∀𝑛 ∈ ℕ (𝐹‘𝑛) ⊆ (𝐹‘(𝑛 + 1))) ∧ ∀𝑘 ∈ ℕ (vol‘(𝐹‘𝑘)) ∈ ℝ) ∧ 𝑗 ∈ ℕ) → ((𝐹‘(𝑗 + 1)) ∖ (𝐹‘𝑗)) ⊆ (𝐹‘(𝑗 + 1)))
118		mblss 25486	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((𝐹‘(𝑗 + 1)) ∈ dom vol → (𝐹‘(𝑗 + 1)) ⊆ ℝ)
119	106, 118	syl 17	. . . . . . . . . . . . . . . . . . 19 ⊢ ((((𝐹:ℕ⟶dom vol ∧ ∀𝑛 ∈ ℕ (𝐹‘𝑛) ⊆ (𝐹‘(𝑛 + 1))) ∧ ∀𝑘 ∈ ℕ (vol‘(𝐹‘𝑘)) ∈ ℝ) ∧ 𝑗 ∈ ℕ) → (𝐹‘(𝑗 + 1)) ⊆ ℝ)
120		mblvol 25485	. . . . . . . . . . . . . . . . . . . . 21 ⊢ ((𝐹‘(𝑗 + 1)) ∈ dom vol → (vol‘(𝐹‘(𝑗 + 1))) = (vol*‘(𝐹‘(𝑗 + 1))))
121	106, 120	syl 17	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((((𝐹:ℕ⟶dom vol ∧ ∀𝑛 ∈ ℕ (𝐹‘𝑛) ⊆ (𝐹‘(𝑛 + 1))) ∧ ∀𝑘 ∈ ℕ (vol‘(𝐹‘𝑘)) ∈ ℝ) ∧ 𝑗 ∈ ℕ) → (vol‘(𝐹‘(𝑗 + 1))) = (vol*‘(𝐹‘(𝑗 + 1))))
122		2fveq3 6837	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (𝑘 = (𝑗 + 1) → (vol‘(𝐹‘𝑘)) = (vol‘(𝐹‘(𝑗 + 1))))
123	122	eleq1d 2819	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (𝑘 = (𝑗 + 1) → ((vol‘(𝐹‘𝑘)) ∈ ℝ ↔ (vol‘(𝐹‘(𝑗 + 1))) ∈ ℝ))
124	123, 113, 105	rspcdva 3575	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((((𝐹:ℕ⟶dom vol ∧ ∀𝑛 ∈ ℕ (𝐹‘𝑛) ⊆ (𝐹‘(𝑛 + 1))) ∧ ∀𝑘 ∈ ℕ (vol‘(𝐹‘𝑘)) ∈ ℝ) ∧ 𝑗 ∈ ℕ) → (vol‘(𝐹‘(𝑗 + 1))) ∈ ℝ)
125	121, 124	eqeltrrd 2835	. . . . . . . . . . . . . . . . . . 19 ⊢ ((((𝐹:ℕ⟶dom vol ∧ ∀𝑛 ∈ ℕ (𝐹‘𝑛) ⊆ (𝐹‘(𝑛 + 1))) ∧ ∀𝑘 ∈ ℕ (vol‘(𝐹‘𝑘)) ∈ ℝ) ∧ 𝑗 ∈ ℕ) → (vol*‘(𝐹‘(𝑗 + 1))) ∈ ℝ)
126		ovolsscl 25441	. . . . . . . . . . . . . . . . . . 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 2834	. . . . . . . . . . . . . . . . 17 ⊢ ((((𝐹:ℕ⟶dom vol ∧ ∀𝑛 ∈ ℕ (𝐹‘𝑛) ⊆ (𝐹‘(𝑛 + 1))) ∧ ∀𝑘 ∈ ℕ (vol‘(𝐹‘𝑘)) ∈ ℝ) ∧ 𝑗 ∈ ℕ) → (vol‘((𝐹‘(𝑗 + 1)) ∖ (𝐹‘𝑗))) ∈ ℝ)
129		volun 25500	. . . . . . . . . . . . . . . . 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 13467	. . . . . . . . . . . . . . . . . . . . . . . . . 26 ⊢ (𝑚 ∈ (1...𝑗) → 𝑚 ∈ ℕ)
133	132	adantl 481	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ (((((𝐹:ℕ⟶dom vol ∧ ∀𝑛 ∈ ℕ (𝐹‘𝑛) ⊆ (𝐹‘(𝑛 + 1))) ∧ ∀𝑘 ∈ ℕ (vol‘(𝐹‘𝑘)) ∈ ℝ) ∧ 𝑗 ∈ ℕ) ∧ 𝑚 ∈ (1...𝑗)) → 𝑚 ∈ ℕ)
134		elfzuz3 13435	. . . . . . . . . . . . . . . . . . . . . . . . . 26 ⊢ (𝑚 ∈ (1...𝑗) → 𝑗 ∈ (ℤ_≥‘𝑚))
135	134	adantl 481	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ (((((𝐹:ℕ⟶dom vol ∧ ∀𝑛 ∈ ℕ (𝐹‘𝑛) ⊆ (𝐹‘(𝑛 + 1))) ∧ ∀𝑘 ∈ ℕ (vol‘(𝐹‘𝑘)) ∈ ℝ) ∧ 𝑗 ∈ ℕ) ∧ 𝑚 ∈ (1...𝑗)) → 𝑗 ∈ (ℤ_≥‘𝑚))
136		volsuplem 25510	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ ((∀𝑛 ∈ ℕ (𝐹‘𝑛) ⊆ (𝐹‘(𝑛 + 1)) ∧ (𝑚 ∈ ℕ ∧ 𝑗 ∈ (ℤ_≥‘𝑚))) → (𝐹‘𝑚) ⊆ (𝐹‘𝑗))
137	131, 133, 135, 136	syl12anc 836	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ (((((𝐹:ℕ⟶dom vol ∧ ∀𝑛 ∈ ℕ (𝐹‘𝑛) ⊆ (𝐹‘(𝑛 + 1))) ∧ ∀𝑘 ∈ ℕ (vol‘(𝐹‘𝑘)) ∈ ℝ) ∧ 𝑗 ∈ ℕ) ∧ 𝑚 ∈ (1...𝑗)) → (𝐹‘𝑚) ⊆ (𝐹‘𝑗))
138	137	ralrimiva 3126	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ ((((𝐹:ℕ⟶dom vol ∧ ∀𝑛 ∈ ℕ (𝐹‘𝑛) ⊆ (𝐹‘(𝑛 + 1))) ∧ ∀𝑘 ∈ ℕ (vol‘(𝐹‘𝑘)) ∈ ℝ) ∧ 𝑗 ∈ ℕ) → ∀𝑚 ∈ (1...𝑗)(𝐹‘𝑚) ⊆ (𝐹‘𝑗))
139		iunss 4998	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ (∪ 𝑚 ∈ (1...𝑗)(𝐹‘𝑚) ⊆ (𝐹‘𝑗) ↔ ∀𝑚 ∈ (1...𝑗)(𝐹‘𝑚) ⊆ (𝐹‘𝑗))
140	138, 139	sylibr 234	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ ((((𝐹:ℕ⟶dom vol ∧ ∀𝑛 ∈ ℕ (𝐹‘𝑛) ⊆ (𝐹‘(𝑛 + 1))) ∧ ∀𝑘 ∈ ℕ (vol‘(𝐹‘𝑘)) ∈ ℝ) ∧ 𝑗 ∈ ℕ) → ∪ 𝑚 ∈ (1...𝑗)(𝐹‘𝑚) ⊆ (𝐹‘𝑗))
141	96, 6	eleqtrdi 2844	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ ((((𝐹:ℕ⟶dom vol ∧ ∀𝑛 ∈ ℕ (𝐹‘𝑛) ⊆ (𝐹‘(𝑛 + 1))) ∧ ∀𝑘 ∈ ℕ (vol‘(𝐹‘𝑘)) ∈ ℝ) ∧ 𝑗 ∈ ℕ) → 𝑗 ∈ (ℤ_≥‘1))
142		eluzfz2 13446	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ (𝑗 ∈ (ℤ_≥‘1) → 𝑗 ∈ (1...𝑗))
143	141, 142	syl 17	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ ((((𝐹:ℕ⟶dom vol ∧ ∀𝑛 ∈ ℕ (𝐹‘𝑛) ⊆ (𝐹‘(𝑛 + 1))) ∧ ∀𝑘 ∈ ℕ (vol‘(𝐹‘𝑘)) ∈ ℝ) ∧ 𝑗 ∈ ℕ) → 𝑗 ∈ (1...𝑗))
144		fveq2 6832	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ (𝑚 = 𝑗 → (𝐹‘𝑚) = (𝐹‘𝑗))
145	144	ssiun2s 5002	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ (𝑗 ∈ (1...𝑗) → (𝐹‘𝑗) ⊆ ∪ 𝑚 ∈ (1...𝑗)(𝐹‘𝑚))
146	143, 145	syl 17	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ ((((𝐹:ℕ⟶dom vol ∧ ∀𝑛 ∈ ℕ (𝐹‘𝑛) ⊆ (𝐹‘(𝑛 + 1))) ∧ ∀𝑘 ∈ ℕ (vol‘(𝐹‘𝑘)) ∈ ℝ) ∧ 𝑗 ∈ ℕ) → (𝐹‘𝑗) ⊆ ∪ 𝑚 ∈ (1...𝑗)(𝐹‘𝑚))
147	140, 146	eqssd 3949	. . . . . . . . . . . . . . . . . . . . 21 ⊢ ((((𝐹:ℕ⟶dom vol ∧ ∀𝑛 ∈ ℕ (𝐹‘𝑛) ⊆ (𝐹‘(𝑛 + 1))) ∧ ∀𝑘 ∈ ℕ (vol‘(𝐹‘𝑘)) ∈ ℝ) ∧ 𝑗 ∈ ℕ) → ∪ 𝑚 ∈ (1...𝑗)(𝐹‘𝑚) = (𝐹‘𝑗))
148	96	nnzd 12512	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ ((((𝐹:ℕ⟶dom vol ∧ ∀𝑛 ∈ ℕ (𝐹‘𝑛) ⊆ (𝐹‘(𝑛 + 1))) ∧ ∀𝑘 ∈ ℕ (vol‘(𝐹‘𝑘)) ∈ ℝ) ∧ 𝑗 ∈ ℕ) → 𝑗 ∈ ℤ)
149		fzval3 13648	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ (𝑗 ∈ ℤ → (1...𝑗) = (1..^(𝑗 + 1)))
150	148, 149	syl 17	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ ((((𝐹:ℕ⟶dom vol ∧ ∀𝑛 ∈ ℕ (𝐹‘𝑛) ⊆ (𝐹‘(𝑛 + 1))) ∧ ∀𝑘 ∈ ℕ (vol‘(𝐹‘𝑘)) ∈ ℝ) ∧ 𝑗 ∈ ℕ) → (1...𝑗) = (1..^(𝑗 + 1)))
151	150	iuneq1d 4972	. . . . . . . . . . . . . . . . . . . . 21 ⊢ ((((𝐹:ℕ⟶dom vol ∧ ∀𝑛 ∈ ℕ (𝐹‘𝑛) ⊆ (𝐹‘(𝑛 + 1))) ∧ ∀𝑘 ∈ ℕ (vol‘(𝐹‘𝑘)) ∈ ℝ) ∧ 𝑗 ∈ ℕ) → ∪ 𝑚 ∈ (1...𝑗)(𝐹‘𝑚) = ∪ 𝑚 ∈ (1..^(𝑗 + 1))(𝐹‘𝑚))
152	147, 151	eqtr3d 2771	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((((𝐹:ℕ⟶dom vol ∧ ∀𝑛 ∈ ℕ (𝐹‘𝑛) ⊆ (𝐹‘(𝑛 + 1))) ∧ ∀𝑘 ∈ ℕ (vol‘(𝐹‘𝑘)) ∈ ℝ) ∧ 𝑗 ∈ ℕ) → (𝐹‘𝑗) = ∪ 𝑚 ∈ (1..^(𝑗 + 1))(𝐹‘𝑚))
153	152	difeq2d 4076	. . . . . . . . . . . . . . . . . . 19 ⊢ ((((𝐹:ℕ⟶dom vol ∧ ∀𝑛 ∈ ℕ (𝐹‘𝑛) ⊆ (𝐹‘(𝑛 + 1))) ∧ ∀𝑘 ∈ ℕ (vol‘(𝐹‘𝑘)) ∈ ℝ) ∧ 𝑗 ∈ ℕ) → ((𝐹‘(𝑗 + 1)) ∖ (𝐹‘𝑗)) = ((𝐹‘(𝑗 + 1)) ∖ ∪ 𝑚 ∈ (1..^(𝑗 + 1))(𝐹‘𝑚)))
154	153	fveq2d 6836	. . . . . . . . . . . . . . . . . 18 ⊢ ((((𝐹:ℕ⟶dom vol ∧ ∀𝑛 ∈ ℕ (𝐹‘𝑛) ⊆ (𝐹‘(𝑛 + 1))) ∧ ∀𝑘 ∈ ℕ (vol‘(𝐹‘𝑘)) ∈ ℝ) ∧ 𝑗 ∈ ℕ) → (vol‘((𝐹‘(𝑗 + 1)) ∖ (𝐹‘𝑗))) = (vol‘((𝐹‘(𝑗 + 1)) ∖ ∪ 𝑚 ∈ (1..^(𝑗 + 1))(𝐹‘𝑚))))
155		fveq2 6832	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (𝑘 = (𝑗 + 1) → (𝐹‘𝑘) = (𝐹‘(𝑗 + 1)))
156		oveq2 7364	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ (𝑘 = (𝑗 + 1) → (1..^𝑘) = (1..^(𝑗 + 1)))
157	156	iuneq1d 4972	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (𝑘 = (𝑗 + 1) → ∪ 𝑚 ∈ (1..^𝑘)(𝐹‘𝑚) = ∪ 𝑚 ∈ (1..^(𝑗 + 1))(𝐹‘𝑚))
158	155, 157	difeq12d 4077	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (𝑘 = (𝑗 + 1) → ((𝐹‘𝑘) ∖ ∪ 𝑚 ∈ (1..^𝑘)(𝐹‘𝑚)) = ((𝐹‘(𝑗 + 1)) ∖ ∪ 𝑚 ∈ (1..^(𝑗 + 1))(𝐹‘𝑚)))
159	158	fveq2d 6836	. . . . . . . . . . . . . . . . . . . 20 ⊢ (𝑘 = (𝑗 + 1) → (vol‘((𝐹‘𝑘) ∖ ∪ 𝑚 ∈ (1..^𝑘)(𝐹‘𝑚))) = (vol‘((𝐹‘(𝑗 + 1)) ∖ ∪ 𝑚 ∈ (1..^(𝑗 + 1))(𝐹‘𝑚))))
160		fvex 6845	. . . . . . . . . . . . . . . . . . . 20 ⊢ (vol‘((𝐹‘(𝑗 + 1)) ∖ ∪ 𝑚 ∈ (1..^(𝑗 + 1))(𝐹‘𝑚))) ∈ V
161	159, 34, 160	fvmpt 6939	. . . . . . . . . . . . . . . . . . 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 2772	. . . . . . . . . . . . . . . . 17 ⊢ ((((𝐹:ℕ⟶dom vol ∧ ∀𝑛 ∈ ℕ (𝐹‘𝑛) ⊆ (𝐹‘(𝑛 + 1))) ∧ ∀𝑘 ∈ ℕ (vol‘(𝐹‘𝑘)) ∈ ℝ) ∧ 𝑗 ∈ ℕ) → (vol‘((𝐹‘(𝑗 + 1)) ∖ (𝐹‘𝑗))) = ((𝑘 ∈ ℕ ↦ (vol‘((𝐹‘𝑘) ∖ ∪ 𝑚 ∈ (1..^𝑘)(𝐹‘𝑚))))‘(𝑗 + 1)))
164	163	oveq2d 7372	. . . . . . . . . . . . . . . 16 ⊢ ((((𝐹:ℕ⟶dom vol ∧ ∀𝑛 ∈ ℕ (𝐹‘𝑛) ⊆ (𝐹‘(𝑛 + 1))) ∧ ∀𝑘 ∈ ℕ (vol‘(𝐹‘𝑘)) ∈ ℝ) ∧ 𝑗 ∈ ℕ) → ((vol‘(𝐹‘𝑗)) + (vol‘((𝐹‘(𝑗 + 1)) ∖ (𝐹‘𝑗)))) = ((vol‘(𝐹‘𝑗)) + ((𝑘 ∈ ℕ ↦ (vol‘((𝐹‘𝑘) ∖ ∪ 𝑚 ∈ (1..^𝑘)(𝐹‘𝑚))))‘(𝑗 + 1))))
165	101, 130, 164	3eqtrd 2773	. . . . . . . . . . . . . . 15 ⊢ ((((𝐹:ℕ⟶dom vol ∧ ∀𝑛 ∈ ℕ (𝐹‘𝑛) ⊆ (𝐹‘(𝑛 + 1))) ∧ ∀𝑘 ∈ ℕ (vol‘(𝐹‘𝑘)) ∈ ℝ) ∧ 𝑗 ∈ ℕ) → (vol‘(𝐹‘(𝑗 + 1))) = ((vol‘(𝐹‘𝑗)) + ((𝑘 ∈ ℕ ↦ (vol‘((𝐹‘𝑘) ∖ ∪ 𝑚 ∈ (1..^𝑘)(𝐹‘𝑚))))‘(𝑗 + 1))))
166	90, 165	eqeq12d 2750	. . . . . . . . . . . . . 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 12161	. . . . . . . . . 10 ⊢ (𝑗 ∈ ℕ → (((𝐹:ℕ⟶dom vol ∧ ∀𝑛 ∈ ℕ (𝐹‘𝑛) ⊆ (𝐹‘(𝑛 + 1))) ∧ ∀𝑘 ∈ ℕ (vol‘(𝐹‘𝑘)) ∈ ℝ) → (seq1( + , (𝑘 ∈ ℕ ↦ (vol‘((𝐹‘𝑘) ∖ ∪ 𝑚 ∈ (1..^𝑘)(𝐹‘𝑚)))))‘𝑗) = (vol‘(𝐹‘𝑗))))
171	170	impcom 407	. . . . . . . . 9 ⊢ ((((𝐹:ℕ⟶dom vol ∧ ∀𝑛 ∈ ℕ (𝐹‘𝑛) ⊆ (𝐹‘(𝑛 + 1))) ∧ ∀𝑘 ∈ ℕ (vol‘(𝐹‘𝑘)) ∈ ℝ) ∧ 𝑗 ∈ ℕ) → (seq1( + , (𝑘 ∈ ℕ ↦ (vol‘((𝐹‘𝑘) ∖ ∪ 𝑚 ∈ (1..^𝑘)(𝐹‘𝑚)))))‘𝑗) = (vol‘(𝐹‘𝑗)))
172		fvco3 6931	. . . . . . . . . 10 ⊢ ((𝐹:ℕ⟶dom vol ∧ 𝑗 ∈ ℕ) → ((vol ∘ 𝐹)‘𝑗) = (vol‘(𝐹‘𝑗)))
173	51, 172	sylan 580	. . . . . . . . 9 ⊢ ((((𝐹:ℕ⟶dom vol ∧ ∀𝑛 ∈ ℕ (𝐹‘𝑛) ⊆ (𝐹‘(𝑛 + 1))) ∧ ∀𝑘 ∈ ℕ (vol‘(𝐹‘𝑘)) ∈ ℝ) ∧ 𝑗 ∈ ℕ) → ((vol ∘ 𝐹)‘𝑗) = (vol‘(𝐹‘𝑗)))
174	171, 173	eqtr4d 2772	. . . . . . . 8 ⊢ ((((𝐹:ℕ⟶dom vol ∧ ∀𝑛 ∈ ℕ (𝐹‘𝑛) ⊆ (𝐹‘(𝑛 + 1))) ∧ ∀𝑘 ∈ ℕ (vol‘(𝐹‘𝑘)) ∈ ℝ) ∧ 𝑗 ∈ ℕ) → (seq1( + , (𝑘 ∈ ℕ ↦ (vol‘((𝐹‘𝑘) ∖ ∪ 𝑚 ∈ (1..^𝑘)(𝐹‘𝑚)))))‘𝑗) = ((vol ∘ 𝐹)‘𝑗))
175	49, 54, 174	eqfnfvd 6977	. . . . . . 7 ⊢ (((𝐹:ℕ⟶dom vol ∧ ∀𝑛 ∈ ℕ (𝐹‘𝑛) ⊆ (𝐹‘(𝑛 + 1))) ∧ ∀𝑘 ∈ ℕ (vol‘(𝐹‘𝑘)) ∈ ℝ) → seq1( + , (𝑘 ∈ ℕ ↦ (vol‘((𝐹‘𝑘) ∖ ∪ 𝑚 ∈ (1..^𝑘)(𝐹‘𝑚))))) = (vol ∘ 𝐹))
176	175	rneqd 5885	. . . . . 6 ⊢ (((𝐹:ℕ⟶dom vol ∧ ∀𝑛 ∈ ℕ (𝐹‘𝑛) ⊆ (𝐹‘(𝑛 + 1))) ∧ ∀𝑘 ∈ ℕ (vol‘(𝐹‘𝑘)) ∈ ℝ) → ran seq1( + , (𝑘 ∈ ℕ ↦ (vol‘((𝐹‘𝑘) ∖ ∪ 𝑚 ∈ (1..^𝑘)(𝐹‘𝑚))))) = ran (vol ∘ 𝐹))
177		rnco2 6210	. . . . . 6 ⊢ ran (vol ∘ 𝐹) = (vol “ ran 𝐹)
178	176, 177	eqtrdi 2785	. . . . 5 ⊢ (((𝐹:ℕ⟶dom vol ∧ ∀𝑛 ∈ ℕ (𝐹‘𝑛) ⊆ (𝐹‘(𝑛 + 1))) ∧ ∀𝑘 ∈ ℕ (vol‘(𝐹‘𝑘)) ∈ ℝ) → ran seq1( + , (𝑘 ∈ ℕ ↦ (vol‘((𝐹‘𝑘) ∖ ∪ 𝑚 ∈ (1..^𝑘)(𝐹‘𝑚))))) = (vol “ ran 𝐹))
179	178	supeq1d 9347	. . . 4 ⊢ (((𝐹:ℕ⟶dom vol ∧ ∀𝑛 ∈ ℕ (𝐹‘𝑛) ⊆ (𝐹‘(𝑛 + 1))) ∧ ∀𝑘 ∈ ℕ (vol‘(𝐹‘𝑘)) ∈ ℝ) → sup(ran seq1( + , (𝑘 ∈ ℕ ↦ (vol‘((𝐹‘𝑘) ∖ ∪ 𝑚 ∈ (1..^𝑘)(𝐹‘𝑚))))), ℝ^, < ) = sup((vol “ ran 𝐹), ℝ^, < ))
180	36, 43, 179	3eqtr3d 2777	. . 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 3086	. . 3 ⊢ (∃𝑘 ∈ ℕ ¬ (vol‘(𝐹‘𝑘)) ∈ ℝ ↔ ¬ ∀𝑘 ∈ ℕ (vol‘(𝐹‘𝑘)) ∈ ℝ)
183		fniunfv 7191	. . . . . . . . . . . 12 ⊢ (𝐹 Fn ℕ → ∪ 𝑛 ∈ ℕ (𝐹‘𝑛) = ∪ ran 𝐹)
184	38, 183	syl 17	. . . . . . . . . . 11 ⊢ (𝐹:ℕ⟶dom vol → ∪ 𝑛 ∈ ℕ (𝐹‘𝑛) = ∪ ran 𝐹)
185		ffvelcdm 7024	. . . . . . . . . . . . 13 ⊢ ((𝐹:ℕ⟶dom vol ∧ 𝑛 ∈ ℕ) → (𝐹‘𝑛) ∈ dom vol)
186	185	ralrimiva 3126	. . . . . . . . . . . 12 ⊢ (𝐹:ℕ⟶dom vol → ∀𝑛 ∈ ℕ (𝐹‘𝑛) ∈ dom vol)
187		iunmbl 25508	. . . . . . . . . . . 12 ⊢ (∀𝑛 ∈ ℕ (𝐹‘𝑛) ∈ dom vol → ∪ 𝑛 ∈ ℕ (𝐹‘𝑛) ∈ dom vol)
188	186, 187	syl 17	. . . . . . . . . . 11 ⊢ (𝐹:ℕ⟶dom vol → ∪ 𝑛 ∈ ℕ (𝐹‘𝑛) ∈ dom vol)
189	184, 188	eqeltrrd 2835	. . . . . . . . . 10 ⊢ (𝐹:ℕ⟶dom vol → ∪ ran 𝐹 ∈ dom vol)
190	189	ad2antrr 726	. . . . . . . . 9 ⊢ (((𝐹:ℕ⟶dom vol ∧ ∀𝑛 ∈ ℕ (𝐹‘𝑛) ⊆ (𝐹‘(𝑛 + 1))) ∧ (𝑘 ∈ ℕ ∧ ¬ (vol‘(𝐹‘𝑘)) ∈ ℝ)) → ∪ ran 𝐹 ∈ dom vol)
191		mblss 25486	. . . . . . . . 9 ⊢ (∪ ran 𝐹 ∈ dom vol → ∪ ran 𝐹 ⊆ ℝ)
192	190, 191	syl 17	. . . . . . . 8 ⊢ (((𝐹:ℕ⟶dom vol ∧ ∀𝑛 ∈ ℕ (𝐹‘𝑛) ⊆ (𝐹‘(𝑛 + 1))) ∧ (𝑘 ∈ ℕ ∧ ¬ (vol‘(𝐹‘𝑘)) ∈ ℝ)) → ∪ ran 𝐹 ⊆ ℝ)
193		ovolcl 25433	. . . . . . . 8 ⊢ (∪ ran 𝐹 ⊆ ℝ → (vol‘∪ ran 𝐹) ∈ ℝ^)
194	192, 193	syl 17	. . . . . . 7 ⊢ (((𝐹:ℕ⟶dom vol ∧ ∀𝑛 ∈ ℕ (𝐹‘𝑛) ⊆ (𝐹‘(𝑛 + 1))) ∧ (𝑘 ∈ ℕ ∧ ¬ (vol‘(𝐹‘𝑘)) ∈ ℝ)) → (vol‘∪ ran 𝐹) ∈ ℝ^)
195		pnfge 13042	. . . . . . 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 25433	. . . . . . . . . . . 12 ⊢ ((𝐹‘𝑘) ⊆ ℝ → (vol‘(𝐹‘𝑘)) ∈ ℝ^)
201	199, 200	syl 17	. . . . . . . . . . 11 ⊢ (((𝐹:ℕ⟶dom vol ∧ ∀𝑛 ∈ ℕ (𝐹‘𝑛) ⊆ (𝐹‘(𝑛 + 1))) ∧ (𝑘 ∈ ℕ ∧ ¬ (vol‘(𝐹‘𝑘)) ∈ ℝ)) → (vol‘(𝐹‘𝑘)) ∈ ℝ^)
202		xrrebnd 13081	. . . . . . . . . . 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 2819	. . . . . . . . . 10 ⊢ (((𝐹:ℕ⟶dom vol ∧ ∀𝑛 ∈ ℕ (𝐹‘𝑛) ⊆ (𝐹‘(𝑛 + 1))) ∧ (𝑘 ∈ ℕ ∧ ¬ (vol‘(𝐹‘𝑘)) ∈ ℝ)) → ((vol‘(𝐹‘𝑘)) ∈ ℝ ↔ (vol*‘(𝐹‘𝑘)) ∈ ℝ))
206		ovolge0 25436	. . . . . . . . . . . . 13 ⊢ ((𝐹‘𝑘) ⊆ ℝ → 0 ≤ (vol*‘(𝐹‘𝑘)))
207		mnflt0 13037	. . . . . . . . . . . . . 14 ⊢ -∞ < 0
208		mnfxr 11187	. . . . . . . . . . . . . . 15 ⊢ -∞ ∈ ℝ^*
209		0xr 11177	. . . . . . . . . . . . . . 15 ⊢ 0 ∈ ℝ^*
210		xrltletr 13069	. . . . . . . . . . . . . . 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 13077	. . . . . . . . 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 7023	. . . . . . . . . 10 ⊢ ((𝐹 Fn ℕ ∧ 𝑘 ∈ ℕ) → (𝐹‘𝑘) ∈ ran 𝐹)
224	221, 222, 223	syl2anc 584	. . . . . . . . 9 ⊢ (((𝐹:ℕ⟶dom vol ∧ ∀𝑛 ∈ ℕ (𝐹‘𝑛) ⊆ (𝐹‘(𝑛 + 1))) ∧ (𝑘 ∈ ℕ ∧ ¬ (vol‘(𝐹‘𝑘)) ∈ ℝ)) → (𝐹‘𝑘) ∈ ran 𝐹)
225		elssuni 4892	. . . . . . . . 9 ⊢ ((𝐹‘𝑘) ∈ ran 𝐹 → (𝐹‘𝑘) ⊆ ∪ ran 𝐹)
226	224, 225	syl 17	. . . . . . . 8 ⊢ (((𝐹:ℕ⟶dom vol ∧ ∀𝑛 ∈ ℕ (𝐹‘𝑛) ⊆ (𝐹‘(𝑛 + 1))) ∧ (𝑘 ∈ ℕ ∧ ¬ (vol‘(𝐹‘𝑘)) ∈ ℝ)) → (𝐹‘𝑘) ⊆ ∪ ran 𝐹)
227		ovolss 25440	. . . . . . . 8 ⊢ (((𝐹‘𝑘) ⊆ ∪ ran 𝐹 ∧ ∪ ran 𝐹 ⊆ ℝ) → (vol‘(𝐹‘𝑘)) ≤ (vol‘∪ ran 𝐹))
228	226, 192, 227	syl2anc 584	. . . . . . 7 ⊢ (((𝐹:ℕ⟶dom vol ∧ ∀𝑛 ∈ ℕ (𝐹‘𝑛) ⊆ (𝐹‘(𝑛 + 1))) ∧ (𝑘 ∈ ℕ ∧ ¬ (vol‘(𝐹‘𝑘)) ∈ ℝ)) → (vol‘(𝐹‘𝑘)) ≤ (vol‘∪ ran 𝐹))
229	220, 228	eqbrtrrd 5120	. . . . . 6 ⊢ (((𝐹:ℕ⟶dom vol ∧ ∀𝑛 ∈ ℕ (𝐹‘𝑛) ⊆ (𝐹‘(𝑛 + 1))) ∧ (𝑘 ∈ ℕ ∧ ¬ (vol‘(𝐹‘𝑘)) ∈ ℝ)) → +∞ ≤ (vol*‘∪ ran 𝐹))
230		pnfxr 11184	. . . . . . 7 ⊢ +∞ ∈ ℝ^*
231		xrletri3 13066	. . . . . . 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 25485	. . . . . 6 ⊢ (∪ ran 𝐹 ∈ dom vol → (vol‘∪ ran 𝐹) = (vol*‘∪ ran 𝐹))
235	190, 234	syl 17	. . . . 5 ⊢ (((𝐹:ℕ⟶dom vol ∧ ∀𝑛 ∈ ℕ (𝐹‘𝑛) ⊆ (𝐹‘(𝑛 + 1))) ∧ (𝑘 ∈ ℕ ∧ ¬ (vol‘(𝐹‘𝑘)) ∈ ℝ)) → (vol‘∪ ran 𝐹) = (vol*‘∪ ran 𝐹))
236		imassrn 6028	. . . . . . 7 ⊢ (vol “ ran 𝐹) ⊆ ran vol
237		frn 6667	. . . . . . . . 9 ⊢ (vol:dom vol⟶(0[,]+∞) → ran vol ⊆ (0[,]+∞))
238	50, 237	ax-mp 5	. . . . . . . 8 ⊢ ran vol ⊆ (0[,]+∞)
239		iccssxr 13344	. . . . . . . 8 ⊢ (0[,]+∞) ⊆ ℝ^*
240	238, 239	sstri 3941	. . . . . . 7 ⊢ ran vol ⊆ ℝ^*
241	236, 240	sstri 3941	. . . . . 6 ⊢ (vol “ ran 𝐹) ⊆ ℝ^*
242	204, 220	eqtrd 2769	. . . . . . 7 ⊢ (((𝐹:ℕ⟶dom vol ∧ ∀𝑛 ∈ ℕ (𝐹‘𝑛) ⊆ (𝐹‘(𝑛 + 1))) ∧ (𝑘 ∈ ℕ ∧ ¬ (vol‘(𝐹‘𝑘)) ∈ ℝ)) → (vol‘(𝐹‘𝑘)) = +∞)
243		simpll 766	. . . . . . . 8 ⊢ (((𝐹:ℕ⟶dom vol ∧ ∀𝑛 ∈ ℕ (𝐹‘𝑛) ⊆ (𝐹‘(𝑛 + 1))) ∧ (𝑘 ∈ ℕ ∧ ¬ (vol‘(𝐹‘𝑘)) ∈ ℝ)) → 𝐹:ℕ⟶dom vol)
244		ffun 6663	. . . . . . . . . 10 ⊢ (vol:dom vol⟶(0[,]+∞) → Fun vol)
245	50, 244	ax-mp 5	. . . . . . . . 9 ⊢ Fun vol
246		frn 6667	. . . . . . . . 9 ⊢ (𝐹:ℕ⟶dom vol → ran 𝐹 ⊆ dom vol)
247		funfvima2 7175	. . . . . . . . 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 2835	. . . . . 6 ⊢ (((𝐹:ℕ⟶dom vol ∧ ∀𝑛 ∈ ℕ (𝐹‘𝑛) ⊆ (𝐹‘(𝑛 + 1))) ∧ (𝑘 ∈ ℕ ∧ ¬ (vol‘(𝐹‘𝑘)) ∈ ℝ)) → +∞ ∈ (vol “ ran 𝐹))
251		supxrpnf 13231	. . . . . 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 2779	. . . 4 ⊢ (((𝐹:ℕ⟶dom vol ∧ ∀𝑛 ∈ ℕ (𝐹‘𝑛) ⊆ (𝐹‘(𝑛 + 1))) ∧ (𝑘 ∈ ℕ ∧ ¬ (vol‘(𝐹‘𝑘)) ∈ ℝ)) → (vol‘∪ ran 𝐹) = sup((vol “ ran 𝐹), ℝ^*, < ))
254	253	rexlimdvaa 3136	. . 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 2113 ∀wral 3049 ∃wrex 3058 ∖ cdif 3896 ∪ cun 3897 ∩ cin 3898 ⊆ wss 3899 ∅c0 4283 ∪ cuni 4861 ∪ ciun 4944 Disj wdisj 5063 class class class wbr 5096 ↦ cmpt 5177 dom cdm 5622 ran crn 5623 “ cima 5625 ∘ ccom 5626 Fun wfun 6484 Fn wfn 6485 ⟶wf 6486 ‘cfv 6490 (class class class)co 7356 Fincfn 8881 supcsup 9341 ℝcr 11023 0cc0 11024 1c1 11025 + caddc 11027 +∞cpnf 11161 -∞cmnf 11162 ℝ^*cxr 11163 < clt 11164 ≤ cle 11165 ℕcn 12143 ℤcz 12486 ℤ_≥cuz 12749 [,]cicc 13262 ...cfz 13421 ..^cfzo 13568 seqcseq 13922 vol*covol 25417 volcvol 25418

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 2115 ax-9 2123 ax-10 2146 ax-11 2162 ax-12 2182 ax-ext 2706 ax-rep 5222 ax-sep 5239 ax-nul 5249 ax-pow 5308 ax-pr 5375 ax-un 7678 ax-inf2 9548 ax-cc 10343 ax-cnex 11080 ax-resscn 11081 ax-1cn 11082 ax-icn 11083 ax-addcl 11084 ax-addrcl 11085 ax-mulcl 11086 ax-mulrcl 11087 ax-mulcom 11088 ax-addass 11089 ax-mulass 11090 ax-distr 11091 ax-i2m1 11092 ax-1ne0 11093 ax-1rid 11094 ax-rnegex 11095 ax-rrecex 11096 ax-cnre 11097 ax-pre-lttri 11098 ax-pre-lttrn 11099 ax-pre-ltadd 11100 ax-pre-mulgt0 11101 ax-pre-sup 11102

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 2537 df-eu 2567 df-clab 2713 df-cleq 2726 df-clel 2809 df-nfc 2883 df-ne 2931 df-nel 3035 df-ral 3050 df-rex 3059 df-rmo 3348 df-reu 3349 df-rab 3398 df-v 3440 df-sbc 3739 df-csb 3848 df-dif 3902 df-un 3904 df-in 3906 df-ss 3916 df-pss 3919 df-nul 4284 df-if 4478 df-pw 4554 df-sn 4579 df-pr 4581 df-op 4585 df-uni 4862 df-int 4901 df-iun 4946 df-disj 5064 df-br 5097 df-opab 5159 df-mpt 5178 df-tr 5204 df-id 5517 df-eprel 5522 df-po 5530 df-so 5531 df-fr 5575 df-se 5576 df-we 5577 df-xp 5628 df-rel 5629 df-cnv 5630 df-co 5631 df-dm 5632 df-rn 5633 df-res 5634 df-ima 5635 df-pred 6257 df-ord 6318 df-on 6319 df-lim 6320 df-suc 6321 df-iota 6446 df-fun 6492 df-fn 6493 df-f 6494 df-f1 6495 df-fo 6496 df-f1o 6497 df-fv 6498 df-isom 6499 df-riota 7313 df-ov 7359 df-oprab 7360 df-mpo 7361 df-of 7620 df-om 7807 df-1st 7931 df-2nd 7932 df-frecs 8221 df-wrecs 8252 df-recs 8301 df-rdg 8339 df-1o 8395 df-2o 8396 df-er 8633 df-map 8763 df-pm 8764 df-en 8882 df-dom 8883 df-sdom 8884 df-fin 8885 df-sup 9343 df-inf 9344 df-oi 9413 df-dju 9811 df-card 9849 df-pnf 11166 df-mnf 11167 df-xr 11168 df-ltxr 11169 df-le 11170 df-sub 11364 df-neg 11365 df-div 11793 df-nn 12144 df-2 12206 df-3 12207 df-n0 12400 df-z 12487 df-uz 12750 df-q 12860 df-rp 12904 df-xadd 13025 df-ioo 13263 df-ico 13265 df-icc 13266 df-fz 13422 df-fzo 13569 df-fl 13710 df-seq 13923 df-exp 13983 df-hash 14252 df-cj 15020 df-re 15021 df-im 15022 df-sqrt 15156 df-abs 15157 df-clim 15409 df-rlim 15410 df-sum 15608 df-xmet 21300 df-met 21301 df-ovol 25419 df-vol 25420

This theorem is referenced by: volsup2 25560 itg1climres 25669 itg2gt0 25715

W3C validator