Theorem voliunnfl 33787

Description: voliun 23543 is incompatible with the Feferman-Levy model; in that model, therefore, the Lebesgue measure as we've defined it isn't actually a measure. (Contributed by Brendan Leahy, 16-Dec-2017.)

Hypotheses

Ref	Expression
voliunnfl.1	⊢ 𝑆 = seq1( + , 𝐺)
voliunnfl.2	⊢ 𝐺 = (𝑛 ∈ ℕ ↦ (vol‘(𝑓‘𝑛)))
voliunnfl.3	⊢ ((∀𝑛 ∈ ℕ ((𝑓‘𝑛) ∈ dom vol ∧ (vol‘(𝑓‘𝑛)) ∈ ℝ) ∧ Disj 𝑛 ∈ ℕ (𝑓‘𝑛)) → (vol‘∪ 𝑛 ∈ ℕ (𝑓‘𝑛)) = sup(ran 𝑆, ℝ*, < ))

Assertion

Ref	Expression
voliunnfl	⊢ ((𝐴 ≼ ℕ ∧ ∀𝑥 ∈ 𝐴 𝑥 ≼ ℕ) → ∪ 𝐴 ≠ ℝ)

Distinct variable group:   𝑓,𝑛,𝑥,𝐴

Allowed substitution hints:   𝑆(𝑥,𝑓,𝑛)   𝐺(𝑥,𝑓,𝑛)

Proof of Theorem voliunnfl

Dummy variables 𝑔 𝑚 𝑙 are mutually distinct and distinct from all other variables.

