Theorem volsupnfl 37635

Description: volsup 25507 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 4894	. . . . . . . . 9 ⊢ (𝐴 = ∅ → ∪ 𝐴 = ∪ ∅)
2		uni0 4911	. . . . . . . . 9 ⊢ ∪ ∅ = ∅
3	1, 2	eqtrdi 2786	. . . . . . . 8 ⊢ (𝐴 = ∅ → ∪ 𝐴 = ∅)
4	3	fveq2d 6879	. . . . . . 7 ⊢ (𝐴 = ∅ → (vol‘∪ 𝐴) = (vol‘∅))
5		0mbl 25490	. . . . . . . . 9 ⊢ ∅ ∈ dom vol
6		mblvol 25481	. . . . . . . . 9 ⊢ (∅ ∈ dom vol → (vol‘∅) = (vol*‘∅))
7	5, 6	ax-mp 5	. . . . . . . 8 ⊢ (vol‘∅) = (vol*‘∅)
8		ovol0 25444	. . . . . . . 8 ⊢ (vol*‘∅) = 0
9	7, 8	eqtri 2758	. . . . . . 7 ⊢ (vol‘∅) = 0
10	4, 9	eqtr2di 2787	. . . . . 6 ⊢ (𝐴 = ∅ → 0 = (vol‘∪ 𝐴))
11	10	a1d 25	. . . . 5 ⊢ (𝐴 = ∅ → ((𝐴 ≼ ℕ ∧ (∀𝑥 ∈ 𝐴 𝑥 ≼ ℕ ∧ ∪ 𝐴 ⊆ ℝ)) → 0 = (vol‘∪ 𝐴)))
12		reldom 8963	. . . . . . . . . . 11 ⊢ Rel ≼
13	12	brrelex1i 5710	. . . . . . . . . 10 ⊢ (𝐴 ≼ ℕ → 𝐴 ∈ V)
14		0sdomg 9116	. . . . . . . . . 10 ⊢ (𝐴 ∈ V → (∅ ≺ 𝐴 ↔ 𝐴 ≠ ∅))
15	13, 14	syl 17	. . . . . . . . 9 ⊢ (𝐴 ≼ ℕ → (∅ ≺ 𝐴 ↔ 𝐴 ≠ ∅))
16	15	biimparc 479	. . . . . . . 8 ⊢ ((𝐴 ≠ ∅ ∧ 𝐴 ≼ ℕ) → ∅ ≺ 𝐴)
17		fodomr 9140	. . . . . . . 8 ⊢ ((∅ ≺ 𝐴 ∧ 𝐴 ≼ ℕ) → ∃𝑔 𝑔:ℕ–onto→𝐴)
18	16, 17	sylancom 588	. . . . . . 7 ⊢ ((𝐴 ≠ ∅ ∧ 𝐴 ≼ ℕ) → ∃𝑔 𝑔:ℕ–onto→𝐴)
19		unissb 4915	. . . . . . . . . . . . 13 ⊢ (∪ 𝐴 ⊆ ℝ ↔ ∀𝑥 ∈ 𝐴 𝑥 ⊆ ℝ)
20	19	anbi1i 624	. . . . . . . . . . . 12 ⊢ ((∪ 𝐴 ⊆ ℝ ∧ ∀𝑥 ∈ 𝐴 𝑥 ≼ ℕ) ↔ (∀𝑥 ∈ 𝐴 𝑥 ⊆ ℝ ∧ ∀𝑥 ∈ 𝐴 𝑥 ≼ ℕ))
21		r19.26 3098	. . . . . . . . . . . 12 ⊢ (∀𝑥 ∈ 𝐴 (𝑥 ⊆ ℝ ∧ 𝑥 ≼ ℕ) ↔ (∀𝑥 ∈ 𝐴 𝑥 ⊆ ℝ ∧ ∀𝑥 ∈ 𝐴 𝑥 ≼ ℕ))
22	20, 21	bitr4i 278	. . . . . . . . . . 11 ⊢ ((∪ 𝐴 ⊆ ℝ ∧ ∀𝑥 ∈ 𝐴 𝑥 ≼ ℕ) ↔ ∀𝑥 ∈ 𝐴 (𝑥 ⊆ ℝ ∧ 𝑥 ≼ ℕ))
23		ovolctb2 25443	. . . . . . . . . . . . 13 ⊢ ((𝑥 ⊆ ℝ ∧ 𝑥 ≼ ℕ) → (vol*‘𝑥) = 0)
24		nulmbl 25486	. . . . . . . . . . . . . 14 ⊢ ((𝑥 ⊆ ℝ ∧ (vol*‘𝑥) = 0) → 𝑥 ∈ dom vol)
25		mblvol 25481	. . . . . . . . . . . . . . . 16 ⊢ (𝑥 ∈ dom vol → (vol‘𝑥) = (vol*‘𝑥))
26		eqtr 2755	. . . . . . . . . . . . . . . . 17 ⊢ (((vol‘𝑥) = (vol*‘𝑥) ∧ (vol*‘𝑥) = 0) → (vol‘𝑥) = 0)
27	26	expcom 413	. . . . . . . . . . . . . . . 16 ⊢ ((vol*‘𝑥) = 0 → ((vol‘𝑥) = (vol*‘𝑥) → (vol‘𝑥) = 0))
28	25, 27	syl5 34	. . . . . . . . . . . . . . 15 ⊢ ((vol*‘𝑥) = 0 → (𝑥 ∈ dom vol → (vol‘𝑥) = 0))
29	28	adantl 481	. . . . . . . . . . . . . 14 ⊢ ((𝑥 ⊆ ℝ ∧ (vol*‘𝑥) = 0) → (𝑥 ∈ dom vol → (vol‘𝑥) = 0))
30	24, 29	jcai 516	. . . . . . . . . . . . 13 ⊢ ((𝑥 ⊆ ℝ ∧ (vol*‘𝑥) = 0) → (𝑥 ∈ dom vol ∧ (vol‘𝑥) = 0))
31	23, 30	syldan 591	. . . . . . . . . . . 12 ⊢ ((𝑥 ⊆ ℝ ∧ 𝑥 ≼ ℕ) → (𝑥 ∈ dom vol ∧ (vol‘𝑥) = 0))
32	31	ralimi 3073	. . . . . . . . . . 11 ⊢ (∀𝑥 ∈ 𝐴 (𝑥 ⊆ ℝ ∧ 𝑥 ≼ ℕ) → ∀𝑥 ∈ 𝐴 (𝑥 ∈ dom vol ∧ (vol‘𝑥) = 0))
33	22, 32	sylbi 217	. . . . . . . . . 10 ⊢ ((∪ 𝐴 ⊆ ℝ ∧ ∀𝑥 ∈ 𝐴 𝑥 ≼ ℕ) → ∀𝑥 ∈ 𝐴 (𝑥 ∈ dom vol ∧ (vol‘𝑥) = 0))
34	33	ancoms 458	. . . . . . . . 9 ⊢ ((∀𝑥 ∈ 𝐴 𝑥 ≼ ℕ ∧ ∪ 𝐴 ⊆ ℝ) → ∀𝑥 ∈ 𝐴 (𝑥 ∈ dom vol ∧ (vol‘𝑥) = 0))
35		fzfi 13988	. . . . . . . . . . . . . . 15 ⊢ (1...𝑚) ∈ Fin
36		fzssuz 13580	. . . . . . . . . . . . . . . . 17 ⊢ (1...𝑚) ⊆ (ℤ≥‘1)
37		nnuz 12893	. . . . . . . . . . . . . . . . 17 ⊢ ℕ = (ℤ≥‘1)
38	36, 37	sseqtrri 4008	. . . . . . . . . . . . . . . 16 ⊢ (1...𝑚) ⊆ ℕ
39		fof 6789	. . . . . . . . . . . . . . . . . . . 20 ⊢ (𝑔:ℕ–onto→𝐴 → 𝑔:ℕ⟶𝐴)
40	39	ffvelcdmda 7073	. . . . . . . . . . . . . . . . . . 19 ⊢ ((𝑔:ℕ–onto→𝐴 ∧ 𝑙 ∈ ℕ) → (𝑔‘𝑙) ∈ 𝐴)
41		eleq1 2822	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ (𝑥 = (𝑔‘𝑙) → (𝑥 ∈ dom vol ↔ (𝑔‘𝑙) ∈ dom vol))
42		fveqeq2 6884	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ (𝑥 = (𝑔‘𝑙) → ((vol‘𝑥) = 0 ↔ (vol‘(𝑔‘𝑙)) = 0))
43	41, 42	anbi12d 632	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (𝑥 = (𝑔‘𝑙) → ((𝑥 ∈ dom vol ∧ (vol‘𝑥) = 0) ↔ ((𝑔‘𝑙) ∈ dom vol ∧ (vol‘(𝑔‘𝑙)) = 0)))
44	43	rspccva 3600	. . . . . . . . . . . . . . . . . . . . 21 ⊢ ((∀𝑥 ∈ 𝐴 (𝑥 ∈ dom vol ∧ (vol‘𝑥) = 0) ∧ (𝑔‘𝑙) ∈ 𝐴) → ((𝑔‘𝑙) ∈ dom vol ∧ (vol‘(𝑔‘𝑙)) = 0))
45	44	simpld 494	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((∀𝑥 ∈ 𝐴 (𝑥 ∈ dom vol ∧ (vol‘𝑥) = 0) ∧ (𝑔‘𝑙) ∈ 𝐴) → (𝑔‘𝑙) ∈ dom vol)
46	45	ancoms 458	. . . . . . . . . . . . . . . . . . 19 ⊢ (((𝑔‘𝑙) ∈ 𝐴 ∧ ∀𝑥 ∈ 𝐴 (𝑥 ∈ dom vol ∧ (vol‘𝑥) = 0)) → (𝑔‘𝑙) ∈ dom vol)
47	40, 46	sylan 580	. . . . . . . . . . . . . . . . . 18 ⊢ (((𝑔:ℕ–onto→𝐴 ∧ 𝑙 ∈ ℕ) ∧ ∀𝑥 ∈ 𝐴 (𝑥 ∈ dom vol ∧ (vol‘𝑥) = 0)) → (𝑔‘𝑙) ∈ dom vol)
48	47	an32s 652	. . . . . . . . . . . . . . . . 17 ⊢ (((𝑔:ℕ–onto→𝐴 ∧ ∀𝑥 ∈ 𝐴 (𝑥 ∈ dom vol ∧ (vol‘𝑥) = 0)) ∧ 𝑙 ∈ ℕ) → (𝑔‘𝑙) ∈ dom vol)
49	48	ralrimiva 3132	. . . . . . . . . . . . . . . 16 ⊢ ((𝑔:ℕ–onto→𝐴 ∧ ∀𝑥 ∈ 𝐴 (𝑥 ∈ dom vol ∧ (vol‘𝑥) = 0)) → ∀𝑙 ∈ ℕ (𝑔‘𝑙) ∈ dom vol)
50		ssralv 4027	. . . . . . . . . . . . . . . 16 ⊢ ((1...𝑚) ⊆ ℕ → (∀𝑙 ∈ ℕ (𝑔‘𝑙) ∈ dom vol → ∀𝑙 ∈ (1...𝑚)(𝑔‘𝑙) ∈ dom vol))
51	38, 49, 50	mpsyl 68	. . . . . . . . . . . . . . 15 ⊢ ((𝑔:ℕ–onto→𝐴 ∧ ∀𝑥 ∈ 𝐴 (𝑥 ∈ dom vol ∧ (vol‘𝑥) = 0)) → ∀𝑙 ∈ (1...𝑚)(𝑔‘𝑙) ∈ dom vol)
52		finiunmbl 25495	. . . . . . . . . . . . . . 15 ⊢ (((1...𝑚) ∈ Fin ∧ ∀𝑙 ∈ (1...𝑚)(𝑔‘𝑙) ∈ dom vol) → ∪ 𝑙 ∈ (1...𝑚)(𝑔‘𝑙) ∈ dom vol)
53	35, 51, 52	sylancr 587	. . . . . . . . . . . . . 14 ⊢ ((𝑔:ℕ–onto→𝐴 ∧ ∀𝑥 ∈ 𝐴 (𝑥 ∈ dom vol ∧ (vol‘𝑥) = 0)) → ∪ 𝑙 ∈ (1...𝑚)(𝑔‘𝑙) ∈ dom vol)
54	53	adantr 480	. . . . . . . . . . . . 13 ⊢ (((𝑔:ℕ–onto→𝐴 ∧ ∀𝑥 ∈ 𝐴 (𝑥 ∈ dom vol ∧ (vol‘𝑥) = 0)) ∧ 𝑚 ∈ ℕ) → ∪ 𝑙 ∈ (1...𝑚)(𝑔‘𝑙) ∈ dom vol)
55	54	fmpttd 7104	. . . . . . . . . . . 12 ⊢ ((𝑔:ℕ–onto→𝐴 ∧ ∀𝑥 ∈ 𝐴 (𝑥 ∈ dom vol ∧ (vol‘𝑥) = 0)) → (𝑚 ∈ ℕ ↦ ∪ 𝑙 ∈ (1...𝑚)(𝑔‘𝑙)):ℕ⟶dom vol)
56		fzssp1 13582	. . . . . . . . . . . . . . 15 ⊢ (1...𝑛) ⊆ (1...(𝑛 + 1))
57		iunss1 4982	. . . . . . . . . . . . . . 15 ⊢ ((1...𝑛) ⊆ (1...(𝑛 + 1)) → ∪ 𝑙 ∈ (1...𝑛)(𝑔‘𝑙) ⊆ ∪ 𝑙 ∈ (1...(𝑛 + 1))(𝑔‘𝑙))
58	56, 57	ax-mp 5	. . . . . . . . . . . . . 14 ⊢ ∪ 𝑙 ∈ (1...𝑛)(𝑔‘𝑙) ⊆ ∪ 𝑙 ∈ (1...(𝑛 + 1))(𝑔‘𝑙)
59		oveq2 7411	. . . . . . . . . . . . . . . . 17 ⊢ (𝑚 = 𝑛 → (1...𝑚) = (1...𝑛))
60	59	iuneq1d 4995	. . . . . . . . . . . . . . . 16 ⊢ (𝑚 = 𝑛 → ∪ 𝑙 ∈ (1...𝑚)(𝑔‘𝑙) = ∪ 𝑙 ∈ (1...𝑛)(𝑔‘𝑙))
61		eqid 2735	. . . . . . . . . . . . . . . 16 ⊢ (𝑚 ∈ ℕ ↦ ∪ 𝑙 ∈ (1...𝑚)(𝑔‘𝑙)) = (𝑚 ∈ ℕ ↦ ∪ 𝑙 ∈ (1...𝑚)(𝑔‘𝑙))
62		ovex 7436	. . . . . . . . . . . . . . . . 17 ⊢ (1...𝑛) ∈ V
63		fvex 6888	. . . . . . . . . . . . . . . . 17 ⊢ (𝑔‘𝑙) ∈ V
64	62, 63	iunex 7965	. . . . . . . . . . . . . . . 16 ⊢ ∪ 𝑙 ∈ (1...𝑛)(𝑔‘𝑙) ∈ V
65	60, 61, 64	fvmpt 6985	. . . . . . . . . . . . . . 15 ⊢ (𝑛 ∈ ℕ → ((𝑚 ∈ ℕ ↦ ∪ 𝑙 ∈ (1...𝑚)(𝑔‘𝑙))‘𝑛) = ∪ 𝑙 ∈ (1...𝑛)(𝑔‘𝑙))
66		peano2nn 12250	. . . . . . . . . . . . . . . 16 ⊢ (𝑛 ∈ ℕ → (𝑛 + 1) ∈ ℕ)
67		oveq2 7411	. . . . . . . . . . . . . . . . . 18 ⊢ (𝑚 = (𝑛 + 1) → (1...𝑚) = (1...(𝑛 + 1)))
68	67	iuneq1d 4995	. . . . . . . . . . . . . . . . 17 ⊢ (𝑚 = (𝑛 + 1) → ∪ 𝑙 ∈ (1...𝑚)(𝑔‘𝑙) = ∪ 𝑙 ∈ (1...(𝑛 + 1))(𝑔‘𝑙))
69		ovex 7436	. . . . . . . . . . . . . . . . . 18 ⊢ (1...(𝑛 + 1)) ∈ V
70	69, 63	iunex 7965	. . . . . . . . . . . . . . . . 17 ⊢ ∪ 𝑙 ∈ (1...(𝑛 + 1))(𝑔‘𝑙) ∈ V
71	68, 61, 70	fvmpt 6985	. . . . . . . . . . . . . . . 16 ⊢ ((𝑛 + 1) ∈ ℕ → ((𝑚 ∈ ℕ ↦ ∪ 𝑙 ∈ (1...𝑚)(𝑔‘𝑙))‘(𝑛 + 1)) = ∪ 𝑙 ∈ (1...(𝑛 + 1))(𝑔‘𝑙))
72	66, 71	syl 17	. . . . . . . . . . . . . . 15 ⊢ (𝑛 ∈ ℕ → ((𝑚 ∈ ℕ ↦ ∪ 𝑙 ∈ (1...𝑚)(𝑔‘𝑙))‘(𝑛 + 1)) = ∪ 𝑙 ∈ (1...(𝑛 + 1))(𝑔‘𝑙))
73	65, 72	sseq12d 3992	. . . . . . . . . . . . . 14 ⊢ (𝑛 ∈ ℕ → (((𝑚 ∈ ℕ ↦ ∪ 𝑙 ∈ (1...𝑚)(𝑔‘𝑙))‘𝑛) ⊆ ((𝑚 ∈ ℕ ↦ ∪ 𝑙 ∈ (1...𝑚)(𝑔‘𝑙))‘(𝑛 + 1)) ↔ ∪ 𝑙 ∈ (1...𝑛)(𝑔‘𝑙) ⊆ ∪ 𝑙 ∈ (1...(𝑛 + 1))(𝑔‘𝑙)))
74	58, 73	mpbiri 258	. . . . . . . . . . . . 13 ⊢ (𝑛 ∈ ℕ → ((𝑚 ∈ ℕ ↦ ∪ 𝑙 ∈ (1...𝑚)(𝑔‘𝑙))‘𝑛) ⊆ ((𝑚 ∈ ℕ ↦ ∪ 𝑙 ∈ (1...𝑚)(𝑔‘𝑙))‘(𝑛 + 1)))
75	74	rgen 3053	. . . . . . . . . . . 12 ⊢ ∀𝑛 ∈ ℕ ((𝑚 ∈ ℕ ↦ ∪ 𝑙 ∈ (1...𝑚)(𝑔‘𝑙))‘𝑛) ⊆ ((𝑚 ∈ ℕ ↦ ∪ 𝑙 ∈ (1...𝑚)(𝑔‘𝑙))‘(𝑛 + 1))
76		nnex 12244	. . . . . . . . . . . . . 14 ⊢ ℕ ∈ V
77	76	mptex 7214	. . . . . . . . . . . . 13 ⊢ (𝑚 ∈ ℕ ↦ ∪ 𝑙 ∈ (1...𝑚)(𝑔‘𝑙)) ∈ V
78		feq1 6685	. . . . . . . . . . . . . . 15 ⊢ (𝑓 = (𝑚 ∈ ℕ ↦ ∪ 𝑙 ∈ (1...𝑚)(𝑔‘𝑙)) → (𝑓:ℕ⟶dom vol ↔ (𝑚 ∈ ℕ ↦ ∪ 𝑙 ∈ (1...𝑚)(𝑔‘𝑙)):ℕ⟶dom vol))
79		fveq1 6874	. . . . . . . . . . . . . . . . 17 ⊢ (𝑓 = (𝑚 ∈ ℕ ↦ ∪ 𝑙 ∈ (1...𝑚)(𝑔‘𝑙)) → (𝑓‘𝑛) = ((𝑚 ∈ ℕ ↦ ∪ 𝑙 ∈ (1...𝑚)(𝑔‘𝑙))‘𝑛))
80		fveq1 6874	. . . . . . . . . . . . . . . . 17 ⊢ (𝑓 = (𝑚 ∈ ℕ ↦ ∪ 𝑙 ∈ (1...𝑚)(𝑔‘𝑙)) → (𝑓‘(𝑛 + 1)) = ((𝑚 ∈ ℕ ↦ ∪ 𝑙 ∈ (1...𝑚)(𝑔‘𝑙))‘(𝑛 + 1)))
81	79, 80	sseq12d 3992	. . . . . . . . . . . . . . . 16 ⊢ (𝑓 = (𝑚 ∈ ℕ ↦ ∪ 𝑙 ∈ (1...𝑚)(𝑔‘𝑙)) → ((𝑓‘𝑛) ⊆ (𝑓‘(𝑛 + 1)) ↔ ((𝑚 ∈ ℕ ↦ ∪ 𝑙 ∈ (1...𝑚)(𝑔‘𝑙))‘𝑛) ⊆ ((𝑚 ∈ ℕ ↦ ∪ 𝑙 ∈ (1...𝑚)(𝑔‘𝑙))‘(𝑛 + 1))))
82	81	ralbidv 3163	. . . . . . . . . . . . . . 15 ⊢ (𝑓 = (𝑚 ∈ ℕ ↦ ∪ 𝑙 ∈ (1...𝑚)(𝑔‘𝑙)) → (∀𝑛 ∈ ℕ (𝑓‘𝑛) ⊆ (𝑓‘(𝑛 + 1)) ↔ ∀𝑛 ∈ ℕ ((𝑚 ∈ ℕ ↦ ∪ 𝑙 ∈ (1...𝑚)(𝑔‘𝑙))‘𝑛) ⊆ ((𝑚 ∈ ℕ ↦ ∪ 𝑙 ∈ (1...𝑚)(𝑔‘𝑙))‘(𝑛 + 1))))
83	78, 82	anbi12d 632	. . . . . . . . . . . . . 14 ⊢ (𝑓 = (𝑚 ∈ ℕ ↦ ∪ 𝑙 ∈ (1...𝑚)(𝑔‘𝑙)) → ((𝑓:ℕ⟶dom vol ∧ ∀𝑛 ∈ ℕ (𝑓‘𝑛) ⊆ (𝑓‘(𝑛 + 1))) ↔ ((𝑚 ∈ ℕ ↦ ∪ 𝑙 ∈ (1...𝑚)(𝑔‘𝑙)):ℕ⟶dom vol ∧ ∀𝑛 ∈ ℕ ((𝑚 ∈ ℕ ↦ ∪ 𝑙 ∈ (1...𝑚)(𝑔‘𝑙))‘𝑛) ⊆ ((𝑚 ∈ ℕ ↦ ∪ 𝑙 ∈ (1...𝑚)(𝑔‘𝑙))‘(𝑛 + 1)))))
84		rneq 5916	. . . . . . . . . . . . . . . . 17 ⊢ (𝑓 = (𝑚 ∈ ℕ ↦ ∪ 𝑙 ∈ (1...𝑚)(𝑔‘𝑙)) → ran 𝑓 = ran (𝑚 ∈ ℕ ↦ ∪ 𝑙 ∈ (1...𝑚)(𝑔‘𝑙)))
85	84	unieqd 4896	. . . . . . . . . . . . . . . 16 ⊢ (𝑓 = (𝑚 ∈ ℕ ↦ ∪ 𝑙 ∈ (1...𝑚)(𝑔‘𝑙)) → ∪ ran 𝑓 = ∪ ran (𝑚 ∈ ℕ ↦ ∪ 𝑙 ∈ (1...𝑚)(𝑔‘𝑙)))
86	85	fveq2d 6879	. . . . . . . . . . . . . . 15 ⊢ (𝑓 = (𝑚 ∈ ℕ ↦ ∪ 𝑙 ∈ (1...𝑚)(𝑔‘𝑙)) → (vol‘∪ ran 𝑓) = (vol‘∪ ran (𝑚 ∈ ℕ ↦ ∪ 𝑙 ∈ (1...𝑚)(𝑔‘𝑙))))
87	84	imaeq2d 6047	. . . . . . . . . . . . . . . 16 ⊢ (𝑓 = (𝑚 ∈ ℕ ↦ ∪ 𝑙 ∈ (1...𝑚)(𝑔‘𝑙)) → (vol “ ran 𝑓) = (vol “ ran (𝑚 ∈ ℕ ↦ ∪ 𝑙 ∈ (1...𝑚)(𝑔‘𝑙))))
88	87	supeq1d 9456	. . . . . . . . . . . . . . 15 ⊢ (𝑓 = (𝑚 ∈ ℕ ↦ ∪ 𝑙 ∈ (1...𝑚)(𝑔‘𝑙)) → sup((vol “ ran 𝑓), ℝ*, < ) = sup((vol “ ran (𝑚 ∈ ℕ ↦ ∪ 𝑙 ∈ (1...𝑚)(𝑔‘𝑙))), ℝ*, < ))
89	86, 88	eqeq12d 2751	. . . . . . . . . . . . . 14 ⊢ (𝑓 = (𝑚 ∈ ℕ ↦ ∪ 𝑙 ∈ (1...𝑚)(𝑔‘𝑙)) → ((vol‘∪ ran 𝑓) = sup((vol “ ran 𝑓), ℝ*, < ) ↔ (vol‘∪ ran (𝑚 ∈ ℕ ↦ ∪ 𝑙 ∈ (1...𝑚)(𝑔‘𝑙))) = sup((vol “ ran (𝑚 ∈ ℕ ↦ ∪ 𝑙 ∈ (1...𝑚)(𝑔‘𝑙))), ℝ*, < )))
90	83, 89	imbi12d 344	. . . . . . . . . . . . 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 3537	. . . . . . . . . . . 12 ⊢ (((𝑚 ∈ ℕ ↦ ∪ 𝑙 ∈ (1...𝑚)(𝑔‘𝑙)):ℕ⟶dom vol ∧ ∀𝑛 ∈ ℕ ((𝑚 ∈ ℕ ↦ ∪ 𝑙 ∈ (1...𝑚)(𝑔‘𝑙))‘𝑛) ⊆ ((𝑚 ∈ ℕ ↦ ∪ 𝑙 ∈ (1...𝑚)(𝑔‘𝑙))‘(𝑛 + 1))) → (vol‘∪ ran (𝑚 ∈ ℕ ↦ ∪ 𝑙 ∈ (1...𝑚)(𝑔‘𝑙))) = sup((vol “ ran (𝑚 ∈ ℕ ↦ ∪ 𝑙 ∈ (1...𝑚)(𝑔‘𝑙))), ℝ*, < ))
93	55, 75, 92	sylancl 586	. . . . . . . . . . 11 ⊢ ((𝑔:ℕ–onto→𝐴 ∧ ∀𝑥 ∈ 𝐴 (𝑥 ∈ dom vol ∧ (vol‘𝑥) = 0)) → (vol‘∪ ran (𝑚 ∈ ℕ ↦ ∪ 𝑙 ∈ (1...𝑚)(𝑔‘𝑙))) = sup((vol “ ran (𝑚 ∈ ℕ ↦ ∪ 𝑙 ∈ (1...𝑚)(𝑔‘𝑙))), ℝ*, < ))
94		df-iun 4969	. . . . . . . . . . . . . . . 16 ⊢ ∪ 𝑥 ∈ ℕ (𝑔‘𝑥) = {𝑛 ∣ ∃𝑥 ∈ ℕ 𝑛 ∈ (𝑔‘𝑥)}
95		eluzfz2 13547	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ (𝑥 ∈ (ℤ≥‘1) → 𝑥 ∈ (1...𝑥))
96	95, 37	eleq2s 2852	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (𝑥 ∈ ℕ → 𝑥 ∈ (1...𝑥))
97		fveq2 6875	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ (𝑙 = 𝑥 → (𝑔‘𝑙) = (𝑔‘𝑥))
98	97	eleq2d 2820	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ (𝑙 = 𝑥 → (𝑛 ∈ (𝑔‘𝑙) ↔ 𝑛 ∈ (𝑔‘𝑥)))
99	98	rspcev 3601	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ ((𝑥 ∈ (1...𝑥) ∧ 𝑛 ∈ (𝑔‘𝑥)) → ∃𝑙 ∈ (1...𝑥)𝑛 ∈ (𝑔‘𝑙))
100	96, 99	sylan 580	. . . . . . . . . . . . . . . . . . . . 21 ⊢ ((𝑥 ∈ ℕ ∧ 𝑛 ∈ (𝑔‘𝑥)) → ∃𝑙 ∈ (1...𝑥)𝑛 ∈ (𝑔‘𝑙))
101		oveq2 7411	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ (𝑚 = 𝑥 → (1...𝑚) = (1...𝑥))
102	101	rexeqdv 3306	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (𝑚 = 𝑥 → (∃𝑙 ∈ (1...𝑚)𝑛 ∈ (𝑔‘𝑙) ↔ ∃𝑙 ∈ (1...𝑥)𝑛 ∈ (𝑔‘𝑙)))
103	102	rspcev 3601	. . . . . . . . . . . . . . . . . . . . 21 ⊢ ((𝑥 ∈ ℕ ∧ ∃𝑙 ∈ (1...𝑥)𝑛 ∈ (𝑔‘𝑙)) → ∃𝑚 ∈ ℕ ∃𝑙 ∈ (1...𝑚)𝑛 ∈ (𝑔‘𝑙))
104	100, 103	syldan 591	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((𝑥 ∈ ℕ ∧ 𝑛 ∈ (𝑔‘𝑥)) → ∃𝑚 ∈ ℕ ∃𝑙 ∈ (1...𝑚)𝑛 ∈ (𝑔‘𝑙))
105	104	rexlimiva 3133	. . . . . . . . . . . . . . . . . . 19 ⊢ (∃𝑥 ∈ ℕ 𝑛 ∈ (𝑔‘𝑥) → ∃𝑚 ∈ ℕ ∃𝑙 ∈ (1...𝑚)𝑛 ∈ (𝑔‘𝑙))
106		ssrexv 4028	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ ((1...𝑚) ⊆ ℕ → (∃𝑙 ∈ (1...𝑚)𝑛 ∈ (𝑔‘𝑙) → ∃𝑙 ∈ ℕ 𝑛 ∈ (𝑔‘𝑙)))
107	38, 106	ax-mp 5	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (∃𝑙 ∈ (1...𝑚)𝑛 ∈ (𝑔‘𝑙) → ∃𝑙 ∈ ℕ 𝑛 ∈ (𝑔‘𝑙))
108	98	cbvrexvw 3221	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (∃𝑙 ∈ ℕ 𝑛 ∈ (𝑔‘𝑙) ↔ ∃𝑥 ∈ ℕ 𝑛 ∈ (𝑔‘𝑥))
109	107, 108	sylib 218	. . . . . . . . . . . . . . . . . . . 20 ⊢ (∃𝑙 ∈ (1...𝑚)𝑛 ∈ (𝑔‘𝑙) → ∃𝑥 ∈ ℕ 𝑛 ∈ (𝑔‘𝑥))
110	109	rexlimivw 3137	. . . . . . . . . . . . . . . . . . 19 ⊢ (∃𝑚 ∈ ℕ ∃𝑙 ∈ (1...𝑚)𝑛 ∈ (𝑔‘𝑙) → ∃𝑥 ∈ ℕ 𝑛 ∈ (𝑔‘𝑥))
111	105, 110	impbii 209	. . . . . . . . . . . . . . . . . 18 ⊢ (∃𝑥 ∈ ℕ 𝑛 ∈ (𝑔‘𝑥) ↔ ∃𝑚 ∈ ℕ ∃𝑙 ∈ (1...𝑚)𝑛 ∈ (𝑔‘𝑙))
112		eliun 4971	. . . . . . . . . . . . . . . . . . 19 ⊢ (𝑛 ∈ ∪ 𝑙 ∈ (1...𝑚)(𝑔‘𝑙) ↔ ∃𝑙 ∈ (1...𝑚)𝑛 ∈ (𝑔‘𝑙))
113	112	rexbii 3083	. . . . . . . . . . . . . . . . . 18 ⊢ (∃𝑚 ∈ ℕ 𝑛 ∈ ∪ 𝑙 ∈ (1...𝑚)(𝑔‘𝑙) ↔ ∃𝑚 ∈ ℕ ∃𝑙 ∈ (1...𝑚)𝑛 ∈ (𝑔‘𝑙))
114	111, 113	bitr4i 278	. . . . . . . . . . . . . . . . 17 ⊢ (∃𝑥 ∈ ℕ 𝑛 ∈ (𝑔‘𝑥) ↔ ∃𝑚 ∈ ℕ 𝑛 ∈ ∪ 𝑙 ∈ (1...𝑚)(𝑔‘𝑙))
115	114	abbii 2802	. . . . . . . . . . . . . . . 16 ⊢ {𝑛 ∣ ∃𝑥 ∈ ℕ 𝑛 ∈ (𝑔‘𝑥)} = {𝑛 ∣ ∃𝑚 ∈ ℕ 𝑛 ∈ ∪ 𝑙 ∈ (1...𝑚)(𝑔‘𝑙)}
116	94, 115	eqtri 2758	. . . . . . . . . . . . . . 15 ⊢ ∪ 𝑥 ∈ ℕ (𝑔‘𝑥) = {𝑛 ∣ ∃𝑚 ∈ ℕ 𝑛 ∈ ∪ 𝑙 ∈ (1...𝑚)(𝑔‘𝑙)}
117		df-iun 4969	. . . . . . . . . . . . . . 15 ⊢ ∪ 𝑚 ∈ ℕ ∪ 𝑙 ∈ (1...𝑚)(𝑔‘𝑙) = {𝑛 ∣ ∃𝑚 ∈ ℕ 𝑛 ∈ ∪ 𝑙 ∈ (1...𝑚)(𝑔‘𝑙)}
118		ovex 7436	. . . . . . . . . . . . . . . . 17 ⊢ (1...𝑚) ∈ V
119	118, 63	iunex 7965	. . . . . . . . . . . . . . . 16 ⊢ ∪ 𝑙 ∈ (1...𝑚)(𝑔‘𝑙) ∈ V
120	119	dfiun3 5949	. . . . . . . . . . . . . . 15 ⊢ ∪ 𝑚 ∈ ℕ ∪ 𝑙 ∈ (1...𝑚)(𝑔‘𝑙) = ∪ ran (𝑚 ∈ ℕ ↦ ∪ 𝑙 ∈ (1...𝑚)(𝑔‘𝑙))
121	116, 117, 120	3eqtr2i 2764	. . . . . . . . . . . . . 14 ⊢ ∪ 𝑥 ∈ ℕ (𝑔‘𝑥) = ∪ ran (𝑚 ∈ ℕ ↦ ∪ 𝑙 ∈ (1...𝑚)(𝑔‘𝑙))
122		fofn 6791	. . . . . . . . . . . . . . . 16 ⊢ (𝑔:ℕ–onto→𝐴 → 𝑔 Fn ℕ)
123		fniunfv 7238	. . . . . . . . . . . . . . . 16 ⊢ (𝑔 Fn ℕ → ∪ 𝑥 ∈ ℕ (𝑔‘𝑥) = ∪ ran 𝑔)
124	122, 123	syl 17	. . . . . . . . . . . . . . 15 ⊢ (𝑔:ℕ–onto→𝐴 → ∪ 𝑥 ∈ ℕ (𝑔‘𝑥) = ∪ ran 𝑔)
125		forn 6792	. . . . . . . . . . . . . . . 16 ⊢ (𝑔:ℕ–onto→𝐴 → ran 𝑔 = 𝐴)
126	125	unieqd 4896	. . . . . . . . . . . . . . 15 ⊢ (𝑔:ℕ–onto→𝐴 → ∪ ran 𝑔 = ∪ 𝐴)
127	124, 126	eqtrd 2770	. . . . . . . . . . . . . 14 ⊢ (𝑔:ℕ–onto→𝐴 → ∪ 𝑥 ∈ ℕ (𝑔‘𝑥) = ∪ 𝐴)
128	121, 127	eqtr3id 2784	. . . . . . . . . . . . 13 ⊢ (𝑔:ℕ–onto→𝐴 → ∪ ran (𝑚 ∈ ℕ ↦ ∪ 𝑙 ∈ (1...𝑚)(𝑔‘𝑙)) = ∪ 𝐴)
129	128	fveq2d 6879	. . . . . . . . . . . 12 ⊢ (𝑔:ℕ–onto→𝐴 → (vol‘∪ ran (𝑚 ∈ ℕ ↦ ∪ 𝑙 ∈ (1...𝑚)(𝑔‘𝑙))) = (vol‘∪ 𝐴))
130	129	adantr 480	. . . . . . . . . . 11 ⊢ ((𝑔:ℕ–onto→𝐴 ∧ ∀𝑥 ∈ 𝐴 (𝑥 ∈ dom vol ∧ (vol‘𝑥) = 0)) → (vol‘∪ ran (𝑚 ∈ ℕ ↦ ∪ 𝑙 ∈ (1...𝑚)(𝑔‘𝑙))) = (vol‘∪ 𝐴))
131		rnco2 6242	. . . . . . . . . . . . . 14 ⊢ ran (vol ∘ (𝑚 ∈ ℕ ↦ ∪ 𝑙 ∈ (1...𝑚)(𝑔‘𝑙))) = (vol “ ran (𝑚 ∈ ℕ ↦ ∪ 𝑙 ∈ (1...𝑚)(𝑔‘𝑙)))
132		eqidd 2736	. . . . . . . . . . . . . . . . 17 ⊢ ((𝑔:ℕ–onto→𝐴 ∧ ∀𝑥 ∈ 𝐴 (𝑥 ∈ dom vol ∧ (vol‘𝑥) = 0)) → (𝑚 ∈ ℕ ↦ ∪ 𝑙 ∈ (1...𝑚)(𝑔‘𝑙)) = (𝑚 ∈ ℕ ↦ ∪ 𝑙 ∈ (1...𝑚)(𝑔‘𝑙)))
133		volf 25480	. . . . . . . . . . . . . . . . . . 19 ⊢ vol:dom vol⟶(0[,]+∞)
134	133	a1i 11	. . . . . . . . . . . . . . . . . 18 ⊢ ((𝑔:ℕ–onto→𝐴 ∧ ∀𝑥 ∈ 𝐴 (𝑥 ∈ dom vol ∧ (vol‘𝑥) = 0)) → vol:dom vol⟶(0[,]+∞))
135	134	feqmptd 6946	. . . . . . . . . . . . . . . . 17 ⊢ ((𝑔:ℕ–onto→𝐴 ∧ ∀𝑥 ∈ 𝐴 (𝑥 ∈ dom vol ∧ (vol‘𝑥) = 0)) → vol = (𝑛 ∈ dom vol ↦ (vol‘𝑛)))
136		fveq2 6875	. . . . . . . . . . . . . . . . 17 ⊢ (𝑛 = ∪ 𝑙 ∈ (1...𝑚)(𝑔‘𝑙) → (vol‘𝑛) = (vol‘∪ 𝑙 ∈ (1...𝑚)(𝑔‘𝑙)))
137	54, 132, 135, 136	fmptco 7118	. . . . . . . . . . . . . . . 16 ⊢ ((𝑔:ℕ–onto→𝐴 ∧ ∀𝑥 ∈ 𝐴 (𝑥 ∈ dom vol ∧ (vol‘𝑥) = 0)) → (vol ∘ (𝑚 ∈ ℕ ↦ ∪ 𝑙 ∈ (1...𝑚)(𝑔‘𝑙))) = (𝑚 ∈ ℕ ↦ (vol‘∪ 𝑙 ∈ (1...𝑚)(𝑔‘𝑙))))
138		mblvol 25481	. . . . . . . . . . . . . . . . . . . 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 25482	. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 ⊢ (𝑥 ∈ dom vol → 𝑥 ⊆ ℝ)
141	140	adantr 480	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28 ⊢ ((𝑥 ∈ dom vol ∧ (vol‘𝑥) = 0) → 𝑥 ⊆ ℝ)
142	25	eqeq1d 2737	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 ⊢ (𝑥 ∈ dom vol → ((vol‘𝑥) = 0 ↔ (vol*‘𝑥) = 0))
143		0re 11235	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 ⊢ 0 ∈ ℝ
144		eleq1a 2829	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 ⊢ (0 ∈ ℝ → ((vol*‘𝑥) = 0 → (vol*‘𝑥) ∈ ℝ))
145	143, 144	ax-mp 5	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 ⊢ ((vol*‘𝑥) = 0 → (vol*‘𝑥) ∈ ℝ)
146	142, 145	biimtrdi 253	. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 ⊢ (𝑥 ∈ dom vol → ((vol‘𝑥) = 0 → (vol*‘𝑥) ∈ ℝ))
147	146	imp 406	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28 ⊢ ((𝑥 ∈ dom vol ∧ (vol‘𝑥) = 0) → (vol*‘𝑥) ∈ ℝ)
148	141, 147	jca 511	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 ⊢ ((𝑥 ∈ dom vol ∧ (vol‘𝑥) = 0) → (𝑥 ⊆ ℝ ∧ (vol*‘𝑥) ∈ ℝ))
149	148	ralimi 3073	. . . . . . . . . . . . . . . . . . . . . . . . . 26 ⊢ (∀𝑥 ∈ 𝐴 (𝑥 ∈ dom vol ∧ (vol‘𝑥) = 0) → ∀𝑥 ∈ 𝐴 (𝑥 ⊆ ℝ ∧ (vol*‘𝑥) ∈ ℝ))
150	149	adantl 481	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ ((𝑔:ℕ–onto→𝐴 ∧ ∀𝑥 ∈ 𝐴 (𝑥 ∈ dom vol ∧ (vol‘𝑥) = 0)) → ∀𝑥 ∈ 𝐴 (𝑥 ⊆ ℝ ∧ (vol*‘𝑥) ∈ ℝ))
151		ssid 3981	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28 ⊢ ℕ ⊆ ℕ
152		sseq1 3984	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 ⊢ (𝑥 = (𝑔‘𝑙) → (𝑥 ⊆ ℝ ↔ (𝑔‘𝑙) ⊆ ℝ))
153		fveq2 6875	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 ⊢ (𝑥 = (𝑔‘𝑙) → (vol*‘𝑥) = (vol*‘(𝑔‘𝑙)))
154	153	eleq1d 2819	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 ⊢ (𝑥 = (𝑔‘𝑙) → ((vol*‘𝑥) ∈ ℝ ↔ (vol*‘(𝑔‘𝑙)) ∈ ℝ))
155	152, 154	anbi12d 632	. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 ⊢ (𝑥 = (𝑔‘𝑙) → ((𝑥 ⊆ ℝ ∧ (vol*‘𝑥) ∈ ℝ) ↔ ((𝑔‘𝑙) ⊆ ℝ ∧ (vol*‘(𝑔‘𝑙)) ∈ ℝ)))
156	155	ralima 7228	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28 ⊢ ((𝑔 Fn ℕ ∧ ℕ ⊆ ℕ) → (∀𝑥 ∈ (𝑔 “ ℕ)(𝑥 ⊆ ℝ ∧ (vol*‘𝑥) ∈ ℝ) ↔ ∀𝑙 ∈ ℕ ((𝑔‘𝑙) ⊆ ℝ ∧ (vol*‘(𝑔‘𝑙)) ∈ ℝ)))
157	122, 151, 156	sylancl 586	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 ⊢ (𝑔:ℕ–onto→𝐴 → (∀𝑥 ∈ (𝑔 “ ℕ)(𝑥 ⊆ ℝ ∧ (vol*‘𝑥) ∈ ℝ) ↔ ∀𝑙 ∈ ℕ ((𝑔‘𝑙) ⊆ ℝ ∧ (vol*‘(𝑔‘𝑙)) ∈ ℝ)))
158		foima 6794	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28 ⊢ (𝑔:ℕ–onto→𝐴 → (𝑔 “ ℕ) = 𝐴)
159	158	raleqdv 3305	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 ⊢ (𝑔:ℕ–onto→𝐴 → (∀𝑥 ∈ (𝑔 “ ℕ)(𝑥 ⊆ ℝ ∧ (vol*‘𝑥) ∈ ℝ) ↔ ∀𝑥 ∈ 𝐴 (𝑥 ⊆ ℝ ∧ (vol*‘𝑥) ∈ ℝ)))
160	157, 159	bitr3d 281	. . . . . . . . . . . . . . . . . . . . . . . . . 26 ⊢ (𝑔:ℕ–onto→𝐴 → (∀𝑙 ∈ ℕ ((𝑔‘𝑙) ⊆ ℝ ∧ (vol*‘(𝑔‘𝑙)) ∈ ℝ) ↔ ∀𝑥 ∈ 𝐴 (𝑥 ⊆ ℝ ∧ (vol*‘𝑥) ∈ ℝ)))
161	160	adantr 480	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ ((𝑔:ℕ–onto→𝐴 ∧ ∀𝑥 ∈ 𝐴 (𝑥 ∈ dom vol ∧ (vol‘𝑥) = 0)) → (∀𝑙 ∈ ℕ ((𝑔‘𝑙) ⊆ ℝ ∧ (vol*‘(𝑔‘𝑙)) ∈ ℝ) ↔ ∀𝑥 ∈ 𝐴 (𝑥 ⊆ ℝ ∧ (vol*‘𝑥) ∈ ℝ)))
162	150, 161	mpbird 257	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ ((𝑔:ℕ–onto→𝐴 ∧ ∀𝑥 ∈ 𝐴 (𝑥 ∈ dom vol ∧ (vol‘𝑥) = 0)) → ∀𝑙 ∈ ℕ ((𝑔‘𝑙) ⊆ ℝ ∧ (vol*‘(𝑔‘𝑙)) ∈ ℝ))
163		ssralv 4027	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ ((1...𝑚) ⊆ ℕ → (∀𝑙 ∈ ℕ ((𝑔‘𝑙) ⊆ ℝ ∧ (vol*‘(𝑔‘𝑙)) ∈ ℝ) → ∀𝑙 ∈ (1...𝑚)((𝑔‘𝑙) ⊆ ℝ ∧ (vol*‘(𝑔‘𝑙)) ∈ ℝ)))
164	38, 162, 163	mpsyl 68	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ ((𝑔:ℕ–onto→𝐴 ∧ ∀𝑥 ∈ 𝐴 (𝑥 ∈ dom vol ∧ (vol‘𝑥) = 0)) → ∀𝑙 ∈ (1...𝑚)((𝑔‘𝑙) ⊆ ℝ ∧ (vol*‘(𝑔‘𝑙)) ∈ ℝ))
165	164	adantr 480	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (((𝑔:ℕ–onto→𝐴 ∧ ∀𝑥 ∈ 𝐴 (𝑥 ∈ dom vol ∧ (vol‘𝑥) = 0)) ∧ 𝑚 ∈ ℕ) → ∀𝑙 ∈ (1...𝑚)((𝑔‘𝑙) ⊆ ℝ ∧ (vol*‘(𝑔‘𝑙)) ∈ ℝ))
166		ovolfiniun 25452	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (((1...𝑚) ∈ Fin ∧ ∀𝑙 ∈ (1...𝑚)((𝑔‘𝑙) ⊆ ℝ ∧ (vol*‘(𝑔‘𝑙)) ∈ ℝ)) → (vol*‘∪ 𝑙 ∈ (1...𝑚)(𝑔‘𝑙)) ≤ Σ𝑙 ∈ (1...𝑚)(vol*‘(𝑔‘𝑙)))
167	35, 165, 166	sylancr 587	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (((𝑔:ℕ–onto→𝐴 ∧ ∀𝑥 ∈ 𝐴 (𝑥 ∈ dom vol ∧ (vol‘𝑥) = 0)) ∧ 𝑚 ∈ ℕ) → (vol*‘∪ 𝑙 ∈ (1...𝑚)(𝑔‘𝑙)) ≤ Σ𝑙 ∈ (1...𝑚)(vol*‘(𝑔‘𝑙)))
168		mblvol 25481	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28 ⊢ ((𝑔‘𝑙) ∈ dom vol → (vol‘(𝑔‘𝑙)) = (vol*‘(𝑔‘𝑙)))
169	48, 168	syl 17	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 ⊢ (((𝑔:ℕ–onto→𝐴 ∧ ∀𝑥 ∈ 𝐴 (𝑥 ∈ dom vol ∧ (vol‘𝑥) = 0)) ∧ 𝑙 ∈ ℕ) → (vol‘(𝑔‘𝑙)) = (vol*‘(𝑔‘𝑙)))
170	44	simprd 495	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 ⊢ ((∀𝑥 ∈ 𝐴 (𝑥 ∈ dom vol ∧ (vol‘𝑥) = 0) ∧ (𝑔‘𝑙) ∈ 𝐴) → (vol‘(𝑔‘𝑙)) = 0)
171	40, 170	sylan2 593	. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 ⊢ ((∀𝑥 ∈ 𝐴 (𝑥 ∈ dom vol ∧ (vol‘𝑥) = 0) ∧ (𝑔:ℕ–onto→𝐴 ∧ 𝑙 ∈ ℕ)) → (vol‘(𝑔‘𝑙)) = 0)
172	171	ancoms 458	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28 ⊢ (((𝑔:ℕ–onto→𝐴 ∧ 𝑙 ∈ ℕ) ∧ ∀𝑥 ∈ 𝐴 (𝑥 ∈ dom vol ∧ (vol‘𝑥) = 0)) → (vol‘(𝑔‘𝑙)) = 0)
173	172	an32s 652	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 ⊢ (((𝑔:ℕ–onto→𝐴 ∧ ∀𝑥 ∈ 𝐴 (𝑥 ∈ dom vol ∧ (vol‘𝑥) = 0)) ∧ 𝑙 ∈ ℕ) → (vol‘(𝑔‘𝑙)) = 0)
174	169, 173	eqtr3d 2772	. . . . . . . . . . . . . . . . . . . . . . . . . 26 ⊢ (((𝑔:ℕ–onto→𝐴 ∧ ∀𝑥 ∈ 𝐴 (𝑥 ∈ dom vol ∧ (vol‘𝑥) = 0)) ∧ 𝑙 ∈ ℕ) → (vol*‘(𝑔‘𝑙)) = 0)
175	174	ralrimiva 3132	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ ((𝑔:ℕ–onto→𝐴 ∧ ∀𝑥 ∈ 𝐴 (𝑥 ∈ dom vol ∧ (vol‘𝑥) = 0)) → ∀𝑙 ∈ ℕ (vol*‘(𝑔‘𝑙)) = 0)
176		ssralv 4027	. . . . . . . . . . . . . . . . . . . . . . . . 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 480	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ (((𝑔:ℕ–onto→𝐴 ∧ ∀𝑥 ∈ 𝐴 (𝑥 ∈ dom vol ∧ (vol‘𝑥) = 0)) ∧ 𝑚 ∈ ℕ) → ∀𝑙 ∈ (1...𝑚)(vol*‘(𝑔‘𝑙)) = 0)
179	178	sumeq2d 15715	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (((𝑔:ℕ–onto→𝐴 ∧ ∀𝑥 ∈ 𝐴 (𝑥 ∈ dom vol ∧ (vol‘𝑥) = 0)) ∧ 𝑚 ∈ ℕ) → Σ𝑙 ∈ (1...𝑚)(vol*‘(𝑔‘𝑙)) = Σ𝑙 ∈ (1...𝑚)0)
180	35	olci 866	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ ((1...𝑚) ⊆ (ℤ≥‘1) ∨ (1...𝑚) ∈ Fin)
181		sumz 15736	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ (((1...𝑚) ⊆ (ℤ≥‘1) ∨ (1...𝑚) ∈ Fin) → Σ𝑙 ∈ (1...𝑚)0 = 0)
182	180, 181	ax-mp 5	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ Σ𝑙 ∈ (1...𝑚)0 = 0
183	179, 182	eqtrdi 2786	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (((𝑔:ℕ–onto→𝐴 ∧ ∀𝑥 ∈ 𝐴 (𝑥 ∈ dom vol ∧ (vol‘𝑥) = 0)) ∧ 𝑚 ∈ ℕ) → Σ𝑙 ∈ (1...𝑚)(vol*‘(𝑔‘𝑙)) = 0)
184	167, 183	breqtrd 5145	. . . . . . . . . . . . . . . . . . . 20 ⊢ (((𝑔:ℕ–onto→𝐴 ∧ ∀𝑥 ∈ 𝐴 (𝑥 ∈ dom vol ∧ (vol‘𝑥) = 0)) ∧ 𝑚 ∈ ℕ) → (vol*‘∪ 𝑙 ∈ (1...𝑚)(𝑔‘𝑙)) ≤ 0)
185		mblss 25482	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ ((𝑔‘𝑙) ∈ dom vol → (𝑔‘𝑙) ⊆ ℝ)
186	185	ralimi 3073	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ (∀𝑙 ∈ (1...𝑚)(𝑔‘𝑙) ∈ dom vol → ∀𝑙 ∈ (1...𝑚)(𝑔‘𝑙) ⊆ ℝ)
187	51, 186	syl 17	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ ((𝑔:ℕ–onto→𝐴 ∧ ∀𝑥 ∈ 𝐴 (𝑥 ∈ dom vol ∧ (vol‘𝑥) = 0)) → ∀𝑙 ∈ (1...𝑚)(𝑔‘𝑙) ⊆ ℝ)
188		iunss 5021	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ (∪ 𝑙 ∈ (1...𝑚)(𝑔‘𝑙) ⊆ ℝ ↔ ∀𝑙 ∈ (1...𝑚)(𝑔‘𝑙) ⊆ ℝ)
189	187, 188	sylibr 234	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ ((𝑔:ℕ–onto→𝐴 ∧ ∀𝑥 ∈ 𝐴 (𝑥 ∈ dom vol ∧ (vol‘𝑥) = 0)) → ∪ 𝑙 ∈ (1...𝑚)(𝑔‘𝑙) ⊆ ℝ)
190	189	adantr 480	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (((𝑔:ℕ–onto→𝐴 ∧ ∀𝑥 ∈ 𝐴 (𝑥 ∈ dom vol ∧ (vol‘𝑥) = 0)) ∧ 𝑚 ∈ ℕ) → ∪ 𝑙 ∈ (1...𝑚)(𝑔‘𝑙) ⊆ ℝ)
191		ovolge0 25432	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (∪ 𝑙 ∈ (1...𝑚)(𝑔‘𝑙) ⊆ ℝ → 0 ≤ (vol*‘∪ 𝑙 ∈ (1...𝑚)(𝑔‘𝑙)))
192	190, 191	syl 17	. . . . . . . . . . . . . . . . . . . 20 ⊢ (((𝑔:ℕ–onto→𝐴 ∧ ∀𝑥 ∈ 𝐴 (𝑥 ∈ dom vol ∧ (vol‘𝑥) = 0)) ∧ 𝑚 ∈ ℕ) → 0 ≤ (vol*‘∪ 𝑙 ∈ (1...𝑚)(𝑔‘𝑙)))
193		ovolcl 25429	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ (∪ 𝑙 ∈ (1...𝑚)(𝑔‘𝑙) ⊆ ℝ → (vol*‘∪ 𝑙 ∈ (1...𝑚)(𝑔‘𝑙)) ∈ ℝ*)
194	189, 193	syl 17	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ ((𝑔:ℕ–onto→𝐴 ∧ ∀𝑥 ∈ 𝐴 (𝑥 ∈ dom vol ∧ (vol‘𝑥) = 0)) → (vol*‘∪ 𝑙 ∈ (1...𝑚)(𝑔‘𝑙)) ∈ ℝ*)
195	194	adantr 480	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (((𝑔:ℕ–onto→𝐴 ∧ ∀𝑥 ∈ 𝐴 (𝑥 ∈ dom vol ∧ (vol‘𝑥) = 0)) ∧ 𝑚 ∈ ℕ) → (vol*‘∪ 𝑙 ∈ (1...𝑚)(𝑔‘𝑙)) ∈ ℝ*)
196		0xr 11280	. . . . . . . . . . . . . . . . . . . . 21 ⊢ 0 ∈ ℝ*
197		xrletri3 13168	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (((vol*‘∪ 𝑙 ∈ (1...𝑚)(𝑔‘𝑙)) ∈ ℝ* ∧ 0 ∈ ℝ*) → ((vol*‘∪ 𝑙 ∈ (1...𝑚)(𝑔‘𝑙)) = 0 ↔ ((vol*‘∪ 𝑙 ∈ (1...𝑚)(𝑔‘𝑙)) ≤ 0 ∧ 0 ≤ (vol*‘∪ 𝑙 ∈ (1...𝑚)(𝑔‘𝑙)))))
198	195, 196, 197	sylancl 586	. . . . . . . . . . . . . . . . . . . 20 ⊢ (((𝑔:ℕ–onto→𝐴 ∧ ∀𝑥 ∈ 𝐴 (𝑥 ∈ dom vol ∧ (vol‘𝑥) = 0)) ∧ 𝑚 ∈ ℕ) → ((vol*‘∪ 𝑙 ∈ (1...𝑚)(𝑔‘𝑙)) = 0 ↔ ((vol*‘∪ 𝑙 ∈ (1...𝑚)(𝑔‘𝑙)) ≤ 0 ∧ 0 ≤ (vol*‘∪ 𝑙 ∈ (1...𝑚)(𝑔‘𝑙)))))
199	184, 192, 198	mpbir2and 713	. . . . . . . . . . . . . . . . . . 19 ⊢ (((𝑔:ℕ–onto→𝐴 ∧ ∀𝑥 ∈ 𝐴 (𝑥 ∈ dom vol ∧ (vol‘𝑥) = 0)) ∧ 𝑚 ∈ ℕ) → (vol*‘∪ 𝑙 ∈ (1...𝑚)(𝑔‘𝑙)) = 0)
200	139, 199	eqtrd 2770	. . . . . . . . . . . . . . . . . 18 ⊢ (((𝑔:ℕ–onto→𝐴 ∧ ∀𝑥 ∈ 𝐴 (𝑥 ∈ dom vol ∧ (vol‘𝑥) = 0)) ∧ 𝑚 ∈ ℕ) → (vol‘∪ 𝑙 ∈ (1...𝑚)(𝑔‘𝑙)) = 0)
201	200	mpteq2dva 5214	. . . . . . . . . . . . . . . . 17 ⊢ ((𝑔:ℕ–onto→𝐴 ∧ ∀𝑥 ∈ 𝐴 (𝑥 ∈ dom vol ∧ (vol‘𝑥) = 0)) → (𝑚 ∈ ℕ ↦ (vol‘∪ 𝑙 ∈ (1...𝑚)(𝑔‘𝑙))) = (𝑚 ∈ ℕ ↦ 0))
202		fconstmpt 5716	. . . . . . . . . . . . . . . . 17 ⊢ (ℕ × {0}) = (𝑚 ∈ ℕ ↦ 0)
203	201, 202	eqtr4di 2788	. . . . . . . . . . . . . . . 16 ⊢ ((𝑔:ℕ–onto→𝐴 ∧ ∀𝑥 ∈ 𝐴 (𝑥 ∈ dom vol ∧ (vol‘𝑥) = 0)) → (𝑚 ∈ ℕ ↦ (vol‘∪ 𝑙 ∈ (1...𝑚)(𝑔‘𝑙))) = (ℕ × {0}))
204	137, 203	eqtrd 2770	. . . . . . . . . . . . . . 15 ⊢ ((𝑔:ℕ–onto→𝐴 ∧ ∀𝑥 ∈ 𝐴 (𝑥 ∈ dom vol ∧ (vol‘𝑥) = 0)) → (vol ∘ (𝑚 ∈ ℕ ↦ ∪ 𝑙 ∈ (1...𝑚)(𝑔‘𝑙))) = (ℕ × {0}))
205		frn 6712	. . . . . . . . . . . . . . . . 17 ⊢ ((𝑚 ∈ ℕ ↦ ∪ 𝑙 ∈ (1...𝑚)(𝑔‘𝑙)):ℕ⟶dom vol → ran (𝑚 ∈ ℕ ↦ ∪ 𝑙 ∈ (1...𝑚)(𝑔‘𝑙)) ⊆ dom vol)
206		ffn 6705	. . . . . . . . . . . . . . . . . . 19 ⊢ (vol:dom vol⟶(0[,]+∞) → vol Fn dom vol)
207	133, 206	ax-mp 5	. . . . . . . . . . . . . . . . . 18 ⊢ vol Fn dom vol
208	119, 61	fnmpti 6680	. . . . . . . . . . . . . . . . . 18 ⊢ (𝑚 ∈ ℕ ↦ ∪ 𝑙 ∈ (1...𝑚)(𝑔‘𝑙)) Fn ℕ
209		fnco 6655	. . . . . . . . . . . . . . . . . 18 ⊢ ((vol Fn dom vol ∧ (𝑚 ∈ ℕ ↦ ∪ 𝑙 ∈ (1...𝑚)(𝑔‘𝑙)) Fn ℕ ∧ ran (𝑚 ∈ ℕ ↦ ∪ 𝑙 ∈ (1...𝑚)(𝑔‘𝑙)) ⊆ dom vol) → (vol ∘ (𝑚 ∈ ℕ ↦ ∪ 𝑙 ∈ (1...𝑚)(𝑔‘𝑙))) Fn ℕ)
210	207, 208, 209	mp3an12 1453	. . . . . . . . . . . . . . . . 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 12249	. . . . . . . . . . . . . . . . 17 ⊢ 1 ∈ ℕ
213	212	ne0ii 4319	. . . . . . . . . . . . . . . 16 ⊢ ℕ ≠ ∅
214		fconst5 7197	. . . . . . . . . . . . . . . 16 ⊢ (((vol ∘ (𝑚 ∈ ℕ ↦ ∪ 𝑙 ∈ (1...𝑚)(𝑔‘𝑙))) Fn ℕ ∧ ℕ ≠ ∅) → ((vol ∘ (𝑚 ∈ ℕ ↦ ∪ 𝑙 ∈ (1...𝑚)(𝑔‘𝑙))) = (ℕ × {0}) ↔ ran (vol ∘ (𝑚 ∈ ℕ ↦ ∪ 𝑙 ∈ (1...𝑚)(𝑔‘𝑙))) = {0}))
215	211, 213, 214	sylancl 586	. . . . . . . . . . . . . . 15 ⊢ ((𝑔:ℕ–onto→𝐴 ∧ ∀𝑥 ∈ 𝐴 (𝑥 ∈ dom vol ∧ (vol‘𝑥) = 0)) → ((vol ∘ (𝑚 ∈ ℕ ↦ ∪ 𝑙 ∈ (1...𝑚)(𝑔‘𝑙))) = (ℕ × {0}) ↔ ran (vol ∘ (𝑚 ∈ ℕ ↦ ∪ 𝑙 ∈ (1...𝑚)(𝑔‘𝑙))) = {0}))
216	204, 215	mpbid 232	. . . . . . . . . . . . . 14 ⊢ ((𝑔:ℕ–onto→𝐴 ∧ ∀𝑥 ∈ 𝐴 (𝑥 ∈ dom vol ∧ (vol‘𝑥) = 0)) → ran (vol ∘ (𝑚 ∈ ℕ ↦ ∪ 𝑙 ∈ (1...𝑚)(𝑔‘𝑙))) = {0})
217	131, 216	eqtr3id 2784	. . . . . . . . . . . . 13 ⊢ ((𝑔:ℕ–onto→𝐴 ∧ ∀𝑥 ∈ 𝐴 (𝑥 ∈ dom vol ∧ (vol‘𝑥) = 0)) → (vol “ ran (𝑚 ∈ ℕ ↦ ∪ 𝑙 ∈ (1...𝑚)(𝑔‘𝑙))) = {0})
218	217	supeq1d 9456	. . . . . . . . . . . 12 ⊢ ((𝑔:ℕ–onto→𝐴 ∧ ∀𝑥 ∈ 𝐴 (𝑥 ∈ dom vol ∧ (vol‘𝑥) = 0)) → sup((vol “ ran (𝑚 ∈ ℕ ↦ ∪ 𝑙 ∈ (1...𝑚)(𝑔‘𝑙))), ℝ*, < ) = sup({0}, ℝ*, < ))
219		xrltso 13155	. . . . . . . . . . . . 13 ⊢ < Or ℝ*
220		supsn 9483	. . . . . . . . . . . . 13 ⊢ (( < Or ℝ* ∧ 0 ∈ ℝ*) → sup({0}, ℝ*, < ) = 0)
221	219, 196, 220	mp2an 692	. . . . . . . . . . . 12 ⊢ sup({0}, ℝ*, < ) = 0
222	218, 221	eqtrdi 2786	. . . . . . . . . . 11 ⊢ ((𝑔:ℕ–onto→𝐴 ∧ ∀𝑥 ∈ 𝐴 (𝑥 ∈ dom vol ∧ (vol‘𝑥) = 0)) → sup((vol “ ran (𝑚 ∈ ℕ ↦ ∪ 𝑙 ∈ (1...𝑚)(𝑔‘𝑙))), ℝ*, < ) = 0)
223	93, 130, 222	3eqtr3rd 2779	. . . . . . . . . 10 ⊢ ((𝑔:ℕ–onto→𝐴 ∧ ∀𝑥 ∈ 𝐴 (𝑥 ∈ dom vol ∧ (vol‘𝑥) = 0)) → 0 = (vol‘∪ 𝐴))
224	223	ex 412	. . . . . . . . 9 ⊢ (𝑔:ℕ–onto→𝐴 → (∀𝑥 ∈ 𝐴 (𝑥 ∈ dom vol ∧ (vol‘𝑥) = 0) → 0 = (vol‘∪ 𝐴)))
225	34, 224	syl5 34	. . . . . . . 8 ⊢ (𝑔:ℕ–onto→𝐴 → ((∀𝑥 ∈ 𝐴 𝑥 ≼ ℕ ∧ ∪ 𝐴 ⊆ ℝ) → 0 = (vol‘∪ 𝐴)))
226	225	exlimiv 1930	. . . . . . 7 ⊢ (∃𝑔 𝑔:ℕ–onto→𝐴 → ((∀𝑥 ∈ 𝐴 𝑥 ≼ ℕ ∧ ∪ 𝐴 ⊆ ℝ) → 0 = (vol‘∪ 𝐴)))
227	18, 226	syl 17	. . . . . 6 ⊢ ((𝐴 ≠ ∅ ∧ 𝐴 ≼ ℕ) → ((∀𝑥 ∈ 𝐴 𝑥 ≼ ℕ ∧ ∪ 𝐴 ⊆ ℝ) → 0 = (vol‘∪ 𝐴)))
228	227	expimpd 453	. . . . 5 ⊢ (𝐴 ≠ ∅ → ((𝐴 ≼ ℕ ∧ (∀𝑥 ∈ 𝐴 𝑥 ≼ ℕ ∧ ∪ 𝐴 ⊆ ℝ)) → 0 = (vol‘∪ 𝐴)))
229	11, 228	pm2.61ine 3015	. . . 4 ⊢ ((𝐴 ≼ ℕ ∧ (∀𝑥 ∈ 𝐴 𝑥 ≼ ℕ ∧ ∪ 𝐴 ⊆ ℝ)) → 0 = (vol‘∪ 𝐴))
230		renepnf 11281	. . . . . . 7 ⊢ (0 ∈ ℝ → 0 ≠ +∞)
231	143, 230	mp1i 13	. . . . . 6 ⊢ (∪ 𝐴 = ℝ → 0 ≠ +∞)
232		fveq2 6875	. . . . . . 7 ⊢ (∪ 𝐴 = ℝ → (vol‘∪ 𝐴) = (vol‘ℝ))
233		rembl 25491	. . . . . . . . 9 ⊢ ℝ ∈ dom vol
234		mblvol 25481	. . . . . . . . 9 ⊢ (ℝ ∈ dom vol → (vol‘ℝ) = (vol*‘ℝ))
235	233, 234	ax-mp 5	. . . . . . . 8 ⊢ (vol‘ℝ) = (vol*‘ℝ)
236		ovolre 25476	. . . . . . . 8 ⊢ (vol*‘ℝ) = +∞
237	235, 236	eqtri 2758	. . . . . . 7 ⊢ (vol‘ℝ) = +∞
238	232, 237	eqtrdi 2786	. . . . . 6 ⊢ (∪ 𝐴 = ℝ → (vol‘∪ 𝐴) = +∞)
239	231, 238	neeqtrrd 3006	. . . . 5 ⊢ (∪ 𝐴 = ℝ → 0 ≠ (vol‘∪ 𝐴))
240	239	necon2i 2966	. . . 4 ⊢ (0 = (vol‘∪ 𝐴) → ∪ 𝐴 ≠ ℝ)
241	229, 240	syl 17	. . 3 ⊢ ((𝐴 ≼ ℕ ∧ (∀𝑥 ∈ 𝐴 𝑥 ≼ ℕ ∧ ∪ 𝐴 ⊆ ℝ)) → ∪ 𝐴 ≠ ℝ)
242	241	expr 456	. 2 ⊢ ((𝐴 ≼ ℕ ∧ ∀𝑥 ∈ 𝐴 𝑥 ≼ ℕ) → (∪ 𝐴 ⊆ ℝ → ∪ 𝐴 ≠ ℝ))
243		eqimss 4017	. . 3 ⊢ (∪ 𝐴 = ℝ → ∪ 𝐴 ⊆ ℝ)
244	243	necon3bi 2958	. 2 ⊢ (¬ ∪ 𝐴 ⊆ ℝ → ∪ 𝐴 ≠ ℝ)
245	242, 244	pm2.61d1 180	1 ⊢ ((𝐴 ≼ ℕ ∧ ∀𝑥 ∈ 𝐴 𝑥 ≼ ℕ) → ∪ 𝐴 ≠ ℝ)

