Theorem voliunnfl 38583

Description: voliun 25875 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 4877	. . . . . . . . 9 ⊢ (𝐴 = ∅ → ∪ 𝐴 = ∪ ∅)
2		uni0 4895	. . . . . . . . 9 ⊢ ∪ ∅ = ∅
3	1, 2	eqtrdi 2811	. . . . . . . 8 ⊢ (𝐴 = ∅ → ∪ 𝐴 = ∅)
4	3	fveq2d 6889	. . . . . . 7 ⊢ (𝐴 = ∅ → (vol‘∪ 𝐴) = (vol‘∅))
5		0mbl 25860	. . . . . . . . 9 ⊢ ∅ ∈ dom vol
6		mblvol 25851	. . . . . . . . 9 ⊢ (∅ ∈ dom vol → (vol‘∅) = (vol*‘∅))
7	5, 6	ax-mp 5	. . . . . . . 8 ⊢ (vol‘∅) = (vol*‘∅)
8		ovol0 25814	. . . . . . . 8 ⊢ (vol*‘∅) = 0
9	7, 8	eqtri 2783	. . . . . . 7 ⊢ (vol‘∅) = 0
10	4, 9	eqtr2di 2812	. . . . . 6 ⊢ (𝐴 = ∅ → 0 = (vol‘∪ 𝐴))
11	10	a1d 26	. . . . 5 ⊢ (𝐴 = ∅ → ((𝐴 ≼ ℕ ∧ (∀𝑥 ∈ 𝐴 𝑥 ≼ ℕ ∧ ∪ 𝐴 ⊆ ℝ)) → 0 = (vol‘∪ 𝐴)))
12		reldom 8979	. . . . . . . . . . 11 ⊢ Rel ≼
13	12	brrelex1i 5706	. . . . . . . . . 10 ⊢ (𝐴 ≼ ℕ → 𝐴 ∈ V)
14		0sdomg 9125	. . . . . . . . . 10 ⊢ (𝐴 ∈ V → (∅ ≺ 𝐴 ↔ 𝐴 ≠ ∅))
15	13, 14	syl 18	. . . . . . . . 9 ⊢ (𝐴 ≼ ℕ → (∅ ≺ 𝐴 ↔ 𝐴 ≠ ∅))
16	15	biimparc 485	. . . . . . . 8 ⊢ ((𝐴 ≠ ∅ ∧ 𝐴 ≼ ℕ) → ∅ ≺ 𝐴)
17		fodomr 9147	. . . . . . . 8 ⊢ ((∅ ≺ 𝐴 ∧ 𝐴 ≼ ℕ) → ∃𝑔 𝑔:ℕ–onto→𝐴)
18	16, 17	sylancom 600	. . . . . . 7 ⊢ ((𝐴 ≠ ∅ ∧ 𝐴 ≼ ℕ) → ∃𝑔 𝑔:ℕ–onto→𝐴)
19		unissb 4900	. . . . . . . . . . . . 13 ⊢ (∪ 𝐴 ⊆ ℝ ↔ ∀𝑥 ∈ 𝐴 𝑥 ⊆ ℝ)
20	19	anbi1i 636	. . . . . . . . . . . 12 ⊢ ((∪ 𝐴 ⊆ ℝ ∧ ∀𝑥 ∈ 𝐴 𝑥 ≼ ℕ) ↔ (∀𝑥 ∈ 𝐴 𝑥 ⊆ ℝ ∧ ∀𝑥 ∈ 𝐴 𝑥 ≼ ℕ))
21		r19.26 3122	. . . . . . . . . . . 12 ⊢ (∀𝑥 ∈ 𝐴 (𝑥 ⊆ ℝ ∧ 𝑥 ≼ ℕ) ↔ (∀𝑥 ∈ 𝐴 𝑥 ⊆ ℝ ∧ ∀𝑥 ∈ 𝐴 𝑥 ≼ ℕ))
22	20, 21	bitr4i 281	. . . . . . . . . . 11 ⊢ ((∪ 𝐴 ⊆ ℝ ∧ ∀𝑥 ∈ 𝐴 𝑥 ≼ ℕ) ↔ ∀𝑥 ∈ 𝐴 (𝑥 ⊆ ℝ ∧ 𝑥 ≼ ℕ))
23		ovolctb2 25813	. . . . . . . . . . . . . 14 ⊢ ((𝑥 ⊆ ℝ ∧ 𝑥 ≼ ℕ) → (vol*‘𝑥) = 0)
24	23	ex 418	. . . . . . . . . . . . 13 ⊢ (𝑥 ⊆ ℝ → (𝑥 ≼ ℕ → (vol*‘𝑥) = 0))
25	24	imdistani 579	. . . . . . . . . . . 12 ⊢ ((𝑥 ⊆ ℝ ∧ 𝑥 ≼ ℕ) → (𝑥 ⊆ ℝ ∧ (vol*‘𝑥) = 0))
26	25	ralimi 3099	. . . . . . . . . . 11 ⊢ (∀𝑥 ∈ 𝐴 (𝑥 ⊆ ℝ ∧ 𝑥 ≼ ℕ) → ∀𝑥 ∈ 𝐴 (𝑥 ⊆ ℝ ∧ (vol*‘𝑥) = 0))
27	22, 26	sylbi 220	. . . . . . . . . 10 ⊢ ((∪ 𝐴 ⊆ ℝ ∧ ∀𝑥 ∈ 𝐴 𝑥 ≼ ℕ) → ∀𝑥 ∈ 𝐴 (𝑥 ⊆ ℝ ∧ (vol*‘𝑥) = 0))
28	27	ancoms 464	. . . . . . . . 9 ⊢ ((∀𝑥 ∈ 𝐴 𝑥 ≼ ℕ ∧ ∪ 𝐴 ⊆ ℝ) → ∀𝑥 ∈ 𝐴 (𝑥 ⊆ ℝ ∧ (vol*‘𝑥) = 0))
29		foima 6801	. . . . . . . . . . . 12 ⊢ (𝑔:ℕ–onto→𝐴 → (𝑔 “ ℕ) = 𝐴)
30	29	raleqdv 3319	. . . . . . . . . . 11 ⊢ (𝑔:ℕ–onto→𝐴 → (∀𝑥 ∈ (𝑔 “ ℕ)(𝑥 ⊆ ℝ ∧ (vol*‘𝑥) = 0) ↔ ∀𝑥 ∈ 𝐴 (𝑥 ⊆ ℝ ∧ (vol*‘𝑥) = 0)))
31		fofn 6798	. . . . . . . . . . . 12 ⊢ (𝑔:ℕ–onto→𝐴 → 𝑔 Fn ℕ)
32		ssid 3930	. . . . . . . . . . . 12 ⊢ ℕ ⊆ ℕ
33		sseq1 3933	. . . . . . . . . . . . . 14 ⊢ (𝑥 = (𝑔‘𝑚) → (𝑥 ⊆ ℝ ↔ (𝑔‘𝑚) ⊆ ℝ))
34		fveqeq2 6894	. . . . . . . . . . . . . 14 ⊢ (𝑥 = (𝑔‘𝑚) → ((vol*‘𝑥) = 0 ↔ (vol*‘(𝑔‘𝑚)) = 0))
35	33, 34	anbi12d 644	. . . . . . . . . . . . 13 ⊢ (𝑥 = (𝑔‘𝑚) → ((𝑥 ⊆ ℝ ∧ (vol*‘𝑥) = 0) ↔ ((𝑔‘𝑚) ⊆ ℝ ∧ (vol*‘(𝑔‘𝑚)) = 0)))
36	35	ralima 7243	. . . . . . . . . . . 12 ⊢ ((𝑔 Fn ℕ ∧ ℕ ⊆ ℕ) → (∀𝑥 ∈ (𝑔 “ ℕ)(𝑥 ⊆ ℝ ∧ (vol*‘𝑥) = 0) ↔ ∀𝑚 ∈ ℕ ((𝑔‘𝑚) ⊆ ℝ ∧ (vol*‘(𝑔‘𝑚)) = 0)))
37	31, 32, 36	sylancl 598	. . . . . . . . . . 11 ⊢ (𝑔:ℕ–onto→𝐴 → (∀𝑥 ∈ (𝑔 “ ℕ)(𝑥 ⊆ ℝ ∧ (vol*‘𝑥) = 0) ↔ ∀𝑚 ∈ ℕ ((𝑔‘𝑚) ⊆ ℝ ∧ (vol*‘(𝑔‘𝑚)) = 0)))
38	30, 37	bitr3d 284	. . . . . . . . . 10 ⊢ (𝑔:ℕ–onto→𝐴 → (∀𝑥 ∈ 𝐴 (𝑥 ⊆ ℝ ∧ (vol*‘𝑥) = 0) ↔ ∀𝑚 ∈ ℕ ((𝑔‘𝑚) ⊆ ℝ ∧ (vol*‘(𝑔‘𝑚)) = 0)))
39		difss 4072	. . . . . . . . . . . . . . . . . 18 ⊢ ((𝑔‘𝑚) ∖ ∪ 𝑙 ∈ (1..^𝑚)(𝑔‘𝑙)) ⊆ (𝑔‘𝑚)
40		ovolssnul 25808	. . . . . . . . . . . . . . . . . 18 ⊢ ((((𝑔‘𝑚) ∖ ∪ 𝑙 ∈ (1..^𝑚)(𝑔‘𝑙)) ⊆ (𝑔‘𝑚) ∧ (𝑔‘𝑚) ⊆ ℝ ∧ (vol*‘(𝑔‘𝑚)) = 0) → (vol*‘((𝑔‘𝑚) ∖ ∪ 𝑙 ∈ (1..^𝑚)(𝑔‘𝑙))) = 0)
41	39, 40	mp3an1 1477	. . . . . . . . . . . . . . . . 17 ⊢ (((𝑔‘𝑚) ⊆ ℝ ∧ (vol*‘(𝑔‘𝑚)) = 0) → (vol*‘((𝑔‘𝑚) ∖ ∪ 𝑙 ∈ (1..^𝑚)(𝑔‘𝑙))) = 0)
42		ssdifss 4076	. . . . . . . . . . . . . . . . . 18 ⊢ ((𝑔‘𝑚) ⊆ ℝ → ((𝑔‘𝑚) ∖ ∪ 𝑙 ∈ (1..^𝑚)(𝑔‘𝑙)) ⊆ ℝ)
43		nulmbl 25856	. . . . . . . . . . . . . . . . . . 19 ⊢ ((((𝑔‘𝑚) ∖ ∪ 𝑙 ∈ (1..^𝑚)(𝑔‘𝑙)) ⊆ ℝ ∧ (vol*‘((𝑔‘𝑚) ∖ ∪ 𝑙 ∈ (1..^𝑚)(𝑔‘𝑙))) = 0) → ((𝑔‘𝑚) ∖ ∪ 𝑙 ∈ (1..^𝑚)(𝑔‘𝑙)) ∈ dom vol)
44		mblvol 25851	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ (((𝑔‘𝑚) ∖ ∪ 𝑙 ∈ (1..^𝑚)(𝑔‘𝑙)) ∈ dom vol → (vol‘((𝑔‘𝑚) ∖ ∪ 𝑙 ∈ (1..^𝑚)(𝑔‘𝑙))) = (vol*‘((𝑔‘𝑚) ∖ ∪ 𝑙 ∈ (1..^𝑚)(𝑔‘𝑙))))
45	44	eqeq1d 2762	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ (((𝑔‘𝑚) ∖ ∪ 𝑙 ∈ (1..^𝑚)(𝑔‘𝑙)) ∈ dom vol → ((vol‘((𝑔‘𝑚) ∖ ∪ 𝑙 ∈ (1..^𝑚)(𝑔‘𝑙))) = 0 ↔ (vol*‘((𝑔‘𝑚) ∖ ∪ 𝑙 ∈ (1..^𝑚)(𝑔‘𝑙))) = 0))
46	45	biimpar 483	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ ((((𝑔‘𝑚) ∖ ∪ 𝑙 ∈ (1..^𝑚)(𝑔‘𝑙)) ∈ dom vol ∧ (vol*‘((𝑔‘𝑚) ∖ ∪ 𝑙 ∈ (1..^𝑚)(𝑔‘𝑙))) = 0) → (vol‘((𝑔‘𝑚) ∖ ∪ 𝑙 ∈ (1..^𝑚)(𝑔‘𝑙))) = 0)
47		0re 11310	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ 0 ∈ ℝ
48	46, 47	eqeltrdi 2868	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ ((((𝑔‘𝑚) ∖ ∪ 𝑙 ∈ (1..^𝑚)(𝑔‘𝑙)) ∈ dom vol ∧ (vol*‘((𝑔‘𝑚) ∖ ∪ 𝑙 ∈ (1..^𝑚)(𝑔‘𝑙))) = 0) → (vol‘((𝑔‘𝑚) ∖ ∪ 𝑙 ∈ (1..^𝑚)(𝑔‘𝑙))) ∈ ℝ)
49	48	expcom 419	. . . . . . . . . . . . . . . . . . . . 21 ⊢ ((vol*‘((𝑔‘𝑚) ∖ ∪ 𝑙 ∈ (1..^𝑚)(𝑔‘𝑙))) = 0 → (((𝑔‘𝑚) ∖ ∪ 𝑙 ∈ (1..^𝑚)(𝑔‘𝑙)) ∈ dom vol → (vol‘((𝑔‘𝑚) ∖ ∪ 𝑙 ∈ (1..^𝑚)(𝑔‘𝑙))) ∈ ℝ))
50	49	ancld 560	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((vol*‘((𝑔‘𝑚) ∖ ∪ 𝑙 ∈ (1..^𝑚)(𝑔‘𝑙))) = 0 → (((𝑔‘𝑚) ∖ ∪ 𝑙 ∈ (1..^𝑚)(𝑔‘𝑙)) ∈ dom vol → (((𝑔‘𝑚) ∖ ∪ 𝑙 ∈ (1..^𝑚)(𝑔‘𝑙)) ∈ dom vol ∧ (vol‘((𝑔‘𝑚) ∖ ∪ 𝑙 ∈ (1..^𝑚)(𝑔‘𝑙))) ∈ ℝ)))
51	50	adantl 487	. . . . . . . . . . . . . . . . . . 19 ⊢ ((((𝑔‘𝑚) ∖ ∪ 𝑙 ∈ (1..^𝑚)(𝑔‘𝑙)) ⊆ ℝ ∧ (vol*‘((𝑔‘𝑚) ∖ ∪ 𝑙 ∈ (1..^𝑚)(𝑔‘𝑙))) = 0) → (((𝑔‘𝑚) ∖ ∪ 𝑙 ∈ (1..^𝑚)(𝑔‘𝑙)) ∈ dom vol → (((𝑔‘𝑚) ∖ ∪ 𝑙 ∈ (1..^𝑚)(𝑔‘𝑙)) ∈ dom vol ∧ (vol‘((𝑔‘𝑚) ∖ ∪ 𝑙 ∈ (1..^𝑚)(𝑔‘𝑙))) ∈ ℝ)))
52	43, 51	mpd 16	. . . . . . . . . . . . . . . . . 18 ⊢ ((((𝑔‘𝑚) ∖ ∪ 𝑙 ∈ (1..^𝑚)(𝑔‘𝑙)) ⊆ ℝ ∧ (vol*‘((𝑔‘𝑚) ∖ ∪ 𝑙 ∈ (1..^𝑚)(𝑔‘𝑙))) = 0) → (((𝑔‘𝑚) ∖ ∪ 𝑙 ∈ (1..^𝑚)(𝑔‘𝑙)) ∈ dom vol ∧ (vol‘((𝑔‘𝑚) ∖ ∪ 𝑙 ∈ (1..^𝑚)(𝑔‘𝑙))) ∈ ℝ))
53	42, 52	sylan 592	. . . . . . . . . . . . . . . . 17 ⊢ (((𝑔‘𝑚) ⊆ ℝ ∧ (vol*‘((𝑔‘𝑚) ∖ ∪ 𝑙 ∈ (1..^𝑚)(𝑔‘𝑙))) = 0) → (((𝑔‘𝑚) ∖ ∪ 𝑙 ∈ (1..^𝑚)(𝑔‘𝑙)) ∈ dom vol ∧ (vol‘((𝑔‘𝑚) ∖ ∪ 𝑙 ∈ (1..^𝑚)(𝑔‘𝑙))) ∈ ℝ))
54	41, 53	syldan 603	. . . . . . . . . . . . . . . 16 ⊢ (((𝑔‘𝑚) ⊆ ℝ ∧ (vol*‘(𝑔‘𝑚)) = 0) → (((𝑔‘𝑚) ∖ ∪ 𝑙 ∈ (1..^𝑚)(𝑔‘𝑙)) ∈ dom vol ∧ (vol‘((𝑔‘𝑚) ∖ ∪ 𝑙 ∈ (1..^𝑚)(𝑔‘𝑙))) ∈ ℝ))
55	54	ralimi 3099	. . . . . . . . . . . . . . 15 ⊢ (∀𝑚 ∈ ℕ ((𝑔‘𝑚) ⊆ ℝ ∧ (vol*‘(𝑔‘𝑚)) = 0) → ∀𝑚 ∈ ℕ (((𝑔‘𝑚) ∖ ∪ 𝑙 ∈ (1..^𝑚)(𝑔‘𝑙)) ∈ dom vol ∧ (vol‘((𝑔‘𝑚) ∖ ∪ 𝑙 ∈ (1..^𝑚)(𝑔‘𝑙))) ∈ ℝ))
56		fveq2 6885	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (𝑚 = 𝑛 → (𝑔‘𝑚) = (𝑔‘𝑛))
57		oveq2 7428	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (𝑚 = 𝑛 → (1..^𝑚) = (1..^𝑛))
58	57	iuneq1d 4978	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (𝑚 = 𝑛 → ∪ 𝑙 ∈ (1..^𝑚)(𝑔‘𝑙) = ∪ 𝑙 ∈ (1..^𝑛)(𝑔‘𝑙))
59	56, 58	difeq12d 4064	. . . . . . . . . . . . . . . . . . . 20 ⊢ (𝑚 = 𝑛 → ((𝑔‘𝑚) ∖ ∪ 𝑙 ∈ (1..^𝑚)(𝑔‘𝑙)) = ((𝑔‘𝑛) ∖ ∪ 𝑙 ∈ (1..^𝑛)(𝑔‘𝑙)))
60		eqid 2760	. . . . . . . . . . . . . . . . . . . 20 ⊢ (𝑚 ∈ ℕ ↦ ((𝑔‘𝑚) ∖ ∪ 𝑙 ∈ (1..^𝑚)(𝑔‘𝑙))) = (𝑚 ∈ ℕ ↦ ((𝑔‘𝑚) ∖ ∪ 𝑙 ∈ (1..^𝑚)(𝑔‘𝑙)))
61		fvex 6898	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (𝑔‘𝑛) ∈ V
62		difexg 5290	. . . . . . . . . . . . . . . . . . . . 21 ⊢ ((𝑔‘𝑛) ∈ V → ((𝑔‘𝑛) ∖ ∪ 𝑙 ∈ (1..^𝑛)(𝑔‘𝑙)) ∈ V)
63	61, 62	ax-mp 5	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((𝑔‘𝑛) ∖ ∪ 𝑙 ∈ (1..^𝑛)(𝑔‘𝑙)) ∈ V
64	59, 60, 63	fvmpt 6993	. . . . . . . . . . . . . . . . . . 19 ⊢ (𝑛 ∈ ℕ → ((𝑚 ∈ ℕ ↦ ((𝑔‘𝑚) ∖ ∪ 𝑙 ∈ (1..^𝑚)(𝑔‘𝑙)))‘𝑛) = ((𝑔‘𝑛) ∖ ∪ 𝑙 ∈ (1..^𝑛)(𝑔‘𝑙)))
65	64	eleq1d 2845	. . . . . . . . . . . . . . . . . 18 ⊢ (𝑛 ∈ ℕ → (((𝑚 ∈ ℕ ↦ ((𝑔‘𝑚) ∖ ∪ 𝑙 ∈ (1..^𝑚)(𝑔‘𝑙)))‘𝑛) ∈ dom vol ↔ ((𝑔‘𝑛) ∖ ∪ 𝑙 ∈ (1..^𝑛)(𝑔‘𝑙)) ∈ dom vol))
66	64	fveq2d 6889	. . . . . . . . . . . . . . . . . . 19 ⊢ (𝑛 ∈ ℕ → (vol‘((𝑚 ∈ ℕ ↦ ((𝑔‘𝑚) ∖ ∪ 𝑙 ∈ (1..^𝑚)(𝑔‘𝑙)))‘𝑛)) = (vol‘((𝑔‘𝑛) ∖ ∪ 𝑙 ∈ (1..^𝑛)(𝑔‘𝑙))))
67	66	eleq1d 2845	. . . . . . . . . . . . . . . . . 18 ⊢ (𝑛 ∈ ℕ → ((vol‘((𝑚 ∈ ℕ ↦ ((𝑔‘𝑚) ∖ ∪ 𝑙 ∈ (1..^𝑚)(𝑔‘𝑙)))‘𝑛)) ∈ ℝ ↔ (vol‘((𝑔‘𝑛) ∖ ∪ 𝑙 ∈ (1..^𝑛)(𝑔‘𝑙))) ∈ ℝ))
68	65, 67	anbi12d 644	. . . . . . . . . . . . . . . . 17 ⊢ (𝑛 ∈ ℕ → ((((𝑚 ∈ ℕ ↦ ((𝑔‘𝑚) ∖ ∪ 𝑙 ∈ (1..^𝑚)(𝑔‘𝑙)))‘𝑛) ∈ dom vol ∧ (vol‘((𝑚 ∈ ℕ ↦ ((𝑔‘𝑚) ∖ ∪ 𝑙 ∈ (1..^𝑚)(𝑔‘𝑙)))‘𝑛)) ∈ ℝ) ↔ (((𝑔‘𝑛) ∖ ∪ 𝑙 ∈ (1..^𝑛)(𝑔‘𝑙)) ∈ dom vol ∧ (vol‘((𝑔‘𝑛) ∖ ∪ 𝑙 ∈ (1..^𝑛)(𝑔‘𝑙))) ∈ ℝ)))
69	68	ralbiia 3106	. . . . . . . . . . . . . . . 16 ⊢ (∀𝑛 ∈ ℕ (((𝑚 ∈ ℕ ↦ ((𝑔‘𝑚) ∖ ∪ 𝑙 ∈ (1..^𝑚)(𝑔‘𝑙)))‘𝑛) ∈ dom vol ∧ (vol‘((𝑚 ∈ ℕ ↦ ((𝑔‘𝑚) ∖ ∪ 𝑙 ∈ (1..^𝑚)(𝑔‘𝑙)))‘𝑛)) ∈ ℝ) ↔ ∀𝑛 ∈ ℕ (((𝑔‘𝑛) ∖ ∪ 𝑙 ∈ (1..^𝑛)(𝑔‘𝑙)) ∈ dom vol ∧ (vol‘((𝑔‘𝑛) ∖ ∪ 𝑙 ∈ (1..^𝑛)(𝑔‘𝑙))) ∈ ℝ))
70		fveq2 6885	. . . . . . . . . . . . . . . . . . . 20 ⊢ (𝑛 = 𝑚 → (𝑔‘𝑛) = (𝑔‘𝑚))
71		oveq2 7428	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (𝑛 = 𝑚 → (1..^𝑛) = (1..^𝑚))
72	71	iuneq1d 4978	. . . . . . . . . . . . . . . . . . . 20 ⊢ (𝑛 = 𝑚 → ∪ 𝑙 ∈ (1..^𝑛)(𝑔‘𝑙) = ∪ 𝑙 ∈ (1..^𝑚)(𝑔‘𝑙))
73	70, 72	difeq12d 4064	. . . . . . . . . . . . . . . . . . 19 ⊢ (𝑛 = 𝑚 → ((𝑔‘𝑛) ∖ ∪ 𝑙 ∈ (1..^𝑛)(𝑔‘𝑙)) = ((𝑔‘𝑚) ∖ ∪ 𝑙 ∈ (1..^𝑚)(𝑔‘𝑙)))
74	73	eleq1d 2845	. . . . . . . . . . . . . . . . . 18 ⊢ (𝑛 = 𝑚 → (((𝑔‘𝑛) ∖ ∪ 𝑙 ∈ (1..^𝑛)(𝑔‘𝑙)) ∈ dom vol ↔ ((𝑔‘𝑚) ∖ ∪ 𝑙 ∈ (1..^𝑚)(𝑔‘𝑙)) ∈ dom vol))
75	73	fveq2d 6889	. . . . . . . . . . . . . . . . . . 19 ⊢ (𝑛 = 𝑚 → (vol‘((𝑔‘𝑛) ∖ ∪ 𝑙 ∈ (1..^𝑛)(𝑔‘𝑙))) = (vol‘((𝑔‘𝑚) ∖ ∪ 𝑙 ∈ (1..^𝑚)(𝑔‘𝑙))))
76	75	eleq1d 2845	. . . . . . . . . . . . . . . . . 18 ⊢ (𝑛 = 𝑚 → ((vol‘((𝑔‘𝑛) ∖ ∪ 𝑙 ∈ (1..^𝑛)(𝑔‘𝑙))) ∈ ℝ ↔ (vol‘((𝑔‘𝑚) ∖ ∪ 𝑙 ∈ (1..^𝑚)(𝑔‘𝑙))) ∈ ℝ))
77	74, 76	anbi12d 644	. . . . . . . . . . . . . . . . 17 ⊢ (𝑛 = 𝑚 → ((((𝑔‘𝑛) ∖ ∪ 𝑙 ∈ (1..^𝑛)(𝑔‘𝑙)) ∈ dom vol ∧ (vol‘((𝑔‘𝑛) ∖ ∪ 𝑙 ∈ (1..^𝑛)(𝑔‘𝑙))) ∈ ℝ) ↔ (((𝑔‘𝑚) ∖ ∪ 𝑙 ∈ (1..^𝑚)(𝑔‘𝑙)) ∈ dom vol ∧ (vol‘((𝑔‘𝑚) ∖ ∪ 𝑙 ∈ (1..^𝑚)(𝑔‘𝑙))) ∈ ℝ)))
78	77	cbvralvw 3240	. . . . . . . . . . . . . . . 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 6885	. . . . . . . . . . . . . . . 16 ⊢ (𝑛 = 𝑙 → (𝑔‘𝑛) = (𝑔‘𝑙))
82	81	iundisj2 25870	. . . . . . . . . . . . . . 15 ⊢ Disj 𝑛 ∈ ℕ ((𝑔‘𝑛) ∖ ∪ 𝑙 ∈ (1..^𝑛)(𝑔‘𝑙))
83		disjeq2 5073	. . . . . . . . . . . . . . . 16 ⊢ (∀𝑛 ∈ ℕ ((𝑚 ∈ ℕ ↦ ((𝑔‘𝑚) ∖ ∪ 𝑙 ∈ (1..^𝑚)(𝑔‘𝑙)))‘𝑛) = ((𝑔‘𝑛) ∖ ∪ 𝑙 ∈ (1..^𝑛)(𝑔‘𝑙)) → (Disj 𝑛 ∈ ℕ ((𝑚 ∈ ℕ ↦ ((𝑔‘𝑚) ∖ ∪ 𝑙 ∈ (1..^𝑚)(𝑔‘𝑙)))‘𝑛) ↔ Disj 𝑛 ∈ ℕ ((𝑔‘𝑛) ∖ ∪ 𝑙 ∈ (1..^𝑛)(𝑔‘𝑙))))
84	83, 64	mprg 3082	. . . . . . . . . . . . . . 15 ⊢ (Disj 𝑛 ∈ ℕ ((𝑚 ∈ ℕ ↦ ((𝑔‘𝑚) ∖ ∪ 𝑙 ∈ (1..^𝑚)(𝑔‘𝑙)))‘𝑛) ↔ Disj 𝑛 ∈ ℕ ((𝑔‘𝑛) ∖ ∪ 𝑙 ∈ (1..^𝑛)(𝑔‘𝑙)))
85	82, 84	mpbir 234	. . . . . . . . . . . . . 14 ⊢ Disj 𝑛 ∈ ℕ ((𝑚 ∈ ℕ ↦ ((𝑔‘𝑚) ∖ ∪ 𝑙 ∈ (1..^𝑚)(𝑔‘𝑙)))‘𝑛)
86		nnex 12341	. . . . . . . . . . . . . . . . 17 ⊢ ℕ ∈ V
87	86	mptex 7229	. . . . . . . . . . . . . . . 16 ⊢ (𝑚 ∈ ℕ ↦ ((𝑔‘𝑚) ∖ ∪ 𝑙 ∈ (1..^𝑚)(𝑔‘𝑙))) ∈ V
88		fveq1 6884	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (𝑓 = (𝑚 ∈ ℕ ↦ ((𝑔‘𝑚) ∖ ∪ 𝑙 ∈ (1..^𝑚)(𝑔‘𝑙))) → (𝑓‘𝑛) = ((𝑚 ∈ ℕ ↦ ((𝑔‘𝑚) ∖ ∪ 𝑙 ∈ (1..^𝑚)(𝑔‘𝑙)))‘𝑛))
89	88	eleq1d 2845	. . . . . . . . . . . . . . . . . . . 20 ⊢ (𝑓 = (𝑚 ∈ ℕ ↦ ((𝑔‘𝑚) ∖ ∪ 𝑙 ∈ (1..^𝑚)(𝑔‘𝑙))) → ((𝑓‘𝑛) ∈ dom vol ↔ ((𝑚 ∈ ℕ ↦ ((𝑔‘𝑚) ∖ ∪ 𝑙 ∈ (1..^𝑚)(𝑔‘𝑙)))‘𝑛) ∈ dom vol))
90	88	fveq2d 6889	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (𝑓 = (𝑚 ∈ ℕ ↦ ((𝑔‘𝑚) ∖ ∪ 𝑙 ∈ (1..^𝑚)(𝑔‘𝑙))) → (vol‘(𝑓‘𝑛)) = (vol‘((𝑚 ∈ ℕ ↦ ((𝑔‘𝑚) ∖ ∪ 𝑙 ∈ (1..^𝑚)(𝑔‘𝑙)))‘𝑛)))
91	90	eleq1d 2845	. . . . . . . . . . . . . . . . . . . 20 ⊢ (𝑓 = (𝑚 ∈ ℕ ↦ ((𝑔‘𝑚) ∖ ∪ 𝑙 ∈ (1..^𝑚)(𝑔‘𝑙))) → ((vol‘(𝑓‘𝑛)) ∈ ℝ ↔ (vol‘((𝑚 ∈ ℕ ↦ ((𝑔‘𝑚) ∖ ∪ 𝑙 ∈ (1..^𝑚)(𝑔‘𝑙)))‘𝑛)) ∈ ℝ))
92	89, 91	anbi12d 644	. . . . . . . . . . . . . . . . . . 19 ⊢ (𝑓 = (𝑚 ∈ ℕ ↦ ((𝑔‘𝑚) ∖ ∪ 𝑙 ∈ (1..^𝑚)(𝑔‘𝑙))) → (((𝑓‘𝑛) ∈ dom vol ∧ (vol‘(𝑓‘𝑛)) ∈ ℝ) ↔ (((𝑚 ∈ ℕ ↦ ((𝑔‘𝑚) ∖ ∪ 𝑙 ∈ (1..^𝑚)(𝑔‘𝑙)))‘𝑛) ∈ dom vol ∧ (vol‘((𝑚 ∈ ℕ ↦ ((𝑔‘𝑚) ∖ ∪ 𝑙 ∈ (1..^𝑚)(𝑔‘𝑙)))‘𝑛)) ∈ ℝ)))
93	92	ralbidv 3185	. . . . . . . . . . . . . . . . . 18 ⊢ (𝑓 = (𝑚 ∈ ℕ ↦ ((𝑔‘𝑚) ∖ ∪ 𝑙 ∈ (1..^𝑚)(𝑔‘𝑙))) → (∀𝑛 ∈ ℕ ((𝑓‘𝑛) ∈ dom vol ∧ (vol‘(𝑓‘𝑛)) ∈ ℝ) ↔ ∀𝑛 ∈ ℕ (((𝑚 ∈ ℕ ↦ ((𝑔‘𝑚) ∖ ∪ 𝑙 ∈ (1..^𝑚)(𝑔‘𝑙)))‘𝑛) ∈ dom vol ∧ (vol‘((𝑚 ∈ ℕ ↦ ((𝑔‘𝑚) ∖ ∪ 𝑙 ∈ (1..^𝑚)(𝑔‘𝑙)))‘𝑛)) ∈ ℝ)))
94	88	adantr 486	. . . . . . . . . . . . . . . . . . 19 ⊢ ((𝑓 = (𝑚 ∈ ℕ ↦ ((𝑔‘𝑚) ∖ ∪ 𝑙 ∈ (1..^𝑚)(𝑔‘𝑙))) ∧ 𝑛 ∈ ℕ) → (𝑓‘𝑛) = ((𝑚 ∈ ℕ ↦ ((𝑔‘𝑚) ∖ ∪ 𝑙 ∈ (1..^𝑚)(𝑔‘𝑙)))‘𝑛))
95	94	disjeq2dv 5074	. . . . . . . . . . . . . . . . . 18 ⊢ (𝑓 = (𝑚 ∈ ℕ ↦ ((𝑔‘𝑚) ∖ ∪ 𝑙 ∈ (1..^𝑚)(𝑔‘𝑙))) → (Disj 𝑛 ∈ ℕ (𝑓‘𝑛) ↔ Disj 𝑛 ∈ ℕ ((𝑚 ∈ ℕ ↦ ((𝑔‘𝑚) ∖ ∪ 𝑙 ∈ (1..^𝑚)(𝑔‘𝑙)))‘𝑛)))
96	93, 95	anbi12d 644	. . . . . . . . . . . . . . . . 17 ⊢ (𝑓 = (𝑚 ∈ ℕ ↦ ((𝑔‘𝑚) ∖ ∪ 𝑙 ∈ (1..^𝑚)(𝑔‘𝑙))) → ((∀𝑛 ∈ ℕ ((𝑓‘𝑛) ∈ dom vol ∧ (vol‘(𝑓‘𝑛)) ∈ ℝ) ∧ Disj 𝑛 ∈ ℕ (𝑓‘𝑛)) ↔ (∀𝑛 ∈ ℕ (((𝑚 ∈ ℕ ↦ ((𝑔‘𝑚) ∖ ∪ 𝑙 ∈ (1..^𝑚)(𝑔‘𝑙)))‘𝑛) ∈ dom vol ∧ (vol‘((𝑚 ∈ ℕ ↦ ((𝑔‘𝑚) ∖ ∪ 𝑙 ∈ (1..^𝑚)(𝑔‘𝑙)))‘𝑛)) ∈ ℝ) ∧ Disj 𝑛 ∈ ℕ ((𝑚 ∈ ℕ ↦ ((𝑔‘𝑚) ∖ ∪ 𝑙 ∈ (1..^𝑚)(𝑔‘𝑙)))‘𝑛))))
97	88	iuneq2d 4980	. . . . . . . . . . . . . . . . . . 19 ⊢ (𝑓 = (𝑚 ∈ ℕ ↦ ((𝑔‘𝑚) ∖ ∪ 𝑙 ∈ (1..^𝑚)(𝑔‘𝑙))) → ∪ 𝑛 ∈ ℕ (𝑓‘𝑛) = ∪ 𝑛 ∈ ℕ ((𝑚 ∈ ℕ ↦ ((𝑔‘𝑚) ∖ ∪ 𝑙 ∈ (1..^𝑚)(𝑔‘𝑙)))‘𝑛))
98	97	fveq2d 6889	. . . . . . . . . . . . . . . . . 18 ⊢ (𝑓 = (𝑚 ∈ ℕ ↦ ((𝑔‘𝑚) ∖ ∪ 𝑙 ∈ (1..^𝑚)(𝑔‘𝑙))) → (vol‘∪ 𝑛 ∈ ℕ (𝑓‘𝑛)) = (vol‘∪ 𝑛 ∈ ℕ ((𝑚 ∈ ℕ ↦ ((𝑔‘𝑚) ∖ ∪ 𝑙 ∈ (1..^𝑚)(𝑔‘𝑙)))‘𝑛)))
99		voliunnfl.1	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ 𝑆 = seq1( + , 𝐺)
100		voliunnfl.2	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ 𝐺 = (𝑛 ∈ ℕ ↦ (vol‘(𝑓‘𝑛)))
101		seqeq3 14149	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ (𝐺 = (𝑛 ∈ ℕ ↦ (vol‘(𝑓‘𝑛))) → seq1( + , 𝐺) = seq1( + , (𝑛 ∈ ℕ ↦ (vol‘(𝑓‘𝑛)))))
102	100, 101	ax-mp 5	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ seq1( + , 𝐺) = seq1( + , (𝑛 ∈ ℕ ↦ (vol‘(𝑓‘𝑛))))
103	99, 102	eqtri 2783	. . . . . . . . . . . . . . . . . . . . 21 ⊢ 𝑆 = seq1( + , (𝑛 ∈ ℕ ↦ (vol‘(𝑓‘𝑛))))
104	103	rneqi 5918	. . . . . . . . . . . . . . . . . . . 20 ⊢ ran 𝑆 = ran seq1( + , (𝑛 ∈ ℕ ↦ (vol‘(𝑓‘𝑛))))
105	104	supeq1i 9439	. . . . . . . . . . . . . . . . . . 19 ⊢ sup(ran 𝑆, ℝ*, < ) = sup(ran seq1( + , (𝑛 ∈ ℕ ↦ (vol‘(𝑓‘𝑛)))), ℝ*, < )
106	90	mpteq2dv 5198	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (𝑓 = (𝑚 ∈ ℕ ↦ ((𝑔‘𝑚) ∖ ∪ 𝑙 ∈ (1..^𝑚)(𝑔‘𝑙))) → (𝑛 ∈ ℕ ↦ (vol‘(𝑓‘𝑛))) = (𝑛 ∈ ℕ ↦ (vol‘((𝑚 ∈ ℕ ↦ ((𝑔‘𝑚) ∖ ∪ 𝑙 ∈ (1..^𝑚)(𝑔‘𝑙)))‘𝑛))))
107	106	seqeq3d 14152	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (𝑓 = (𝑚 ∈ ℕ ↦ ((𝑔‘𝑚) ∖ ∪ 𝑙 ∈ (1..^𝑚)(𝑔‘𝑙))) → seq1( + , (𝑛 ∈ ℕ ↦ (vol‘(𝑓‘𝑛)))) = seq1( + , (𝑛 ∈ ℕ ↦ (vol‘((𝑚 ∈ ℕ ↦ ((𝑔‘𝑚) ∖ ∪ 𝑙 ∈ (1..^𝑚)(𝑔‘𝑙)))‘𝑛)))))
108	107	rneqd 5919	. . . . . . . . . . . . . . . . . . . 20 ⊢ (𝑓 = (𝑚 ∈ ℕ ↦ ((𝑔‘𝑚) ∖ ∪ 𝑙 ∈ (1..^𝑚)(𝑔‘𝑙))) → ran seq1( + , (𝑛 ∈ ℕ ↦ (vol‘(𝑓‘𝑛)))) = ran seq1( + , (𝑛 ∈ ℕ ↦ (vol‘((𝑚 ∈ ℕ ↦ ((𝑔‘𝑚) ∖ ∪ 𝑙 ∈ (1..^𝑚)(𝑔‘𝑙)))‘𝑛)))))
109	108	supeq1d 9438	. . . . . . . . . . . . . . . . . . 19 ⊢ (𝑓 = (𝑚 ∈ ℕ ↦ ((𝑔‘𝑚) ∖ ∪ 𝑙 ∈ (1..^𝑚)(𝑔‘𝑙))) → sup(ran seq1( + , (𝑛 ∈ ℕ ↦ (vol‘(𝑓‘𝑛)))), ℝ*, < ) = sup(ran seq1( + , (𝑛 ∈ ℕ ↦ (vol‘((𝑚 ∈ ℕ ↦ ((𝑔‘𝑚) ∖ ∪ 𝑙 ∈ (1..^𝑚)(𝑔‘𝑙)))‘𝑛)))), ℝ*, < ))
110	105, 109	eqtrid 2807	. . . . . . . . . . . . . . . . . 18 ⊢ (𝑓 = (𝑚 ∈ ℕ ↦ ((𝑔‘𝑚) ∖ ∪ 𝑙 ∈ (1..^𝑚)(𝑔‘𝑙))) → sup(ran 𝑆, ℝ*, < ) = sup(ran seq1( + , (𝑛 ∈ ℕ ↦ (vol‘((𝑚 ∈ ℕ ↦ ((𝑔‘𝑚) ∖ ∪ 𝑙 ∈ (1..^𝑚)(𝑔‘𝑙)))‘𝑛)))), ℝ*, < ))
111	98, 110	eqeq12d 2776	. . . . . . . . . . . . . . . . 17 ⊢ (𝑓 = (𝑚 ∈ ℕ ↦ ((𝑔‘𝑚) ∖ ∪ 𝑙 ∈ (1..^𝑚)(𝑔‘𝑙))) → ((vol‘∪ 𝑛 ∈ ℕ (𝑓‘𝑛)) = sup(ran 𝑆, ℝ*, < ) ↔ (vol‘∪ 𝑛 ∈ ℕ ((𝑚 ∈ ℕ ↦ ((𝑔‘𝑚) ∖ ∪ 𝑙 ∈ (1..^𝑚)(𝑔‘𝑙)))‘𝑛)) = sup(ran seq1( + , (𝑛 ∈ ℕ ↦ (vol‘((𝑚 ∈ ℕ ↦ ((𝑔‘𝑚) ∖ ∪ 𝑙 ∈ (1..^𝑚)(𝑔‘𝑙)))‘𝑛)))), ℝ*, < )))
112	96, 111	imbi12d 347	. . . . . . . . . . . . . . . 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 3520	. . . . . . . . . . . . . . 15 ⊢ ((∀𝑛 ∈ ℕ (((𝑚 ∈ ℕ ↦ ((𝑔‘𝑚) ∖ ∪ 𝑙 ∈ (1..^𝑚)(𝑔‘𝑙)))‘𝑛) ∈ dom vol ∧ (vol‘((𝑚 ∈ ℕ ↦ ((𝑔‘𝑚) ∖ ∪ 𝑙 ∈ (1..^𝑚)(𝑔‘𝑙)))‘𝑛)) ∈ ℝ) ∧ Disj 𝑛 ∈ ℕ ((𝑚 ∈ ℕ ↦ ((𝑔‘𝑚) ∖ ∪ 𝑙 ∈ (1..^𝑚)(𝑔‘𝑙)))‘𝑛)) → (vol‘∪ 𝑛 ∈ ℕ ((𝑚 ∈ ℕ ↦ ((𝑔‘𝑚) ∖ ∪ 𝑙 ∈ (1..^𝑚)(𝑔‘𝑙)))‘𝑛)) = sup(ran seq1( + , (𝑛 ∈ ℕ ↦ (vol‘((𝑚 ∈ ℕ ↦ ((𝑔‘𝑚) ∖ ∪ 𝑙 ∈ (1..^𝑚)(𝑔‘𝑙)))‘𝑛)))), ℝ*, < ))
115	64	iuneq2i 4972	. . . . . . . . . . . . . . . 16 ⊢ ∪ 𝑛 ∈ ℕ ((𝑚 ∈ ℕ ↦ ((𝑔‘𝑚) ∖ ∪ 𝑙 ∈ (1..^𝑚)(𝑔‘𝑙)))‘𝑛) = ∪ 𝑛 ∈ ℕ ((𝑔‘𝑛) ∖ ∪ 𝑙 ∈ (1..^𝑛)(𝑔‘𝑙))
116	115	fveq2i 6888	. . . . . . . . . . . . . . 15 ⊢ (vol‘∪ 𝑛 ∈ ℕ ((𝑚 ∈ ℕ ↦ ((𝑔‘𝑚) ∖ ∪ 𝑙 ∈ (1..^𝑚)(𝑔‘𝑙)))‘𝑛)) = (vol‘∪ 𝑛 ∈ ℕ ((𝑔‘𝑛) ∖ ∪ 𝑙 ∈ (1..^𝑛)(𝑔‘𝑙)))
117	66	mpteq2ia 5199	. . . . . . . . . . . . . . . . . 18 ⊢ (𝑛 ∈ ℕ ↦ (vol‘((𝑚 ∈ ℕ ↦ ((𝑔‘𝑚) ∖ ∪ 𝑙 ∈ (1..^𝑚)(𝑔‘𝑙)))‘𝑛))) = (𝑛 ∈ ℕ ↦ (vol‘((𝑔‘𝑛) ∖ ∪ 𝑙 ∈ (1..^𝑛)(𝑔‘𝑙))))
118		seqeq3 14149	. . . . . . . . . . . . . . . . . 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 5918	. . . . . . . . . . . . . . . 16 ⊢ ran seq1( + , (𝑛 ∈ ℕ ↦ (vol‘((𝑚 ∈ ℕ ↦ ((𝑔‘𝑚) ∖ ∪ 𝑙 ∈ (1..^𝑚)(𝑔‘𝑙)))‘𝑛)))) = ran seq1( + , (𝑛 ∈ ℕ ↦ (vol‘((𝑔‘𝑛) ∖ ∪ 𝑙 ∈ (1..^𝑛)(𝑔‘𝑙)))))
121	120	supeq1i 9439	. . . . . . . . . . . . . . 15 ⊢ sup(ran seq1( + , (𝑛 ∈ ℕ ↦ (vol‘((𝑚 ∈ ℕ ↦ ((𝑔‘𝑚) ∖ ∪ 𝑙 ∈ (1..^𝑚)(𝑔‘𝑙)))‘𝑛)))), ℝ*, < ) = sup(ran seq1( + , (𝑛 ∈ ℕ ↦ (vol‘((𝑔‘𝑛) ∖ ∪ 𝑙 ∈ (1..^𝑛)(𝑔‘𝑙))))), ℝ*, < )
122	114, 116, 121	3eqtr3g 2818	. . . . . . . . . . . . . 14 ⊢ ((∀𝑛 ∈ ℕ (((𝑚 ∈ ℕ ↦ ((𝑔‘𝑚) ∖ ∪ 𝑙 ∈ (1..^𝑚)(𝑔‘𝑙)))‘𝑛) ∈ dom vol ∧ (vol‘((𝑚 ∈ ℕ ↦ ((𝑔‘𝑚) ∖ ∪ 𝑙 ∈ (1..^𝑚)(𝑔‘𝑙)))‘𝑛)) ∈ ℝ) ∧ Disj 𝑛 ∈ ℕ ((𝑚 ∈ ℕ ↦ ((𝑔‘𝑚) ∖ ∪ 𝑙 ∈ (1..^𝑚)(𝑔‘𝑙)))‘𝑛)) → (vol‘∪ 𝑛 ∈ ℕ ((𝑔‘𝑛) ∖ ∪ 𝑙 ∈ (1..^𝑛)(𝑔‘𝑙))) = sup(ran seq1( + , (𝑛 ∈ ℕ ↦ (vol‘((𝑔‘𝑛) ∖ ∪ 𝑙 ∈ (1..^𝑛)(𝑔‘𝑙))))), ℝ*, < ))
123	80, 85, 122	sylancl 598	. . . . . . . . . . . . 13 ⊢ (∀𝑚 ∈ ℕ ((𝑔‘𝑚) ⊆ ℝ ∧ (vol*‘(𝑔‘𝑚)) = 0) → (vol‘∪ 𝑛 ∈ ℕ ((𝑔‘𝑛) ∖ ∪ 𝑙 ∈ (1..^𝑛)(𝑔‘𝑙))) = sup(ran seq1( + , (𝑛 ∈ ℕ ↦ (vol‘((𝑔‘𝑛) ∖ ∪ 𝑙 ∈ (1..^𝑛)(𝑔‘𝑙))))), ℝ*, < ))
124	123	adantl 487	. . . . . . . . . . . 12 ⊢ ((𝑔:ℕ–onto→𝐴 ∧ ∀𝑚 ∈ ℕ ((𝑔‘𝑚) ⊆ ℝ ∧ (vol*‘(𝑔‘𝑚)) = 0)) → (vol‘∪ 𝑛 ∈ ℕ ((𝑔‘𝑛) ∖ ∪ 𝑙 ∈ (1..^𝑛)(𝑔‘𝑙))) = sup(ran seq1( + , (𝑛 ∈ ℕ ↦ (vol‘((𝑔‘𝑛) ∖ ∪ 𝑙 ∈ (1..^𝑛)(𝑔‘𝑙))))), ℝ*, < ))
125	81	iundisj 25869	. . . . . . . . . . . . . . . 16 ⊢ ∪ 𝑛 ∈ ℕ (𝑔‘𝑛) = ∪ 𝑛 ∈ ℕ ((𝑔‘𝑛) ∖ ∪ 𝑙 ∈ (1..^𝑛)(𝑔‘𝑙))
126		fofun 6797	. . . . . . . . . . . . . . . . 17 ⊢ (𝑔:ℕ–onto→𝐴 → Fun 𝑔)
127		funiunfv 7252	. . . . . . . . . . . . . . . . 17 ⊢ (Fun 𝑔 → ∪ 𝑛 ∈ ℕ (𝑔‘𝑛) = ∪ (𝑔 “ ℕ))
128	126, 127	syl 18	. . . . . . . . . . . . . . . 16 ⊢ (𝑔:ℕ–onto→𝐴 → ∪ 𝑛 ∈ ℕ (𝑔‘𝑛) = ∪ (𝑔 “ ℕ))
129	125, 128	eqtr3id 2809	. . . . . . . . . . . . . . 15 ⊢ (𝑔:ℕ–onto→𝐴 → ∪ 𝑛 ∈ ℕ ((𝑔‘𝑛) ∖ ∪ 𝑙 ∈ (1..^𝑛)(𝑔‘𝑙)) = ∪ (𝑔 “ ℕ))
130	29	unieqd 4879	. . . . . . . . . . . . . . 15 ⊢ (𝑔:ℕ–onto→𝐴 → ∪ (𝑔 “ ℕ) = ∪ 𝐴)
131	129, 130	eqtrd 2795	. . . . . . . . . . . . . 14 ⊢ (𝑔:ℕ–onto→𝐴 → ∪ 𝑛 ∈ ℕ ((𝑔‘𝑛) ∖ ∪ 𝑙 ∈ (1..^𝑛)(𝑔‘𝑙)) = ∪ 𝐴)
132	131	fveq2d 6889	. . . . . . . . . . . . 13 ⊢ (𝑔:ℕ–onto→𝐴 → (vol‘∪ 𝑛 ∈ ℕ ((𝑔‘𝑛) ∖ ∪ 𝑙 ∈ (1..^𝑛)(𝑔‘𝑙))) = (vol‘∪ 𝐴))
133	132	adantr 486	. . . . . . . . . . . 12 ⊢ ((𝑔:ℕ–onto→𝐴 ∧ ∀𝑚 ∈ ℕ ((𝑔‘𝑚) ⊆ ℝ ∧ (vol*‘(𝑔‘𝑚)) = 0)) → (vol‘∪ 𝑛 ∈ ℕ ((𝑔‘𝑛) ∖ ∪ 𝑙 ∈ (1..^𝑛)(𝑔‘𝑙))) = (vol‘∪ 𝐴))
134	56	sseq1d 3939	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (𝑚 = 𝑛 → ((𝑔‘𝑚) ⊆ ℝ ↔ (𝑔‘𝑛) ⊆ ℝ))
135	56	fveqeq2d 6893	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (𝑚 = 𝑛 → ((vol*‘(𝑔‘𝑚)) = 0 ↔ (vol*‘(𝑔‘𝑛)) = 0))
136	134, 135	anbi12d 644	. . . . . . . . . . . . . . . . . . . 20 ⊢ (𝑚 = 𝑛 → (((𝑔‘𝑚) ⊆ ℝ ∧ (vol*‘(𝑔‘𝑚)) = 0) ↔ ((𝑔‘𝑛) ⊆ ℝ ∧ (vol*‘(𝑔‘𝑛)) = 0)))
137	136	rspccva 3575	. . . . . . . . . . . . . . . . . . 19 ⊢ ((∀𝑚 ∈ ℕ ((𝑔‘𝑚) ⊆ ℝ ∧ (vol*‘(𝑔‘𝑚)) = 0) ∧ 𝑛 ∈ ℕ) → ((𝑔‘𝑛) ⊆ ℝ ∧ (vol*‘(𝑔‘𝑛)) = 0))
138		ssdifss 4076	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ ((𝑔‘𝑛) ⊆ ℝ → ((𝑔‘𝑛) ∖ ∪ 𝑙 ∈ (1..^𝑛)(𝑔‘𝑙)) ⊆ ℝ)
139	138	adantr 486	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (((𝑔‘𝑛) ⊆ ℝ ∧ (vol*‘(𝑔‘𝑛)) = 0) → ((𝑔‘𝑛) ∖ ∪ 𝑙 ∈ (1..^𝑛)(𝑔‘𝑙)) ⊆ ℝ)
140		difss 4072	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ ((𝑔‘𝑛) ∖ ∪ 𝑙 ∈ (1..^𝑛)(𝑔‘𝑙)) ⊆ (𝑔‘𝑛)
141		ovolssnul 25808	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ ((((𝑔‘𝑛) ∖ ∪ 𝑙 ∈ (1..^𝑛)(𝑔‘𝑙)) ⊆ (𝑔‘𝑛) ∧ (𝑔‘𝑛) ⊆ ℝ ∧ (vol*‘(𝑔‘𝑛)) = 0) → (vol*‘((𝑔‘𝑛) ∖ ∪ 𝑙 ∈ (1..^𝑛)(𝑔‘𝑙))) = 0)
142	140, 141	mp3an1 1477	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (((𝑔‘𝑛) ⊆ ℝ ∧ (vol*‘(𝑔‘𝑛)) = 0) → (vol*‘((𝑔‘𝑛) ∖ ∪ 𝑙 ∈ (1..^𝑛)(𝑔‘𝑙))) = 0)
143	139, 142	jca 521	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (((𝑔‘𝑛) ⊆ ℝ ∧ (vol*‘(𝑔‘𝑛)) = 0) → (((𝑔‘𝑛) ∖ ∪ 𝑙 ∈ (1..^𝑛)(𝑔‘𝑙)) ⊆ ℝ ∧ (vol*‘((𝑔‘𝑛) ∖ ∪ 𝑙 ∈ (1..^𝑛)(𝑔‘𝑙))) = 0))
144		nulmbl 25856	. . . . . . . . . . . . . . . . . . . . 21 ⊢ ((((𝑔‘𝑛) ∖ ∪ 𝑙 ∈ (1..^𝑛)(𝑔‘𝑙)) ⊆ ℝ ∧ (vol*‘((𝑔‘𝑛) ∖ ∪ 𝑙 ∈ (1..^𝑛)(𝑔‘𝑙))) = 0) → ((𝑔‘𝑛) ∖ ∪ 𝑙 ∈ (1..^𝑛)(𝑔‘𝑙)) ∈ dom vol)
145		mblvol 25851	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (((𝑔‘𝑛) ∖ ∪ 𝑙 ∈ (1..^𝑛)(𝑔‘𝑙)) ∈ dom vol → (vol‘((𝑔‘𝑛) ∖ ∪ 𝑙 ∈ (1..^𝑛)(𝑔‘𝑙))) = (vol*‘((𝑔‘𝑛) ∖ ∪ 𝑙 ∈ (1..^𝑛)(𝑔‘𝑙))))
146	143, 144, 145	3syl 19	. . . . . . . . . . . . . . . . . . . 20 ⊢ (((𝑔‘𝑛) ⊆ ℝ ∧ (vol*‘(𝑔‘𝑛)) = 0) → (vol‘((𝑔‘𝑛) ∖ ∪ 𝑙 ∈ (1..^𝑛)(𝑔‘𝑙))) = (vol*‘((𝑔‘𝑛) ∖ ∪ 𝑙 ∈ (1..^𝑛)(𝑔‘𝑙))))
147	146, 142	eqtrd 2795	. . . . . . . . . . . . . . . . . . 19 ⊢ (((𝑔‘𝑛) ⊆ ℝ ∧ (vol*‘(𝑔‘𝑛)) = 0) → (vol‘((𝑔‘𝑛) ∖ ∪ 𝑙 ∈ (1..^𝑛)(𝑔‘𝑙))) = 0)
148	137, 147	syl 18	. . . . . . . . . . . . . . . . . 18 ⊢ ((∀𝑚 ∈ ℕ ((𝑔‘𝑚) ⊆ ℝ ∧ (vol*‘(𝑔‘𝑚)) = 0) ∧ 𝑛 ∈ ℕ) → (vol‘((𝑔‘𝑛) ∖ ∪ 𝑙 ∈ (1..^𝑛)(𝑔‘𝑙))) = 0)
149	148	mpteq2dva 5197	. . . . . . . . . . . . . . . . 17 ⊢ (∀𝑚 ∈ ℕ ((𝑔‘𝑚) ⊆ ℝ ∧ (vol*‘(𝑔‘𝑚)) = 0) → (𝑛 ∈ ℕ ↦ (vol‘((𝑔‘𝑛) ∖ ∪ 𝑙 ∈ (1..^𝑛)(𝑔‘𝑙)))) = (𝑛 ∈ ℕ ↦ 0))
150	149	seqeq3d 14152	. . . . . . . . . . . . . . . 16 ⊢ (∀𝑚 ∈ ℕ ((𝑔‘𝑚) ⊆ ℝ ∧ (vol*‘(𝑔‘𝑚)) = 0) → seq1( + , (𝑛 ∈ ℕ ↦ (vol‘((𝑔‘𝑛) ∖ ∪ 𝑙 ∈ (1..^𝑛)(𝑔‘𝑙))))) = seq1( + , (𝑛 ∈ ℕ ↦ 0)))
151	150	rneqd 5919	. . . . . . . . . . . . . . 15 ⊢ (∀𝑚 ∈ ℕ ((𝑔‘𝑚) ⊆ ℝ ∧ (vol*‘(𝑔‘𝑚)) = 0) → ran seq1( + , (𝑛 ∈ ℕ ↦ (vol‘((𝑔‘𝑛) ∖ ∪ 𝑙 ∈ (1..^𝑛)(𝑔‘𝑙))))) = ran seq1( + , (𝑛 ∈ ℕ ↦ 0)))
152	151	supeq1d 9438	. . . . . . . . . . . . . 14 ⊢ (∀𝑚 ∈ ℕ ((𝑔‘𝑚) ⊆ ℝ ∧ (vol*‘(𝑔‘𝑚)) = 0) → sup(ran seq1( + , (𝑛 ∈ ℕ ↦ (vol‘((𝑔‘𝑛) ∖ ∪ 𝑙 ∈ (1..^𝑛)(𝑔‘𝑙))))), ℝ*, < ) = sup(ran seq1( + , (𝑛 ∈ ℕ ↦ 0)), ℝ*, < ))
153		0cn 11298	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ 0 ∈ ℂ
154		ser1const 14201	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ ((0 ∈ ℂ ∧ 𝑚 ∈ ℕ) → (seq1( + , (ℕ × {0}))‘𝑚) = (𝑚 · 0))
155	153, 154	mpan 703	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (𝑚 ∈ ℕ → (seq1( + , (ℕ × {0}))‘𝑚) = (𝑚 · 0))
156		nncn 12343	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (𝑚 ∈ ℕ → 𝑚 ∈ ℂ)
157	156	mul01d 11509	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (𝑚 ∈ ℕ → (𝑚 · 0) = 0)
158	155, 157	eqtrd 2795	. . . . . . . . . . . . . . . . . . . 20 ⊢ (𝑚 ∈ ℕ → (seq1( + , (ℕ × {0}))‘𝑚) = 0)
159	158	mpteq2ia 5199	. . . . . . . . . . . . . . . . . . 19 ⊢ (𝑚 ∈ ℕ ↦ (seq1( + , (ℕ × {0}))‘𝑚)) = (𝑚 ∈ ℕ ↦ 0)
160		fconstmpt 5712	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (ℕ × {0}) = (𝑛 ∈ ℕ ↦ 0)
161		seqeq3 14149	. . . . . . . . . . . . . . . . . . . . 21 ⊢ ((ℕ × {0}) = (𝑛 ∈ ℕ ↦ 0) → seq1( + , (ℕ × {0})) = seq1( + , (𝑛 ∈ ℕ ↦ 0)))
162	160, 161	ax-mp 5	. . . . . . . . . . . . . . . . . . . 20 ⊢ seq1( + , (ℕ × {0})) = seq1( + , (𝑛 ∈ ℕ ↦ 0))
163		1z 12726	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ 1 ∈ ℤ
164		seqfn 14156	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (1 ∈ ℤ → seq1( + , (ℕ × {0})) Fn (ℤ≥‘1))
165	163, 164	ax-mp 5	. . . . . . . . . . . . . . . . . . . . 21 ⊢ seq1( + , (ℕ × {0})) Fn (ℤ≥‘1)
166		nnuz 13004	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ ℕ = (ℤ≥‘1)
167	166	fneq2i 6637	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (seq1( + , (ℕ × {0})) Fn ℕ ↔ seq1( + , (ℕ × {0})) Fn (ℤ≥‘1))
168		dffn5 6943	. . . . . . . . . . . . . . . . . . . . . 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 2785	. . . . . . . . . . . . . . . . . . 19 ⊢ seq1( + , (𝑛 ∈ ℕ ↦ 0)) = (𝑚 ∈ ℕ ↦ (seq1( + , (ℕ × {0}))‘𝑚))
172		fconstmpt 5712	. . . . . . . . . . . . . . . . . . 19 ⊢ (ℕ × {0}) = (𝑚 ∈ ℕ ↦ 0)
173	159, 171, 172	3eqtr4i 2793	. . . . . . . . . . . . . . . . . 18 ⊢ seq1( + , (𝑛 ∈ ℕ ↦ 0)) = (ℕ × {0})
174	173	rneqi 5918	. . . . . . . . . . . . . . . . 17 ⊢ ran seq1( + , (𝑛 ∈ ℕ ↦ 0)) = ran (ℕ × {0})
175		1nn 12346	. . . . . . . . . . . . . . . . . 18 ⊢ 1 ∈ ℕ
176		ne0i 4286	. . . . . . . . . . . . . . . . . 18 ⊢ (1 ∈ ℕ → ℕ ≠ ∅)
177		rnxp 6161	. . . . . . . . . . . . . . . . . 18 ⊢ (ℕ ≠ ∅ → ran (ℕ × {0}) = {0})
178	175, 176, 177	mp2b 10	. . . . . . . . . . . . . . . . 17 ⊢ ran (ℕ × {0}) = {0}
179	174, 178	eqtri 2783	. . . . . . . . . . . . . . . 16 ⊢ ran seq1( + , (𝑛 ∈ ℕ ↦ 0)) = {0}
180	179	supeq1i 9439	. . . . . . . . . . . . . . 15 ⊢ sup(ran seq1( + , (𝑛 ∈ ℕ ↦ 0)), ℝ*, < ) = sup({0}, ℝ*, < )
181		xrltso 13270	. . . . . . . . . . . . . . . 16 ⊢ < Or ℝ*
182		0xr 11356	. . . . . . . . . . . . . . . 16 ⊢ 0 ∈ ℝ*
183		supsn 9465	. . . . . . . . . . . . . . . 16 ⊢ (( < Or ℝ* ∧ 0 ∈ ℝ*) → sup({0}, ℝ*, < ) = 0)
184	181, 182, 183	mp2an 705	. . . . . . . . . . . . . . 15 ⊢ sup({0}, ℝ*, < ) = 0
185	180, 184	eqtri 2783	. . . . . . . . . . . . . 14 ⊢ sup(ran seq1( + , (𝑛 ∈ ℕ ↦ 0)), ℝ*, < ) = 0
186	152, 185	eqtrdi 2811	. . . . . . . . . . . . 13 ⊢ (∀𝑚 ∈ ℕ ((𝑔‘𝑚) ⊆ ℝ ∧ (vol*‘(𝑔‘𝑚)) = 0) → sup(ran seq1( + , (𝑛 ∈ ℕ ↦ (vol‘((𝑔‘𝑛) ∖ ∪ 𝑙 ∈ (1..^𝑛)(𝑔‘𝑙))))), ℝ*, < ) = 0)
187	186	adantl 487	. . . . . . . . . . . 12 ⊢ ((𝑔:ℕ–onto→𝐴 ∧ ∀𝑚 ∈ ℕ ((𝑔‘𝑚) ⊆ ℝ ∧ (vol*‘(𝑔‘𝑚)) = 0)) → sup(ran seq1( + , (𝑛 ∈ ℕ ↦ (vol‘((𝑔‘𝑛) ∖ ∪ 𝑙 ∈ (1..^𝑛)(𝑔‘𝑙))))), ℝ*, < ) = 0)
188	124, 133, 187	3eqtr3rd 2804	. . . . . . . . . . 11 ⊢ ((𝑔:ℕ–onto→𝐴 ∧ ∀𝑚 ∈ ℕ ((𝑔‘𝑚) ⊆ ℝ ∧ (vol*‘(𝑔‘𝑚)) = 0)) → 0 = (vol‘∪ 𝐴))
189	188	ex 418	. . . . . . . . . 10 ⊢ (𝑔:ℕ–onto→𝐴 → (∀𝑚 ∈ ℕ ((𝑔‘𝑚) ⊆ ℝ ∧ (vol*‘(𝑔‘𝑚)) = 0) → 0 = (vol‘∪ 𝐴)))
190	38, 189	sylbid 243	. . . . . . . . 9 ⊢ (𝑔:ℕ–onto→𝐴 → (∀𝑥 ∈ 𝐴 (𝑥 ⊆ ℝ ∧ (vol*‘𝑥) = 0) → 0 = (vol‘∪ 𝐴)))
191	28, 190	syl5 35	. . . . . . . 8 ⊢ (𝑔:ℕ–onto→𝐴 → ((∀𝑥 ∈ 𝐴 𝑥 ≼ ℕ ∧ ∪ 𝐴 ⊆ ℝ) → 0 = (vol‘∪ 𝐴)))
192	191	exlimiv 1962	. . . . . . 7 ⊢ (∃𝑔 𝑔:ℕ–onto→𝐴 → ((∀𝑥 ∈ 𝐴 𝑥 ≼ ℕ ∧ ∪ 𝐴 ⊆ ℝ) → 0 = (vol‘∪ 𝐴)))
193	18, 192	syl 18	. . . . . 6 ⊢ ((𝐴 ≠ ∅ ∧ 𝐴 ≼ ℕ) → ((∀𝑥 ∈ 𝐴 𝑥 ≼ ℕ ∧ ∪ 𝐴 ⊆ ℝ) → 0 = (vol‘∪ 𝐴)))
194	193	expimpd 459	. . . . 5 ⊢ (𝐴 ≠ ∅ → ((𝐴 ≼ ℕ ∧ (∀𝑥 ∈ 𝐴 𝑥 ≼ ℕ ∧ ∪ 𝐴 ⊆ ℝ)) → 0 = (vol‘∪ 𝐴)))
195	11, 194	pm2.61ine 3038	. . . 4 ⊢ ((𝐴 ≼ ℕ ∧ (∀𝑥 ∈ 𝐴 𝑥 ≼ ℕ ∧ ∪ 𝐴 ⊆ ℝ)) → 0 = (vol‘∪ 𝐴))
196		renepnf 11357	. . . . . . 7 ⊢ (0 ∈ ℝ → 0 ≠ +∞)
197	47, 196	mp1i 14	. . . . . 6 ⊢ (∪ 𝐴 = ℝ → 0 ≠ +∞)
198		fveq2 6885	. . . . . . 7 ⊢ (∪ 𝐴 = ℝ → (vol‘∪ 𝐴) = (vol‘ℝ))
199		rembl 25861	. . . . . . . . 9 ⊢ ℝ ∈ dom vol
200		mblvol 25851	. . . . . . . . 9 ⊢ (ℝ ∈ dom vol → (vol‘ℝ) = (vol*‘ℝ))
201	199, 200	ax-mp 5	. . . . . . . 8 ⊢ (vol‘ℝ) = (vol*‘ℝ)
202		ovolre 25846	. . . . . . . 8 ⊢ (vol*‘ℝ) = +∞
203	201, 202	eqtri 2783	. . . . . . 7 ⊢ (vol‘ℝ) = +∞
204	198, 203	eqtrdi 2811	. . . . . 6 ⊢ (∪ 𝐴 = ℝ → (vol‘∪ 𝐴) = +∞)
205	197, 204	neeqtrrd 3029	. . . . 5 ⊢ (∪ 𝐴 = ℝ → 0 ≠ (vol‘∪ 𝐴))
206	205	necon2i 2989	. . . 4 ⊢ (0 = (vol‘∪ 𝐴) → ∪ 𝐴 ≠ ℝ)
207	195, 206	syl 18	. . 3 ⊢ ((𝐴 ≼ ℕ ∧ (∀𝑥 ∈ 𝐴 𝑥 ≼ ℕ ∧ ∪ 𝐴 ⊆ ℝ)) → ∪ 𝐴 ≠ ℝ)
208	207	expr 462	. 2 ⊢ ((𝐴 ≼ ℕ ∧ ∀𝑥 ∈ 𝐴 𝑥 ≼ ℕ) → (∪ 𝐴 ⊆ ℝ → ∪ 𝐴 ≠ ℝ))
209		eqimss 3966	. . 3 ⊢ (∪ 𝐴 = ℝ → ∪ 𝐴 ⊆ ℝ)
210	209	necon3bi 2981	. 2 ⊢ (¬ ∪ 𝐴 ⊆ ℝ → ∪ 𝐴 ≠ ℝ)
211	208, 210	pm2.61d1 182	1 ⊢ ((𝐴 ≼ ℕ ∧ ∀𝑥 ∈ 𝐴 𝑥 ≼ ℕ) → ∪ 𝐴 ≠ ℝ)

