Theorem voliunnfl 37834

Description: voliun 25513 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 4873	. . . . . . . . 9 ⊢ (𝐴 = ∅ → ∪ 𝐴 = ∪ ∅)
2		uni0 4890	. . . . . . . . 9 ⊢ ∪ ∅ = ∅
3	1, 2	eqtrdi 2786	. . . . . . . 8 ⊢ (𝐴 = ∅ → ∪ 𝐴 = ∅)
4	3	fveq2d 6837	. . . . . . 7 ⊢ (𝐴 = ∅ → (vol‘∪ 𝐴) = (vol‘∅))
5		0mbl 25498	. . . . . . . . 9 ⊢ ∅ ∈ dom vol
6		mblvol 25489	. . . . . . . . 9 ⊢ (∅ ∈ dom vol → (vol‘∅) = (vol*‘∅))
7	5, 6	ax-mp 5	. . . . . . . 8 ⊢ (vol‘∅) = (vol*‘∅)
8		ovol0 25452	. . . . . . . 8 ⊢ (vol*‘∅) = 0
9	7, 8	eqtri 2758	. . . . . . 7 ⊢ (vol‘∅) = 0
10	4, 9	eqtr2di 2787	. . . . . 6 ⊢ (𝐴 = ∅ → 0 = (vol‘∪ 𝐴))
11	10	a1d 25	. . . . 5 ⊢ (𝐴 = ∅ → ((𝐴 ≼ ℕ ∧ (∀𝑥 ∈ 𝐴 𝑥 ≼ ℕ ∧ ∪ 𝐴 ⊆ ℝ)) → 0 = (vol‘∪ 𝐴)))
12		reldom 8891	. . . . . . . . . . 11 ⊢ Rel ≼
13	12	brrelex1i 5679	. . . . . . . . . 10 ⊢ (𝐴 ≼ ℕ → 𝐴 ∈ V)
14		0sdomg 9036	. . . . . . . . . 10 ⊢ (𝐴 ∈ V → (∅ ≺ 𝐴 ↔ 𝐴 ≠ ∅))
15	13, 14	syl 17	. . . . . . . . 9 ⊢ (𝐴 ≼ ℕ → (∅ ≺ 𝐴 ↔ 𝐴 ≠ ∅))
16	15	biimparc 479	. . . . . . . 8 ⊢ ((𝐴 ≠ ∅ ∧ 𝐴 ≼ ℕ) → ∅ ≺ 𝐴)
17		fodomr 9058	. . . . . . . 8 ⊢ ((∅ ≺ 𝐴 ∧ 𝐴 ≼ ℕ) → ∃𝑔 𝑔:ℕ–onto→𝐴)
18	16, 17	sylancom 589	. . . . . . 7 ⊢ ((𝐴 ≠ ∅ ∧ 𝐴 ≼ ℕ) → ∃𝑔 𝑔:ℕ–onto→𝐴)
19		unissb 4895	. . . . . . . . . . . . 13 ⊢ (∪ 𝐴 ⊆ ℝ ↔ ∀𝑥 ∈ 𝐴 𝑥 ⊆ ℝ)
20	19	anbi1i 625	. . . . . . . . . . . 12 ⊢ ((∪ 𝐴 ⊆ ℝ ∧ ∀𝑥 ∈ 𝐴 𝑥 ≼ ℕ) ↔ (∀𝑥 ∈ 𝐴 𝑥 ⊆ ℝ ∧ ∀𝑥 ∈ 𝐴 𝑥 ≼ ℕ))
21		r19.26 3095	. . . . . . . . . . . 12 ⊢ (∀𝑥 ∈ 𝐴 (𝑥 ⊆ ℝ ∧ 𝑥 ≼ ℕ) ↔ (∀𝑥 ∈ 𝐴 𝑥 ⊆ ℝ ∧ ∀𝑥 ∈ 𝐴 𝑥 ≼ ℕ))
22	20, 21	bitr4i 278	. . . . . . . . . . 11 ⊢ ((∪ 𝐴 ⊆ ℝ ∧ ∀𝑥 ∈ 𝐴 𝑥 ≼ ℕ) ↔ ∀𝑥 ∈ 𝐴 (𝑥 ⊆ ℝ ∧ 𝑥 ≼ ℕ))
23		ovolctb2 25451	. . . . . . . . . . . . . 14 ⊢ ((𝑥 ⊆ ℝ ∧ 𝑥 ≼ ℕ) → (vol*‘𝑥) = 0)
24	23	ex 412	. . . . . . . . . . . . 13 ⊢ (𝑥 ⊆ ℝ → (𝑥 ≼ ℕ → (vol*‘𝑥) = 0))
25	24	imdistani 568	. . . . . . . . . . . 12 ⊢ ((𝑥 ⊆ ℝ ∧ 𝑥 ≼ ℕ) → (𝑥 ⊆ ℝ ∧ (vol*‘𝑥) = 0))
26	25	ralimi 3072	. . . . . . . . . . 11 ⊢ (∀𝑥 ∈ 𝐴 (𝑥 ⊆ ℝ ∧ 𝑥 ≼ ℕ) → ∀𝑥 ∈ 𝐴 (𝑥 ⊆ ℝ ∧ (vol*‘𝑥) = 0))
27	22, 26	sylbi 217	. . . . . . . . . 10 ⊢ ((∪ 𝐴 ⊆ ℝ ∧ ∀𝑥 ∈ 𝐴 𝑥 ≼ ℕ) → ∀𝑥 ∈ 𝐴 (𝑥 ⊆ ℝ ∧ (vol*‘𝑥) = 0))
28	27	ancoms 458	. . . . . . . . 9 ⊢ ((∀𝑥 ∈ 𝐴 𝑥 ≼ ℕ ∧ ∪ 𝐴 ⊆ ℝ) → ∀𝑥 ∈ 𝐴 (𝑥 ⊆ ℝ ∧ (vol*‘𝑥) = 0))
29		foima 6750	. . . . . . . . . . . 12 ⊢ (𝑔:ℕ–onto→𝐴 → (𝑔 “ ℕ) = 𝐴)
30	29	raleqdv 3295	. . . . . . . . . . 11 ⊢ (𝑔:ℕ–onto→𝐴 → (∀𝑥 ∈ (𝑔 “ ℕ)(𝑥 ⊆ ℝ ∧ (vol*‘𝑥) = 0) ↔ ∀𝑥 ∈ 𝐴 (𝑥 ⊆ ℝ ∧ (vol*‘𝑥) = 0)))
31		fofn 6747	. . . . . . . . . . . 12 ⊢ (𝑔:ℕ–onto→𝐴 → 𝑔 Fn ℕ)
32		ssid 3955	. . . . . . . . . . . 12 ⊢ ℕ ⊆ ℕ
33		sseq1 3958	. . . . . . . . . . . . . 14 ⊢ (𝑥 = (𝑔‘𝑚) → (𝑥 ⊆ ℝ ↔ (𝑔‘𝑚) ⊆ ℝ))
34		fveqeq2 6842	. . . . . . . . . . . . . 14 ⊢ (𝑥 = (𝑔‘𝑚) → ((vol*‘𝑥) = 0 ↔ (vol*‘(𝑔‘𝑚)) = 0))
35	33, 34	anbi12d 633	. . . . . . . . . . . . 13 ⊢ (𝑥 = (𝑔‘𝑚) → ((𝑥 ⊆ ℝ ∧ (vol*‘𝑥) = 0) ↔ ((𝑔‘𝑚) ⊆ ℝ ∧ (vol*‘(𝑔‘𝑚)) = 0)))
36	35	ralima 7183	. . . . . . . . . . . 12 ⊢ ((𝑔 Fn ℕ ∧ ℕ ⊆ ℕ) → (∀𝑥 ∈ (𝑔 “ ℕ)(𝑥 ⊆ ℝ ∧ (vol*‘𝑥) = 0) ↔ ∀𝑚 ∈ ℕ ((𝑔‘𝑚) ⊆ ℝ ∧ (vol*‘(𝑔‘𝑚)) = 0)))
37	31, 32, 36	sylancl 587	. . . . . . . . . . 11 ⊢ (𝑔:ℕ–onto→𝐴 → (∀𝑥 ∈ (𝑔 “ ℕ)(𝑥 ⊆ ℝ ∧ (vol*‘𝑥) = 0) ↔ ∀𝑚 ∈ ℕ ((𝑔‘𝑚) ⊆ ℝ ∧ (vol*‘(𝑔‘𝑚)) = 0)))
38	30, 37	bitr3d 281	. . . . . . . . . 10 ⊢ (𝑔:ℕ–onto→𝐴 → (∀𝑥 ∈ 𝐴 (𝑥 ⊆ ℝ ∧ (vol*‘𝑥) = 0) ↔ ∀𝑚 ∈ ℕ ((𝑔‘𝑚) ⊆ ℝ ∧ (vol*‘(𝑔‘𝑚)) = 0)))
39		difss 4087	. . . . . . . . . . . . . . . . . 18 ⊢ ((𝑔‘𝑚) ∖ ∪ 𝑙 ∈ (1..^𝑚)(𝑔‘𝑙)) ⊆ (𝑔‘𝑚)
40		ovolssnul 25446	. . . . . . . . . . . . . . . . . 18 ⊢ ((((𝑔‘𝑚) ∖ ∪ 𝑙 ∈ (1..^𝑚)(𝑔‘𝑙)) ⊆ (𝑔‘𝑚) ∧ (𝑔‘𝑚) ⊆ ℝ ∧ (vol*‘(𝑔‘𝑚)) = 0) → (vol*‘((𝑔‘𝑚) ∖ ∪ 𝑙 ∈ (1..^𝑚)(𝑔‘𝑙))) = 0)
41	39, 40	mp3an1 1451	. . . . . . . . . . . . . . . . 17 ⊢ (((𝑔‘𝑚) ⊆ ℝ ∧ (vol*‘(𝑔‘𝑚)) = 0) → (vol*‘((𝑔‘𝑚) ∖ ∪ 𝑙 ∈ (1..^𝑚)(𝑔‘𝑙))) = 0)
42		ssdifss 4091	. . . . . . . . . . . . . . . . . 18 ⊢ ((𝑔‘𝑚) ⊆ ℝ → ((𝑔‘𝑚) ∖ ∪ 𝑙 ∈ (1..^𝑚)(𝑔‘𝑙)) ⊆ ℝ)
43		nulmbl 25494	. . . . . . . . . . . . . . . . . . 19 ⊢ ((((𝑔‘𝑚) ∖ ∪ 𝑙 ∈ (1..^𝑚)(𝑔‘𝑙)) ⊆ ℝ ∧ (vol*‘((𝑔‘𝑚) ∖ ∪ 𝑙 ∈ (1..^𝑚)(𝑔‘𝑙))) = 0) → ((𝑔‘𝑚) ∖ ∪ 𝑙 ∈ (1..^𝑚)(𝑔‘𝑙)) ∈ dom vol)
44		mblvol 25489	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ (((𝑔‘𝑚) ∖ ∪ 𝑙 ∈ (1..^𝑚)(𝑔‘𝑙)) ∈ dom vol → (vol‘((𝑔‘𝑚) ∖ ∪ 𝑙 ∈ (1..^𝑚)(𝑔‘𝑙))) = (vol*‘((𝑔‘𝑚) ∖ ∪ 𝑙 ∈ (1..^𝑚)(𝑔‘𝑙))))
45	44	eqeq1d 2737	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ (((𝑔‘𝑚) ∖ ∪ 𝑙 ∈ (1..^𝑚)(𝑔‘𝑙)) ∈ dom vol → ((vol‘((𝑔‘𝑚) ∖ ∪ 𝑙 ∈ (1..^𝑚)(𝑔‘𝑙))) = 0 ↔ (vol*‘((𝑔‘𝑚) ∖ ∪ 𝑙 ∈ (1..^𝑚)(𝑔‘𝑙))) = 0))
46	45	biimpar 477	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ ((((𝑔‘𝑚) ∖ ∪ 𝑙 ∈ (1..^𝑚)(𝑔‘𝑙)) ∈ dom vol ∧ (vol*‘((𝑔‘𝑚) ∖ ∪ 𝑙 ∈ (1..^𝑚)(𝑔‘𝑙))) = 0) → (vol‘((𝑔‘𝑚) ∖ ∪ 𝑙 ∈ (1..^𝑚)(𝑔‘𝑙))) = 0)
47		0re 11136	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ 0 ∈ ℝ
48	46, 47	eqeltrdi 2843	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ ((((𝑔‘𝑚) ∖ ∪ 𝑙 ∈ (1..^𝑚)(𝑔‘𝑙)) ∈ dom vol ∧ (vol*‘((𝑔‘𝑚) ∖ ∪ 𝑙 ∈ (1..^𝑚)(𝑔‘𝑙))) = 0) → (vol‘((𝑔‘𝑚) ∖ ∪ 𝑙 ∈ (1..^𝑚)(𝑔‘𝑙))) ∈ ℝ)
49	48	expcom 413	. . . . . . . . . . . . . . . . . . . . 21 ⊢ ((vol*‘((𝑔‘𝑚) ∖ ∪ 𝑙 ∈ (1..^𝑚)(𝑔‘𝑙))) = 0 → (((𝑔‘𝑚) ∖ ∪ 𝑙 ∈ (1..^𝑚)(𝑔‘𝑙)) ∈ dom vol → (vol‘((𝑔‘𝑚) ∖ ∪ 𝑙 ∈ (1..^𝑚)(𝑔‘𝑙))) ∈ ℝ))
50	49	ancld 550	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((vol*‘((𝑔‘𝑚) ∖ ∪ 𝑙 ∈ (1..^𝑚)(𝑔‘𝑙))) = 0 → (((𝑔‘𝑚) ∖ ∪ 𝑙 ∈ (1..^𝑚)(𝑔‘𝑙)) ∈ dom vol → (((𝑔‘𝑚) ∖ ∪ 𝑙 ∈ (1..^𝑚)(𝑔‘𝑙)) ∈ dom vol ∧ (vol‘((𝑔‘𝑚) ∖ ∪ 𝑙 ∈ (1..^𝑚)(𝑔‘𝑙))) ∈ ℝ)))
51	50	adantl 481	. . . . . . . . . . . . . . . . . . 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 581	. . . . . . . . . . . . . . . . 17 ⊢ (((𝑔‘𝑚) ⊆ ℝ ∧ (vol*‘((𝑔‘𝑚) ∖ ∪ 𝑙 ∈ (1..^𝑚)(𝑔‘𝑙))) = 0) → (((𝑔‘𝑚) ∖ ∪ 𝑙 ∈ (1..^𝑚)(𝑔‘𝑙)) ∈ dom vol ∧ (vol‘((𝑔‘𝑚) ∖ ∪ 𝑙 ∈ (1..^𝑚)(𝑔‘𝑙))) ∈ ℝ))
54	41, 53	syldan 592	. . . . . . . . . . . . . . . 16 ⊢ (((𝑔‘𝑚) ⊆ ℝ ∧ (vol*‘(𝑔‘𝑚)) = 0) → (((𝑔‘𝑚) ∖ ∪ 𝑙 ∈ (1..^𝑚)(𝑔‘𝑙)) ∈ dom vol ∧ (vol‘((𝑔‘𝑚) ∖ ∪ 𝑙 ∈ (1..^𝑚)(𝑔‘𝑙))) ∈ ℝ))
55	54	ralimi 3072	. . . . . . . . . . . . . . 15 ⊢ (∀𝑚 ∈ ℕ ((𝑔‘𝑚) ⊆ ℝ ∧ (vol*‘(𝑔‘𝑚)) = 0) → ∀𝑚 ∈ ℕ (((𝑔‘𝑚) ∖ ∪ 𝑙 ∈ (1..^𝑚)(𝑔‘𝑙)) ∈ dom vol ∧ (vol‘((𝑔‘𝑚) ∖ ∪ 𝑙 ∈ (1..^𝑚)(𝑔‘𝑙))) ∈ ℝ))
56		fveq2 6833	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (𝑚 = 𝑛 → (𝑔‘𝑚) = (𝑔‘𝑛))
57		oveq2 7366	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (𝑚 = 𝑛 → (1..^𝑚) = (1..^𝑛))
58	57	iuneq1d 4973	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (𝑚 = 𝑛 → ∪ 𝑙 ∈ (1..^𝑚)(𝑔‘𝑙) = ∪ 𝑙 ∈ (1..^𝑛)(𝑔‘𝑙))
59	56, 58	difeq12d 4078	. . . . . . . . . . . . . . . . . . . 20 ⊢ (𝑚 = 𝑛 → ((𝑔‘𝑚) ∖ ∪ 𝑙 ∈ (1..^𝑚)(𝑔‘𝑙)) = ((𝑔‘𝑛) ∖ ∪ 𝑙 ∈ (1..^𝑛)(𝑔‘𝑙)))
60		eqid 2735	. . . . . . . . . . . . . . . . . . . 20 ⊢ (𝑚 ∈ ℕ ↦ ((𝑔‘𝑚) ∖ ∪ 𝑙 ∈ (1..^𝑚)(𝑔‘𝑙))) = (𝑚 ∈ ℕ ↦ ((𝑔‘𝑚) ∖ ∪ 𝑙 ∈ (1..^𝑚)(𝑔‘𝑙)))
61		fvex 6846	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (𝑔‘𝑛) ∈ V
62		difexg 5273	. . . . . . . . . . . . . . . . . . . . 21 ⊢ ((𝑔‘𝑛) ∈ V → ((𝑔‘𝑛) ∖ ∪ 𝑙 ∈ (1..^𝑛)(𝑔‘𝑙)) ∈ V)
63	61, 62	ax-mp 5	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((𝑔‘𝑛) ∖ ∪ 𝑙 ∈ (1..^𝑛)(𝑔‘𝑙)) ∈ V
64	59, 60, 63	fvmpt 6940	. . . . . . . . . . . . . . . . . . 19 ⊢ (𝑛 ∈ ℕ → ((𝑚 ∈ ℕ ↦ ((𝑔‘𝑚) ∖ ∪ 𝑙 ∈ (1..^𝑚)(𝑔‘𝑙)))‘𝑛) = ((𝑔‘𝑛) ∖ ∪ 𝑙 ∈ (1..^𝑛)(𝑔‘𝑙)))
65	64	eleq1d 2820	. . . . . . . . . . . . . . . . . 18 ⊢ (𝑛 ∈ ℕ → (((𝑚 ∈ ℕ ↦ ((𝑔‘𝑚) ∖ ∪ 𝑙 ∈ (1..^𝑚)(𝑔‘𝑙)))‘𝑛) ∈ dom vol ↔ ((𝑔‘𝑛) ∖ ∪ 𝑙 ∈ (1..^𝑛)(𝑔‘𝑙)) ∈ dom vol))
66	64	fveq2d 6837	. . . . . . . . . . . . . . . . . . 19 ⊢ (𝑛 ∈ ℕ → (vol‘((𝑚 ∈ ℕ ↦ ((𝑔‘𝑚) ∖ ∪ 𝑙 ∈ (1..^𝑚)(𝑔‘𝑙)))‘𝑛)) = (vol‘((𝑔‘𝑛) ∖ ∪ 𝑙 ∈ (1..^𝑛)(𝑔‘𝑙))))
67	66	eleq1d 2820	. . . . . . . . . . . . . . . . . 18 ⊢ (𝑛 ∈ ℕ → ((vol‘((𝑚 ∈ ℕ ↦ ((𝑔‘𝑚) ∖ ∪ 𝑙 ∈ (1..^𝑚)(𝑔‘𝑙)))‘𝑛)) ∈ ℝ ↔ (vol‘((𝑔‘𝑛) ∖ ∪ 𝑙 ∈ (1..^𝑛)(𝑔‘𝑙))) ∈ ℝ))
68	65, 67	anbi12d 633	. . . . . . . . . . . . . . . . 17 ⊢ (𝑛 ∈ ℕ → ((((𝑚 ∈ ℕ ↦ ((𝑔‘𝑚) ∖ ∪ 𝑙 ∈ (1..^𝑚)(𝑔‘𝑙)))‘𝑛) ∈ dom vol ∧ (vol‘((𝑚 ∈ ℕ ↦ ((𝑔‘𝑚) ∖ ∪ 𝑙 ∈ (1..^𝑚)(𝑔‘𝑙)))‘𝑛)) ∈ ℝ) ↔ (((𝑔‘𝑛) ∖ ∪ 𝑙 ∈ (1..^𝑛)(𝑔‘𝑙)) ∈ dom vol ∧ (vol‘((𝑔‘𝑛) ∖ ∪ 𝑙 ∈ (1..^𝑛)(𝑔‘𝑙))) ∈ ℝ)))
69	68	ralbiia 3079	. . . . . . . . . . . . . . . 16 ⊢ (∀𝑛 ∈ ℕ (((𝑚 ∈ ℕ ↦ ((𝑔‘𝑚) ∖ ∪ 𝑙 ∈ (1..^𝑚)(𝑔‘𝑙)))‘𝑛) ∈ dom vol ∧ (vol‘((𝑚 ∈ ℕ ↦ ((𝑔‘𝑚) ∖ ∪ 𝑙 ∈ (1..^𝑚)(𝑔‘𝑙)))‘𝑛)) ∈ ℝ) ↔ ∀𝑛 ∈ ℕ (((𝑔‘𝑛) ∖ ∪ 𝑙 ∈ (1..^𝑛)(𝑔‘𝑙)) ∈ dom vol ∧ (vol‘((𝑔‘𝑛) ∖ ∪ 𝑙 ∈ (1..^𝑛)(𝑔‘𝑙))) ∈ ℝ))
70		fveq2 6833	. . . . . . . . . . . . . . . . . . . 20 ⊢ (𝑛 = 𝑚 → (𝑔‘𝑛) = (𝑔‘𝑚))
71		oveq2 7366	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (𝑛 = 𝑚 → (1..^𝑛) = (1..^𝑚))
72	71	iuneq1d 4973	. . . . . . . . . . . . . . . . . . . 20 ⊢ (𝑛 = 𝑚 → ∪ 𝑙 ∈ (1..^𝑛)(𝑔‘𝑙) = ∪ 𝑙 ∈ (1..^𝑚)(𝑔‘𝑙))
73	70, 72	difeq12d 4078	. . . . . . . . . . . . . . . . . . 19 ⊢ (𝑛 = 𝑚 → ((𝑔‘𝑛) ∖ ∪ 𝑙 ∈ (1..^𝑛)(𝑔‘𝑙)) = ((𝑔‘𝑚) ∖ ∪ 𝑙 ∈ (1..^𝑚)(𝑔‘𝑙)))
74	73	eleq1d 2820	. . . . . . . . . . . . . . . . . 18 ⊢ (𝑛 = 𝑚 → (((𝑔‘𝑛) ∖ ∪ 𝑙 ∈ (1..^𝑛)(𝑔‘𝑙)) ∈ dom vol ↔ ((𝑔‘𝑚) ∖ ∪ 𝑙 ∈ (1..^𝑚)(𝑔‘𝑙)) ∈ dom vol))
75	73	fveq2d 6837	. . . . . . . . . . . . . . . . . . 19 ⊢ (𝑛 = 𝑚 → (vol‘((𝑔‘𝑛) ∖ ∪ 𝑙 ∈ (1..^𝑛)(𝑔‘𝑙))) = (vol‘((𝑔‘𝑚) ∖ ∪ 𝑙 ∈ (1..^𝑚)(𝑔‘𝑙))))
76	75	eleq1d 2820	. . . . . . . . . . . . . . . . . 18 ⊢ (𝑛 = 𝑚 → ((vol‘((𝑔‘𝑛) ∖ ∪ 𝑙 ∈ (1..^𝑛)(𝑔‘𝑙))) ∈ ℝ ↔ (vol‘((𝑔‘𝑚) ∖ ∪ 𝑙 ∈ (1..^𝑚)(𝑔‘𝑙))) ∈ ℝ))
77	74, 76	anbi12d 633	. . . . . . . . . . . . . . . . 17 ⊢ (𝑛 = 𝑚 → ((((𝑔‘𝑛) ∖ ∪ 𝑙 ∈ (1..^𝑛)(𝑔‘𝑙)) ∈ dom vol ∧ (vol‘((𝑔‘𝑛) ∖ ∪ 𝑙 ∈ (1..^𝑛)(𝑔‘𝑙))) ∈ ℝ) ↔ (((𝑔‘𝑚) ∖ ∪ 𝑙 ∈ (1..^𝑚)(𝑔‘𝑙)) ∈ dom vol ∧ (vol‘((𝑔‘𝑚) ∖ ∪ 𝑙 ∈ (1..^𝑚)(𝑔‘𝑙))) ∈ ℝ)))
78	77	cbvralvw 3213	. . . . . . . . . . . . . . . 16 ⊢ (∀𝑛 ∈ ℕ (((𝑔‘𝑛) ∖ ∪ 𝑙 ∈ (1..^𝑛)(𝑔‘𝑙)) ∈ dom vol ∧ (vol‘((𝑔‘𝑛) ∖ ∪ 𝑙 ∈ (1..^𝑛)(𝑔‘𝑙))) ∈ ℝ) ↔ ∀𝑚 ∈ ℕ (((𝑔‘𝑚) ∖ ∪ 𝑙 ∈ (1..^𝑚)(𝑔‘𝑙)) ∈ dom vol ∧ (vol‘((𝑔‘𝑚) ∖ ∪ 𝑙 ∈ (1..^𝑚)(𝑔‘𝑙))) ∈ ℝ))
79	69, 78	bitri 275	. . . . . . . . . . . . . . 15 ⊢ (∀𝑛 ∈ ℕ (((𝑚 ∈ ℕ ↦ ((𝑔‘𝑚) ∖ ∪ 𝑙 ∈ (1..^𝑚)(𝑔‘𝑙)))‘𝑛) ∈ dom vol ∧ (vol‘((𝑚 ∈ ℕ ↦ ((𝑔‘𝑚) ∖ ∪ 𝑙 ∈ (1..^𝑚)(𝑔‘𝑙)))‘𝑛)) ∈ ℝ) ↔ ∀𝑚 ∈ ℕ (((𝑔‘𝑚) ∖ ∪ 𝑙 ∈ (1..^𝑚)(𝑔‘𝑙)) ∈ dom vol ∧ (vol‘((𝑔‘𝑚) ∖ ∪ 𝑙 ∈ (1..^𝑚)(𝑔‘𝑙))) ∈ ℝ))
80	55, 79	sylibr 234	. . . . . . . . . . . . . 14 ⊢ (∀𝑚 ∈ ℕ ((𝑔‘𝑚) ⊆ ℝ ∧ (vol*‘(𝑔‘𝑚)) = 0) → ∀𝑛 ∈ ℕ (((𝑚 ∈ ℕ ↦ ((𝑔‘𝑚) ∖ ∪ 𝑙 ∈ (1..^𝑚)(𝑔‘𝑙)))‘𝑛) ∈ dom vol ∧ (vol‘((𝑚 ∈ ℕ ↦ ((𝑔‘𝑚) ∖ ∪ 𝑙 ∈ (1..^𝑚)(𝑔‘𝑙)))‘𝑛)) ∈ ℝ))
81		fveq2 6833	. . . . . . . . . . . . . . . 16 ⊢ (𝑛 = 𝑙 → (𝑔‘𝑛) = (𝑔‘𝑙))
82	81	iundisj2 25508	. . . . . . . . . . . . . . 15 ⊢ Disj 𝑛 ∈ ℕ ((𝑔‘𝑛) ∖ ∪ 𝑙 ∈ (1..^𝑛)(𝑔‘𝑙))
83		disjeq2 5068	. . . . . . . . . . . . . . . 16 ⊢ (∀𝑛 ∈ ℕ ((𝑚 ∈ ℕ ↦ ((𝑔‘𝑚) ∖ ∪ 𝑙 ∈ (1..^𝑚)(𝑔‘𝑙)))‘𝑛) = ((𝑔‘𝑛) ∖ ∪ 𝑙 ∈ (1..^𝑛)(𝑔‘𝑙)) → (Disj 𝑛 ∈ ℕ ((𝑚 ∈ ℕ ↦ ((𝑔‘𝑚) ∖ ∪ 𝑙 ∈ (1..^𝑚)(𝑔‘𝑙)))‘𝑛) ↔ Disj 𝑛 ∈ ℕ ((𝑔‘𝑛) ∖ ∪ 𝑙 ∈ (1..^𝑛)(𝑔‘𝑙))))
84	83, 64	mprg 3056	. . . . . . . . . . . . . . 15 ⊢ (Disj 𝑛 ∈ ℕ ((𝑚 ∈ ℕ ↦ ((𝑔‘𝑚) ∖ ∪ 𝑙 ∈ (1..^𝑚)(𝑔‘𝑙)))‘𝑛) ↔ Disj 𝑛 ∈ ℕ ((𝑔‘𝑛) ∖ ∪ 𝑙 ∈ (1..^𝑛)(𝑔‘𝑙)))
85	82, 84	mpbir 231	. . . . . . . . . . . . . 14 ⊢ Disj 𝑛 ∈ ℕ ((𝑚 ∈ ℕ ↦ ((𝑔‘𝑚) ∖ ∪ 𝑙 ∈ (1..^𝑚)(𝑔‘𝑙)))‘𝑛)
86		nnex 12153	. . . . . . . . . . . . . . . . 17 ⊢ ℕ ∈ V
87	86	mptex 7169	. . . . . . . . . . . . . . . 16 ⊢ (𝑚 ∈ ℕ ↦ ((𝑔‘𝑚) ∖ ∪ 𝑙 ∈ (1..^𝑚)(𝑔‘𝑙))) ∈ V
88		fveq1 6832	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (𝑓 = (𝑚 ∈ ℕ ↦ ((𝑔‘𝑚) ∖ ∪ 𝑙 ∈ (1..^𝑚)(𝑔‘𝑙))) → (𝑓‘𝑛) = ((𝑚 ∈ ℕ ↦ ((𝑔‘𝑚) ∖ ∪ 𝑙 ∈ (1..^𝑚)(𝑔‘𝑙)))‘𝑛))
89	88	eleq1d 2820	. . . . . . . . . . . . . . . . . . . 20 ⊢ (𝑓 = (𝑚 ∈ ℕ ↦ ((𝑔‘𝑚) ∖ ∪ 𝑙 ∈ (1..^𝑚)(𝑔‘𝑙))) → ((𝑓‘𝑛) ∈ dom vol ↔ ((𝑚 ∈ ℕ ↦ ((𝑔‘𝑚) ∖ ∪ 𝑙 ∈ (1..^𝑚)(𝑔‘𝑙)))‘𝑛) ∈ dom vol))
90	88	fveq2d 6837	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (𝑓 = (𝑚 ∈ ℕ ↦ ((𝑔‘𝑚) ∖ ∪ 𝑙 ∈ (1..^𝑚)(𝑔‘𝑙))) → (vol‘(𝑓‘𝑛)) = (vol‘((𝑚 ∈ ℕ ↦ ((𝑔‘𝑚) ∖ ∪ 𝑙 ∈ (1..^𝑚)(𝑔‘𝑙)))‘𝑛)))
91	90	eleq1d 2820	. . . . . . . . . . . . . . . . . . . 20 ⊢ (𝑓 = (𝑚 ∈ ℕ ↦ ((𝑔‘𝑚) ∖ ∪ 𝑙 ∈ (1..^𝑚)(𝑔‘𝑙))) → ((vol‘(𝑓‘𝑛)) ∈ ℝ ↔ (vol‘((𝑚 ∈ ℕ ↦ ((𝑔‘𝑚) ∖ ∪ 𝑙 ∈ (1..^𝑚)(𝑔‘𝑙)))‘𝑛)) ∈ ℝ))
92	89, 91	anbi12d 633	. . . . . . . . . . . . . . . . . . 19 ⊢ (𝑓 = (𝑚 ∈ ℕ ↦ ((𝑔‘𝑚) ∖ ∪ 𝑙 ∈ (1..^𝑚)(𝑔‘𝑙))) → (((𝑓‘𝑛) ∈ dom vol ∧ (vol‘(𝑓‘𝑛)) ∈ ℝ) ↔ (((𝑚 ∈ ℕ ↦ ((𝑔‘𝑚) ∖ ∪ 𝑙 ∈ (1..^𝑚)(𝑔‘𝑙)))‘𝑛) ∈ dom vol ∧ (vol‘((𝑚 ∈ ℕ ↦ ((𝑔‘𝑚) ∖ ∪ 𝑙 ∈ (1..^𝑚)(𝑔‘𝑙)))‘𝑛)) ∈ ℝ)))
93	92	ralbidv 3158	. . . . . . . . . . . . . . . . . 18 ⊢ (𝑓 = (𝑚 ∈ ℕ ↦ ((𝑔‘𝑚) ∖ ∪ 𝑙 ∈ (1..^𝑚)(𝑔‘𝑙))) → (∀𝑛 ∈ ℕ ((𝑓‘𝑛) ∈ dom vol ∧ (vol‘(𝑓‘𝑛)) ∈ ℝ) ↔ ∀𝑛 ∈ ℕ (((𝑚 ∈ ℕ ↦ ((𝑔‘𝑚) ∖ ∪ 𝑙 ∈ (1..^𝑚)(𝑔‘𝑙)))‘𝑛) ∈ dom vol ∧ (vol‘((𝑚 ∈ ℕ ↦ ((𝑔‘𝑚) ∖ ∪ 𝑙 ∈ (1..^𝑚)(𝑔‘𝑙)))‘𝑛)) ∈ ℝ)))
94	88	adantr 480	. . . . . . . . . . . . . . . . . . 19 ⊢ ((𝑓 = (𝑚 ∈ ℕ ↦ ((𝑔‘𝑚) ∖ ∪ 𝑙 ∈ (1..^𝑚)(𝑔‘𝑙))) ∧ 𝑛 ∈ ℕ) → (𝑓‘𝑛) = ((𝑚 ∈ ℕ ↦ ((𝑔‘𝑚) ∖ ∪ 𝑙 ∈ (1..^𝑚)(𝑔‘𝑙)))‘𝑛))
95	94	disjeq2dv 5069	. . . . . . . . . . . . . . . . . 18 ⊢ (𝑓 = (𝑚 ∈ ℕ ↦ ((𝑔‘𝑚) ∖ ∪ 𝑙 ∈ (1..^𝑚)(𝑔‘𝑙))) → (Disj 𝑛 ∈ ℕ (𝑓‘𝑛) ↔ Disj 𝑛 ∈ ℕ ((𝑚 ∈ ℕ ↦ ((𝑔‘𝑚) ∖ ∪ 𝑙 ∈ (1..^𝑚)(𝑔‘𝑙)))‘𝑛)))
96	93, 95	anbi12d 633	. . . . . . . . . . . . . . . . 17 ⊢ (𝑓 = (𝑚 ∈ ℕ ↦ ((𝑔‘𝑚) ∖ ∪ 𝑙 ∈ (1..^𝑚)(𝑔‘𝑙))) → ((∀𝑛 ∈ ℕ ((𝑓‘𝑛) ∈ dom vol ∧ (vol‘(𝑓‘𝑛)) ∈ ℝ) ∧ Disj 𝑛 ∈ ℕ (𝑓‘𝑛)) ↔ (∀𝑛 ∈ ℕ (((𝑚 ∈ ℕ ↦ ((𝑔‘𝑚) ∖ ∪ 𝑙 ∈ (1..^𝑚)(𝑔‘𝑙)))‘𝑛) ∈ dom vol ∧ (vol‘((𝑚 ∈ ℕ ↦ ((𝑔‘𝑚) ∖ ∪ 𝑙 ∈ (1..^𝑚)(𝑔‘𝑙)))‘𝑛)) ∈ ℝ) ∧ Disj 𝑛 ∈ ℕ ((𝑚 ∈ ℕ ↦ ((𝑔‘𝑚) ∖ ∪ 𝑙 ∈ (1..^𝑚)(𝑔‘𝑙)))‘𝑛))))
97	88	iuneq2d 4976	. . . . . . . . . . . . . . . . . . 19 ⊢ (𝑓 = (𝑚 ∈ ℕ ↦ ((𝑔‘𝑚) ∖ ∪ 𝑙 ∈ (1..^𝑚)(𝑔‘𝑙))) → ∪ 𝑛 ∈ ℕ (𝑓‘𝑛) = ∪ 𝑛 ∈ ℕ ((𝑚 ∈ ℕ ↦ ((𝑔‘𝑚) ∖ ∪ 𝑙 ∈ (1..^𝑚)(𝑔‘𝑙)))‘𝑛))
98	97	fveq2d 6837	. . . . . . . . . . . . . . . . . 18 ⊢ (𝑓 = (𝑚 ∈ ℕ ↦ ((𝑔‘𝑚) ∖ ∪ 𝑙 ∈ (1..^𝑚)(𝑔‘𝑙))) → (vol‘∪ 𝑛 ∈ ℕ (𝑓‘𝑛)) = (vol‘∪ 𝑛 ∈ ℕ ((𝑚 ∈ ℕ ↦ ((𝑔‘𝑚) ∖ ∪ 𝑙 ∈ (1..^𝑚)(𝑔‘𝑙)))‘𝑛)))
99		voliunnfl.1	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ 𝑆 = seq1( + , 𝐺)
100		voliunnfl.2	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ 𝐺 = (𝑛 ∈ ℕ ↦ (vol‘(𝑓‘𝑛)))
101		seqeq3 13931	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ (𝐺 = (𝑛 ∈ ℕ ↦ (vol‘(𝑓‘𝑛))) → seq1( + , 𝐺) = seq1( + , (𝑛 ∈ ℕ ↦ (vol‘(𝑓‘𝑛)))))
102	100, 101	ax-mp 5	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ seq1( + , 𝐺) = seq1( + , (𝑛 ∈ ℕ ↦ (vol‘(𝑓‘𝑛))))
103	99, 102	eqtri 2758	. . . . . . . . . . . . . . . . . . . . 21 ⊢ 𝑆 = seq1( + , (𝑛 ∈ ℕ ↦ (vol‘(𝑓‘𝑛))))
104	103	rneqi 5885	. . . . . . . . . . . . . . . . . . . 20 ⊢ ran 𝑆 = ran seq1( + , (𝑛 ∈ ℕ ↦ (vol‘(𝑓‘𝑛))))
105	104	supeq1i 9352	. . . . . . . . . . . . . . . . . . 19 ⊢ sup(ran 𝑆, ℝ*, < ) = sup(ran seq1( + , (𝑛 ∈ ℕ ↦ (vol‘(𝑓‘𝑛)))), ℝ*, < )
106	90	mpteq2dv 5191	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (𝑓 = (𝑚 ∈ ℕ ↦ ((𝑔‘𝑚) ∖ ∪ 𝑙 ∈ (1..^𝑚)(𝑔‘𝑙))) → (𝑛 ∈ ℕ ↦ (vol‘(𝑓‘𝑛))) = (𝑛 ∈ ℕ ↦ (vol‘((𝑚 ∈ ℕ ↦ ((𝑔‘𝑚) ∖ ∪ 𝑙 ∈ (1..^𝑚)(𝑔‘𝑙)))‘𝑛))))
107	106	seqeq3d 13934	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (𝑓 = (𝑚 ∈ ℕ ↦ ((𝑔‘𝑚) ∖ ∪ 𝑙 ∈ (1..^𝑚)(𝑔‘𝑙))) → seq1( + , (𝑛 ∈ ℕ ↦ (vol‘(𝑓‘𝑛)))) = seq1( + , (𝑛 ∈ ℕ ↦ (vol‘((𝑚 ∈ ℕ ↦ ((𝑔‘𝑚) ∖ ∪ 𝑙 ∈ (1..^𝑚)(𝑔‘𝑙)))‘𝑛)))))
108	107	rneqd 5886	. . . . . . . . . . . . . . . . . . . 20 ⊢ (𝑓 = (𝑚 ∈ ℕ ↦ ((𝑔‘𝑚) ∖ ∪ 𝑙 ∈ (1..^𝑚)(𝑔‘𝑙))) → ran seq1( + , (𝑛 ∈ ℕ ↦ (vol‘(𝑓‘𝑛)))) = ran seq1( + , (𝑛 ∈ ℕ ↦ (vol‘((𝑚 ∈ ℕ ↦ ((𝑔‘𝑚) ∖ ∪ 𝑙 ∈ (1..^𝑚)(𝑔‘𝑙)))‘𝑛)))))
109	108	supeq1d 9351	. . . . . . . . . . . . . . . . . . 19 ⊢ (𝑓 = (𝑚 ∈ ℕ ↦ ((𝑔‘𝑚) ∖ ∪ 𝑙 ∈ (1..^𝑚)(𝑔‘𝑙))) → sup(ran seq1( + , (𝑛 ∈ ℕ ↦ (vol‘(𝑓‘𝑛)))), ℝ*, < ) = sup(ran seq1( + , (𝑛 ∈ ℕ ↦ (vol‘((𝑚 ∈ ℕ ↦ ((𝑔‘𝑚) ∖ ∪ 𝑙 ∈ (1..^𝑚)(𝑔‘𝑙)))‘𝑛)))), ℝ*, < ))
110	105, 109	eqtrid 2782	. . . . . . . . . . . . . . . . . 18 ⊢ (𝑓 = (𝑚 ∈ ℕ ↦ ((𝑔‘𝑚) ∖ ∪ 𝑙 ∈ (1..^𝑚)(𝑔‘𝑙))) → sup(ran 𝑆, ℝ*, < ) = sup(ran seq1( + , (𝑛 ∈ ℕ ↦ (vol‘((𝑚 ∈ ℕ ↦ ((𝑔‘𝑚) ∖ ∪ 𝑙 ∈ (1..^𝑚)(𝑔‘𝑙)))‘𝑛)))), ℝ*, < ))
111	98, 110	eqeq12d 2751	. . . . . . . . . . . . . . . . 17 ⊢ (𝑓 = (𝑚 ∈ ℕ ↦ ((𝑔‘𝑚) ∖ ∪ 𝑙 ∈ (1..^𝑚)(𝑔‘𝑙))) → ((vol‘∪ 𝑛 ∈ ℕ (𝑓‘𝑛)) = sup(ran 𝑆, ℝ*, < ) ↔ (vol‘∪ 𝑛 ∈ ℕ ((𝑚 ∈ ℕ ↦ ((𝑔‘𝑚) ∖ ∪ 𝑙 ∈ (1..^𝑚)(𝑔‘𝑙)))‘𝑛)) = sup(ran seq1( + , (𝑛 ∈ ℕ ↦ (vol‘((𝑚 ∈ ℕ ↦ ((𝑔‘𝑚) ∖ ∪ 𝑙 ∈ (1..^𝑚)(𝑔‘𝑙)))‘𝑛)))), ℝ*, < )))
112	96, 111	imbi12d 344	. . . . . . . . . . . . . . . 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 3514	. . . . . . . . . . . . . . 15 ⊢ ((∀𝑛 ∈ ℕ (((𝑚 ∈ ℕ ↦ ((𝑔‘𝑚) ∖ ∪ 𝑙 ∈ (1..^𝑚)(𝑔‘𝑙)))‘𝑛) ∈ dom vol ∧ (vol‘((𝑚 ∈ ℕ ↦ ((𝑔‘𝑚) ∖ ∪ 𝑙 ∈ (1..^𝑚)(𝑔‘𝑙)))‘𝑛)) ∈ ℝ) ∧ Disj 𝑛 ∈ ℕ ((𝑚 ∈ ℕ ↦ ((𝑔‘𝑚) ∖ ∪ 𝑙 ∈ (1..^𝑚)(𝑔‘𝑙)))‘𝑛)) → (vol‘∪ 𝑛 ∈ ℕ ((𝑚 ∈ ℕ ↦ ((𝑔‘𝑚) ∖ ∪ 𝑙 ∈ (1..^𝑚)(𝑔‘𝑙)))‘𝑛)) = sup(ran seq1( + , (𝑛 ∈ ℕ ↦ (vol‘((𝑚 ∈ ℕ ↦ ((𝑔‘𝑚) ∖ ∪ 𝑙 ∈ (1..^𝑚)(𝑔‘𝑙)))‘𝑛)))), ℝ*, < ))
115	64	iuneq2i 4967	. . . . . . . . . . . . . . . 16 ⊢ ∪ 𝑛 ∈ ℕ ((𝑚 ∈ ℕ ↦ ((𝑔‘𝑚) ∖ ∪ 𝑙 ∈ (1..^𝑚)(𝑔‘𝑙)))‘𝑛) = ∪ 𝑛 ∈ ℕ ((𝑔‘𝑛) ∖ ∪ 𝑙 ∈ (1..^𝑛)(𝑔‘𝑙))
116	115	fveq2i 6836	. . . . . . . . . . . . . . 15 ⊢ (vol‘∪ 𝑛 ∈ ℕ ((𝑚 ∈ ℕ ↦ ((𝑔‘𝑚) ∖ ∪ 𝑙 ∈ (1..^𝑚)(𝑔‘𝑙)))‘𝑛)) = (vol‘∪ 𝑛 ∈ ℕ ((𝑔‘𝑛) ∖ ∪ 𝑙 ∈ (1..^𝑛)(𝑔‘𝑙)))
117	66	mpteq2ia 5192	. . . . . . . . . . . . . . . . . 18 ⊢ (𝑛 ∈ ℕ ↦ (vol‘((𝑚 ∈ ℕ ↦ ((𝑔‘𝑚) ∖ ∪ 𝑙 ∈ (1..^𝑚)(𝑔‘𝑙)))‘𝑛))) = (𝑛 ∈ ℕ ↦ (vol‘((𝑔‘𝑛) ∖ ∪ 𝑙 ∈ (1..^𝑛)(𝑔‘𝑙))))
118		seqeq3 13931	. . . . . . . . . . . . . . . . . 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 5885	. . . . . . . . . . . . . . . 16 ⊢ ran seq1( + , (𝑛 ∈ ℕ ↦ (vol‘((𝑚 ∈ ℕ ↦ ((𝑔‘𝑚) ∖ ∪ 𝑙 ∈ (1..^𝑚)(𝑔‘𝑙)))‘𝑛)))) = ran seq1( + , (𝑛 ∈ ℕ ↦ (vol‘((𝑔‘𝑛) ∖ ∪ 𝑙 ∈ (1..^𝑛)(𝑔‘𝑙)))))
121	120	supeq1i 9352	. . . . . . . . . . . . . . 15 ⊢ sup(ran seq1( + , (𝑛 ∈ ℕ ↦ (vol‘((𝑚 ∈ ℕ ↦ ((𝑔‘𝑚) ∖ ∪ 𝑙 ∈ (1..^𝑚)(𝑔‘𝑙)))‘𝑛)))), ℝ*, < ) = sup(ran seq1( + , (𝑛 ∈ ℕ ↦ (vol‘((𝑔‘𝑛) ∖ ∪ 𝑙 ∈ (1..^𝑛)(𝑔‘𝑙))))), ℝ*, < )
122	114, 116, 121	3eqtr3g 2793	. . . . . . . . . . . . . 14 ⊢ ((∀𝑛 ∈ ℕ (((𝑚 ∈ ℕ ↦ ((𝑔‘𝑚) ∖ ∪ 𝑙 ∈ (1..^𝑚)(𝑔‘𝑙)))‘𝑛) ∈ dom vol ∧ (vol‘((𝑚 ∈ ℕ ↦ ((𝑔‘𝑚) ∖ ∪ 𝑙 ∈ (1..^𝑚)(𝑔‘𝑙)))‘𝑛)) ∈ ℝ) ∧ Disj 𝑛 ∈ ℕ ((𝑚 ∈ ℕ ↦ ((𝑔‘𝑚) ∖ ∪ 𝑙 ∈ (1..^𝑚)(𝑔‘𝑙)))‘𝑛)) → (vol‘∪ 𝑛 ∈ ℕ ((𝑔‘𝑛) ∖ ∪ 𝑙 ∈ (1..^𝑛)(𝑔‘𝑙))) = sup(ran seq1( + , (𝑛 ∈ ℕ ↦ (vol‘((𝑔‘𝑛) ∖ ∪ 𝑙 ∈ (1..^𝑛)(𝑔‘𝑙))))), ℝ*, < ))
123	80, 85, 122	sylancl 587	. . . . . . . . . . . . 13 ⊢ (∀𝑚 ∈ ℕ ((𝑔‘𝑚) ⊆ ℝ ∧ (vol*‘(𝑔‘𝑚)) = 0) → (vol‘∪ 𝑛 ∈ ℕ ((𝑔‘𝑛) ∖ ∪ 𝑙 ∈ (1..^𝑛)(𝑔‘𝑙))) = sup(ran seq1( + , (𝑛 ∈ ℕ ↦ (vol‘((𝑔‘𝑛) ∖ ∪ 𝑙 ∈ (1..^𝑛)(𝑔‘𝑙))))), ℝ*, < ))
124	123	adantl 481	. . . . . . . . . . . 12 ⊢ ((𝑔:ℕ–onto→𝐴 ∧ ∀𝑚 ∈ ℕ ((𝑔‘𝑚) ⊆ ℝ ∧ (vol*‘(𝑔‘𝑚)) = 0)) → (vol‘∪ 𝑛 ∈ ℕ ((𝑔‘𝑛) ∖ ∪ 𝑙 ∈ (1..^𝑛)(𝑔‘𝑙))) = sup(ran seq1( + , (𝑛 ∈ ℕ ↦ (vol‘((𝑔‘𝑛) ∖ ∪ 𝑙 ∈ (1..^𝑛)(𝑔‘𝑙))))), ℝ*, < ))
125	81	iundisj 25507	. . . . . . . . . . . . . . . 16 ⊢ ∪ 𝑛 ∈ ℕ (𝑔‘𝑛) = ∪ 𝑛 ∈ ℕ ((𝑔‘𝑛) ∖ ∪ 𝑙 ∈ (1..^𝑛)(𝑔‘𝑙))
126		fofun 6746	. . . . . . . . . . . . . . . . 17 ⊢ (𝑔:ℕ–onto→𝐴 → Fun 𝑔)
127		funiunfv 7194	. . . . . . . . . . . . . . . . 17 ⊢ (Fun 𝑔 → ∪ 𝑛 ∈ ℕ (𝑔‘𝑛) = ∪ (𝑔 “ ℕ))
128	126, 127	syl 17	. . . . . . . . . . . . . . . 16 ⊢ (𝑔:ℕ–onto→𝐴 → ∪ 𝑛 ∈ ℕ (𝑔‘𝑛) = ∪ (𝑔 “ ℕ))
129	125, 128	eqtr3id 2784	. . . . . . . . . . . . . . 15 ⊢ (𝑔:ℕ–onto→𝐴 → ∪ 𝑛 ∈ ℕ ((𝑔‘𝑛) ∖ ∪ 𝑙 ∈ (1..^𝑛)(𝑔‘𝑙)) = ∪ (𝑔 “ ℕ))
130	29	unieqd 4875	. . . . . . . . . . . . . . 15 ⊢ (𝑔:ℕ–onto→𝐴 → ∪ (𝑔 “ ℕ) = ∪ 𝐴)
131	129, 130	eqtrd 2770	. . . . . . . . . . . . . 14 ⊢ (𝑔:ℕ–onto→𝐴 → ∪ 𝑛 ∈ ℕ ((𝑔‘𝑛) ∖ ∪ 𝑙 ∈ (1..^𝑛)(𝑔‘𝑙)) = ∪ 𝐴)
132	131	fveq2d 6837	. . . . . . . . . . . . 13 ⊢ (𝑔:ℕ–onto→𝐴 → (vol‘∪ 𝑛 ∈ ℕ ((𝑔‘𝑛) ∖ ∪ 𝑙 ∈ (1..^𝑛)(𝑔‘𝑙))) = (vol‘∪ 𝐴))
133	132	adantr 480	. . . . . . . . . . . 12 ⊢ ((𝑔:ℕ–onto→𝐴 ∧ ∀𝑚 ∈ ℕ ((𝑔‘𝑚) ⊆ ℝ ∧ (vol*‘(𝑔‘𝑚)) = 0)) → (vol‘∪ 𝑛 ∈ ℕ ((𝑔‘𝑛) ∖ ∪ 𝑙 ∈ (1..^𝑛)(𝑔‘𝑙))) = (vol‘∪ 𝐴))
134	56	sseq1d 3964	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (𝑚 = 𝑛 → ((𝑔‘𝑚) ⊆ ℝ ↔ (𝑔‘𝑛) ⊆ ℝ))
135	56	fveqeq2d 6841	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (𝑚 = 𝑛 → ((vol*‘(𝑔‘𝑚)) = 0 ↔ (vol*‘(𝑔‘𝑛)) = 0))
136	134, 135	anbi12d 633	. . . . . . . . . . . . . . . . . . . 20 ⊢ (𝑚 = 𝑛 → (((𝑔‘𝑚) ⊆ ℝ ∧ (vol*‘(𝑔‘𝑚)) = 0) ↔ ((𝑔‘𝑛) ⊆ ℝ ∧ (vol*‘(𝑔‘𝑛)) = 0)))
137	136	rspccva 3574	. . . . . . . . . . . . . . . . . . 19 ⊢ ((∀𝑚 ∈ ℕ ((𝑔‘𝑚) ⊆ ℝ ∧ (vol*‘(𝑔‘𝑚)) = 0) ∧ 𝑛 ∈ ℕ) → ((𝑔‘𝑛) ⊆ ℝ ∧ (vol*‘(𝑔‘𝑛)) = 0))
138		ssdifss 4091	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ ((𝑔‘𝑛) ⊆ ℝ → ((𝑔‘𝑛) ∖ ∪ 𝑙 ∈ (1..^𝑛)(𝑔‘𝑙)) ⊆ ℝ)
139	138	adantr 480	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (((𝑔‘𝑛) ⊆ ℝ ∧ (vol*‘(𝑔‘𝑛)) = 0) → ((𝑔‘𝑛) ∖ ∪ 𝑙 ∈ (1..^𝑛)(𝑔‘𝑙)) ⊆ ℝ)
140		difss 4087	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ ((𝑔‘𝑛) ∖ ∪ 𝑙 ∈ (1..^𝑛)(𝑔‘𝑙)) ⊆ (𝑔‘𝑛)
141		ovolssnul 25446	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ ((((𝑔‘𝑛) ∖ ∪ 𝑙 ∈ (1..^𝑛)(𝑔‘𝑙)) ⊆ (𝑔‘𝑛) ∧ (𝑔‘𝑛) ⊆ ℝ ∧ (vol*‘(𝑔‘𝑛)) = 0) → (vol*‘((𝑔‘𝑛) ∖ ∪ 𝑙 ∈ (1..^𝑛)(𝑔‘𝑙))) = 0)
142	140, 141	mp3an1 1451	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (((𝑔‘𝑛) ⊆ ℝ ∧ (vol*‘(𝑔‘𝑛)) = 0) → (vol*‘((𝑔‘𝑛) ∖ ∪ 𝑙 ∈ (1..^𝑛)(𝑔‘𝑙))) = 0)
143	139, 142	jca 511	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (((𝑔‘𝑛) ⊆ ℝ ∧ (vol*‘(𝑔‘𝑛)) = 0) → (((𝑔‘𝑛) ∖ ∪ 𝑙 ∈ (1..^𝑛)(𝑔‘𝑙)) ⊆ ℝ ∧ (vol*‘((𝑔‘𝑛) ∖ ∪ 𝑙 ∈ (1..^𝑛)(𝑔‘𝑙))) = 0))
144		nulmbl 25494	. . . . . . . . . . . . . . . . . . . . 21 ⊢ ((((𝑔‘𝑛) ∖ ∪ 𝑙 ∈ (1..^𝑛)(𝑔‘𝑙)) ⊆ ℝ ∧ (vol*‘((𝑔‘𝑛) ∖ ∪ 𝑙 ∈ (1..^𝑛)(𝑔‘𝑙))) = 0) → ((𝑔‘𝑛) ∖ ∪ 𝑙 ∈ (1..^𝑛)(𝑔‘𝑙)) ∈ dom vol)
145		mblvol 25489	. . . . . . . . . . . . . . . . . . . . 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 2770	. . . . . . . . . . . . . . . . . . 19 ⊢ (((𝑔‘𝑛) ⊆ ℝ ∧ (vol*‘(𝑔‘𝑛)) = 0) → (vol‘((𝑔‘𝑛) ∖ ∪ 𝑙 ∈ (1..^𝑛)(𝑔‘𝑙))) = 0)
148	137, 147	syl 17	. . . . . . . . . . . . . . . . . 18 ⊢ ((∀𝑚 ∈ ℕ ((𝑔‘𝑚) ⊆ ℝ ∧ (vol*‘(𝑔‘𝑚)) = 0) ∧ 𝑛 ∈ ℕ) → (vol‘((𝑔‘𝑛) ∖ ∪ 𝑙 ∈ (1..^𝑛)(𝑔‘𝑙))) = 0)
149	148	mpteq2dva 5190	. . . . . . . . . . . . . . . . 17 ⊢ (∀𝑚 ∈ ℕ ((𝑔‘𝑚) ⊆ ℝ ∧ (vol*‘(𝑔‘𝑚)) = 0) → (𝑛 ∈ ℕ ↦ (vol‘((𝑔‘𝑛) ∖ ∪ 𝑙 ∈ (1..^𝑛)(𝑔‘𝑙)))) = (𝑛 ∈ ℕ ↦ 0))
150	149	seqeq3d 13934	. . . . . . . . . . . . . . . 16 ⊢ (∀𝑚 ∈ ℕ ((𝑔‘𝑚) ⊆ ℝ ∧ (vol*‘(𝑔‘𝑚)) = 0) → seq1( + , (𝑛 ∈ ℕ ↦ (vol‘((𝑔‘𝑛) ∖ ∪ 𝑙 ∈ (1..^𝑛)(𝑔‘𝑙))))) = seq1( + , (𝑛 ∈ ℕ ↦ 0)))
151	150	rneqd 5886	. . . . . . . . . . . . . . 15 ⊢ (∀𝑚 ∈ ℕ ((𝑔‘𝑚) ⊆ ℝ ∧ (vol*‘(𝑔‘𝑚)) = 0) → ran seq1( + , (𝑛 ∈ ℕ ↦ (vol‘((𝑔‘𝑛) ∖ ∪ 𝑙 ∈ (1..^𝑛)(𝑔‘𝑙))))) = ran seq1( + , (𝑛 ∈ ℕ ↦ 0)))
152	151	supeq1d 9351	. . . . . . . . . . . . . 14 ⊢ (∀𝑚 ∈ ℕ ((𝑔‘𝑚) ⊆ ℝ ∧ (vol*‘(𝑔‘𝑚)) = 0) → sup(ran seq1( + , (𝑛 ∈ ℕ ↦ (vol‘((𝑔‘𝑛) ∖ ∪ 𝑙 ∈ (1..^𝑛)(𝑔‘𝑙))))), ℝ*, < ) = sup(ran seq1( + , (𝑛 ∈ ℕ ↦ 0)), ℝ*, < ))
153		0cn 11126	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ 0 ∈ ℂ
154		ser1const 13983	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ ((0 ∈ ℂ ∧ 𝑚 ∈ ℕ) → (seq1( + , (ℕ × {0}))‘𝑚) = (𝑚 · 0))
155	153, 154	mpan 691	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (𝑚 ∈ ℕ → (seq1( + , (ℕ × {0}))‘𝑚) = (𝑚 · 0))
156		nncn 12155	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (𝑚 ∈ ℕ → 𝑚 ∈ ℂ)
157	156	mul01d 11334	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (𝑚 ∈ ℕ → (𝑚 · 0) = 0)
158	155, 157	eqtrd 2770	. . . . . . . . . . . . . . . . . . . 20 ⊢ (𝑚 ∈ ℕ → (seq1( + , (ℕ × {0}))‘𝑚) = 0)
159	158	mpteq2ia 5192	. . . . . . . . . . . . . . . . . . 19 ⊢ (𝑚 ∈ ℕ ↦ (seq1( + , (ℕ × {0}))‘𝑚)) = (𝑚 ∈ ℕ ↦ 0)
160		fconstmpt 5685	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (ℕ × {0}) = (𝑛 ∈ ℕ ↦ 0)
161		seqeq3 13931	. . . . . . . . . . . . . . . . . . . . 21 ⊢ ((ℕ × {0}) = (𝑛 ∈ ℕ ↦ 0) → seq1( + , (ℕ × {0})) = seq1( + , (𝑛 ∈ ℕ ↦ 0)))
162	160, 161	ax-mp 5	. . . . . . . . . . . . . . . . . . . 20 ⊢ seq1( + , (ℕ × {0})) = seq1( + , (𝑛 ∈ ℕ ↦ 0))
163		1z 12523	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ 1 ∈ ℤ
164		seqfn 13938	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (1 ∈ ℤ → seq1( + , (ℕ × {0})) Fn (ℤ≥‘1))
165	163, 164	ax-mp 5	. . . . . . . . . . . . . . . . . . . . 21 ⊢ seq1( + , (ℕ × {0})) Fn (ℤ≥‘1)
166		nnuz 12792	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ ℕ = (ℤ≥‘1)
167	166	fneq2i 6589	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (seq1( + , (ℕ × {0})) Fn ℕ ↔ seq1( + , (ℕ × {0})) Fn (ℤ≥‘1))
168		dffn5 6891	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (seq1( + , (ℕ × {0})) Fn ℕ ↔ seq1( + , (ℕ × {0})) = (𝑚 ∈ ℕ ↦ (seq1( + , (ℕ × {0}))‘𝑚)))
169	167, 168	bitr3i 277	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (seq1( + , (ℕ × {0})) Fn (ℤ≥‘1) ↔ seq1( + , (ℕ × {0})) = (𝑚 ∈ ℕ ↦ (seq1( + , (ℕ × {0}))‘𝑚)))
170	165, 169	mpbi 230	. . . . . . . . . . . . . . . . . . . 20 ⊢ seq1( + , (ℕ × {0})) = (𝑚 ∈ ℕ ↦ (seq1( + , (ℕ × {0}))‘𝑚))
171	162, 170	eqtr3i 2760	. . . . . . . . . . . . . . . . . . 19 ⊢ seq1( + , (𝑛 ∈ ℕ ↦ 0)) = (𝑚 ∈ ℕ ↦ (seq1( + , (ℕ × {0}))‘𝑚))
172		fconstmpt 5685	. . . . . . . . . . . . . . . . . . 19 ⊢ (ℕ × {0}) = (𝑚 ∈ ℕ ↦ 0)
173	159, 171, 172	3eqtr4i 2768	. . . . . . . . . . . . . . . . . 18 ⊢ seq1( + , (𝑛 ∈ ℕ ↦ 0)) = (ℕ × {0})
174	173	rneqi 5885	. . . . . . . . . . . . . . . . 17 ⊢ ran seq1( + , (𝑛 ∈ ℕ ↦ 0)) = ran (ℕ × {0})
175		1nn 12158	. . . . . . . . . . . . . . . . . 18 ⊢ 1 ∈ ℕ
176		ne0i 4292	. . . . . . . . . . . . . . . . . 18 ⊢ (1 ∈ ℕ → ℕ ≠ ∅)
177		rnxp 6127	. . . . . . . . . . . . . . . . . 18 ⊢ (ℕ ≠ ∅ → ran (ℕ × {0}) = {0})
178	175, 176, 177	mp2b 10	. . . . . . . . . . . . . . . . 17 ⊢ ran (ℕ × {0}) = {0}
179	174, 178	eqtri 2758	. . . . . . . . . . . . . . . 16 ⊢ ran seq1( + , (𝑛 ∈ ℕ ↦ 0)) = {0}
180	179	supeq1i 9352	. . . . . . . . . . . . . . 15 ⊢ sup(ran seq1( + , (𝑛 ∈ ℕ ↦ 0)), ℝ*, < ) = sup({0}, ℝ*, < )
181		xrltso 13057	. . . . . . . . . . . . . . . 16 ⊢ < Or ℝ*
182		0xr 11181	. . . . . . . . . . . . . . . 16 ⊢ 0 ∈ ℝ*
183		supsn 9378	. . . . . . . . . . . . . . . 16 ⊢ (( < Or ℝ* ∧ 0 ∈ ℝ*) → sup({0}, ℝ*, < ) = 0)
184	181, 182, 183	mp2an 693	. . . . . . . . . . . . . . 15 ⊢ sup({0}, ℝ*, < ) = 0
185	180, 184	eqtri 2758	. . . . . . . . . . . . . 14 ⊢ sup(ran seq1( + , (𝑛 ∈ ℕ ↦ 0)), ℝ*, < ) = 0
186	152, 185	eqtrdi 2786	. . . . . . . . . . . . 13 ⊢ (∀𝑚 ∈ ℕ ((𝑔‘𝑚) ⊆ ℝ ∧ (vol*‘(𝑔‘𝑚)) = 0) → sup(ran seq1( + , (𝑛 ∈ ℕ ↦ (vol‘((𝑔‘𝑛) ∖ ∪ 𝑙 ∈ (1..^𝑛)(𝑔‘𝑙))))), ℝ*, < ) = 0)
187	186	adantl 481	. . . . . . . . . . . 12 ⊢ ((𝑔:ℕ–onto→𝐴 ∧ ∀𝑚 ∈ ℕ ((𝑔‘𝑚) ⊆ ℝ ∧ (vol*‘(𝑔‘𝑚)) = 0)) → sup(ran seq1( + , (𝑛 ∈ ℕ ↦ (vol‘((𝑔‘𝑛) ∖ ∪ 𝑙 ∈ (1..^𝑛)(𝑔‘𝑙))))), ℝ*, < ) = 0)
188	124, 133, 187	3eqtr3rd 2779	. . . . . . . . . . 11 ⊢ ((𝑔:ℕ–onto→𝐴 ∧ ∀𝑚 ∈ ℕ ((𝑔‘𝑚) ⊆ ℝ ∧ (vol*‘(𝑔‘𝑚)) = 0)) → 0 = (vol‘∪ 𝐴))
189	188	ex 412	. . . . . . . . . 10 ⊢ (𝑔:ℕ–onto→𝐴 → (∀𝑚 ∈ ℕ ((𝑔‘𝑚) ⊆ ℝ ∧ (vol*‘(𝑔‘𝑚)) = 0) → 0 = (vol‘∪ 𝐴)))
190	38, 189	sylbid 240	. . . . . . . . 9 ⊢ (𝑔:ℕ–onto→𝐴 → (∀𝑥 ∈ 𝐴 (𝑥 ⊆ ℝ ∧ (vol*‘𝑥) = 0) → 0 = (vol‘∪ 𝐴)))
191	28, 190	syl5 34	. . . . . . . 8 ⊢ (𝑔:ℕ–onto→𝐴 → ((∀𝑥 ∈ 𝐴 𝑥 ≼ ℕ ∧ ∪ 𝐴 ⊆ ℝ) → 0 = (vol‘∪ 𝐴)))
192	191	exlimiv 1932	. . . . . . 7 ⊢ (∃𝑔 𝑔:ℕ–onto→𝐴 → ((∀𝑥 ∈ 𝐴 𝑥 ≼ ℕ ∧ ∪ 𝐴 ⊆ ℝ) → 0 = (vol‘∪ 𝐴)))
193	18, 192	syl 17	. . . . . 6 ⊢ ((𝐴 ≠ ∅ ∧ 𝐴 ≼ ℕ) → ((∀𝑥 ∈ 𝐴 𝑥 ≼ ℕ ∧ ∪ 𝐴 ⊆ ℝ) → 0 = (vol‘∪ 𝐴)))
194	193	expimpd 453	. . . . 5 ⊢ (𝐴 ≠ ∅ → ((𝐴 ≼ ℕ ∧ (∀𝑥 ∈ 𝐴 𝑥 ≼ ℕ ∧ ∪ 𝐴 ⊆ ℝ)) → 0 = (vol‘∪ 𝐴)))
195	11, 194	pm2.61ine 3014	. . . 4 ⊢ ((𝐴 ≼ ℕ ∧ (∀𝑥 ∈ 𝐴 𝑥 ≼ ℕ ∧ ∪ 𝐴 ⊆ ℝ)) → 0 = (vol‘∪ 𝐴))
196		renepnf 11182	. . . . . . 7 ⊢ (0 ∈ ℝ → 0 ≠ +∞)
197	47, 196	mp1i 13	. . . . . 6 ⊢ (∪ 𝐴 = ℝ → 0 ≠ +∞)
198		fveq2 6833	. . . . . . 7 ⊢ (∪ 𝐴 = ℝ → (vol‘∪ 𝐴) = (vol‘ℝ))
199		rembl 25499	. . . . . . . . 9 ⊢ ℝ ∈ dom vol
200		mblvol 25489	. . . . . . . . 9 ⊢ (ℝ ∈ dom vol → (vol‘ℝ) = (vol*‘ℝ))
201	199, 200	ax-mp 5	. . . . . . . 8 ⊢ (vol‘ℝ) = (vol*‘ℝ)
202		ovolre 25484	. . . . . . . 8 ⊢ (vol*‘ℝ) = +∞
203	201, 202	eqtri 2758	. . . . . . 7 ⊢ (vol‘ℝ) = +∞
204	198, 203	eqtrdi 2786	. . . . . 6 ⊢ (∪ 𝐴 = ℝ → (vol‘∪ 𝐴) = +∞)
205	197, 204	neeqtrrd 3005	. . . . 5 ⊢ (∪ 𝐴 = ℝ → 0 ≠ (vol‘∪ 𝐴))
206	205	necon2i 2965	. . . 4 ⊢ (0 = (vol‘∪ 𝐴) → ∪ 𝐴 ≠ ℝ)
207	195, 206	syl 17	. . 3 ⊢ ((𝐴 ≼ ℕ ∧ (∀𝑥 ∈ 𝐴 𝑥 ≼ ℕ ∧ ∪ 𝐴 ⊆ ℝ)) → ∪ 𝐴 ≠ ℝ)
208	207	expr 456	. 2 ⊢ ((𝐴 ≼ ℕ ∧ ∀𝑥 ∈ 𝐴 𝑥 ≼ ℕ) → (∪ 𝐴 ⊆ ℝ → ∪ 𝐴 ≠ ℝ))
209		eqimss 3991	. . 3 ⊢ (∪ 𝐴 = ℝ → ∪ 𝐴 ⊆ ℝ)
210	209	necon3bi 2957	. 2 ⊢ (¬ ∪ 𝐴 ⊆ ℝ → ∪ 𝐴 ≠ ℝ)
211	208, 210	pm2.61d1 180	1 ⊢ ((𝐴 ≼ ℕ ∧ ∀𝑥 ∈ 𝐴 𝑥 ≼ ℕ) → ∪ 𝐴 ≠ ℝ)