Syntax hints:   → wi 4   ↔ wb 206   ∧ wa 395   ∨ wo 847   = wceq 1540  ∃wex 1779   ∈ wcel 2108  {cab 2713   ≠ wne 2932  ∀wral 3051  ∃wrex 3060  Vcvv 3459   ⊆ wss 3926  ∅c0 4308  {csn 4601  ∪ cuni 4883  ∪ ciun 4967   class class class wbr 5119   ↦ cmpt 5201   Or wor 5560   × cxp 5652  dom cdm 5654  ran crn 5655   “ cima 5657   ∘ ccom 5658   Fn wfn 6525  ⟶wf 6526  –onto→wfo 6528  ‘cfv 6530  (class class class)co 7403   ≼ cdom 8955   ≺ csdm 8956  Fincfn 8957  supcsup 9450  ℝcr 11126  0cc0 11127  1c1 11128   + caddc 11130  +∞cpnf 11264  ℝ^*cxr 11266   < clt 11267   ≤ cle 11268  ℕcn 12238  ℤ_≥cuz 12850  [,]cicc 13363  ...cfz 13522  Σcsu 15700  vol*covol 25413  volcvol 25414

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1795  ax-4 1809  ax-5 1910  ax-6 1967  ax-7 2007  ax-8 2110  ax-9 2118  ax-10 2141  ax-11 2157  ax-12 2177  ax-ext 2707  ax-rep 5249  ax-sep 5266  ax-nul 5276  ax-pow 5335  ax-pr 5402  ax-un 7727  ax-inf2 9653  ax-cnex 11183  ax-resscn 11184  ax-1cn 11185  ax-icn 11186  ax-addcl 11187  ax-addrcl 11188  ax-mulcl 11189  ax-mulrcl 11190  ax-mulcom 11191  ax-addass 11192  ax-mulass 11193  ax-distr 11194  ax-i2m1 11195  ax-1ne0 11196  ax-1rid 11197  ax-rnegex 11198  ax-rrecex 11199  ax-cnre 11200  ax-pre-lttri 11201  ax-pre-lttrn 11202  ax-pre-ltadd 11203  ax-pre-mulgt0 11204  ax-pre-sup 11205

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 848  df-3or 1087  df-3an 1088  df-tru 1543  df-fal 1553  df-ex 1780  df-nf 1784  df-sb 2065  df-mo 2539  df-eu 2568  df-clab 2714  df-cleq 2727  df-clel 2809  df-nfc 2885  df-ne 2933  df-nel 3037  df-ral 3052  df-rex 3061  df-rmo 3359  df-reu 3360  df-rab 3416  df-v 3461  df-sbc 3766  df-csb 3875  df-dif 3929  df-un 3931  df-in 3933  df-ss 3943  df-pss 3946  df-nul 4309  df-if 4501  df-pw 4577  df-sn 4602  df-pr 4604  df-op 4608  df-uni 4884  df-int 4923  df-iun 4969  df-br 5120  df-opab 5182  df-mpt 5202  df-tr 5230  df-id 5548  df-eprel 5553  df-po 5561  df-so 5562  df-fr 5606  df-se 5607  df-we 5608  df-xp 5660  df-rel 5661  df-cnv 5662  df-co 5663  df-dm 5664  df-rn 5665  df-res 5666  df-ima 5667  df-pred 6290  df-ord 6355  df-on 6356  df-lim 6357  df-suc 6358  df-iota 6483  df-fun 6532  df-fn 6533  df-f 6534  df-f1 6535  df-fo 6536  df-f1o 6537  df-fv 6538  df-isom 6539  df-riota 7360  df-ov 7406  df-oprab 7407  df-mpo 7408  df-of 7669  df-om 7860  df-1st 7986  df-2nd 7987  df-frecs 8278  df-wrecs 8309  df-recs 8383  df-rdg 8422  df-1o 8478  df-2o 8479  df-er 8717  df-map 8840  df-en 8958  df-dom 8959  df-sdom 8960  df-fin 8961  df-fi 9421  df-sup 9452  df-inf 9453  df-oi 9522  df-dju 9913  df-card 9951  df-pnf 11269  df-mnf 11270  df-xr 11271  df-ltxr 11272  df-le 11273  df-sub 11466  df-neg 11467  df-div 11893  df-nn 12239  df-2 12301  df-3 12302  df-n0 12500  df-z 12587  df-uz 12851  df-q 12963  df-rp 13007  df-xneg 13126  df-xadd 13127  df-xmul 13128  df-ioo 13364  df-ico 13366  df-icc 13367  df-fz 13523  df-fzo 13670  df-fl 13807  df-seq 14018  df-exp 14078  df-hash 14347  df-cj 15116  df-re 15117  df-im 15118  df-sqrt 15252  df-abs 15253  df-clim 15502  df-sum 15701  df-rest 17434  df-topgen 17455  df-psmet 21305  df-xmet 21306  df-met 21307  df-bl 21308  df-mopn 21309  df-top 22830  df-topon 22847  df-bases 22882  df-cmp 23323  df-ovol 25415  df-vol 25416

This theorem is referenced by: (None)