Metamath Proof Explorer

Theorem ovoliunnul

Description: A countable union of nullsets is null. (Contributed by Mario Carneiro, 8-Apr-2015)

Ref Expression
Assertion ovoliunnul ( ( 𝐴 ≼ ℕ ∧ ∀ 𝑛 ∈ 𝐴 ( 𝐵 ⊆ ℝ ∧ ( vol* ‘ 𝐵 ) = 0 ) ) → ( vol* ‘ ∪ 𝑛 ∈ 𝐴 𝐵 ) = 0 )

Proof

Step Hyp Ref Expression
1 iuneq1 ⊢ ( 𝐴 = ∅ → ∪ 𝑛 ∈ 𝐴 𝐵 = ∪ 𝑛 ∈ ∅ 𝐵 )
2 0iun ⊢ ∪ 𝑛 ∈ ∅ 𝐵 = ∅
3 1 2 eqtrdi ⊢ ( 𝐴 = ∅ → ∪ 𝑛 ∈ 𝐴 𝐵 = ∅ )
4 3 fveq2d ⊢ ( 𝐴 = ∅ → ( vol* ‘ ∪ 𝑛 ∈ 𝐴 𝐵 ) = ( vol* ‘ ∅ ) )
5 ovol0 ⊢ ( vol* ‘ ∅ ) = 0
6 4 5 eqtrdi ⊢ ( 𝐴 = ∅ → ( vol* ‘ ∪ 𝑛 ∈ 𝐴 𝐵 ) = 0 )
7 6 a1i ⊢ ( ( 𝐴 ≼ ℕ ∧ ∀ 𝑛 ∈ 𝐴 ( 𝐵 ⊆ ℝ ∧ ( vol* ‘ 𝐵 ) = 0 ) ) → ( 𝐴 = ∅ → ( vol* ‘ ∪ 𝑛 ∈ 𝐴 𝐵 ) = 0 ) )
8 reldom ⊢ Rel ≼
9 8 brrelex1i ⊢ ( 𝐴 ≼ ℕ → 𝐴 ∈ V )
10 9 adantr ⊢ ( ( 𝐴 ≼ ℕ ∧ ∀ 𝑛 ∈ 𝐴 ( 𝐵 ⊆ ℝ ∧ ( vol* ‘ 𝐵 ) = 0 ) ) → 𝐴 ∈ V )
11 0sdomg ⊢ ( 𝐴 ∈ V → ( ∅ ≺ 𝐴 ↔ 𝐴 ≠ ∅ ) )
12 10 11 syl ⊢ ( ( 𝐴 ≼ ℕ ∧ ∀ 𝑛 ∈ 𝐴 ( 𝐵 ⊆ ℝ ∧ ( vol* ‘ 𝐵 ) = 0 ) ) → ( ∅ ≺ 𝐴 ↔ 𝐴 ≠ ∅ ) )
13 fodomr ⊢ ( ( ∅ ≺ 𝐴 ∧ 𝐴 ≼ ℕ ) → ∃ 𝑓 𝑓 : ℕ –onto→ 𝐴 )
14 13 expcom ⊢ ( 𝐴 ≼ ℕ → ( ∅ ≺ 𝐴 → ∃ 𝑓 𝑓 : ℕ –onto→ 𝐴 ) )
15 14 adantr ⊢ ( ( 𝐴 ≼ ℕ ∧ ∀ 𝑛 ∈ 𝐴 ( 𝐵 ⊆ ℝ ∧ ( vol* ‘ 𝐵 ) = 0 ) ) → ( ∅ ≺ 𝐴 → ∃ 𝑓 𝑓 : ℕ –onto→ 𝐴 ) )
16 eliun ⊢ ( 𝑥 ∈ ∪ 𝑛 ∈ 𝐴 𝐵 ↔ ∃ 𝑛 ∈ 𝐴 𝑥 ∈ 𝐵 )
17 nfv ⊢ Ⅎ 𝑛 𝑓 : ℕ –onto→ 𝐴
18 nfcv ⊢ Ⅎ 𝑛 ℕ
19 nfcsb1v ⊢ Ⅎ 𝑛 ⦋ ( 𝑓 ‘ 𝑘 ) / 𝑛 ⦌ 𝐵
20 18 19 nfiun ⊢ Ⅎ 𝑛 ∪ 𝑘 ∈ ℕ ⦋ ( 𝑓 ‘ 𝑘 ) / 𝑛 ⦌ 𝐵
21 20 nfcri ⊢ Ⅎ 𝑛 𝑥 ∈ ∪ 𝑘 ∈ ℕ ⦋ ( 𝑓 ‘ 𝑘 ) / 𝑛 ⦌ 𝐵
22 foelrn ⊢ ( ( 𝑓 : ℕ –onto→ 𝐴 ∧ 𝑛 ∈ 𝐴 ) → ∃ 𝑘 ∈ ℕ 𝑛 = ( 𝑓 ‘ 𝑘 ) )
23 22 ex ⊢ ( 𝑓 : ℕ –onto→ 𝐴 → ( 𝑛 ∈ 𝐴 → ∃ 𝑘 ∈ ℕ 𝑛 = ( 𝑓 ‘ 𝑘 ) ) )
24 csbeq1a ⊢ ( 𝑛 = ( 𝑓 ‘ 𝑘 ) → 𝐵 = ⦋ ( 𝑓 ‘ 𝑘 ) / 𝑛 ⦌ 𝐵 )
25 24 adantl ⊢ ( ( 𝑓 : ℕ –onto→ 𝐴 ∧ 𝑛 = ( 𝑓 ‘ 𝑘 ) ) → 𝐵 = ⦋ ( 𝑓 ‘ 𝑘 ) / 𝑛 ⦌ 𝐵 )
26 25 eleq2d ⊢ ( ( 𝑓 : ℕ –onto→ 𝐴 ∧ 𝑛 = ( 𝑓 ‘ 𝑘 ) ) → ( 𝑥 ∈ 𝐵 ↔ 𝑥 ∈ ⦋ ( 𝑓 ‘ 𝑘 ) / 𝑛 ⦌ 𝐵 ) )
27 26 biimpd ⊢ ( ( 𝑓 : ℕ –onto→ 𝐴 ∧ 𝑛 = ( 𝑓 ‘ 𝑘 ) ) → ( 𝑥 ∈ 𝐵 → 𝑥 ∈ ⦋ ( 𝑓 ‘ 𝑘 ) / 𝑛 ⦌ 𝐵 ) )
28 27 impancom ⊢ ( ( 𝑓 : ℕ –onto→ 𝐴 ∧ 𝑥 ∈ 𝐵 ) → ( 𝑛 = ( 𝑓 ‘ 𝑘 ) → 𝑥 ∈ ⦋ ( 𝑓 ‘ 𝑘 ) / 𝑛 ⦌ 𝐵 ) )
29 28 reximdv ⊢ ( ( 𝑓 : ℕ –onto→ 𝐴 ∧ 𝑥 ∈ 𝐵 ) → ( ∃ 𝑘 ∈ ℕ 𝑛 = ( 𝑓 ‘ 𝑘 ) → ∃ 𝑘 ∈ ℕ 𝑥 ∈ ⦋ ( 𝑓 ‘ 𝑘 ) / 𝑛 ⦌ 𝐵 ) )
30 eliun ⊢ ( 𝑥 ∈ ∪ 𝑘 ∈ ℕ ⦋ ( 𝑓 ‘ 𝑘 ) / 𝑛 ⦌ 𝐵 ↔ ∃ 𝑘 ∈ ℕ 𝑥 ∈ ⦋ ( 𝑓 ‘ 𝑘 ) / 𝑛 ⦌ 𝐵 )
31 29 30 imbitrrdi ⊢ ( ( 𝑓 : ℕ –onto→ 𝐴 ∧ 𝑥 ∈ 𝐵 ) → ( ∃ 𝑘 ∈ ℕ 𝑛 = ( 𝑓 ‘ 𝑘 ) → 𝑥 ∈ ∪ 𝑘 ∈ ℕ ⦋ ( 𝑓 ‘ 𝑘 ) / 𝑛 ⦌ 𝐵 ) )
32 31 ex ⊢ ( 𝑓 : ℕ –onto→ 𝐴 → ( 𝑥 ∈ 𝐵 → ( ∃ 𝑘 ∈ ℕ 𝑛 = ( 𝑓 ‘ 𝑘 ) → 𝑥 ∈ ∪ 𝑘 ∈ ℕ ⦋ ( 𝑓 ‘ 𝑘 ) / 𝑛 ⦌ 𝐵 ) ) )
33 32 com23 ⊢ ( 𝑓 : ℕ –onto→ 𝐴 → ( ∃ 𝑘 ∈ ℕ 𝑛 = ( 𝑓 ‘ 𝑘 ) → ( 𝑥 ∈ 𝐵 → 𝑥 ∈ ∪ 𝑘 ∈ ℕ ⦋ ( 𝑓 ‘ 𝑘 ) / 𝑛 ⦌ 𝐵 ) ) )
34 23 33 syld ⊢ ( 𝑓 : ℕ –onto→ 𝐴 → ( 𝑛 ∈ 𝐴 → ( 𝑥 ∈ 𝐵 → 𝑥 ∈ ∪ 𝑘 ∈ ℕ ⦋ ( 𝑓 ‘ 𝑘 ) / 𝑛 ⦌ 𝐵 ) ) )
35 17 21 34 rexlimd ⊢ ( 𝑓 : ℕ –onto→ 𝐴 → ( ∃ 𝑛 ∈ 𝐴 𝑥 ∈ 𝐵 → 𝑥 ∈ ∪ 𝑘 ∈ ℕ ⦋ ( 𝑓 ‘ 𝑘 ) / 𝑛 ⦌ 𝐵 ) )
36 16 35 biimtrid ⊢ ( 𝑓 : ℕ –onto→ 𝐴 → ( 𝑥 ∈ ∪ 𝑛 ∈ 𝐴 𝐵 → 𝑥 ∈ ∪ 𝑘 ∈ ℕ ⦋ ( 𝑓 ‘ 𝑘 ) / 𝑛 ⦌ 𝐵 ) )
37 36 ssrdv ⊢ ( 𝑓 : ℕ –onto→ 𝐴 → ∪ 𝑛 ∈ 𝐴 𝐵 ⊆ ∪ 𝑘 ∈ ℕ ⦋ ( 𝑓 ‘ 𝑘 ) / 𝑛 ⦌ 𝐵 )
38 37 adantl ⊢ ( ( ( 𝐴 ≼ ℕ ∧ ∀ 𝑛 ∈ 𝐴 ( 𝐵 ⊆ ℝ ∧ ( vol* ‘ 𝐵 ) = 0 ) ) ∧ 𝑓 : ℕ –onto→ 𝐴 ) → ∪ 𝑛 ∈ 𝐴 𝐵 ⊆ ∪ 𝑘 ∈ ℕ ⦋ ( 𝑓 ‘ 𝑘 ) / 𝑛 ⦌ 𝐵 )
39 fof ⊢ ( 𝑓 : ℕ –onto→ 𝐴 → 𝑓 : ℕ ⟶ 𝐴 )
40 39 adantl ⊢ ( ( ( 𝐴 ≼ ℕ ∧ ∀ 𝑛 ∈ 𝐴 ( 𝐵 ⊆ ℝ ∧ ( vol* ‘ 𝐵 ) = 0 ) ) ∧ 𝑓 : ℕ –onto→ 𝐴 ) → 𝑓 : ℕ ⟶ 𝐴 )
41 40 ffvelcdmda ⊢ ( ( ( ( 𝐴 ≼ ℕ ∧ ∀ 𝑛 ∈ 𝐴 ( 𝐵 ⊆ ℝ ∧ ( vol* ‘ 𝐵 ) = 0 ) ) ∧ 𝑓 : ℕ –onto→ 𝐴 ) ∧ 𝑘 ∈ ℕ ) → ( 𝑓 ‘ 𝑘 ) ∈ 𝐴 )
42 simpllr ⊢ ( ( ( ( 𝐴 ≼ ℕ ∧ ∀ 𝑛 ∈ 𝐴 ( 𝐵 ⊆ ℝ ∧ ( vol* ‘ 𝐵 ) = 0 ) ) ∧ 𝑓 : ℕ –onto→ 𝐴 ) ∧ 𝑘 ∈ ℕ ) → ∀ 𝑛 ∈ 𝐴 ( 𝐵 ⊆ ℝ ∧ ( vol* ‘ 𝐵 ) = 0 ) )
43 nfcv ⊢ Ⅎ 𝑛 ℝ
44 19 43 nfss ⊢ Ⅎ 𝑛 ⦋ ( 𝑓 ‘ 𝑘 ) / 𝑛 ⦌ 𝐵 ⊆ ℝ
45 nfcv ⊢ Ⅎ 𝑛 vol*
46 45 19 nffv ⊢ Ⅎ 𝑛 ( vol* ‘ ⦋ ( 𝑓 ‘ 𝑘 ) / 𝑛 ⦌ 𝐵 )
47 46 nfeq1 ⊢ Ⅎ 𝑛 ( vol* ‘ ⦋ ( 𝑓 ‘ 𝑘 ) / 𝑛 ⦌ 𝐵 ) = 0
48 44 47 nfan ⊢ Ⅎ 𝑛 ( ⦋ ( 𝑓 ‘ 𝑘 ) / 𝑛 ⦌ 𝐵 ⊆ ℝ ∧ ( vol* ‘ ⦋ ( 𝑓 ‘ 𝑘 ) / 𝑛 ⦌ 𝐵 ) = 0 )
49 24 sseq1d ⊢ ( 𝑛 = ( 𝑓 ‘ 𝑘 ) → ( 𝐵 ⊆ ℝ ↔ ⦋ ( 𝑓 ‘ 𝑘 ) / 𝑛 ⦌ 𝐵 ⊆ ℝ ) )
50 24 fveqeq2d ⊢ ( 𝑛 = ( 𝑓 ‘ 𝑘 ) → ( ( vol* ‘ 𝐵 ) = 0 ↔ ( vol* ‘ ⦋ ( 𝑓 ‘ 𝑘 ) / 𝑛 ⦌ 𝐵 ) = 0 ) )
51 49 50 anbi12d ⊢ ( 𝑛 = ( 𝑓 ‘ 𝑘 ) → ( ( 𝐵 ⊆ ℝ ∧ ( vol* ‘ 𝐵 ) = 0 ) ↔ ( ⦋ ( 𝑓 ‘ 𝑘 ) / 𝑛 ⦌ 𝐵 ⊆ ℝ ∧ ( vol* ‘ ⦋ ( 𝑓 ‘ 𝑘 ) / 𝑛 ⦌ 𝐵 ) = 0 ) ) )
52 48 51 rspc ⊢ ( ( 𝑓 ‘ 𝑘 ) ∈ 𝐴 → ( ∀ 𝑛 ∈ 𝐴 ( 𝐵 ⊆ ℝ ∧ ( vol* ‘ 𝐵 ) = 0 ) → ( ⦋ ( 𝑓 ‘ 𝑘 ) / 𝑛 ⦌ 𝐵 ⊆ ℝ ∧ ( vol* ‘ ⦋ ( 𝑓 ‘ 𝑘 ) / 𝑛 ⦌ 𝐵 ) = 0 ) ) )
53 41 42 52 sylc ⊢ ( ( ( ( 𝐴 ≼ ℕ ∧ ∀ 𝑛 ∈ 𝐴 ( 𝐵 ⊆ ℝ ∧ ( vol* ‘ 𝐵 ) = 0 ) ) ∧ 𝑓 : ℕ –onto→ 𝐴 ) ∧ 𝑘 ∈ ℕ ) → ( ⦋ ( 𝑓 ‘ 𝑘 ) / 𝑛 ⦌ 𝐵 ⊆ ℝ ∧ ( vol* ‘ ⦋ ( 𝑓 ‘ 𝑘 ) / 𝑛 ⦌ 𝐵 ) = 0 ) )
54 53 simpld ⊢ ( ( ( ( 𝐴 ≼ ℕ ∧ ∀ 𝑛 ∈ 𝐴 ( 𝐵 ⊆ ℝ ∧ ( vol* ‘ 𝐵 ) = 0 ) ) ∧ 𝑓 : ℕ –onto→ 𝐴 ) ∧ 𝑘 ∈ ℕ ) → ⦋ ( 𝑓 ‘ 𝑘 ) / 𝑛 ⦌ 𝐵 ⊆ ℝ )
55 54 ralrimiva ⊢ ( ( ( 𝐴 ≼ ℕ ∧ ∀ 𝑛 ∈ 𝐴 ( 𝐵 ⊆ ℝ ∧ ( vol* ‘ 𝐵 ) = 0 ) ) ∧ 𝑓 : ℕ –onto→ 𝐴 ) → ∀ 𝑘 ∈ ℕ ⦋ ( 𝑓 ‘ 𝑘 ) / 𝑛 ⦌ 𝐵 ⊆ ℝ )
56 iunss ⊢ ( ∪ 𝑘 ∈ ℕ ⦋ ( 𝑓 ‘ 𝑘 ) / 𝑛 ⦌ 𝐵 ⊆ ℝ ↔ ∀ 𝑘 ∈ ℕ ⦋ ( 𝑓 ‘ 𝑘 ) / 𝑛 ⦌ 𝐵 ⊆ ℝ )
57 55 56 sylibr ⊢ ( ( ( 𝐴 ≼ ℕ ∧ ∀ 𝑛 ∈ 𝐴 ( 𝐵 ⊆ ℝ ∧ ( vol* ‘ 𝐵 ) = 0 ) ) ∧ 𝑓 : ℕ –onto→ 𝐴 ) → ∪ 𝑘 ∈ ℕ ⦋ ( 𝑓 ‘ 𝑘 ) / 𝑛 ⦌ 𝐵 ⊆ ℝ )
58 eqid ⊢ seq 1 ( + , ( 𝑘 ∈ ℕ ↦ ( vol* ‘ ⦋ ( 𝑓 ‘ 𝑘 ) / 𝑛 ⦌ 𝐵 ) ) ) = seq 1 ( + , ( 𝑘 ∈ ℕ ↦ ( vol* ‘ ⦋ ( 𝑓 ‘ 𝑘 ) / 𝑛 ⦌ 𝐵 ) ) )
59 eqid ⊢ ( 𝑘 ∈ ℕ ↦ ( vol* ‘ ⦋ ( 𝑓 ‘ 𝑘 ) / 𝑛 ⦌ 𝐵 ) ) = ( 𝑘 ∈ ℕ ↦ ( vol* ‘ ⦋ ( 𝑓 ‘ 𝑘 ) / 𝑛 ⦌ 𝐵 ) )
60 53 simprd ⊢ ( ( ( ( 𝐴 ≼ ℕ ∧ ∀ 𝑛 ∈ 𝐴 ( 𝐵 ⊆ ℝ ∧ ( vol* ‘ 𝐵 ) = 0 ) ) ∧ 𝑓 : ℕ –onto→ 𝐴 ) ∧ 𝑘 ∈ ℕ ) → ( vol* ‘ ⦋ ( 𝑓 ‘ 𝑘 ) / 𝑛 ⦌ 𝐵 ) = 0 )
61 0re ⊢ 0 ∈ ℝ
62 60 61 eqeltrdi ⊢ ( ( ( ( 𝐴 ≼ ℕ ∧ ∀ 𝑛 ∈ 𝐴 ( 𝐵 ⊆ ℝ ∧ ( vol* ‘ 𝐵 ) = 0 ) ) ∧ 𝑓 : ℕ –onto→ 𝐴 ) ∧ 𝑘 ∈ ℕ ) → ( vol* ‘ ⦋ ( 𝑓 ‘ 𝑘 ) / 𝑛 ⦌ 𝐵 ) ∈ ℝ )
63 60 mpteq2dva ⊢ ( ( ( 𝐴 ≼ ℕ ∧ ∀ 𝑛 ∈ 𝐴 ( 𝐵 ⊆ ℝ ∧ ( vol* ‘ 𝐵 ) = 0 ) ) ∧ 𝑓 : ℕ –onto→ 𝐴 ) → ( 𝑘 ∈ ℕ ↦ ( vol* ‘ ⦋ ( 𝑓 ‘ 𝑘 ) / 𝑛 ⦌ 𝐵 ) ) = ( 𝑘 ∈ ℕ ↦ 0 ) )
64 fconstmpt ⊢ ( ℕ × { 0 } ) = ( 𝑘 ∈ ℕ ↦ 0 )
65 nnuz ⊢ ℕ = ( ℤ≥ ‘ 1 )
66 65 xpeq1i ⊢ ( ℕ × { 0 } ) = ( ( ℤ≥ ‘ 1 ) × { 0 } )
67 64 66 eqtr3i ⊢ ( 𝑘 ∈ ℕ ↦ 0 ) = ( ( ℤ≥ ‘ 1 ) × { 0 } )
68 63 67 eqtrdi ⊢ ( ( ( 𝐴 ≼ ℕ ∧ ∀ 𝑛 ∈ 𝐴 ( 𝐵 ⊆ ℝ ∧ ( vol* ‘ 𝐵 ) = 0 ) ) ∧ 𝑓 : ℕ –onto→ 𝐴 ) → ( 𝑘 ∈ ℕ ↦ ( vol* ‘ ⦋ ( 𝑓 ‘ 𝑘 ) / 𝑛 ⦌ 𝐵 ) ) = ( ( ℤ≥ ‘ 1 ) × { 0 } ) )
69 68 seqeq3d ⊢ ( ( ( 𝐴 ≼ ℕ ∧ ∀ 𝑛 ∈ 𝐴 ( 𝐵 ⊆ ℝ ∧ ( vol* ‘ 𝐵 ) = 0 ) ) ∧ 𝑓 : ℕ –onto→ 𝐴 ) → seq 1 ( + , ( 𝑘 ∈ ℕ ↦ ( vol* ‘ ⦋ ( 𝑓 ‘ 𝑘 ) / 𝑛 ⦌ 𝐵 ) ) ) = seq 1 ( + , ( ( ℤ≥ ‘ 1 ) × { 0 } ) ) )
70 1z ⊢ 1 ∈ ℤ
71 serclim0 ⊢ ( 1 ∈ ℤ → seq 1 ( + , ( ( ℤ≥ ‘ 1 ) × { 0 } ) ) ⇝ 0 )
72 seqex ⊢ seq 1 ( + , ( ( ℤ≥ ‘ 1 ) × { 0 } ) ) ∈ V
73 c0ex ⊢ 0 ∈ V
74 72 73 breldm ⊢ ( seq 1 ( + , ( ( ℤ≥ ‘ 1 ) × { 0 } ) ) ⇝ 0 → seq 1 ( + , ( ( ℤ≥ ‘ 1 ) × { 0 } ) ) ∈ dom ⇝ )
75 70 71 74 mp2b ⊢ seq 1 ( + , ( ( ℤ≥ ‘ 1 ) × { 0 } ) ) ∈ dom ⇝
76 69 75 eqeltrdi ⊢ ( ( ( 𝐴 ≼ ℕ ∧ ∀ 𝑛 ∈ 𝐴 ( 𝐵 ⊆ ℝ ∧ ( vol* ‘ 𝐵 ) = 0 ) ) ∧ 𝑓 : ℕ –onto→ 𝐴 ) → seq 1 ( + , ( 𝑘 ∈ ℕ ↦ ( vol* ‘ ⦋ ( 𝑓 ‘ 𝑘 ) / 𝑛 ⦌ 𝐵 ) ) ) ∈ dom ⇝ )
77 58 59 54 62 76 ovoliun2 ⊢ ( ( ( 𝐴 ≼ ℕ ∧ ∀ 𝑛 ∈ 𝐴 ( 𝐵 ⊆ ℝ ∧ ( vol* ‘ 𝐵 ) = 0 ) ) ∧ 𝑓 : ℕ –onto→ 𝐴 ) → ( vol* ‘ ∪ 𝑘 ∈ ℕ ⦋ ( 𝑓 ‘ 𝑘 ) / 𝑛 ⦌ 𝐵 ) ≤ Σ 𝑘 ∈ ℕ ( vol* ‘ ⦋ ( 𝑓 ‘ 𝑘 ) / 𝑛 ⦌ 𝐵 ) )
78 60 sumeq2dv ⊢ ( ( ( 𝐴 ≼ ℕ ∧ ∀ 𝑛 ∈ 𝐴 ( 𝐵 ⊆ ℝ ∧ ( vol* ‘ 𝐵 ) = 0 ) ) ∧ 𝑓 : ℕ –onto→ 𝐴 ) → Σ 𝑘 ∈ ℕ ( vol* ‘ ⦋ ( 𝑓 ‘ 𝑘 ) / 𝑛 ⦌ 𝐵 ) = Σ 𝑘 ∈ ℕ 0 )
79 65 eqimssi ⊢ ℕ ⊆ ( ℤ≥ ‘ 1 )
80 79 orci ⊢ ( ℕ ⊆ ( ℤ≥ ‘ 1 ) ∨ ℕ ∈ Fin )
81 sumz ⊢ ( ( ℕ ⊆ ( ℤ≥ ‘ 1 ) ∨ ℕ ∈ Fin ) → Σ 𝑘 ∈ ℕ 0 = 0 )
82 80 81 ax-mp ⊢ Σ 𝑘 ∈ ℕ 0 = 0
83 78 82 eqtrdi ⊢ ( ( ( 𝐴 ≼ ℕ ∧ ∀ 𝑛 ∈ 𝐴 ( 𝐵 ⊆ ℝ ∧ ( vol* ‘ 𝐵 ) = 0 ) ) ∧ 𝑓 : ℕ –onto→ 𝐴 ) → Σ 𝑘 ∈ ℕ ( vol* ‘ ⦋ ( 𝑓 ‘ 𝑘 ) / 𝑛 ⦌ 𝐵 ) = 0 )
84 77 83 breqtrd ⊢ ( ( ( 𝐴 ≼ ℕ ∧ ∀ 𝑛 ∈ 𝐴 ( 𝐵 ⊆ ℝ ∧ ( vol* ‘ 𝐵 ) = 0 ) ) ∧ 𝑓 : ℕ –onto→ 𝐴 ) → ( vol* ‘ ∪ 𝑘 ∈ ℕ ⦋ ( 𝑓 ‘ 𝑘 ) / 𝑛 ⦌ 𝐵 ) ≤ 0 )
85 ovolge0 ⊢ ( ∪ 𝑘 ∈ ℕ ⦋ ( 𝑓 ‘ 𝑘 ) / 𝑛 ⦌ 𝐵 ⊆ ℝ → 0 ≤ ( vol* ‘ ∪ 𝑘 ∈ ℕ ⦋ ( 𝑓 ‘ 𝑘 ) / 𝑛 ⦌ 𝐵 ) )
86 57 85 syl ⊢ ( ( ( 𝐴 ≼ ℕ ∧ ∀ 𝑛 ∈ 𝐴 ( 𝐵 ⊆ ℝ ∧ ( vol* ‘ 𝐵 ) = 0 ) ) ∧ 𝑓 : ℕ –onto→ 𝐴 ) → 0 ≤ ( vol* ‘ ∪ 𝑘 ∈ ℕ ⦋ ( 𝑓 ‘ 𝑘 ) / 𝑛 ⦌ 𝐵 ) )
87 ovolcl ⊢ ( ∪ 𝑘 ∈ ℕ ⦋ ( 𝑓 ‘ 𝑘 ) / 𝑛 ⦌ 𝐵 ⊆ ℝ → ( vol* ‘ ∪ 𝑘 ∈ ℕ ⦋ ( 𝑓 ‘ 𝑘 ) / 𝑛 ⦌ 𝐵 ) ∈ ℝ* )
88 57 87 syl ⊢ ( ( ( 𝐴 ≼ ℕ ∧ ∀ 𝑛 ∈ 𝐴 ( 𝐵 ⊆ ℝ ∧ ( vol* ‘ 𝐵 ) = 0 ) ) ∧ 𝑓 : ℕ –onto→ 𝐴 ) → ( vol* ‘ ∪ 𝑘 ∈ ℕ ⦋ ( 𝑓 ‘ 𝑘 ) / 𝑛 ⦌ 𝐵 ) ∈ ℝ* )
89 0xr ⊢ 0 ∈ ℝ*
90 xrletri3 ⊢ ( ( ( vol* ‘ ∪ 𝑘 ∈ ℕ ⦋ ( 𝑓 ‘ 𝑘 ) / 𝑛 ⦌ 𝐵 ) ∈ ℝ* ∧ 0 ∈ ℝ* ) → ( ( vol* ‘ ∪ 𝑘 ∈ ℕ ⦋ ( 𝑓 ‘ 𝑘 ) / 𝑛 ⦌ 𝐵 ) = 0 ↔ ( ( vol* ‘ ∪ 𝑘 ∈ ℕ ⦋ ( 𝑓 ‘ 𝑘 ) / 𝑛 ⦌ 𝐵 ) ≤ 0 ∧ 0 ≤ ( vol* ‘ ∪ 𝑘 ∈ ℕ ⦋ ( 𝑓 ‘ 𝑘 ) / 𝑛 ⦌ 𝐵 ) ) ) )
91 88 89 90 sylancl ⊢ ( ( ( 𝐴 ≼ ℕ ∧ ∀ 𝑛 ∈ 𝐴 ( 𝐵 ⊆ ℝ ∧ ( vol* ‘ 𝐵 ) = 0 ) ) ∧ 𝑓 : ℕ –onto→ 𝐴 ) → ( ( vol* ‘ ∪ 𝑘 ∈ ℕ ⦋ ( 𝑓 ‘ 𝑘 ) / 𝑛 ⦌ 𝐵 ) = 0 ↔ ( ( vol* ‘ ∪ 𝑘 ∈ ℕ ⦋ ( 𝑓 ‘ 𝑘 ) / 𝑛 ⦌ 𝐵 ) ≤ 0 ∧ 0 ≤ ( vol* ‘ ∪ 𝑘 ∈ ℕ ⦋ ( 𝑓 ‘ 𝑘 ) / 𝑛 ⦌ 𝐵 ) ) ) )
92 84 86 91 mpbir2and ⊢ ( ( ( 𝐴 ≼ ℕ ∧ ∀ 𝑛 ∈ 𝐴 ( 𝐵 ⊆ ℝ ∧ ( vol* ‘ 𝐵 ) = 0 ) ) ∧ 𝑓 : ℕ –onto→ 𝐴 ) → ( vol* ‘ ∪ 𝑘 ∈ ℕ ⦋ ( 𝑓 ‘ 𝑘 ) / 𝑛 ⦌ 𝐵 ) = 0 )
93 ovolssnul ⊢ ( ( ∪ 𝑛 ∈ 𝐴 𝐵 ⊆ ∪ 𝑘 ∈ ℕ ⦋ ( 𝑓 ‘ 𝑘 ) / 𝑛 ⦌ 𝐵 ∧ ∪ 𝑘 ∈ ℕ ⦋ ( 𝑓 ‘ 𝑘 ) / 𝑛 ⦌ 𝐵 ⊆ ℝ ∧ ( vol* ‘ ∪ 𝑘 ∈ ℕ ⦋ ( 𝑓 ‘ 𝑘 ) / 𝑛 ⦌ 𝐵 ) = 0 ) → ( vol* ‘ ∪ 𝑛 ∈ 𝐴 𝐵 ) = 0 )
94 38 57 92 93 syl3anc ⊢ ( ( ( 𝐴 ≼ ℕ ∧ ∀ 𝑛 ∈ 𝐴 ( 𝐵 ⊆ ℝ ∧ ( vol* ‘ 𝐵 ) = 0 ) ) ∧ 𝑓 : ℕ –onto→ 𝐴 ) → ( vol* ‘ ∪ 𝑛 ∈ 𝐴 𝐵 ) = 0 )
95 94 ex ⊢ ( ( 𝐴 ≼ ℕ ∧ ∀ 𝑛 ∈ 𝐴 ( 𝐵 ⊆ ℝ ∧ ( vol* ‘ 𝐵 ) = 0 ) ) → ( 𝑓 : ℕ –onto→ 𝐴 → ( vol* ‘ ∪ 𝑛 ∈ 𝐴 𝐵 ) = 0 ) )
96 95 exlimdv ⊢ ( ( 𝐴 ≼ ℕ ∧ ∀ 𝑛 ∈ 𝐴 ( 𝐵 ⊆ ℝ ∧ ( vol* ‘ 𝐵 ) = 0 ) ) → ( ∃ 𝑓 𝑓 : ℕ –onto→ 𝐴 → ( vol* ‘ ∪ 𝑛 ∈ 𝐴 𝐵 ) = 0 ) )
97 15 96 syld ⊢ ( ( 𝐴 ≼ ℕ ∧ ∀ 𝑛 ∈ 𝐴 ( 𝐵 ⊆ ℝ ∧ ( vol* ‘ 𝐵 ) = 0 ) ) → ( ∅ ≺ 𝐴 → ( vol* ‘ ∪ 𝑛 ∈ 𝐴 𝐵 ) = 0 ) )
98 12 97 sylbird ⊢ ( ( 𝐴 ≼ ℕ ∧ ∀ 𝑛 ∈ 𝐴 ( 𝐵 ⊆ ℝ ∧ ( vol* ‘ 𝐵 ) = 0 ) ) → ( 𝐴 ≠ ∅ → ( vol* ‘ ∪ 𝑛 ∈ 𝐴 𝐵 ) = 0 ) )
99 7 98 pm2.61dne ⊢ ( ( 𝐴 ≼ ℕ ∧ ∀ 𝑛 ∈ 𝐴 ( 𝐵 ⊆ ℝ ∧ ( vol* ‘ 𝐵 ) = 0 ) ) → ( vol* ‘ ∪ 𝑛 ∈ 𝐴 𝐵 ) = 0 )