volfiniune - Mathbox for Thierry Arnoux

	Mathbox for Thierry Arnoux		< Previous Next > Nearby theorems
Mirrors > Home > MPE Home > Th. List > Mathboxes > volfiniune		Structured version Visualization version GIF version

Theorem volfiniune 33758

Description: The Lebesgue measure function is countably additive. This theorem is to volfiniun 25431 what voliune 33757 is to voliun 25438. (Contributed by Thierry Arnoux, 16-Oct-2017.)

**Assertion**
Ref	Expression
volfiniune	⊢ ((𝐴 ∈ Fin ∧ ∀𝑛 ∈ 𝐴 𝐵 ∈ dom vol ∧ Disj 𝑛 ∈ 𝐴 𝐵) → (vol‘∪ 𝑛 ∈ 𝐴 𝐵) = Σ^*𝑛 ∈ 𝐴(vol‘𝐵))

Distinct variable group: 𝐴,𝑛 Allowed substitution hint: 𝐵(𝑛)

Proof of Theorem volfiniune Dummy variable 𝑘 is distinct from all other variables.

Step	Hyp	Ref	Expression
1		simpl1 1188	. . . 4 ⊢ (((𝐴 ∈ Fin ∧ ∀𝑛 ∈ 𝐴 𝐵 ∈ dom vol ∧ Disj 𝑛 ∈ 𝐴 𝐵) ∧ ∀𝑛 ∈ 𝐴 (vol‘𝐵) ∈ ℝ) → 𝐴 ∈ Fin)
2		simpl2 1189	. . . . 5 ⊢ (((𝐴 ∈ Fin ∧ ∀𝑛 ∈ 𝐴 𝐵 ∈ dom vol ∧ Disj 𝑛 ∈ 𝐴 𝐵) ∧ ∀𝑛 ∈ 𝐴 (vol‘𝐵) ∈ ℝ) → ∀𝑛 ∈ 𝐴 𝐵 ∈ dom vol)
3		simpr 484	. . . . 5 ⊢ (((𝐴 ∈ Fin ∧ ∀𝑛 ∈ 𝐴 𝐵 ∈ dom vol ∧ Disj 𝑛 ∈ 𝐴 𝐵) ∧ ∀𝑛 ∈ 𝐴 (vol‘𝐵) ∈ ℝ) → ∀𝑛 ∈ 𝐴 (vol‘𝐵) ∈ ℝ)
4		r19.26 3105	. . . . 5 ⊢ (∀𝑛 ∈ 𝐴 (𝐵 ∈ dom vol ∧ (vol‘𝐵) ∈ ℝ) ↔ (∀𝑛 ∈ 𝐴 𝐵 ∈ dom vol ∧ ∀𝑛 ∈ 𝐴 (vol‘𝐵) ∈ ℝ))
5	2, 3, 4	sylanbrc 582	. . . 4 ⊢ (((𝐴 ∈ Fin ∧ ∀𝑛 ∈ 𝐴 𝐵 ∈ dom vol ∧ Disj 𝑛 ∈ 𝐴 𝐵) ∧ ∀𝑛 ∈ 𝐴 (vol‘𝐵) ∈ ℝ) → ∀𝑛 ∈ 𝐴 (𝐵 ∈ dom vol ∧ (vol‘𝐵) ∈ ℝ))
6		simpl3 1190	. . . 4 ⊢ (((𝐴 ∈ Fin ∧ ∀𝑛 ∈ 𝐴 𝐵 ∈ dom vol ∧ Disj 𝑛 ∈ 𝐴 𝐵) ∧ ∀𝑛 ∈ 𝐴 (vol‘𝐵) ∈ ℝ) → Disj 𝑛 ∈ 𝐴 𝐵)
7		volfiniun 25431	. . . 4 ⊢ ((𝐴 ∈ Fin ∧ ∀𝑛 ∈ 𝐴 (𝐵 ∈ dom vol ∧ (vol‘𝐵) ∈ ℝ) ∧ Disj 𝑛 ∈ 𝐴 𝐵) → (vol‘∪ 𝑛 ∈ 𝐴 𝐵) = Σ𝑛 ∈ 𝐴 (vol‘𝐵))
8	1, 5, 6, 7	syl3anc 1368	. . 3 ⊢ (((𝐴 ∈ Fin ∧ ∀𝑛 ∈ 𝐴 𝐵 ∈ dom vol ∧ Disj 𝑛 ∈ 𝐴 𝐵) ∧ ∀𝑛 ∈ 𝐴 (vol‘𝐵) ∈ ℝ) → (vol‘∪ 𝑛 ∈ 𝐴 𝐵) = Σ𝑛 ∈ 𝐴 (vol‘𝐵))
9		nfcv 2897	. . . 4 ⊢ Ⅎ𝑛𝐴
10	9	nfel1 2913	. . . . . 6 ⊢ Ⅎ𝑛 𝐴 ∈ Fin
11		nfra1 3275	. . . . . 6 ⊢ Ⅎ𝑛∀𝑛 ∈ 𝐴 𝐵 ∈ dom vol
12		nfdisj1 5120	. . . . . 6 ⊢ Ⅎ𝑛Disj 𝑛 ∈ 𝐴 𝐵
13	10, 11, 12	nf3an 1896	. . . . 5 ⊢ Ⅎ𝑛(𝐴 ∈ Fin ∧ ∀𝑛 ∈ 𝐴 𝐵 ∈ dom vol ∧ Disj 𝑛 ∈ 𝐴 𝐵)
14		nfra1 3275	. . . . 5 ⊢ Ⅎ𝑛∀𝑛 ∈ 𝐴 (vol‘𝐵) ∈ ℝ
15	13, 14	nfan 1894	. . . 4 ⊢ Ⅎ𝑛((𝐴 ∈ Fin ∧ ∀𝑛 ∈ 𝐴 𝐵 ∈ dom vol ∧ Disj 𝑛 ∈ 𝐴 𝐵) ∧ ∀𝑛 ∈ 𝐴 (vol‘𝐵) ∈ ℝ)
16	3	r19.21bi 3242	. . . . 5 ⊢ ((((𝐴 ∈ Fin ∧ ∀𝑛 ∈ 𝐴 𝐵 ∈ dom vol ∧ Disj 𝑛 ∈ 𝐴 𝐵) ∧ ∀𝑛 ∈ 𝐴 (vol‘𝐵) ∈ ℝ) ∧ 𝑛 ∈ 𝐴) → (vol‘𝐵) ∈ ℝ)
17		rspa 3239	. . . . . . . 8 ⊢ ((∀𝑛 ∈ 𝐴 𝐵 ∈ dom vol ∧ 𝑛 ∈ 𝐴) → 𝐵 ∈ dom vol)
18		volf 25413	. . . . . . . . 9 ⊢ vol:dom vol⟶(0[,]+∞)
19	18	ffvelcdmi 7079	. . . . . . . 8 ⊢ (𝐵 ∈ dom vol → (vol‘𝐵) ∈ (0[,]+∞))
20	17, 19	syl 17	. . . . . . 7 ⊢ ((∀𝑛 ∈ 𝐴 𝐵 ∈ dom vol ∧ 𝑛 ∈ 𝐴) → (vol‘𝐵) ∈ (0[,]+∞))
21	2, 20	sylan 579	. . . . . 6 ⊢ ((((𝐴 ∈ Fin ∧ ∀𝑛 ∈ 𝐴 𝐵 ∈ dom vol ∧ Disj 𝑛 ∈ 𝐴 𝐵) ∧ ∀𝑛 ∈ 𝐴 (vol‘𝐵) ∈ ℝ) ∧ 𝑛 ∈ 𝐴) → (vol‘𝐵) ∈ (0[,]+∞))
22		0xr 11265	. . . . . . . 8 ⊢ 0 ∈ ℝ^*
23		pnfxr 11272	. . . . . . . 8 ⊢ +∞ ∈ ℝ^*
24		elicc1 13374	. . . . . . . 8 ⊢ ((0 ∈ ℝ^* ∧ +∞ ∈ ℝ^) → ((vol‘𝐵) ∈ (0[,]+∞) ↔ ((vol‘𝐵) ∈ ℝ^ ∧ 0 ≤ (vol‘𝐵) ∧ (vol‘𝐵) ≤ +∞)))
25	22, 23, 24	mp2an 689	. . . . . . 7 ⊢ ((vol‘𝐵) ∈ (0[,]+∞) ↔ ((vol‘𝐵) ∈ ℝ^* ∧ 0 ≤ (vol‘𝐵) ∧ (vol‘𝐵) ≤ +∞))
26	25	simp2bi 1143	. . . . . 6 ⊢ ((vol‘𝐵) ∈ (0[,]+∞) → 0 ≤ (vol‘𝐵))
27	21, 26	syl 17	. . . . 5 ⊢ ((((𝐴 ∈ Fin ∧ ∀𝑛 ∈ 𝐴 𝐵 ∈ dom vol ∧ Disj 𝑛 ∈ 𝐴 𝐵) ∧ ∀𝑛 ∈ 𝐴 (vol‘𝐵) ∈ ℝ) ∧ 𝑛 ∈ 𝐴) → 0 ≤ (vol‘𝐵))
28		ltpnf 13106	. . . . . 6 ⊢ ((vol‘𝐵) ∈ ℝ → (vol‘𝐵) < +∞)
29	16, 28	syl 17	. . . . 5 ⊢ ((((𝐴 ∈ Fin ∧ ∀𝑛 ∈ 𝐴 𝐵 ∈ dom vol ∧ Disj 𝑛 ∈ 𝐴 𝐵) ∧ ∀𝑛 ∈ 𝐴 (vol‘𝐵) ∈ ℝ) ∧ 𝑛 ∈ 𝐴) → (vol‘𝐵) < +∞)
30		0re 11220	. . . . . 6 ⊢ 0 ∈ ℝ
31		elico2 13394	. . . . . 6 ⊢ ((0 ∈ ℝ ∧ +∞ ∈ ℝ^*) → ((vol‘𝐵) ∈ (0[,)+∞) ↔ ((vol‘𝐵) ∈ ℝ ∧ 0 ≤ (vol‘𝐵) ∧ (vol‘𝐵) < +∞)))
32	30, 23, 31	mp2an 689	. . . . 5 ⊢ ((vol‘𝐵) ∈ (0[,)+∞) ↔ ((vol‘𝐵) ∈ ℝ ∧ 0 ≤ (vol‘𝐵) ∧ (vol‘𝐵) < +∞))
33	16, 27, 29, 32	syl3anbrc 1340	. . . 4 ⊢ ((((𝐴 ∈ Fin ∧ ∀𝑛 ∈ 𝐴 𝐵 ∈ dom vol ∧ Disj 𝑛 ∈ 𝐴 𝐵) ∧ ∀𝑛 ∈ 𝐴 (vol‘𝐵) ∈ ℝ) ∧ 𝑛 ∈ 𝐴) → (vol‘𝐵) ∈ (0[,)+∞))
34	9, 15, 1, 33	esumpfinvalf 33604	. . 3 ⊢ (((𝐴 ∈ Fin ∧ ∀𝑛 ∈ 𝐴 𝐵 ∈ dom vol ∧ Disj 𝑛 ∈ 𝐴 𝐵) ∧ ∀𝑛 ∈ 𝐴 (vol‘𝐵) ∈ ℝ) → Σ^*𝑛 ∈ 𝐴(vol‘𝐵) = Σ𝑛 ∈ 𝐴 (vol‘𝐵))
35	8, 34	eqtr4d 2769	. 2 ⊢ (((𝐴 ∈ Fin ∧ ∀𝑛 ∈ 𝐴 𝐵 ∈ dom vol ∧ Disj 𝑛 ∈ 𝐴 𝐵) ∧ ∀𝑛 ∈ 𝐴 (vol‘𝐵) ∈ ℝ) → (vol‘∪ 𝑛 ∈ 𝐴 𝐵) = Σ^*𝑛 ∈ 𝐴(vol‘𝐵))
36		simpr 484	. . . . . . . 8 ⊢ (((𝐴 ∈ Fin ∧ ∀𝑛 ∈ 𝐴 𝐵 ∈ dom vol ∧ Disj 𝑛 ∈ 𝐴 𝐵) ∧ ∃𝑛 ∈ 𝐴 (vol‘𝐵) = +∞) → ∃𝑛 ∈ 𝐴 (vol‘𝐵) = +∞)
37		nfv 1909	. . . . . . . . 9 ⊢ Ⅎ𝑘(vol‘𝐵) = +∞
38		nfcv 2897	. . . . . . . . . . 11 ⊢ Ⅎ𝑛vol
39		nfcsb1v 3913	. . . . . . . . . . 11 ⊢ Ⅎ𝑛⦋𝑘 / 𝑛⦌𝐵
40	38, 39	nffv 6895	. . . . . . . . . 10 ⊢ Ⅎ𝑛(vol‘⦋𝑘 / 𝑛⦌𝐵)
41	40	nfeq1 2912	. . . . . . . . 9 ⊢ Ⅎ𝑛(vol‘⦋𝑘 / 𝑛⦌𝐵) = +∞
42		csbeq1a 3902	. . . . . . . . . 10 ⊢ (𝑛 = 𝑘 → 𝐵 = ⦋𝑘 / 𝑛⦌𝐵)
43	42	fveqeq2d 6893	. . . . . . . . 9 ⊢ (𝑛 = 𝑘 → ((vol‘𝐵) = +∞ ↔ (vol‘⦋𝑘 / 𝑛⦌𝐵) = +∞))
44	37, 41, 43	cbvrexw 3298	. . . . . . . 8 ⊢ (∃𝑛 ∈ 𝐴 (vol‘𝐵) = +∞ ↔ ∃𝑘 ∈ 𝐴 (vol‘⦋𝑘 / 𝑛⦌𝐵) = +∞)
45	36, 44	sylib 217	. . . . . . 7 ⊢ (((𝐴 ∈ Fin ∧ ∀𝑛 ∈ 𝐴 𝐵 ∈ dom vol ∧ Disj 𝑛 ∈ 𝐴 𝐵) ∧ ∃𝑛 ∈ 𝐴 (vol‘𝐵) = +∞) → ∃𝑘 ∈ 𝐴 (vol‘⦋𝑘 / 𝑛⦌𝐵) = +∞)
46	39	nfel1 2913	. . . . . . . . . . . . . 14 ⊢ Ⅎ𝑛⦋𝑘 / 𝑛⦌𝐵 ∈ dom vol
47	42	eleq1d 2812	. . . . . . . . . . . . . 14 ⊢ (𝑛 = 𝑘 → (𝐵 ∈ dom vol ↔ ⦋𝑘 / 𝑛⦌𝐵 ∈ dom vol))
48	46, 47	rspc 3594	. . . . . . . . . . . . 13 ⊢ (𝑘 ∈ 𝐴 → (∀𝑛 ∈ 𝐴 𝐵 ∈ dom vol → ⦋𝑘 / 𝑛⦌𝐵 ∈ dom vol))
49	48	impcom 407	. . . . . . . . . . . 12 ⊢ ((∀𝑛 ∈ 𝐴 𝐵 ∈ dom vol ∧ 𝑘 ∈ 𝐴) → ⦋𝑘 / 𝑛⦌𝐵 ∈ dom vol)
50	49	adantll 711	. . . . . . . . . . 11 ⊢ (((𝐴 ∈ Fin ∧ ∀𝑛 ∈ 𝐴 𝐵 ∈ dom vol) ∧ 𝑘 ∈ 𝐴) → ⦋𝑘 / 𝑛⦌𝐵 ∈ dom vol)
51		finiunmbl 25428	. . . . . . . . . . . 12 ⊢ ((𝐴 ∈ Fin ∧ ∀𝑛 ∈ 𝐴 𝐵 ∈ dom vol) → ∪ 𝑛 ∈ 𝐴 𝐵 ∈ dom vol)
52	51	adantr 480	. . . . . . . . . . 11 ⊢ (((𝐴 ∈ Fin ∧ ∀𝑛 ∈ 𝐴 𝐵 ∈ dom vol) ∧ 𝑘 ∈ 𝐴) → ∪ 𝑛 ∈ 𝐴 𝐵 ∈ dom vol)
53		nfcv 2897	. . . . . . . . . . . . 13 ⊢ Ⅎ𝑛𝑘
54	9, 53, 39, 42	ssiun2sf 32300	. . . . . . . . . . . 12 ⊢ (𝑘 ∈ 𝐴 → ⦋𝑘 / 𝑛⦌𝐵 ⊆ ∪ 𝑛 ∈ 𝐴 𝐵)
55	54	adantl 481	. . . . . . . . . . 11 ⊢ (((𝐴 ∈ Fin ∧ ∀𝑛 ∈ 𝐴 𝐵 ∈ dom vol) ∧ 𝑘 ∈ 𝐴) → ⦋𝑘 / 𝑛⦌𝐵 ⊆ ∪ 𝑛 ∈ 𝐴 𝐵)
56		volss 25417	. . . . . . . . . . 11 ⊢ ((⦋𝑘 / 𝑛⦌𝐵 ∈ dom vol ∧ ∪ 𝑛 ∈ 𝐴 𝐵 ∈ dom vol ∧ ⦋𝑘 / 𝑛⦌𝐵 ⊆ ∪ 𝑛 ∈ 𝐴 𝐵) → (vol‘⦋𝑘 / 𝑛⦌𝐵) ≤ (vol‘∪ 𝑛 ∈ 𝐴 𝐵))
57	50, 52, 55, 56	syl3anc 1368	. . . . . . . . . 10 ⊢ (((𝐴 ∈ Fin ∧ ∀𝑛 ∈ 𝐴 𝐵 ∈ dom vol) ∧ 𝑘 ∈ 𝐴) → (vol‘⦋𝑘 / 𝑛⦌𝐵) ≤ (vol‘∪ 𝑛 ∈ 𝐴 𝐵))
58	57	3adantl3 1165	. . . . . . . . 9 ⊢ (((𝐴 ∈ Fin ∧ ∀𝑛 ∈ 𝐴 𝐵 ∈ dom vol ∧ Disj 𝑛 ∈ 𝐴 𝐵) ∧ 𝑘 ∈ 𝐴) → (vol‘⦋𝑘 / 𝑛⦌𝐵) ≤ (vol‘∪ 𝑛 ∈ 𝐴 𝐵))
59	58	adantlr 712	. . . . . . . 8 ⊢ ((((𝐴 ∈ Fin ∧ ∀𝑛 ∈ 𝐴 𝐵 ∈ dom vol ∧ Disj 𝑛 ∈ 𝐴 𝐵) ∧ ∃𝑛 ∈ 𝐴 (vol‘𝐵) = +∞) ∧ 𝑘 ∈ 𝐴) → (vol‘⦋𝑘 / 𝑛⦌𝐵) ≤ (vol‘∪ 𝑛 ∈ 𝐴 𝐵))
60	59	ralrimiva 3140	. . . . . . 7 ⊢ (((𝐴 ∈ Fin ∧ ∀𝑛 ∈ 𝐴 𝐵 ∈ dom vol ∧ Disj 𝑛 ∈ 𝐴 𝐵) ∧ ∃𝑛 ∈ 𝐴 (vol‘𝐵) = +∞) → ∀𝑘 ∈ 𝐴 (vol‘⦋𝑘 / 𝑛⦌𝐵) ≤ (vol‘∪ 𝑛 ∈ 𝐴 𝐵))
61		r19.29r 3110	. . . . . . 7 ⊢ ((∃𝑘 ∈ 𝐴 (vol‘⦋𝑘 / 𝑛⦌𝐵) = +∞ ∧ ∀𝑘 ∈ 𝐴 (vol‘⦋𝑘 / 𝑛⦌𝐵) ≤ (vol‘∪ 𝑛 ∈ 𝐴 𝐵)) → ∃𝑘 ∈ 𝐴 ((vol‘⦋𝑘 / 𝑛⦌𝐵) = +∞ ∧ (vol‘⦋𝑘 / 𝑛⦌𝐵) ≤ (vol‘∪ 𝑛 ∈ 𝐴 𝐵)))
62	45, 60, 61	syl2anc 583	. . . . . 6 ⊢ (((𝐴 ∈ Fin ∧ ∀𝑛 ∈ 𝐴 𝐵 ∈ dom vol ∧ Disj 𝑛 ∈ 𝐴 𝐵) ∧ ∃𝑛 ∈ 𝐴 (vol‘𝐵) = +∞) → ∃𝑘 ∈ 𝐴 ((vol‘⦋𝑘 / 𝑛⦌𝐵) = +∞ ∧ (vol‘⦋𝑘 / 𝑛⦌𝐵) ≤ (vol‘∪ 𝑛 ∈ 𝐴 𝐵)))
63		breq1 5144	. . . . . . . 8 ⊢ ((vol‘⦋𝑘 / 𝑛⦌𝐵) = +∞ → ((vol‘⦋𝑘 / 𝑛⦌𝐵) ≤ (vol‘∪ 𝑛 ∈ 𝐴 𝐵) ↔ +∞ ≤ (vol‘∪ 𝑛 ∈ 𝐴 𝐵)))
64	63	biimpa 476	. . . . . . 7 ⊢ (((vol‘⦋𝑘 / 𝑛⦌𝐵) = +∞ ∧ (vol‘⦋𝑘 / 𝑛⦌𝐵) ≤ (vol‘∪ 𝑛 ∈ 𝐴 𝐵)) → +∞ ≤ (vol‘∪ 𝑛 ∈ 𝐴 𝐵))
65	64	reximi 3078	. . . . . 6 ⊢ (∃𝑘 ∈ 𝐴 ((vol‘⦋𝑘 / 𝑛⦌𝐵) = +∞ ∧ (vol‘⦋𝑘 / 𝑛⦌𝐵) ≤ (vol‘∪ 𝑛 ∈ 𝐴 𝐵)) → ∃𝑘 ∈ 𝐴 +∞ ≤ (vol‘∪ 𝑛 ∈ 𝐴 𝐵))
66	62, 65	syl 17	. . . . 5 ⊢ (((𝐴 ∈ Fin ∧ ∀𝑛 ∈ 𝐴 𝐵 ∈ dom vol ∧ Disj 𝑛 ∈ 𝐴 𝐵) ∧ ∃𝑛 ∈ 𝐴 (vol‘𝐵) = +∞) → ∃𝑘 ∈ 𝐴 +∞ ≤ (vol‘∪ 𝑛 ∈ 𝐴 𝐵))
67		rexex 3070	. . . . . 6 ⊢ (∃𝑘 ∈ 𝐴 +∞ ≤ (vol‘∪ 𝑛 ∈ 𝐴 𝐵) → ∃𝑘+∞ ≤ (vol‘∪ 𝑛 ∈ 𝐴 𝐵))
68		19.9v 1979	. . . . . 6 ⊢ (∃𝑘+∞ ≤ (vol‘∪ 𝑛 ∈ 𝐴 𝐵) ↔ +∞ ≤ (vol‘∪ 𝑛 ∈ 𝐴 𝐵))
69	67, 68	sylib 217	. . . . 5 ⊢ (∃𝑘 ∈ 𝐴 +∞ ≤ (vol‘∪ 𝑛 ∈ 𝐴 𝐵) → +∞ ≤ (vol‘∪ 𝑛 ∈ 𝐴 𝐵))
70	66, 69	syl 17	. . . 4 ⊢ (((𝐴 ∈ Fin ∧ ∀𝑛 ∈ 𝐴 𝐵 ∈ dom vol ∧ Disj 𝑛 ∈ 𝐴 𝐵) ∧ ∃𝑛 ∈ 𝐴 (vol‘𝐵) = +∞) → +∞ ≤ (vol‘∪ 𝑛 ∈ 𝐴 𝐵))
71		iccssxr 13413	. . . . . . . . 9 ⊢ (0[,]+∞) ⊆ ℝ^*
72	18	ffvelcdmi 7079	. . . . . . . . 9 ⊢ (∪ 𝑛 ∈ 𝐴 𝐵 ∈ dom vol → (vol‘∪ 𝑛 ∈ 𝐴 𝐵) ∈ (0[,]+∞))
73	71, 72	sselid 3975	. . . . . . . 8 ⊢ (∪ 𝑛 ∈ 𝐴 𝐵 ∈ dom vol → (vol‘∪ 𝑛 ∈ 𝐴 𝐵) ∈ ℝ^*)
74	51, 73	syl 17	. . . . . . 7 ⊢ ((𝐴 ∈ Fin ∧ ∀𝑛 ∈ 𝐴 𝐵 ∈ dom vol) → (vol‘∪ 𝑛 ∈ 𝐴 𝐵) ∈ ℝ^*)
75	74	3adant3 1129	. . . . . 6 ⊢ ((𝐴 ∈ Fin ∧ ∀𝑛 ∈ 𝐴 𝐵 ∈ dom vol ∧ Disj 𝑛 ∈ 𝐴 𝐵) → (vol‘∪ 𝑛 ∈ 𝐴 𝐵) ∈ ℝ^*)
76	75	adantr 480	. . . . 5 ⊢ (((𝐴 ∈ Fin ∧ ∀𝑛 ∈ 𝐴 𝐵 ∈ dom vol ∧ Disj 𝑛 ∈ 𝐴 𝐵) ∧ ∃𝑛 ∈ 𝐴 (vol‘𝐵) = +∞) → (vol‘∪ 𝑛 ∈ 𝐴 𝐵) ∈ ℝ^*)
77		xgepnf 13150	. . . . 5 ⊢ ((vol‘∪ 𝑛 ∈ 𝐴 𝐵) ∈ ℝ^* → (+∞ ≤ (vol‘∪ 𝑛 ∈ 𝐴 𝐵) ↔ (vol‘∪ 𝑛 ∈ 𝐴 𝐵) = +∞))
78	76, 77	syl 17	. . . 4 ⊢ (((𝐴 ∈ Fin ∧ ∀𝑛 ∈ 𝐴 𝐵 ∈ dom vol ∧ Disj 𝑛 ∈ 𝐴 𝐵) ∧ ∃𝑛 ∈ 𝐴 (vol‘𝐵) = +∞) → (+∞ ≤ (vol‘∪ 𝑛 ∈ 𝐴 𝐵) ↔ (vol‘∪ 𝑛 ∈ 𝐴 𝐵) = +∞))
79	70, 78	mpbid 231	. . 3 ⊢ (((𝐴 ∈ Fin ∧ ∀𝑛 ∈ 𝐴 𝐵 ∈ dom vol ∧ Disj 𝑛 ∈ 𝐴 𝐵) ∧ ∃𝑛 ∈ 𝐴 (vol‘𝐵) = +∞) → (vol‘∪ 𝑛 ∈ 𝐴 𝐵) = +∞)
80		nfre1 3276	. . . . 5 ⊢ Ⅎ𝑛∃𝑛 ∈ 𝐴 (vol‘𝐵) = +∞
81	13, 80	nfan 1894	. . . 4 ⊢ Ⅎ𝑛((𝐴 ∈ Fin ∧ ∀𝑛 ∈ 𝐴 𝐵 ∈ dom vol ∧ Disj 𝑛 ∈ 𝐴 𝐵) ∧ ∃𝑛 ∈ 𝐴 (vol‘𝐵) = +∞)
82		simpl1 1188	. . . 4 ⊢ (((𝐴 ∈ Fin ∧ ∀𝑛 ∈ 𝐴 𝐵 ∈ dom vol ∧ Disj 𝑛 ∈ 𝐴 𝐵) ∧ ∃𝑛 ∈ 𝐴 (vol‘𝐵) = +∞) → 𝐴 ∈ Fin)
83	20	3ad2antl2 1183	. . . . 5 ⊢ (((𝐴 ∈ Fin ∧ ∀𝑛 ∈ 𝐴 𝐵 ∈ dom vol ∧ Disj 𝑛 ∈ 𝐴 𝐵) ∧ 𝑛 ∈ 𝐴) → (vol‘𝐵) ∈ (0[,]+∞))
84	83	adantlr 712	. . . 4 ⊢ ((((𝐴 ∈ Fin ∧ ∀𝑛 ∈ 𝐴 𝐵 ∈ dom vol ∧ Disj 𝑛 ∈ 𝐴 𝐵) ∧ ∃𝑛 ∈ 𝐴 (vol‘𝐵) = +∞) ∧ 𝑛 ∈ 𝐴) → (vol‘𝐵) ∈ (0[,]+∞))
85	81, 82, 84, 36	esumpinfval 33601	. . 3 ⊢ (((𝐴 ∈ Fin ∧ ∀𝑛 ∈ 𝐴 𝐵 ∈ dom vol ∧ Disj 𝑛 ∈ 𝐴 𝐵) ∧ ∃𝑛 ∈ 𝐴 (vol‘𝐵) = +∞) → Σ^*𝑛 ∈ 𝐴(vol‘𝐵) = +∞)
86	79, 85	eqtr4d 2769	. 2 ⊢ (((𝐴 ∈ Fin ∧ ∀𝑛 ∈ 𝐴 𝐵 ∈ dom vol ∧ Disj 𝑛 ∈ 𝐴 𝐵) ∧ ∃𝑛 ∈ 𝐴 (vol‘𝐵) = +∞) → (vol‘∪ 𝑛 ∈ 𝐴 𝐵) = Σ^*𝑛 ∈ 𝐴(vol‘𝐵))
87		exmid 891	. . . . 5 ⊢ (∀𝑛 ∈ 𝐴 (vol‘𝐵) ∈ ℝ ∨ ¬ ∀𝑛 ∈ 𝐴 (vol‘𝐵) ∈ ℝ)
88		rexnal 3094	. . . . . 6 ⊢ (∃𝑛 ∈ 𝐴 ¬ (vol‘𝐵) ∈ ℝ ↔ ¬ ∀𝑛 ∈ 𝐴 (vol‘𝐵) ∈ ℝ)
89	88	orbi2i 909	. . . . 5 ⊢ ((∀𝑛 ∈ 𝐴 (vol‘𝐵) ∈ ℝ ∨ ∃𝑛 ∈ 𝐴 ¬ (vol‘𝐵) ∈ ℝ) ↔ (∀𝑛 ∈ 𝐴 (vol‘𝐵) ∈ ℝ ∨ ¬ ∀𝑛 ∈ 𝐴 (vol‘𝐵) ∈ ℝ))
90	87, 89	mpbir 230	. . . 4 ⊢ (∀𝑛 ∈ 𝐴 (vol‘𝐵) ∈ ℝ ∨ ∃𝑛 ∈ 𝐴 ¬ (vol‘𝐵) ∈ ℝ)
91		r19.29 3108	. . . . . . 7 ⊢ ((∀𝑛 ∈ 𝐴 𝐵 ∈ dom vol ∧ ∃𝑛 ∈ 𝐴 ¬ (vol‘𝐵) ∈ ℝ) → ∃𝑛 ∈ 𝐴 (𝐵 ∈ dom vol ∧ ¬ (vol‘𝐵) ∈ ℝ))
92		xrge0nre 13436	. . . . . . . . 9 ⊢ (((vol‘𝐵) ∈ (0[,]+∞) ∧ ¬ (vol‘𝐵) ∈ ℝ) → (vol‘𝐵) = +∞)
93	19, 92	sylan 579	. . . . . . . 8 ⊢ ((𝐵 ∈ dom vol ∧ ¬ (vol‘𝐵) ∈ ℝ) → (vol‘𝐵) = +∞)
94	93	reximi 3078	. . . . . . 7 ⊢ (∃𝑛 ∈ 𝐴 (𝐵 ∈ dom vol ∧ ¬ (vol‘𝐵) ∈ ℝ) → ∃𝑛 ∈ 𝐴 (vol‘𝐵) = +∞)
95	91, 94	syl 17	. . . . . 6 ⊢ ((∀𝑛 ∈ 𝐴 𝐵 ∈ dom vol ∧ ∃𝑛 ∈ 𝐴 ¬ (vol‘𝐵) ∈ ℝ) → ∃𝑛 ∈ 𝐴 (vol‘𝐵) = +∞)
96	95	ex 412	. . . . 5 ⊢ (∀𝑛 ∈ 𝐴 𝐵 ∈ dom vol → (∃𝑛 ∈ 𝐴 ¬ (vol‘𝐵) ∈ ℝ → ∃𝑛 ∈ 𝐴 (vol‘𝐵) = +∞))
97	96	orim2d 963	. . . 4 ⊢ (∀𝑛 ∈ 𝐴 𝐵 ∈ dom vol → ((∀𝑛 ∈ 𝐴 (vol‘𝐵) ∈ ℝ ∨ ∃𝑛 ∈ 𝐴 ¬ (vol‘𝐵) ∈ ℝ) → (∀𝑛 ∈ 𝐴 (vol‘𝐵) ∈ ℝ ∨ ∃𝑛 ∈ 𝐴 (vol‘𝐵) = +∞)))
98	90, 97	mpi 20	. . 3 ⊢ (∀𝑛 ∈ 𝐴 𝐵 ∈ dom vol → (∀𝑛 ∈ 𝐴 (vol‘𝐵) ∈ ℝ ∨ ∃𝑛 ∈ 𝐴 (vol‘𝐵) = +∞))
99	98	3ad2ant2 1131	. 2 ⊢ ((𝐴 ∈ Fin ∧ ∀𝑛 ∈ 𝐴 𝐵 ∈ dom vol ∧ Disj 𝑛 ∈ 𝐴 𝐵) → (∀𝑛 ∈ 𝐴 (vol‘𝐵) ∈ ℝ ∨ ∃𝑛 ∈ 𝐴 (vol‘𝐵) = +∞))
100	35, 86, 99	mpjaodan 955	1 ⊢ ((𝐴 ∈ Fin ∧ ∀𝑛 ∈ 𝐴 𝐵 ∈ dom vol ∧ Disj 𝑛 ∈ 𝐴 𝐵) → (vol‘∪ 𝑛 ∈ 𝐴 𝐵) = Σ^*𝑛 ∈ 𝐴(vol‘𝐵))

