Theorem voliunnfl 37131

Description: voliun 25476 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 4914	. . . . . . . . 9 ⊢ (𝐴 = ∅ → ∪ 𝐴 = ∪ ∅)
2		uni0 4933	. . . . . . . . 9 ⊢ ∪ ∅ = ∅
3	1, 2	eqtrdi 2784	. . . . . . . 8 ⊢ (𝐴 = ∅ → ∪ 𝐴 = ∅)
4	3	fveq2d 6895	. . . . . . 7 ⊢ (𝐴 = ∅ → (vol‘∪ 𝐴) = (vol‘∅))
5		0mbl 25461	. . . . . . . . 9 ⊢ ∅ ∈ dom vol
6		mblvol 25452	. . . . . . . . 9 ⊢ (∅ ∈ dom vol → (vol‘∅) = (vol*‘∅))
7	5, 6	ax-mp 5	. . . . . . . 8 ⊢ (vol‘∅) = (vol*‘∅)
8		ovol0 25415	. . . . . . . 8 ⊢ (vol*‘∅) = 0
9	7, 8	eqtri 2756	. . . . . . 7 ⊢ (vol‘∅) = 0
10	4, 9	eqtr2di 2785	. . . . . 6 ⊢ (𝐴 = ∅ → 0 = (vol‘∪ 𝐴))
11	10	a1d 25	. . . . 5 ⊢ (𝐴 = ∅ → ((𝐴 ≼ ℕ ∧ (∀𝑥 ∈ 𝐴 𝑥 ≼ ℕ ∧ ∪ 𝐴 ⊆ ℝ)) → 0 = (vol‘∪ 𝐴)))
12		reldom 8963	. . . . . . . . . . 11 ⊢ Rel ≼
13	12	brrelex1i 5728	. . . . . . . . . 10 ⊢ (𝐴 ≼ ℕ → 𝐴 ∈ V)
14		0sdomg 9122	. . . . . . . . . 10 ⊢ (𝐴 ∈ V → (∅ ≺ 𝐴 ↔ 𝐴 ≠ ∅))
15	13, 14	syl 17	. . . . . . . . 9 ⊢ (𝐴 ≼ ℕ → (∅ ≺ 𝐴 ↔ 𝐴 ≠ ∅))
16	15	biimparc 479	. . . . . . . 8 ⊢ ((𝐴 ≠ ∅ ∧ 𝐴 ≼ ℕ) → ∅ ≺ 𝐴)
17		fodomr 9146	. . . . . . . 8 ⊢ ((∅ ≺ 𝐴 ∧ 𝐴 ≼ ℕ) → ∃𝑔 𝑔:ℕ–onto→𝐴)
18	16, 17	sylancom 587	. . . . . . 7 ⊢ ((𝐴 ≠ ∅ ∧ 𝐴 ≼ ℕ) → ∃𝑔 𝑔:ℕ–onto→𝐴)
19		unissb 4937	. . . . . . . . . . . . 13 ⊢ (∪ 𝐴 ⊆ ℝ ↔ ∀𝑥 ∈ 𝐴 𝑥 ⊆ ℝ)
20	19	anbi1i 623	. . . . . . . . . . . 12 ⊢ ((∪ 𝐴 ⊆ ℝ ∧ ∀𝑥 ∈ 𝐴 𝑥 ≼ ℕ) ↔ (∀𝑥 ∈ 𝐴 𝑥 ⊆ ℝ ∧ ∀𝑥 ∈ 𝐴 𝑥 ≼ ℕ))
21		r19.26 3107	. . . . . . . . . . . 12 ⊢ (∀𝑥 ∈ 𝐴 (𝑥 ⊆ ℝ ∧ 𝑥 ≼ ℕ) ↔ (∀𝑥 ∈ 𝐴 𝑥 ⊆ ℝ ∧ ∀𝑥 ∈ 𝐴 𝑥 ≼ ℕ))
22	20, 21	bitr4i 278	. . . . . . . . . . 11 ⊢ ((∪ 𝐴 ⊆ ℝ ∧ ∀𝑥 ∈ 𝐴 𝑥 ≼ ℕ) ↔ ∀𝑥 ∈ 𝐴 (𝑥 ⊆ ℝ ∧ 𝑥 ≼ ℕ))
23		ovolctb2 25414	. . . . . . . . . . . . . 14 ⊢ ((𝑥 ⊆ ℝ ∧ 𝑥 ≼ ℕ) → (vol*‘𝑥) = 0)
24	23	ex 412	. . . . . . . . . . . . 13 ⊢ (𝑥 ⊆ ℝ → (𝑥 ≼ ℕ → (vol*‘𝑥) = 0))
25	24	imdistani 568	. . . . . . . . . . . 12 ⊢ ((𝑥 ⊆ ℝ ∧ 𝑥 ≼ ℕ) → (𝑥 ⊆ ℝ ∧ (vol*‘𝑥) = 0))
26	25	ralimi 3079	. . . . . . . . . . 11 ⊢ (∀𝑥 ∈ 𝐴 (𝑥 ⊆ ℝ ∧ 𝑥 ≼ ℕ) → ∀𝑥 ∈ 𝐴 (𝑥 ⊆ ℝ ∧ (vol*‘𝑥) = 0))
27	22, 26	sylbi 216	. . . . . . . . . 10 ⊢ ((∪ 𝐴 ⊆ ℝ ∧ ∀𝑥 ∈ 𝐴 𝑥 ≼ ℕ) → ∀𝑥 ∈ 𝐴 (𝑥 ⊆ ℝ ∧ (vol*‘𝑥) = 0))
28	27	ancoms 458	. . . . . . . . 9 ⊢ ((∀𝑥 ∈ 𝐴 𝑥 ≼ ℕ ∧ ∪ 𝐴 ⊆ ℝ) → ∀𝑥 ∈ 𝐴 (𝑥 ⊆ ℝ ∧ (vol*‘𝑥) = 0))
29		foima 6810	. . . . . . . . . . . 12 ⊢ (𝑔:ℕ–onto→𝐴 → (𝑔 “ ℕ) = 𝐴)
30	29	raleqdv 3321	. . . . . . . . . . 11 ⊢ (𝑔:ℕ–onto→𝐴 → (∀𝑥 ∈ (𝑔 “ ℕ)(𝑥 ⊆ ℝ ∧ (vol*‘𝑥) = 0) ↔ ∀𝑥 ∈ 𝐴 (𝑥 ⊆ ℝ ∧ (vol*‘𝑥) = 0)))
31		fofn 6807	. . . . . . . . . . . 12 ⊢ (𝑔:ℕ–onto→𝐴 → 𝑔 Fn ℕ)
32		ssid 4000	. . . . . . . . . . . 12 ⊢ ℕ ⊆ ℕ
33		sseq1 4003	. . . . . . . . . . . . . 14 ⊢ (𝑥 = (𝑔‘𝑚) → (𝑥 ⊆ ℝ ↔ (𝑔‘𝑚) ⊆ ℝ))
34		fveqeq2 6900	. . . . . . . . . . . . . 14 ⊢ (𝑥 = (𝑔‘𝑚) → ((vol*‘𝑥) = 0 ↔ (vol*‘(𝑔‘𝑚)) = 0))
35	33, 34	anbi12d 631	. . . . . . . . . . . . 13 ⊢ (𝑥 = (𝑔‘𝑚) → ((𝑥 ⊆ ℝ ∧ (vol*‘𝑥) = 0) ↔ ((𝑔‘𝑚) ⊆ ℝ ∧ (vol*‘(𝑔‘𝑚)) = 0)))
36	35	ralima 7244	. . . . . . . . . . . 12 ⊢ ((𝑔 Fn ℕ ∧ ℕ ⊆ ℕ) → (∀𝑥 ∈ (𝑔 “ ℕ)(𝑥 ⊆ ℝ ∧ (vol*‘𝑥) = 0) ↔ ∀𝑚 ∈ ℕ ((𝑔‘𝑚) ⊆ ℝ ∧ (vol*‘(𝑔‘𝑚)) = 0)))
37	31, 32, 36	sylancl 585	. . . . . . . . . . 11 ⊢ (𝑔:ℕ–onto→𝐴 → (∀𝑥 ∈ (𝑔 “ ℕ)(𝑥 ⊆ ℝ ∧ (vol*‘𝑥) = 0) ↔ ∀𝑚 ∈ ℕ ((𝑔‘𝑚) ⊆ ℝ ∧ (vol*‘(𝑔‘𝑚)) = 0)))
38	30, 37	bitr3d 281	. . . . . . . . . 10 ⊢ (𝑔:ℕ–onto→𝐴 → (∀𝑥 ∈ 𝐴 (𝑥 ⊆ ℝ ∧ (vol*‘𝑥) = 0) ↔ ∀𝑚 ∈ ℕ ((𝑔‘𝑚) ⊆ ℝ ∧ (vol*‘(𝑔‘𝑚)) = 0)))
39		difss 4127	. . . . . . . . . . . . . . . . . 18 ⊢ ((𝑔‘𝑚) ∖ ∪ 𝑙 ∈ (1..^𝑚)(𝑔‘𝑙)) ⊆ (𝑔‘𝑚)
40		ovolssnul 25409	. . . . . . . . . . . . . . . . . 18 ⊢ ((((𝑔‘𝑚) ∖ ∪ 𝑙 ∈ (1..^𝑚)(𝑔‘𝑙)) ⊆ (𝑔‘𝑚) ∧ (𝑔‘𝑚) ⊆ ℝ ∧ (vol*‘(𝑔‘𝑚)) = 0) → (vol*‘((𝑔‘𝑚) ∖ ∪ 𝑙 ∈ (1..^𝑚)(𝑔‘𝑙))) = 0)
41	39, 40	mp3an1 1445	. . . . . . . . . . . . . . . . 17 ⊢ (((𝑔‘𝑚) ⊆ ℝ ∧ (vol*‘(𝑔‘𝑚)) = 0) → (vol*‘((𝑔‘𝑚) ∖ ∪ 𝑙 ∈ (1..^𝑚)(𝑔‘𝑙))) = 0)
42		ssdifss 4131	. . . . . . . . . . . . . . . . . 18 ⊢ ((𝑔‘𝑚) ⊆ ℝ → ((𝑔‘𝑚) ∖ ∪ 𝑙 ∈ (1..^𝑚)(𝑔‘𝑙)) ⊆ ℝ)
43		nulmbl 25457	. . . . . . . . . . . . . . . . . . 19 ⊢ ((((𝑔‘𝑚) ∖ ∪ 𝑙 ∈ (1..^𝑚)(𝑔‘𝑙)) ⊆ ℝ ∧ (vol*‘((𝑔‘𝑚) ∖ ∪ 𝑙 ∈ (1..^𝑚)(𝑔‘𝑙))) = 0) → ((𝑔‘𝑚) ∖ ∪ 𝑙 ∈ (1..^𝑚)(𝑔‘𝑙)) ∈ dom vol)
44		mblvol 25452	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ (((𝑔‘𝑚) ∖ ∪ 𝑙 ∈ (1..^𝑚)(𝑔‘𝑙)) ∈ dom vol → (vol‘((𝑔‘𝑚) ∖ ∪ 𝑙 ∈ (1..^𝑚)(𝑔‘𝑙))) = (vol*‘((𝑔‘𝑚) ∖ ∪ 𝑙 ∈ (1..^𝑚)(𝑔‘𝑙))))
45	44	eqeq1d 2730	. . . . . . . . . . . . . . . . . . . . . . . 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 11240	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ 0 ∈ ℝ
48	46, 47	eqeltrdi 2837	. . . . . . . . . . . . . . . . . . . . . 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 579	. . . . . . . . . . . . . . . . 17 ⊢ (((𝑔‘𝑚) ⊆ ℝ ∧ (vol*‘((𝑔‘𝑚) ∖ ∪ 𝑙 ∈ (1..^𝑚)(𝑔‘𝑙))) = 0) → (((𝑔‘𝑚) ∖ ∪ 𝑙 ∈ (1..^𝑚)(𝑔‘𝑙)) ∈ dom vol ∧ (vol‘((𝑔‘𝑚) ∖ ∪ 𝑙 ∈ (1..^𝑚)(𝑔‘𝑙))) ∈ ℝ))
54	41, 53	syldan 590	. . . . . . . . . . . . . . . 16 ⊢ (((𝑔‘𝑚) ⊆ ℝ ∧ (vol*‘(𝑔‘𝑚)) = 0) → (((𝑔‘𝑚) ∖ ∪ 𝑙 ∈ (1..^𝑚)(𝑔‘𝑙)) ∈ dom vol ∧ (vol‘((𝑔‘𝑚) ∖ ∪ 𝑙 ∈ (1..^𝑚)(𝑔‘𝑙))) ∈ ℝ))
55	54	ralimi 3079	. . . . . . . . . . . . . . 15 ⊢ (∀𝑚 ∈ ℕ ((𝑔‘𝑚) ⊆ ℝ ∧ (vol*‘(𝑔‘𝑚)) = 0) → ∀𝑚 ∈ ℕ (((𝑔‘𝑚) ∖ ∪ 𝑙 ∈ (1..^𝑚)(𝑔‘𝑙)) ∈ dom vol ∧ (vol‘((𝑔‘𝑚) ∖ ∪ 𝑙 ∈ (1..^𝑚)(𝑔‘𝑙))) ∈ ℝ))
56		fveq2 6891	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (𝑚 = 𝑛 → (𝑔‘𝑚) = (𝑔‘𝑛))
57		oveq2 7422	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (𝑚 = 𝑛 → (1..^𝑚) = (1..^𝑛))
58	57	iuneq1d 5018	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (𝑚 = 𝑛 → ∪ 𝑙 ∈ (1..^𝑚)(𝑔‘𝑙) = ∪ 𝑙 ∈ (1..^𝑛)(𝑔‘𝑙))
59	56, 58	difeq12d 4119	. . . . . . . . . . . . . . . . . . . 20 ⊢ (𝑚 = 𝑛 → ((𝑔‘𝑚) ∖ ∪ 𝑙 ∈ (1..^𝑚)(𝑔‘𝑙)) = ((𝑔‘𝑛) ∖ ∪ 𝑙 ∈ (1..^𝑛)(𝑔‘𝑙)))
60		eqid 2728	. . . . . . . . . . . . . . . . . . . 20 ⊢ (𝑚 ∈ ℕ ↦ ((𝑔‘𝑚) ∖ ∪ 𝑙 ∈ (1..^𝑚)(𝑔‘𝑙))) = (𝑚 ∈ ℕ ↦ ((𝑔‘𝑚) ∖ ∪ 𝑙 ∈ (1..^𝑚)(𝑔‘𝑙)))
61		fvex 6904	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (𝑔‘𝑛) ∈ V
62		difexg 5323	. . . . . . . . . . . . . . . . . . . . 21 ⊢ ((𝑔‘𝑛) ∈ V → ((𝑔‘𝑛) ∖ ∪ 𝑙 ∈ (1..^𝑛)(𝑔‘𝑙)) ∈ V)
63	61, 62	ax-mp 5	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((𝑔‘𝑛) ∖ ∪ 𝑙 ∈ (1..^𝑛)(𝑔‘𝑙)) ∈ V
64	59, 60, 63	fvmpt 6999	. . . . . . . . . . . . . . . . . . 19 ⊢ (𝑛 ∈ ℕ → ((𝑚 ∈ ℕ ↦ ((𝑔‘𝑚) ∖ ∪ 𝑙 ∈ (1..^𝑚)(𝑔‘𝑙)))‘𝑛) = ((𝑔‘𝑛) ∖ ∪ 𝑙 ∈ (1..^𝑛)(𝑔‘𝑙)))
65	64	eleq1d 2814	. . . . . . . . . . . . . . . . . 18 ⊢ (𝑛 ∈ ℕ → (((𝑚 ∈ ℕ ↦ ((𝑔‘𝑚) ∖ ∪ 𝑙 ∈ (1..^𝑚)(𝑔‘𝑙)))‘𝑛) ∈ dom vol ↔ ((𝑔‘𝑛) ∖ ∪ 𝑙 ∈ (1..^𝑛)(𝑔‘𝑙)) ∈ dom vol))
66	64	fveq2d 6895	. . . . . . . . . . . . . . . . . . 19 ⊢ (𝑛 ∈ ℕ → (vol‘((𝑚 ∈ ℕ ↦ ((𝑔‘𝑚) ∖ ∪ 𝑙 ∈ (1..^𝑚)(𝑔‘𝑙)))‘𝑛)) = (vol‘((𝑔‘𝑛) ∖ ∪ 𝑙 ∈ (1..^𝑛)(𝑔‘𝑙))))
67	66	eleq1d 2814	. . . . . . . . . . . . . . . . . 18 ⊢ (𝑛 ∈ ℕ → ((vol‘((𝑚 ∈ ℕ ↦ ((𝑔‘𝑚) ∖ ∪ 𝑙 ∈ (1..^𝑚)(𝑔‘𝑙)))‘𝑛)) ∈ ℝ ↔ (vol‘((𝑔‘𝑛) ∖ ∪ 𝑙 ∈ (1..^𝑛)(𝑔‘𝑙))) ∈ ℝ))
68	65, 67	anbi12d 631	. . . . . . . . . . . . . . . . 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 6891	. . . . . . . . . . . . . . . . . . . 20 ⊢ (𝑛 = 𝑚 → (𝑔‘𝑛) = (𝑔‘𝑚))
71		oveq2 7422	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (𝑛 = 𝑚 → (1..^𝑛) = (1..^𝑚))
72	71	iuneq1d 5018	. . . . . . . . . . . . . . . . . . . 20 ⊢ (𝑛 = 𝑚 → ∪ 𝑙 ∈ (1..^𝑛)(𝑔‘𝑙) = ∪ 𝑙 ∈ (1..^𝑚)(𝑔‘𝑙))
73	70, 72	difeq12d 4119	. . . . . . . . . . . . . . . . . . 19 ⊢ (𝑛 = 𝑚 → ((𝑔‘𝑛) ∖ ∪ 𝑙 ∈ (1..^𝑛)(𝑔‘𝑙)) = ((𝑔‘𝑚) ∖ ∪ 𝑙 ∈ (1..^𝑚)(𝑔‘𝑙)))
74	73	eleq1d 2814	. . . . . . . . . . . . . . . . . 18 ⊢ (𝑛 = 𝑚 → (((𝑔‘𝑛) ∖ ∪ 𝑙 ∈ (1..^𝑛)(𝑔‘𝑙)) ∈ dom vol ↔ ((𝑔‘𝑚) ∖ ∪ 𝑙 ∈ (1..^𝑚)(𝑔‘𝑙)) ∈ dom vol))
75	73	fveq2d 6895	. . . . . . . . . . . . . . . . . . 19 ⊢ (𝑛 = 𝑚 → (vol‘((𝑔‘𝑛) ∖ ∪ 𝑙 ∈ (1..^𝑛)(𝑔‘𝑙))) = (vol‘((𝑔‘𝑚) ∖ ∪ 𝑙 ∈ (1..^𝑚)(𝑔‘𝑙))))
76	75	eleq1d 2814	. . . . . . . . . . . . . . . . . 18 ⊢ (𝑛 = 𝑚 → ((vol‘((𝑔‘𝑛) ∖ ∪ 𝑙 ∈ (1..^𝑛)(𝑔‘𝑙))) ∈ ℝ ↔ (vol‘((𝑔‘𝑚) ∖ ∪ 𝑙 ∈ (1..^𝑚)(𝑔‘𝑙))) ∈ ℝ))
77	74, 76	anbi12d 631	. . . . . . . . . . . . . . . . 17 ⊢ (𝑛 = 𝑚 → ((((𝑔‘𝑛) ∖ ∪ 𝑙 ∈ (1..^𝑛)(𝑔‘𝑙)) ∈ dom vol ∧ (vol‘((𝑔‘𝑛) ∖ ∪ 𝑙 ∈ (1..^𝑛)(𝑔‘𝑙))) ∈ ℝ) ↔ (((𝑔‘𝑚) ∖ ∪ 𝑙 ∈ (1..^𝑚)(𝑔‘𝑙)) ∈ dom vol ∧ (vol‘((𝑔‘𝑚) ∖ ∪ 𝑙 ∈ (1..^𝑚)(𝑔‘𝑙))) ∈ ℝ)))
78	77	cbvralvw 3230	. . . . . . . . . . . . . . . 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 233	. . . . . . . . . . . . . 14 ⊢ (∀𝑚 ∈ ℕ ((𝑔‘𝑚) ⊆ ℝ ∧ (vol*‘(𝑔‘𝑚)) = 0) → ∀𝑛 ∈ ℕ (((𝑚 ∈ ℕ ↦ ((𝑔‘𝑚) ∖ ∪ 𝑙 ∈ (1..^𝑚)(𝑔‘𝑙)))‘𝑛) ∈ dom vol ∧ (vol‘((𝑚 ∈ ℕ ↦ ((𝑔‘𝑚) ∖ ∪ 𝑙 ∈ (1..^𝑚)(𝑔‘𝑙)))‘𝑛)) ∈ ℝ))
81		fveq2 6891	. . . . . . . . . . . . . . . 16 ⊢ (𝑛 = 𝑙 → (𝑔‘𝑛) = (𝑔‘𝑙))
82	81	iundisj2 25471	. . . . . . . . . . . . . . 15 ⊢ Disj 𝑛 ∈ ℕ ((𝑔‘𝑛) ∖ ∪ 𝑙 ∈ (1..^𝑛)(𝑔‘𝑙))
83		disjeq2 5111	. . . . . . . . . . . . . . . 16 ⊢ (∀𝑛 ∈ ℕ ((𝑚 ∈ ℕ ↦ ((𝑔‘𝑚) ∖ ∪ 𝑙 ∈ (1..^𝑚)(𝑔‘𝑙)))‘𝑛) = ((𝑔‘𝑛) ∖ ∪ 𝑙 ∈ (1..^𝑛)(𝑔‘𝑙)) → (Disj 𝑛 ∈ ℕ ((𝑚 ∈ ℕ ↦ ((𝑔‘𝑚) ∖ ∪ 𝑙 ∈ (1..^𝑚)(𝑔‘𝑙)))‘𝑛) ↔ Disj 𝑛 ∈ ℕ ((𝑔‘𝑛) ∖ ∪ 𝑙 ∈ (1..^𝑛)(𝑔‘𝑙))))
84	83, 64	mprg 3063	. . . . . . . . . . . . . . 15 ⊢ (Disj 𝑛 ∈ ℕ ((𝑚 ∈ ℕ ↦ ((𝑔‘𝑚) ∖ ∪ 𝑙 ∈ (1..^𝑚)(𝑔‘𝑙)))‘𝑛) ↔ Disj 𝑛 ∈ ℕ ((𝑔‘𝑛) ∖ ∪ 𝑙 ∈ (1..^𝑛)(𝑔‘𝑙)))
85	82, 84	mpbir 230	. . . . . . . . . . . . . 14 ⊢ Disj 𝑛 ∈ ℕ ((𝑚 ∈ ℕ ↦ ((𝑔‘𝑚) ∖ ∪ 𝑙 ∈ (1..^𝑚)(𝑔‘𝑙)))‘𝑛)
86		nnex 12242	. . . . . . . . . . . . . . . . 17 ⊢ ℕ ∈ V
87	86	mptex 7229	. . . . . . . . . . . . . . . 16 ⊢ (𝑚 ∈ ℕ ↦ ((𝑔‘𝑚) ∖ ∪ 𝑙 ∈ (1..^𝑚)(𝑔‘𝑙))) ∈ V
88		fveq1 6890	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (𝑓 = (𝑚 ∈ ℕ ↦ ((𝑔‘𝑚) ∖ ∪ 𝑙 ∈ (1..^𝑚)(𝑔‘𝑙))) → (𝑓‘𝑛) = ((𝑚 ∈ ℕ ↦ ((𝑔‘𝑚) ∖ ∪ 𝑙 ∈ (1..^𝑚)(𝑔‘𝑙)))‘𝑛))
89	88	eleq1d 2814	. . . . . . . . . . . . . . . . . . . 20 ⊢ (𝑓 = (𝑚 ∈ ℕ ↦ ((𝑔‘𝑚) ∖ ∪ 𝑙 ∈ (1..^𝑚)(𝑔‘𝑙))) → ((𝑓‘𝑛) ∈ dom vol ↔ ((𝑚 ∈ ℕ ↦ ((𝑔‘𝑚) ∖ ∪ 𝑙 ∈ (1..^𝑚)(𝑔‘𝑙)))‘𝑛) ∈ dom vol))
90	88	fveq2d 6895	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (𝑓 = (𝑚 ∈ ℕ ↦ ((𝑔‘𝑚) ∖ ∪ 𝑙 ∈ (1..^𝑚)(𝑔‘𝑙))) → (vol‘(𝑓‘𝑛)) = (vol‘((𝑚 ∈ ℕ ↦ ((𝑔‘𝑚) ∖ ∪ 𝑙 ∈ (1..^𝑚)(𝑔‘𝑙)))‘𝑛)))
91	90	eleq1d 2814	. . . . . . . . . . . . . . . . . . . 20 ⊢ (𝑓 = (𝑚 ∈ ℕ ↦ ((𝑔‘𝑚) ∖ ∪ 𝑙 ∈ (1..^𝑚)(𝑔‘𝑙))) → ((vol‘(𝑓‘𝑛)) ∈ ℝ ↔ (vol‘((𝑚 ∈ ℕ ↦ ((𝑔‘𝑚) ∖ ∪ 𝑙 ∈ (1..^𝑚)(𝑔‘𝑙)))‘𝑛)) ∈ ℝ))
92	89, 91	anbi12d 631	. . . . . . . . . . . . . . . . . . 19 ⊢ (𝑓 = (𝑚 ∈ ℕ ↦ ((𝑔‘𝑚) ∖ ∪ 𝑙 ∈ (1..^𝑚)(𝑔‘𝑙))) → (((𝑓‘𝑛) ∈ dom vol ∧ (vol‘(𝑓‘𝑛)) ∈ ℝ) ↔ (((𝑚 ∈ ℕ ↦ ((𝑔‘𝑚) ∖ ∪ 𝑙 ∈ (1..^𝑚)(𝑔‘𝑙)))‘𝑛) ∈ dom vol ∧ (vol‘((𝑚 ∈ ℕ ↦ ((𝑔‘𝑚) ∖ ∪ 𝑙 ∈ (1..^𝑚)(𝑔‘𝑙)))‘𝑛)) ∈ ℝ)))
93	92	ralbidv 3173	. . . . . . . . . . . . . . . . . 18 ⊢ (𝑓 = (𝑚 ∈ ℕ ↦ ((𝑔‘𝑚) ∖ ∪ 𝑙 ∈ (1..^𝑚)(𝑔‘𝑙))) → (∀𝑛 ∈ ℕ ((𝑓‘𝑛) ∈ dom vol ∧ (vol‘(𝑓‘𝑛)) ∈ ℝ) ↔ ∀𝑛 ∈ ℕ (((𝑚 ∈ ℕ ↦ ((𝑔‘𝑚) ∖ ∪ 𝑙 ∈ (1..^𝑚)(𝑔‘𝑙)))‘𝑛) ∈ dom vol ∧ (vol‘((𝑚 ∈ ℕ ↦ ((𝑔‘𝑚) ∖ ∪ 𝑙 ∈ (1..^𝑚)(𝑔‘𝑙)))‘𝑛)) ∈ ℝ)))
94	88	adantr 480	. . . . . . . . . . . . . . . . . . 19 ⊢ ((𝑓 = (𝑚 ∈ ℕ ↦ ((𝑔‘𝑚) ∖ ∪ 𝑙 ∈ (1..^𝑚)(𝑔‘𝑙))) ∧ 𝑛 ∈ ℕ) → (𝑓‘𝑛) = ((𝑚 ∈ ℕ ↦ ((𝑔‘𝑚) ∖ ∪ 𝑙 ∈ (1..^𝑚)(𝑔‘𝑙)))‘𝑛))
95	94	disjeq2dv 5112	. . . . . . . . . . . . . . . . . 18 ⊢ (𝑓 = (𝑚 ∈ ℕ ↦ ((𝑔‘𝑚) ∖ ∪ 𝑙 ∈ (1..^𝑚)(𝑔‘𝑙))) → (Disj 𝑛 ∈ ℕ (𝑓‘𝑛) ↔ Disj 𝑛 ∈ ℕ ((𝑚 ∈ ℕ ↦ ((𝑔‘𝑚) ∖ ∪ 𝑙 ∈ (1..^𝑚)(𝑔‘𝑙)))‘𝑛)))
96	93, 95	anbi12d 631	. . . . . . . . . . . . . . . . 17 ⊢ (𝑓 = (𝑚 ∈ ℕ ↦ ((𝑔‘𝑚) ∖ ∪ 𝑙 ∈ (1..^𝑚)(𝑔‘𝑙))) → ((∀𝑛 ∈ ℕ ((𝑓‘𝑛) ∈ dom vol ∧ (vol‘(𝑓‘𝑛)) ∈ ℝ) ∧ Disj 𝑛 ∈ ℕ (𝑓‘𝑛)) ↔ (∀𝑛 ∈ ℕ (((𝑚 ∈ ℕ ↦ ((𝑔‘𝑚) ∖ ∪ 𝑙 ∈ (1..^𝑚)(𝑔‘𝑙)))‘𝑛) ∈ dom vol ∧ (vol‘((𝑚 ∈ ℕ ↦ ((𝑔‘𝑚) ∖ ∪ 𝑙 ∈ (1..^𝑚)(𝑔‘𝑙)))‘𝑛)) ∈ ℝ) ∧ Disj 𝑛 ∈ ℕ ((𝑚 ∈ ℕ ↦ ((𝑔‘𝑚) ∖ ∪ 𝑙 ∈ (1..^𝑚)(𝑔‘𝑙)))‘𝑛))))
97	88	iuneq2d 5020	. . . . . . . . . . . . . . . . . . 19 ⊢ (𝑓 = (𝑚 ∈ ℕ ↦ ((𝑔‘𝑚) ∖ ∪ 𝑙 ∈ (1..^𝑚)(𝑔‘𝑙))) → ∪ 𝑛 ∈ ℕ (𝑓‘𝑛) = ∪ 𝑛 ∈ ℕ ((𝑚 ∈ ℕ ↦ ((𝑔‘𝑚) ∖ ∪ 𝑙 ∈ (1..^𝑚)(𝑔‘𝑙)))‘𝑛))
98	97	fveq2d 6895	. . . . . . . . . . . . . . . . . 18 ⊢ (𝑓 = (𝑚 ∈ ℕ ↦ ((𝑔‘𝑚) ∖ ∪ 𝑙 ∈ (1..^𝑚)(𝑔‘𝑙))) → (vol‘∪ 𝑛 ∈ ℕ (𝑓‘𝑛)) = (vol‘∪ 𝑛 ∈ ℕ ((𝑚 ∈ ℕ ↦ ((𝑔‘𝑚) ∖ ∪ 𝑙 ∈ (1..^𝑚)(𝑔‘𝑙)))‘𝑛)))
99		voliunnfl.1	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ 𝑆 = seq1( + , 𝐺)
100		voliunnfl.2	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ 𝐺 = (𝑛 ∈ ℕ ↦ (vol‘(𝑓‘𝑛)))
101		seqeq3 13997	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ (𝐺 = (𝑛 ∈ ℕ ↦ (vol‘(𝑓‘𝑛))) → seq1( + , 𝐺) = seq1( + , (𝑛 ∈ ℕ ↦ (vol‘(𝑓‘𝑛)))))
102	100, 101	ax-mp 5	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ seq1( + , 𝐺) = seq1( + , (𝑛 ∈ ℕ ↦ (vol‘(𝑓‘𝑛))))
103	99, 102	eqtri 2756	. . . . . . . . . . . . . . . . . . . . 21 ⊢ 𝑆 = seq1( + , (𝑛 ∈ ℕ ↦ (vol‘(𝑓‘𝑛))))
104	103	rneqi 5933	. . . . . . . . . . . . . . . . . . . 20 ⊢ ran 𝑆 = ran seq1( + , (𝑛 ∈ ℕ ↦ (vol‘(𝑓‘𝑛))))
105	104	supeq1i 9464	. . . . . . . . . . . . . . . . . . 19 ⊢ sup(ran 𝑆, ℝ*, < ) = sup(ran seq1( + , (𝑛 ∈ ℕ ↦ (vol‘(𝑓‘𝑛)))), ℝ*, < )
106	90	mpteq2dv 5244	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (𝑓 = (𝑚 ∈ ℕ ↦ ((𝑔‘𝑚) ∖ ∪ 𝑙 ∈ (1..^𝑚)(𝑔‘𝑙))) → (𝑛 ∈ ℕ ↦ (vol‘(𝑓‘𝑛))) = (𝑛 ∈ ℕ ↦ (vol‘((𝑚 ∈ ℕ ↦ ((𝑔‘𝑚) ∖ ∪ 𝑙 ∈ (1..^𝑚)(𝑔‘𝑙)))‘𝑛))))
107	106	seqeq3d 14000	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (𝑓 = (𝑚 ∈ ℕ ↦ ((𝑔‘𝑚) ∖ ∪ 𝑙 ∈ (1..^𝑚)(𝑔‘𝑙))) → seq1( + , (𝑛 ∈ ℕ ↦ (vol‘(𝑓‘𝑛)))) = seq1( + , (𝑛 ∈ ℕ ↦ (vol‘((𝑚 ∈ ℕ ↦ ((𝑔‘𝑚) ∖ ∪ 𝑙 ∈ (1..^𝑚)(𝑔‘𝑙)))‘𝑛)))))
108	107	rneqd 5934	. . . . . . . . . . . . . . . . . . . 20 ⊢ (𝑓 = (𝑚 ∈ ℕ ↦ ((𝑔‘𝑚) ∖ ∪ 𝑙 ∈ (1..^𝑚)(𝑔‘𝑙))) → ran seq1( + , (𝑛 ∈ ℕ ↦ (vol‘(𝑓‘𝑛)))) = ran seq1( + , (𝑛 ∈ ℕ ↦ (vol‘((𝑚 ∈ ℕ ↦ ((𝑔‘𝑚) ∖ ∪ 𝑙 ∈ (1..^𝑚)(𝑔‘𝑙)))‘𝑛)))))
109	108	supeq1d 9463	. . . . . . . . . . . . . . . . . . 19 ⊢ (𝑓 = (𝑚 ∈ ℕ ↦ ((𝑔‘𝑚) ∖ ∪ 𝑙 ∈ (1..^𝑚)(𝑔‘𝑙))) → sup(ran seq1( + , (𝑛 ∈ ℕ ↦ (vol‘(𝑓‘𝑛)))), ℝ*, < ) = sup(ran seq1( + , (𝑛 ∈ ℕ ↦ (vol‘((𝑚 ∈ ℕ ↦ ((𝑔‘𝑚) ∖ ∪ 𝑙 ∈ (1..^𝑚)(𝑔‘𝑙)))‘𝑛)))), ℝ*, < ))
110	105, 109	eqtrid 2780	. . . . . . . . . . . . . . . . . 18 ⊢ (𝑓 = (𝑚 ∈ ℕ ↦ ((𝑔‘𝑚) ∖ ∪ 𝑙 ∈ (1..^𝑚)(𝑔‘𝑙))) → sup(ran 𝑆, ℝ*, < ) = sup(ran seq1( + , (𝑛 ∈ ℕ ↦ (vol‘((𝑚 ∈ ℕ ↦ ((𝑔‘𝑚) ∖ ∪ 𝑙 ∈ (1..^𝑚)(𝑔‘𝑙)))‘𝑛)))), ℝ*, < ))
111	98, 110	eqeq12d 2744	. . . . . . . . . . . . . . . . 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 3542	. . . . . . . . . . . . . . 15 ⊢ ((∀𝑛 ∈ ℕ (((𝑚 ∈ ℕ ↦ ((𝑔‘𝑚) ∖ ∪ 𝑙 ∈ (1..^𝑚)(𝑔‘𝑙)))‘𝑛) ∈ dom vol ∧ (vol‘((𝑚 ∈ ℕ ↦ ((𝑔‘𝑚) ∖ ∪ 𝑙 ∈ (1..^𝑚)(𝑔‘𝑙)))‘𝑛)) ∈ ℝ) ∧ Disj 𝑛 ∈ ℕ ((𝑚 ∈ ℕ ↦ ((𝑔‘𝑚) ∖ ∪ 𝑙 ∈ (1..^𝑚)(𝑔‘𝑙)))‘𝑛)) → (vol‘∪ 𝑛 ∈ ℕ ((𝑚 ∈ ℕ ↦ ((𝑔‘𝑚) ∖ ∪ 𝑙 ∈ (1..^𝑚)(𝑔‘𝑙)))‘𝑛)) = sup(ran seq1( + , (𝑛 ∈ ℕ ↦ (vol‘((𝑚 ∈ ℕ ↦ ((𝑔‘𝑚) ∖ ∪ 𝑙 ∈ (1..^𝑚)(𝑔‘𝑙)))‘𝑛)))), ℝ*, < ))
115	64	iuneq2i 5012	. . . . . . . . . . . . . . . 16 ⊢ ∪ 𝑛 ∈ ℕ ((𝑚 ∈ ℕ ↦ ((𝑔‘𝑚) ∖ ∪ 𝑙 ∈ (1..^𝑚)(𝑔‘𝑙)))‘𝑛) = ∪ 𝑛 ∈ ℕ ((𝑔‘𝑛) ∖ ∪ 𝑙 ∈ (1..^𝑛)(𝑔‘𝑙))
116	115	fveq2i 6894	. . . . . . . . . . . . . . 15 ⊢ (vol‘∪ 𝑛 ∈ ℕ ((𝑚 ∈ ℕ ↦ ((𝑔‘𝑚) ∖ ∪ 𝑙 ∈ (1..^𝑚)(𝑔‘𝑙)))‘𝑛)) = (vol‘∪ 𝑛 ∈ ℕ ((𝑔‘𝑛) ∖ ∪ 𝑙 ∈ (1..^𝑛)(𝑔‘𝑙)))
117	66	mpteq2ia 5245	. . . . . . . . . . . . . . . . . 18 ⊢ (𝑛 ∈ ℕ ↦ (vol‘((𝑚 ∈ ℕ ↦ ((𝑔‘𝑚) ∖ ∪ 𝑙 ∈ (1..^𝑚)(𝑔‘𝑙)))‘𝑛))) = (𝑛 ∈ ℕ ↦ (vol‘((𝑔‘𝑛) ∖ ∪ 𝑙 ∈ (1..^𝑛)(𝑔‘𝑙))))
118		seqeq3 13997	. . . . . . . . . . . . . . . . . 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 5933	. . . . . . . . . . . . . . . 16 ⊢ ran seq1( + , (𝑛 ∈ ℕ ↦ (vol‘((𝑚 ∈ ℕ ↦ ((𝑔‘𝑚) ∖ ∪ 𝑙 ∈ (1..^𝑚)(𝑔‘𝑙)))‘𝑛)))) = ran seq1( + , (𝑛 ∈ ℕ ↦ (vol‘((𝑔‘𝑛) ∖ ∪ 𝑙 ∈ (1..^𝑛)(𝑔‘𝑙)))))
121	120	supeq1i 9464	. . . . . . . . . . . . . . 15 ⊢ sup(ran seq1( + , (𝑛 ∈ ℕ ↦ (vol‘((𝑚 ∈ ℕ ↦ ((𝑔‘𝑚) ∖ ∪ 𝑙 ∈ (1..^𝑚)(𝑔‘𝑙)))‘𝑛)))), ℝ*, < ) = sup(ran seq1( + , (𝑛 ∈ ℕ ↦ (vol‘((𝑔‘𝑛) ∖ ∪ 𝑙 ∈ (1..^𝑛)(𝑔‘𝑙))))), ℝ*, < )
122	114, 116, 121	3eqtr3g 2791	. . . . . . . . . . . . . 14 ⊢ ((∀𝑛 ∈ ℕ (((𝑚 ∈ ℕ ↦ ((𝑔‘𝑚) ∖ ∪ 𝑙 ∈ (1..^𝑚)(𝑔‘𝑙)))‘𝑛) ∈ dom vol ∧ (vol‘((𝑚 ∈ ℕ ↦ ((𝑔‘𝑚) ∖ ∪ 𝑙 ∈ (1..^𝑚)(𝑔‘𝑙)))‘𝑛)) ∈ ℝ) ∧ Disj 𝑛 ∈ ℕ ((𝑚 ∈ ℕ ↦ ((𝑔‘𝑚) ∖ ∪ 𝑙 ∈ (1..^𝑚)(𝑔‘𝑙)))‘𝑛)) → (vol‘∪ 𝑛 ∈ ℕ ((𝑔‘𝑛) ∖ ∪ 𝑙 ∈ (1..^𝑛)(𝑔‘𝑙))) = sup(ran seq1( + , (𝑛 ∈ ℕ ↦ (vol‘((𝑔‘𝑛) ∖ ∪ 𝑙 ∈ (1..^𝑛)(𝑔‘𝑙))))), ℝ*, < ))
123	80, 85, 122	sylancl 585	. . . . . . . . . . . . 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 25470	. . . . . . . . . . . . . . . 16 ⊢ ∪ 𝑛 ∈ ℕ (𝑔‘𝑛) = ∪ 𝑛 ∈ ℕ ((𝑔‘𝑛) ∖ ∪ 𝑙 ∈ (1..^𝑛)(𝑔‘𝑙))
126		fofun 6806	. . . . . . . . . . . . . . . . 17 ⊢ (𝑔:ℕ–onto→𝐴 → Fun 𝑔)
127		funiunfv 7252	. . . . . . . . . . . . . . . . 17 ⊢ (Fun 𝑔 → ∪ 𝑛 ∈ ℕ (𝑔‘𝑛) = ∪ (𝑔 “ ℕ))
128	126, 127	syl 17	. . . . . . . . . . . . . . . 16 ⊢ (𝑔:ℕ–onto→𝐴 → ∪ 𝑛 ∈ ℕ (𝑔‘𝑛) = ∪ (𝑔 “ ℕ))
129	125, 128	eqtr3id 2782	. . . . . . . . . . . . . . 15 ⊢ (𝑔:ℕ–onto→𝐴 → ∪ 𝑛 ∈ ℕ ((𝑔‘𝑛) ∖ ∪ 𝑙 ∈ (1..^𝑛)(𝑔‘𝑙)) = ∪ (𝑔 “ ℕ))
130	29	unieqd 4916	. . . . . . . . . . . . . . 15 ⊢ (𝑔:ℕ–onto→𝐴 → ∪ (𝑔 “ ℕ) = ∪ 𝐴)
131	129, 130	eqtrd 2768	. . . . . . . . . . . . . 14 ⊢ (𝑔:ℕ–onto→𝐴 → ∪ 𝑛 ∈ ℕ ((𝑔‘𝑛) ∖ ∪ 𝑙 ∈ (1..^𝑛)(𝑔‘𝑙)) = ∪ 𝐴)
132	131	fveq2d 6895	. . . . . . . . . . . . 13 ⊢ (𝑔:ℕ–onto→𝐴 → (vol‘∪ 𝑛 ∈ ℕ ((𝑔‘𝑛) ∖ ∪ 𝑙 ∈ (1..^𝑛)(𝑔‘𝑙))) = (vol‘∪ 𝐴))
133	132	adantr 480	. . . . . . . . . . . 12 ⊢ ((𝑔:ℕ–onto→𝐴 ∧ ∀𝑚 ∈ ℕ ((𝑔‘𝑚) ⊆ ℝ ∧ (vol*‘(𝑔‘𝑚)) = 0)) → (vol‘∪ 𝑛 ∈ ℕ ((𝑔‘𝑛) ∖ ∪ 𝑙 ∈ (1..^𝑛)(𝑔‘𝑙))) = (vol‘∪ 𝐴))
134	56	sseq1d 4009	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (𝑚 = 𝑛 → ((𝑔‘𝑚) ⊆ ℝ ↔ (𝑔‘𝑛) ⊆ ℝ))
135	56	fveqeq2d 6899	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (𝑚 = 𝑛 → ((vol*‘(𝑔‘𝑚)) = 0 ↔ (vol*‘(𝑔‘𝑛)) = 0))
136	134, 135	anbi12d 631	. . . . . . . . . . . . . . . . . . . 20 ⊢ (𝑚 = 𝑛 → (((𝑔‘𝑚) ⊆ ℝ ∧ (vol*‘(𝑔‘𝑚)) = 0) ↔ ((𝑔‘𝑛) ⊆ ℝ ∧ (vol*‘(𝑔‘𝑛)) = 0)))
137	136	rspccva 3607	. . . . . . . . . . . . . . . . . . 19 ⊢ ((∀𝑚 ∈ ℕ ((𝑔‘𝑚) ⊆ ℝ ∧ (vol*‘(𝑔‘𝑚)) = 0) ∧ 𝑛 ∈ ℕ) → ((𝑔‘𝑛) ⊆ ℝ ∧ (vol*‘(𝑔‘𝑛)) = 0))
138		ssdifss 4131	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ ((𝑔‘𝑛) ⊆ ℝ → ((𝑔‘𝑛) ∖ ∪ 𝑙 ∈ (1..^𝑛)(𝑔‘𝑙)) ⊆ ℝ)
139	138	adantr 480	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (((𝑔‘𝑛) ⊆ ℝ ∧ (vol*‘(𝑔‘𝑛)) = 0) → ((𝑔‘𝑛) ∖ ∪ 𝑙 ∈ (1..^𝑛)(𝑔‘𝑙)) ⊆ ℝ)
140		difss 4127	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ ((𝑔‘𝑛) ∖ ∪ 𝑙 ∈ (1..^𝑛)(𝑔‘𝑙)) ⊆ (𝑔‘𝑛)
141		ovolssnul 25409	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ ((((𝑔‘𝑛) ∖ ∪ 𝑙 ∈ (1..^𝑛)(𝑔‘𝑙)) ⊆ (𝑔‘𝑛) ∧ (𝑔‘𝑛) ⊆ ℝ ∧ (vol*‘(𝑔‘𝑛)) = 0) → (vol*‘((𝑔‘𝑛) ∖ ∪ 𝑙 ∈ (1..^𝑛)(𝑔‘𝑙))) = 0)
142	140, 141	mp3an1 1445	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (((𝑔‘𝑛) ⊆ ℝ ∧ (vol*‘(𝑔‘𝑛)) = 0) → (vol*‘((𝑔‘𝑛) ∖ ∪ 𝑙 ∈ (1..^𝑛)(𝑔‘𝑙))) = 0)
143	139, 142	jca 511	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (((𝑔‘𝑛) ⊆ ℝ ∧ (vol*‘(𝑔‘𝑛)) = 0) → (((𝑔‘𝑛) ∖ ∪ 𝑙 ∈ (1..^𝑛)(𝑔‘𝑙)) ⊆ ℝ ∧ (vol*‘((𝑔‘𝑛) ∖ ∪ 𝑙 ∈ (1..^𝑛)(𝑔‘𝑙))) = 0))
144		nulmbl 25457	. . . . . . . . . . . . . . . . . . . . 21 ⊢ ((((𝑔‘𝑛) ∖ ∪ 𝑙 ∈ (1..^𝑛)(𝑔‘𝑙)) ⊆ ℝ ∧ (vol*‘((𝑔‘𝑛) ∖ ∪ 𝑙 ∈ (1..^𝑛)(𝑔‘𝑙))) = 0) → ((𝑔‘𝑛) ∖ ∪ 𝑙 ∈ (1..^𝑛)(𝑔‘𝑙)) ∈ dom vol)
145		mblvol 25452	. . . . . . . . . . . . . . . . . . . . 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 2768	. . . . . . . . . . . . . . . . . . 19 ⊢ (((𝑔‘𝑛) ⊆ ℝ ∧ (vol*‘(𝑔‘𝑛)) = 0) → (vol‘((𝑔‘𝑛) ∖ ∪ 𝑙 ∈ (1..^𝑛)(𝑔‘𝑙))) = 0)
148	137, 147	syl 17	. . . . . . . . . . . . . . . . . 18 ⊢ ((∀𝑚 ∈ ℕ ((𝑔‘𝑚) ⊆ ℝ ∧ (vol*‘(𝑔‘𝑚)) = 0) ∧ 𝑛 ∈ ℕ) → (vol‘((𝑔‘𝑛) ∖ ∪ 𝑙 ∈ (1..^𝑛)(𝑔‘𝑙))) = 0)
149	148	mpteq2dva 5242	. . . . . . . . . . . . . . . . 17 ⊢ (∀𝑚 ∈ ℕ ((𝑔‘𝑚) ⊆ ℝ ∧ (vol*‘(𝑔‘𝑚)) = 0) → (𝑛 ∈ ℕ ↦ (vol‘((𝑔‘𝑛) ∖ ∪ 𝑙 ∈ (1..^𝑛)(𝑔‘𝑙)))) = (𝑛 ∈ ℕ ↦ 0))
150	149	seqeq3d 14000	. . . . . . . . . . . . . . . 16 ⊢ (∀𝑚 ∈ ℕ ((𝑔‘𝑚) ⊆ ℝ ∧ (vol*‘(𝑔‘𝑚)) = 0) → seq1( + , (𝑛 ∈ ℕ ↦ (vol‘((𝑔‘𝑛) ∖ ∪ 𝑙 ∈ (1..^𝑛)(𝑔‘𝑙))))) = seq1( + , (𝑛 ∈ ℕ ↦ 0)))
151	150	rneqd 5934	. . . . . . . . . . . . . . 15 ⊢ (∀𝑚 ∈ ℕ ((𝑔‘𝑚) ⊆ ℝ ∧ (vol*‘(𝑔‘𝑚)) = 0) → ran seq1( + , (𝑛 ∈ ℕ ↦ (vol‘((𝑔‘𝑛) ∖ ∪ 𝑙 ∈ (1..^𝑛)(𝑔‘𝑙))))) = ran seq1( + , (𝑛 ∈ ℕ ↦ 0)))
152	151	supeq1d 9463	. . . . . . . . . . . . . 14 ⊢ (∀𝑚 ∈ ℕ ((𝑔‘𝑚) ⊆ ℝ ∧ (vol*‘(𝑔‘𝑚)) = 0) → sup(ran seq1( + , (𝑛 ∈ ℕ ↦ (vol‘((𝑔‘𝑛) ∖ ∪ 𝑙 ∈ (1..^𝑛)(𝑔‘𝑙))))), ℝ*, < ) = sup(ran seq1( + , (𝑛 ∈ ℕ ↦ 0)), ℝ*, < ))
153		0cn 11230	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ 0 ∈ ℂ
154		ser1const 14049	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ ((0 ∈ ℂ ∧ 𝑚 ∈ ℕ) → (seq1( + , (ℕ × {0}))‘𝑚) = (𝑚 · 0))
155	153, 154	mpan 689	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (𝑚 ∈ ℕ → (seq1( + , (ℕ × {0}))‘𝑚) = (𝑚 · 0))
156		nncn 12244	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (𝑚 ∈ ℕ → 𝑚 ∈ ℂ)
157	156	mul01d 11437	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (𝑚 ∈ ℕ → (𝑚 · 0) = 0)
158	155, 157	eqtrd 2768	. . . . . . . . . . . . . . . . . . . 20 ⊢ (𝑚 ∈ ℕ → (seq1( + , (ℕ × {0}))‘𝑚) = 0)
159	158	mpteq2ia 5245	. . . . . . . . . . . . . . . . . . 19 ⊢ (𝑚 ∈ ℕ ↦ (seq1( + , (ℕ × {0}))‘𝑚)) = (𝑚 ∈ ℕ ↦ 0)
160		fconstmpt 5734	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (ℕ × {0}) = (𝑛 ∈ ℕ ↦ 0)
161		seqeq3 13997	. . . . . . . . . . . . . . . . . . . . 21 ⊢ ((ℕ × {0}) = (𝑛 ∈ ℕ ↦ 0) → seq1( + , (ℕ × {0})) = seq1( + , (𝑛 ∈ ℕ ↦ 0)))
162	160, 161	ax-mp 5	. . . . . . . . . . . . . . . . . . . 20 ⊢ seq1( + , (ℕ × {0})) = seq1( + , (𝑛 ∈ ℕ ↦ 0))
163		1z 12616	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ 1 ∈ ℤ
164		seqfn 14004	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (1 ∈ ℤ → seq1( + , (ℕ × {0})) Fn (ℤ≥‘1))
165	163, 164	ax-mp 5	. . . . . . . . . . . . . . . . . . . . 21 ⊢ seq1( + , (ℕ × {0})) Fn (ℤ≥‘1)
166		nnuz 12889	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ ℕ = (ℤ≥‘1)
167	166	fneq2i 6646	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (seq1( + , (ℕ × {0})) Fn ℕ ↔ seq1( + , (ℕ × {0})) Fn (ℤ≥‘1))
168		dffn5 6951	. . . . . . . . . . . . . . . . . . . . . 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 229	. . . . . . . . . . . . . . . . . . . 20 ⊢ seq1( + , (ℕ × {0})) = (𝑚 ∈ ℕ ↦ (seq1( + , (ℕ × {0}))‘𝑚))
171	162, 170	eqtr3i 2758	. . . . . . . . . . . . . . . . . . 19 ⊢ seq1( + , (𝑛 ∈ ℕ ↦ 0)) = (𝑚 ∈ ℕ ↦ (seq1( + , (ℕ × {0}))‘𝑚))
172		fconstmpt 5734	. . . . . . . . . . . . . . . . . . 19 ⊢ (ℕ × {0}) = (𝑚 ∈ ℕ ↦ 0)
173	159, 171, 172	3eqtr4i 2766	. . . . . . . . . . . . . . . . . 18 ⊢ seq1( + , (𝑛 ∈ ℕ ↦ 0)) = (ℕ × {0})
174	173	rneqi 5933	. . . . . . . . . . . . . . . . 17 ⊢ ran seq1( + , (𝑛 ∈ ℕ ↦ 0)) = ran (ℕ × {0})
175		1nn 12247	. . . . . . . . . . . . . . . . . 18 ⊢ 1 ∈ ℕ
176		ne0i 4330	. . . . . . . . . . . . . . . . . 18 ⊢ (1 ∈ ℕ → ℕ ≠ ∅)
177		rnxp 6168	. . . . . . . . . . . . . . . . . 18 ⊢ (ℕ ≠ ∅ → ran (ℕ × {0}) = {0})
178	175, 176, 177	mp2b 10	. . . . . . . . . . . . . . . . 17 ⊢ ran (ℕ × {0}) = {0}
179	174, 178	eqtri 2756	. . . . . . . . . . . . . . . 16 ⊢ ran seq1( + , (𝑛 ∈ ℕ ↦ 0)) = {0}
180	179	supeq1i 9464	. . . . . . . . . . . . . . 15 ⊢ sup(ran seq1( + , (𝑛 ∈ ℕ ↦ 0)), ℝ*, < ) = sup({0}, ℝ*, < )
181		xrltso 13146	. . . . . . . . . . . . . . . 16 ⊢ < Or ℝ*
182		0xr 11285	. . . . . . . . . . . . . . . 16 ⊢ 0 ∈ ℝ*
183		supsn 9489	. . . . . . . . . . . . . . . 16 ⊢ (( < Or ℝ* ∧ 0 ∈ ℝ*) → sup({0}, ℝ*, < ) = 0)
184	181, 182, 183	mp2an 691	. . . . . . . . . . . . . . 15 ⊢ sup({0}, ℝ*, < ) = 0
185	180, 184	eqtri 2756	. . . . . . . . . . . . . 14 ⊢ sup(ran seq1( + , (𝑛 ∈ ℕ ↦ 0)), ℝ*, < ) = 0
186	152, 185	eqtrdi 2784	. . . . . . . . . . . . 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 2777	. . . . . . . . . . 11 ⊢ ((𝑔:ℕ–onto→𝐴 ∧ ∀𝑚 ∈ ℕ ((𝑔‘𝑚) ⊆ ℝ ∧ (vol*‘(𝑔‘𝑚)) = 0)) → 0 = (vol‘∪ 𝐴))
189	188	ex 412	. . . . . . . . . 10 ⊢ (𝑔:ℕ–onto→𝐴 → (∀𝑚 ∈ ℕ ((𝑔‘𝑚) ⊆ ℝ ∧ (vol*‘(𝑔‘𝑚)) = 0) → 0 = (vol‘∪ 𝐴)))
190	38, 189	sylbid 239	. . . . . . . . 9 ⊢ (𝑔:ℕ–onto→𝐴 → (∀𝑥 ∈ 𝐴 (𝑥 ⊆ ℝ ∧ (vol*‘𝑥) = 0) → 0 = (vol‘∪ 𝐴)))
191	28, 190	syl5 34	. . . . . . . 8 ⊢ (𝑔:ℕ–onto→𝐴 → ((∀𝑥 ∈ 𝐴 𝑥 ≼ ℕ ∧ ∪ 𝐴 ⊆ ℝ) → 0 = (vol‘∪ 𝐴)))
192	191	exlimiv 1926	. . . . . . 7 ⊢ (∃𝑔 𝑔:ℕ–onto→𝐴 → ((∀𝑥 ∈ 𝐴 𝑥 ≼ ℕ ∧ ∪ 𝐴 ⊆ ℝ) → 0 = (vol‘∪ 𝐴)))
193	18, 192	syl 17	. . . . . 6 ⊢ ((𝐴 ≠ ∅ ∧ 𝐴 ≼ ℕ) → ((∀𝑥 ∈ 𝐴 𝑥 ≼ ℕ ∧ ∪ 𝐴 ⊆ ℝ) → 0 = (vol‘∪ 𝐴)))
194	193	expimpd 453	. . . . 5 ⊢ (𝐴 ≠ ∅ → ((𝐴 ≼ ℕ ∧ (∀𝑥 ∈ 𝐴 𝑥 ≼ ℕ ∧ ∪ 𝐴 ⊆ ℝ)) → 0 = (vol‘∪ 𝐴)))
195	11, 194	pm2.61ine 3021	. . . 4 ⊢ ((𝐴 ≼ ℕ ∧ (∀𝑥 ∈ 𝐴 𝑥 ≼ ℕ ∧ ∪ 𝐴 ⊆ ℝ)) → 0 = (vol‘∪ 𝐴))
196		renepnf 11286	. . . . . . 7 ⊢ (0 ∈ ℝ → 0 ≠ +∞)
197	47, 196	mp1i 13	. . . . . 6 ⊢ (∪ 𝐴 = ℝ → 0 ≠ +∞)
198		fveq2 6891	. . . . . . 7 ⊢ (∪ 𝐴 = ℝ → (vol‘∪ 𝐴) = (vol‘ℝ))
199		rembl 25462	. . . . . . . . 9 ⊢ ℝ ∈ dom vol
200		mblvol 25452	. . . . . . . . 9 ⊢ (ℝ ∈ dom vol → (vol‘ℝ) = (vol*‘ℝ))
201	199, 200	ax-mp 5	. . . . . . . 8 ⊢ (vol‘ℝ) = (vol*‘ℝ)
202		ovolre 25447	. . . . . . . 8 ⊢ (vol*‘ℝ) = +∞
203	201, 202	eqtri 2756	. . . . . . 7 ⊢ (vol‘ℝ) = +∞
204	198, 203	eqtrdi 2784	. . . . . 6 ⊢ (∪ 𝐴 = ℝ → (vol‘∪ 𝐴) = +∞)
205	197, 204	neeqtrrd 3011	. . . . 5 ⊢ (∪ 𝐴 = ℝ → 0 ≠ (vol‘∪ 𝐴))
206	205	necon2i 2971	. . . 4 ⊢ (0 = (vol‘∪ 𝐴) → ∪ 𝐴 ≠ ℝ)
207	195, 206	syl 17	. . 3 ⊢ ((𝐴 ≼ ℕ ∧ (∀𝑥 ∈ 𝐴 𝑥 ≼ ℕ ∧ ∪ 𝐴 ⊆ ℝ)) → ∪ 𝐴 ≠ ℝ)
208	207	expr 456	. 2 ⊢ ((𝐴 ≼ ℕ ∧ ∀𝑥 ∈ 𝐴 𝑥 ≼ ℕ) → (∪ 𝐴 ⊆ ℝ → ∪ 𝐴 ≠ ℝ))
209		eqimss 4036	. . 3 ⊢ (∪ 𝐴 = ℝ → ∪ 𝐴 ⊆ ℝ)
210	209	necon3bi 2963	. 2 ⊢ (¬ ∪ 𝐴 ⊆ ℝ → ∪ 𝐴 ≠ ℝ)
211	208, 210	pm2.61d1 180	1 ⊢ ((𝐴 ≼ ℕ ∧ ∀𝑥 ∈ 𝐴 𝑥 ≼ ℕ) → ∪ 𝐴 ≠ ℝ)

