Metamath Proof Explorer

Theorem ovolicc2lem1

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

Ref Expression
Hypotheses ovolicc.1 ⊢ φ → A ∈ ℝ
ovolicc.2 ⊢ φ → B ∈ ℝ
ovolicc.3 ⊢ φ → A ≤ B
ovolicc2.4 ⊢ S = seq 1 + abs ∘ − ∘ F
ovolicc2.5 ⊢ φ → F : ℕ ⟶ ≤ ∩ ℝ 2
ovolicc2.6 ⊢ φ → U ∈ 𝒫 ran ⁡ . ∘ F ∩ Fin
ovolicc2.7 ⊢ φ → A B ⊆ ⋃ U
ovolicc2.8 ⊢ φ → G : U ⟶ ℕ
ovolicc2.9 ⊢ φ ∧ t ∈ U → . ∘ F ⁡ G ⁡ t = t
Assertion ovolicc2lem1 ⊢ φ ∧ X ∈ U → P ∈ X ↔ P ∈ ℝ ∧ 1 st ⁡ F ⁡ G ⁡ X < P ∧ P < 2 nd ⁡ F ⁡ G ⁡ X

Proof

Step Hyp Ref Expression
1 ovolicc.1 ⊢ φ → A ∈ ℝ
2 ovolicc.2 ⊢ φ → B ∈ ℝ
3 ovolicc.3 ⊢ φ → A ≤ B
4 ovolicc2.4 ⊢ S = seq 1 + abs ∘ − ∘ F
5 ovolicc2.5 ⊢ φ → F : ℕ ⟶ ≤ ∩ ℝ 2
6 ovolicc2.6 ⊢ φ → U ∈ 𝒫 ran ⁡ . ∘ F ∩ Fin
7 ovolicc2.7 ⊢ φ → A B ⊆ ⋃ U
8 ovolicc2.8 ⊢ φ → G : U ⟶ ℕ
9 ovolicc2.9 ⊢ φ ∧ t ∈ U → . ∘ F ⁡ G ⁡ t = t
10 inss2 ⊢ ≤ ∩ ℝ 2 ⊆ ℝ 2
11 fss ⊢ F : ℕ ⟶ ≤ ∩ ℝ 2 ∧ ≤ ∩ ℝ 2 ⊆ ℝ 2 → F : ℕ ⟶ ℝ 2
12 5 10 11 sylancl ⊢ φ → F : ℕ ⟶ ℝ 2
13 8 ffvelrnda ⊢ φ ∧ X ∈ U → G ⁡ X ∈ ℕ
14 fvco3 ⊢ F : ℕ ⟶ ℝ 2 ∧ G ⁡ X ∈ ℕ → . ∘ F ⁡ G ⁡ X = . ⁡ F ⁡ G ⁡ X
15 12 13 14 syl2an2r ⊢ φ ∧ X ∈ U → . ∘ F ⁡ G ⁡ X = . ⁡ F ⁡ G ⁡ X
16 9 ralrimiva ⊢ φ → ∀ t ∈ U . ∘ F ⁡ G ⁡ t = t
17 2fveq3 ⊢ t = X → . ∘ F ⁡ G ⁡ t = . ∘ F ⁡ G ⁡ X
18 id ⊢ t = X → t = X
19 17 18 eqeq12d ⊢ t = X → . ∘ F ⁡ G ⁡ t = t ↔ . ∘ F ⁡ G ⁡ X = X
20 19 rspccva ⊢ ∀ t ∈ U . ∘ F ⁡ G ⁡ t = t ∧ X ∈ U → . ∘ F ⁡ G ⁡ X = X
21 16 20 sylan ⊢ φ ∧ X ∈ U → . ∘ F ⁡ G ⁡ X = X
22 12 adantr ⊢ φ ∧ X ∈ U → F : ℕ ⟶ ℝ 2
23 22 13 ffvelrnd ⊢ φ ∧ X ∈ U → F ⁡ G ⁡ X ∈ ℝ 2
24 1st2nd2 ⊢ F ⁡ G ⁡ X ∈ ℝ 2 → F ⁡ G ⁡ X = 1 st ⁡ F ⁡ G ⁡ X 2 nd ⁡ F ⁡ G ⁡ X
25 23 24 syl ⊢ φ ∧ X ∈ U → F ⁡ G ⁡ X = 1 st ⁡ F ⁡ G ⁡ X 2 nd ⁡ F ⁡ G ⁡ X
26 25 fveq2d ⊢ φ ∧ X ∈ U → . ⁡ F ⁡ G ⁡ X = . ⁡ 1 st ⁡ F ⁡ G ⁡ X 2 nd ⁡ F ⁡ G ⁡ X
27 df-ov ⊢ 1 st ⁡ F ⁡ G ⁡ X 2 nd ⁡ F ⁡ G ⁡ X = . ⁡ 1 st ⁡ F ⁡ G ⁡ X 2 nd ⁡ F ⁡ G ⁡ X
28 26 27 eqtr4di ⊢ φ ∧ X ∈ U → . ⁡ F ⁡ G ⁡ X = 1 st ⁡ F ⁡ G ⁡ X 2 nd ⁡ F ⁡ G ⁡ X
29 15 21 28 3eqtr3d ⊢ φ ∧ X ∈ U → X = 1 st ⁡ F ⁡ G ⁡ X 2 nd ⁡ F ⁡ G ⁡ X
30 29 eleq2d ⊢ φ ∧ X ∈ U → P ∈ X ↔ P ∈ 1 st ⁡ F ⁡ G ⁡ X 2 nd ⁡ F ⁡ G ⁡ X
31 xp1st ⊢ F ⁡ G ⁡ X ∈ ℝ 2 → 1 st ⁡ F ⁡ G ⁡ X ∈ ℝ
32 23 31 syl ⊢ φ ∧ X ∈ U → 1 st ⁡ F ⁡ G ⁡ X ∈ ℝ
33 xp2nd ⊢ F ⁡ G ⁡ X ∈ ℝ 2 → 2 nd ⁡ F ⁡ G ⁡ X ∈ ℝ
34 23 33 syl ⊢ φ ∧ X ∈ U → 2 nd ⁡ F ⁡ G ⁡ X ∈ ℝ
35 rexr ⊢ 1 st ⁡ F ⁡ G ⁡ X ∈ ℝ → 1 st ⁡ F ⁡ G ⁡ X ∈ ℝ *
36 rexr ⊢ 2 nd ⁡ F ⁡ G ⁡ X ∈ ℝ → 2 nd ⁡ F ⁡ G ⁡ X ∈ ℝ *
37 elioo2 ⊢ 1 st ⁡ F ⁡ G ⁡ X ∈ ℝ * ∧ 2 nd ⁡ F ⁡ G ⁡ X ∈ ℝ * → P ∈ 1 st ⁡ F ⁡ G ⁡ X 2 nd ⁡ F ⁡ G ⁡ X ↔ P ∈ ℝ ∧ 1 st ⁡ F ⁡ G ⁡ X < P ∧ P < 2 nd ⁡ F ⁡ G ⁡ X
38 35 36 37 syl2an ⊢ 1 st ⁡ F ⁡ G ⁡ X ∈ ℝ ∧ 2 nd ⁡ F ⁡ G ⁡ X ∈ ℝ → P ∈ 1 st ⁡ F ⁡ G ⁡ X 2 nd ⁡ F ⁡ G ⁡ X ↔ P ∈ ℝ ∧ 1 st ⁡ F ⁡ G ⁡ X < P ∧ P < 2 nd ⁡ F ⁡ G ⁡ X
39 32 34 38 syl2anc ⊢ φ ∧ X ∈ U → P ∈ 1 st ⁡ F ⁡ G ⁡ X 2 nd ⁡ F ⁡ G ⁡ X ↔ P ∈ ℝ ∧ 1 st ⁡ F ⁡ G ⁡ X < P ∧ P < 2 nd ⁡ F ⁡ G ⁡ X
40 30 39 bitrd ⊢ φ ∧ X ∈ U → P ∈ X ↔ P ∈ ℝ ∧ 1 st ⁡ F ⁡ G ⁡ X < P ∧ P < 2 nd ⁡ F ⁡ G ⁡ X