Colors of variables: wff setvar class

Syntax hints: ¬ wn 3 → wi 4 ↔ wb 205 ∧ wa 395 ∨ wo 844 ∧ w3a 1084 = wceq 1533 ∃wex 1773 ∈ wcel 2098 ∀wral 3055 ∃wrex 3064 ⦋csb 3888 ⊆ wss 3943 ∪ ciun 4990 Disj wdisj 5106 class class class wbr 5141 dom cdm 5669 ‘cfv 6537 (class class class)co 7405 Fincfn 8941 ℝcr 11111 0cc0 11112 +∞cpnf 11249 ℝ^*cxr 11251 < clt 11252 ≤ cle 11253 [,)cico 13332 [,]cicc 13333 Σcsu 15638 volcvol 25347 Σ^*cesum 33555

This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1789 ax-4 1803 ax-5 1905 ax-6 1963 ax-7 2003 ax-8 2100 ax-9 2108 ax-10 2129 ax-11 2146 ax-12 2163 ax-ext 2697 ax-rep 5278 ax-sep 5292 ax-nul 5299 ax-pow 5356 ax-pr 5420 ax-un 7722 ax-inf2 9638 ax-cnex 11168 ax-resscn 11169 ax-1cn 11170 ax-icn 11171 ax-addcl 11172 ax-addrcl 11173 ax-mulcl 11174 ax-mulrcl 11175 ax-mulcom 11176 ax-addass 11177 ax-mulass 11178 ax-distr 11179 ax-i2m1 11180 ax-1ne0 11181 ax-1rid 11182 ax-rnegex 11183 ax-rrecex 11184 ax-cnre 11185 ax-pre-lttri 11186 ax-pre-lttrn 11187 ax-pre-ltadd 11188 ax-pre-mulgt0 11189 ax-pre-sup 11190 ax-addf 11191 ax-mulf 11192

