Theorem volsupnfl 34411

Description: volsup 23876 is incompatible with the Feferman-Levy model. (Contributed by Brendan Leahy, 2-Jan-2018.)

Hypothesis

Ref	Expression
volsupnfl.0	⊢ ((𝑓:ℕ⟶dom vol ∧ ∀𝑛 ∈ ℕ (𝑓‘𝑛) ⊆ (𝑓‘(𝑛 + 1))) → (vol‘∪ ran 𝑓) = sup((vol “ ran 𝑓), ℝ*, < ))

Assertion

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

Distinct variable group:   𝑓,𝑛,𝑥,𝐴

Proof of Theorem volsupnfl

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

Step	Hyp	Ref	Expression
1		unieq 4717	. . . . . . . . 9 ⊢ (𝐴 = ∅ → ∪ 𝐴 = ∪ ∅)
2		uni0 4736	. . . . . . . . 9 ⊢ ∪ ∅ = ∅
3	1, 2	syl6eq 2825	. . . . . . . 8 ⊢ (𝐴 = ∅ → ∪ 𝐴 = ∅)
4	3	fveq2d 6501	. . . . . . 7 ⊢ (𝐴 = ∅ → (vol‘∪ 𝐴) = (vol‘∅))
5		0mbl 23859	. . . . . . . . 9 ⊢ ∅ ∈ dom vol
6		mblvol 23850	. . . . . . . . 9 ⊢ (∅ ∈ dom vol → (vol‘∅) = (vol*‘∅))
7	5, 6	ax-mp 5	. . . . . . . 8 ⊢ (vol‘∅) = (vol*‘∅)
8		ovol0 23813	. . . . . . . 8 ⊢ (vol*‘∅) = 0
9	7, 8	eqtri 2797	. . . . . . 7 ⊢ (vol‘∅) = 0
10	4, 9	syl6req 2826	. . . . . 6 ⊢ (𝐴 = ∅ → 0 = (vol‘∪ 𝐴))
11	10	a1d 25	. . . . 5 ⊢ (𝐴 = ∅ → ((𝐴 ≼ ℕ ∧ (∀𝑥 ∈ 𝐴 𝑥 ≼ ℕ ∧ ∪ 𝐴 ⊆ ℝ)) → 0 = (vol‘∪ 𝐴)))
12		reldom 8311	. . . . . . . . . . 11 ⊢ Rel ≼
13	12	brrelex1i 5455	. . . . . . . . . 10 ⊢ (𝐴 ≼ ℕ → 𝐴 ∈ V)
14		0sdomg 8441	. . . . . . . . . 10 ⊢ (𝐴 ∈ V → (∅ ≺ 𝐴 ↔ 𝐴 ≠ ∅))
15	13, 14	syl 17	. . . . . . . . 9 ⊢ (𝐴 ≼ ℕ → (∅ ≺ 𝐴 ↔ 𝐴 ≠ ∅))
16	15	biimparc 472	. . . . . . . 8 ⊢ ((𝐴 ≠ ∅ ∧ 𝐴 ≼ ℕ) → ∅ ≺ 𝐴)
17		fodomr 8463	. . . . . . . 8 ⊢ ((∅ ≺ 𝐴 ∧ 𝐴 ≼ ℕ) → ∃𝑔 𝑔:ℕ–onto→𝐴)
18	16, 17	sylancom 580	. . . . . . 7 ⊢ ((𝐴 ≠ ∅ ∧ 𝐴 ≼ ℕ) → ∃𝑔 𝑔:ℕ–onto→𝐴)
19		unissb 4740	. . . . . . . . . . . . 13 ⊢ (∪ 𝐴 ⊆ ℝ ↔ ∀𝑥 ∈ 𝐴 𝑥 ⊆ ℝ)
20	19	anbi1i 615	. . . . . . . . . . . 12 ⊢ ((∪ 𝐴 ⊆ ℝ ∧ ∀𝑥 ∈ 𝐴 𝑥 ≼ ℕ) ↔ (∀𝑥 ∈ 𝐴 𝑥 ⊆ ℝ ∧ ∀𝑥 ∈ 𝐴 𝑥 ≼ ℕ))
21		r19.26 3115	. . . . . . . . . . . 12 ⊢ (∀𝑥 ∈ 𝐴 (𝑥 ⊆ ℝ ∧ 𝑥 ≼ ℕ) ↔ (∀𝑥 ∈ 𝐴 𝑥 ⊆ ℝ ∧ ∀𝑥 ∈ 𝐴 𝑥 ≼ ℕ))
22	20, 21	bitr4i 270	. . . . . . . . . . 11 ⊢ ((∪ 𝐴 ⊆ ℝ ∧ ∀𝑥 ∈ 𝐴 𝑥 ≼ ℕ) ↔ ∀𝑥 ∈ 𝐴 (𝑥 ⊆ ℝ ∧ 𝑥 ≼ ℕ))
23		ovolctb2 23812	. . . . . . . . . . . . 13 ⊢ ((𝑥 ⊆ ℝ ∧ 𝑥 ≼ ℕ) → (vol*‘𝑥) = 0)
24		nulmbl 23855	. . . . . . . . . . . . . 14 ⊢ ((𝑥 ⊆ ℝ ∧ (vol*‘𝑥) = 0) → 𝑥 ∈ dom vol)
25		mblvol 23850	. . . . . . . . . . . . . . . 16 ⊢ (𝑥 ∈ dom vol → (vol‘𝑥) = (vol*‘𝑥))
26		eqtr 2794	. . . . . . . . . . . . . . . . 17 ⊢ (((vol‘𝑥) = (vol*‘𝑥) ∧ (vol*‘𝑥) = 0) → (vol‘𝑥) = 0)
27	26	expcom 406	. . . . . . . . . . . . . . . 16 ⊢ ((vol*‘𝑥) = 0 → ((vol‘𝑥) = (vol*‘𝑥) → (vol‘𝑥) = 0))
28	25, 27	syl5 34	. . . . . . . . . . . . . . 15 ⊢ ((vol*‘𝑥) = 0 → (𝑥 ∈ dom vol → (vol‘𝑥) = 0))
29	28	adantl 474	. . . . . . . . . . . . . 14 ⊢ ((𝑥 ⊆ ℝ ∧ (vol*‘𝑥) = 0) → (𝑥 ∈ dom vol → (vol‘𝑥) = 0))
30	24, 29	jcai 509	. . . . . . . . . . . . 13 ⊢ ((𝑥 ⊆ ℝ ∧ (vol*‘𝑥) = 0) → (𝑥 ∈ dom vol ∧ (vol‘𝑥) = 0))
31	23, 30	syldan 583	. . . . . . . . . . . 12 ⊢ ((𝑥 ⊆ ℝ ∧ 𝑥 ≼ ℕ) → (𝑥 ∈ dom vol ∧ (vol‘𝑥) = 0))
32	31	ralimi 3105	. . . . . . . . . . 11 ⊢ (∀𝑥 ∈ 𝐴 (𝑥 ⊆ ℝ ∧ 𝑥 ≼ ℕ) → ∀𝑥 ∈ 𝐴 (𝑥 ∈ dom vol ∧ (vol‘𝑥) = 0))
33	22, 32	sylbi 209	. . . . . . . . . 10 ⊢ ((∪ 𝐴 ⊆ ℝ ∧ ∀𝑥 ∈ 𝐴 𝑥 ≼ ℕ) → ∀𝑥 ∈ 𝐴 (𝑥 ∈ dom vol ∧ (vol‘𝑥) = 0))
34	33	ancoms 451	. . . . . . . . 9 ⊢ ((∀𝑥 ∈ 𝐴 𝑥 ≼ ℕ ∧ ∪ 𝐴 ⊆ ℝ) → ∀𝑥 ∈ 𝐴 (𝑥 ∈ dom vol ∧ (vol‘𝑥) = 0))
35		fzfi 13154	. . . . . . . . . . . . . . 15 ⊢ (1...𝑚) ∈ Fin
36		fzssuz 12763	. . . . . . . . . . . . . . . . 17 ⊢ (1...𝑚) ⊆ (ℤ≥‘1)
37		nnuz 12094	. . . . . . . . . . . . . . . . 17 ⊢ ℕ = (ℤ≥‘1)
38	36, 37	sseqtr4i 3889	. . . . . . . . . . . . . . . 16 ⊢ (1...𝑚) ⊆ ℕ
39		fof 6417	. . . . . . . . . . . . . . . . . . . 20 ⊢ (𝑔:ℕ–onto→𝐴 → 𝑔:ℕ⟶𝐴)
40	39	ffvelrnda 6675	. . . . . . . . . . . . . . . . . . 19 ⊢ ((𝑔:ℕ–onto→𝐴 ∧ 𝑙 ∈ ℕ) → (𝑔‘𝑙) ∈ 𝐴)
41		eleq1 2848	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ (𝑥 = (𝑔‘𝑙) → (𝑥 ∈ dom vol ↔ (𝑔‘𝑙) ∈ dom vol))
42		fveqeq2 6506	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ (𝑥 = (𝑔‘𝑙) → ((vol‘𝑥) = 0 ↔ (vol‘(𝑔‘𝑙)) = 0))
43	41, 42	anbi12d 622	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (𝑥 = (𝑔‘𝑙) → ((𝑥 ∈ dom vol ∧ (vol‘𝑥) = 0) ↔ ((𝑔‘𝑙) ∈ dom vol ∧ (vol‘(𝑔‘𝑙)) = 0)))
44	43	rspccva 3529	. . . . . . . . . . . . . . . . . . . . 21 ⊢ ((∀𝑥 ∈ 𝐴 (𝑥 ∈ dom vol ∧ (vol‘𝑥) = 0) ∧ (𝑔‘𝑙) ∈ 𝐴) → ((𝑔‘𝑙) ∈ dom vol ∧ (vol‘(𝑔‘𝑙)) = 0))
45	44	simpld 487	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((∀𝑥 ∈ 𝐴 (𝑥 ∈ dom vol ∧ (vol‘𝑥) = 0) ∧ (𝑔‘𝑙) ∈ 𝐴) → (𝑔‘𝑙) ∈ dom vol)
46	45	ancoms 451	. . . . . . . . . . . . . . . . . . 19 ⊢ (((𝑔‘𝑙) ∈ 𝐴 ∧ ∀𝑥 ∈ 𝐴 (𝑥 ∈ dom vol ∧ (vol‘𝑥) = 0)) → (𝑔‘𝑙) ∈ dom vol)
47	40, 46	sylan 572	. . . . . . . . . . . . . . . . . 18 ⊢ (((𝑔:ℕ–onto→𝐴 ∧ 𝑙 ∈ ℕ) ∧ ∀𝑥 ∈ 𝐴 (𝑥 ∈ dom vol ∧ (vol‘𝑥) = 0)) → (𝑔‘𝑙) ∈ dom vol)
48	47	an32s 640	. . . . . . . . . . . . . . . . 17 ⊢ (((𝑔:ℕ–onto→𝐴 ∧ ∀𝑥 ∈ 𝐴 (𝑥 ∈ dom vol ∧ (vol‘𝑥) = 0)) ∧ 𝑙 ∈ ℕ) → (𝑔‘𝑙) ∈ dom vol)
49	48	ralrimiva 3127	. . . . . . . . . . . . . . . 16 ⊢ ((𝑔:ℕ–onto→𝐴 ∧ ∀𝑥 ∈ 𝐴 (𝑥 ∈ dom vol ∧ (vol‘𝑥) = 0)) → ∀𝑙 ∈ ℕ (𝑔‘𝑙) ∈ dom vol)
50		ssralv 3918	. . . . . . . . . . . . . . . 16 ⊢ ((1...𝑚) ⊆ ℕ → (∀𝑙 ∈ ℕ (𝑔‘𝑙) ∈ dom vol → ∀𝑙 ∈ (1...𝑚)(𝑔‘𝑙) ∈ dom vol))
51	38, 49, 50	mpsyl 68	. . . . . . . . . . . . . . 15 ⊢ ((𝑔:ℕ–onto→𝐴 ∧ ∀𝑥 ∈ 𝐴 (𝑥 ∈ dom vol ∧ (vol‘𝑥) = 0)) → ∀𝑙 ∈ (1...𝑚)(𝑔‘𝑙) ∈ dom vol)
52		finiunmbl 23864	. . . . . . . . . . . . . . 15 ⊢ (((1...𝑚) ∈ Fin ∧ ∀𝑙 ∈ (1...𝑚)(𝑔‘𝑙) ∈ dom vol) → ∪ 𝑙 ∈ (1...𝑚)(𝑔‘𝑙) ∈ dom vol)
53	35, 51, 52	sylancr 579	. . . . . . . . . . . . . 14 ⊢ ((𝑔:ℕ–onto→𝐴 ∧ ∀𝑥 ∈ 𝐴 (𝑥 ∈ dom vol ∧ (vol‘𝑥) = 0)) → ∪ 𝑙 ∈ (1...𝑚)(𝑔‘𝑙) ∈ dom vol)
54	53	adantr 473	. . . . . . . . . . . . 13 ⊢ (((𝑔:ℕ–onto→𝐴 ∧ ∀𝑥 ∈ 𝐴 (𝑥 ∈ dom vol ∧ (vol‘𝑥) = 0)) ∧ 𝑚 ∈ ℕ) → ∪ 𝑙 ∈ (1...𝑚)(𝑔‘𝑙) ∈ dom vol)
55	54	fmpttd 6701	. . . . . . . . . . . 12 ⊢ ((𝑔:ℕ–onto→𝐴 ∧ ∀𝑥 ∈ 𝐴 (𝑥 ∈ dom vol ∧ (vol‘𝑥) = 0)) → (𝑚 ∈ ℕ ↦ ∪ 𝑙 ∈ (1...𝑚)(𝑔‘𝑙)):ℕ⟶dom vol)
56		fzssp1 12765	. . . . . . . . . . . . . . 15 ⊢ (1...𝑛) ⊆ (1...(𝑛 + 1))
57		iunss1 4802	. . . . . . . . . . . . . . 15 ⊢ ((1...𝑛) ⊆ (1...(𝑛 + 1)) → ∪ 𝑙 ∈ (1...𝑛)(𝑔‘𝑙) ⊆ ∪ 𝑙 ∈ (1...(𝑛 + 1))(𝑔‘𝑙))
58	56, 57	ax-mp 5	. . . . . . . . . . . . . 14 ⊢ ∪ 𝑙 ∈ (1...𝑛)(𝑔‘𝑙) ⊆ ∪ 𝑙 ∈ (1...(𝑛 + 1))(𝑔‘𝑙)
59		oveq2 6983	. . . . . . . . . . . . . . . . 17 ⊢ (𝑚 = 𝑛 → (1...𝑚) = (1...𝑛))
60	59	iuneq1d 4815	. . . . . . . . . . . . . . . 16 ⊢ (𝑚 = 𝑛 → ∪ 𝑙 ∈ (1...𝑚)(𝑔‘𝑙) = ∪ 𝑙 ∈ (1...𝑛)(𝑔‘𝑙))
61		eqid 2773	. . . . . . . . . . . . . . . 16 ⊢ (𝑚 ∈ ℕ ↦ ∪ 𝑙 ∈ (1...𝑚)(𝑔‘𝑙)) = (𝑚 ∈ ℕ ↦ ∪ 𝑙 ∈ (1...𝑚)(𝑔‘𝑙))
62		ovex 7007	. . . . . . . . . . . . . . . . 17 ⊢ (1...𝑛) ∈ V
63		fvex 6510	. . . . . . . . . . . . . . . . 17 ⊢ (𝑔‘𝑙) ∈ V
64	62, 63	iunex 7480	. . . . . . . . . . . . . . . 16 ⊢ ∪ 𝑙 ∈ (1...𝑛)(𝑔‘𝑙) ∈ V
65	60, 61, 64	fvmpt 6594	. . . . . . . . . . . . . . 15 ⊢ (𝑛 ∈ ℕ → ((𝑚 ∈ ℕ ↦ ∪ 𝑙 ∈ (1...𝑚)(𝑔‘𝑙))‘𝑛) = ∪ 𝑙 ∈ (1...𝑛)(𝑔‘𝑙))
66		peano2nn 11452	. . . . . . . . . . . . . . . 16 ⊢ (𝑛 ∈ ℕ → (𝑛 + 1) ∈ ℕ)
67		oveq2 6983	. . . . . . . . . . . . . . . . . 18 ⊢ (𝑚 = (𝑛 + 1) → (1...𝑚) = (1...(𝑛 + 1)))
68	67	iuneq1d 4815	. . . . . . . . . . . . . . . . 17 ⊢ (𝑚 = (𝑛 + 1) → ∪ 𝑙 ∈ (1...𝑚)(𝑔‘𝑙) = ∪ 𝑙 ∈ (1...(𝑛 + 1))(𝑔‘𝑙))
69		ovex 7007	. . . . . . . . . . . . . . . . . 18 ⊢ (1...(𝑛 + 1)) ∈ V
70	69, 63	iunex 7480	. . . . . . . . . . . . . . . . 17 ⊢ ∪ 𝑙 ∈ (1...(𝑛 + 1))(𝑔‘𝑙) ∈ V
71	68, 61, 70	fvmpt 6594	. . . . . . . . . . . . . . . 16 ⊢ ((𝑛 + 1) ∈ ℕ → ((𝑚 ∈ ℕ ↦ ∪ 𝑙 ∈ (1...𝑚)(𝑔‘𝑙))‘(𝑛 + 1)) = ∪ 𝑙 ∈ (1...(𝑛 + 1))(𝑔‘𝑙))
72	66, 71	syl 17	. . . . . . . . . . . . . . 15 ⊢ (𝑛 ∈ ℕ → ((𝑚 ∈ ℕ ↦ ∪ 𝑙 ∈ (1...𝑚)(𝑔‘𝑙))‘(𝑛 + 1)) = ∪ 𝑙 ∈ (1...(𝑛 + 1))(𝑔‘𝑙))
73	65, 72	sseq12d 3885	. . . . . . . . . . . . . 14 ⊢ (𝑛 ∈ ℕ → (((𝑚 ∈ ℕ ↦ ∪ 𝑙 ∈ (1...𝑚)(𝑔‘𝑙))‘𝑛) ⊆ ((𝑚 ∈ ℕ ↦ ∪ 𝑙 ∈ (1...𝑚)(𝑔‘𝑙))‘(𝑛 + 1)) ↔ ∪ 𝑙 ∈ (1...𝑛)(𝑔‘𝑙) ⊆ ∪ 𝑙 ∈ (1...(𝑛 + 1))(𝑔‘𝑙)))
74	58, 73	mpbiri 250	. . . . . . . . . . . . 13 ⊢ (𝑛 ∈ ℕ → ((𝑚 ∈ ℕ ↦ ∪ 𝑙 ∈ (1...𝑚)(𝑔‘𝑙))‘𝑛) ⊆ ((𝑚 ∈ ℕ ↦ ∪ 𝑙 ∈ (1...𝑚)(𝑔‘𝑙))‘(𝑛 + 1)))
75	74	rgen 3093	. . . . . . . . . . . 12 ⊢ ∀𝑛 ∈ ℕ ((𝑚 ∈ ℕ ↦ ∪ 𝑙 ∈ (1...𝑚)(𝑔‘𝑙))‘𝑛) ⊆ ((𝑚 ∈ ℕ ↦ ∪ 𝑙 ∈ (1...𝑚)(𝑔‘𝑙))‘(𝑛 + 1))
76		nnex 11445	. . . . . . . . . . . . . 14 ⊢ ℕ ∈ V
77	76	mptex 6811	. . . . . . . . . . . . 13 ⊢ (𝑚 ∈ ℕ ↦ ∪ 𝑙 ∈ (1...𝑚)(𝑔‘𝑙)) ∈ V
78		feq1 6323	. . . . . . . . . . . . . . 15 ⊢ (𝑓 = (𝑚 ∈ ℕ ↦ ∪ 𝑙 ∈ (1...𝑚)(𝑔‘𝑙)) → (𝑓:ℕ⟶dom vol ↔ (𝑚 ∈ ℕ ↦ ∪ 𝑙 ∈ (1...𝑚)(𝑔‘𝑙)):ℕ⟶dom vol))
79		fveq1 6496	. . . . . . . . . . . . . . . . 17 ⊢ (𝑓 = (𝑚 ∈ ℕ ↦ ∪ 𝑙 ∈ (1...𝑚)(𝑔‘𝑙)) → (𝑓‘𝑛) = ((𝑚 ∈ ℕ ↦ ∪ 𝑙 ∈ (1...𝑚)(𝑔‘𝑙))‘𝑛))
80		fveq1 6496	. . . . . . . . . . . . . . . . 17 ⊢ (𝑓 = (𝑚 ∈ ℕ ↦ ∪ 𝑙 ∈ (1...𝑚)(𝑔‘𝑙)) → (𝑓‘(𝑛 + 1)) = ((𝑚 ∈ ℕ ↦ ∪ 𝑙 ∈ (1...𝑚)(𝑔‘𝑙))‘(𝑛 + 1)))
81	79, 80	sseq12d 3885	. . . . . . . . . . . . . . . 16 ⊢ (𝑓 = (𝑚 ∈ ℕ ↦ ∪ 𝑙 ∈ (1...𝑚)(𝑔‘𝑙)) → ((𝑓‘𝑛) ⊆ (𝑓‘(𝑛 + 1)) ↔ ((𝑚 ∈ ℕ ↦ ∪ 𝑙 ∈ (1...𝑚)(𝑔‘𝑙))‘𝑛) ⊆ ((𝑚 ∈ ℕ ↦ ∪ 𝑙 ∈ (1...𝑚)(𝑔‘𝑙))‘(𝑛 + 1))))
82	81	ralbidv 3142	. . . . . . . . . . . . . . 15 ⊢ (𝑓 = (𝑚 ∈ ℕ ↦ ∪ 𝑙 ∈ (1...𝑚)(𝑔‘𝑙)) → (∀𝑛 ∈ ℕ (𝑓‘𝑛) ⊆ (𝑓‘(𝑛 + 1)) ↔ ∀𝑛 ∈ ℕ ((𝑚 ∈ ℕ ↦ ∪ 𝑙 ∈ (1...𝑚)(𝑔‘𝑙))‘𝑛) ⊆ ((𝑚 ∈ ℕ ↦ ∪ 𝑙 ∈ (1...𝑚)(𝑔‘𝑙))‘(𝑛 + 1))))
83	78, 82	anbi12d 622	. . . . . . . . . . . . . 14 ⊢ (𝑓 = (𝑚 ∈ ℕ ↦ ∪ 𝑙 ∈ (1...𝑚)(𝑔‘𝑙)) → ((𝑓:ℕ⟶dom vol ∧ ∀𝑛 ∈ ℕ (𝑓‘𝑛) ⊆ (𝑓‘(𝑛 + 1))) ↔ ((𝑚 ∈ ℕ ↦ ∪ 𝑙 ∈ (1...𝑚)(𝑔‘𝑙)):ℕ⟶dom vol ∧ ∀𝑛 ∈ ℕ ((𝑚 ∈ ℕ ↦ ∪ 𝑙 ∈ (1...𝑚)(𝑔‘𝑙))‘𝑛) ⊆ ((𝑚 ∈ ℕ ↦ ∪ 𝑙 ∈ (1...𝑚)(𝑔‘𝑙))‘(𝑛 + 1)))))
84		rneq 5647	. . . . . . . . . . . . . . . . 17 ⊢ (𝑓 = (𝑚 ∈ ℕ ↦ ∪ 𝑙 ∈ (1...𝑚)(𝑔‘𝑙)) → ran 𝑓 = ran (𝑚 ∈ ℕ ↦ ∪ 𝑙 ∈ (1...𝑚)(𝑔‘𝑙)))
85	84	unieqd 4719	. . . . . . . . . . . . . . . 16 ⊢ (𝑓 = (𝑚 ∈ ℕ ↦ ∪ 𝑙 ∈ (1...𝑚)(𝑔‘𝑙)) → ∪ ran 𝑓 = ∪ ran (𝑚 ∈ ℕ ↦ ∪ 𝑙 ∈ (1...𝑚)(𝑔‘𝑙)))
86	85	fveq2d 6501	. . . . . . . . . . . . . . 15 ⊢ (𝑓 = (𝑚 ∈ ℕ ↦ ∪ 𝑙 ∈ (1...𝑚)(𝑔‘𝑙)) → (vol‘∪ ran 𝑓) = (vol‘∪ ran (𝑚 ∈ ℕ ↦ ∪ 𝑙 ∈ (1...𝑚)(𝑔‘𝑙))))
87	84	imaeq2d 5768	. . . . . . . . . . . . . . . 16 ⊢ (𝑓 = (𝑚 ∈ ℕ ↦ ∪ 𝑙 ∈ (1...𝑚)(𝑔‘𝑙)) → (vol “ ran 𝑓) = (vol “ ran (𝑚 ∈ ℕ ↦ ∪ 𝑙 ∈ (1...𝑚)(𝑔‘𝑙))))
88	87	supeq1d 8704	. . . . . . . . . . . . . . 15 ⊢ (𝑓 = (𝑚 ∈ ℕ ↦ ∪ 𝑙 ∈ (1...𝑚)(𝑔‘𝑙)) → sup((vol “ ran 𝑓), ℝ*, < ) = sup((vol “ ran (𝑚 ∈ ℕ ↦ ∪ 𝑙 ∈ (1...𝑚)(𝑔‘𝑙))), ℝ*, < ))
89	86, 88	eqeq12d 2788	. . . . . . . . . . . . . 14 ⊢ (𝑓 = (𝑚 ∈ ℕ ↦ ∪ 𝑙 ∈ (1...𝑚)(𝑔‘𝑙)) → ((vol‘∪ ran 𝑓) = sup((vol “ ran 𝑓), ℝ*, < ) ↔ (vol‘∪ ran (𝑚 ∈ ℕ ↦ ∪ 𝑙 ∈ (1...𝑚)(𝑔‘𝑙))) = sup((vol “ ran (𝑚 ∈ ℕ ↦ ∪ 𝑙 ∈ (1...𝑚)(𝑔‘𝑙))), ℝ*, < )))
90	83, 89	imbi12d 337	. . . . . . . . . . . . 13 ⊢ (𝑓 = (𝑚 ∈ ℕ ↦ ∪ 𝑙 ∈ (1...𝑚)(𝑔‘𝑙)) → (((𝑓:ℕ⟶dom vol ∧ ∀𝑛 ∈ ℕ (𝑓‘𝑛) ⊆ (𝑓‘(𝑛 + 1))) → (vol‘∪ ran 𝑓) = sup((vol “ ran 𝑓), ℝ*, < )) ↔ (((𝑚 ∈ ℕ ↦ ∪ 𝑙 ∈ (1...𝑚)(𝑔‘𝑙)):ℕ⟶dom vol ∧ ∀𝑛 ∈ ℕ ((𝑚 ∈ ℕ ↦ ∪ 𝑙 ∈ (1...𝑚)(𝑔‘𝑙))‘𝑛) ⊆ ((𝑚 ∈ ℕ ↦ ∪ 𝑙 ∈ (1...𝑚)(𝑔‘𝑙))‘(𝑛 + 1))) → (vol‘∪ ran (𝑚 ∈ ℕ ↦ ∪ 𝑙 ∈ (1...𝑚)(𝑔‘𝑙))) = sup((vol “ ran (𝑚 ∈ ℕ ↦ ∪ 𝑙 ∈ (1...𝑚)(𝑔‘𝑙))), ℝ*, < ))))
91		volsupnfl.0	. . . . . . . . . . . . 13 ⊢ ((𝑓:ℕ⟶dom vol ∧ ∀𝑛 ∈ ℕ (𝑓‘𝑛) ⊆ (𝑓‘(𝑛 + 1))) → (vol‘∪ ran 𝑓) = sup((vol “ ran 𝑓), ℝ*, < ))
92	77, 90, 91	vtocl 3473	. . . . . . . . . . . 12 ⊢ (((𝑚 ∈ ℕ ↦ ∪ 𝑙 ∈ (1...𝑚)(𝑔‘𝑙)):ℕ⟶dom vol ∧ ∀𝑛 ∈ ℕ ((𝑚 ∈ ℕ ↦ ∪ 𝑙 ∈ (1...𝑚)(𝑔‘𝑙))‘𝑛) ⊆ ((𝑚 ∈ ℕ ↦ ∪ 𝑙 ∈ (1...𝑚)(𝑔‘𝑙))‘(𝑛 + 1))) → (vol‘∪ ran (𝑚 ∈ ℕ ↦ ∪ 𝑙 ∈ (1...𝑚)(𝑔‘𝑙))) = sup((vol “ ran (𝑚 ∈ ℕ ↦ ∪ 𝑙 ∈ (1...𝑚)(𝑔‘𝑙))), ℝ*, < ))
93	55, 75, 92	sylancl 578	. . . . . . . . . . 11 ⊢ ((𝑔:ℕ–onto→𝐴 ∧ ∀𝑥 ∈ 𝐴 (𝑥 ∈ dom vol ∧ (vol‘𝑥) = 0)) → (vol‘∪ ran (𝑚 ∈ ℕ ↦ ∪ 𝑙 ∈ (1...𝑚)(𝑔‘𝑙))) = sup((vol “ ran (𝑚 ∈ ℕ ↦ ∪ 𝑙 ∈ (1...𝑚)(𝑔‘𝑙))), ℝ*, < ))
94		df-iun 4791	. . . . . . . . . . . . . . . 16 ⊢ ∪ 𝑥 ∈ ℕ (𝑔‘𝑥) = {𝑛 ∣ ∃𝑥 ∈ ℕ 𝑛 ∈ (𝑔‘𝑥)}
95		eluzfz2 12730	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ (𝑥 ∈ (ℤ≥‘1) → 𝑥 ∈ (1...𝑥))
96	95, 37	eleq2s 2879	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (𝑥 ∈ ℕ → 𝑥 ∈ (1...𝑥))
97		fveq2 6497	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ (𝑙 = 𝑥 → (𝑔‘𝑙) = (𝑔‘𝑥))
98	97	eleq2d 2846	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ (𝑙 = 𝑥 → (𝑛 ∈ (𝑔‘𝑙) ↔ 𝑛 ∈ (𝑔‘𝑥)))
99	98	rspcev 3530	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ ((𝑥 ∈ (1...𝑥) ∧ 𝑛 ∈ (𝑔‘𝑥)) → ∃𝑙 ∈ (1...𝑥)𝑛 ∈ (𝑔‘𝑙))
100	96, 99	sylan 572	. . . . . . . . . . . . . . . . . . . . 21 ⊢ ((𝑥 ∈ ℕ ∧ 𝑛 ∈ (𝑔‘𝑥)) → ∃𝑙 ∈ (1...𝑥)𝑛 ∈ (𝑔‘𝑙))
101		oveq2 6983	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ (𝑚 = 𝑥 → (1...𝑚) = (1...𝑥))
102	101	rexeqdv 3351	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (𝑚 = 𝑥 → (∃𝑙 ∈ (1...𝑚)𝑛 ∈ (𝑔‘𝑙) ↔ ∃𝑙 ∈ (1...𝑥)𝑛 ∈ (𝑔‘𝑙)))
103	102	rspcev 3530	. . . . . . . . . . . . . . . . . . . . 21 ⊢ ((𝑥 ∈ ℕ ∧ ∃𝑙 ∈ (1...𝑥)𝑛 ∈ (𝑔‘𝑙)) → ∃𝑚 ∈ ℕ ∃𝑙 ∈ (1...𝑚)𝑛 ∈ (𝑔‘𝑙))
104	100, 103	syldan 583	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((𝑥 ∈ ℕ ∧ 𝑛 ∈ (𝑔‘𝑥)) → ∃𝑚 ∈ ℕ ∃𝑙 ∈ (1...𝑚)𝑛 ∈ (𝑔‘𝑙))
105	104	rexlimiva 3221	. . . . . . . . . . . . . . . . . . 19 ⊢ (∃𝑥 ∈ ℕ 𝑛 ∈ (𝑔‘𝑥) → ∃𝑚 ∈ ℕ ∃𝑙 ∈ (1...𝑚)𝑛 ∈ (𝑔‘𝑙))
106		ssrexv 3919	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ ((1...𝑚) ⊆ ℕ → (∃𝑙 ∈ (1...𝑚)𝑛 ∈ (𝑔‘𝑙) → ∃𝑙 ∈ ℕ 𝑛 ∈ (𝑔‘𝑙)))
107	38, 106	ax-mp 5	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (∃𝑙 ∈ (1...𝑚)𝑛 ∈ (𝑔‘𝑙) → ∃𝑙 ∈ ℕ 𝑛 ∈ (𝑔‘𝑙))
108	98	cbvrexv 3379	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (∃𝑙 ∈ ℕ 𝑛 ∈ (𝑔‘𝑙) ↔ ∃𝑥 ∈ ℕ 𝑛 ∈ (𝑔‘𝑥))
109	107, 108	sylib 210	. . . . . . . . . . . . . . . . . . . 20 ⊢ (∃𝑙 ∈ (1...𝑚)𝑛 ∈ (𝑔‘𝑙) → ∃𝑥 ∈ ℕ 𝑛 ∈ (𝑔‘𝑥))
110	109	rexlimivw 3222	. . . . . . . . . . . . . . . . . . 19 ⊢ (∃𝑚 ∈ ℕ ∃𝑙 ∈ (1...𝑚)𝑛 ∈ (𝑔‘𝑙) → ∃𝑥 ∈ ℕ 𝑛 ∈ (𝑔‘𝑥))
111	105, 110	impbii 201	. . . . . . . . . . . . . . . . . 18 ⊢ (∃𝑥 ∈ ℕ 𝑛 ∈ (𝑔‘𝑥) ↔ ∃𝑚 ∈ ℕ ∃𝑙 ∈ (1...𝑚)𝑛 ∈ (𝑔‘𝑙))
112		eliun 4793	. . . . . . . . . . . . . . . . . . 19 ⊢ (𝑛 ∈ ∪ 𝑙 ∈ (1...𝑚)(𝑔‘𝑙) ↔ ∃𝑙 ∈ (1...𝑚)𝑛 ∈ (𝑔‘𝑙))
113	112	rexbii 3189	. . . . . . . . . . . . . . . . . 18 ⊢ (∃𝑚 ∈ ℕ 𝑛 ∈ ∪ 𝑙 ∈ (1...𝑚)(𝑔‘𝑙) ↔ ∃𝑚 ∈ ℕ ∃𝑙 ∈ (1...𝑚)𝑛 ∈ (𝑔‘𝑙))
114	111, 113	bitr4i 270	. . . . . . . . . . . . . . . . 17 ⊢ (∃𝑥 ∈ ℕ 𝑛 ∈ (𝑔‘𝑥) ↔ ∃𝑚 ∈ ℕ 𝑛 ∈ ∪ 𝑙 ∈ (1...𝑚)(𝑔‘𝑙))
115	114	abbii 2839	. . . . . . . . . . . . . . . 16 ⊢ {𝑛 ∣ ∃𝑥 ∈ ℕ 𝑛 ∈ (𝑔‘𝑥)} = {𝑛 ∣ ∃𝑚 ∈ ℕ 𝑛 ∈ ∪ 𝑙 ∈ (1...𝑚)(𝑔‘𝑙)}
116	94, 115	eqtri 2797	. . . . . . . . . . . . . . 15 ⊢ ∪ 𝑥 ∈ ℕ (𝑔‘𝑥) = {𝑛 ∣ ∃𝑚 ∈ ℕ 𝑛 ∈ ∪ 𝑙 ∈ (1...𝑚)(𝑔‘𝑙)}
117		df-iun 4791	. . . . . . . . . . . . . . 15 ⊢ ∪ 𝑚 ∈ ℕ ∪ 𝑙 ∈ (1...𝑚)(𝑔‘𝑙) = {𝑛 ∣ ∃𝑚 ∈ ℕ 𝑛 ∈ ∪ 𝑙 ∈ (1...𝑚)(𝑔‘𝑙)}
118		ovex 7007	. . . . . . . . . . . . . . . . 17 ⊢ (1...𝑚) ∈ V
119	118, 63	iunex 7480	. . . . . . . . . . . . . . . 16 ⊢ ∪ 𝑙 ∈ (1...𝑚)(𝑔‘𝑙) ∈ V
120	119	dfiun3 5677	. . . . . . . . . . . . . . 15 ⊢ ∪ 𝑚 ∈ ℕ ∪ 𝑙 ∈ (1...𝑚)(𝑔‘𝑙) = ∪ ran (𝑚 ∈ ℕ ↦ ∪ 𝑙 ∈ (1...𝑚)(𝑔‘𝑙))
121	116, 117, 120	3eqtr2i 2803	. . . . . . . . . . . . . 14 ⊢ ∪ 𝑥 ∈ ℕ (𝑔‘𝑥) = ∪ ran (𝑚 ∈ ℕ ↦ ∪ 𝑙 ∈ (1...𝑚)(𝑔‘𝑙))
122		fofn 6419	. . . . . . . . . . . . . . . 16 ⊢ (𝑔:ℕ–onto→𝐴 → 𝑔 Fn ℕ)
123		fniunfv 6830	. . . . . . . . . . . . . . . 16 ⊢ (𝑔 Fn ℕ → ∪ 𝑥 ∈ ℕ (𝑔‘𝑥) = ∪ ran 𝑔)
124	122, 123	syl 17	. . . . . . . . . . . . . . 15 ⊢ (𝑔:ℕ–onto→𝐴 → ∪ 𝑥 ∈ ℕ (𝑔‘𝑥) = ∪ ran 𝑔)
125		forn 6420	. . . . . . . . . . . . . . . 16 ⊢ (𝑔:ℕ–onto→𝐴 → ran 𝑔 = 𝐴)
126	125	unieqd 4719	. . . . . . . . . . . . . . 15 ⊢ (𝑔:ℕ–onto→𝐴 → ∪ ran 𝑔 = ∪ 𝐴)
127	124, 126	eqtrd 2809	. . . . . . . . . . . . . 14 ⊢ (𝑔:ℕ–onto→𝐴 → ∪ 𝑥 ∈ ℕ (𝑔‘𝑥) = ∪ 𝐴)
128	121, 127	syl5eqr 2823	. . . . . . . . . . . . 13 ⊢ (𝑔:ℕ–onto→𝐴 → ∪ ran (𝑚 ∈ ℕ ↦ ∪ 𝑙 ∈ (1...𝑚)(𝑔‘𝑙)) = ∪ 𝐴)
129	128	fveq2d 6501	. . . . . . . . . . . 12 ⊢ (𝑔:ℕ–onto→𝐴 → (vol‘∪ ran (𝑚 ∈ ℕ ↦ ∪ 𝑙 ∈ (1...𝑚)(𝑔‘𝑙))) = (vol‘∪ 𝐴))
130	129	adantr 473	. . . . . . . . . . 11 ⊢ ((𝑔:ℕ–onto→𝐴 ∧ ∀𝑥 ∈ 𝐴 (𝑥 ∈ dom vol ∧ (vol‘𝑥) = 0)) → (vol‘∪ ran (𝑚 ∈ ℕ ↦ ∪ 𝑙 ∈ (1...𝑚)(𝑔‘𝑙))) = (vol‘∪ 𝐴))
131		rnco2 5943	. . . . . . . . . . . . . 14 ⊢ ran (vol ∘ (𝑚 ∈ ℕ ↦ ∪ 𝑙 ∈ (1...𝑚)(𝑔‘𝑙))) = (vol “ ran (𝑚 ∈ ℕ ↦ ∪ 𝑙 ∈ (1...𝑚)(𝑔‘𝑙)))
132		eqidd 2774	. . . . . . . . . . . . . . . . 17 ⊢ ((𝑔:ℕ–onto→𝐴 ∧ ∀𝑥 ∈ 𝐴 (𝑥 ∈ dom vol ∧ (vol‘𝑥) = 0)) → (𝑚 ∈ ℕ ↦ ∪ 𝑙 ∈ (1...𝑚)(𝑔‘𝑙)) = (𝑚 ∈ ℕ ↦ ∪ 𝑙 ∈ (1...𝑚)(𝑔‘𝑙)))
133		volf 23849	. . . . . . . . . . . . . . . . . . 19 ⊢ vol:dom vol⟶(0[,]+∞)
134	133	a1i 11	. . . . . . . . . . . . . . . . . 18 ⊢ ((𝑔:ℕ–onto→𝐴 ∧ ∀𝑥 ∈ 𝐴 (𝑥 ∈ dom vol ∧ (vol‘𝑥) = 0)) → vol:dom vol⟶(0[,]+∞))
135	134	feqmptd 6561	. . . . . . . . . . . . . . . . 17 ⊢ ((𝑔:ℕ–onto→𝐴 ∧ ∀𝑥 ∈ 𝐴 (𝑥 ∈ dom vol ∧ (vol‘𝑥) = 0)) → vol = (𝑛 ∈ dom vol ↦ (vol‘𝑛)))
136		fveq2 6497	. . . . . . . . . . . . . . . . 17 ⊢ (𝑛 = ∪ 𝑙 ∈ (1...𝑚)(𝑔‘𝑙) → (vol‘𝑛) = (vol‘∪ 𝑙 ∈ (1...𝑚)(𝑔‘𝑙)))
137	54, 132, 135, 136	fmptco 6713	. . . . . . . . . . . . . . . 16 ⊢ ((𝑔:ℕ–onto→𝐴 ∧ ∀𝑥 ∈ 𝐴 (𝑥 ∈ dom vol ∧ (vol‘𝑥) = 0)) → (vol ∘ (𝑚 ∈ ℕ ↦ ∪ 𝑙 ∈ (1...𝑚)(𝑔‘𝑙))) = (𝑚 ∈ ℕ ↦ (vol‘∪ 𝑙 ∈ (1...𝑚)(𝑔‘𝑙))))
138		mblvol 23850	. . . . . . . . . . . . . . . . . . . 20 ⊢ (∪ 𝑙 ∈ (1...𝑚)(𝑔‘𝑙) ∈ dom vol → (vol‘∪ 𝑙 ∈ (1...𝑚)(𝑔‘𝑙)) = (vol*‘∪ 𝑙 ∈ (1...𝑚)(𝑔‘𝑙)))
139	54, 138	syl 17	. . . . . . . . . . . . . . . . . . 19 ⊢ (((𝑔:ℕ–onto→𝐴 ∧ ∀𝑥 ∈ 𝐴 (𝑥 ∈ dom vol ∧ (vol‘𝑥) = 0)) ∧ 𝑚 ∈ ℕ) → (vol‘∪ 𝑙 ∈ (1...𝑚)(𝑔‘𝑙)) = (vol*‘∪ 𝑙 ∈ (1...𝑚)(𝑔‘𝑙)))
140		mblss 23851	. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 ⊢ (𝑥 ∈ dom vol → 𝑥 ⊆ ℝ)
141	140	adantr 473	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28 ⊢ ((𝑥 ∈ dom vol ∧ (vol‘𝑥) = 0) → 𝑥 ⊆ ℝ)
142	25	eqeq1d 2775	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 ⊢ (𝑥 ∈ dom vol → ((vol‘𝑥) = 0 ↔ (vol*‘𝑥) = 0))
143		0re 10440	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 ⊢ 0 ∈ ℝ
144		eleq1a 2856	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 ⊢ (0 ∈ ℝ → ((vol*‘𝑥) = 0 → (vol*‘𝑥) ∈ ℝ))
145	143, 144	ax-mp 5	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 ⊢ ((vol*‘𝑥) = 0 → (vol*‘𝑥) ∈ ℝ)
146	142, 145	syl6bi 245	. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 ⊢ (𝑥 ∈ dom vol → ((vol‘𝑥) = 0 → (vol*‘𝑥) ∈ ℝ))
147	146	imp 398	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28 ⊢ ((𝑥 ∈ dom vol ∧ (vol‘𝑥) = 0) → (vol*‘𝑥) ∈ ℝ)
148	141, 147	jca 504	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 ⊢ ((𝑥 ∈ dom vol ∧ (vol‘𝑥) = 0) → (𝑥 ⊆ ℝ ∧ (vol*‘𝑥) ∈ ℝ))
149	148	ralimi 3105	. . . . . . . . . . . . . . . . . . . . . . . . . 26 ⊢ (∀𝑥 ∈ 𝐴 (𝑥 ∈ dom vol ∧ (vol‘𝑥) = 0) → ∀𝑥 ∈ 𝐴 (𝑥 ⊆ ℝ ∧ (vol*‘𝑥) ∈ ℝ))
150	149	adantl 474	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ ((𝑔:ℕ–onto→𝐴 ∧ ∀𝑥 ∈ 𝐴 (𝑥 ∈ dom vol ∧ (vol‘𝑥) = 0)) → ∀𝑥 ∈ 𝐴 (𝑥 ⊆ ℝ ∧ (vol*‘𝑥) ∈ ℝ))
151		ssid 3874	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28 ⊢ ℕ ⊆ ℕ
152		sseq1 3877	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 ⊢ (𝑥 = (𝑔‘𝑙) → (𝑥 ⊆ ℝ ↔ (𝑔‘𝑙) ⊆ ℝ))
153		fveq2 6497	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 ⊢ (𝑥 = (𝑔‘𝑙) → (vol*‘𝑥) = (vol*‘(𝑔‘𝑙)))
154	153	eleq1d 2845	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 ⊢ (𝑥 = (𝑔‘𝑙) → ((vol*‘𝑥) ∈ ℝ ↔ (vol*‘(𝑔‘𝑙)) ∈ ℝ))
155	152, 154	anbi12d 622	. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 ⊢ (𝑥 = (𝑔‘𝑙) → ((𝑥 ⊆ ℝ ∧ (vol*‘𝑥) ∈ ℝ) ↔ ((𝑔‘𝑙) ⊆ ℝ ∧ (vol*‘(𝑔‘𝑙)) ∈ ℝ)))
156	155	ralima 6824	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28 ⊢ ((𝑔 Fn ℕ ∧ ℕ ⊆ ℕ) → (∀𝑥 ∈ (𝑔 “ ℕ)(𝑥 ⊆ ℝ ∧ (vol*‘𝑥) ∈ ℝ) ↔ ∀𝑙 ∈ ℕ ((𝑔‘𝑙) ⊆ ℝ ∧ (vol*‘(𝑔‘𝑙)) ∈ ℝ)))
157	122, 151, 156	sylancl 578	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 ⊢ (𝑔:ℕ–onto→𝐴 → (∀𝑥 ∈ (𝑔 “ ℕ)(𝑥 ⊆ ℝ ∧ (vol*‘𝑥) ∈ ℝ) ↔ ∀𝑙 ∈ ℕ ((𝑔‘𝑙) ⊆ ℝ ∧ (vol*‘(𝑔‘𝑙)) ∈ ℝ)))
158		foima 6422	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28 ⊢ (𝑔:ℕ–onto→𝐴 → (𝑔 “ ℕ) = 𝐴)
159	158	raleqdv 3350	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 ⊢ (𝑔:ℕ–onto→𝐴 → (∀𝑥 ∈ (𝑔 “ ℕ)(𝑥 ⊆ ℝ ∧ (vol*‘𝑥) ∈ ℝ) ↔ ∀𝑥 ∈ 𝐴 (𝑥 ⊆ ℝ ∧ (vol*‘𝑥) ∈ ℝ)))
160	157, 159	bitr3d 273	. . . . . . . . . . . . . . . . . . . . . . . . . 26 ⊢ (𝑔:ℕ–onto→𝐴 → (∀𝑙 ∈ ℕ ((𝑔‘𝑙) ⊆ ℝ ∧ (vol*‘(𝑔‘𝑙)) ∈ ℝ) ↔ ∀𝑥 ∈ 𝐴 (𝑥 ⊆ ℝ ∧ (vol*‘𝑥) ∈ ℝ)))
161	160	adantr 473	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ ((𝑔:ℕ–onto→𝐴 ∧ ∀𝑥 ∈ 𝐴 (𝑥 ∈ dom vol ∧ (vol‘𝑥) = 0)) → (∀𝑙 ∈ ℕ ((𝑔‘𝑙) ⊆ ℝ ∧ (vol*‘(𝑔‘𝑙)) ∈ ℝ) ↔ ∀𝑥 ∈ 𝐴 (𝑥 ⊆ ℝ ∧ (vol*‘𝑥) ∈ ℝ)))
162	150, 161	mpbird 249	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ ((𝑔:ℕ–onto→𝐴 ∧ ∀𝑥 ∈ 𝐴 (𝑥 ∈ dom vol ∧ (vol‘𝑥) = 0)) → ∀𝑙 ∈ ℕ ((𝑔‘𝑙) ⊆ ℝ ∧ (vol*‘(𝑔‘𝑙)) ∈ ℝ))
163		ssralv 3918	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ ((1...𝑚) ⊆ ℕ → (∀𝑙 ∈ ℕ ((𝑔‘𝑙) ⊆ ℝ ∧ (vol*‘(𝑔‘𝑙)) ∈ ℝ) → ∀𝑙 ∈ (1...𝑚)((𝑔‘𝑙) ⊆ ℝ ∧ (vol*‘(𝑔‘𝑙)) ∈ ℝ)))
164	38, 162, 163	mpsyl 68	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ ((𝑔:ℕ–onto→𝐴 ∧ ∀𝑥 ∈ 𝐴 (𝑥 ∈ dom vol ∧ (vol‘𝑥) = 0)) → ∀𝑙 ∈ (1...𝑚)((𝑔‘𝑙) ⊆ ℝ ∧ (vol*‘(𝑔‘𝑙)) ∈ ℝ))
165	164	adantr 473	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (((𝑔:ℕ–onto→𝐴 ∧ ∀𝑥 ∈ 𝐴 (𝑥 ∈ dom vol ∧ (vol‘𝑥) = 0)) ∧ 𝑚 ∈ ℕ) → ∀𝑙 ∈ (1...𝑚)((𝑔‘𝑙) ⊆ ℝ ∧ (vol*‘(𝑔‘𝑙)) ∈ ℝ))
166		ovolfiniun 23821	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (((1...𝑚) ∈ Fin ∧ ∀𝑙 ∈ (1...𝑚)((𝑔‘𝑙) ⊆ ℝ ∧ (vol*‘(𝑔‘𝑙)) ∈ ℝ)) → (vol*‘∪ 𝑙 ∈ (1...𝑚)(𝑔‘𝑙)) ≤ Σ𝑙 ∈ (1...𝑚)(vol*‘(𝑔‘𝑙)))
167	35, 165, 166	sylancr 579	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (((𝑔:ℕ–onto→𝐴 ∧ ∀𝑥 ∈ 𝐴 (𝑥 ∈ dom vol ∧ (vol‘𝑥) = 0)) ∧ 𝑚 ∈ ℕ) → (vol*‘∪ 𝑙 ∈ (1...𝑚)(𝑔‘𝑙)) ≤ Σ𝑙 ∈ (1...𝑚)(vol*‘(𝑔‘𝑙)))
168		mblvol 23850	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28 ⊢ ((𝑔‘𝑙) ∈ dom vol → (vol‘(𝑔‘𝑙)) = (vol*‘(𝑔‘𝑙)))
169	48, 168	syl 17	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 ⊢ (((𝑔:ℕ–onto→𝐴 ∧ ∀𝑥 ∈ 𝐴 (𝑥 ∈ dom vol ∧ (vol‘𝑥) = 0)) ∧ 𝑙 ∈ ℕ) → (vol‘(𝑔‘𝑙)) = (vol*‘(𝑔‘𝑙)))
170	44	simprd 488	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 ⊢ ((∀𝑥 ∈ 𝐴 (𝑥 ∈ dom vol ∧ (vol‘𝑥) = 0) ∧ (𝑔‘𝑙) ∈ 𝐴) → (vol‘(𝑔‘𝑙)) = 0)
171	40, 170	sylan2 584	. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 ⊢ ((∀𝑥 ∈ 𝐴 (𝑥 ∈ dom vol ∧ (vol‘𝑥) = 0) ∧ (𝑔:ℕ–onto→𝐴 ∧ 𝑙 ∈ ℕ)) → (vol‘(𝑔‘𝑙)) = 0)
172	171	ancoms 451	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28 ⊢ (((𝑔:ℕ–onto→𝐴 ∧ 𝑙 ∈ ℕ) ∧ ∀𝑥 ∈ 𝐴 (𝑥 ∈ dom vol ∧ (vol‘𝑥) = 0)) → (vol‘(𝑔‘𝑙)) = 0)
173	172	an32s 640	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 ⊢ (((𝑔:ℕ–onto→𝐴 ∧ ∀𝑥 ∈ 𝐴 (𝑥 ∈ dom vol ∧ (vol‘𝑥) = 0)) ∧ 𝑙 ∈ ℕ) → (vol‘(𝑔‘𝑙)) = 0)
174	169, 173	eqtr3d 2811	. . . . . . . . . . . . . . . . . . . . . . . . . 26 ⊢ (((𝑔:ℕ–onto→𝐴 ∧ ∀𝑥 ∈ 𝐴 (𝑥 ∈ dom vol ∧ (vol‘𝑥) = 0)) ∧ 𝑙 ∈ ℕ) → (vol*‘(𝑔‘𝑙)) = 0)
175	174	ralrimiva 3127	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ ((𝑔:ℕ–onto→𝐴 ∧ ∀𝑥 ∈ 𝐴 (𝑥 ∈ dom vol ∧ (vol‘𝑥) = 0)) → ∀𝑙 ∈ ℕ (vol*‘(𝑔‘𝑙)) = 0)
176		ssralv 3918	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ ((1...𝑚) ⊆ ℕ → (∀𝑙 ∈ ℕ (vol*‘(𝑔‘𝑙)) = 0 → ∀𝑙 ∈ (1...𝑚)(vol*‘(𝑔‘𝑙)) = 0))
177	38, 175, 176	mpsyl 68	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ ((𝑔:ℕ–onto→𝐴 ∧ ∀𝑥 ∈ 𝐴 (𝑥 ∈ dom vol ∧ (vol‘𝑥) = 0)) → ∀𝑙 ∈ (1...𝑚)(vol*‘(𝑔‘𝑙)) = 0)
178	177	adantr 473	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ (((𝑔:ℕ–onto→𝐴 ∧ ∀𝑥 ∈ 𝐴 (𝑥 ∈ dom vol ∧ (vol‘𝑥) = 0)) ∧ 𝑚 ∈ ℕ) → ∀𝑙 ∈ (1...𝑚)(vol*‘(𝑔‘𝑙)) = 0)
179	178	sumeq2d 14918	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (((𝑔:ℕ–onto→𝐴 ∧ ∀𝑥 ∈ 𝐴 (𝑥 ∈ dom vol ∧ (vol‘𝑥) = 0)) ∧ 𝑚 ∈ ℕ) → Σ𝑙 ∈ (1...𝑚)(vol*‘(𝑔‘𝑙)) = Σ𝑙 ∈ (1...𝑚)0)
180	35	olci 853	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ ((1...𝑚) ⊆ (ℤ≥‘1) ∨ (1...𝑚) ∈ Fin)
181		sumz 14938	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ (((1...𝑚) ⊆ (ℤ≥‘1) ∨ (1...𝑚) ∈ Fin) → Σ𝑙 ∈ (1...𝑚)0 = 0)
182	180, 181	ax-mp 5	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ Σ𝑙 ∈ (1...𝑚)0 = 0
183	179, 182	syl6eq 2825	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (((𝑔:ℕ–onto→𝐴 ∧ ∀𝑥 ∈ 𝐴 (𝑥 ∈ dom vol ∧ (vol‘𝑥) = 0)) ∧ 𝑚 ∈ ℕ) → Σ𝑙 ∈ (1...𝑚)(vol*‘(𝑔‘𝑙)) = 0)
184	167, 183	breqtrd 4952	. . . . . . . . . . . . . . . . . . . 20 ⊢ (((𝑔:ℕ–onto→𝐴 ∧ ∀𝑥 ∈ 𝐴 (𝑥 ∈ dom vol ∧ (vol‘𝑥) = 0)) ∧ 𝑚 ∈ ℕ) → (vol*‘∪ 𝑙 ∈ (1...𝑚)(𝑔‘𝑙)) ≤ 0)
185		mblss 23851	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ ((𝑔‘𝑙) ∈ dom vol → (𝑔‘𝑙) ⊆ ℝ)
186	185	ralimi 3105	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ (∀𝑙 ∈ (1...𝑚)(𝑔‘𝑙) ∈ dom vol → ∀𝑙 ∈ (1...𝑚)(𝑔‘𝑙) ⊆ ℝ)
187	51, 186	syl 17	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ ((𝑔:ℕ–onto→𝐴 ∧ ∀𝑥 ∈ 𝐴 (𝑥 ∈ dom vol ∧ (vol‘𝑥) = 0)) → ∀𝑙 ∈ (1...𝑚)(𝑔‘𝑙) ⊆ ℝ)
188		iunss 4832	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ (∪ 𝑙 ∈ (1...𝑚)(𝑔‘𝑙) ⊆ ℝ ↔ ∀𝑙 ∈ (1...𝑚)(𝑔‘𝑙) ⊆ ℝ)
189	187, 188	sylibr 226	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ ((𝑔:ℕ–onto→𝐴 ∧ ∀𝑥 ∈ 𝐴 (𝑥 ∈ dom vol ∧ (vol‘𝑥) = 0)) → ∪ 𝑙 ∈ (1...𝑚)(𝑔‘𝑙) ⊆ ℝ)
190	189	adantr 473	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (((𝑔:ℕ–onto→𝐴 ∧ ∀𝑥 ∈ 𝐴 (𝑥 ∈ dom vol ∧ (vol‘𝑥) = 0)) ∧ 𝑚 ∈ ℕ) → ∪ 𝑙 ∈ (1...𝑚)(𝑔‘𝑙) ⊆ ℝ)
191		ovolge0 23801	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (∪ 𝑙 ∈ (1...𝑚)(𝑔‘𝑙) ⊆ ℝ → 0 ≤ (vol*‘∪ 𝑙 ∈ (1...𝑚)(𝑔‘𝑙)))
192	190, 191	syl 17	. . . . . . . . . . . . . . . . . . . 20 ⊢ (((𝑔:ℕ–onto→𝐴 ∧ ∀𝑥 ∈ 𝐴 (𝑥 ∈ dom vol ∧ (vol‘𝑥) = 0)) ∧ 𝑚 ∈ ℕ) → 0 ≤ (vol*‘∪ 𝑙 ∈ (1...𝑚)(𝑔‘𝑙)))
193		ovolcl 23798	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ (∪ 𝑙 ∈ (1...𝑚)(𝑔‘𝑙) ⊆ ℝ → (vol*‘∪ 𝑙 ∈ (1...𝑚)(𝑔‘𝑙)) ∈ ℝ*)
194	189, 193	syl 17	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ ((𝑔:ℕ–onto→𝐴 ∧ ∀𝑥 ∈ 𝐴 (𝑥 ∈ dom vol ∧ (vol‘𝑥) = 0)) → (vol*‘∪ 𝑙 ∈ (1...𝑚)(𝑔‘𝑙)) ∈ ℝ*)
195	194	adantr 473	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (((𝑔:ℕ–onto→𝐴 ∧ ∀𝑥 ∈ 𝐴 (𝑥 ∈ dom vol ∧ (vol‘𝑥) = 0)) ∧ 𝑚 ∈ ℕ) → (vol*‘∪ 𝑙 ∈ (1...𝑚)(𝑔‘𝑙)) ∈ ℝ*)
196		0xr 10486	. . . . . . . . . . . . . . . . . . . . 21 ⊢ 0 ∈ ℝ*
197		xrletri3 12363	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (((vol*‘∪ 𝑙 ∈ (1...𝑚)(𝑔‘𝑙)) ∈ ℝ* ∧ 0 ∈ ℝ*) → ((vol*‘∪ 𝑙 ∈ (1...𝑚)(𝑔‘𝑙)) = 0 ↔ ((vol*‘∪ 𝑙 ∈ (1...𝑚)(𝑔‘𝑙)) ≤ 0 ∧ 0 ≤ (vol*‘∪ 𝑙 ∈ (1...𝑚)(𝑔‘𝑙)))))
198	195, 196, 197	sylancl 578	. . . . . . . . . . . . . . . . . . . 20 ⊢ (((𝑔:ℕ–onto→𝐴 ∧ ∀𝑥 ∈ 𝐴 (𝑥 ∈ dom vol ∧ (vol‘𝑥) = 0)) ∧ 𝑚 ∈ ℕ) → ((vol*‘∪ 𝑙 ∈ (1...𝑚)(𝑔‘𝑙)) = 0 ↔ ((vol*‘∪ 𝑙 ∈ (1...𝑚)(𝑔‘𝑙)) ≤ 0 ∧ 0 ≤ (vol*‘∪ 𝑙 ∈ (1...𝑚)(𝑔‘𝑙)))))
199	184, 192, 198	mpbir2and 701	. . . . . . . . . . . . . . . . . . 19 ⊢ (((𝑔:ℕ–onto→𝐴 ∧ ∀𝑥 ∈ 𝐴 (𝑥 ∈ dom vol ∧ (vol‘𝑥) = 0)) ∧ 𝑚 ∈ ℕ) → (vol*‘∪ 𝑙 ∈ (1...𝑚)(𝑔‘𝑙)) = 0)
200	139, 199	eqtrd 2809	. . . . . . . . . . . . . . . . . 18 ⊢ (((𝑔:ℕ–onto→𝐴 ∧ ∀𝑥 ∈ 𝐴 (𝑥 ∈ dom vol ∧ (vol‘𝑥) = 0)) ∧ 𝑚 ∈ ℕ) → (vol‘∪ 𝑙 ∈ (1...𝑚)(𝑔‘𝑙)) = 0)
201	200	mpteq2dva 5019	. . . . . . . . . . . . . . . . 17 ⊢ ((𝑔:ℕ–onto→𝐴 ∧ ∀𝑥 ∈ 𝐴 (𝑥 ∈ dom vol ∧ (vol‘𝑥) = 0)) → (𝑚 ∈ ℕ ↦ (vol‘∪ 𝑙 ∈ (1...𝑚)(𝑔‘𝑙))) = (𝑚 ∈ ℕ ↦ 0))
202		fconstmpt 5461	. . . . . . . . . . . . . . . . 17 ⊢ (ℕ × {0}) = (𝑚 ∈ ℕ ↦ 0)
203	201, 202	syl6eqr 2827	. . . . . . . . . . . . . . . 16 ⊢ ((𝑔:ℕ–onto→𝐴 ∧ ∀𝑥 ∈ 𝐴 (𝑥 ∈ dom vol ∧ (vol‘𝑥) = 0)) → (𝑚 ∈ ℕ ↦ (vol‘∪ 𝑙 ∈ (1...𝑚)(𝑔‘𝑙))) = (ℕ × {0}))
204	137, 203	eqtrd 2809	. . . . . . . . . . . . . . 15 ⊢ ((𝑔:ℕ–onto→𝐴 ∧ ∀𝑥 ∈ 𝐴 (𝑥 ∈ dom vol ∧ (vol‘𝑥) = 0)) → (vol ∘ (𝑚 ∈ ℕ ↦ ∪ 𝑙 ∈ (1...𝑚)(𝑔‘𝑙))) = (ℕ × {0}))
205		frn 6348	. . . . . . . . . . . . . . . . 17 ⊢ ((𝑚 ∈ ℕ ↦ ∪ 𝑙 ∈ (1...𝑚)(𝑔‘𝑙)):ℕ⟶dom vol → ran (𝑚 ∈ ℕ ↦ ∪ 𝑙 ∈ (1...𝑚)(𝑔‘𝑙)) ⊆ dom vol)
206		ffn 6342	. . . . . . . . . . . . . . . . . . 19 ⊢ (vol:dom vol⟶(0[,]+∞) → vol Fn dom vol)
207	133, 206	ax-mp 5	. . . . . . . . . . . . . . . . . 18 ⊢ vol Fn dom vol
208	119, 61	fnmpti 6319	. . . . . . . . . . . . . . . . . 18 ⊢ (𝑚 ∈ ℕ ↦ ∪ 𝑙 ∈ (1...𝑚)(𝑔‘𝑙)) Fn ℕ
209		fnco 6296	. . . . . . . . . . . . . . . . . 18 ⊢ ((vol Fn dom vol ∧ (𝑚 ∈ ℕ ↦ ∪ 𝑙 ∈ (1...𝑚)(𝑔‘𝑙)) Fn ℕ ∧ ran (𝑚 ∈ ℕ ↦ ∪ 𝑙 ∈ (1...𝑚)(𝑔‘𝑙)) ⊆ dom vol) → (vol ∘ (𝑚 ∈ ℕ ↦ ∪ 𝑙 ∈ (1...𝑚)(𝑔‘𝑙))) Fn ℕ)
210	207, 208, 209	mp3an12 1431	. . . . . . . . . . . . . . . . 17 ⊢ (ran (𝑚 ∈ ℕ ↦ ∪ 𝑙 ∈ (1...𝑚)(𝑔‘𝑙)) ⊆ dom vol → (vol ∘ (𝑚 ∈ ℕ ↦ ∪ 𝑙 ∈ (1...𝑚)(𝑔‘𝑙))) Fn ℕ)
211	55, 205, 210	3syl 18	. . . . . . . . . . . . . . . 16 ⊢ ((𝑔:ℕ–onto→𝐴 ∧ ∀𝑥 ∈ 𝐴 (𝑥 ∈ dom vol ∧ (vol‘𝑥) = 0)) → (vol ∘ (𝑚 ∈ ℕ ↦ ∪ 𝑙 ∈ (1...𝑚)(𝑔‘𝑙))) Fn ℕ)
212		1nn 11451	. . . . . . . . . . . . . . . . 17 ⊢ 1 ∈ ℕ
213	212	ne0ii 4184	. . . . . . . . . . . . . . . 16 ⊢ ℕ ≠ ∅
214		fconst5 6794	. . . . . . . . . . . . . . . 16 ⊢ (((vol ∘ (𝑚 ∈ ℕ ↦ ∪ 𝑙 ∈ (1...𝑚)(𝑔‘𝑙))) Fn ℕ ∧ ℕ ≠ ∅) → ((vol ∘ (𝑚 ∈ ℕ ↦ ∪ 𝑙 ∈ (1...𝑚)(𝑔‘𝑙))) = (ℕ × {0}) ↔ ran (vol ∘ (𝑚 ∈ ℕ ↦ ∪ 𝑙 ∈ (1...𝑚)(𝑔‘𝑙))) = {0}))
215	211, 213, 214	sylancl 578	. . . . . . . . . . . . . . 15 ⊢ ((𝑔:ℕ–onto→𝐴 ∧ ∀𝑥 ∈ 𝐴 (𝑥 ∈ dom vol ∧ (vol‘𝑥) = 0)) → ((vol ∘ (𝑚 ∈ ℕ ↦ ∪ 𝑙 ∈ (1...𝑚)(𝑔‘𝑙))) = (ℕ × {0}) ↔ ran (vol ∘ (𝑚 ∈ ℕ ↦ ∪ 𝑙 ∈ (1...𝑚)(𝑔‘𝑙))) = {0}))
216	204, 215	mpbid 224	. . . . . . . . . . . . . 14 ⊢ ((𝑔:ℕ–onto→𝐴 ∧ ∀𝑥 ∈ 𝐴 (𝑥 ∈ dom vol ∧ (vol‘𝑥) = 0)) → ran (vol ∘ (𝑚 ∈ ℕ ↦ ∪ 𝑙 ∈ (1...𝑚)(𝑔‘𝑙))) = {0})
217	131, 216	syl5eqr 2823	. . . . . . . . . . . . 13 ⊢ ((𝑔:ℕ–onto→𝐴 ∧ ∀𝑥 ∈ 𝐴 (𝑥 ∈ dom vol ∧ (vol‘𝑥) = 0)) → (vol “ ran (𝑚 ∈ ℕ ↦ ∪ 𝑙 ∈ (1...𝑚)(𝑔‘𝑙))) = {0})
218	217	supeq1d 8704	. . . . . . . . . . . 12 ⊢ ((𝑔:ℕ–onto→𝐴 ∧ ∀𝑥 ∈ 𝐴 (𝑥 ∈ dom vol ∧ (vol‘𝑥) = 0)) → sup((vol “ ran (𝑚 ∈ ℕ ↦ ∪ 𝑙 ∈ (1...𝑚)(𝑔‘𝑙))), ℝ*, < ) = sup({0}, ℝ*, < ))
219		xrltso 12350	. . . . . . . . . . . . 13 ⊢ < Or ℝ*
220		supsn 8730	. . . . . . . . . . . . 13 ⊢ (( < Or ℝ* ∧ 0 ∈ ℝ*) → sup({0}, ℝ*, < ) = 0)
221	219, 196, 220	mp2an 680	. . . . . . . . . . . 12 ⊢ sup({0}, ℝ*, < ) = 0
222	218, 221	syl6eq 2825	. . . . . . . . . . 11 ⊢ ((𝑔:ℕ–onto→𝐴 ∧ ∀𝑥 ∈ 𝐴 (𝑥 ∈ dom vol ∧ (vol‘𝑥) = 0)) → sup((vol “ ran (𝑚 ∈ ℕ ↦ ∪ 𝑙 ∈ (1...𝑚)(𝑔‘𝑙))), ℝ*, < ) = 0)
223	93, 130, 222	3eqtr3rd 2818	. . . . . . . . . 10 ⊢ ((𝑔:ℕ–onto→𝐴 ∧ ∀𝑥 ∈ 𝐴 (𝑥 ∈ dom vol ∧ (vol‘𝑥) = 0)) → 0 = (vol‘∪ 𝐴))
224	223	ex 405	. . . . . . . . 9 ⊢ (𝑔:ℕ–onto→𝐴 → (∀𝑥 ∈ 𝐴 (𝑥 ∈ dom vol ∧ (vol‘𝑥) = 0) → 0 = (vol‘∪ 𝐴)))
225	34, 224	syl5 34	. . . . . . . 8 ⊢ (𝑔:ℕ–onto→𝐴 → ((∀𝑥 ∈ 𝐴 𝑥 ≼ ℕ ∧ ∪ 𝐴 ⊆ ℝ) → 0 = (vol‘∪ 𝐴)))
226	225	exlimiv 1890	. . . . . . 7 ⊢ (∃𝑔 𝑔:ℕ–onto→𝐴 → ((∀𝑥 ∈ 𝐴 𝑥 ≼ ℕ ∧ ∪ 𝐴 ⊆ ℝ) → 0 = (vol‘∪ 𝐴)))
227	18, 226	syl 17	. . . . . 6 ⊢ ((𝐴 ≠ ∅ ∧ 𝐴 ≼ ℕ) → ((∀𝑥 ∈ 𝐴 𝑥 ≼ ℕ ∧ ∪ 𝐴 ⊆ ℝ) → 0 = (vol‘∪ 𝐴)))
228	227	expimpd 446	. . . . 5 ⊢ (𝐴 ≠ ∅ → ((𝐴 ≼ ℕ ∧ (∀𝑥 ∈ 𝐴 𝑥 ≼ ℕ ∧ ∪ 𝐴 ⊆ ℝ)) → 0 = (vol‘∪ 𝐴)))
229	11, 228	pm2.61ine 3046	. . . 4 ⊢ ((𝐴 ≼ ℕ ∧ (∀𝑥 ∈ 𝐴 𝑥 ≼ ℕ ∧ ∪ 𝐴 ⊆ ℝ)) → 0 = (vol‘∪ 𝐴))
230		renepnf 10487	. . . . . . 7 ⊢ (0 ∈ ℝ → 0 ≠ +∞)
231	143, 230	mp1i 13	. . . . . 6 ⊢ (∪ 𝐴 = ℝ → 0 ≠ +∞)
232		fveq2 6497	. . . . . . 7 ⊢ (∪ 𝐴 = ℝ → (vol‘∪ 𝐴) = (vol‘ℝ))
233		rembl 23860	. . . . . . . . 9 ⊢ ℝ ∈ dom vol
234		mblvol 23850	. . . . . . . . 9 ⊢ (ℝ ∈ dom vol → (vol‘ℝ) = (vol*‘ℝ))
235	233, 234	ax-mp 5	. . . . . . . 8 ⊢ (vol‘ℝ) = (vol*‘ℝ)
236		ovolre 23845	. . . . . . . 8 ⊢ (vol*‘ℝ) = +∞
237	235, 236	eqtri 2797	. . . . . . 7 ⊢ (vol‘ℝ) = +∞
238	232, 237	syl6eq 2825	. . . . . 6 ⊢ (∪ 𝐴 = ℝ → (vol‘∪ 𝐴) = +∞)
239	231, 238	neeqtrrd 3036	. . . . 5 ⊢ (∪ 𝐴 = ℝ → 0 ≠ (vol‘∪ 𝐴))
240	239	necon2i 2996	. . . 4 ⊢ (0 = (vol‘∪ 𝐴) → ∪ 𝐴 ≠ ℝ)
241	229, 240	syl 17	. . 3 ⊢ ((𝐴 ≼ ℕ ∧ (∀𝑥 ∈ 𝐴 𝑥 ≼ ℕ ∧ ∪ 𝐴 ⊆ ℝ)) → ∪ 𝐴 ≠ ℝ)
242	241	expr 449	. 2 ⊢ ((𝐴 ≼ ℕ ∧ ∀𝑥 ∈ 𝐴 𝑥 ≼ ℕ) → (∪ 𝐴 ⊆ ℝ → ∪ 𝐴 ≠ ℝ))
243		eqimss 3908	. . 3 ⊢ (∪ 𝐴 = ℝ → ∪ 𝐴 ⊆ ℝ)
244	243	necon3bi 2988	. 2 ⊢ (¬ ∪ 𝐴 ⊆ ℝ → ∪ 𝐴 ≠ ℝ)
245	242, 244	pm2.61d1 173	1 ⊢ ((𝐴 ≼ ℕ ∧ ∀𝑥 ∈ 𝐴 𝑥 ≼ ℕ) → ∪ 𝐴 ≠ ℝ)

