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 34216

Description: The Lebesgue measure function is countably additive. This theorem is to volfiniun 25465 what voliune 34215 is to voliun 25472. (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 25465	. . . 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 5076	. . . . . 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 25447	. . . . . . . . 9 ⊢ vol:dom vol⟶(0[,]+∞)
19	18	ffvelcdmi 7021	. . . . . . . 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 11181	. . . . . . . 8 ⊢ 0 ∈ ℝ^*
23		pnfxr 11188	. . . . . . . 8 ⊢ +∞ ∈ ℝ^*
24		elicc1 13311	. . . . . . . 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 13041	. . . . . 6 ⊢ ((vol‘𝐵) ∈ ℝ → (vol‘𝐵) < +∞)
29	16, 28	syl 17	. . . . 5 ⊢ ((((𝐴 ∈ Fin ∧ ∀𝑛 ∈ 𝐴 𝐵 ∈ dom vol ∧ Disj 𝑛 ∈ 𝐴 𝐵) ∧ ∀𝑛 ∈ 𝐴 (vol‘𝐵) ∈ ℝ) ∧ 𝑛 ∈ 𝐴) → (vol‘𝐵) < +∞)
30		0re 11136	. . . . . 6 ⊢ 0 ∈ ℝ
31		elico2 13332	. . . . . 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 34062	. . 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 3877	. . . . . . . . . . 11 ⊢ Ⅎ𝑛⦋𝑘 / 𝑛⦌𝐵
40	38, 39	nffv 6836	. . . . . . . . . 10 ⊢ Ⅎ𝑛(vol‘⦋𝑘 / 𝑛⦌𝐵)
41	40	nfeq1 2907	. . . . . . . . 9 ⊢ Ⅎ𝑛(vol‘⦋𝑘 / 𝑛⦌𝐵) = +∞
42		csbeq1a 3867	. . . . . . . . . 10 ⊢ (𝑛 = 𝑘 → 𝐵 = ⦋𝑘 / 𝑛⦌𝐵)
43	42	fveqeq2d 6834	. . . . . . . . 9 ⊢ (𝑛 = 𝑘 → ((vol‘𝐵) = +∞ ↔ (vol‘⦋𝑘 / 𝑛⦌𝐵) = +∞))
44	37, 41, 43	cbvrexw 3273	. . . . . . . 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 3567	. . . . . . . . . . . . 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 25462	. . . . . . . . . . . 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 32522	. . . . . . . . . . . 12 ⊢ (𝑘 ∈ 𝐴 → ⦋𝑘 / 𝑛⦌𝐵 ⊆ ∪ 𝑛 ∈ 𝐴 𝐵)
55	54	adantl 481	. . . . . . . . . . 11 ⊢ (((𝐴 ∈ Fin ∧ ∀𝑛 ∈ 𝐴 𝐵 ∈ dom vol) ∧ 𝑘 ∈ 𝐴) → ⦋𝑘 / 𝑛⦌𝐵 ⊆ ∪ 𝑛 ∈ 𝐴 𝐵)
56		volss 25451	. . . . . . . . . . 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 5098	. . . . . . . 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 13352	. . . . . . . . 9 ⊢ (0[,]+∞) ⊆ ℝ^*
72	18	ffvelcdmi 7021	. . . . . . . . 9 ⊢ (∪ 𝑛 ∈ 𝐴 𝐵 ∈ dom vol → (vol‘∪ 𝑛 ∈ 𝐴 𝐵) ∈ (0[,]+∞))
73	71, 72	sselid 3935	. . . . . . . 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 13086	. . . . 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 34059	. . 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 13375	. . . . . . . . 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 3853 ⊆ wss 3905 ∪ ciun 4944 Disj wdisj 5062 class class class wbr 5095 dom cdm 5623 ‘cfv 6486 (class class class)co 7353 Fincfn 8879 ℝcr 11027 0cc0 11028 +∞cpnf 11165 ℝ^*cxr 11167 < clt 11168 ≤ cle 11169 [,)cico 13269 [,]cicc 13270 Σcsu 15612 volcvol 25381 Σ^*cesum 34013

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 5221 ax-sep 5238 ax-nul 5248 ax-pow 5307 ax-pr 5374 ax-un 7675 ax-inf2 9556 ax-cnex 11084 ax-resscn 11085 ax-1cn 11086 ax-icn 11087 ax-addcl 11088 ax-addrcl 11089 ax-mulcl 11090 ax-mulrcl 11091 ax-mulcom 11092 ax-addass 11093 ax-mulass 11094 ax-distr 11095 ax-i2m1 11096 ax-1ne0 11097 ax-1rid 11098 ax-rnegex 11099 ax-rrecex 11100 ax-cnre 11101 ax-pre-lttri 11102 ax-pre-lttrn 11103 ax-pre-ltadd 11104 ax-pre-mulgt0 11105 ax-pre-sup 11106 ax-addf 11107 ax-mulf 11108

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 3345 df-reu 3346 df-rab 3397 df-v 3440 df-sbc 3745 df-csb 3854 df-dif 3908 df-un 3910 df-in 3912 df-ss 3922 df-pss 3925 df-nul 4287 df-if 4479 df-pw 4555 df-sn 4580 df-pr 4582 df-tp 4584 df-op 4586 df-uni 4862 df-int 4900 df-iun 4946 df-iin 4947 df-disj 5063 df-br 5096 df-opab 5158 df-mpt 5177 df-tr 5203 df-id 5518 df-eprel 5523 df-po 5531 df-so 5532 df-fr 5576 df-se 5577 df-we 5578 df-xp 5629 df-rel 5630 df-cnv 5631 df-co 5632 df-dm 5633 df-rn 5634 df-res 5635 df-ima 5636 df-pred 6253 df-ord 6314 df-on 6315 df-lim 6316 df-suc 6317 df-iota 6442 df-fun 6488 df-fn 6489 df-f 6490 df-f1 6491 df-fo 6492 df-f1o 6493 df-fv 6494 df-isom 6495 df-riota 7310 df-ov 7356 df-oprab 7357 df-mpo 7358 df-of 7617 df-om 7807 df-1st 7931 df-2nd 7932 df-supp 8101 df-frecs 8221 df-wrecs 8252 df-recs 8301 df-rdg 8339 df-1o 8395 df-2o 8396 df-oadd 8399 df-er 8632 df-map 8762 df-pm 8763 df-ixp 8832 df-en 8880 df-dom 8881 df-sdom 8882 df-fin 8883 df-fsupp 9271 df-fi 9320 df-sup 9351 df-inf 9352 df-oi 9421 df-dju 9816 df-card 9854 df-pnf 11170 df-mnf 11171 df-xr 11172 df-ltxr 11173 df-le 11174 df-sub 11368 df-neg 11369 df-div 11797 df-nn 12148 df-2 12210 df-3 12211 df-4 12212 df-5 12213 df-6 12214 df-7 12215 df-8 12216 df-9 12217 df-n0 12404 df-xnn0 12477 df-z 12491 df-dec 12611 df-uz 12755 df-q 12869 df-rp 12913 df-xneg 13033 df-xadd 13034 df-xmul 13035 df-ioo 13271 df-ioc 13272 df-ico 13273 df-icc 13274 df-fz 13430 df-fzo 13577 df-fl 13715 df-mod 13793 df-seq 13928 df-exp 13988 df-fac 14200 df-bc 14229 df-hash 14257 df-shft 14993 df-cj 15025 df-re 15026 df-im 15027 df-sqrt 15161 df-abs 15162 df-limsup 15397 df-clim 15414 df-rlim 15415 df-sum 15613 df-ef 15993 df-sin 15995 df-cos 15996 df-pi 15998 df-struct 17077 df-sets 17094 df-slot 17112 df-ndx 17124 df-base 17140 df-ress 17161 df-plusg 17193 df-mulr 17194 df-starv 17195 df-sca 17196 df-vsca 17197 df-ip 17198 df-tset 17199 df-ple 17200 df-ds 17202 df-unif 17203 df-hom 17204 df-cco 17205 df-rest 17345 df-topn 17346 df-0g 17364 df-gsum 17365 df-topgen 17366 df-pt 17367 df-prds 17370 df-ordt 17424 df-xrs 17425 df-qtop 17430 df-imas 17431 df-xps 17433 df-mre 17507 df-mrc 17508 df-acs 17510 df-ps 18491 df-tsr 18492 df-plusf 18532 df-mgm 18533 df-sgrp 18612 df-mnd 18628 df-mhm 18676 df-submnd 18677 df-grp 18834 df-minusg 18835 df-sbg 18836 df-mulg 18966 df-subg 19021 df-cntz 19215 df-cmn 19680 df-abl 19681 df-mgp 20045 df-rng 20057 df-ur 20086 df-ring 20139 df-cring 20140 df-subrng 20450 df-subrg 20474 df-abv 20713 df-lmod 20784 df-scaf 20785 df-sra 21096 df-rgmod 21097 df-psmet 21272 df-xmet 21273 df-met 21274 df-bl 21275 df-mopn 21276 df-fbas 21277 df-fg 21278 df-cnfld 21281 df-top 22798 df-topon 22815 df-topsp 22837 df-bases 22850 df-cld 22923 df-ntr 22924 df-cls 22925 df-nei 23002 df-lp 23040 df-perf 23041 df-cn 23131 df-cnp 23132 df-haus 23219 df-tx 23466 df-hmeo 23659 df-fil 23750 df-fm 23842 df-flim 23843 df-flf 23844 df-tmd 23976 df-tgp 23977 df-tsms 24031 df-trg 24064 df-xms 24225 df-ms 24226 df-tms 24227 df-nm 24487 df-ngp 24488 df-nrg 24490 df-nlm 24491 df-ii 24787 df-cncf 24788 df-ovol 25382 df-vol 25383 df-limc 25784 df-dv 25785 df-log 26482 df-esum 34014

This theorem is referenced by: volmeas 34217

W3C validator