This proof depends on syntax axioms:   → wi 4   ↔ wb 209   ∧ wa 401   = wceq 1569  ∃wex 1811   ∈ wcel 2144   ≠ wne 2955  ∀wral 3076  Vcvv 3450   ⊆ wss 3895   ∖ cdif 4045  ∅c0 4278  {csn 4583  ∪ cuni 4866  ∪ ciun 4950  Disj wdisj 5069   class class class wbr 5102   ↦ cmpt 5185   Or wor 5557   × cxp 5648  dom cdm 5650  ran crn 5651   “ cima 5653  Fun wfun 6532   Fn wfn 6533  –onto→wfo 6536  ‘cfv 6538  (class class class)co 7420   ≼ cdom 8971   ≺ csdm 8972  supcsup 9432  ℂcc 11198  ℝcr 11199  0cc0 11200  1c1 11201   + caddc 11203   · cmul 11205  +∞cpnf 11340  ℝ^*cxr 11342   < clt 11343  ℕcn 12335  ℤcz 12693  ℤ_≥cuz 12965  ..^cfzo 13788  seqcseq 14144  vol*covol 25783  volcvol 25784

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1827  ax-4 1841  ax-5 1942  ax-6 1999  ax-7 2040  ax-8 2146  ax-9 2154  ax-10 2177  ax-11 2193  ax-12 2212  ax-ext 2732  ax-rep 5231  ax-sep 5248  ax-nul 5259  ax-pow 5326  ax-pr 5390  ax-un 7751  ax-inf2 9642  ax-cnex 11256  ax-resscn 11257  ax-1cn 11258  ax-icn 11259  ax-addcl 11260  ax-addrcl 11261  ax-mulcl 11262  ax-mulrcl 11263  ax-mulcom 11264  ax-addass 11265  ax-mulass 11266  ax-distr 11267  ax-i2m1 11268  ax-1ne0 11269  ax-1rid 11270  ax-rnegex 11271  ax-rrecex 11272  ax-cnre 11273  ax-pre-lttri 11274  ax-pre-lttrn 11275  ax-pre-ltadd 11276  ax-pre-mulgt0 11277  ax-pre-sup 11278

This proof depends on definitions:  df-bi 210  df-an 402  df-or 862  df-3or 1104  df-3an 1105  df-tru 1572  df-fal 1582  df-ex 1812  df-nf 1816  df-sb 2099  df-mo 2564  df-eu 2594  df-clab 2739  df-cleq 2752  df-clel 2835  df-nfc 2909  df-ne 2956  df-nel 3062  df-ral 3077  df-rex 3087  df-rmo 3365  df-reu 3366  df-rab 3413  df-v 3452  df-sbc 3739  df-csb 3847  df-ss 3896  df-pss 4014  df-dif 4047  df-in 4091  df-un 4151  df-nul 4279  df-if 4482  df-pw 4558  df-sn 4584  df-pr 4586  df-op 4590  df-uni 4867  df-int 4907  df-iun 4952  df-disj 5070  df-br 5103  df-opab 5167  df-mpt 5186  df-tr 5212  df-id 5545  df-eprel 5550  df-po 5558  df-so 5559  df-fr 5603  df-se 5604  df-we 5605  df-xp 5656  df-rel 5657  df-cnv 5658  df-co 5659  df-dm 5660  df-rn 5661  df-res 5662  df-ima 5663  df-pred 6304  df-ord 6365  df-on 6366  df-lim 6367  df-suc 6368  df-iota 6494  df-fun 6540  df-fn 6541  df-f 6542  df-f1 6543  df-fo 6544  df-f1o 6545  df-fv 6546  df-isom 6547  df-riota 7377  df-ov 7423  df-oprab 7424  df-mpo 7425  df-of 7693  df-om 7878  df-1st 8001  df-2nd 8002  df-frecs 8299  df-wrecs 8330  df-recs 8379  df-rdg 8418  df-1o 8476  df-2o 8477  df-er 8717  df-map 8849  df-en 8974  df-dom 8975  df-sdom 8976  df-fin 8977  df-fi 9403  df-sup 9434  df-inf 9435  df-oi 9504  df-dju 9982  df-card 10020  df-pnf 11345  df-mnf 11346  df-xr 11347  df-ltxr 11348  df-le 11349  df-sub 11543  df-neg 11544  df-div 11974  df-nn 12336  df-2 12405  df-3 12406  df-n0 12607  df-z 12694  df-uz 12966  df-q 13076  df-rp 13121  df-xneg 13241  df-xadd 13242  df-xmul 13243  df-ioo 13480  df-ico 13482  df-icc 13483  df-fz 13640  df-fzo 13789  df-fl 13932  df-seq 14145  df-exp 14205  df-hash 14475  df-cj 15266  df-re 15267  df-im 15268  df-sqrt 15402  df-abs 15403  df-clim 15655  df-sum 15854  df-rest 17593  df-topgen 17614  df-psmet 21670  df-xmet 21671  df-met 21672  df-bl 21673  df-mopn 21674  df-top 23212  df-topon 23229  df-bases 23264  df-cmp 23705  df-ovol 25785  df-vol 25786

This theorem is used by: (None)