ILE Home Intuitionistic Logic Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  ILE Home  >  Th. List  >  prarloclemup Unicode version
Theorem prarloclemup 7690
Description: Contracting the upper side of an interval which straddles a Dedekind cut. Lemma for prarloc 7698. (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 534 . . 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 529 . . 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 528 . . 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 2579 . . 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 1269 . 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 364 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 104   /\ w3a 1002   e. wcel 2200   E.wrex 2509   <.cop 3669   suc csuc 4456   omcom 4682  (class class class)co 6007   1oc1o 6561   2oc2o 6562   +o coa 6565   [cec 6686   ~Q ceq 7474   Q.cnq 7475   +Q cplq 7477   .Q cmq 7478   ~Q0 ceq0 7481   +Q0 cplq0 7484   ·Q0 cmq0 7485   P.cnp 7486
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia1 106  ax-ia2 107  ax-ia3 108  ax-gen 1495  ax-ie1 1539  ax-ie2 1540  ax-4 1556
This theorem depends on definitions:  df-bi 117  df-rex 2514
This theorem is referenced by:  prarloclem3step  7691
  Copyright terms: Public domain W3C validator