Syntax hints:   → wi 4   ↔ wb 206   ∧ wa 395   = wceq 1542  ∃wex 1781   ∈ wcel 2114   ≠ wne 2931  ∀wral 3050  Vcvv 3439   ∖ cdif 3897   ⊆ wss 3900  ∅c0 4284  {csn 4579  ∪ cuni 4862  ∪ ciun 4945  Disj wdisj 5064   class class class wbr 5097   ↦ cmpt 5178   Or wor 5530   × cxp 5621  dom cdm 5623  ran crn 5624   “ cima 5626  Fun wfun 6485   Fn wfn 6486  –onto→wfo 6489  ‘cfv 6491  (class class class)co 7358   ≼ cdom 8883   ≺ csdm 8884  supcsup 9345  ℂcc 11026  ℝcr 11027  0cc0 11028  1c1 11029   + caddc 11031   · cmul 11033  +∞cpnf 11165  ℝ^*cxr 11167   < clt 11168  ℕcn 12147  ℤcz 12490  ℤ_≥cuz 12753  ..^cfzo 13572  seqcseq 13926  vol*covol 25421  volcvol 25422

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1797  ax-4 1811  ax-5 1912  ax-6 1969  ax-7 2010  ax-8 2116  ax-9 2124  ax-10 2147  ax-11 2163  ax-12 2183  ax-ext 2707  ax-rep 5223  ax-sep 5240  ax-nul 5250  ax-pow 5309  ax-pr 5376  ax-un 7680  ax-inf2 9552  ax-cnex 11084  ax-resscn 11085  ax-1cn 11086  ax-icn 11087  ax-addcl 11088  ax-addrcl 11089  ax-mulcl 11090  ax-mulrcl 11091  ax-mulcom 11092  ax-addass 11093  ax-mulass 11094  ax-distr 11095  ax-i2m1 11096  ax-1ne0 11097  ax-1rid 11098  ax-rnegex 11099  ax-rrecex 11100  ax-cnre 11101  ax-pre-lttri 11102  ax-pre-lttrn 11103  ax-pre-ltadd 11104  ax-pre-mulgt0 11105  ax-pre-sup 11106

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 849  df-3or 1088  df-3an 1089  df-tru 1545  df-fal 1555  df-ex 1782  df-nf 1786  df-sb 2069  df-mo 2538  df-eu 2568  df-clab 2714  df-cleq 2727  df-clel 2810  df-nfc 2884  df-ne 2932  df-nel 3036  df-ral 3051  df-rex 3060  df-rmo 3349  df-reu 3350  df-rab 3399  df-v 3441  df-sbc 3740  df-csb 3849  df-dif 3903  df-un 3905  df-in 3907  df-ss 3917  df-pss 3920  df-nul 4285  df-if 4479  df-pw 4555  df-sn 4580  df-pr 4582  df-op 4586  df-uni 4863  df-int 4902  df-iun 4947  df-disj 5065  df-br 5098  df-opab 5160  df-mpt 5179  df-tr 5205  df-id 5518  df-eprel 5523  df-po 5531  df-so 5532  df-fr 5576  df-se 5577  df-we 5578  df-xp 5629  df-rel 5630  df-cnv 5631  df-co 5632  df-dm 5633  df-rn 5634  df-res 5635  df-ima 5636  df-pred 6258  df-ord 6319  df-on 6320  df-lim 6321  df-suc 6322  df-iota 6447  df-fun 6493  df-fn 6494  df-f 6495  df-f1 6496  df-fo 6497  df-f1o 6498  df-fv 6499  df-isom 6500  df-riota 7315  df-ov 7361  df-oprab 7362  df-mpo 7363  df-of 7622  df-om 7809  df-1st 7933  df-2nd 7934  df-frecs 8223  df-wrecs 8254  df-recs 8303  df-rdg 8341  df-1o 8397  df-2o 8398  df-er 8635  df-map 8767  df-en 8886  df-dom 8887  df-sdom 8888  df-fin 8889  df-fi 9316  df-sup 9347  df-inf 9348  df-oi 9417  df-dju 9815  df-card 9853  df-pnf 11170  df-mnf 11171  df-xr 11172  df-ltxr 11173  df-le 11174  df-sub 11368  df-neg 11369  df-div 11797  df-nn 12148  df-2 12210  df-3 12211  df-n0 12404  df-z 12491  df-uz 12754  df-q 12864  df-rp 12908  df-xneg 13028  df-xadd 13029  df-xmul 13030  df-ioo 13267  df-ico 13269  df-icc 13270  df-fz 13426  df-fzo 13573  df-fl 13714  df-seq 13927  df-exp 13987  df-hash 14256  df-cj 15024  df-re 15025  df-im 15026  df-sqrt 15160  df-abs 15161  df-clim 15413  df-sum 15612  df-rest 17344  df-topgen 17365  df-psmet 21303  df-xmet 21304  df-met 21305  df-bl 21306  df-mopn 21307  df-top 22840  df-topon 22857  df-bases 22892  df-cmp 23333  df-ovol 25423  df-vol 25424

This theorem is referenced by: (None)