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 34211

Description: The Lebesgue measure function is countably additive. This theorem is to volfiniun 25429 what voliune 34210 is to voliun 25436. (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 1192	. . . 4 ⊢ (((𝐴 ∈ Fin ∧ ∀𝑛 ∈ 𝐴 𝐵 ∈ dom vol ∧ Disj 𝑛 ∈ 𝐴 𝐵) ∧ ∀𝑛 ∈ 𝐴 (vol‘𝐵) ∈ ℝ) → 𝐴 ∈ Fin)
2		simpl2 1193	. . . . 5 ⊢ (((𝐴 ∈ Fin ∧ ∀𝑛 ∈ 𝐴 𝐵 ∈ dom vol ∧ Disj 𝑛 ∈ 𝐴 𝐵) ∧ ∀𝑛 ∈ 𝐴 (vol‘𝐵) ∈ ℝ) → ∀𝑛 ∈ 𝐴 𝐵 ∈ dom vol)
3		simpr 484	. . . . 5 ⊢ (((𝐴 ∈ Fin ∧ ∀𝑛 ∈ 𝐴 𝐵 ∈ dom vol ∧ Disj 𝑛 ∈ 𝐴 𝐵) ∧ ∀𝑛 ∈ 𝐴 (vol‘𝐵) ∈ ℝ) → ∀𝑛 ∈ 𝐴 (vol‘𝐵) ∈ ℝ)
4		r19.26 3089	. . . . 5 ⊢ (∀𝑛 ∈ 𝐴 (𝐵 ∈ dom vol ∧ (vol‘𝐵) ∈ ℝ) ↔ (∀𝑛 ∈ 𝐴 𝐵 ∈ dom vol ∧ ∀𝑛 ∈ 𝐴 (vol‘𝐵) ∈ ℝ))
5	2, 3, 4	sylanbrc 583	. . . 4 ⊢ (((𝐴 ∈ Fin ∧ ∀𝑛 ∈ 𝐴 𝐵 ∈ dom vol ∧ Disj 𝑛 ∈ 𝐴 𝐵) ∧ ∀𝑛 ∈ 𝐴 (vol‘𝐵) ∈ ℝ) → ∀𝑛 ∈ 𝐴 (𝐵 ∈ dom vol ∧ (vol‘𝐵) ∈ ℝ))
6		simpl3 1194	. . . 4 ⊢ (((𝐴 ∈ Fin ∧ ∀𝑛 ∈ 𝐴 𝐵 ∈ dom vol ∧ Disj 𝑛 ∈ 𝐴 𝐵) ∧ ∀𝑛 ∈ 𝐴 (vol‘𝐵) ∈ ℝ) → Disj 𝑛 ∈ 𝐴 𝐵)
7		volfiniun 25429	. . . 4 ⊢ ((𝐴 ∈ Fin ∧ ∀𝑛 ∈ 𝐴 (𝐵 ∈ dom vol ∧ (vol‘𝐵) ∈ ℝ) ∧ Disj 𝑛 ∈ 𝐴 𝐵) → (vol‘∪ 𝑛 ∈ 𝐴 𝐵) = Σ𝑛 ∈ 𝐴 (vol‘𝐵))
8	1, 5, 6, 7	syl3anc 1373	. . 3 ⊢ (((𝐴 ∈ Fin ∧ ∀𝑛 ∈ 𝐴 𝐵 ∈ dom vol ∧ Disj 𝑛 ∈ 𝐴 𝐵) ∧ ∀𝑛 ∈ 𝐴 (vol‘𝐵) ∈ ℝ) → (vol‘∪ 𝑛 ∈ 𝐴 𝐵) = Σ𝑛 ∈ 𝐴 (vol‘𝐵))
9		nfcv 2891	. . . 4 ⊢ Ⅎ𝑛𝐴
10	9	nfel1 2908	. . . . . 6 ⊢ Ⅎ𝑛 𝐴 ∈ Fin
11		nfra1 3253	. . . . . 6 ⊢ Ⅎ𝑛∀𝑛 ∈ 𝐴 𝐵 ∈ dom vol
12		nfdisj1 5069	. . . . . 6 ⊢ Ⅎ𝑛Disj 𝑛 ∈ 𝐴 𝐵
13	10, 11, 12	nf3an 1901	. . . . 5 ⊢ Ⅎ𝑛(𝐴 ∈ Fin ∧ ∀𝑛 ∈ 𝐴 𝐵 ∈ dom vol ∧ Disj 𝑛 ∈ 𝐴 𝐵)
14		nfra1 3253	. . . . 5 ⊢ Ⅎ𝑛∀𝑛 ∈ 𝐴 (vol‘𝐵) ∈ ℝ
15	13, 14	nfan 1899	. . . 4 ⊢ Ⅎ𝑛((𝐴 ∈ Fin ∧ ∀𝑛 ∈ 𝐴 𝐵 ∈ dom vol ∧ Disj 𝑛 ∈ 𝐴 𝐵) ∧ ∀𝑛 ∈ 𝐴 (vol‘𝐵) ∈ ℝ)
16	3	r19.21bi 3221	. . . . 5 ⊢ ((((𝐴 ∈ Fin ∧ ∀𝑛 ∈ 𝐴 𝐵 ∈ dom vol ∧ Disj 𝑛 ∈ 𝐴 𝐵) ∧ ∀𝑛 ∈ 𝐴 (vol‘𝐵) ∈ ℝ) ∧ 𝑛 ∈ 𝐴) → (vol‘𝐵) ∈ ℝ)
17		rspa 3218	. . . . . . . 8 ⊢ ((∀𝑛 ∈ 𝐴 𝐵 ∈ dom vol ∧ 𝑛 ∈ 𝐴) → 𝐵 ∈ dom vol)
18		volf 25411	. . . . . . . . 9 ⊢ vol:dom vol⟶(0[,]+∞)
19	18	ffvelcdmi 7010	. . . . . . . 8 ⊢ (𝐵 ∈ dom vol → (vol‘𝐵) ∈ (0[,]+∞))
20	17, 19	syl 17	. . . . . . 7 ⊢ ((∀𝑛 ∈ 𝐴 𝐵 ∈ dom vol ∧ 𝑛 ∈ 𝐴) → (vol‘𝐵) ∈ (0[,]+∞))
21	2, 20	sylan 580	. . . . . 6 ⊢ ((((𝐴 ∈ Fin ∧ ∀𝑛 ∈ 𝐴 𝐵 ∈ dom vol ∧ Disj 𝑛 ∈ 𝐴 𝐵) ∧ ∀𝑛 ∈ 𝐴 (vol‘𝐵) ∈ ℝ) ∧ 𝑛 ∈ 𝐴) → (vol‘𝐵) ∈ (0[,]+∞))
22		0xr 11150	. . . . . . . 8 ⊢ 0 ∈ ℝ^*
23		pnfxr 11157	. . . . . . . 8 ⊢ +∞ ∈ ℝ^*
24		elicc1 13280	. . . . . . . 8 ⊢ ((0 ∈ ℝ^* ∧ +∞ ∈ ℝ^) → ((vol‘𝐵) ∈ (0[,]+∞) ↔ ((vol‘𝐵) ∈ ℝ^ ∧ 0 ≤ (vol‘𝐵) ∧ (vol‘𝐵) ≤ +∞)))
25	22, 23, 24	mp2an 692	. . . . . . 7 ⊢ ((vol‘𝐵) ∈ (0[,]+∞) ↔ ((vol‘𝐵) ∈ ℝ^* ∧ 0 ≤ (vol‘𝐵) ∧ (vol‘𝐵) ≤ +∞))
26	25	simp2bi 1146	. . . . . 6 ⊢ ((vol‘𝐵) ∈ (0[,]+∞) → 0 ≤ (vol‘𝐵))
27	21, 26	syl 17	. . . . 5 ⊢ ((((𝐴 ∈ Fin ∧ ∀𝑛 ∈ 𝐴 𝐵 ∈ dom vol ∧ Disj 𝑛 ∈ 𝐴 𝐵) ∧ ∀𝑛 ∈ 𝐴 (vol‘𝐵) ∈ ℝ) ∧ 𝑛 ∈ 𝐴) → 0 ≤ (vol‘𝐵))
28		ltpnf 13010	. . . . . 6 ⊢ ((vol‘𝐵) ∈ ℝ → (vol‘𝐵) < +∞)
29	16, 28	syl 17	. . . . 5 ⊢ ((((𝐴 ∈ Fin ∧ ∀𝑛 ∈ 𝐴 𝐵 ∈ dom vol ∧ Disj 𝑛 ∈ 𝐴 𝐵) ∧ ∀𝑛 ∈ 𝐴 (vol‘𝐵) ∈ ℝ) ∧ 𝑛 ∈ 𝐴) → (vol‘𝐵) < +∞)
30		0re 11105	. . . . . 6 ⊢ 0 ∈ ℝ
31		elico2 13301	. . . . . 6 ⊢ ((0 ∈ ℝ ∧ +∞ ∈ ℝ^*) → ((vol‘𝐵) ∈ (0[,)+∞) ↔ ((vol‘𝐵) ∈ ℝ ∧ 0 ≤ (vol‘𝐵) ∧ (vol‘𝐵) < +∞)))
32	30, 23, 31	mp2an 692	. . . . 5 ⊢ ((vol‘𝐵) ∈ (0[,)+∞) ↔ ((vol‘𝐵) ∈ ℝ ∧ 0 ≤ (vol‘𝐵) ∧ (vol‘𝐵) < +∞))
33	16, 27, 29, 32	syl3anbrc 1344	. . . 4 ⊢ ((((𝐴 ∈ Fin ∧ ∀𝑛 ∈ 𝐴 𝐵 ∈ dom vol ∧ Disj 𝑛 ∈ 𝐴 𝐵) ∧ ∀𝑛 ∈ 𝐴 (vol‘𝐵) ∈ ℝ) ∧ 𝑛 ∈ 𝐴) → (vol‘𝐵) ∈ (0[,)+∞))
34	9, 15, 1, 33	esumpfinvalf 34057	. . 3 ⊢ (((𝐴 ∈ Fin ∧ ∀𝑛 ∈ 𝐴 𝐵 ∈ dom vol ∧ Disj 𝑛 ∈ 𝐴 𝐵) ∧ ∀𝑛 ∈ 𝐴 (vol‘𝐵) ∈ ℝ) → Σ^*𝑛 ∈ 𝐴(vol‘𝐵) = Σ𝑛 ∈ 𝐴 (vol‘𝐵))
35	8, 34	eqtr4d 2767	. 2 ⊢ (((𝐴 ∈ Fin ∧ ∀𝑛 ∈ 𝐴 𝐵 ∈ dom vol ∧ Disj 𝑛 ∈ 𝐴 𝐵) ∧ ∀𝑛 ∈ 𝐴 (vol‘𝐵) ∈ ℝ) → (vol‘∪ 𝑛 ∈ 𝐴 𝐵) = Σ^*𝑛 ∈ 𝐴(vol‘𝐵))
36		simpr 484	. . . . . . . 8 ⊢ (((𝐴 ∈ Fin ∧ ∀𝑛 ∈ 𝐴 𝐵 ∈ dom vol ∧ Disj 𝑛 ∈ 𝐴 𝐵) ∧ ∃𝑛 ∈ 𝐴 (vol‘𝐵) = +∞) → ∃𝑛 ∈ 𝐴 (vol‘𝐵) = +∞)
37		nfv 1914	. . . . . . . . 9 ⊢ Ⅎ𝑘(vol‘𝐵) = +∞
38		nfcv 2891	. . . . . . . . . . 11 ⊢ Ⅎ𝑛vol
39		nfcsb1v 3871	. . . . . . . . . . 11 ⊢ Ⅎ𝑛⦋𝑘 / 𝑛⦌𝐵
40	38, 39	nffv 6826	. . . . . . . . . 10 ⊢ Ⅎ𝑛(vol‘⦋𝑘 / 𝑛⦌𝐵)
41	40	nfeq1 2907	. . . . . . . . 9 ⊢ Ⅎ𝑛(vol‘⦋𝑘 / 𝑛⦌𝐵) = +∞
42		csbeq1a 3861	. . . . . . . . . 10 ⊢ (𝑛 = 𝑘 → 𝐵 = ⦋𝑘 / 𝑛⦌𝐵)
43	42	fveqeq2d 6824	. . . . . . . . 9 ⊢ (𝑛 = 𝑘 → ((vol‘𝐵) = +∞ ↔ (vol‘⦋𝑘 / 𝑛⦌𝐵) = +∞))
44	37, 41, 43	cbvrexw 3272	. . . . . . . 8 ⊢ (∃𝑛 ∈ 𝐴 (vol‘𝐵) = +∞ ↔ ∃𝑘 ∈ 𝐴 (vol‘⦋𝑘 / 𝑛⦌𝐵) = +∞)
45	36, 44	sylib 218	. . . . . . 7 ⊢ (((𝐴 ∈ Fin ∧ ∀𝑛 ∈ 𝐴 𝐵 ∈ dom vol ∧ Disj 𝑛 ∈ 𝐴 𝐵) ∧ ∃𝑛 ∈ 𝐴 (vol‘𝐵) = +∞) → ∃𝑘 ∈ 𝐴 (vol‘⦋𝑘 / 𝑛⦌𝐵) = +∞)
46	39	nfel1 2908	. . . . . . . . . . . . . 14 ⊢ Ⅎ𝑛⦋𝑘 / 𝑛⦌𝐵 ∈ dom vol
47	42	eleq1d 2813	. . . . . . . . . . . . . 14 ⊢ (𝑛 = 𝑘 → (𝐵 ∈ dom vol ↔ ⦋𝑘 / 𝑛⦌𝐵 ∈ dom vol))
48	46, 47	rspc 3562	. . . . . . . . . . . . 13 ⊢ (𝑘 ∈ 𝐴 → (∀𝑛 ∈ 𝐴 𝐵 ∈ dom vol → ⦋𝑘 / 𝑛⦌𝐵 ∈ dom vol))
49	48	impcom 407	. . . . . . . . . . . 12 ⊢ ((∀𝑛 ∈ 𝐴 𝐵 ∈ dom vol ∧ 𝑘 ∈ 𝐴) → ⦋𝑘 / 𝑛⦌𝐵 ∈ dom vol)
50	49	adantll 714	. . . . . . . . . . 11 ⊢ (((𝐴 ∈ Fin ∧ ∀𝑛 ∈ 𝐴 𝐵 ∈ dom vol) ∧ 𝑘 ∈ 𝐴) → ⦋𝑘 / 𝑛⦌𝐵 ∈ dom vol)
51		finiunmbl 25426	. . . . . . . . . . . 12 ⊢ ((𝐴 ∈ Fin ∧ ∀𝑛 ∈ 𝐴 𝐵 ∈ dom vol) → ∪ 𝑛 ∈ 𝐴 𝐵 ∈ dom vol)
52	51	adantr 480	. . . . . . . . . . 11 ⊢ (((𝐴 ∈ Fin ∧ ∀𝑛 ∈ 𝐴 𝐵 ∈ dom vol) ∧ 𝑘 ∈ 𝐴) → ∪ 𝑛 ∈ 𝐴 𝐵 ∈ dom vol)
53		nfcv 2891	. . . . . . . . . . . . 13 ⊢ Ⅎ𝑛𝑘
54	9, 53, 39, 42	ssiun2sf 32491	. . . . . . . . . . . 12 ⊢ (𝑘 ∈ 𝐴 → ⦋𝑘 / 𝑛⦌𝐵 ⊆ ∪ 𝑛 ∈ 𝐴 𝐵)
55	54	adantl 481	. . . . . . . . . . 11 ⊢ (((𝐴 ∈ Fin ∧ ∀𝑛 ∈ 𝐴 𝐵 ∈ dom vol) ∧ 𝑘 ∈ 𝐴) → ⦋𝑘 / 𝑛⦌𝐵 ⊆ ∪ 𝑛 ∈ 𝐴 𝐵)
56		volss 25415	. . . . . . . . . . 11 ⊢ ((⦋𝑘 / 𝑛⦌𝐵 ∈ dom vol ∧ ∪ 𝑛 ∈ 𝐴 𝐵 ∈ dom vol ∧ ⦋𝑘 / 𝑛⦌𝐵 ⊆ ∪ 𝑛 ∈ 𝐴 𝐵) → (vol‘⦋𝑘 / 𝑛⦌𝐵) ≤ (vol‘∪ 𝑛 ∈ 𝐴 𝐵))
57	50, 52, 55, 56	syl3anc 1373	. . . . . . . . . 10 ⊢ (((𝐴 ∈ Fin ∧ ∀𝑛 ∈ 𝐴 𝐵 ∈ dom vol) ∧ 𝑘 ∈ 𝐴) → (vol‘⦋𝑘 / 𝑛⦌𝐵) ≤ (vol‘∪ 𝑛 ∈ 𝐴 𝐵))
58	57	3adantl3 1169	. . . . . . . . 9 ⊢ (((𝐴 ∈ Fin ∧ ∀𝑛 ∈ 𝐴 𝐵 ∈ dom vol ∧ Disj 𝑛 ∈ 𝐴 𝐵) ∧ 𝑘 ∈ 𝐴) → (vol‘⦋𝑘 / 𝑛⦌𝐵) ≤ (vol‘∪ 𝑛 ∈ 𝐴 𝐵))
59	58	adantlr 715	. . . . . . . 8 ⊢ ((((𝐴 ∈ Fin ∧ ∀𝑛 ∈ 𝐴 𝐵 ∈ dom vol ∧ Disj 𝑛 ∈ 𝐴 𝐵) ∧ ∃𝑛 ∈ 𝐴 (vol‘𝐵) = +∞) ∧ 𝑘 ∈ 𝐴) → (vol‘⦋𝑘 / 𝑛⦌𝐵) ≤ (vol‘∪ 𝑛 ∈ 𝐴 𝐵))
60	59	ralrimiva 3121	. . . . . . 7 ⊢ (((𝐴 ∈ Fin ∧ ∀𝑛 ∈ 𝐴 𝐵 ∈ dom vol ∧ Disj 𝑛 ∈ 𝐴 𝐵) ∧ ∃𝑛 ∈ 𝐴 (vol‘𝐵) = +∞) → ∀𝑘 ∈ 𝐴 (vol‘⦋𝑘 / 𝑛⦌𝐵) ≤ (vol‘∪ 𝑛 ∈ 𝐴 𝐵))
61		r19.29r 3093	. . . . . . 7 ⊢ ((∃𝑘 ∈ 𝐴 (vol‘⦋𝑘 / 𝑛⦌𝐵) = +∞ ∧ ∀𝑘 ∈ 𝐴 (vol‘⦋𝑘 / 𝑛⦌𝐵) ≤ (vol‘∪ 𝑛 ∈ 𝐴 𝐵)) → ∃𝑘 ∈ 𝐴 ((vol‘⦋𝑘 / 𝑛⦌𝐵) = +∞ ∧ (vol‘⦋𝑘 / 𝑛⦌𝐵) ≤ (vol‘∪ 𝑛 ∈ 𝐴 𝐵)))
62	45, 60, 61	syl2anc 584	. . . . . 6 ⊢ (((𝐴 ∈ Fin ∧ ∀𝑛 ∈ 𝐴 𝐵 ∈ dom vol ∧ Disj 𝑛 ∈ 𝐴 𝐵) ∧ ∃𝑛 ∈ 𝐴 (vol‘𝐵) = +∞) → ∃𝑘 ∈ 𝐴 ((vol‘⦋𝑘 / 𝑛⦌𝐵) = +∞ ∧ (vol‘⦋𝑘 / 𝑛⦌𝐵) ≤ (vol‘∪ 𝑛 ∈ 𝐴 𝐵)))
63		breq1 5091	. . . . . . . 8 ⊢ ((vol‘⦋𝑘 / 𝑛⦌𝐵) = +∞ → ((vol‘⦋𝑘 / 𝑛⦌𝐵) ≤ (vol‘∪ 𝑛 ∈ 𝐴 𝐵) ↔ +∞ ≤ (vol‘∪ 𝑛 ∈ 𝐴 𝐵)))
64	63	biimpa 476	. . . . . . 7 ⊢ (((vol‘⦋𝑘 / 𝑛⦌𝐵) = +∞ ∧ (vol‘⦋𝑘 / 𝑛⦌𝐵) ≤ (vol‘∪ 𝑛 ∈ 𝐴 𝐵)) → +∞ ≤ (vol‘∪ 𝑛 ∈ 𝐴 𝐵))
65	64	reximi 3067	. . . . . 6 ⊢ (∃𝑘 ∈ 𝐴 ((vol‘⦋𝑘 / 𝑛⦌𝐵) = +∞ ∧ (vol‘⦋𝑘 / 𝑛⦌𝐵) ≤ (vol‘∪ 𝑛 ∈ 𝐴 𝐵)) → ∃𝑘 ∈ 𝐴 +∞ ≤ (vol‘∪ 𝑛 ∈ 𝐴 𝐵))
66	62, 65	syl 17	. . . . 5 ⊢ (((𝐴 ∈ Fin ∧ ∀𝑛 ∈ 𝐴 𝐵 ∈ dom vol ∧ Disj 𝑛 ∈ 𝐴 𝐵) ∧ ∃𝑛 ∈ 𝐴 (vol‘𝐵) = +∞) → ∃𝑘 ∈ 𝐴 +∞ ≤ (vol‘∪ 𝑛 ∈ 𝐴 𝐵))
67		rexex 3059	. . . . . 6 ⊢ (∃𝑘 ∈ 𝐴 +∞ ≤ (vol‘∪ 𝑛 ∈ 𝐴 𝐵) → ∃𝑘+∞ ≤ (vol‘∪ 𝑛 ∈ 𝐴 𝐵))
68		19.9v 1984	. . . . . 6 ⊢ (∃𝑘+∞ ≤ (vol‘∪ 𝑛 ∈ 𝐴 𝐵) ↔ +∞ ≤ (vol‘∪ 𝑛 ∈ 𝐴 𝐵))
69	67, 68	sylib 218	. . . . 5 ⊢ (∃𝑘 ∈ 𝐴 +∞ ≤ (vol‘∪ 𝑛 ∈ 𝐴 𝐵) → +∞ ≤ (vol‘∪ 𝑛 ∈ 𝐴 𝐵))
70	66, 69	syl 17	. . . 4 ⊢ (((𝐴 ∈ Fin ∧ ∀𝑛 ∈ 𝐴 𝐵 ∈ dom vol ∧ Disj 𝑛 ∈ 𝐴 𝐵) ∧ ∃𝑛 ∈ 𝐴 (vol‘𝐵) = +∞) → +∞ ≤ (vol‘∪ 𝑛 ∈ 𝐴 𝐵))
71		iccssxr 13321	. . . . . . . . 9 ⊢ (0[,]+∞) ⊆ ℝ^*
72	18	ffvelcdmi 7010	. . . . . . . . 9 ⊢ (∪ 𝑛 ∈ 𝐴 𝐵 ∈ dom vol → (vol‘∪ 𝑛 ∈ 𝐴 𝐵) ∈ (0[,]+∞))
73	71, 72	sselid 3929	. . . . . . . 8 ⊢ (∪ 𝑛 ∈ 𝐴 𝐵 ∈ dom vol → (vol‘∪ 𝑛 ∈ 𝐴 𝐵) ∈ ℝ^*)
74	51, 73	syl 17	. . . . . . 7 ⊢ ((𝐴 ∈ Fin ∧ ∀𝑛 ∈ 𝐴 𝐵 ∈ dom vol) → (vol‘∪ 𝑛 ∈ 𝐴 𝐵) ∈ ℝ^*)
75	74	3adant3 1132	. . . . . 6 ⊢ ((𝐴 ∈ Fin ∧ ∀𝑛 ∈ 𝐴 𝐵 ∈ dom vol ∧ Disj 𝑛 ∈ 𝐴 𝐵) → (vol‘∪ 𝑛 ∈ 𝐴 𝐵) ∈ ℝ^*)
76	75	adantr 480	. . . . 5 ⊢ (((𝐴 ∈ Fin ∧ ∀𝑛 ∈ 𝐴 𝐵 ∈ dom vol ∧ Disj 𝑛 ∈ 𝐴 𝐵) ∧ ∃𝑛 ∈ 𝐴 (vol‘𝐵) = +∞) → (vol‘∪ 𝑛 ∈ 𝐴 𝐵) ∈ ℝ^*)
77		xgepnf 13055	. . . . 5 ⊢ ((vol‘∪ 𝑛 ∈ 𝐴 𝐵) ∈ ℝ^* → (+∞ ≤ (vol‘∪ 𝑛 ∈ 𝐴 𝐵) ↔ (vol‘∪ 𝑛 ∈ 𝐴 𝐵) = +∞))
78	76, 77	syl 17	. . . 4 ⊢ (((𝐴 ∈ Fin ∧ ∀𝑛 ∈ 𝐴 𝐵 ∈ dom vol ∧ Disj 𝑛 ∈ 𝐴 𝐵) ∧ ∃𝑛 ∈ 𝐴 (vol‘𝐵) = +∞) → (+∞ ≤ (vol‘∪ 𝑛 ∈ 𝐴 𝐵) ↔ (vol‘∪ 𝑛 ∈ 𝐴 𝐵) = +∞))
79	70, 78	mpbid 232	. . 3 ⊢ (((𝐴 ∈ Fin ∧ ∀𝑛 ∈ 𝐴 𝐵 ∈ dom vol ∧ Disj 𝑛 ∈ 𝐴 𝐵) ∧ ∃𝑛 ∈ 𝐴 (vol‘𝐵) = +∞) → (vol‘∪ 𝑛 ∈ 𝐴 𝐵) = +∞)
80		nfre1 3254	. . . . 5 ⊢ Ⅎ𝑛∃𝑛 ∈ 𝐴 (vol‘𝐵) = +∞
81	13, 80	nfan 1899	. . . 4 ⊢ Ⅎ𝑛((𝐴 ∈ Fin ∧ ∀𝑛 ∈ 𝐴 𝐵 ∈ dom vol ∧ Disj 𝑛 ∈ 𝐴 𝐵) ∧ ∃𝑛 ∈ 𝐴 (vol‘𝐵) = +∞)
82		simpl1 1192	. . . 4 ⊢ (((𝐴 ∈ Fin ∧ ∀𝑛 ∈ 𝐴 𝐵 ∈ dom vol ∧ Disj 𝑛 ∈ 𝐴 𝐵) ∧ ∃𝑛 ∈ 𝐴 (vol‘𝐵) = +∞) → 𝐴 ∈ Fin)
83	20	3ad2antl2 1187	. . . . 5 ⊢ (((𝐴 ∈ Fin ∧ ∀𝑛 ∈ 𝐴 𝐵 ∈ dom vol ∧ Disj 𝑛 ∈ 𝐴 𝐵) ∧ 𝑛 ∈ 𝐴) → (vol‘𝐵) ∈ (0[,]+∞))
84	83	adantlr 715	. . . 4 ⊢ ((((𝐴 ∈ Fin ∧ ∀𝑛 ∈ 𝐴 𝐵 ∈ dom vol ∧ Disj 𝑛 ∈ 𝐴 𝐵) ∧ ∃𝑛 ∈ 𝐴 (vol‘𝐵) = +∞) ∧ 𝑛 ∈ 𝐴) → (vol‘𝐵) ∈ (0[,]+∞))
85	81, 82, 84, 36	esumpinfval 34054	. . 3 ⊢ (((𝐴 ∈ Fin ∧ ∀𝑛 ∈ 𝐴 𝐵 ∈ dom vol ∧ Disj 𝑛 ∈ 𝐴 𝐵) ∧ ∃𝑛 ∈ 𝐴 (vol‘𝐵) = +∞) → Σ^*𝑛 ∈ 𝐴(vol‘𝐵) = +∞)
86	79, 85	eqtr4d 2767	. 2 ⊢ (((𝐴 ∈ Fin ∧ ∀𝑛 ∈ 𝐴 𝐵 ∈ dom vol ∧ Disj 𝑛 ∈ 𝐴 𝐵) ∧ ∃𝑛 ∈ 𝐴 (vol‘𝐵) = +∞) → (vol‘∪ 𝑛 ∈ 𝐴 𝐵) = Σ^*𝑛 ∈ 𝐴(vol‘𝐵))
87		exmid 894	. . . . 5 ⊢ (∀𝑛 ∈ 𝐴 (vol‘𝐵) ∈ ℝ ∨ ¬ ∀𝑛 ∈ 𝐴 (vol‘𝐵) ∈ ℝ)
88		rexnal 3081	. . . . . 6 ⊢ (∃𝑛 ∈ 𝐴 ¬ (vol‘𝐵) ∈ ℝ ↔ ¬ ∀𝑛 ∈ 𝐴 (vol‘𝐵) ∈ ℝ)
89	88	orbi2i 912	. . . . 5 ⊢ ((∀𝑛 ∈ 𝐴 (vol‘𝐵) ∈ ℝ ∨ ∃𝑛 ∈ 𝐴 ¬ (vol‘𝐵) ∈ ℝ) ↔ (∀𝑛 ∈ 𝐴 (vol‘𝐵) ∈ ℝ ∨ ¬ ∀𝑛 ∈ 𝐴 (vol‘𝐵) ∈ ℝ))
90	87, 89	mpbir 231	. . . 4 ⊢ (∀𝑛 ∈ 𝐴 (vol‘𝐵) ∈ ℝ ∨ ∃𝑛 ∈ 𝐴 ¬ (vol‘𝐵) ∈ ℝ)
91		r19.29 3092	. . . . . . 7 ⊢ ((∀𝑛 ∈ 𝐴 𝐵 ∈ dom vol ∧ ∃𝑛 ∈ 𝐴 ¬ (vol‘𝐵) ∈ ℝ) → ∃𝑛 ∈ 𝐴 (𝐵 ∈ dom vol ∧ ¬ (vol‘𝐵) ∈ ℝ))
92		xrge0nre 13344	. . . . . . . . 9 ⊢ (((vol‘𝐵) ∈ (0[,]+∞) ∧ ¬ (vol‘𝐵) ∈ ℝ) → (vol‘𝐵) = +∞)
93	19, 92	sylan 580	. . . . . . . 8 ⊢ ((𝐵 ∈ dom vol ∧ ¬ (vol‘𝐵) ∈ ℝ) → (vol‘𝐵) = +∞)
94	93	reximi 3067	. . . . . . 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 968	. . . 4 ⊢ (∀𝑛 ∈ 𝐴 𝐵 ∈ dom vol → ((∀𝑛 ∈ 𝐴 (vol‘𝐵) ∈ ℝ ∨ ∃𝑛 ∈ 𝐴 ¬ (vol‘𝐵) ∈ ℝ) → (∀𝑛 ∈ 𝐴 (vol‘𝐵) ∈ ℝ ∨ ∃𝑛 ∈ 𝐴 (vol‘𝐵) = +∞)))
98	90, 97	mpi 20	. . 3 ⊢ (∀𝑛 ∈ 𝐴 𝐵 ∈ dom vol → (∀𝑛 ∈ 𝐴 (vol‘𝐵) ∈ ℝ ∨ ∃𝑛 ∈ 𝐴 (vol‘𝐵) = +∞))
99	98	3ad2ant2 1134	. 2 ⊢ ((𝐴 ∈ Fin ∧ ∀𝑛 ∈ 𝐴 𝐵 ∈ dom vol ∧ Disj 𝑛 ∈ 𝐴 𝐵) → (∀𝑛 ∈ 𝐴 (vol‘𝐵) ∈ ℝ ∨ ∃𝑛 ∈ 𝐴 (vol‘𝐵) = +∞))
100	35, 86, 99	mpjaodan 960	1 ⊢ ((𝐴 ∈ Fin ∧ ∀𝑛 ∈ 𝐴 𝐵 ∈ dom vol ∧ Disj 𝑛 ∈ 𝐴 𝐵) → (vol‘∪ 𝑛 ∈ 𝐴 𝐵) = Σ^*𝑛 ∈ 𝐴(vol‘𝐵))

Colors of variables: wff setvar class

Syntax hints: ¬ wn 3 → wi 4 ↔ wb 206 ∧ wa 395 ∨ wo 847 ∧ w3a 1086 = wceq 1540 ∃wex 1779 ∈ wcel 2109 ∀wral 3044 ∃wrex 3053 ⦋csb 3847 ⊆ wss 3899 ∪ ciun 4938 Disj wdisj 5055 class class class wbr 5088 dom cdm 5613 ‘cfv 6476 (class class class)co 7340 Fincfn 8863 ℝcr 10996 0cc0 10997 +∞cpnf 11134 ℝ^*cxr 11136 < clt 11137 ≤ cle 11138 [,)cico 13238 [,]cicc 13239 Σcsu 15580 volcvol 25345 Σ^*cesum 34008

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 2008 ax-8 2111 ax-9 2119 ax-10 2142 ax-11 2158 ax-12 2178 ax-ext 2701 ax-rep 5214 ax-sep 5231 ax-nul 5241 ax-pow 5300 ax-pr 5367 ax-un 7662 ax-inf2 9525 ax-cnex 11053 ax-resscn 11054 ax-1cn 11055 ax-icn 11056 ax-addcl 11057 ax-addrcl 11058 ax-mulcl 11059 ax-mulrcl 11060 ax-mulcom 11061 ax-addass 11062 ax-mulass 11063 ax-distr 11064 ax-i2m1 11065 ax-1ne0 11066 ax-1rid 11067 ax-rnegex 11068 ax-rrecex 11069 ax-cnre 11070 ax-pre-lttri 11071 ax-pre-lttrn 11072 ax-pre-ltadd 11073 ax-pre-mulgt0 11074 ax-pre-sup 11075 ax-addf 11076 ax-mulf 11077

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 2066 df-mo 2533 df-eu 2562 df-clab 2708 df-cleq 2721 df-clel 2803 df-nfc 2878 df-ne 2926 df-nel 3030 df-ral 3045 df-rex 3054 df-rmo 3343 df-reu 3344 df-rab 3393 df-v 3435 df-sbc 3739 df-csb 3848 df-dif 3902 df-un 3904 df-in 3906 df-ss 3916 df-pss 3919 df-nul 4281 df-if 4473 df-pw 4549 df-sn 4574 df-pr 4576 df-tp 4578 df-op 4580 df-uni 4857 df-int 4895 df-iun 4940 df-iin 4941 df-disj 5056 df-br 5089 df-opab 5151 df-mpt 5170 df-tr 5196 df-id 5508 df-eprel 5513 df-po 5521 df-so 5522 df-fr 5566 df-se 5567 df-we 5568 df-xp 5619 df-rel 5620 df-cnv 5621 df-co 5622 df-dm 5623 df-rn 5624 df-res 5625 df-ima 5626 df-pred 6243 df-ord 6304 df-on 6305 df-lim 6306 df-suc 6307 df-iota 6432 df-fun 6478 df-fn 6479 df-f 6480 df-f1 6481 df-fo 6482 df-f1o 6483 df-fv 6484 df-isom 6485 df-riota 7297 df-ov 7343 df-oprab 7344 df-mpo 7345 df-of 7604 df-om 7791 df-1st 7915 df-2nd 7916 df-supp 8085 df-frecs 8205 df-wrecs 8236 df-recs 8285 df-rdg 8323 df-1o 8379 df-2o 8380 df-oadd 8383 df-er 8616 df-map 8746 df-pm 8747 df-ixp 8816 df-en 8864 df-dom 8865 df-sdom 8866 df-fin 8867 df-fsupp 9240 df-fi 9289 df-sup 9320 df-inf 9321 df-oi 9390 df-dju 9785 df-card 9823 df-pnf 11139 df-mnf 11140 df-xr 11141 df-ltxr 11142 df-le 11143 df-sub 11337 df-neg 11338 df-div 11766 df-nn 12117 df-2 12179 df-3 12180 df-4 12181 df-5 12182 df-6 12183 df-7 12184 df-8 12185 df-9 12186 df-n0 12373 df-xnn0 12446 df-z 12460 df-dec 12580 df-uz 12724 df-q 12838 df-rp 12882 df-xneg 13002 df-xadd 13003 df-xmul 13004 df-ioo 13240 df-ioc 13241 df-ico 13242 df-icc 13243 df-fz 13399 df-fzo 13546 df-fl 13684 df-mod 13762 df-seq 13897 df-exp 13957 df-fac 14169 df-bc 14198 df-hash 14226 df-shft 14961 df-cj 14993 df-re 14994 df-im 14995 df-sqrt 15129 df-abs 15130 df-limsup 15365 df-clim 15382 df-rlim 15383 df-sum 15581 df-ef 15961 df-sin 15963 df-cos 15964 df-pi 15966 df-struct 17045 df-sets 17062 df-slot 17080 df-ndx 17092 df-base 17108 df-ress 17129 df-plusg 17161 df-mulr 17162 df-starv 17163 df-sca 17164 df-vsca 17165 df-ip 17166 df-tset 17167 df-ple 17168 df-ds 17170 df-unif 17171 df-hom 17172 df-cco 17173 df-rest 17313 df-topn 17314 df-0g 17332 df-gsum 17333 df-topgen 17334 df-pt 17335 df-prds 17338 df-ordt 17392 df-xrs 17393 df-qtop 17398 df-imas 17399 df-xps 17401 df-mre 17475 df-mrc 17476 df-acs 17478 df-ps 18459 df-tsr 18460 df-plusf 18500 df-mgm 18501 df-sgrp 18580 df-mnd 18596 df-mhm 18644 df-submnd 18645 df-grp 18802 df-minusg 18803 df-sbg 18804 df-mulg 18934 df-subg 18989 df-cntz 19183 df-cmn 19648 df-abl 19649 df-mgp 20013 df-rng 20025 df-ur 20054 df-ring 20107 df-cring 20108 df-subrng 20415 df-subrg 20439 df-abv 20678 df-lmod 20749 df-scaf 20750 df-sra 21061 df-rgmod 21062 df-psmet 21237 df-xmet 21238 df-met 21239 df-bl 21240 df-mopn 21241 df-fbas 21242 df-fg 21243 df-cnfld 21246 df-top 22763 df-topon 22780 df-topsp 22802 df-bases 22815 df-cld 22888 df-ntr 22889 df-cls 22890 df-nei 22967 df-lp 23005 df-perf 23006 df-cn 23096 df-cnp 23097 df-haus 23184 df-tx 23431 df-hmeo 23624 df-fil 23715 df-fm 23807 df-flim 23808 df-flf 23809 df-tmd 23941 df-tgp 23942 df-tsms 23996 df-trg 24029 df-xms 24189 df-ms 24190 df-tms 24191 df-nm 24451 df-ngp 24452 df-nrg 24454 df-nlm 24455 df-ii 24751 df-cncf 24752 df-ovol 25346 df-vol 25347 df-limc 25748 df-dv 25749 df-log 26446 df-esum 34009

This theorem is referenced by: volmeas 34212

W3C validator