Theorem voliunnfl 35558

Description: voliun 24451 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 4830	. . . . . . . . 9 ⊢ (𝐴 = ∅ → ∪ 𝐴 = ∪ ∅)
2		uni0 4849	. . . . . . . . 9 ⊢ ∪ ∅ = ∅
3	1, 2	eqtrdi 2794	. . . . . . . 8 ⊢ (𝐴 = ∅ → ∪ 𝐴 = ∅)
4	3	fveq2d 6721	. . . . . . 7 ⊢ (𝐴 = ∅ → (vol‘∪ 𝐴) = (vol‘∅))
5		0mbl 24436	. . . . . . . . 9 ⊢ ∅ ∈ dom vol
6		mblvol 24427	. . . . . . . . 9 ⊢ (∅ ∈ dom vol → (vol‘∅) = (vol*‘∅))
7	5, 6	ax-mp 5	. . . . . . . 8 ⊢ (vol‘∅) = (vol*‘∅)
8		ovol0 24390	. . . . . . . 8 ⊢ (vol*‘∅) = 0
9	7, 8	eqtri 2765	. . . . . . 7 ⊢ (vol‘∅) = 0
10	4, 9	eqtr2di 2795	. . . . . 6 ⊢ (𝐴 = ∅ → 0 = (vol‘∪ 𝐴))
11	10	a1d 25	. . . . 5 ⊢ (𝐴 = ∅ → ((𝐴 ≼ ℕ ∧ (∀𝑥 ∈ 𝐴 𝑥 ≼ ℕ ∧ ∪ 𝐴 ⊆ ℝ)) → 0 = (vol‘∪ 𝐴)))
12		reldom 8632	. . . . . . . . . . 11 ⊢ Rel ≼
13	12	brrelex1i 5605	. . . . . . . . . 10 ⊢ (𝐴 ≼ ℕ → 𝐴 ∈ V)
14		0sdomg 8775	. . . . . . . . . 10 ⊢ (𝐴 ∈ V → (∅ ≺ 𝐴 ↔ 𝐴 ≠ ∅))
15	13, 14	syl 17	. . . . . . . . 9 ⊢ (𝐴 ≼ ℕ → (∅ ≺ 𝐴 ↔ 𝐴 ≠ ∅))
16	15	biimparc 483	. . . . . . . 8 ⊢ ((𝐴 ≠ ∅ ∧ 𝐴 ≼ ℕ) → ∅ ≺ 𝐴)
17		fodomr 8797	. . . . . . . 8 ⊢ ((∅ ≺ 𝐴 ∧ 𝐴 ≼ ℕ) → ∃𝑔 𝑔:ℕ–onto→𝐴)
18	16, 17	sylancom 591	. . . . . . 7 ⊢ ((𝐴 ≠ ∅ ∧ 𝐴 ≼ ℕ) → ∃𝑔 𝑔:ℕ–onto→𝐴)
19		unissb 4853	. . . . . . . . . . . . 13 ⊢ (∪ 𝐴 ⊆ ℝ ↔ ∀𝑥 ∈ 𝐴 𝑥 ⊆ ℝ)
20	19	anbi1i 627	. . . . . . . . . . . 12 ⊢ ((∪ 𝐴 ⊆ ℝ ∧ ∀𝑥 ∈ 𝐴 𝑥 ≼ ℕ) ↔ (∀𝑥 ∈ 𝐴 𝑥 ⊆ ℝ ∧ ∀𝑥 ∈ 𝐴 𝑥 ≼ ℕ))
21		r19.26 3092	. . . . . . . . . . . 12 ⊢ (∀𝑥 ∈ 𝐴 (𝑥 ⊆ ℝ ∧ 𝑥 ≼ ℕ) ↔ (∀𝑥 ∈ 𝐴 𝑥 ⊆ ℝ ∧ ∀𝑥 ∈ 𝐴 𝑥 ≼ ℕ))
22	20, 21	bitr4i 281	. . . . . . . . . . 11 ⊢ ((∪ 𝐴 ⊆ ℝ ∧ ∀𝑥 ∈ 𝐴 𝑥 ≼ ℕ) ↔ ∀𝑥 ∈ 𝐴 (𝑥 ⊆ ℝ ∧ 𝑥 ≼ ℕ))
23		ovolctb2 24389	. . . . . . . . . . . . . 14 ⊢ ((𝑥 ⊆ ℝ ∧ 𝑥 ≼ ℕ) → (vol*‘𝑥) = 0)
24	23	ex 416	. . . . . . . . . . . . 13 ⊢ (𝑥 ⊆ ℝ → (𝑥 ≼ ℕ → (vol*‘𝑥) = 0))
25	24	imdistani 572	. . . . . . . . . . . 12 ⊢ ((𝑥 ⊆ ℝ ∧ 𝑥 ≼ ℕ) → (𝑥 ⊆ ℝ ∧ (vol*‘𝑥) = 0))
26	25	ralimi 3083	. . . . . . . . . . 11 ⊢ (∀𝑥 ∈ 𝐴 (𝑥 ⊆ ℝ ∧ 𝑥 ≼ ℕ) → ∀𝑥 ∈ 𝐴 (𝑥 ⊆ ℝ ∧ (vol*‘𝑥) = 0))
27	22, 26	sylbi 220	. . . . . . . . . 10 ⊢ ((∪ 𝐴 ⊆ ℝ ∧ ∀𝑥 ∈ 𝐴 𝑥 ≼ ℕ) → ∀𝑥 ∈ 𝐴 (𝑥 ⊆ ℝ ∧ (vol*‘𝑥) = 0))
28	27	ancoms 462	. . . . . . . . 9 ⊢ ((∀𝑥 ∈ 𝐴 𝑥 ≼ ℕ ∧ ∪ 𝐴 ⊆ ℝ) → ∀𝑥 ∈ 𝐴 (𝑥 ⊆ ℝ ∧ (vol*‘𝑥) = 0))
29		foima 6638	. . . . . . . . . . . 12 ⊢ (𝑔:ℕ–onto→𝐴 → (𝑔 “ ℕ) = 𝐴)
30	29	raleqdv 3325	. . . . . . . . . . 11 ⊢ (𝑔:ℕ–onto→𝐴 → (∀𝑥 ∈ (𝑔 “ ℕ)(𝑥 ⊆ ℝ ∧ (vol*‘𝑥) = 0) ↔ ∀𝑥 ∈ 𝐴 (𝑥 ⊆ ℝ ∧ (vol*‘𝑥) = 0)))
31		fofn 6635	. . . . . . . . . . . 12 ⊢ (𝑔:ℕ–onto→𝐴 → 𝑔 Fn ℕ)
32		ssid 3923	. . . . . . . . . . . 12 ⊢ ℕ ⊆ ℕ
33		sseq1 3926	. . . . . . . . . . . . . 14 ⊢ (𝑥 = (𝑔‘𝑚) → (𝑥 ⊆ ℝ ↔ (𝑔‘𝑚) ⊆ ℝ))
34		fveqeq2 6726	. . . . . . . . . . . . . 14 ⊢ (𝑥 = (𝑔‘𝑚) → ((vol*‘𝑥) = 0 ↔ (vol*‘(𝑔‘𝑚)) = 0))
35	33, 34	anbi12d 634	. . . . . . . . . . . . 13 ⊢ (𝑥 = (𝑔‘𝑚) → ((𝑥 ⊆ ℝ ∧ (vol*‘𝑥) = 0) ↔ ((𝑔‘𝑚) ⊆ ℝ ∧ (vol*‘(𝑔‘𝑚)) = 0)))
36	35	ralima 7054	. . . . . . . . . . . 12 ⊢ ((𝑔 Fn ℕ ∧ ℕ ⊆ ℕ) → (∀𝑥 ∈ (𝑔 “ ℕ)(𝑥 ⊆ ℝ ∧ (vol*‘𝑥) = 0) ↔ ∀𝑚 ∈ ℕ ((𝑔‘𝑚) ⊆ ℝ ∧ (vol*‘(𝑔‘𝑚)) = 0)))
37	31, 32, 36	sylancl 589	. . . . . . . . . . 11 ⊢ (𝑔:ℕ–onto→𝐴 → (∀𝑥 ∈ (𝑔 “ ℕ)(𝑥 ⊆ ℝ ∧ (vol*‘𝑥) = 0) ↔ ∀𝑚 ∈ ℕ ((𝑔‘𝑚) ⊆ ℝ ∧ (vol*‘(𝑔‘𝑚)) = 0)))
38	30, 37	bitr3d 284	. . . . . . . . . 10 ⊢ (𝑔:ℕ–onto→𝐴 → (∀𝑥 ∈ 𝐴 (𝑥 ⊆ ℝ ∧ (vol*‘𝑥) = 0) ↔ ∀𝑚 ∈ ℕ ((𝑔‘𝑚) ⊆ ℝ ∧ (vol*‘(𝑔‘𝑚)) = 0)))
39		difss 4046	. . . . . . . . . . . . . . . . . 18 ⊢ ((𝑔‘𝑚) ∖ ∪ 𝑙 ∈ (1..^𝑚)(𝑔‘𝑙)) ⊆ (𝑔‘𝑚)
40		ovolssnul 24384	. . . . . . . . . . . . . . . . . 18 ⊢ ((((𝑔‘𝑚) ∖ ∪ 𝑙 ∈ (1..^𝑚)(𝑔‘𝑙)) ⊆ (𝑔‘𝑚) ∧ (𝑔‘𝑚) ⊆ ℝ ∧ (vol*‘(𝑔‘𝑚)) = 0) → (vol*‘((𝑔‘𝑚) ∖ ∪ 𝑙 ∈ (1..^𝑚)(𝑔‘𝑙))) = 0)
41	39, 40	mp3an1 1450	. . . . . . . . . . . . . . . . 17 ⊢ (((𝑔‘𝑚) ⊆ ℝ ∧ (vol*‘(𝑔‘𝑚)) = 0) → (vol*‘((𝑔‘𝑚) ∖ ∪ 𝑙 ∈ (1..^𝑚)(𝑔‘𝑙))) = 0)
42		ssdifss 4050	. . . . . . . . . . . . . . . . . 18 ⊢ ((𝑔‘𝑚) ⊆ ℝ → ((𝑔‘𝑚) ∖ ∪ 𝑙 ∈ (1..^𝑚)(𝑔‘𝑙)) ⊆ ℝ)
43		nulmbl 24432	. . . . . . . . . . . . . . . . . . 19 ⊢ ((((𝑔‘𝑚) ∖ ∪ 𝑙 ∈ (1..^𝑚)(𝑔‘𝑙)) ⊆ ℝ ∧ (vol*‘((𝑔‘𝑚) ∖ ∪ 𝑙 ∈ (1..^𝑚)(𝑔‘𝑙))) = 0) → ((𝑔‘𝑚) ∖ ∪ 𝑙 ∈ (1..^𝑚)(𝑔‘𝑙)) ∈ dom vol)
44		mblvol 24427	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ (((𝑔‘𝑚) ∖ ∪ 𝑙 ∈ (1..^𝑚)(𝑔‘𝑙)) ∈ dom vol → (vol‘((𝑔‘𝑚) ∖ ∪ 𝑙 ∈ (1..^𝑚)(𝑔‘𝑙))) = (vol*‘((𝑔‘𝑚) ∖ ∪ 𝑙 ∈ (1..^𝑚)(𝑔‘𝑙))))
45	44	eqeq1d 2739	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ (((𝑔‘𝑚) ∖ ∪ 𝑙 ∈ (1..^𝑚)(𝑔‘𝑙)) ∈ dom vol → ((vol‘((𝑔‘𝑚) ∖ ∪ 𝑙 ∈ (1..^𝑚)(𝑔‘𝑙))) = 0 ↔ (vol*‘((𝑔‘𝑚) ∖ ∪ 𝑙 ∈ (1..^𝑚)(𝑔‘𝑙))) = 0))
46	45	biimpar 481	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ ((((𝑔‘𝑚) ∖ ∪ 𝑙 ∈ (1..^𝑚)(𝑔‘𝑙)) ∈ dom vol ∧ (vol*‘((𝑔‘𝑚) ∖ ∪ 𝑙 ∈ (1..^𝑚)(𝑔‘𝑙))) = 0) → (vol‘((𝑔‘𝑚) ∖ ∪ 𝑙 ∈ (1..^𝑚)(𝑔‘𝑙))) = 0)
47		0re 10835	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ 0 ∈ ℝ
48	46, 47	eqeltrdi 2846	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ ((((𝑔‘𝑚) ∖ ∪ 𝑙 ∈ (1..^𝑚)(𝑔‘𝑙)) ∈ dom vol ∧ (vol*‘((𝑔‘𝑚) ∖ ∪ 𝑙 ∈ (1..^𝑚)(𝑔‘𝑙))) = 0) → (vol‘((𝑔‘𝑚) ∖ ∪ 𝑙 ∈ (1..^𝑚)(𝑔‘𝑙))) ∈ ℝ)
49	48	expcom 417	. . . . . . . . . . . . . . . . . . . . 21 ⊢ ((vol*‘((𝑔‘𝑚) ∖ ∪ 𝑙 ∈ (1..^𝑚)(𝑔‘𝑙))) = 0 → (((𝑔‘𝑚) ∖ ∪ 𝑙 ∈ (1..^𝑚)(𝑔‘𝑙)) ∈ dom vol → (vol‘((𝑔‘𝑚) ∖ ∪ 𝑙 ∈ (1..^𝑚)(𝑔‘𝑙))) ∈ ℝ))
50	49	ancld 554	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((vol*‘((𝑔‘𝑚) ∖ ∪ 𝑙 ∈ (1..^𝑚)(𝑔‘𝑙))) = 0 → (((𝑔‘𝑚) ∖ ∪ 𝑙 ∈ (1..^𝑚)(𝑔‘𝑙)) ∈ dom vol → (((𝑔‘𝑚) ∖ ∪ 𝑙 ∈ (1..^𝑚)(𝑔‘𝑙)) ∈ dom vol ∧ (vol‘((𝑔‘𝑚) ∖ ∪ 𝑙 ∈ (1..^𝑚)(𝑔‘𝑙))) ∈ ℝ)))
51	50	adantl 485	. . . . . . . . . . . . . . . . . . 19 ⊢ ((((𝑔‘𝑚) ∖ ∪ 𝑙 ∈ (1..^𝑚)(𝑔‘𝑙)) ⊆ ℝ ∧ (vol*‘((𝑔‘𝑚) ∖ ∪ 𝑙 ∈ (1..^𝑚)(𝑔‘𝑙))) = 0) → (((𝑔‘𝑚) ∖ ∪ 𝑙 ∈ (1..^𝑚)(𝑔‘𝑙)) ∈ dom vol → (((𝑔‘𝑚) ∖ ∪ 𝑙 ∈ (1..^𝑚)(𝑔‘𝑙)) ∈ dom vol ∧ (vol‘((𝑔‘𝑚) ∖ ∪ 𝑙 ∈ (1..^𝑚)(𝑔‘𝑙))) ∈ ℝ)))
52	43, 51	mpd 15	. . . . . . . . . . . . . . . . . 18 ⊢ ((((𝑔‘𝑚) ∖ ∪ 𝑙 ∈ (1..^𝑚)(𝑔‘𝑙)) ⊆ ℝ ∧ (vol*‘((𝑔‘𝑚) ∖ ∪ 𝑙 ∈ (1..^𝑚)(𝑔‘𝑙))) = 0) → (((𝑔‘𝑚) ∖ ∪ 𝑙 ∈ (1..^𝑚)(𝑔‘𝑙)) ∈ dom vol ∧ (vol‘((𝑔‘𝑚) ∖ ∪ 𝑙 ∈ (1..^𝑚)(𝑔‘𝑙))) ∈ ℝ))
53	42, 52	sylan 583	. . . . . . . . . . . . . . . . 17 ⊢ (((𝑔‘𝑚) ⊆ ℝ ∧ (vol*‘((𝑔‘𝑚) ∖ ∪ 𝑙 ∈ (1..^𝑚)(𝑔‘𝑙))) = 0) → (((𝑔‘𝑚) ∖ ∪ 𝑙 ∈ (1..^𝑚)(𝑔‘𝑙)) ∈ dom vol ∧ (vol‘((𝑔‘𝑚) ∖ ∪ 𝑙 ∈ (1..^𝑚)(𝑔‘𝑙))) ∈ ℝ))
54	41, 53	syldan 594	. . . . . . . . . . . . . . . 16 ⊢ (((𝑔‘𝑚) ⊆ ℝ ∧ (vol*‘(𝑔‘𝑚)) = 0) → (((𝑔‘𝑚) ∖ ∪ 𝑙 ∈ (1..^𝑚)(𝑔‘𝑙)) ∈ dom vol ∧ (vol‘((𝑔‘𝑚) ∖ ∪ 𝑙 ∈ (1..^𝑚)(𝑔‘𝑙))) ∈ ℝ))
55	54	ralimi 3083	. . . . . . . . . . . . . . 15 ⊢ (∀𝑚 ∈ ℕ ((𝑔‘𝑚) ⊆ ℝ ∧ (vol*‘(𝑔‘𝑚)) = 0) → ∀𝑚 ∈ ℕ (((𝑔‘𝑚) ∖ ∪ 𝑙 ∈ (1..^𝑚)(𝑔‘𝑙)) ∈ dom vol ∧ (vol‘((𝑔‘𝑚) ∖ ∪ 𝑙 ∈ (1..^𝑚)(𝑔‘𝑙))) ∈ ℝ))
56		fveq2 6717	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (𝑚 = 𝑛 → (𝑔‘𝑚) = (𝑔‘𝑛))
57		oveq2 7221	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (𝑚 = 𝑛 → (1..^𝑚) = (1..^𝑛))
58	57	iuneq1d 4931	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (𝑚 = 𝑛 → ∪ 𝑙 ∈ (1..^𝑚)(𝑔‘𝑙) = ∪ 𝑙 ∈ (1..^𝑛)(𝑔‘𝑙))
59	56, 58	difeq12d 4038	. . . . . . . . . . . . . . . . . . . 20 ⊢ (𝑚 = 𝑛 → ((𝑔‘𝑚) ∖ ∪ 𝑙 ∈ (1..^𝑚)(𝑔‘𝑙)) = ((𝑔‘𝑛) ∖ ∪ 𝑙 ∈ (1..^𝑛)(𝑔‘𝑙)))
60		eqid 2737	. . . . . . . . . . . . . . . . . . . 20 ⊢ (𝑚 ∈ ℕ ↦ ((𝑔‘𝑚) ∖ ∪ 𝑙 ∈ (1..^𝑚)(𝑔‘𝑙))) = (𝑚 ∈ ℕ ↦ ((𝑔‘𝑚) ∖ ∪ 𝑙 ∈ (1..^𝑚)(𝑔‘𝑙)))
61		fvex 6730	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (𝑔‘𝑛) ∈ V
62		difexg 5220	. . . . . . . . . . . . . . . . . . . . 21 ⊢ ((𝑔‘𝑛) ∈ V → ((𝑔‘𝑛) ∖ ∪ 𝑙 ∈ (1..^𝑛)(𝑔‘𝑙)) ∈ V)
63	61, 62	ax-mp 5	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((𝑔‘𝑛) ∖ ∪ 𝑙 ∈ (1..^𝑛)(𝑔‘𝑙)) ∈ V
64	59, 60, 63	fvmpt 6818	. . . . . . . . . . . . . . . . . . 19 ⊢ (𝑛 ∈ ℕ → ((𝑚 ∈ ℕ ↦ ((𝑔‘𝑚) ∖ ∪ 𝑙 ∈ (1..^𝑚)(𝑔‘𝑙)))‘𝑛) = ((𝑔‘𝑛) ∖ ∪ 𝑙 ∈ (1..^𝑛)(𝑔‘𝑙)))
65	64	eleq1d 2822	. . . . . . . . . . . . . . . . . 18 ⊢ (𝑛 ∈ ℕ → (((𝑚 ∈ ℕ ↦ ((𝑔‘𝑚) ∖ ∪ 𝑙 ∈ (1..^𝑚)(𝑔‘𝑙)))‘𝑛) ∈ dom vol ↔ ((𝑔‘𝑛) ∖ ∪ 𝑙 ∈ (1..^𝑛)(𝑔‘𝑙)) ∈ dom vol))
66	64	fveq2d 6721	. . . . . . . . . . . . . . . . . . 19 ⊢ (𝑛 ∈ ℕ → (vol‘((𝑚 ∈ ℕ ↦ ((𝑔‘𝑚) ∖ ∪ 𝑙 ∈ (1..^𝑚)(𝑔‘𝑙)))‘𝑛)) = (vol‘((𝑔‘𝑛) ∖ ∪ 𝑙 ∈ (1..^𝑛)(𝑔‘𝑙))))
67	66	eleq1d 2822	. . . . . . . . . . . . . . . . . 18 ⊢ (𝑛 ∈ ℕ → ((vol‘((𝑚 ∈ ℕ ↦ ((𝑔‘𝑚) ∖ ∪ 𝑙 ∈ (1..^𝑚)(𝑔‘𝑙)))‘𝑛)) ∈ ℝ ↔ (vol‘((𝑔‘𝑛) ∖ ∪ 𝑙 ∈ (1..^𝑛)(𝑔‘𝑙))) ∈ ℝ))
68	65, 67	anbi12d 634	. . . . . . . . . . . . . . . . 17 ⊢ (𝑛 ∈ ℕ → ((((𝑚 ∈ ℕ ↦ ((𝑔‘𝑚) ∖ ∪ 𝑙 ∈ (1..^𝑚)(𝑔‘𝑙)))‘𝑛) ∈ dom vol ∧ (vol‘((𝑚 ∈ ℕ ↦ ((𝑔‘𝑚) ∖ ∪ 𝑙 ∈ (1..^𝑚)(𝑔‘𝑙)))‘𝑛)) ∈ ℝ) ↔ (((𝑔‘𝑛) ∖ ∪ 𝑙 ∈ (1..^𝑛)(𝑔‘𝑙)) ∈ dom vol ∧ (vol‘((𝑔‘𝑛) ∖ ∪ 𝑙 ∈ (1..^𝑛)(𝑔‘𝑙))) ∈ ℝ)))
69	68	ralbiia 3087	. . . . . . . . . . . . . . . 16 ⊢ (∀𝑛 ∈ ℕ (((𝑚 ∈ ℕ ↦ ((𝑔‘𝑚) ∖ ∪ 𝑙 ∈ (1..^𝑚)(𝑔‘𝑙)))‘𝑛) ∈ dom vol ∧ (vol‘((𝑚 ∈ ℕ ↦ ((𝑔‘𝑚) ∖ ∪ 𝑙 ∈ (1..^𝑚)(𝑔‘𝑙)))‘𝑛)) ∈ ℝ) ↔ ∀𝑛 ∈ ℕ (((𝑔‘𝑛) ∖ ∪ 𝑙 ∈ (1..^𝑛)(𝑔‘𝑙)) ∈ dom vol ∧ (vol‘((𝑔‘𝑛) ∖ ∪ 𝑙 ∈ (1..^𝑛)(𝑔‘𝑙))) ∈ ℝ))
70		fveq2 6717	. . . . . . . . . . . . . . . . . . . 20 ⊢ (𝑛 = 𝑚 → (𝑔‘𝑛) = (𝑔‘𝑚))
71		oveq2 7221	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (𝑛 = 𝑚 → (1..^𝑛) = (1..^𝑚))
72	71	iuneq1d 4931	. . . . . . . . . . . . . . . . . . . 20 ⊢ (𝑛 = 𝑚 → ∪ 𝑙 ∈ (1..^𝑛)(𝑔‘𝑙) = ∪ 𝑙 ∈ (1..^𝑚)(𝑔‘𝑙))
73	70, 72	difeq12d 4038	. . . . . . . . . . . . . . . . . . 19 ⊢ (𝑛 = 𝑚 → ((𝑔‘𝑛) ∖ ∪ 𝑙 ∈ (1..^𝑛)(𝑔‘𝑙)) = ((𝑔‘𝑚) ∖ ∪ 𝑙 ∈ (1..^𝑚)(𝑔‘𝑙)))
74	73	eleq1d 2822	. . . . . . . . . . . . . . . . . 18 ⊢ (𝑛 = 𝑚 → (((𝑔‘𝑛) ∖ ∪ 𝑙 ∈ (1..^𝑛)(𝑔‘𝑙)) ∈ dom vol ↔ ((𝑔‘𝑚) ∖ ∪ 𝑙 ∈ (1..^𝑚)(𝑔‘𝑙)) ∈ dom vol))
75	73	fveq2d 6721	. . . . . . . . . . . . . . . . . . 19 ⊢ (𝑛 = 𝑚 → (vol‘((𝑔‘𝑛) ∖ ∪ 𝑙 ∈ (1..^𝑛)(𝑔‘𝑙))) = (vol‘((𝑔‘𝑚) ∖ ∪ 𝑙 ∈ (1..^𝑚)(𝑔‘𝑙))))
76	75	eleq1d 2822	. . . . . . . . . . . . . . . . . 18 ⊢ (𝑛 = 𝑚 → ((vol‘((𝑔‘𝑛) ∖ ∪ 𝑙 ∈ (1..^𝑛)(𝑔‘𝑙))) ∈ ℝ ↔ (vol‘((𝑔‘𝑚) ∖ ∪ 𝑙 ∈ (1..^𝑚)(𝑔‘𝑙))) ∈ ℝ))
77	74, 76	anbi12d 634	. . . . . . . . . . . . . . . . 17 ⊢ (𝑛 = 𝑚 → ((((𝑔‘𝑛) ∖ ∪ 𝑙 ∈ (1..^𝑛)(𝑔‘𝑙)) ∈ dom vol ∧ (vol‘((𝑔‘𝑛) ∖ ∪ 𝑙 ∈ (1..^𝑛)(𝑔‘𝑙))) ∈ ℝ) ↔ (((𝑔‘𝑚) ∖ ∪ 𝑙 ∈ (1..^𝑚)(𝑔‘𝑙)) ∈ dom vol ∧ (vol‘((𝑔‘𝑚) ∖ ∪ 𝑙 ∈ (1..^𝑚)(𝑔‘𝑙))) ∈ ℝ)))
78	77	cbvralvw 3358	. . . . . . . . . . . . . . . 16 ⊢ (∀𝑛 ∈ ℕ (((𝑔‘𝑛) ∖ ∪ 𝑙 ∈ (1..^𝑛)(𝑔‘𝑙)) ∈ dom vol ∧ (vol‘((𝑔‘𝑛) ∖ ∪ 𝑙 ∈ (1..^𝑛)(𝑔‘𝑙))) ∈ ℝ) ↔ ∀𝑚 ∈ ℕ (((𝑔‘𝑚) ∖ ∪ 𝑙 ∈ (1..^𝑚)(𝑔‘𝑙)) ∈ dom vol ∧ (vol‘((𝑔‘𝑚) ∖ ∪ 𝑙 ∈ (1..^𝑚)(𝑔‘𝑙))) ∈ ℝ))
79	69, 78	bitri 278	. . . . . . . . . . . . . . 15 ⊢ (∀𝑛 ∈ ℕ (((𝑚 ∈ ℕ ↦ ((𝑔‘𝑚) ∖ ∪ 𝑙 ∈ (1..^𝑚)(𝑔‘𝑙)))‘𝑛) ∈ dom vol ∧ (vol‘((𝑚 ∈ ℕ ↦ ((𝑔‘𝑚) ∖ ∪ 𝑙 ∈ (1..^𝑚)(𝑔‘𝑙)))‘𝑛)) ∈ ℝ) ↔ ∀𝑚 ∈ ℕ (((𝑔‘𝑚) ∖ ∪ 𝑙 ∈ (1..^𝑚)(𝑔‘𝑙)) ∈ dom vol ∧ (vol‘((𝑔‘𝑚) ∖ ∪ 𝑙 ∈ (1..^𝑚)(𝑔‘𝑙))) ∈ ℝ))
80	55, 79	sylibr 237	. . . . . . . . . . . . . 14 ⊢ (∀𝑚 ∈ ℕ ((𝑔‘𝑚) ⊆ ℝ ∧ (vol*‘(𝑔‘𝑚)) = 0) → ∀𝑛 ∈ ℕ (((𝑚 ∈ ℕ ↦ ((𝑔‘𝑚) ∖ ∪ 𝑙 ∈ (1..^𝑚)(𝑔‘𝑙)))‘𝑛) ∈ dom vol ∧ (vol‘((𝑚 ∈ ℕ ↦ ((𝑔‘𝑚) ∖ ∪ 𝑙 ∈ (1..^𝑚)(𝑔‘𝑙)))‘𝑛)) ∈ ℝ))
81		fveq2 6717	. . . . . . . . . . . . . . . 16 ⊢ (𝑛 = 𝑙 → (𝑔‘𝑛) = (𝑔‘𝑙))
82	81	iundisj2 24446	. . . . . . . . . . . . . . 15 ⊢ Disj 𝑛 ∈ ℕ ((𝑔‘𝑛) ∖ ∪ 𝑙 ∈ (1..^𝑛)(𝑔‘𝑙))
83		disjeq2 5022	. . . . . . . . . . . . . . . 16 ⊢ (∀𝑛 ∈ ℕ ((𝑚 ∈ ℕ ↦ ((𝑔‘𝑚) ∖ ∪ 𝑙 ∈ (1..^𝑚)(𝑔‘𝑙)))‘𝑛) = ((𝑔‘𝑛) ∖ ∪ 𝑙 ∈ (1..^𝑛)(𝑔‘𝑙)) → (Disj 𝑛 ∈ ℕ ((𝑚 ∈ ℕ ↦ ((𝑔‘𝑚) ∖ ∪ 𝑙 ∈ (1..^𝑚)(𝑔‘𝑙)))‘𝑛) ↔ Disj 𝑛 ∈ ℕ ((𝑔‘𝑛) ∖ ∪ 𝑙 ∈ (1..^𝑛)(𝑔‘𝑙))))
84	83, 64	mprg 3075	. . . . . . . . . . . . . . 15 ⊢ (Disj 𝑛 ∈ ℕ ((𝑚 ∈ ℕ ↦ ((𝑔‘𝑚) ∖ ∪ 𝑙 ∈ (1..^𝑚)(𝑔‘𝑙)))‘𝑛) ↔ Disj 𝑛 ∈ ℕ ((𝑔‘𝑛) ∖ ∪ 𝑙 ∈ (1..^𝑛)(𝑔‘𝑙)))
85	82, 84	mpbir 234	. . . . . . . . . . . . . 14 ⊢ Disj 𝑛 ∈ ℕ ((𝑚 ∈ ℕ ↦ ((𝑔‘𝑚) ∖ ∪ 𝑙 ∈ (1..^𝑚)(𝑔‘𝑙)))‘𝑛)
86		nnex 11836	. . . . . . . . . . . . . . . . 17 ⊢ ℕ ∈ V
87	86	mptex 7039	. . . . . . . . . . . . . . . 16 ⊢ (𝑚 ∈ ℕ ↦ ((𝑔‘𝑚) ∖ ∪ 𝑙 ∈ (1..^𝑚)(𝑔‘𝑙))) ∈ V
88		fveq1 6716	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (𝑓 = (𝑚 ∈ ℕ ↦ ((𝑔‘𝑚) ∖ ∪ 𝑙 ∈ (1..^𝑚)(𝑔‘𝑙))) → (𝑓‘𝑛) = ((𝑚 ∈ ℕ ↦ ((𝑔‘𝑚) ∖ ∪ 𝑙 ∈ (1..^𝑚)(𝑔‘𝑙)))‘𝑛))
89	88	eleq1d 2822	. . . . . . . . . . . . . . . . . . . 20 ⊢ (𝑓 = (𝑚 ∈ ℕ ↦ ((𝑔‘𝑚) ∖ ∪ 𝑙 ∈ (1..^𝑚)(𝑔‘𝑙))) → ((𝑓‘𝑛) ∈ dom vol ↔ ((𝑚 ∈ ℕ ↦ ((𝑔‘𝑚) ∖ ∪ 𝑙 ∈ (1..^𝑚)(𝑔‘𝑙)))‘𝑛) ∈ dom vol))
90	88	fveq2d 6721	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (𝑓 = (𝑚 ∈ ℕ ↦ ((𝑔‘𝑚) ∖ ∪ 𝑙 ∈ (1..^𝑚)(𝑔‘𝑙))) → (vol‘(𝑓‘𝑛)) = (vol‘((𝑚 ∈ ℕ ↦ ((𝑔‘𝑚) ∖ ∪ 𝑙 ∈ (1..^𝑚)(𝑔‘𝑙)))‘𝑛)))
91	90	eleq1d 2822	. . . . . . . . . . . . . . . . . . . 20 ⊢ (𝑓 = (𝑚 ∈ ℕ ↦ ((𝑔‘𝑚) ∖ ∪ 𝑙 ∈ (1..^𝑚)(𝑔‘𝑙))) → ((vol‘(𝑓‘𝑛)) ∈ ℝ ↔ (vol‘((𝑚 ∈ ℕ ↦ ((𝑔‘𝑚) ∖ ∪ 𝑙 ∈ (1..^𝑚)(𝑔‘𝑙)))‘𝑛)) ∈ ℝ))
92	89, 91	anbi12d 634	. . . . . . . . . . . . . . . . . . 19 ⊢ (𝑓 = (𝑚 ∈ ℕ ↦ ((𝑔‘𝑚) ∖ ∪ 𝑙 ∈ (1..^𝑚)(𝑔‘𝑙))) → (((𝑓‘𝑛) ∈ dom vol ∧ (vol‘(𝑓‘𝑛)) ∈ ℝ) ↔ (((𝑚 ∈ ℕ ↦ ((𝑔‘𝑚) ∖ ∪ 𝑙 ∈ (1..^𝑚)(𝑔‘𝑙)))‘𝑛) ∈ dom vol ∧ (vol‘((𝑚 ∈ ℕ ↦ ((𝑔‘𝑚) ∖ ∪ 𝑙 ∈ (1..^𝑚)(𝑔‘𝑙)))‘𝑛)) ∈ ℝ)))
93	92	ralbidv 3118	. . . . . . . . . . . . . . . . . 18 ⊢ (𝑓 = (𝑚 ∈ ℕ ↦ ((𝑔‘𝑚) ∖ ∪ 𝑙 ∈ (1..^𝑚)(𝑔‘𝑙))) → (∀𝑛 ∈ ℕ ((𝑓‘𝑛) ∈ dom vol ∧ (vol‘(𝑓‘𝑛)) ∈ ℝ) ↔ ∀𝑛 ∈ ℕ (((𝑚 ∈ ℕ ↦ ((𝑔‘𝑚) ∖ ∪ 𝑙 ∈ (1..^𝑚)(𝑔‘𝑙)))‘𝑛) ∈ dom vol ∧ (vol‘((𝑚 ∈ ℕ ↦ ((𝑔‘𝑚) ∖ ∪ 𝑙 ∈ (1..^𝑚)(𝑔‘𝑙)))‘𝑛)) ∈ ℝ)))
94	88	adantr 484	. . . . . . . . . . . . . . . . . . 19 ⊢ ((𝑓 = (𝑚 ∈ ℕ ↦ ((𝑔‘𝑚) ∖ ∪ 𝑙 ∈ (1..^𝑚)(𝑔‘𝑙))) ∧ 𝑛 ∈ ℕ) → (𝑓‘𝑛) = ((𝑚 ∈ ℕ ↦ ((𝑔‘𝑚) ∖ ∪ 𝑙 ∈ (1..^𝑚)(𝑔‘𝑙)))‘𝑛))
95	94	disjeq2dv 5023	. . . . . . . . . . . . . . . . . 18 ⊢ (𝑓 = (𝑚 ∈ ℕ ↦ ((𝑔‘𝑚) ∖ ∪ 𝑙 ∈ (1..^𝑚)(𝑔‘𝑙))) → (Disj 𝑛 ∈ ℕ (𝑓‘𝑛) ↔ Disj 𝑛 ∈ ℕ ((𝑚 ∈ ℕ ↦ ((𝑔‘𝑚) ∖ ∪ 𝑙 ∈ (1..^𝑚)(𝑔‘𝑙)))‘𝑛)))
96	93, 95	anbi12d 634	. . . . . . . . . . . . . . . . 17 ⊢ (𝑓 = (𝑚 ∈ ℕ ↦ ((𝑔‘𝑚) ∖ ∪ 𝑙 ∈ (1..^𝑚)(𝑔‘𝑙))) → ((∀𝑛 ∈ ℕ ((𝑓‘𝑛) ∈ dom vol ∧ (vol‘(𝑓‘𝑛)) ∈ ℝ) ∧ Disj 𝑛 ∈ ℕ (𝑓‘𝑛)) ↔ (∀𝑛 ∈ ℕ (((𝑚 ∈ ℕ ↦ ((𝑔‘𝑚) ∖ ∪ 𝑙 ∈ (1..^𝑚)(𝑔‘𝑙)))‘𝑛) ∈ dom vol ∧ (vol‘((𝑚 ∈ ℕ ↦ ((𝑔‘𝑚) ∖ ∪ 𝑙 ∈ (1..^𝑚)(𝑔‘𝑙)))‘𝑛)) ∈ ℝ) ∧ Disj 𝑛 ∈ ℕ ((𝑚 ∈ ℕ ↦ ((𝑔‘𝑚) ∖ ∪ 𝑙 ∈ (1..^𝑚)(𝑔‘𝑙)))‘𝑛))))
97	88	iuneq2d 4933	. . . . . . . . . . . . . . . . . . 19 ⊢ (𝑓 = (𝑚 ∈ ℕ ↦ ((𝑔‘𝑚) ∖ ∪ 𝑙 ∈ (1..^𝑚)(𝑔‘𝑙))) → ∪ 𝑛 ∈ ℕ (𝑓‘𝑛) = ∪ 𝑛 ∈ ℕ ((𝑚 ∈ ℕ ↦ ((𝑔‘𝑚) ∖ ∪ 𝑙 ∈ (1..^𝑚)(𝑔‘𝑙)))‘𝑛))
98	97	fveq2d 6721	. . . . . . . . . . . . . . . . . 18 ⊢ (𝑓 = (𝑚 ∈ ℕ ↦ ((𝑔‘𝑚) ∖ ∪ 𝑙 ∈ (1..^𝑚)(𝑔‘𝑙))) → (vol‘∪ 𝑛 ∈ ℕ (𝑓‘𝑛)) = (vol‘∪ 𝑛 ∈ ℕ ((𝑚 ∈ ℕ ↦ ((𝑔‘𝑚) ∖ ∪ 𝑙 ∈ (1..^𝑚)(𝑔‘𝑙)))‘𝑛)))
99		voliunnfl.1	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ 𝑆 = seq1( + , 𝐺)
100		voliunnfl.2	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ 𝐺 = (𝑛 ∈ ℕ ↦ (vol‘(𝑓‘𝑛)))
101		seqeq3 13579	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ (𝐺 = (𝑛 ∈ ℕ ↦ (vol‘(𝑓‘𝑛))) → seq1( + , 𝐺) = seq1( + , (𝑛 ∈ ℕ ↦ (vol‘(𝑓‘𝑛)))))
102	100, 101	ax-mp 5	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ seq1( + , 𝐺) = seq1( + , (𝑛 ∈ ℕ ↦ (vol‘(𝑓‘𝑛))))
103	99, 102	eqtri 2765	. . . . . . . . . . . . . . . . . . . . 21 ⊢ 𝑆 = seq1( + , (𝑛 ∈ ℕ ↦ (vol‘(𝑓‘𝑛))))
104	103	rneqi 5806	. . . . . . . . . . . . . . . . . . . 20 ⊢ ran 𝑆 = ran seq1( + , (𝑛 ∈ ℕ ↦ (vol‘(𝑓‘𝑛))))
105	104	supeq1i 9063	. . . . . . . . . . . . . . . . . . 19 ⊢ sup(ran 𝑆, ℝ*, < ) = sup(ran seq1( + , (𝑛 ∈ ℕ ↦ (vol‘(𝑓‘𝑛)))), ℝ*, < )
106	90	mpteq2dv 5151	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (𝑓 = (𝑚 ∈ ℕ ↦ ((𝑔‘𝑚) ∖ ∪ 𝑙 ∈ (1..^𝑚)(𝑔‘𝑙))) → (𝑛 ∈ ℕ ↦ (vol‘(𝑓‘𝑛))) = (𝑛 ∈ ℕ ↦ (vol‘((𝑚 ∈ ℕ ↦ ((𝑔‘𝑚) ∖ ∪ 𝑙 ∈ (1..^𝑚)(𝑔‘𝑙)))‘𝑛))))
107	106	seqeq3d 13582	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (𝑓 = (𝑚 ∈ ℕ ↦ ((𝑔‘𝑚) ∖ ∪ 𝑙 ∈ (1..^𝑚)(𝑔‘𝑙))) → seq1( + , (𝑛 ∈ ℕ ↦ (vol‘(𝑓‘𝑛)))) = seq1( + , (𝑛 ∈ ℕ ↦ (vol‘((𝑚 ∈ ℕ ↦ ((𝑔‘𝑚) ∖ ∪ 𝑙 ∈ (1..^𝑚)(𝑔‘𝑙)))‘𝑛)))))
108	107	rneqd 5807	. . . . . . . . . . . . . . . . . . . 20 ⊢ (𝑓 = (𝑚 ∈ ℕ ↦ ((𝑔‘𝑚) ∖ ∪ 𝑙 ∈ (1..^𝑚)(𝑔‘𝑙))) → ran seq1( + , (𝑛 ∈ ℕ ↦ (vol‘(𝑓‘𝑛)))) = ran seq1( + , (𝑛 ∈ ℕ ↦ (vol‘((𝑚 ∈ ℕ ↦ ((𝑔‘𝑚) ∖ ∪ 𝑙 ∈ (1..^𝑚)(𝑔‘𝑙)))‘𝑛)))))
109	108	supeq1d 9062	. . . . . . . . . . . . . . . . . . 19 ⊢ (𝑓 = (𝑚 ∈ ℕ ↦ ((𝑔‘𝑚) ∖ ∪ 𝑙 ∈ (1..^𝑚)(𝑔‘𝑙))) → sup(ran seq1( + , (𝑛 ∈ ℕ ↦ (vol‘(𝑓‘𝑛)))), ℝ*, < ) = sup(ran seq1( + , (𝑛 ∈ ℕ ↦ (vol‘((𝑚 ∈ ℕ ↦ ((𝑔‘𝑚) ∖ ∪ 𝑙 ∈ (1..^𝑚)(𝑔‘𝑙)))‘𝑛)))), ℝ*, < ))
110	105, 109	syl5eq 2790	. . . . . . . . . . . . . . . . . 18 ⊢ (𝑓 = (𝑚 ∈ ℕ ↦ ((𝑔‘𝑚) ∖ ∪ 𝑙 ∈ (1..^𝑚)(𝑔‘𝑙))) → sup(ran 𝑆, ℝ*, < ) = sup(ran seq1( + , (𝑛 ∈ ℕ ↦ (vol‘((𝑚 ∈ ℕ ↦ ((𝑔‘𝑚) ∖ ∪ 𝑙 ∈ (1..^𝑚)(𝑔‘𝑙)))‘𝑛)))), ℝ*, < ))
111	98, 110	eqeq12d 2753	. . . . . . . . . . . . . . . . 17 ⊢ (𝑓 = (𝑚 ∈ ℕ ↦ ((𝑔‘𝑚) ∖ ∪ 𝑙 ∈ (1..^𝑚)(𝑔‘𝑙))) → ((vol‘∪ 𝑛 ∈ ℕ (𝑓‘𝑛)) = sup(ran 𝑆, ℝ*, < ) ↔ (vol‘∪ 𝑛 ∈ ℕ ((𝑚 ∈ ℕ ↦ ((𝑔‘𝑚) ∖ ∪ 𝑙 ∈ (1..^𝑚)(𝑔‘𝑙)))‘𝑛)) = sup(ran seq1( + , (𝑛 ∈ ℕ ↦ (vol‘((𝑚 ∈ ℕ ↦ ((𝑔‘𝑚) ∖ ∪ 𝑙 ∈ (1..^𝑚)(𝑔‘𝑙)))‘𝑛)))), ℝ*, < )))
112	96, 111	imbi12d 348	. . . . . . . . . . . . . . . 16 ⊢ (𝑓 = (𝑚 ∈ ℕ ↦ ((𝑔‘𝑚) ∖ ∪ 𝑙 ∈ (1..^𝑚)(𝑔‘𝑙))) → (((∀𝑛 ∈ ℕ ((𝑓‘𝑛) ∈ dom vol ∧ (vol‘(𝑓‘𝑛)) ∈ ℝ) ∧ Disj 𝑛 ∈ ℕ (𝑓‘𝑛)) → (vol‘∪ 𝑛 ∈ ℕ (𝑓‘𝑛)) = sup(ran 𝑆, ℝ*, < )) ↔ ((∀𝑛 ∈ ℕ (((𝑚 ∈ ℕ ↦ ((𝑔‘𝑚) ∖ ∪ 𝑙 ∈ (1..^𝑚)(𝑔‘𝑙)))‘𝑛) ∈ dom vol ∧ (vol‘((𝑚 ∈ ℕ ↦ ((𝑔‘𝑚) ∖ ∪ 𝑙 ∈ (1..^𝑚)(𝑔‘𝑙)))‘𝑛)) ∈ ℝ) ∧ Disj 𝑛 ∈ ℕ ((𝑚 ∈ ℕ ↦ ((𝑔‘𝑚) ∖ ∪ 𝑙 ∈ (1..^𝑚)(𝑔‘𝑙)))‘𝑛)) → (vol‘∪ 𝑛 ∈ ℕ ((𝑚 ∈ ℕ ↦ ((𝑔‘𝑚) ∖ ∪ 𝑙 ∈ (1..^𝑚)(𝑔‘𝑙)))‘𝑛)) = sup(ran seq1( + , (𝑛 ∈ ℕ ↦ (vol‘((𝑚 ∈ ℕ ↦ ((𝑔‘𝑚) ∖ ∪ 𝑙 ∈ (1..^𝑚)(𝑔‘𝑙)))‘𝑛)))), ℝ*, < ))))
113		voliunnfl.3	. . . . . . . . . . . . . . . 16 ⊢ ((∀𝑛 ∈ ℕ ((𝑓‘𝑛) ∈ dom vol ∧ (vol‘(𝑓‘𝑛)) ∈ ℝ) ∧ Disj 𝑛 ∈ ℕ (𝑓‘𝑛)) → (vol‘∪ 𝑛 ∈ ℕ (𝑓‘𝑛)) = sup(ran 𝑆, ℝ*, < ))
114	87, 112, 113	vtocl 3474	. . . . . . . . . . . . . . 15 ⊢ ((∀𝑛 ∈ ℕ (((𝑚 ∈ ℕ ↦ ((𝑔‘𝑚) ∖ ∪ 𝑙 ∈ (1..^𝑚)(𝑔‘𝑙)))‘𝑛) ∈ dom vol ∧ (vol‘((𝑚 ∈ ℕ ↦ ((𝑔‘𝑚) ∖ ∪ 𝑙 ∈ (1..^𝑚)(𝑔‘𝑙)))‘𝑛)) ∈ ℝ) ∧ Disj 𝑛 ∈ ℕ ((𝑚 ∈ ℕ ↦ ((𝑔‘𝑚) ∖ ∪ 𝑙 ∈ (1..^𝑚)(𝑔‘𝑙)))‘𝑛)) → (vol‘∪ 𝑛 ∈ ℕ ((𝑚 ∈ ℕ ↦ ((𝑔‘𝑚) ∖ ∪ 𝑙 ∈ (1..^𝑚)(𝑔‘𝑙)))‘𝑛)) = sup(ran seq1( + , (𝑛 ∈ ℕ ↦ (vol‘((𝑚 ∈ ℕ ↦ ((𝑔‘𝑚) ∖ ∪ 𝑙 ∈ (1..^𝑚)(𝑔‘𝑙)))‘𝑛)))), ℝ*, < ))
115	64	iuneq2i 4925	. . . . . . . . . . . . . . . 16 ⊢ ∪ 𝑛 ∈ ℕ ((𝑚 ∈ ℕ ↦ ((𝑔‘𝑚) ∖ ∪ 𝑙 ∈ (1..^𝑚)(𝑔‘𝑙)))‘𝑛) = ∪ 𝑛 ∈ ℕ ((𝑔‘𝑛) ∖ ∪ 𝑙 ∈ (1..^𝑛)(𝑔‘𝑙))
116	115	fveq2i 6720	. . . . . . . . . . . . . . 15 ⊢ (vol‘∪ 𝑛 ∈ ℕ ((𝑚 ∈ ℕ ↦ ((𝑔‘𝑚) ∖ ∪ 𝑙 ∈ (1..^𝑚)(𝑔‘𝑙)))‘𝑛)) = (vol‘∪ 𝑛 ∈ ℕ ((𝑔‘𝑛) ∖ ∪ 𝑙 ∈ (1..^𝑛)(𝑔‘𝑙)))
117	66	mpteq2ia 5146	. . . . . . . . . . . . . . . . . 18 ⊢ (𝑛 ∈ ℕ ↦ (vol‘((𝑚 ∈ ℕ ↦ ((𝑔‘𝑚) ∖ ∪ 𝑙 ∈ (1..^𝑚)(𝑔‘𝑙)))‘𝑛))) = (𝑛 ∈ ℕ ↦ (vol‘((𝑔‘𝑛) ∖ ∪ 𝑙 ∈ (1..^𝑛)(𝑔‘𝑙))))
118		seqeq3 13579	. . . . . . . . . . . . . . . . . 18 ⊢ ((𝑛 ∈ ℕ ↦ (vol‘((𝑚 ∈ ℕ ↦ ((𝑔‘𝑚) ∖ ∪ 𝑙 ∈ (1..^𝑚)(𝑔‘𝑙)))‘𝑛))) = (𝑛 ∈ ℕ ↦ (vol‘((𝑔‘𝑛) ∖ ∪ 𝑙 ∈ (1..^𝑛)(𝑔‘𝑙)))) → seq1( + , (𝑛 ∈ ℕ ↦ (vol‘((𝑚 ∈ ℕ ↦ ((𝑔‘𝑚) ∖ ∪ 𝑙 ∈ (1..^𝑚)(𝑔‘𝑙)))‘𝑛)))) = seq1( + , (𝑛 ∈ ℕ ↦ (vol‘((𝑔‘𝑛) ∖ ∪ 𝑙 ∈ (1..^𝑛)(𝑔‘𝑙))))))
119	117, 118	ax-mp 5	. . . . . . . . . . . . . . . . 17 ⊢ seq1( + , (𝑛 ∈ ℕ ↦ (vol‘((𝑚 ∈ ℕ ↦ ((𝑔‘𝑚) ∖ ∪ 𝑙 ∈ (1..^𝑚)(𝑔‘𝑙)))‘𝑛)))) = seq1( + , (𝑛 ∈ ℕ ↦ (vol‘((𝑔‘𝑛) ∖ ∪ 𝑙 ∈ (1..^𝑛)(𝑔‘𝑙)))))
120	119	rneqi 5806	. . . . . . . . . . . . . . . 16 ⊢ ran seq1( + , (𝑛 ∈ ℕ ↦ (vol‘((𝑚 ∈ ℕ ↦ ((𝑔‘𝑚) ∖ ∪ 𝑙 ∈ (1..^𝑚)(𝑔‘𝑙)))‘𝑛)))) = ran seq1( + , (𝑛 ∈ ℕ ↦ (vol‘((𝑔‘𝑛) ∖ ∪ 𝑙 ∈ (1..^𝑛)(𝑔‘𝑙)))))
121	120	supeq1i 9063	. . . . . . . . . . . . . . 15 ⊢ sup(ran seq1( + , (𝑛 ∈ ℕ ↦ (vol‘((𝑚 ∈ ℕ ↦ ((𝑔‘𝑚) ∖ ∪ 𝑙 ∈ (1..^𝑚)(𝑔‘𝑙)))‘𝑛)))), ℝ*, < ) = sup(ran seq1( + , (𝑛 ∈ ℕ ↦ (vol‘((𝑔‘𝑛) ∖ ∪ 𝑙 ∈ (1..^𝑛)(𝑔‘𝑙))))), ℝ*, < )
122	114, 116, 121	3eqtr3g 2801	. . . . . . . . . . . . . 14 ⊢ ((∀𝑛 ∈ ℕ (((𝑚 ∈ ℕ ↦ ((𝑔‘𝑚) ∖ ∪ 𝑙 ∈ (1..^𝑚)(𝑔‘𝑙)))‘𝑛) ∈ dom vol ∧ (vol‘((𝑚 ∈ ℕ ↦ ((𝑔‘𝑚) ∖ ∪ 𝑙 ∈ (1..^𝑚)(𝑔‘𝑙)))‘𝑛)) ∈ ℝ) ∧ Disj 𝑛 ∈ ℕ ((𝑚 ∈ ℕ ↦ ((𝑔‘𝑚) ∖ ∪ 𝑙 ∈ (1..^𝑚)(𝑔‘𝑙)))‘𝑛)) → (vol‘∪ 𝑛 ∈ ℕ ((𝑔‘𝑛) ∖ ∪ 𝑙 ∈ (1..^𝑛)(𝑔‘𝑙))) = sup(ran seq1( + , (𝑛 ∈ ℕ ↦ (vol‘((𝑔‘𝑛) ∖ ∪ 𝑙 ∈ (1..^𝑛)(𝑔‘𝑙))))), ℝ*, < ))
123	80, 85, 122	sylancl 589	. . . . . . . . . . . . 13 ⊢ (∀𝑚 ∈ ℕ ((𝑔‘𝑚) ⊆ ℝ ∧ (vol*‘(𝑔‘𝑚)) = 0) → (vol‘∪ 𝑛 ∈ ℕ ((𝑔‘𝑛) ∖ ∪ 𝑙 ∈ (1..^𝑛)(𝑔‘𝑙))) = sup(ran seq1( + , (𝑛 ∈ ℕ ↦ (vol‘((𝑔‘𝑛) ∖ ∪ 𝑙 ∈ (1..^𝑛)(𝑔‘𝑙))))), ℝ*, < ))
124	123	adantl 485	. . . . . . . . . . . 12 ⊢ ((𝑔:ℕ–onto→𝐴 ∧ ∀𝑚 ∈ ℕ ((𝑔‘𝑚) ⊆ ℝ ∧ (vol*‘(𝑔‘𝑚)) = 0)) → (vol‘∪ 𝑛 ∈ ℕ ((𝑔‘𝑛) ∖ ∪ 𝑙 ∈ (1..^𝑛)(𝑔‘𝑙))) = sup(ran seq1( + , (𝑛 ∈ ℕ ↦ (vol‘((𝑔‘𝑛) ∖ ∪ 𝑙 ∈ (1..^𝑛)(𝑔‘𝑙))))), ℝ*, < ))
125	81	iundisj 24445	. . . . . . . . . . . . . . . 16 ⊢ ∪ 𝑛 ∈ ℕ (𝑔‘𝑛) = ∪ 𝑛 ∈ ℕ ((𝑔‘𝑛) ∖ ∪ 𝑙 ∈ (1..^𝑛)(𝑔‘𝑙))
126		fofun 6634	. . . . . . . . . . . . . . . . 17 ⊢ (𝑔:ℕ–onto→𝐴 → Fun 𝑔)
127		funiunfv 7061	. . . . . . . . . . . . . . . . 17 ⊢ (Fun 𝑔 → ∪ 𝑛 ∈ ℕ (𝑔‘𝑛) = ∪ (𝑔 “ ℕ))
128	126, 127	syl 17	. . . . . . . . . . . . . . . 16 ⊢ (𝑔:ℕ–onto→𝐴 → ∪ 𝑛 ∈ ℕ (𝑔‘𝑛) = ∪ (𝑔 “ ℕ))
129	125, 128	eqtr3id 2792	. . . . . . . . . . . . . . 15 ⊢ (𝑔:ℕ–onto→𝐴 → ∪ 𝑛 ∈ ℕ ((𝑔‘𝑛) ∖ ∪ 𝑙 ∈ (1..^𝑛)(𝑔‘𝑙)) = ∪ (𝑔 “ ℕ))
130	29	unieqd 4833	. . . . . . . . . . . . . . 15 ⊢ (𝑔:ℕ–onto→𝐴 → ∪ (𝑔 “ ℕ) = ∪ 𝐴)
131	129, 130	eqtrd 2777	. . . . . . . . . . . . . 14 ⊢ (𝑔:ℕ–onto→𝐴 → ∪ 𝑛 ∈ ℕ ((𝑔‘𝑛) ∖ ∪ 𝑙 ∈ (1..^𝑛)(𝑔‘𝑙)) = ∪ 𝐴)
132	131	fveq2d 6721	. . . . . . . . . . . . 13 ⊢ (𝑔:ℕ–onto→𝐴 → (vol‘∪ 𝑛 ∈ ℕ ((𝑔‘𝑛) ∖ ∪ 𝑙 ∈ (1..^𝑛)(𝑔‘𝑙))) = (vol‘∪ 𝐴))
133	132	adantr 484	. . . . . . . . . . . 12 ⊢ ((𝑔:ℕ–onto→𝐴 ∧ ∀𝑚 ∈ ℕ ((𝑔‘𝑚) ⊆ ℝ ∧ (vol*‘(𝑔‘𝑚)) = 0)) → (vol‘∪ 𝑛 ∈ ℕ ((𝑔‘𝑛) ∖ ∪ 𝑙 ∈ (1..^𝑛)(𝑔‘𝑙))) = (vol‘∪ 𝐴))
134	56	sseq1d 3932	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (𝑚 = 𝑛 → ((𝑔‘𝑚) ⊆ ℝ ↔ (𝑔‘𝑛) ⊆ ℝ))
135	56	fveqeq2d 6725	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (𝑚 = 𝑛 → ((vol*‘(𝑔‘𝑚)) = 0 ↔ (vol*‘(𝑔‘𝑛)) = 0))
136	134, 135	anbi12d 634	. . . . . . . . . . . . . . . . . . . 20 ⊢ (𝑚 = 𝑛 → (((𝑔‘𝑚) ⊆ ℝ ∧ (vol*‘(𝑔‘𝑚)) = 0) ↔ ((𝑔‘𝑛) ⊆ ℝ ∧ (vol*‘(𝑔‘𝑛)) = 0)))
137	136	rspccva 3536	. . . . . . . . . . . . . . . . . . 19 ⊢ ((∀𝑚 ∈ ℕ ((𝑔‘𝑚) ⊆ ℝ ∧ (vol*‘(𝑔‘𝑚)) = 0) ∧ 𝑛 ∈ ℕ) → ((𝑔‘𝑛) ⊆ ℝ ∧ (vol*‘(𝑔‘𝑛)) = 0))
138		ssdifss 4050	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ ((𝑔‘𝑛) ⊆ ℝ → ((𝑔‘𝑛) ∖ ∪ 𝑙 ∈ (1..^𝑛)(𝑔‘𝑙)) ⊆ ℝ)
139	138	adantr 484	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (((𝑔‘𝑛) ⊆ ℝ ∧ (vol*‘(𝑔‘𝑛)) = 0) → ((𝑔‘𝑛) ∖ ∪ 𝑙 ∈ (1..^𝑛)(𝑔‘𝑙)) ⊆ ℝ)
140		difss 4046	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ ((𝑔‘𝑛) ∖ ∪ 𝑙 ∈ (1..^𝑛)(𝑔‘𝑙)) ⊆ (𝑔‘𝑛)
141		ovolssnul 24384	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ ((((𝑔‘𝑛) ∖ ∪ 𝑙 ∈ (1..^𝑛)(𝑔‘𝑙)) ⊆ (𝑔‘𝑛) ∧ (𝑔‘𝑛) ⊆ ℝ ∧ (vol*‘(𝑔‘𝑛)) = 0) → (vol*‘((𝑔‘𝑛) ∖ ∪ 𝑙 ∈ (1..^𝑛)(𝑔‘𝑙))) = 0)
142	140, 141	mp3an1 1450	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (((𝑔‘𝑛) ⊆ ℝ ∧ (vol*‘(𝑔‘𝑛)) = 0) → (vol*‘((𝑔‘𝑛) ∖ ∪ 𝑙 ∈ (1..^𝑛)(𝑔‘𝑙))) = 0)
143	139, 142	jca 515	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (((𝑔‘𝑛) ⊆ ℝ ∧ (vol*‘(𝑔‘𝑛)) = 0) → (((𝑔‘𝑛) ∖ ∪ 𝑙 ∈ (1..^𝑛)(𝑔‘𝑙)) ⊆ ℝ ∧ (vol*‘((𝑔‘𝑛) ∖ ∪ 𝑙 ∈ (1..^𝑛)(𝑔‘𝑙))) = 0))
144		nulmbl 24432	. . . . . . . . . . . . . . . . . . . . 21 ⊢ ((((𝑔‘𝑛) ∖ ∪ 𝑙 ∈ (1..^𝑛)(𝑔‘𝑙)) ⊆ ℝ ∧ (vol*‘((𝑔‘𝑛) ∖ ∪ 𝑙 ∈ (1..^𝑛)(𝑔‘𝑙))) = 0) → ((𝑔‘𝑛) ∖ ∪ 𝑙 ∈ (1..^𝑛)(𝑔‘𝑙)) ∈ dom vol)
145		mblvol 24427	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (((𝑔‘𝑛) ∖ ∪ 𝑙 ∈ (1..^𝑛)(𝑔‘𝑙)) ∈ dom vol → (vol‘((𝑔‘𝑛) ∖ ∪ 𝑙 ∈ (1..^𝑛)(𝑔‘𝑙))) = (vol*‘((𝑔‘𝑛) ∖ ∪ 𝑙 ∈ (1..^𝑛)(𝑔‘𝑙))))
146	143, 144, 145	3syl 18	. . . . . . . . . . . . . . . . . . . 20 ⊢ (((𝑔‘𝑛) ⊆ ℝ ∧ (vol*‘(𝑔‘𝑛)) = 0) → (vol‘((𝑔‘𝑛) ∖ ∪ 𝑙 ∈ (1..^𝑛)(𝑔‘𝑙))) = (vol*‘((𝑔‘𝑛) ∖ ∪ 𝑙 ∈ (1..^𝑛)(𝑔‘𝑙))))
147	146, 142	eqtrd 2777	. . . . . . . . . . . . . . . . . . 19 ⊢ (((𝑔‘𝑛) ⊆ ℝ ∧ (vol*‘(𝑔‘𝑛)) = 0) → (vol‘((𝑔‘𝑛) ∖ ∪ 𝑙 ∈ (1..^𝑛)(𝑔‘𝑙))) = 0)
148	137, 147	syl 17	. . . . . . . . . . . . . . . . . 18 ⊢ ((∀𝑚 ∈ ℕ ((𝑔‘𝑚) ⊆ ℝ ∧ (vol*‘(𝑔‘𝑚)) = 0) ∧ 𝑛 ∈ ℕ) → (vol‘((𝑔‘𝑛) ∖ ∪ 𝑙 ∈ (1..^𝑛)(𝑔‘𝑙))) = 0)
149	148	mpteq2dva 5150	. . . . . . . . . . . . . . . . 17 ⊢ (∀𝑚 ∈ ℕ ((𝑔‘𝑚) ⊆ ℝ ∧ (vol*‘(𝑔‘𝑚)) = 0) → (𝑛 ∈ ℕ ↦ (vol‘((𝑔‘𝑛) ∖ ∪ 𝑙 ∈ (1..^𝑛)(𝑔‘𝑙)))) = (𝑛 ∈ ℕ ↦ 0))
150	149	seqeq3d 13582	. . . . . . . . . . . . . . . 16 ⊢ (∀𝑚 ∈ ℕ ((𝑔‘𝑚) ⊆ ℝ ∧ (vol*‘(𝑔‘𝑚)) = 0) → seq1( + , (𝑛 ∈ ℕ ↦ (vol‘((𝑔‘𝑛) ∖ ∪ 𝑙 ∈ (1..^𝑛)(𝑔‘𝑙))))) = seq1( + , (𝑛 ∈ ℕ ↦ 0)))
151	150	rneqd 5807	. . . . . . . . . . . . . . 15 ⊢ (∀𝑚 ∈ ℕ ((𝑔‘𝑚) ⊆ ℝ ∧ (vol*‘(𝑔‘𝑚)) = 0) → ran seq1( + , (𝑛 ∈ ℕ ↦ (vol‘((𝑔‘𝑛) ∖ ∪ 𝑙 ∈ (1..^𝑛)(𝑔‘𝑙))))) = ran seq1( + , (𝑛 ∈ ℕ ↦ 0)))
152	151	supeq1d 9062	. . . . . . . . . . . . . 14 ⊢ (∀𝑚 ∈ ℕ ((𝑔‘𝑚) ⊆ ℝ ∧ (vol*‘(𝑔‘𝑚)) = 0) → sup(ran seq1( + , (𝑛 ∈ ℕ ↦ (vol‘((𝑔‘𝑛) ∖ ∪ 𝑙 ∈ (1..^𝑛)(𝑔‘𝑙))))), ℝ*, < ) = sup(ran seq1( + , (𝑛 ∈ ℕ ↦ 0)), ℝ*, < ))
153		0cn 10825	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ 0 ∈ ℂ
154		ser1const 13632	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ ((0 ∈ ℂ ∧ 𝑚 ∈ ℕ) → (seq1( + , (ℕ × {0}))‘𝑚) = (𝑚 · 0))
155	153, 154	mpan 690	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (𝑚 ∈ ℕ → (seq1( + , (ℕ × {0}))‘𝑚) = (𝑚 · 0))
156		nncn 11838	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (𝑚 ∈ ℕ → 𝑚 ∈ ℂ)
157	156	mul01d 11031	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (𝑚 ∈ ℕ → (𝑚 · 0) = 0)
158	155, 157	eqtrd 2777	. . . . . . . . . . . . . . . . . . . 20 ⊢ (𝑚 ∈ ℕ → (seq1( + , (ℕ × {0}))‘𝑚) = 0)
159	158	mpteq2ia 5146	. . . . . . . . . . . . . . . . . . 19 ⊢ (𝑚 ∈ ℕ ↦ (seq1( + , (ℕ × {0}))‘𝑚)) = (𝑚 ∈ ℕ ↦ 0)
160		fconstmpt 5611	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (ℕ × {0}) = (𝑛 ∈ ℕ ↦ 0)
161		seqeq3 13579	. . . . . . . . . . . . . . . . . . . . 21 ⊢ ((ℕ × {0}) = (𝑛 ∈ ℕ ↦ 0) → seq1( + , (ℕ × {0})) = seq1( + , (𝑛 ∈ ℕ ↦ 0)))
162	160, 161	ax-mp 5	. . . . . . . . . . . . . . . . . . . 20 ⊢ seq1( + , (ℕ × {0})) = seq1( + , (𝑛 ∈ ℕ ↦ 0))
163		1z 12207	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ 1 ∈ ℤ
164		seqfn 13586	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (1 ∈ ℤ → seq1( + , (ℕ × {0})) Fn (ℤ≥‘1))
165	163, 164	ax-mp 5	. . . . . . . . . . . . . . . . . . . . 21 ⊢ seq1( + , (ℕ × {0})) Fn (ℤ≥‘1)
166		nnuz 12477	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ ℕ = (ℤ≥‘1)
167	166	fneq2i 6477	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (seq1( + , (ℕ × {0})) Fn ℕ ↔ seq1( + , (ℕ × {0})) Fn (ℤ≥‘1))
168		dffn5 6771	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (seq1( + , (ℕ × {0})) Fn ℕ ↔ seq1( + , (ℕ × {0})) = (𝑚 ∈ ℕ ↦ (seq1( + , (ℕ × {0}))‘𝑚)))
169	167, 168	bitr3i 280	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (seq1( + , (ℕ × {0})) Fn (ℤ≥‘1) ↔ seq1( + , (ℕ × {0})) = (𝑚 ∈ ℕ ↦ (seq1( + , (ℕ × {0}))‘𝑚)))
170	165, 169	mpbi 233	. . . . . . . . . . . . . . . . . . . 20 ⊢ seq1( + , (ℕ × {0})) = (𝑚 ∈ ℕ ↦ (seq1( + , (ℕ × {0}))‘𝑚))
171	162, 170	eqtr3i 2767	. . . . . . . . . . . . . . . . . . 19 ⊢ seq1( + , (𝑛 ∈ ℕ ↦ 0)) = (𝑚 ∈ ℕ ↦ (seq1( + , (ℕ × {0}))‘𝑚))
172		fconstmpt 5611	. . . . . . . . . . . . . . . . . . 19 ⊢ (ℕ × {0}) = (𝑚 ∈ ℕ ↦ 0)
173	159, 171, 172	3eqtr4i 2775	. . . . . . . . . . . . . . . . . 18 ⊢ seq1( + , (𝑛 ∈ ℕ ↦ 0)) = (ℕ × {0})
174	173	rneqi 5806	. . . . . . . . . . . . . . . . 17 ⊢ ran seq1( + , (𝑛 ∈ ℕ ↦ 0)) = ran (ℕ × {0})
175		1nn 11841	. . . . . . . . . . . . . . . . . 18 ⊢ 1 ∈ ℕ
176		ne0i 4249	. . . . . . . . . . . . . . . . . 18 ⊢ (1 ∈ ℕ → ℕ ≠ ∅)
177		rnxp 6033	. . . . . . . . . . . . . . . . . 18 ⊢ (ℕ ≠ ∅ → ran (ℕ × {0}) = {0})
178	175, 176, 177	mp2b 10	. . . . . . . . . . . . . . . . 17 ⊢ ran (ℕ × {0}) = {0}
179	174, 178	eqtri 2765	. . . . . . . . . . . . . . . 16 ⊢ ran seq1( + , (𝑛 ∈ ℕ ↦ 0)) = {0}
180	179	supeq1i 9063	. . . . . . . . . . . . . . 15 ⊢ sup(ran seq1( + , (𝑛 ∈ ℕ ↦ 0)), ℝ*, < ) = sup({0}, ℝ*, < )
181		xrltso 12731	. . . . . . . . . . . . . . . 16 ⊢ < Or ℝ*
182		0xr 10880	. . . . . . . . . . . . . . . 16 ⊢ 0 ∈ ℝ*
183		supsn 9088	. . . . . . . . . . . . . . . 16 ⊢ (( < Or ℝ* ∧ 0 ∈ ℝ*) → sup({0}, ℝ*, < ) = 0)
184	181, 182, 183	mp2an 692	. . . . . . . . . . . . . . 15 ⊢ sup({0}, ℝ*, < ) = 0
185	180, 184	eqtri 2765	. . . . . . . . . . . . . 14 ⊢ sup(ran seq1( + , (𝑛 ∈ ℕ ↦ 0)), ℝ*, < ) = 0
186	152, 185	eqtrdi 2794	. . . . . . . . . . . . 13 ⊢ (∀𝑚 ∈ ℕ ((𝑔‘𝑚) ⊆ ℝ ∧ (vol*‘(𝑔‘𝑚)) = 0) → sup(ran seq1( + , (𝑛 ∈ ℕ ↦ (vol‘((𝑔‘𝑛) ∖ ∪ 𝑙 ∈ (1..^𝑛)(𝑔‘𝑙))))), ℝ*, < ) = 0)
187	186	adantl 485	. . . . . . . . . . . 12 ⊢ ((𝑔:ℕ–onto→𝐴 ∧ ∀𝑚 ∈ ℕ ((𝑔‘𝑚) ⊆ ℝ ∧ (vol*‘(𝑔‘𝑚)) = 0)) → sup(ran seq1( + , (𝑛 ∈ ℕ ↦ (vol‘((𝑔‘𝑛) ∖ ∪ 𝑙 ∈ (1..^𝑛)(𝑔‘𝑙))))), ℝ*, < ) = 0)
188	124, 133, 187	3eqtr3rd 2786	. . . . . . . . . . 11 ⊢ ((𝑔:ℕ–onto→𝐴 ∧ ∀𝑚 ∈ ℕ ((𝑔‘𝑚) ⊆ ℝ ∧ (vol*‘(𝑔‘𝑚)) = 0)) → 0 = (vol‘∪ 𝐴))
189	188	ex 416	. . . . . . . . . 10 ⊢ (𝑔:ℕ–onto→𝐴 → (∀𝑚 ∈ ℕ ((𝑔‘𝑚) ⊆ ℝ ∧ (vol*‘(𝑔‘𝑚)) = 0) → 0 = (vol‘∪ 𝐴)))
190	38, 189	sylbid 243	. . . . . . . . 9 ⊢ (𝑔:ℕ–onto→𝐴 → (∀𝑥 ∈ 𝐴 (𝑥 ⊆ ℝ ∧ (vol*‘𝑥) = 0) → 0 = (vol‘∪ 𝐴)))
191	28, 190	syl5 34	. . . . . . . 8 ⊢ (𝑔:ℕ–onto→𝐴 → ((∀𝑥 ∈ 𝐴 𝑥 ≼ ℕ ∧ ∪ 𝐴 ⊆ ℝ) → 0 = (vol‘∪ 𝐴)))
192	191	exlimiv 1938	. . . . . . 7 ⊢ (∃𝑔 𝑔:ℕ–onto→𝐴 → ((∀𝑥 ∈ 𝐴 𝑥 ≼ ℕ ∧ ∪ 𝐴 ⊆ ℝ) → 0 = (vol‘∪ 𝐴)))
193	18, 192	syl 17	. . . . . 6 ⊢ ((𝐴 ≠ ∅ ∧ 𝐴 ≼ ℕ) → ((∀𝑥 ∈ 𝐴 𝑥 ≼ ℕ ∧ ∪ 𝐴 ⊆ ℝ) → 0 = (vol‘∪ 𝐴)))
194	193	expimpd 457	. . . . 5 ⊢ (𝐴 ≠ ∅ → ((𝐴 ≼ ℕ ∧ (∀𝑥 ∈ 𝐴 𝑥 ≼ ℕ ∧ ∪ 𝐴 ⊆ ℝ)) → 0 = (vol‘∪ 𝐴)))
195	11, 194	pm2.61ine 3025	. . . 4 ⊢ ((𝐴 ≼ ℕ ∧ (∀𝑥 ∈ 𝐴 𝑥 ≼ ℕ ∧ ∪ 𝐴 ⊆ ℝ)) → 0 = (vol‘∪ 𝐴))
196		renepnf 10881	. . . . . . 7 ⊢ (0 ∈ ℝ → 0 ≠ +∞)
197	47, 196	mp1i 13	. . . . . 6 ⊢ (∪ 𝐴 = ℝ → 0 ≠ +∞)
198		fveq2 6717	. . . . . . 7 ⊢ (∪ 𝐴 = ℝ → (vol‘∪ 𝐴) = (vol‘ℝ))
199		rembl 24437	. . . . . . . . 9 ⊢ ℝ ∈ dom vol
200		mblvol 24427	. . . . . . . . 9 ⊢ (ℝ ∈ dom vol → (vol‘ℝ) = (vol*‘ℝ))
201	199, 200	ax-mp 5	. . . . . . . 8 ⊢ (vol‘ℝ) = (vol*‘ℝ)
202		ovolre 24422	. . . . . . . 8 ⊢ (vol*‘ℝ) = +∞
203	201, 202	eqtri 2765	. . . . . . 7 ⊢ (vol‘ℝ) = +∞
204	198, 203	eqtrdi 2794	. . . . . 6 ⊢ (∪ 𝐴 = ℝ → (vol‘∪ 𝐴) = +∞)
205	197, 204	neeqtrrd 3015	. . . . 5 ⊢ (∪ 𝐴 = ℝ → 0 ≠ (vol‘∪ 𝐴))
206	205	necon2i 2975	. . . 4 ⊢ (0 = (vol‘∪ 𝐴) → ∪ 𝐴 ≠ ℝ)
207	195, 206	syl 17	. . 3 ⊢ ((𝐴 ≼ ℕ ∧ (∀𝑥 ∈ 𝐴 𝑥 ≼ ℕ ∧ ∪ 𝐴 ⊆ ℝ)) → ∪ 𝐴 ≠ ℝ)
208	207	expr 460	. 2 ⊢ ((𝐴 ≼ ℕ ∧ ∀𝑥 ∈ 𝐴 𝑥 ≼ ℕ) → (∪ 𝐴 ⊆ ℝ → ∪ 𝐴 ≠ ℝ))
209		eqimss 3957	. . 3 ⊢ (∪ 𝐴 = ℝ → ∪ 𝐴 ⊆ ℝ)
210	209	necon3bi 2967	. 2 ⊢ (¬ ∪ 𝐴 ⊆ ℝ → ∪ 𝐴 ≠ ℝ)
211	208, 210	pm2.61d1 183	1 ⊢ ((𝐴 ≼ ℕ ∧ ∀𝑥 ∈ 𝐴 𝑥 ≼ ℕ) → ∪ 𝐴 ≠ ℝ)