This theorem depends on definitions: df-bi 206 df-an 396 df-or 845 df-3or 1085 df-3an 1086 df-tru 1536 df-fal 1546 df-ex 1774 df-nf 1778 df-sb 2060 df-mo 2528 df-eu 2557 df-clab 2704 df-cleq 2718 df-clel 2804 df-nfc 2879 df-ne 2935 df-nel 3041 df-ral 3056 df-rex 3065 df-rmo 3370 df-reu 3371 df-rab 3427 df-v 3470 df-sbc 3773 df-csb 3889 df-dif 3946 df-un 3948 df-in 3950 df-ss 3960 df-pss 3962 df-nul 4318 df-if 4524 df-pw 4599 df-sn 4624 df-pr 4626 df-tp 4628 df-op 4630 df-uni 4903 df-int 4944 df-iun 4992 df-iin 4993 df-disj 5107 df-br 5142 df-opab 5204 df-mpt 5225 df-tr 5259 df-id 5567 df-eprel 5573 df-po 5581 df-so 5582 df-fr 5624 df-se 5625 df-we 5626 df-xp 5675 df-rel 5676 df-cnv 5677 df-co 5678 df-dm 5679 df-rn 5680 df-res 5681 df-ima 5682 df-pred 6294 df-ord 6361 df-on 6362 df-lim 6363 df-suc 6364 df-iota 6489 df-fun 6539 df-fn 6540 df-f 6541 df-f1 6542 df-fo 6543 df-f1o 6544 df-fv 6545 df-isom 6546 df-riota 7361 df-ov 7408 df-oprab 7409 df-mpo 7410 df-of 7667 df-om 7853 df-1st 7974 df-2nd 7975 df-supp 8147 df-frecs 8267 df-wrecs 8298 df-recs 8372 df-rdg 8411 df-1o 8467 df-2o 8468 df-oadd 8471 df-er 8705 df-map 8824 df-pm 8825 df-ixp 8894 df-en 8942 df-dom 8943 df-sdom 8944 df-fin 8945 df-fsupp 9364 df-fi 9408 df-sup 9439 df-inf 9440 df-oi 9507 df-dju 9898 df-card 9936 df-pnf 11254 df-mnf 11255 df-xr 11256 df-ltxr 11257 df-le 11258 df-sub 11450 df-neg 11451 df-div 11876 df-nn 12217 df-2 12279 df-3 12280 df-4 12281 df-5 12282 df-6 12283 df-7 12284 df-8 12285 df-9 12286 df-n0 12477 df-xnn0 12549 df-z 12563 df-dec 12682 df-uz 12827 df-q 12937 df-rp 12981 df-xneg 13098 df-xadd 13099 df-xmul 13100 df-ioo 13334 df-ioc 13335 df-ico 13336 df-icc 13337 df-fz 13491 df-fzo 13634 df-fl 13763 df-mod 13841 df-seq 13973 df-exp 14033 df-fac 14239 df-bc 14268 df-hash 14296 df-shft 15020 df-cj 15052 df-re 15053 df-im 15054 df-sqrt 15188 df-abs 15189 df-limsup 15421 df-clim 15438 df-rlim 15439 df-sum 15639 df-ef 16017 df-sin 16019 df-cos 16020 df-pi 16022 df-struct 17089 df-sets 17106 df-slot 17124 df-ndx 17136 df-base 17154 df-ress 17183 df-plusg 17219 df-mulr 17220 df-starv 17221 df-sca 17222 df-vsca 17223 df-ip 17224 df-tset 17225 df-ple 17226 df-ds 17228 df-unif 17229 df-hom 17230 df-cco 17231 df-rest 17377 df-topn 17378 df-0g 17396 df-gsum 17397 df-topgen 17398 df-pt 17399 df-prds 17402 df-ordt 17456 df-xrs 17457 df-qtop 17462 df-imas 17463 df-xps 17465 df-mre 17539 df-mrc 17540 df-acs 17542 df-ps 18531 df-tsr 18532 df-plusf 18572 df-mgm 18573 df-sgrp 18652 df-mnd 18668 df-mhm 18713 df-submnd 18714 df-grp 18866 df-minusg 18867 df-sbg 18868 df-mulg 18996 df-subg 19050 df-cntz 19233 df-cmn 19702 df-abl 19703 df-mgp 20040 df-rng 20058 df-ur 20087 df-ring 20140 df-cring 20141 df-subrng 20446 df-subrg 20471 df-abv 20660 df-lmod 20708 df-scaf 20709 df-sra 21021 df-rgmod 21022 df-psmet 21232 df-xmet 21233 df-met 21234 df-bl 21235 df-mopn 21236 df-fbas 21237 df-fg 21238 df-cnfld 21241 df-top 22751 df-topon 22768 df-topsp 22790 df-bases 22804 df-cld 22878 df-ntr 22879 df-cls 22880 df-nei 22957 df-lp 22995 df-perf 22996 df-cn 23086 df-cnp 23087 df-haus 23174 df-tx 23421 df-hmeo 23614 df-fil 23705 df-fm 23797 df-flim 23798 df-flf 23799 df-tmd 23931 df-tgp 23932 df-tsms 23986 df-trg 24019 df-xms 24181 df-ms 24182 df-tms 24183 df-nm 24446 df-ngp 24447 df-nrg 24449 df-nlm 24450 df-ii 24752 df-cncf 24753 df-ovol 25348 df-vol 25349 df-limc 25750 df-dv 25751 df-log 26445 df-esum 33556

This theorem is referenced by: volmeas 33759

W3C validator