Step	Hyp	Ref	Expression
1		unieq 4583	. . . . . . . . 9 ⊢ (𝐴 = ∅ → ∪ 𝐴 = ∪ ∅)
2		uni0 4602	. . . . . . . . 9 ⊢ ∪ ∅ = ∅
3	1, 2	syl6eq 2821	. . . . . . . 8 ⊢ (𝐴 = ∅ → ∪ 𝐴 = ∅)
4	3	fveq2d 6337	. . . . . . 7 ⊢ (𝐴 = ∅ → (vol‘∪ 𝐴) = (vol‘∅))
5		0mbl 23528	. . . . . . . . 9 ⊢ ∅ ∈ dom vol
6		mblvol 23519	. . . . . . . . 9 ⊢ (∅ ∈ dom vol → (vol‘∅) = (vol*‘∅))
7	5, 6	ax-mp 5	. . . . . . . 8 ⊢ (vol‘∅) = (vol*‘∅)
8		ovol0 23482	. . . . . . . 8 ⊢ (vol*‘∅) = 0
9	7, 8	eqtri 2793	. . . . . . 7 ⊢ (vol‘∅) = 0
10	4, 9	syl6req 2822	. . . . . 6 ⊢ (𝐴 = ∅ → 0 = (vol‘∪ 𝐴))
11	10	a1d 25	. . . . 5 ⊢ (𝐴 = ∅ → ((𝐴 ≼ ℕ ∧ (∀𝑥 ∈ 𝐴 𝑥 ≼ ℕ ∧ ∪ 𝐴 ⊆ ℝ)) → 0 = (vol‘∪ 𝐴)))
12		reldom 8116	. . . . . . . . . . 11 ⊢ Rel ≼
13	12	brrelexi 5299	. . . . . . . . . 10 ⊢ (𝐴 ≼ ℕ → 𝐴 ∈ V)
14		0sdomg 8246	. . . . . . . . . 10 ⊢ (𝐴 ∈ V → (∅ ≺ 𝐴 ↔ 𝐴 ≠ ∅))
15	13, 14	syl 17	. . . . . . . . 9 ⊢ (𝐴 ≼ ℕ → (∅ ≺ 𝐴 ↔ 𝐴 ≠ ∅))
16	15	biimparc 465	. . . . . . . 8 ⊢ ((𝐴 ≠ ∅ ∧ 𝐴 ≼ ℕ) → ∅ ≺ 𝐴)
17		fodomr 8268	. . . . . . . 8 ⊢ ((∅ ≺ 𝐴 ∧ 𝐴 ≼ ℕ) → ∃𝑔 𝑔:ℕ–onto→𝐴)
18	16, 17	sylancom 570	. . . . . . 7 ⊢ ((𝐴 ≠ ∅ ∧ 𝐴 ≼ ℕ) → ∃𝑔 𝑔:ℕ–onto→𝐴)
19		unissb 4606	. . . . . . . . . . . . 13 ⊢ (∪ 𝐴 ⊆ ℝ ↔ ∀𝑥 ∈ 𝐴 𝑥 ⊆ ℝ)
20	19	anbi1i 604	. . . . . . . . . . . 12 ⊢ ((∪ 𝐴 ⊆ ℝ ∧ ∀𝑥 ∈ 𝐴 𝑥 ≼ ℕ) ↔ (∀𝑥 ∈ 𝐴 𝑥 ⊆ ℝ ∧ ∀𝑥 ∈ 𝐴 𝑥 ≼ ℕ))
21		r19.26 3212	. . . . . . . . . . . 12 ⊢ (∀𝑥 ∈ 𝐴 (𝑥 ⊆ ℝ ∧ 𝑥 ≼ ℕ) ↔ (∀𝑥 ∈ 𝐴 𝑥 ⊆ ℝ ∧ ∀𝑥 ∈ 𝐴 𝑥 ≼ ℕ))
22	20, 21	bitr4i 267	. . . . . . . . . . 11 ⊢ ((∪ 𝐴 ⊆ ℝ ∧ ∀𝑥 ∈ 𝐴 𝑥 ≼ ℕ) ↔ ∀𝑥 ∈ 𝐴 (𝑥 ⊆ ℝ ∧ 𝑥 ≼ ℕ))
23		ovolctb2 23481	. . . . . . . . . . . . . 14 ⊢ ((𝑥 ⊆ ℝ ∧ 𝑥 ≼ ℕ) → (vol*‘𝑥) = 0)
24	23	ex 397	. . . . . . . . . . . . 13 ⊢ (𝑥 ⊆ ℝ → (𝑥 ≼ ℕ → (vol*‘𝑥) = 0))
25	24	imdistani 552	. . . . . . . . . . . 12 ⊢ ((𝑥 ⊆ ℝ ∧ 𝑥 ≼ ℕ) → (𝑥 ⊆ ℝ ∧ (vol*‘𝑥) = 0))
26	25	ralimi 3101	. . . . . . . . . . 11 ⊢ (∀𝑥 ∈ 𝐴 (𝑥 ⊆ ℝ ∧ 𝑥 ≼ ℕ) → ∀𝑥 ∈ 𝐴 (𝑥 ⊆ ℝ ∧ (vol*‘𝑥) = 0))
27	22, 26	sylbi 207	. . . . . . . . . 10 ⊢ ((∪ 𝐴 ⊆ ℝ ∧ ∀𝑥 ∈ 𝐴 𝑥 ≼ ℕ) → ∀𝑥 ∈ 𝐴 (𝑥 ⊆ ℝ ∧ (vol*‘𝑥) = 0))
28	27	ancoms 455	. . . . . . . . 9 ⊢ ((∀𝑥 ∈ 𝐴 𝑥 ≼ ℕ ∧ ∪ 𝐴 ⊆ ℝ) → ∀𝑥 ∈ 𝐴 (𝑥 ⊆ ℝ ∧ (vol*‘𝑥) = 0))
29		foima 6262	. . . . . . . . . . . 12 ⊢ (𝑔:ℕ–onto→𝐴 → (𝑔 “ ℕ) = 𝐴)
30	29	raleqdv 3293	. . . . . . . . . . 11 ⊢ (𝑔:ℕ–onto→𝐴 → (∀𝑥 ∈ (𝑔 “ ℕ)(𝑥 ⊆ ℝ ∧ (vol*‘𝑥) = 0) ↔ ∀𝑥 ∈ 𝐴 (𝑥 ⊆ ℝ ∧ (vol*‘𝑥) = 0)))
31		fofn 6259	. . . . . . . . . . . 12 ⊢ (𝑔:ℕ–onto→𝐴 → 𝑔 Fn ℕ)
32		ssid 3774	. . . . . . . . . . . 12 ⊢ ℕ ⊆ ℕ
33		sseq1 3776	. . . . . . . . . . . . . 14 ⊢ (𝑥 = (𝑔‘𝑚) → (𝑥 ⊆ ℝ ↔ (𝑔‘𝑚) ⊆ ℝ))
34		fveq2 6333	. . . . . . . . . . . . . . 15 ⊢ (𝑥 = (𝑔‘𝑚) → (vol*‘𝑥) = (vol*‘(𝑔‘𝑚)))
35	34	eqeq1d 2773	. . . . . . . . . . . . . 14 ⊢ (𝑥 = (𝑔‘𝑚) → ((vol*‘𝑥) = 0 ↔ (vol*‘(𝑔‘𝑚)) = 0))
36	33, 35	anbi12d 610	. . . . . . . . . . . . 13 ⊢ (𝑥 = (𝑔‘𝑚) → ((𝑥 ⊆ ℝ ∧ (vol*‘𝑥) = 0) ↔ ((𝑔‘𝑚) ⊆ ℝ ∧ (vol*‘(𝑔‘𝑚)) = 0)))
37	36	ralima 6642	. . . . . . . . . . . 12 ⊢ ((𝑔 Fn ℕ ∧ ℕ ⊆ ℕ) → (∀𝑥 ∈ (𝑔 “ ℕ)(𝑥 ⊆ ℝ ∧ (vol*‘𝑥) = 0) ↔ ∀𝑚 ∈ ℕ ((𝑔‘𝑚) ⊆ ℝ ∧ (vol*‘(𝑔‘𝑚)) = 0)))
38	31, 32, 37	sylancl 568	. . . . . . . . . . 11 ⊢ (𝑔:ℕ–onto→𝐴 → (∀𝑥 ∈ (𝑔 “ ℕ)(𝑥 ⊆ ℝ ∧ (vol*‘𝑥) = 0) ↔ ∀𝑚 ∈ ℕ ((𝑔‘𝑚) ⊆ ℝ ∧ (vol*‘(𝑔‘𝑚)) = 0)))
39	30, 38	bitr3d 270	. . . . . . . . . 10 ⊢ (𝑔:ℕ–onto→𝐴 → (∀𝑥 ∈ 𝐴 (𝑥 ⊆ ℝ ∧ (vol*‘𝑥) = 0) ↔ ∀𝑚 ∈ ℕ ((𝑔‘𝑚) ⊆ ℝ ∧ (vol*‘(𝑔‘𝑚)) = 0)))
40		difss 3889	. . . . . . . . . . . . . . . . . 18 ⊢ ((𝑔‘𝑚) ∖ ∪ 𝑙 ∈ (1..^𝑚)(𝑔‘𝑙)) ⊆ (𝑔‘𝑚)
41		ovolssnul 23476	. . . . . . . . . . . . . . . . . 18 ⊢ ((((𝑔‘𝑚) ∖ ∪ 𝑙 ∈ (1..^𝑚)(𝑔‘𝑙)) ⊆ (𝑔‘𝑚) ∧ (𝑔‘𝑚) ⊆ ℝ ∧ (vol*‘(𝑔‘𝑚)) = 0) → (vol*‘((𝑔‘𝑚) ∖ ∪ 𝑙 ∈ (1..^𝑚)(𝑔‘𝑙))) = 0)
42	40, 41	mp3an1 1559	. . . . . . . . . . . . . . . . 17 ⊢ (((𝑔‘𝑚) ⊆ ℝ ∧ (vol*‘(𝑔‘𝑚)) = 0) → (vol*‘((𝑔‘𝑚) ∖ ∪ 𝑙 ∈ (1..^𝑚)(𝑔‘𝑙))) = 0)
43		ssdifss 3893	. . . . . . . . . . . . . . . . . 18 ⊢ ((𝑔‘𝑚) ⊆ ℝ → ((𝑔‘𝑚) ∖ ∪ 𝑙 ∈ (1..^𝑚)(𝑔‘𝑙)) ⊆ ℝ)
44		nulmbl 23524	. . . . . . . . . . . . . . . . . . 19 ⊢ ((((𝑔‘𝑚) ∖ ∪ 𝑙 ∈ (1..^𝑚)(𝑔‘𝑙)) ⊆ ℝ ∧ (vol*‘((𝑔‘𝑚) ∖ ∪ 𝑙 ∈ (1..^𝑚)(𝑔‘𝑙))) = 0) → ((𝑔‘𝑚) ∖ ∪ 𝑙 ∈ (1..^𝑚)(𝑔‘𝑙)) ∈ dom vol)
45		mblvol 23519	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ (((𝑔‘𝑚) ∖ ∪ 𝑙 ∈ (1..^𝑚)(𝑔‘𝑙)) ∈ dom vol → (vol‘((𝑔‘𝑚) ∖ ∪ 𝑙 ∈ (1..^𝑚)(𝑔‘𝑙))) = (vol*‘((𝑔‘𝑚) ∖ ∪ 𝑙 ∈ (1..^𝑚)(𝑔‘𝑙))))
46	45	eqeq1d 2773	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ (((𝑔‘𝑚) ∖ ∪ 𝑙 ∈ (1..^𝑚)(𝑔‘𝑙)) ∈ dom vol → ((vol‘((𝑔‘𝑚) ∖ ∪ 𝑙 ∈ (1..^𝑚)(𝑔‘𝑙))) = 0 ↔ (vol*‘((𝑔‘𝑚) ∖ ∪ 𝑙 ∈ (1..^𝑚)(𝑔‘𝑙))) = 0))
47	46	biimpar 463	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ ((((𝑔‘𝑚) ∖ ∪ 𝑙 ∈ (1..^𝑚)(𝑔‘𝑙)) ∈ dom vol ∧ (vol*‘((𝑔‘𝑚) ∖ ∪ 𝑙 ∈ (1..^𝑚)(𝑔‘𝑙))) = 0) → (vol‘((𝑔‘𝑚) ∖ ∪ 𝑙 ∈ (1..^𝑚)(𝑔‘𝑙))) = 0)
48		0re 10243	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ 0 ∈ ℝ
49	47, 48	syl6eqel 2858	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ ((((𝑔‘𝑚) ∖ ∪ 𝑙 ∈ (1..^𝑚)(𝑔‘𝑙)) ∈ dom vol ∧ (vol*‘((𝑔‘𝑚) ∖ ∪ 𝑙 ∈ (1..^𝑚)(𝑔‘𝑙))) = 0) → (vol‘((𝑔‘𝑚) ∖ ∪ 𝑙 ∈ (1..^𝑚)(𝑔‘𝑙))) ∈ ℝ)
50	49	expcom 398	. . . . . . . . . . . . . . . . . . . . 21 ⊢ ((vol*‘((𝑔‘𝑚) ∖ ∪ 𝑙 ∈ (1..^𝑚)(𝑔‘𝑙))) = 0 → (((𝑔‘𝑚) ∖ ∪ 𝑙 ∈ (1..^𝑚)(𝑔‘𝑙)) ∈ dom vol → (vol‘((𝑔‘𝑚) ∖ ∪ 𝑙 ∈ (1..^𝑚)(𝑔‘𝑙))) ∈ ℝ))
51	50	ancld 534	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((vol*‘((𝑔‘𝑚) ∖ ∪ 𝑙 ∈ (1..^𝑚)(𝑔‘𝑙))) = 0 → (((𝑔‘𝑚) ∖ ∪ 𝑙 ∈ (1..^𝑚)(𝑔‘𝑙)) ∈ dom vol → (((𝑔‘𝑚) ∖ ∪ 𝑙 ∈ (1..^𝑚)(𝑔‘𝑙)) ∈ dom vol ∧ (vol‘((𝑔‘𝑚) ∖ ∪ 𝑙 ∈ (1..^𝑚)(𝑔‘𝑙))) ∈ ℝ)))
52	51	adantl 467	. . . . . . . . . . . . . . . . . . 19 ⊢ ((((𝑔‘𝑚) ∖ ∪ 𝑙 ∈ (1..^𝑚)(𝑔‘𝑙)) ⊆ ℝ ∧ (vol*‘((𝑔‘𝑚) ∖ ∪ 𝑙 ∈ (1..^𝑚)(𝑔‘𝑙))) = 0) → (((𝑔‘𝑚) ∖ ∪ 𝑙 ∈ (1..^𝑚)(𝑔‘𝑙)) ∈ dom vol → (((𝑔‘𝑚) ∖ ∪ 𝑙 ∈ (1..^𝑚)(𝑔‘𝑙)) ∈ dom vol ∧ (vol‘((𝑔‘𝑚) ∖ ∪ 𝑙 ∈ (1..^𝑚)(𝑔‘𝑙))) ∈ ℝ)))
53	44, 52	mpd 15	. . . . . . . . . . . . . . . . . 18 ⊢ ((((𝑔‘𝑚) ∖ ∪ 𝑙 ∈ (1..^𝑚)(𝑔‘𝑙)) ⊆ ℝ ∧ (vol*‘((𝑔‘𝑚) ∖ ∪ 𝑙 ∈ (1..^𝑚)(𝑔‘𝑙))) = 0) → (((𝑔‘𝑚) ∖ ∪ 𝑙 ∈ (1..^𝑚)(𝑔‘𝑙)) ∈ dom vol ∧ (vol‘((𝑔‘𝑚) ∖ ∪ 𝑙 ∈ (1..^𝑚)(𝑔‘𝑙))) ∈ ℝ))
54	43, 53	sylan 563	. . . . . . . . . . . . . . . . 17 ⊢ (((𝑔‘𝑚) ⊆ ℝ ∧ (vol*‘((𝑔‘𝑚) ∖ ∪ 𝑙 ∈ (1..^𝑚)(𝑔‘𝑙))) = 0) → (((𝑔‘𝑚) ∖ ∪ 𝑙 ∈ (1..^𝑚)(𝑔‘𝑙)) ∈ dom vol ∧ (vol‘((𝑔‘𝑚) ∖ ∪ 𝑙 ∈ (1..^𝑚)(𝑔‘𝑙))) ∈ ℝ))
55	42, 54	syldan 573	. . . . . . . . . . . . . . . 16 ⊢ (((𝑔‘𝑚) ⊆ ℝ ∧ (vol*‘(𝑔‘𝑚)) = 0) → (((𝑔‘𝑚) ∖ ∪ 𝑙 ∈ (1..^𝑚)(𝑔‘𝑙)) ∈ dom vol ∧ (vol‘((𝑔‘𝑚) ∖ ∪ 𝑙 ∈ (1..^𝑚)(𝑔‘𝑙))) ∈ ℝ))
56	55	ralimi 3101	. . . . . . . . . . . . . . 15 ⊢ (∀𝑚 ∈ ℕ ((𝑔‘𝑚) ⊆ ℝ ∧ (vol*‘(𝑔‘𝑚)) = 0) → ∀𝑚 ∈ ℕ (((𝑔‘𝑚) ∖ ∪ 𝑙 ∈ (1..^𝑚)(𝑔‘𝑙)) ∈ dom vol ∧ (vol‘((𝑔‘𝑚) ∖ ∪ 𝑙 ∈ (1..^𝑚)(𝑔‘𝑙))) ∈ ℝ))
57		fveq2 6333	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (𝑚 = 𝑛 → (𝑔‘𝑚) = (𝑔‘𝑛))
58		oveq2 6802	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (𝑚 = 𝑛 → (1..^𝑚) = (1..^𝑛))
59	58	iuneq1d 4680	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (𝑚 = 𝑛 → ∪ 𝑙 ∈ (1..^𝑚)(𝑔‘𝑙) = ∪ 𝑙 ∈ (1..^𝑛)(𝑔‘𝑙))
60	57, 59	difeq12d 3881	. . . . . . . . . . . . . . . . . . . 20 ⊢ (𝑚 = 𝑛 → ((𝑔‘𝑚) ∖ ∪ 𝑙 ∈ (1..^𝑚)(𝑔‘𝑙)) = ((𝑔‘𝑛) ∖ ∪ 𝑙 ∈ (1..^𝑛)(𝑔‘𝑙)))
61		eqid 2771	. . . . . . . . . . . . . . . . . . . 20 ⊢ (𝑚 ∈ ℕ ↦ ((𝑔‘𝑚) ∖ ∪ 𝑙 ∈ (1..^𝑚)(𝑔‘𝑙))) = (𝑚 ∈ ℕ ↦ ((𝑔‘𝑚) ∖ ∪ 𝑙 ∈ (1..^𝑚)(𝑔‘𝑙)))
62		fvex 6343	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (𝑔‘𝑛) ∈ V
63		difexg 4943	. . . . . . . . . . . . . . . . . . . . 21 ⊢ ((𝑔‘𝑛) ∈ V → ((𝑔‘𝑛) ∖ ∪ 𝑙 ∈ (1..^𝑛)(𝑔‘𝑙)) ∈ V)
64	62, 63	ax-mp 5	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((𝑔‘𝑛) ∖ ∪ 𝑙 ∈ (1..^𝑛)(𝑔‘𝑙)) ∈ V
65	60, 61, 64	fvmpt 6425	. . . . . . . . . . . . . . . . . . 19 ⊢ (𝑛 ∈ ℕ → ((𝑚 ∈ ℕ ↦ ((𝑔‘𝑚) ∖ ∪ 𝑙 ∈ (1..^𝑚)(𝑔‘𝑙)))‘𝑛) = ((𝑔‘𝑛) ∖ ∪ 𝑙 ∈ (1..^𝑛)(𝑔‘𝑙)))
66	65	eleq1d 2835	. . . . . . . . . . . . . . . . . 18 ⊢ (𝑛 ∈ ℕ → (((𝑚 ∈ ℕ ↦ ((𝑔‘𝑚) ∖ ∪ 𝑙 ∈ (1..^𝑚)(𝑔‘𝑙)))‘𝑛) ∈ dom vol ↔ ((𝑔‘𝑛) ∖ ∪ 𝑙 ∈ (1..^𝑛)(𝑔‘𝑙)) ∈ dom vol))
67	65	fveq2d 6337	. . . . . . . . . . . . . . . . . . 19 ⊢ (𝑛 ∈ ℕ → (vol‘((𝑚 ∈ ℕ ↦ ((𝑔‘𝑚) ∖ ∪ 𝑙 ∈ (1..^𝑚)(𝑔‘𝑙)))‘𝑛)) = (vol‘((𝑔‘𝑛) ∖ ∪ 𝑙 ∈ (1..^𝑛)(𝑔‘𝑙))))
68	67	eleq1d 2835	. . . . . . . . . . . . . . . . . 18 ⊢ (𝑛 ∈ ℕ → ((vol‘((𝑚 ∈ ℕ ↦ ((𝑔‘𝑚) ∖ ∪ 𝑙 ∈ (1..^𝑚)(𝑔‘𝑙)))‘𝑛)) ∈ ℝ ↔ (vol‘((𝑔‘𝑛) ∖ ∪ 𝑙 ∈ (1..^𝑛)(𝑔‘𝑙))) ∈ ℝ))
69	66, 68	anbi12d 610	. . . . . . . . . . . . . . . . 17 ⊢ (𝑛 ∈ ℕ → ((((𝑚 ∈ ℕ ↦ ((𝑔‘𝑚) ∖ ∪ 𝑙 ∈ (1..^𝑚)(𝑔‘𝑙)))‘𝑛) ∈ dom vol ∧ (vol‘((𝑚 ∈ ℕ ↦ ((𝑔‘𝑚) ∖ ∪ 𝑙 ∈ (1..^𝑚)(𝑔‘𝑙)))‘𝑛)) ∈ ℝ) ↔ (((𝑔‘𝑛) ∖ ∪ 𝑙 ∈ (1..^𝑛)(𝑔‘𝑙)) ∈ dom vol ∧ (vol‘((𝑔‘𝑛) ∖ ∪ 𝑙 ∈ (1..^𝑛)(𝑔‘𝑙))) ∈ ℝ)))
70	69	ralbiia 3128	. . . . . . . . . . . . . . . 16 ⊢ (∀𝑛 ∈ ℕ (((𝑚 ∈ ℕ ↦ ((𝑔‘𝑚) ∖ ∪ 𝑙 ∈ (1..^𝑚)(𝑔‘𝑙)))‘𝑛) ∈ dom vol ∧ (vol‘((𝑚 ∈ ℕ ↦ ((𝑔‘𝑚) ∖ ∪ 𝑙 ∈ (1..^𝑚)(𝑔‘𝑙)))‘𝑛)) ∈ ℝ) ↔ ∀𝑛 ∈ ℕ (((𝑔‘𝑛) ∖ ∪ 𝑙 ∈ (1..^𝑛)(𝑔‘𝑙)) ∈ dom vol ∧ (vol‘((𝑔‘𝑛) ∖ ∪ 𝑙 ∈ (1..^𝑛)(𝑔‘𝑙))) ∈ ℝ))
71		fveq2 6333	. . . . . . . . . . . . . . . . . . . 20 ⊢ (𝑛 = 𝑚 → (𝑔‘𝑛) = (𝑔‘𝑚))
72		oveq2 6802	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (𝑛 = 𝑚 → (1..^𝑛) = (1..^𝑚))
73	72	iuneq1d 4680	. . . . . . . . . . . . . . . . . . . 20 ⊢ (𝑛 = 𝑚 → ∪ 𝑙 ∈ (1..^𝑛)(𝑔‘𝑙) = ∪ 𝑙 ∈ (1..^𝑚)(𝑔‘𝑙))
74	71, 73	difeq12d 3881	. . . . . . . . . . . . . . . . . . 19 ⊢ (𝑛 = 𝑚 → ((𝑔‘𝑛) ∖ ∪ 𝑙 ∈ (1..^𝑛)(𝑔‘𝑙)) = ((𝑔‘𝑚) ∖ ∪ 𝑙 ∈ (1..^𝑚)(𝑔‘𝑙)))
75	74	eleq1d 2835	. . . . . . . . . . . . . . . . . 18 ⊢ (𝑛 = 𝑚 → (((𝑔‘𝑛) ∖ ∪ 𝑙 ∈ (1..^𝑛)(𝑔‘𝑙)) ∈ dom vol ↔ ((𝑔‘𝑚) ∖ ∪ 𝑙 ∈ (1..^𝑚)(𝑔‘𝑙)) ∈ dom vol))
76	74	fveq2d 6337	. . . . . . . . . . . . . . . . . . 19 ⊢ (𝑛 = 𝑚 → (vol‘((𝑔‘𝑛) ∖ ∪ 𝑙 ∈ (1..^𝑛)(𝑔‘𝑙))) = (vol‘((𝑔‘𝑚) ∖ ∪ 𝑙 ∈ (1..^𝑚)(𝑔‘𝑙))))
77	76	eleq1d 2835	. . . . . . . . . . . . . . . . . 18 ⊢ (𝑛 = 𝑚 → ((vol‘((𝑔‘𝑛) ∖ ∪ 𝑙 ∈ (1..^𝑛)(𝑔‘𝑙))) ∈ ℝ ↔ (vol‘((𝑔‘𝑚) ∖ ∪ 𝑙 ∈ (1..^𝑚)(𝑔‘𝑙))) ∈ ℝ))
78	75, 77	anbi12d 610	. . . . . . . . . . . . . . . . 17 ⊢ (𝑛 = 𝑚 → ((((𝑔‘𝑛) ∖ ∪ 𝑙 ∈ (1..^𝑛)(𝑔‘𝑙)) ∈ dom vol ∧ (vol‘((𝑔‘𝑛) ∖ ∪ 𝑙 ∈ (1..^𝑛)(𝑔‘𝑙))) ∈ ℝ) ↔ (((𝑔‘𝑚) ∖ ∪ 𝑙 ∈ (1..^𝑚)(𝑔‘𝑙)) ∈ dom vol ∧ (vol‘((𝑔‘𝑚) ∖ ∪ 𝑙 ∈ (1..^𝑚)(𝑔‘𝑙))) ∈ ℝ)))
79	78	cbvralv 3320	. . . . . . . . . . . . . . . 16 ⊢ (∀𝑛 ∈ ℕ (((𝑔‘𝑛) ∖ ∪ 𝑙 ∈ (1..^𝑛)(𝑔‘𝑙)) ∈ dom vol ∧ (vol‘((𝑔‘𝑛) ∖ ∪ 𝑙 ∈ (1..^𝑛)(𝑔‘𝑙))) ∈ ℝ) ↔ ∀𝑚 ∈ ℕ (((𝑔‘𝑚) ∖ ∪ 𝑙 ∈ (1..^𝑚)(𝑔‘𝑙)) ∈ dom vol ∧ (vol‘((𝑔‘𝑚) ∖ ∪ 𝑙 ∈ (1..^𝑚)(𝑔‘𝑙))) ∈ ℝ))
80	70, 79	bitri 264	. . . . . . . . . . . . . . 15 ⊢ (∀𝑛 ∈ ℕ (((𝑚 ∈ ℕ ↦ ((𝑔‘𝑚) ∖ ∪ 𝑙 ∈ (1..^𝑚)(𝑔‘𝑙)))‘𝑛) ∈ dom vol ∧ (vol‘((𝑚 ∈ ℕ ↦ ((𝑔‘𝑚) ∖ ∪ 𝑙 ∈ (1..^𝑚)(𝑔‘𝑙)))‘𝑛)) ∈ ℝ) ↔ ∀𝑚 ∈ ℕ (((𝑔‘𝑚) ∖ ∪ 𝑙 ∈ (1..^𝑚)(𝑔‘𝑙)) ∈ dom vol ∧ (vol‘((𝑔‘𝑚) ∖ ∪ 𝑙 ∈ (1..^𝑚)(𝑔‘𝑙))) ∈ ℝ))
81	56, 80	sylibr 224	. . . . . . . . . . . . . 14 ⊢ (∀𝑚 ∈ ℕ ((𝑔‘𝑚) ⊆ ℝ ∧ (vol*‘(𝑔‘𝑚)) = 0) → ∀𝑛 ∈ ℕ (((𝑚 ∈ ℕ ↦ ((𝑔‘𝑚) ∖ ∪ 𝑙 ∈ (1..^𝑚)(𝑔‘𝑙)))‘𝑛) ∈ dom vol ∧ (vol‘((𝑚 ∈ ℕ ↦ ((𝑔‘𝑚) ∖ ∪ 𝑙 ∈ (1..^𝑚)(𝑔‘𝑙)))‘𝑛)) ∈ ℝ))
82		fveq2 6333	. . . . . . . . . . . . . . . 16 ⊢ (𝑛 = 𝑙 → (𝑔‘𝑛) = (𝑔‘𝑙))
83	82	iundisj2 23538	. . . . . . . . . . . . . . 15 ⊢ Disj 𝑛 ∈ ℕ ((𝑔‘𝑛) ∖ ∪ 𝑙 ∈ (1..^𝑛)(𝑔‘𝑙))
84		disjeq2 4759	. . . . . . . . . . . . . . . 16 ⊢ (∀𝑛 ∈ ℕ ((𝑚 ∈ ℕ ↦ ((𝑔‘𝑚) ∖ ∪ 𝑙 ∈ (1..^𝑚)(𝑔‘𝑙)))‘𝑛) = ((𝑔‘𝑛) ∖ ∪ 𝑙 ∈ (1..^𝑛)(𝑔‘𝑙)) → (Disj 𝑛 ∈ ℕ ((𝑚 ∈ ℕ ↦ ((𝑔‘𝑚) ∖ ∪ 𝑙 ∈ (1..^𝑚)(𝑔‘𝑙)))‘𝑛) ↔ Disj 𝑛 ∈ ℕ ((𝑔‘𝑛) ∖ ∪ 𝑙 ∈ (1..^𝑛)(𝑔‘𝑙))))
85	84, 65	mprg 3075	. . . . . . . . . . . . . . 15 ⊢ (Disj 𝑛 ∈ ℕ ((𝑚 ∈ ℕ ↦ ((𝑔‘𝑚) ∖ ∪ 𝑙 ∈ (1..^𝑚)(𝑔‘𝑙)))‘𝑛) ↔ Disj 𝑛 ∈ ℕ ((𝑔‘𝑛) ∖ ∪ 𝑙 ∈ (1..^𝑛)(𝑔‘𝑙)))
86	83, 85	mpbir 221	. . . . . . . . . . . . . 14 ⊢ Disj 𝑛 ∈ ℕ ((𝑚 ∈ ℕ ↦ ((𝑔‘𝑚) ∖ ∪ 𝑙 ∈ (1..^𝑚)(𝑔‘𝑙)))‘𝑛)
87		nnex 11229	. . . . . . . . . . . . . . . . 17 ⊢ ℕ ∈ V
88	87	mptex 6631	. . . . . . . . . . . . . . . 16 ⊢ (𝑚 ∈ ℕ ↦ ((𝑔‘𝑚) ∖ ∪ 𝑙 ∈ (1..^𝑚)(𝑔‘𝑙))) ∈ V
89		fveq1 6332	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (𝑓 = (𝑚 ∈ ℕ ↦ ((𝑔‘𝑚) ∖ ∪ 𝑙 ∈ (1..^𝑚)(𝑔‘𝑙))) → (𝑓‘𝑛) = ((𝑚 ∈ ℕ ↦ ((𝑔‘𝑚) ∖ ∪ 𝑙 ∈ (1..^𝑚)(𝑔‘𝑙)))‘𝑛))
90	89	eleq1d 2835	. . . . . . . . . . . . . . . . . . . 20 ⊢ (𝑓 = (𝑚 ∈ ℕ ↦ ((𝑔‘𝑚) ∖ ∪ 𝑙 ∈ (1..^𝑚)(𝑔‘𝑙))) → ((𝑓‘𝑛) ∈ dom vol ↔ ((𝑚 ∈ ℕ ↦ ((𝑔‘𝑚) ∖ ∪ 𝑙 ∈ (1..^𝑚)(𝑔‘𝑙)))‘𝑛) ∈ dom vol))
91	89	fveq2d 6337	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (𝑓 = (𝑚 ∈ ℕ ↦ ((𝑔‘𝑚) ∖ ∪ 𝑙 ∈ (1..^𝑚)(𝑔‘𝑙))) → (vol‘(𝑓‘𝑛)) = (vol‘((𝑚 ∈ ℕ ↦ ((𝑔‘𝑚) ∖ ∪ 𝑙 ∈ (1..^𝑚)(𝑔‘𝑙)))‘𝑛)))
92	91	eleq1d 2835	. . . . . . . . . . . . . . . . . . . 20 ⊢ (𝑓 = (𝑚 ∈ ℕ ↦ ((𝑔‘𝑚) ∖ ∪ 𝑙 ∈ (1..^𝑚)(𝑔‘𝑙))) → ((vol‘(𝑓‘𝑛)) ∈ ℝ ↔ (vol‘((𝑚 ∈ ℕ ↦ ((𝑔‘𝑚) ∖ ∪ 𝑙 ∈ (1..^𝑚)(𝑔‘𝑙)))‘𝑛)) ∈ ℝ))
93	90, 92	anbi12d 610	. . . . . . . . . . . . . . . . . . 19 ⊢ (𝑓 = (𝑚 ∈ ℕ ↦ ((𝑔‘𝑚) ∖ ∪ 𝑙 ∈ (1..^𝑚)(𝑔‘𝑙))) → (((𝑓‘𝑛) ∈ dom vol ∧ (vol‘(𝑓‘𝑛)) ∈ ℝ) ↔ (((𝑚 ∈ ℕ ↦ ((𝑔‘𝑚) ∖ ∪ 𝑙 ∈ (1..^𝑚)(𝑔‘𝑙)))‘𝑛) ∈ dom vol ∧ (vol‘((𝑚 ∈ ℕ ↦ ((𝑔‘𝑚) ∖ ∪ 𝑙 ∈ (1..^𝑚)(𝑔‘𝑙)))‘𝑛)) ∈ ℝ)))
94	93	ralbidv 3135	. . . . . . . . . . . . . . . . . 18 ⊢ (𝑓 = (𝑚 ∈ ℕ ↦ ((𝑔‘𝑚) ∖ ∪ 𝑙 ∈ (1..^𝑚)(𝑔‘𝑙))) → (∀𝑛 ∈ ℕ ((𝑓‘𝑛) ∈ dom vol ∧ (vol‘(𝑓‘𝑛)) ∈ ℝ) ↔ ∀𝑛 ∈ ℕ (((𝑚 ∈ ℕ ↦ ((𝑔‘𝑚) ∖ ∪ 𝑙 ∈ (1..^𝑚)(𝑔‘𝑙)))‘𝑛) ∈ dom vol ∧ (vol‘((𝑚 ∈ ℕ ↦ ((𝑔‘𝑚) ∖ ∪ 𝑙 ∈ (1..^𝑚)(𝑔‘𝑙)))‘𝑛)) ∈ ℝ)))
95	89	adantr 466	. . . . . . . . . . . . . . . . . . 19 ⊢ ((𝑓 = (𝑚 ∈ ℕ ↦ ((𝑔‘𝑚) ∖ ∪ 𝑙 ∈ (1..^𝑚)(𝑔‘𝑙))) ∧ 𝑛 ∈ ℕ) → (𝑓‘𝑛) = ((𝑚 ∈ ℕ ↦ ((𝑔‘𝑚) ∖ ∪ 𝑙 ∈ (1..^𝑚)(𝑔‘𝑙)))‘𝑛))
96	95	disjeq2dv 4760	. . . . . . . . . . . . . . . . . 18 ⊢ (𝑓 = (𝑚 ∈ ℕ ↦ ((𝑔‘𝑚) ∖ ∪ 𝑙 ∈ (1..^𝑚)(𝑔‘𝑙))) → (Disj 𝑛 ∈ ℕ (𝑓‘𝑛) ↔ Disj 𝑛 ∈ ℕ ((𝑚 ∈ ℕ ↦ ((𝑔‘𝑚) ∖ ∪ 𝑙 ∈ (1..^𝑚)(𝑔‘𝑙)))‘𝑛)))
97	94, 96	anbi12d 610	. . . . . . . . . . . . . . . . 17 ⊢ (𝑓 = (𝑚 ∈ ℕ ↦ ((𝑔‘𝑚) ∖ ∪ 𝑙 ∈ (1..^𝑚)(𝑔‘𝑙))) → ((∀𝑛 ∈ ℕ ((𝑓‘𝑛) ∈ dom vol ∧ (vol‘(𝑓‘𝑛)) ∈ ℝ) ∧ Disj 𝑛 ∈ ℕ (𝑓‘𝑛)) ↔ (∀𝑛 ∈ ℕ (((𝑚 ∈ ℕ ↦ ((𝑔‘𝑚) ∖ ∪ 𝑙 ∈ (1..^𝑚)(𝑔‘𝑙)))‘𝑛) ∈ dom vol ∧ (vol‘((𝑚 ∈ ℕ ↦ ((𝑔‘𝑚) ∖ ∪ 𝑙 ∈ (1..^𝑚)(𝑔‘𝑙)))‘𝑛)) ∈ ℝ) ∧ Disj 𝑛 ∈ ℕ ((𝑚 ∈ ℕ ↦ ((𝑔‘𝑚) ∖ ∪ 𝑙 ∈ (1..^𝑚)(𝑔‘𝑙)))‘𝑛))))
98	89	iuneq2d 4682	. . . . . . . . . . . . . . . . . . 19 ⊢ (𝑓 = (𝑚 ∈ ℕ ↦ ((𝑔‘𝑚) ∖ ∪ 𝑙 ∈ (1..^𝑚)(𝑔‘𝑙))) → ∪ 𝑛 ∈ ℕ (𝑓‘𝑛) = ∪ 𝑛 ∈ ℕ ((𝑚 ∈ ℕ ↦ ((𝑔‘𝑚) ∖ ∪ 𝑙 ∈ (1..^𝑚)(𝑔‘𝑙)))‘𝑛))
99	98	fveq2d 6337	. . . . . . . . . . . . . . . . . 18 ⊢ (𝑓 = (𝑚 ∈ ℕ ↦ ((𝑔‘𝑚) ∖ ∪ 𝑙 ∈ (1..^𝑚)(𝑔‘𝑙))) → (vol‘∪ 𝑛 ∈ ℕ (𝑓‘𝑛)) = (vol‘∪ 𝑛 ∈ ℕ ((𝑚 ∈ ℕ ↦ ((𝑔‘𝑚) ∖ ∪ 𝑙 ∈ (1..^𝑚)(𝑔‘𝑙)))‘𝑛)))
100		voliunnfl.1	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ 𝑆 = seq1( + , 𝐺)
101		voliunnfl.2	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ 𝐺 = (𝑛 ∈ ℕ ↦ (vol‘(𝑓‘𝑛)))
102		seqeq3 13014	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ (𝐺 = (𝑛 ∈ ℕ ↦ (vol‘(𝑓‘𝑛))) → seq1( + , 𝐺) = seq1( + , (𝑛 ∈ ℕ ↦ (vol‘(𝑓‘𝑛)))))
103	101, 102	ax-mp 5	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ seq1( + , 𝐺) = seq1( + , (𝑛 ∈ ℕ ↦ (vol‘(𝑓‘𝑛))))
104	100, 103	eqtri 2793	. . . . . . . . . . . . . . . . . . . . 21 ⊢ 𝑆 = seq1( + , (𝑛 ∈ ℕ ↦ (vol‘(𝑓‘𝑛))))
105	104	rneqi 5491	. . . . . . . . . . . . . . . . . . . 20 ⊢ ran 𝑆 = ran seq1( + , (𝑛 ∈ ℕ ↦ (vol‘(𝑓‘𝑛))))
106	105	supeq1i 8510	. . . . . . . . . . . . . . . . . . 19 ⊢ sup(ran 𝑆, ℝ*, < ) = sup(ran seq1( + , (𝑛 ∈ ℕ ↦ (vol‘(𝑓‘𝑛)))), ℝ*, < )
107	91	mpteq2dv 4880	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (𝑓 = (𝑚 ∈ ℕ ↦ ((𝑔‘𝑚) ∖ ∪ 𝑙 ∈ (1..^𝑚)(𝑔‘𝑙))) → (𝑛 ∈ ℕ ↦ (vol‘(𝑓‘𝑛))) = (𝑛 ∈ ℕ ↦ (vol‘((𝑚 ∈ ℕ ↦ ((𝑔‘𝑚) ∖ ∪ 𝑙 ∈ (1..^𝑚)(𝑔‘𝑙)))‘𝑛))))
108	107	seqeq3d 13017	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (𝑓 = (𝑚 ∈ ℕ ↦ ((𝑔‘𝑚) ∖ ∪ 𝑙 ∈ (1..^𝑚)(𝑔‘𝑙))) → seq1( + , (𝑛 ∈ ℕ ↦ (vol‘(𝑓‘𝑛)))) = seq1( + , (𝑛 ∈ ℕ ↦ (vol‘((𝑚 ∈ ℕ ↦ ((𝑔‘𝑚) ∖ ∪ 𝑙 ∈ (1..^𝑚)(𝑔‘𝑙)))‘𝑛)))))
109	108	rneqd 5492	. . . . . . . . . . . . . . . . . . . 20 ⊢ (𝑓 = (𝑚 ∈ ℕ ↦ ((𝑔‘𝑚) ∖ ∪ 𝑙 ∈ (1..^𝑚)(𝑔‘𝑙))) → ran seq1( + , (𝑛 ∈ ℕ ↦ (vol‘(𝑓‘𝑛)))) = ran seq1( + , (𝑛 ∈ ℕ ↦ (vol‘((𝑚 ∈ ℕ ↦ ((𝑔‘𝑚) ∖ ∪ 𝑙 ∈ (1..^𝑚)(𝑔‘𝑙)))‘𝑛)))))
110	109	supeq1d 8509	. . . . . . . . . . . . . . . . . . 19 ⊢ (𝑓 = (𝑚 ∈ ℕ ↦ ((𝑔‘𝑚) ∖ ∪ 𝑙 ∈ (1..^𝑚)(𝑔‘𝑙))) → sup(ran seq1( + , (𝑛 ∈ ℕ ↦ (vol‘(𝑓‘𝑛)))), ℝ*, < ) = sup(ran seq1( + , (𝑛 ∈ ℕ ↦ (vol‘((𝑚 ∈ ℕ ↦ ((𝑔‘𝑚) ∖ ∪ 𝑙 ∈ (1..^𝑚)(𝑔‘𝑙)))‘𝑛)))), ℝ*, < ))
111	106, 110	syl5eq 2817	. . . . . . . . . . . . . . . . . 18 ⊢ (𝑓 = (𝑚 ∈ ℕ ↦ ((𝑔‘𝑚) ∖ ∪ 𝑙 ∈ (1..^𝑚)(𝑔‘𝑙))) → sup(ran 𝑆, ℝ*, < ) = sup(ran seq1( + , (𝑛 ∈ ℕ ↦ (vol‘((𝑚 ∈ ℕ ↦ ((𝑔‘𝑚) ∖ ∪ 𝑙 ∈ (1..^𝑚)(𝑔‘𝑙)))‘𝑛)))), ℝ*, < ))
112	99, 111	eqeq12d 2786	. . . . . . . . . . . . . . . . 17 ⊢ (𝑓 = (𝑚 ∈ ℕ ↦ ((𝑔‘𝑚) ∖ ∪ 𝑙 ∈ (1..^𝑚)(𝑔‘𝑙))) → ((vol‘∪ 𝑛 ∈ ℕ (𝑓‘𝑛)) = sup(ran 𝑆, ℝ*, < ) ↔ (vol‘∪ 𝑛 ∈ ℕ ((𝑚 ∈ ℕ ↦ ((𝑔‘𝑚) ∖ ∪ 𝑙 ∈ (1..^𝑚)(𝑔‘𝑙)))‘𝑛)) = sup(ran seq1( + , (𝑛 ∈ ℕ ↦ (vol‘((𝑚 ∈ ℕ ↦ ((𝑔‘𝑚) ∖ ∪ 𝑙 ∈ (1..^𝑚)(𝑔‘𝑙)))‘𝑛)))), ℝ*, < )))
113	97, 112	imbi12d 333	. . . . . . . . . . . . . . . 16 ⊢ (𝑓 = (𝑚 ∈ ℕ ↦ ((𝑔‘𝑚) ∖ ∪ 𝑙 ∈ (1..^𝑚)(𝑔‘𝑙))) → (((∀𝑛 ∈ ℕ ((𝑓‘𝑛) ∈ dom vol ∧ (vol‘(𝑓‘𝑛)) ∈ ℝ) ∧ Disj 𝑛 ∈ ℕ (𝑓‘𝑛)) → (vol‘∪ 𝑛 ∈ ℕ (𝑓‘𝑛)) = sup(ran 𝑆, ℝ*, < )) ↔ ((∀𝑛 ∈ ℕ (((𝑚 ∈ ℕ ↦ ((𝑔‘𝑚) ∖ ∪ 𝑙 ∈ (1..^𝑚)(𝑔‘𝑙)))‘𝑛) ∈ dom vol ∧ (vol‘((𝑚 ∈ ℕ ↦ ((𝑔‘𝑚) ∖ ∪ 𝑙 ∈ (1..^𝑚)(𝑔‘𝑙)))‘𝑛)) ∈ ℝ) ∧ Disj 𝑛 ∈ ℕ ((𝑚 ∈ ℕ ↦ ((𝑔‘𝑚) ∖ ∪ 𝑙 ∈ (1..^𝑚)(𝑔‘𝑙)))‘𝑛)) → (vol‘∪ 𝑛 ∈ ℕ ((𝑚 ∈ ℕ ↦ ((𝑔‘𝑚) ∖ ∪ 𝑙 ∈ (1..^𝑚)(𝑔‘𝑙)))‘𝑛)) = sup(ran seq1( + , (𝑛 ∈ ℕ ↦ (vol‘((𝑚 ∈ ℕ ↦ ((𝑔‘𝑚) ∖ ∪ 𝑙 ∈ (1..^𝑚)(𝑔‘𝑙)))‘𝑛)))), ℝ*, < ))))
114		voliunnfl.3	. . . . . . . . . . . . . . . 16 ⊢ ((∀𝑛 ∈ ℕ ((𝑓‘𝑛) ∈ dom vol ∧ (vol‘(𝑓‘𝑛)) ∈ ℝ) ∧ Disj 𝑛 ∈ ℕ (𝑓‘𝑛)) → (vol‘∪ 𝑛 ∈ ℕ (𝑓‘𝑛)) = sup(ran 𝑆, ℝ*, < ))
115	88, 113, 114	vtocl 3411	. . . . . . . . . . . . . . 15 ⊢ ((∀𝑛 ∈ ℕ (((𝑚 ∈ ℕ ↦ ((𝑔‘𝑚) ∖ ∪ 𝑙 ∈ (1..^𝑚)(𝑔‘𝑙)))‘𝑛) ∈ dom vol ∧ (vol‘((𝑚 ∈ ℕ ↦ ((𝑔‘𝑚) ∖ ∪ 𝑙 ∈ (1..^𝑚)(𝑔‘𝑙)))‘𝑛)) ∈ ℝ) ∧ Disj 𝑛 ∈ ℕ ((𝑚 ∈ ℕ ↦ ((𝑔‘𝑚) ∖ ∪ 𝑙 ∈ (1..^𝑚)(𝑔‘𝑙)))‘𝑛)) → (vol‘∪ 𝑛 ∈ ℕ ((𝑚 ∈ ℕ ↦ ((𝑔‘𝑚) ∖ ∪ 𝑙 ∈ (1..^𝑚)(𝑔‘𝑙)))‘𝑛)) = sup(ran seq1( + , (𝑛 ∈ ℕ ↦ (vol‘((𝑚 ∈ ℕ ↦ ((𝑔‘𝑚) ∖ ∪ 𝑙 ∈ (1..^𝑚)(𝑔‘𝑙)))‘𝑛)))), ℝ*, < ))
116	65	iuneq2i 4674	. . . . . . . . . . . . . . . 16 ⊢ ∪ 𝑛 ∈ ℕ ((𝑚 ∈ ℕ ↦ ((𝑔‘𝑚) ∖ ∪ 𝑙 ∈ (1..^𝑚)(𝑔‘𝑙)))‘𝑛) = ∪ 𝑛 ∈ ℕ ((𝑔‘𝑛) ∖ ∪ 𝑙 ∈ (1..^𝑛)(𝑔‘𝑙))
117	116	fveq2i 6336	. . . . . . . . . . . . . . 15 ⊢ (vol‘∪ 𝑛 ∈ ℕ ((𝑚 ∈ ℕ ↦ ((𝑔‘𝑚) ∖ ∪ 𝑙 ∈ (1..^𝑚)(𝑔‘𝑙)))‘𝑛)) = (vol‘∪ 𝑛 ∈ ℕ ((𝑔‘𝑛) ∖ ∪ 𝑙 ∈ (1..^𝑛)(𝑔‘𝑙)))
118	67	mpteq2ia 4875	. . . . . . . . . . . . . . . . . 18 ⊢ (𝑛 ∈ ℕ ↦ (vol‘((𝑚 ∈ ℕ ↦ ((𝑔‘𝑚) ∖ ∪ 𝑙 ∈ (1..^𝑚)(𝑔‘𝑙)))‘𝑛))) = (𝑛 ∈ ℕ ↦ (vol‘((𝑔‘𝑛) ∖ ∪ 𝑙 ∈ (1..^𝑛)(𝑔‘𝑙))))
119		seqeq3 13014	. . . . . . . . . . . . . . . . . 18 ⊢ ((𝑛 ∈ ℕ ↦ (vol‘((𝑚 ∈ ℕ ↦ ((𝑔‘𝑚) ∖ ∪ 𝑙 ∈ (1..^𝑚)(𝑔‘𝑙)))‘𝑛))) = (𝑛 ∈ ℕ ↦ (vol‘((𝑔‘𝑛) ∖ ∪ 𝑙 ∈ (1..^𝑛)(𝑔‘𝑙)))) → seq1( + , (𝑛 ∈ ℕ ↦ (vol‘((𝑚 ∈ ℕ ↦ ((𝑔‘𝑚) ∖ ∪ 𝑙 ∈ (1..^𝑚)(𝑔‘𝑙)))‘𝑛)))) = seq1( + , (𝑛 ∈ ℕ ↦ (vol‘((𝑔‘𝑛) ∖ ∪ 𝑙 ∈ (1..^𝑛)(𝑔‘𝑙))))))
120	118, 119	ax-mp 5	. . . . . . . . . . . . . . . . 17 ⊢ seq1( + , (𝑛 ∈ ℕ ↦ (vol‘((𝑚 ∈ ℕ ↦ ((𝑔‘𝑚) ∖ ∪ 𝑙 ∈ (1..^𝑚)(𝑔‘𝑙)))‘𝑛)))) = seq1( + , (𝑛 ∈ ℕ ↦ (vol‘((𝑔‘𝑛) ∖ ∪ 𝑙 ∈ (1..^𝑛)(𝑔‘𝑙)))))
121	120	rneqi 5491	. . . . . . . . . . . . . . . 16 ⊢ ran seq1( + , (𝑛 ∈ ℕ ↦ (vol‘((𝑚 ∈ ℕ ↦ ((𝑔‘𝑚) ∖ ∪ 𝑙 ∈ (1..^𝑚)(𝑔‘𝑙)))‘𝑛)))) = ran seq1( + , (𝑛 ∈ ℕ ↦ (vol‘((𝑔‘𝑛) ∖ ∪ 𝑙 ∈ (1..^𝑛)(𝑔‘𝑙)))))
122	121	supeq1i 8510	. . . . . . . . . . . . . . 15 ⊢ sup(ran seq1( + , (𝑛 ∈ ℕ ↦ (vol‘((𝑚 ∈ ℕ ↦ ((𝑔‘𝑚) ∖ ∪ 𝑙 ∈ (1..^𝑚)(𝑔‘𝑙)))‘𝑛)))), ℝ*, < ) = sup(ran seq1( + , (𝑛 ∈ ℕ ↦ (vol‘((𝑔‘𝑛) ∖ ∪ 𝑙 ∈ (1..^𝑛)(𝑔‘𝑙))))), ℝ*, < )
123	115, 117, 122	3eqtr3g 2828	. . . . . . . . . . . . . 14 ⊢ ((∀𝑛 ∈ ℕ (((𝑚 ∈ ℕ ↦ ((𝑔‘𝑚) ∖ ∪ 𝑙 ∈ (1..^𝑚)(𝑔‘𝑙)))‘𝑛) ∈ dom vol ∧ (vol‘((𝑚 ∈ ℕ ↦ ((𝑔‘𝑚) ∖ ∪ 𝑙 ∈ (1..^𝑚)(𝑔‘𝑙)))‘𝑛)) ∈ ℝ) ∧ Disj 𝑛 ∈ ℕ ((𝑚 ∈ ℕ ↦ ((𝑔‘𝑚) ∖ ∪ 𝑙 ∈ (1..^𝑚)(𝑔‘𝑙)))‘𝑛)) → (vol‘∪ 𝑛 ∈ ℕ ((𝑔‘𝑛) ∖ ∪ 𝑙 ∈ (1..^𝑛)(𝑔‘𝑙))) = sup(ran seq1( + , (𝑛 ∈ ℕ ↦ (vol‘((𝑔‘𝑛) ∖ ∪ 𝑙 ∈ (1..^𝑛)(𝑔‘𝑙))))), ℝ*, < ))
124	81, 86, 123	sylancl 568	. . . . . . . . . . . . 13 ⊢ (∀𝑚 ∈ ℕ ((𝑔‘𝑚) ⊆ ℝ ∧ (vol*‘(𝑔‘𝑚)) = 0) → (vol‘∪ 𝑛 ∈ ℕ ((𝑔‘𝑛) ∖ ∪ 𝑙 ∈ (1..^𝑛)(𝑔‘𝑙))) = sup(ran seq1( + , (𝑛 ∈ ℕ ↦ (vol‘((𝑔‘𝑛) ∖ ∪ 𝑙 ∈ (1..^𝑛)(𝑔‘𝑙))))), ℝ*, < ))
125	124	adantl 467	. . . . . . . . . . . 12 ⊢ ((𝑔:ℕ–onto→𝐴 ∧ ∀𝑚 ∈ ℕ ((𝑔‘𝑚) ⊆ ℝ ∧ (vol*‘(𝑔‘𝑚)) = 0)) → (vol‘∪ 𝑛 ∈ ℕ ((𝑔‘𝑛) ∖ ∪ 𝑙 ∈ (1..^𝑛)(𝑔‘𝑙))) = sup(ran seq1( + , (𝑛 ∈ ℕ ↦ (vol‘((𝑔‘𝑛) ∖ ∪ 𝑙 ∈ (1..^𝑛)(𝑔‘𝑙))))), ℝ*, < ))
126	82	iundisj 23537	. . . . . . . . . . . . . . . 16 ⊢ ∪ 𝑛 ∈ ℕ (𝑔‘𝑛) = ∪ 𝑛 ∈ ℕ ((𝑔‘𝑛) ∖ ∪ 𝑙 ∈ (1..^𝑛)(𝑔‘𝑙))
127		fofun 6258	. . . . . . . . . . . . . . . . 17 ⊢ (𝑔:ℕ–onto→𝐴 → Fun 𝑔)
128		funiunfv 6650	. . . . . . . . . . . . . . . . 17 ⊢ (Fun 𝑔 → ∪ 𝑛 ∈ ℕ (𝑔‘𝑛) = ∪ (𝑔 “ ℕ))
129	127, 128	syl 17	. . . . . . . . . . . . . . . 16 ⊢ (𝑔:ℕ–onto→𝐴 → ∪ 𝑛 ∈ ℕ (𝑔‘𝑛) = ∪ (𝑔 “ ℕ))
130	126, 129	syl5eqr 2819	. . . . . . . . . . . . . . 15 ⊢ (𝑔:ℕ–onto→𝐴 → ∪ 𝑛 ∈ ℕ ((𝑔‘𝑛) ∖ ∪ 𝑙 ∈ (1..^𝑛)(𝑔‘𝑙)) = ∪ (𝑔 “ ℕ))
131	29	unieqd 4585	. . . . . . . . . . . . . . 15 ⊢ (𝑔:ℕ–onto→𝐴 → ∪ (𝑔 “ ℕ) = ∪ 𝐴)
132	130, 131	eqtrd 2805	. . . . . . . . . . . . . 14 ⊢ (𝑔:ℕ–onto→𝐴 → ∪ 𝑛 ∈ ℕ ((𝑔‘𝑛) ∖ ∪ 𝑙 ∈ (1..^𝑛)(𝑔‘𝑙)) = ∪ 𝐴)
133	132	fveq2d 6337	. . . . . . . . . . . . 13 ⊢ (𝑔:ℕ–onto→𝐴 → (vol‘∪ 𝑛 ∈ ℕ ((𝑔‘𝑛) ∖ ∪ 𝑙 ∈ (1..^𝑛)(𝑔‘𝑙))) = (vol‘∪ 𝐴))
134	133	adantr 466	. . . . . . . . . . . 12 ⊢ ((𝑔:ℕ–onto→𝐴 ∧ ∀𝑚 ∈ ℕ ((𝑔‘𝑚) ⊆ ℝ ∧ (vol*‘(𝑔‘𝑚)) = 0)) → (vol‘∪ 𝑛 ∈ ℕ ((𝑔‘𝑛) ∖ ∪ 𝑙 ∈ (1..^𝑛)(𝑔‘𝑙))) = (vol‘∪ 𝐴))
135	57	sseq1d 3782	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (𝑚 = 𝑛 → ((𝑔‘𝑚) ⊆ ℝ ↔ (𝑔‘𝑛) ⊆ ℝ))
136	57	fveq2d 6337	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (𝑚 = 𝑛 → (vol*‘(𝑔‘𝑚)) = (vol*‘(𝑔‘𝑛)))
137	136	eqeq1d 2773	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (𝑚 = 𝑛 → ((vol*‘(𝑔‘𝑚)) = 0 ↔ (vol*‘(𝑔‘𝑛)) = 0))
138	135, 137	anbi12d 610	. . . . . . . . . . . . . . . . . . . 20 ⊢ (𝑚 = 𝑛 → (((𝑔‘𝑚) ⊆ ℝ ∧ (vol*‘(𝑔‘𝑚)) = 0) ↔ ((𝑔‘𝑛) ⊆ ℝ ∧ (vol*‘(𝑔‘𝑛)) = 0)))
139	138	rspccva 3460	. . . . . . . . . . . . . . . . . . 19 ⊢ ((∀𝑚 ∈ ℕ ((𝑔‘𝑚) ⊆ ℝ ∧ (vol*‘(𝑔‘𝑚)) = 0) ∧ 𝑛 ∈ ℕ) → ((𝑔‘𝑛) ⊆ ℝ ∧ (vol*‘(𝑔‘𝑛)) = 0))
140		ssdifss 3893	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ ((𝑔‘𝑛) ⊆ ℝ → ((𝑔‘𝑛) ∖ ∪ 𝑙 ∈ (1..^𝑛)(𝑔‘𝑙)) ⊆ ℝ)
141	140	adantr 466	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (((𝑔‘𝑛) ⊆ ℝ ∧ (vol*‘(𝑔‘𝑛)) = 0) → ((𝑔‘𝑛) ∖ ∪ 𝑙 ∈ (1..^𝑛)(𝑔‘𝑙)) ⊆ ℝ)
142		difss 3889	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ ((𝑔‘𝑛) ∖ ∪ 𝑙 ∈ (1..^𝑛)(𝑔‘𝑙)) ⊆ (𝑔‘𝑛)
143		ovolssnul 23476	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ ((((𝑔‘𝑛) ∖ ∪ 𝑙 ∈ (1..^𝑛)(𝑔‘𝑙)) ⊆ (𝑔‘𝑛) ∧ (𝑔‘𝑛) ⊆ ℝ ∧ (vol*‘(𝑔‘𝑛)) = 0) → (vol*‘((𝑔‘𝑛) ∖ ∪ 𝑙 ∈ (1..^𝑛)(𝑔‘𝑙))) = 0)
144	142, 143	mp3an1 1559	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (((𝑔‘𝑛) ⊆ ℝ ∧ (vol*‘(𝑔‘𝑛)) = 0) → (vol*‘((𝑔‘𝑛) ∖ ∪ 𝑙 ∈ (1..^𝑛)(𝑔‘𝑙))) = 0)
145	141, 144	jca 497	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (((𝑔‘𝑛) ⊆ ℝ ∧ (vol*‘(𝑔‘𝑛)) = 0) → (((𝑔‘𝑛) ∖ ∪ 𝑙 ∈ (1..^𝑛)(𝑔‘𝑙)) ⊆ ℝ ∧ (vol*‘((𝑔‘𝑛) ∖ ∪ 𝑙 ∈ (1..^𝑛)(𝑔‘𝑙))) = 0))
146		nulmbl 23524	. . . . . . . . . . . . . . . . . . . . 21 ⊢ ((((𝑔‘𝑛) ∖ ∪ 𝑙 ∈ (1..^𝑛)(𝑔‘𝑙)) ⊆ ℝ ∧ (vol*‘((𝑔‘𝑛) ∖ ∪ 𝑙 ∈ (1..^𝑛)(𝑔‘𝑙))) = 0) → ((𝑔‘𝑛) ∖ ∪ 𝑙 ∈ (1..^𝑛)(𝑔‘𝑙)) ∈ dom vol)
147		mblvol 23519	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (((𝑔‘𝑛) ∖ ∪ 𝑙 ∈ (1..^𝑛)(𝑔‘𝑙)) ∈ dom vol → (vol‘((𝑔‘𝑛) ∖ ∪ 𝑙 ∈ (1..^𝑛)(𝑔‘𝑙))) = (vol*‘((𝑔‘𝑛) ∖ ∪ 𝑙 ∈ (1..^𝑛)(𝑔‘𝑙))))
148	145, 146, 147	3syl 18	. . . . . . . . . . . . . . . . . . . 20 ⊢ (((𝑔‘𝑛) ⊆ ℝ ∧ (vol*‘(𝑔‘𝑛)) = 0) → (vol‘((𝑔‘𝑛) ∖ ∪ 𝑙 ∈ (1..^𝑛)(𝑔‘𝑙))) = (vol*‘((𝑔‘𝑛) ∖ ∪ 𝑙 ∈ (1..^𝑛)(𝑔‘𝑙))))
149	148, 144	eqtrd 2805	. . . . . . . . . . . . . . . . . . 19 ⊢ (((𝑔‘𝑛) ⊆ ℝ ∧ (vol*‘(𝑔‘𝑛)) = 0) → (vol‘((𝑔‘𝑛) ∖ ∪ 𝑙 ∈ (1..^𝑛)(𝑔‘𝑙))) = 0)
150	139, 149	syl 17	. . . . . . . . . . . . . . . . . 18 ⊢ ((∀𝑚 ∈ ℕ ((𝑔‘𝑚) ⊆ ℝ ∧ (vol*‘(𝑔‘𝑚)) = 0) ∧ 𝑛 ∈ ℕ) → (vol‘((𝑔‘𝑛) ∖ ∪ 𝑙 ∈ (1..^𝑛)(𝑔‘𝑙))) = 0)
151	150	mpteq2dva 4879	. . . . . . . . . . . . . . . . 17 ⊢ (∀𝑚 ∈ ℕ ((𝑔‘𝑚) ⊆ ℝ ∧ (vol*‘(𝑔‘𝑚)) = 0) → (𝑛 ∈ ℕ ↦ (vol‘((𝑔‘𝑛) ∖ ∪ 𝑙 ∈ (1..^𝑛)(𝑔‘𝑙)))) = (𝑛 ∈ ℕ ↦ 0))
152	151	seqeq3d 13017	. . . . . . . . . . . . . . . 16 ⊢ (∀𝑚 ∈ ℕ ((𝑔‘𝑚) ⊆ ℝ ∧ (vol*‘(𝑔‘𝑚)) = 0) → seq1( + , (𝑛 ∈ ℕ ↦ (vol‘((𝑔‘𝑛) ∖ ∪ 𝑙 ∈ (1..^𝑛)(𝑔‘𝑙))))) = seq1( + , (𝑛 ∈ ℕ ↦ 0)))
153	152	rneqd 5492	. . . . . . . . . . . . . . 15 ⊢ (∀𝑚 ∈ ℕ ((𝑔‘𝑚) ⊆ ℝ ∧ (vol*‘(𝑔‘𝑚)) = 0) → ran seq1( + , (𝑛 ∈ ℕ ↦ (vol‘((𝑔‘𝑛) ∖ ∪ 𝑙 ∈ (1..^𝑛)(𝑔‘𝑙))))) = ran seq1( + , (𝑛 ∈ ℕ ↦ 0)))
154	153	supeq1d 8509	. . . . . . . . . . . . . 14 ⊢ (∀𝑚 ∈ ℕ ((𝑔‘𝑚) ⊆ ℝ ∧ (vol*‘(𝑔‘𝑚)) = 0) → sup(ran seq1( + , (𝑛 ∈ ℕ ↦ (vol‘((𝑔‘𝑛) ∖ ∪ 𝑙 ∈ (1..^𝑛)(𝑔‘𝑙))))), ℝ*, < ) = sup(ran seq1( + , (𝑛 ∈ ℕ ↦ 0)), ℝ*, < ))
155		0cn 10235	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ 0 ∈ ℂ
156		ser1const 13065	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ ((0 ∈ ℂ ∧ 𝑚 ∈ ℕ) → (seq1( + , (ℕ × {0}))‘𝑚) = (𝑚 · 0))
157	155, 156	mpan 664	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (𝑚 ∈ ℕ → (seq1( + , (ℕ × {0}))‘𝑚) = (𝑚 · 0))
158		nncn 11231	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (𝑚 ∈ ℕ → 𝑚 ∈ ℂ)
159	158	mul01d 10438	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (𝑚 ∈ ℕ → (𝑚 · 0) = 0)
160	157, 159	eqtrd 2805	. . . . . . . . . . . . . . . . . . . 20 ⊢ (𝑚 ∈ ℕ → (seq1( + , (ℕ × {0}))‘𝑚) = 0)
161	160	mpteq2ia 4875	. . . . . . . . . . . . . . . . . . 19 ⊢ (𝑚 ∈ ℕ ↦ (seq1( + , (ℕ × {0}))‘𝑚)) = (𝑚 ∈ ℕ ↦ 0)
162		fconstmpt 5304	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (ℕ × {0}) = (𝑛 ∈ ℕ ↦ 0)
163		seqeq3 13014	. . . . . . . . . . . . . . . . . . . . 21 ⊢ ((ℕ × {0}) = (𝑛 ∈ ℕ ↦ 0) → seq1( + , (ℕ × {0})) = seq1( + , (𝑛 ∈ ℕ ↦ 0)))
164	162, 163	ax-mp 5	. . . . . . . . . . . . . . . . . . . 20 ⊢ seq1( + , (ℕ × {0})) = seq1( + , (𝑛 ∈ ℕ ↦ 0))
165		1z 11610	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ 1 ∈ ℤ
166		seqfn 13021	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (1 ∈ ℤ → seq1( + , (ℕ × {0})) Fn (ℤ≥‘1))
167	165, 166	ax-mp 5	. . . . . . . . . . . . . . . . . . . . 21 ⊢ seq1( + , (ℕ × {0})) Fn (ℤ≥‘1)
168		nnuz 11926	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ ℕ = (ℤ≥‘1)
169	168	fneq2i 6127	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (seq1( + , (ℕ × {0})) Fn ℕ ↔ seq1( + , (ℕ × {0})) Fn (ℤ≥‘1))
170		dffn5 6384	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (seq1( + , (ℕ × {0})) Fn ℕ ↔ seq1( + , (ℕ × {0})) = (𝑚 ∈ ℕ ↦ (seq1( + , (ℕ × {0}))‘𝑚)))
171	169, 170	bitr3i 266	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (seq1( + , (ℕ × {0})) Fn (ℤ≥‘1) ↔ seq1( + , (ℕ × {0})) = (𝑚 ∈ ℕ ↦ (seq1( + , (ℕ × {0}))‘𝑚)))
172	167, 171	mpbi 220	. . . . . . . . . . . . . . . . . . . 20 ⊢ seq1( + , (ℕ × {0})) = (𝑚 ∈ ℕ ↦ (seq1( + , (ℕ × {0}))‘𝑚))
173	164, 172	eqtr3i 2795	. . . . . . . . . . . . . . . . . . 19 ⊢ seq1( + , (𝑛 ∈ ℕ ↦ 0)) = (𝑚 ∈ ℕ ↦ (seq1( + , (ℕ × {0}))‘𝑚))
174		fconstmpt 5304	. . . . . . . . . . . . . . . . . . 19 ⊢ (ℕ × {0}) = (𝑚 ∈ ℕ ↦ 0)
175	161, 173, 174	3eqtr4i 2803	. . . . . . . . . . . . . . . . . 18 ⊢ seq1( + , (𝑛 ∈ ℕ ↦ 0)) = (ℕ × {0})
176	175	rneqi 5491	. . . . . . . . . . . . . . . . 17 ⊢ ran seq1( + , (𝑛 ∈ ℕ ↦ 0)) = ran (ℕ × {0})
177		1nn 11234	. . . . . . . . . . . . . . . . . 18 ⊢ 1 ∈ ℕ
178		ne0i 4070	. . . . . . . . . . . . . . . . . 18 ⊢ (1 ∈ ℕ → ℕ ≠ ∅)
179		rnxp 5706	. . . . . . . . . . . . . . . . . 18 ⊢ (ℕ ≠ ∅ → ran (ℕ × {0}) = {0})
180	177, 178, 179	mp2b 10	. . . . . . . . . . . . . . . . 17 ⊢ ran (ℕ × {0}) = {0}
181	176, 180	eqtri 2793	. . . . . . . . . . . . . . . 16 ⊢ ran seq1( + , (𝑛 ∈ ℕ ↦ 0)) = {0}
182	181	supeq1i 8510	. . . . . . . . . . . . . . 15 ⊢ sup(ran seq1( + , (𝑛 ∈ ℕ ↦ 0)), ℝ*, < ) = sup({0}, ℝ*, < )
183		xrltso 12180	. . . . . . . . . . . . . . . 16 ⊢ < Or ℝ*
184		0xr 10289	. . . . . . . . . . . . . . . 16 ⊢ 0 ∈ ℝ*
185		supsn 8535	. . . . . . . . . . . . . . . 16 ⊢ (( < Or ℝ* ∧ 0 ∈ ℝ*) → sup({0}, ℝ*, < ) = 0)
186	183, 184, 185	mp2an 666	. . . . . . . . . . . . . . 15 ⊢ sup({0}, ℝ*, < ) = 0
187	182, 186	eqtri 2793	. . . . . . . . . . . . . 14 ⊢ sup(ran seq1( + , (𝑛 ∈ ℕ ↦ 0)), ℝ*, < ) = 0
188	154, 187	syl6eq 2821	. . . . . . . . . . . . 13 ⊢ (∀𝑚 ∈ ℕ ((𝑔‘𝑚) ⊆ ℝ ∧ (vol*‘(𝑔‘𝑚)) = 0) → sup(ran seq1( + , (𝑛 ∈ ℕ ↦ (vol‘((𝑔‘𝑛) ∖ ∪ 𝑙 ∈ (1..^𝑛)(𝑔‘𝑙))))), ℝ*, < ) = 0)
189	188	adantl 467	. . . . . . . . . . . 12 ⊢ ((𝑔:ℕ–onto→𝐴 ∧ ∀𝑚 ∈ ℕ ((𝑔‘𝑚) ⊆ ℝ ∧ (vol*‘(𝑔‘𝑚)) = 0)) → sup(ran seq1( + , (𝑛 ∈ ℕ ↦ (vol‘((𝑔‘𝑛) ∖ ∪ 𝑙 ∈ (1..^𝑛)(𝑔‘𝑙))))), ℝ*, < ) = 0)
190	125, 134, 189	3eqtr3rd 2814	. . . . . . . . . . 11 ⊢ ((𝑔:ℕ–onto→𝐴 ∧ ∀𝑚 ∈ ℕ ((𝑔‘𝑚) ⊆ ℝ ∧ (vol*‘(𝑔‘𝑚)) = 0)) → 0 = (vol‘∪ 𝐴))
191	190	ex 397	. . . . . . . . . 10 ⊢ (𝑔:ℕ–onto→𝐴 → (∀𝑚 ∈ ℕ ((𝑔‘𝑚) ⊆ ℝ ∧ (vol*‘(𝑔‘𝑚)) = 0) → 0 = (vol‘∪ 𝐴)))
192	39, 191	sylbid 230	. . . . . . . . 9 ⊢ (𝑔:ℕ–onto→𝐴 → (∀𝑥 ∈ 𝐴 (𝑥 ⊆ ℝ ∧ (vol*‘𝑥) = 0) → 0 = (vol‘∪ 𝐴)))
193	28, 192	syl5 34	. . . . . . . 8 ⊢ (𝑔:ℕ–onto→𝐴 → ((∀𝑥 ∈ 𝐴 𝑥 ≼ ℕ ∧ ∪ 𝐴 ⊆ ℝ) → 0 = (vol‘∪ 𝐴)))
194	193	exlimiv 2010	. . . . . . 7 ⊢ (∃𝑔 𝑔:ℕ–onto→𝐴 → ((∀𝑥 ∈ 𝐴 𝑥 ≼ ℕ ∧ ∪ 𝐴 ⊆ ℝ) → 0 = (vol‘∪ 𝐴)))
195	18, 194	syl 17	. . . . . 6 ⊢ ((𝐴 ≠ ∅ ∧ 𝐴 ≼ ℕ) → ((∀𝑥 ∈ 𝐴 𝑥 ≼ ℕ ∧ ∪ 𝐴 ⊆ ℝ) → 0 = (vol‘∪ 𝐴)))
196	195	expimpd 441	. . . . 5 ⊢ (𝐴 ≠ ∅ → ((𝐴 ≼ ℕ ∧ (∀𝑥 ∈ 𝐴 𝑥 ≼ ℕ ∧ ∪ 𝐴 ⊆ ℝ)) → 0 = (vol‘∪ 𝐴)))
197	11, 196	pm2.61ine 3026	. . . 4 ⊢ ((𝐴 ≼ ℕ ∧ (∀𝑥 ∈ 𝐴 𝑥 ≼ ℕ ∧ ∪ 𝐴 ⊆ ℝ)) → 0 = (vol‘∪ 𝐴))
198		renepnf 10290	. . . . . . 7 ⊢ (0 ∈ ℝ → 0 ≠ +∞)
199	48, 198	mp1i 13	. . . . . 6 ⊢ (∪ 𝐴 = ℝ → 0 ≠ +∞)
200		fveq2 6333	. . . . . . 7 ⊢ (∪ 𝐴 = ℝ → (vol‘∪ 𝐴) = (vol‘ℝ))
201		rembl 23529	. . . . . . . . 9 ⊢ ℝ ∈ dom vol
202		mblvol 23519	. . . . . . . . 9 ⊢ (ℝ ∈ dom vol → (vol‘ℝ) = (vol*‘ℝ))
203	201, 202	ax-mp 5	. . . . . . . 8 ⊢ (vol‘ℝ) = (vol*‘ℝ)
204		ovolre 23514	. . . . . . . 8 ⊢ (vol*‘ℝ) = +∞
205	203, 204	eqtri 2793	. . . . . . 7 ⊢ (vol‘ℝ) = +∞
206	200, 205	syl6eq 2821	. . . . . 6 ⊢ (∪ 𝐴 = ℝ → (vol‘∪ 𝐴) = +∞)
207	199, 206	neeqtrrd 3017	. . . . 5 ⊢ (∪ 𝐴 = ℝ → 0 ≠ (vol‘∪ 𝐴))
208	207	necon2i 2977	. . . 4 ⊢ (0 = (vol‘∪ 𝐴) → ∪ 𝐴 ≠ ℝ)
209	197, 208	syl 17	. . 3 ⊢ ((𝐴 ≼ ℕ ∧ (∀𝑥 ∈ 𝐴 𝑥 ≼ ℕ ∧ ∪ 𝐴 ⊆ ℝ)) → ∪ 𝐴 ≠ ℝ)
210	209	expr 444	. 2 ⊢ ((𝐴 ≼ ℕ ∧ ∀𝑥 ∈ 𝐴 𝑥 ≼ ℕ) → (∪ 𝐴 ⊆ ℝ → ∪ 𝐴 ≠ ℝ))
211		eqimss 3807	. . 3 ⊢ (∪ 𝐴 = ℝ → ∪ 𝐴 ⊆ ℝ)
212	211	necon3bi 2969	. 2 ⊢ (¬ ∪ 𝐴 ⊆ ℝ → ∪ 𝐴 ≠ ℝ)
213	210, 212	pm2.61d1 172	1 ⊢ ((𝐴 ≼ ℕ ∧ ∀𝑥 ∈ 𝐴 𝑥 ≼ ℕ) → ∪ 𝐴 ≠ ℝ)

