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

Metamath Proof Explorer

Theorem ovolicc2lem1

Description: Lemma for ovolicc2 . (Contributed by Mario Carneiro, 14-Jun-2014)

Ref Expression
Hypotheses ovolicc.1 ⊢ ( 𝜑 → 𝐴 ∈ ℝ )
ovolicc.2 ⊢ ( 𝜑 → 𝐵 ∈ ℝ )
ovolicc.3 ⊢ ( 𝜑 → 𝐴 ≤ 𝐵 )
ovolicc2.4 ⊢ 𝑆 = seq 1 ( + , ( ( abs ∘ − ) ∘ 𝐹 ) )
ovolicc2.5 ⊢ ( 𝜑 → 𝐹 : ℕ ⟶ ( ≤ ∩ ( ℝ × ℝ ) ) )
ovolicc2.6 ⊢ ( 𝜑 → 𝑈 ∈ ( 𝒫 ran ( (,) ∘ 𝐹 ) ∩ Fin ) )
ovolicc2.7 ⊢ ( 𝜑 → ( 𝐴 [,] 𝐵 ) ⊆ ∪ 𝑈 )
ovolicc2.8 ⊢ ( 𝜑 → 𝐺 : 𝑈 ⟶ ℕ )
ovolicc2.9 ⊢ ( ( 𝜑 ∧ 𝑡 ∈ 𝑈 ) → ( ( (,) ∘ 𝐹 ) ‘ ( 𝐺 ‘ 𝑡 ) ) = 𝑡 )
Assertion ovolicc2lem1 ( ( 𝜑 ∧ 𝑋 ∈ 𝑈 ) → ( 𝑃 ∈ 𝑋 ↔ ( 𝑃 ∈ ℝ ∧ ( 1st ‘ ( 𝐹 ‘ ( 𝐺 ‘ 𝑋 ) ) ) < 𝑃 ∧ 𝑃 < ( 2nd ‘ ( 𝐹 ‘ ( 𝐺 ‘ 𝑋 ) ) ) ) ) )

Proof