Syntax hints:   → wi 4   ↔ wb 198   ∧ wa 387   ∨ wo 834   = wceq 1508  ∃wex 1743   ∈ wcel 2051  {cab 2753   ≠ wne 2962  ∀wral 3083  ∃wrex 3084  Vcvv 3410   ⊆ wss 3824  ∅c0 4173  {csn 4436  ∪ cuni 4709  ∪ ciun 4789   class class class wbr 4926   ↦ cmpt 5005   Or wor 5322   × cxp 5402  dom cdm 5404  ran crn 5405   “ cima 5407   ∘ ccom 5408   Fn wfn 6181  ⟶wf 6182  –onto→wfo 6184  ‘cfv 6186  (class class class)co 6975   ≼ cdom 8303   ≺ csdm 8304  Fincfn 8305  supcsup 8698  ℝcr 10333  0cc0 10334  1c1 10335   + caddc 10337  +∞cpnf 10470  ℝ^*cxr 10472   < clt 10473   ≤ cle 10474  ℕcn 11438  ℤ_≥cuz 12057  [,]cicc 12556  ...cfz 12707  Σcsu 14902  vol*covol 23782  volcvol 23783

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1759  ax-4 1773  ax-5 1870  ax-6 1929  ax-7 1966  ax-8 2053  ax-9 2060  ax-10 2080  ax-11 2094  ax-12 2107  ax-13 2302  ax-ext 2745  ax-rep 5046  ax-sep 5057  ax-nul 5064  ax-pow 5116  ax-pr 5183  ax-un 7278  ax-inf2 8897  ax-cnex 10390  ax-resscn 10391  ax-1cn 10392  ax-icn 10393  ax-addcl 10394  ax-addrcl 10395  ax-mulcl 10396  ax-mulrcl 10397  ax-mulcom 10398  ax-addass 10399  ax-mulass 10400  ax-distr 10401  ax-i2m1 10402  ax-1ne0 10403  ax-1rid 10404  ax-rnegex 10405  ax-rrecex 10406  ax-cnre 10407  ax-pre-lttri 10408  ax-pre-lttrn 10409  ax-pre-ltadd 10410  ax-pre-mulgt0 10411  ax-pre-sup 10412

This theorem depends on definitions:  df-bi 199  df-an 388  df-or 835  df-3or 1070  df-3an 1071  df-tru 1511  df-fal 1521  df-ex 1744  df-nf 1748  df-sb 2017  df-mo 2548  df-eu 2585  df-clab 2754  df-cleq 2766  df-clel 2841  df-nfc 2913  df-ne 2963  df-nel 3069  df-ral 3088  df-rex 3089  df-reu 3090  df-rmo 3091  df-rab 3092  df-v 3412  df-sbc 3677  df-csb 3782  df-dif 3827  df-un 3829  df-in 3831  df-ss 3838  df-pss 3840  df-nul 4174  df-if 4346  df-pw 4419  df-sn 4437  df-pr 4439  df-tp 4441  df-op 4443  df-uni 4710  df-int 4747  df-iun 4791  df-br 4927  df-opab 4989  df-mpt 5006  df-tr 5028  df-id 5309  df-eprel 5314  df-po 5323  df-so 5324  df-fr 5363  df-se 5364  df-we 5365  df-xp 5410  df-rel 5411  df-cnv 5412  df-co 5413  df-dm 5414  df-rn 5415  df-res 5416  df-ima 5417  df-pred 5984  df-ord 6030  df-on 6031  df-lim 6032  df-suc 6033  df-iota 6150  df-fun 6188  df-fn 6189  df-f 6190  df-f1 6191  df-fo 6192  df-f1o 6193  df-fv 6194  df-isom 6195  df-riota 6936  df-ov 6978  df-oprab 6979  df-mpo 6980  df-of 7226  df-om 7396  df-1st 7500  df-2nd 7501  df-wrecs 7749  df-recs 7811  df-rdg 7849  df-1o 7904  df-2o 7905  df-oadd 7908  df-er 8088  df-map 8207  df-en 8306  df-dom 8307  df-sdom 8308  df-fin 8309  df-fi 8669  df-sup 8700  df-inf 8701  df-oi 8768  df-dju 9123  df-card 9161  df-pnf 10475  df-mnf 10476  df-xr 10477  df-ltxr 10478  df-le 10479  df-sub 10671  df-neg 10672  df-div 11098  df-nn 11439  df-2 11502  df-3 11503  df-n0 11707  df-z 11793  df-uz 12058  df-q 12162  df-rp 12204  df-xneg 12323  df-xadd 12324  df-xmul 12325  df-ioo 12557  df-ico 12559  df-icc 12560  df-fz 12708  df-fzo 12849  df-fl 12976  df-seq 13184  df-exp 13244  df-hash 13505  df-cj 14318  df-re 14319  df-im 14320  df-sqrt 14454  df-abs 14455  df-clim 14705  df-sum 14903  df-rest 16551  df-topgen 16572  df-psmet 20255  df-xmet 20256  df-met 20257  df-bl 20258  df-mopn 20259  df-top 21222  df-topon 21239  df-bases 21274  df-cmp 21715  df-ovol 23784  df-vol 23785

This theorem is referenced by: (None)