Syntax hints:   → wi 4   ↔ wb 196   ∧ wa 382   = wceq 1631  ∃wex 1852   ∈ wcel 2145   ≠ wne 2943  ∀wral 3061  Vcvv 3351   ∖ cdif 3721   ⊆ wss 3724  ∅c0 4064  {csn 4317  ∪ cuni 4575  ∪ ciun 4655  Disj wdisj 4755   class class class wbr 4787   ↦ cmpt 4864   Or wor 5170   × cxp 5248  dom cdm 5250  ran crn 5251   “ cima 5253  Fun wfun 6026   Fn wfn 6027  –onto→wfo 6030  ‘cfv 6032  (class class class)co 6794   ≼ cdom 8108   ≺ csdm 8109  supcsup 8503  ℂcc 10137  ℝcr 10138  0cc0 10139  1c1 10140   + caddc 10142   · cmul 10144  +∞cpnf 10274  ℝ^*cxr 10276   < clt 10277  ℕcn 11223  ℤcz 11580  ℤ_≥cuz 11889  ..^cfzo 12674  seqcseq 13009  vol*covol 23451  volcvol 23452

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1870  ax-4 1885  ax-5 1991  ax-6 2057  ax-7 2093  ax-8 2147  ax-9 2154  ax-10 2174  ax-11 2190  ax-12 2203  ax-13 2408  ax-ext 2751  ax-rep 4905  ax-sep 4916  ax-nul 4924  ax-pow 4975  ax-pr 5035  ax-un 7097  ax-inf2 8703  ax-cnex 10195  ax-resscn 10196  ax-1cn 10197  ax-icn 10198  ax-addcl 10199  ax-addrcl 10200  ax-mulcl 10201  ax-mulrcl 10202  ax-mulcom 10203  ax-addass 10204  ax-mulass 10205  ax-distr 10206  ax-i2m1 10207  ax-1ne0 10208  ax-1rid 10209  ax-rnegex 10210  ax-rrecex 10211  ax-cnre 10212  ax-pre-lttri 10213  ax-pre-lttrn 10214  ax-pre-ltadd 10215  ax-pre-mulgt0 10216  ax-pre-sup 10217

This theorem depends on definitions:  df-bi 197  df-an 383  df-or 829  df-3or 1072  df-3an 1073  df-tru 1634  df-fal 1637  df-ex 1853  df-nf 1858  df-sb 2050  df-eu 2622  df-mo 2623  df-clab 2758  df-cleq 2764  df-clel 2767  df-nfc 2902  df-ne 2944  df-nel 3047  df-ral 3066  df-rex 3067  df-reu 3068  df-rmo 3069  df-rab 3070  df-v 3353  df-sbc 3589  df-csb 3684  df-dif 3727  df-un 3729  df-in 3731  df-ss 3738  df-pss 3740  df-nul 4065  df-if 4227  df-pw 4300  df-sn 4318  df-pr 4320  df-tp 4322  df-op 4324  df-uni 4576  df-int 4613  df-iun 4657  df-disj 4756  df-br 4788  df-opab 4848  df-mpt 4865  df-tr 4888  df-id 5158  df-eprel 5163  df-po 5171  df-so 5172  df-fr 5209  df-se 5210  df-we 5211  df-xp 5256  df-rel 5257  df-cnv 5258  df-co 5259  df-dm 5260  df-rn 5261  df-res 5262  df-ima 5263  df-pred 5824  df-ord 5870  df-on 5871  df-lim 5872  df-suc 5873  df-iota 5995  df-fun 6034  df-fn 6035  df-f 6036  df-f1 6037  df-fo 6038  df-f1o 6039  df-fv 6040  df-isom 6041  df-riota 6755  df-ov 6797  df-oprab 6798  df-mpt2 6799  df-of 7045  df-om 7214  df-1st 7316  df-2nd 7317  df-wrecs 7560  df-recs 7622  df-rdg 7660  df-1o 7714  df-2o 7715  df-oadd 7718  df-er 7897  df-map 8012  df-en 8111  df-dom 8112  df-sdom 8113  df-fin 8114  df-fi 8474  df-sup 8505  df-inf 8506  df-oi 8572  df-card 8966  df-cda 9193  df-pnf 10279  df-mnf 10280  df-xr 10281  df-ltxr 10282  df-le 10283  df-sub 10471  df-neg 10472  df-div 10888  df-nn 11224  df-2 11282  df-3 11283  df-n0 11496  df-z 11581  df-uz 11890  df-q 11993  df-rp 12037  df-xneg 12152  df-xadd 12153  df-xmul 12154  df-ioo 12385  df-ico 12387  df-icc 12388  df-fz 12535  df-fzo 12675  df-fl 12802  df-seq 13010  df-exp 13069  df-hash 13323  df-cj 14048  df-re 14049  df-im 14050  df-sqrt 14184  df-abs 14185  df-clim 14428  df-sum 14626  df-rest 16292  df-topgen 16313  df-psmet 19954  df-xmet 19955  df-met 19956  df-bl 19957  df-mopn 19958  df-top 20920  df-topon 20937  df-bases 20972  df-cmp 21412  df-ovol 23453  df-vol 23454

This theorem is referenced by: (None)