Syntax hints:   → wi 4   ↔ wb 205   ∧ wa 395   = wceq 1534  ∃wex 1774   ∈ wcel 2099   ≠ wne 2936  ∀wral 3057  Vcvv 3470   ∖ cdif 3942   ⊆ wss 3945  ∅c0 4318  {csn 4624  ∪ cuni 4903  ∪ ciun 4991  Disj wdisj 5107   class class class wbr 5142   ↦ cmpt 5225   Or wor 5583   × cxp 5670  dom cdm 5672  ran crn 5673   “ cima 5675  Fun wfun 6536   Fn wfn 6537  –onto→wfo 6540  ‘cfv 6542  (class class class)co 7414   ≼ cdom 8955   ≺ csdm 8956  supcsup 9457  ℂcc 11130  ℝcr 11131  0cc0 11132  1c1 11133   + caddc 11135   · cmul 11137  +∞cpnf 11269  ℝ^*cxr 11271   < clt 11272  ℕcn 12236  ℤcz 12582  ℤ_≥cuz 12846  ..^cfzo 13653  seqcseq 13992  vol*covol 25384  volcvol 25385

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1790  ax-4 1804  ax-5 1906  ax-6 1964  ax-7 2004  ax-8 2101  ax-9 2109  ax-10 2130  ax-11 2147  ax-12 2167  ax-ext 2699  ax-rep 5279  ax-sep 5293  ax-nul 5300  ax-pow 5359  ax-pr 5423  ax-un 7734  ax-inf2 9658  ax-cnex 11188  ax-resscn 11189  ax-1cn 11190  ax-icn 11191  ax-addcl 11192  ax-addrcl 11193  ax-mulcl 11194  ax-mulrcl 11195  ax-mulcom 11196  ax-addass 11197  ax-mulass 11198  ax-distr 11199  ax-i2m1 11200  ax-1ne0 11201  ax-1rid 11202  ax-rnegex 11203  ax-rrecex 11204  ax-cnre 11205  ax-pre-lttri 11206  ax-pre-lttrn 11207  ax-pre-ltadd 11208  ax-pre-mulgt0 11209  ax-pre-sup 11210

This theorem depends on definitions:  df-bi 206  df-an 396  df-or 847  df-3or 1086  df-3an 1087  df-tru 1537  df-fal 1547  df-ex 1775  df-nf 1779  df-sb 2061  df-mo 2530  df-eu 2559  df-clab 2706  df-cleq 2720  df-clel 2806  df-nfc 2881  df-ne 2937  df-nel 3043  df-ral 3058  df-rex 3067  df-rmo 3372  df-reu 3373  df-rab 3429  df-v 3472  df-sbc 3776  df-csb 3891  df-dif 3948  df-un 3950  df-in 3952  df-ss 3962  df-pss 3964  df-nul 4319  df-if 4525  df-pw 4600  df-sn 4625  df-pr 4627  df-op 4631  df-uni 4904  df-int 4945  df-iun 4993  df-disj 5108  df-br 5143  df-opab 5205  df-mpt 5226  df-tr 5260  df-id 5570  df-eprel 5576  df-po 5584  df-so 5585  df-fr 5627  df-se 5628  df-we 5629  df-xp 5678  df-rel 5679  df-cnv 5680  df-co 5681  df-dm 5682  df-rn 5683  df-res 5684  df-ima 5685  df-pred 6299  df-ord 6366  df-on 6367  df-lim 6368  df-suc 6369  df-iota 6494  df-fun 6544  df-fn 6545  df-f 6546  df-f1 6547  df-fo 6548  df-f1o 6549  df-fv 6550  df-isom 6551  df-riota 7370  df-ov 7417  df-oprab 7418  df-mpo 7419  df-of 7679  df-om 7865  df-1st 7987  df-2nd 7988  df-frecs 8280  df-wrecs 8311  df-recs 8385  df-rdg 8424  df-1o 8480  df-2o 8481  df-er 8718  df-map 8840  df-en 8958  df-dom 8959  df-sdom 8960  df-fin 8961  df-fi 9428  df-sup 9459  df-inf 9460  df-oi 9527  df-dju 9918  df-card 9956  df-pnf 11274  df-mnf 11275  df-xr 11276  df-ltxr 11277  df-le 11278  df-sub 11470  df-neg 11471  df-div 11896  df-nn 12237  df-2 12299  df-3 12300  df-n0 12497  df-z 12583  df-uz 12847  df-q 12957  df-rp 13001  df-xneg 13118  df-xadd 13119  df-xmul 13120  df-ioo 13354  df-ico 13356  df-icc 13357  df-fz 13511  df-fzo 13654  df-fl 13783  df-seq 13993  df-exp 14053  df-hash 14316  df-cj 15072  df-re 15073  df-im 15074  df-sqrt 15208  df-abs 15209  df-clim 15458  df-sum 15659  df-rest 17397  df-topgen 17418  df-psmet 21264  df-xmet 21265  df-met 21266  df-bl 21267  df-mopn 21268  df-top 22789  df-topon 22806  df-bases 22842  df-cmp 23284  df-ovol 25386  df-vol 25387

This theorem is referenced by: (None)

Otomatik - 173.255.232.114 CloudFlare DNS Türk Telekom DNS Google DNS Open DNS

OSZAR »