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

Theorem prarloclemup 7496
Description: Contracting the upper side of an interval which straddles a Dedekind cut. Lemma for prarloc 7504. (Contributed by Jim Kingdon, 10-Nov-2019.)
Assertion
Ref Expression
prarloclemup (((๐‘‹ โˆˆ ฯ‰ โˆง (โŸจ๐ฟ, ๐‘ˆโŸฉ โˆˆ P โˆง ๐ด โˆˆ ๐ฟ โˆง ๐‘ƒ โˆˆ Q)) โˆง ๐‘ฆ โˆˆ ฯ‰) โ†’ ((๐ด +Q ([โŸจ((๐‘ฆ +o 2o) +o ๐‘‹), 1oโŸฉ] ~Q ยทQ ๐‘ƒ)) โˆˆ ๐‘ˆ โ†’ (((๐ด +Q0 ([โŸจ๐‘ฆ, 1oโŸฉ] ~Q0 ยทQ0 ๐‘ƒ)) โˆˆ ๐ฟ โˆง (๐ด +Q ([โŸจ((๐‘ฆ +o 2o) +o suc ๐‘‹), 1oโŸฉ] ~Q ยทQ ๐‘ƒ)) โˆˆ ๐‘ˆ) โ†’ โˆƒ๐‘ฆ โˆˆ ฯ‰ ((๐ด +Q0 ([โŸจ๐‘ฆ, 1oโŸฉ] ~Q0 ยทQ0 ๐‘ƒ)) โˆˆ ๐ฟ โˆง (๐ด +Q ([โŸจ((๐‘ฆ +o 2o) +o ๐‘‹), 1oโŸฉ] ~Q ยทQ ๐‘ƒ)) โˆˆ ๐‘ˆ))))

