Metamath Proof Explorer

Theorem ovolicc2lem1

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

Ref Expression
Hypotheses ovolicc.1 
|- ( ph -> A e. RR )
ovolicc.2 
|- ( ph -> B e. RR )
ovolicc.3 
|- ( ph -> A <_ B )
ovolicc2.4 
|- S = seq 1 ( + , ( ( abs o. - ) o. F ) )
ovolicc2.5 
|- ( ph -> F : NN --> ( <_ i^i ( RR X. RR ) ) )
ovolicc2.6 
|- ( ph -> U e. ( ~P ran ( (,) o. F ) i^i Fin ) )
ovolicc2.7 
|- ( ph -> ( A [,] B ) C_ U. U )
ovolicc2.8 
|- ( ph -> G : U --> NN )
ovolicc2.9 
|- ( ( ph /\ t e. U ) -> ( ( (,) o. F ) ` ( G ` t ) ) = t )
Assertion ovolicc2lem1 
|- ( ( ph /\ X e. U ) -> ( P e. X <-> ( P e. RR /\ ( 1st ` ( F ` ( G ` X ) ) ) < P /\ P < ( 2nd ` ( F ` ( G ` X ) ) ) ) ) )

Proof

Step Hyp Ref Expression
1 ovolicc.1 
 |-  ( ph -> A e. RR )
2 ovolicc.2 
 |-  ( ph -> B e. RR )
3 ovolicc.3 
 |-  ( ph -> A <_ B )
4 ovolicc2.4 
 |-  S = seq 1 ( + , ( ( abs o. - ) o. F ) )
5 ovolicc2.5 
 |-  ( ph -> F : NN --> ( <_ i^i ( RR X. RR ) ) )
6 ovolicc2.6 
 |-  ( ph -> U e. ( ~P ran ( (,) o. F ) i^i Fin ) )
7 ovolicc2.7 
 |-  ( ph -> ( A [,] B ) C_ U. U )
8 ovolicc2.8 
 |-  ( ph -> G : U --> NN )
9 ovolicc2.9 
 |-  ( ( ph /\ t e. U ) -> ( ( (,) o. F ) ` ( G ` t ) ) = t )
10 inss2 
 |-  ( <_ i^i ( RR X. RR ) ) C_ ( RR X. RR )
11 fss 
 |-  ( ( F : NN --> ( <_ i^i ( RR X. RR ) ) /\ ( <_ i^i ( RR X. RR ) ) C_ ( RR X. RR ) ) -> F : NN --> ( RR X. RR ) )
12 5 10 11 sylancl 
 |-  ( ph -> F : NN --> ( RR X. RR ) )
13 8 ffvelrnda 
 |-  ( ( ph /\ X e. U ) -> ( G ` X ) e. NN )
14 fvco3 
 |-  ( ( F : NN --> ( RR X. RR ) /\ ( G ` X ) e. NN ) -> ( ( (,) o. F ) ` ( G ` X ) ) = ( (,) ` ( F ` ( G ` X ) ) ) )
15 12 13 14 syl2an2r 
 |-  ( ( ph /\ X e. U ) -> ( ( (,) o. F ) ` ( G ` X ) ) = ( (,) ` ( F ` ( G ` X ) ) ) )
16 9 ralrimiva 
 |-  ( ph -> A. t e. U ( ( (,) o. F ) ` ( G ` t ) ) = t )
17 2fveq3 
 |-  ( t = X -> ( ( (,) o. F ) ` ( G ` t ) ) = ( ( (,) o. F ) ` ( G ` X ) ) )
18 id 
 |-  ( t = X -> t = X )
19 17 18 eqeq12d 
 |-  ( t = X -> ( ( ( (,) o. F ) ` ( G ` t ) ) = t <-> ( ( (,) o. F ) ` ( G ` X ) ) = X ) )
20 19 rspccva 
 |-  ( ( A. t e. U ( ( (,) o. F ) ` ( G ` t ) ) = t /\ X e. U ) -> ( ( (,) o. F ) ` ( G ` X ) ) = X )
21 16 20 sylan 
 |-  ( ( ph /\ X e. U ) -> ( ( (,) o. F ) ` ( G ` X ) ) = X )
22 12 adantr 
 |-  ( ( ph /\ X e. U ) -> F : NN --> ( RR X. RR ) )
23 22 13 ffvelrnd 
 |-  ( ( ph /\ X e. U ) -> ( F ` ( G ` X ) ) e. ( RR X. RR ) )
24 1st2nd2 
 |-  ( ( F ` ( G ` X ) ) e. ( RR X. RR ) -> ( F ` ( G ` X ) ) = <. ( 1st ` ( F ` ( G ` X ) ) ) , ( 2nd ` ( F ` ( G ` X ) ) ) >. )
