Metamath Proof Explorer

Theorem volfiniune

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

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

Proof

Step Hyp Ref Expression
1 simpl1 ⊢ ( ( ( 𝐴 ∈ Fin ∧ ∀ 𝑛 ∈ 𝐴 𝐵 ∈ dom vol ∧ Disj 𝑛 ∈ 𝐴 𝐵 ) ∧ ∀ 𝑛 ∈ 𝐴 ( vol ‘ 𝐵 ) ∈ ℝ ) → 𝐴 ∈ Fin )
2 simpl2 ⊢ ( ( ( 𝐴 ∈ Fin ∧ ∀ 𝑛 ∈ 𝐴 𝐵 ∈ dom vol ∧ Disj 𝑛 ∈ 𝐴 𝐵 ) ∧ ∀ 𝑛 ∈ 𝐴 ( vol ‘ 𝐵 ) ∈ ℝ ) → ∀ 𝑛 ∈ 𝐴 𝐵 ∈ dom vol )
3 simpr ⊢ ( ( ( 𝐴 ∈ Fin ∧ ∀ 𝑛 ∈ 𝐴 𝐵 ∈ dom vol ∧ Disj 𝑛 ∈ 𝐴 𝐵 ) ∧ ∀ 𝑛 ∈ 𝐴 ( vol ‘ 𝐵 ) ∈ ℝ ) → ∀ 𝑛 ∈ 𝐴 ( vol ‘ 𝐵 ) ∈ ℝ )
4 r19.26 ⊢ ( ∀ 𝑛 ∈ 𝐴 ( 𝐵 ∈ dom vol ∧ ( vol ‘ 𝐵 ) ∈ ℝ ) ↔ ( ∀ 𝑛 ∈ 𝐴 𝐵 ∈ dom vol ∧ ∀ 𝑛 ∈ 𝐴 ( vol ‘ 𝐵 ) ∈ ℝ ) )
5 2 3 4 sylanbrc ⊢ ( ( ( 𝐴 ∈ Fin ∧ ∀ 𝑛 ∈ 𝐴 𝐵 ∈ dom vol ∧ Disj 𝑛 ∈ 𝐴 𝐵 ) ∧ ∀ 𝑛 ∈ 𝐴 ( vol ‘ 𝐵 ) ∈ ℝ ) → ∀ 𝑛 ∈ 𝐴 ( 𝐵 ∈ dom vol ∧ ( vol ‘ 𝐵 ) ∈ ℝ ) )
6 simpl3 ⊢ ( ( ( 𝐴 ∈ Fin ∧ ∀ 𝑛 ∈ 𝐴 𝐵 ∈ dom vol ∧ Disj 𝑛 ∈ 𝐴 𝐵 ) ∧ ∀ 𝑛 ∈ 𝐴 ( vol ‘ 𝐵 ) ∈ ℝ ) → Disj 𝑛 ∈ 𝐴 𝐵 )
7 volfiniun ⊢ ( ( 𝐴 ∈ Fin ∧ ∀ 𝑛 ∈ 𝐴 ( 𝐵 ∈ dom vol ∧ ( vol ‘ 𝐵 ) ∈ ℝ ) ∧ Disj 𝑛 ∈ 𝐴 𝐵 ) → ( vol ‘ ∪ 𝑛 ∈ 𝐴 𝐵 ) = Σ 𝑛 ∈ 𝐴 ( vol ‘ 𝐵 ) )
8 1 5 6 7 syl3anc ⊢ ( ( ( 𝐴 ∈ Fin ∧ ∀ 𝑛 ∈ 𝐴 𝐵 ∈ dom vol ∧ Disj 𝑛 ∈ 𝐴 𝐵 ) ∧ ∀ 𝑛 ∈ 𝐴 ( vol ‘ 𝐵 ) ∈ ℝ ) → ( vol ‘ ∪ 𝑛 ∈ 𝐴 𝐵 ) = Σ 𝑛 ∈ 𝐴 ( vol ‘ 𝐵 ) )
9 nfcv ⊢ Ⅎ 𝑛 𝐴
10 9 nfel1 ⊢ Ⅎ 𝑛 𝐴 ∈ Fin
11 nfra1 ⊢ Ⅎ 𝑛 ∀ 𝑛 ∈ 𝐴 𝐵 ∈ dom vol
12 nfdisj1 ⊢ Ⅎ 𝑛 Disj 𝑛 ∈ 𝐴 𝐵
13 10 11 12 nf3an ⊢ Ⅎ 𝑛 ( 𝐴 ∈ Fin ∧ ∀ 𝑛 ∈ 𝐴 𝐵 ∈ dom vol ∧ Disj 𝑛 ∈ 𝐴 𝐵 )
14 nfra1 ⊢ Ⅎ 𝑛 ∀ 𝑛 ∈ 𝐴 ( vol ‘ 𝐵 ) ∈ ℝ
15 13 14 nfan ⊢ Ⅎ 𝑛 ( ( 𝐴 ∈ Fin ∧ ∀ 𝑛 ∈ 𝐴 𝐵 ∈ dom vol ∧ Disj 𝑛 ∈ 𝐴 𝐵 ) ∧ ∀ 𝑛 ∈ 𝐴 ( vol ‘ 𝐵 ) ∈ ℝ )
16 3 r19.21bi ⊢ ( ( ( ( 𝐴 ∈ Fin ∧ ∀ 𝑛 ∈ 𝐴 𝐵 ∈ dom vol ∧ Disj 𝑛 ∈ 𝐴 𝐵 ) ∧ ∀ 𝑛 ∈ 𝐴 ( vol ‘ 𝐵 ) ∈ ℝ ) ∧ 𝑛 ∈ 𝐴 ) → ( vol ‘ 𝐵 ) ∈ ℝ )
17 rspa ⊢ ( ( ∀ 𝑛 ∈ 𝐴 𝐵 ∈ dom vol ∧ 𝑛 ∈ 𝐴 ) → 𝐵 ∈ dom vol )
18 volf ⊢ vol : dom vol ⟶ ( 0 [,] +∞ )
19 18 ffvelcdmi ⊢ ( 𝐵 ∈ dom vol → ( vol ‘ 𝐵 ) ∈ ( 0 [,] +∞ ) )
20 17 19 syl ⊢ ( ( ∀ 𝑛 ∈ 𝐴 𝐵 ∈ dom vol ∧ 𝑛 ∈ 𝐴 ) → ( vol ‘ 𝐵 ) ∈ ( 0 [,] +∞ ) )
21 2 20 sylan ⊢ ( ( ( ( 𝐴 ∈ Fin ∧ ∀ 𝑛 ∈ 𝐴 𝐵 ∈ dom vol ∧ Disj 𝑛 ∈ 𝐴 𝐵 ) ∧ ∀ 𝑛 ∈ 𝐴 ( vol ‘ 𝐵 ) ∈ ℝ ) ∧ 𝑛 ∈ 𝐴 ) → ( vol ‘ 𝐵 ) ∈ ( 0 [,] +∞ ) )
22 0xr ⊢ 0 ∈ ℝ*
23 pnfxr ⊢ +∞ ∈ ℝ*
24 elicc1 ⊢ ( ( 0 ∈ ℝ* ∧ +∞ ∈ ℝ* ) → ( ( vol ‘ 𝐵 ) ∈ ( 0 [,] +∞ ) ↔ ( ( vol ‘ 𝐵 ) ∈ ℝ* ∧ 0 ≤ ( vol ‘ 𝐵 ) ∧ ( vol ‘ 𝐵 ) ≤ +∞ ) ) )
25 22 23 24 mp2an ⊢ ( ( vol ‘ 𝐵 ) ∈ ( 0 [,] +∞ ) ↔ ( ( vol ‘ 𝐵 ) ∈ ℝ* ∧ 0 ≤ ( vol ‘ 𝐵 ) ∧ ( vol ‘ 𝐵 ) ≤ +∞ ) )
26 25 simp2bi ⊢ ( ( vol ‘ 𝐵 ) ∈ ( 0 [,] +∞ ) → 0 ≤ ( vol ‘ 𝐵 ) )
27 21 26 syl ⊢ ( ( ( ( 𝐴 ∈ Fin ∧ ∀ 𝑛 ∈ 𝐴 𝐵 ∈ dom vol ∧ Disj 𝑛 ∈ 𝐴 𝐵 ) ∧ ∀ 𝑛 ∈ 𝐴 ( vol ‘ 𝐵 ) ∈ ℝ ) ∧ 𝑛 ∈ 𝐴 ) → 0 ≤ ( vol ‘ 𝐵 ) )
28 ltpnf ⊢ ( ( vol ‘ 𝐵 ) ∈ ℝ → ( vol ‘ 𝐵 ) < +∞ )
29 16 28 syl ⊢ ( ( ( ( 𝐴 ∈ Fin ∧ ∀ 𝑛 ∈ 𝐴 𝐵 ∈ dom vol ∧ Disj 𝑛 ∈ 𝐴 𝐵 ) ∧ ∀ 𝑛 ∈ 𝐴 ( vol ‘ 𝐵 ) ∈ ℝ ) ∧ 𝑛 ∈ 𝐴 ) → ( vol ‘ 𝐵 ) < +∞ )
30 0re ⊢ 0 ∈ ℝ
31 elico2 ⊢ ( ( 0 ∈ ℝ ∧ +∞ ∈ ℝ* ) → ( ( vol ‘ 𝐵 ) ∈ ( 0 [,) +∞ ) ↔ ( ( vol ‘ 𝐵 ) ∈ ℝ ∧ 0 ≤ ( vol ‘ 𝐵 ) ∧ ( vol ‘ 𝐵 ) < +∞ ) ) )
32 30 23 31 mp2an ⊢ ( ( vol ‘ 𝐵 ) ∈ ( 0 [,) +∞ ) ↔ ( ( vol ‘ 𝐵 ) ∈ ℝ ∧ 0 ≤ ( vol ‘ 𝐵 ) ∧ ( vol ‘ 𝐵 ) < +∞ ) )
33 16 27 29 32 syl3anbrc ⊢ ( ( ( ( 𝐴 ∈ Fin ∧ ∀ 𝑛 ∈ 𝐴 𝐵 ∈ dom vol ∧ Disj 𝑛 ∈ 𝐴 𝐵 ) ∧ ∀ 𝑛 ∈ 𝐴 ( vol ‘ 𝐵 ) ∈ ℝ ) ∧ 𝑛 ∈ 𝐴 ) → ( vol ‘ 𝐵 ) ∈ ( 0 [,) +∞ ) )
34 9 15 1 33 esumpfinvalf ⊢ ( ( ( 𝐴 ∈ Fin ∧ ∀ 𝑛 ∈ 𝐴 𝐵 ∈ dom vol ∧ Disj 𝑛 ∈ 𝐴 𝐵 ) ∧ ∀ 𝑛 ∈ 𝐴 ( vol ‘ 𝐵 ) ∈ ℝ ) → Σ* 𝑛 ∈ 𝐴 ( vol ‘ 𝐵 ) = Σ 𝑛 ∈ 𝐴 ( vol ‘ 𝐵 ) )
35 8 34 eqtr4d ⊢ ( ( ( 𝐴 ∈ Fin ∧ ∀ 𝑛 ∈ 𝐴 𝐵 ∈ dom vol ∧ Disj 𝑛 ∈ 𝐴 𝐵 ) ∧ ∀ 𝑛 ∈ 𝐴 ( vol ‘ 𝐵 ) ∈ ℝ ) → ( vol ‘ ∪ 𝑛 ∈ 𝐴 𝐵 ) = Σ* 𝑛 ∈ 𝐴 ( vol ‘ 𝐵 ) )
36 simpr ⊢ ( ( ( 𝐴 ∈ Fin ∧ ∀ 𝑛 ∈ 𝐴 𝐵 ∈ dom vol ∧ Disj 𝑛 ∈ 𝐴 𝐵 ) ∧ ∃ 𝑛 ∈ 𝐴 ( vol ‘ 𝐵 ) = +∞ ) → ∃ 𝑛 ∈ 𝐴 ( vol ‘ 𝐵 ) = +∞ )
37 nfv ⊢ Ⅎ 𝑘 ( vol ‘ 𝐵 ) = +∞
38 nfcv ⊢ Ⅎ 𝑛 vol
39 nfcsb1v ⊢ Ⅎ 𝑛 ⦋ 𝑘 / 𝑛 ⦌ 𝐵
40 38 39 nffv ⊢ Ⅎ 𝑛 ( vol ‘ ⦋ 𝑘 / 𝑛 ⦌ 𝐵 )
41 40 nfeq1 ⊢ Ⅎ 𝑛 ( vol ‘ ⦋ 𝑘 / 𝑛 ⦌ 𝐵 ) = +∞
42 csbeq1a ⊢ ( 𝑛 = 𝑘 → 𝐵 = ⦋ 𝑘 / 𝑛 ⦌ 𝐵 )
43 42 fveqeq2d ⊢ ( 𝑛 = 𝑘 → ( ( vol ‘ 𝐵 ) = +∞ ↔ ( vol ‘ ⦋ 𝑘 / 𝑛 ⦌ 𝐵 ) = +∞ ) )
44 37 41 43 cbvrexw ⊢ ( ∃ 𝑛 ∈ 𝐴 ( vol ‘ 𝐵 ) = +∞ ↔ ∃ 𝑘 ∈ 𝐴 ( vol ‘ ⦋ 𝑘 / 𝑛 ⦌ 𝐵 ) = +∞ )
45 36 44 sylib ⊢ ( ( ( 𝐴 ∈ Fin ∧ ∀ 𝑛 ∈ 𝐴 𝐵 ∈ dom vol ∧ Disj 𝑛 ∈ 𝐴 𝐵 ) ∧ ∃ 𝑛 ∈ 𝐴 ( vol ‘ 𝐵 ) = +∞ ) → ∃ 𝑘 ∈ 𝐴 ( vol ‘ ⦋ 𝑘 / 𝑛 ⦌ 𝐵 ) = +∞ )
46 39 nfel1 ⊢ Ⅎ 𝑛 ⦋ 𝑘 / 𝑛 ⦌ 𝐵 ∈ dom vol
47 42 eleq1d ⊢ ( 𝑛 = 𝑘 → ( 𝐵 ∈ dom vol ↔ ⦋ 𝑘 / 𝑛 ⦌ 𝐵 ∈ dom vol ) )
48 46 47 rspc ⊢ ( 𝑘 ∈ 𝐴 → ( ∀ 𝑛 ∈ 𝐴 𝐵 ∈ dom vol → ⦋ 𝑘 / 𝑛 ⦌ 𝐵 ∈ dom vol ) )
49 48 impcom ⊢ ( ( ∀ 𝑛 ∈ 𝐴 𝐵 ∈ dom vol ∧ 𝑘 ∈ 𝐴 ) → ⦋ 𝑘 / 𝑛 ⦌ 𝐵 ∈ dom vol )
50 49 adantll ⊢ ( ( ( 𝐴 ∈ Fin ∧ ∀ 𝑛 ∈ 𝐴 𝐵 ∈ dom vol ) ∧ 𝑘 ∈ 𝐴 ) → ⦋ 𝑘 / 𝑛 ⦌ 𝐵 ∈ dom vol )
51 finiunmbl ⊢ ( ( 𝐴 ∈ Fin ∧ ∀ 𝑛 ∈ 𝐴 𝐵 ∈ dom vol ) → ∪ 𝑛 ∈ 𝐴 𝐵 ∈ dom vol )
52 51 adantr ⊢ ( ( ( 𝐴 ∈ Fin ∧ ∀ 𝑛 ∈ 𝐴 𝐵 ∈ dom vol ) ∧ 𝑘 ∈ 𝐴 ) → ∪ 𝑛 ∈ 𝐴 𝐵 ∈ dom vol )
53 nfcv ⊢ Ⅎ 𝑛 𝑘
54 9 53 39 42 ssiun2sf ⊢ ( 𝑘 ∈ 𝐴 → ⦋ 𝑘 / 𝑛 ⦌ 𝐵 ⊆ ∪ 𝑛 ∈ 𝐴 𝐵 )
55 54 adantl ⊢ ( ( ( 𝐴 ∈ Fin ∧ ∀ 𝑛 ∈ 𝐴 𝐵 ∈ dom vol ) ∧ 𝑘 ∈ 𝐴 ) → ⦋ 𝑘 / 𝑛 ⦌ 𝐵 ⊆ ∪ 𝑛 ∈ 𝐴 𝐵 )
56 volss ⊢ ( ( ⦋ 𝑘 / 𝑛 ⦌ 𝐵 ∈ dom vol ∧ ∪ 𝑛 ∈ 𝐴 𝐵 ∈ dom vol ∧ ⦋ 𝑘 / 𝑛 ⦌ 𝐵 ⊆ ∪ 𝑛 ∈ 𝐴 𝐵 ) → ( vol ‘ ⦋ 𝑘 / 𝑛 ⦌ 𝐵 ) ≤ ( vol ‘ ∪ 𝑛 ∈ 𝐴 𝐵 ) )
57 50 52 55 56 syl3anc ⊢ ( ( ( 𝐴 ∈ Fin ∧ ∀ 𝑛 ∈ 𝐴 𝐵 ∈ dom vol ) ∧ 𝑘 ∈ 𝐴 ) → ( vol ‘ ⦋ 𝑘 / 𝑛 ⦌ 𝐵 ) ≤ ( vol ‘ ∪ 𝑛 ∈ 𝐴 𝐵 ) )
58 57 3adantl3 ⊢ ( ( ( 𝐴 ∈ Fin ∧ ∀ 𝑛 ∈ 𝐴 𝐵 ∈ dom vol ∧ Disj 𝑛 ∈ 𝐴 𝐵 ) ∧ 𝑘 ∈ 𝐴 ) → ( vol ‘ ⦋ 𝑘 / 𝑛 ⦌ 𝐵 ) ≤ ( vol ‘ ∪ 𝑛 ∈ 𝐴 𝐵 ) )
59 58 adantlr ⊢ ( ( ( ( 𝐴 ∈ Fin ∧ ∀ 𝑛 ∈ 𝐴 𝐵 ∈ dom vol ∧ Disj 𝑛 ∈ 𝐴 𝐵 ) ∧ ∃ 𝑛 ∈ 𝐴 ( vol ‘ 𝐵 ) = +∞ ) ∧ 𝑘 ∈ 𝐴 ) → ( vol ‘ ⦋ 𝑘 / 𝑛 ⦌ 𝐵 ) ≤ ( vol ‘ ∪ 𝑛 ∈ 𝐴 𝐵 ) )
60 59 ralrimiva ⊢ ( ( ( 𝐴 ∈ Fin ∧ ∀ 𝑛 ∈ 𝐴 𝐵 ∈ dom vol ∧ Disj 𝑛 ∈ 𝐴 𝐵 ) ∧ ∃ 𝑛 ∈ 𝐴 ( vol ‘ 𝐵 ) = +∞ ) → ∀ 𝑘 ∈ 𝐴 ( vol ‘ ⦋ 𝑘 / 𝑛 ⦌ 𝐵 ) ≤ ( vol ‘ ∪ 𝑛 ∈ 𝐴 𝐵 ) )
61 r19.29r ⊢ ( ( ∃ 𝑘 ∈ 𝐴 ( vol ‘ ⦋ 𝑘 / 𝑛 ⦌ 𝐵 ) = +∞ ∧ ∀ 𝑘 ∈ 𝐴 ( vol ‘ ⦋ 𝑘 / 𝑛 ⦌ 𝐵 ) ≤ ( vol ‘ ∪ 𝑛 ∈ 𝐴 𝐵 ) ) → ∃ 𝑘 ∈ 𝐴 ( ( vol ‘ ⦋ 𝑘 / 𝑛 ⦌ 𝐵 ) = +∞ ∧ ( vol ‘ ⦋ 𝑘 / 𝑛 ⦌ 𝐵 ) ≤ ( vol ‘ ∪ 𝑛 ∈ 𝐴 𝐵 ) ) )
62 45 60 61 syl2anc ⊢ ( ( ( 𝐴 ∈ Fin ∧ ∀ 𝑛 ∈ 𝐴 𝐵 ∈ dom vol ∧ Disj 𝑛 ∈ 𝐴 𝐵 ) ∧ ∃ 𝑛 ∈ 𝐴 ( vol ‘ 𝐵 ) = +∞ ) → ∃ 𝑘 ∈ 𝐴 ( ( vol ‘ ⦋ 𝑘 / 𝑛 ⦌ 𝐵 ) = +∞ ∧ ( vol ‘ ⦋ 𝑘 / 𝑛 ⦌ 𝐵 ) ≤ ( vol ‘ ∪ 𝑛 ∈ 𝐴 𝐵 ) ) )
63 breq1 ⊢ ( ( vol ‘ ⦋ 𝑘 / 𝑛 ⦌ 𝐵 ) = +∞ → ( ( vol ‘ ⦋ 𝑘 / 𝑛 ⦌ 𝐵 ) ≤ ( vol ‘ ∪ 𝑛 ∈ 𝐴 𝐵 ) ↔ +∞ ≤ ( vol ‘ ∪ 𝑛 ∈ 𝐴 𝐵 ) ) )
64 63 biimpa ⊢ ( ( ( vol ‘ ⦋ 𝑘 / 𝑛 ⦌ 𝐵 ) = +∞ ∧ ( vol ‘ ⦋ 𝑘 / 𝑛 ⦌ 𝐵 ) ≤ ( vol ‘ ∪ 𝑛 ∈ 𝐴 𝐵 ) ) → +∞ ≤ ( vol ‘ ∪ 𝑛 ∈ 𝐴 𝐵 ) )
65 64 reximi ⊢ ( ∃ 𝑘 ∈ 𝐴 ( ( vol ‘ ⦋ 𝑘 / 𝑛 ⦌ 𝐵 ) = +∞ ∧ ( vol ‘ ⦋ 𝑘 / 𝑛 ⦌ 𝐵 ) ≤ ( vol ‘ ∪ 𝑛 ∈ 𝐴 𝐵 ) ) → ∃ 𝑘 ∈ 𝐴 +∞ ≤ ( vol ‘ ∪ 𝑛 ∈ 𝐴 𝐵 ) )
66 62 65 syl ⊢ ( ( ( 𝐴 ∈ Fin ∧ ∀ 𝑛 ∈ 𝐴 𝐵 ∈ dom vol ∧ Disj 𝑛 ∈ 𝐴 𝐵 ) ∧ ∃ 𝑛 ∈ 𝐴 ( vol ‘ 𝐵 ) = +∞ ) → ∃ 𝑘 ∈ 𝐴 +∞ ≤ ( vol ‘ ∪ 𝑛 ∈ 𝐴 𝐵 ) )
67 rexex ⊢ ( ∃ 𝑘 ∈ 𝐴 +∞ ≤ ( vol ‘ ∪ 𝑛 ∈ 𝐴 𝐵 ) → ∃ 𝑘 +∞ ≤ ( vol ‘ ∪ 𝑛 ∈ 𝐴 𝐵 ) )
68 19.9v ⊢ ( ∃ 𝑘 +∞ ≤ ( vol ‘ ∪ 𝑛 ∈ 𝐴 𝐵 ) ↔ +∞ ≤ ( vol ‘ ∪ 𝑛 ∈ 𝐴 𝐵 ) )
69 67 68 sylib ⊢ ( ∃ 𝑘 ∈ 𝐴 +∞ ≤ ( vol ‘ ∪ 𝑛 ∈ 𝐴 𝐵 ) → +∞ ≤ ( vol ‘ ∪ 𝑛 ∈ 𝐴 𝐵 ) )
70 66 69 syl ⊢ ( ( ( 𝐴 ∈ Fin ∧ ∀ 𝑛 ∈ 𝐴 𝐵 ∈ dom vol ∧ Disj 𝑛 ∈ 𝐴 𝐵 ) ∧ ∃ 𝑛 ∈ 𝐴 ( vol ‘ 𝐵 ) = +∞ ) → +∞ ≤ ( vol ‘ ∪ 𝑛 ∈ 𝐴 𝐵 ) )
71 iccssxr ⊢ ( 0 [,] +∞ ) ⊆ ℝ*
72 18 ffvelcdmi ⊢ ( ∪ 𝑛 ∈ 𝐴 𝐵 ∈ dom vol → ( vol ‘ ∪ 𝑛 ∈ 𝐴 𝐵 ) ∈ ( 0 [,] +∞ ) )
73 71 72 sselid ⊢ ( ∪ 𝑛 ∈ 𝐴 𝐵 ∈ dom vol → ( vol ‘ ∪ 𝑛 ∈ 𝐴 𝐵 ) ∈ ℝ* )
74 51 73 syl ⊢ ( ( 𝐴 ∈ Fin ∧ ∀ 𝑛 ∈ 𝐴 𝐵 ∈ dom vol ) → ( vol ‘ ∪ 𝑛 ∈ 𝐴 𝐵 ) ∈ ℝ* )
75 74 3adant3 ⊢ ( ( 𝐴 ∈ Fin ∧ ∀ 𝑛 ∈ 𝐴 𝐵 ∈ dom vol ∧ Disj 𝑛 ∈ 𝐴 𝐵 ) → ( vol ‘ ∪ 𝑛 ∈ 𝐴 𝐵 ) ∈ ℝ* )
76 75 adantr ⊢ ( ( ( 𝐴 ∈ Fin ∧ ∀ 𝑛 ∈ 𝐴 𝐵 ∈ dom vol ∧ Disj 𝑛 ∈ 𝐴 𝐵 ) ∧ ∃ 𝑛 ∈ 𝐴 ( vol ‘ 𝐵 ) = +∞ ) → ( vol ‘ ∪ 𝑛 ∈ 𝐴 𝐵 ) ∈ ℝ* )
77 xgepnf ⊢ ( ( vol ‘ ∪ 𝑛 ∈ 𝐴 𝐵 ) ∈ ℝ* → ( +∞ ≤ ( vol ‘ ∪ 𝑛 ∈ 𝐴 𝐵 ) ↔ ( vol ‘ ∪ 𝑛 ∈ 𝐴 𝐵 ) = +∞ ) )
78 76 77 syl ⊢ ( ( ( 𝐴 ∈ Fin ∧ ∀ 𝑛 ∈ 𝐴 𝐵 ∈ dom vol ∧ Disj 𝑛 ∈ 𝐴 𝐵 ) ∧ ∃ 𝑛 ∈ 𝐴 ( vol ‘ 𝐵 ) = +∞ ) → ( +∞ ≤ ( vol ‘ ∪ 𝑛 ∈ 𝐴 𝐵 ) ↔ ( vol ‘ ∪ 𝑛 ∈ 𝐴 𝐵 ) = +∞ ) )
79 70 78 mpbid ⊢ ( ( ( 𝐴 ∈ Fin ∧ ∀ 𝑛 ∈ 𝐴 𝐵 ∈ dom vol ∧ Disj 𝑛 ∈ 𝐴 𝐵 ) ∧ ∃ 𝑛 ∈ 𝐴 ( vol ‘ 𝐵 ) = +∞ ) → ( vol ‘ ∪ 𝑛 ∈ 𝐴 𝐵 ) = +∞ )
80 nfre1 ⊢ Ⅎ 𝑛 ∃ 𝑛 ∈ 𝐴 ( vol ‘ 𝐵 ) = +∞
81 13 80 nfan ⊢ Ⅎ 𝑛 ( ( 𝐴 ∈ Fin ∧ ∀ 𝑛 ∈ 𝐴 𝐵 ∈ dom vol ∧ Disj 𝑛 ∈ 𝐴 𝐵 ) ∧ ∃ 𝑛 ∈ 𝐴 ( vol ‘ 𝐵 ) = +∞ )
82 simpl1 ⊢ ( ( ( 𝐴 ∈ Fin ∧ ∀ 𝑛 ∈ 𝐴 𝐵 ∈ dom vol ∧ Disj 𝑛 ∈ 𝐴 𝐵 ) ∧ ∃ 𝑛 ∈ 𝐴 ( vol ‘ 𝐵 ) = +∞ ) → 𝐴 ∈ Fin )
83 20 3ad2antl2 ⊢ ( ( ( 𝐴 ∈ Fin ∧ ∀ 𝑛 ∈ 𝐴 𝐵 ∈ dom vol ∧ Disj 𝑛 ∈ 𝐴 𝐵 ) ∧ 𝑛 ∈ 𝐴 ) → ( vol ‘ 𝐵 ) ∈ ( 0 [,] +∞ ) )
84 83 adantlr ⊢ ( ( ( ( 𝐴 ∈ Fin ∧ ∀ 𝑛 ∈ 𝐴 𝐵 ∈ dom vol ∧ Disj 𝑛 ∈ 𝐴 𝐵 ) ∧ ∃ 𝑛 ∈ 𝐴 ( vol ‘ 𝐵 ) = +∞ ) ∧ 𝑛 ∈ 𝐴 ) → ( vol ‘ 𝐵 ) ∈ ( 0 [,] +∞ ) )
85 81 82 84 36 esumpinfval ⊢ ( ( ( 𝐴 ∈ Fin ∧ ∀ 𝑛 ∈ 𝐴 𝐵 ∈ dom vol ∧ Disj 𝑛 ∈ 𝐴 𝐵 ) ∧ ∃ 𝑛 ∈ 𝐴 ( vol ‘ 𝐵 ) = +∞ ) → Σ* 𝑛 ∈ 𝐴 ( vol ‘ 𝐵 ) = +∞ )
86 79 85 eqtr4d ⊢ ( ( ( 𝐴 ∈ Fin ∧ ∀ 𝑛 ∈ 𝐴 𝐵 ∈ dom vol ∧ Disj 𝑛 ∈ 𝐴 𝐵 ) ∧ ∃ 𝑛 ∈ 𝐴 ( vol ‘ 𝐵 ) = +∞ ) → ( vol ‘ ∪ 𝑛 ∈ 𝐴 𝐵 ) = Σ* 𝑛 ∈ 𝐴 ( vol ‘ 𝐵 ) )
87 exmid ⊢ ( ∀ 𝑛 ∈ 𝐴 ( vol ‘ 𝐵 ) ∈ ℝ ∨ ¬ ∀ 𝑛 ∈ 𝐴 ( vol ‘ 𝐵 ) ∈ ℝ )
88 rexnal ⊢ ( ∃ 𝑛 ∈ 𝐴 ¬ ( vol ‘ 𝐵 ) ∈ ℝ ↔ ¬ ∀ 𝑛 ∈ 𝐴 ( vol ‘ 𝐵 ) ∈ ℝ )
89 88 orbi2i ⊢ ( ( ∀ 𝑛 ∈ 𝐴 ( vol ‘ 𝐵 ) ∈ ℝ ∨ ∃ 𝑛 ∈ 𝐴 ¬ ( vol ‘ 𝐵 ) ∈ ℝ ) ↔ ( ∀ 𝑛 ∈ 𝐴 ( vol ‘ 𝐵 ) ∈ ℝ ∨ ¬ ∀ 𝑛 ∈ 𝐴 ( vol ‘ 𝐵 ) ∈ ℝ ) )
90 87 89 mpbir ⊢ ( ∀ 𝑛 ∈ 𝐴 ( vol ‘ 𝐵 ) ∈ ℝ ∨ ∃ 𝑛 ∈ 𝐴 ¬ ( vol ‘ 𝐵 ) ∈ ℝ )
91 r19.29 ⊢ ( ( ∀ 𝑛 ∈ 𝐴 𝐵 ∈ dom vol ∧ ∃ 𝑛 ∈ 𝐴 ¬ ( vol ‘ 𝐵 ) ∈ ℝ ) → ∃ 𝑛 ∈ 𝐴 ( 𝐵 ∈ dom vol ∧ ¬ ( vol ‘ 𝐵 ) ∈ ℝ ) )
92 xrge0nre ⊢ ( ( ( vol ‘ 𝐵 ) ∈ ( 0 [,] +∞ ) ∧ ¬ ( vol ‘ 𝐵 ) ∈ ℝ ) → ( vol ‘ 𝐵 ) = +∞ )
93 19 92 sylan ⊢ ( ( 𝐵 ∈ dom vol ∧ ¬ ( vol ‘ 𝐵 ) ∈ ℝ ) → ( vol ‘ 𝐵 ) = +∞ )
94 93 reximi ⊢ ( ∃ 𝑛 ∈ 𝐴 ( 𝐵 ∈ dom vol ∧ ¬ ( vol ‘ 𝐵 ) ∈ ℝ ) → ∃ 𝑛 ∈ 𝐴 ( vol ‘ 𝐵 ) = +∞ )
95 91 94 syl ⊢ ( ( ∀ 𝑛 ∈ 𝐴 𝐵 ∈ dom vol ∧ ∃ 𝑛 ∈ 𝐴 ¬ ( vol ‘ 𝐵 ) ∈ ℝ ) → ∃ 𝑛 ∈ 𝐴 ( vol ‘ 𝐵 ) = +∞ )
96 95 ex ⊢ ( ∀ 𝑛 ∈ 𝐴 𝐵 ∈ dom vol → ( ∃ 𝑛 ∈ 𝐴 ¬ ( vol ‘ 𝐵 ) ∈ ℝ → ∃ 𝑛 ∈ 𝐴 ( vol ‘ 𝐵 ) = +∞ ) )
97 96 orim2d ⊢ ( ∀ 𝑛 ∈ 𝐴 𝐵 ∈ dom vol → ( ( ∀ 𝑛 ∈ 𝐴 ( vol ‘ 𝐵 ) ∈ ℝ ∨ ∃ 𝑛 ∈ 𝐴 ¬ ( vol ‘ 𝐵 ) ∈ ℝ ) → ( ∀ 𝑛 ∈ 𝐴 ( vol ‘ 𝐵 ) ∈ ℝ ∨ ∃ 𝑛 ∈ 𝐴 ( vol ‘ 𝐵 ) = +∞ ) ) )
98 90 97 mpi ⊢ ( ∀ 𝑛 ∈ 𝐴 𝐵 ∈ dom vol → ( ∀ 𝑛 ∈ 𝐴 ( vol ‘ 𝐵 ) ∈ ℝ ∨ ∃ 𝑛 ∈ 𝐴 ( vol ‘ 𝐵 ) = +∞ ) )
99 98 3ad2ant2 ⊢ ( ( 𝐴 ∈ Fin ∧ ∀ 𝑛 ∈ 𝐴 𝐵 ∈ dom vol ∧ Disj 𝑛 ∈ 𝐴 𝐵 ) → ( ∀ 𝑛 ∈ 𝐴 ( vol ‘ 𝐵 ) ∈ ℝ ∨ ∃ 𝑛 ∈ 𝐴 ( vol ‘ 𝐵 ) = +∞ ) )
100 35 86 99 mpjaodan ⊢ ( ( 𝐴 ∈ Fin ∧ ∀ 𝑛 ∈ 𝐴 𝐵 ∈ dom vol ∧ Disj 𝑛 ∈ 𝐴 𝐵 ) → ( vol ‘ ∪ 𝑛 ∈ 𝐴 𝐵 ) = Σ* 𝑛 ∈ 𝐴 ( vol ‘ 𝐵 ) )