Proof of Theorem prarloclemup
StepHypRef Expression
1 simpllr 534 . . 3 (((((๐‘‹ โˆˆ ฯ‰ โˆง (โŸจ๐ฟ, ๐‘ˆโŸฉ โˆˆ P โˆง ๐ด โˆˆ ๐ฟ โˆง ๐‘ƒ โˆˆ Q)) โˆง ๐‘ฆ โˆˆ ฯ‰) โˆง (๐ด +Q ([โŸจ((๐‘ฆ +o 2o) +o ๐‘‹), 1oโŸฉ] ~Q ยทQ ๐‘ƒ)) โˆˆ ๐‘ˆ) โˆง ((๐ด +Q0 ([โŸจ๐‘ฆ, 1oโŸฉ] ~Q0 ยทQ0 ๐‘ƒ)) โˆˆ ๐ฟ โˆง (๐ด +Q ([โŸจ((๐‘ฆ +o 2o) +o suc ๐‘‹), 1oโŸฉ] ~Q ยทQ ๐‘ƒ)) โˆˆ ๐‘ˆ)) โ†’ ๐‘ฆ โˆˆ ฯ‰)
2 simprl 529 . . 3 (((((๐‘‹ โˆˆ ฯ‰ โˆง (โŸจ๐ฟ, ๐‘ˆโŸฉ โˆˆ P โˆง ๐ด โˆˆ ๐ฟ โˆง ๐‘ƒ โˆˆ Q)) โˆง ๐‘ฆ โˆˆ ฯ‰) โˆง (๐ด +Q ([โŸจ((๐‘ฆ +o 2o) +o ๐‘‹), 1oโŸฉ] ~Q ยทQ ๐‘ƒ)) โˆˆ ๐‘ˆ) โˆง ((๐ด +Q0 ([โŸจ๐‘ฆ, 1oโŸฉ] ~Q0 ยทQ0 ๐‘ƒ)) โˆˆ ๐ฟ โˆง (๐ด +Q ([โŸจ((๐‘ฆ +o 2o) +o suc ๐‘‹), 1oโŸฉ] ~Q ยทQ ๐‘ƒ)) โˆˆ ๐‘ˆ)) โ†’ (๐ด +Q0 ([โŸจ๐‘ฆ, 1oโŸฉ] ~Q0 ยทQ0 ๐‘ƒ)) โˆˆ ๐ฟ)
3 simplr 528 . . 3 (((((๐‘‹ โˆˆ ฯ‰ โˆง (โŸจ๐ฟ, ๐‘ˆโŸฉ โˆˆ P โˆง ๐ด โˆˆ ๐ฟ โˆง ๐‘ƒ โˆˆ Q)) โˆง ๐‘ฆ โˆˆ ฯ‰) โˆง (๐ด +Q ([โŸจ((๐‘ฆ +o 2o) +o ๐‘‹), 1oโŸฉ] ~Q ยทQ ๐‘ƒ)) โˆˆ ๐‘ˆ) โˆง ((๐ด +Q0 ([โŸจ๐‘ฆ, 1oโŸฉ] ~Q0 ยทQ0 ๐‘ƒ)) โˆˆ ๐ฟ โˆง (๐ด +Q ([โŸจ((๐‘ฆ +o 2o) +o suc ๐‘‹), 1oโŸฉ] ~Q ยทQ ๐‘ƒ)) โˆˆ ๐‘ˆ)) โ†’ (๐ด +Q ([โŸจ((๐‘ฆ +o 2o) +o ๐‘‹), 1oโŸฉ] ~Q ยทQ ๐‘ƒ)) โˆˆ ๐‘ˆ)
4 rspe 2526 . . 3 ((๐‘ฆ โˆˆ ฯ‰ โˆง ((๐ด +Q0 ([โŸจ๐‘ฆ, 1oโŸฉ] ~Q0 ยทQ0 ๐‘ƒ)) โˆˆ ๐ฟ โˆง (๐ด +Q ([โŸจ((๐‘ฆ +o 2o) +o ๐‘‹), 1oโŸฉ] ~Q ยทQ ๐‘ƒ)) โˆˆ ๐‘ˆ)) โ†’ โˆƒ๐‘ฆ โˆˆ ฯ‰ ((๐ด +Q0 ([โŸจ๐‘ฆ, 1oโŸฉ] ~Q0 ยทQ0 ๐‘ƒ)) โˆˆ ๐ฟ โˆง (๐ด +Q ([โŸจ((๐‘ฆ +o 2o) +o ๐‘‹), 1oโŸฉ] ~Q ยทQ ๐‘ƒ)) โˆˆ ๐‘ˆ))
51, 2, 3, 4syl12anc 1236 . 2 (((((๐‘‹ โˆˆ ฯ‰ โˆง (โŸจ๐ฟ, ๐‘ˆโŸฉ โˆˆ P โˆง ๐ด โˆˆ ๐ฟ โˆง ๐‘ƒ โˆˆ Q)) โˆง ๐‘ฆ โˆˆ ฯ‰) โˆง (๐ด +Q ([โŸจ((๐‘ฆ +o 2o) +o ๐‘‹), 1oโŸฉ] ~Q ยทQ ๐‘ƒ)) โˆˆ ๐‘ˆ) โˆง ((๐ด +Q0 ([โŸจ๐‘ฆ, 1oโŸฉ] ~Q0 ยทQ0 ๐‘ƒ)) โˆˆ ๐ฟ โˆง (๐ด +Q ([โŸจ((๐‘ฆ +o 2o) +o suc ๐‘‹), 1oโŸฉ] ~Q ยทQ ๐‘ƒ)) โˆˆ ๐‘ˆ)) โ†’ โˆƒ๐‘ฆ โˆˆ ฯ‰ ((๐ด +Q0 ([โŸจ๐‘ฆ, 1oโŸฉ] ~Q0 ยทQ0 ๐‘ƒ)) โˆˆ ๐ฟ โˆง (๐ด +Q ([โŸจ((๐‘ฆ +o 2o) +o ๐‘‹), 1oโŸฉ] ~Q ยทQ ๐‘ƒ)) โˆˆ ๐‘ˆ))
65exp31 364 1 (((๐‘‹ โˆˆ ฯ‰ โˆง (โŸจ๐ฟ, ๐‘ˆโŸฉ โˆˆ P โˆง ๐ด โˆˆ ๐ฟ โˆง ๐‘ƒ โˆˆ Q)) โˆง ๐‘ฆ โˆˆ ฯ‰) โ†’ ((๐ด +Q ([โŸจ((๐‘ฆ +o 2o) +o ๐‘‹), 1oโŸฉ] ~Q ยทQ ๐‘ƒ)) โˆˆ ๐‘ˆ โ†’ (((๐ด +Q0 ([โŸจ๐‘ฆ, 1oโŸฉ] ~Q0 ยทQ0 ๐‘ƒ)) โˆˆ ๐ฟ โˆง (๐ด +Q ([โŸจ((๐‘ฆ +o 2o) +o suc ๐‘‹), 1oโŸฉ] ~Q ยทQ ๐‘ƒ)) โˆˆ ๐‘ˆ) โ†’ โˆƒ๐‘ฆ โˆˆ ฯ‰ ((๐ด +Q0 ([โŸจ๐‘ฆ, 1oโŸฉ] ~Q0 ยทQ0 ๐‘ƒ)) โˆˆ ๐ฟ โˆง (๐ด +Q ([โŸจ((๐‘ฆ +o 2o) +o ๐‘‹), 1oโŸฉ] ~Q ยทQ ๐‘ƒ)) โˆˆ ๐‘ˆ))))
Colors of variables: wff set class
Syntax hints:   โ†’ wi 4   โˆง wa 104   โˆง w3a 978   โˆˆ wcel 2148  โˆƒwrex 2456  โŸจcop 3597  suc csuc 4367  ฯ‰com 4591  (class class class)co 5877  1oc1o 6412  2oc2o 6413   +o coa 6416  [cec 6535   ~Q ceq 7280  Qcnq 7281   +Q cplq 7283   ยทQ cmq 7284   ~Q0 ceq0 7287   +Q0 cplq0 7290   ยทQ0 cmq0 7291  Pcnp 7292
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 1449  ax-ie1 1493  ax-ie2 1494  ax-4 1510
This theorem depends on definitions:  df-bi 117  df-rex 2461
This theorem is referenced by:  prarloclem3step  7497
  Copyright terms: Public domain W3C validator