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=seq1+abs∘−∘F
ovolicc2.5 ⊢φ→F:ℕ⟶≤∩ℝ2
ovolicc2.6 ⊢φ→U∈𝒫ran⁡.∘F∩Fin
ovolicc2.7 ⊢φ→AB⊆⋃U
ovolicc2.8 ⊢φ→G:U⟶ℕ
ovolicc2.9 ⊢φ∧t∈U→.∘F⁡G⁡t=t
Assertion ovolicc2lem1 ⊢φ∧X∈U→P∈X↔P∈ℝ∧1st⁡F⁡G⁡X<P∧P<2nd⁡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=seq1+abs∘−∘F
5 ovolicc2.5 ⊢φ→F:ℕ⟶≤∩ℝ2
6 ovolicc2.6 ⊢φ→U∈𝒫ran⁡.∘F∩Fin
7 ovolicc2.7 ⊢φ→AB⊆⋃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 ffvelcdmda ⊢φ∧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 ffvelcdmd ⊢φ∧X∈U→F⁡G⁡X∈ℝ2
24 1st2nd2 ⊢F⁡G⁡X∈ℝ2→F⁡G⁡X=1st⁡F⁡G⁡X2nd⁡F⁡G⁡X
25 23 24 syl ⊢φ∧X∈U→F⁡G⁡X=1st⁡F⁡G⁡X2nd⁡F⁡G⁡X
26 25 fveq2d ⊢φ∧X∈U→.⁡F⁡G⁡X=.⁡1st⁡F⁡G⁡X2nd⁡F⁡G⁡X
27 df-ov ⊢1st⁡F⁡G⁡X2nd⁡F⁡G⁡X=.⁡1st⁡F⁡G⁡X2nd⁡F⁡G⁡X
28 26 27 eqtr4di ⊢φ∧X∈U→.⁡F⁡G⁡X=1st⁡F⁡G⁡X2nd⁡F⁡G⁡X
29 15 21 28 3eqtr3d ⊢φ∧X∈U→X=1st⁡F⁡G⁡X2nd⁡F⁡G⁡X
30 29 eleq2d ⊢φ∧X∈U→P∈X↔P∈1st⁡F⁡G⁡X2nd⁡F⁡G⁡X
31 xp1st ⊢F⁡G⁡X∈ℝ2→1st⁡F⁡G⁡X∈ℝ
32 23 31 syl ⊢φ∧X∈U→1st⁡F⁡G⁡X∈ℝ
33 xp2nd ⊢F⁡G⁡X∈ℝ2→2nd⁡F⁡G⁡X∈ℝ
34 23 33 syl ⊢φ∧X∈U→2nd⁡F⁡G⁡X∈ℝ
35 rexr ⊢1st⁡F⁡G⁡X∈ℝ→1st⁡F⁡G⁡X∈ℝ*
36 rexr ⊢2nd⁡F⁡G⁡X∈ℝ→2nd⁡F⁡G⁡X∈ℝ*
37 elioo2 ⊢1st⁡F⁡G⁡X∈ℝ*∧2nd⁡F⁡G⁡X∈ℝ*→P∈1st⁡F⁡G⁡X2nd⁡F⁡G⁡X↔P∈ℝ∧1st⁡F⁡G⁡X<P∧P<2nd⁡F⁡G⁡X
38 35 36 37 syl2an ⊢1st⁡F⁡G⁡X∈ℝ∧2nd⁡F⁡G⁡X∈ℝ→P∈1st⁡F⁡G⁡X2nd⁡F⁡G⁡X↔P∈ℝ∧1st⁡F⁡G⁡X<P∧P<2nd⁡F⁡G⁡X
39 32 34 38 syl2anc ⊢φ∧X∈U→P∈1st⁡F⁡G⁡X2nd⁡F⁡G⁡X↔P∈ℝ∧1st⁡F⁡G⁡X<P∧P<2nd⁡F⁡G⁡X
40 30 39 bitrd ⊢φ∧X∈U→P∈X↔P∈ℝ∧1st⁡F⁡G⁡X<P∧P<2nd⁡F⁡G⁡X