Step Hyp Ref Expression
1 ovolicc.1 ⊢ ( 𝜑 → 𝐴 ∈ ℝ )
2 ovolicc.2 ⊢ ( 𝜑 → 𝐵 ∈ ℝ )
3 ovolicc.3 ⊢ ( 𝜑 → 𝐴 ≤ 𝐵 )
4 ovolicc2.4 ⊢ 𝑆 = seq 1 ( + , ( ( abs ∘ − ) ∘ 𝐹 ) )
5 ovolicc2.5 ⊢ ( 𝜑 → 𝐹 : ℕ ⟶ ( ≤ ∩ ( ℝ × ℝ ) ) )
6 ovolicc2.6 ⊢ ( 𝜑 → 𝑈 ∈ ( 𝒫 ran ( (,) ∘ 𝐹 ) ∩ Fin ) )
7 ovolicc2.7 ⊢ ( 𝜑 → ( 𝐴 [,] 𝐵 ) ⊆ ∪ 𝑈 )
8 ovolicc2.8 ⊢ ( 𝜑 → 𝐺 : 𝑈 ⟶ ℕ )
9 ovolicc2.9 ⊢ ( ( 𝜑 ∧ 𝑡 ∈ 𝑈 ) → ( ( (,) ∘ 𝐹 ) ‘ ( 𝐺 ‘ 𝑡 ) ) = 𝑡 )
10 inss2 ⊢ ( ≤ ∩ ( ℝ × ℝ ) ) ⊆ ( ℝ × ℝ )
11 fss ⊢ ( ( 𝐹 : ℕ ⟶ ( ≤ ∩ ( ℝ × ℝ ) ) ∧ ( ≤ ∩ ( ℝ × ℝ ) ) ⊆ ( ℝ × ℝ ) ) → 𝐹 : ℕ ⟶ ( ℝ × ℝ ) )
12 5 10 11 sylancl ⊢ ( 𝜑 → 𝐹 : ℕ ⟶ ( ℝ × ℝ ) )
13 8 ffvelcdmda ⊢ ( ( 𝜑 ∧ 𝑋 ∈ 𝑈 ) → ( 𝐺 ‘ 𝑋 ) ∈ ℕ )
14 fvco3 ⊢ ( ( 𝐹 : ℕ ⟶ ( ℝ × ℝ ) ∧ ( 𝐺 ‘ 𝑋 ) ∈ ℕ ) → ( ( (,) ∘ 𝐹 ) ‘ ( 𝐺 ‘ 𝑋 ) ) = ( (,) ‘ ( 𝐹 ‘ ( 𝐺 ‘ 𝑋 ) ) ) )
15 12 13 14 syl2an2r ⊢ ( ( 𝜑 ∧ 𝑋 ∈ 𝑈 ) → ( ( (,) ∘ 𝐹 ) ‘ ( 𝐺 ‘ 𝑋 ) ) = ( (,) ‘ ( 𝐹 ‘ ( 𝐺 ‘ 𝑋 ) ) ) )
16 9 ralrimiva ⊢ ( 𝜑 → ∀ 𝑡 ∈ 𝑈 ( ( (,) ∘ 𝐹 ) ‘ ( 𝐺 ‘ 𝑡 ) ) = 𝑡 )
17 2fveq3 ⊢ ( 𝑡 = 𝑋 → ( ( (,) ∘ 𝐹 ) ‘ ( 𝐺 ‘ 𝑡 ) ) = ( ( (,) ∘ 𝐹 ) ‘ ( 𝐺 ‘ 𝑋 ) ) )
18 id ⊢ ( 𝑡 = 𝑋 → 𝑡 = 𝑋 )
19 17 18 eqeq12d ⊢ ( 𝑡 = 𝑋 → ( ( ( (,) ∘ 𝐹 ) ‘ ( 𝐺 ‘ 𝑡 ) ) = 𝑡 ↔ ( ( (,) ∘ 𝐹 ) ‘ ( 𝐺 ‘ 𝑋 ) ) = 𝑋 ) )
20 19 rspccva ⊢ ( ( ∀ 𝑡 ∈ 𝑈 ( ( (,) ∘ 𝐹 ) ‘ ( 𝐺 ‘ 𝑡 ) ) = 𝑡 ∧ 𝑋 ∈ 𝑈 ) → ( ( (,) ∘ 𝐹 ) ‘ ( 𝐺 ‘ 𝑋 ) ) = 𝑋 )
21 16 20 sylan ⊢ ( ( 𝜑 ∧ 𝑋 ∈ 𝑈 ) → ( ( (,) ∘ 𝐹 ) ‘ ( 𝐺 ‘ 𝑋 ) ) = 𝑋 )
22 12 adantr ⊢ ( ( 𝜑 ∧ 𝑋 ∈ 𝑈 ) → 𝐹 : ℕ ⟶ ( ℝ × ℝ ) )
23 22 13 ffvelcdmd ⊢ ( ( 𝜑 ∧ 𝑋 ∈ 𝑈 ) → ( 𝐹 ‘ ( 𝐺 ‘ 𝑋 ) ) ∈ ( ℝ × ℝ ) )
24 1st2nd2 ⊢ ( ( 𝐹 ‘ ( 𝐺 ‘ 𝑋 ) ) ∈ ( ℝ × ℝ ) → ( 𝐹 ‘ ( 𝐺 ‘ 𝑋 ) ) = ⟨ ( 1st ‘ ( 𝐹 ‘ ( 𝐺 ‘ 𝑋 ) ) ) , ( 2nd ‘ ( 𝐹 ‘ ( 𝐺 ‘ 𝑋 ) ) ) ⟩ )
25 23 24 syl ⊢ ( ( 𝜑 ∧ 𝑋 ∈ 𝑈 ) → ( 𝐹 ‘ ( 𝐺 ‘ 𝑋 ) ) = ⟨ ( 1st ‘ ( 𝐹 ‘ ( 𝐺 ‘ 𝑋 ) ) ) , ( 2nd ‘ ( 𝐹 ‘ ( 𝐺 ‘ 𝑋 ) ) ) ⟩ )
26 25 fveq2d ⊢ ( ( 𝜑 ∧ 𝑋 ∈ 𝑈 ) → ( (,) ‘ ( 𝐹 ‘ ( 𝐺 ‘ 𝑋 ) ) ) = ( (,) ‘ ⟨ ( 1st ‘ ( 𝐹 ‘ ( 𝐺 ‘ 𝑋 ) ) ) , ( 2nd ‘ ( 𝐹 ‘ ( 𝐺 ‘ 𝑋 ) ) ) ⟩ ) )
27 df-ov ⊢ ( ( 1st ‘ ( 𝐹 ‘ ( 𝐺 ‘ 𝑋 ) ) ) (,) ( 2nd ‘ ( 𝐹 ‘ ( 𝐺 ‘ 𝑋 ) ) ) ) = ( (,) ‘ ⟨ ( 1st ‘ ( 𝐹 ‘ ( 𝐺 ‘ 𝑋 ) ) ) , ( 2nd ‘ ( 𝐹 ‘ ( 𝐺 ‘ 𝑋 ) ) ) ⟩ )
28 26 27 eqtr4di ⊢ ( ( 𝜑 ∧ 𝑋 ∈ 𝑈 ) → ( (,) ‘ ( 𝐹 ‘ ( 𝐺 ‘ 𝑋 ) ) ) = ( ( 1st ‘ ( 𝐹 ‘ ( 𝐺 ‘ 𝑋 ) ) ) (,) ( 2nd ‘ ( 𝐹 ‘ ( 𝐺 ‘ 𝑋 ) ) ) ) )
29 15 21 28 3eqtr3d ⊢ ( ( 𝜑 ∧ 𝑋 ∈ 𝑈 ) → 𝑋 = ( ( 1st ‘ ( 𝐹 ‘ ( 𝐺 ‘ 𝑋 ) ) ) (,) ( 2nd ‘ ( 𝐹 ‘ ( 𝐺 ‘ 𝑋 ) ) ) ) )
30 29 eleq2d ⊢ ( ( 𝜑 ∧ 𝑋 ∈ 𝑈 ) → ( 𝑃 ∈ 𝑋 ↔ 𝑃 ∈ ( ( 1st ‘ ( 𝐹 ‘ ( 𝐺 ‘ 𝑋 ) ) ) (,) ( 2nd ‘ ( 𝐹 ‘ ( 𝐺 ‘ 𝑋 ) ) ) ) ) )
31 xp1st ⊢ ( ( 𝐹 ‘ ( 𝐺 ‘ 𝑋 ) ) ∈ ( ℝ × ℝ ) → ( 1st ‘ ( 𝐹 ‘ ( 𝐺 ‘ 𝑋 ) ) ) ∈ ℝ )
32 23 31 syl ⊢ ( ( 𝜑 ∧ 𝑋 ∈ 𝑈 ) → ( 1st ‘ ( 𝐹 ‘ ( 𝐺 ‘ 𝑋 ) ) ) ∈ ℝ )
33 xp2nd ⊢ ( ( 𝐹 ‘ ( 𝐺 ‘ 𝑋 ) ) ∈ ( ℝ × ℝ ) → ( 2nd ‘ ( 𝐹 ‘ ( 𝐺 ‘ 𝑋 ) ) ) ∈ ℝ )
34 23 33 syl ⊢ ( ( 𝜑 ∧ 𝑋 ∈ 𝑈 ) → ( 2nd ‘ ( 𝐹 ‘ ( 𝐺 ‘ 𝑋 ) ) ) ∈ ℝ )
35 rexr ⊢ ( ( 1st ‘ ( 𝐹 ‘ ( 𝐺 ‘ 𝑋 ) ) ) ∈ ℝ → ( 1st ‘ ( 𝐹 ‘ ( 𝐺 ‘ 𝑋 ) ) ) ∈ ℝ* )
36 rexr ⊢ ( ( 2nd ‘ ( 𝐹 ‘ ( 𝐺 ‘ 𝑋 ) ) ) ∈ ℝ → ( 2nd ‘ ( 𝐹 ‘ ( 𝐺 ‘ 𝑋 ) ) ) ∈ ℝ* )
37 elioo2 ⊢ ( ( ( 1st ‘ ( 𝐹 ‘ ( 𝐺 ‘ 𝑋 ) ) ) ∈ ℝ* ∧ ( 2nd ‘ ( 𝐹 ‘ ( 𝐺 ‘ 𝑋 ) ) ) ∈ ℝ* ) → ( 𝑃 ∈ ( ( 1st ‘ ( 𝐹 ‘ ( 𝐺 ‘ 𝑋 ) ) ) (,) ( 2nd ‘ ( 𝐹 ‘ ( 𝐺 ‘ 𝑋 ) ) ) ) ↔ ( 𝑃 ∈ ℝ ∧ ( 1st ‘ ( 𝐹 ‘ ( 𝐺 ‘ 𝑋 ) ) ) < 𝑃 ∧ 𝑃 < ( 2nd ‘ ( 𝐹 ‘ ( 𝐺 ‘ 𝑋 ) ) ) ) ) )
38 35 36 37 syl2an ⊢ ( ( ( 1st ‘ ( 𝐹 ‘ ( 𝐺 ‘ 𝑋 ) ) ) ∈ ℝ ∧ ( 2nd ‘ ( 𝐹 ‘ ( 𝐺 ‘ 𝑋 ) ) ) ∈ ℝ ) → ( 𝑃 ∈ ( ( 1st ‘ ( 𝐹 ‘ ( 𝐺 ‘ 𝑋 ) ) ) (,) ( 2nd ‘ ( 𝐹 ‘ ( 𝐺 ‘ 𝑋 ) ) ) ) ↔ ( 𝑃 ∈ ℝ ∧ ( 1st ‘ ( 𝐹 ‘ ( 𝐺 ‘ 𝑋 ) ) ) < 𝑃 ∧ 𝑃 < ( 2nd ‘ ( 𝐹 ‘ ( 𝐺 ‘ 𝑋 ) ) ) ) ) )
39 32 34 38 syl2anc ⊢ ( ( 𝜑 ∧ 𝑋 ∈ 𝑈 ) → ( 𝑃 ∈ ( ( 1st ‘ ( 𝐹 ‘ ( 𝐺 ‘ 𝑋 ) ) ) (,) ( 2nd ‘ ( 𝐹 ‘ ( 𝐺 ‘ 𝑋 ) ) ) ) ↔ ( 𝑃 ∈ ℝ ∧ ( 1st ‘ ( 𝐹 ‘ ( 𝐺 ‘ 𝑋 ) ) ) < 𝑃 ∧ 𝑃 < ( 2nd ‘ ( 𝐹 ‘ ( 𝐺 ‘ 𝑋 ) ) ) ) ) )
40 30 39 bitrd ⊢ ( ( 𝜑 ∧ 𝑋 ∈ 𝑈 ) → ( 𝑃 ∈ 𝑋 ↔ ( 𝑃 ∈ ℝ ∧ ( 1st ‘ ( 𝐹 ‘ ( 𝐺 ‘ 𝑋 ) ) ) < 𝑃 ∧ 𝑃 < ( 2nd ‘ ( 𝐹 ‘ ( 𝐺 ‘ 𝑋 ) ) ) ) ) )