ILE Home Intuitionistic Logic Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  ILE Home  >  Th. List  >  prarloclemup Unicode version

Theorem prarloclemup 7317
Description: Contracting the upper side of an interval which straddles a Dedekind cut. Lemma for prarloc 7325. (Contributed by Jim Kingdon, 10-Nov-2019.)
Assertion
Ref Expression
prarloclemup  |-  ( ( ( X  e.  om  /\  ( <. L ,  U >.  e.  P.  /\  A  e.  L  /\  P  e. 
Q. ) )  /\  y  e.  om )  ->  ( ( A  +Q  ( [ <. ( ( y  +o  2o )  +o  X ) ,  1o >. ]  ~Q  .Q  P
) )  e.  U  ->  ( ( ( A +Q0  ( [ <. y ,  1o >. ] ~Q0 ·Q0  P )
)  e.  L  /\  ( A  +Q  ( [ <. ( ( y  +o  2o )  +o 
suc  X ) ,  1o >. ]  ~Q  .Q  P ) )  e.  U )  ->  E. y  e.  om  ( ( A +Q0  ( [ <. y ,  1o >. ] ~Q0 ·Q0  P )
)  e.  L  /\  ( A  +Q  ( [ <. ( ( y  +o  2o )  +o  X ) ,  1o >. ]  ~Q  .Q  P
) )  e.  U
) ) ) )

Proof of Theorem prarloclemup
StepHypRef Expression
1 simpllr 523 . . 3  |-  ( ( ( ( ( X  e.  om  /\  ( <. L ,  U >.  e. 
P.  /\  A  e.  L  /\  P  e.  Q. ) )  /\  y  e.  om )  /\  ( A  +Q  ( [ <. ( ( y  +o  2o )  +o  X ) ,  1o >. ]  ~Q  .Q  P ) )  e.  U )  /\  (
( A +Q0  ( [ <. y ,  1o >. ] ~Q0 ·Q0  P ) )  e.  L  /\  ( A  +Q  ( [ <. ( ( y  +o  2o )  +o 
suc  X ) ,  1o >. ]  ~Q  .Q  P ) )  e.  U ) )  -> 
y  e.  om )
2 simprl 520 . . 3  |-  ( ( ( ( ( X  e.  om  /\  ( <. L ,  U >.  e. 
P.  /\  A  e.  L  /\  P  e.  Q. ) )  /\  y  e.  om )  /\  ( A  +Q  ( [ <. ( ( y  +o  2o )  +o  X ) ,  1o >. ]  ~Q  .Q  P ) )  e.  U )  /\  (
( A +Q0  ( [ <. y ,  1o >. ] ~Q0 ·Q0  P ) )  e.  L  /\  ( A  +Q  ( [ <. ( ( y  +o  2o )  +o 
suc  X ) ,  1o >. ]  ~Q  .Q  P ) )  e.  U ) )  -> 
( A +Q0  ( [ <. y ,  1o >. ] ~Q0 ·Q0  P ) )  e.  L )
3 simplr 519 . . 3  |-  ( ( ( ( ( X  e.  om  /\  ( <. L ,  U >.  e. 
P.  /\  A  e.  L  /\  P  e.  Q. ) )  /\  y  e.  om )  /\  ( A  +Q  ( [ <. ( ( y  +o  2o )  +o  X ) ,  1o >. ]  ~Q  .Q  P ) )  e.  U )  /\  (
( A +Q0  ( [ <. y ,  1o >. ] ~Q0 ·Q0  P ) )  e.  L  /\  ( A  +Q  ( [ <. ( ( y  +o  2o )  +o 
suc  X ) ,  1o >. ]  ~Q  .Q  P ) )  e.  U ) )  -> 
( A  +Q  ( [ <. ( ( y  +o  2o )  +o  X ) ,  1o >. ]  ~Q  .Q  P
) )  e.  U
)
4 rspe 2481 . . 3  |-  ( ( y  e.  om  /\  ( ( A +Q0  ( [ <. y ,  1o >. ] ~Q0 ·Q0  P ) )  e.  L  /\  ( A  +Q  ( [ <. ( ( y  +o  2o )  +o  X ) ,  1o >. ]  ~Q  .Q  P
) )  e.  U
) )  ->  E. y  e.  om  ( ( A +Q0  ( [ <. y ,  1o >. ] ~Q0 ·Q0  P )
)  e.  L  /\  ( A  +Q  ( [ <. ( ( y  +o  2o )  +o  X ) ,  1o >. ]  ~Q  .Q  P
) )  e.  U
) )
51, 2, 3, 4syl12anc 1214 . 2  |-  ( ( ( ( ( X  e.  om  /\  ( <. L ,  U >.  e. 
P.  /\  A  e.  L  /\  P  e.  Q. ) )  /\  y  e.  om )  /\  ( A  +Q  ( [ <. ( ( y  +o  2o )  +o  X ) ,  1o >. ]  ~Q  .Q  P ) )  e.  U )  /\  (
( A +Q0  ( [ <. y ,  1o >. ] ~Q0 ·Q0  P ) )  e.  L  /\  ( A  +Q  ( [ <. ( ( y  +o  2o )  +o 
suc  X ) ,  1o >. ]  ~Q  .Q  P ) )  e.  U ) )  ->  E. y  e.  om  ( ( A +Q0  ( [ <. y ,  1o >. ] ~Q0 ·Q0  P ) )  e.  L  /\  ( A  +Q  ( [ <. ( ( y  +o  2o )  +o  X ) ,  1o >. ]  ~Q  .Q  P
) )  e.  U
) )
65exp31 361 1  |-  ( ( ( X  e.  om  /\  ( <. L ,  U >.  e.  P.  /\  A  e.  L  /\  P  e. 
Q. ) )  /\  y  e.  om )  ->  ( ( A  +Q  ( [ <. ( ( y  +o  2o )  +o  X ) ,  1o >. ]  ~Q  .Q  P
) )  e.  U  ->  ( ( ( A +Q0  ( [ <. y ,  1o >. ] ~Q0 ·Q0  P )
)  e.  L  /\  ( A  +Q  ( [ <. ( ( y  +o  2o )  +o 
suc  X ) ,  1o >. ]  ~Q  .Q  P ) )  e.  U )  ->  E. y  e.  om  ( ( A +Q0  ( [ <. y ,  1o >. ] ~Q0 ·Q0  P )
)  e.  L  /\  ( A  +Q  ( [ <. ( ( y  +o  2o )  +o  X ) ,  1o >. ]  ~Q  .Q  P
) )  e.  U
) ) ) )
Colors of variables: wff set class
Syntax hints:    -> wi 4    /\ wa 103    /\ w3a 962    e. wcel 1480   E.wrex 2417   <.cop 3530   suc csuc 4287   omcom 4504  (class class class)co 5774   1oc1o 6306   2oc2o 6307    +o coa 6310   [cec 6427    ~Q ceq 7101   Q.cnq 7102    +Q cplq 7104    .Q cmq 7105   ~Q0 ceq0 7108   +Q0 cplq0 7111   ·Q0 cmq0 7112   P.cnp 7113
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia1 105  ax-ia2 106  ax-ia3 107  ax-gen 1425  ax-ie1 1469  ax-ie2 1470  ax-4 1487
This theorem depends on definitions:  df-bi 116  df-rex 2422
This theorem is referenced by:  prarloclem3step  7318
  Copyright terms: Public domain W3C validator