Theorem volsupnfl 38584

Description: volsup 25877 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 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	. . . . . . . . . . . . 13 ⊢ ((𝑥 ⊆ ℝ ∧ 𝑥 ≼ ℕ) → (vol*‘𝑥) = 0)
24		nulmbl 25856	. . . . . . . . . . . . . 14 ⊢ ((𝑥 ⊆ ℝ ∧ (vol*‘𝑥) = 0) → 𝑥 ∈ dom vol)
25		mblvol 25851	. . . . . . . . . . . . . . . 16 ⊢ (𝑥 ∈ dom vol → (vol‘𝑥) = (vol*‘𝑥))
26		eqtr 2780	. . . . . . . . . . . . . . . . 17 ⊢ (((vol‘𝑥) = (vol*‘𝑥) ∧ (vol*‘𝑥) = 0) → (vol‘𝑥) = 0)
27	26	expcom 419	. . . . . . . . . . . . . . . 16 ⊢ ((vol*‘𝑥) = 0 → ((vol‘𝑥) = (vol*‘𝑥) → (vol‘𝑥) = 0))
28	25, 27	syl5 35	. . . . . . . . . . . . . . 15 ⊢ ((vol*‘𝑥) = 0 → (𝑥 ∈ dom vol → (vol‘𝑥) = 0))
29	28	adantl 487	. . . . . . . . . . . . . 14 ⊢ ((𝑥 ⊆ ℝ ∧ (vol*‘𝑥) = 0) → (𝑥 ∈ dom vol → (vol‘𝑥) = 0))
30	24, 29	jcai 526	. . . . . . . . . . . . 13 ⊢ ((𝑥 ⊆ ℝ ∧ (vol*‘𝑥) = 0) → (𝑥 ∈ dom vol ∧ (vol‘𝑥) = 0))
31	23, 30	syldan 603	. . . . . . . . . . . 12 ⊢ ((𝑥 ⊆ ℝ ∧ 𝑥 ≼ ℕ) → (𝑥 ∈ dom vol ∧ (vol‘𝑥) = 0))
32	31	ralimi 3099	. . . . . . . . . . 11 ⊢ (∀𝑥 ∈ 𝐴 (𝑥 ⊆ ℝ ∧ 𝑥 ≼ ℕ) → ∀𝑥 ∈ 𝐴 (𝑥 ∈ dom vol ∧ (vol‘𝑥) = 0))
33	22, 32	sylbi 220	. . . . . . . . . 10 ⊢ ((∪ 𝐴 ⊆ ℝ ∧ ∀𝑥 ∈ 𝐴 𝑥 ≼ ℕ) → ∀𝑥 ∈ 𝐴 (𝑥 ∈ dom vol ∧ (vol‘𝑥) = 0))
34	33	ancoms 464	. . . . . . . . 9 ⊢ ((∀𝑥 ∈ 𝐴 𝑥 ≼ ℕ ∧ ∪ 𝐴 ⊆ ℝ) → ∀𝑥 ∈ 𝐴 (𝑥 ∈ dom vol ∧ (vol‘𝑥) = 0))
35		fzfi 14115	. . . . . . . . . . . . . . 15 ⊢ (1...𝑚) ∈ Fin
36		fzssuz 13699	. . . . . . . . . . . . . . . . 17 ⊢ (1...𝑚) ⊆ (ℤ≥‘1)
37		nnuz 13004	. . . . . . . . . . . . . . . . 17 ⊢ ℕ = (ℤ≥‘1)
38	36, 37	sseqtrri 3957	. . . . . . . . . . . . . . . 16 ⊢ (1...𝑚) ⊆ ℕ
39		fof 6796	. . . . . . . . . . . . . . . . . . . 20 ⊢ (𝑔:ℕ–onto→𝐴 → 𝑔:ℕ⟶𝐴)
40	39	ffvelcdmda 7084	. . . . . . . . . . . . . . . . . . 19 ⊢ ((𝑔:ℕ–onto→𝐴 ∧ 𝑙 ∈ ℕ) → (𝑔‘𝑙) ∈ 𝐴)
41		eleq1 2848	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ (𝑥 = (𝑔‘𝑙) → (𝑥 ∈ dom vol ↔ (𝑔‘𝑙) ∈ dom vol))
42		fveqeq2 6894	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ (𝑥 = (𝑔‘𝑙) → ((vol‘𝑥) = 0 ↔ (vol‘(𝑔‘𝑙)) = 0))
43	41, 42	anbi12d 644	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (𝑥 = (𝑔‘𝑙) → ((𝑥 ∈ dom vol ∧ (vol‘𝑥) = 0) ↔ ((𝑔‘𝑙) ∈ dom vol ∧ (vol‘(𝑔‘𝑙)) = 0)))
44	43	rspccva 3575	. . . . . . . . . . . . . . . . . . . . 21 ⊢ ((∀𝑥 ∈ 𝐴 (𝑥 ∈ dom vol ∧ (vol‘𝑥) = 0) ∧ (𝑔‘𝑙) ∈ 𝐴) → ((𝑔‘𝑙) ∈ dom vol ∧ (vol‘(𝑔‘𝑙)) = 0))
45	44	simpld 500	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((∀𝑥 ∈ 𝐴 (𝑥 ∈ dom vol ∧ (vol‘𝑥) = 0) ∧ (𝑔‘𝑙) ∈ 𝐴) → (𝑔‘𝑙) ∈ dom vol)
46	45	ancoms 464	. . . . . . . . . . . . . . . . . . 19 ⊢ (((𝑔‘𝑙) ∈ 𝐴 ∧ ∀𝑥 ∈ 𝐴 (𝑥 ∈ dom vol ∧ (vol‘𝑥) = 0)) → (𝑔‘𝑙) ∈ dom vol)
47	40, 46	sylan 592	. . . . . . . . . . . . . . . . . 18 ⊢ (((𝑔:ℕ–onto→𝐴 ∧ 𝑙 ∈ ℕ) ∧ ∀𝑥 ∈ 𝐴 (𝑥 ∈ dom vol ∧ (vol‘𝑥) = 0)) → (𝑔‘𝑙) ∈ dom vol)
48	47	an32s 665	. . . . . . . . . . . . . . . . 17 ⊢ (((𝑔:ℕ–onto→𝐴 ∧ ∀𝑥 ∈ 𝐴 (𝑥 ∈ dom vol ∧ (vol‘𝑥) = 0)) ∧ 𝑙 ∈ ℕ) → (𝑔‘𝑙) ∈ dom vol)
49	48	ralrimiva 3154	. . . . . . . . . . . . . . . 16 ⊢ ((𝑔:ℕ–onto→𝐴 ∧ ∀𝑥 ∈ 𝐴 (𝑥 ∈ dom vol ∧ (vol‘𝑥) = 0)) → ∀𝑙 ∈ ℕ (𝑔‘𝑙) ∈ dom vol)
50		ssralv 3977	. . . . . . . . . . . . . . . 16 ⊢ ((1...𝑚) ⊆ ℕ → (∀𝑙 ∈ ℕ (𝑔‘𝑙) ∈ dom vol → ∀𝑙 ∈ (1...𝑚)(𝑔‘𝑙) ∈ dom vol))
51	38, 49, 50	mpsyl 69	. . . . . . . . . . . . . . 15 ⊢ ((𝑔:ℕ–onto→𝐴 ∧ ∀𝑥 ∈ 𝐴 (𝑥 ∈ dom vol ∧ (vol‘𝑥) = 0)) → ∀𝑙 ∈ (1...𝑚)(𝑔‘𝑙) ∈ dom vol)
52		finiunmbl 25865	. . . . . . . . . . . . . . 15 ⊢ (((1...𝑚) ∈ Fin ∧ ∀𝑙 ∈ (1...𝑚)(𝑔‘𝑙) ∈ dom vol) → ∪ 𝑙 ∈ (1...𝑚)(𝑔‘𝑙) ∈ dom vol)
53	35, 51, 52	sylancr 599	. . . . . . . . . . . . . 14 ⊢ ((𝑔:ℕ–onto→𝐴 ∧ ∀𝑥 ∈ 𝐴 (𝑥 ∈ dom vol ∧ (vol‘𝑥) = 0)) → ∪ 𝑙 ∈ (1...𝑚)(𝑔‘𝑙) ∈ dom vol)
54	53	adantr 486	. . . . . . . . . . . . 13 ⊢ (((𝑔:ℕ–onto→𝐴 ∧ ∀𝑥 ∈ 𝐴 (𝑥 ∈ dom vol ∧ (vol‘𝑥) = 0)) ∧ 𝑚 ∈ ℕ) → ∪ 𝑙 ∈ (1...𝑚)(𝑔‘𝑙) ∈ dom vol)
55	54	fmpttd 7115	. . . . . . . . . . . 12 ⊢ ((𝑔:ℕ–onto→𝐴 ∧ ∀𝑥 ∈ 𝐴 (𝑥 ∈ dom vol ∧ (vol‘𝑥) = 0)) → (𝑚 ∈ ℕ ↦ ∪ 𝑙 ∈ (1...𝑚)(𝑔‘𝑙)):ℕ⟶dom vol)
56		fzssp1 13701	. . . . . . . . . . . . . . 15 ⊢ (1...𝑛) ⊆ (1...(𝑛 + 1))
57		iunss1 4965	. . . . . . . . . . . . . . 15 ⊢ ((1...𝑛) ⊆ (1...(𝑛 + 1)) → ∪ 𝑙 ∈ (1...𝑛)(𝑔‘𝑙) ⊆ ∪ 𝑙 ∈ (1...(𝑛 + 1))(𝑔‘𝑙))
58	56, 57	ax-mp 5	. . . . . . . . . . . . . 14 ⊢ ∪ 𝑙 ∈ (1...𝑛)(𝑔‘𝑙) ⊆ ∪ 𝑙 ∈ (1...(𝑛 + 1))(𝑔‘𝑙)
59		oveq2 7428	. . . . . . . . . . . . . . . . 17 ⊢ (𝑚 = 𝑛 → (1...𝑚) = (1...𝑛))
60	59	iuneq1d 4978	. . . . . . . . . . . . . . . 16 ⊢ (𝑚 = 𝑛 → ∪ 𝑙 ∈ (1...𝑚)(𝑔‘𝑙) = ∪ 𝑙 ∈ (1...𝑛)(𝑔‘𝑙))
61		eqid 2760	. . . . . . . . . . . . . . . 16 ⊢ (𝑚 ∈ ℕ ↦ ∪ 𝑙 ∈ (1...𝑚)(𝑔‘𝑙)) = (𝑚 ∈ ℕ ↦ ∪ 𝑙 ∈ (1...𝑚)(𝑔‘𝑙))
62		ovex 7453	. . . . . . . . . . . . . . . . 17 ⊢ (1...𝑛) ∈ V
63		fvex 6898	. . . . . . . . . . . . . . . . 17 ⊢ (𝑔‘𝑙) ∈ V
64	62, 63	iunex 7980	. . . . . . . . . . . . . . . 16 ⊢ ∪ 𝑙 ∈ (1...𝑛)(𝑔‘𝑙) ∈ V
65	60, 61, 64	fvmpt 6993	. . . . . . . . . . . . . . 15 ⊢ (𝑛 ∈ ℕ → ((𝑚 ∈ ℕ ↦ ∪ 𝑙 ∈ (1...𝑚)(𝑔‘𝑙))‘𝑛) = ∪ 𝑙 ∈ (1...𝑛)(𝑔‘𝑙))
66		peano2nn 12347	. . . . . . . . . . . . . . . 16 ⊢ (𝑛 ∈ ℕ → (𝑛 + 1) ∈ ℕ)
67		oveq2 7428	. . . . . . . . . . . . . . . . . 18 ⊢ (𝑚 = (𝑛 + 1) → (1...𝑚) = (1...(𝑛 + 1)))
68	67	iuneq1d 4978	. . . . . . . . . . . . . . . . 17 ⊢ (𝑚 = (𝑛 + 1) → ∪ 𝑙 ∈ (1...𝑚)(𝑔‘𝑙) = ∪ 𝑙 ∈ (1...(𝑛 + 1))(𝑔‘𝑙))
69		ovex 7453	. . . . . . . . . . . . . . . . . 18 ⊢ (1...(𝑛 + 1)) ∈ V
70	69, 63	iunex 7980	. . . . . . . . . . . . . . . . 17 ⊢ ∪ 𝑙 ∈ (1...(𝑛 + 1))(𝑔‘𝑙) ∈ V
71	68, 61, 70	fvmpt 6993	. . . . . . . . . . . . . . . 16 ⊢ ((𝑛 + 1) ∈ ℕ → ((𝑚 ∈ ℕ ↦ ∪ 𝑙 ∈ (1...𝑚)(𝑔‘𝑙))‘(𝑛 + 1)) = ∪ 𝑙 ∈ (1...(𝑛 + 1))(𝑔‘𝑙))
72	66, 71	syl 18	. . . . . . . . . . . . . . 15 ⊢ (𝑛 ∈ ℕ → ((𝑚 ∈ ℕ ↦ ∪ 𝑙 ∈ (1...𝑚)(𝑔‘𝑙))‘(𝑛 + 1)) = ∪ 𝑙 ∈ (1...(𝑛 + 1))(𝑔‘𝑙))
73	65, 72	sseq12d 3941	. . . . . . . . . . . . . 14 ⊢ (𝑛 ∈ ℕ → (((𝑚 ∈ ℕ ↦ ∪ 𝑙 ∈ (1...𝑚)(𝑔‘𝑙))‘𝑛) ⊆ ((𝑚 ∈ ℕ ↦ ∪ 𝑙 ∈ (1...𝑚)(𝑔‘𝑙))‘(𝑛 + 1)) ↔ ∪ 𝑙 ∈ (1...𝑛)(𝑔‘𝑙) ⊆ ∪ 𝑙 ∈ (1...(𝑛 + 1))(𝑔‘𝑙)))
74	58, 73	mpbiri 261	. . . . . . . . . . . . 13 ⊢ (𝑛 ∈ ℕ → ((𝑚 ∈ ℕ ↦ ∪ 𝑙 ∈ (1...𝑚)(𝑔‘𝑙))‘𝑛) ⊆ ((𝑚 ∈ ℕ ↦ ∪ 𝑙 ∈ (1...𝑚)(𝑔‘𝑙))‘(𝑛 + 1)))
75	74	rgen 3078	. . . . . . . . . . . 12 ⊢ ∀𝑛 ∈ ℕ ((𝑚 ∈ ℕ ↦ ∪ 𝑙 ∈ (1...𝑚)(𝑔‘𝑙))‘𝑛) ⊆ ((𝑚 ∈ ℕ ↦ ∪ 𝑙 ∈ (1...𝑚)(𝑔‘𝑙))‘(𝑛 + 1))
76		nnex 12341	. . . . . . . . . . . . . 14 ⊢ ℕ ∈ V
77	76	mptex 7229	. . . . . . . . . . . . 13 ⊢ (𝑚 ∈ ℕ ↦ ∪ 𝑙 ∈ (1...𝑚)(𝑔‘𝑙)) ∈ V
78		feq1 6687	. . . . . . . . . . . . . . 15 ⊢ (𝑓 = (𝑚 ∈ ℕ ↦ ∪ 𝑙 ∈ (1...𝑚)(𝑔‘𝑙)) → (𝑓:ℕ⟶dom vol ↔ (𝑚 ∈ ℕ ↦ ∪ 𝑙 ∈ (1...𝑚)(𝑔‘𝑙)):ℕ⟶dom vol))
79		fveq1 6884	. . . . . . . . . . . . . . . . 17 ⊢ (𝑓 = (𝑚 ∈ ℕ ↦ ∪ 𝑙 ∈ (1...𝑚)(𝑔‘𝑙)) → (𝑓‘𝑛) = ((𝑚 ∈ ℕ ↦ ∪ 𝑙 ∈ (1...𝑚)(𝑔‘𝑙))‘𝑛))
80		fveq1 6884	. . . . . . . . . . . . . . . . 17 ⊢ (𝑓 = (𝑚 ∈ ℕ ↦ ∪ 𝑙 ∈ (1...𝑚)(𝑔‘𝑙)) → (𝑓‘(𝑛 + 1)) = ((𝑚 ∈ ℕ ↦ ∪ 𝑙 ∈ (1...𝑚)(𝑔‘𝑙))‘(𝑛 + 1)))
81	79, 80	sseq12d 3941	. . . . . . . . . . . . . . . 16 ⊢ (𝑓 = (𝑚 ∈ ℕ ↦ ∪ 𝑙 ∈ (1...𝑚)(𝑔‘𝑙)) → ((𝑓‘𝑛) ⊆ (𝑓‘(𝑛 + 1)) ↔ ((𝑚 ∈ ℕ ↦ ∪ 𝑙 ∈ (1...𝑚)(𝑔‘𝑙))‘𝑛) ⊆ ((𝑚 ∈ ℕ ↦ ∪ 𝑙 ∈ (1...𝑚)(𝑔‘𝑙))‘(𝑛 + 1))))
82	81	ralbidv 3185	. . . . . . . . . . . . . . 15 ⊢ (𝑓 = (𝑚 ∈ ℕ ↦ ∪ 𝑙 ∈ (1...𝑚)(𝑔‘𝑙)) → (∀𝑛 ∈ ℕ (𝑓‘𝑛) ⊆ (𝑓‘(𝑛 + 1)) ↔ ∀𝑛 ∈ ℕ ((𝑚 ∈ ℕ ↦ ∪ 𝑙 ∈ (1...𝑚)(𝑔‘𝑙))‘𝑛) ⊆ ((𝑚 ∈ ℕ ↦ ∪ 𝑙 ∈ (1...𝑚)(𝑔‘𝑙))‘(𝑛 + 1))))
83	78, 82	anbi12d 644	. . . . . . . . . . . . . 14 ⊢ (𝑓 = (𝑚 ∈ ℕ ↦ ∪ 𝑙 ∈ (1...𝑚)(𝑔‘𝑙)) → ((𝑓:ℕ⟶dom vol ∧ ∀𝑛 ∈ ℕ (𝑓‘𝑛) ⊆ (𝑓‘(𝑛 + 1))) ↔ ((𝑚 ∈ ℕ ↦ ∪ 𝑙 ∈ (1...𝑚)(𝑔‘𝑙)):ℕ⟶dom vol ∧ ∀𝑛 ∈ ℕ ((𝑚 ∈ ℕ ↦ ∪ 𝑙 ∈ (1...𝑚)(𝑔‘𝑙))‘𝑛) ⊆ ((𝑚 ∈ ℕ ↦ ∪ 𝑙 ∈ (1...𝑚)(𝑔‘𝑙))‘(𝑛 + 1)))))
84		rneq 5917	. . . . . . . . . . . . . . . . 17 ⊢ (𝑓 = (𝑚 ∈ ℕ ↦ ∪ 𝑙 ∈ (1...𝑚)(𝑔‘𝑙)) → ran 𝑓 = ran (𝑚 ∈ ℕ ↦ ∪ 𝑙 ∈ (1...𝑚)(𝑔‘𝑙)))
85	84	unieqd 4879	. . . . . . . . . . . . . . . 16 ⊢ (𝑓 = (𝑚 ∈ ℕ ↦ ∪ 𝑙 ∈ (1...𝑚)(𝑔‘𝑙)) → ∪ ran 𝑓 = ∪ ran (𝑚 ∈ ℕ ↦ ∪ 𝑙 ∈ (1...𝑚)(𝑔‘𝑙)))
86	85	fveq2d 6889	. . . . . . . . . . . . . . 15 ⊢ (𝑓 = (𝑚 ∈ ℕ ↦ ∪ 𝑙 ∈ (1...𝑚)(𝑔‘𝑙)) → (vol‘∪ ran 𝑓) = (vol‘∪ ran (𝑚 ∈ ℕ ↦ ∪ 𝑙 ∈ (1...𝑚)(𝑔‘𝑙))))
87	84	imaeq2d 6051	. . . . . . . . . . . . . . . 16 ⊢ (𝑓 = (𝑚 ∈ ℕ ↦ ∪ 𝑙 ∈ (1...𝑚)(𝑔‘𝑙)) → (vol “ ran 𝑓) = (vol “ ran (𝑚 ∈ ℕ ↦ ∪ 𝑙 ∈ (1...𝑚)(𝑔‘𝑙))))
88	87	supeq1d 9438	. . . . . . . . . . . . . . 15 ⊢ (𝑓 = (𝑚 ∈ ℕ ↦ ∪ 𝑙 ∈ (1...𝑚)(𝑔‘𝑙)) → sup((vol “ ran 𝑓), ℝ*, < ) = sup((vol “ ran (𝑚 ∈ ℕ ↦ ∪ 𝑙 ∈ (1...𝑚)(𝑔‘𝑙))), ℝ*, < ))
89	86, 88	eqeq12d 2776	. . . . . . . . . . . . . 14 ⊢ (𝑓 = (𝑚 ∈ ℕ ↦ ∪ 𝑙 ∈ (1...𝑚)(𝑔‘𝑙)) → ((vol‘∪ ran 𝑓) = sup((vol “ ran 𝑓), ℝ*, < ) ↔ (vol‘∪ ran (𝑚 ∈ ℕ ↦ ∪ 𝑙 ∈ (1...𝑚)(𝑔‘𝑙))) = sup((vol “ ran (𝑚 ∈ ℕ ↦ ∪ 𝑙 ∈ (1...𝑚)(𝑔‘𝑙))), ℝ*, < )))
90	83, 89	imbi12d 347	. . . . . . . . . . . . 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 3520	. . . . . . . . . . . 12 ⊢ (((𝑚 ∈ ℕ ↦ ∪ 𝑙 ∈ (1...𝑚)(𝑔‘𝑙)):ℕ⟶dom vol ∧ ∀𝑛 ∈ ℕ ((𝑚 ∈ ℕ ↦ ∪ 𝑙 ∈ (1...𝑚)(𝑔‘𝑙))‘𝑛) ⊆ ((𝑚 ∈ ℕ ↦ ∪ 𝑙 ∈ (1...𝑚)(𝑔‘𝑙))‘(𝑛 + 1))) → (vol‘∪ ran (𝑚 ∈ ℕ ↦ ∪ 𝑙 ∈ (1...𝑚)(𝑔‘𝑙))) = sup((vol “ ran (𝑚 ∈ ℕ ↦ ∪ 𝑙 ∈ (1...𝑚)(𝑔‘𝑙))), ℝ*, < ))
93	55, 75, 92	sylancl 598	. . . . . . . . . . 11 ⊢ ((𝑔:ℕ–onto→𝐴 ∧ ∀𝑥 ∈ 𝐴 (𝑥 ∈ dom vol ∧ (vol‘𝑥) = 0)) → (vol‘∪ ran (𝑚 ∈ ℕ ↦ ∪ 𝑙 ∈ (1...𝑚)(𝑔‘𝑙))) = sup((vol “ ran (𝑚 ∈ ℕ ↦ ∪ 𝑙 ∈ (1...𝑚)(𝑔‘𝑙))), ℝ*, < ))
94		df-iun 4952	. . . . . . . . . . . . . . . 16 ⊢ ∪ 𝑥 ∈ ℕ (𝑔‘𝑥) = {𝑛 ∣ ∃𝑥 ∈ ℕ 𝑛 ∈ (𝑔‘𝑥)}
95		eluzfz2 13665	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ (𝑥 ∈ (ℤ≥‘1) → 𝑥 ∈ (1...𝑥))
96	95, 37	eleq2s 2878	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (𝑥 ∈ ℕ → 𝑥 ∈ (1...𝑥))
97		fveq2 6885	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ (𝑙 = 𝑥 → (𝑔‘𝑙) = (𝑔‘𝑥))
98	97	eleq2d 2846	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ (𝑙 = 𝑥 → (𝑛 ∈ (𝑔‘𝑙) ↔ 𝑛 ∈ (𝑔‘𝑥)))
99	98	rspcev 3576	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ ((𝑥 ∈ (1...𝑥) ∧ 𝑛 ∈ (𝑔‘𝑥)) → ∃𝑙 ∈ (1...𝑥)𝑛 ∈ (𝑔‘𝑙))
100	96, 99	sylan 592	. . . . . . . . . . . . . . . . . . . . 21 ⊢ ((𝑥 ∈ ℕ ∧ 𝑛 ∈ (𝑔‘𝑥)) → ∃𝑙 ∈ (1...𝑥)𝑛 ∈ (𝑔‘𝑙))
101		oveq2 7428	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ (𝑚 = 𝑥 → (1...𝑚) = (1...𝑥))
102	101	rexeqdv 3320	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (𝑚 = 𝑥 → (∃𝑙 ∈ (1...𝑚)𝑛 ∈ (𝑔‘𝑙) ↔ ∃𝑙 ∈ (1...𝑥)𝑛 ∈ (𝑔‘𝑙)))
103	102	rspcev 3576	. . . . . . . . . . . . . . . . . . . . 21 ⊢ ((𝑥 ∈ ℕ ∧ ∃𝑙 ∈ (1...𝑥)𝑛 ∈ (𝑔‘𝑙)) → ∃𝑚 ∈ ℕ ∃𝑙 ∈ (1...𝑚)𝑛 ∈ (𝑔‘𝑙))
104	100, 103	syldan 603	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((𝑥 ∈ ℕ ∧ 𝑛 ∈ (𝑔‘𝑥)) → ∃𝑚 ∈ ℕ ∃𝑙 ∈ (1...𝑚)𝑛 ∈ (𝑔‘𝑙))
105	104	rexlimiva 3155	. . . . . . . . . . . . . . . . . . 19 ⊢ (∃𝑥 ∈ ℕ 𝑛 ∈ (𝑔‘𝑥) → ∃𝑚 ∈ ℕ ∃𝑙 ∈ (1...𝑚)𝑛 ∈ (𝑔‘𝑙))
106		ssrexv 3978	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ ((1...𝑚) ⊆ ℕ → (∃𝑙 ∈ (1...𝑚)𝑛 ∈ (𝑔‘𝑙) → ∃𝑙 ∈ ℕ 𝑛 ∈ (𝑔‘𝑙)))
107	38, 106	ax-mp 5	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (∃𝑙 ∈ (1...𝑚)𝑛 ∈ (𝑔‘𝑙) → ∃𝑙 ∈ ℕ 𝑛 ∈ (𝑔‘𝑙))
108	98	cbvrexvw 3241	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (∃𝑙 ∈ ℕ 𝑛 ∈ (𝑔‘𝑙) ↔ ∃𝑥 ∈ ℕ 𝑛 ∈ (𝑔‘𝑥))
109	107, 108	sylib 221	. . . . . . . . . . . . . . . . . . . 20 ⊢ (∃𝑙 ∈ (1...𝑚)𝑛 ∈ (𝑔‘𝑙) → ∃𝑥 ∈ ℕ 𝑛 ∈ (𝑔‘𝑥))
110	109	rexlimivw 3159	. . . . . . . . . . . . . . . . . . 19 ⊢ (∃𝑚 ∈ ℕ ∃𝑙 ∈ (1...𝑚)𝑛 ∈ (𝑔‘𝑙) → ∃𝑥 ∈ ℕ 𝑛 ∈ (𝑔‘𝑥))
111	105, 110	impbii 212	. . . . . . . . . . . . . . . . . 18 ⊢ (∃𝑥 ∈ ℕ 𝑛 ∈ (𝑔‘𝑥) ↔ ∃𝑚 ∈ ℕ ∃𝑙 ∈ (1...𝑚)𝑛 ∈ (𝑔‘𝑙))
112		eliun 4954	. . . . . . . . . . . . . . . . . . 19 ⊢ (𝑛 ∈ ∪ 𝑙 ∈ (1...𝑚)(𝑔‘𝑙) ↔ ∃𝑙 ∈ (1...𝑚)𝑛 ∈ (𝑔‘𝑙))
113	112	rexbii 3109	. . . . . . . . . . . . . . . . . 18 ⊢ (∃𝑚 ∈ ℕ 𝑛 ∈ ∪ 𝑙 ∈ (1...𝑚)(𝑔‘𝑙) ↔ ∃𝑚 ∈ ℕ ∃𝑙 ∈ (1...𝑚)𝑛 ∈ (𝑔‘𝑙))
114	111, 113	bitr4i 281	. . . . . . . . . . . . . . . . 17 ⊢ (∃𝑥 ∈ ℕ 𝑛 ∈ (𝑔‘𝑥) ↔ ∃𝑚 ∈ ℕ 𝑛 ∈ ∪ 𝑙 ∈ (1...𝑚)(𝑔‘𝑙))
115	114	abbii 2827	. . . . . . . . . . . . . . . 16 ⊢ {𝑛 ∣ ∃𝑥 ∈ ℕ 𝑛 ∈ (𝑔‘𝑥)} = {𝑛 ∣ ∃𝑚 ∈ ℕ 𝑛 ∈ ∪ 𝑙 ∈ (1...𝑚)(𝑔‘𝑙)}
116	94, 115	eqtri 2783	. . . . . . . . . . . . . . 15 ⊢ ∪ 𝑥 ∈ ℕ (𝑔‘𝑥) = {𝑛 ∣ ∃𝑚 ∈ ℕ 𝑛 ∈ ∪ 𝑙 ∈ (1...𝑚)(𝑔‘𝑙)}
117		df-iun 4952	. . . . . . . . . . . . . . 15 ⊢ ∪ 𝑚 ∈ ℕ ∪ 𝑙 ∈ (1...𝑚)(𝑔‘𝑙) = {𝑛 ∣ ∃𝑚 ∈ ℕ 𝑛 ∈ ∪ 𝑙 ∈ (1...𝑚)(𝑔‘𝑙)}
118		ovex 7453	. . . . . . . . . . . . . . . . 17 ⊢ (1...𝑚) ∈ V
119	118, 63	iunex 7980	. . . . . . . . . . . . . . . 16 ⊢ ∪ 𝑙 ∈ (1...𝑚)(𝑔‘𝑙) ∈ V
120	119	dfiun3 5951	. . . . . . . . . . . . . . 15 ⊢ ∪ 𝑚 ∈ ℕ ∪ 𝑙 ∈ (1...𝑚)(𝑔‘𝑙) = ∪ ran (𝑚 ∈ ℕ ↦ ∪ 𝑙 ∈ (1...𝑚)(𝑔‘𝑙))
121	116, 117, 120	3eqtr2i 2789	. . . . . . . . . . . . . 14 ⊢ ∪ 𝑥 ∈ ℕ (𝑔‘𝑥) = ∪ ran (𝑚 ∈ ℕ ↦ ∪ 𝑙 ∈ (1...𝑚)(𝑔‘𝑙))
122		fofn 6798	. . . . . . . . . . . . . . . 16 ⊢ (𝑔:ℕ–onto→𝐴 → 𝑔 Fn ℕ)
123		fniunfv 7251	. . . . . . . . . . . . . . . 16 ⊢ (𝑔 Fn ℕ → ∪ 𝑥 ∈ ℕ (𝑔‘𝑥) = ∪ ran 𝑔)
124	122, 123	syl 18	. . . . . . . . . . . . . . 15 ⊢ (𝑔:ℕ–onto→𝐴 → ∪ 𝑥 ∈ ℕ (𝑔‘𝑥) = ∪ ran 𝑔)
125		forn 6799	. . . . . . . . . . . . . . . 16 ⊢ (𝑔:ℕ–onto→𝐴 → ran 𝑔 = 𝐴)
126	125	unieqd 4879	. . . . . . . . . . . . . . 15 ⊢ (𝑔:ℕ–onto→𝐴 → ∪ ran 𝑔 = ∪ 𝐴)
127	124, 126	eqtrd 2795	. . . . . . . . . . . . . 14 ⊢ (𝑔:ℕ–onto→𝐴 → ∪ 𝑥 ∈ ℕ (𝑔‘𝑥) = ∪ 𝐴)
128	121, 127	eqtr3id 2809	. . . . . . . . . . . . 13 ⊢ (𝑔:ℕ–onto→𝐴 → ∪ ran (𝑚 ∈ ℕ ↦ ∪ 𝑙 ∈ (1...𝑚)(𝑔‘𝑙)) = ∪ 𝐴)
129	128	fveq2d 6889	. . . . . . . . . . . 12 ⊢ (𝑔:ℕ–onto→𝐴 → (vol‘∪ ran (𝑚 ∈ ℕ ↦ ∪ 𝑙 ∈ (1...𝑚)(𝑔‘𝑙))) = (vol‘∪ 𝐴))
130	129	adantr 486	. . . . . . . . . . 11 ⊢ ((𝑔:ℕ–onto→𝐴 ∧ ∀𝑥 ∈ 𝐴 (𝑥 ∈ dom vol ∧ (vol‘𝑥) = 0)) → (vol‘∪ ran (𝑚 ∈ ℕ ↦ ∪ 𝑙 ∈ (1...𝑚)(𝑔‘𝑙))) = (vol‘∪ 𝐴))
131		rnco2 6255	. . . . . . . . . . . . . 14 ⊢ ran (vol ∘ (𝑚 ∈ ℕ ↦ ∪ 𝑙 ∈ (1...𝑚)(𝑔‘𝑙))) = (vol “ ran (𝑚 ∈ ℕ ↦ ∪ 𝑙 ∈ (1...𝑚)(𝑔‘𝑙)))
132		eqidd 2761	. . . . . . . . . . . . . . . . 17 ⊢ ((𝑔:ℕ–onto→𝐴 ∧ ∀𝑥 ∈ 𝐴 (𝑥 ∈ dom vol ∧ (vol‘𝑥) = 0)) → (𝑚 ∈ ℕ ↦ ∪ 𝑙 ∈ (1...𝑚)(𝑔‘𝑙)) = (𝑚 ∈ ℕ ↦ ∪ 𝑙 ∈ (1...𝑚)(𝑔‘𝑙)))
133		volf 25850	. . . . . . . . . . . . . . . . . . 19 ⊢ vol:dom vol⟶(0[,]+∞)
134	133	a1i 11	. . . . . . . . . . . . . . . . . 18 ⊢ ((𝑔:ℕ–onto→𝐴 ∧ ∀𝑥 ∈ 𝐴 (𝑥 ∈ dom vol ∧ (vol‘𝑥) = 0)) → vol:dom vol⟶(0[,]+∞))
135	134	feqmptd 6953	. . . . . . . . . . . . . . . . 17 ⊢ ((𝑔:ℕ–onto→𝐴 ∧ ∀𝑥 ∈ 𝐴 (𝑥 ∈ dom vol ∧ (vol‘𝑥) = 0)) → vol = (𝑛 ∈ dom vol ↦ (vol‘𝑛)))
136		fveq2 6885	. . . . . . . . . . . . . . . . 17 ⊢ (𝑛 = ∪ 𝑙 ∈ (1...𝑚)(𝑔‘𝑙) → (vol‘𝑛) = (vol‘∪ 𝑙 ∈ (1...𝑚)(𝑔‘𝑙)))
137	54, 132, 135, 136	fmptco 7130	. . . . . . . . . . . . . . . 16 ⊢ ((𝑔:ℕ–onto→𝐴 ∧ ∀𝑥 ∈ 𝐴 (𝑥 ∈ dom vol ∧ (vol‘𝑥) = 0)) → (vol ∘ (𝑚 ∈ ℕ ↦ ∪ 𝑙 ∈ (1...𝑚)(𝑔‘𝑙))) = (𝑚 ∈ ℕ ↦ (vol‘∪ 𝑙 ∈ (1...𝑚)(𝑔‘𝑙))))
138		mblvol 25851	. . . . . . . . . . . . . . . . . . . 20 ⊢ (∪ 𝑙 ∈ (1...𝑚)(𝑔‘𝑙) ∈ dom vol → (vol‘∪ 𝑙 ∈ (1...𝑚)(𝑔‘𝑙)) = (vol*‘∪ 𝑙 ∈ (1...𝑚)(𝑔‘𝑙)))
139	54, 138	syl 18	. . . . . . . . . . . . . . . . . . 19 ⊢ (((𝑔:ℕ–onto→𝐴 ∧ ∀𝑥 ∈ 𝐴 (𝑥 ∈ dom vol ∧ (vol‘𝑥) = 0)) ∧ 𝑚 ∈ ℕ) → (vol‘∪ 𝑙 ∈ (1...𝑚)(𝑔‘𝑙)) = (vol*‘∪ 𝑙 ∈ (1...𝑚)(𝑔‘𝑙)))
140		mblss 25852	. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 ⊢ (𝑥 ∈ dom vol → 𝑥 ⊆ ℝ)
141	140	adantr 486	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28 ⊢ ((𝑥 ∈ dom vol ∧ (vol‘𝑥) = 0) → 𝑥 ⊆ ℝ)
142	25	eqeq1d 2762	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 ⊢ (𝑥 ∈ dom vol → ((vol‘𝑥) = 0 ↔ (vol*‘𝑥) = 0))
143		0re 11310	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 ⊢ 0 ∈ ℝ
144		eleq1a 2855	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 ⊢ (0 ∈ ℝ → ((vol*‘𝑥) = 0 → (vol*‘𝑥) ∈ ℝ))
145	143, 144	ax-mp 5	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 ⊢ ((vol*‘𝑥) = 0 → (vol*‘𝑥) ∈ ℝ)
146	142, 145	biimtrdi 256	. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 ⊢ (𝑥 ∈ dom vol → ((vol‘𝑥) = 0 → (vol*‘𝑥) ∈ ℝ))
147	146	imp 412	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28 ⊢ ((𝑥 ∈ dom vol ∧ (vol‘𝑥) = 0) → (vol*‘𝑥) ∈ ℝ)
148	141, 147	jca 521	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 ⊢ ((𝑥 ∈ dom vol ∧ (vol‘𝑥) = 0) → (𝑥 ⊆ ℝ ∧ (vol*‘𝑥) ∈ ℝ))
149	148	ralimi 3099	. . . . . . . . . . . . . . . . . . . . . . . . . 26 ⊢ (∀𝑥 ∈ 𝐴 (𝑥 ∈ dom vol ∧ (vol‘𝑥) = 0) → ∀𝑥 ∈ 𝐴 (𝑥 ⊆ ℝ ∧ (vol*‘𝑥) ∈ ℝ))
150	149	adantl 487	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ ((𝑔:ℕ–onto→𝐴 ∧ ∀𝑥 ∈ 𝐴 (𝑥 ∈ dom vol ∧ (vol‘𝑥) = 0)) → ∀𝑥 ∈ 𝐴 (𝑥 ⊆ ℝ ∧ (vol*‘𝑥) ∈ ℝ))
151		ssid 3930	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28 ⊢ ℕ ⊆ ℕ
152		sseq1 3933	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 ⊢ (𝑥 = (𝑔‘𝑙) → (𝑥 ⊆ ℝ ↔ (𝑔‘𝑙) ⊆ ℝ))
153		fveq2 6885	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 ⊢ (𝑥 = (𝑔‘𝑙) → (vol*‘𝑥) = (vol*‘(𝑔‘𝑙)))
154	153	eleq1d 2845	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 ⊢ (𝑥 = (𝑔‘𝑙) → ((vol*‘𝑥) ∈ ℝ ↔ (vol*‘(𝑔‘𝑙)) ∈ ℝ))
155	152, 154	anbi12d 644	. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 ⊢ (𝑥 = (𝑔‘𝑙) → ((𝑥 ⊆ ℝ ∧ (vol*‘𝑥) ∈ ℝ) ↔ ((𝑔‘𝑙) ⊆ ℝ ∧ (vol*‘(𝑔‘𝑙)) ∈ ℝ)))
156	155	ralima 7243	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28 ⊢ ((𝑔 Fn ℕ ∧ ℕ ⊆ ℕ) → (∀𝑥 ∈ (𝑔 “ ℕ)(𝑥 ⊆ ℝ ∧ (vol*‘𝑥) ∈ ℝ) ↔ ∀𝑙 ∈ ℕ ((𝑔‘𝑙) ⊆ ℝ ∧ (vol*‘(𝑔‘𝑙)) ∈ ℝ)))
157	122, 151, 156	sylancl 598	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 ⊢ (𝑔:ℕ–onto→𝐴 → (∀𝑥 ∈ (𝑔 “ ℕ)(𝑥 ⊆ ℝ ∧ (vol*‘𝑥) ∈ ℝ) ↔ ∀𝑙 ∈ ℕ ((𝑔‘𝑙) ⊆ ℝ ∧ (vol*‘(𝑔‘𝑙)) ∈ ℝ)))
158		foima 6801	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28 ⊢ (𝑔:ℕ–onto→𝐴 → (𝑔 “ ℕ) = 𝐴)
159	158	raleqdv 3319	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 ⊢ (𝑔:ℕ–onto→𝐴 → (∀𝑥 ∈ (𝑔 “ ℕ)(𝑥 ⊆ ℝ ∧ (vol*‘𝑥) ∈ ℝ) ↔ ∀𝑥 ∈ 𝐴 (𝑥 ⊆ ℝ ∧ (vol*‘𝑥) ∈ ℝ)))
160	157, 159	bitr3d 284	. . . . . . . . . . . . . . . . . . . . . . . . . 26 ⊢ (𝑔:ℕ–onto→𝐴 → (∀𝑙 ∈ ℕ ((𝑔‘𝑙) ⊆ ℝ ∧ (vol*‘(𝑔‘𝑙)) ∈ ℝ) ↔ ∀𝑥 ∈ 𝐴 (𝑥 ⊆ ℝ ∧ (vol*‘𝑥) ∈ ℝ)))
161	160	adantr 486	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ ((𝑔:ℕ–onto→𝐴 ∧ ∀𝑥 ∈ 𝐴 (𝑥 ∈ dom vol ∧ (vol‘𝑥) = 0)) → (∀𝑙 ∈ ℕ ((𝑔‘𝑙) ⊆ ℝ ∧ (vol*‘(𝑔‘𝑙)) ∈ ℝ) ↔ ∀𝑥 ∈ 𝐴 (𝑥 ⊆ ℝ ∧ (vol*‘𝑥) ∈ ℝ)))
162	150, 161	mpbird 260	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ ((𝑔:ℕ–onto→𝐴 ∧ ∀𝑥 ∈ 𝐴 (𝑥 ∈ dom vol ∧ (vol‘𝑥) = 0)) → ∀𝑙 ∈ ℕ ((𝑔‘𝑙) ⊆ ℝ ∧ (vol*‘(𝑔‘𝑙)) ∈ ℝ))
163		ssralv 3977	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ ((1...𝑚) ⊆ ℕ → (∀𝑙 ∈ ℕ ((𝑔‘𝑙) ⊆ ℝ ∧ (vol*‘(𝑔‘𝑙)) ∈ ℝ) → ∀𝑙 ∈ (1...𝑚)((𝑔‘𝑙) ⊆ ℝ ∧ (vol*‘(𝑔‘𝑙)) ∈ ℝ)))
164	38, 162, 163	mpsyl 69	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ ((𝑔:ℕ–onto→𝐴 ∧ ∀𝑥 ∈ 𝐴 (𝑥 ∈ dom vol ∧ (vol‘𝑥) = 0)) → ∀𝑙 ∈ (1...𝑚)((𝑔‘𝑙) ⊆ ℝ ∧ (vol*‘(𝑔‘𝑙)) ∈ ℝ))
165	164	adantr 486	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (((𝑔:ℕ–onto→𝐴 ∧ ∀𝑥 ∈ 𝐴 (𝑥 ∈ dom vol ∧ (vol‘𝑥) = 0)) ∧ 𝑚 ∈ ℕ) → ∀𝑙 ∈ (1...𝑚)((𝑔‘𝑙) ⊆ ℝ ∧ (vol*‘(𝑔‘𝑙)) ∈ ℝ))
166		ovolfiniun 25822	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (((1...𝑚) ∈ Fin ∧ ∀𝑙 ∈ (1...𝑚)((𝑔‘𝑙) ⊆ ℝ ∧ (vol*‘(𝑔‘𝑙)) ∈ ℝ)) → (vol*‘∪ 𝑙 ∈ (1...𝑚)(𝑔‘𝑙)) ≤ Σ𝑙 ∈ (1...𝑚)(vol*‘(𝑔‘𝑙)))
167	35, 165, 166	sylancr 599	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (((𝑔:ℕ–onto→𝐴 ∧ ∀𝑥 ∈ 𝐴 (𝑥 ∈ dom vol ∧ (vol‘𝑥) = 0)) ∧ 𝑚 ∈ ℕ) → (vol*‘∪ 𝑙 ∈ (1...𝑚)(𝑔‘𝑙)) ≤ Σ𝑙 ∈ (1...𝑚)(vol*‘(𝑔‘𝑙)))
168		mblvol 25851	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28 ⊢ ((𝑔‘𝑙) ∈ dom vol → (vol‘(𝑔‘𝑙)) = (vol*‘(𝑔‘𝑙)))
169	48, 168	syl 18	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 ⊢ (((𝑔:ℕ–onto→𝐴 ∧ ∀𝑥 ∈ 𝐴 (𝑥 ∈ dom vol ∧ (vol‘𝑥) = 0)) ∧ 𝑙 ∈ ℕ) → (vol‘(𝑔‘𝑙)) = (vol*‘(𝑔‘𝑙)))
170	44	simprd 501	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 ⊢ ((∀𝑥 ∈ 𝐴 (𝑥 ∈ dom vol ∧ (vol‘𝑥) = 0) ∧ (𝑔‘𝑙) ∈ 𝐴) → (vol‘(𝑔‘𝑙)) = 0)
171	40, 170	sylan2 605	. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 ⊢ ((∀𝑥 ∈ 𝐴 (𝑥 ∈ dom vol ∧ (vol‘𝑥) = 0) ∧ (𝑔:ℕ–onto→𝐴 ∧ 𝑙 ∈ ℕ)) → (vol‘(𝑔‘𝑙)) = 0)
172	171	ancoms 464	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28 ⊢ (((𝑔:ℕ–onto→𝐴 ∧ 𝑙 ∈ ℕ) ∧ ∀𝑥 ∈ 𝐴 (𝑥 ∈ dom vol ∧ (vol‘𝑥) = 0)) → (vol‘(𝑔‘𝑙)) = 0)
173	172	an32s 665	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 ⊢ (((𝑔:ℕ–onto→𝐴 ∧ ∀𝑥 ∈ 𝐴 (𝑥 ∈ dom vol ∧ (vol‘𝑥) = 0)) ∧ 𝑙 ∈ ℕ) → (vol‘(𝑔‘𝑙)) = 0)
174	169, 173	eqtr3d 2797	. . . . . . . . . . . . . . . . . . . . . . . . . 26 ⊢ (((𝑔:ℕ–onto→𝐴 ∧ ∀𝑥 ∈ 𝐴 (𝑥 ∈ dom vol ∧ (vol‘𝑥) = 0)) ∧ 𝑙 ∈ ℕ) → (vol*‘(𝑔‘𝑙)) = 0)
175	174	ralrimiva 3154	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ ((𝑔:ℕ–onto→𝐴 ∧ ∀𝑥 ∈ 𝐴 (𝑥 ∈ dom vol ∧ (vol‘𝑥) = 0)) → ∀𝑙 ∈ ℕ (vol*‘(𝑔‘𝑙)) = 0)
176		ssralv 3977	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ ((1...𝑚) ⊆ ℕ → (∀𝑙 ∈ ℕ (vol*‘(𝑔‘𝑙)) = 0 → ∀𝑙 ∈ (1...𝑚)(vol*‘(𝑔‘𝑙)) = 0))
177	38, 175, 176	mpsyl 69	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ ((𝑔:ℕ–onto→𝐴 ∧ ∀𝑥 ∈ 𝐴 (𝑥 ∈ dom vol ∧ (vol‘𝑥) = 0)) → ∀𝑙 ∈ (1...𝑚)(vol*‘(𝑔‘𝑙)) = 0)
178	177	adantr 486	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ (((𝑔:ℕ–onto→𝐴 ∧ ∀𝑥 ∈ 𝐴 (𝑥 ∈ dom vol ∧ (vol‘𝑥) = 0)) ∧ 𝑚 ∈ ℕ) → ∀𝑙 ∈ (1...𝑚)(vol*‘(𝑔‘𝑙)) = 0)
179	178	sumeq2d 15868	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (((𝑔:ℕ–onto→𝐴 ∧ ∀𝑥 ∈ 𝐴 (𝑥 ∈ dom vol ∧ (vol‘𝑥) = 0)) ∧ 𝑚 ∈ ℕ) → Σ𝑙 ∈ (1...𝑚)(vol*‘(𝑔‘𝑙)) = Σ𝑙 ∈ (1...𝑚)0)
180	35	olci 880	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ ((1...𝑚) ⊆ (ℤ≥‘1) ∨ (1...𝑚) ∈ Fin)
181		sumz 15888	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ (((1...𝑚) ⊆ (ℤ≥‘1) ∨ (1...𝑚) ∈ Fin) → Σ𝑙 ∈ (1...𝑚)0 = 0)
182	180, 181	ax-mp 5	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ Σ𝑙 ∈ (1...𝑚)0 = 0
183	179, 182	eqtrdi 2811	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (((𝑔:ℕ–onto→𝐴 ∧ ∀𝑥 ∈ 𝐴 (𝑥 ∈ dom vol ∧ (vol‘𝑥) = 0)) ∧ 𝑚 ∈ ℕ) → Σ𝑙 ∈ (1...𝑚)(vol*‘(𝑔‘𝑙)) = 0)
184	167, 183	breqtrd 5130	. . . . . . . . . . . . . . . . . . . 20 ⊢ (((𝑔:ℕ–onto→𝐴 ∧ ∀𝑥 ∈ 𝐴 (𝑥 ∈ dom vol ∧ (vol‘𝑥) = 0)) ∧ 𝑚 ∈ ℕ) → (vol*‘∪ 𝑙 ∈ (1...𝑚)(𝑔‘𝑙)) ≤ 0)
185		mblss 25852	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ ((𝑔‘𝑙) ∈ dom vol → (𝑔‘𝑙) ⊆ ℝ)
186	185	ralimi 3099	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ (∀𝑙 ∈ (1...𝑚)(𝑔‘𝑙) ∈ dom vol → ∀𝑙 ∈ (1...𝑚)(𝑔‘𝑙) ⊆ ℝ)
187	51, 186	syl 18	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ ((𝑔:ℕ–onto→𝐴 ∧ ∀𝑥 ∈ 𝐴 (𝑥 ∈ dom vol ∧ (vol‘𝑥) = 0)) → ∀𝑙 ∈ (1...𝑚)(𝑔‘𝑙) ⊆ ℝ)
188		iunss 5002	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ (∪ 𝑙 ∈ (1...𝑚)(𝑔‘𝑙) ⊆ ℝ ↔ ∀𝑙 ∈ (1...𝑚)(𝑔‘𝑙) ⊆ ℝ)
189	187, 188	sylibr 237	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ ((𝑔:ℕ–onto→𝐴 ∧ ∀𝑥 ∈ 𝐴 (𝑥 ∈ dom vol ∧ (vol‘𝑥) = 0)) → ∪ 𝑙 ∈ (1...𝑚)(𝑔‘𝑙) ⊆ ℝ)
190	189	adantr 486	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (((𝑔:ℕ–onto→𝐴 ∧ ∀𝑥 ∈ 𝐴 (𝑥 ∈ dom vol ∧ (vol‘𝑥) = 0)) ∧ 𝑚 ∈ ℕ) → ∪ 𝑙 ∈ (1...𝑚)(𝑔‘𝑙) ⊆ ℝ)
191		ovolge0 25802	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (∪ 𝑙 ∈ (1...𝑚)(𝑔‘𝑙) ⊆ ℝ → 0 ≤ (vol*‘∪ 𝑙 ∈ (1...𝑚)(𝑔‘𝑙)))
192	190, 191	syl 18	. . . . . . . . . . . . . . . . . . . 20 ⊢ (((𝑔:ℕ–onto→𝐴 ∧ ∀𝑥 ∈ 𝐴 (𝑥 ∈ dom vol ∧ (vol‘𝑥) = 0)) ∧ 𝑚 ∈ ℕ) → 0 ≤ (vol*‘∪ 𝑙 ∈ (1...𝑚)(𝑔‘𝑙)))
193		ovolcl 25799	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ (∪ 𝑙 ∈ (1...𝑚)(𝑔‘𝑙) ⊆ ℝ → (vol*‘∪ 𝑙 ∈ (1...𝑚)(𝑔‘𝑙)) ∈ ℝ*)
194	189, 193	syl 18	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ ((𝑔:ℕ–onto→𝐴 ∧ ∀𝑥 ∈ 𝐴 (𝑥 ∈ dom vol ∧ (vol‘𝑥) = 0)) → (vol*‘∪ 𝑙 ∈ (1...𝑚)(𝑔‘𝑙)) ∈ ℝ*)
195	194	adantr 486	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (((𝑔:ℕ–onto→𝐴 ∧ ∀𝑥 ∈ 𝐴 (𝑥 ∈ dom vol ∧ (vol‘𝑥) = 0)) ∧ 𝑚 ∈ ℕ) → (vol*‘∪ 𝑙 ∈ (1...𝑚)(𝑔‘𝑙)) ∈ ℝ*)
196		0xr 11356	. . . . . . . . . . . . . . . . . . . . 21 ⊢ 0 ∈ ℝ*
197		xrletri3 13283	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (((vol*‘∪ 𝑙 ∈ (1...𝑚)(𝑔‘𝑙)) ∈ ℝ* ∧ 0 ∈ ℝ*) → ((vol*‘∪ 𝑙 ∈ (1...𝑚)(𝑔‘𝑙)) = 0 ↔ ((vol*‘∪ 𝑙 ∈ (1...𝑚)(𝑔‘𝑙)) ≤ 0 ∧ 0 ≤ (vol*‘∪ 𝑙 ∈ (1...𝑚)(𝑔‘𝑙)))))
198	195, 196, 197	sylancl 598	. . . . . . . . . . . . . . . . . . . 20 ⊢ (((𝑔:ℕ–onto→𝐴 ∧ ∀𝑥 ∈ 𝐴 (𝑥 ∈ dom vol ∧ (vol‘𝑥) = 0)) ∧ 𝑚 ∈ ℕ) → ((vol*‘∪ 𝑙 ∈ (1...𝑚)(𝑔‘𝑙)) = 0 ↔ ((vol*‘∪ 𝑙 ∈ (1...𝑚)(𝑔‘𝑙)) ≤ 0 ∧ 0 ≤ (vol*‘∪ 𝑙 ∈ (1...𝑚)(𝑔‘𝑙)))))
199	184, 192, 198	mpbir2and 726	. . . . . . . . . . . . . . . . . . 19 ⊢ (((𝑔:ℕ–onto→𝐴 ∧ ∀𝑥 ∈ 𝐴 (𝑥 ∈ dom vol ∧ (vol‘𝑥) = 0)) ∧ 𝑚 ∈ ℕ) → (vol*‘∪ 𝑙 ∈ (1...𝑚)(𝑔‘𝑙)) = 0)
200	139, 199	eqtrd 2795	. . . . . . . . . . . . . . . . . 18 ⊢ (((𝑔:ℕ–onto→𝐴 ∧ ∀𝑥 ∈ 𝐴 (𝑥 ∈ dom vol ∧ (vol‘𝑥) = 0)) ∧ 𝑚 ∈ ℕ) → (vol‘∪ 𝑙 ∈ (1...𝑚)(𝑔‘𝑙)) = 0)
201	200	mpteq2dva 5197	. . . . . . . . . . . . . . . . 17 ⊢ ((𝑔:ℕ–onto→𝐴 ∧ ∀𝑥 ∈ 𝐴 (𝑥 ∈ dom vol ∧ (vol‘𝑥) = 0)) → (𝑚 ∈ ℕ ↦ (vol‘∪ 𝑙 ∈ (1...𝑚)(𝑔‘𝑙))) = (𝑚 ∈ ℕ ↦ 0))
202		fconstmpt 5712	. . . . . . . . . . . . . . . . 17 ⊢ (ℕ × {0}) = (𝑚 ∈ ℕ ↦ 0)
203	201, 202	eqtr4di 2813	. . . . . . . . . . . . . . . 16 ⊢ ((𝑔:ℕ–onto→𝐴 ∧ ∀𝑥 ∈ 𝐴 (𝑥 ∈ dom vol ∧ (vol‘𝑥) = 0)) → (𝑚 ∈ ℕ ↦ (vol‘∪ 𝑙 ∈ (1...𝑚)(𝑔‘𝑙))) = (ℕ × {0}))
204	137, 203	eqtrd 2795	. . . . . . . . . . . . . . 15 ⊢ ((𝑔:ℕ–onto→𝐴 ∧ ∀𝑥 ∈ 𝐴 (𝑥 ∈ dom vol ∧ (vol‘𝑥) = 0)) → (vol ∘ (𝑚 ∈ ℕ ↦ ∪ 𝑙 ∈ (1...𝑚)(𝑔‘𝑙))) = (ℕ × {0}))
205		frn 6717	. . . . . . . . . . . . . . . . 17 ⊢ ((𝑚 ∈ ℕ ↦ ∪ 𝑙 ∈ (1...𝑚)(𝑔‘𝑙)):ℕ⟶dom vol → ran (𝑚 ∈ ℕ ↦ ∪ 𝑙 ∈ (1...𝑚)(𝑔‘𝑙)) ⊆ dom vol)
206		ffn 6709	. . . . . . . . . . . . . . . . . . 19 ⊢ (vol:dom vol⟶(0[,]+∞) → vol Fn dom vol)
207	133, 206	ax-mp 5	. . . . . . . . . . . . . . . . . 18 ⊢ vol Fn dom vol
208	119, 61	fnmpti 6682	. . . . . . . . . . . . . . . . . 18 ⊢ (𝑚 ∈ ℕ ↦ ∪ 𝑙 ∈ (1...𝑚)(𝑔‘𝑙)) Fn ℕ
209		fnco 6657	. . . . . . . . . . . . . . . . . 18 ⊢ ((vol Fn dom vol ∧ (𝑚 ∈ ℕ ↦ ∪ 𝑙 ∈ (1...𝑚)(𝑔‘𝑙)) Fn ℕ ∧ ran (𝑚 ∈ ℕ ↦ ∪ 𝑙 ∈ (1...𝑚)(𝑔‘𝑙)) ⊆ dom vol) → (vol ∘ (𝑚 ∈ ℕ ↦ ∪ 𝑙 ∈ (1...𝑚)(𝑔‘𝑙))) Fn ℕ)
210	207, 208, 209	mp3an12 1480	. . . . . . . . . . . . . . . . 17 ⊢ (ran (𝑚 ∈ ℕ ↦ ∪ 𝑙 ∈ (1...𝑚)(𝑔‘𝑙)) ⊆ dom vol → (vol ∘ (𝑚 ∈ ℕ ↦ ∪ 𝑙 ∈ (1...𝑚)(𝑔‘𝑙))) Fn ℕ)
211	55, 205, 210	3syl 19	. . . . . . . . . . . . . . . 16 ⊢ ((𝑔:ℕ–onto→𝐴 ∧ ∀𝑥 ∈ 𝐴 (𝑥 ∈ dom vol ∧ (vol‘𝑥) = 0)) → (vol ∘ (𝑚 ∈ ℕ ↦ ∪ 𝑙 ∈ (1...𝑚)(𝑔‘𝑙))) Fn ℕ)
212		1nn 12346	. . . . . . . . . . . . . . . . 17 ⊢ 1 ∈ ℕ
213	212	ne0ii 4289	. . . . . . . . . . . . . . . 16 ⊢ ℕ ≠ ∅
214		fconst5 7212	. . . . . . . . . . . . . . . 16 ⊢ (((vol ∘ (𝑚 ∈ ℕ ↦ ∪ 𝑙 ∈ (1...𝑚)(𝑔‘𝑙))) Fn ℕ ∧ ℕ ≠ ∅) → ((vol ∘ (𝑚 ∈ ℕ ↦ ∪ 𝑙 ∈ (1...𝑚)(𝑔‘𝑙))) = (ℕ × {0}) ↔ ran (vol ∘ (𝑚 ∈ ℕ ↦ ∪ 𝑙 ∈ (1...𝑚)(𝑔‘𝑙))) = {0}))
215	211, 213, 214	sylancl 598	. . . . . . . . . . . . . . 15 ⊢ ((𝑔:ℕ–onto→𝐴 ∧ ∀𝑥 ∈ 𝐴 (𝑥 ∈ dom vol ∧ (vol‘𝑥) = 0)) → ((vol ∘ (𝑚 ∈ ℕ ↦ ∪ 𝑙 ∈ (1...𝑚)(𝑔‘𝑙))) = (ℕ × {0}) ↔ ran (vol ∘ (𝑚 ∈ ℕ ↦ ∪ 𝑙 ∈ (1...𝑚)(𝑔‘𝑙))) = {0}))
216	204, 215	mpbid 235	. . . . . . . . . . . . . 14 ⊢ ((𝑔:ℕ–onto→𝐴 ∧ ∀𝑥 ∈ 𝐴 (𝑥 ∈ dom vol ∧ (vol‘𝑥) = 0)) → ran (vol ∘ (𝑚 ∈ ℕ ↦ ∪ 𝑙 ∈ (1...𝑚)(𝑔‘𝑙))) = {0})
217	131, 216	eqtr3id 2809	. . . . . . . . . . . . 13 ⊢ ((𝑔:ℕ–onto→𝐴 ∧ ∀𝑥 ∈ 𝐴 (𝑥 ∈ dom vol ∧ (vol‘𝑥) = 0)) → (vol “ ran (𝑚 ∈ ℕ ↦ ∪ 𝑙 ∈ (1...𝑚)(𝑔‘𝑙))) = {0})
218	217	supeq1d 9438	. . . . . . . . . . . 12 ⊢ ((𝑔:ℕ–onto→𝐴 ∧ ∀𝑥 ∈ 𝐴 (𝑥 ∈ dom vol ∧ (vol‘𝑥) = 0)) → sup((vol “ ran (𝑚 ∈ ℕ ↦ ∪ 𝑙 ∈ (1...𝑚)(𝑔‘𝑙))), ℝ*, < ) = sup({0}, ℝ*, < ))
219		xrltso 13270	. . . . . . . . . . . . 13 ⊢ < Or ℝ*
220		supsn 9465	. . . . . . . . . . . . 13 ⊢ (( < Or ℝ* ∧ 0 ∈ ℝ*) → sup({0}, ℝ*, < ) = 0)
221	219, 196, 220	mp2an 705	. . . . . . . . . . . 12 ⊢ sup({0}, ℝ*, < ) = 0
222	218, 221	eqtrdi 2811	. . . . . . . . . . 11 ⊢ ((𝑔:ℕ–onto→𝐴 ∧ ∀𝑥 ∈ 𝐴 (𝑥 ∈ dom vol ∧ (vol‘𝑥) = 0)) → sup((vol “ ran (𝑚 ∈ ℕ ↦ ∪ 𝑙 ∈ (1...𝑚)(𝑔‘𝑙))), ℝ*, < ) = 0)
223	93, 130, 222	3eqtr3rd 2804	. . . . . . . . . 10 ⊢ ((𝑔:ℕ–onto→𝐴 ∧ ∀𝑥 ∈ 𝐴 (𝑥 ∈ dom vol ∧ (vol‘𝑥) = 0)) → 0 = (vol‘∪ 𝐴))
224	223	ex 418	. . . . . . . . 9 ⊢ (𝑔:ℕ–onto→𝐴 → (∀𝑥 ∈ 𝐴 (𝑥 ∈ dom vol ∧ (vol‘𝑥) = 0) → 0 = (vol‘∪ 𝐴)))
225	34, 224	syl5 35	. . . . . . . 8 ⊢ (𝑔:ℕ–onto→𝐴 → ((∀𝑥 ∈ 𝐴 𝑥 ≼ ℕ ∧ ∪ 𝐴 ⊆ ℝ) → 0 = (vol‘∪ 𝐴)))
226	225	exlimiv 1962	. . . . . . 7 ⊢ (∃𝑔 𝑔:ℕ–onto→𝐴 → ((∀𝑥 ∈ 𝐴 𝑥 ≼ ℕ ∧ ∪ 𝐴 ⊆ ℝ) → 0 = (vol‘∪ 𝐴)))
227	18, 226	syl 18	. . . . . 6 ⊢ ((𝐴 ≠ ∅ ∧ 𝐴 ≼ ℕ) → ((∀𝑥 ∈ 𝐴 𝑥 ≼ ℕ ∧ ∪ 𝐴 ⊆ ℝ) → 0 = (vol‘∪ 𝐴)))
228	227	expimpd 459	. . . . 5 ⊢ (𝐴 ≠ ∅ → ((𝐴 ≼ ℕ ∧ (∀𝑥 ∈ 𝐴 𝑥 ≼ ℕ ∧ ∪ 𝐴 ⊆ ℝ)) → 0 = (vol‘∪ 𝐴)))
229	11, 228	pm2.61ine 3038	. . . 4 ⊢ ((𝐴 ≼ ℕ ∧ (∀𝑥 ∈ 𝐴 𝑥 ≼ ℕ ∧ ∪ 𝐴 ⊆ ℝ)) → 0 = (vol‘∪ 𝐴))
230		renepnf 11357	. . . . . . 7 ⊢ (0 ∈ ℝ → 0 ≠ +∞)
231	143, 230	mp1i 14	. . . . . 6 ⊢ (∪ 𝐴 = ℝ → 0 ≠ +∞)
232		fveq2 6885	. . . . . . 7 ⊢ (∪ 𝐴 = ℝ → (vol‘∪ 𝐴) = (vol‘ℝ))
233		rembl 25861	. . . . . . . . 9 ⊢ ℝ ∈ dom vol
234		mblvol 25851	. . . . . . . . 9 ⊢ (ℝ ∈ dom vol → (vol‘ℝ) = (vol*‘ℝ))
235	233, 234	ax-mp 5	. . . . . . . 8 ⊢ (vol‘ℝ) = (vol*‘ℝ)
236		ovolre 25846	. . . . . . . 8 ⊢ (vol*‘ℝ) = +∞
237	235, 236	eqtri 2783	. . . . . . 7 ⊢ (vol‘ℝ) = +∞
238	232, 237	eqtrdi 2811	. . . . . 6 ⊢ (∪ 𝐴 = ℝ → (vol‘∪ 𝐴) = +∞)
239	231, 238	neeqtrrd 3029	. . . . 5 ⊢ (∪ 𝐴 = ℝ → 0 ≠ (vol‘∪ 𝐴))
240	239	necon2i 2989	. . . 4 ⊢ (0 = (vol‘∪ 𝐴) → ∪ 𝐴 ≠ ℝ)
241	229, 240	syl 18	. . 3 ⊢ ((𝐴 ≼ ℕ ∧ (∀𝑥 ∈ 𝐴 𝑥 ≼ ℕ ∧ ∪ 𝐴 ⊆ ℝ)) → ∪ 𝐴 ≠ ℝ)
242	241	expr 462	. 2 ⊢ ((𝐴 ≼ ℕ ∧ ∀𝑥 ∈ 𝐴 𝑥 ≼ ℕ) → (∪ 𝐴 ⊆ ℝ → ∪ 𝐴 ≠ ℝ))
243		eqimss 3966	. . 3 ⊢ (∪ 𝐴 = ℝ → ∪ 𝐴 ⊆ ℝ)
244	243	necon3bi 2981	. 2 ⊢ (¬ ∪ 𝐴 ⊆ ℝ → ∪ 𝐴 ≠ ℝ)
245	242, 244	pm2.61d1 182	1 ⊢ ((𝐴 ≼ ℕ ∧ ∀𝑥 ∈ 𝐴 𝑥 ≼ ℕ) → ∪ 𝐴 ≠ ℝ)

This proof depends on syntax axioms:   → wi 4   ↔ wb 209   ∧ wa 401   ∨ wo 861   = wceq 1569  ∃wex 1811   ∈ wcel 2144  {cab 2738   ≠ wne 2955  ∀wral 3076  ∃wrex 3086  Vcvv 3450   ⊆ wss 3895  ∅c0 4278  {csn 4583  ∪ cuni 4866  ∪ ciun 4950   class class class wbr 5102   ↦ cmpt 5185   Or wor 5557   × cxp 5648  dom cdm 5650  ran crn 5651   “ cima 5653   ∘ ccom 5654   Fn wfn 6533  ⟶wf 6534  –onto→wfo 6536  ‘cfv 6538  (class class class)co 7420   ≼ cdom 8971   ≺ csdm 8972  Fincfn 8973  supcsup 9432  ℝcr 11199  0cc0 11200  1c1 11201   + caddc 11203  +∞cpnf 11340  ℝ^*cxr 11342   < clt 11343   ≤ cle 11344  ℕcn 12335  ℤ_≥cuz 12965  [,]cicc 13479  ...cfz 13639  Σcsu 15853  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-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)