MPE Home Metamath Proof Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >  ovolfcl Structured version   Unicode version

Theorem ovolfcl 20919
Description: Closure for the interval endpoint function. (Contributed by Mario Carneiro, 16-Mar-2014.)
Assertion
Ref Expression
ovolfcl  |-  ( ( F : NN --> (  <_  i^i  ( RR  X.  RR ) )  /\  N  e.  NN )  ->  (
( 1st `  ( F `  N )
)  e.  RR  /\  ( 2nd `  ( F `
 N ) )  e.  RR  /\  ( 1st `  ( F `  N ) )  <_ 
( 2nd `  ( F `  N )
) ) )

Proof of Theorem ovolfcl
StepHypRef Expression
1 inss2 3564 . . . . 5  |-  (  <_  i^i  ( RR  X.  RR ) )  C_  ( RR  X.  RR )
2 ffvelrn 5834 . . . . 5  |-  ( ( F : NN --> (  <_  i^i  ( RR  X.  RR ) )  /\  N  e.  NN )  ->  ( F `  N )  e.  (  <_  i^i  ( RR  X.  RR ) ) )
31, 2sseldi 3347 . . . 4  |-  ( ( F : NN --> (  <_  i^i  ( RR  X.  RR ) )  /\  N  e.  NN )  ->  ( F `  N )  e.  ( RR  X.  RR ) )
4 1st2nd2 6608 . . . 4  |-  ( ( F `  N )  e.  ( RR  X.  RR )  ->  ( F `
 N )  = 
<. ( 1st `  ( F `  N )
) ,  ( 2nd `  ( F `  N
) ) >. )
53, 4syl 16 . . 3  |-  ( ( F : NN --> (  <_  i^i  ( RR  X.  RR ) )  /\  N  e.  NN )  ->  ( F `  N )  =  <. ( 1st `  ( F `  N )
) ,  ( 2nd `  ( F `  N
) ) >. )
65, 2eqeltrrd 2512 . 2  |-  ( ( F : NN --> (  <_  i^i  ( RR  X.  RR ) )  /\  N  e.  NN )  ->  <. ( 1st `  ( F `  N ) ) ,  ( 2nd `  ( F `  N )
) >.  e.  (  <_  i^i  ( RR  X.  RR ) ) )
7 ancom 450 . . 3  |-  ( ( ( 1st `  ( F `  N )
)  <_  ( 2nd `  ( F `  N
) )  /\  (
( 1st `  ( F `  N )
)  e.  RR  /\  ( 2nd `  ( F `
 N ) )  e.  RR ) )  <-> 
( ( ( 1st `  ( F `  N
) )  e.  RR  /\  ( 2nd `  ( F `  N )
)  e.  RR )  /\  ( 1st `  ( F `  N )
)  <_  ( 2nd `  ( F `  N
) ) ) )
8 elin 3532 . . . 4  |-  ( <.
( 1st `  ( F `  N )
) ,  ( 2nd `  ( F `  N
) ) >.  e.  (  <_  i^i  ( RR  X.  RR ) )  <->  ( <. ( 1st `  ( F `
 N ) ) ,  ( 2nd `  ( F `  N )
) >.  e.  <_  /\  <. ( 1st `  ( F `
 N ) ) ,  ( 2nd `  ( F `  N )
) >.  e.  ( RR 
X.  RR ) ) )
9 df-br 4286 . . . . . 6  |-  ( ( 1st `  ( F `
 N ) )  <_  ( 2nd `  ( F `  N )
)  <->  <. ( 1st `  ( F `  N )
) ,  ( 2nd `  ( F `  N
) ) >.  e.  <_  )
109bicomi 202 . . . . 5  |-  ( <.
( 1st `  ( F `  N )
) ,  ( 2nd `  ( F `  N
) ) >.  e.  <_  <->  ( 1st `  ( F `  N ) )  <_ 
( 2nd `  ( F `  N )
) )
11 opelxp 4861 . . . . 5  |-  ( <.
( 1st `  ( F `  N )
) ,  ( 2nd `  ( F `  N
) ) >.  e.  ( RR  X.  RR )  <-> 
( ( 1st `  ( F `  N )
)  e.  RR  /\  ( 2nd `  ( F `
 N ) )  e.  RR ) )
1210, 11anbi12i 697 . . . 4  |-  ( (
<. ( 1st `  ( F `  N )
) ,  ( 2nd `  ( F `  N
) ) >.  e.  <_  /\ 
<. ( 1st `  ( F `  N )
) ,  ( 2nd `  ( F `  N
) ) >.  e.  ( RR  X.  RR ) )  <->  ( ( 1st `  ( F `  N
) )  <_  ( 2nd `  ( F `  N ) )  /\  ( ( 1st `  ( F `  N )
)  e.  RR  /\  ( 2nd `  ( F `
 N ) )  e.  RR ) ) )
138, 12bitri 249 . . 3  |-  ( <.
( 1st `  ( F `  N )
) ,  ( 2nd `  ( F `  N
) ) >.  e.  (  <_  i^i  ( RR  X.  RR ) )  <->  ( ( 1st `  ( F `  N ) )  <_ 
( 2nd `  ( F `  N )
)  /\  ( ( 1st `  ( F `  N ) )  e.  RR  /\  ( 2nd `  ( F `  N
) )  e.  RR ) ) )
14 df-3an 967 . . 3  |-  ( ( ( 1st `  ( F `  N )
)  e.  RR  /\  ( 2nd `  ( F `
 N ) )  e.  RR  /\  ( 1st `  ( F `  N ) )  <_ 
( 2nd `  ( F `  N )
) )  <->  ( (
( 1st `  ( F `  N )
)  e.  RR  /\  ( 2nd `  ( F `
 N ) )  e.  RR )  /\  ( 1st `  ( F `
 N ) )  <_  ( 2nd `  ( F `  N )
) ) )
157, 13, 143bitr4i 277 . 2  |-  ( <.
( 1st `  ( F `  N )
) ,  ( 2nd `  ( F `  N
) ) >.  e.  (  <_  i^i  ( RR  X.  RR ) )  <->  ( ( 1st `  ( F `  N ) )  e.  RR  /\  ( 2nd `  ( F `  N
) )  e.  RR  /\  ( 1st `  ( F `  N )
)  <_  ( 2nd `  ( F `  N
) ) ) )
166, 15sylib 196 1  |-  ( ( F : NN --> (  <_  i^i  ( RR  X.  RR ) )  /\  N  e.  NN )  ->  (
( 1st `  ( F `  N )
)  e.  RR  /\  ( 2nd `  ( F `
 N ) )  e.  RR  /\  ( 1st `  ( F `  N ) )  <_ 
( 2nd `  ( F `  N )
) ) )
Colors of variables: wff setvar class
Syntax hints:    -> wi 4    /\ wa 369    /\ w3a 965    = wceq 1369    e. wcel 1756    i^i cin 3320   <.cop 3876   class class class wbr 4285    X. cxp 4830   -->wf 5407   ` cfv 5411   1stc1st 6570   2ndc2nd 6571   RRcr 9273    <_ cle 9411   NNcn 10314
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1591  ax-4 1602  ax-5 1670  ax-6 1708  ax-7 1728  ax-8 1758  ax-9 1760  ax-10 1775  ax-11 1780  ax-12 1792  ax-13 1943  ax-ext 2418  ax-sep 4406  ax-nul 4414  ax-pow 4463  ax-pr 4524  ax-un 6367
This theorem depends on definitions:  df-bi 185  df-or 370  df-an 371  df-3an 967  df-tru 1372  df-ex 1587  df-nf 1590  df-sb 1701  df-eu 2256  df-mo 2257  df-clab 2424  df-cleq 2430  df-clel 2433  df-nfc 2562  df-ne 2602  df-ral 2714  df-rex 2715  df-rab 2718  df-v 2968  df-sbc 3180  df-dif 3324  df-un 3326  df-in 3328  df-ss 3335  df-nul 3631  df-if 3785  df-sn 3871  df-pr 3873  df-op 3877  df-uni 4085  df-br 4286  df-opab 4344  df-mpt 4345  df-id 4628  df-xp 4838  df-rel 4839  df-cnv 4840  df-co 4841  df-dm 4842  df-rn 4843  df-iota 5374  df-fun 5413  df-fn 5414  df-f 5415  df-fv 5419  df-1st 6572  df-2nd 6573
This theorem is referenced by:  ovolfioo  20920  ovolficc  20921  ovolfsval  20923  ovolfsf  20924  ovollb2lem  20940  ovolshftlem1  20961  ovolscalem1  20965  ioombl1lem1  21008  ioombl1lem3  21010  ioombl1lem4  21011  ovolfs2  21020  uniiccdif  21027  uniioovol  21028  uniioombllem2a  21031  uniioombllem2  21032  uniioombllem3a  21033  uniioombllem3  21034  uniioombllem4  21035  uniioombllem6  21037
  Copyright terms: Public domain W3C validator