Metamath Proof Explorer

Theorem uniioombllem3a

Description: Lemma for uniioombl . (Contributed by Mario Carneiro, 8-May-2015)

Ref Expression
Hypotheses uniioombl.1 ⊢ ( 𝜑 → 𝐹 : ℕ ⟶ ( ≤ ∩ ( ℝ × ℝ ) ) )
uniioombl.2 ⊢ ( 𝜑 → Disj 𝑥 ∈ ℕ ( (,) ‘ ( 𝐹 ‘ 𝑥 ) ) )
uniioombl.3 ⊢ 𝑆 = seq 1 ( + , ( ( abs ∘ − ) ∘ 𝐹 ) )
uniioombl.a ⊢ 𝐴 = ∪ ran ( (,) ∘ 𝐹 )
uniioombl.e ⊢ ( 𝜑 → ( vol* ‘ 𝐸 ) ∈ ℝ )
uniioombl.c ⊢ ( 𝜑 → 𝐶 ∈ ℝ+ )
uniioombl.g ⊢ ( 𝜑 → 𝐺 : ℕ ⟶ ( ≤ ∩ ( ℝ × ℝ ) ) )
uniioombl.s ⊢ ( 𝜑 → 𝐸 ⊆ ∪ ran ( (,) ∘ 𝐺 ) )
uniioombl.t ⊢ 𝑇 = seq 1 ( + , ( ( abs ∘ − ) ∘ 𝐺 ) )
uniioombl.v ⊢ ( 𝜑 → sup ( ran 𝑇 , ℝ* , < ) ≤ ( ( vol* ‘ 𝐸 ) + 𝐶 ) )
uniioombl.m ⊢ ( 𝜑 → 𝑀 ∈ ℕ )
uniioombl.m2 ⊢ ( 𝜑 → ( abs ‘ ( ( 𝑇 ‘ 𝑀 ) − sup ( ran 𝑇 , ℝ* , < ) ) ) < 𝐶 )
uniioombl.k ⊢ 𝐾 = ∪ ( ( (,) ∘ 𝐺 ) “ ( 1 ... 𝑀 ) )
Assertion uniioombllem3a ( 𝜑 → ( 𝐾 = ∪ 𝑗 ∈ ( 1 ... 𝑀 ) ( (,) ‘ ( 𝐺 ‘ 𝑗 ) ) ∧ ( vol* ‘ 𝐾 ) ∈ ℝ ) )

Proof

