Metamath Proof Explorer

Theorem uniioombllem2a

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

Ref Expression
Hypotheses uniioombl.1 ⊢ φ → F : ℕ ⟶ ≤ ∩ ℝ 2
uniioombl.2 ⊢ φ → Disj x ∈ ℕ . ⁡ F ⁡ x
uniioombl.3 ⊢ S = seq 1 + abs ∘ − ∘ F
uniioombl.a ⊢ A = ⋃ ran ⁡ . ∘ F
uniioombl.e ⊢ φ → vol * ⁡ E ∈ ℝ
uniioombl.c ⊢ φ → C ∈ ℝ +
uniioombl.g ⊢ φ → G : ℕ ⟶ ≤ ∩ ℝ 2
uniioombl.s ⊢ φ → E ⊆ ⋃ ran ⁡ . ∘ G
uniioombl.t ⊢ T = seq 1 + abs ∘ − ∘ G
uniioombl.v ⊢ φ → sup ran ⁡ T ℝ * < ≤ vol * ⁡ E + C
Assertion uniioombllem2a ⊢ φ ∧ J ∈ ℕ ∧ z ∈ ℕ → . ⁡ F ⁡ z ∩ . ⁡ G ⁡ J ∈ ran ⁡ .

Proof

Step Hyp Ref Expression
1 uniioombl.1 ⊢ φ → F : ℕ ⟶ ≤ ∩ ℝ 2
2 uniioombl.2 ⊢ φ → Disj x ∈ ℕ . ⁡ F ⁡ x
3 uniioombl.3 ⊢ S = seq 1 + abs ∘ − ∘ F
4 uniioombl.a ⊢ A = ⋃ ran ⁡ . ∘ F
5 uniioombl.e ⊢ φ → vol * ⁡ E ∈ ℝ
6 uniioombl.c ⊢ φ → C ∈ ℝ +
7 uniioombl.g ⊢ φ → G : ℕ ⟶ ≤ ∩ ℝ 2
8 uniioombl.s ⊢ φ → E ⊆ ⋃ ran ⁡ . ∘ G
9 uniioombl.t ⊢ T = seq 1 + abs ∘ − ∘ G
10 uniioombl.v ⊢ φ → sup ran ⁡ T ℝ * < ≤ vol * ⁡ E + C
11 1 adantr ⊢ φ ∧ J ∈ ℕ → F : ℕ ⟶ ≤ ∩ ℝ 2
12 11 ffvelrnda ⊢ φ ∧ J ∈ ℕ ∧ z ∈ ℕ → F ⁡ z ∈ ≤ ∩ ℝ 2
13 12 elin2d ⊢ φ ∧ J ∈ ℕ ∧ z ∈ ℕ → F ⁡ z ∈ ℝ 2
14 1st2nd2 ⊢ F ⁡ z ∈ ℝ 2 → F ⁡ z = 1 st ⁡ F ⁡ z 2 nd ⁡ F ⁡ z
15 13 14 syl ⊢ φ ∧ J ∈ ℕ ∧ z ∈ ℕ → F ⁡ z = 1 st ⁡ F ⁡ z 2 nd ⁡ F ⁡ z
16 15 fveq2d ⊢ φ ∧ J ∈ ℕ ∧ z ∈ ℕ → . ⁡ F ⁡ z = . ⁡ 1 st ⁡ F ⁡ z 2 nd ⁡ F ⁡ z
17 df-ov ⊢ 1 st ⁡ F ⁡ z 2 nd ⁡ F ⁡ z = . ⁡ 1 st ⁡ F ⁡ z 2 nd ⁡ F ⁡ z
18 16 17 eqtr4di ⊢ φ ∧ J ∈ ℕ ∧ z ∈ ℕ → . ⁡ F ⁡ z = 1 st ⁡ F ⁡ z 2 nd ⁡ F ⁡ z
19 7 ffvelrnda ⊢ φ ∧ J ∈ ℕ → G ⁡ J ∈ ≤ ∩ ℝ 2
20 19 elin2d ⊢ φ ∧ J ∈ ℕ → G ⁡ J ∈ ℝ 2
21 1st2nd2 ⊢ G ⁡ J ∈ ℝ 2 → G ⁡ J = 1 st ⁡ G ⁡ J 2 nd ⁡ G ⁡ J
22 20 21 syl ⊢ φ ∧ J ∈ ℕ → G ⁡ J = 1 st ⁡ G ⁡ J 2 nd ⁡ G ⁡ J
23 22 fveq2d ⊢ φ ∧ J ∈ ℕ → . ⁡ G ⁡ J = . ⁡ 1 st ⁡ G ⁡ J 2 nd ⁡ G ⁡ J
24 df-ov ⊢ 1 st ⁡ G ⁡ J 2 nd ⁡ G ⁡ J = . ⁡ 1 st ⁡ G ⁡ J 2 nd ⁡ G ⁡ J
25 23 24 eqtr4di ⊢ φ ∧ J ∈ ℕ → . ⁡ G ⁡ J = 1 st ⁡ G ⁡ J 2 nd ⁡ G ⁡ J
26 25 adantr ⊢ φ ∧ J ∈ ℕ ∧ z ∈ ℕ → . ⁡ G ⁡ J = 1 st ⁡ G ⁡ J 2 nd ⁡ G ⁡ J
27 18 26 ineq12d ⊢ φ ∧ J ∈ ℕ ∧ z ∈ ℕ → . ⁡ F ⁡ z ∩ . ⁡ G ⁡ J = 1 st ⁡ F ⁡ z 2 nd ⁡ F ⁡ z ∩ 1 st ⁡ G ⁡ J 2 nd ⁡ G ⁡ J
28 ovolfcl ⊢ F : ℕ ⟶ ≤ ∩ ℝ 2 ∧ z ∈ ℕ → 1 st ⁡ F ⁡ z ∈ ℝ ∧ 2 nd ⁡ F ⁡ z ∈ ℝ ∧ 1 st ⁡ F ⁡ z ≤ 2 nd ⁡ F ⁡ z
29 11 28 sylan ⊢ φ ∧ J ∈ ℕ ∧ z ∈ ℕ → 1 st ⁡ F ⁡ z ∈ ℝ ∧ 2 nd ⁡ F ⁡ z ∈ ℝ ∧ 1 st ⁡ F ⁡ z ≤ 2 nd ⁡ F ⁡ z
30 29 simp1d ⊢ φ ∧ J ∈ ℕ ∧ z ∈ ℕ → 1 st ⁡ F ⁡ z ∈ ℝ
31 30 rexrd ⊢ φ ∧ J ∈ ℕ ∧ z ∈ ℕ → 1 st ⁡ F ⁡ z ∈ ℝ *
32 29 simp2d ⊢ φ ∧ J ∈ ℕ ∧ z ∈ ℕ → 2 nd ⁡ F ⁡ z ∈ ℝ
33 32 rexrd ⊢ φ ∧ J ∈ ℕ ∧ z ∈ ℕ → 2 nd ⁡ F ⁡ z ∈ ℝ *
34 ovolfcl ⊢ G : ℕ ⟶ ≤ ∩ ℝ 2 ∧ J ∈ ℕ → 1 st ⁡ G ⁡ J ∈ ℝ ∧ 2 nd ⁡ G ⁡ J ∈ ℝ ∧ 1 st ⁡ G ⁡ J ≤ 2 nd ⁡ G ⁡ J
35 7 34 sylan ⊢ φ ∧ J ∈ ℕ → 1 st ⁡ G ⁡ J ∈ ℝ ∧ 2 nd ⁡ G ⁡ J ∈ ℝ ∧ 1 st ⁡ G ⁡ J ≤ 2 nd ⁡ G ⁡ J
36 35 simp1d ⊢ φ ∧ J ∈ ℕ → 1 st ⁡ G ⁡ J ∈ ℝ
37 36 rexrd ⊢ φ ∧ J ∈ ℕ → 1 st ⁡ G ⁡ J ∈ ℝ *
38 37 adantr ⊢ φ ∧ J ∈ ℕ ∧ z ∈ ℕ → 1 st ⁡ G ⁡ J ∈ ℝ *
39 35 simp2d ⊢ φ ∧ J ∈ ℕ → 2 nd ⁡ G ⁡ J ∈ ℝ
40 39 rexrd ⊢ φ ∧ J ∈ ℕ → 2 nd ⁡ G ⁡ J ∈ ℝ *
41 40 adantr ⊢ φ ∧ J ∈ ℕ ∧ z ∈ ℕ → 2 nd ⁡ G ⁡ J ∈ ℝ *
42 iooin ⊢ 1 st ⁡ F ⁡ z ∈ ℝ * ∧ 2 nd ⁡ F ⁡ z ∈ ℝ * ∧ 1 st ⁡ G ⁡ J ∈ ℝ * ∧ 2 nd ⁡ G ⁡ J ∈ ℝ * → 1 st ⁡ F ⁡ z 2 nd ⁡ F ⁡ z ∩ 1 st ⁡ G ⁡ J 2 nd ⁡ G ⁡ J = if 1 st ⁡ F ⁡ z ≤ 1 st ⁡ G ⁡ J 1 st ⁡ G ⁡ J 1 st ⁡ F ⁡ z if 2 nd ⁡ F ⁡ z ≤ 2 nd ⁡ G ⁡ J 2 nd ⁡ F ⁡ z 2 nd ⁡ G ⁡ J
43 31 33 38 41 42 syl22anc ⊢ φ ∧ J ∈ ℕ ∧ z ∈ ℕ → 1 st ⁡ F ⁡ z 2 nd ⁡ F ⁡ z ∩ 1 st ⁡ G ⁡ J 2 nd ⁡ G ⁡ J = if 1 st ⁡ F ⁡ z ≤ 1 st ⁡ G ⁡ J 1 st ⁡ G ⁡ J 1 st ⁡ F ⁡ z if 2 nd ⁡ F ⁡ z ≤ 2 nd ⁡ G ⁡ J 2 nd ⁡ F ⁡ z 2 nd ⁡ G ⁡ J
44 27 43 eqtrd ⊢ φ ∧ J ∈ ℕ ∧ z ∈ ℕ → . ⁡ F ⁡ z ∩ . ⁡ G ⁡ J = if 1 st ⁡ F ⁡ z ≤ 1 st ⁡ G ⁡ J 1 st ⁡ G ⁡ J 1 st ⁡ F ⁡ z if 2 nd ⁡ F ⁡ z ≤ 2 nd ⁡ G ⁡ J 2 nd ⁡ F ⁡ z 2 nd ⁡ G ⁡ J
45 ioorebas ⊢ if 1 st ⁡ F ⁡ z ≤ 1 st ⁡ G ⁡ J 1 st ⁡ G ⁡ J 1 st ⁡ F ⁡ z if 2 nd ⁡ F ⁡ z ≤ 2 nd ⁡ G ⁡ J 2 nd ⁡ F ⁡ z 2 nd ⁡ G ⁡ J ∈ ran ⁡ .
46 44 45 eqeltrdi ⊢ φ ∧ J ∈ ℕ ∧ z ∈ ℕ → . ⁡ F ⁡ z ∩ . ⁡ G ⁡ J ∈ ran ⁡ .