25 23 24 syl 
 |-  ( ( ph /\ X e. U ) -> ( F ` ( G ` X ) ) = <. ( 1st ` ( F ` ( G ` X ) ) ) , ( 2nd ` ( F ` ( G ` X ) ) ) >. )
26 25 fveq2d 
 |-  ( ( ph /\ X e. U ) -> ( (,) ` ( F ` ( G ` X ) ) ) = ( (,) ` <. ( 1st ` ( F ` ( G ` X ) ) ) , ( 2nd ` ( F ` ( G ` X ) ) ) >. ) )
27 df-ov 
 |-  ( ( 1st ` ( F ` ( G ` X ) ) ) (,) ( 2nd ` ( F ` ( G ` X ) ) ) ) = ( (,) ` <. ( 1st ` ( F ` ( G ` X ) ) ) , ( 2nd ` ( F ` ( G ` X ) ) ) >. )
28 26 27 eqtr4di 
 |-  ( ( ph /\ X e. U ) -> ( (,) ` ( F ` ( G ` X ) ) ) = ( ( 1st ` ( F ` ( G ` X ) ) ) (,) ( 2nd ` ( F ` ( G ` X ) ) ) ) )
29 15 21 28 3eqtr3d 
 |-  ( ( ph /\ X e. U ) -> X = ( ( 1st ` ( F ` ( G ` X ) ) ) (,) ( 2nd ` ( F ` ( G ` X ) ) ) ) )
30 29 eleq2d 
 |-  ( ( ph /\ X e. U ) -> ( P e. X <-> P e. ( ( 1st ` ( F ` ( G ` X ) ) ) (,) ( 2nd ` ( F ` ( G ` X ) ) ) ) ) )
31 xp1st 
 |-  ( ( F ` ( G ` X ) ) e. ( RR X. RR ) -> ( 1st ` ( F ` ( G ` X ) ) ) e. RR )
32 23 31 syl 
 |-  ( ( ph /\ X e. U ) -> ( 1st ` ( F ` ( G ` X ) ) ) e. RR )
33 xp2nd 
 |-  ( ( F ` ( G ` X ) ) e. ( RR X. RR ) -> ( 2nd ` ( F ` ( G ` X ) ) ) e. RR )
34 23 33 syl 
 |-  ( ( ph /\ X e. U ) -> ( 2nd ` ( F ` ( G ` X ) ) ) e. RR )
35 rexr 
 |-  ( ( 1st ` ( F ` ( G ` X ) ) ) e. RR -> ( 1st ` ( F ` ( G ` X ) ) ) e. RR* )
36 rexr 
 |-  ( ( 2nd ` ( F ` ( G ` X ) ) ) e. RR -> ( 2nd ` ( F ` ( G ` X ) ) ) e. RR* )
37 elioo2 
 |-  ( ( ( 1st ` ( F ` ( G ` X ) ) ) e. RR* /\ ( 2nd ` ( F ` ( G ` X ) ) ) e. RR* ) -> ( P e. ( ( 1st ` ( F ` ( G ` X ) ) ) (,) ( 2nd ` ( F ` ( G ` X ) ) ) ) <-> ( P e. RR /\ ( 1st ` ( F ` ( G ` X ) ) ) < P /\ P < ( 2nd ` ( F ` ( G ` X ) ) ) ) ) )
38 35 36 37 syl2an 
 |-  ( ( ( 1st ` ( F ` ( G ` X ) ) ) e. RR /\ ( 2nd ` ( F ` ( G ` X ) ) ) e. RR ) -> ( P e. ( ( 1st ` ( F ` ( G ` X ) ) ) (,) ( 2nd ` ( F ` ( G ` X ) ) ) ) <-> ( P e. RR /\ ( 1st ` ( F ` ( G ` X ) ) ) < P /\ P < ( 2nd ` ( F ` ( G ` X ) ) ) ) ) )
39 32 34 38 syl2anc 
 |-  ( ( ph /\ X e. U ) -> ( P e. ( ( 1st ` ( F ` ( G ` X ) ) ) (,) ( 2nd ` ( F ` ( G ` X ) ) ) ) <-> ( P e. RR /\ ( 1st ` ( F ` ( G ` X ) ) ) < P /\ P < ( 2nd ` ( F ` ( G ` X ) ) ) ) ) )
40 30 39 bitrd 
 |-  ( ( ph /\ X e. U ) -> ( P e. X <-> ( P e. RR /\ ( 1st ` ( F ` ( G ` X ) ) ) < P /\ P < ( 2nd ` ( F ` ( G ` X ) ) ) ) ) )