Step Hyp Ref Expression
1 uniioombl.1 ⊢ ( 𝜑 → 𝐹 : ℕ ⟶ ( ≤ ∩ ( ℝ × ℝ ) ) )
2 uniioombl.2 ⊢ ( 𝜑 → Disj 𝑥 ∈ ℕ ( (,) ‘ ( 𝐹 ‘ 𝑥 ) ) )
3 uniioombl.3 ⊢ 𝑆 = seq 1 ( + , ( ( abs ∘ − ) ∘ 𝐹 ) )
4 uniioombl.a ⊢ 𝐴 = ∪ ran ( (,) ∘ 𝐹 )
5 uniioombl.e ⊢ ( 𝜑 → ( vol* ‘ 𝐸 ) ∈ ℝ )
6 uniioombl.c ⊢ ( 𝜑 → 𝐶 ∈ ℝ+ )
7 uniioombl.g ⊢ ( 𝜑 → 𝐺 : ℕ ⟶ ( ≤ ∩ ( ℝ × ℝ ) ) )
8 uniioombl.s ⊢ ( 𝜑 → 𝐸 ⊆ ∪ ran ( (,) ∘ 𝐺 ) )
9 uniioombl.t ⊢ 𝑇 = seq 1 ( + , ( ( abs ∘ − ) ∘ 𝐺 ) )
10 uniioombl.v ⊢ ( 𝜑 → sup ( ran 𝑇 , ℝ* , < ) ≤ ( ( vol* ‘ 𝐸 ) + 𝐶 ) )
11 uniioombl.m ⊢ ( 𝜑 → 𝑀 ∈ ℕ )
12 uniioombl.m2 ⊢ ( 𝜑 → ( abs ‘ ( ( 𝑇 ‘ 𝑀 ) − sup ( ran 𝑇 , ℝ* , < ) ) ) < 𝐶 )
13 uniioombl.k ⊢ 𝐾 = ∪ ( ( (,) ∘ 𝐺 ) “ ( 1 ... 𝑀 ) )
14 ioof ⊢ (,) : ( ℝ* × ℝ* ) ⟶ 𝒫 ℝ
15 inss2 ⊢ ( ≤ ∩ ( ℝ × ℝ ) ) ⊆ ( ℝ × ℝ )
16 rexpssxrxp ⊢ ( ℝ × ℝ ) ⊆ ( ℝ* × ℝ* )
17 15 16 sstri ⊢ ( ≤ ∩ ( ℝ × ℝ ) ) ⊆ ( ℝ* × ℝ* )
18 fss ⊢ ( ( 𝐺 : ℕ ⟶ ( ≤ ∩ ( ℝ × ℝ ) ) ∧ ( ≤ ∩ ( ℝ × ℝ ) ) ⊆ ( ℝ* × ℝ* ) ) → 𝐺 : ℕ ⟶ ( ℝ* × ℝ* ) )
19 7 17 18 sylancl ⊢ ( 𝜑 → 𝐺 : ℕ ⟶ ( ℝ* × ℝ* ) )
20 fco ⊢ ( ( (,) : ( ℝ* × ℝ* ) ⟶ 𝒫 ℝ ∧ 𝐺 : ℕ ⟶ ( ℝ* × ℝ* ) ) → ( (,) ∘ 𝐺 ) : ℕ ⟶ 𝒫 ℝ )
21 14 19 20 sylancr ⊢ ( 𝜑 → ( (,) ∘ 𝐺 ) : ℕ ⟶ 𝒫 ℝ )
22 ffun ⊢ ( ( (,) ∘ 𝐺 ) : ℕ ⟶ 𝒫 ℝ → Fun ( (,) ∘ 𝐺 ) )
23 funiunfv ⊢ ( Fun ( (,) ∘ 𝐺 ) → ∪ 𝑗 ∈ ( 1 ... 𝑀 ) ( ( (,) ∘ 𝐺 ) ‘ 𝑗 ) = ∪ ( ( (,) ∘ 𝐺 ) “ ( 1 ... 𝑀 ) ) )
24 21 22 23 3syl ⊢ ( 𝜑 → ∪ 𝑗 ∈ ( 1 ... 𝑀 ) ( ( (,) ∘ 𝐺 ) ‘ 𝑗 ) = ∪ ( ( (,) ∘ 𝐺 ) “ ( 1 ... 𝑀 ) ) )
25 elfznn ⊢ ( 𝑗 ∈ ( 1 ... 𝑀 ) → 𝑗 ∈ ℕ )
26 fvco3 ⊢ ( ( 𝐺 : ℕ ⟶ ( ≤ ∩ ( ℝ × ℝ ) ) ∧ 𝑗 ∈ ℕ ) → ( ( (,) ∘ 𝐺 ) ‘ 𝑗 ) = ( (,) ‘ ( 𝐺 ‘ 𝑗 ) ) )
27 7 25 26 syl2an ⊢ ( ( 𝜑 ∧ 𝑗 ∈ ( 1 ... 𝑀 ) ) → ( ( (,) ∘ 𝐺 ) ‘ 𝑗 ) = ( (,) ‘ ( 𝐺 ‘ 𝑗 ) ) )
28 27 iuneq2dv ⊢ ( 𝜑 → ∪ 𝑗 ∈ ( 1 ... 𝑀 ) ( ( (,) ∘ 𝐺 ) ‘ 𝑗 ) = ∪ 𝑗 ∈ ( 1 ... 𝑀 ) ( (,) ‘ ( 𝐺 ‘ 𝑗 ) ) )
29 24 28 eqtr3d ⊢ ( 𝜑 → ∪ ( ( (,) ∘ 𝐺 ) “ ( 1 ... 𝑀 ) ) = ∪ 𝑗 ∈ ( 1 ... 𝑀 ) ( (,) ‘ ( 𝐺 ‘ 𝑗 ) ) )
30 13 29 syl5eq ⊢ ( 𝜑 → 𝐾 = ∪ 𝑗 ∈ ( 1 ... 𝑀 ) ( (,) ‘ ( 𝐺 ‘ 𝑗 ) ) )
31 ffvelrn ⊢ ( ( 𝐺 : ℕ ⟶ ( ≤ ∩ ( ℝ × ℝ ) ) ∧ 𝑗 ∈ ℕ ) → ( 𝐺 ‘ 𝑗 ) ∈ ( ≤ ∩ ( ℝ × ℝ ) ) )
32 7 25 31 syl2an ⊢ ( ( 𝜑 ∧ 𝑗 ∈ ( 1 ... 𝑀 ) ) → ( 𝐺 ‘ 𝑗 ) ∈ ( ≤ ∩ ( ℝ × ℝ ) ) )
33 32 elin2d ⊢ ( ( 𝜑 ∧ 𝑗 ∈ ( 1 ... 𝑀 ) ) → ( 𝐺 ‘ 𝑗 ) ∈ ( ℝ × ℝ ) )
34 1st2nd2 ⊢ ( ( 𝐺 ‘ 𝑗 ) ∈ ( ℝ × ℝ ) → ( 𝐺 ‘ 𝑗 ) = ⟨ ( 1st ‘ ( 𝐺 ‘ 𝑗 ) ) , ( 2nd ‘ ( 𝐺 ‘ 𝑗 ) ) ⟩ )
35 33 34 syl ⊢ ( ( 𝜑 ∧ 𝑗 ∈ ( 1 ... 𝑀 ) ) → ( 𝐺 ‘ 𝑗 ) = ⟨ ( 1st ‘ ( 𝐺 ‘ 𝑗 ) ) , ( 2nd ‘ ( 𝐺 ‘ 𝑗 ) ) ⟩ )
36 35 fveq2d ⊢ ( ( 𝜑 ∧ 𝑗 ∈ ( 1 ... 𝑀 ) ) → ( (,) ‘ ( 𝐺 ‘ 𝑗 ) ) = ( (,) ‘ ⟨ ( 1st ‘ ( 𝐺 ‘ 𝑗 ) ) , ( 2nd ‘ ( 𝐺 ‘ 𝑗 ) ) ⟩ ) )
37 df-ov ⊢ ( ( 1st ‘ ( 𝐺 ‘ 𝑗 ) ) (,) ( 2nd ‘ ( 𝐺 ‘ 𝑗 ) ) ) = ( (,) ‘ ⟨ ( 1st ‘ ( 𝐺 ‘ 𝑗 ) ) , ( 2nd ‘ ( 𝐺 ‘ 𝑗 ) ) ⟩ )
38 36 37 eqtr4di ⊢ ( ( 𝜑 ∧ 𝑗 ∈ ( 1 ... 𝑀 ) ) → ( (,) ‘ ( 𝐺 ‘ 𝑗 ) ) = ( ( 1st ‘ ( 𝐺 ‘ 𝑗 ) ) (,) ( 2nd ‘ ( 𝐺 ‘ 𝑗 ) ) ) )
39 ioossre ⊢ ( ( 1st ‘ ( 𝐺 ‘ 𝑗 ) ) (,) ( 2nd ‘ ( 𝐺 ‘ 𝑗 ) ) ) ⊆ ℝ
40 38 39 eqsstrdi ⊢ ( ( 𝜑 ∧ 𝑗 ∈ ( 1 ... 𝑀 ) ) → ( (,) ‘ ( 𝐺 ‘ 𝑗 ) ) ⊆ ℝ )
41 40 ralrimiva ⊢ ( 𝜑 → ∀ 𝑗 ∈ ( 1 ... 𝑀 ) ( (,) ‘ ( 𝐺 ‘ 𝑗 ) ) ⊆ ℝ )
42 iunss ⊢ ( ∪ 𝑗 ∈ ( 1 ... 𝑀 ) ( (,) ‘ ( 𝐺 ‘ 𝑗 ) ) ⊆ ℝ ↔ ∀ 𝑗 ∈ ( 1 ... 𝑀 ) ( (,) ‘ ( 𝐺 ‘ 𝑗 ) ) ⊆ ℝ )
43 41 42 sylibr ⊢ ( 𝜑 → ∪ 𝑗 ∈ ( 1 ... 𝑀 ) ( (,) ‘ ( 𝐺 ‘ 𝑗 ) ) ⊆ ℝ )
44 30 43 eqsstrd ⊢ ( 𝜑 → 𝐾 ⊆ ℝ )
45 fzfid ⊢ ( 𝜑 → ( 1 ... 𝑀 ) ∈ Fin )
46 38 fveq2d ⊢ ( ( 𝜑 ∧ 𝑗 ∈ ( 1 ... 𝑀 ) ) → ( vol* ‘ ( (,) ‘ ( 𝐺 ‘ 𝑗 ) ) ) = ( vol* ‘ ( ( 1st ‘ ( 𝐺 ‘ 𝑗 ) ) (,) ( 2nd ‘ ( 𝐺 ‘ 𝑗 ) ) ) ) )
47 ovolfcl ⊢ ( ( 𝐺 : ℕ ⟶ ( ≤ ∩ ( ℝ × ℝ ) ) ∧ 𝑗 ∈ ℕ ) → ( ( 1st ‘ ( 𝐺 ‘ 𝑗 ) ) ∈ ℝ ∧ ( 2nd ‘ ( 𝐺 ‘ 𝑗 ) ) ∈ ℝ ∧ ( 1st ‘ ( 𝐺 ‘ 𝑗 ) ) ≤ ( 2nd ‘ ( 𝐺 ‘ 𝑗 ) ) ) )
48 7 25 47 syl2an ⊢ ( ( 𝜑 ∧ 𝑗 ∈ ( 1 ... 𝑀 ) ) → ( ( 1st ‘ ( 𝐺 ‘ 𝑗 ) ) ∈ ℝ ∧ ( 2nd ‘ ( 𝐺 ‘ 𝑗 ) ) ∈ ℝ ∧ ( 1st ‘ ( 𝐺 ‘ 𝑗 ) ) ≤ ( 2nd ‘ ( 𝐺 ‘ 𝑗 ) ) ) )
49 ovolioo ⊢ ( ( ( 1st ‘ ( 𝐺 ‘ 𝑗 ) ) ∈ ℝ ∧ ( 2nd ‘ ( 𝐺 ‘ 𝑗 ) ) ∈ ℝ ∧ ( 1st ‘ ( 𝐺 ‘ 𝑗 ) ) ≤ ( 2nd ‘ ( 𝐺 ‘ 𝑗 ) ) ) → ( vol* ‘ ( ( 1st ‘ ( 𝐺 ‘ 𝑗 ) ) (,) ( 2nd ‘ ( 𝐺 ‘ 𝑗 ) ) ) ) = ( ( 2nd ‘ ( 𝐺 ‘ 𝑗 ) ) − ( 1st ‘ ( 𝐺 ‘ 𝑗 ) ) ) )
50 48 49 syl ⊢ ( ( 𝜑 ∧ 𝑗 ∈ ( 1 ... 𝑀 ) ) → ( vol* ‘ ( ( 1st ‘ ( 𝐺 ‘ 𝑗 ) ) (,) ( 2nd ‘ ( 𝐺 ‘ 𝑗 ) ) ) ) = ( ( 2nd ‘ ( 𝐺 ‘ 𝑗 ) ) − ( 1st ‘ ( 𝐺 ‘ 𝑗 ) ) ) )
51 46 50 eqtrd ⊢ ( ( 𝜑 ∧ 𝑗 ∈ ( 1 ... 𝑀 ) ) → ( vol* ‘ ( (,) ‘ ( 𝐺 ‘ 𝑗 ) ) ) = ( ( 2nd ‘ ( 𝐺 ‘ 𝑗 ) ) − ( 1st ‘ ( 𝐺 ‘ 𝑗 ) ) ) )
52 48 simp2d ⊢ ( ( 𝜑 ∧ 𝑗 ∈ ( 1 ... 𝑀 ) ) → ( 2nd ‘ ( 𝐺 ‘ 𝑗 ) ) ∈ ℝ )
53 48 simp1d ⊢ ( ( 𝜑 ∧ 𝑗 ∈ ( 1 ... 𝑀 ) ) → ( 1st ‘ ( 𝐺 ‘ 𝑗 ) ) ∈ ℝ )
54 52 53 resubcld ⊢ ( ( 𝜑 ∧ 𝑗 ∈ ( 1 ... 𝑀 ) ) → ( ( 2nd ‘ ( 𝐺 ‘ 𝑗 ) ) − ( 1st ‘ ( 𝐺 ‘ 𝑗 ) ) ) ∈ ℝ )
55 51 54 eqeltrd ⊢ ( ( 𝜑 ∧ 𝑗 ∈ ( 1 ... 𝑀 ) ) → ( vol* ‘ ( (,) ‘ ( 𝐺 ‘ 𝑗 ) ) ) ∈ ℝ )
56 45 55 fsumrecl ⊢ ( 𝜑 → Σ 𝑗 ∈ ( 1 ... 𝑀 ) ( vol* ‘ ( (,) ‘ ( 𝐺 ‘ 𝑗 ) ) ) ∈ ℝ )
57 30 fveq2d ⊢ ( 𝜑 → ( vol* ‘ 𝐾 ) = ( vol* ‘ ∪ 𝑗 ∈ ( 1 ... 𝑀 ) ( (,) ‘ ( 𝐺 ‘ 𝑗 ) ) ) )
58 40 55 jca ⊢ ( ( 𝜑 ∧ 𝑗 ∈ ( 1 ... 𝑀 ) ) → ( ( (,) ‘ ( 𝐺 ‘ 𝑗 ) ) ⊆ ℝ ∧ ( vol* ‘ ( (,) ‘ ( 𝐺 ‘ 𝑗 ) ) ) ∈ ℝ ) )
59 58 ralrimiva ⊢ ( 𝜑 → ∀ 𝑗 ∈ ( 1 ... 𝑀 ) ( ( (,) ‘ ( 𝐺 ‘ 𝑗 ) ) ⊆ ℝ ∧ ( vol* ‘ ( (,) ‘ ( 𝐺 ‘ 𝑗 ) ) ) ∈ ℝ ) )
60 ovolfiniun ⊢ ( ( ( 1 ... 𝑀 ) ∈ Fin ∧ ∀ 𝑗 ∈ ( 1 ... 𝑀 ) ( ( (,) ‘ ( 𝐺 ‘ 𝑗 ) ) ⊆ ℝ ∧ ( vol* ‘ ( (,) ‘ ( 𝐺 ‘ 𝑗 ) ) ) ∈ ℝ ) ) → ( vol* ‘ ∪ 𝑗 ∈ ( 1 ... 𝑀 ) ( (,) ‘ ( 𝐺 ‘ 𝑗 ) ) ) ≤ Σ 𝑗 ∈ ( 1 ... 𝑀 ) ( vol* ‘ ( (,) ‘ ( 𝐺 ‘ 𝑗 ) ) ) )
61 45 59 60 syl2anc ⊢ ( 𝜑 → ( vol* ‘ ∪ 𝑗 ∈ ( 1 ... 𝑀 ) ( (,) ‘ ( 𝐺 ‘ 𝑗 ) ) ) ≤ Σ 𝑗 ∈ ( 1 ... 𝑀 ) ( vol* ‘ ( (,) ‘ ( 𝐺 ‘ 𝑗 ) ) ) )
62 57 61 eqbrtrd ⊢ ( 𝜑 → ( vol* ‘ 𝐾 ) ≤ Σ 𝑗 ∈ ( 1 ... 𝑀 ) ( vol* ‘ ( (,) ‘ ( 𝐺 ‘ 𝑗 ) ) ) )
63 ovollecl ⊢ ( ( 𝐾 ⊆ ℝ ∧ Σ 𝑗 ∈ ( 1 ... 𝑀 ) ( vol* ‘ ( (,) ‘ ( 𝐺 ‘ 𝑗 ) ) ) ∈ ℝ ∧ ( vol* ‘ 𝐾 ) ≤ Σ 𝑗 ∈ ( 1 ... 𝑀 ) ( vol* ‘ ( (,) ‘ ( 𝐺 ‘ 𝑗 ) ) ) ) → ( vol* ‘ 𝐾 ) ∈ ℝ )
64 44 56 62 63 syl3anc ⊢ ( 𝜑 → ( vol* ‘ 𝐾 ) ∈ ℝ )
65 30 64 jca ⊢ ( 𝜑 → ( 𝐾 = ∪ 𝑗 ∈ ( 1 ... 𝑀 ) ( (,) ‘ ( 𝐺 ‘ 𝑗 ) ) ∧ ( vol* ‘ 𝐾 ) ∈ ℝ ) )