This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

Theorem uniioombllem2a

Description: Lemma for uniioombl . (Contributed by Mario Carneiro, 7-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* ‘ 𝐸 ) + 𝐶 ) )
Assertion uniioombllem2a ( ( ( 𝜑 ∧ 𝐽 ∈ ℕ ) ∧ 𝑧 ∈ ℕ ) → ( ( (,) ‘ ( 𝐹 ‘ 𝑧 ) ) ∩ ( (,) ‘ ( 𝐺 ‘ 𝐽 ) ) ) ∈ ran (,) )

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 1 adantr ⊢ ( ( 𝜑 ∧ 𝐽 ∈ ℕ ) → 𝐹 : ℕ ⟶ ( ≤ ∩ ( ℝ × ℝ ) ) )
12 11 ffvelcdmda ⊢ ( ( ( 𝜑 ∧ 𝐽 ∈ ℕ ) ∧ 𝑧 ∈ ℕ ) → ( 𝐹 ‘ 𝑧 ) ∈ ( ≤ ∩ ( ℝ × ℝ ) ) )
13 12 elin2d ⊢ ( ( ( 𝜑 ∧ 𝐽 ∈ ℕ ) ∧ 𝑧 ∈ ℕ ) → ( 𝐹 ‘ 𝑧 ) ∈ ( ℝ × ℝ ) )
14 1st2nd2 ⊢ ( ( 𝐹 ‘ 𝑧 ) ∈ ( ℝ × ℝ ) → ( 𝐹 ‘ 𝑧 ) = ⟨ ( 1st ‘ ( 𝐹 ‘ 𝑧 ) ) , ( 2nd ‘ ( 𝐹 ‘ 𝑧 ) ) ⟩ )
15 13 14 syl ⊢ ( ( ( 𝜑 ∧ 𝐽 ∈ ℕ ) ∧ 𝑧 ∈ ℕ ) → ( 𝐹 ‘ 𝑧 ) = ⟨ ( 1st ‘ ( 𝐹 ‘ 𝑧 ) ) , ( 2nd ‘ ( 𝐹 ‘ 𝑧 ) ) ⟩ )
16 15 fveq2d ⊢ ( ( ( 𝜑 ∧ 𝐽 ∈ ℕ ) ∧ 𝑧 ∈ ℕ ) → ( (,) ‘ ( 𝐹 ‘ 𝑧 ) ) = ( (,) ‘ ⟨ ( 1st ‘ ( 𝐹 ‘ 𝑧 ) ) , ( 2nd ‘ ( 𝐹 ‘ 𝑧 ) ) ⟩ ) )
17 df-ov ⊢ ( ( 1st ‘ ( 𝐹 ‘ 𝑧 ) ) (,) ( 2nd ‘ ( 𝐹 ‘ 𝑧 ) ) ) = ( (,) ‘ ⟨ ( 1st ‘ ( 𝐹 ‘ 𝑧 ) ) , ( 2nd ‘ ( 𝐹 ‘ 𝑧 ) ) ⟩ )
18 16 17 eqtr4di ⊢ ( ( ( 𝜑 ∧ 𝐽 ∈ ℕ ) ∧ 𝑧 ∈ ℕ ) → ( (,) ‘ ( 𝐹 ‘ 𝑧 ) ) = ( ( 1st ‘ ( 𝐹 ‘ 𝑧 ) ) (,) ( 2nd ‘ ( 𝐹 ‘ 𝑧 ) ) ) )
19 7 ffvelcdmda ⊢ ( ( 𝜑 ∧ 𝐽 ∈ ℕ ) → ( 𝐺 ‘ 𝐽 ) ∈ ( ≤ ∩ ( ℝ × ℝ ) ) )
20 19 elin2d ⊢ ( ( 𝜑 ∧ 𝐽 ∈ ℕ ) → ( 𝐺 ‘ 𝐽 ) ∈ ( ℝ × ℝ ) )
21 1st2nd2 ⊢ ( ( 𝐺 ‘ 𝐽 ) ∈ ( ℝ × ℝ ) → ( 𝐺 ‘ 𝐽 ) = ⟨ ( 1st ‘ ( 𝐺 ‘ 𝐽 ) ) , ( 2nd ‘ ( 𝐺 ‘ 𝐽 ) ) ⟩ )
22 20 21 syl ⊢ ( ( 𝜑 ∧ 𝐽 ∈ ℕ ) → ( 𝐺 ‘ 𝐽 ) = ⟨ ( 1st ‘ ( 𝐺 ‘ 𝐽 ) ) , ( 2nd ‘ ( 𝐺 ‘ 𝐽 ) ) ⟩ )
23 22 fveq2d ⊢ ( ( 𝜑 ∧ 𝐽 ∈ ℕ ) → ( (,) ‘ ( 𝐺 ‘ 𝐽 ) ) = ( (,) ‘ ⟨ ( 1st ‘ ( 𝐺 ‘ 𝐽 ) ) , ( 2nd ‘ ( 𝐺 ‘ 𝐽 ) ) ⟩ ) )
24 df-ov ⊢ ( ( 1st ‘ ( 𝐺 ‘ 𝐽 ) ) (,) ( 2nd ‘ ( 𝐺 ‘ 𝐽 ) ) ) = ( (,) ‘ ⟨ ( 1st ‘ ( 𝐺 ‘ 𝐽 ) ) , ( 2nd ‘ ( 𝐺 ‘ 𝐽 ) ) ⟩ )
25 23 24 eqtr4di ⊢ ( ( 𝜑 ∧ 𝐽 ∈ ℕ ) → ( (,) ‘ ( 𝐺 ‘ 𝐽 ) ) = ( ( 1st ‘ ( 𝐺 ‘ 𝐽 ) ) (,) ( 2nd ‘ ( 𝐺 ‘ 𝐽 ) ) ) )
26 25 adantr ⊢ ( ( ( 𝜑 ∧ 𝐽 ∈ ℕ ) ∧ 𝑧 ∈ ℕ ) → ( (,) ‘ ( 𝐺 ‘ 𝐽 ) ) = ( ( 1st ‘ ( 𝐺 ‘ 𝐽 ) ) (,) ( 2nd ‘ ( 𝐺 ‘ 𝐽 ) ) ) )
27 18 26 ineq12d ⊢ ( ( ( 𝜑 ∧ 𝐽 ∈ ℕ ) ∧ 𝑧 ∈ ℕ ) → ( ( (,) ‘ ( 𝐹 ‘ 𝑧 ) ) ∩ ( (,) ‘ ( 𝐺 ‘ 𝐽 ) ) ) = ( ( ( 1st ‘ ( 𝐹 ‘ 𝑧 ) ) (,) ( 2nd ‘ ( 𝐹 ‘ 𝑧 ) ) ) ∩ ( ( 1st ‘ ( 𝐺 ‘ 𝐽 ) ) (,) ( 2nd ‘ ( 𝐺 ‘ 𝐽 ) ) ) ) )
28 ovolfcl ⊢ ( ( 𝐹 : ℕ ⟶ ( ≤ ∩ ( ℝ × ℝ ) ) ∧ 𝑧 ∈ ℕ ) → ( ( 1st ‘ ( 𝐹 ‘ 𝑧 ) ) ∈ ℝ ∧ ( 2nd ‘ ( 𝐹 ‘ 𝑧 ) ) ∈ ℝ ∧ ( 1st ‘ ( 𝐹 ‘ 𝑧 ) ) ≤ ( 2nd ‘ ( 𝐹 ‘ 𝑧 ) ) ) )
29 11 28 sylan ⊢ ( ( ( 𝜑 ∧ 𝐽 ∈ ℕ ) ∧ 𝑧 ∈ ℕ ) → ( ( 1st ‘ ( 𝐹 ‘ 𝑧 ) ) ∈ ℝ ∧ ( 2nd ‘ ( 𝐹 ‘ 𝑧 ) ) ∈ ℝ ∧ ( 1st ‘ ( 𝐹 ‘ 𝑧 ) ) ≤ ( 2nd ‘ ( 𝐹 ‘ 𝑧 ) ) ) )
30 29 simp1d ⊢ ( ( ( 𝜑 ∧ 𝐽 ∈ ℕ ) ∧ 𝑧 ∈ ℕ ) → ( 1st ‘ ( 𝐹 ‘ 𝑧 ) ) ∈ ℝ )
31 30 rexrd ⊢ ( ( ( 𝜑 ∧ 𝐽 ∈ ℕ ) ∧ 𝑧 ∈ ℕ ) → ( 1st ‘ ( 𝐹 ‘ 𝑧 ) ) ∈ ℝ* )
32 29 simp2d ⊢ ( ( ( 𝜑 ∧ 𝐽 ∈ ℕ ) ∧ 𝑧 ∈ ℕ ) → ( 2nd ‘ ( 𝐹 ‘ 𝑧 ) ) ∈ ℝ )
33 32 rexrd ⊢ ( ( ( 𝜑 ∧ 𝐽 ∈ ℕ ) ∧ 𝑧 ∈ ℕ ) → ( 2nd ‘ ( 𝐹 ‘ 𝑧 ) ) ∈ ℝ* )
34 ovolfcl ⊢ ( ( 𝐺 : ℕ ⟶ ( ≤ ∩ ( ℝ × ℝ ) ) ∧ 𝐽 ∈ ℕ ) → ( ( 1st ‘ ( 𝐺 ‘ 𝐽 ) ) ∈ ℝ ∧ ( 2nd ‘ ( 𝐺 ‘ 𝐽 ) ) ∈ ℝ ∧ ( 1st ‘ ( 𝐺 ‘ 𝐽 ) ) ≤ ( 2nd ‘ ( 𝐺 ‘ 𝐽 ) ) ) )
35 7 34 sylan ⊢ ( ( 𝜑 ∧ 𝐽 ∈ ℕ ) → ( ( 1st ‘ ( 𝐺 ‘ 𝐽 ) ) ∈ ℝ ∧ ( 2nd ‘ ( 𝐺 ‘ 𝐽 ) ) ∈ ℝ ∧ ( 1st ‘ ( 𝐺 ‘ 𝐽 ) ) ≤ ( 2nd ‘ ( 𝐺 ‘ 𝐽 ) ) ) )
36 35 simp1d ⊢ ( ( 𝜑 ∧ 𝐽 ∈ ℕ ) → ( 1st ‘ ( 𝐺 ‘ 𝐽 ) ) ∈ ℝ )
37 36 rexrd ⊢ ( ( 𝜑 ∧ 𝐽 ∈ ℕ ) → ( 1st ‘ ( 𝐺 ‘ 𝐽 ) ) ∈ ℝ* )
38 37 adantr ⊢ ( ( ( 𝜑 ∧ 𝐽 ∈ ℕ ) ∧ 𝑧 ∈ ℕ ) → ( 1st ‘ ( 𝐺 ‘ 𝐽 ) ) ∈ ℝ* )
39 35 simp2d ⊢ ( ( 𝜑 ∧ 𝐽 ∈ ℕ ) → ( 2nd ‘ ( 𝐺 ‘ 𝐽 ) ) ∈ ℝ )
40 39 rexrd ⊢ ( ( 𝜑 ∧ 𝐽 ∈ ℕ ) → ( 2nd ‘ ( 𝐺 ‘ 𝐽 ) ) ∈ ℝ* )
41 40 adantr ⊢ ( ( ( 𝜑 ∧ 𝐽 ∈ ℕ ) ∧ 𝑧 ∈ ℕ ) → ( 2nd ‘ ( 𝐺 ‘ 𝐽 ) ) ∈ ℝ* )
42 iooin ⊢ ( ( ( ( 1st ‘ ( 𝐹 ‘ 𝑧 ) ) ∈ ℝ* ∧ ( 2nd ‘ ( 𝐹 ‘ 𝑧 ) ) ∈ ℝ* ) ∧ ( ( 1st ‘ ( 𝐺 ‘ 𝐽 ) ) ∈ ℝ* ∧ ( 2nd ‘ ( 𝐺 ‘ 𝐽 ) ) ∈ ℝ* ) ) → ( ( ( 1st ‘ ( 𝐹 ‘ 𝑧 ) ) (,) ( 2nd ‘ ( 𝐹 ‘ 𝑧 ) ) ) ∩ ( ( 1st ‘ ( 𝐺 ‘ 𝐽 ) ) (,) ( 2nd ‘ ( 𝐺 ‘ 𝐽 ) ) ) ) = ( if ( ( 1st ‘ ( 𝐹 ‘ 𝑧 ) ) ≤ ( 1st ‘ ( 𝐺 ‘ 𝐽 ) ) , ( 1st ‘ ( 𝐺 ‘ 𝐽 ) ) , ( 1st ‘ ( 𝐹 ‘ 𝑧 ) ) ) (,) if ( ( 2nd ‘ ( 𝐹 ‘ 𝑧 ) ) ≤ ( 2nd ‘ ( 𝐺 ‘ 𝐽 ) ) , ( 2nd ‘ ( 𝐹 ‘ 𝑧 ) ) , ( 2nd ‘ ( 𝐺 ‘ 𝐽 ) ) ) ) )
43 31 33 38 41 42 syl22anc ⊢ ( ( ( 𝜑 ∧ 𝐽 ∈ ℕ ) ∧ 𝑧 ∈ ℕ ) → ( ( ( 1st ‘ ( 𝐹 ‘ 𝑧 ) ) (,) ( 2nd ‘ ( 𝐹 ‘ 𝑧 ) ) ) ∩ ( ( 1st ‘ ( 𝐺 ‘ 𝐽 ) ) (,) ( 2nd ‘ ( 𝐺 ‘ 𝐽 ) ) ) ) = ( if ( ( 1st ‘ ( 𝐹 ‘ 𝑧 ) ) ≤ ( 1st ‘ ( 𝐺 ‘ 𝐽 ) ) , ( 1st ‘ ( 𝐺 ‘ 𝐽 ) ) , ( 1st ‘ ( 𝐹 ‘ 𝑧 ) ) ) (,) if ( ( 2nd ‘ ( 𝐹 ‘ 𝑧 ) ) ≤ ( 2nd ‘ ( 𝐺 ‘ 𝐽 ) ) , ( 2nd ‘ ( 𝐹 ‘ 𝑧 ) ) , ( 2nd ‘ ( 𝐺 ‘ 𝐽 ) ) ) ) )
44 27 43 eqtrd ⊢ ( ( ( 𝜑 ∧ 𝐽 ∈ ℕ ) ∧ 𝑧 ∈ ℕ ) → ( ( (,) ‘ ( 𝐹 ‘ 𝑧 ) ) ∩ ( (,) ‘ ( 𝐺 ‘ 𝐽 ) ) ) = ( if ( ( 1st ‘ ( 𝐹 ‘ 𝑧 ) ) ≤ ( 1st ‘ ( 𝐺 ‘ 𝐽 ) ) , ( 1st ‘ ( 𝐺 ‘ 𝐽 ) ) , ( 1st ‘ ( 𝐹 ‘ 𝑧 ) ) ) (,) if ( ( 2nd ‘ ( 𝐹 ‘ 𝑧 ) ) ≤ ( 2nd ‘ ( 𝐺 ‘ 𝐽 ) ) , ( 2nd ‘ ( 𝐹 ‘ 𝑧 ) ) , ( 2nd ‘ ( 𝐺 ‘ 𝐽 ) ) ) ) )
45 ioorebas ⊢ ( if ( ( 1st ‘ ( 𝐹 ‘ 𝑧 ) ) ≤ ( 1st ‘ ( 𝐺 ‘ 𝐽 ) ) , ( 1st ‘ ( 𝐺 ‘ 𝐽 ) ) , ( 1st ‘ ( 𝐹 ‘ 𝑧 ) ) ) (,) if ( ( 2nd ‘ ( 𝐹 ‘ 𝑧 ) ) ≤ ( 2nd ‘ ( 𝐺 ‘ 𝐽 ) ) , ( 2nd ‘ ( 𝐹 ‘ 𝑧 ) ) , ( 2nd ‘ ( 𝐺 ‘ 𝐽 ) ) ) ) ∈ ran (,)
46 44 45 eqeltrdi ⊢ ( ( ( 𝜑 ∧ 𝐽 ∈ ℕ ) ∧ 𝑧 ∈ ℕ ) → ( ( (,) ‘ ( 𝐹 ‘ 𝑧 ) ) ∩ ( (,) ‘ ( 𝐺 ‘ 𝐽 ) ) ) ∈ ran (,) )