Metamath Proof Explorer

Theorem ovoliunlem3

Description: Lemma for ovoliun . (Contributed by Mario Carneiro, 12-Jun-2014)

Ref Expression
Hypotheses ovoliun.t ⊢ 𝑇 = seq 1 ( + , 𝐺 )
ovoliun.g ⊢ 𝐺 = ( 𝑛 ∈ ℕ ↦ ( vol* ‘ 𝐴 ) )
ovoliun.a ⊢ ( ( 𝜑 ∧ 𝑛 ∈ ℕ ) → 𝐴 ⊆ ℝ )
ovoliun.v ⊢ ( ( 𝜑 ∧ 𝑛 ∈ ℕ ) → ( vol* ‘ 𝐴 ) ∈ ℝ )
ovoliun.r ⊢ ( 𝜑 → sup ( ran 𝑇 , ℝ* , < ) ∈ ℝ )
ovoliun.b ⊢ ( 𝜑 → 𝐵 ∈ ℝ+ )
Assertion ovoliunlem3 ( 𝜑 → ( vol* ‘ ∪ 𝑛 ∈ ℕ 𝐴 ) ≤ ( sup ( ran 𝑇 , ℝ* , < ) + 𝐵 ) )

Proof

Step Hyp Ref Expression
1 ovoliun.t ⊢ 𝑇 = seq 1 ( + , 𝐺 )
2 ovoliun.g ⊢ 𝐺 = ( 𝑛 ∈ ℕ ↦ ( vol* ‘ 𝐴 ) )
3 ovoliun.a ⊢ ( ( 𝜑 ∧ 𝑛 ∈ ℕ ) → 𝐴 ⊆ ℝ )
4 ovoliun.v ⊢ ( ( 𝜑 ∧ 𝑛 ∈ ℕ ) → ( vol* ‘ 𝐴 ) ∈ ℝ )
5 ovoliun.r ⊢ ( 𝜑 → sup ( ran 𝑇 , ℝ* , < ) ∈ ℝ )
6 ovoliun.b ⊢ ( 𝜑 → 𝐵 ∈ ℝ+ )
7 nfcv ⊢ Ⅎ 𝑚 𝐴
8 nfcsb1v ⊢ Ⅎ 𝑛 ⦋ 𝑚 / 𝑛 ⦌ 𝐴
9 csbeq1a ⊢ ( 𝑛 = 𝑚 → 𝐴 = ⦋ 𝑚 / 𝑛 ⦌ 𝐴 )
10 7 8 9 cbviun ⊢ ∪ 𝑛 ∈ ℕ 𝐴 = ∪ 𝑚 ∈ ℕ ⦋ 𝑚 / 𝑛 ⦌ 𝐴
11 10 fveq2i ⊢ ( vol* ‘ ∪ 𝑛 ∈ ℕ 𝐴 ) = ( vol* ‘ ∪ 𝑚 ∈ ℕ ⦋ 𝑚 / 𝑛 ⦌ 𝐴 )
12 2nn ⊢ 2 ∈ ℕ
13 nnnn0 ⊢ ( 𝑛 ∈ ℕ → 𝑛 ∈ ℕ0 )
14 nnexpcl ⊢ ( ( 2 ∈ ℕ ∧ 𝑛 ∈ ℕ0 ) → ( 2 ↑ 𝑛 ) ∈ ℕ )
15 12 13 14 sylancr ⊢ ( 𝑛 ∈ ℕ → ( 2 ↑ 𝑛 ) ∈ ℕ )
16 15 nnrpd ⊢ ( 𝑛 ∈ ℕ → ( 2 ↑ 𝑛 ) ∈ ℝ+ )
17 rpdivcl ⊢ ( ( 𝐵 ∈ ℝ+ ∧ ( 2 ↑ 𝑛 ) ∈ ℝ+ ) → ( 𝐵 / ( 2 ↑ 𝑛 ) ) ∈ ℝ+ )
18 6 16 17 syl2an ⊢ ( ( 𝜑 ∧ 𝑛 ∈ ℕ ) → ( 𝐵 / ( 2 ↑ 𝑛 ) ) ∈ ℝ+ )
19 eqid ⊢ seq 1 ( + , ( ( abs ∘ − ) ∘ 𝑓 ) ) = seq 1 ( + , ( ( abs ∘ − ) ∘ 𝑓 ) )
20 19 ovolgelb ⊢ ( ( 𝐴 ⊆ ℝ ∧ ( vol* ‘ 𝐴 ) ∈ ℝ ∧ ( 𝐵 / ( 2 ↑ 𝑛 ) ) ∈ ℝ+ ) → ∃ 𝑓 ∈ ( ( ≤ ∩ ( ℝ × ℝ ) ) ↑m ℕ ) ( 𝐴 ⊆ ∪ ran ( (,) ∘ 𝑓 ) ∧ sup ( ran seq 1 ( + , ( ( abs ∘ − ) ∘ 𝑓 ) ) , ℝ* , < ) ≤ ( ( vol* ‘ 𝐴 ) + ( 𝐵 / ( 2 ↑ 𝑛 ) ) ) ) )
21 3 4 18 20 syl3anc ⊢ ( ( 𝜑 ∧ 𝑛 ∈ ℕ ) → ∃ 𝑓 ∈ ( ( ≤ ∩ ( ℝ × ℝ ) ) ↑m ℕ ) ( 𝐴 ⊆ ∪ ran ( (,) ∘ 𝑓 ) ∧ sup ( ran seq 1 ( + , ( ( abs ∘ − ) ∘ 𝑓 ) ) , ℝ* , < ) ≤ ( ( vol* ‘ 𝐴 ) + ( 𝐵 / ( 2 ↑ 𝑛 ) ) ) ) )
22 21 ralrimiva ⊢ ( 𝜑 → ∀ 𝑛 ∈ ℕ ∃ 𝑓 ∈ ( ( ≤ ∩ ( ℝ × ℝ ) ) ↑m ℕ ) ( 𝐴 ⊆ ∪ ran ( (,) ∘ 𝑓 ) ∧ sup ( ran seq 1 ( + , ( ( abs ∘ − ) ∘ 𝑓 ) ) , ℝ* , < ) ≤ ( ( vol* ‘ 𝐴 ) + ( 𝐵 / ( 2 ↑ 𝑛 ) ) ) ) )
23 ovex ⊢ ( ( ≤ ∩ ( ℝ × ℝ ) ) ↑m ℕ ) ∈ V
24 nnenom ⊢ ℕ ≈ ω
25 coeq2 ⊢ ( 𝑓 = ( 𝑔 ‘ 𝑛 ) → ( (,) ∘ 𝑓 ) = ( (,) ∘ ( 𝑔 ‘ 𝑛 ) ) )
26 25 rneqd ⊢ ( 𝑓 = ( 𝑔 ‘ 𝑛 ) → ran ( (,) ∘ 𝑓 ) = ran ( (,) ∘ ( 𝑔 ‘ 𝑛 ) ) )
27 26 unieqd ⊢ ( 𝑓 = ( 𝑔 ‘ 𝑛 ) → ∪ ran ( (,) ∘ 𝑓 ) = ∪ ran ( (,) ∘ ( 𝑔 ‘ 𝑛 ) ) )
28 27 sseq2d ⊢ ( 𝑓 = ( 𝑔 ‘ 𝑛 ) → ( 𝐴 ⊆ ∪ ran ( (,) ∘ 𝑓 ) ↔ 𝐴 ⊆ ∪ ran ( (,) ∘ ( 𝑔 ‘ 𝑛 ) ) ) )
29 coeq2 ⊢ ( 𝑓 = ( 𝑔 ‘ 𝑛 ) → ( ( abs ∘ − ) ∘ 𝑓 ) = ( ( abs ∘ − ) ∘ ( 𝑔 ‘ 𝑛 ) ) )
30 29 seqeq3d ⊢ ( 𝑓 = ( 𝑔 ‘ 𝑛 ) → seq 1 ( + , ( ( abs ∘ − ) ∘ 𝑓 ) ) = seq 1 ( + , ( ( abs ∘ − ) ∘ ( 𝑔 ‘ 𝑛 ) ) ) )
31 30 rneqd ⊢ ( 𝑓 = ( 𝑔 ‘ 𝑛 ) → ran seq 1 ( + , ( ( abs ∘ − ) ∘ 𝑓 ) ) = ran seq 1 ( + , ( ( abs ∘ − ) ∘ ( 𝑔 ‘ 𝑛 ) ) ) )
32 31 supeq1d ⊢ ( 𝑓 = ( 𝑔 ‘ 𝑛 ) → sup ( ran seq 1 ( + , ( ( abs ∘ − ) ∘ 𝑓 ) ) , ℝ* , < ) = sup ( ran seq 1 ( + , ( ( abs ∘ − ) ∘ ( 𝑔 ‘ 𝑛 ) ) ) , ℝ* , < ) )
33 32 breq1d ⊢ ( 𝑓 = ( 𝑔 ‘ 𝑛 ) → ( sup ( ran seq 1 ( + , ( ( abs ∘ − ) ∘ 𝑓 ) ) , ℝ* , < ) ≤ ( ( vol* ‘ 𝐴 ) + ( 𝐵 / ( 2 ↑ 𝑛 ) ) ) ↔ sup ( ran seq 1 ( + , ( ( abs ∘ − ) ∘ ( 𝑔 ‘ 𝑛 ) ) ) , ℝ* , < ) ≤ ( ( vol* ‘ 𝐴 ) + ( 𝐵 / ( 2 ↑ 𝑛 ) ) ) ) )
34 28 33 anbi12d ⊢ ( 𝑓 = ( 𝑔 ‘ 𝑛 ) → ( ( 𝐴 ⊆ ∪ ran ( (,) ∘ 𝑓 ) ∧ sup ( ran seq 1 ( + , ( ( abs ∘ − ) ∘ 𝑓 ) ) , ℝ* , < ) ≤ ( ( vol* ‘ 𝐴 ) + ( 𝐵 / ( 2 ↑ 𝑛 ) ) ) ) ↔ ( 𝐴 ⊆ ∪ ran ( (,) ∘ ( 𝑔 ‘ 𝑛 ) ) ∧ sup ( ran seq 1 ( + , ( ( abs ∘ − ) ∘ ( 𝑔 ‘ 𝑛 ) ) ) , ℝ* , < ) ≤ ( ( vol* ‘ 𝐴 ) + ( 𝐵 / ( 2 ↑ 𝑛 ) ) ) ) ) )
35 23 24 34 axcc4 ⊢ ( ∀ 𝑛 ∈ ℕ ∃ 𝑓 ∈ ( ( ≤ ∩ ( ℝ × ℝ ) ) ↑m ℕ ) ( 𝐴 ⊆ ∪ ran ( (,) ∘ 𝑓 ) ∧ sup ( ran seq 1 ( + , ( ( abs ∘ − ) ∘ 𝑓 ) ) , ℝ* , < ) ≤ ( ( vol* ‘ 𝐴 ) + ( 𝐵 / ( 2 ↑ 𝑛 ) ) ) ) → ∃ 𝑔 ( 𝑔 : ℕ ⟶ ( ( ≤ ∩ ( ℝ × ℝ ) ) ↑m ℕ ) ∧ ∀ 𝑛 ∈ ℕ ( 𝐴 ⊆ ∪ ran ( (,) ∘ ( 𝑔 ‘ 𝑛 ) ) ∧ sup ( ran seq 1 ( + , ( ( abs ∘ − ) ∘ ( 𝑔 ‘ 𝑛 ) ) ) , ℝ* , < ) ≤ ( ( vol* ‘ 𝐴 ) + ( 𝐵 / ( 2 ↑ 𝑛 ) ) ) ) ) )
36 22 35 syl ⊢ ( 𝜑 → ∃ 𝑔 ( 𝑔 : ℕ ⟶ ( ( ≤ ∩ ( ℝ × ℝ ) ) ↑m ℕ ) ∧ ∀ 𝑛 ∈ ℕ ( 𝐴 ⊆ ∪ ran ( (,) ∘ ( 𝑔 ‘ 𝑛 ) ) ∧ sup ( ran seq 1 ( + , ( ( abs ∘ − ) ∘ ( 𝑔 ‘ 𝑛 ) ) ) , ℝ* , < ) ≤ ( ( vol* ‘ 𝐴 ) + ( 𝐵 / ( 2 ↑ 𝑛 ) ) ) ) ) )
37 xpnnen ⊢ ( ℕ × ℕ ) ≈ ℕ
38 37 ensymi ⊢ ℕ ≈ ( ℕ × ℕ )
39 bren ⊢ ( ℕ ≈ ( ℕ × ℕ ) ↔ ∃ 𝑗 𝑗 : ℕ –1-1-onto→ ( ℕ × ℕ ) )
40 38 39 mpbi ⊢ ∃ 𝑗 𝑗 : ℕ –1-1-onto→ ( ℕ × ℕ )
41 nfcv ⊢ Ⅎ 𝑚 ( vol* ‘ 𝐴 )
42 nfcv ⊢ Ⅎ 𝑛 vol*
43 42 8 nffv ⊢ Ⅎ 𝑛 ( vol* ‘ ⦋ 𝑚 / 𝑛 ⦌ 𝐴 )
44 9 fveq2d ⊢ ( 𝑛 = 𝑚 → ( vol* ‘ 𝐴 ) = ( vol* ‘ ⦋ 𝑚 / 𝑛 ⦌ 𝐴 ) )
45 41 43 44 cbvmpt ⊢ ( 𝑛 ∈ ℕ ↦ ( vol* ‘ 𝐴 ) ) = ( 𝑚 ∈ ℕ ↦ ( vol* ‘ ⦋ 𝑚 / 𝑛 ⦌ 𝐴 ) )
46 2 45 eqtri ⊢ 𝐺 = ( 𝑚 ∈ ℕ ↦ ( vol* ‘ ⦋ 𝑚 / 𝑛 ⦌ 𝐴 ) )
47 3 ralrimiva ⊢ ( 𝜑 → ∀ 𝑛 ∈ ℕ 𝐴 ⊆ ℝ )
48 nfv ⊢ Ⅎ 𝑚 𝐴 ⊆ ℝ
49 nfcv ⊢ Ⅎ 𝑛 ℝ
50 8 49 nfss ⊢ Ⅎ 𝑛 ⦋ 𝑚 / 𝑛 ⦌ 𝐴 ⊆ ℝ
51 9 sseq1d ⊢ ( 𝑛 = 𝑚 → ( 𝐴 ⊆ ℝ ↔ ⦋ 𝑚 / 𝑛 ⦌ 𝐴 ⊆ ℝ ) )
52 48 50 51 cbvralw ⊢ ( ∀ 𝑛 ∈ ℕ 𝐴 ⊆ ℝ ↔ ∀ 𝑚 ∈ ℕ ⦋ 𝑚 / 𝑛 ⦌ 𝐴 ⊆ ℝ )
53 47 52 sylib ⊢ ( 𝜑 → ∀ 𝑚 ∈ ℕ ⦋ 𝑚 / 𝑛 ⦌ 𝐴 ⊆ ℝ )
54 53 r19.21bi ⊢ ( ( 𝜑 ∧ 𝑚 ∈ ℕ ) → ⦋ 𝑚 / 𝑛 ⦌ 𝐴 ⊆ ℝ )
55 54 ad4ant14 ⊢ ( ( ( ( 𝜑 ∧ 𝑗 : ℕ –1-1-onto→ ( ℕ × ℕ ) ) ∧ ( 𝑔 : ℕ ⟶ ( ( ≤ ∩ ( ℝ × ℝ ) ) ↑m ℕ ) ∧ ∀ 𝑛 ∈ ℕ ( 𝐴 ⊆ ∪ ran ( (,) ∘ ( 𝑔 ‘ 𝑛 ) ) ∧ sup ( ran seq 1 ( + , ( ( abs ∘ − ) ∘ ( 𝑔 ‘ 𝑛 ) ) ) , ℝ* , < ) ≤ ( ( vol* ‘ 𝐴 ) + ( 𝐵 / ( 2 ↑ 𝑛 ) ) ) ) ) ) ∧ 𝑚 ∈ ℕ ) → ⦋ 𝑚 / 𝑛 ⦌ 𝐴 ⊆ ℝ )
56 4 ralrimiva ⊢ ( 𝜑 → ∀ 𝑛 ∈ ℕ ( vol* ‘ 𝐴 ) ∈ ℝ )
57 41 nfel1 ⊢ Ⅎ 𝑚 ( vol* ‘ 𝐴 ) ∈ ℝ
58 43 nfel1 ⊢ Ⅎ 𝑛 ( vol* ‘ ⦋ 𝑚 / 𝑛 ⦌ 𝐴 ) ∈ ℝ
59 44 eleq1d ⊢ ( 𝑛 = 𝑚 → ( ( vol* ‘ 𝐴 ) ∈ ℝ ↔ ( vol* ‘ ⦋ 𝑚 / 𝑛 ⦌ 𝐴 ) ∈ ℝ ) )
60 57 58 59 cbvralw ⊢ ( ∀ 𝑛 ∈ ℕ ( vol* ‘ 𝐴 ) ∈ ℝ ↔ ∀ 𝑚 ∈ ℕ ( vol* ‘ ⦋ 𝑚 / 𝑛 ⦌ 𝐴 ) ∈ ℝ )
61 56 60 sylib ⊢ ( 𝜑 → ∀ 𝑚 ∈ ℕ ( vol* ‘ ⦋ 𝑚 / 𝑛 ⦌ 𝐴 ) ∈ ℝ )
62 61 r19.21bi ⊢ ( ( 𝜑 ∧ 𝑚 ∈ ℕ ) → ( vol* ‘ ⦋ 𝑚 / 𝑛 ⦌ 𝐴 ) ∈ ℝ )
63 62 ad4ant14 ⊢ ( ( ( ( 𝜑 ∧ 𝑗 : ℕ –1-1-onto→ ( ℕ × ℕ ) ) ∧ ( 𝑔 : ℕ ⟶ ( ( ≤ ∩ ( ℝ × ℝ ) ) ↑m ℕ ) ∧ ∀ 𝑛 ∈ ℕ ( 𝐴 ⊆ ∪ ran ( (,) ∘ ( 𝑔 ‘ 𝑛 ) ) ∧ sup ( ran seq 1 ( + , ( ( abs ∘ − ) ∘ ( 𝑔 ‘ 𝑛 ) ) ) , ℝ* , < ) ≤ ( ( vol* ‘ 𝐴 ) + ( 𝐵 / ( 2 ↑ 𝑛 ) ) ) ) ) ) ∧ 𝑚 ∈ ℕ ) → ( vol* ‘ ⦋ 𝑚 / 𝑛 ⦌ 𝐴 ) ∈ ℝ )
64 5 ad2antrr ⊢ ( ( ( 𝜑 ∧ 𝑗 : ℕ –1-1-onto→ ( ℕ × ℕ ) ) ∧ ( 𝑔 : ℕ ⟶ ( ( ≤ ∩ ( ℝ × ℝ ) ) ↑m ℕ ) ∧ ∀ 𝑛 ∈ ℕ ( 𝐴 ⊆ ∪ ran ( (,) ∘ ( 𝑔 ‘ 𝑛 ) ) ∧ sup ( ran seq 1 ( + , ( ( abs ∘ − ) ∘ ( 𝑔 ‘ 𝑛 ) ) ) , ℝ* , < ) ≤ ( ( vol* ‘ 𝐴 ) + ( 𝐵 / ( 2 ↑ 𝑛 ) ) ) ) ) ) → sup ( ran 𝑇 , ℝ* , < ) ∈ ℝ )
65 6 ad2antrr ⊢ ( ( ( 𝜑 ∧ 𝑗 : ℕ –1-1-onto→ ( ℕ × ℕ ) ) ∧ ( 𝑔 : ℕ ⟶ ( ( ≤ ∩ ( ℝ × ℝ ) ) ↑m ℕ ) ∧ ∀ 𝑛 ∈ ℕ ( 𝐴 ⊆ ∪ ran ( (,) ∘ ( 𝑔 ‘ 𝑛 ) ) ∧ sup ( ran seq 1 ( + , ( ( abs ∘ − ) ∘ ( 𝑔 ‘ 𝑛 ) ) ) , ℝ* , < ) ≤ ( ( vol* ‘ 𝐴 ) + ( 𝐵 / ( 2 ↑ 𝑛 ) ) ) ) ) ) → 𝐵 ∈ ℝ+ )
66 eqid ⊢ seq 1 ( + , ( ( abs ∘ − ) ∘ ( 𝑔 ‘ 𝑚 ) ) ) = seq 1 ( + , ( ( abs ∘ − ) ∘ ( 𝑔 ‘ 𝑚 ) ) )
67 eqid ⊢ seq 1 ( + , ( ( abs ∘ − ) ∘ ( 𝑘 ∈ ℕ ↦ ( ( 𝑔 ‘ ( 1st ‘ ( 𝑗 ‘ 𝑘 ) ) ) ‘ ( 2nd ‘ ( 𝑗 ‘ 𝑘 ) ) ) ) ) ) = seq 1 ( + , ( ( abs ∘ − ) ∘ ( 𝑘 ∈ ℕ ↦ ( ( 𝑔 ‘ ( 1st ‘ ( 𝑗 ‘ 𝑘 ) ) ) ‘ ( 2nd ‘ ( 𝑗 ‘ 𝑘 ) ) ) ) ) )
68 eqid ⊢ ( 𝑘 ∈ ℕ ↦ ( ( 𝑔 ‘ ( 1st ‘ ( 𝑗 ‘ 𝑘 ) ) ) ‘ ( 2nd ‘ ( 𝑗 ‘ 𝑘 ) ) ) ) = ( 𝑘 ∈ ℕ ↦ ( ( 𝑔 ‘ ( 1st ‘ ( 𝑗 ‘ 𝑘 ) ) ) ‘ ( 2nd ‘ ( 𝑗 ‘ 𝑘 ) ) ) )
69 simplr ⊢ ( ( ( 𝜑 ∧ 𝑗 : ℕ –1-1-onto→ ( ℕ × ℕ ) ) ∧ ( 𝑔 : ℕ ⟶ ( ( ≤ ∩ ( ℝ × ℝ ) ) ↑m ℕ ) ∧ ∀ 𝑛 ∈ ℕ ( 𝐴 ⊆ ∪ ran ( (,) ∘ ( 𝑔 ‘ 𝑛 ) ) ∧ sup ( ran seq 1 ( + , ( ( abs ∘ − ) ∘ ( 𝑔 ‘ 𝑛 ) ) ) , ℝ* , < ) ≤ ( ( vol* ‘ 𝐴 ) + ( 𝐵 / ( 2 ↑ 𝑛 ) ) ) ) ) ) → 𝑗 : ℕ –1-1-onto→ ( ℕ × ℕ ) )
70 simprl ⊢ ( ( ( 𝜑 ∧ 𝑗 : ℕ –1-1-onto→ ( ℕ × ℕ ) ) ∧ ( 𝑔 : ℕ ⟶ ( ( ≤ ∩ ( ℝ × ℝ ) ) ↑m ℕ ) ∧ ∀ 𝑛 ∈ ℕ ( 𝐴 ⊆ ∪ ran ( (,) ∘ ( 𝑔 ‘ 𝑛 ) ) ∧ sup ( ran seq 1 ( + , ( ( abs ∘ − ) ∘ ( 𝑔 ‘ 𝑛 ) ) ) , ℝ* , < ) ≤ ( ( vol* ‘ 𝐴 ) + ( 𝐵 / ( 2 ↑ 𝑛 ) ) ) ) ) ) → 𝑔 : ℕ ⟶ ( ( ≤ ∩ ( ℝ × ℝ ) ) ↑m ℕ ) )
71 simprr ⊢ ( ( ( 𝜑 ∧ 𝑗 : ℕ –1-1-onto→ ( ℕ × ℕ ) ) ∧ ( 𝑔 : ℕ ⟶ ( ( ≤ ∩ ( ℝ × ℝ ) ) ↑m ℕ ) ∧ ∀ 𝑛 ∈ ℕ ( 𝐴 ⊆ ∪ ran ( (,) ∘ ( 𝑔 ‘ 𝑛 ) ) ∧ sup ( ran seq 1 ( + , ( ( abs ∘ − ) ∘ ( 𝑔 ‘ 𝑛 ) ) ) , ℝ* , < ) ≤ ( ( vol* ‘ 𝐴 ) + ( 𝐵 / ( 2 ↑ 𝑛 ) ) ) ) ) ) → ∀ 𝑛 ∈ ℕ ( 𝐴 ⊆ ∪ ran ( (,) ∘ ( 𝑔 ‘ 𝑛 ) ) ∧ sup ( ran seq 1 ( + , ( ( abs ∘ − ) ∘ ( 𝑔 ‘ 𝑛 ) ) ) , ℝ* , < ) ≤ ( ( vol* ‘ 𝐴 ) + ( 𝐵 / ( 2 ↑ 𝑛 ) ) ) ) )
72 nfv ⊢ Ⅎ 𝑚 ( 𝐴 ⊆ ∪ ran ( (,) ∘ ( 𝑔 ‘ 𝑛 ) ) ∧ sup ( ran seq 1 ( + , ( ( abs ∘ − ) ∘ ( 𝑔 ‘ 𝑛 ) ) ) , ℝ* , < ) ≤ ( ( vol* ‘ 𝐴 ) + ( 𝐵 / ( 2 ↑ 𝑛 ) ) ) )
73 nfcv ⊢ Ⅎ 𝑛 ∪ ran ( (,) ∘ ( 𝑔 ‘ 𝑚 ) )
74 8 73 nfss ⊢ Ⅎ 𝑛 ⦋ 𝑚 / 𝑛 ⦌ 𝐴 ⊆ ∪ ran ( (,) ∘ ( 𝑔 ‘ 𝑚 ) )
75 nfcv ⊢ Ⅎ 𝑛 sup ( ran seq 1 ( + , ( ( abs ∘ − ) ∘ ( 𝑔 ‘ 𝑚 ) ) ) , ℝ* , < )
76 nfcv ⊢ Ⅎ 𝑛 ≤
77 nfcv ⊢ Ⅎ 𝑛 +
78 nfcv ⊢ Ⅎ 𝑛 ( 𝐵 / ( 2 ↑ 𝑚 ) )
79 43 77 78 nfov ⊢ Ⅎ 𝑛 ( ( vol* ‘ ⦋ 𝑚 / 𝑛 ⦌ 𝐴 ) + ( 𝐵 / ( 2 ↑ 𝑚 ) ) )
80 75 76 79 nfbr ⊢ Ⅎ 𝑛 sup ( ran seq 1 ( + , ( ( abs ∘ − ) ∘ ( 𝑔 ‘ 𝑚 ) ) ) , ℝ* , < ) ≤ ( ( vol* ‘ ⦋ 𝑚 / 𝑛 ⦌ 𝐴 ) + ( 𝐵 / ( 2 ↑ 𝑚 ) ) )
81 74 80 nfan ⊢ Ⅎ 𝑛 ( ⦋ 𝑚 / 𝑛 ⦌ 𝐴 ⊆ ∪ ran ( (,) ∘ ( 𝑔 ‘ 𝑚 ) ) ∧ sup ( ran seq 1 ( + , ( ( abs ∘ − ) ∘ ( 𝑔 ‘ 𝑚 ) ) ) , ℝ* , < ) ≤ ( ( vol* ‘ ⦋ 𝑚 / 𝑛 ⦌ 𝐴 ) + ( 𝐵 / ( 2 ↑ 𝑚 ) ) ) )
82 fveq2 ⊢ ( 𝑛 = 𝑚 → ( 𝑔 ‘ 𝑛 ) = ( 𝑔 ‘ 𝑚 ) )
83 82 coeq2d ⊢ ( 𝑛 = 𝑚 → ( (,) ∘ ( 𝑔 ‘ 𝑛 ) ) = ( (,) ∘ ( 𝑔 ‘ 𝑚 ) ) )
84 83 rneqd ⊢ ( 𝑛 = 𝑚 → ran ( (,) ∘ ( 𝑔 ‘ 𝑛 ) ) = ran ( (,) ∘ ( 𝑔 ‘ 𝑚 ) ) )
85 84 unieqd ⊢ ( 𝑛 = 𝑚 → ∪ ran ( (,) ∘ ( 𝑔 ‘ 𝑛 ) ) = ∪ ran ( (,) ∘ ( 𝑔 ‘ 𝑚 ) ) )
86 9 85 sseq12d ⊢ ( 𝑛 = 𝑚 → ( 𝐴 ⊆ ∪ ran ( (,) ∘ ( 𝑔 ‘ 𝑛 ) ) ↔ ⦋ 𝑚 / 𝑛 ⦌ 𝐴 ⊆ ∪ ran ( (,) ∘ ( 𝑔 ‘ 𝑚 ) ) ) )
87 82 coeq2d ⊢ ( 𝑛 = 𝑚 → ( ( abs ∘ − ) ∘ ( 𝑔 ‘ 𝑛 ) ) = ( ( abs ∘ − ) ∘ ( 𝑔 ‘ 𝑚 ) ) )
88 87 seqeq3d ⊢ ( 𝑛 = 𝑚 → seq 1 ( + , ( ( abs ∘ − ) ∘ ( 𝑔 ‘ 𝑛 ) ) ) = seq 1 ( + , ( ( abs ∘ − ) ∘ ( 𝑔 ‘ 𝑚 ) ) ) )
89 88 rneqd ⊢ ( 𝑛 = 𝑚 → ran seq 1 ( + , ( ( abs ∘ − ) ∘ ( 𝑔 ‘ 𝑛 ) ) ) = ran seq 1 ( + , ( ( abs ∘ − ) ∘ ( 𝑔 ‘ 𝑚 ) ) ) )
90 89 supeq1d ⊢ ( 𝑛 = 𝑚 → sup ( ran seq 1 ( + , ( ( abs ∘ − ) ∘ ( 𝑔 ‘ 𝑛 ) ) ) , ℝ* , < ) = sup ( ran seq 1 ( + , ( ( abs ∘ − ) ∘ ( 𝑔 ‘ 𝑚 ) ) ) , ℝ* , < ) )
91 oveq2 ⊢ ( 𝑛 = 𝑚 → ( 2 ↑ 𝑛 ) = ( 2 ↑ 𝑚 ) )
92 91 oveq2d ⊢ ( 𝑛 = 𝑚 → ( 𝐵 / ( 2 ↑ 𝑛 ) ) = ( 𝐵 / ( 2 ↑ 𝑚 ) ) )
93 44 92 oveq12d ⊢ ( 𝑛 = 𝑚 → ( ( vol* ‘ 𝐴 ) + ( 𝐵 / ( 2 ↑ 𝑛 ) ) ) = ( ( vol* ‘ ⦋ 𝑚 / 𝑛 ⦌ 𝐴 ) + ( 𝐵 / ( 2 ↑ 𝑚 ) ) ) )
94 90 93 breq12d ⊢ ( 𝑛 = 𝑚 → ( sup ( ran seq 1 ( + , ( ( abs ∘ − ) ∘ ( 𝑔 ‘ 𝑛 ) ) ) , ℝ* , < ) ≤ ( ( vol* ‘ 𝐴 ) + ( 𝐵 / ( 2 ↑ 𝑛 ) ) ) ↔ sup ( ran seq 1 ( + , ( ( abs ∘ − ) ∘ ( 𝑔 ‘ 𝑚 ) ) ) , ℝ* , < ) ≤ ( ( vol* ‘ ⦋ 𝑚 / 𝑛 ⦌ 𝐴 ) + ( 𝐵 / ( 2 ↑ 𝑚 ) ) ) ) )
95 86 94 anbi12d ⊢ ( 𝑛 = 𝑚 → ( ( 𝐴 ⊆ ∪ ran ( (,) ∘ ( 𝑔 ‘ 𝑛 ) ) ∧ sup ( ran seq 1 ( + , ( ( abs ∘ − ) ∘ ( 𝑔 ‘ 𝑛 ) ) ) , ℝ* , < ) ≤ ( ( vol* ‘ 𝐴 ) + ( 𝐵 / ( 2 ↑ 𝑛 ) ) ) ) ↔ ( ⦋ 𝑚 / 𝑛 ⦌ 𝐴 ⊆ ∪ ran ( (,) ∘ ( 𝑔 ‘ 𝑚 ) ) ∧ sup ( ran seq 1 ( + , ( ( abs ∘ − ) ∘ ( 𝑔 ‘ 𝑚 ) ) ) , ℝ* , < ) ≤ ( ( vol* ‘ ⦋ 𝑚 / 𝑛 ⦌ 𝐴 ) + ( 𝐵 / ( 2 ↑ 𝑚 ) ) ) ) ) )
96 72 81 95 cbvralw ⊢ ( ∀ 𝑛 ∈ ℕ ( 𝐴 ⊆ ∪ ran ( (,) ∘ ( 𝑔 ‘ 𝑛 ) ) ∧ sup ( ran seq 1 ( + , ( ( abs ∘ − ) ∘ ( 𝑔 ‘ 𝑛 ) ) ) , ℝ* , < ) ≤ ( ( vol* ‘ 𝐴 ) + ( 𝐵 / ( 2 ↑ 𝑛 ) ) ) ) ↔ ∀ 𝑚 ∈ ℕ ( ⦋ 𝑚 / 𝑛 ⦌ 𝐴 ⊆ ∪ ran ( (,) ∘ ( 𝑔 ‘ 𝑚 ) ) ∧ sup ( ran seq 1 ( + , ( ( abs ∘ − ) ∘ ( 𝑔 ‘ 𝑚 ) ) ) , ℝ* , < ) ≤ ( ( vol* ‘ ⦋ 𝑚 / 𝑛 ⦌ 𝐴 ) + ( 𝐵 / ( 2 ↑ 𝑚 ) ) ) ) )
97 71 96 sylib ⊢ ( ( ( 𝜑 ∧ 𝑗 : ℕ –1-1-onto→ ( ℕ × ℕ ) ) ∧ ( 𝑔 : ℕ ⟶ ( ( ≤ ∩ ( ℝ × ℝ ) ) ↑m ℕ ) ∧ ∀ 𝑛 ∈ ℕ ( 𝐴 ⊆ ∪ ran ( (,) ∘ ( 𝑔 ‘ 𝑛 ) ) ∧ sup ( ran seq 1 ( + , ( ( abs ∘ − ) ∘ ( 𝑔 ‘ 𝑛 ) ) ) , ℝ* , < ) ≤ ( ( vol* ‘ 𝐴 ) + ( 𝐵 / ( 2 ↑ 𝑛 ) ) ) ) ) ) → ∀ 𝑚 ∈ ℕ ( ⦋ 𝑚 / 𝑛 ⦌ 𝐴 ⊆ ∪ ran ( (,) ∘ ( 𝑔 ‘ 𝑚 ) ) ∧ sup ( ran seq 1 ( + , ( ( abs ∘ − ) ∘ ( 𝑔 ‘ 𝑚 ) ) ) , ℝ* , < ) ≤ ( ( vol* ‘ ⦋ 𝑚 / 𝑛 ⦌ 𝐴 ) + ( 𝐵 / ( 2 ↑ 𝑚 ) ) ) ) )
98 97 r19.21bi ⊢ ( ( ( ( 𝜑 ∧ 𝑗 : ℕ –1-1-onto→ ( ℕ × ℕ ) ) ∧ ( 𝑔 : ℕ ⟶ ( ( ≤ ∩ ( ℝ × ℝ ) ) ↑m ℕ ) ∧ ∀ 𝑛 ∈ ℕ ( 𝐴 ⊆ ∪ ran ( (,) ∘ ( 𝑔 ‘ 𝑛 ) ) ∧ sup ( ran seq 1 ( + , ( ( abs ∘ − ) ∘ ( 𝑔 ‘ 𝑛 ) ) ) , ℝ* , < ) ≤ ( ( vol* ‘ 𝐴 ) + ( 𝐵 / ( 2 ↑ 𝑛 ) ) ) ) ) ) ∧ 𝑚 ∈ ℕ ) → ( ⦋ 𝑚 / 𝑛 ⦌ 𝐴 ⊆ ∪ ran ( (,) ∘ ( 𝑔 ‘ 𝑚 ) ) ∧ sup ( ran seq 1 ( + , ( ( abs ∘ − ) ∘ ( 𝑔 ‘ 𝑚 ) ) ) , ℝ* , < ) ≤ ( ( vol* ‘ ⦋ 𝑚 / 𝑛 ⦌ 𝐴 ) + ( 𝐵 / ( 2 ↑ 𝑚 ) ) ) ) )
99 98 simpld ⊢ ( ( ( ( 𝜑 ∧ 𝑗 : ℕ –1-1-onto→ ( ℕ × ℕ ) ) ∧ ( 𝑔 : ℕ ⟶ ( ( ≤ ∩ ( ℝ × ℝ ) ) ↑m ℕ ) ∧ ∀ 𝑛 ∈ ℕ ( 𝐴 ⊆ ∪ ran ( (,) ∘ ( 𝑔 ‘ 𝑛 ) ) ∧ sup ( ran seq 1 ( + , ( ( abs ∘ − ) ∘ ( 𝑔 ‘ 𝑛 ) ) ) , ℝ* , < ) ≤ ( ( vol* ‘ 𝐴 ) + ( 𝐵 / ( 2 ↑ 𝑛 ) ) ) ) ) ) ∧ 𝑚 ∈ ℕ ) → ⦋ 𝑚 / 𝑛 ⦌ 𝐴 ⊆ ∪ ran ( (,) ∘ ( 𝑔 ‘ 𝑚 ) ) )
100 98 simprd ⊢ ( ( ( ( 𝜑 ∧ 𝑗 : ℕ –1-1-onto→ ( ℕ × ℕ ) ) ∧ ( 𝑔 : ℕ ⟶ ( ( ≤ ∩ ( ℝ × ℝ ) ) ↑m ℕ ) ∧ ∀ 𝑛 ∈ ℕ ( 𝐴 ⊆ ∪ ran ( (,) ∘ ( 𝑔 ‘ 𝑛 ) ) ∧ sup ( ran seq 1 ( + , ( ( abs ∘ − ) ∘ ( 𝑔 ‘ 𝑛 ) ) ) , ℝ* , < ) ≤ ( ( vol* ‘ 𝐴 ) + ( 𝐵 / ( 2 ↑ 𝑛 ) ) ) ) ) ) ∧ 𝑚 ∈ ℕ ) → sup ( ran seq 1 ( + , ( ( abs ∘ − ) ∘ ( 𝑔 ‘ 𝑚 ) ) ) , ℝ* , < ) ≤ ( ( vol* ‘ ⦋ 𝑚 / 𝑛 ⦌ 𝐴 ) + ( 𝐵 / ( 2 ↑ 𝑚 ) ) ) )
101 1 46 55 63 64 65 66 67 68 69 70 99 100 ovoliunlem2 ⊢ ( ( ( 𝜑 ∧ 𝑗 : ℕ –1-1-onto→ ( ℕ × ℕ ) ) ∧ ( 𝑔 : ℕ ⟶ ( ( ≤ ∩ ( ℝ × ℝ ) ) ↑m ℕ ) ∧ ∀ 𝑛 ∈ ℕ ( 𝐴 ⊆ ∪ ran ( (,) ∘ ( 𝑔 ‘ 𝑛 ) ) ∧ sup ( ran seq 1 ( + , ( ( abs ∘ − ) ∘ ( 𝑔 ‘ 𝑛 ) ) ) , ℝ* , < ) ≤ ( ( vol* ‘ 𝐴 ) + ( 𝐵 / ( 2 ↑ 𝑛 ) ) ) ) ) ) → ( vol* ‘ ∪ 𝑚 ∈ ℕ ⦋ 𝑚 / 𝑛 ⦌ 𝐴 ) ≤ ( sup ( ran 𝑇 , ℝ* , < ) + 𝐵 ) )
102 101 exp31 ⊢ ( 𝜑 → ( 𝑗 : ℕ –1-1-onto→ ( ℕ × ℕ ) → ( ( 𝑔 : ℕ ⟶ ( ( ≤ ∩ ( ℝ × ℝ ) ) ↑m ℕ ) ∧ ∀ 𝑛 ∈ ℕ ( 𝐴 ⊆ ∪ ran ( (,) ∘ ( 𝑔 ‘ 𝑛 ) ) ∧ sup ( ran seq 1 ( + , ( ( abs ∘ − ) ∘ ( 𝑔 ‘ 𝑛 ) ) ) , ℝ* , < ) ≤ ( ( vol* ‘ 𝐴 ) + ( 𝐵 / ( 2 ↑ 𝑛 ) ) ) ) ) → ( vol* ‘ ∪ 𝑚 ∈ ℕ ⦋ 𝑚 / 𝑛 ⦌ 𝐴 ) ≤ ( sup ( ran 𝑇 , ℝ* , < ) + 𝐵 ) ) ) )
103 102 exlimdv ⊢ ( 𝜑 → ( ∃ 𝑗 𝑗 : ℕ –1-1-onto→ ( ℕ × ℕ ) → ( ( 𝑔 : ℕ ⟶ ( ( ≤ ∩ ( ℝ × ℝ ) ) ↑m ℕ ) ∧ ∀ 𝑛 ∈ ℕ ( 𝐴 ⊆ ∪ ran ( (,) ∘ ( 𝑔 ‘ 𝑛 ) ) ∧ sup ( ran seq 1 ( + , ( ( abs ∘ − ) ∘ ( 𝑔 ‘ 𝑛 ) ) ) , ℝ* , < ) ≤ ( ( vol* ‘ 𝐴 ) + ( 𝐵 / ( 2 ↑ 𝑛 ) ) ) ) ) → ( vol* ‘ ∪ 𝑚 ∈ ℕ ⦋ 𝑚 / 𝑛 ⦌ 𝐴 ) ≤ ( sup ( ran 𝑇 , ℝ* , < ) + 𝐵 ) ) ) )
104 40 103 mpi ⊢ ( 𝜑 → ( ( 𝑔 : ℕ ⟶ ( ( ≤ ∩ ( ℝ × ℝ ) ) ↑m ℕ ) ∧ ∀ 𝑛 ∈ ℕ ( 𝐴 ⊆ ∪ ran ( (,) ∘ ( 𝑔 ‘ 𝑛 ) ) ∧ sup ( ran seq 1 ( + , ( ( abs ∘ − ) ∘ ( 𝑔 ‘ 𝑛 ) ) ) , ℝ* , < ) ≤ ( ( vol* ‘ 𝐴 ) + ( 𝐵 / ( 2 ↑ 𝑛 ) ) ) ) ) → ( vol* ‘ ∪ 𝑚 ∈ ℕ ⦋ 𝑚 / 𝑛 ⦌ 𝐴 ) ≤ ( sup ( ran 𝑇 , ℝ* , < ) + 𝐵 ) ) )
105 104 exlimdv ⊢ ( 𝜑 → ( ∃ 𝑔 ( 𝑔 : ℕ ⟶ ( ( ≤ ∩ ( ℝ × ℝ ) ) ↑m ℕ ) ∧ ∀ 𝑛 ∈ ℕ ( 𝐴 ⊆ ∪ ran ( (,) ∘ ( 𝑔 ‘ 𝑛 ) ) ∧ sup ( ran seq 1 ( + , ( ( abs ∘ − ) ∘ ( 𝑔 ‘ 𝑛 ) ) ) , ℝ* , < ) ≤ ( ( vol* ‘ 𝐴 ) + ( 𝐵 / ( 2 ↑ 𝑛 ) ) ) ) ) → ( vol* ‘ ∪ 𝑚 ∈ ℕ ⦋ 𝑚 / 𝑛 ⦌ 𝐴 ) ≤ ( sup ( ran 𝑇 , ℝ* , < ) + 𝐵 ) ) )
106 36 105 mpd ⊢ ( 𝜑 → ( vol* ‘ ∪ 𝑚 ∈ ℕ ⦋ 𝑚 / 𝑛 ⦌ 𝐴 ) ≤ ( sup ( ran 𝑇 , ℝ* , < ) + 𝐵 ) )
107 11 106 eqbrtrid ⊢ ( 𝜑 → ( vol* ‘ ∪ 𝑛 ∈ ℕ 𝐴 ) ≤ ( sup ( ran 𝑇 , ℝ* , < ) + 𝐵 ) )