Syntax hints:   → wi 4   ↔ wb 209   ∧ wa 399   = wceq 1543  ∃wex 1787   ∈ wcel 2110   ≠ wne 2940  ∀wral 3061  Vcvv 3408   ∖ cdif 3863   ⊆ wss 3866  ∅c0 4237  {csn 4541  ∪ cuni 4819  ∪ ciun 4904  Disj wdisj 5018   class class class wbr 5053   ↦ cmpt 5135   Or wor 5467   × cxp 5549  dom cdm 5551  ran crn 5552   “ cima 5554  Fun wfun 6374   Fn wfn 6375  –onto→wfo 6378  ‘cfv 6380  (class class class)co 7213   ≼ cdom 8624   ≺ csdm 8625  supcsup 9056  ℂcc 10727  ℝcr 10728  0cc0 10729  1c1 10730   + caddc 10732   · cmul 10734  +∞cpnf 10864  ℝ^*cxr 10866   < clt 10867  ℕcn 11830  ℤcz 12176  ℤ_≥cuz 12438  ..^cfzo 13238  seqcseq 13574  vol*covol 24359  volcvol 24360

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1803  ax-4 1817  ax-5 1918  ax-6 1976  ax-7 2016  ax-8 2112  ax-9 2120  ax-10 2141  ax-11 2158  ax-12 2175  ax-ext 2708  ax-rep 5179  ax-sep 5192  ax-nul 5199  ax-pow 5258  ax-pr 5322  ax-un 7523  ax-inf2 9256  ax-cnex 10785  ax-resscn 10786  ax-1cn 10787  ax-icn 10788  ax-addcl 10789  ax-addrcl 10790  ax-mulcl 10791  ax-mulrcl 10792  ax-mulcom 10793  ax-addass 10794  ax-mulass 10795  ax-distr 10796  ax-i2m1 10797  ax-1ne0 10798  ax-1rid 10799  ax-rnegex 10800  ax-rrecex 10801  ax-cnre 10802  ax-pre-lttri 10803  ax-pre-lttrn 10804  ax-pre-ltadd 10805  ax-pre-mulgt0 10806  ax-pre-sup 10807

This theorem depends on definitions:  df-bi 210  df-an 400  df-or 848  df-3or 1090  df-3an 1091  df-tru 1546  df-fal 1556  df-ex 1788  df-nf 1792  df-sb 2071  df-mo 2539  df-eu 2568  df-clab 2715  df-cleq 2729  df-clel 2816  df-nfc 2886  df-ne 2941  df-nel 3047  df-ral 3066  df-rex 3067  df-reu 3068  df-rmo 3069  df-rab 3070  df-v 3410  df-sbc 3695  df-csb 3812  df-dif 3869  df-un 3871  df-in 3873  df-ss 3883  df-pss 3885  df-nul 4238  df-if 4440  df-pw 4515  df-sn 4542  df-pr 4544  df-tp 4546  df-op 4548  df-uni 4820  df-int 4860  df-iun 4906  df-disj 5019  df-br 5054  df-opab 5116  df-mpt 5136  df-tr 5162  df-id 5455  df-eprel 5460  df-po 5468  df-so 5469  df-fr 5509  df-se 5510  df-we 5511  df-xp 5557  df-rel 5558  df-cnv 5559  df-co 5560  df-dm 5561  df-rn 5562  df-res 5563  df-ima 5564  df-pred 6160  df-ord 6216  df-on 6217  df-lim 6218  df-suc 6219  df-iota 6338  df-fun 6382  df-fn 6383  df-f 6384  df-f1 6385  df-fo 6386  df-f1o 6387  df-fv 6388  df-isom 6389  df-riota 7170  df-ov 7216  df-oprab 7217  df-mpo 7218  df-of 7469  df-om 7645  df-1st 7761  df-2nd 7762  df-wrecs 8047  df-recs 8108  df-rdg 8146  df-1o 8202  df-2o 8203  df-er 8391  df-map 8510  df-en 8627  df-dom 8628  df-sdom 8629  df-fin 8630  df-fi 9027  df-sup 9058  df-inf 9059  df-oi 9126  df-dju 9517  df-card 9555  df-pnf 10869  df-mnf 10870  df-xr 10871  df-ltxr 10872  df-le 10873  df-sub 11064  df-neg 11065  df-div 11490  df-nn 11831  df-2 11893  df-3 11894  df-n0 12091  df-z 12177  df-uz 12439  df-q 12545  df-rp 12587  df-xneg 12704  df-xadd 12705  df-xmul 12706  df-ioo 12939  df-ico 12941  df-icc 12942  df-fz 13096  df-fzo 13239  df-fl 13367  df-seq 13575  df-exp 13636  df-hash 13897  df-cj 14662  df-re 14663  df-im 14664  df-sqrt 14798  df-abs 14799  df-clim 15049  df-sum 15250  df-rest 16927  df-topgen 16948  df-psmet 20355  df-xmet 20356  df-met 20357  df-bl 20358  df-mopn 20359  df-top 21791  df-topon 21808  df-bases 21843  df-cmp 22284  df-ovol 24361  df-vol 24362

This theorem is referenced by: (None)